refined var lookup in xcfa prec

ftsrg · Nov 21, 2023 · b1d8c26 · b1d8c26
1 parent c6860e6
commit b1d8c26
Show file tree

Hide file tree

Showing 2 changed files with 18 additions and 8 deletions.
diff --git a/...ojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaPrecRefiner.kt b/...ojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaPrecRefiner.kt
@@ -39,11 +39,21 @@ class XcfaPrecRefiner<S : ExprState, P : Prec, R : Refutation>(refToPrec: Refuta
         Preconditions.checkNotNull(trace)
         Preconditions.checkNotNull<Any>(prec)
         Preconditions.checkNotNull<R>(refutation)
+        val checkForPop = !(trace.states.first() as XcfaState<*>).xcfa!!.isInlined
         var runningPrec: P = prec.p
         for (i in trace.states.indices) {
-            val tempLookup = if (i > 0) getTempLookup(trace.actions[i - 1].edge.label).entries
-                .associateBy({ it.value }) { it.key } else emptyMap()
-            val precFromRef = refToPrec.toPrec(refutation, i).changeVars(tempLookup)
+            val reverseLookup = trace.states[i].processes.values.map {
+                it.varLookup.map {
+                    it.map {
+                        Pair(it.value, it.key)
+                    }
+                }.flatten()
+            }.flatten().toMap()
+            val additionalLookup = if (i > 0) getTempLookup(
+                trace.actions[i - 1].edge.label).entries.associateBy(
+                { it.value }) { it.key } else emptyMap()
+            val varLookup = if (checkForPop) additionalLookup else (reverseLookup + additionalLookup)
+            val precFromRef = refToPrec.toPrec(refutation, i).changeVars(varLookup)
             runningPrec = refToPrec.join(runningPrec, precFromRef)
         }
         return prec.refine(runningPrec)

diff --git a/...s/xcfa/xcfa-analysis/src/test/java/hu/bme/mit/theta/xcfa/analysis/XcfaPredAnalysisTest.kt b/...s/xcfa/xcfa-analysis/src/test/java/hu/bme/mit/theta/xcfa/analysis/XcfaPredAnalysisTest.kt
@@ -91,7 +91,7 @@ class XcfaPredAnalysisTest {
             ItpRefToPredPrec(ExprSplitters.whole()))
 
         val refiner =
-            SingleExprTraceRefiner.create(
+            XcfaSingleExprTraceRefiner.create(
                 ExprTraceBwBinItpChecker.create(BoolExprs.True(), BoolExprs.True(),
                     Z3SolverFactory.getInstance().createItpSolver()),
                 precRefiner, PruneStrategy.FULL,
@@ -137,7 +137,7 @@ class XcfaPredAnalysisTest {
             ItpRefToPredPrec(ExprSplitters.whole()))
 
         val refiner =
-            SingleExprTraceRefiner.create(
+            XcfaSingleExprTraceRefiner.create(
                 ExprTraceBwBinItpChecker.create(BoolExprs.True(), BoolExprs.True(),
                     Z3SolverFactory.getInstance().createItpSolver()),
                 precRefiner, PruneStrategy.FULL,
@@ -183,7 +183,7 @@ class XcfaPredAnalysisTest {
             ItpRefToPredPrec(ExprSplitters.whole()))
 
         val refiner =
-            SingleExprTraceRefiner.create(
+            XcfaSingleExprTraceRefiner.create(
                 ExprTraceBwBinItpChecker.create(BoolExprs.True(), BoolExprs.True(),
                     Z3SolverFactory.getInstance().createItpSolver()),
                 precRefiner, PruneStrategy.FULL,
@@ -229,7 +229,7 @@ class XcfaPredAnalysisTest {
         val atomicNodePruner = AtomicNodePruner<XcfaState<PredState>, XcfaAction>()
 
         val refiner =
-            SingleExprTraceRefiner.create(
+            XcfaSingleExprTraceRefiner.create(
                 ExprTraceBwBinItpChecker.create(BoolExprs.True(), BoolExprs.True(),
                     Z3SolverFactory.getInstance().createItpSolver()),
                 precRefiner, PruneStrategy.FULL, NullLogger.getInstance(),
@@ -274,7 +274,7 @@ class XcfaPredAnalysisTest {
         val precRefiner = XcfaPrecRefiner<PredState, PredPrec, ItpRefutation>(ItpRefToPredPrec(ExprSplitters.whole()))
 
         val refiner =
-            SingleExprTraceRefiner.create(
+            XcfaSingleExprTraceRefiner.create(
                 ExprTraceBwBinItpChecker.create(BoolExprs.True(), BoolExprs.True(),
                     Z3SolverFactory.getInstance().createItpSolver()),
                 precRefiner, PruneStrategy.FULL,