Bug fixes

ftsrg · Nov 13, 2023 · 4cecd1b · 4cecd1b
1 parent d8328f4
commit 4cecd1b
Show file tree

Hide file tree

Showing 7 changed files with 46 additions and 17 deletions.
diff --git a/.gitignore b/.gitignore
@@ -19,3 +19,4 @@ dest/
 
 # Other
 wdl-output.json
+witness.graphml
diff --git a/...mmon/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/debug/ARGWebDebugger.java b/...mmon/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/debug/ARGWebDebugger.java
@@ -33,7 +33,7 @@
  */
 
 public final class ARGWebDebugger {
-    private static final boolean debug = false;
+    public static boolean on = false;
     private static final Integer PORT = 8080;
 
     private static SocketIOServer server;
@@ -49,7 +49,7 @@ private ARGWebDebugger() {
     }
 
     private static void startServer() {
-        if (!debug) return;
+        if (!on) return;
         Configuration config = new Configuration();
         config.setPort(PORT);
 
@@ -107,7 +107,7 @@ private static <A extends Action> String nodeToString(ArgNode<? extends State, ?
     }
 
     public static void create(ArgNode<? extends State, ? extends Action> initNode) {
-        if (!debug) {
+        if (!on) {
             return;
         }
         replayLog.clear();
@@ -118,15 +118,15 @@ public static void create(ArgNode<? extends State, ? extends Action> initNode) {
     public static <A extends Action> void add(ArgNode<? extends State, ? extends Action> parent,
                                               A action,
                                               ArgNode<? extends State, ? extends Action> child) {
-        if (!debug) {
+        if (!on) {
             return;
         }
         send("{\"method\": \"add\", \"parent\": " + parent.getId() + ", \"child\": " + nodeToString(child, action) + "}", true);
         waitUntil();
     }
 
     public static <A extends Action> void remove(ArgEdge<? extends State, ? extends Action> edge) {
-        if (!debug) {
+        if (!on) {
             return;
         }
         send("{\"method\": \"delete\", \"parent\": " + edge.getSource().getId() + ", \"child\": " + edge.getTarget().getId() + "}", true);

diff --git a/...n/java/hu/bme/mit/theta/frontend/transformation/grammar/expression/ExpressionVisitor.java b/...n/java/hu/bme/mit/theta/frontend/transformation/grammar/expression/ExpressionVisitor.java
@@ -393,6 +393,8 @@ public Expr<?> visitMultiplicativeExpression(CParser.MultiplicativeExpressionCon
                     case "%":
                         if (leftExpr.getType() instanceof IntType && rightExpr.getType() instanceof IntType) {
                             expr = createIntMod(leftExpr, rightExpr);
+                        } else if (leftExpr.getType() instanceof BvType && rightExpr.getType() instanceof BvType) {
+                            expr = AbstractExprs.Rem(leftExpr, rightExpr);
                         } else {
                             expr = AbstractExprs.Mod(leftExpr, rightExpr);
                         }

diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/XcfaCegarConfig.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/XcfaCegarConfig.kt
@@ -221,7 +221,7 @@ data class XcfaCegarConfig(
         ProcessHandle.current().info().command().orElse("java")
 
     fun checkInProcess(xcfa: XCFA, smtHome: String, writeWitness: Boolean, sourceFileName: String,
-        logger: Logger, parseContext: ParseContext): () -> SafetyResult<*, *> {
+        logger: Logger, parseContext: ParseContext, argdebug: Boolean): () -> SafetyResult<*, *> {
         val pb = NuProcessBuilder(listOf(
             getJavaExecutable(),
             "-cp",
@@ -233,8 +233,9 @@ data class XcfaCegarConfig(
             "" + !writeWitness,
             "--input",
             sourceFileName,
-            "--gzip"
-        ))
+            "--gzip",
+            if (argdebug) "--arg-debug" else null,
+        ).filterNotNull())
         val processHandler = ProcessHandler(logger)
         pb.setProcessListener(processHandler)
         val process: NuProcess = pb.start()

diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/XcfaCegarServer.java b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/XcfaCegarServer.java
@@ -22,13 +22,17 @@
 import com.google.common.base.Stopwatch;
 import com.google.gson.Gson;
 import hu.bme.mit.theta.analysis.algorithm.SafetyResult;
+import hu.bme.mit.theta.analysis.algorithm.debug.ARGWebDebugger;
 import hu.bme.mit.theta.analysis.expr.ExprAction;
 import hu.bme.mit.theta.analysis.expr.ExprState;
 import hu.bme.mit.theta.common.logging.ConsoleLabelledLogger;
 import hu.bme.mit.theta.common.logging.Logger;
 import hu.bme.mit.theta.common.logging.Logger.Level;
 import hu.bme.mit.theta.frontend.ParseContext;
 import hu.bme.mit.theta.solver.smtlib.SmtLibSolverManager;
+import hu.bme.mit.theta.xcfa.analysis.coi.XcfaCoiKt;
+import hu.bme.mit.theta.xcfa.analysis.coi.XcfaCoiMultiThread;
+import hu.bme.mit.theta.xcfa.analysis.coi.XcfaCoiSingleThread;
 import hu.bme.mit.theta.xcfa.cli.utils.XcfaWitnessWriter;
 import hu.bme.mit.theta.xcfa.model.XCFA;
 
@@ -79,6 +83,11 @@ class XcfaCegarServer {
     @Parameter(names = "--debug", description = "Debug mode (will not create a socket)")
     Boolean debug = false;
 
+
+    @Parameter(names = "--arg-debug", description = "ARG debug mode (use the web-based debugger for ARG visualization)")
+    Boolean argdebug = false;
+
+
     @Parameter(names = "--gzip", description = "Expect stdin to contain gzipped text")
     Boolean gzip = false;
 
@@ -92,6 +101,8 @@ private void run(String[] args) {
             System.exit(ExitCodes.INVALID_PARAM.getCode());
         }
 
+        if (argdebug) ARGWebDebugger.on = true;
+
         final Logger logger = new ConsoleLabelledLogger();
 
         exitOnError(true, debug, () -> {
@@ -159,6 +170,10 @@ private void run(String[] args) {
                             System.err.println("Erroneous parsecontext, see file " + tempFile.getAbsolutePath());
                             throw e;
                         }
+                        XcfaCoiKt.ConeOfInfluence =
+                                (parseContext.getMultiThreading()) ?
+                                        new XcfaCoiMultiThread(xcfa) :
+                                        new XcfaCoiSingleThread(xcfa);
 
                         logger.write(Logger.Level.INFO, "Parsed parsecontext.\n");
 

diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/XcfaCli.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/XcfaCli.kt
@@ -24,6 +24,7 @@ import com.google.gson.GsonBuilder
 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.expl.ExplState
 import hu.bme.mit.theta.analysis.utils.ArgVisualizer
 import hu.bme.mit.theta.analysis.utils.TraceVisualizer
@@ -112,6 +113,10 @@ class XcfaCli(private val args: Array<String>) {
     @Parameter(names = ["--debug"], description = "Debug mode (not exiting when encountering an exception)")
     var debug: Boolean = false
 
+    @Parameter(names = ["--arg-debug"],
+        description = "ARG debug mode (use the web-based debugger for ARG visualization)")
+    var argdebug: Boolean = false
+
     //////////// debug options ////////////
     @Parameter(names = ["--stacktrace"],
         description = "Print full stack trace in case of exception")
@@ -205,6 +210,7 @@ class XcfaCli(private val args: Array<String>) {
             WebDebuggerLogger.getInstance().setTitle(input?.name)
         }
         LoopUnrollPass.UNROLL_LIMIT = loopUnroll
+        ARGWebDebugger.on = argdebug
 
         logger.write(Logger.Level.INFO, "Parsing the input $input as $inputType\n")
         val parseContext = ParseContext()
@@ -237,9 +243,9 @@ class XcfaCli(private val args: Array<String>) {
         val safetyResult: SafetyResult<*, *> =
             when (strategy) {
                 Strategy.DIRECT -> runDirect(xcfa, config, logger)
-                Strategy.SERVER -> runServer(xcfa, config, logger, parseContext)
+                Strategy.SERVER -> runServer(xcfa, config, logger, parseContext, argdebug)
                 Strategy.SERVER_DEBUG -> runServerDebug(xcfa, config, logger, parseContext)
-                Strategy.PORTFOLIO -> runPortfolio(xcfa, explicitProperty, logger, parseContext, debug)
+                Strategy.PORTFOLIO -> runPortfolio(xcfa, explicitProperty, logger, parseContext, debug, argdebug)
             }
         // post verification
         postVerificationLogging(safetyResult, parseContext)
@@ -250,9 +256,9 @@ class XcfaCli(private val args: Array<String>) {
         exitOnError(stacktrace, debug) { config.check(xcfa, logger) }
 
     private fun runServer(xcfa: XCFA, config: XcfaCegarConfig,
-        logger: ConsoleLogger, parseContext: ParseContext): SafetyResult<*, *> {
+        logger: ConsoleLogger, parseContext: ParseContext, argdebug: Boolean): SafetyResult<*, *> {
         val safetyResultSupplier = config.checkInProcess(xcfa, solverHome, true,
-            input!!.absolutePath, logger, parseContext)
+            input!!.absolutePath, logger, parseContext, argdebug)
         return try {
             safetyResultSupplier()
         } catch (e: ErrorCodeException) {
@@ -272,10 +278,11 @@ class XcfaCli(private val args: Array<String>) {
     }
 
     private fun runPortfolio(xcfa: XCFA, explicitProperty: ErrorDetection,
-        logger: ConsoleLogger, parseContext: ParseContext, debug: Boolean = false): SafetyResult<*, *> {
+        logger: ConsoleLogger, parseContext: ParseContext, debug: Boolean = false,
+        argdebug: Boolean): SafetyResult<*, *> {
         return try {
             val portfolioResult = if (File(portfolio).exists()) {
-                val portfolioDescriptor = portfolio!!.lowercase() + ".kts"
+                val portfolioDescriptor = portfolio!!
                 val kotlinEngine: ScriptEngine = ScriptEngineManager().getEngineByExtension("kts")
                 val bindings: Bindings = kotlinEngine.createBindings()
                 bindings["xcfa"] = xcfa
@@ -288,6 +295,7 @@ class XcfaCli(private val args: Array<String>) {
                     multithreaded = parseContext.multiThreading,
                     arithmetic = parseContext.bitwiseOption,
                 )
+                bindings["argdebug"] = argdebug
 
                 kotlinEngine as Compilable
                 val stopwatch = Stopwatch.createStarted()
@@ -308,7 +316,7 @@ class XcfaCli(private val args: Array<String>) {
                 complexPortfolio(xcfa, input!!.absolutePath, logger, solverHome, VerificationTraits(
                     multithreaded = parseContext.multiThreading,
                     arithmetic = parseContext.bitwiseOption,
-                ), explicitProperty, parseContext)
+                ), explicitProperty, parseContext, argdebug)
             } else throw Exception("No known portfolio $portfolio")
 
             concretizerSolver = portfolioResult.first.refinementSolver

diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/portfolio/complex.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/portfolio/complex.kt
@@ -27,11 +27,13 @@ import hu.bme.mit.theta.xcfa.model.XCFA
 
 fun complexPortfolio(xcfaTyped: XCFA, cFileNameTyped: String, loggerTyped: Logger, smtHomeTyped: String,
     traitsTyped: VerificationTraits, propertyTyped: ErrorDetection,
-    parseContextTyped: ParseContext): Pair<XcfaCegarConfig, SafetyResult<*, *>> {
+    parseContextTyped: ParseContext,
+    argdebug: Boolean): Pair<XcfaCegarConfig, SafetyResult<*, *>> {
 
     val checker = { p: Boolean, config: XcfaCegarConfig ->
         if (p)
-            config.checkInProcess(xcfaTyped, smtHomeTyped, true, cFileNameTyped, loggerTyped, parseContextTyped)()
+            config.checkInProcess(xcfaTyped, smtHomeTyped, true, cFileNameTyped, loggerTyped, parseContextTyped,
+                argdebug)()
         else config.check(xcfaTyped, loggerTyped)
     }
Original file line number	Diff line number	Diff line change
Expand Up		@@ -19,3 +19,4 @@ dest/

		# Other
		wdl-output.json
		witness.graphml