diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/boogie/PthreadsProcedures.java b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/boogie/PthreadsProcedures.java index cbe5708763..148df0ebc5 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/boogie/PthreadsProcedures.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/boogie/PthreadsProcedures.java @@ -15,12 +15,15 @@ public static boolean handlePthreadsFunctions(VisitorBoogie visitor, Call_cmdCon case "pthread_cond_wait": case "pthread_cond_signal": case "pthread_cond_broadcast": - case "pthread_exit": case "pthread_mutex_destroy": // TODO: These are skipped for now VisitorBoogie.logger.warn( "Skipped call to {} because the function is not supported right now.", funcName); return true; + case "pthread_exit": + final Expression retVal = (Expression) ctx.call_params().exprs().expr(0).accept(visitor); + visitor.addEvent(EventFactory.newFunctionReturn(retVal)); + return true; case "pthread_mutex_init": mutexInit(visitor, ctx); return true; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/boogie/VisitorBoogie.java b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/boogie/VisitorBoogie.java index 4245c2fbe6..ddba204e27 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/boogie/VisitorBoogie.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/boogie/VisitorBoogie.java @@ -173,6 +173,9 @@ private void visitDeclarations(MainContext ctx) { for (Func_declContext funDecContext : ctx.func_decl()) { registerBoogieFunction(funDecContext); } + for (Proc_declContext procDecContext : ctx.proc_decl()) { + registerProcedure(procDecContext); + } for (Const_declContext constDecContext : ctx.const_decl()) { registerConstants(constDecContext); } @@ -182,9 +185,6 @@ private void visitDeclarations(MainContext ctx) { for (Var_declContext varDecContext : ctx.var_decl()) { visitVar_decl(varDecContext); } - for (Proc_declContext procDecContext : ctx.proc_decl()) { - registerProcedure(procDecContext); - } //FIXME: Some Svcomp loop benchmarks reference declared but unassigned constants!? // Those should probably be non-deterministic, but we set them to zero here to match our previous semantics. diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/SyntacticContextAnalysis.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/SyntacticContextAnalysis.java index 37ff47d9e9..4fbbe508a9 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/SyntacticContextAnalysis.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/SyntacticContextAnalysis.java @@ -3,8 +3,8 @@ import com.dat3m.dartagnan.program.Program; import com.dat3m.dartagnan.program.Thread; import com.dat3m.dartagnan.program.event.core.Event; -import com.dat3m.dartagnan.program.event.core.annotations.FunCall; -import com.dat3m.dartagnan.program.event.core.annotations.FunRet; +import com.dat3m.dartagnan.program.event.core.annotations.FunCallMarker; +import com.dat3m.dartagnan.program.event.core.annotations.FunReturnMarker; import com.dat3m.dartagnan.program.event.metadata.SourceLocation; import com.google.common.collect.ImmutableList; import com.google.common.collect.Iterables; @@ -66,15 +66,15 @@ public String toString() { } public static class CallContext implements Context { - private final FunCall funCall; + private final FunCallMarker funCallMarker; - private CallContext(FunCall funCall) { this.funCall = funCall; } + private CallContext(FunCallMarker funCallMarker) { this.funCallMarker = funCallMarker; } - public FunCall getFunctionCall() { return this.funCall; } + public FunCallMarker getFunctionCall() { return this.funCallMarker; } @Override public String toString() { - return String.format("%s %s", funCall.getFunctionName(), getSourceLocationString(funCall)); + return String.format("%s %s", funCallMarker.getFunctionName(), getSourceLocationString(funCallMarker)); } } @@ -161,9 +161,9 @@ private void run(Thread thread, LoopAnalysis loops) { infoMap.put(ev, new Info(ev, copyOfCurContextStack)); // TODO: The above could be made more efficient by sharing unchanged context - if (ev instanceof FunCall fc) { + if (ev instanceof FunCallMarker fc) { curContextStack.push(new CallContext(fc)); - } else if (ev instanceof FunRet) { + } else if (ev instanceof FunReturnMarker) { assert curContextStack.peek() instanceof CallContext; curContextStack.pop(); } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/EventFactory.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/EventFactory.java index cf52f06501..fcac320c18 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/EventFactory.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/EventFactory.java @@ -14,8 +14,8 @@ import com.dat3m.dartagnan.program.event.arch.ptx.PTXRedOp; import com.dat3m.dartagnan.program.event.arch.tso.TSOXchg; import com.dat3m.dartagnan.program.event.core.*; -import com.dat3m.dartagnan.program.event.core.annotations.FunCall; -import com.dat3m.dartagnan.program.event.core.annotations.FunRet; +import com.dat3m.dartagnan.program.event.core.annotations.FunCallMarker; +import com.dat3m.dartagnan.program.event.core.annotations.FunReturnMarker; import com.dat3m.dartagnan.program.event.core.annotations.StringAnnotation; import com.dat3m.dartagnan.program.event.core.rmw.RMWStore; import com.dat3m.dartagnan.program.event.core.rmw.RMWStoreExclusive; @@ -145,12 +145,12 @@ public static Skip newSkip() { return new Skip(); } - public static FunCall newFunctionCall(String funName) { - return new FunCall(funName); + public static FunCallMarker newFunctionCallMarker(String funName) { + return new FunCallMarker(funName); } - public static FunRet newFunctionReturn(String funName) { - return new FunRet(funName); + public static FunReturnMarker newFunctionReturnMarker(String funName) { + return new FunReturnMarker(funName); } public static StringAnnotation newStringAnnotation(String annotation) { diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/common/FenceBase.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/common/FenceBase.java index a7692abdd3..7c8b89d0b9 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/common/FenceBase.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/common/FenceBase.java @@ -14,7 +14,7 @@ public FenceBase(String name, String mo) { this.mo = mo; this.addTags(Tag.VISIBLE, Tag.FENCE); if (mo != null && !mo.isEmpty()) { - this.tags.add(mo); + addTags(mo); } } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/AbstractEvent.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/AbstractEvent.java index 9cb3634c78..1b6857aacd 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/AbstractEvent.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/AbstractEvent.java @@ -17,14 +17,15 @@ public abstract class AbstractEvent implements Event { - protected final MetadataMap metadataMap = new MetadataMap(); - protected final Set tags; - protected Function function; // The thread this event belongs to + private final MetadataMap metadataMap = new MetadataMap(); + private final Set tags; + private final Set currentUsers = new HashSet<>(); // This id is dynamically changing during processing. - protected transient int globalId = -1; // (Global) ID within a program + private transient int globalId = -1; // (Global) ID within a program + + private transient Function function; // The function this event belongs to private transient AbstractEvent successor; private transient AbstractEvent predecessor; - private final Set currentUsers = new HashSet<>(); protected AbstractEvent() { tags = new HashSet<>(); @@ -33,7 +34,6 @@ protected AbstractEvent() { protected AbstractEvent(AbstractEvent other) { copyAllMetadataFrom(other); this.tags = other.tags; // TODO: Dangerous code! A Copy-on-Write Set should be used (e.g. PersistentSet/Map) - this.function = other.function; } @Override @@ -68,8 +68,7 @@ public Thread getThread() { @Override public void replaceAllUsages(Event replacement) { final Map replacementMap = Map.of(this, replacement); - - new ArrayList<>(getUsers()).forEach(e -> e.updateReferences(replacementMap)); + List.copyOf(getUsers()).forEach(e -> e.updateReferences(replacementMap)); } // ============================================ Metadata ============================================ diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/ExecutionStatus.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/ExecutionStatus.java index d1aa0f1927..198245e552 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/ExecutionStatus.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/ExecutionStatus.java @@ -1,6 +1,7 @@ package com.dat3m.dartagnan.program.event.core; import com.dat3m.dartagnan.encoding.EncodingContext; +import com.dat3m.dartagnan.expression.type.BooleanType; import com.dat3m.dartagnan.expression.type.IntegerType; import com.dat3m.dartagnan.expression.type.Type; import com.dat3m.dartagnan.program.Register; @@ -55,31 +56,36 @@ public boolean doesTrackDep() { @Override public String defaultString() { - return register + " <- status(" + event.toString() + ")"; + return register + " <- not_exec(" + event + ")"; } @Override public BooleanFormula encodeExec(EncodingContext context) { - FormulaManager formulaManager = context.getFormulaManager(); - BooleanFormulaManager booleanFormulaManager = context.getBooleanFormulaManager(); - Type type = register.getType(); - BooleanFormula eventExecuted = context.execution(event); - Formula result = context.result(this); + final FormulaManager fmgr = context.getFormulaManager(); + final BooleanFormulaManager bmgr = context.getBooleanFormulaManager(); + final Type type = register.getType(); + final BooleanFormula eventExecuted = context.execution(event); + final Formula result = context.result(this); + if (type instanceof IntegerType integerType) { - Formula one; + final Formula one; if (integerType.isMathematical()) { - IntegerFormulaManager integerFormulaManager = formulaManager.getIntegerFormulaManager(); + IntegerFormulaManager integerFormulaManager = fmgr.getIntegerFormulaManager(); one = integerFormulaManager.makeNumber(1); } else { - BitvectorFormulaManager bitvectorFormulaManager = formulaManager.getBitvectorFormulaManager(); + BitvectorFormulaManager bitvectorFormulaManager = fmgr.getBitvectorFormulaManager(); int bitWidth = integerType.getBitWidth(); one = bitvectorFormulaManager.makeBitvector(bitWidth, 1); } - return booleanFormulaManager.and(super.encodeExec(context), - booleanFormulaManager.implication(eventExecuted, - context.equalZero(result)), - booleanFormulaManager.or(eventExecuted, - context.equal(result, one))); + return bmgr.and(super.encodeExec(context), + bmgr.ifThenElse(eventExecuted, context.equalZero(result), context.equal(result, one)) + ); + } else if (type instanceof BooleanType) { + //TODO: We have "result == not exec(event)", because we use 0/false for executed events. + // The reason is that ExecutionStatus follows the behavior of Store-Conditionals on hardware. + // However, this is very counterintuitive and I think we should return 1/true on success and instead + // change the compilation of Store-Conditional to invert the value. + return bmgr.and(super.encodeExec(context), context.equal(result, bmgr.not(eventExecuted))); } throw new UnsupportedOperationException(String.format("Encoding ExecutionStatus on type %s.", type)); } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/annotations/FunCall.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/annotations/FunCallMarker.java similarity index 60% rename from dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/annotations/FunCall.java rename to dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/annotations/FunCallMarker.java index e05191a9f0..44960b5efb 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/annotations/FunCall.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/annotations/FunCallMarker.java @@ -1,15 +1,15 @@ package com.dat3m.dartagnan.program.event.core.annotations; -public class FunCall extends StringAnnotation { +public class FunCallMarker extends StringAnnotation { private final String funName; - public FunCall(String funName) { + public FunCallMarker(String funName) { super("=== Calling " + funName + " ==="); this.funName = funName; } - protected FunCall(FunCall other) { + protected FunCallMarker(FunCallMarker other) { super(other); this.funName = other.funName; } @@ -19,7 +19,7 @@ public String getFunctionName() { } @Override - public FunCall getCopy() { - return new FunCall(this); + public FunCallMarker getCopy() { + return new FunCallMarker(this); } } \ No newline at end of file diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/annotations/FunRet.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/annotations/FunReturnMarker.java similarity index 59% rename from dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/annotations/FunRet.java rename to dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/annotations/FunReturnMarker.java index 854daae84b..a7fa55c700 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/annotations/FunRet.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/annotations/FunReturnMarker.java @@ -1,15 +1,15 @@ package com.dat3m.dartagnan.program.event.core.annotations; -public class FunRet extends StringAnnotation { +public class FunReturnMarker extends StringAnnotation { private final String funName; - public FunRet(String funName) { + public FunReturnMarker(String funName) { super("=== Returning from " + funName + " ==="); this.funName = funName; } - protected FunRet(FunRet other) { + protected FunReturnMarker(FunReturnMarker other) { super(other); this.funName = other.funName; } @@ -19,7 +19,7 @@ public String getFunctionName() { } @Override - public FunRet getCopy() { - return new FunRet(this); + public FunReturnMarker getCopy() { + return new FunReturnMarker(this); } } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/functions/DirectFunctionCall.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/functions/DirectFunctionCall.java index 007138edca..237de9a306 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/functions/DirectFunctionCall.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/functions/DirectFunctionCall.java @@ -32,6 +32,7 @@ protected DirectFunctionCall(Function func, List arguments) { } protected DirectFunctionCall(DirectFunctionCall other) { + super(other); this.callTarget = other.callTarget; this.arguments = new ArrayList<>(other.arguments); } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/svcomp/EndAtomic.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/svcomp/EndAtomic.java index cb0b4d8375..559ebb3565 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/svcomp/EndAtomic.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/svcomp/EndAtomic.java @@ -49,7 +49,7 @@ public List getBlock() { public void runLocalAnalysis(Program program, Context context) { //===== Temporary fix to rematch atomic blocks correctly ===== BranchEquivalence eq = context.requires(BranchEquivalence.class); - List begins = this.function.getEvents() + List begins = this.getFunction().getEvents() .stream().filter(x -> x instanceof BeginAtomic && eq.isReachableFrom(x, this)) .toList(); this.begin = (BeginAtomic) begins.get(begins.size() - 1); diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/DynamicPureLoopCutting.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/DynamicPureLoopCutting.java index f9bf7c8d5e..351db6e925 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/DynamicPureLoopCutting.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/DynamicPureLoopCutting.java @@ -2,7 +2,7 @@ import com.dat3m.dartagnan.expression.Expression; import com.dat3m.dartagnan.expression.ExpressionFactory; -import com.dat3m.dartagnan.expression.type.IntegerType; +import com.dat3m.dartagnan.expression.type.Type; import com.dat3m.dartagnan.expression.type.TypeFactory; import com.dat3m.dartagnan.program.Program; import com.dat3m.dartagnan.program.Register; @@ -122,13 +122,11 @@ private void insertSideEffectChecks(IterationData iter) { final List sideEffects = iter.sideEffects; final List trackingRegs = new ArrayList<>(); + final Type type = TypeFactory.getInstance().getBooleanType(); Event insertionPoint = iterInfo.getIterationEnd(); - IntegerType type = TypeFactory.getInstance().getArchType(); for (int i = 0; i < sideEffects.size(); i++) { final Event sideEffect = sideEffects.get(i); - final Register trackingReg = thread.newRegister( - String.format("Loop%s_%s_%s", loopNumber, iterNumber, i), - type); + final Register trackingReg = thread.newRegister(String.format("Loop%s_%s_%s", loopNumber, iterNumber, i), type); trackingRegs.add(trackingReg); final Event execCheck = EventFactory.newExecutionStatus(trackingReg, sideEffect); @@ -136,9 +134,8 @@ private void insertSideEffectChecks(IterationData iter) { insertionPoint = execCheck; } - ExpressionFactory expressionFactory = ExpressionFactory.getInstance(); + final ExpressionFactory expressionFactory = ExpressionFactory.getInstance(); final Expression atLeastOneSideEffect = trackingRegs.stream() - .map(expressionFactory::makeBooleanCast) .map(expressionFactory::makeNot) .reduce(expressionFactory.makeFalse(), expressionFactory::makeOr); final CondJump assumeSideEffect = EventFactory.newJumpUnless(atLeastOneSideEffect, (Label) thread.getExit()); diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/Inlining.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/Inlining.java index a6f2530775..b536489a40 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/Inlining.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/Inlining.java @@ -82,8 +82,12 @@ private void inlineAllCalls(Function function) { String.format("Cannot call thread %s directly.", call.getCallTarget())); } - call.getPredecessor().insertAfter(EventFactory.newFunctionCall(callTarget.getName())); - call.insertAfter(EventFactory.newFunctionReturn(callTarget.getName())); + final Event callMarker = EventFactory.newFunctionCallMarker(callTarget.getName()); + final Event returnMarker = EventFactory.newFunctionReturnMarker(callTarget.getName()); + callMarker.copyAllMetadataFrom(call); + returnMarker.copyAllMetadataFrom(call); + call.getPredecessor().insertAfter(callMarker); + call.insertAfter(returnMarker); // Calls with result will write the return value to this register. Register result = call instanceof DirectValueFunctionCall c ? c.getResultRegister() : null; inlineBodyAfterCall(call, result, call.getArguments(), callTarget, ++scopeCounter); diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/LogProgramStatistics.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/LogProgramStatistics.java index c8df419a29..25e71b8217 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/LogProgramStatistics.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/LogProgramStatistics.java @@ -39,11 +39,6 @@ public void run(Program program) { } int numNonInitThreads = (int)program.getThreads().stream().filter(t -> !(t.getEntry() instanceof Init)).count(); - if (program.getFormat() == Program.SourceLanguage.BOOGIE) { - numNonInitThreads--; // We subtract 1, because for Boogie code we always create an extra empty thread - // TODO: Why do we do this? - } - int staticAddressSpaceSize = program.getMemory().getObjects().stream() .filter(MemoryObject::isStaticallyAllocated).mapToInt(MemoryObject::size).sum(); int dynamicAddressSpaceSize = program.getMemory().getObjects().stream() diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/MemoryAllocation.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/MemoryAllocation.java index ad4ae2b468..8556bc2c81 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/MemoryAllocation.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/MemoryAllocation.java @@ -86,10 +86,10 @@ private void createInitEvents(Program program) { int nextThreadId = threads.get(threads.size() - 1).getId() + 1; for(MemoryObject memObj : program.getMemory().getObjects()) { // The last case "heuristically checks" if Smack generated initialization or not: - // we expect at least every 8 bytes to be initialized. + // if any field is statically initialized, then likely everything is initialized. final boolean isStaticallyInitialized = !isLitmus && memObj.isStaticallyAllocated() - && (memObj.getStaticallyInitializedFields().size() >= memObj.size() / 8); + && memObj.getStaticallyInitializedFields().size() > 1; final Iterable fieldsToInit = isStaticallyInitialized ? memObj.getStaticallyInitializedFields() : IntStream.range(0, memObj.size()).boxed()::iterator; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/Simplifier.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/Simplifier.java index 972d870d7a..244ae73c10 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/Simplifier.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/Simplifier.java @@ -9,8 +9,8 @@ import com.dat3m.dartagnan.program.event.core.CondJump; import com.dat3m.dartagnan.program.event.core.Event; import com.dat3m.dartagnan.program.event.core.Label; -import com.dat3m.dartagnan.program.event.core.annotations.FunCall; -import com.dat3m.dartagnan.program.event.core.annotations.FunRet; +import com.dat3m.dartagnan.program.event.core.annotations.FunCallMarker; +import com.dat3m.dartagnan.program.event.core.annotations.FunReturnMarker; import com.google.common.base.Preconditions; import org.apache.logging.log4j.LogManager; import org.apache.logging.log4j.Logger; @@ -64,7 +64,7 @@ private boolean simplifyEvent(Event next) { changed = simplifyJump(jump); } else if (next instanceof Label label) { changed = simplifyLabel(label); - } else if (next instanceof FunCall fc) { + } else if (next instanceof FunCallMarker fc) { changed = simplifyFunCall(fc); } return changed; @@ -87,13 +87,13 @@ private boolean simplifyLabel(Label label) { return false; } - private boolean simplifyFunCall(FunCall call) { + private boolean simplifyFunCall(FunCallMarker call) { // If simplifyEvent returns false, the function is either non-empty or we reached the return statement while (simplifyEvent(call.getSuccessor())) { } // Check if we reached the return statement final Event successor = call.getSuccessor(); - if(successor instanceof FunRet funRet && funRet.getFunctionName().equals(call.getFunctionName())) { + if(successor instanceof FunReturnMarker funRet && funRet.getFunctionName().equals(call.getFunctionName())) { call.tryDelete(); successor.tryDelete(); return true; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/ThreadCreation.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/ThreadCreation.java index 79fdca83e6..c203ce5efc 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/ThreadCreation.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/ThreadCreation.java @@ -29,6 +29,7 @@ import com.dat3m.dartagnan.program.event.functions.DirectValueFunctionCall; import com.dat3m.dartagnan.program.event.functions.Return; import com.dat3m.dartagnan.program.event.lang.llvm.LlvmCmpXchg; +import com.dat3m.dartagnan.program.event.metadata.OriginalId; import com.dat3m.dartagnan.program.memory.Memory; import com.dat3m.dartagnan.program.memory.MemoryObject; import com.google.common.base.Preconditions; @@ -188,6 +189,7 @@ public void run(Program program) { } EventIdReassignment.newInstance().run(program); + program.getEvents().forEach(e -> e.setMetadata(new OriginalId(e.getGlobalId()))); logger.info("Number of threads (including main): " + program.getThreads().size()); } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorPower.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorPower.java index f104148f03..f737e0a9cb 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorPower.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorPower.java @@ -337,7 +337,7 @@ public List visitAtomicCmpXchg(AtomicCmpXchg e) { ExecutionStatus optionalExecStatus = null; Local optionalUpdateCasCmpResult = null; if (e.isWeak()) { - Register statusReg = e.getFunction().newRegister(type); + Register statusReg = e.getFunction().newRegister(types.getBooleanType()); optionalExecStatus = newExecutionStatus(statusReg, storeValue); optionalUpdateCasCmpResult = newLocal(booleanResultRegister, expressions.makeNot(statusReg)); } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorRISCV.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorRISCV.java index 2d666d053c..40de0ed0ed 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorRISCV.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorRISCV.java @@ -124,10 +124,6 @@ public List visitLlvmXchg(LlvmXchg e) { Load load = newRMWLoadExclusiveWithMo(resultRegister, address, Tag.RISCV.extractLoadMoFromCMo(mo)); Store store = RISCV.newRMWStoreConditional(address, e.getValue(), Tag.RISCV.extractStoreMoFromCMo(mo), true); - Register statusReg = e.getThread().newRegister("status(" + e.getGlobalId() + ")", resultRegister.getType()); - // We normally make the following optional. - // Here we make it mandatory to guarantee correct dependencies. - ExecutionStatus execStatus = newExecutionStatusWithDependencyTracking(statusReg, store); Label label = newLabel("FakeDep"); Event fakeCtrlDep = newFakeCtrlDep(resultRegister, label); @@ -135,8 +131,7 @@ public List visitLlvmXchg(LlvmXchg e) { load, fakeCtrlDep, label, - store, - execStatus + store ); } @@ -152,11 +147,6 @@ public List visitLlvmRMW(LlvmRMW e) { Load load = newRMWLoadExclusiveWithMo(resultRegister, address, Tag.RISCV.extractLoadMoFromCMo(mo)); Store store = RISCV.newRMWStoreConditional(address, dummyReg, Tag.RISCV.extractStoreMoFromCMo(mo), true); - Register statusReg = e.getFunction().newRegister("status(" + e.getGlobalId() + ")", type); - // We normally make the following optional. - // Here we make it mandatory to guarantee correct dependencies. - ExecutionStatus execStatus = newExecutionStatusWithDependencyTracking(statusReg, store); - Label label = newLabel("FakeDep"); Event fakeCtrlDep = newFakeCtrlDep(resultRegister, label); @@ -165,8 +155,7 @@ public List visitLlvmRMW(LlvmRMW e) { fakeCtrlDep, label, localOp, - store, - execStatus + store ); } @@ -187,6 +176,7 @@ public List visitLlvmCmpXchg(LlvmCmpXchg e) { Load load = newRMWLoadExclusiveWithMo(oldValueRegister, address, Tag.RISCV.extractLoadMoFromCMo(mo)); Store store = newRMWStoreExclusiveWithMo(address, e.getStoreValue(), true, Tag.RISCV.extractStoreMoFromCMo(mo)); + //TODO: We only do strong CAS here? return eventSequence( load, casCmpResult, @@ -279,11 +269,6 @@ public List visitAtomicFetchOp(AtomicFetchOp e) { Load load = newRMWLoadExclusiveWithMo(resultRegister, address, Tag.RISCV.extractLoadMoFromCMo(mo)); Store store = RISCV.newRMWStoreConditional(address, dummyReg, Tag.RISCV.extractStoreMoFromCMo(mo), true); - Register statusReg = e.getFunction().newRegister("status(" + e.getGlobalId() + ")", type); - // We normally make the following optional. - // Here we make it mandatory to guarantee correct dependencies. - ExecutionStatus execStatus = newExecutionStatusWithDependencyTracking(statusReg, store); - Label label = newLabel("FakeDep"); Event fakeCtrlDep = newFakeCtrlDep(resultRegister, label); @@ -292,8 +277,7 @@ public List visitAtomicFetchOp(AtomicFetchOp e) { fakeCtrlDep, label, localOp, - store, - execStatus + store ); } @@ -352,10 +336,6 @@ public List visitAtomicXchg(AtomicXchg e) { Load load = newRMWLoadExclusiveWithMo(resultRegister, address, Tag.RISCV.extractLoadMoFromCMo(mo)); Store store = RISCV.newRMWStoreConditional(address, e.getValue(), Tag.RISCV.extractStoreMoFromCMo(mo), true); - Register statusReg = e.getFunction().newRegister("status(" + e.getGlobalId() + ")", resultRegister.getType()); - // We normally make the following optional. - // Here we make it mandatory to guarantee correct dependencies. - ExecutionStatus execStatus = newExecutionStatusWithDependencyTracking(statusReg, store); Label label = newLabel("FakeDep"); Event fakeCtrlDep = newFakeCtrlDep(resultRegister, label); @@ -363,8 +343,7 @@ public List visitAtomicXchg(AtomicXchg e) { load, fakeCtrlDep, label, - store, - execStatus + store ); } @@ -454,7 +433,7 @@ public List visitLKMMCmpXchg(LKMMCmpXchg e) { String mo = e.getMo(); Register dummy = e.getFunction().newRegister(e.getResultRegister().getType()); - Register statusReg = e.getFunction().newRegister(e.getResultRegister().getType()); + Register statusReg = e.getFunction().newRegister(types.getBooleanType()); Label casEnd = newLabel("CAS_end"); CondJump branchOnCasCmpResult = newJump(expressions.makeNEQ(dummy, e.getExpectedValue()), casEnd); @@ -462,7 +441,7 @@ public List visitLKMMCmpXchg(LKMMCmpXchg e) { Store store = RISCV.newRMWStoreConditional(address, e.getStoreValue(), mo.equals(Tag.Linux.MO_MB) ? Tag.RISCV.MO_REL : "", true); ExecutionStatus status = newExecutionStatusWithDependencyTracking(statusReg, store); Label label = newLabel("FakeDep"); - Event fakeCtrlDep = newJump(expressions.makeEQ(statusReg, expressions.makeZero(types.getArchType())), label); + Event fakeCtrlDep = newJump(statusReg, label); // TODO: Do we really need a fakedep from the store? Fence optionalMemoryBarrierBefore = mo.equals(Tag.Linux.MO_RELEASE) ? RISCV.newRWWFence() : null; Fence optionalMemoryBarrierAfter = mo.equals(Tag.Linux.MO_MB) ? RISCV.newRWRWFence() : mo.equals(Tag.Linux.MO_ACQUIRE) ? RISCV.newRRWFence() : null; @@ -491,14 +470,14 @@ public List visitLKMMXchg(LKMMXchg e) { String mo = e.getMo(); Register dummy = e.getFunction().newRegister(type); - Register statusReg = e.getFunction().newRegister(type); + Register statusReg = e.getFunction().newRegister(types.getBooleanType()); String moLoad = mo.equals(Tag.Linux.MO_MB) || mo.equals(Tag.Linux.MO_ACQUIRE) ? Tag.RISCV.MO_ACQ : ""; Load load = newRMWLoadExclusiveWithMo(dummy, address, moLoad); String moStore = mo.equals(Tag.Linux.MO_MB) || mo.equals(Tag.Linux.MO_RELEASE) ? Tag.RISCV.MO_ACQ_REL : ""; Store store = RISCV.newRMWStoreConditional(address, e.getValue(), moStore, true); ExecutionStatus status = newExecutionStatusWithDependencyTracking(statusReg, store); Label label = newLabel("FakeDep"); - Event fakeCtrlDep = newJumpUnless(expressions.makeBooleanCast(statusReg), label); + Event fakeCtrlDep = newJump(statusReg, label); // TODO: Do we really need a fakedep from the store? Fence optionalMemoryBarrierAfter = mo.equals(Tag.Linux.MO_MB) ? RISCV.newRWRWFence() : mo.equals(Tag.Linux.MO_ACQUIRE) ? RISCV.newRRWFence() : null; return eventSequence( @@ -522,7 +501,7 @@ public List visitLKMMOpNoReturn(LKMMOpNoReturn e) { IntegerType type = types.getArchType(); Register dummy = e.getFunction().newRegister(type); - Register statusReg = e.getFunction().newRegister(type); + Register statusReg = e.getFunction().newRegister(types.getBooleanType()); Expression storeValue = expressions.makeBinary(dummy, e.getOperator(), e.getOperand()); String moLoad = mo.equals(Tag.Linux.MO_MB) || mo.equals(Tag.Linux.MO_ACQUIRE) ? Tag.RISCV.MO_ACQ : ""; Load load = newRMWLoadExclusiveWithMo(dummy, address, moLoad); @@ -530,7 +509,7 @@ public List visitLKMMOpNoReturn(LKMMOpNoReturn e) { Store store = RISCV.newRMWStoreConditional(address, storeValue, moStore, true); ExecutionStatus status = newExecutionStatusWithDependencyTracking(statusReg, store); Label label = newLabel("FakeDep"); - Event fakeCtrlDep = newJump(expressions.makeEQ(statusReg, expressions.makeZero(type)), label); + Event fakeCtrlDep = newJump(statusReg, label); // TODO: Do we really need a fakedep from the store? return eventSequence( load, @@ -556,14 +535,14 @@ public List visitLKMMFetchOp(LKMMFetchOp e) { String mo = e.getMo(); Register dummy = e.getFunction().newRegister(type); - Register statusReg = e.getFunction().newRegister(type); + Register statusReg = e.getFunction().newRegister(types.getBooleanType()); Load load = newRMWLoadExclusive(dummy, address); // TODO: No mo on the load? Store store = RISCV.newRMWStoreConditional(address, expressions.makeBinary(dummy, e.getOperator(), e.getOperand()), mo.equals(Tag.Linux.MO_MB) ? Tag.RISCV.MO_REL : "", true); ExecutionStatus status = newExecutionStatusWithDependencyTracking(statusReg, store); Label label = newLabel("FakeDep"); - Event fakeCtrlDep = newJumpUnless(expressions.makeBooleanCast(statusReg), label); + Event fakeCtrlDep = newJump(statusReg, label); // TODO: Do we really need a fakedep from the store? Fence optionalMemoryBarrierBefore = mo.equals(Tag.Linux.MO_RELEASE) ? RISCV.newRWWFence() : null; Fence optionalMemoryBarrierAfter = mo.equals(Tag.Linux.MO_MB) ? RISCV.newRWRWFence() : mo.equals(Tag.Linux.MO_ACQUIRE) ? RISCV.newRRWFence() : null; @@ -592,13 +571,13 @@ public List visitLKMMOpReturn(LKMMOpReturn e) { String mo = e.getMo(); Register dummy = e.getFunction().newRegister(type); - Register statusReg = e.getFunction().newRegister(type); + Register statusReg = e.getFunction().newRegister(types.getBooleanType()); Load load = newRMWLoadExclusive(dummy, address); // TODO: No mo on the load? Store store = RISCV.newRMWStoreConditional(address, dummy, mo.equals(Tag.Linux.MO_MB) ? Tag.RISCV.MO_REL : "", true); ExecutionStatus status = newExecutionStatusWithDependencyTracking(statusReg, store); Label label = newLabel("FakeDep"); - Event fakeCtrlDep = newJumpUnless(expressions.makeBooleanCast(statusReg), label); + Event fakeCtrlDep = newJump(statusReg, label); // TODO: Do we really need a fakedep from the store? Fence optionalMemoryBarrierBefore = mo.equals(Tag.Linux.MO_RELEASE) ? RISCV.newRWWFence() : null; Fence optionalMemoryBarrierAfter = mo.equals(Tag.Linux.MO_MB) ? RISCV.newRWRWFence() : mo.equals(Tag.Linux.MO_ACQUIRE) ? RISCV.newRRWFence() : null; @@ -630,12 +609,11 @@ public List visitLKMMAddUnless(LKMMAddUnless e) { String mo = e.getMo(); Register regValue = e.getFunction().newRegister(type); - Register statusReg = e.getFunction().newRegister(type); Load load = newRMWLoadExclusive(regValue, address); // TODO: No mo on the load? Store store = RISCV.newRMWStoreConditional(address, expressions.makeADD(regValue, e.getOperand()), mo.equals(Tag.Linux.MO_MB) ? Tag.RISCV.MO_REL : "", true); - ExecutionStatus status = newExecutionStatusWithDependencyTracking(statusReg, store); + // TODO: Why does this use a different fake dep (from the load) than the other RMW events (from the store)? Label label = newLabel("FakeDep"); Event fakeCtrlDep = newFakeCtrlDep(regValue, label); @@ -650,7 +628,6 @@ public List visitLKMMAddUnless(LKMMAddUnless e) { newLocal(dummy, expressions.makeNEQ(regValue, unless)), branchOnCauCmpResult, store, - status, fakeCtrlDep, label, optionalMemoryBarrierAfter, diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/utils/visualization/ExecutionGraphVisualizer.java b/dartagnan/src/main/java/com/dat3m/dartagnan/utils/visualization/ExecutionGraphVisualizer.java index 5660ce11a1..c9061985c2 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/utils/visualization/ExecutionGraphVisualizer.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/utils/visualization/ExecutionGraphVisualizer.java @@ -7,7 +7,6 @@ import com.dat3m.dartagnan.program.event.Tag; import com.dat3m.dartagnan.program.event.core.MemoryCoreEvent; import com.dat3m.dartagnan.program.event.metadata.MemoryOrder; -import com.dat3m.dartagnan.program.event.metadata.SourceLocation; import com.dat3m.dartagnan.verification.model.EventData; import com.dat3m.dartagnan.verification.model.ExecutionModel; import org.apache.logging.log4j.LogManager; @@ -23,7 +22,6 @@ import java.util.Map; import java.util.concurrent.TimeUnit; import java.util.function.BiPredicate; -import java.util.stream.Collectors; import static com.dat3m.dartagnan.program.analysis.SyntacticContextAnalysis.*; @@ -89,10 +87,9 @@ public void generateGraphOfExecutionModel(Writer writer, String graphName, Execu } private boolean ignore(EventData e) { - return !e.getEvent().hasMetadata(SourceLocation.class) && !e.isInit(); + return false; // We ignore no events for now. } - private ExecutionGraphVisualizer addReadFrom(ExecutionModel model) { graphviz.beginSubgraph("ReadFrom"); @@ -105,7 +102,7 @@ private ExecutionGraphVisualizer addReadFrom(ExecutionModel model) { continue; } - appendEdge(w, r, model, "label=rf"); + appendEdge(w, r, "label=rf"); } graphviz.end(); return this; @@ -128,7 +125,7 @@ private ExecutionGraphVisualizer addFromRead(ExecutionModel model) { if (co.indexOf(w) + 1 < co.size()) { EventData w2 = co.get(co.indexOf(w) + 1); if (!ignore(w2) && frFilter.test(r, w2)) { - appendEdge(r, w2, model, "label=fr"); + appendEdge(r, w2, "label=fr"); } } } @@ -149,7 +146,7 @@ private ExecutionGraphVisualizer addCoherence(ExecutionModel model) { if (ignore(w1) || ignore(w2) || !coFilter.test(w1, w2)) { continue; } - appendEdge(w1, w2, model, "label=co"); + appendEdge(w1, w2, "label=co"); } } graphviz.end(); @@ -165,14 +162,15 @@ private ExecutionGraphVisualizer addAllThreadPos(ExecutionModel model) { private ExecutionGraphVisualizer addThreadPo(Thread thread, ExecutionModel model) { List threadEvents = model.getThreadEventsMap().get(thread) - .stream().filter(e -> e.hasTag(Tag.VISIBLE)).collect(Collectors.toList()); + .stream().filter(e -> e.hasTag(Tag.VISIBLE)).toList(); if (threadEvents.size() <= 1) { + // This skips init threads. return this; } // --- Subgraph start --- graphviz.beginSubgraph("T" + thread.getId()); - graphviz.setEdgeAttributes("weight=10"); + graphviz.setEdgeAttributes("weight=100"); // --- Node list --- for (int i = 1; i < threadEvents.size(); i++) { EventData e1 = threadEvents.get(i - 1); @@ -182,7 +180,7 @@ private ExecutionGraphVisualizer addThreadPo(Thread thread, ExecutionModel model continue; } - appendEdge(e1, e2, model, (String[]) null); + appendEdge(e1, e2, (String[]) null); } // --- Subgraph end --- @@ -192,17 +190,9 @@ private ExecutionGraphVisualizer addThreadPo(Thread thread, ExecutionModel model } - private String eventToNode(EventData e, ExecutionModel model) { + private String eventToNode(EventData e) { if (e.isInit()) { return String.format("\"I(%s, %d)\"", addresses.get(e.getAccessedAddress()), e.getValue()); - } else if (!e.getEvent().hasMetadata(SourceLocation.class)) { - // Special write of each thread - int threadSize = model.getThreadEventsMap().get(e.getThread()).size(); - if (e.getLocalId() <= threadSize / 2) { - return String.format("\"T%d:start\"", e.getThread().getId()); - } else { - return String.format("\"T%d:end\"", e.getThread().getId()); - } } // We have MemEvent + Fence String tag = e.getEvent().toString(); @@ -217,7 +207,8 @@ private String eventToNode(EventData e, ExecutionModel model) { } final String callStack = makeContextString( synContext.getContextInfo(e.getEvent()).getContextOfType(CallContext.class), " -> \\n"); - return String.format("\"T%s:E%s\\n%s%s\n%s\"", + return String.format("\"%s:T%s/E%s\\n%s%s\n%s\"", + e.getThread().getName(), e.getThread().getId(), e.getEvent().getGlobalId(), callStack.isEmpty() ? callStack : callStack + " -> \\n", @@ -225,8 +216,8 @@ private String eventToNode(EventData e, ExecutionModel model) { tag); } - private void appendEdge(EventData a, EventData b, ExecutionModel model, String... options) { - graphviz.addEdge(eventToNode(a, model), eventToNode(b, model), options); + private void appendEdge(EventData a, EventData b, String... options) { + graphviz.addEdge(eventToNode(a), eventToNode(b), options); } public static void generateGraphvizFile(ExecutionModel model, int iterationCount, diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/ExecutionModel.java b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/ExecutionModel.java index ae281e9df8..98c45dc11a 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/ExecutionModel.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/ExecutionModel.java @@ -394,7 +394,7 @@ private void initDepTracking() { private void trackDependencies(Event e) { while (!endIfs.isEmpty() && e.getGlobalId() >= endIfs.peek().getGlobalId()) { - // We exited an If and remove the dependencies associated with it + // We exited an If-then-else block and remove the dependencies associated with it. // We do this inside a loop just in case multiple Ifs are left simultaneously endIfs.pop(); curCtrlDeps.removeAll(ifCtrlDeps.pop()); @@ -455,9 +455,9 @@ private void trackDependencies(Event e) { } lastRegWrites.put(status.getResultRegister(), deps); } else if (regWriter instanceof RegReader regReader) { - // Note: This code might work for more cases than the two we check for here, + // Note: This code might work for more cases than we check for here, // but we want to throw an exception if an unexpected event appears. - assert regWriter instanceof Local || regWriter instanceof ThreadArgument; + assert regWriter instanceof Local; // ---- internal data dependency ---- final Set dataDeps = new HashSet<>(); for (Register.Read regRead : regReader.getRegisterReads()) { @@ -472,6 +472,10 @@ private void trackDependencies(Event e) { dataDeps.addAll(visibleRootDependencies); } lastRegWrites.put(regWriter.getResultRegister(), dataDeps); + } else { + assert e instanceof ThreadArgument; + // We have a RegWriter that doesn't read registers, so there are no dependencies. + lastRegWrites.put(regWriter.getResultRegister(), new HashSet<>()); } } } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/Assumption.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/Assumption.java index 03538e6dbb..bd843d0dcd 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/Assumption.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/Assumption.java @@ -36,7 +36,9 @@ public Map computeInitialKnowledgeClos RelationAnalysis.Knowledge k = knowledgeMap.get(rel); Set d = difference(k.getMaySet(), may); Set e = difference(must, k.getMustSet()); - logger.info("Assumption disables {} and enables {} at {}", d.size(), e.size(), rel.getNameOrTerm()); + if (d.size() + e.size() != 0) { + logger.info("Assumption disables {} and enables {} at {}", d.size(), e.size(), rel.getNameOrTerm()); + } return Map.of(rel, new RelationAnalysis.ExtendedDelta(d, e)); } } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/Relation.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/Relation.java index b19b1bb7e2..9b1d2d2485 100755 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/Relation.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/Relation.java @@ -1,7 +1,8 @@ package com.dat3m.dartagnan.wmm; import com.dat3m.dartagnan.utils.dependable.Dependent; -import com.dat3m.dartagnan.wmm.definition.*; +import com.dat3m.dartagnan.wmm.definition.Composition; +import com.dat3m.dartagnan.wmm.definition.Union; import org.sosy_lab.common.configuration.Configuration; import org.sosy_lab.common.configuration.InvalidConfigurationException; @@ -14,11 +15,13 @@ public final class Relation implements Dependent { + private final Wmm wmm; Definition definition = new Definition.Undefined(this); private boolean isRecursive; final List names = new ArrayList<>(); - Relation() { + Relation(Wmm wmm) { + this.wmm = wmm; } /** @@ -46,6 +49,8 @@ public List getDependencies() { public void configure(Configuration config) throws InvalidConfigurationException { } + public Wmm getMemoryModel() { return this.wmm; } + public Optional getName() { return names.isEmpty() ? Optional.empty() : Optional.of(names.get(0)); } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/Wmm.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/Wmm.java index d6c7edc468..b6f17d236d 100755 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/Wmm.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/Wmm.java @@ -3,26 +3,41 @@ import com.dat3m.dartagnan.program.event.Tag; import com.dat3m.dartagnan.program.filter.Filter; import com.dat3m.dartagnan.wmm.axiom.Axiom; -import com.dat3m.dartagnan.wmm.definition.SameScope; -import com.dat3m.dartagnan.wmm.relation.RelationNameRepository; import com.dat3m.dartagnan.wmm.definition.*; +import com.dat3m.dartagnan.wmm.relation.RelationNameRepository; import com.google.common.collect.ImmutableSet; import org.apache.logging.log4j.LogManager; import org.apache.logging.log4j.Logger; import org.sosy_lab.common.configuration.Configuration; import org.sosy_lab.common.configuration.InvalidConfigurationException; +import org.sosy_lab.common.configuration.Option; +import org.sosy_lab.common.configuration.Options; import java.util.*; import java.util.function.BiFunction; import java.util.stream.Collectors; import java.util.stream.Stream; +import static com.dat3m.dartagnan.configuration.OptionNames.ENABLE_ACTIVE_SETS; +import static com.dat3m.dartagnan.configuration.OptionNames.REDUCE_ACYCLICITY_ENCODE_SETS; import static com.dat3m.dartagnan.wmm.relation.RelationNameRepository.*; import static com.google.common.base.Preconditions.checkArgument; import static com.google.common.base.Verify.verify; public class Wmm { + @Options + public static class Config { + + @Option(name = REDUCE_ACYCLICITY_ENCODE_SETS, + description = "Omit adding transitively implied relationships to the encode set of an acyclic relation." + + " This option is only relevant if \"" + ENABLE_ACTIVE_SETS + "\" is set.", + secure = true) + private boolean reduceAcyclicityEncoding = true; + + public boolean isReduceAcyclicityEncoding() { return reduceAcyclicityEncoding; } + } + private static final Logger logger = LogManager.getLogger(Wmm.class); public final static ImmutableSet BASE_RELATIONS = ImmutableSet.of(CO, RF, RMW); @@ -31,10 +46,14 @@ public class Wmm { private final Map filters = new HashMap<>(); private final Set relations = new HashSet<>(); + private final Config config = new Config(); + public Wmm() { BASE_RELATIONS.forEach(this::getRelation); } + public Config getConfig() { return this.config; } + /** * Inserts a constraint into this model. * @param constraint Constraint over relations in this model, to be inserted. @@ -50,17 +69,14 @@ public void addConstraint(Constraint constraint) { } public List getConstraints() { - return Stream.concat(constraints.stream(), relations.stream().map(Relation::getDefinition)) - .collect(Collectors.toList()); + return Stream.concat(constraints.stream(), relations.stream().map(Relation::getDefinition)).toList(); } /** * @return View of all axioms in this model in insertion order. */ public List getAxioms() { - return constraints.stream() - .filter(Axiom.class::isInstance).map(Axiom.class::cast) - .collect(Collectors.toList()); + return constraints.stream().filter(Axiom.class::isInstance).map(Axiom.class::cast).toList(); } /** @@ -115,7 +131,7 @@ public void addAlias(String name, Relation relation) { * @return The created relation. */ public Relation newRelation() { - Relation relation = new Relation(); + Relation relation = new Relation(this); relations.add(relation); return relation; } @@ -128,7 +144,7 @@ public Relation newRelation() { public Relation newRelation(String name) { checkArgument(relations.stream().noneMatch(r -> r.hasName(name)), "Already bound name %s.", name); - Relation relation = new Relation(); + Relation relation = new Relation(this); relation.names.add(name); relations.add(relation); return relation; @@ -191,6 +207,7 @@ public Filter getFilter(String name) { // ====================== Utility Methods ==================== public void configureAll(Configuration config) throws InvalidConfigurationException { + config.inject(this.config); for (Relation rel : getRelations()) { rel.configure(config); } @@ -200,6 +217,8 @@ public void configureAll(Configuration config) throws InvalidConfigurationExcept axiom.configure(config); } } + + logger.info("{}: {}", REDUCE_ACYCLICITY_ENCODE_SETS, this.config.isReduceAcyclicityEncoding()); } public void simplify() { @@ -223,9 +242,7 @@ private void simplifyAssociatives(Class cls, BiFunction ((Axiom) c).getRelation().equals(r))) { continue; } - List parents = relations.stream() - .filter(x -> x.getDependencies().contains(r)) - .collect(Collectors.toList()); + List parents = relations.stream().filter(x -> x.getDependencies().contains(r)).toList(); Relation p = parents.size() == 1 ? parents.get(0) : null; if (p != null && cls.isInstance(p.definition)) { Relation[] o = Stream.of(r, p) @@ -246,102 +263,65 @@ private void simplifyAssociatives(Class cls, BiFunction new ProgramOrder(r, Filter.byTag(Tag.VISIBLE)); + case LOC -> new SameAddress(r); + case ID -> new Identity(r, Filter.byTag(Tag.VISIBLE)); + case INT -> new SameThread(r); + case EXT -> new DifferentThreads(r); + case CO -> new Coherence(r); + case RF -> new ReadFrom(r); + case RMW -> new ReadModifyWrites(r); + case CASDEP -> new CompareAndSwapDependency(r); + case CRIT -> new CriticalSections(r); + case IDD -> new DirectDataDependency(r); + case ADDRDIRECT -> new DirectAddressDependency(r); + case CTRLDIRECT -> new DirectControlDependency(r); + case EMPTY -> new Empty(r); + case RFINV -> { + //FIXME: We don't need a name for "rf^-1", this is a normal relation! + // This causes models that explicitly mention "rf^-1" to have two versions of the same relation! + yield new Inverse(r, getRelation(RF)); + } + case FR -> composition(r, getRelation(RFINV), getRelation(CO)); + case MM -> new CartesianProduct(r, Filter.byTag(Tag.MEMORY), Filter.byTag(Tag.MEMORY)); + case MV -> new CartesianProduct(r, Filter.byTag(Tag.MEMORY), Filter.byTag(Tag.VISIBLE)); + case IDDTRANS -> new TransitiveClosure(r, getRelation(IDD)); + case DATA -> intersection(r, getRelation(IDDTRANS), getRelation(MM)); + case ADDR -> { Relation addrdirect = getRelation(ADDRDIRECT); Relation comp = addDefinition(composition(newRelation(), getRelation(IDDTRANS), addrdirect)); Relation union = addDefinition(union(newRelation(), addrdirect, comp)); - return intersection(r, union, getRelation(MM)); + yield intersection(r, union, getRelation(MM)); } - case CTRL: { + case CTRL -> { Relation comp = addDefinition(composition(newRelation(), getRelation(IDDTRANS), getRelation(CTRLDIRECT))); - return intersection(r, comp, getRelation(MV)); + yield intersection(r, comp, getRelation(MV)); } - case POLOC: - return intersection(r, getRelation(PO), getRelation(LOC)); - case RFE: - return intersection(r, getRelation(RF), getRelation(EXT)); - case RFI: - return intersection(r, getRelation(RF), getRelation(INT)); - case COE: - return intersection(r, getRelation(CO), getRelation(EXT)); - case COI: - return intersection(r, getRelation(CO), getRelation(INT)); - case FRE: - return intersection(r, getRelation(FR), getRelation(EXT)); - case FRI: - return intersection(r, getRelation(FR), getRelation(INT)); - case MFENCE: - return fence(r, MFENCE); - case ISH: - return fence(r, ISH); - case ISB: - return fence(r, ISB); - case SYNC: - return fence(r, SYNC); - case ISYNC: - return fence(r, ISYNC); - case LWSYNC: - return fence(r, LWSYNC); - case CTRLISYNC: - return intersection(r, getRelation(CTRL), getRelation(ISYNC)); - case CTRLISB: - return intersection(r, getRelation(CTRL), getRelation(ISB)); - case SR: - return new SameScope(r); - case SCTA: - return new SameScope(r, Tag.PTX.CTA); - case SYNCBAR: - return new SyncBar(r); - case SYNC_BARRIER: - return intersection(r, getRelation(SYNCBAR), getRelation(SCTA)); - case SYNC_FENCE: - return new SyncFence(r); - case VLOC: - return new VirtualLocation(r); - default: - throw new RuntimeException(name + "is part of RelationNameRepository but it has no associated relation."); - } + case POLOC -> intersection(r, getRelation(PO), getRelation(LOC)); + case RFE -> intersection(r, getRelation(RF), getRelation(EXT)); + case RFI -> intersection(r, getRelation(RF), getRelation(INT)); + case COE -> intersection(r, getRelation(CO), getRelation(EXT)); + case COI -> intersection(r, getRelation(CO), getRelation(INT)); + case FRE -> intersection(r, getRelation(FR), getRelation(EXT)); + case FRI -> intersection(r, getRelation(FR), getRelation(INT)); + case MFENCE -> fence(r, MFENCE); + case ISH -> fence(r, ISH); + case ISB -> fence(r, ISB); + case SYNC -> fence(r, SYNC); + case ISYNC -> fence(r, ISYNC); + case LWSYNC -> fence(r, LWSYNC); + case CTRLISYNC -> intersection(r, getRelation(CTRL), getRelation(ISYNC)); + case CTRLISB -> intersection(r, getRelation(CTRL), getRelation(ISB)); + case SR -> new SameScope(r); + case SCTA -> new SameScope(r, Tag.PTX.CTA); + case SYNCBAR -> new SyncBar(r); + case SYNC_BARRIER -> intersection(r, getRelation(SYNCBAR), getRelation(SCTA)); + case SYNC_FENCE -> new SyncFence(r); + case VLOC -> new VirtualLocation(r); + default -> + throw new RuntimeException(name + "is part of RelationNameRepository but it has no associated relation."); + }; } private Definition union(Relation r0, Relation r1, Relation r2) { diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/analysis/RelationAnalysis.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/analysis/RelationAnalysis.java index 449fe0bf68..7fb7b58d72 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/analysis/RelationAnalysis.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/analysis/RelationAnalysis.java @@ -36,7 +36,6 @@ import java.util.*; import java.util.function.Function; -import java.util.stream.Collectors; import java.util.stream.Stream; import static com.dat3m.dartagnan.configuration.Arch.RISCV; @@ -112,39 +111,48 @@ private RelationAnalysis(VerificationTask t, Context context, Configuration conf public static RelationAnalysis fromConfig(VerificationTask task, Context context, Configuration config) throws InvalidConfigurationException { RelationAnalysis a = new RelationAnalysis(task, context, config); task.getConfig().inject(a); - logger.info("{}: {}", ENABLE_RELATION_ANALYSIS, a.enable); + + final StringBuilder configSummary = new StringBuilder().append("\n"); + configSummary.append("\t").append(ENABLE_RELATION_ANALYSIS).append(": ").append(a.enable).append("\n"); + configSummary.append("\t").append(ENABLE_MUST_SETS).append(": ").append(a.enableMustSets).append("\n"); + configSummary.append("\t").append(ENABLE_EXTENDED_RELATION_ANALYSIS).append(": ").append(a.enableExtended); + logger.info(configSummary); + if (a.enableMustSets && !a.enable) { logger.warn("{} implies {}", ENABLE_MUST_SETS, ENABLE_RELATION_ANALYSIS); a.enableMustSets = false; } - logger.info("{}: {}", ENABLE_MUST_SETS, a.enableMustSets); if (a.enableExtended && !a.enable) { logger.warn("{} implies {}", ENABLE_EXTENDED_RELATION_ANALYSIS, ENABLE_RELATION_ANALYSIS); a.enableExtended = false; } - logger.info("{}: {}", ENABLE_EXTENDED_RELATION_ANALYSIS, a.enableExtended); + long t0 = System.currentTimeMillis(); a.run(); long t1 = System.currentTimeMillis(); logger.info("Finished regular analysis in {}ms", t1 - t0); + + final StringBuilder summary = new StringBuilder() + .append("\n======== RelationAnalysis summary ======== \n"); + summary.append("\t#Relations: ").append(task.getMemoryModel().getRelations().size()).append("\n"); + summary.append("\t#Axioms: ").append(task.getMemoryModel().getAxioms().size()).append("\n"); if (a.enableExtended) { long mayCount = a.countMaySet(); long mustCount = a.countMustSet(); a.runExtended(); logger.info("Finished extended analysis in {}ms", System.currentTimeMillis() - t1); - logger.info("Count of may-tuples removed: {}", mayCount - a.countMaySet()); - logger.info("Count of must-tuples added: {}", a.countMustSet() - mustCount); + summary.append("\t#may-tuples removed (extended): ").append(mayCount - a.countMaySet()).append("\n"); + summary.append("\t#must-tuples added (extended): ").append(a.countMustSet() - mustCount).append("\n"); } verify(a.enableMustSets || a.knowledgeMap.values().stream().allMatch(k -> k.must.isEmpty())); - logger.info("Number of may-tuples: {}", a.countMaySet()); - logger.info("Number of must-tuples: {}", a.countMustSet()); - logger.info("Number of mutually-exclusive tuples: {}", a.mutex.size()); Knowledge rf = a.knowledgeMap.get(task.getMemoryModel().getRelation(RF)); - logger.info("Number of may-read-from-tuples: {}", rf.may.size()); - logger.info("Number of must-read-from-tuples: {}", rf.must.size()); Knowledge co = a.knowledgeMap.get(task.getMemoryModel().getRelation(CO)); - logger.info("Number of may-coherence-tuples: {}", co.may.size()); - logger.info("Number of must-coherence-tuples: {}", co.must.size()); + summary.append("\ttotal #must|may|exclusive tuples: ") + .append(a.countMustSet()).append("|").append(a.countMaySet()).append("|").append(a.mutex.size()).append("\n"); + summary.append("\t#must|may rf tuples: ").append(rf.must.size()).append("|").append(rf.may.size()).append("\n"); + summary.append("\t#must|may co tuples: ").append(co.must.size()).append("|").append(co.may.size()).append("\n"); + summary.append("==========================================="); + logger.info(summary); return a; } @@ -472,8 +480,8 @@ public Knowledge visitDefinition(Relation r, List d) { @Override public Knowledge visitProduct(Relation rel, Filter domain, Filter range) { Set must = new HashSet<>(); - List l1 = program.getEvents().stream().filter(domain::apply).collect(toList()); - List l2 = program.getEvents().stream().filter(range::apply).collect(toList()); + List l1 = program.getEvents().stream().filter(domain::apply).toList(); + List l2 = program.getEvents().stream().filter(range::apply).toList(); for (Event e1 : l1) { for (Event e2 : l2) { if (!exec.areMutuallyExclusive(e1, e2)) { @@ -536,7 +544,7 @@ public Knowledge visitInternal(Relation rel) { public Knowledge visitProgramOrder(Relation rel, Filter type) { Set must = new HashSet<>(); for (Thread t : program.getThreads()) { - List events = t.getEvents().stream().filter(type::apply).collect(toList()); + List events = t.getEvents().stream().filter(type::apply).toList(); for (int i = 0; i < events.size(); i++) { Event e1 = events.get(i); for (int j = i + 1; j < events.size(); j++) { @@ -707,7 +715,7 @@ public Knowledge visitReadModifyWrites(Relation rel) { Set may = new HashSet<>(must); // LoadExcl -> StoreExcl for (Thread thread : program.getThreads()) { - List events = thread.getEvents().stream().filter(e -> e.hasTag(EXCL)).collect(toList()); + List events = thread.getEvents().stream().filter(e -> e.hasTag(EXCL)).toList(); // assume order by globalId // assume globalId describes a topological sorting over the control flow for (int end = 1; end < events.size(); end++) { @@ -804,7 +812,7 @@ public Knowledge visitReadFrom(Relation rel) { .filter(e -> (e.getThread() == read.getThread() || e.hasTag(INIT))) .map(x -> (MemoryCoreEvent) x) .sorted((o1, o2) -> o1.hasTag(INIT) == o2.hasTag(INIT) ? (o1.getGlobalId() - o2.getGlobalId()) : o1.hasTag(INIT) ? -1 : 1) - .collect(Collectors.toList()); + .toList(); // The set of writes that won't be readable due getting overwritten. Set deletedWrites = new HashSet<>(); // A rf-edge (w1, r) is impossible, if there exists a write w2 such that diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/axiom/Acyclic.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/axiom/Acyclic.java index 0bd68c658f..ce486623b9 100755 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/axiom/Acyclic.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/axiom/Acyclic.java @@ -11,9 +11,6 @@ import com.dat3m.dartagnan.wmm.utils.Tuple; import org.apache.logging.log4j.LogManager; import org.apache.logging.log4j.Logger; -import org.sosy_lab.common.configuration.Configuration; -import org.sosy_lab.common.configuration.InvalidConfigurationException; -import org.sosy_lab.common.configuration.Option; import org.sosy_lab.common.configuration.Options; import org.sosy_lab.java_smt.api.BooleanFormula; import org.sosy_lab.java_smt.api.BooleanFormulaManager; @@ -24,21 +21,13 @@ import java.util.function.Function; import java.util.stream.Collectors; -import static com.dat3m.dartagnan.configuration.OptionNames.ENABLE_ACTIVE_SETS; -import static com.dat3m.dartagnan.configuration.OptionNames.REDUCE_ACYCLICITY_ENCODE_SETS; import static com.google.common.base.Preconditions.checkArgument; import static com.google.common.collect.Sets.difference; @Options public class Acyclic extends Axiom { - private static final Logger logger = LogManager.getLogger(Acyclic.class); - - @Option(name = REDUCE_ACYCLICITY_ENCODE_SETS, - description = "Omit adding transitively implied relationships to the encode set of an acyclic relation." + - " This option is only relevant if \"" + ENABLE_ACTIVE_SETS + "\" is set.", - secure = true) - private boolean reduceAcyclicityEncoding = true; + private static final Logger logger = LogManager.getLogger(Acyclic.class); public Acyclic(Relation rel, boolean negated, boolean flag) { super(rel, negated, flag); @@ -48,12 +37,6 @@ public Acyclic(Relation rel) { super(rel, false, false); } - @Override - public void configure(Configuration config) throws InvalidConfigurationException { - config.inject(this); - logger.info("{}: {}", REDUCE_ACYCLICITY_ENCODE_SETS, reduceAcyclicityEncoding); - } - @Override public String toString() { return (negated ? "~" : "") + "acyclic " + rel.getNameOrTerm(); @@ -206,7 +189,7 @@ private Set getEncodeTupleSet(ExecutionAnalysis exec, RelationAnalysis ra } logger.info("encodeTupleSet size: {}", result.size()); - if (reduceAcyclicityEncoding) { + if (getMemoryModel().getConfig().isReduceAcyclicityEncoding()) { Set obsolete = transitivelyDerivableMustTuples(exec, ra.getKnowledge(rel)); result.removeAll(obsolete); logger.info("reduced encodeTupleSet size: {}", result.size()); diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/axiom/Axiom.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/axiom/Axiom.java index dccce574f7..fe3e502e8b 100755 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/axiom/Axiom.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/axiom/Axiom.java @@ -4,15 +4,12 @@ import com.dat3m.dartagnan.verification.VerificationTask; import com.dat3m.dartagnan.wmm.Constraint; import com.dat3m.dartagnan.wmm.Relation; +import com.dat3m.dartagnan.wmm.Wmm; import com.dat3m.dartagnan.wmm.utils.Tuple; import org.sosy_lab.common.configuration.Configuration; import org.sosy_lab.common.configuration.InvalidConfigurationException; -import java.util.Collections; -import java.util.List; -import java.util.Map; -import java.util.Objects; -import java.util.Set; +import java.util.*; /** * @@ -43,6 +40,8 @@ public Relation getRelation() { return rel; } + public Wmm getMemoryModel() { return rel.getMemoryModel(); } + /** * Users have the option to not enforce consistency checks, but rather * to use axioms to report properties of the candidate execution. diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/relation/RelationNameRepository.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/relation/RelationNameRepository.java index 8095df3fee..aa9ec01ae2 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/relation/RelationNameRepository.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/relation/RelationNameRepository.java @@ -49,7 +49,6 @@ public class RelationNameRepository { public static final String SYNC_FENCE = "sync_fence"; public static final String SYNCBAR = "syncbar"; public static final String VLOC = "vloc"; - // Any new string must be also added to method contains() below public static final ImmutableSet RELATION_NAMES; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/utils/Flag.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/utils/Flag.java index 7a2fffc156..e58d38db6d 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/utils/Flag.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/utils/Flag.java @@ -1,16 +1,15 @@ package com.dat3m.dartagnan.wmm.utils; +import com.google.common.collect.ImmutableSet; import org.sosy_lab.java_smt.api.BooleanFormula; import org.sosy_lab.java_smt.api.FormulaManager; -import com.google.common.collect.ImmutableSet; - public enum Flag { ARM_UNPREDICTABLE_BEHAVIOUR, LINUX_UNBALANCED_RCU; // TODO: Add linux when implemented - public static ImmutableSet all = ImmutableSet.of(ARM_UNPREDICTABLE_BEHAVIOUR); + public static final ImmutableSet ALL = ImmutableSet.of(ARM_UNPREDICTABLE_BEHAVIOUR); public BooleanFormula repr(FormulaManager m){ return m.getBooleanFormulaManager().makeVariable(code()); @@ -18,22 +17,16 @@ public BooleanFormula repr(FormulaManager m){ @Override public String toString(){ - switch (this){ - case ARM_UNPREDICTABLE_BEHAVIOUR: - return "ARM unpredictable behaviour"; - case LINUX_UNBALANCED_RCU: - return "Linux unbalanced RCU lock-unlock"; - } - throw new UnsupportedOperationException("Illegal flag type"); + return switch (this) { + case ARM_UNPREDICTABLE_BEHAVIOUR -> "ARM unpredictable behaviour"; + case LINUX_UNBALANCED_RCU -> "Linux unbalanced RCU lock-unlock"; + }; } private String code(){ - switch (this){ - case ARM_UNPREDICTABLE_BEHAVIOUR: - return "ARM_unpredictable_flag"; - case LINUX_UNBALANCED_RCU: - return "Linux_unbalanced_RCU_flag"; - } - throw new UnsupportedOperationException("Illegal flag type"); + return switch (this) { + case ARM_UNPREDICTABLE_BEHAVIOUR -> "ARM_unpredictable_flag"; + case LINUX_UNBALANCED_RCU -> "Linux_unbalanced_RCU_flag"; + }; } }