From dc427f65d471a2b5afa17ee3f1793cbc8e0abbc4 Mon Sep 17 00:00:00 2001
From: Levente Bajczi <bajczilevi@gmail.com>
Date: Fri, 17 Nov 2023 15:47:56 +0100
Subject: [PATCH] Some fixes based on bechmarking

---
 .../mit/theta/xcfa/passes/HavocPromotionAndRange.kt    | 10 +---------
 .../main/java/hu/bme/mit/theta/xcfa/passes/LbePass.kt  |  2 +-
 .../java/hu/bme/mit/theta/xcfa/passes/NormalizePass.kt |  4 ++++
 .../bme/mit/theta/xcfa/passes/ProcedurePassManager.kt  |  1 +
 4 files changed, 7 insertions(+), 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
index 707fbd4db6..e05160d6fe 100644
--- 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
index 64e5a66931..8dc4983876 100644
--- 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
index dcb7426944..78dedb0a00 100644
--- 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
index 2ab650f279..b175b98fe0 100644
--- 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