Bounded analysis improvements, CLI bindings for CFA,STS,XSTS

build.gradle.kts

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

subprojects/cfa/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/config/CfaConfigBuilder.java

@@ -145,6 +145,7 @@ public CfaConfigBuilder pruneStrategy(final PruneStrategy pruneStrategy) {
 
     public enum Algorithm {
         CEGAR,
+        BMC,
         KINDUCTION,
         IMC
     }

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

@@ -0,0 +1,88 @@
+/*
+ *  Copyright 2024 Budapest University of Technology and Economics
+ *
+ *  Licensed under the Apache License, Version 2.0 (the "License");
+ *  you may not use this file except in compliance with the License.
+ *  You may obtain a copy of the License at
+ *
+ *      http://www.apache.org/licenses/LICENSE-2.0
+ *
+ *  Unless required by applicable law or agreed to in writing, software
+ *  distributed under the License is distributed on an "AS IS" BASIS,
+ *  WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ *  See the License for the specific language governing permissions and
+ *  limitations under the License.
+ */
+
+package hu.bme.mit.theta.cfa.analysis;
+
+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.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 java.util.*
+
+fun CFA.toMonolithicExpr(): MonolithicExpr {
+    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(
+            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()]!!))
+
+    val offsetIndex = transUnfold.indexing
+
+    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++
+    }
+    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)
+    )
+}
+

subprojects/cfa/cfa-cli/src/main/java/hu/bme/mit/theta/cfa/cli/CfaCli.java

@@ -22,12 +22,18 @@
 import hu.bme.mit.theta.analysis.Trace;
 import hu.bme.mit.theta.analysis.algorithm.SafetyResult;
 import hu.bme.mit.theta.analysis.algorithm.arg.ARG;
+import hu.bme.mit.theta.analysis.algorithm.bounded.BoundedChecker;
+import hu.bme.mit.theta.analysis.algorithm.bounded.BoundedCheckerBuilderKt;
+import hu.bme.mit.theta.analysis.algorithm.bounded.MonolithicExpr;
 import hu.bme.mit.theta.analysis.algorithm.cegar.CegarStatistics;
 import hu.bme.mit.theta.analysis.expl.ExplState;
+import hu.bme.mit.theta.analysis.expr.ExprAction;
+import hu.bme.mit.theta.analysis.expr.ExprState;
 import hu.bme.mit.theta.analysis.expr.refinement.PruneStrategy;
 import hu.bme.mit.theta.cfa.CFA;
 import hu.bme.mit.theta.cfa.analysis.CfaAction;
 import hu.bme.mit.theta.cfa.analysis.CfaState;
+import hu.bme.mit.theta.cfa.analysis.CfaToMonolithicExprKt;
 import hu.bme.mit.theta.cfa.analysis.CfaTraceConcretizer;
 import hu.bme.mit.theta.cfa.analysis.config.CfaConfig;
 import hu.bme.mit.theta.cfa.analysis.config.CfaConfigBuilder;
@@ -233,14 +239,17 @@ private void run() {
                 refinementSolverFactory = SolverManager.resolveSolverFactory(solver);
             }
 
-            final SafetyResult<? extends ARG<?, ?>, ? extends Trace<?, ?>> status;
+            final SafetyResult<?, ? extends Trace<?, ?>> status;
             if (algorithm == Algorithm.CEGAR) {
                 final CfaConfig<?, ?, ?> configuration = buildConfiguration(cfa, errLoc, abstractionSolverFactory, refinementSolverFactory);
                 status = check(configuration);
-                sw.stop();
+            } else if (algorithm == Algorithm.BMC || algorithm == Algorithm.KINDUCTION || algorithm == Algorithm.IMC) {
+                final BoundedChecker<?, ?> checker = buildBoundedChecker(cfa, abstractionSolverFactory);
+                status = checker.check(null);
             } else {
                 throw new UnsupportedOperationException("Algorithm " + algorithm + " not supported");
             }
+            sw.stop();
 
             printResult(status, sw.elapsed(TimeUnit.MILLISECONDS));
             if (status.isUnsafe() && cexfile != null) {
@@ -282,6 +291,39 @@ private CFA loadModel() throws Exception {
         }
     }
 
+    private BoundedChecker<?, ?> buildBoundedChecker(final CFA cfa, final SolverFactory abstractionSolverFactory) {
+        final MonolithicExpr monolithicExpr = CfaToMonolithicExprKt.toMonolithicExpr(cfa);
+        final BoundedChecker<?, ?> checker;
+        switch (algorithm) {
+            case BMC -> checker = BoundedCheckerBuilderKt.buildBMC(
+                    monolithicExpr,
+                    abstractionSolverFactory.createSolver(),
+                    val -> CfaToMonolithicExprKt.valToState(cfa, val),
+                    (val1, val2) -> CfaToMonolithicExprKt.valToAction(cfa, val1, val2),
+                    logger
+            );
+            case KINDUCTION -> checker = BoundedCheckerBuilderKt.buildKIND(
+                    monolithicExpr,
+                    abstractionSolverFactory.createSolver(),
+                    abstractionSolverFactory.createSolver(),
+                    val -> CfaToMonolithicExprKt.valToState(cfa, val),
+                    (val1, val2) -> CfaToMonolithicExprKt.valToAction(cfa, val1, val2),
+                    logger
+            );
+            case IMC -> checker = BoundedCheckerBuilderKt.buildIMC(
+                    monolithicExpr,
+                    abstractionSolverFactory.createSolver(),
+                    abstractionSolverFactory.createItpSolver(),
+                    val -> CfaToMonolithicExprKt.valToState(cfa, val),
+                    (val1, val2) -> CfaToMonolithicExprKt.valToAction(cfa, val1, val2),
+                    logger
+            );
+            default ->
+                    throw new UnsupportedOperationException("Algorithm " + algorithm + " not supported");
+        }
+        return checker;
+    }
+
     private SafetyResult<? extends ARG<?, ?>, ? extends Trace<?, ?>> check(CfaConfig<?, ?, ?> configuration) throws Exception {
         try {
             return configuration.check();
@@ -293,7 +335,7 @@ private CFA loadModel() throws Exception {
         }
     }
 
-    private void printResult(final SafetyResult<? extends ARG<?, ?>, ? extends Trace<?, ?>> status, final long totalTimeMs) {
+    private void printResult(final SafetyResult<?, ? extends Trace<?, ?>> status, final long totalTimeMs) {
         final CegarStatistics stats = (CegarStatistics)
                 status.getStats().orElse(new CegarStatistics(0, 0, 0, 0));
         if (benchmarkMode) {
@@ -303,9 +345,15 @@ private void printResult(final SafetyResult<? extends ARG<?, ?>, ? extends Trace
             writer.cell(stats.getAbstractorTimeMs());
             writer.cell(stats.getRefinerTimeMs());
             writer.cell(stats.getIterations());
-            writer.cell(status.getWitness().size());
-            writer.cell(status.getWitness().getDepth());
-            writer.cell(status.getWitness().getMeanBranchingFactor());
+            if (status.getWitness() instanceof ARG<?, ?> arg) {
+                writer.cell(arg.size());
+                writer.cell(arg.getDepth());
+                writer.cell(arg.getMeanBranchingFactor());
+            } else {
+                writer.cell("");
+                writer.cell("");
+                writer.cell("");
+            }
             if (status.isUnsafe()) {
                 writer.cell(status.asUnsafe().getCex().length() + "");
             } else {

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

@@ -62,21 +62,21 @@ class BoundedChecker<S : ExprState, A : ExprAction> @JvmOverloads constructor(
     private val monolithicExpr: MonolithicExpr,
     private val shouldGiveUp: (Int) -> Boolean = { false },
     private val bmcSolver: Solver? = null,
-    private val bmcEnabled: () -> Boolean = { true },
+    private val bmcEnabled: () -> Boolean = { bmcSolver != null },
     private val lfPathOnly: () -> Boolean = { true },
     private val itpSolver: ItpSolver? = null,
-    private val imcEnabled: (Int) -> Boolean = { true },
+    private val imcEnabled: (Int) -> Boolean = { itpSolver != null },
     private val indSolver: Solver? = null,
-    private val kindEnabled: (Int) -> Boolean = { true },
+    private val kindEnabled: (Int) -> Boolean = { indSolver != null },
     private val valToState: (Valuation) -> S,
     private val biValToAction: (Valuation, Valuation) -> A,
     private val logger: Logger,
 ) : SafetyChecker<EmptyWitness, Trace<S, A>, UnitPrec> {
 
     private val vars = monolithicExpr.vars()
-    private val unfoldedInitExpr = PathUtils.unfold(monolithicExpr.initExpr, 0)
+    private val unfoldedInitExpr = PathUtils.unfold(monolithicExpr.initExpr, VarIndexingFactory.indexing(0))
     private val unfoldedPropExpr = { i: VarIndexing -> PathUtils.unfold(monolithicExpr.propExpr, i) }
-    private val indices = mutableListOf(VarIndexingFactory.indexing(0))
+    private val indices = mutableListOf(monolithicExpr.initOffsetIndex)
     private val exprs = mutableListOf<Expr<BoolType>>()
     private var kindLastIterLookup = 0
 
@@ -98,7 +98,7 @@ class BoundedChecker<S : ExprState, A : ExprAction> @JvmOverloads constructor(
 
             exprs.add(PathUtils.unfold(monolithicExpr.transExpr, indices.last()))
 
-            indices.add(indices.last().add(monolithicExpr.offsetIndex))
+            indices.add(indices.last().add(monolithicExpr.transOffsetIndex))
 
             if (isBmcEnabled) {
                 bmc()?.let { return it }