fixed tests

ftsrg · Nov 1, 2023 · 5163050 · 5163050
1 parent a37364b
commit 5163050
Show file tree

Hide file tree

Showing 6 changed files with 21 additions and 8 deletions.
diff --git a/...cfa/llvm2xcfa/src/main/java/hu/bme/mit/theta/llvm2xcfa/handlers/states/FunctionState.java b/...cfa/llvm2xcfa/src/main/java/hu/bme/mit/theta/llvm2xcfa/handlers/states/FunctionState.java
@@ -58,7 +58,7 @@ public class FunctionState {
     public FunctionState(GlobalState globalState, Tuple3<String, Optional<String>, List<Tuple2<String, String>>> function) {
         this.globalState = globalState;
         this.function = function;
-        procedureBuilder = new XcfaProcedureBuilder(function.get1(), new ProcedurePassManager(List.of()));
+        procedureBuilder = new XcfaProcedureBuilder(function.get1(), new ProcedurePassManager());
 //        procedureBuilder.setName(function.get1());
         localVars = new HashMap<>();
         params = new HashSet<>();

diff --git a/...s/xcfa/xcfa-analysis/src/test/java/hu/bme/mit/theta/xcfa/analysis/XcfaExplAnalysisTest.kt b/...s/xcfa/xcfa-analysis/src/test/java/hu/bme/mit/theta/xcfa/analysis/XcfaExplAnalysisTest.kt
@@ -32,6 +32,9 @@ import hu.bme.mit.theta.common.logging.NullLogger
 import hu.bme.mit.theta.core.type.booltype.BoolExprs
 import hu.bme.mit.theta.frontend.ParseContext
 import hu.bme.mit.theta.solver.z3.Z3SolverFactory
+import hu.bme.mit.theta.xcfa.analysis.coi.ConeOfInfluence
+import hu.bme.mit.theta.xcfa.analysis.coi.XcfaCoiMultiThread
+import hu.bme.mit.theta.xcfa.analysis.coi.XcfaCoiSingleThread
 import hu.bme.mit.theta.xcfa.analysis.por.*
 import org.junit.jupiter.api.Assertions
 import org.junit.jupiter.params.ParameterizedTest
@@ -65,6 +68,7 @@ class XcfaExplAnalysisTest {
         println("Testing NOPOR on $filepath...")
         val stream = javaClass.getResourceAsStream(filepath)
         val xcfa = getXcfaFromC(stream!!, ParseContext(), false, false).first
+        ConeOfInfluence = XcfaCoiMultiThread(xcfa)
 
         val analysis = ExplXcfaAnalysis(
             xcfa,
@@ -108,6 +112,7 @@ class XcfaExplAnalysisTest {
         println("Testing SPOR on $filepath...")
         val stream = javaClass.getResourceAsStream(filepath)
         val xcfa = getXcfaFromC(stream!!, ParseContext(), false, false).first
+        ConeOfInfluence = XcfaCoiMultiThread(xcfa)
 
         val analysis = ExplXcfaAnalysis(
             xcfa,
@@ -152,6 +157,7 @@ class XcfaExplAnalysisTest {
         println("Testing DPOR on $filepath...")
         val stream = javaClass.getResourceAsStream(filepath)
         val xcfa = getXcfaFromC(stream!!, ParseContext(), false, false).first
+        ConeOfInfluence = XcfaCoiMultiThread(xcfa)
 
         val analysis = ExplXcfaAnalysis(
             xcfa,
@@ -194,6 +200,7 @@ class XcfaExplAnalysisTest {
         println("Testing AASPOR on $filepath...")
         val stream = javaClass.getResourceAsStream(filepath)
         val xcfa = getXcfaFromC(stream!!, ParseContext(), false, false).first
+        ConeOfInfluence = XcfaCoiMultiThread(xcfa)
 
         val analysis = ExplXcfaAnalysis(
             xcfa,
@@ -239,6 +246,7 @@ class XcfaExplAnalysisTest {
         println("Testing AADPOR on $filepath...")
         val stream = javaClass.getResourceAsStream(filepath)
         val xcfa = getXcfaFromC(stream!!, ParseContext(), false, false).first
+        ConeOfInfluence = XcfaCoiMultiThread(xcfa)
 
         val analysis = ExplXcfaAnalysis(
             xcfa,

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
@@ -32,6 +32,8 @@ import hu.bme.mit.theta.common.logging.NullLogger
 import hu.bme.mit.theta.core.type.booltype.BoolExprs
 import hu.bme.mit.theta.frontend.ParseContext
 import hu.bme.mit.theta.solver.z3.Z3SolverFactory
+import hu.bme.mit.theta.xcfa.analysis.coi.ConeOfInfluence
+import hu.bme.mit.theta.xcfa.analysis.coi.XcfaCoiMultiThread
 import hu.bme.mit.theta.xcfa.analysis.por.*
 import org.junit.jupiter.api.Assertions
 import org.junit.jupiter.params.ParameterizedTest
@@ -65,6 +67,7 @@ class XcfaPredAnalysisTest {
         println("Testing NOPOR on $filepath...")
         val stream = javaClass.getResourceAsStream(filepath)
         val xcfa = getXcfaFromC(stream!!, ParseContext(), false, false).first
+        ConeOfInfluence = XcfaCoiMultiThread(xcfa)
 
         val solver = Z3SolverFactory.getInstance().createSolver()
         val analysis = PredXcfaAnalysis(
@@ -110,6 +113,7 @@ class XcfaPredAnalysisTest {
         println("Testing SPOR on $filepath...")
         val stream = javaClass.getResourceAsStream(filepath)
         val xcfa = getXcfaFromC(stream!!, ParseContext(), false, false).first
+        ConeOfInfluence = XcfaCoiMultiThread(xcfa)
 
         val solver = Z3SolverFactory.getInstance().createSolver()
         val analysis = PredXcfaAnalysis(
@@ -156,6 +160,7 @@ class XcfaPredAnalysisTest {
         println("Testing DPOR on $filepath...")
         val stream = javaClass.getResourceAsStream(filepath)
         val xcfa = getXcfaFromC(stream!!, ParseContext(), false, false).first
+        ConeOfInfluence = XcfaCoiMultiThread(xcfa)
 
         val solver = Z3SolverFactory.getInstance().createSolver()
         val analysis = PredXcfaAnalysis(
@@ -200,6 +205,7 @@ class XcfaPredAnalysisTest {
         println("Testing AASPOR on $filepath...")
         val stream = javaClass.getResourceAsStream(filepath)
         val xcfa = getXcfaFromC(stream!!, ParseContext(), false, false).first
+        ConeOfInfluence = XcfaCoiMultiThread(xcfa)
 
         val solver = Z3SolverFactory.getInstance().createSolver()
         val analysis = PredXcfaAnalysis(
@@ -246,6 +252,7 @@ class XcfaPredAnalysisTest {
         println("Testing AADPOR on $filepath...")
         val stream = javaClass.getResourceAsStream(filepath)
         val xcfa = getXcfaFromC(stream!!, ParseContext(), false, false).first
+        ConeOfInfluence = XcfaCoiMultiThread(xcfa)
 
         val solver = Z3SolverFactory.getInstance().createSolver()
         val analysis = PredXcfaAnalysis(

diff --git a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/model/Dsl.kt b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/model/Dsl.kt
@@ -312,5 +312,5 @@ fun XcfaBuilder.procedure(name: String, passManager: ProcedurePassManager,
 
 fun XcfaBuilder.procedure(name: String,
     lambda: XcfaProcedureBuilderContext.() -> Unit): XcfaProcedureBuilderContext {
-    return procedure(name, ProcedurePassManager(emptyList()), lambda)
+    return procedure(name, ProcedurePassManager(), lambda)
 }
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
@@ -278,9 +278,7 @@ class LbePass(val parseContext: ParseContext) : ProcedurePass {
         if (location.outgoingEdges.size != 1) return false
         val outEdge = location.outgoingEdges.first()
         if (
-            location.incomingEdges.any { edge ->
-                edge.getFlatLabels().any { it is InvokeLabel || (it is StmtLabel && it.stmt is AssumeStmt) }
-            }
+            location.incomingEdges.any { edge -> edge.getFlatLabels().any { it is InvokeLabel } }
             || location.outgoingEdges.any { edge -> edge.getFlatLabels().any { it is InvokeLabel } }
             || (level == LbeLevel.LBE_LOCAL && !atomicPhase && isNotLocal(outEdge))
         ) {

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
@@ -61,7 +61,7 @@ class CPasses(checkOverflow: Boolean, parseContext: ParseContext) : ProcedurePas
     )
 )
 
-class ChcPasses : ProcedurePassManager(listOf(/*
+class ChcPasses : ProcedurePassManager(/*listOf(
         // formatting
         NormalizePass(),
         DeterministicPass(),
@@ -88,6 +88,6 @@ class ChcPasses : ProcedurePassManager(listOf(/*
 //        HavocPromotionAndRange(),
         // Final cleanup
         UnusedVarPass(),
-*/))
+)*/)
 
-class LitmusPasses : ProcedurePassManager(emptyList())
+class LitmusPasses : ProcedurePassManager()