From 2e797b9518082b0ce35ff505ba6c466a2101e3a7 Mon Sep 17 00:00:00 2001 From: Levente Bajczi Date: Thu, 14 Nov 2024 00:27:56 +0100 Subject: [PATCH] Added back atomic_begin,_end, and a pass to remove them afterwards. --- .../grammar/expression/ExpressionVisitor.java | 8 ++- .../theta/xcfa/passes/ProcedurePassManager.kt | 1 + .../mit/theta/xcfa/passes/RemoveAtomics.kt | 51 +++++++++++++++++++ 3 files changed, 58 insertions(+), 2 deletions(-) create mode 100644 subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/RemoveAtomics.kt 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 e02516a644..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 @@ -743,6 +743,10 @@ 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(); } @@ -983,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; @@ -1004,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/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 0e624b12d3..89a0808921 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 @@ -70,6 +70,7 @@ class CPasses(checkOverflow: Boolean, parseContext: ParseContext, uniqueWarningL UnusedLocRemovalPass(), ), listOf(FetchExecuteWriteback(parseContext)), + listOf(RemoveAtomics()), ) class ChcPasses(parseContext: ParseContext, uniqueWarningLogger: Logger) : diff --git a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/RemoveAtomics.kt b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/RemoveAtomics.kt new file mode 100644 index 0000000000..58ca3bd7ba --- /dev/null +++ b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/RemoveAtomics.kt @@ -0,0 +1,51 @@ +/* + * Copyright 2024 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.passes + +import hu.bme.mit.theta.xcfa.getFlatLabels +import hu.bme.mit.theta.xcfa.model.FenceLabel +import hu.bme.mit.theta.xcfa.model.SequenceLabel +import hu.bme.mit.theta.xcfa.model.XcfaProcedureBuilder + +class RemoveAtomics : ProcedurePass { + + override fun run(builder: XcfaProcedureBuilder): XcfaProcedureBuilder { + for (xcfaEdge in LinkedHashSet(builder.getEdges())) { + val labels = xcfaEdge.getFlatLabels() + val (beginIndex, beginLabel) = + labels + .mapIndexed { i1, i2 -> Pair(i1, i2) } + .firstOrNull { + it.second is FenceLabel && (it.second as FenceLabel).labels.contains("ATOMIC_BEGIN") + } ?: continue + val (endIndex, endLabel) = + labels + .mapIndexed { i1, i2 -> Pair(i1, i2) } + .lastOrNull { + it.second is FenceLabel && (it.second as FenceLabel).labels.contains("ATOMIC_END") + } ?: continue + val newLabels = + labels.subList(0, beginIndex) + + labels.subList(beginIndex + 1, endIndex).filter { + it !is FenceLabel || !it.labels.contains("ATOMIC_") + } + + labels.subList(endIndex + 1, labels.size) + builder.removeEdge(xcfaEdge) + builder.addEdge(xcfaEdge.withLabel(SequenceLabel(newLabels))) + } + return builder + } +}