diff --git a/subprojects/xcfa/llvm2xcfa/src/main/java/hu/bme/mit/theta/llvm2xcfa/handlers/states/FunctionState.java b/subprojects/xcfa/llvm2xcfa/src/main/java/hu/bme/mit/theta/llvm2xcfa/handlers/states/FunctionState.java index 9198b2fb51..907865b70a 100644 --- a/subprojects/xcfa/llvm2xcfa/src/main/java/hu/bme/mit/theta/llvm2xcfa/handlers/states/FunctionState.java +++ b/subprojects/xcfa/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, List>> 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/subprojects/xcfa/xcfa-analysis/src/test/java/hu/bme/mit/theta/xcfa/analysis/XcfaExplAnalysisTest.kt b/subprojects/xcfa/xcfa-analysis/src/test/java/hu/bme/mit/theta/xcfa/analysis/XcfaExplAnalysisTest.kt index 769a6d5845..5550cdb22b 100644 --- a/subprojects/xcfa/xcfa-analysis/src/test/java/hu/bme/mit/theta/xcfa/analysis/XcfaExplAnalysisTest.kt +++ b/subprojects/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/subprojects/xcfa/xcfa-analysis/src/test/java/hu/bme/mit/theta/xcfa/analysis/XcfaPredAnalysisTest.kt b/subprojects/xcfa/xcfa-analysis/src/test/java/hu/bme/mit/theta/xcfa/analysis/XcfaPredAnalysisTest.kt index 42d75b94d6..c8caf4ef11 100644 --- a/subprojects/xcfa/xcfa-analysis/src/test/java/hu/bme/mit/theta/xcfa/analysis/XcfaPredAnalysisTest.kt +++ b/subprojects/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 index 303380f610..3be0685c52 100644 --- 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) } \ No newline at end of file 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 677094835e..4f7e8b8f68 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 @@ -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 index dc457d87cd..50017bf05d 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 @@ -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()) \ No newline at end of file +class LitmusPasses : ProcedurePassManager() \ No newline at end of file