Skip to content

Commit

Permalink
Merge branch 'master' into portfolio-update
Browse files Browse the repository at this point in the history
  • Loading branch information
leventeBajczi authored Nov 11, 2024
2 parents 283c651 + f042054 commit 236c2f9
Show file tree
Hide file tree
Showing 8 changed files with 100 additions and 25 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -71,6 +71,7 @@ public class ExpressionVisitor extends CBaseVisitor<Expr<?>> {
protected final List<CStatement> preStatements = new ArrayList<>();
protected final List<CStatement> postStatements = new ArrayList<>();
protected final Deque<Tuple2<String, Map<String, VarDecl<?>>>> variables;
protected final Set<VarDecl<?>> atomicVars;
protected final Map<VarDecl<?>, CDeclaration> functions;
private final ParseContext parseContext;
private final FunctionVisitor functionVisitor;
Expand All @@ -80,13 +81,15 @@ public class ExpressionVisitor extends CBaseVisitor<Expr<?>> {
private final Logger uniqueWarningLogger;

public ExpressionVisitor(
Set<VarDecl<?>> atomicVars,
ParseContext parseContext,
FunctionVisitor functionVisitor,
Deque<Tuple2<String, Map<String, VarDecl<?>>>> variables,
Map<VarDecl<?>, CDeclaration> functions,
TypedefVisitor typedefVisitor,
TypeVisitor typeVisitor,
Logger uniqueWarningLogger) {
this.atomicVars = atomicVars;
this.parseContext = parseContext;
this.functionVisitor = functionVisitor;
this.variables = variables;
Expand Down Expand Up @@ -739,7 +742,8 @@ 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());
return variable.getRef();
}

@Override
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down Expand Up @@ -77,11 +76,13 @@ public class FunctionVisitor extends CBaseVisitor<CStatement> {

public void clear() {
variables.clear();
atomicVariables.clear();
flatVariables.clear();
functions.clear();
}

private final Deque<Tuple2<String, Map<String, VarDecl<?>>>> variables;
private final Set<VarDecl<?>> atomicVariables;
private int anonCnt = 0;
private final List<VarDecl<?>> flatVariables;
private final Map<VarDecl<?>, CDeclaration> functions;
Expand All @@ -104,8 +105,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<String, Map<String, VarDecl<?>>> peek = variables.peek();
VarDecl<?> varDecl = Var(getName(name), type.getSmtType());
if (peek.get2().containsKey(name)) {
Expand All @@ -115,6 +114,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);
Expand All @@ -131,11 +133,13 @@ public FunctionVisitor(final ParseContext parseContext, Logger uniqueWarningLogg
functions = new LinkedHashMap<>();
this.parseContext = parseContext;
globalDeclUsageVisitor = new GlobalDeclUsageVisitor(declarationVisitor);
atomicVariables = new LinkedHashSet<>();
}

@Override
public CStatement visitCompilationUnit(CParser.CompilationUnitContext ctx) {
variables.clear();
atomicVariables.clear();
variables.push(Tuple2.of("", new LinkedHashMap<>()));
flatVariables.clear();
functions.clear();
Expand All @@ -148,7 +152,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<ArithmeticTrait> arithmeticTraits =
BitwiseChecker.gatherArithmeticTraits(parseContext, globalUsages);
Expand Down Expand Up @@ -267,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;
Expand Down Expand Up @@ -315,6 +329,7 @@ public CStatement visitCaseStatement(CParser.CaseStatementContext ctx) {
ctx.constantExpression()
.accept(
new ExpressionVisitor(
atomicVariables,
parseContext,
this,
variables,
Expand Down Expand Up @@ -612,6 +627,7 @@ public CStatement visitAssignmentExpressionAssignmentExpression(
CParser.AssignmentExpressionAssignmentExpressionContext ctx) {
ExpressionVisitor expressionVisitor =
new ExpressionVisitor(
atomicVariables,
parseContext,
this,
variables,
Expand Down Expand Up @@ -737,6 +753,7 @@ public CStatement visitConditionalExpression(CParser.ConditionalExpressionContex

ExpressionVisitor expressionVisitor =
new ExpressionVisitor(
atomicVariables,
parseContext,
this,
variables,
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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<VarDecl<?>> flatVariables;
private final Set<VarDecl<?>> atomicVariables;

public CFunction(CDeclaration funcDecl, CStatement compound, List<VarDecl<?>> flatVariables, ParseContext parseContext) {
public CFunction(
CDeclaration funcDecl,
CStatement compound,
List<VarDecl<?>> flatVariables,
ParseContext parseContext,
Set<VarDecl<?>> 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));
}

Expand All @@ -53,4 +61,8 @@ public List<VarDecl<?>> getFlatVariables() {
public <P, R> R accept(CStatementVisitor<P, R> visitor, P param) {
return visitor.visit(this, param);
}

public Set<VarDecl<?>> getAtomicVariables() {
return atomicVariables;
}
}
Original file line number Diff line number Diff line change
Expand Up @@ -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(
Expand Down Expand Up @@ -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 =
Expand Down Expand Up @@ -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 }
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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
}
Expand Down
26 changes: 16 additions & 10 deletions subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/Utils.kt
Original file line number Diff line number Diff line change
Expand Up @@ -121,6 +121,8 @@ typealias AccessType = Pair<Boolean, Boolean>

typealias VarAccessMap = Map<VarDecl<*>, AccessType>

typealias GlobalVarAccessMap = Map<XcfaGlobalVar, AccessType>

val AccessType?.isRead
get() = this?.first == true
val AccessType?.isWritten
Expand Down Expand Up @@ -245,17 +247,21 @@ 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<VarDecl<*>>): VarAccessMap =
collectVarsWithAccessType().filter { labelVar -> globalVars.any { it == labelVar.key } }
private fun XcfaLabel.collectGlobalVars(globalVars: Set<XcfaGlobalVar>): 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
* 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.collectIndirectGlobalVarAccesses(xcfa: XCFA): VarAccessMap {
val globalVars = xcfa.globalVars.map(XcfaGlobalVar::wrappedVar).toSet()
fun XcfaEdge.collectIndirectGlobalVarAccesses(xcfa: XCFA): GlobalVarAccessMap {
val globalVars = xcfa.globalVars
val flatLabels = getFlatLabels()
val mutexes =
flatLabels.filterIsInstance<FenceLabel>().flatMap { it.acquiredMutexes }.toMutableSet()
Expand All @@ -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<String>,
)
Expand All @@ -287,7 +293,7 @@ fun XcfaEdge.getGlobalVarsWithNeededMutexes(
xcfa: XCFA,
currentMutexes: Set<String>,
): List<GlobalVarAccessWithMutexes> {
val globalVars = xcfa.globalVars.map(XcfaGlobalVar::wrappedVar).toSet()
val globalVars = xcfa.globalVars
val neededMutexes = currentMutexes.toMutableSet()
val accesses = mutableListOf<GlobalVarAccessWithMutexes>()
getFlatLabels().forEach { label ->
Expand All @@ -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
Expand All @@ -320,10 +326,10 @@ fun XcfaEdge.getGlobalVarsWithNeededMutexes(
* @return the set of encountered shared objects
*/
private fun XcfaEdge.collectGlobalVarsWithTraversal(
globalVars: Set<VarDecl<*>>,
globalVars: Set<XcfaGlobalVar>,
goFurther: Predicate<XcfaEdge>,
): VarAccessMap {
val vars = mutableMapOf<VarDecl<*>, AccessType>()
): GlobalVarAccessMap {
val vars = mutableMapOf<XcfaGlobalVar, AccessType>()
val exploredEdges = mutableListOf<XcfaEdge>()
val edgesToExplore = mutableListOf<XcfaEdge>()
edgesToExplore.add(this)
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -20,6 +20,7 @@ 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

Expand Down Expand Up @@ -75,6 +76,7 @@ constructor(
val manager: ProcedurePassManager,
private val params: MutableList<Pair<VarDecl<*>, ParamDirection>> = ArrayList(),
private val vars: MutableSet<VarDecl<*>> = LinkedHashSet(),
private val atomicVars: MutableSet<VarDecl<*>> = LinkedHashSet(),
private val locs: MutableSet<XcfaLocation> = LinkedHashSet(),
private val edges: MutableSet<XcfaEdge> = LinkedHashSet(),
val metaData: MutableMap<String, Any> = LinkedHashMap(),
Expand Down Expand Up @@ -109,6 +111,14 @@ constructor(
else -> vars
}

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 getLocs(): Set<XcfaLocation> =
when {
this::optimized.isInitialized -> optimized.locs
Expand Down Expand Up @@ -184,6 +194,13 @@ constructor(
vars.add(toAdd)
}

fun setAtomic(v: VarDecl<*>) {
check(!this::optimized.isInitialized) {
"Cannot add/remove/modify elements after optimization passes!"
}
atomicVars.add(v)
}

fun removeVar(toRemove: VarDecl<*>) {
check(!this::optimized.isInitialized) {
"Cannot add/remove new elements after optimization passes!"
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -155,6 +155,7 @@ constructor(
val wrappedVar: VarDecl<*>,
val initValue: LitExpr<*>,
val threadLocal: Boolean = false,
val atomic: Boolean = false,
)

enum class ParamDirection {
Expand Down

0 comments on commit 236c2f9

Please sign in to comment.