Some fixes based on bechmarking

ftsrg · Nov 17, 2023 · dc427f6 · dc427f6
1 parent f39ba00
commit dc427f6
Show file tree

Hide file tree

Showing 4 changed files with 7 additions and 10 deletions.
diff --git a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/HavocPromotionAndRange.kt b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/HavocPromotionAndRange.kt
@@ -38,21 +38,13 @@ class HavocPromotionAndRange(val parseContext: ParseContext) : ProcedurePass {
 
     override fun run(builder: XcfaProcedureBuilder): XcfaProcedureBuilder {
         checkNotNull(builder.metaData["deterministic"])
-
-//        val varEdgeLut = LinkedHashMap<VarDecl<*>, MutableList<XcfaEdge>>()
-//        builder.getEdges().forEach { it.label.collectVars().forEach { v ->
-//            varEdgeLut.putIfAbsent(v, ArrayList())
-//            varEdgeLut[v]!!.add(it)
-//        } }
-
         val edges = LinkedHashSet(builder.getEdges())
         for (edge in edges) {
             var candidates = (edge.label as SequenceLabel).labels
                 .mapIndexed { index, it -> Pair(index, it) }
                 .filter {
                     it.second is StmtLabel &&
-                        (it.second as StmtLabel).stmt is HavocStmt<*> //&&
-//                        varEdgeLut[((it.second as StmtLabel).stmt as HavocStmt<*>).varDecl]!!.size == 1
+                        (it.second as StmtLabel).stmt is HavocStmt<*>
                 }
             if (candidates.isNotEmpty()) {
                 val labelEdgeLut = LinkedHashMap<VarDecl<*>, MutableList<XcfaLabel>>()

diff --git a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/LbePass.kt b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/LbePass.kt
@@ -98,7 +98,7 @@ class LbePass(val parseContext: ParseContext) : ProcedurePass {
     override fun run(builder: XcfaProcedureBuilder): XcfaProcedureBuilder {
         if (level == LbeLevel.NO_LBE) return builder
 
-        if (level == LbeLevel.LBE_SEQ || level == LbeLevel.LBE_FULL && parseContext.multiThreading) {
+        if ((level == LbeLevel.LBE_SEQ || level == LbeLevel.LBE_FULL) && parseContext.multiThreading) {
             level = LbeLevel.LBE_LOCAL
         }
 

diff --git a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/NormalizePass.kt b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/NormalizePass.kt
@@ -16,6 +16,8 @@
 
 package hu.bme.mit.theta.xcfa.passes
 
+import hu.bme.mit.theta.core.stmt.AssumeStmt
+import hu.bme.mit.theta.core.type.booltype.BoolExprs.True
 import hu.bme.mit.theta.frontend.ParseContext
 import hu.bme.mit.theta.xcfa.model.*
 
@@ -63,6 +65,8 @@ class NormalizePass(val parseContext: ParseContext) : ProcedurePass {
             }
 
             is NopLabel -> {}
+            is StmtLabel -> if (!(label.stmt is AssumeStmt && label.stmt.cond.equals(
+                    True()))) collector.forEach { it.add(label) }
             else -> collector.forEach { it.add(label) }
         }
     }

diff --git a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/ProcedurePassManager.kt b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/ProcedurePassManager.kt
@@ -53,6 +53,7 @@ class CPasses(checkOverflow: Boolean, parseContext: ParseContext, uniqueWarningL
     listOf(
         // handling remaining function calls
         NondetFunctionPass(parseContext),
+        HavocPromotionAndRange(parseContext),
         LbePass(parseContext),
         NormalizePass(parseContext), // needed after lbe, TODO
         DeterministicPass(parseContext), // needed after lbe, TODO