Sanitized branch

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, Z3SolverFactory.getInstance().createSolver(), Z3SolverFactory.getInstance().createSolver(), ExplState::of, cfa.getVars());
+                var checker = new KIndChecker<>(transFunc, Integer.MAX_VALUE, inductionStartBound, inductionFrequency, Z3SolverFactory.getInstance().createSolver(), Z3SolverFactory.getInstance().createSolver(), ExplState::of, cfa.getVars());
                 status = checker.check(null);
                 logger.write(Logger.Level.RESULT, "%s%n", status);
                 sw.stop();

subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/kind/KIndChecker.java

@@ -45,20 +45,24 @@
 
 
 public class KIndChecker<S extends ExprState, A extends ExprAction> implements SafetyChecker<S, A, UnitPrec> {
-    final Expr<BoolType> trans;
-    final Expr<BoolType> init;
-    final Expr<BoolType> prop;
-    final int upperBound;
-    Solver solver1;
-    Solver solver2;
-    final VarIndexing firstIndexing;
-    final VarIndexing offset;
-    final Function<Valuation, S> valToState;
-    final Collection<VarDecl<?>> vars;
+    private final Expr<BoolType> trans;
+    private final Expr<BoolType> init;
+    private final Expr<BoolType> prop;
+    private final int upperBound;
+    private final int inductionStartBound;
+    private final int inductionFrequency;
+    private Solver solver1;
+    private Solver solver2;
+    private final VarIndexing firstIndexing;
+    private final VarIndexing offset;
+    private final Function<Valuation, S> valToState;
+    private final Collection<VarDecl<?>> vars;
 
 
     public KIndChecker(MonolithicTransFunc transFunc,
                        int upperBound,
+                       int inductionStartBound,
+                       int inductionFrequency,
                        Solver solver1,
                        Solver solver2,
                        Function<Valuation, S> valToState,
@@ -67,6 +71,8 @@ public KIndChecker(MonolithicTransFunc transFunc,
         this.init = transFunc.getInitExpr();
         this.prop = transFunc.getPropExpr();
         this.upperBound = upperBound;
+        this.inductionStartBound = inductionStartBound;
+        this.inductionFrequency = inductionFrequency;
         this.solver1 = solver1;
         this.solver2 = solver2;
         this.firstIndexing = transFunc.getInitIndexing();
@@ -78,32 +84,24 @@ public KIndChecker(MonolithicTransFunc transFunc,
 
     @Override
     public SafetyResult<S, A> check(UnitPrec prec) {
-        //var trans = action.toExpr();
-        //var offset = action.nextIndexing();
-
         int i = 0;
         var currIndex = firstIndexing;
 
 
-        var exprsFromStart = new ArrayList<Expr<BoolType>>();
-        var exprsForInductivity = new ArrayList<Expr<BoolType>>();
         var listOfIndexes = new ArrayList<VarIndexing>();
 
-        solver1.add(PathUtils.unfold(init, VarIndexingFactory.indexing(0))); // VarIndexingFactory.indexing(0)?
+        solver1.add(PathUtils.unfold(init, VarIndexingFactory.indexing(0)));
         var eqList = new ArrayList<Expr<BoolType>>();
         while (i < upperBound) {
 
 
             solver1.add(PathUtils.unfold(trans, currIndex));
 
-            // külső lista üres
             var finalList = new ArrayList<Expr<BoolType>>();
 
             for (int j = 0; j < listOfIndexes.size(); j++) {
-                // új belső lista az adott indexű állapothoz
                 var tempList = new ArrayList<Expr<BoolType>>();
                 for (var v : vars) {
-                    // a mostani listához adom az Eq-et
                     tempList.add(Eq(PathUtils.unfold(v.getRef(), currIndex), PathUtils.unfold(v.getRef(), listOfIndexes.get(j))));
                 }
                 finalList.add(Not(And(tempList)));

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, Z3SolverFactory.getInstance().createSolver(), Z3SolverFactory.getInstance().createSolver(), ExplState::of, sts.getVars());
+                var checker = new KIndChecker<>(transFunc, Integer.MAX_VALUE, inductionStartBound, inductionFrequency, 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);

subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaMonolithicTransFunc.java

@@ -53,7 +53,7 @@ private XcfaMonolithicTransFunc(XCFA xcfa) {
         for (var x : proc.getLocs()) {
             map.put(x, i++);
         }
-        var locVar = Decls.Var("loc", Int());
+        var locVar = Decls.Var("__loc_", Int());
         List<Stmt> tranList = proc.getEdges().stream().map(e -> SequenceStmt.of(List.of(
                 AssumeStmt.of(Eq(locVar.getRef(), Int(map.get(e.getSource())))),
                 e.getLabel().toStmt(),

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

@@ -59,7 +59,8 @@ enum class InputType {
 
 enum class Backend {
     CEGAR,
-    BMC,
+    KIND,
+    IMC,
     LAZY
 }
 

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

@@ -25,10 +25,7 @@ import com.google.gson.JsonParser
 import hu.bme.mit.theta.analysis.Trace
 import hu.bme.mit.theta.analysis.algorithm.SafetyResult
 import hu.bme.mit.theta.analysis.algorithm.debug.ARGWebDebugger
-import hu.bme.mit.theta.analysis.algorithm.imc.ImcChecker
-import hu.bme.mit.theta.analysis.algorithm.kind.KIndChecker
 import hu.bme.mit.theta.analysis.expl.ExplState
-import hu.bme.mit.theta.analysis.expr.StmtAction
 import hu.bme.mit.theta.analysis.utils.ArgVisualizer
 import hu.bme.mit.theta.analysis.utils.TraceVisualizer
 import hu.bme.mit.theta.c2xcfa.getXcfaFromC
@@ -39,7 +36,6 @@ import hu.bme.mit.theta.common.logging.UniqueWarningLogger
 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.WebDebuggerLogger
-import hu.bme.mit.theta.core.utils.ExprUtils
 import hu.bme.mit.theta.frontend.ParseContext
 import hu.bme.mit.theta.frontend.chc.ChcFrontend
 import hu.bme.mit.theta.frontend.transformation.ArchitectureConfig
@@ -48,7 +44,6 @@ import hu.bme.mit.theta.llvm2xcfa.XcfaUtils.fromFile
 import hu.bme.mit.theta.solver.smtlib.SmtLibSolverManager
 import hu.bme.mit.theta.xcfa.analysis.ErrorDetection
 import hu.bme.mit.theta.xcfa.analysis.XcfaAction
-import hu.bme.mit.theta.xcfa.analysis.XcfaMonolithicTransFunc
 import hu.bme.mit.theta.xcfa.analysis.XcfaState
 import hu.bme.mit.theta.xcfa.analysis.coi.ConeOfInfluence
 import hu.bme.mit.theta.xcfa.analysis.coi.XcfaCoiMultiThread
@@ -83,16 +78,6 @@ class XcfaCli(private val args: Array<String>) {
 
     //////////// CONFIGURATION OPTIONS BEGIN ////////////
     //////////// input task ////////////
-    public enum class Algorithm {
-
-        CEGAR,
-        KINDUCTION,
-        IMC
-    }
-
-    @Parameter(names = ["--algorithm"], description = "Algorithm")
-    var algorithm: Algorithm = Algorithm.CEGAR
-
     @Parameter(names = ["--input"], description = "Path of the input C program", required = true)
     var input: File? = null
 
@@ -168,6 +153,10 @@ class XcfaCli(private val args: Array<String>) {
     @Parameter(names = ["--cex-solver"], description = "Concretizer solver name")
     var concretizerSolver: String = "Z3"
 
+    @Parameter(names = ["--validate-cex-solver"],
+        description = "Activates a wrapper, which validates the assertions in the solver in each (SAT) check. Filters some solver issues.")
+    var validateConcretizerSolver: Boolean = false
+
     @Parameter(names = ["--to-c-use-arrays"])
     var useArr: Boolean = false
 
@@ -177,10 +166,6 @@ class XcfaCli(private val args: Array<String>) {
     @Parameter(names = ["--to-c-use-ranges"])
     var useRange: Boolean = false
 
-    @Parameter(names = ["--validate-cex-solver"],
-        description = "Activates a wrapper, which validates the assertions in the solver in each (SAT) check. Filters some solver issues.")
-    var validateConcretizerSolver: Boolean = false
-
     @Parameter(names = ["--seed"], description = "Random seed used for DPOR")
     var randomSeed: Int = -1
 
@@ -245,47 +230,44 @@ class XcfaCli(private val args: Array<String>) {
         // verification
         stopwatch.reset().start()
 
+        val safetyResult: SafetyResult<*, *> =
+            if (backend == Backend.CEGAR) {
+                logger.write(Logger.Level.INFO,
+                    "Starting verification of ${if (xcfa.name == "") "UnnamedXcfa" else xcfa.name} using $backend\n")
+                registerAllSolverManagers(solverHome, logger)
+                logger.write(Logger.Level.INFO,
+                    "Registered solver managers successfully (in ${stopwatch.elapsed(TimeUnit.MILLISECONDS)} ms)\n")
+                stopwatch.reset().start()
+                val config = parseCEGARConfigFromCli(parseContext)
+                if (strategy != Strategy.PORTFOLIO && printConfigFile != null) {
+                    printConfigFile!!.writeText(gsonForOutput.toJson(config))
+                }
+                logger.write(Logger.Level.INFO, "Parsed config (in ${stopwatch.elapsed(TimeUnit.MILLISECONDS)} ms)\n")
+                stopwatch.reset().start()
 
-        if (algorithm == Algorithm.CEGAR) {
-            logger.write(Logger.Level.INFO,
-                "Starting verification of ${if (xcfa.name == "") "UnnamedXcfa" else xcfa.name} using $backend\n")
-            registerAllSolverManagers(solverHome, logger)
-            logger.write(Logger.Level.INFO,
-                "Registered solver managers successfully (in ${stopwatch.elapsed(TimeUnit.MILLISECONDS)} ms)\n")
-            stopwatch.reset().start()
-            val config = parseConfigFromCli(parseContext)
-            if (strategy != Strategy.PORTFOLIO && printConfigFile != null) {
-                printConfigFile!!.writeText(gsonForOutput.toJson(config))
-            }
-            logger.write(Logger.Level.INFO, "Parsed config (in ${stopwatch.elapsed(TimeUnit.MILLISECONDS)} ms)\n")
-            stopwatch.reset().start()
-            val safetyResult: SafetyResult<*, *> =
                 when (strategy) {
                     Strategy.DIRECT -> runDirect(xcfa, config, logger)
                     Strategy.SERVER -> runServer(xcfa, config, logger, parseContext, argdebug)
                     Strategy.SERVER_DEBUG -> runServerDebug(xcfa, config, logger, parseContext)
                     Strategy.PORTFOLIO -> runPortfolio(xcfa, explicitProperty, logger, parseContext, debug,
                         argdebug)
                 }
-            // post verification
-            postVerificationLogging(safetyResult, parseContext)
-            logger.write(Logger.Level.RESULT, safetyResult.toString() + "\n")
-        } else {
-            val transFunc = XcfaMonolithicTransFunc.create(xcfa)
-            registerAllSolverManagers(solverHome, logger)
-            val checker = if (algorithm == Algorithm.KINDUCTION) {
-                KIndChecker(transFunc, Int.MAX_VALUE,
-                    getSolver(concretizerSolver, validateConcretizerSolver).createSolver(),
-                    getSolver(concretizerSolver, validateConcretizerSolver).createSolver(), ExplState::of,
-                    ExprUtils.getVars(transFunc.transExpr))
             } else {
-                ImcChecker<ExplState, StmtAction>(transFunc, Int.MAX_VALUE,
-                    getSolver(concretizerSolver, validateConcretizerSolver).createItpSolver(), ExplState::of,
-                    ExprUtils.getVars(transFunc.transExpr), true)
+                registerAllSolverManagers(solverHome, logger)
+                val checker = if (backend == Backend.KIND) {
+                    val kindConfig = parseKindConfigFromCli()
+                    kindConfig.getKindChecker(xcfa)
+                } else if (backend == Backend.IMC) {
+                    val kindConfig = parseIMCConfigFromCli()
+                    kindConfig.getIMCChecker(xcfa)
+                } else {
+                    error("Backend $backend not supported")
+                }
+                checker.check(null)
             }
-            val result = checker.check(null)
-            logger.write(Logger.Level.RESULT, result.toString() + "\n")
-        }
+        // post verification
+        postVerificationLogging(safetyResult, parseContext)
+        logger.write(Logger.Level.RESULT, safetyResult.toString() + "\n")
     }
 
     private fun runDirect(xcfa: XCFA, config: XcfaCegarConfig, logger: ConsoleLogger) =
@@ -534,7 +516,35 @@ class XcfaCli(private val args: Array<String>) {
         }
     } else ErrorDetection.ERROR_LOCATION
 
-    private fun parseConfigFromCli(parseContext: ParseContext): XcfaCegarConfig {
+    private fun parseIMCConfigFromCli(): XcfaImcConfig {
+        val imcConfig = XcfaImcConfig()
+        try {
+            JCommander.newBuilder().addObject(imcConfig).programName(JAR_NAME).build()
+                .parse(*remainingFlags.toTypedArray())
+        } catch (ex: ParameterException) {
+            println("Invalid parameters, details:")
+            ex.printStackTrace()
+            ex.usage()
+            exitProcess(ExitCodes.INVALID_PARAM.code)
+        }
+        return imcConfig
+    }
+
+    private fun parseKindConfigFromCli(): XcfaKindConfig {
+        val kindConfig = XcfaKindConfig()
+        try {
+            JCommander.newBuilder().addObject(kindConfig).programName(JAR_NAME).build()
+                .parse(*remainingFlags.toTypedArray())
+        } catch (ex: ParameterException) {
+            println("Invalid parameters, details:")
+            ex.printStackTrace()
+            ex.usage()
+            exitProcess(ExitCodes.INVALID_PARAM.code)
+        }
+        return kindConfig
+    }
+
+    private fun parseCEGARConfigFromCli(parseContext: ParseContext): XcfaCegarConfig {
         val cegarConfig = XcfaCegarConfig()
         try {
             JCommander.newBuilder().addObject(cegarConfig).programName(JAR_NAME).build()

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

@@ -0,0 +1,50 @@
+/*
+ *  Copyright 2023 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.xcfa.cli
+
+import com.beust.jcommander.Parameter
+import hu.bme.mit.theta.analysis.algorithm.imc.ImcChecker
+import hu.bme.mit.theta.analysis.expl.ExplState
+import hu.bme.mit.theta.analysis.expr.ExprState
+import hu.bme.mit.theta.analysis.expr.StmtAction
+import hu.bme.mit.theta.core.utils.ExprUtils
+import hu.bme.mit.theta.xcfa.analysis.XcfaMonolithicTransFunc
+import hu.bme.mit.theta.xcfa.model.XCFA
+
+data class XcfaImcConfig(
+    @Parameter(names = ["--imc-solver"], description = "BMC solver name")
+    var imcSolver: String = "Z3",
+    @Parameter(names = ["--validate-imc-solver"],
+        description = "Activates a wrapper, which validates the assertions in the solver in each (SAT) check. Filters some solver issues.")
+    var validateIMCSolver: Boolean = false,
+    @Parameter(names = ["--max-bound"],
+        description = "How many successors to enumerate in a transition. Only relevant to the explicit domain. Use 0 for no limit.")
+    var maxBound: Int = Int.MAX_VALUE,
+) {
+
+    fun getIMCChecker(xcfa: XCFA): ImcChecker<ExprState, StmtAction> {
+        val transFunc = XcfaMonolithicTransFunc.create(xcfa)
+        return ImcChecker<ExprState, StmtAction>(
+            transFunc,
+            maxBound,
+            getSolver(imcSolver, validateIMCSolver).createItpSolver(),
+            ExplState::of,
+            ExprUtils.getVars(transFunc.transExpr),
+            true)
+    }
+
+}