diff --git a/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/grammar/expression/ExpressionVisitor.java b/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/grammar/expression/ExpressionVisitor.java index 90dd48cbce..d898745256 100644 --- a/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/grammar/expression/ExpressionVisitor.java +++ b/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/grammar/expression/ExpressionVisitor.java @@ -388,6 +388,7 @@ public Expr visitMultiplicativeExpression(CParser.MultiplicativeExpressionCon /** * Conversion from C (/) semantics to solver (div) semantics. + * * @param a dividend * @param b divisor * @return expression representing C division semantics with solver operations @@ -395,21 +396,22 @@ public Expr visitMultiplicativeExpression(CParser.MultiplicativeExpressionCon private Expr createIntDiv(Expr a, Expr b) { DivExpr aDivB = Div(a, b); return Ite(Geq(a, Int(0)), // if (a >= 0) - aDivB, // a div b - // else - Ite(Neq(Mod(a, b), Int(0)), // if (a mod b != 0) - Ite(Geq(b, Int(0)), // if (b >= 0) - Add(aDivB, Int(1)), // a div b + 1 - // else - Sub(aDivB, Int(1)) // a div b - 1 - ), // else - aDivB // a div b - ) + aDivB, // a div b + // else + Ite(Neq(Mod(a, b), Int(0)), // if (a mod b != 0) + Ite(Geq(b, Int(0)), // if (b >= 0) + Add(aDivB, Int(1)), // a div b + 1 + // else + Sub(aDivB, Int(1)) // a div b - 1 + ), // else + aDivB // a div b + ) ); } /** * Conversion from C (%) semantics to solver (mod) semantics. + * * @param a dividend * @param b divisor * @return expression representing C modulo semantics with solver operations @@ -417,12 +419,12 @@ private Expr createIntDiv(Expr a, Expr b) { private Expr createIntMod(Expr a, Expr b) { ModExpr aModB = Mod(a, b); return Ite(Geq(a, Int(0)), // if (a >= 0) - aModB, // a mod b - // else - Ite(Geq(b, Int(0)), // if (b >= 0) - Sub(aModB, b), // a mod b - b - Add(aModB, b) // a mod b + b - ) + aModB, // a mod b + // else + Ite(Geq(b, Int(0)), // if (b >= 0) + Sub(aModB, b), // a mod b - b + Add(aModB, b) // a mod b + b + ) ); } diff --git a/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/grammar/expression/UnsupportedInitializer.java b/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/grammar/expression/UnsupportedInitializer.java new file mode 100644 index 0000000000..042df61d24 --- /dev/null +++ b/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/grammar/expression/UnsupportedInitializer.java @@ -0,0 +1,42 @@ +/* + * Copyright 2023 Budapest University of Technology and Economics + * + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ + +package hu.bme.mit.theta.frontend.transformation.grammar.expression; + +import hu.bme.mit.theta.core.model.Valuation; +import hu.bme.mit.theta.core.type.LitExpr; +import hu.bme.mit.theta.core.type.NullaryExpr; +import hu.bme.mit.theta.core.type.inttype.IntType; + +import static hu.bme.mit.theta.core.type.inttype.IntExprs.Int; + +public class UnsupportedInitializer extends NullaryExpr { + + @Override + public IntType getType() { + return Int(); + } + + @Override + public LitExpr eval(Valuation val) { + throw new UnsupportedOperationException("UnsupportedInitializer expressions are not supported."); + } + + @Override + public String toString() { + return "UnsupportedInitializer"; + } +} diff --git a/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/grammar/type/DeclarationVisitor.java b/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/grammar/type/DeclarationVisitor.java index 4dd23f9ad9..7442159bbe 100644 --- a/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/grammar/type/DeclarationVisitor.java +++ b/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/grammar/type/DeclarationVisitor.java @@ -19,9 +19,11 @@ import hu.bme.mit.theta.c.frontend.dsl.gen.CBaseVisitor; import hu.bme.mit.theta.c.frontend.dsl.gen.CParser; import hu.bme.mit.theta.frontend.ParseContext; +import hu.bme.mit.theta.frontend.transformation.grammar.expression.UnsupportedInitializer; import hu.bme.mit.theta.frontend.transformation.grammar.function.FunctionVisitor; import hu.bme.mit.theta.frontend.transformation.grammar.preprocess.TypedefVisitor; import hu.bme.mit.theta.frontend.transformation.model.declaration.CDeclaration; +import hu.bme.mit.theta.frontend.transformation.model.statements.CExpr; import hu.bme.mit.theta.frontend.transformation.model.statements.CInitializerList; import hu.bme.mit.theta.frontend.transformation.model.statements.CStatement; import hu.bme.mit.theta.frontend.transformation.model.types.simple.CSimpleType; @@ -81,13 +83,17 @@ public List getDeclarations(CParser.DeclarationSpecifiersContext d "Initializer list designators not yet implemented!"); CInitializerList cInitializerList = new CInitializerList( cSimpleType.getActualType(), parseContext); - for (CParser.InitializerContext initializer : context.initializer() - .initializerList().initializers) { - CStatement expr = initializer.assignmentExpression() - .accept(functionVisitor); - cInitializerList.addStatement(null /* TODO: add designator */, expr); + try { + for (CParser.InitializerContext initializer : context.initializer() + .initializerList().initializers) { + CStatement expr = initializer.assignmentExpression().accept(functionVisitor); + cInitializerList.addStatement(null /* TODO: add designator */, expr); + } + initializerExpression = cInitializerList; + } catch (NullPointerException e) { + initializerExpression = new CExpr(new UnsupportedInitializer(), parseContext); + parseContext.getMetadata().create(initializerExpression.getExpression(), "cType", cSimpleType); } - initializerExpression = cInitializerList; } else { initializerExpression = context.initializer().assignmentExpression() .accept(functionVisitor); 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/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaAnalysis.kt b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaAnalysis.kt index 29f55d2bdb..3abddfbfaf 100644 --- a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaAnalysis.kt +++ b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaAnalysis.kt @@ -37,14 +37,12 @@ import hu.bme.mit.theta.core.stmt.Stmts import hu.bme.mit.theta.core.type.booltype.BoolExprs.True import hu.bme.mit.theta.core.utils.TypeUtils import hu.bme.mit.theta.solver.Solver +import hu.bme.mit.theta.xcfa.* import hu.bme.mit.theta.xcfa.analysis.XcfaProcessState.Companion.createLookup import hu.bme.mit.theta.xcfa.analysis.coi.ConeOfInfluence -import hu.bme.mit.theta.xcfa.getFlatLabels -import hu.bme.mit.theta.xcfa.getGlobalVars import hu.bme.mit.theta.xcfa.isWritten import hu.bme.mit.theta.xcfa.model.* import hu.bme.mit.theta.xcfa.passes.changeVars -import hu.bme.mit.theta.xcfa.startsAtomic import java.util.* import java.util.function.Predicate @@ -153,15 +151,16 @@ fun getXcfaErrorPredicate( if (process1.key != process2.key) for (edge1 in process1.value.locs.peek().outgoingEdges) for (edge2 in process2.value.locs.peek().outgoingEdges) { - val globalVars1 = edge1.getGlobalVars(xcfa) - val globalVars2 = edge2.getGlobalVars(xcfa) - val isAtomic1 = edge1.startsAtomic() - val isAtomic2 = edge2.startsAtomic() - if (!isAtomic1 || !isAtomic2) { - val intersection = globalVars1.keys intersect globalVars2.keys - if (intersection.any { globalVars1[it].isWritten || globalVars2[it].isWritten }) - return@Predicate true - } + val mutexes1 = s.mutexes.filterValues { it == process1.key }.keys + val mutexes2 = s.mutexes.filterValues { it == process2.key }.keys + val globalVars1 = edge1.getGlobalVarsWithNeededMutexes(xcfa, mutexes1) + val globalVars2 = edge2.getGlobalVarsWithNeededMutexes(xcfa, mutexes2) + for (v1 in globalVars1) + for (v2 in globalVars2) + if (v1.varDecl == v2.varDecl) + if (v1.access.isWritten || v2.access.isWritten) + if ((v1.mutexes intersect v2.mutexes).isEmpty()) + return@Predicate true } false } diff --git a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/coi/XcfaCoi.kt b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/coi/XcfaCoi.kt index fc38995493..6b3238eca4 100644 --- a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/coi/XcfaCoi.kt +++ b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/coi/XcfaCoi.kt @@ -1,3 +1,19 @@ +/* + * Copyright 2023 Budapest University of Technology and Economics + * + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ + package hu.bme.mit.theta.xcfa.analysis.coi import hu.bme.mit.theta.analysis.LTS @@ -88,7 +104,7 @@ abstract class XcfaCoi(protected val xcfa: XCFA) { protected fun findDirectObservers(edge: XcfaEdge, prec: Prec) { val precVars = prec.usedVars - val writtenVars = edge.getVars().filter { it.value.isWritten && it.key in precVars } + val writtenVars = edge.collectVarsWithAccessType().filter { it.value.isWritten && it.key in precVars } if (writtenVars.isEmpty()) return val toVisit = mutableListOf(edge) @@ -105,7 +121,7 @@ abstract class XcfaCoi(protected val xcfa: XCFA) { source: XcfaEdge, target: XcfaEdge, observableVars: Map, AccessType>, precVars: Collection>, relation: MutableMap> ) { - val vars = target.getVars() + val vars = target.collectVarsWithAccessType() var relevantAction = vars.any { it.value.isWritten && it.key in precVars } if (!relevantAction) { val assumeVars = target.label.collectAssumesVars() diff --git a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/coi/XcfaCoiMultiThread.kt b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/coi/XcfaCoiMultiThread.kt index 14802dc422..7774dafb16 100644 --- a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/coi/XcfaCoiMultiThread.kt +++ b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/coi/XcfaCoiMultiThread.kt @@ -1,9 +1,25 @@ +/* + * Copyright 2023 Budapest University of Technology and Economics + * + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ + package hu.bme.mit.theta.xcfa.analysis.coi import hu.bme.mit.theta.analysis.LTS import hu.bme.mit.theta.analysis.Prec import hu.bme.mit.theta.xcfa.getFlatLabels -import hu.bme.mit.theta.xcfa.getVars +import hu.bme.mit.theta.xcfa.collectVarsWithAccessType import hu.bme.mit.theta.xcfa.isWritten import hu.bme.mit.theta.xcfa.model.StartLabel import hu.bme.mit.theta.xcfa.model.XCFA @@ -125,7 +141,7 @@ class XcfaCoiMultiThread(xcfa: XCFA) : XcfaCoi(xcfa) { private fun findInterProcessObservers(edge: XcfaEdge, prec: Prec) { val precVars = prec.usedVars - val writtenVars = edge.getVars().filter { it.value.isWritten && it.key in precVars } + val writtenVars = edge.collectVarsWithAccessType().filter { it.value.isWritten && it.key in precVars } if (writtenVars.isEmpty()) return xcfa.procedures.forEach { procedure -> diff --git a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/coi/XcfaCoiSingleThread.kt b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/coi/XcfaCoiSingleThread.kt index e86648fd6d..9d6b3fa8bb 100644 --- a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/coi/XcfaCoiSingleThread.kt +++ b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/coi/XcfaCoiSingleThread.kt @@ -1,3 +1,19 @@ +/* + * Copyright 2023 Budapest University of Technology and Economics + * + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ + package hu.bme.mit.theta.xcfa.analysis.coi import hu.bme.mit.theta.analysis.LTS diff --git a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/por/XcfaAasporCoiLts.kt b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/por/XcfaAasporCoiLts.kt index 562dd1e800..247eadcf47 100644 --- a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/por/XcfaAasporCoiLts.kt +++ b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/por/XcfaAasporCoiLts.kt @@ -1,3 +1,19 @@ +/* + * Copyright 2023 Budapest University of Technology and Economics + * + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ + package hu.bme.mit.theta.xcfa.analysis.por import hu.bme.mit.theta.analysis.LTS diff --git a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/por/XcfaAasporLts.kt b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/por/XcfaAasporLts.kt index ee5bcc5e21..6bcdb06dff 100644 --- a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/por/XcfaAasporLts.kt +++ b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/por/XcfaAasporLts.kt @@ -23,8 +23,10 @@ import hu.bme.mit.theta.xcfa.analysis.XcfaAction import hu.bme.mit.theta.xcfa.analysis.XcfaState import hu.bme.mit.theta.xcfa.model.XCFA -open class XcfaAasporLts(xcfa: XCFA, private val ignoredVarRegistry: MutableMap, MutableSet>) : - XcfaSporLts(xcfa) { +open class XcfaAasporLts( + xcfa: XCFA, + private val ignoredVarRegistry: MutableMap, MutableSet> +) : XcfaSporLts(xcfa) { override fun

getEnabledActionsFor(state: XcfaState<*>, exploredActions: Collection, prec: P): Set { diff --git a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/por/XcfaDporLts.kt b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/por/XcfaDporLts.kt index 6a60b9a5ae..88be0f44ed 100644 --- a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/por/XcfaDporLts.kt +++ b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/por/XcfaDporLts.kt @@ -25,7 +25,7 @@ import hu.bme.mit.theta.analysis.waitlist.Waitlist import hu.bme.mit.theta.xcfa.analysis.XcfaAction import hu.bme.mit.theta.xcfa.analysis.XcfaState import hu.bme.mit.theta.xcfa.analysis.getXcfaLts -import hu.bme.mit.theta.xcfa.getGlobalVars +import hu.bme.mit.theta.xcfa.collectIndirectGlobalVarAccesses import hu.bme.mit.theta.xcfa.isWritten import hu.bme.mit.theta.xcfa.model.XCFA import java.util.* @@ -456,8 +456,8 @@ open class XcfaDporLts(private val xcfa: XCFA) : LTS { protected open fun dependent(a: A, b: A): Boolean { if (a.pid == b.pid) return true - val aGlobalVars = a.edge.getGlobalVars(xcfa) - val bGlobalVars = b.edge.getGlobalVars(xcfa) + val aGlobalVars = a.edge.collectIndirectGlobalVarAccesses(xcfa) + val bGlobalVars = b.edge.collectIndirectGlobalVarAccesses(xcfa) // dependent if they access the same variable (at least one write) return (aGlobalVars.keys intersect bGlobalVars.keys).any { aGlobalVars[it].isWritten || bGlobalVars[it].isWritten } } @@ -488,8 +488,8 @@ class XcfaAadporLts(private val xcfa: XCFA) : XcfaDporLts(xcfa) { if (a.pid == b.pid) return true val precVars = prec?.usedVars?.toSet() ?: return super.dependent(a, b) - val aGlobalVars = a.edge.getGlobalVars(xcfa) - val bGlobalVars = b.edge.getGlobalVars(xcfa) + val aGlobalVars = a.edge.collectIndirectGlobalVarAccesses(xcfa) + val bGlobalVars = b.edge.collectIndirectGlobalVarAccesses(xcfa) // dependent if they access the same variable in the precision (at least one write) return (aGlobalVars.keys intersect bGlobalVars.keys intersect precVars).any { aGlobalVars[it].isWritten || bGlobalVars[it].isWritten } } diff --git a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/por/XcfaSporLts.kt b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/por/XcfaSporLts.kt index b384f1bc25..c2dac34f9e 100644 --- a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/por/XcfaSporLts.kt +++ b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/por/XcfaSporLts.kt @@ -19,13 +19,10 @@ import hu.bme.mit.theta.analysis.LTS import hu.bme.mit.theta.core.decl.Decl import hu.bme.mit.theta.core.decl.VarDecl import hu.bme.mit.theta.core.type.Type +import hu.bme.mit.theta.xcfa.* import hu.bme.mit.theta.xcfa.analysis.XcfaAction import hu.bme.mit.theta.xcfa.analysis.XcfaState import hu.bme.mit.theta.xcfa.analysis.getXcfaLts -import hu.bme.mit.theta.xcfa.collectVars -import hu.bme.mit.theta.xcfa.getFlatLabels -import hu.bme.mit.theta.xcfa.isAtomicBegin -import hu.bme.mit.theta.xcfa.isAtomicEnd import hu.bme.mit.theta.xcfa.model.* import java.util.* import java.util.function.Predicate @@ -78,7 +75,7 @@ open class XcfaSporLts(protected val xcfa: XCFA) : LTS, XcfaAction> */ override fun getEnabledActionsFor(state: XcfaState<*>): Set { // Collecting enabled actions - val allEnabledActions = getAllEnabledActionsFor(state) + val allEnabledActions = simpleXcfaLts.getEnabledActionsFor(state) // Calculating the source set starting from every (or some of the) enabled transition; the minimal source set is stored var minimalSourceSet = setOf() @@ -92,15 +89,6 @@ open class XcfaSporLts(protected val xcfa: XCFA) : LTS, XcfaAction> return minimalSourceSet } - /** - * Returns all enabled actions in the given state. - * - * @param state the state whose enabled actions we would like to know - * @return the enabled actions - */ - protected fun getAllEnabledActionsFor(state: XcfaState<*>): Collection = - simpleXcfaLts.getEnabledActionsFor(state) - /** * Returns the possible starting actions of a source set. * @@ -230,21 +218,11 @@ open class XcfaSporLts(protected val xcfa: XCFA) : LTS, XcfaAction> */ private fun getUsedSharedObjects(edge: XcfaEdge): Set> { val flatLabels = edge.getFlatLabels() - return if (flatLabels.any(XcfaLabel::isAtomicBegin)) { - getSharedObjectsWithBFS(edge) { it.getFlatLabels().none(XcfaLabel::isAtomicEnd) }.toSet() + val mutexes = flatLabels.filterIsInstance().flatMap { it.acquiredMutexes }.toMutableSet() + return if (mutexes.isEmpty()) { + getDirectlyUsedSharedObjects(edge) } else { - val lock = flatLabels.firstOrNull { - it is FenceLabel && it.labels.any { l -> l.startsWith("mutex_lock") } - } as FenceLabel? - if (lock != null) { - val mutex = lock.labels.first { l -> l.startsWith("mutex_lock") } - .substringAfter('(').substringBefore(')') - getSharedObjectsWithBFS(edge) { - it.getFlatLabels().none { fl -> fl is FenceLabel && "mutex_unlock(${mutex})" in fl.labels } - }.toSet() - } else { - getDirectlyUsedSharedObjects(edge) - } + getSharedObjectsWithBFS(edge) { it.mutexOperations(mutexes) }.toSet() } } @@ -287,21 +265,21 @@ open class XcfaSporLts(protected val xcfa: XCFA) : LTS, XcfaAction> private fun getSharedObjectsWithBFS(startTransition: XcfaEdge, goFurther: Predicate): Set> { val vars = mutableSetOf>() - val exploredTransitions = mutableListOf() - val transitionsToExplore = mutableListOf() - transitionsToExplore.add(startTransition) - while (transitionsToExplore.isNotEmpty()) { - val exploring = transitionsToExplore.removeFirst() + val exploredEdges = mutableListOf() + val edgesToExplore = mutableListOf() + edgesToExplore.add(startTransition) + while (edgesToExplore.isNotEmpty()) { + val exploring = edgesToExplore.removeFirst() vars.addAll(getDirectlyUsedSharedObjects(exploring)) if (goFurther.test(exploring)) { - val successiveTransitions = getSuccessiveTransitions(exploring) - for (newTransition in successiveTransitions) { - if (newTransition !in exploredTransitions) { - transitionsToExplore.add(newTransition) + val successiveEdges = getSuccessiveTransitions(exploring) + for (newEdge in successiveEdges) { + if (newEdge !in exploredEdges) { + edgesToExplore.add(newEdge) } } } - exploredTransitions.add(exploring) + exploredEdges.add(exploring) } return vars } @@ -325,8 +303,7 @@ open class XcfaSporLts(protected val xcfa: XCFA) : LTS, XcfaAction> val startThreads = edge.getFlatLabels().filterIsInstance().toList() if (startThreads.isNotEmpty()) { // for start thread labels, the thread procedure must be explored, too! startThreads.forEach { startThread -> - outgoingEdges.addAll( - xcfa.procedures.first { it.name == startThread.name }.initLoc.outgoingEdges) + outgoingEdges.addAll(xcfa.procedures.first { it.name == startThread.name }.initLoc.outgoingEdges) } } return outgoingEdges 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-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/ConfigOptions.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/ConfigOptions.kt index 5dda459fa4..e015dca75e 100644 --- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/ConfigOptions.kt +++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/ConfigOptions.kt @@ -181,7 +181,7 @@ enum class Refinement( ), MULTI_SEQ( refiner = { s, m -> - if(m == CexMonitorOptions.CHECK) error("CexMonitor is not implemented for MULTI_SEQ") + if (m == CexMonitorOptions.CHECK) error("CexMonitor is not implemented for MULTI_SEQ") ExprTraceSeqItpChecker.create(BoolExprs.True(), BoolExprs.True(), s.createItpSolver()) }, stopCriterion = StopCriterions.fullExploration() @@ -333,12 +333,14 @@ enum class ConeOfInfluenceMode( XcfaAasporCoiLts(xcfa, ivr, ConeOfInfluence.lts) }) ; + var porLts: LTS, XcfaAction>? = null } // TODO CexMonitor: disable for multi_seq // TODO add new monitor to xsts cli enum class CexMonitorOptions { + CHECK, DISABLE } diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/XcfaCegarConfig.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/XcfaCegarConfig.kt index 13b080036f..04f274e821 100644 --- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/XcfaCegarConfig.kt +++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/XcfaCegarConfig.kt @@ -92,7 +92,7 @@ data class XcfaCegarConfig( var pruneStrategy: PruneStrategy = PruneStrategy.LAZY, @Parameter(names = ["--cex-monitor"], description = "Warning: With some configurations (e.g. lazy pruning) it is POSSIBLE (but rare) that analysis is stopped, " + - "even though it could still progress. If in doubt, disable this monitor and check results.") + "even though it could still progress. If in doubt, disable this monitor and check results.") var cexMonitor: CexMonitorOptions = CexMonitorOptions.DISABLE, @Parameter(names = ["--timeout-ms"], description = "Timeout for verification (only valid with --strategy SERVER), use 0 for no timeout") diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/XcfaCli.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/XcfaCli.kt index 19cd03eb05..119ec83fe9 100644 --- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/XcfaCli.kt +++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/XcfaCli.kt @@ -149,7 +149,8 @@ class XcfaCli(private val args: Array) { @Parameter(names = ["--seed"], description = "Random seed used for DPOR") var randomSeed: Int = -1 - @Parameter(names = ["--arg-to-file"], description = "Visualize the resulting file here: https://ftsrg-edu.github.io/student-sisak-argviz/") + @Parameter(names = ["--arg-to-file"], + description = "Visualize the resulting file here: https://ftsrg-edu.github.io/student-sisak-argviz/") var argToFile: Boolean = false @Parameter diff --git a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/Utils.kt b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/Utils.kt index 1d59429472..799d6bfd1b 100644 --- a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/Utils.kt +++ b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/Utils.kt @@ -16,7 +16,6 @@ package hu.bme.mit.theta.xcfa -import com.google.common.collect.Sets import hu.bme.mit.theta.common.dsl.Env import hu.bme.mit.theta.common.dsl.Symbol import hu.bme.mit.theta.common.dsl.SymbolTable @@ -29,13 +28,28 @@ import hu.bme.mit.theta.core.type.booltype.BoolType import hu.bme.mit.theta.core.utils.ExprUtils import hu.bme.mit.theta.core.utils.StmtUtils import hu.bme.mit.theta.xcfa.model.* +import java.util.function.Predicate -fun XCFA.collectVars(): Iterable> = vars.map { it.wrappedVar } - .union(procedures.map { it.vars }.flatten()) +/** + * Get flattened label list (without sequence labels). + */ +fun XcfaEdge.getFlatLabels(): List = label.getFlatLabels() + +fun XcfaLabel.getFlatLabels(): List = when (this) { + is SequenceLabel -> { + val ret = mutableListOf() + labels.forEach { ret.addAll(it.getFlatLabels()) } + ret + } -fun XCFA.collectAssumes(): Iterable> = procedures.map { - it.edges.map { it.label.collectAssumes() }.flatten() + else -> listOf(this) +} + +fun XCFA.collectVars(): Iterable> = vars.map { it.wrappedVar } union procedures.map { it.vars }.flatten() + +fun XCFA.collectAssumes(): Iterable> = procedures.map { procedure -> + procedure.edges.map { it.label.collectAssumes() }.flatten() }.flatten() fun XcfaLabel.collectAssumes(): Iterable> = when (this) { @@ -75,14 +89,15 @@ fun XcfaLabel.collectVars(): Iterable> = when (this) { is InvokeLabel -> params.map { ExprUtils.getVars(it) }.flatten() is JoinLabel -> setOf(pidVar) is ReadLabel -> setOf(global, local) - is StartLabel -> Sets.union(params.map { ExprUtils.getVars(it) }.flatten().toSet(), - setOf(pidVar)) - + is StartLabel -> params.map { ExprUtils.getVars(it) }.flatten().toSet() union setOf(pidVar) is WriteLabel -> setOf(global, local) else -> emptySet() } +// Complex var access requests + typealias AccessType = Pair +private typealias VarAccessMap = Map, AccessType> val AccessType?.isRead get() = this?.first == true val AccessType?.isWritten get() = this?.second == true @@ -92,41 +107,60 @@ fun AccessType?.merge(other: AccessType?) = val WRITE: AccessType get() = Pair(false, true) val READ: AccessType get() = Pair(true, false) -private typealias VarAccessMap = Map, AccessType> - private fun List.mergeAndCollect(): VarAccessMap = this.fold(mapOf()) { acc, next -> (acc.keys + next.keys).associateWith { acc[it].merge(next[it]) } } +/** + * The list of mutexes acquired by the label. + */ +inline val FenceLabel.acquiredMutexes: Set + get() = labels.mapNotNull { + when { + it == "ATOMIC_BEGIN" -> "___atomic_block_mutex___" + it.startsWith("mutex_lock") -> it.substringAfter('(').substringBefore(')') + it.startsWith("cond_wait") -> it.substring("cond_wait".length + 1, it.length - 1).split(",")[1] + else -> null + } + }.toSet() + +/** + * The list of mutexes released by the label. + */ +inline val FenceLabel.releasedMutexes: Set + get() = labels.mapNotNull { + when { + it == "ATOMIC_END" -> "___atomic_block_mutex___" + it.startsWith("mutex_unlock") -> it.substringAfter('(').substringBefore(')') + it.startsWith("start_cond_wait") -> it.substring("start_cond_wait".length + 1, it.length - 1).split(",")[1] + else -> null + } + }.toSet() + +/** + * Returns the list of accessed variables by the edge associated with an AccessType object. + */ +fun XcfaEdge.collectVarsWithAccessType(): VarAccessMap = label.collectVarsWithAccessType() + /** * Returns the list of accessed variables by the label. * The variable is associated with an AccessType object based on whether the variable is read/written by the label. */ -internal fun XcfaLabel.collectVarsWithAccessType(): VarAccessMap = when (this) { +fun XcfaLabel.collectVarsWithAccessType(): VarAccessMap = when (this) { is StmtLabel -> { when (stmt) { is HavocStmt<*> -> mapOf(stmt.varDecl to WRITE) - is AssignStmt<*> -> StmtUtils.getVars(stmt).associateWith { READ } + mapOf( - stmt.varDecl to WRITE) - + is AssignStmt<*> -> StmtUtils.getVars(stmt).associateWith { READ } + mapOf(stmt.varDecl to WRITE) else -> StmtUtils.getVars(stmt).associateWith { READ } } } - is NondetLabel -> { - labels.map { it.collectVarsWithAccessType() }.mergeAndCollect() - } - - is SequenceLabel -> { - labels.map { it.collectVarsWithAccessType() }.mergeAndCollect() - } - + is NondetLabel -> labels.map { it.collectVarsWithAccessType() }.mergeAndCollect() + is SequenceLabel -> labels.map { it.collectVarsWithAccessType() }.mergeAndCollect() is InvokeLabel -> params.map { ExprUtils.getVars(it) }.flatten().associateWith { READ } is JoinLabel -> mapOf(pidVar to READ) is ReadLabel -> mapOf(global to READ, local to READ) - is StartLabel -> params.map { ExprUtils.getVars(it) }.flatten().associateWith { READ } + mapOf( - pidVar to READ) - + is StartLabel -> params.map { ExprUtils.getVars(it) }.flatten().associateWith { READ } + mapOf(pidVar to READ) is WriteLabel -> mapOf(global to WRITE, local to WRITE) else -> emptyMap() } @@ -134,56 +168,108 @@ internal fun XcfaLabel.collectVarsWithAccessType(): VarAccessMap = when (this) { /** * Returns the global variables accessed by the label (the variables present in the given argument). */ -private fun XcfaLabel.collectGlobalVars(globalVars: Set>) = +private fun XcfaLabel.collectGlobalVars(globalVars: Set>): VarAccessMap = collectVarsWithAccessType().filter { labelVar -> globalVars.any { it == labelVar.key } } -inline val XcfaLabel.isAtomicBegin - get() = this is FenceLabel && this.labels.contains("ATOMIC_BEGIN") -inline val XcfaLabel.isAtomicEnd get() = this is FenceLabel && this.labels.contains("ATOMIC_END") - /** * Returns the global variables (potentially indirectly) accessed by the edge. - * If the edge starts an atomic block, all variable accesses in the atomic block is returned. + * If the edge starts an atomic block, all variable accesses in the atomic block are returned. * Variables are associated with a pair of boolean values: the first is true if the variable is read and false otherwise. The second is similar for write access. */ -fun XcfaEdge.getGlobalVars(xcfa: XCFA): Map, AccessType> { +fun XcfaEdge.collectIndirectGlobalVarAccesses(xcfa: XCFA): VarAccessMap { val globalVars = xcfa.vars.map(XcfaGlobalVar::wrappedVar).toSet() - var label = this.label - if (label is SequenceLabel && label.labels.size == 1) label = label.labels[0] - if (label.isAtomicBegin || (label is SequenceLabel && label.labels.any { it.isAtomicBegin } && label.labels.none { it.isAtomicEnd })) { - val vars = mutableMapOf, AccessType>() - val processed = mutableSetOf() - val unprocessed = mutableListOf(this) - while (unprocessed.isNotEmpty()) { - val e = unprocessed.removeFirst() - var eLabel = e.label - if (eLabel is SequenceLabel && eLabel.labels.size == 1) eLabel = eLabel.labels[0] - eLabel.collectGlobalVars(globalVars).forEach { (varDecl, accessType) -> - vars[varDecl] = accessType.merge(vars[varDecl]) - } - processed.add(e) - if (!(eLabel.isAtomicEnd || (eLabel is SequenceLabel && eLabel.labels.any { it.isAtomicEnd }))) { - unprocessed.addAll(e.target.outgoingEdges subtract processed) - } - } - return vars + val flatLabels = getFlatLabels() + val mutexes = flatLabels.filterIsInstance().flatMap { it.acquiredMutexes }.toMutableSet() + return if (mutexes.isEmpty()) { + label.collectGlobalVars(globalVars) } else { - return label.collectGlobalVars(globalVars) + collectGlobalVarsWithTraversal(globalVars) { it.mutexOperations(mutexes) } } } /** - * Returns the list of accessed variables by the edge associated with an AccessType object. + * Represents a global variable access: stores the variable declaration, the access type (read/write) and the set of + * mutexes that are needed to perform the variable access. */ -fun XcfaEdge.getVars(): Map, AccessType> = label.collectVarsWithAccessType() +class GlobalVarAccessWithMutexes(val varDecl: VarDecl<*>, val access: AccessType, val mutexes: Set) /** - * Returns true if the edge starts an atomic block. + * Returns the global variable accesses of the edge. + * + * @param xcfa the XCFA that contains the edge + * @param currentMutexes the set of mutexes currently acquired by the process of the edge + * @return the list of global variable accesses (c.f., [GlobalVarAccessWithMutexes]) */ -fun XcfaEdge.startsAtomic(): Boolean { - var label = this.label - if (label is SequenceLabel && label.labels.size == 1) label = label.labels[0] - return label is FenceLabel && label.labels.contains("ATOMIC_BEGIN") +fun XcfaEdge.getGlobalVarsWithNeededMutexes(xcfa: XCFA, currentMutexes: Set): List { + val globalVars = xcfa.vars.map(XcfaGlobalVar::wrappedVar).toSet() + val neededMutexes = currentMutexes.toMutableSet() + val accesses = mutableListOf() + getFlatLabels().forEach { label -> + if (label is FenceLabel) { + neededMutexes.addAll(label.acquiredMutexes) + } else { + val vars = label.collectGlobalVars(globalVars) + accesses.addAll(vars.mapNotNull { (varDecl, accessType) -> + if (accesses.any { it.varDecl == varDecl && (it.access == accessType && it.access == WRITE) }) { + null + } else { + GlobalVarAccessWithMutexes(varDecl, accessType, neededMutexes.toSet()) + } + }) + } + } + return accesses +} + +/** + * Returns global variables encountered in a search starting from the edge. + * + * @param goFurther the predicate that tells whether more edges have to be explored through an edge + * @return the set of encountered shared objects + */ +private fun XcfaEdge.collectGlobalVarsWithTraversal(globalVars: Set>, goFurther: Predicate) + : VarAccessMap { + val vars = mutableMapOf, AccessType>() + val exploredEdges = mutableListOf() + val edgesToExplore = mutableListOf() + edgesToExplore.add(this) + while (edgesToExplore.isNotEmpty()) { + val exploring = edgesToExplore.removeFirst() + exploring.label.collectGlobalVars(globalVars).forEach { (varDecl, access) -> + vars[varDecl] = vars[varDecl].merge(access) + } + if (goFurther.test(exploring)) { + for (newEdge in exploring.target.outgoingEdges) { + if (newEdge !in exploredEdges) { + edgesToExplore.add(newEdge) + } + } + } + exploredEdges.add(exploring) + } + return vars +} + +/** + * Follows the mutex operations of the given edge and updates the given set of mutexes. + * + * @param mutexes the set of mutexes currently acquired + * @return true if the set of mutexes is non-empty after the mutex operations + */ +fun XcfaEdge.mutexOperations(mutexes: MutableSet): Boolean { + val edgeFlatLabels = getFlatLabels() + val acquiredLocks = mutableSetOf() + val releasedLocks = mutableSetOf() + edgeFlatLabels.filterIsInstance().forEach { fence -> + releasedLocks.addAll(fence.releasedMutexes) + acquiredLocks.removeAll(fence.releasedMutexes) + + acquiredLocks.addAll(fence.acquiredMutexes) + releasedLocks.removeAll(fence.acquiredMutexes) + } + mutexes.removeAll(releasedLocks) + mutexes.addAll(acquiredLocks) + return mutexes.isNotEmpty() } fun XCFA.getSymbols(): Pair { @@ -199,25 +285,6 @@ fun XCFA.getSymbols(): Pair { return Pair(scope, env) } -private val atomicBlockInnerLocationsCache: HashMap> = HashMap() - -/** - * Returns XCFA locations that are inner locations of any atomic block (after an edge with an AtomicBegin and before - * an edge with an AtomicEnd). - * - * @param xcfaProcedure the atomic block inner locations of this XCFA procedure will be returned - * @return the list of locations in an atomic block - */ -fun getAtomicBlockInnerLocations(xcfaProcedure: XcfaProcedure): List? { - if (atomicBlockInnerLocationsCache.containsKey(xcfaProcedure)) { - return atomicBlockInnerLocationsCache[xcfaProcedure] - } - val atomicBlockInnerLocations: List = getAtomicBlockInnerLocations( - xcfaProcedure.initLoc) - atomicBlockInnerLocationsCache[xcfaProcedure] = atomicBlockInnerLocations - return atomicBlockInnerLocations -} - /** * Returns XCFA locations that are inner locations of any atomic block (after an edge with an AtomicBegin and before * an edge with an AtomicEnd). @@ -225,55 +292,32 @@ fun getAtomicBlockInnerLocations(xcfaProcedure: XcfaProcedure): List { - return getAtomicBlockInnerLocations(builder.initLoc) -} - -/** - * Get flattened label list (without sequence labels). - */ -fun XcfaEdge.getFlatLabels(): List = label.getFlatLabels() - -fun XcfaLabel.getFlatLabels(): List = when (this) { - is SequenceLabel -> { - val ret = ArrayList() - labels.forEach { ret.addAll(it.getFlatLabels()) } - ret - } - - else -> listOf(this) -} - +fun getAtomicBlockInnerLocations(builder: XcfaProcedureBuilder): List = + getAtomicBlockInnerLocations(builder.initLoc) private fun getAtomicBlockInnerLocations(initialLocation: XcfaLocation): List { - val atomicLocations: MutableList = ArrayList() - val visitedLocations: MutableList = ArrayList() - val locationsToVisit: MutableList = ArrayList() - val isAtomic: HashMap = HashMap() - locationsToVisit.add(initialLocation) - isAtomic[initialLocation] = false - while (!locationsToVisit.isEmpty()) { + val atomicLocations = mutableListOf() + val visitedLocations = mutableListOf() + val locationsToVisit = mutableListOf(initialLocation) + val isAtomic = mutableMapOf(initialLocation to false) + while (locationsToVisit.isNotEmpty()) { val visiting = locationsToVisit.removeAt(0) if (checkNotNull(isAtomic[visiting])) atomicLocations.add(visiting) visitedLocations.add(visiting) for (outEdge in visiting.outgoingEdges) { var isNextAtomic = checkNotNull(isAtomic[visiting]) - if (outEdge.getFlatLabels().stream().anyMatch { label -> - label is FenceLabel && label.labels.contains("ATOMIC_BEGIN") - }) { + if (outEdge.getFlatLabels().any { it is FenceLabel && it.labels.contains("ATOMIC_BEGIN") }) { isNextAtomic = true } - if (outEdge.getFlatLabels().stream().anyMatch { label -> - label is FenceLabel && label.labels.contains("ATOMIC_END") - }) { + if (outEdge.getFlatLabels().any { it is FenceLabel && it.labels.contains("ATOMIC_END") }) { isNextAtomic = false } val target = outEdge.target isAtomic[target] = isNextAtomic - if (atomicLocations.contains(target) && !isNextAtomic) { + if (target in atomicLocations && !isNextAtomic) { atomicLocations.remove(target) } - if (!locationsToVisit.contains(target) && !visitedLocations.contains(target)) { + if (target !in locationsToVisit && target !in visitedLocations) { locationsToVisit.add(outEdge.target) } } diff --git a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/model/Builders.kt b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/model/Builders.kt index 5590f2f048..b0dbbac1d2 100644 --- a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/model/Builders.kt +++ b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/model/Builders.kt @@ -30,7 +30,8 @@ class XcfaBuilder @JvmOverloads constructor( private val vars: MutableSet = LinkedHashSet(), private val procedures: MutableSet = LinkedHashSet(), private val initProcedures: MutableList>>> = ArrayList(), - val metaData: MutableMap = LinkedHashMap()) { + val metaData: MutableMap = LinkedHashMap() +) { fun getVars(): Set = vars fun getProcedures(): Set = procedures @@ -63,7 +64,7 @@ class XcfaBuilder @JvmOverloads constructor( @XcfaDsl class XcfaProcedureBuilder @JvmOverloads constructor( var name: String, - private val manager: ProcedurePassManager, + val manager: ProcedurePassManager, private val params: MutableList, ParamDirection>> = ArrayList(), private val vars: MutableSet> = LinkedHashSet(), private val locs: MutableSet = LinkedHashSet(), @@ -78,23 +79,60 @@ class XcfaProcedureBuilder @JvmOverloads constructor( var errorLoc: Optional = Optional.empty() private set lateinit var parent: XcfaBuilder - private lateinit var optimized: XcfaProcedureBuilder private lateinit var built: XcfaProcedure - fun getParams(): List, ParamDirection>> = if (this::optimized.isInitialized) optimized.params else params - fun getVars(): Set> = if (this::optimized.isInitialized) optimized.vars else vars - fun getLocs(): Set = if (this::optimized.isInitialized) optimized.locs else locs - fun getEdges(): Set = if (this::optimized.isInitialized) optimized.edges else edges + private lateinit var optimized: XcfaProcedureBuilder + private lateinit var partlyOptimized: XcfaProcedureBuilder + private var lastOptimized: Int = -1 + fun getParams(): List, ParamDirection>> = when { + this::optimized.isInitialized -> optimized.params + this::partlyOptimized.isInitialized -> partlyOptimized.params + else -> params + } + + fun getVars(): Set> = when { + this::optimized.isInitialized -> optimized.vars + this::partlyOptimized.isInitialized -> partlyOptimized.vars + else -> vars + } + + fun getLocs(): Set = when { + this::optimized.isInitialized -> optimized.locs + this::partlyOptimized.isInitialized -> partlyOptimized.locs + else -> locs + } + + fun getEdges(): Set = when { + this::optimized.isInitialized -> optimized.edges + this::partlyOptimized.isInitialized -> partlyOptimized.edges + else -> edges + } fun optimize() { if (!this::optimized.isInitialized) { var that = this - for (pass in manager.passes) { + for (pass in manager.passes.flatten()) { that = pass.run(that) } optimized = that } } + fun optimize(phase: Int): Boolean { // true, if optimization is finished (no more phases to execute) + if (this::optimized.isInitialized || phase >= manager.passes.size) return true + if (phase <= lastOptimized) return lastOptimized >= manager.passes.size - 1 + check(phase == lastOptimized + 1) { "Wrong optimization phase!" } + + var that = if (this::partlyOptimized.isInitialized) partlyOptimized else this + for (pass in manager.passes[phase]) { + that = pass.run(that) + } + + partlyOptimized = that + lastOptimized = phase + if (phase >= manager.passes.size - 1) optimized = that + return phase >= manager.passes.size - 1 + } + fun build(parent: XCFA): XcfaProcedure { if (this::built.isInitialized) return built; if (!this::optimized.isInitialized) optimize() @@ -113,21 +151,18 @@ class XcfaProcedureBuilder @JvmOverloads constructor( } fun addParam(toAdd: VarDecl<*>, dir: ParamDirection) { - check( - !this::optimized.isInitialized) { "Cannot add/remove new elements after optimization passes!" } + check(!this::optimized.isInitialized) { "Cannot add/remove new elements after optimization passes!" } params.add(Pair(toAdd, dir)) vars.add(toAdd) } fun addVar(toAdd: VarDecl<*>) { - check( - !this::optimized.isInitialized) { "Cannot add/remove new elements after optimization passes!" } + check(!this::optimized.isInitialized) { "Cannot add/remove new elements after optimization passes!" } vars.add(toAdd) } fun removeVar(toRemove: VarDecl<*>) { - check( - !this::optimized.isInitialized) { "Cannot add/remove new elements after optimization passes!" } + check(!this::optimized.isInitialized) { "Cannot add/remove new elements after optimization passes!" } vars.remove(toRemove) } @@ -159,8 +194,7 @@ class XcfaProcedureBuilder @JvmOverloads constructor( } fun addEdge(toAdd: XcfaEdge) { - check( - !this::optimized.isInitialized) { "Cannot add/remove new elements after optimization passes!" } + check(!this::optimized.isInitialized) { "Cannot add/remove new elements after optimization passes!" } addLoc(toAdd.source) addLoc(toAdd.target) edges.add(toAdd) @@ -169,8 +203,7 @@ class XcfaProcedureBuilder @JvmOverloads constructor( } fun addLoc(toAdd: XcfaLocation) { - check( - !this::optimized.isInitialized) { "Cannot add/remove new elements after optimization passes!" } + check(!this::optimized.isInitialized) { "Cannot add/remove new elements after optimization passes!" } if (!locs.contains(toAdd)) { check(!toAdd.error) check(!toAdd.initial) @@ -180,22 +213,19 @@ class XcfaProcedureBuilder @JvmOverloads constructor( } fun removeEdge(toRemove: XcfaEdge) { - check( - !this::optimized.isInitialized) { "Cannot add/remove new elements after optimization passes!" } + check(!this::optimized.isInitialized) { "Cannot add/remove new elements after optimization passes!" } toRemove.source.outgoingEdges.remove(toRemove) toRemove.target.incomingEdges.remove(toRemove) edges.remove(toRemove) } fun removeLoc(toRemove: XcfaLocation) { - check( - !this::optimized.isInitialized) { "Cannot add/remove new elements after optimization passes!" } + check(!this::optimized.isInitialized) { "Cannot add/remove new elements after optimization passes!" } locs.remove(toRemove) } fun removeLocs(pred: (XcfaLocation) -> Boolean) { - check( - !this::optimized.isInitialized) { "Cannot add/remove new elements after optimization passes!" } + check(!this::optimized.isInitialized) { "Cannot add/remove new elements after optimization passes!" } while (locs.any(pred)) { locs.removeIf(pred) edges.removeIf { @@ -209,8 +239,7 @@ class XcfaProcedureBuilder @JvmOverloads constructor( } fun changeVars(varLut: Map, VarDecl<*>>) { - check( - !this::optimized.isInitialized) { "Cannot add/remove new elements after optimization passes!" } + check(!this::optimized.isInitialized) { "Cannot add/remove new elements after optimization passes!" } val savedVars = ArrayList(vars) vars.clear() savedVars.forEach { vars.add(checkNotNull(varLut[it])) } 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/model/XCFA.kt b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/model/XCFA.kt index 2f3f367246..0916e1e5ca 100644 --- a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/model/XCFA.kt +++ b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/model/XCFA.kt @@ -30,19 +30,29 @@ class XCFA( var cachedHash: Int? = null - var procedures: Set = // procedure definitions - procedureBuilders.map { it.build(this) }.toSet() + var procedures: Set // procedure definitions private set - var initProcedures: List>>> = // procedure names and parameter assignments - initProcedureBuilders.map { Pair(it.first.build(this), it.second) } + + var initProcedures: List>>> // procedure names and parameter assignments private set + init { + var phase = 0 + do { + var ready = true + procedureBuilders.forEach { ready = it.optimize(phase) && ready } + initProcedureBuilders.forEach { ready = it.first.optimize(phase) && ready } + phase++ + } while (!ready) + + procedures = procedureBuilders.map { it.build(this) }.toSet() + initProcedures = initProcedureBuilders.map { Pair(it.first.build(this), it.second) } + } + /** * Recreate an existing XCFA by substituting the procedures and initProcedures fields. */ - fun recreate(procedures: Set, - initProcedures: List>>> - ): XCFA { + fun recreate(procedures: Set, initProcedures: List>>>): XCFA { this.procedures = procedures this.initProcedures = initProcedures return this diff --git a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/PthreadFunctionsPass.kt b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/CLibraryFunctionsPass.kt similarity index 86% rename from subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/PthreadFunctionsPass.kt rename to subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/CLibraryFunctionsPass.kt index eae9425e8d..4d9a952f18 100644 --- a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/PthreadFunctionsPass.kt +++ b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/CLibraryFunctionsPass.kt @@ -25,12 +25,22 @@ import hu.bme.mit.theta.frontend.transformation.grammar.expression.Reference import hu.bme.mit.theta.xcfa.model.* /** - * Transforms the following pthread procedure calls into model elements: - * - pthread_create() - * - pthread_join() + * Transforms the library procedure calls with names in supportedFunctions into model elements. * Requires the ProcedureBuilder be `deterministic`. */ -class PthreadFunctionsPass(val parseContext: ParseContext) : ProcedurePass { +class CLibraryFunctionsPass(val parseContext: ParseContext) : ProcedurePass { + + private val supportedFunctions = setOf( + "printf", + "pthread_join", + "pthread_create", + "pthread_mutex_lock", + "pthread_mutex_unlock", + "pthread_cond_wait", + "pthread_cond_signal", + "pthread_mutex_init", + "pthread_cond_init" + ) override fun run(builder: XcfaProcedureBuilder): XcfaProcedureBuilder { checkNotNull(builder.metaData["deterministic"]) @@ -42,7 +52,8 @@ class PthreadFunctionsPass(val parseContext: ParseContext) : ProcedurePass { if (predicate((it.label as SequenceLabel).labels[0])) { val invokeLabel = it.label.labels[0] as InvokeLabel val metadata = invokeLabel.metadata - val fences: List = when (invokeLabel.name) { + val labels: List = when (invokeLabel.name) { + "printf" -> listOf(NopLabel) "pthread_join" -> { var handle = invokeLabel.params[1] while (handle is Reference<*, *>) handle = handle.op @@ -107,10 +118,10 @@ class PthreadFunctionsPass(val parseContext: ParseContext) : ProcedurePass { "pthread_mutex_init", "pthread_cond_init" -> listOf(NopLabel) - else -> error("Unknown pthread function ${invokeLabel.name}") + else -> error("Unsupported library function ${invokeLabel.name}") } - edge.withLabel(SequenceLabel(fences)).splitIf { fence -> - fence is FenceLabel && fence.labels.any { l -> l.startsWith("start_cond_wait") } + edge.withLabel(SequenceLabel(labels)).splitIf { label -> + label is FenceLabel && label.labels.any { l -> l.startsWith("start_cond_wait") } }.forEach(builder::addEdge) } else { builder.addEdge(edge.withLabel(SequenceLabel(it.label.labels))) @@ -122,6 +133,6 @@ class PthreadFunctionsPass(val parseContext: ParseContext) : ProcedurePass { } private fun predicate(it: XcfaLabel): Boolean { - return it is InvokeLabel && it.name.startsWith("pthread_") + return it is InvokeLabel && it.name in supportedFunctions } } \ No newline at end of file diff --git a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/InlineProceduresPass.kt b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/InlineProceduresPass.kt index 3a42d18c37..5cfbfa728c 100644 --- a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/InlineProceduresPass.kt +++ b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/InlineProceduresPass.kt @@ -34,19 +34,16 @@ class InlineProceduresPass(val parseContext: ParseContext) : ProcedurePass { override fun run(builder: XcfaProcedureBuilder): XcfaProcedureBuilder { if (!builder.canInline()) return builder checkNotNull(builder.metaData["deterministic"]) - check( - builder.metaData["inlined"] == null) { "Recursive programs are not supported by inlining." } + check(builder.metaData["inlined"] == null) { "Recursive programs are not supported by inlining." } builder.metaData["inlined"] = Unit while (true) { var foundOne = false for (edge in ArrayList(builder.getEdges())) { val pred: (XcfaLabel) -> Boolean = { it -> - it is InvokeLabel && builder.parent.getProcedures() - .any { p -> p.name == it.name } + it is InvokeLabel && builder.parent.getProcedures().any { p -> p.name == it.name } } val edges = edge.splitIf(pred) - if (edges.size > 1 || (edges.size == 1 && pred( - (edges[0].label as SequenceLabel).labels[0]))) { + if (edges.size > 1 || (edges.size == 1 && pred((edges[0].label as SequenceLabel).labels[0]))) { builder.removeEdge(edge) edges.forEach { if (pred((it.label as SequenceLabel).labels[0])) { @@ -54,10 +51,12 @@ class InlineProceduresPass(val parseContext: ParseContext) : ProcedurePass { val source = it.source val target = it.target val invokeLabel: InvokeLabel = it.label.labels[0] as InvokeLabel - val procedure = builder.parent.getProcedures() - .find { p -> p.name == invokeLabel.name } + val procedure = builder.parent.getProcedures().find { p -> p.name == invokeLabel.name } checkNotNull(procedure) - procedure.optimize() + val inlineIndex = builder.manager.passes.indexOfFirst { phase -> + phase.any { pass -> pass is InlineProceduresPass } + } + procedure.optimize(inlineIndex) val newLocs: MutableMap = LinkedHashMap() procedure.getLocs().forEach { newLocs.put(it, it.inlinedCopy()) } @@ -91,8 +90,7 @@ class InlineProceduresPass(val parseContext: ParseContext) : ProcedurePass { val finalLoc = procedure.finalLoc val errorLoc = procedure.errorLoc - builder.addEdge( - XcfaEdge(source, checkNotNull(newLocs[initLoc]), SequenceLabel(inStmts))) + builder.addEdge(XcfaEdge(source, checkNotNull(newLocs[initLoc]), SequenceLabel(inStmts))) if (finalLoc.isPresent) builder.addEdge(XcfaEdge(checkNotNull(newLocs[finalLoc.get()]), target, SequenceLabel(outStmts))) @@ -116,7 +114,6 @@ class InlineProceduresPass(val parseContext: ParseContext) : ProcedurePass { } private fun XcfaLocation.inlinedCopy(): XcfaLocation { - return copy(name + XcfaLocation.uniqueCounter(), initial = false, final = false, - error = false) + return copy(name + XcfaLocation.uniqueCounter(), initial = false, final = false, error = false) } } \ 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 4889fc3a18..64e5a66931 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 @@ -126,9 +126,6 @@ class LbePass(val parseContext: ParseContext) : ProcedurePass { return builder } - val isPostInlining: Boolean - get() = true - /** * Collapses atomic blocks sequentially. */ @@ -278,7 +275,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)) ) { @@ -308,7 +305,10 @@ class LbePass(val parseContext: ParseContext) : ProcedurePass { private fun isNotLocal(edge: XcfaEdge): Boolean { return !edge.getFlatLabels().all { label -> !(label is StartLabel || label is JoinLabel) && label.collectVars().all(builder.getVars()::contains) && - !(label is StmtLabel && label.stmt is AssumeStmt && label.stmt.cond is FalseExpr) + !(label is StmtLabel && label.stmt is AssumeStmt && label.stmt.cond is FalseExpr) && + !(label is FenceLabel && label.labels.any { name -> + listOf("ATOMIC_BEGIN", "mutex_lock", "cond_wait").any { name.startsWith(it) } + }) } } } \ No newline at end of file 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 ab2faf0fe3..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 @@ -18,39 +18,50 @@ package hu.bme.mit.theta.xcfa.passes import hu.bme.mit.theta.frontend.ParseContext -open class ProcedurePassManager(val passes: List) +open class ProcedurePassManager(vararg passes: List) { -class CPasses(checkOverflow: Boolean, parseContext: ParseContext) : ProcedurePassManager(listOf( - // formatting - NormalizePass(parseContext), - DeterministicPass(parseContext), - // removing redundant elements - EmptyEdgeRemovalPass(parseContext), - UnusedLocRemovalPass(parseContext), - // optimizing - SimplifyExprsPass(parseContext), - // handling intrinsics - ErrorLocationPass(checkOverflow, parseContext), - FinalLocationPass(checkOverflow, parseContext), - SvCompIntrinsicsPass(parseContext), - FpFunctionsToExprsPass(parseContext), - PthreadFunctionsPass(parseContext), - LoopUnrollPass(), - // trying to inline procedures - InlineProceduresPass(parseContext), - RemoveDeadEnds(parseContext), - EliminateSelfLoops(parseContext), - // handling remaining function calls - NondetFunctionPass(parseContext), - LbePass(parseContext), - NormalizePass(parseContext), // needed after lbe, TODO - DeterministicPass(parseContext), // needed after lbe, TODO - HavocPromotionAndRange(parseContext), - // Final cleanup - UnusedVarPass(parseContext), -)) + val passes: List> = passes.toList() +} -class ChcPasses : ProcedurePassManager(listOf(/* +class CPasses(checkOverflow: Boolean, parseContext: ParseContext) : ProcedurePassManager( + listOf( + // formatting + NormalizePass(parseContext), + DeterministicPass(parseContext), + // removing redundant elements + EmptyEdgeRemovalPass(parseContext), + UnusedLocRemovalPass(parseContext), + // handling intrinsics + ErrorLocationPass(checkOverflow, parseContext), + FinalLocationPass(checkOverflow, parseContext), + SvCompIntrinsicsPass(parseContext), + FpFunctionsToExprsPass(parseContext), + CLibraryFunctionsPass(parseContext), + ), + listOf( + // optimizing + SimplifyExprsPass(parseContext), + LoopUnrollPass(), + ), + listOf( + // trying to inline procedures + InlineProceduresPass(parseContext), + RemoveDeadEnds(parseContext), + EliminateSelfLoops(parseContext), + ), + listOf( + // handling remaining function calls + NondetFunctionPass(parseContext), + LbePass(parseContext), + NormalizePass(parseContext), // needed after lbe, TODO + DeterministicPass(parseContext), // needed after lbe, TODO + HavocPromotionAndRange(parseContext), + // Final cleanup + UnusedVarPass(parseContext), + ) +) + +class ChcPasses : ProcedurePassManager(/*listOf( // formatting NormalizePass(), DeterministicPass(), @@ -77,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 diff --git a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/SimplifyExprsPass.kt b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/SimplifyExprsPass.kt index 7a6f23df8a..2f1d5c3540 100644 --- a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/SimplifyExprsPass.kt +++ b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/SimplifyExprsPass.kt @@ -33,7 +33,10 @@ import hu.bme.mit.theta.core.utils.StmtUtils import hu.bme.mit.theta.core.utils.TypeUtils.cast import hu.bme.mit.theta.frontend.ParseContext import hu.bme.mit.theta.frontend.transformation.model.types.complex.CComplexType +import hu.bme.mit.theta.xcfa.collectVarsWithAccessType +import hu.bme.mit.theta.xcfa.isRead import hu.bme.mit.theta.xcfa.model.* +import java.lang.UnsupportedOperationException /** * This pass simplifies the expressions inside statements and substitutes the values of constant variables @@ -46,6 +49,7 @@ class SimplifyExprsPass(val parseContext: ParseContext) : ProcedurePass { override fun run(builder: XcfaProcedureBuilder): XcfaProcedureBuilder { checkNotNull(builder.metaData["deterministic"]) + removeUnusedGlobalVarWrites(builder) val valuation = findConstVariables(builder) val edges = LinkedHashSet(builder.getEdges()) for (edge in edges) { @@ -82,6 +86,25 @@ class SimplifyExprsPass(val parseContext: ParseContext) : ProcedurePass { return builder } + private fun removeUnusedGlobalVarWrites(builder: XcfaProcedureBuilder) { + val usedVars = mutableSetOf>() + val xcfaBuilder = builder.parent + xcfaBuilder.getProcedures().flatMap { it.getEdges() }.forEach { + it.label.collectVarsWithAccessType().forEach { (varDecl, access) -> + if (access.isRead) usedVars.add(varDecl) + } + } + val unusedVars = xcfaBuilder.getVars().map { it.wrappedVar } union builder.getVars() subtract + usedVars subtract builder.getParams().map { it.first }.toSet() + xcfaBuilder.getProcedures().forEach { b -> + b.getEdges().toList().forEach { edge -> + val newLabel = edge.label.removeUnusedWrites(unusedVars) + b.removeEdge(edge) + b.addEdge(edge.withLabel(newLabel)) + } + } + } + private fun findConstVariables(builder: XcfaProcedureBuilder): Valuation { val valuation = MutableValuation() builder.parent.getProcedures() @@ -100,7 +123,10 @@ class SimplifyExprsPass(val parseContext: ParseContext) : ProcedurePass { } .filterNotNull() .forEach { assignment -> - valuation.put(assignment.varDecl, assignment.expr.eval(ImmutableValuation.empty())) + try { + valuation.put(assignment.varDecl, assignment.expr.eval(ImmutableValuation.empty())) + } catch (_: UnsupportedOperationException) { + } } return valuation } diff --git a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/Utils.kt b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/Utils.kt index bab9af5875..5ae232290c 100644 --- a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/Utils.kt +++ b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/Utils.kt @@ -29,12 +29,6 @@ import hu.bme.mit.theta.xcfa.getFlatLabels import hu.bme.mit.theta.xcfa.model.* import java.util.* -fun label2edge(edge: XcfaEdge, label: XcfaLabel) { - val source = edge.source - val target = edge.target - -} - /** * XcfaEdge must be in a `deterministic` ProcedureBuilder */ @@ -154,4 +148,34 @@ private fun XcfaProcedureBuilder.canInline(tally: LinkedList): Boolean { tally.pop() metaData[if (recursive) "recursive" else "canInline"] = Unit return !recursive +} + +internal fun XcfaLabel.removeUnusedWrites(unusedVars: Set>): XcfaLabel { + return when (this) { + is SequenceLabel -> { + val newLabels = mutableListOf() + this.labels.forEach { label -> + val newLabel = label.removeUnusedWrites(unusedVars) + if (newLabel !is NopLabel) newLabels.add(newLabel) + } + SequenceLabel(newLabels) + } + + is NondetLabel -> { + val newLabels = mutableSetOf() + this.labels.forEach { label -> + val newLabel = label.removeUnusedWrites(unusedVars) + if (newLabel !is NopLabel) newLabels.add(newLabel) + } + NondetLabel(newLabels) + } + + is StmtLabel -> when (this.stmt) { + is AssignStmt<*> -> if (unusedVars.contains(this.stmt.varDecl)) NopLabel else this + is HavocStmt<*> -> if (unusedVars.contains(this.stmt.varDecl)) NopLabel else this + else -> this + } + + else -> this + } } \ No newline at end of file diff --git a/subprojects/xcfa/xcfa/src/test/java/hu/bme/mit/theta/xcfa/passes/PassTests.kt b/subprojects/xcfa/xcfa/src/test/java/hu/bme/mit/theta/xcfa/passes/PassTests.kt index 1bc7f624e8..30f58edbd7 100644 --- a/subprojects/xcfa/xcfa/src/test/java/hu/bme/mit/theta/xcfa/passes/PassTests.kt +++ b/subprojects/xcfa/xcfa/src/test/java/hu/bme/mit/theta/xcfa/passes/PassTests.kt @@ -373,7 +373,7 @@ class PassTests { passes = listOf( NormalizePass(parseContext), DeterministicPass(parseContext), - PthreadFunctionsPass(parseContext), + CLibraryFunctionsPass(parseContext), ), input = { (init to "L1") {