Merge pull request #379 from ftsrg/xcfa-mdd-trace

XCFA MDD Trace

Author: leventeBajczi

build.gradle.kts

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

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

@@ -32,6 +32,7 @@
 import hu.bme.mit.theta.analysis.unit.UnitPrec;
 import hu.bme.mit.theta.common.logging.Logger;
 import hu.bme.mit.theta.solver.SolverFactory;
+import java.util.ArrayList;
 import java.util.List;
 import java.util.function.Function;
 
@@ -103,7 +104,21 @@ public MonolithicExprCegarChecker(
                     if (concretizationResult.isFeasible()) {
                         logger.write(Logger.Level.MAINSTEP, "Model is unsafe, stopping CEGAR\n");
 
-                        return SafetyResult.unsafe(trace, result.getProof());
+                        final var valuations =
+                                concretizationResult.asFeasible().getValuations().getStates();
+                        final List<ExprState> states = new ArrayList<>();
+                        final List<ExprAction> actions = new ArrayList<>();
+                        for (int i = 0; i < valuations.size(); ++i) {
+                            states.add(model.getValToState().invoke(valuations.get(i)));
+                            if (i > 0) {
+                                actions.add(
+                                        model.getBiValToAction()
+                                                .invoke(valuations.get(i - 1), valuations.get(i)));
+                            }
+                        }
+
+                        return SafetyResult.Unsafe.unsafe(
+                                Trace.of(states, actions), result.getProof());
                     } else {
                         final var ref = concretizationResult.asInfeasible().getRefutation();
                         final var newPred = ref.get(ref.getPruneIndex());

subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mdd/MddChecker.java

@@ -283,7 +283,6 @@ public SafetyResult<MddProof, Trace<S, A>> check(UnitPrec prec) {
         } else {
             result = SafetyResult.safe(MddProof.of(stateSpace), statistics);
         }
-        logger.write(Level.RESULT, "%s\n", result);
         return result;
     }
 }

subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToMddChecker.kt

@@ -18,14 +18,21 @@ package hu.bme.mit.theta.xcfa.cli.checkers
 import hu.bme.mit.theta.analysis.Trace
 import hu.bme.mit.theta.analysis.algorithm.SafetyChecker
 import hu.bme.mit.theta.analysis.algorithm.SafetyResult
+import hu.bme.mit.theta.analysis.algorithm.bounded.MonolithicExpr
+import hu.bme.mit.theta.analysis.algorithm.bounded.MonolithicExprCegarChecker
 import hu.bme.mit.theta.analysis.algorithm.bounded.createMonolithicL2S
 import hu.bme.mit.theta.analysis.algorithm.bounded.createReversed
 import hu.bme.mit.theta.analysis.algorithm.mdd.MddChecker
+import hu.bme.mit.theta.analysis.algorithm.mdd.MddProof
 import hu.bme.mit.theta.analysis.algorithm.mdd.MddValuationCollector
 import hu.bme.mit.theta.analysis.algorithm.mdd.varordering.orderVarsFromRandomStartingPoints
 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.pred.PredPrec
+import hu.bme.mit.theta.analysis.pred.PredState
+import hu.bme.mit.theta.analysis.ptr.PtrPrec
+import hu.bme.mit.theta.analysis.ptr.PtrState
 import hu.bme.mit.theta.analysis.unit.UnitPrec
 import hu.bme.mit.theta.common.logging.Logger
 import hu.bme.mit.theta.core.decl.IndexedConstDecl
@@ -68,33 +75,71 @@ fun getMddChecker(
           it.copy(propExpr = True()).createMonolithicL2S()
         else it
       }
-      .let {
-        if (mddConfig.cegar) {
-          TODO("MDD cannot return traces, and thus, --cegar won't work yet.")
-        } else it
-      }
       .let { if (mddConfig.reversed) it.createReversed() else it }
 
   val stmts =
     xcfa.procedures
       .flatMap { it.edges.flatMap { xcfaEdge -> xcfaEdge.getFlatLabels().map { it.toStmt() } } }
       .toSet()
-  val variableOrder = orderVarsFromRandomStartingPoints(monolithicExpr.vars, stmts, 20)
   val solverPool = SolverPool(refinementSolverFactory)
   val iterationStrategy = mddConfig.iterationStrategy
 
-  val checker =
-    MddChecker.create<ExprState, ExprAction>(
-      monolithicExpr,
-      variableOrder,
+  val baseChecker = { abstractME: MonolithicExpr ->
+    MddChecker.create(
+      abstractME,
+      orderVarsFromRandomStartingPoints(abstractME.vars, stmts, 20),
       solverPool,
       logger,
       iterationStrategy,
-      monolithicExpr.valToState,
-      monolithicExpr.biValToAction,
+      abstractME.valToState,
+      abstractME.biValToAction,
     )
-  return SafetyChecker<LocationInvariants, Trace<ExprState, ExprAction>, UnitPrec> { input ->
-    val result = checker.check(input)
+  }
+
+  val checker: SafetyChecker<MddProof, Trace<ExprState, ExprAction>, UnitPrec> =
+    (if (mddConfig.cegar) {
+      val cegarChecker =
+        MonolithicExprCegarChecker(
+          monolithicExpr,
+          baseChecker,
+          logger,
+          getSolver(mddConfig.solver, false),
+        )
+      object :
+        SafetyChecker<
+          MddProof,
+          Trace<XcfaState<PtrState<PredState>>, XcfaAction>,
+          XcfaPrec<PtrPrec<PredPrec>>,
+        > {
+        override fun check(
+          initPrec: XcfaPrec<PtrPrec<PredPrec>>
+        ): SafetyResult<MddProof, Trace<XcfaState<PtrState<PredState>>, XcfaAction>> {
+          val result =
+            cegarChecker.check(initPrec.p.innerPrec) // states are PredState, actions are XcfaAction
+          if (result.isUnsafe) {
+            val cex = result.asUnsafe().cex as Trace<PredState, XcfaAction>
+            val locs =
+              (0 until cex.length()).map { i -> cex.actions[i].source } +
+                cex.actions[cex.length() - 1].target
+            val states = locs.mapIndexed { i, it -> XcfaState(xcfa, it, PtrState(cex.states[i])) }
+            return SafetyResult.unsafe(Trace.of(states, cex.actions), result.proof)
+          } else
+            return result
+              as SafetyResult<MddProof, Trace<XcfaState<PtrState<PredState>>, XcfaAction>>
+        }
+
+        override fun check():
+          SafetyResult<MddProof, Trace<XcfaState<PtrState<PredState>>, XcfaAction>> {
+          return check(mddConfig.initPrec.predPrec(xcfa))
+        }
+      }
+    } else {
+      baseChecker(monolithicExpr)
+    })
+      as SafetyChecker<MddProof, Trace<ExprState, ExprAction>, UnitPrec>
+
+  return SafetyChecker<LocationInvariants, Trace<ExprState, ExprAction>, UnitPrec> {
+    val result = checker.check()
     if (result.isUnsafe) {
       SafetyResult.unsafe(result.asUnsafe().cex, LocationInvariants())
     } else {

subprojects/xcfa/xcfa-cli/src/test/resources/c/litmustest/singlethread/22nondet.c

@@ -1,8 +1,8 @@
 void reach_error(){}
-extern int __VERIFIER_nondet_int();
+extern char __VERIFIER_nondet_char();
 int main() {
     int i = 0;
-    if(__VERIFIER_nondet_int() % 2) {
+    if(__VERIFIER_nondet_char() % 2) {
         i = 1;
     } else {
         i = 2;

subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/XcfaToC.kt

@@ -65,6 +65,7 @@ fun XCFA.toC(
   """         
     extern void abort();
     extern unsigned short __VERIFIER_nondet_ushort();
+    extern char __VERIFIER_nondet_char();
     extern short __VERIFIER_nondet_short();
     extern int __VERIFIER_nondet_int();
     extern _Bool __VERIFIER_nondet__Bool();