From 79a30a22c27b6980ec2f19aac3dcda0289e793d7 Mon Sep 17 00:00:00 2001 From: Levente Bajczi Date: Sun, 10 Nov 2024 21:46:14 +0100 Subject: [PATCH 1/5] Added support for _Atomic variable --- .../grammar/expression/ExpressionVisitor.java | 14 +++++++++++--- .../grammar/function/FunctionVisitor.java | 13 +++++++++---- 2 files changed, 20 insertions(+), 7 deletions(-) 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 39c85365fb..79b5e3ee7b 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 @@ -71,6 +71,7 @@ public class ExpressionVisitor extends CBaseVisitor> { protected final List preStatements = new ArrayList<>(); protected final List postStatements = new ArrayList<>(); protected final Deque>>> variables; + protected final Set> atomicVars; protected final Map, CDeclaration> functions; private final ParseContext parseContext; private final FunctionVisitor functionVisitor; @@ -80,6 +81,7 @@ public class ExpressionVisitor extends CBaseVisitor> { private final Logger uniqueWarningLogger; public ExpressionVisitor( + Set> atomicVars, ParseContext parseContext, FunctionVisitor functionVisitor, Deque>>> variables, @@ -87,6 +89,7 @@ public ExpressionVisitor( TypedefVisitor typedefVisitor, TypeVisitor typeVisitor, Logger uniqueWarningLogger) { + this.atomicVars = atomicVars; this.parseContext = parseContext; this.functionVisitor = functionVisitor; this.variables = variables; @@ -739,7 +742,12 @@ public Expr visitGccPrettyFunc(CParser.GccPrettyFuncContext ctx) { @Override public Expr visitPrimaryExpressionId(CParser.PrimaryExpressionIdContext ctx) { - return getVar(ctx.Identifier().getText()).getRef(); + final var variable = getVar(ctx.Identifier().getText()); + if (atomicVars.contains(variable)) { + preStatements.add(new CCall("__VERIFIER_atomic_begin", List.of(), parseContext)); + postStatements.add(new CCall("__VERIFIER_atomic_end", List.of(), parseContext)); + } + return variable.getRef(); } @Override @@ -979,7 +987,7 @@ public Function, Expr> visitPostfixExpressionIncrement( cexpr = new CExpr(expr, parseContext); // no need to truncate here, as left and right side types are the same CAssignment cAssignment = new CAssignment(primary, cexpr, "=", parseContext); - postStatements.add(cAssignment); + postStatements.add(0, cAssignment); functionVisitor.recordMetadata(ctx, cAssignment); functionVisitor.recordMetadata(ctx, cexpr); return primary; @@ -1000,7 +1008,7 @@ public Function, Expr> visitPostfixExpressionDecrement( cexpr = new CExpr(expr, parseContext); // no need to truncate here, as left and right side types are the same CAssignment cAssignment = new CAssignment(primary, cexpr, "=", parseContext); - postStatements.add(cAssignment); + postStatements.add(0, cAssignment); functionVisitor.recordMetadata(ctx, cAssignment); functionVisitor.recordMetadata(ctx, cexpr); return expr; diff --git a/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/grammar/function/FunctionVisitor.java b/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/grammar/function/FunctionVisitor.java index d45fe00e83..98f45b07e4 100644 --- a/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/grammar/function/FunctionVisitor.java +++ b/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/grammar/function/FunctionVisitor.java @@ -38,7 +38,6 @@ import hu.bme.mit.theta.core.type.arraytype.ArrayType; import hu.bme.mit.theta.core.type.booltype.BoolType; import hu.bme.mit.theta.frontend.ParseContext; -import hu.bme.mit.theta.frontend.transformation.ArchitectureConfig; import hu.bme.mit.theta.frontend.transformation.ArchitectureConfig.ArithmeticType; import hu.bme.mit.theta.frontend.transformation.grammar.expression.ExpressionVisitor; import hu.bme.mit.theta.frontend.transformation.grammar.preprocess.ArithmeticTrait; @@ -82,6 +81,7 @@ public void clear() { } private final Deque>>> variables; + private final Set> atomicVariables; private int anonCnt = 0; private final List> flatVariables; private final Map, CDeclaration> functions; @@ -104,8 +104,6 @@ private String getName(final String name) { } private void createVars(String name, CDeclaration declaration, CComplexType type) { - // checkState(declaration.getArrayDimensions().size() <= 1, "Currently, higher - // dimension arrays not supported"); Tuple2>> peek = variables.peek(); VarDecl varDecl = Var(getName(name), type.getSmtType()); if (peek.get2().containsKey(name)) { @@ -115,6 +113,9 @@ private void createVars(String name, CDeclaration declaration, CComplexType type } peek.get2().put(name, varDecl); flatVariables.add(varDecl); + if (declaration.getType().isAtomic()) { + atomicVariables.add(varDecl); + } parseContext.getMetadata().create(varDecl.getRef(), "cType", type); parseContext.getMetadata().create(varDecl.getName(), "cName", name); declaration.addVarDecl(varDecl); @@ -131,6 +132,7 @@ public FunctionVisitor(final ParseContext parseContext, Logger uniqueWarningLogg functions = new LinkedHashMap<>(); this.parseContext = parseContext; globalDeclUsageVisitor = new GlobalDeclUsageVisitor(declarationVisitor); + atomicVariables = new LinkedHashSet<>(); } @Override @@ -148,7 +150,7 @@ public CStatement visitCompilationUnit(CParser.CompilationUnitContext ctx) { // if arithemetic is set on efficient, we change it to either bv or int arithmetic here if (parseContext.getArithmetic() - == ArchitectureConfig.ArithmeticType + == ArithmeticType .efficient) { // if it wasn't on efficient, the check returns manual Set arithmeticTraits = BitwiseChecker.gatherArithmeticTraits(parseContext, globalUsages); @@ -315,6 +317,7 @@ public CStatement visitCaseStatement(CParser.CaseStatementContext ctx) { ctx.constantExpression() .accept( new ExpressionVisitor( + atomicVariables, parseContext, this, variables, @@ -612,6 +615,7 @@ public CStatement visitAssignmentExpressionAssignmentExpression( CParser.AssignmentExpressionAssignmentExpressionContext ctx) { ExpressionVisitor expressionVisitor = new ExpressionVisitor( + atomicVariables, parseContext, this, variables, @@ -737,6 +741,7 @@ public CStatement visitConditionalExpression(CParser.ConditionalExpressionContex ExpressionVisitor expressionVisitor = new ExpressionVisitor( + atomicVariables, parseContext, this, variables, From 9af341c7fd24bb952d83c98ae130c76fcf978035 Mon Sep 17 00:00:00 2001 From: Levente Bajczi Date: Sun, 10 Nov 2024 21:48:14 +0100 Subject: [PATCH 2/5] Version bump --- build.gradle.kts | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/build.gradle.kts b/build.gradle.kts index 8c3f9a43bb..88f64206e0 100644 --- a/build.gradle.kts +++ b/build.gradle.kts @@ -29,7 +29,7 @@ buildscript { allprojects { group = "hu.bme.mit.theta" - version = "6.7.2" + version = "6.7.3" apply(from = rootDir.resolve("gradle/shared-with-buildSrc/mirrors.gradle.kts")) } From d85d701e530136e09eac9592dd1d3ab221719830 Mon Sep 17 00:00:00 2001 From: Levente Bajczi Date: Mon, 11 Nov 2024 10:55:25 +0100 Subject: [PATCH 3/5] Instead of ATOMIC_BEGIN,_END, we use atomic flags for variables --- .../grammar/expression/ExpressionVisitor.java | 4 - .../grammar/function/FunctionVisitor.java | 16 +- .../model/statements/CFunction.java | 20 +- .../mit/theta/c2xcfa/FrontendXcfaBuilder.kt | 12 +- .../mit/theta/xcfa/analysis/XcfaAnalysis.kt | 14 +- .../main/java/hu/bme/mit/theta/xcfa/Utils.kt | 26 +- .../hu/bme/mit/theta/xcfa/model/Builders.kt | 432 ++++++++++-------- .../java/hu/bme/mit/theta/xcfa/model/XCFA.kt | 1 + 8 files changed, 314 insertions(+), 211 deletions(-) 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 79b5e3ee7b..15f9d3d548 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 @@ -743,10 +743,6 @@ public Expr visitGccPrettyFunc(CParser.GccPrettyFuncContext ctx) { @Override public Expr visitPrimaryExpressionId(CParser.PrimaryExpressionIdContext ctx) { final var variable = getVar(ctx.Identifier().getText()); - if (atomicVars.contains(variable)) { - preStatements.add(new CCall("__VERIFIER_atomic_begin", List.of(), parseContext)); - postStatements.add(new CCall("__VERIFIER_atomic_end", List.of(), parseContext)); - } return variable.getRef(); } diff --git a/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/grammar/function/FunctionVisitor.java b/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/grammar/function/FunctionVisitor.java index 98f45b07e4..596107bee2 100644 --- a/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/grammar/function/FunctionVisitor.java +++ b/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/grammar/function/FunctionVisitor.java @@ -76,6 +76,7 @@ public class FunctionVisitor extends CBaseVisitor { public void clear() { variables.clear(); + atomicVariables.clear(); flatVariables.clear(); functions.clear(); } @@ -138,6 +139,7 @@ public FunctionVisitor(final ParseContext parseContext, Logger uniqueWarningLogg @Override public CStatement visitCompilationUnit(CParser.CompilationUnitContext ctx) { variables.clear(); + atomicVariables.clear(); variables.push(Tuple2.of("", new LinkedHashMap<>())); flatVariables.clear(); functions.clear(); @@ -269,14 +271,24 @@ public CStatement visitFunctionDefinition(CParser.FunctionDefinitionContext ctx) CStatement accept = blockItemListContext.accept(this); variables.pop(); CFunction cFunction = - new CFunction(funcDecl, accept, new ArrayList<>(flatVariables), parseContext); + new CFunction( + funcDecl, + accept, + new ArrayList<>(flatVariables), + parseContext, + atomicVariables); recordMetadata(ctx, cFunction); return cFunction; } variables.pop(); CCompound cCompound = new CCompound(parseContext); CFunction cFunction = - new CFunction(funcDecl, cCompound, new ArrayList<>(flatVariables), parseContext); + new CFunction( + funcDecl, + cCompound, + new ArrayList<>(flatVariables), + parseContext, + atomicVariables); recordMetadata(ctx, cCompound); recordMetadata(ctx, cFunction); return cFunction; diff --git a/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/model/statements/CFunction.java b/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/model/statements/CFunction.java index 8cca542745..8da47ca0db 100644 --- a/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/model/statements/CFunction.java +++ b/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/model/statements/CFunction.java @@ -13,27 +13,35 @@ * See the License for the specific language governing permissions and * limitations under the License. */ - package hu.bme.mit.theta.frontend.transformation.model.statements; import hu.bme.mit.theta.core.decl.VarDecl; import hu.bme.mit.theta.frontend.ParseContext; import hu.bme.mit.theta.frontend.transformation.model.declaration.CDeclaration; - import java.util.List; +import java.util.Set; public class CFunction extends CStatement { private final CDeclaration funcDecl; private final CStatement compound; private final List> flatVariables; + private final Set> atomicVariables; - public CFunction(CDeclaration funcDecl, CStatement compound, List> flatVariables, ParseContext parseContext) { + public CFunction( + CDeclaration funcDecl, + CStatement compound, + List> flatVariables, + ParseContext parseContext, + Set> atomicVariables) { super(parseContext); this.funcDecl = funcDecl; this.compound = compound; this.flatVariables = flatVariables; - parseContext.getMetadata().lookupMetadata(funcDecl) + this.atomicVariables = atomicVariables; + parseContext + .getMetadata() + .lookupMetadata(funcDecl) .forEach((s, o) -> parseContext.getMetadata().create(this, s, o)); } @@ -53,4 +61,8 @@ public List> getFlatVariables() { public R accept(CStatementVisitor visitor, P param) { return visitor.visit(this, param); } + + public Set> getAtomicVariables() { + return atomicVariables; + } } diff --git a/subprojects/xcfa/c2xcfa/src/main/java/hu/bme/mit/theta/c2xcfa/FrontendXcfaBuilder.kt b/subprojects/xcfa/c2xcfa/src/main/java/hu/bme/mit/theta/c2xcfa/FrontendXcfaBuilder.kt index 0c922fc0b7..fe963cb479 100644 --- a/subprojects/xcfa/c2xcfa/src/main/java/hu/bme/mit/theta/c2xcfa/FrontendXcfaBuilder.kt +++ b/subprojects/xcfa/c2xcfa/src/main/java/hu/bme/mit/theta/c2xcfa/FrontendXcfaBuilder.kt @@ -106,7 +106,13 @@ class FrontendXcfaBuilder( "Not handling init expression of struct array ${globalDeclaration.get1()}", ) } - builder.addVar(XcfaGlobalVar(globalDeclaration.get2(), type.nullValue)) + builder.addVar( + XcfaGlobalVar( + globalDeclaration.get2(), + type.nullValue, + atomic = globalDeclaration.get1().type.isAtomic, + ) + ) if (type is CArray) { initStmtList.add( StmtLabel( @@ -203,6 +209,7 @@ class FrontendXcfaBuilder( ): XcfaProcedureBuilder { locationLut.clear() val flatVariables = function.flatVariables + val isAtomic = function.atomicVariables::contains val funcDecl = function.funcDecl val compound = function.compound val builder = @@ -238,6 +245,9 @@ class FrontendXcfaBuilder( for (flatVariable in flatVariables) { builder.addVar(flatVariable) + if (isAtomic(flatVariable)) { + builder.setAtomic(flatVariable) + } val type = CComplexType.getType(flatVariable.ref, parseContext) if ( (type is CArray || type is CStruct) && builder.getParams().none { it.first == flatVariable } 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 2fc5cbf6ba..115be3a907 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 @@ -228,9 +228,17 @@ fun getXcfaErrorPredicate( 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 + for (v1 in globalVars1) { + for (v2 in globalVars2) { + if ( + v1.globalVar == v2.globalVar && + !v1.globalVar.atomic && + (v1.access.isWritten || v2.access.isWritten) && + (v1.mutexes intersect v2.mutexes).isEmpty() + ) + return@Predicate true + } + } } false } 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 f48bd757d8..ffe0a44b5d 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 @@ -121,6 +121,8 @@ typealias AccessType = Pair typealias VarAccessMap = Map, AccessType> +typealias GlobalVarAccessMap = Map + val AccessType?.isRead get() = this?.first == true val AccessType?.isWritten @@ -245,8 +247,12 @@ fun XcfaLabel.collectVarsWithAccessType(): VarAccessMap = /** * Returns the global variables accessed by the label (the variables present in the given argument). */ -private fun XcfaLabel.collectGlobalVars(globalVars: Set>): VarAccessMap = - collectVarsWithAccessType().filter { labelVar -> globalVars.any { it == labelVar.key } } +private fun XcfaLabel.collectGlobalVars(globalVars: Set): GlobalVarAccessMap = + collectVarsWithAccessType() + .mapNotNull { labelVar -> + globalVars.firstOrNull { it.wrappedVar == labelVar.key }?.let { Pair(it, labelVar.value) } + } + .toMap() /** * Returns the global variables (potentially indirectly) accessed by the edge. If the edge starts an @@ -254,8 +260,8 @@ private fun XcfaLabel.collectGlobalVars(globalVars: Set>): VarAccessM * 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.collectIndirectGlobalVarAccesses(xcfa: XCFA): VarAccessMap { - val globalVars = xcfa.vars.map(XcfaGlobalVar::wrappedVar).toSet() +fun XcfaEdge.collectIndirectGlobalVarAccesses(xcfa: XCFA): GlobalVarAccessMap { + val globalVars = xcfa.vars val flatLabels = getFlatLabels() val mutexes = flatLabels.filterIsInstance().flatMap { it.acquiredMutexes }.toMutableSet() @@ -271,7 +277,7 @@ fun XcfaEdge.collectIndirectGlobalVarAccesses(xcfa: XCFA): VarAccessMap { * (read/write) and the set of mutexes that are needed to perform the variable access. */ class GlobalVarAccessWithMutexes( - val varDecl: VarDecl<*>, + val globalVar: XcfaGlobalVar, val access: AccessType, val mutexes: Set, ) @@ -287,7 +293,7 @@ fun XcfaEdge.getGlobalVarsWithNeededMutexes( xcfa: XCFA, currentMutexes: Set, ): List { - val globalVars = xcfa.vars.map(XcfaGlobalVar::wrappedVar).toSet() + val globalVars = xcfa.vars val neededMutexes = currentMutexes.toMutableSet() val accesses = mutableListOf() getFlatLabels().forEach { label -> @@ -299,7 +305,7 @@ fun XcfaEdge.getGlobalVarsWithNeededMutexes( vars.mapNotNull { (varDecl, accessType) -> if ( accesses.any { - it.varDecl == varDecl && (it.access == accessType && it.access == WRITE) + it.globalVar == varDecl && (it.access == accessType && it.access == WRITE) } ) { null @@ -320,10 +326,10 @@ fun XcfaEdge.getGlobalVarsWithNeededMutexes( * @return the set of encountered shared objects */ private fun XcfaEdge.collectGlobalVarsWithTraversal( - globalVars: Set>, + globalVars: Set, goFurther: Predicate, -): VarAccessMap { - val vars = mutableMapOf, AccessType>() +): GlobalVarAccessMap { + val vars = mutableMapOf() val exploredEdges = mutableListOf() val edgesToExplore = mutableListOf() edgesToExplore.add(this) 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 bf8d3e3730..4893216479 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 @@ -13,7 +13,6 @@ * See the License for the specific language governing permissions and * limitations under the License. */ - package hu.bme.mit.theta.xcfa.model import hu.bme.mit.theta.core.decl.VarDecl @@ -21,239 +20,298 @@ import hu.bme.mit.theta.core.type.Expr import hu.bme.mit.theta.core.type.Type import hu.bme.mit.theta.xcfa.passes.ProcedurePassManager import java.util.* +import kotlin.collections.LinkedHashSet -@DslMarker -annotation class XcfaDsl +@DslMarker annotation class XcfaDsl @XcfaDsl -class XcfaBuilder @JvmOverloads constructor( - var name: String, - private val vars: MutableSet = LinkedHashSet(), - val heapMap: MutableMap, VarDecl<*>> = LinkedHashMap(), - private val procedures: MutableSet = LinkedHashSet(), - private val initProcedures: MutableList>>> = ArrayList(), - val metaData: MutableMap = LinkedHashMap() +class XcfaBuilder +@JvmOverloads +constructor( + var name: String, + private val vars: MutableSet = LinkedHashSet(), + val heapMap: MutableMap, VarDecl<*>> = LinkedHashMap(), + private val procedures: MutableSet = LinkedHashSet(), + private val initProcedures: MutableList>>> = ArrayList(), + val metaData: MutableMap = LinkedHashMap(), ) { - fun getVars(): Set = vars - fun getProcedures(): Set = procedures - fun getInitProcedures(): List>>> = initProcedures - - fun build(): XCFA { - return XCFA( - name = name, - vars = vars, - procedureBuilders = procedures, - initProcedureBuilders = initProcedures - ) - } + fun getVars(): Set = vars - fun addVar(toAdd: XcfaGlobalVar) { - vars.add(toAdd) - } + fun getProcedures(): Set = procedures - fun addProcedure(toAdd: XcfaProcedureBuilder) { - procedures.add(toAdd) - toAdd.parent = this - } + fun getInitProcedures(): List>>> = initProcedures - fun addEntryPoint(toAdd: XcfaProcedureBuilder, params: List>) { - addProcedure(toAdd) - initProcedures.add(Pair(toAdd, params)) - } + fun build(): XCFA { + return XCFA( + name = name, + vars = vars, + procedureBuilders = procedures, + initProcedureBuilders = initProcedures, + ) + } + + fun addVar(toAdd: XcfaGlobalVar) { + vars.add(toAdd) + } + + fun addProcedure(toAdd: XcfaProcedureBuilder) { + procedures.add(toAdd) + toAdd.parent = this + } + + fun addEntryPoint(toAdd: XcfaProcedureBuilder, params: List>) { + addProcedure(toAdd) + initProcedures.add(Pair(toAdd, params)) + } } @XcfaDsl -class XcfaProcedureBuilder @JvmOverloads constructor( - var name: String, - val manager: ProcedurePassManager, - private val params: MutableList, ParamDirection>> = ArrayList(), - private val vars: MutableSet> = LinkedHashSet(), - private val locs: MutableSet = LinkedHashSet(), - private val edges: MutableSet = LinkedHashSet(), - val metaData: MutableMap = LinkedHashMap() +class XcfaProcedureBuilder +@JvmOverloads +constructor( + var name: String, + val manager: ProcedurePassManager, + private val params: MutableList, ParamDirection>> = ArrayList(), + private val vars: MutableSet> = LinkedHashSet(), + private val atomicVars: MutableSet> = LinkedHashSet(), + private val locs: MutableSet = LinkedHashSet(), + private val edges: MutableSet = LinkedHashSet(), + val metaData: MutableMap = LinkedHashMap(), ) { - lateinit var initLoc: XcfaLocation - private set - var finalLoc: Optional = Optional.empty() - private set - var errorLoc: Optional = Optional.empty() - private set - lateinit var parent: XcfaBuilder - private lateinit var built: XcfaProcedure - 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 - } + lateinit var initLoc: XcfaLocation + private set - fun getVars(): Set> = when { - this::optimized.isInitialized -> optimized.vars - this::partlyOptimized.isInitialized -> partlyOptimized.vars - else -> vars - } + var finalLoc: Optional = Optional.empty() + private set - fun getLocs(): Set = when { - this::optimized.isInitialized -> optimized.locs - this::partlyOptimized.isInitialized -> partlyOptimized.locs - else -> locs - } + var errorLoc: Optional = Optional.empty() + private set - fun getEdges(): Set = when { - this::optimized.isInitialized -> optimized.edges - this::partlyOptimized.isInitialized -> partlyOptimized.edges - else -> edges - } + lateinit var parent: XcfaBuilder + private lateinit var built: XcfaProcedure + private lateinit var optimized: XcfaProcedureBuilder + private lateinit var partlyOptimized: XcfaProcedureBuilder + private var lastOptimized: Int = -1 - fun optimize() { - if (!this::optimized.isInitialized) { - var that = this - for (pass in manager.passes.flatten()) { - that = pass.run(that) - } - optimized = that - } + fun getParams(): List, ParamDirection>> = + when { + this::optimized.isInitialized -> optimized.params + this::partlyOptimized.isInitialized -> partlyOptimized.params + else -> params } - 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) - } + fun getVars(): Set> = + when { + this::optimized.isInitialized -> optimized.vars + this::partlyOptimized.isInitialized -> partlyOptimized.vars + else -> vars + } - partlyOptimized = that - lastOptimized = phase - if (phase >= manager.passes.size - 1) optimized = that - return phase >= manager.passes.size - 1 + fun VarDecl<*>.isAtomic() = + when { + this@XcfaProcedureBuilder::optimized.isInitialized -> optimized.atomicVars.contains(this) + this@XcfaProcedureBuilder::partlyOptimized.isInitialized -> + partlyOptimized.vars.contains(this) + else -> atomicVars.contains(this) } - fun build(parent: XCFA): XcfaProcedure { - if (this::built.isInitialized) return built; - if (!this::optimized.isInitialized) optimize() - built = XcfaProcedure( - name = optimized.name, - params = optimized.params, - vars = optimized.vars, - locs = optimized.locs, - edges = optimized.edges, - initLoc = optimized.initLoc, - finalLoc = optimized.finalLoc, - errorLoc = optimized.errorLoc - ) - built.parent = parent - return built + fun getLocs(): Set = + when { + this::optimized.isInitialized -> optimized.locs + this::partlyOptimized.isInitialized -> partlyOptimized.locs + else -> locs } - fun addParam(toAdd: VarDecl<*>, dir: ParamDirection) { - check(!this::optimized.isInitialized) { "Cannot add/remove new elements after optimization passes!" } - params.add(Pair(toAdd, dir)) - vars.add(toAdd) + fun getEdges(): Set = + when { + this::optimized.isInitialized -> optimized.edges + this::partlyOptimized.isInitialized -> partlyOptimized.edges + else -> edges } - fun addVar(toAdd: VarDecl<*>) { - check(!this::optimized.isInitialized) { "Cannot add/remove new elements after optimization passes!" } - vars.add(toAdd) + fun optimize() { + if (!this::optimized.isInitialized) { + var that = this + 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) } - fun removeVar(toRemove: VarDecl<*>) { - check(!this::optimized.isInitialized) { "Cannot add/remove new elements after optimization passes!" } - vars.remove(toRemove) + 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() + built = + XcfaProcedure( + name = optimized.name, + params = optimized.params, + vars = optimized.vars, + locs = optimized.locs, + edges = optimized.edges, + initLoc = optimized.initLoc, + finalLoc = optimized.finalLoc, + errorLoc = optimized.errorLoc, + ) + built.parent = parent + return built + } + + fun addParam(toAdd: VarDecl<*>, dir: ParamDirection) { + check(!this::optimized.isInitialized) { + "Cannot add/remove new elements after optimization passes!" } + params.add(Pair(toAdd, dir)) + vars.add(toAdd) + } - @JvmOverloads - fun createErrorLoc(metaData: MetaData = EmptyMetaData) { - check(!this::optimized.isInitialized) { "Cannot add/remove new elements after optimization passes!" } - if (errorLoc.isEmpty) { - errorLoc = Optional.of(XcfaLocation(name + "_error", error = true, metadata = metaData)) - locs.add(errorLoc.get()) - } + fun addVar(toAdd: VarDecl<*>) { + check(!this::optimized.isInitialized) { + "Cannot add/remove new elements after optimization passes!" } + vars.add(toAdd) + } - @JvmOverloads - fun createFinalLoc(metaData: MetaData = EmptyMetaData) { - check(!this::optimized.isInitialized) { "Cannot add/remove new elements after optimization passes!" } - if (finalLoc.isEmpty) { - finalLoc = Optional.of(XcfaLocation(name + "_final", final = true, metadata = metaData)) - locs.add(finalLoc.get()) - } + fun setAtomic(v: VarDecl<*>) { + check(!this::optimized.isInitialized) { + "Cannot add/remove/modify elements after optimization passes!" } + atomicVars.add(v) + } - @JvmOverloads - fun createInitLoc(metaData: MetaData = EmptyMetaData) { - check(!this::optimized.isInitialized) { "Cannot add/remove new elements after optimization passes!" } - if (!this::initLoc.isInitialized) { - initLoc = XcfaLocation(name + "_init", initial = true, metadata = metaData) - locs.add(initLoc) - } + fun removeVar(toRemove: VarDecl<*>) { + check(!this::optimized.isInitialized) { + "Cannot add/remove new elements after optimization passes!" } + vars.remove(toRemove) + } - fun copyMetaLocs(from: XcfaProcedureBuilder) { - check(!this::optimized.isInitialized) { "Cannot add/remove new elements after optimization passes!" } - initLoc = from.initLoc - finalLoc = from.finalLoc - errorLoc = from.errorLoc + @JvmOverloads + fun createErrorLoc(metaData: MetaData = EmptyMetaData) { + check(!this::optimized.isInitialized) { + "Cannot add/remove new elements after optimization passes!" + } + if (errorLoc.isEmpty) { + errorLoc = Optional.of(XcfaLocation(name + "_error", error = true, metadata = metaData)) + locs.add(errorLoc.get()) } + } - fun addEdge(toAdd: XcfaEdge) { - check(!this::optimized.isInitialized) { "Cannot add/remove new elements after optimization passes!" } - addLoc(toAdd.source) - addLoc(toAdd.target) - edges.add(toAdd) - toAdd.source.outgoingEdges.add(toAdd) - toAdd.target.incomingEdges.add(toAdd) + @JvmOverloads + fun createFinalLoc(metaData: MetaData = EmptyMetaData) { + check(!this::optimized.isInitialized) { + "Cannot add/remove new elements after optimization passes!" } + if (finalLoc.isEmpty) { + finalLoc = Optional.of(XcfaLocation(name + "_final", final = true, metadata = metaData)) + locs.add(finalLoc.get()) + } + } - fun addLoc(toAdd: XcfaLocation) { - check(!this::optimized.isInitialized) { "Cannot add/remove new elements after optimization passes!" } - if (!locs.contains(toAdd)) { - check(!toAdd.error) - check(!toAdd.initial) - check(!toAdd.final) - locs.add(toAdd) - } + @JvmOverloads + fun createInitLoc(metaData: MetaData = EmptyMetaData) { + check(!this::optimized.isInitialized) { + "Cannot add/remove new elements after optimization passes!" } + if (!this::initLoc.isInitialized) { + initLoc = XcfaLocation(name + "_init", initial = true, metadata = metaData) + locs.add(initLoc) + } + } - fun removeEdge(toRemove: XcfaEdge) { - 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 copyMetaLocs(from: XcfaProcedureBuilder) { + check(!this::optimized.isInitialized) { + "Cannot add/remove new elements after optimization passes!" + } + initLoc = from.initLoc + finalLoc = from.finalLoc + errorLoc = from.errorLoc + } + + fun addEdge(toAdd: XcfaEdge) { + check(!this::optimized.isInitialized) { + "Cannot add/remove new elements after optimization passes!" + } + addLoc(toAdd.source) + addLoc(toAdd.target) + edges.add(toAdd) + toAdd.source.outgoingEdges.add(toAdd) + toAdd.target.incomingEdges.add(toAdd) + } + + fun addLoc(toAdd: XcfaLocation) { + check(!this::optimized.isInitialized) { + "Cannot add/remove new elements after optimization passes!" + } + if (!locs.contains(toAdd)) { + check(!toAdd.error) + check(!toAdd.initial) + check(!toAdd.final) + locs.add(toAdd) } + } - fun removeLoc(toRemove: XcfaLocation) { - check(!this::optimized.isInitialized) { "Cannot add/remove new elements after optimization passes!" } - locs.remove(toRemove) + fun removeEdge(toRemove: XcfaEdge) { + 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!" + } + locs.remove(toRemove) + } - fun removeLocs(pred: (XcfaLocation) -> Boolean) { - check(!this::optimized.isInitialized) { "Cannot add/remove new elements after optimization passes!" } - while (locs.any(pred)) { - locs.removeIf(pred) - edges.removeIf { - pred(it.source).also { removing -> - if (removing) { - it.target.incomingEdges.remove(it) - } - } - } + fun removeLocs(pred: (XcfaLocation) -> Boolean) { + check(!this::optimized.isInitialized) { + "Cannot add/remove new elements after optimization passes!" + } + while (locs.any(pred)) { + locs.removeIf(pred) + edges.removeIf { + pred(it.source).also { removing -> + if (removing) { + it.target.incomingEdges.remove(it) + } } + } } + } - fun changeVars(varLut: Map, VarDecl<*>>) { - 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])) } - val savedParams = ArrayList(params) - params.clear() - savedParams.forEach { params.add(Pair(checkNotNull(varLut[it.first]), it.second)) } + fun changeVars(varLut: Map, VarDecl<*>>) { + check(!this::optimized.isInitialized) { + "Cannot add/remove new elements after optimization passes!" } -} \ No newline at end of file + val savedVars = ArrayList(vars) + vars.clear() + savedVars.forEach { vars.add(checkNotNull(varLut[it])) } + val savedParams = ArrayList(params) + params.clear() + savedParams.forEach { params.add(Pair(checkNotNull(varLut[it.first]), it.second)) } + } +} 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 107af4e127..a36d813310 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 @@ -154,6 +154,7 @@ constructor( val wrappedVar: VarDecl<*>, val initValue: LitExpr<*>, val threadLocal: Boolean = false, + val atomic: Boolean = false, ) enum class ParamDirection { From 978ac72da0f93d60aac6ebcb3225ca73fb4d3830 Mon Sep 17 00:00:00 2001 From: Levente Bajczi Date: Mon, 11 Nov 2024 16:13:17 +0100 Subject: [PATCH 4/5] revert poststatement-ordering --- .../transformation/grammar/expression/ExpressionVisitor.java | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) 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 15f9d3d548..e02516a644 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 @@ -983,7 +983,7 @@ public Function, Expr> visitPostfixExpressionIncrement( cexpr = new CExpr(expr, parseContext); // no need to truncate here, as left and right side types are the same CAssignment cAssignment = new CAssignment(primary, cexpr, "=", parseContext); - postStatements.add(0, cAssignment); + postStatements.add(cAssignment); functionVisitor.recordMetadata(ctx, cAssignment); functionVisitor.recordMetadata(ctx, cexpr); return primary; @@ -1004,7 +1004,7 @@ public Function, Expr> visitPostfixExpressionDecrement( cexpr = new CExpr(expr, parseContext); // no need to truncate here, as left and right side types are the same CAssignment cAssignment = new CAssignment(primary, cexpr, "=", parseContext); - postStatements.add(0, cAssignment); + postStatements.add(cAssignment); functionVisitor.recordMetadata(ctx, cAssignment); functionVisitor.recordMetadata(ctx, cexpr); return expr; From 6c5384a991bb9c161e8251604ad8c838d03a395e Mon Sep 17 00:00:00 2001 From: Levente Bajczi Date: Mon, 11 Nov 2024 17:44:06 +0100 Subject: [PATCH 5/5] vars -> globalvars (merge fix) --- .../xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/Utils.kt | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) 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 92e025866d..ab6378d3f6 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 @@ -261,7 +261,7 @@ private fun XcfaLabel.collectGlobalVars(globalVars: Set): GlobalV * second is similar for write access. */ fun XcfaEdge.collectIndirectGlobalVarAccesses(xcfa: XCFA): GlobalVarAccessMap { - val globalVars = xcfa.vars + val globalVars = xcfa.globalVars val flatLabels = getFlatLabels() val mutexes = flatLabels.filterIsInstance().flatMap { it.acquiredMutexes }.toMutableSet() @@ -293,7 +293,7 @@ fun XcfaEdge.getGlobalVarsWithNeededMutexes( xcfa: XCFA, currentMutexes: Set, ): List { - val globalVars = xcfa.vars + val globalVars = xcfa.globalVars val neededMutexes = currentMutexes.toMutableSet() val accesses = mutableListOf() getFlatLabels().forEach { label ->