Merge pull request #248 from csanadtelbisz/xcfa-coi-benchmark

Xcfa COI SPIN artifact code
ftsrg · Jan 18, 2024 · 6255313 · 6255313
2 parents 2c863d7 + e712a35
commit 6255313
Show file tree

Hide file tree

Showing 20 changed files with 632 additions and 34 deletions.
diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/ArgNode.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/ArgNode.java
@@ -86,7 +86,7 @@ public void setState(final S state) {
 
     public boolean mayCover(final ArgNode<S, A> node) {
         if (arg.getPartialOrd().isLeq(node.getState(), this.getState())) {
-            return ancestors().noneMatch(n -> n.equals(node) || n.isSubsumed());
+            return !(this.equals(node) || this.isSubsumed());
         } else {
             return false;
         }

diff --git a/...mon/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/BasicAbstractor.java b/...mon/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/BasicAbstractor.java
@@ -129,6 +129,7 @@ private void close(final ArgNode<S, A> node, final Collection<ArgNode<S, A>> can
         for (final ArgNode<S, A> candidate : candidates) {
             if (candidate.mayCover(node)) {
                 node.cover(candidate);
+                COILogger.incCovers();
                 return;
             }
         }

diff --git a/...ts/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/COILogger.java b/...ts/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/COILogger.java
@@ -0,0 +1,67 @@
+package hu.bme.mit.theta.analysis.algorithm.cegar;
+
+import java.util.ArrayList;
+import java.util.List;
+
+public class COILogger {
+    static long coiTimer = 0;
+    static long transFuncTimer = 0;
+    private static long startCoi = 0;
+    private static long startTransFunc = 0;
+    public static void startCoiTimer() {
+        startCoi = System.currentTimeMillis();
+    }
+    public static void stopCoiTimer() {
+        coiTimer += System.currentTimeMillis() - startCoi;
+    }
+    public static void startTransFuncTimer() {
+        startTransFunc = System.currentTimeMillis();
+    }
+    public static void stopTransFuncTimer() {
+        transFuncTimer += System.currentTimeMillis() - startTransFunc;
+    }
+
+    static long nops = 0;
+    static List<Long> nopsList = new ArrayList<>();
+    public static void incNops() {
+        nops++;
+    }
+    public static void decNops() {
+        nops--;
+    }
+    static long havocs = 0;
+    static List<Long> havocsList = new ArrayList<>();
+    public static void incHavocs() {
+        havocs++;
+    }
+    public static void decHavocs() {
+        havocs--;
+    }
+    static long allLabels = 0;
+    static List<Long> allLabelsList = new ArrayList<>();
+    public static void incAllLabels() {
+        allLabels++;
+    }
+    static long exploredActions = 0;
+    static List<Long> exploredActionsList = new ArrayList<>();
+    public static void incExploredActions() {
+        exploredActions++;
+    }
+    static long covers = 0;
+    static List<Long> coversList = new ArrayList<>();
+    public static void incCovers() {
+        covers++;
+    }
+    public static void newIteration() {
+        nopsList.add(nops);
+        havocsList.add(havocs);
+        allLabelsList.add(allLabels);
+        exploredActionsList.add(exploredActions);
+        coversList.add(covers);
+        nops = 0;
+        havocs = 0;
+        allLabels = 0;
+        exploredActions = 0;
+        covers = 0;
+    }
+}
diff --git a/...common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/CegarChecker.java b/...common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/CegarChecker.java
@@ -29,9 +29,13 @@
 import hu.bme.mit.theta.common.logging.Logger.Level;
 import hu.bme.mit.theta.common.logging.NullLogger;
 
+import hu.bme.mit.theta.common.visualization.Graph;
+import hu.bme.mit.theta.common.visualization.writer.GraphvizWriter;
 import hu.bme.mit.theta.common.visualization.writer.JSONWriter;
 import hu.bme.mit.theta.common.visualization.writer.WebDebuggerLogger;
 
+import java.io.FileWriter;
+import java.io.IOException;
 import java.util.concurrent.TimeUnit;
 
 import static com.google.common.base.Preconditions.checkNotNull;
@@ -80,7 +84,7 @@ public SafetyResult<S, A> check(final P initPrec) {
         AbstractorResult abstractorResult = null;
         P prec = initPrec;
         int iteration = 0;
-        WebDebuggerLogger wdl = WebDebuggerLogger.getInstance();
+//        WebDebuggerLogger wdl = WebDebuggerLogger.getInstance();
         do {
             ++iteration;
 
@@ -91,10 +95,11 @@ public SafetyResult<S, A> check(final P initPrec) {
             abstractorTime += stopwatch.elapsed(TimeUnit.MILLISECONDS) - abstractorStartTime;
             logger.write(Level.MAINSTEP, "| Checking abstraction done, result: %s%n", abstractorResult);
 
-            String argGraph = JSONWriter.getInstance().writeString(ArgVisualizer.getDefault().visualize(arg));
-            String precString = prec.toString();
+//            String argGraph = JSONWriter.getInstance().writeString(ArgVisualizer.getDefault().visualize(arg));
+//            String precString = prec.toString();
 
-            wdl.addIteration(iteration, argGraph, precString);
+//            wdl.addIteration(iteration, argGraph, precString);
+            COILogger.newIteration();
 
             if (abstractorResult.isUnsafe()) {
                 MonitorCheckpoint.Checkpoints.execute("CegarChecker.unsafeARG");
@@ -136,6 +141,15 @@ public SafetyResult<S, A> check(final P initPrec) {
         assert cegarResult != null;
         logger.write(Level.RESULT, "%s%n", cegarResult);
         logger.write(Level.INFO, "%s%n", stats);
+        System.err.println("Abstractor time: " + stats.getAbstractorTimeMs());
+        System.err.println("Refiner time: " + stats.getRefinerTimeMs());
+        System.err.println("COI time: " + COILogger.coiTimer);
+        System.err.println("TransFunc time: " + COILogger.transFuncTimer);
+        System.err.println("COI NOP labels: " + COILogger.nopsList);
+        System.err.println("COI havoc labels: " + COILogger.havocsList);
+        System.err.println("COI all labels: " + COILogger.allLabelsList);
+        System.err.println("Covers: " + COILogger.coversList);
+        System.err.println("Explored actions: " + COILogger.exploredActionsList);
         return cegarResult;
     }
 

diff --git a/...rojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/pred/PredAbstractors.java b/...rojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/pred/PredAbstractors.java
@@ -15,6 +15,7 @@
  */
 package hu.bme.mit.theta.analysis.pred;
 
+import hu.bme.mit.theta.analysis.expr.ExprAction;
 import hu.bme.mit.theta.common.container.Containers;
 import hu.bme.mit.theta.core.decl.ConstDecl;
 import hu.bme.mit.theta.core.decl.Decls;
@@ -23,6 +24,7 @@
 import hu.bme.mit.theta.core.type.LitExpr;
 import hu.bme.mit.theta.core.type.booltype.BoolExprs;
 import hu.bme.mit.theta.core.type.booltype.BoolType;
+import hu.bme.mit.theta.core.utils.ExprUtils;
 import hu.bme.mit.theta.core.utils.PathUtils;
 import hu.bme.mit.theta.core.utils.indexings.VarIndexing;
 import hu.bme.mit.theta.solver.Solver;
@@ -69,6 +71,15 @@ public interface PredAbstractor {
         Collection<PredState> createStatesForExpr(final Expr<BoolType> expr,
                                                   final VarIndexing exprIndexing,
                                                   final PredPrec prec, final VarIndexing precIndexing);
+
+        default Collection<PredState> createStatesForExpr(final Expr<BoolType> expr,
+                                                          final VarIndexing exprIndexing,
+                                                          final PredPrec prec,
+                                                          final VarIndexing precIndexing,
+                                                          final PredState state,
+                                                          final ExprAction action) {
+            return createStatesForExpr(expr, exprIndexing, prec, precIndexing);
+        }
     }
 
     /**
@@ -225,5 +236,23 @@ public Collection<PredState> createStatesForExpr(final Expr<BoolType> expr,
             return Collections.singleton(PredState.of(newStatePreds));
         }
 
+        @Override
+        public Collection<PredState> createStatesForExpr(final Expr<BoolType> expr,
+                                                         final VarIndexing exprIndexing,
+                                                         final PredPrec prec,
+                                                         final VarIndexing precIndexing,
+                                                         final PredState state,
+                                                         final ExprAction action) {
+            var actionExpr = action.toExpr();
+            if (actionExpr.equals(True())) {
+                var filteredPreds = state.getPreds().stream().filter(p -> {
+                    var vars = ExprUtils.getVars(p);
+                    var indexing = action.nextIndexing();
+                    return vars.stream().allMatch(v -> indexing.get(v) == 0);
+                }).collect(Collectors.toList());
+                return Collections.singleton(PredState.of(filteredPreds));
+            }
+            return createStatesForExpr(expr, exprIndexing, prec, precIndexing);
+        }
     }
 }
diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/pred/PredTransFunc.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/pred/PredTransFunc.java
@@ -50,7 +50,7 @@ public Collection<? extends PredState> getSuccStates(final PredState state,
 
         final Collection<PredState> succStates = predAbstractor.createStatesForExpr(
                 And(state.toExpr(), action.toExpr()), VarIndexingFactory.indexing(0), prec,
-                action.nextIndexing());
+                action.nextIndexing(), state, action);
         return succStates.isEmpty() ? Collections.singleton(PredState.bottom()) : succStates;
     }
 

diff --git a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaAnalysis.kt b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaAnalysis.kt
@@ -38,6 +38,7 @@ import hu.bme.mit.theta.core.type.booltype.BoolExprs.True
 import hu.bme.mit.theta.core.utils.TypeUtils
 import hu.bme.mit.theta.solver.Solver
 import hu.bme.mit.theta.xcfa.analysis.XcfaProcessState.Companion.createLookup
+import hu.bme.mit.theta.xcfa.analysis.coi.COI
 import hu.bme.mit.theta.xcfa.getFlatLabels
 import hu.bme.mit.theta.xcfa.getGlobalVars
 import hu.bme.mit.theta.xcfa.isWritten
@@ -50,9 +51,14 @@ import java.util.function.Predicate
 open class XcfaAnalysis<S : ExprState, P : Prec>(
     private val corePartialOrd: PartialOrd<XcfaState<S>>,
     private val coreInitFunc: InitFunc<XcfaState<S>, XcfaPrec<P>>,
-    private val coreTransFunc: TransFunc<XcfaState<S>, XcfaAction, XcfaPrec<P>>,
+    private var coreTransFunc: TransFunc<XcfaState<S>, XcfaAction, XcfaPrec<P>>,
 ) : Analysis<XcfaState<S>, XcfaAction, XcfaPrec<P>> {
 
+    init {
+        COI.coreTransFunc = transFunc as TransFunc<XcfaState<out ExprState>, XcfaAction, XcfaPrec<out Prec>>
+        coreTransFunc = COI.transFunc as TransFunc<XcfaState<S>, XcfaAction, XcfaPrec<P>>
+    }
+
     override fun getPartialOrd(): PartialOrd<XcfaState<S>> = corePartialOrd
     override fun getInitFunc(): InitFunc<XcfaState<S>, XcfaPrec<P>> = coreInitFunc
     override fun getTransFunc(): TransFunc<XcfaState<S>, XcfaAction, XcfaPrec<P>> = coreTransFunc
@@ -192,6 +198,7 @@ fun <S : XcfaState<out ExprState>, P : XcfaPrec<out Prec>> getXcfaAbstractor(
     BasicAbstractor.builder(getXcfaArgBuilder(analysis, lts, errorDetection))
         .waitlist(waitlist as Waitlist<ArgNode<S, XcfaAction>>) // TODO: can we do this nicely?
         .stopCriterion(stopCriterion as StopCriterion<S, XcfaAction>).logger(logger)
+        .projection { it.processes }
         .build() // TODO: can we do this nicely?
 
 /// EXPL