OC checker

build.gradle.kts

@@ -29,7 +29,7 @@ buildscript {
 
 allprojects {
     group = "hu.bme.mit.theta"
-    version = "6.6.2"
+    version = "6.7.0"
 
     apply(from = rootDir.resolve("gradle/shared-with-buildSrc/mirrors.gradle.kts"))
 }

subprojects/cfa/cfa-analysis/src/main/kotlin/hu/bme/mit/theta/cfa/analysis/CfaToMonolithicExpr.kt

@@ -13,76 +13,80 @@
  *  See the License for the specific language governing permissions and
  *  limitations under the License.
  */
+package hu.bme.mit.theta.cfa.analysis
 
-package hu.bme.mit.theta.cfa.analysis;
-
-import com.google.common.base.Preconditions;
+import com.google.common.base.Preconditions
 import hu.bme.mit.theta.analysis.algorithm.bounded.MonolithicExpr
 import hu.bme.mit.theta.analysis.expl.ExplState
-import hu.bme.mit.theta.analysis.ptr.PtrState
-import hu.bme.mit.theta.cfa.CFA;
-import hu.bme.mit.theta.core.decl.Decls;
-import hu.bme.mit.theta.core.model.ImmutableValuation
+import hu.bme.mit.theta.cfa.CFA
+import hu.bme.mit.theta.core.decl.Decls
 import hu.bme.mit.theta.core.model.Valuation
 import hu.bme.mit.theta.core.stmt.*
 import hu.bme.mit.theta.core.type.booltype.BoolExprs.And
 import hu.bme.mit.theta.core.type.inttype.IntExprs.*
 import hu.bme.mit.theta.core.type.inttype.IntLitExpr
-import hu.bme.mit.theta.core.utils.StmtUtils;
-import hu.bme.mit.theta.core.utils.indexings.VarIndexingFactory;
+import hu.bme.mit.theta.core.utils.StmtUtils
+import hu.bme.mit.theta.core.utils.indexings.VarIndexingFactory
 import java.util.*
 
 fun CFA.toMonolithicExpr(): MonolithicExpr {
-    Preconditions.checkArgument(this.errorLoc.isPresent);
+  Preconditions.checkArgument(this.errorLoc.isPresent)
 
-    val map = mutableMapOf<CFA.Loc, Int>()
-    for ((i, x) in this.locs.withIndex()) {
-        map[x] = i;
-    }
-    val locVar = Decls.Var("__loc__", Int())
-    val tranList = this.edges.map { e ->
-        SequenceStmt.of(listOf(
+  val map = mutableMapOf<CFA.Loc, Int>()
+  for ((i, x) in this.locs.withIndex()) {
+    map[x] = i
+  }
+  val locVar = Decls.Var("__loc__", Int())
+  val tranList =
+    this.edges
+      .map { e ->
+        SequenceStmt.of(
+          listOf(
             AssumeStmt.of(Eq(locVar.ref, Int(map[e.source]!!))),
             e.stmt,
-            AssignStmt.of(locVar, Int(map[e.target]!!))
-        ))
-    }.toList()
-    val trans = NonDetStmt.of(tranList);
-    val transUnfold = StmtUtils.toExpr(trans, VarIndexingFactory.indexing(0));
-    val transExpr = And(transUnfold.exprs)
-    val initExpr = Eq(locVar.ref, Int(map[this.initLoc]!!))
-    val propExpr = Neq(locVar.ref, Int(map[this.errorLoc.orElseThrow()]!!))
+            AssignStmt.of(locVar, Int(map[e.target]!!)),
+          )
+        )
+      }
+      .toList()
+  val trans = NonDetStmt.of(tranList)
+  val transUnfold = StmtUtils.toExpr(trans, VarIndexingFactory.indexing(0))
+  val transExpr = And(transUnfold.exprs)
+  val initExpr = Eq(locVar.ref, Int(map[this.initLoc]!!))
+  val propExpr = Neq(locVar.ref, Int(map[this.errorLoc.orElseThrow()]!!))
 
-    val offsetIndex = transUnfold.indexing
+  val offsetIndex = transUnfold.indexing
 
-    return MonolithicExpr(initExpr, transExpr, propExpr, offsetIndex)
+  return MonolithicExpr(initExpr, transExpr, propExpr, offsetIndex)
 }
 
 fun CFA.valToAction(val1: Valuation, val2: Valuation): CfaAction {
-    val val1Map = val1.toMap()
-    val val2Map = val2.toMap()
-    var i = 0
-    val map: MutableMap<CFA.Loc, Int> = mutableMapOf()
-    for (x in this.locs) {
-        map[x] = i++
+  val val1Map = val1.toMap()
+  val val2Map = val2.toMap()
+  var i = 0
+  val map: MutableMap<CFA.Loc, Int> = mutableMapOf()
+  for (x in this.locs) {
+    map[x] = i++
+  }
+  return CfaAction.create(
+    this.edges.first { edge ->
+      map[edge.source] ==
+        (val1Map[val1Map.keys.first { it.name == "__loc_" }] as IntLitExpr).value.toInt() &&
+        map[edge.target] ==
+          (val2Map[val2Map.keys.first { it.name == "__loc_" }] as IntLitExpr).value.toInt()
     }
-    return CfaAction.create(
-        this.edges.first { edge ->
-            map[edge.source] == (val1Map[val1Map.keys.first { it.name == "__loc_" }] as IntLitExpr).value.toInt() &&
-                map[edge.target] == (val2Map[val2Map.keys.first { it.name == "__loc_" }] as IntLitExpr).value.toInt()
-        })
+  )
 }
 
 fun CFA.valToState(val1: Valuation): CfaState<ExplState> {
-    val valMap = val1.toMap()
-    var i = 0
-    val map: MutableMap<Int, CFA.Loc> = mutableMapOf()
-    for (x in this.locs) {
-        map[i++] = x
-    }
-    return CfaState.of(
-        map[(valMap[valMap.keys.first { it.name == "__loc_" }] as IntLitExpr).value.toInt()],
-        ExplState.of(val1)
-    )
+  val valMap = val1.toMap()
+  var i = 0
+  val map: MutableMap<Int, CFA.Loc> = mutableMapOf()
+  for (x in this.locs) {
+    map[i++] = x
+  }
+  return CfaState.of(
+    map[(valMap[valMap.keys.first { it.name == "__loc_" }] as IntLitExpr).value.toInt()],
+    ExplState.of(val1),
+  )
 }
-

subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/bounded/BoundedCheckerBuilder.kt

@@ -13,7 +13,6 @@
  *  See the License for the specific language governing permissions and
  *  limitations under the License.
  */
-
 package hu.bme.mit.theta.analysis.algorithm.bounded
 
 import hu.bme.mit.theta.analysis.expr.ExprAction
@@ -25,49 +24,85 @@ import hu.bme.mit.theta.solver.Solver
 
 @JvmOverloads
 fun <S : ExprState, A : ExprAction> buildBMC(
-    monolithicExpr: MonolithicExpr,
-    bmcSolver: Solver,
-    valToState: (Valuation) -> S,
-    biValToAction: (Valuation, Valuation) -> A,
-    logger: Logger,
-    shouldGiveUp: (Int) -> Boolean = { false },
-    bmcEnabled: () -> Boolean = { true },
-    lfPathOnly: () -> Boolean = { true },
+  monolithicExpr: MonolithicExpr,
+  bmcSolver: Solver,
+  valToState: (Valuation) -> S,
+  biValToAction: (Valuation, Valuation) -> A,
+  logger: Logger,
+  shouldGiveUp: (Int) -> Boolean = { false },
+  bmcEnabled: () -> Boolean = { true },
+  lfPathOnly: () -> Boolean = { true },
 ): BoundedChecker<S, A> {
-    return BoundedChecker(monolithicExpr, shouldGiveUp, bmcSolver, bmcEnabled, lfPathOnly, null, { false }, null,
-        { false }, valToState, biValToAction, logger)
+  return BoundedChecker(
+    monolithicExpr,
+    shouldGiveUp,
+    bmcSolver,
+    bmcEnabled,
+    lfPathOnly,
+    null,
+    { false },
+    null,
+    { false },
+    valToState,
+    biValToAction,
+    logger,
+  )
 }
 
 @JvmOverloads
 fun <S : ExprState, A : ExprAction> buildKIND(
-    monolithicExpr: MonolithicExpr,
-    bmcSolver: Solver,
-    indSolver: Solver,
-    valToState: (Valuation) -> S,
-    biValToAction: (Valuation, Valuation) -> A,
-    logger: Logger,
-    shouldGiveUp: (Int) -> Boolean = { false },
-    bmcEnabled: () -> Boolean = { true },
-    lfPathOnly: () -> Boolean = { true },
-    kindEnabled: (Int) -> Boolean = { true },
+  monolithicExpr: MonolithicExpr,
+  bmcSolver: Solver,
+  indSolver: Solver,
+  valToState: (Valuation) -> S,
+  biValToAction: (Valuation, Valuation) -> A,
+  logger: Logger,
+  shouldGiveUp: (Int) -> Boolean = { false },
+  bmcEnabled: () -> Boolean = { true },
+  lfPathOnly: () -> Boolean = { true },
+  kindEnabled: (Int) -> Boolean = { true },
 ): BoundedChecker<S, A> {
-    return BoundedChecker(monolithicExpr, shouldGiveUp, bmcSolver, bmcEnabled, lfPathOnly, null, { false }, indSolver,
-        kindEnabled, valToState, biValToAction, logger)
+  return BoundedChecker(
+    monolithicExpr,
+    shouldGiveUp,
+    bmcSolver,
+    bmcEnabled,
+    lfPathOnly,
+    null,
+    { false },
+    indSolver,
+    kindEnabled,
+    valToState,
+    biValToAction,
+    logger,
+  )
 }
 
 @JvmOverloads
 fun <S : ExprState, A : ExprAction> buildIMC(
-    monolithicExpr: MonolithicExpr,
-    bmcSolver: Solver,
-    itpSolver: ItpSolver,
-    valToState: (Valuation) -> S,
-    biValToAction: (Valuation, Valuation) -> A,
-    logger: Logger,
-    shouldGiveUp: (Int) -> Boolean = { false },
-    bmcEnabled: () -> Boolean = { true },
-    lfPathOnly: () -> Boolean = { true },
-    imcEnabled: (Int) -> Boolean = { true },
+  monolithicExpr: MonolithicExpr,
+  bmcSolver: Solver,
+  itpSolver: ItpSolver,
+  valToState: (Valuation) -> S,
+  biValToAction: (Valuation, Valuation) -> A,
+  logger: Logger,
+  shouldGiveUp: (Int) -> Boolean = { false },
+  bmcEnabled: () -> Boolean = { true },
+  lfPathOnly: () -> Boolean = { true },
+  imcEnabled: (Int) -> Boolean = { true },
 ): BoundedChecker<S, A> {
-    return BoundedChecker(monolithicExpr, shouldGiveUp, bmcSolver, bmcEnabled, lfPathOnly, itpSolver, imcEnabled, null,
-        { false }, valToState, biValToAction, logger)
-}
+  return BoundedChecker(
+    monolithicExpr,
+    shouldGiveUp,
+    bmcSolver,
+    bmcEnabled,
+    lfPathOnly,
+    itpSolver,
+    imcEnabled,
+    null,
+    { false },
+    valToState,
+    biValToAction,
+    logger,
+  )
+}

subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/chc/HornChecker.kt

@@ -13,7 +13,6 @@
  *  See the License for the specific language governing permissions and
  *  limitations under the License.
  */
-
 package hu.bme.mit.theta.analysis.algorithm.chc
 
 import hu.bme.mit.theta.analysis.Cex
@@ -34,54 +33,58 @@ data class Invariant(val lookup: Map<Relation, Expr<BoolType>>) : Witness
 
 data class CexTree(val proofNode: ProofNode) : Cex {
 
-    override fun length(): Int = proofNode.depth()
+  override fun length(): Int = proofNode.depth()
 }
 
-/**
- * A checker for CHC-based verification.
- */
+/** A checker for CHC-based verification. */
 class HornChecker(
-    private val relations: List<Relation>,
-    private val hornSolverFactory: SolverFactory,
-    private val logger: Logger,
+  private val relations: List<Relation>,
+  private val hornSolverFactory: SolverFactory,
+  private val logger: Logger,
 ) : SafetyChecker<Invariant, CexTree, UnitPrec> {
 
-    override fun check(prec: UnitPrec?): SafetyResult<Invariant, CexTree> {
-        val solver = hornSolverFactory.createHornSolver()
-        logger.write(Logger.Level.MAINSTEP, "Starting encoding\n")
-        solver.add(relations)
-        logger.write(Logger.Level.DETAIL, "Relations:\n\t${
+  override fun check(prec: UnitPrec?): SafetyResult<Invariant, CexTree> {
+    val solver = hornSolverFactory.createHornSolver()
+    logger.write(Logger.Level.MAINSTEP, "Starting encoding\n")
+    solver.add(relations)
+    logger.write(
+      Logger.Level.DETAIL,
+      "Relations:\n\t${
             relations.joinToString("\n\t") {
                 it.constDecl.toString()
             }
-        }\n")
-        logger.write(Logger.Level.DETAIL, "Rules:\n\t${
+        }\n",
+    )
+    logger.write(
+      Logger.Level.DETAIL,
+      "Rules:\n\t${
             solver.assertions.joinToString("\n\t") {
                 it.toString().replace(Regex("[\r\n\t ]+"), " ")
             }
-        }\n")
-        logger.write(Logger.Level.MAINSTEP, "Added constraints to solver\n")
-        solver.check()
-        logger.write(Logger.Level.MAINSTEP, "Check() finished (result: ${solver.status})\n")
-        return when (solver.status) {
-            SolverStatus.SAT -> {
-                logger.write(Logger.Level.MAINSTEP, "Proof (model) found\n")
-                val model = solver.model.toMap()
-                SafetyResult.safe(
-                    Invariant(relations.associateWith { model[it.constDecl] as? Expr<BoolType> ?: True() }))
-            }
+        }\n",
+    )
+    logger.write(Logger.Level.MAINSTEP, "Added constraints to solver\n")
+    solver.check()
+    logger.write(Logger.Level.MAINSTEP, "Check() finished (result: ${solver.status})\n")
+    return when (solver.status) {
+      SolverStatus.SAT -> {
+        logger.write(Logger.Level.MAINSTEP, "Proof (model) found\n")
+        val model = solver.model.toMap()
+        SafetyResult.safe(
+          Invariant(relations.associateWith { model[it.constDecl] as? Expr<BoolType> ?: True() })
+        )
+      }
 
-            SolverStatus.UNSAT -> {
-                logger.write(Logger.Level.MAINSTEP, "Counterexample found\n")
-                val proof = solver.proof
-                SafetyResult.unsafe(CexTree(proof), Invariant(emptyMap()))
-            }
+      SolverStatus.UNSAT -> {
+        logger.write(Logger.Level.MAINSTEP, "Counterexample found\n")
+        val proof = solver.proof
+        SafetyResult.unsafe(CexTree(proof), Invariant(emptyMap()))
+      }
 
-            else -> {
-                logger.write(Logger.Level.MAINSTEP, "No solution found.\n")
-                SafetyResult.unknown()
-            }
-        }
+      else -> {
+        logger.write(Logger.Level.MAINSTEP, "No solution found.\n")
+        SafetyResult.unknown()
+      }
     }
-
-}
+  }
+}