Bugfixes, kind sanitization

ftsrg · Nov 16, 2023 · 757c652 · 757c652
1 parent fdce131
commit 757c652
Show file tree

Hide file tree

Showing 5 changed files with 39 additions and 18 deletions.
diff --git a/subprojects/cfa/cfa-cli/src/main/java/hu/bme/mit/theta/cfa/cli/CfaCli.java b/subprojects/cfa/cfa-cli/src/main/java/hu/bme/mit/theta/cfa/cli/CfaCli.java
@@ -243,7 +243,7 @@ private void run() {
                 sw.stop();
             } else if (algorithm == Algorithm.KINDUCTION) {
                 var transFunc = CfaToMonoliticTransFunc.create(cfa);
-                var checker = new KIndChecker<>(transFunc, Integer.MAX_VALUE, inductionStartBound, inductionFrequency, Z3SolverFactory.getInstance().createSolver(), Z3SolverFactory.getInstance().createSolver(), ExplState::of, cfa.getVars());
+                var checker = new KIndChecker<>(transFunc, Integer.MAX_VALUE, 0, 1, Z3SolverFactory.getInstance().createSolver(), Z3SolverFactory.getInstance().createSolver(), ExplState::of, cfa.getVars());
                 status = checker.check(null);
                 logger.write(Logger.Level.RESULT, "%s%n", status);
                 sw.stop();

diff --git a/...s/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/kind/KIndChecker.java b/...s/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/kind/KIndChecker.java
@@ -93,7 +93,7 @@ public SafetyResult<S, A> check(UnitPrec prec) {
         solver1.add(PathUtils.unfold(init, VarIndexingFactory.indexing(0)));
         var eqList = new ArrayList<Expr<BoolType>>();
         while (i < upperBound) {
-
+            // BMC part
 
             solver1.add(PathUtils.unfold(trans, currIndex));
 
@@ -109,10 +109,6 @@ public SafetyResult<S, A> check(UnitPrec prec) {
             eqList.addAll(finalList);
             listOfIndexes.add(currIndex);
 
-
-            solver2.add(PathUtils.unfold(prop, currIndex.sub(firstIndexing))); //0-ról indítva
-            solver2.add(PathUtils.unfold(trans, currIndex.sub(firstIndexing)));
-
             currIndex = currIndex.add(offset);
 
             // Checking loop free path of length i
@@ -148,19 +144,23 @@ public SafetyResult<S, A> check(UnitPrec prec) {
             }
             solver1.pop();
 
-
-            // Property k-inductivity check
+            // KIND part
 
             // P1 and T1-2 and P2 and ... and Tk-k+1
 
+            solver2.add(PathUtils.unfold(prop, currIndex.sub(firstIndexing)));
+            solver2.add(PathUtils.unfold(trans, currIndex.sub(firstIndexing)));
+
             // Not Pk+1
-            solver2.push();
-            solver2.add(PathUtils.unfold(Not(prop), currIndex.sub(firstIndexing)));
+            if (i >= inductionStartBound && (i - inductionStartBound) % inductionFrequency == 0) {
+                solver2.push();
+                solver2.add(PathUtils.unfold(Not(prop), currIndex.sub(firstIndexing)));
 
-            if (solver2.check().isUnsat()) {
-                return SafetyResult.safe(ARG.create(null));
+                if (solver2.check().isUnsat()) {
+                    return SafetyResult.safe(ARG.create(null));
+                }
+                solver2.pop();
             }
-            solver2.pop();
             i++;
         }
         return null;

diff --git a/subprojects/sts/sts-cli/src/main/java/hu/bme/mit/theta/sts/cli/StsCli.java b/subprojects/sts/sts-cli/src/main/java/hu/bme/mit/theta/sts/cli/StsCli.java
@@ -168,7 +168,7 @@ private void run() {
                 status = check(configuration);
             } else if (algorithm.equals(Algorithm.KINDUCTION)) {
                 var transFunc = StsToMonoliticTransFunc.create(sts);
-                var checker = new KIndChecker<>(transFunc, Integer.MAX_VALUE, inductionStartBound, inductionFrequency, Z3SolverFactory.getInstance().createSolver(), Z3SolverFactory.getInstance().createSolver(), ExplState::of, sts.getVars());
+                var checker = new KIndChecker<>(transFunc, Integer.MAX_VALUE, 0, 1, Z3SolverFactory.getInstance().createSolver(), Z3SolverFactory.getInstance().createSolver(), ExplState::of, sts.getVars());
                 status = checker.check(null);
             } else if (algorithm.equals(Algorithm.IMC)) {
                 var transFunc = StsToMonoliticTransFunc.create(sts);

diff --git a/subprojects/xcfa/xcfa-cli/src/test/java/hu/bme/mit/theta/xcfa/cli/XcfaCliVerifyTest.kt b/subprojects/xcfa/xcfa-cli/src/test/java/hu/bme/mit/theta/xcfa/cli/XcfaCliVerifyTest.kt
@@ -56,6 +56,28 @@ class XcfaCliVerifyTest {
             )
         }
 
+        @JvmStatic
+        fun singleThreadedCFiles(): Stream<Arguments> {
+            return Stream.of(
+                Arguments.of("/c/litmustest/singlethread/00assignment.c", null),
+                Arguments.of("/c/litmustest/singlethread/01cast.c", null),
+                Arguments.of("/c/litmustest/singlethread/02types.c", null),
+                Arguments.of("/c/litmustest/singlethread/03bitwise.c", null),
+                Arguments.of("/c/litmustest/singlethread/04real.c", null),
+                Arguments.of("/c/litmustest/singlethread/06arrays.c", null),
+                Arguments.of("/c/litmustest/singlethread/07arrayinit.c", null),
+                Arguments.of("/c/litmustest/singlethread/08vararray.c", null),
+                Arguments.of("/c/litmustest/singlethread/13typedef.c", "--domain PRED_CART"),
+                Arguments.of("/c/litmustest/singlethread/14ushort.c", null),
+                Arguments.of("/c/litmustest/singlethread/15addition.c", null),
+                Arguments.of("/c/litmustest/singlethread/16loop.c", null),
+                Arguments.of("/c/litmustest/singlethread/20testinline.c", null),
+                Arguments.of("/c/litmustest/singlethread/21namecollision.c", null),
+                Arguments.of("/c/litmustest/singlethread/22nondet.c", null),
+                Arguments.of("/c/litmustest/singlethread/23overflow.c", "--domain PRED_CART"),
+            )
+        }
+
         @JvmStatic
         fun cFilesShort(): Stream<Arguments> {
             return Stream.of(
@@ -164,14 +186,13 @@ class XcfaCliVerifyTest {
     }
 
     @ParameterizedTest
-    @MethodSource("cFiles")
+    @MethodSource("singleThreadedCFiles")
     fun testCVerifyKind(filePath: String, extraArgs: String?) {
         val params = arrayOf(
-            "--algorithm", "KINDUCTION",
+            "--backend", "KIND",
             "--input-type", "C",
             "--input", javaClass.getResource(filePath)!!.path,
             "--stacktrace",
-            *(extraArgs?.split(" ")?.toTypedArray() ?: emptyArray()),
             "--debug"
         )
         main(params)

diff --git a/subprojects/xsts/xsts-cli/src/main/java/hu/bme/mit/theta/xsts/cli/XstsCli.java b/subprojects/xsts/xsts-cli/src/main/java/hu/bme/mit/theta/xsts/cli/XstsCli.java
@@ -205,7 +205,7 @@ private void run() {
                 sw.stop();
             } else if (algorithm.equals(Algorithm.KINDUCTION)) {
                 var transFunc = XstsToMonoliticTransFunc.create(xsts);
-                var checker = new KIndChecker<XstsState<ExplState>, XstsAction>(transFunc, Integer.MAX_VALUE, inductionStartBound, inductionFrequency, Z3SolverFactory.getInstance().createSolver(), Z3SolverFactory.getInstance().createSolver(), (x) -> XstsState.of(ExplState.of(x), false, true), xsts.getVars());
+                var checker = new KIndChecker<XstsState<ExplState>, XstsAction>(transFunc, Integer.MAX_VALUE, 0, 1, Z3SolverFactory.getInstance().createSolver(), Z3SolverFactory.getInstance().createSolver(), (x) -> XstsState.of(ExplState.of(x), false, true), xsts.getVars());
                 status = checker.check(null);
                 logger.write(Logger.Level.RESULT, "%s%n", status);
                 sw.stop();