accept unreliable safe config option

ftsrg · Oct 18, 2024 · d873017 · d873017
1 parent 58b9204
commit d873017
Show file tree

Hide file tree

Showing 3 changed files with 21 additions and 13 deletions.
diff --git a/...jects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/oc/XcfaOcChecker.kt b/...jects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/oc/XcfaOcChecker.kt
@@ -477,6 +477,6 @@ class XcfaOcChecker(
 
     private fun exit(msg: String): Nothing {
         System.err.println(msg)
-        exitProcess(203)
+        error(203)
     }
 }
diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/ExecuteConfig.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/ExecuteConfig.kt
@@ -176,13 +176,14 @@ fun frontend(config: XcfaConfig<*, *>, logger: Logger, uniqueLogger: Logger): Tr
 
     logger.write(
         Logger.Level.INFO, "Frontend finished: ${xcfa.name}  (in ${
-        stopwatch.elapsed(TimeUnit.MILLISECONDS)
-    } ms)\n"
+            stopwatch.elapsed(TimeUnit.MILLISECONDS)
+        } ms)\n"
     )
 
-//    logger.write(RESULT, "ParsingResult Success\n")
+    logger.write(RESULT, "ParsingResult Success\n")
     logger.write(RESULT,
-        "Alias graph size: ${xcfa.pointsToGraph.size} -> ${xcfa.pointsToGraph.values.map { it.size }.toList()}\n")
+        "Alias graph size: ${xcfa.pointsToGraph.size} -> ${xcfa.pointsToGraph.values.map { it.size }.toList()}\n"
+    )
 
     return Triple(xcfa, mcm, parseContext)
 }
@@ -217,8 +218,8 @@ private fun backend(
                 when {
                     result.isSafe && LoopUnrollPass.FORCE_UNROLL_USED -> { // cannot report safe if force unroll was used
                         logger.write(RESULT, "Incomplete loop unroll used: safe result is unreliable.\n")
-                        //SafetyResult.unknown<EmptyWitness, EmptyCex>() // for comparison with BMC tools
-                        result
+                        if (config.outputConfig.acceptUnreliableSafe) result // for comparison with BMC tools
+                        else SafetyResult.unknown<EmptyWitness, EmptyCex>()
                     }
 
                     else -> result
@@ -227,8 +228,8 @@ private fun backend(
 
             logger.write(
                 Logger.Level.INFO, "Backend finished (in ${
-                stopwatch.elapsed(TimeUnit.MILLISECONDS)
-            } ms)\n"
+                    stopwatch.elapsed(TimeUnit.MILLISECONDS)
+                } ms)\n"
             )
 
             logger.write(RESULT, result.toString() + "\n")
@@ -332,8 +333,10 @@ private fun postVerificationLogging(
                     traceFile.writeText(GraphvizWriter.getInstance().writeString(traceG))
 
                     val sequenceFile = File(resultFolder, "trace.plantuml")
-                    writeSequenceTrace(sequenceFile,
-                        safetyResult.asUnsafe().cex as Trace<XcfaState<ExplState>, XcfaAction>) { (_, act) ->
+                    writeSequenceTrace(
+                        sequenceFile,
+                        safetyResult.asUnsafe().cex as Trace<XcfaState<ExplState>, XcfaAction>
+                    ) { (_, act) ->
                         act.label.getFlatLabels().map(XcfaLabel::toString)
                     }
 
@@ -364,8 +367,10 @@ private fun postVerificationLogging(
     }
 }
 
-private fun writeSequenceTrace(sequenceFile: File, trace: Trace<XcfaState<ExplState>, XcfaAction>,
-    printer: (Pair<XcfaState<ExplState>, XcfaAction>) -> List<String>) {
+private fun writeSequenceTrace(
+    sequenceFile: File, trace: Trace<XcfaState<ExplState>, XcfaAction>,
+    printer: (Pair<XcfaState<ExplState>, XcfaAction>) -> List<String>
+) {
     sequenceFile.writeText("@startuml\n")
     var maxWidth = 0
     trace.actions.forEachIndexed { i, it ->

diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/params/XcfaConfig.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/params/XcfaConfig.kt
@@ -355,6 +355,9 @@ data class OutputConfig(
     @Parameter(names = ["--output-directory"], description = "Specify the directory where the result files are stored")
     var resultFolder: File = Paths.get("./").toFile(),
 
+    @Parameter(names = ["--accept-unreliable-safe"], description = "Accept safe results even with unsafe loop unroll")
+    var acceptUnreliableSafe: Boolean = false,
+
     val cOutputConfig: COutputConfig = COutputConfig(),
     val xcfaOutputConfig: XcfaOutputConfig = XcfaOutputConfig(),
     val chcOutputConfig: ChcOutputConfig = ChcOutputConfig(),