From 6326445a3923987549c4299678a6fc5cc3d4c9a8 Mon Sep 17 00:00:00 2001 From: Thomas Haas Date: Tue, 3 Sep 2024 21:12:46 +0200 Subject: [PATCH 01/18] Improved liveness detection for store exclusives (#722) --- .../dartagnan/encoding/PropertyEncoder.java | 163 +++++++++++------- .../dat3m/dartagnan/program/event/Tag.java | 8 +- .../processing/DynamicSpinLoopDetection.java | 19 +- .../program/processing/Inlining.java | 2 +- .../program/processing/Intrinsics.java | 2 +- .../program/processing/LoopUnrolling.java | 2 +- 6 files changed, 125 insertions(+), 71 deletions(-) diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/PropertyEncoder.java b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/PropertyEncoder.java index fa7ed2b267..36427a5adf 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/PropertyEncoder.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/PropertyEncoder.java @@ -21,7 +21,6 @@ import com.dat3m.dartagnan.wmm.utils.EventGraph; import com.google.common.base.Preconditions; import com.google.common.collect.Lists; -import com.google.common.collect.Maps; import org.apache.logging.log4j.LogManager; import org.apache.logging.log4j.Logger; import org.sosy_lab.common.configuration.InvalidConfigurationException; @@ -36,8 +35,8 @@ import java.util.stream.Collectors; import static com.dat3m.dartagnan.configuration.Property.*; -import static com.dat3m.dartagnan.wmm.RelationNameRepository.CO; import static com.dat3m.dartagnan.program.Program.SourceLanguage.LLVM; +import static com.dat3m.dartagnan.wmm.RelationNameRepository.CO; public class PropertyEncoder implements Encoder { @@ -66,7 +65,7 @@ public class PropertyEncoder implements Encoder { Since we encode a lot of potential violations, and we want to trace back which one lead to our query being SAT, we use trackable formulas. */ - private static class TrackableFormula { + public static class TrackableFormula { private final BooleanFormula trackingLiteral; private final BooleanFormula trackedFormula; @@ -304,7 +303,7 @@ public List encodeCATSpecificationViolations() { final EncodingContext ctx = this.context; final Wmm memoryModel = this.memoryModel; final List flaggedAxioms = memoryModel.getAxioms().stream() - .filter(Axiom::isFlagged).collect(Collectors.toList()); + .filter(Axiom::isFlagged).toList(); if (flaggedAxioms.isEmpty()) { logger.info("No CAT specification in the WMM. Skipping encoding."); @@ -402,22 +401,30 @@ public TrackableFormula encodeDataRaces() { private TrackableFormula encodeDeadlocks() { logger.info("Encoding dead locks"); - return new LivenessEncoder().encodeDeadlocks(); + return new LivenessEncoder().encodeLivenessBugs(); } /* Encoder for the liveness property. We have a liveness violation in some execution if - - At least one thread is stuck inside a loop (*) + - At least one thread is stuck (*) - All other threads are either stuck or terminated normally (**) - (*) A thread is stuck if it finishes a loop iteration - - without causing side-effects (e.g., visible stores) - - while reading only from co-maximal stores - => Without external help, a stuck thread will never be able to exit the loop. + (*) A thread is stuck if + (1) it performs a loop iteration without causing side-effects (e.g., visible stores) + while satisfying fairness conditions + => Without external help, a stuck thread will never be able to exit the loop. + OR (2) the thread is blocked by a control barrier. + + Fairness conditions for loops: + - Memory fairness: the loop iteration reads only co-maximal values + - Excl-Store progress: all exclusive stores in the iteration succeed (infinite spurious failures are unfair) + NOTE: Here we assume strong progress. Under weak fairness, a loop with two exclusive stores that need + to succeed in the same iteration could fail liveness if they succeed in alternation. - (**) A thread terminates normally IFF it does not terminate early (denoted by EARLYTERMINATION-tagged jumps) + (**) A thread terminates normally IFF it does terminate (no NONTERMINATION-tagged jumps) non-exceptionally + (no EXCEPTIONAL_TERMINATION-tagged jumps) due to e.g., - violating an assertion - reaching the loop unrolling bound @@ -429,36 +436,19 @@ in a deadlock without satisfying the stated conditions (e.g., while producing si */ private class LivenessEncoder { - private static class SpinIteration { - public final List containedLoads = new ArrayList<>(); - // Execution of the means the loop performed a side-effect-free - // iteration without exiting. If such a jump is executed + all loads inside the loop - // were co-maximal, then we have a deadlock condition. - public final List spinningJumps = new ArrayList<>(); - } - - public TrackableFormula encodeDeadlocks() { + public TrackableFormula encodeLivenessBugs() { final Program program = PropertyEncoder.this.program; final EncodingContext context = PropertyEncoder.this.context; final BooleanFormulaManager bmgr = context.getBooleanFormulaManager(); - final LoopAnalysis loopAnalysis = LoopAnalysis.newInstance(program); - - // Find spin loops of all threads - final Map> spinloopsMap = - Maps.toMap(program.getThreads(), t -> this.findSpinLoopsInThread(t, loopAnalysis)); - // Compute "stuckness" encoding for all threads - final Map isStuckMap = Maps.toMap(program.getThreads(), t -> - bmgr.or(generateBarrierStucknessEncoding(t, context), - this.generateSpinloopStucknessEncoding(spinloopsMap.get(t), context))); // Deadlock <=> allStuckOrDone /\ atLeastOneStuck BooleanFormula allStuckOrDone = bmgr.makeTrue(); BooleanFormula atLeastOneStuck = bmgr.makeFalse(); for (Thread thread : program.getThreads()) { - final BooleanFormula isStuck = isStuckMap.get(thread); + final BooleanFormula isStuck = isStuckEncoding(thread, context); final BooleanFormula isTerminatingNormally = thread .getEvents().stream() - .filter(e -> e.hasTag(Tag.EARLYTERMINATION)) + .filter(e -> e.hasTag(Tag.EXCEPTIONAL_TERMINATION) || e.hasTag(Tag.NONTERMINATION)) .map(CondJump.class::cast) .map(j -> bmgr.not(bmgr.and(context.execution(j), context.jumpCondition(j)))) .reduce(bmgr.makeTrue(), bmgr::and); @@ -471,6 +461,16 @@ public TrackableFormula encodeDeadlocks() { return new TrackableFormula(bmgr.not(LIVENESS.getSMTVariable(context)), hasDeadlock); } + private BooleanFormula isStuckEncoding(Thread thread, EncodingContext context) { + return context.getBooleanFormulaManager().or( + generateSpinloopStucknessEncoding(thread, context), + generateBarrierStucknessEncoding(thread, context) + ); + } + + // ------------------------------------------------------------------------------ + // Liveness issue due to blocked execution (due to ControlBarrier) + private BooleanFormula generateBarrierStucknessEncoding(Thread thread, EncodingContext context) { final BooleanFormulaManager bmgr = context.getBooleanFormulaManager(); return bmgr.or(thread.getEvents().stream() @@ -479,37 +479,85 @@ private BooleanFormula generateBarrierStucknessEncoding(Thread thread, EncodingC .toList()); } - // Compute "stuckness": A thread is stuck if it reaches a spin loop bound event - // while only reading from co-maximal stores. - private BooleanFormula generateSpinloopStucknessEncoding(List loops, EncodingContext context) { + // ------------------------------------------------------------------------------ + // Liveness issue due to non-terminating loops (~ deadlocks) + + private record SpinIteration(List body, List spinningJumps) { + // Execution of the means the loop performed a side-effect-free + // iteration without exiting. If such a jump is executed + all loads inside the loop + // were co-maximal, then we have a deadlock condition. + } + + private BooleanFormula generateSpinloopStucknessEncoding(Thread thread, EncodingContext context) { + final LoopAnalysis loopAnalysis = LoopAnalysis.onFunction(thread); + final BooleanFormulaManager bmgr = context.getBooleanFormulaManager(); + + return this.findSpinLoopsInThread(thread, loopAnalysis).stream() + .map(loop -> generateSpinloopStucknessEncoding(loop, context)) + .reduce(bmgr.makeFalse(), bmgr::or); + } + + private BooleanFormula generateSpinloopStucknessEncoding(SpinIteration loop, EncodingContext context) { + return context.getBooleanFormulaManager().and( + isSideEffectFreeEncoding(loop, context), + fairnessEncoding(loop, context) + ); + } + + private BooleanFormula isSideEffectFreeEncoding(SpinIteration loop, EncodingContext context) { + // Note that we assume (for now) that a SPINLOOP-tagged jump is executed only if the loop iteration + // was side-effect free. + final BooleanFormulaManager bmgr = context.getBooleanFormulaManager(); + final BooleanFormula isSideEffectFree = loop.spinningJumps.stream() + .map(j -> bmgr.and(context.execution(j), context.jumpCondition(j))) + .reduce(bmgr.makeFalse(), bmgr::or); + return isSideEffectFree; + } + + private BooleanFormula fairnessEncoding(SpinIteration loop, EncodingContext context) { + return context.getBooleanFormulaManager().and( + memoryFairnessEncoding(loop, context), + exclStoreFairnessEncoding(loop, context) + ); + } + + private BooleanFormula memoryFairnessEncoding(SpinIteration loop, EncodingContext context) { final BooleanFormulaManager bmgr = context.getBooleanFormulaManager(); final RelationAnalysis ra = PropertyEncoder.this.ra; final Relation rf = memoryModel.getRelation(RelationNameRepository.RF); final EncodingContext.EdgeEncoder rfEncoder = context.edge(rf); final Map> rfMayIn = ra.getKnowledge(rf).getMaySet().getInMap(); - if (loops.isEmpty()) { - return bmgr.makeFalse(); - } + final List loads = loop.body.stream() + .filter(Load.class::isInstance) + .map(Load.class::cast) + .toList(); - BooleanFormula isStuck = bmgr.makeFalse(); - for (SpinIteration loop : loops) { - BooleanFormula allLoadsAreCoMaximal = bmgr.makeTrue(); - for (Load load : loop.containedLoads) { - final BooleanFormula readsCoMaximalStore = rfMayIn.getOrDefault(load, Set.of()).stream() - .map(store -> bmgr.and(rfEncoder.encode(store, load), lastCoVar(store))) - .reduce(bmgr.makeFalse(), bmgr::or); - final BooleanFormula isCoMaximalLoad = bmgr.implication(context.execution(load), readsCoMaximalStore); - allLoadsAreCoMaximal = bmgr.and(allLoadsAreCoMaximal, isCoMaximalLoad); - } - // Note that we assume (for now) that a SPINLOOP-tagged jump is executed only if the loop iteration - // was side-effect free. - final BooleanFormula isSideEffectFree = loop.spinningJumps.stream() - .map(j -> bmgr.and(context.execution(j), context.jumpCondition(j))) + BooleanFormula allLoadsAreCoMaximal = bmgr.makeTrue(); + for (Load load : loads) { + final BooleanFormula readsCoMaximalStore = rfMayIn.getOrDefault(load, Set.of()).stream() + .map(store -> bmgr.and(rfEncoder.encode(store, load), lastCoVar(store))) .reduce(bmgr.makeFalse(), bmgr::or); - isStuck = bmgr.or(isStuck, bmgr.and(isSideEffectFree, allLoadsAreCoMaximal)); + final BooleanFormula isCoMaximalLoad = bmgr.implication(context.execution(load), readsCoMaximalStore); + allLoadsAreCoMaximal = bmgr.and(allLoadsAreCoMaximal, isCoMaximalLoad); + } + + return allLoadsAreCoMaximal; + } + + private BooleanFormula exclStoreFairnessEncoding(SpinIteration loop, EncodingContext context) { + final BooleanFormulaManager bmgr = context.getBooleanFormulaManager(); + final List exclStores = loop.body.stream() + .filter(RMWStoreExclusive.class::isInstance) + .map(RMWStoreExclusive.class::cast) + .toList(); + BooleanFormula allExclStoresExecuted = bmgr.makeTrue(); + for (RMWStoreExclusive exclStore : exclStores) { + final BooleanFormula executedIfPossible = bmgr.implication(context.controlFlow(exclStore), context.execution(exclStore)); + allExclStoresExecuted = bmgr.and(allExclStoresExecuted, executedIfPossible); } - return isStuck; + + return allExclStoresExecuted; } private List findSpinLoopsInThread(Thread thread, LoopAnalysis loopAnalysis) { @@ -525,14 +573,7 @@ private List findSpinLoopsInThread(Thread thread, LoopAnalysis lo .toList(); if (!spinningJumps.isEmpty()) { - final List loads = iterBody.stream() - .filter(Load.class::isInstance) - .map(Load.class::cast) - .toList(); - - final SpinIteration spinIter = new SpinIteration(); - spinIter.spinningJumps.addAll(spinningJumps); - spinIter.containedLoads.addAll(loads); + final SpinIteration spinIter = new SpinIteration(iterBody, spinningJumps); spinIterations.add(spinIter); } } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/Tag.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/Tag.java index b4cb282558..03cacda223 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/Tag.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/Tag.java @@ -27,9 +27,11 @@ private Tag() { } public static final String EXCL = "__EXCL"; // Marks the event that is reachable IFF a loop has not been fully unrolled. public static final String BOUND = "__BOUND"; - // Marks jumps that somehow terminate a thread earlier than "normally" - // This can be bound events, spinning events, assertion violations, etc. - public static final String EARLYTERMINATION = "__EARLYTERMINATION"; + // Marks jumps that designate an exceptional termination, typically due to assertion failures + public static final String EXCEPTIONAL_TERMINATION = "__EXCEPTIONAL_TERMINATION"; + // Marks jumps that designate non-termination, typically spinloops and bound events + // (and control barriers in the future) + public static final String NONTERMINATION = "__NONTERMINATION"; // Marks jumps that terminate a thread due to spinning behaviour, i.e. side-effect-free loop iterations public static final String SPINLOOP = "__SPINLOOP"; // Some events should not be optimized (e.g. fake dependencies) or deleted (e.g. bounds) diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/DynamicSpinLoopDetection.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/DynamicSpinLoopDetection.java index 1c65201ce4..1a002d6b52 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/DynamicSpinLoopDetection.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/DynamicSpinLoopDetection.java @@ -132,6 +132,7 @@ private void reduceToDominatingSideEffects(LoopData loop) { final List sideEffects = loop.sideEffects; final Event start = loop.getStart(); final Event end = loop.getEnd(); + final Predicate isAlwaysSideEffectful = (e -> e.cfImpliesExec() && sideEffects.contains(e)); final DominatorTree preDominatorTree = DominatorAnalysis.computePreDominatorTree(start, end); final DominatorTree postDominatorTree = DominatorAnalysis.computePostDominatorTree(start, end); @@ -144,7 +145,7 @@ private void reduceToDominatingSideEffects(LoopData loop) { // (2) Check if always side-effect-full at the end of an iteration directly before entering the next one. // This is an approximation: If the end of the iteration is predominated by some side effect // then we always observe side effects. - loop.isAlwaysSideEffectful = Streams.stream(preDominatorTree.getDominators(end)).anyMatch(sideEffects::contains); + loop.isAlwaysSideEffectful = Streams.stream(preDominatorTree.getDominators(end)).anyMatch(isAlwaysSideEffectful); if (loop.isAlwaysSideEffectful) { return; } @@ -157,7 +158,7 @@ private void reduceToDominatingSideEffects(LoopData loop) { preDominatorTree.getStrictDominators(sideEffect), postDominatorTree.getStrictDominators(sideEffect) ); - final boolean isDominated = Iterables.tryFind(dominators, sideEffects::contains).isPresent(); + final boolean isDominated = Iterables.tryFind(dominators, isAlwaysSideEffectful::test).isPresent(); if (isDominated) { sideEffects.remove(i); } @@ -173,12 +174,22 @@ private void instrumentLoop(LoopData loop) { final ExpressionFactory expressions = ExpressionFactory.getInstance(); final Function func = loop.loopInfo.function(); final int loopNum = loop.loopInfo.loopNumber(); + final Register tempReg = func.newRegister("__possiblySideEffectless#" + loopNum, types.getBooleanType()); final Register trackingReg = func.newRegister("__sideEffect#" + loopNum, types.getBooleanType()); final Event init = EventFactory.newLocal(trackingReg, expressions.makeFalse()); loop.getStart().insertAfter(init); for (Event sideEffect : loop.sideEffects) { - final Event updateSideEffect = EventFactory.newLocal(trackingReg, expressions.makeTrue()); + final List updateSideEffect = new ArrayList<>(); + if (sideEffect.cfImpliesExec()) { + updateSideEffect.add(EventFactory.newLocal(trackingReg, expressions.makeTrue())); + } else { + updateSideEffect.addAll(List.of( + EventFactory.newExecutionStatus(tempReg, sideEffect), + EventFactory.newLocal(trackingReg, expressions.makeOr(trackingReg, expressions.makeNot(tempReg))) + )); + + } sideEffect.getPredecessor().insertAfter(updateSideEffect); } @@ -197,7 +208,7 @@ private Event newSpinTerminator(Expression guard, Function func) { final Event terminator = func instanceof Thread thread ? EventFactory.newJump(guard, (Label) thread.getExit()) : EventFactory.newAbortIf(guard); - terminator.addTags(Tag.SPINLOOP, Tag.EARLYTERMINATION, Tag.NOOPT); + terminator.addTags(Tag.SPINLOOP, Tag.NONTERMINATION, Tag.NOOPT); return terminator; } 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 38b2e1814f..a755d09f1e 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 @@ -88,7 +88,7 @@ private void inlineAllCalls(Function function, Map snapshots if (depth > bound) { final AbortIf boundEvent = newAbortIf(ExpressionFactory.getInstance().makeTrue()); boundEvent.copyAllMetadataFrom(call); - boundEvent.addTags(Tag.BOUND, Tag.EARLYTERMINATION, Tag.NOOPT); + boundEvent.addTags(Tag.BOUND, Tag.NONTERMINATION, Tag.NOOPT); call.replaceBy(boundEvent); event = boundEvent; } else { diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/Intrinsics.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/Intrinsics.java index db2871e546..b81f2a43e5 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/Intrinsics.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/Intrinsics.java @@ -901,7 +901,7 @@ private List inlineAssert(FunctionCall call, AssertionType skip, String e final Expression condition = expressions.makeFalse(); final Event assertion = EventFactory.newAssert(condition, errorMsg); final Event abort = EventFactory.newAbortIf(expressions.makeTrue()); - abort.addTags(Tag.EARLYTERMINATION); + abort.addTags(Tag.EXCEPTIONAL_TERMINATION); return List.of(assertion, abort); } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/LoopUnrolling.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/LoopUnrolling.java index 7b6bca60a9..293f15f489 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/LoopUnrolling.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/LoopUnrolling.java @@ -191,7 +191,7 @@ private Event newBoundEvent(Function func) { final Event boundEvent = func instanceof Thread thread ? EventFactory.newGoto((Label) thread.getExit()) : EventFactory.newAbortIf(ExpressionFactory.getInstance().makeTrue()); - boundEvent.addTags(Tag.BOUND, Tag.EARLYTERMINATION, Tag.NOOPT); + boundEvent.addTags(Tag.BOUND, Tag.NONTERMINATION, Tag.NOOPT); return boundEvent; } From 5e10cda3235bf920317d5764fc247645ae0ce3d5 Mon Sep 17 00:00:00 2001 From: Thomas Haas Date: Tue, 3 Sep 2024 22:28:12 +0200 Subject: [PATCH 02/18] Renamed Location to FinalMemoryValue. (#725) --- .../dartagnan/encoding/ExpressionEncoder.java | 10 +++---- .../dartagnan/expression/Expression.java | 8 ++--- .../dartagnan/expression/ExpressionKind.java | 1 + .../expression/ExpressionVisitor.java | 4 +-- .../visitors/VisitorLitmusAssertions.java | 4 +-- .../visitors/spirv/VisitorSpirvOutput.java | 30 ++++++++----------- .../{Location.java => FinalMemoryValue.java} | 25 +++++++--------- .../processing/RemoveUnusedMemory.java | 8 ++--- 8 files changed, 41 insertions(+), 49 deletions(-) rename dartagnan/src/main/java/com/dat3m/dartagnan/program/memory/{Location.java => FinalMemoryValue.java} (59%) diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ExpressionEncoder.java b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ExpressionEncoder.java index f82fdea03b..914fb9c383 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ExpressionEncoder.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ExpressionEncoder.java @@ -11,7 +11,7 @@ import com.dat3m.dartagnan.expression.type.TypeFactory; import com.dat3m.dartagnan.program.Register; import com.dat3m.dartagnan.program.event.Event; -import com.dat3m.dartagnan.program.memory.Location; +import com.dat3m.dartagnan.program.memory.FinalMemoryValue; import com.dat3m.dartagnan.program.memory.MemoryObject; import com.dat3m.dartagnan.program.misc.NonDetValue; import org.sosy_lab.java_smt.api.*; @@ -298,9 +298,9 @@ public Formula visitMemoryObject(MemoryObject memObj) { } @Override - public Formula visitLocation(Location location) { - checkState(event == null, "Cannot evaluate %s at event %s.", location, event); - int size = types.getMemorySizeInBits(location.getType()); - return context.lastValue(location.getMemoryObject(), location.getOffset(), size); + public Formula visitFinalMemoryValue(FinalMemoryValue val) { + checkState(event == null, "Cannot evaluate final memory value of %s at event %s.", val, event); + int size = types.getMemorySizeInBits(val.getType()); + return context.lastValue(val.getMemoryObject(), val.getOffset(), size); } } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/expression/Expression.java b/dartagnan/src/main/java/com/dat3m/dartagnan/expression/Expression.java index afc86451c1..a2891b877c 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/expression/Expression.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/expression/Expression.java @@ -2,7 +2,7 @@ import com.dat3m.dartagnan.expression.processing.ExpressionInspector; import com.dat3m.dartagnan.program.Register; -import com.dat3m.dartagnan.program.memory.Location; +import com.dat3m.dartagnan.program.memory.FinalMemoryValue; import com.dat3m.dartagnan.program.memory.MemoryObject; import com.google.common.collect.ImmutableSet; @@ -40,9 +40,9 @@ public MemoryObject visitMemoryObject(MemoryObject memObj) { } @Override - public Expression visitLocation(Location location) { - objects.add(location.getMemoryObject()); - return location; + public Expression visitFinalMemoryValue(FinalMemoryValue val) { + objects.add(val.getMemoryObject()); + return val; } } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/expression/ExpressionKind.java b/dartagnan/src/main/java/com/dat3m/dartagnan/expression/ExpressionKind.java index 57e26ad293..9abbc42896 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/expression/ExpressionKind.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/expression/ExpressionKind.java @@ -16,6 +16,7 @@ enum Other implements ExpressionKind { NONDET, FUNCTION_ADDR, MEMORY_ADDR, + FINAL_MEM_VAL, REGISTER, GEP, CONSTRUCT, diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/expression/ExpressionVisitor.java b/dartagnan/src/main/java/com/dat3m/dartagnan/expression/ExpressionVisitor.java index b72021dd0a..1e4640b963 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/expression/ExpressionVisitor.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/expression/ExpressionVisitor.java @@ -11,7 +11,7 @@ import com.dat3m.dartagnan.expression.misc.ITEExpr; import com.dat3m.dartagnan.program.Function; import com.dat3m.dartagnan.program.Register; -import com.dat3m.dartagnan.program.memory.Location; +import com.dat3m.dartagnan.program.memory.FinalMemoryValue; import com.dat3m.dartagnan.program.memory.MemoryObject; import com.dat3m.dartagnan.program.misc.NonDetValue; @@ -59,7 +59,7 @@ public interface ExpressionVisitor { default TRet visitRegister(Register reg) { return visitLeafExpression(reg); } default TRet visitFunction(Function function) { return visitLeafExpression(function); } default TRet visitMemoryObject(MemoryObject memObj) { return visitLeafExpression(memObj); } - default TRet visitLocation(Location loc) { return visitLeafExpression(loc); } + default TRet visitFinalMemoryValue(FinalMemoryValue val) { return visitLeafExpression(val); } default TRet visitNonDetValue(NonDetValue nonDet) { return visitLeafExpression(nonDet); } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusAssertions.java b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusAssertions.java index c8ce2ca1d4..5f720d48b9 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusAssertions.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusAssertions.java @@ -8,7 +8,7 @@ import com.dat3m.dartagnan.parsers.LitmusAssertionsLexer; import com.dat3m.dartagnan.parsers.LitmusAssertionsParser; import com.dat3m.dartagnan.parsers.program.utils.ProgramBuilder; -import com.dat3m.dartagnan.program.memory.Location; +import com.dat3m.dartagnan.program.memory.FinalMemoryValue; import com.dat3m.dartagnan.program.memory.MemoryObject; import org.antlr.v4.runtime.CharStream; import org.antlr.v4.runtime.CharStreams; @@ -115,6 +115,6 @@ private Expression acceptAssertionValue(LitmusAssertionsParser.AssertionValueCon checkState(base != null, "uninitialized location %s", name); TerminalNode offset = ctx.DigitSequence(); int o = offset == null ? 0 : Integer.parseInt(offset.getText()); - return right && offset == null ? base : new Location(name, archType, base, o); + return right && offset == null ? base : new FinalMemoryValue(name, archType, base, o); } } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/spirv/VisitorSpirvOutput.java b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/spirv/VisitorSpirvOutput.java index 1fbf076f80..6185fc6933 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/spirv/VisitorSpirvOutput.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/spirv/VisitorSpirvOutput.java @@ -4,7 +4,6 @@ import com.dat3m.dartagnan.expression.Expression; import com.dat3m.dartagnan.expression.ExpressionFactory; import com.dat3m.dartagnan.expression.Type; -import com.dat3m.dartagnan.expression.base.LiteralExpressionBase; import com.dat3m.dartagnan.expression.integers.IntCmpOp; import com.dat3m.dartagnan.expression.integers.IntLiteral; import com.dat3m.dartagnan.expression.type.AggregateType; @@ -13,15 +12,13 @@ import com.dat3m.dartagnan.expression.type.TypeFactory; import com.dat3m.dartagnan.parsers.SpirvBaseVisitor; import com.dat3m.dartagnan.parsers.SpirvParser; -import com.dat3m.dartagnan.parsers.program.visitors.spirv.helpers.HelperTypes; import com.dat3m.dartagnan.parsers.program.visitors.spirv.builders.ProgramBuilder; +import com.dat3m.dartagnan.parsers.program.visitors.spirv.helpers.HelperTypes; import com.dat3m.dartagnan.program.Program; -import com.dat3m.dartagnan.program.memory.Location; +import com.dat3m.dartagnan.program.memory.FinalMemoryValue; import com.dat3m.dartagnan.program.memory.ScopedPointerVariable; -import java.util.HashMap; import java.util.List; -import java.util.Map; import static com.dat3m.dartagnan.expression.integers.IntCmpOp.*; import static com.dat3m.dartagnan.program.Program.SpecificationType.*; @@ -30,7 +27,6 @@ public class VisitorSpirvOutput extends SpirvBaseVisitor { private static final TypeFactory types = TypeFactory.getInstance(); private static final ExpressionFactory expressions = ExpressionFactory.getInstance(); - private final Map locationTypes = new HashMap<>(); private final ProgramBuilder builder; private Program.SpecificationType type; private Expression condition; @@ -48,7 +44,7 @@ public Expression visitSpvHeaders(SpirvParser.SpvHeadersContext ctx) { } if (type == null) { type = FORALL; - condition = ExpressionFactory.getInstance().makeTrue(); + condition = expressions.makeTrue(); } builder.setSpecification(type, condition); return null; @@ -103,7 +99,7 @@ public Expression visitAssertionValue(SpirvParser.AssertionValueContext ctx) { List indexes = ctx.indexValue().stream() .map(c -> Integer.parseInt(c.ModeHeader_PositiveInteger().getText())) .toList(); - return createLocation(base, indexes); + return createFinalMemoryValue(base, indexes); } throw new ParsingException("Uninitialized location %s", name); } @@ -114,9 +110,9 @@ private void appendAssertion(Program.SpecificationType newType, Expression expre condition = expression; } else if (newType.equals(type)) { if (type.equals(FORALL)) { - condition = ExpressionFactory.getInstance().makeAnd(condition, expression); + condition = expressions.makeAnd(condition, expression); } else if (type.equals(NOT_EXISTS)) { - condition = ExpressionFactory.getInstance().makeOr(condition, expression); + condition = expressions.makeOr(condition, expression); } else { throw new ParsingException("Multiline assertion is not supported for type " + newType); } @@ -126,15 +122,15 @@ private void appendAssertion(Program.SpecificationType newType, Expression expre } private Expression normalize(Expression target, Expression other) { - Type targetType = target instanceof Location ? locationTypes.get(target) : target.getType(); - Type otherType = other instanceof Location ? locationTypes.get(other) : other.getType(); + Type targetType = target.getType(); + Type otherType = other.getType(); if (targetType.equals(otherType)) { return target; } - if (target instanceof Location && other instanceof LiteralExpressionBase) { + if (target instanceof FinalMemoryValue && other.getKind() == Other.LITERAL) { return target; } - if (target instanceof IntLiteral iValue && other instanceof Location) { + if (target instanceof IntLiteral iValue && other instanceof FinalMemoryValue) { int size = types.getMemorySizeInBits(otherType); IntegerType newType = types.getIntegerType(size); return new IntLiteral(newType, iValue.getValue()); @@ -178,7 +174,7 @@ private IntCmpOp parseOperand(SpirvParser.AssertionCompareContext ctx) { throw new ParsingException("Unrecognised comparison operator"); } - private Location createLocation(ScopedPointerVariable base, List indexes) { + private FinalMemoryValue createFinalMemoryValue(ScopedPointerVariable base, List indexes) { String name = indexes.isEmpty() ? base.getId() : base.getId() + "[" + String.join("][", indexes.stream().map(Object::toString).toArray(String[]::new)) + "]"; Type elType = HelperTypes.getMemberType(base.getId(), base.getInnerType(), indexes); @@ -186,8 +182,6 @@ private Location createLocation(ScopedPointerVariable base, List indexe throw new ParsingException("Index is not deep enough for variable '%s'", name); } int offset = HelperTypes.getMemberOffset(base.getId(), 0, base.getInnerType(), indexes); - Location location = new Location(name, elType, base.getAddress(), offset); - locationTypes.put(location, elType); - return location; + return new FinalMemoryValue(name, elType, base.getAddress(), offset); } } \ No newline at end of file diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/memory/Location.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/memory/FinalMemoryValue.java similarity index 59% rename from dartagnan/src/main/java/com/dat3m/dartagnan/program/memory/Location.java rename to dartagnan/src/main/java/com/dat3m/dartagnan/program/memory/FinalMemoryValue.java index 094ecf5592..051152c72f 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/memory/Location.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/memory/FinalMemoryValue.java @@ -5,15 +5,17 @@ import com.dat3m.dartagnan.expression.Type; import com.dat3m.dartagnan.expression.base.LeafExpressionBase; -// TODO: Should be replaced with a Pointer class -public class Location extends LeafExpressionBase { +// TODO: Should work with an arbitrary pointer rather than "base + offset" +// Represents the final (co-maximal) value at a memory address as if read by a load instruction +// that observed the final store. +public class FinalMemoryValue extends LeafExpressionBase { private final String name; private final MemoryObject base; private final int offset; - public Location(String name, Type type, MemoryObject base, int offset) { - super(type); + public FinalMemoryValue(String name, Type loadType, MemoryObject base, int offset) { + super(loadType); this.name = name; this.base = base; this.offset = offset; @@ -33,12 +35,12 @@ public int getOffset() { @Override public ExpressionKind getKind() { - return ExpressionKind.Other.MEMORY_ADDR; + return ExpressionKind.Other.FINAL_MEM_VAL; } @Override public T accept(ExpressionVisitor visitor) { - return visitor.visitLocation(this); + return visitor.visitFinalMemoryValue(this); } @Override @@ -48,17 +50,12 @@ public String toString() { @Override public int hashCode() { - return base.hashCode() + offset; + return base.hashCode() + 31 * offset; } @Override public boolean equals(Object obj) { - if (this == obj) { - return true; - } else if (obj == null || getClass() != obj.getClass()) { - return false; - } - Location o = (Location) obj; - return base.equals(o.base) && offset == o.offset; + return (obj instanceof FinalMemoryValue o) && + base.equals(o.base) && offset == o.offset; } } \ No newline at end of file diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/RemoveUnusedMemory.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/RemoveUnusedMemory.java index 6feca6db62..0aeea91d3d 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/RemoveUnusedMemory.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/RemoveUnusedMemory.java @@ -4,7 +4,7 @@ import com.dat3m.dartagnan.expression.processing.ExpressionInspector; import com.dat3m.dartagnan.program.Program; import com.dat3m.dartagnan.program.event.RegReader; -import com.dat3m.dartagnan.program.memory.Location; +import com.dat3m.dartagnan.program.memory.FinalMemoryValue; import com.dat3m.dartagnan.program.memory.Memory; import com.dat3m.dartagnan.program.memory.MemoryObject; import com.google.common.collect.Sets; @@ -52,9 +52,9 @@ public Expression visitMemoryObject(MemoryObject address) { } @Override - public Expression visitLocation(Location location) { - memoryObjects.add(location.getMemoryObject()); - return location; + public Expression visitFinalMemoryValue(FinalMemoryValue val) { + memoryObjects.add(val.getMemoryObject()); + return val; } } } From 2d5695e4ddb7f300e1a69fc454d11a016c6a024d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ren=C3=A9=20Pascal=20Maseli?= Date: Sun, 11 Aug 2024 18:08:30 +0200 Subject: [PATCH 03/18] Add ReachingDefinitionsAnalysis --- .../dartagnan/encoding/ProgramEncoder.java | 49 ++++++------- .../dat3m/dartagnan/encoding/WmmEncoder.java | 17 +++-- .../program/analysis/Dependency.java | 55 ++++++++++++--- .../analysis/ReachingDefinitionsAnalysis.java | 69 +++++++++++++++++++ .../program/analysis/UseDefAnalysis.java | 56 ++++++++++++++- .../alias/InclusionBasedPointerAnalysis.java | 13 ++-- .../verification/solving/ModelChecker.java | 4 +- .../wmm/analysis/CoarseRelationAnalysis.java | 4 +- .../wmm/analysis/NativeRelationAnalysis.java | 15 ++-- .../wmm/analysis/RelationAnalysis.java | 4 +- .../dartagnan/miscellaneous/AnalysisTest.java | 37 +++++----- 11 files changed, 245 insertions(+), 78 deletions(-) create mode 100644 dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/ReachingDefinitionsAnalysis.java diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProgramEncoder.java b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProgramEncoder.java index d8d65418af..6c002e609d 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProgramEncoder.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProgramEncoder.java @@ -7,9 +7,10 @@ import com.dat3m.dartagnan.program.ScopeHierarchy; import com.dat3m.dartagnan.program.Thread; import com.dat3m.dartagnan.program.analysis.BranchEquivalence; -import com.dat3m.dartagnan.program.analysis.Dependency; import com.dat3m.dartagnan.program.analysis.ExecutionAnalysis; +import com.dat3m.dartagnan.program.analysis.ReachingDefinitionsAnalysis; import com.dat3m.dartagnan.program.event.Event; +import com.dat3m.dartagnan.program.event.RegReader; import com.dat3m.dartagnan.program.event.RegWriter; import com.dat3m.dartagnan.program.event.Tag; import com.dat3m.dartagnan.program.event.core.CondJump; @@ -51,14 +52,14 @@ public class ProgramEncoder implements Encoder { private final EncodingContext context; private final ExecutionAnalysis exec; - private final Dependency dep; + private final ReachingDefinitionsAnalysis definitions; private ProgramEncoder(EncodingContext c) { Preconditions.checkArgument(c.getTask().getProgram().isCompiled(), "The program must be compiled before encoding."); context = c; c.getAnalysisContext().requires(BranchEquivalence.class); this.exec = c.getAnalysisContext().requires(ExecutionAnalysis.class); - this.dep = c.getAnalysisContext().requires(Dependency.class); + this.definitions = c.getAnalysisContext().requires(ReachingDefinitionsAnalysis.class); } public static ProgramEncoder withContext(EncodingContext context) throws InvalidConfigurationException { @@ -243,22 +244,21 @@ public BooleanFormula encodeDependencies() { logger.info("Encoding dependencies"); final BooleanFormulaManager bmgr = context.getBooleanFormulaManager(); List enc = new ArrayList<>(); - for(Map.Entry> e : dep.getAll()) { - final Event reader = e.getKey(); - for(Map.Entry r : e.getValue().entrySet()) { - final Formula value = context.encodeExpressionAt(r.getKey(), reader); - final Dependency.State state = r.getValue(); - List overwrite = new ArrayList<>(); - for(Event writer : reverse(state.may)) { - assert writer instanceof RegWriter; + for (RegReader reader : context.getTask().getProgram().getThreadEvents(RegReader.class)) { + final ReachingDefinitionsAnalysis.Writers writers = definitions.getWriters(reader); + for (Register register : writers.getUsedRegisters()) { + final Formula value = context.encodeExpressionAt(register, reader); + final List overwrite = new ArrayList<>(); + final ReachingDefinitionsAnalysis.RegisterWriters reg = writers.ofRegister(register); + for (RegWriter writer : reverse(reg.getMayWriters())) { BooleanFormula edge; - if(state.must.contains(writer)) { + if (reg.getMustWriters().contains(writer)) { if (exec.isImplied(reader, writer) && reader.cfImpliesExec()) { // This special case is important. Usually, we encode "dep => regValue = regWriterResult" // By getting rid of the guard "dep" in this special case, we end up with an unconditional // "regValue = regWriterResult", which allows the solver to eliminate one of the variables // in preprocessing. - assert state.may.size() == 1; + assert reg.getMayWriters().size() == 1; edge = bmgr.makeTrue(); } else { edge = bmgr.and(context.execution(writer), context.controlFlow(reader)); @@ -267,10 +267,10 @@ public BooleanFormula encodeDependencies() { edge = context.dependency(writer, reader); enc.add(bmgr.equivalence(edge, bmgr.and(context.execution(writer), context.controlFlow(reader), bmgr.not(bmgr.or(overwrite))))); } - enc.add(bmgr.implication(edge, context.equal(value, context.result((RegWriter) writer)))); + enc.add(bmgr.implication(edge, context.equal(value, context.result(writer)))); overwrite.add(context.execution(writer)); } - if(initializeRegisters && !state.initialized) { + if(initializeRegisters && !reg.mustBeInitialized()) { overwrite.add(bmgr.not(context.controlFlow(reader))); overwrite.add(context.equalZero(value)); enc.add(bmgr.or(overwrite)); @@ -296,25 +296,26 @@ public BooleanFormula encodeFinalRegisterValues() { logger.info("Encoding final register values"); List enc = new ArrayList<>(); - for(Map.Entry e : dep.finalWriters().entrySet()) { - final Formula value = context.encodeFinalExpression(e.getKey()); - final Dependency.State state = e.getValue(); - final List writers = state.may; - if(initializeRegisters && !state.initialized) { + final ReachingDefinitionsAnalysis.Writers finalState = definitions.getFinalWriters(); + for (Register register : finalState.getUsedRegisters()) { + final Formula value = context.encodeFinalExpression(register); + final ReachingDefinitionsAnalysis.RegisterWriters registerWriters = finalState.ofRegister(register); + final List writers = registerWriters.getMayWriters(); + if (initializeRegisters && !registerWriters.mustBeInitialized()) { List clause = new ArrayList<>(); clause.add(context.equalZero(value)); - for(Event w : writers) { + for (Event w : writers) { clause.add(context.execution(w)); } enc.add(bmgr.or(clause)); } - for(int i = 0; i < writers.size(); i++) { + for (int i = 0; i < writers.size(); i++) { final RegWriter writer = writers.get(i); List clause = new ArrayList<>(); clause.add(context.equal(value, context.result(writer))); clause.add(bmgr.not(context.execution(writer))); - for(Event w : writers.subList(i + 1, writers.size())) { - if(!exec.areMutuallyExclusive(writer, w)) { + for (Event w : writers.subList(i + 1, writers.size())) { + if (!exec.areMutuallyExclusive(writer, w)) { clause.add(context.execution(w)); } } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/WmmEncoder.java b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/WmmEncoder.java index 47c66da65b..e966b03774 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/WmmEncoder.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/WmmEncoder.java @@ -4,9 +4,10 @@ import com.dat3m.dartagnan.configuration.Arch; import com.dat3m.dartagnan.expression.Expression; import com.dat3m.dartagnan.program.Program; -import com.dat3m.dartagnan.program.analysis.Dependency; +import com.dat3m.dartagnan.program.analysis.ReachingDefinitionsAnalysis; import com.dat3m.dartagnan.program.event.Event; import com.dat3m.dartagnan.program.event.MemoryEvent; +import com.dat3m.dartagnan.program.event.RegReader; import com.dat3m.dartagnan.program.event.RegWriter; import com.dat3m.dartagnan.program.event.Tag; import com.dat3m.dartagnan.program.event.core.ControlBarrier; @@ -390,16 +391,18 @@ public Void visitAddressDependency(DirectAddressDependency addrDirect) { } private Void visitDirectDependency(Relation r) { - Dependency dep = context.getAnalysisContext().get(Dependency.class); - EncodingContext.EdgeEncoder edge = context.edge(r); + final ReachingDefinitionsAnalysis definitions = context.getAnalysisContext() + .get(ReachingDefinitionsAnalysis.class); + final EncodingContext.EdgeEncoder edge = context.edge(r); encodeSets.get(r).apply((writer, reader) -> { - if (!(writer instanceof RegWriter rw)) { + if (!(writer instanceof RegWriter wr) || !(reader instanceof RegReader rr)) { enc.add(bmgr.not(edge.encode(writer, reader))); } else { - Dependency.State s = dep.of(reader, rw.getResultRegister()); - if (s.must.contains(writer)) { + final ReachingDefinitionsAnalysis.RegisterWriters state = definitions.getWriters(rr) + .ofRegister(wr.getResultRegister()); + if (state.getMustWriters().contains(writer)) { enc.add(bmgr.equivalence(edge.encode(writer, reader), context.execution(writer, reader))); - } else if (!s.may.contains(writer)) { + } else if (!state.getMayWriters().contains(writer)) { enc.add(bmgr.not(edge.encode(writer, reader))); } } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/Dependency.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/Dependency.java index 5faa5a7c2b..784c406897 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/Dependency.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/Dependency.java @@ -29,7 +29,7 @@ * Instances of this class store the results of the analysis, * which was performed on the instance's creation. */ -public final class Dependency { +public final class Dependency implements ReachingDefinitionsAnalysis { private static final Logger logger = LogManager.getLogger(Dependency.class); @@ -67,19 +67,20 @@ public static Dependency fromConfig(Program program, Context analysisContext, Co * Queries the collection of providers for a variable, given a certain state of the program. * * @param reader Event containing some computation over values of the register space. - * @param register Thread-local program variable used by {@code reader}. * @return Local result of this analysis. */ - public State of(Event reader, Register register) { - return map.getOrDefault(reader, Map.of()).getOrDefault(register, new State(false, List.of(), List.of())); + @Override + public Writers getWriters(RegReader reader) { + return new StateMap(map.getOrDefault(reader, Map.of())); } /** * @return Complete set of registers of the analyzed program, * mapped to program-ordered list of writers. */ - public Map finalWriters() { - return finalWriters; + @Override + public Writers getFinalWriters() { + return new StateMap(finalWriters); } /** @@ -215,24 +216,24 @@ public int hashCode() { * Indirectly associated with an instance of {@link Register}, as well as an optional event of the respective thread. * When no such event exists, the instance describes the final register values. */ - public static final class State { + public static final class State implements RegisterWriters { /** * The analysis was able to determine that in all executions, there is a provider for the register. */ - public final boolean initialized; + private final boolean initialized; /** * Complete, but unsound, program-ordered list of direct providers for the register: * If there is a program execution where an event of the program was the latest writer, that event is contained in this list. */ - public final List may; + private final List may; /** * Sound, but incomplete, program-ordered list of direct providers with no overwriting event in between: * Each event in this list will be the latest writer in any execution that contains that event. */ - public final List must; + private final List must; private State(boolean initialized, List may, List must) { verify(new HashSet<>(may).containsAll(must), "Each must-writer must also be a may-writer."); @@ -241,5 +242,39 @@ private State(boolean initialized, List may, List must) { this.may = may; this.must = must; } + + @Override + public boolean mustBeInitialized() { + return initialized; + } + + @Override + public List getMayWriters() { + return Collections.unmodifiableList(may); + } + + @Override + public List getMustWriters() { + return Collections.unmodifiableList(must); + } + } + + private static final class StateMap implements Writers { + + private final Map map; + + private StateMap(Map m) { + map = m; + } + + @Override + public Set getUsedRegisters() { + return Collections.unmodifiableSet(map.keySet()); + } + + @Override + public RegisterWriters ofRegister(Register register) { + return map.getOrDefault(register, new State(false, List.of(), List.of())); + } } } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/ReachingDefinitionsAnalysis.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/ReachingDefinitionsAnalysis.java new file mode 100644 index 0000000000..576f59ea84 --- /dev/null +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/ReachingDefinitionsAnalysis.java @@ -0,0 +1,69 @@ +package com.dat3m.dartagnan.program.analysis; + +import com.dat3m.dartagnan.program.Register; +import com.dat3m.dartagnan.program.event.RegReader; +import com.dat3m.dartagnan.program.event.RegWriter; + +import java.util.*; + +/** + * Instances of this analysis shall over-approximate the relationship between {@link RegWriter} and {@link RegReader}, + * where the writer performs the latest reassignment on the register being used by the reader. + */ +public interface ReachingDefinitionsAnalysis { + + /** + * Lists all potential definitions for registers used by an event. + * @param reader Event of interest to fetch information about. + */ + Writers getWriters(RegReader reader); + + /** + * Lists all relevant definitions for registers marked as used at the end of the program. + */ + Writers getFinalWriters(); + + /** + * Local information for either a {@link RegReader} or the final state of the program. + */ + interface Writers { + + /** + * Lists all registers directly read by the associated reader. + * @return Registers of interest. + */ + Set getUsedRegisters(); + + /** + * Fetches register-specific information from the associated state. + * @param register Contained in {@link #getUsedRegisters()}. + * @return Writers in program order. + */ + RegisterWriters ofRegister(Register register); + } + + /** + * Instances of this class are associated with a {@link Register} and either a {@link RegReader} or the final state of the program or function. + */ + interface RegisterWriters { + + /** + * Checks if the program guarantees that the register is initialized. + * @return {@code true}, if all executions have the associated reader use an initialized state, + * otherwise this property is unknown. + */ + boolean mustBeInitialized(); + + /** + * Lists writers s.t. there may be executions, where some instance of the associated reader directly uses the result of an instance of that writer. + * @return Writers in program order. + */ + List getMayWriters(); + + /** + * Lists writers s.t. all event instances of the associated reader in any execution read from all instances of that writer in that execution. + * @return Writers in program order. + */ + List getMustWriters(); + } +} diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/UseDefAnalysis.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/UseDefAnalysis.java index af83d85a66..15557f5c82 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/UseDefAnalysis.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/UseDefAnalysis.java @@ -9,8 +9,11 @@ import com.dat3m.dartagnan.program.event.core.CondJump; import com.dat3m.dartagnan.program.event.core.Label; +import java.util.Collections; +import java.util.Comparator; import java.util.HashMap; import java.util.HashSet; +import java.util.List; import java.util.Map; import java.util.Set; @@ -27,7 +30,7 @@ then it does not necessarily mean that the writer is the only one (maybe an unin The main difference is that this analysis works independently of other analyses (e.g., it does not depend on ExecutionAnalysis) and can be used on single functions. */ -public class UseDefAnalysis { +public class UseDefAnalysis implements ReachingDefinitionsAnalysis { private Map>> useDefGraph; @@ -47,6 +50,57 @@ public Set getDefs(Event regReader, Register register) { return getDefs(regReader).getOrDefault(register, Set.of()); } + @Override + public Writers getWriters(RegReader reader) { + return new WritersView(useDefGraph.getOrDefault(reader, new HashMap<>())); + } + + @Override + public Writers getFinalWriters() { + return new WritersView(new HashMap<>()); + } + + private static final class WritersView implements Writers { + private final Map> useDefByRegister; + + private WritersView(Map> useDefByRegister) { + this.useDefByRegister = useDefByRegister; + } + + @Override + public Set getUsedRegisters() { + return Collections.unmodifiableSet(useDefByRegister.keySet()); + } + + @Override + public RegisterWriters ofRegister(Register register) { + return new RegisterInfo(useDefByRegister.getOrDefault(register, new HashSet<>())); + } + } + + private static final class RegisterInfo implements RegisterWriters { + private final Set useDefSet; + + private RegisterInfo(Set useDefSet) { + this.useDefSet = useDefSet; + } + + @Override + public boolean mustBeInitialized() { + return false; + } + + @Override + public List getMayWriters() { + return useDefSet.stream().sorted(Comparator.comparingInt(Event::getGlobalId)).toList(); + } + + @Override + public List getMustWriters() { + return List.of(); + } + } + // ====================================================================== private void computeForFunction(Function function) { diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/alias/InclusionBasedPointerAnalysis.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/alias/InclusionBasedPointerAnalysis.java index 996c23a160..1784be5cc8 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/alias/InclusionBasedPointerAnalysis.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/alias/InclusionBasedPointerAnalysis.java @@ -6,7 +6,7 @@ import com.dat3m.dartagnan.expression.misc.ITEExpr; import com.dat3m.dartagnan.program.Program; import com.dat3m.dartagnan.program.Register; -import com.dat3m.dartagnan.program.analysis.Dependency; +import com.dat3m.dartagnan.program.analysis.ReachingDefinitionsAnalysis; import com.dat3m.dartagnan.program.analysis.SyntacticContextAnalysis; import com.dat3m.dartagnan.program.event.RegReader; import com.dat3m.dartagnan.program.event.RegWriter; @@ -71,8 +71,8 @@ public class InclusionBasedPointerAnalysis implements AliasAnalysis { private static final Logger logger = LogManager.getLogger(InclusionBasedPointerAnalysis.class); - // This analysis depends on the results of a Dependency analysis, mapping used registers to a list of possible writers. - private final Dependency dependency; + // This analysis depends on another, that maps used registers to a list of possible direct writers. + private final ReachingDefinitionsAnalysis dependency; // For providing helpful error messages, this analysis prints call-stack and loop information for events. private final Supplier synContext; @@ -117,7 +117,8 @@ private record IntPair(int x, int y) { // ================================ Construction ================================ public static InclusionBasedPointerAnalysis fromConfig(Program program, Context analysisContext, AliasAnalysis.Config config) { - final var analysis = new InclusionBasedPointerAnalysis(program, analysisContext.requires(Dependency.class)); + final ReachingDefinitionsAnalysis def = analysisContext.requires(ReachingDefinitionsAnalysis.class); + final var analysis = new InclusionBasedPointerAnalysis(program, def); analysis.run(program, config); logger.debug("variable count: {}", analysis.totalVariables); @@ -138,7 +139,7 @@ public static InclusionBasedPointerAnalysis fromConfig(Program program, Context return analysis; } - private InclusionBasedPointerAnalysis(Program p, Dependency d) { + private InclusionBasedPointerAnalysis(Program p, ReachingDefinitionsAnalysis d) { dependency = d; synContext = Suppliers.memoize(() -> SyntacticContextAnalysis.newInstance(p)); } @@ -892,7 +893,7 @@ private DerivedVariable getResultVariable(Expression expression, RegReader reade // Constructs a new node, if there are multiple writers. private DerivedVariable getPhiNodeVariable(Register register, RegReader reader) { // We assume here that uninitialized values carry no meaningful address to any memory object. - final List writers = dependency.of(reader, register).may; + final List writers = dependency.getWriters(reader).ofRegister(register).getMayWriters(); final DerivedVariable find = registerVariables.get(writers); if (find != null) { return find; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/ModelChecker.java b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/ModelChecker.java index cac688c576..1a6b417fe8 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/ModelChecker.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/ModelChecker.java @@ -83,7 +83,9 @@ public static void performStaticProgramAnalyses(VerificationTask task, Context a Program program = task.getProgram(); analysisContext.register(BranchEquivalence.class, BranchEquivalence.fromConfig(program, config)); analysisContext.register(ExecutionAnalysis.class, ExecutionAnalysis.fromConfig(program, analysisContext, config)); - analysisContext.register(Dependency.class, Dependency.fromConfig(program, analysisContext, config)); + final Dependency dependency = Dependency.fromConfig(program, analysisContext, config); + analysisContext.register(ReachingDefinitionsAnalysis.class, dependency); + analysisContext.register(Dependency.class, dependency); analysisContext.register(AliasAnalysis.class, AliasAnalysis.fromConfig(program, analysisContext, config)); analysisContext.register(ThreadSymmetry.class, ThreadSymmetry.fromConfig(program, config)); for(Thread thread : program.getThreads()) { diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/analysis/CoarseRelationAnalysis.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/analysis/CoarseRelationAnalysis.java index ed6e99e5c1..34ac4b120f 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/analysis/CoarseRelationAnalysis.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/analysis/CoarseRelationAnalysis.java @@ -1,7 +1,7 @@ package com.dat3m.dartagnan.wmm.analysis; -import com.dat3m.dartagnan.program.analysis.Dependency; import com.dat3m.dartagnan.program.analysis.ExecutionAnalysis; +import com.dat3m.dartagnan.program.analysis.ReachingDefinitionsAnalysis; import com.dat3m.dartagnan.program.analysis.alias.AliasAnalysis; import com.dat3m.dartagnan.program.event.Event; import com.dat3m.dartagnan.utils.dependable.DependencyGraph; @@ -31,7 +31,7 @@ private CoarseRelationAnalysis(VerificationTask t, Context context, Configuratio * Should at least include the following elements: *
    *
  • {@link ExecutionAnalysis} - *
  • {@link Dependency} + *
  • {@link ReachingDefinitionsAnalysis} *
  • {@link AliasAnalysis} *
  • {@link WmmAnalysis} *
diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/analysis/NativeRelationAnalysis.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/analysis/NativeRelationAnalysis.java index 2f9ec76059..cf004b8c9d 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/analysis/NativeRelationAnalysis.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/analysis/NativeRelationAnalysis.java @@ -5,8 +5,8 @@ import com.dat3m.dartagnan.program.Register.UsageType; import com.dat3m.dartagnan.program.Thread; import com.dat3m.dartagnan.program.analysis.BranchEquivalence; -import com.dat3m.dartagnan.program.analysis.Dependency; import com.dat3m.dartagnan.program.analysis.ExecutionAnalysis; +import com.dat3m.dartagnan.program.analysis.ReachingDefinitionsAnalysis; import com.dat3m.dartagnan.program.analysis.alias.AliasAnalysis; import com.dat3m.dartagnan.program.event.Event; import com.dat3m.dartagnan.program.event.MemoryEvent; @@ -57,8 +57,8 @@ public class NativeRelationAnalysis implements RelationAnalysis { protected final VerificationTask task; protected final Context analysisContext; protected final ExecutionAnalysis exec; + protected final ReachingDefinitionsAnalysis definitions; protected final AliasAnalysis alias; - protected final Dependency dep; protected final WmmAnalysis wmmAnalysis; protected final Map knowledgeMap = new HashMap<>(); protected final EventGraph mutex = new EventGraph(); @@ -67,8 +67,8 @@ protected NativeRelationAnalysis(VerificationTask t, Context context, Configurat task = checkNotNull(t); analysisContext = context; exec = context.requires(ExecutionAnalysis.class); + definitions = context.requires(ReachingDefinitionsAnalysis.class); alias = context.requires(AliasAnalysis.class); - dep = context.requires(Dependency.class); wmmAnalysis = context.requires(WmmAnalysis.class); } @@ -80,7 +80,7 @@ protected NativeRelationAnalysis(VerificationTask t, Context context, Configurat * Should at least include the following elements: *
    *
  • {@link ExecutionAnalysis} - *
  • {@link Dependency} + *
  • {@link ReachingDefinitionsAnalysis} *
  • {@link AliasAnalysis} *
  • {@link WmmAnalysis} *
@@ -937,6 +937,7 @@ private Knowledge computeInternalDependencies(Set usageTypes) { EventGraph must = new EventGraph(); for (RegReader regReader : program.getThreadEvents(RegReader.class)) { + final ReachingDefinitionsAnalysis.Writers state = definitions.getWriters(regReader); for (Register.Read regRead : regReader.getRegisterReads()) { if (!usageTypes.contains(regRead.usageType())) { continue; @@ -950,11 +951,11 @@ private Knowledge computeInternalDependencies(Set usageTypes) { if (program.getArch().equals(RISCV) && register.getName().equals("x0")) { continue; } - Dependency.State r = dep.of(regReader, register); - for (Event regWriter : r.may) { + final List writers = state.ofRegister(register).getMayWriters(); + for (Event regWriter : writers) { may.add(regWriter, regReader); } - for (Event regWriter : r.must) { + for (Event regWriter : writers) { must.add(regWriter, regReader); } } 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 de5de01ce1..3649ded132 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 @@ -1,8 +1,8 @@ package com.dat3m.dartagnan.wmm.analysis; import com.dat3m.dartagnan.configuration.RelationAnalysisMethod; -import com.dat3m.dartagnan.program.analysis.Dependency; import com.dat3m.dartagnan.program.analysis.ExecutionAnalysis; +import com.dat3m.dartagnan.program.analysis.ReachingDefinitionsAnalysis; import com.dat3m.dartagnan.program.analysis.alias.AliasAnalysis; import com.dat3m.dartagnan.utils.Utils; import com.dat3m.dartagnan.verification.Context; @@ -35,7 +35,7 @@ public interface RelationAnalysis { * Should at least include the following elements: *
    *
  • {@link ExecutionAnalysis} - *
  • {@link Dependency} + *
  • {@link ReachingDefinitionsAnalysis} *
  • {@link AliasAnalysis} *
  • {@link WmmAnalysis} *
diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/miscellaneous/AnalysisTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/miscellaneous/AnalysisTest.java index 78a4bd0b85..c4809d640f 100644 --- a/dartagnan/src/test/java/com/dat3m/dartagnan/miscellaneous/AnalysisTest.java +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/miscellaneous/AnalysisTest.java @@ -15,6 +15,7 @@ import com.dat3m.dartagnan.program.analysis.alias.AliasAnalysis; import com.dat3m.dartagnan.program.event.Event; import com.dat3m.dartagnan.program.event.EventFactory; +import com.dat3m.dartagnan.program.event.RegReader; import com.dat3m.dartagnan.program.event.core.*; import com.dat3m.dartagnan.program.event.metadata.OriginalId; import com.dat3m.dartagnan.program.memory.MemoryObject; @@ -80,24 +81,24 @@ public void dependencyMustOverride() throws InvalidConfigurationException { context.register(BranchEquivalence.class, BranchEquivalence.fromConfig(program, config)); context.register(ExecutionAnalysis.class, ExecutionAnalysis.fromConfig(program, context, config)); Dependency dep = Dependency.fromConfig(program, context, config); - Event me0 = findMatchingEventAfterProcessing(program, e0); - Event me1 = findMatchingEventAfterProcessing(program, e1); - Event me2 = findMatchingEventAfterProcessing(program, e2); - Event me3 = findMatchingEventAfterProcessing(program, e3); - Event me4 = findMatchingEventAfterProcessing(program, e4); - Event me5 = findMatchingEventAfterProcessing(program, e5); - assertTrue(dep.of(me1, r0).initialized); - assertList(dep.of(me1, r0).may, me0); - assertList(dep.of(me1, r0).must, me0); - assertFalse(dep.of(me3, r0).initialized); - assertList(dep.of(me3, r0).may, me0); - assertList(dep.of(me3, r0).must, me0); - assertTrue(dep.of(me4, r1).initialized); - assertList(dep.of(me4, r1).may, me1, me2); - assertList(dep.of(me4, r1).must, me1, me2); - assertTrue(dep.of(me5, r2).initialized); - assertList(dep.of(me5, r2).may, me4); - assertList(dep.of(me5, r2).must, me4); + var me0 = (RegReader) findMatchingEventAfterProcessing(program, e0); + var me1 = (RegReader) findMatchingEventAfterProcessing(program, e1); + var me2 = (RegReader) findMatchingEventAfterProcessing(program, e2); + var me3 = (RegReader) findMatchingEventAfterProcessing(program, e3); + var me4 = (RegReader) findMatchingEventAfterProcessing(program, e4); + var me5 = (RegReader) findMatchingEventAfterProcessing(program, e5); + assertTrue(dep.getWriters(me1).ofRegister(r0).mustBeInitialized()); + assertList(dep.getWriters(me1).ofRegister(r0).getMayWriters(), me0); + assertList(dep.getWriters(me1).ofRegister(r0).getMustWriters(), me0); + assertFalse(dep.getWriters(me3).ofRegister(r0).mustBeInitialized()); + assertList(dep.getWriters(me3).ofRegister(r0).getMayWriters(), me0); + assertList(dep.getWriters(me3).ofRegister(r0).getMustWriters(), me0); + assertTrue(dep.getWriters(me4).ofRegister(r1).mustBeInitialized()); + assertList(dep.getWriters(me4).ofRegister(r1).getMayWriters(), me1, me2); + assertList(dep.getWriters(me4).ofRegister(r1).getMustWriters(), me1, me2); + assertTrue(dep.getWriters(me5).ofRegister(r2).mustBeInitialized()); + assertList(dep.getWriters(me5).ofRegister(r2).getMayWriters(), me4); + assertList(dep.getWriters(me5).ofRegister(r2).getMustWriters(), me4); } @Test From 27cee4fdc2b307a1f9c5e0c7fe78eeb7741808a0 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ren=C3=A9=20Pascal=20Maseli?= Date: Mon, 2 Sep 2024 11:07:36 +0200 Subject: [PATCH 04/18] Add BackwardsReachingDefinitionsAnalysis --- .../BackwardsReachingDefinitionsAnalysis.java | 388 ++++++++++++++++++ 1 file changed, 388 insertions(+) create mode 100644 dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/BackwardsReachingDefinitionsAnalysis.java diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/BackwardsReachingDefinitionsAnalysis.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/BackwardsReachingDefinitionsAnalysis.java new file mode 100644 index 0000000000..5495a97005 --- /dev/null +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/BackwardsReachingDefinitionsAnalysis.java @@ -0,0 +1,388 @@ +package com.dat3m.dartagnan.program.analysis; + +import com.dat3m.dartagnan.program.Function; +import com.dat3m.dartagnan.program.Program; +import com.dat3m.dartagnan.program.Register; +import com.dat3m.dartagnan.program.event.Event; +import com.dat3m.dartagnan.program.event.RegReader; +import com.dat3m.dartagnan.program.event.RegWriter; +import com.dat3m.dartagnan.program.event.core.CondJump; +import com.dat3m.dartagnan.program.event.core.Label; +import com.dat3m.dartagnan.verification.Context; +import com.google.common.base.Preconditions; +import com.google.common.collect.Iterables; + +import java.util.ArrayList; +import java.util.Collection; +import java.util.Collections; +import java.util.Comparator; +import java.util.HashMap; +import java.util.HashSet; +import java.util.List; +import java.util.Map; +import java.util.Set; + +/** + * Collects all direct usage relationships between {@link RegWriter} and {@link RegReader}. + *

+ * In contrast to a usual Reaching-Definitions-Analysis, + * this implementation analyzes the program from back to front, + * assigning each program point the set of readers, + * who may still require a register initialization. + * This means that it does not collect definitions for unused registers. + * Especially, it does not collect last writers for all registers. + *

+ * This analysis is control-flow-sensitive; + * that is, {@link Label} splits the information among the jumps to it + * and {@link CondJump} merges the information. + *

+ * This analysis supports loops; + * that is, backward jumps cause re-evaluation of the loop body until convergence. + * This results in a squared worst-case time complexity. + */ +public class BackwardsReachingDefinitionsAnalysis implements ReachingDefinitionsAnalysis { + + private final Map readerMap = new HashMap<>(); + private final Map writerMap = new HashMap<>(); + + @Override + public Writers getWriters(RegReader reader) { + Preconditions.checkNotNull(reader, "reader is null"); + final ReaderInfo result = readerMap.get(reader); + Preconditions.checkArgument(result != null, "reader %s has not been analyzed.", reader); + return result; + } + + @Override + public Writers getFinalWriters() { + final ReaderInfo result = readerMap.get(null); + Preconditions.checkState(result != null, "final state has not been analyzed."); + return result; + } + + /** + * Lists all potential users of the result of an event. + * @param writer Event of interest to fetch information about. + * @throws IllegalArgumentException If {@code writer} was not inside the program when it was analyzed. + */ + public Readers getReaders(RegWriter writer) { + Preconditions.checkNotNull(writer, "writer is null"); + final Readers result = writerMap.get(writer); + Preconditions.checkArgument(result != null, "writer %s has not been analyzed.", writer); + return result; + } + + /** + * Lists all potential users of uninitialized registers. + */ + public Readers getInitialReaders() { + final Readers result = writerMap.get(null); + Preconditions.checkState(result != null, "initial state has not been analyzed."); + return result; + } + + /** + * Analyzes an entire function definition. + * @param function Defined function to be analyzed. Its parameters are marked as initialized. + */ + public static BackwardsReachingDefinitionsAnalysis forFunction(Function function) { + final var analysis = new BackwardsReachingDefinitionsAnalysis(); + final Set finalRegisters = new HashSet<>(); + analysis.initialize(function, finalRegisters); + analysis.run(function, finalRegisters); + analysis.postProcess(); + return analysis; + } + + /** + * Analyzes an entire set of threads. + * @param program Contains a set of threads to be analyzed. Additionally-defined functions are ignored. + * @param branch Optional, queried for possibility of pairs of writers appearing together in an execution. + */ + public static BackwardsReachingDefinitionsAnalysis forProgram(Program program, BranchEquivalence branch) { + final var analysis = new BackwardsReachingDefinitionsAnalysis(); + final Set finalRegisters = finalRegisters(program); + for (Function function : program.isUnrolled() ? program.getThreads() : + Iterables.concat(program.getThreads(), program.getFunctions())) { + analysis.initialize(function, finalRegisters); + analysis.run(function, finalRegisters); + } + analysis.postProcess(); + if (branch != null && program.isUnrolled()) { + analysis.analyzeMust(branch); + } + return analysis; + } + + public static BackwardsReachingDefinitionsAnalysis injectForProgram(Program program, Context analysisContext) { + final BranchEquivalence branch = analysisContext.get(BranchEquivalence.class); + final BackwardsReachingDefinitionsAnalysis analysis = forProgram(program, branch); + analysisContext.register(BackwardsReachingDefinitionsAnalysis.class, analysis); + analysisContext.register(ReachingDefinitionsAnalysis.class, analysis); + return analysis; + } + + private static Set finalRegisters(Program program) { + final Set finalRegisters = new HashSet<>(); + if (program.getSpecification() != null) { + finalRegisters.addAll(program.getSpecification().getRegs()); + } + if (program.getFilterSpecification() != null) { + finalRegisters.addAll(program.getFilterSpecification().getRegs()); + } + return finalRegisters; + } + + /** + * Local information for either a {@link RegReader} or the final state of the program. + */ + private static final class ReaderInfo implements Writers { + + private final Set used; + private final List mayWriters = new ArrayList<>(); + private final List mustWriters = new ArrayList<>(); + private final Set uninitialized = new HashSet<>(); + + private ReaderInfo(Set u) { + used = Set.copyOf(u); + } + + @Override + public Set getUsedRegisters() { + return used; + } + + @Override + public RegisterWriters ofRegister(Register register) { + return new RegisterWritersView(this, register); + } + } + + private static final class RegisterWritersView implements RegisterWriters { + + private final ReaderInfo info; + private final Register register; + + private RegisterWritersView(ReaderInfo info, Register register) { + this.info = info; + this.register = register; + } + + @Override + public List getMayWriters() { + return info.mayWriters.stream().filter(w -> w.getResultRegister().equals(register)).toList(); + } + + @Override + public List getMustWriters() { + return info.mustWriters.stream().filter(w -> w.getResultRegister().equals(register)).toList(); + } + + @Override + public boolean mustBeInitialized() { + return !info.uninitialized.contains(register); + } + } + + /** + * Local information for either a {@link RegWriter} or the initial state of the program. + */ + public static final class Readers { + + private final Set readers = new HashSet<>(); + private boolean mayBeFinal; + + private Readers() {} + + /** + * Lists readers s.t. there may be an execution where an instance of that reader uses the result of an instance of the associated writer. + * @return Unordered set of Readers. + */ + public Collection getReaders() { + return Collections.unmodifiableCollection(readers); + } + + /** + * @return {@code true} if there may be an execution, where an instance of the associated writer defines the last value of its register. + */ + public boolean mayBeFinal() { + return mayBeFinal; + } + } + + private BackwardsReachingDefinitionsAnalysis() {} + + private void initialize(Function function, Set finalRegisters) { + for (Event event : function.getEvents()) { + if (event instanceof RegWriter writer) { + writerMap.put(writer, new Readers()); + } + } + writerMap.put(null, new Readers()); + for (Event event : function.getEvents()) { + if (event instanceof RegReader reader) { + final Set usedRegisters = new HashSet<>(); + for (Register.Read read : reader.getRegisterReads()) { + usedRegisters.add(read.register()); + } + readerMap.put(reader, new ReaderInfo(usedRegisters)); + } + } + readerMap.put(null, new ReaderInfo(finalRegisters)); + } + + private void run(Function function, Set finalRegisters) { + //For each register used after this state, all future users. + final State currentState = new State(); + for (Register finalRegister : finalRegisters) { + final var info = new StateInfo(); + info.mayReaders.add(null); + currentState.put(finalRegister, info); + } + final Map trueStates = new HashMap<>(); + final Map falseStates = new HashMap<>(); + final List events = function.getEvents(); + for (int i = events.size() - 1; i >= 0; i--) { + final CondJump loop = runLocal(events.get(i), currentState, trueStates, falseStates); + if (loop != null) { + merge(currentState, falseStates.getOrDefault(loop, new State())); + update(currentState, loop); + i = events.indexOf(loop); + } + } + // set the uninitialized flags + final Readers uninitialized = writerMap.get(null); + for (Map.Entry entry : currentState.entrySet()) { + uninitialized.readers.addAll(entry.getValue().mayReaders); + for (RegReader reader : entry.getValue().mayReaders) { + readerMap.get(reader).uninitialized.add(entry.getKey()); + } + } + } + + private void postProcess() { + // build the reverse association + for (Map.Entry entry : writerMap.entrySet()) { + if (entry.getKey() == null) { + continue; + } + for (RegReader reader : entry.getValue().readers) { + List mayWriters = readerMap.get(reader).mayWriters; + assert !mayWriters.contains(entry.getKey()); + mayWriters.add(entry.getKey()); + } + } + final Comparator byGlobalId = Comparator.comparingInt(RegWriter::getGlobalId); + for (Map.Entry entry : readerMap.entrySet()) { + entry.getValue().mayWriters.sort(byGlobalId); + } + // set the final flag + for (Readers writer : writerMap.values()) { + writer.mayBeFinal = writer.readers.remove(null); + } + } + + private static final class State extends HashMap {} + + private static final class StateInfo { + private Set mayReaders = new HashSet<>(); + private boolean copyOnWrite; + } + + private CondJump runLocal(Event event, State currentState, Map trueStates, Map falseStates) { + if (event instanceof Label label) { + CondJump latest = null; + // Update all jumps. + for (CondJump jump : label.getJumpSet()) { + if (jump.isDead()) { + continue; + } + final boolean change = merge(trueStates.computeIfAbsent(jump, k -> new State()), currentState); + if (change && (latest == null || latest.getGlobalId() < jump.getGlobalId())) { + latest = jump; + } + } + // If exists, repeat from most distant back jump. + // Occurs linear-many times due to guaranteed progress. + if (latest != null && label.getGlobalId() < latest.getGlobalId()) { + return latest; + } + } + if (event instanceof CondJump jump && !jump.isDead()) { + if (jump.isGoto()) { + currentState.clear(); + } else { + merge(falseStates.computeIfAbsent(jump, k -> new State()), currentState); + } + merge(currentState, trueStates.getOrDefault(jump, new State())); + } + if (event instanceof RegWriter writer) { + final Register register = writer.getResultRegister(); + final StateInfo state = writer.cfImpliesExec() ? currentState.remove(register) : currentState.get(register); + if (state != null) { + writerMap.get(writer).readers.addAll(state.mayReaders); + } + } + if (event instanceof RegReader reader) { + update(currentState, reader); + } + return null; + } + + private static void update(State states, RegReader reader) { + for (Register register : reader.getRegisterReads().stream().map(Register.Read::register).distinct().toList()) { + final StateInfo state = states.computeIfAbsent(register, k -> new StateInfo()); + state.mayReaders = state.copyOnWrite ? new HashSet<>(state.mayReaders) : state.mayReaders; + state.copyOnWrite = false; + state.mayReaders.add(reader); + } + } + + private static boolean merge(State target, State source) { + boolean change = false; + for (Map.Entry entry : source.entrySet()) { + change |= merge(target.computeIfAbsent(entry.getKey(), k -> new StateInfo()), entry.getValue()); + } + return change; + } + + private static boolean merge(StateInfo target, StateInfo source) { + if (target.mayReaders.containsAll(source.mayReaders)) { + return false; + } + assert !source.mayReaders.isEmpty(); + if (target.mayReaders.isEmpty()) { + target.mayReaders = source.mayReaders; + target.copyOnWrite = source.copyOnWrite = true; + return true; + } + target.mayReaders = target.copyOnWrite ? new HashSet<>(target.mayReaders) : target.mayReaders; + target.copyOnWrite = false; + target.mayReaders.addAll(source.mayReaders); + return true; + } + + private void analyzeMust(BranchEquivalence branch) { + // Require that function is unrolled. + for (ReaderInfo reader : readerMap.values()) { + for (int i = 0; i < reader.mayWriters.size(); i++) { + final RegWriter writer = reader.mayWriters.get(i); + if (!mayBeOverwritten(writer, reader.mayWriters.subList(i+1, reader.mayWriters.size()), branch)) { + reader.mustWriters.add(writer); + } + } + } + } + + private static boolean mayBeOverwritten(RegWriter earlyWriter, List lateWriters, BranchEquivalence branch) { + final Register resultRegister = earlyWriter.getResultRegister(); + final Set exclusiveClasses = branch.getEquivalenceClass(earlyWriter).getExclusiveClasses(); + for (RegWriter lateWriter : lateWriters) { + if (lateWriter.getResultRegister().equals(resultRegister) && + !exclusiveClasses.contains(branch.getEquivalenceClass(lateWriter))) { + return true; + } + } + return false; + } +} From c12af07e5c080108cad26b8c4ae81ea40b05e8a5 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ren=C3=A9=20Pascal=20Maseli?= Date: Mon, 2 Sep 2024 11:29:48 +0200 Subject: [PATCH 05/18] Replace Dependency with BackwardsReachingDefinitionsAnalysis --- .../dat3m/dartagnan/verification/solving/ModelChecker.java | 4 +--- .../com/dat3m/dartagnan/miscellaneous/AnalysisTest.java | 7 +++---- 2 files changed, 4 insertions(+), 7 deletions(-) diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/ModelChecker.java b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/ModelChecker.java index 1a6b417fe8..2b004a1cb8 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/ModelChecker.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/ModelChecker.java @@ -83,9 +83,7 @@ public static void performStaticProgramAnalyses(VerificationTask task, Context a Program program = task.getProgram(); analysisContext.register(BranchEquivalence.class, BranchEquivalence.fromConfig(program, config)); analysisContext.register(ExecutionAnalysis.class, ExecutionAnalysis.fromConfig(program, analysisContext, config)); - final Dependency dependency = Dependency.fromConfig(program, analysisContext, config); - analysisContext.register(ReachingDefinitionsAnalysis.class, dependency); - analysisContext.register(Dependency.class, dependency); + BackwardsReachingDefinitionsAnalysis.injectForProgram(program, analysisContext); analysisContext.register(AliasAnalysis.class, AliasAnalysis.fromConfig(program, analysisContext, config)); analysisContext.register(ThreadSymmetry.class, ThreadSymmetry.fromConfig(program, config)); for(Thread thread : program.getThreads()) { diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/miscellaneous/AnalysisTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/miscellaneous/AnalysisTest.java index c4809d640f..6eda1dcb70 100644 --- a/dartagnan/src/test/java/com/dat3m/dartagnan/miscellaneous/AnalysisTest.java +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/miscellaneous/AnalysisTest.java @@ -9,8 +9,8 @@ import com.dat3m.dartagnan.program.Program; import com.dat3m.dartagnan.program.Program.SourceLanguage; import com.dat3m.dartagnan.program.Register; +import com.dat3m.dartagnan.program.analysis.BackwardsReachingDefinitionsAnalysis; import com.dat3m.dartagnan.program.analysis.BranchEquivalence; -import com.dat3m.dartagnan.program.analysis.Dependency; import com.dat3m.dartagnan.program.analysis.ExecutionAnalysis; import com.dat3m.dartagnan.program.analysis.alias.AliasAnalysis; import com.dat3m.dartagnan.program.event.Event; @@ -79,8 +79,7 @@ public void dependencyMustOverride() throws InvalidConfigurationException { Configuration config = Configuration.defaultConfiguration(); Context context = Context.create(); context.register(BranchEquivalence.class, BranchEquivalence.fromConfig(program, config)); - context.register(ExecutionAnalysis.class, ExecutionAnalysis.fromConfig(program, context, config)); - Dependency dep = Dependency.fromConfig(program, context, config); + final var dep = BackwardsReachingDefinitionsAnalysis.injectForProgram(program, context); var me0 = (RegReader) findMatchingEventAfterProcessing(program, e0); var me1 = (RegReader) findMatchingEventAfterProcessing(program, e1); var me2 = (RegReader) findMatchingEventAfterProcessing(program, e2); @@ -514,7 +513,7 @@ private AliasAnalysis analyze(Program program, Alias method) throws InvalidConfi Context analysisContext = Context.create(); analysisContext.register(BranchEquivalence.class, BranchEquivalence.fromConfig(program, configuration)); analysisContext.register(ExecutionAnalysis.class, ExecutionAnalysis.fromConfig(program, analysisContext, configuration)); - analysisContext.register(Dependency.class, Dependency.fromConfig(program, analysisContext, configuration)); + BackwardsReachingDefinitionsAnalysis.injectForProgram(program, analysisContext); return AliasAnalysis.fromConfig(program, analysisContext, configuration); } From ae5c2bc59c7771987e7311a3e7cf87c7c3f416ad Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ren=C3=A9=20Pascal=20Maseli?= Date: Mon, 2 Sep 2024 11:32:14 +0200 Subject: [PATCH 06/18] Replace UseDefAnalysis with BackwardsReachingDefinitionsAnalysis --- .../processing/NaiveLoopBoundAnnotation.java | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/NaiveLoopBoundAnnotation.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/NaiveLoopBoundAnnotation.java index a558858f51..f40fe4c62f 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/NaiveLoopBoundAnnotation.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/NaiveLoopBoundAnnotation.java @@ -6,10 +6,11 @@ import com.dat3m.dartagnan.expression.misc.ITEExpr; import com.dat3m.dartagnan.program.Function; import com.dat3m.dartagnan.program.Register; +import com.dat3m.dartagnan.program.analysis.BackwardsReachingDefinitionsAnalysis; import com.dat3m.dartagnan.program.analysis.DominatorAnalysis; import com.dat3m.dartagnan.program.analysis.LiveRegistersAnalysis; import com.dat3m.dartagnan.program.analysis.LoopAnalysis; -import com.dat3m.dartagnan.program.analysis.UseDefAnalysis; +import com.dat3m.dartagnan.program.analysis.ReachingDefinitionsAnalysis; import com.dat3m.dartagnan.program.event.Event; import com.dat3m.dartagnan.program.event.EventFactory; import com.dat3m.dartagnan.program.event.RegWriter; @@ -19,7 +20,6 @@ import com.dat3m.dartagnan.utils.DominatorTree; import java.util.List; -import java.util.Set; /* This pass adds a loop bound annotation to static loops of the form @@ -56,7 +56,7 @@ public void run(Function function) { } final LiveRegistersAnalysis liveAnalysis = LiveRegistersAnalysis.forFunction(function); - final UseDefAnalysis useDefAnalysis = UseDefAnalysis.forFunction(function); + final ReachingDefinitionsAnalysis useDefAnalysis = BackwardsReachingDefinitionsAnalysis.forFunction(function); final DominatorTree preDominatorTree = DominatorAnalysis.computePreDominatorTree(function.getEntry(), function.getExit()); final List loops = LoopAnalysis.onFunction(function).getLoopsOfFunction(function); @@ -123,7 +123,7 @@ public void run(Function function) { // Check if there is a single increment to the register. // If there is, it returns the event performing the increment, otherwise it returns null. private Event findUniqueIncrement(List events, Register register, - UseDefAnalysis useDefAnalysis, DominatorTree preDominatorTree) { + ReachingDefinitionsAnalysis useDefAnalysis, DominatorTree preDominatorTree) { final RegWriter source = findUniqueSource(events, register, useDefAnalysis, preDominatorTree); if (source == null) { return null; @@ -142,7 +142,7 @@ private Event findUniqueIncrement(List events, Register register, } private Expression computeLoopBound(List events, Register exitReg, Register counterReg, int counterRegInitVal, - UseDefAnalysis useDefAnalysis, DominatorTree preDominatorTree) { + ReachingDefinitionsAnalysis useDefAnalysis, DominatorTree preDominatorTree) { final RegWriter exitSource = findUniqueSource(events, exitReg, useDefAnalysis, preDominatorTree); if (exitSource == null) { @@ -168,7 +168,7 @@ private Expression computeLoopBound(List events, Register exitReg, Regist // Finds the unique non-trivial assignment that (possibly indirectly) provides the value of // Returns NULL, if no such unique assignment exists. - private RegWriter findUniqueSource(List events, Register register, UseDefAnalysis useDefAnalysis, DominatorTree preDominatorTree) { + private RegWriter findUniqueSource(List events, Register register, ReachingDefinitionsAnalysis useDefAnalysis, DominatorTree preDominatorTree) { final List writers = events.stream() .filter(e -> e instanceof RegWriter writer && writer.getResultRegister().equals(register)) .map(RegWriter.class::cast).toList(); @@ -187,10 +187,10 @@ private RegWriter findUniqueSource(List events, Register register, UseDef return source; } - private RegWriter chaseUseDefChain(RegWriter assignment, UseDefAnalysis useDefAnalysis, DominatorTree preDominatorTree) { + private RegWriter chaseUseDefChain(RegWriter assignment, ReachingDefinitionsAnalysis useDefAnalysis, DominatorTree preDominatorTree) { RegWriter cur = assignment; while (cur instanceof Local loc && loc.getExpr() instanceof Register reg) { - final Set defs = useDefAnalysis.getDefs(loc, reg); + final List defs = useDefAnalysis.getWriters(loc).ofRegister(reg).getMayWriters(); if (defs.size() != 1) { // Multiple assignments (or none): too complex so give up. return null; From 38bd709a65eea325ee0de1b827fe594ba6047f83 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ren=C3=A9=20Pascal=20Maseli?= Date: Mon, 2 Sep 2024 12:50:04 +0200 Subject: [PATCH 07/18] Add AnalysisTest.reachingDefinitionSupportsLoops --- .../dartagnan/miscellaneous/AnalysisTest.java | 117 +++++++++++++++++- 1 file changed, 115 insertions(+), 2 deletions(-) diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/miscellaneous/AnalysisTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/miscellaneous/AnalysisTest.java index 6eda1dcb70..26a219ef5e 100644 --- a/dartagnan/src/test/java/com/dat3m/dartagnan/miscellaneous/AnalysisTest.java +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/miscellaneous/AnalysisTest.java @@ -17,6 +17,7 @@ import com.dat3m.dartagnan.program.event.EventFactory; import com.dat3m.dartagnan.program.event.RegReader; import com.dat3m.dartagnan.program.event.core.*; +import com.dat3m.dartagnan.program.event.functions.Return; import com.dat3m.dartagnan.program.event.metadata.OriginalId; import com.dat3m.dartagnan.program.memory.MemoryObject; import com.dat3m.dartagnan.program.processing.LoopUnrolling; @@ -47,7 +48,7 @@ private enum Result {NONE, MAY, MUST} private static final ExpressionFactory expressions = ExpressionFactory.getInstance(); @Test - public void dependencyMustOverride() throws InvalidConfigurationException { + public void reachingDefinitionMustOverride() throws InvalidConfigurationException { ProgramBuilder b = ProgramBuilder.forLanguage(SourceLanguage.LITMUS); b.newThread(0); Register r0 = b.getOrNewRegister(0, "r0"); @@ -59,7 +60,7 @@ public void dependencyMustOverride() throws InvalidConfigurationException { b.addChild(0, e0); Local e1 = newLocal(r1, r0); b.addChild(0, e1); - Label join = b.getOrCreateLabel(0,"join"); + Label join = b.getOrCreateLabel(0, "join"); b.addChild(0, newGoto(join)); b.addChild(0, alt); Local e2 = newLocal(r1, value(2)); @@ -100,6 +101,118 @@ public void dependencyMustOverride() throws InvalidConfigurationException { assertList(dep.getWriters(me5).ofRegister(r2).getMustWriters(), me4); } + + + @Test + public void reachingDefinitionSupportsLoops() { + ProgramBuilder b = ProgramBuilder.forLanguage(SourceLanguage.LITMUS); + b.newFunction("test", 0, types.getFunctionType(types.getArchType(), List.of()), List.of()); + Register r0 = b.getOrNewRegister(0, "r0"); + Register r1 = b.getOrNewRegister(0, "r1"); + Register r2 = b.getOrNewRegister(0, "r2"); + Register r3 = b.getOrNewRegister(0, "r3"); + // if * { + Label skip0 = b.getOrCreateLabel(0, "skip0"); + b.addChild(0, newJump(b.newConstant(types.getBooleanType()), skip0)); + // r0 = r0 + Local r00 = newLocal(r0, r0); + b.addChild(0, r00); + // } + b.addChild(0, skip0); + // r1 = r0 + Local r10 = newLocal(r1, r0); + b.addChild(0, r10); + // r2 = r0 + Local r20 = newLocal(r2, r0); + b.addChild(0, r20); + // r3 = 0 + Local r30 = newLocal(r3, expressions.makeZero(types.getArchType())); + b.addChild(0, r30); + // do { + Label begin = b.getOrCreateLabel(0, "begin"); + b.addChild(0, begin); + // if * { + Label skip1 = b.getOrCreateLabel(0, "skip1"); + b.addChild(0, newJump(b.newConstant(types.getBooleanType()), skip1)); + // r0 = r1 + Local r01 = newLocal(r0, r1); + b.addChild(0, r01); + // r1 = r1 + Local r11 = newLocal(r1, r1); + b.addChild(0, r11); + // r2 = r1 + Local r21 = newLocal(r2, r1); + b.addChild(0, r21); + // } + b.addChild(0, skip1); + // r3 = r1 + Local r31 = newLocal(r3, r1); + b.addChild(0, r31); + // } while * + b.addChild(0, newJump(b.newConstant(types.getBooleanType()), begin)); + // if * { + Label skip2 = b.getOrCreateLabel(0, "skip2"); + b.addChild(0, newJump(b.newConstant(types.getBooleanType()), skip2)); + // r0 = r2 + Local r02 = newLocal(r0, r2); + b.addChild(0, r02); + // r1 = r2 + Local r12 = newLocal(r1, r2); + b.addChild(0, r12); + // } + b.addChild(0, skip2); + // r2 = r2 + Local r22 = newLocal(r2, r2); + b.addChild(0, r22); + // if * { + Label skip3 = b.getOrCreateLabel(0, "skip3"); + b.addChild(0, newJump(b.newConstant(types.getBooleanType()), skip3)); + // r3 = r2 + Local r32 = newLocal(r3, r2); + b.addChild(0, r32); + // } + b.addChild(0, skip3); + // return (r0 + r1) ^ (r2 | r3) + Return ret = newFunctionReturn( + expressions.makeIntXor(expressions.makeAdd(r0, r1), expressions.makeIntOr(r2, r3))); + b.addChild(0, ret); + + Program program = b.build(); + final var dep = BackwardsReachingDefinitionsAnalysis.forFunction(program.getFunctions().get(0)); + assertFalse(dep.getWriters(r00).ofRegister(r0).mustBeInitialized()); + assertList(dep.getWriters(r00).ofRegister(r0).getMayWriters()); + assertFalse(dep.getWriters(r10).ofRegister(r0).mustBeInitialized()); + assertList(dep.getWriters(r10).ofRegister(r0).getMayWriters(), r00); + assertFalse(dep.getWriters(r20).ofRegister(r0).mustBeInitialized()); + assertList(dep.getWriters(r20).ofRegister(r0).getMayWriters(), r00); + assertTrue(dep.getWriters(r30).getUsedRegisters().isEmpty()); + assertList(dep.getWriters(r30).ofRegister(r0).getMayWriters()); + assertTrue(dep.getWriters(r01).ofRegister(r1).mustBeInitialized()); + assertList(dep.getWriters(r01).ofRegister(r1).getMayWriters(), r10, r11); + assertTrue(dep.getWriters(r11).ofRegister(r1).mustBeInitialized()); + assertList(dep.getWriters(r11).ofRegister(r1).getMayWriters(), r10, r11); + assertTrue(dep.getWriters(r21).ofRegister(r1).mustBeInitialized()); + assertList(dep.getWriters(r21).ofRegister(r1).getMayWriters(), r11); + assertTrue(dep.getWriters(r31).ofRegister(r1).mustBeInitialized()); + assertList(dep.getWriters(r31).ofRegister(r1).getMayWriters(), r10, r11); + assertTrue(dep.getWriters(r02).ofRegister(r2).mustBeInitialized()); + assertList(dep.getWriters(r02).ofRegister(r2).getMayWriters(), r20, r21); + assertTrue(dep.getWriters(r12).ofRegister(r2).mustBeInitialized()); + assertList(dep.getWriters(r12).ofRegister(r2).getMayWriters(), r20, r21); + assertTrue(dep.getWriters(r22).ofRegister(r2).mustBeInitialized()); + assertList(dep.getWriters(r22).ofRegister(r2).getMayWriters(), r20, r21); + assertTrue(dep.getWriters(r32).ofRegister(r2).mustBeInitialized()); + assertList(dep.getWriters(r32).ofRegister(r2).getMayWriters(), r22); + assertFalse(dep.getWriters(ret).ofRegister(r0).mustBeInitialized()); + assertList(dep.getWriters(ret).ofRegister(r0).getMayWriters(), r00, r01, r02); + assertTrue(dep.getWriters(ret).ofRegister(r1).mustBeInitialized()); + assertList(dep.getWriters(ret).ofRegister(r1).getMayWriters(), r10, r11, r12); + assertTrue(dep.getWriters(ret).ofRegister(r2).mustBeInitialized()); + assertList(dep.getWriters(ret).ofRegister(r2).getMayWriters(), r22); + assertTrue(dep.getWriters(ret).ofRegister(r3).mustBeInitialized()); + assertList(dep.getWriters(ret).ofRegister(r3).getMayWriters(), r31, r32); + } + @Test public void fieldsensitive0() throws InvalidConfigurationException { program0(FIELD_SENSITIVE, MAY, MAY, NONE, NONE, NONE, NONE); From 494ebb7806384cfd00118174bb16063ad1da2314 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ren=C3=A9=20Pascal=20Maseli?= Date: Wed, 4 Sep 2024 14:41:03 +0200 Subject: [PATCH 08/18] Suggested changes --- .../BackwardsReachingDefinitionsAnalysis.java | 22 +++++++++---------- .../dartagnan/miscellaneous/AnalysisTest.java | 1 + 2 files changed, 11 insertions(+), 12 deletions(-) diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/BackwardsReachingDefinitionsAnalysis.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/BackwardsReachingDefinitionsAnalysis.java index 5495a97005..b9a5f27e51 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/BackwardsReachingDefinitionsAnalysis.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/BackwardsReachingDefinitionsAnalysis.java @@ -97,9 +97,9 @@ public static BackwardsReachingDefinitionsAnalysis forFunction(Function function /** * Analyzes an entire set of threads. * @param program Contains a set of threads to be analyzed. Additionally-defined functions are ignored. - * @param branch Optional, queried for possibility of pairs of writers appearing together in an execution. + * @param exec Optional, queried for possibility of pairs of writers appearing together in an execution. */ - public static BackwardsReachingDefinitionsAnalysis forProgram(Program program, BranchEquivalence branch) { + public static BackwardsReachingDefinitionsAnalysis forProgram(Program program, ExecutionAnalysis exec) { final var analysis = new BackwardsReachingDefinitionsAnalysis(); final Set finalRegisters = finalRegisters(program); for (Function function : program.isUnrolled() ? program.getThreads() : @@ -108,16 +108,15 @@ public static BackwardsReachingDefinitionsAnalysis forProgram(Program program, B analysis.run(function, finalRegisters); } analysis.postProcess(); - if (branch != null && program.isUnrolled()) { - analysis.analyzeMust(branch); + if (exec != null && program.isUnrolled()) { + analysis.analyzeMust(exec); } return analysis; } public static BackwardsReachingDefinitionsAnalysis injectForProgram(Program program, Context analysisContext) { - final BranchEquivalence branch = analysisContext.get(BranchEquivalence.class); - final BackwardsReachingDefinitionsAnalysis analysis = forProgram(program, branch); - analysisContext.register(BackwardsReachingDefinitionsAnalysis.class, analysis); + final ExecutionAnalysis exec = analysisContext.get(ExecutionAnalysis.class); + final BackwardsReachingDefinitionsAnalysis analysis = forProgram(program, exec); analysisContext.register(ReachingDefinitionsAnalysis.class, analysis); return analysis; } @@ -362,24 +361,23 @@ private static boolean merge(StateInfo target, StateInfo source) { return true; } - private void analyzeMust(BranchEquivalence branch) { + private void analyzeMust(ExecutionAnalysis exec) { // Require that function is unrolled. for (ReaderInfo reader : readerMap.values()) { for (int i = 0; i < reader.mayWriters.size(); i++) { final RegWriter writer = reader.mayWriters.get(i); - if (!mayBeOverwritten(writer, reader.mayWriters.subList(i+1, reader.mayWriters.size()), branch)) { + if (!mayBeOverwritten(writer, reader.mayWriters.subList(i+1, reader.mayWriters.size()), exec)) { reader.mustWriters.add(writer); } } } } - private static boolean mayBeOverwritten(RegWriter earlyWriter, List lateWriters, BranchEquivalence branch) { + private static boolean mayBeOverwritten(RegWriter earlyWriter, List lateWriters, ExecutionAnalysis exec) { final Register resultRegister = earlyWriter.getResultRegister(); - final Set exclusiveClasses = branch.getEquivalenceClass(earlyWriter).getExclusiveClasses(); for (RegWriter lateWriter : lateWriters) { if (lateWriter.getResultRegister().equals(resultRegister) && - !exclusiveClasses.contains(branch.getEquivalenceClass(lateWriter))) { + !exec.areMutuallyExclusive(earlyWriter, lateWriter)) { return true; } } diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/miscellaneous/AnalysisTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/miscellaneous/AnalysisTest.java index 26a219ef5e..2d3dd80f7c 100644 --- a/dartagnan/src/test/java/com/dat3m/dartagnan/miscellaneous/AnalysisTest.java +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/miscellaneous/AnalysisTest.java @@ -80,6 +80,7 @@ public void reachingDefinitionMustOverride() throws InvalidConfigurationExceptio Configuration config = Configuration.defaultConfiguration(); Context context = Context.create(); context.register(BranchEquivalence.class, BranchEquivalence.fromConfig(program, config)); + context.register(ExecutionAnalysis.class, ExecutionAnalysis.fromConfig(program, context, config)); final var dep = BackwardsReachingDefinitionsAnalysis.injectForProgram(program, context); var me0 = (RegReader) findMatchingEventAfterProcessing(program, e0); var me1 = (RegReader) findMatchingEventAfterProcessing(program, e1); From 7887589f634344384acfa274a4f0d5ebc745d896 Mon Sep 17 00:00:00 2001 From: Thomas Haas Date: Thu, 5 Sep 2024 10:46:00 +0200 Subject: [PATCH 09/18] Add support to CAAT for SyncBar, SyncFence and Vloc relations (#724) --- .../verification/solving/RefinementSolver.java | 15 ++++++++++++--- .../spirv/basic/SpirvAssertionsTest.java | 4 ++-- .../spirv/benchmarks/SpirvAssertionsTest.java | 4 ++-- .../spirv/benchmarks/SpirvChecksTest.java | 4 ++-- .../spirv/benchmarks/SpirvRacesTest.java | 4 ++-- .../spirv/gpuverify/SpirvChecksTest.java | 4 ++-- .../dartagnan/spirv/gpuverify/SpirvRacesTest.java | 4 ++-- 7 files changed, 24 insertions(+), 15 deletions(-) diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/RefinementSolver.java b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/RefinementSolver.java index bebb12fd78..f432c68d0f 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/RefinementSolver.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/RefinementSolver.java @@ -469,6 +469,13 @@ private RefinementIteration doRefinementIteration(ProverEnvironment prover, WMMS // ================================================================================================================ // Special memory model processing + private static boolean isUnknownDefinitionForCAAT(Definition def) { + // TODO: We should probably automatically cut all "unknown relation", + // i.e., use a white-list of known relations instead of a blacklist of unknown one's. + return def instanceof LinuxCriticalSections // LKMM + || def instanceof SyncFence || def instanceof SyncBar || def instanceof SameVirtualLocation; // GPUs + } + private static RefinementModel generateRefinementModel(Wmm original) { // We cut (i) negated axioms, (ii) negated relations (if derived), // and (iii) some special relations because they are derived from internal relations (like data/addr/ctrl) @@ -492,7 +499,7 @@ private static RefinementModel generateRefinementModel(Wmm original) { } else if (c instanceof Definition def && def.getDefinedRelation().hasName()) { // (iii) Special relations final String name = def.getDefinedRelation().getName().get(); - if (name.equals(DATA) || name.equals(CTRL) || name.equals(ADDR) || name.equals(CRIT)) { + if (name.equals(DATA) || name.equals(CTRL) || name.equals(ADDR) || isUnknownDefinitionForCAAT(def)) { constraintsToCut.add(c); } } else if (c instanceof Definition def && def instanceof Fences) { @@ -516,7 +523,8 @@ private static void addBiases(Wmm memoryModel, EnumSet biases) { memoryModel.getOrCreatePredefinedRelation(POLOC), rf, memoryModel.getOrCreatePredefinedRelation(CO), - memoryModel.getOrCreatePredefinedRelation(FR))))); + memoryModel.getOrCreatePredefinedRelation(FR) + )))); } if (biases.contains(Baseline.NO_OOTA)) { // ---- acyclic (dep | rf) ---- @@ -524,7 +532,8 @@ private static void addBiases(Wmm memoryModel, EnumSet biases) { memoryModel.getOrCreatePredefinedRelation(CTRL), memoryModel.getOrCreatePredefinedRelation(DATA), memoryModel.getOrCreatePredefinedRelation(ADDR), - rf)))); + rf) + ))); } if (biases.contains(Baseline.ATOMIC_RMW)) { // ---- empty (rmw & fre;coe) ---- diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/basic/SpirvAssertionsTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/basic/SpirvAssertionsTest.java index 18878d7f92..9c2f3fa06c 100644 --- a/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/basic/SpirvAssertionsTest.java +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/basic/SpirvAssertionsTest.java @@ -7,6 +7,7 @@ import com.dat3m.dartagnan.utils.Result; import com.dat3m.dartagnan.verification.VerificationTask; import com.dat3m.dartagnan.verification.solving.AssumeSolver; +import com.dat3m.dartagnan.verification.solving.RefinementSolver; import com.dat3m.dartagnan.wmm.Wmm; import org.junit.Test; import org.junit.runner.RunWith; @@ -120,10 +121,9 @@ public static Iterable data() throws IOException { @Test public void testAllSolvers() throws Exception { - /* TODO: Implementation try (SolverContext ctx = mkCtx(); ProverEnvironment prover = mkProver(ctx)) { assertEquals(expected, RefinementSolver.run(ctx, prover, mkTask()).getResult()); - }*/ + } try (SolverContext ctx = mkCtx(); ProverEnvironment prover = mkProver(ctx)) { assertEquals(expected, AssumeSolver.run(ctx, prover, mkTask()).getResult()); } diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/benchmarks/SpirvAssertionsTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/benchmarks/SpirvAssertionsTest.java index 96acad8bbc..9006c1b99f 100644 --- a/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/benchmarks/SpirvAssertionsTest.java +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/benchmarks/SpirvAssertionsTest.java @@ -7,6 +7,7 @@ import com.dat3m.dartagnan.utils.Result; import com.dat3m.dartagnan.verification.VerificationTask; import com.dat3m.dartagnan.verification.solving.AssumeSolver; +import com.dat3m.dartagnan.verification.solving.RefinementSolver; import com.dat3m.dartagnan.wmm.Wmm; import org.junit.Test; import org.junit.runner.RunWith; @@ -113,10 +114,9 @@ public static Iterable data() throws IOException { @Test public void testAllSolvers() throws Exception { - /* TODO: Implementation try (SolverContext ctx = mkCtx(); ProverEnvironment prover = mkProver(ctx)) { assertEquals(expected, RefinementSolver.run(ctx, prover, mkTask()).getResult()); - }*/ + } try (SolverContext ctx = mkCtx(); ProverEnvironment prover = mkProver(ctx)) { assertEquals(expected, AssumeSolver.run(ctx, prover, mkTask()).getResult()); } diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/benchmarks/SpirvChecksTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/benchmarks/SpirvChecksTest.java index 6043e53303..c217abd6f7 100644 --- a/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/benchmarks/SpirvChecksTest.java +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/benchmarks/SpirvChecksTest.java @@ -7,6 +7,7 @@ import com.dat3m.dartagnan.utils.Result; import com.dat3m.dartagnan.verification.VerificationTask; import com.dat3m.dartagnan.verification.solving.AssumeSolver; +import com.dat3m.dartagnan.verification.solving.RefinementSolver; import com.dat3m.dartagnan.wmm.Wmm; import org.junit.Test; import org.junit.runner.RunWith; @@ -117,10 +118,9 @@ public static Iterable data() throws IOException { @Test public void testAllSolvers() throws Exception { - /* TODO: Implementation try (SolverContext ctx = mkCtx(); ProverEnvironment prover = mkProver(ctx)) { assertEquals(expected, RefinementSolver.run(ctx, prover, mkTask()).getResult()); - }*/ + } try (SolverContext ctx = mkCtx(); ProverEnvironment prover = mkProver(ctx)) { assertEquals(expected, AssumeSolver.run(ctx, prover, mkTask()).getResult()); } diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/benchmarks/SpirvRacesTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/benchmarks/SpirvRacesTest.java index 5f4ac94440..a5c88e5f77 100644 --- a/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/benchmarks/SpirvRacesTest.java +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/benchmarks/SpirvRacesTest.java @@ -7,6 +7,7 @@ import com.dat3m.dartagnan.utils.Result; import com.dat3m.dartagnan.verification.VerificationTask; import com.dat3m.dartagnan.verification.solving.AssumeSolver; +import com.dat3m.dartagnan.verification.solving.RefinementSolver; import com.dat3m.dartagnan.wmm.Wmm; import org.junit.Test; import org.junit.runner.RunWith; @@ -118,10 +119,9 @@ public static Iterable data() throws IOException { @Test public void testAllSolvers() throws Exception { - /* TODO: Implementation try (SolverContext ctx = mkCtx(); ProverEnvironment prover = mkProver(ctx)) { assertEquals(expected, RefinementSolver.run(ctx, prover, mkTask()).getResult()); - }*/ + } try (SolverContext ctx = mkCtx(); ProverEnvironment prover = mkProver(ctx)) { assertEquals(expected, AssumeSolver.run(ctx, prover, mkTask()).getResult()); } diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/gpuverify/SpirvChecksTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/gpuverify/SpirvChecksTest.java index 6124efb5b0..b682b3505e 100644 --- a/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/gpuverify/SpirvChecksTest.java +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/gpuverify/SpirvChecksTest.java @@ -7,6 +7,7 @@ import com.dat3m.dartagnan.utils.Result; import com.dat3m.dartagnan.verification.VerificationTask; import com.dat3m.dartagnan.verification.solving.AssumeSolver; +import com.dat3m.dartagnan.verification.solving.RefinementSolver; import com.dat3m.dartagnan.wmm.Wmm; import org.junit.Test; import org.junit.runner.RunWith; @@ -345,10 +346,9 @@ public static Iterable data() throws IOException { @Test public void testAllSolvers() throws Exception { - /* TODO: Implementation try (SolverContext ctx = mkCtx(); ProverEnvironment prover = mkProver(ctx)) { assertEquals(expected, RefinementSolver.run(ctx, prover, mkTask()).getResult()); - }*/ + } try (SolverContext ctx = mkCtx(); ProverEnvironment prover = mkProver(ctx)) { assertEquals(expected, AssumeSolver.run(ctx, prover, mkTask()).getResult()); } diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/gpuverify/SpirvRacesTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/gpuverify/SpirvRacesTest.java index 29b7ad7990..da21d9fb30 100644 --- a/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/gpuverify/SpirvRacesTest.java +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/gpuverify/SpirvRacesTest.java @@ -7,6 +7,7 @@ import com.dat3m.dartagnan.utils.Result; import com.dat3m.dartagnan.verification.VerificationTask; import com.dat3m.dartagnan.verification.solving.AssumeSolver; +import com.dat3m.dartagnan.verification.solving.RefinementSolver; import com.dat3m.dartagnan.wmm.Wmm; import org.junit.Test; import org.junit.runner.RunWith; @@ -345,10 +346,9 @@ public static Iterable data() throws IOException { @Test public void testAllSolvers() throws Exception { - /* TODO: Implementation try (SolverContext ctx = mkCtx(); ProverEnvironment prover = mkProver(ctx)) { assertEquals(expected, RefinementSolver.run(ctx, prover, mkTask()).getResult()); - }*/ + } try (SolverContext ctx = mkCtx(); ProverEnvironment prover = mkProver(ctx)) { assertEquals(expected, AssumeSolver.run(ctx, prover, mkTask()).getResult()); } From 1bd4bd02171badff84a45d9789afe058e9621266 Mon Sep 17 00:00:00 2001 From: natgavrilenko Date: Thu, 5 Sep 2024 16:17:29 +0200 Subject: [PATCH 10/18] Add unrolling bound to program spec encoding (#727) --- .../dartagnan/encoding/PropertyEncoder.java | 6 +++-- .../spirv/basic/SpirvAssertionsTest.java | 24 +++++++------------ 2 files changed, 12 insertions(+), 18 deletions(-) diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/PropertyEncoder.java b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/PropertyEncoder.java index 36427a5adf..994f9da6bd 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/PropertyEncoder.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/PropertyEncoder.java @@ -36,6 +36,7 @@ import static com.dat3m.dartagnan.configuration.Property.*; import static com.dat3m.dartagnan.program.Program.SourceLanguage.LLVM; +import static com.dat3m.dartagnan.program.Program.SpecificationType.ASSERT; import static com.dat3m.dartagnan.wmm.RelationNameRepository.CO; public class PropertyEncoder implements Encoder { @@ -275,7 +276,7 @@ private TrackableFormula encodeProgramSpecification() { case FORALL, NOT_EXISTS, ASSERT -> bmgr.not(PROGRAM_SPEC.getSMTVariable(context)); case EXISTS -> PROGRAM_SPEC.getSMTVariable(context); }; - if (!program.getFormat().equals(LLVM)) { + if (!ASSERT.equals(program.getSpecificationType())) { encoding = bmgr.and(encoding, encodeProgramTermination()); } return new TrackableFormula(trackingLiteral, encoding); @@ -283,9 +284,10 @@ private TrackableFormula encodeProgramSpecification() { private BooleanFormula encodeProgramTermination() { final BooleanFormulaManager bmgr = context.getBooleanFormulaManager(); - return bmgr.and(program.getThreads().stream() + BooleanFormula exitReached = bmgr.and(program.getThreads().stream() .map(t -> bmgr.equivalence(context.execution(t.getEntry()), context.execution(t.getExit()))) .toList()); + return bmgr.and(exitReached, bmgr.not(encodeBoundEventExec())); } // ====================================================================== diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/basic/SpirvAssertionsTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/basic/SpirvAssertionsTest.java index 9c2f3fa06c..e86077b009 100644 --- a/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/basic/SpirvAssertionsTest.java +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/basic/SpirvAssertionsTest.java @@ -28,8 +28,7 @@ import static com.dat3m.dartagnan.configuration.Property.PROGRAM_SPEC; import static com.dat3m.dartagnan.utils.ResourceHelper.getRootPath; import static com.dat3m.dartagnan.utils.ResourceHelper.getTestResourcePath; -import static com.dat3m.dartagnan.utils.Result.FAIL; -import static com.dat3m.dartagnan.utils.Result.PASS; +import static com.dat3m.dartagnan.utils.Result.*; import static org.junit.Assert.assertEquals; @RunWith(Parameterized.class) @@ -79,30 +78,23 @@ public static Iterable data() throws IOException { {"builtin-all-321.spv.dis", 1, PASS}, {"branch-cond-ff.spv.dis", 1, PASS}, {"branch-cond-ff-inverted.spv.dis", 1, PASS}, - {"branch-cond-bf.spv.dis", 1, FAIL}, + {"branch-cond-bf.spv.dis", 1, UNKNOWN}, {"branch-cond-bf.spv.dis", 2, PASS}, - {"branch-cond-bf.spv.dis", 3, PASS}, - {"branch-cond-fb.spv.dis", 1, FAIL}, + {"branch-cond-fb.spv.dis", 1, UNKNOWN}, {"branch-cond-fb.spv.dis", 2, PASS}, - {"branch-cond-fb.spv.dis", 3, PASS}, {"branch-cond-struct.spv.dis", 1, PASS}, {"branch-cond-struct-read-write.spv.dis", 1, PASS}, {"branch-race.spv.dis", 1, PASS}, - {"branch-loop.spv.dis", 2, FAIL}, + {"branch-loop.spv.dis", 2, UNKNOWN}, {"branch-loop.spv.dis", 3, PASS}, - {"branch-loop.spv.dis", 4, PASS}, - {"loop-struct-cond.spv.dis", 1, FAIL}, + {"loop-struct-cond.spv.dis", 1, UNKNOWN}, {"loop-struct-cond.spv.dis", 2, PASS}, - {"loop-struct-cond.spv.dis", 3, PASS}, - {"loop-struct-cond-suffix.spv.dis", 1, FAIL}, + {"loop-struct-cond-suffix.spv.dis", 1, UNKNOWN}, {"loop-struct-cond-suffix.spv.dis", 2, PASS}, - {"loop-struct-cond-suffix.spv.dis", 3, PASS}, - {"loop-struct-cond-sequence.spv.dis", 2, FAIL}, + {"loop-struct-cond-sequence.spv.dis", 2, UNKNOWN}, {"loop-struct-cond-sequence.spv.dis", 3, PASS}, - {"loop-struct-cond-sequence.spv.dis", 4, PASS}, - {"loop-struct-cond-nested.spv.dis", 2, FAIL}, + {"loop-struct-cond-nested.spv.dis", 2, UNKNOWN}, {"loop-struct-cond-nested.spv.dis", 3, PASS}, - {"loop-struct-cond-nested.spv.dis", 4, PASS}, {"phi.spv.dis", 1, PASS}, {"phi-unstruct-true.spv.dis", 1, PASS}, {"phi-unstruct-false.spv.dis", 1, PASS}, From 3e6f2474f6ea975ba9a528e11f8bf0c37a4708ca Mon Sep 17 00:00:00 2001 From: Hernan Ponce de Leon Date: Fri, 6 Sep 2024 07:43:58 +0200 Subject: [PATCH 11/18] Add option to dump encoding to smtlib2 file (#721) --- .../java/com/dat3m/dartagnan/Dartagnan.java | 6 +- .../dartagnan/configuration/OptionNames.java | 1 + .../dartagnan/encoding/ProverWithTracker.java | 200 ++++++++++++++++++ .../processing/compilation/VisitorLKMM.java | 2 - .../dartagnan/utils/options/BaseOptions.java | 7 + .../verification/solving/AssumeSolver.java | 12 +- .../verification/solving/DataRaceSolver.java | 98 +++++---- .../solving/RefinementSolver.java | 15 +- .../com/dat3m/dartagnan/wmm/Assumption.java | 6 - .../com/dat3m/dartagnan/wmm/Constraint.java | 1 - .../com/dat3m/dartagnan/c/AbstractCTest.java | 4 +- .../compilation/AbstractCompilationTest.java | 6 +- .../dartagnan/litmus/AbstractLitmusTest.java | 6 +- .../miscellaneous/ArrayValidTest.java | 4 +- .../dartagnan/miscellaneous/BranchTest.java | 4 +- .../spirv/basic/SpirvAssertionsTest.java | 12 +- .../spirv/benchmarks/SpirvAssertionsTest.java | 10 +- .../spirv/benchmarks/SpirvChecksTest.java | 12 +- .../spirv/benchmarks/SpirvRacesTest.java | 12 +- .../spirv/gpuverify/SpirvChecksTest.java | 12 +- .../spirv/gpuverify/SpirvRacesTest.java | 12 +- .../dartagnan/utils/rules/Providers.java | 8 +- .../dartagnan/witness/BuildWitnessTest.java | 4 +- .../dat3m/ui/result/ReachabilityResult.java | 4 +- 24 files changed, 339 insertions(+), 119 deletions(-) create mode 100644 dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProverWithTracker.java diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java b/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java index 3ccab85b38..161486f7cd 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java @@ -3,6 +3,7 @@ import com.dat3m.dartagnan.configuration.OptionNames; import com.dat3m.dartagnan.configuration.Property; import com.dat3m.dartagnan.encoding.EncodingContext; +import com.dat3m.dartagnan.encoding.ProverWithTracker; import com.dat3m.dartagnan.expression.ExpressionPrinter; import com.dat3m.dartagnan.parsers.cat.ParserCat; import com.dat3m.dartagnan.parsers.program.ProgramParser; @@ -163,7 +164,10 @@ public static void main(String[] args) throws Exception { BasicLogManager.create(solverConfig), sdm.getNotifier(), o.getSolver()); - ProverEnvironment prover = ctx.newProverEnvironment(ProverOptions.GENERATE_MODELS)) { + ProverWithTracker prover = new ProverWithTracker(ctx, + o.getDumpSmtLib() ? + System.getenv("DAT3M_OUTPUT") + String.format("/%s.smt2", p.getName()) : "", + ProverOptions.GENERATE_MODELS)) { ModelChecker modelChecker; if (properties.contains(DATARACEFREEDOM)) { if (properties.size() > 1) { diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/configuration/OptionNames.java b/dartagnan/src/main/java/com/dat3m/dartagnan/configuration/OptionNames.java index 3cec00bf75..18a0ca89fc 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/configuration/OptionNames.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/configuration/OptionNames.java @@ -12,6 +12,7 @@ public class OptionNames { public static final String VALIDATE = "validate"; public static final String COVERAGE = "coverage"; public static final String WITNESS = "witness"; + public static final String SMTLIB2 = "smtlib2"; // Modeling Options public static final String THREAD_CREATE_ALWAYS_SUCCEEDS = "modeling.threadCreateAlwaysSucceeds"; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProverWithTracker.java b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProverWithTracker.java new file mode 100644 index 0000000000..24d6ad8be4 --- /dev/null +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProverWithTracker.java @@ -0,0 +1,200 @@ +package com.dat3m.dartagnan.encoding; + +import java.io.File; +import java.io.FileWriter; +import java.io.IOException; +import java.io.PrintWriter; +import java.nio.file.Files; +import java.nio.file.Paths; +import java.time.LocalDate; +import java.time.format.DateTimeFormatter; +import java.util.Collection; +import java.util.HashSet; +import java.util.List; +import java.util.Optional; +import java.util.Set; + +import org.sosy_lab.java_smt.api.*; +import org.sosy_lab.java_smt.api.SolverContext.ProverOptions; + +import com.google.common.collect.ImmutableMap; + +public class ProverWithTracker implements ProverEnvironment { + + private final FormulaManager fmgr; + private final ProverEnvironment prover; + private final String fileName; + private final Set declarations; + + public ProverWithTracker(SolverContext ctx, String fileName, ProverOptions... options) { + this.fmgr = ctx.getFormulaManager(); + this.prover = ctx.newProverEnvironment(options); + this.fileName = fileName; + this.declarations = new HashSet<>(); + init(); + } + + // An empty filename means there is no need to dump the encoding + private boolean dump() { + return !fileName.isEmpty(); + } + + private void init() { + if(dump()) { + try { + Files.deleteIfExists(Paths.get(fileName)); + } catch (IOException e) { + e.printStackTrace(); + } + StringBuilder description = new StringBuilder(); + LocalDate currentDate = LocalDate.now(); + DateTimeFormatter formatter = DateTimeFormatter.ofPattern("YYYY-MM-DD"); + description.append("Generated on: " + currentDate.format(formatter) + "\n"); + description.append("Generator: Dartagnan\n"); + description.append("Application: Bounded model checking for weak memory models\n"); + description.append("Publications: \n" + + "- Hernán Ponce de León, Florian Furbach, Keijo Heljanko, " + + "Roland Meyer: Dartagnan: Bounded Model Checking for Weak Memory Models " + + "(Competition Contribution). TACAS (2) 2020: 378-382\n" + + "- Thomas Haas, Roland Meyer, Hernán Ponce de León: " + + "CAAT: consistency as a theory. Proc. ACM Program. Lang. 6(OOPSLA2): 114-144 (2022)" + ); + write("(set-info :smt-lib-version 2.6)\n"); + write("(set-logic ALL)\n"); + write("(set-info :category \"industrial\")\n"); + write("(set-info :source |\n" + description + "\n|)\n"); + write("(set-info :license \"https://creativecommons.org/licenses/by/4.0/\")\n"); + } + } + + @Override + public void close() { + if(dump()) { + removeDuplicatedDeclarations(fileName); + write("(exit)\n"); + } + prover.close(); + } + + @Override + public Void addConstraint(BooleanFormula f) throws InterruptedException { + if(dump()) { + write(fmgr.dumpFormula(f).toString()); + } + return prover.addConstraint(f); + } + + @Override + public boolean isUnsatWithAssumptions(Collection fs) throws SolverException, InterruptedException { + + if(dump()) { + write("(push)\n"); + for(BooleanFormula f : fs) { + write(fmgr.dumpFormula(f).toString()); + } + } + + long start = System.currentTimeMillis(); + boolean result = prover.isUnsatWithAssumptions(fs); + long end = System.currentTimeMillis(); + + if(dump()) { + write("(set-info :status " + (result ? "unsat" : "sat") + ")\n"); + write("(check-sat)\n"); + writeComment("Original solving time: " + (end - start) + " ms"); + write("(pop)\n"); + } + + return result; + } + + @Override + public boolean isUnsat() throws SolverException, InterruptedException { + long start = System.currentTimeMillis(); + boolean result = prover.isUnsat(); + long end = System.currentTimeMillis(); + if(dump()) { + write("(set-info :status " + (result ? "unsat" : "sat") + ")\n"); + write("(check-sat)\n"); + writeComment("Original solving time: " + (end - start) + " ms"); + } + return result; + } + + @Override + public ImmutableMap getStatistics() { + return prover.getStatistics(); + } + + @Override + public Model getModel() throws SolverException { + return prover.getModel(); + } + + @Override + public void push() throws InterruptedException { + if(dump()) { + write("(push)\n"); + } + prover.push(); + } + + @Override + public void pop() { + if(dump()) { + write("(pop)\n"); + } + prover.pop(); + } + + @Override + public R allSat(AllSatCallback arg0, List arg1) throws InterruptedException, SolverException { + return prover.allSat(arg0, arg1); + } + + @Override + public List getUnsatCore() { + return prover.getUnsatCore(); + } + + @Override + public int size() { + return prover.size(); + } + + @Override + public Optional> unsatCoreOverAssumptions(Collection arg0) + throws SolverException, InterruptedException { + return prover.unsatCoreOverAssumptions(arg0); + } + + private void write(String content) { + if (dump()) { + File file = new File(fileName); + try (FileWriter writer = new FileWriter(file, true); + PrintWriter printer = new PrintWriter(writer)) { + printer.append(removeDuplicatedDeclarations(content)); + printer.close(); + } catch (IOException e) { + e.printStackTrace(); + } + } + } + + public void writeComment(String content) { + write("; " + content); + } + + // FIXME: This is only correct as long as no declarations are popped and then + // later redeclared (which is currently guarenteed by the way we use the solver) + private StringBuilder removeDuplicatedDeclarations(String content) { + StringBuilder builder = new StringBuilder(); + for(String line : content.split("\n")) { + if(line.contains("declare-fun") && !declarations.add(line)) { + continue; + } + builder.append(line + "\n"); + } + return builder; + } +} diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorLKMM.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorLKMM.java index b448471580..d858308a5f 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorLKMM.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorLKMM.java @@ -2,10 +2,8 @@ import com.dat3m.dartagnan.expression.Expression; import com.dat3m.dartagnan.expression.ExpressionFactory; -import com.dat3m.dartagnan.expression.Type; import com.dat3m.dartagnan.expression.type.IntegerType; import com.dat3m.dartagnan.program.Register; -import com.dat3m.dartagnan.program.Program.SourceLanguage; import com.dat3m.dartagnan.program.event.Event; import com.dat3m.dartagnan.program.event.EventFactory; import com.dat3m.dartagnan.program.event.Tag; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/utils/options/BaseOptions.java b/dartagnan/src/main/java/com/dat3m/dartagnan/utils/options/BaseOptions.java index 32cfec175a..fd166a38e0 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/utils/options/BaseOptions.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/utils/options/BaseOptions.java @@ -68,4 +68,11 @@ public abstract class BaseOptions { private WitnessType witnessType=WitnessType.getDefault(); public WitnessType getWitnessType() { return witnessType; } + + @Option( + name=SMTLIB2, + description="Dump encoding to an SMTLIB2 file.") + private boolean smtlib=false; + + public boolean getDumpSmtLib() { return smtlib; } } \ No newline at end of file diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/AssumeSolver.java b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/AssumeSolver.java index cc0200630b..a8108aa9f1 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/AssumeSolver.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/AssumeSolver.java @@ -21,16 +21,16 @@ public class AssumeSolver extends ModelChecker { private static final Logger logger = LogManager.getLogger(AssumeSolver.class); private final SolverContext ctx; - private final ProverEnvironment prover; + private final ProverWithTracker prover; private final VerificationTask task; - private AssumeSolver(SolverContext c, ProverEnvironment p, VerificationTask t) { + private AssumeSolver(SolverContext c, ProverWithTracker p, VerificationTask t) { ctx = c; prover = p; task = t; } - public static AssumeSolver run(SolverContext ctx, ProverEnvironment prover, VerificationTask task) + public static AssumeSolver run(SolverContext ctx, ProverWithTracker prover, VerificationTask task) throws InterruptedException, SolverException, InvalidConfigurationException { AssumeSolver s = new AssumeSolver(ctx, prover, task); s.run(); @@ -55,21 +55,27 @@ private void run() throws InterruptedException, SolverException, InvalidConfigur SymmetryEncoder symmetryEncoder = SymmetryEncoder.withContext(context); logger.info("Starting encoding using " + ctx.getVersion()); + prover.writeComment("Program encoding"); prover.addConstraint(programEncoder.encodeFullProgram()); + prover.writeComment("Memory model encoding"); prover.addConstraint(wmmEncoder.encodeFullMemoryModel()); // For validation this contains information. // For verification graph.encode() just returns ctx.mkTrue() + prover.writeComment("Witness encoding"); prover.addConstraint(task.getWitness().encode(context)); + prover.writeComment("Symmetry breaking encoding"); prover.addConstraint(symmetryEncoder.encodeFullSymmetryBreaking()); BooleanFormulaManager bmgr = ctx.getFormulaManager().getBooleanFormulaManager(); BooleanFormula assumptionLiteral = bmgr.makeVariable("DAT3M_spec_assumption"); BooleanFormula propertyEncoding = propertyEncoder.encodeProperties(task.getProperty()); BooleanFormula assumedSpec = bmgr.implication(assumptionLiteral, propertyEncoding); + prover.writeComment("Property encoding"); prover.addConstraint(assumedSpec); logger.info("Starting first solver.check()"); if(prover.isUnsatWithAssumptions(singletonList(assumptionLiteral))) { + prover.writeComment("Bound encoding"); prover.addConstraint(propertyEncoder.encodeBoundEventExec()); logger.info("Starting second solver.check()"); res = prover.isUnsat()? PASS : Result.UNKNOWN; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/DataRaceSolver.java b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/DataRaceSolver.java index 5190ef5d4c..0941215cc3 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/DataRaceSolver.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/DataRaceSolver.java @@ -9,7 +9,7 @@ import org.apache.logging.log4j.Logger; import org.sosy_lab.common.configuration.Configuration; import org.sosy_lab.common.configuration.InvalidConfigurationException; -import org.sosy_lab.java_smt.api.ProverEnvironment; +import com.dat3m.dartagnan.encoding.ProverWithTracker; import org.sosy_lab.java_smt.api.SolverContext; import org.sosy_lab.java_smt.api.SolverException; @@ -18,63 +18,67 @@ import static com.dat3m.dartagnan.utils.Result.*; public class DataRaceSolver extends ModelChecker { - - // This analysis assumes that CAT file defining the memory model has a happens-before - // relation named hb: it should contain the following axiom "acyclic hb" + + // This analysis assumes that CAT file defining the memory model has a happens-before + // relation named hb: it should contain the following axiom "acyclic hb" private static final Logger logger = LogManager.getLogger(DataRaceSolver.class); - private final SolverContext ctx; - private final ProverEnvironment prover; - private final VerificationTask task; + private final SolverContext ctx; + private final ProverWithTracker prover; + private final VerificationTask task; - private DataRaceSolver(SolverContext c, ProverEnvironment p, VerificationTask t) { - ctx = c; - prover = p; - task = t; - } + private DataRaceSolver(SolverContext c, ProverWithTracker p, VerificationTask t) { + ctx = c; + prover = p; + task = t; + } - public static DataRaceSolver run(SolverContext ctx, ProverEnvironment prover, VerificationTask task) - throws InterruptedException, SolverException, InvalidConfigurationException { - DataRaceSolver s = new DataRaceSolver(ctx, prover, task); - s.run(); - return s; - } + public static DataRaceSolver run(SolverContext ctx, ProverWithTracker prover, VerificationTask task) + throws InterruptedException, SolverException, InvalidConfigurationException { + DataRaceSolver s = new DataRaceSolver(ctx, prover, task); + s.run(); + return s; + } - private void run() throws InterruptedException, SolverException, InvalidConfigurationException { - Wmm memoryModel = task.getMemoryModel(); - Context analysisContext = Context.create(); - Configuration config = task.getConfig(); + private void run() throws InterruptedException, SolverException, InvalidConfigurationException { + Wmm memoryModel = task.getMemoryModel(); + Context analysisContext = Context.create(); + Configuration config = task.getConfig(); - memoryModel.configureAll(config); - preprocessProgram(task, config); - preprocessMemoryModel(task, config); - performStaticProgramAnalyses(task, analysisContext, config); - performStaticWmmAnalyses(task, analysisContext, config); + memoryModel.configureAll(config); + preprocessProgram(task, config); + preprocessMemoryModel(task, config); + performStaticProgramAnalyses(task, analysisContext, config); + performStaticWmmAnalyses(task, analysisContext, config); - context = EncodingContext.of(task, analysisContext, ctx.getFormulaManager()); - ProgramEncoder programEncoder = ProgramEncoder.withContext(context); - PropertyEncoder propertyEncoder = PropertyEncoder.withContext(context); - WmmEncoder wmmEncoder = WmmEncoder.withContext(context); - SymmetryEncoder symmetryEncoder = SymmetryEncoder.withContext(context); + context = EncodingContext.of(task, analysisContext, ctx.getFormulaManager()); + ProgramEncoder programEncoder = ProgramEncoder.withContext(context); + PropertyEncoder propertyEncoder = PropertyEncoder.withContext(context); + WmmEncoder wmmEncoder = WmmEncoder.withContext(context); + SymmetryEncoder symmetryEncoder = SymmetryEncoder.withContext(context); logger.info("Starting encoding using " + ctx.getVersion()); - prover.addConstraint(programEncoder.encodeFullProgram()); - prover.addConstraint(wmmEncoder.encodeFullMemoryModel()); - prover.addConstraint(symmetryEncoder.encodeFullSymmetryBreaking()); - prover.push(); - - prover.addConstraint(propertyEncoder.encodeProperties(EnumSet.of(Property.DATARACEFREEDOM))); + prover.writeComment("Program encoding"); + prover.addConstraint(programEncoder.encodeFullProgram()); + prover.writeComment("Memory model encoding"); + prover.addConstraint(wmmEncoder.encodeFullMemoryModel()); + prover.writeComment("Symmetry breaking encoding"); + prover.addConstraint(symmetryEncoder.encodeFullSymmetryBreaking()); + prover.push(); + prover.writeComment("Property encoding"); + prover.addConstraint(propertyEncoder.encodeProperties(EnumSet.of(Property.DATARACEFREEDOM))); - logger.info("Starting first solver.check()"); - if(prover.isUnsat()) { - prover.pop(); - prover.addConstraint(propertyEncoder.encodeBoundEventExec()); - logger.info("Starting second solver.check()"); - res = prover.isUnsat() ? PASS : UNKNOWN; - } else { - res = FAIL; - } + logger.info("Starting first solver.check()"); + if (prover.isUnsat()) { + prover.pop(); + prover.writeComment("Bound encoding"); + prover.addConstraint(propertyEncoder.encodeBoundEventExec()); + logger.info("Starting second solver.check()"); + res = prover.isUnsat() ? PASS : UNKNOWN; + } else { + res = FAIL; + } logger.info("Verification finished with result " + res); } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/RefinementSolver.java b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/RefinementSolver.java index f432c68d0f..bce614c3ba 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/RefinementSolver.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/RefinementSolver.java @@ -162,7 +162,7 @@ private RefinementSolver() { //TODO: We do not yet use Witness information. The problem is that WitnessGraph.encode() generates // constraints on hb, which is not encoded in Refinement. //TODO (2): Add possibility for Refinement to handle CAT-properties (it ignores them for now). - public static RefinementSolver run(SolverContext ctx, ProverEnvironment prover, VerificationTask task) + public static RefinementSolver run(SolverContext ctx, ProverWithTracker prover, VerificationTask task) throws InterruptedException, SolverException, InvalidConfigurationException { RefinementSolver solver = new RefinementSolver(); task.getConfig().inject(solver); @@ -171,7 +171,7 @@ public static RefinementSolver run(SolverContext ctx, ProverEnvironment prover, return solver; } - private void runInternal(SolverContext ctx, ProverEnvironment prover, VerificationTask task) + private void runInternal(SolverContext ctx, ProverWithTracker prover, VerificationTask task) throws InterruptedException, SolverException, InvalidConfigurationException { final Program program = task.getProgram(); final Wmm memoryModel = task.getMemoryModel(); @@ -224,8 +224,11 @@ private void runInternal(SolverContext ctx, ProverEnvironment prover, Verificati final Property.Type propertyType = Property.getCombinedType(task.getProperty(), task); logger.info("Starting encoding using " + ctx.getVersion()); + prover.writeComment("Program encoding"); prover.addConstraint(programEncoder.encodeFullProgram()); + prover.writeComment("Memory model (baseline) encoding"); prover.addConstraint(baselineEncoder.encodeFullMemoryModel()); + prover.writeComment("Symmetry breaking encoding"); prover.addConstraint(symmetryEncoder.encodeFullSymmetryBreaking()); // ------------------------ Solving ------------------------ @@ -233,6 +236,7 @@ private void runInternal(SolverContext ctx, ProverEnvironment prover, Verificati logger.info("Checking target property."); prover.push(); + prover.writeComment("Property encoding"); prover.addConstraint(propertyEncoder.encodeProperties(task.getProperty())); final RefinementTrace propertyTrace = runRefinement(task, prover, solver, refiner); @@ -265,8 +269,10 @@ private void runInternal(SolverContext ctx, ProverEnvironment prover, Verificati logger.info("Checking unrolling bounds."); final long lastTime = System.currentTimeMillis(); prover.pop(); + prover.writeComment("Bound encoding"); prover.addConstraint(propertyEncoder.encodeBoundEventExec()); // Add back the refinement clauses we already found, hoping that this improves the performance. + prover.writeComment("Refinement encoding"); prover.addConstraint(bmgr.and(propertyTrace.getRefinementFormulas())); final RefinementTrace boundTrace = runRefinement(task, prover, solver, refiner); boundCheckTime = System.currentTimeMillis() - lastTime; @@ -358,7 +364,7 @@ private void analyzeInconclusiveness(VerificationTask task, Context analysisCont // Refinement core algorithm // TODO: We could expose the following method(s) to allow for more general application of refinement. - private RefinementTrace runRefinement(VerificationTask task, ProverEnvironment prover, WMMSolver solver, Refiner refiner) + private RefinementTrace runRefinement(VerificationTask task, ProverWithTracker prover, WMMSolver solver, Refiner refiner) throws SolverException, InterruptedException { final List trace = new ArrayList<>(); @@ -418,7 +424,7 @@ private boolean checkProgress(List trace) { return !last.inconsistencyReasons.equals(prev.inconsistencyReasons); } - private RefinementIteration doRefinementIteration(ProverEnvironment prover, WMMSolver solver, Refiner refiner) + private RefinementIteration doRefinementIteration(ProverWithTracker prover, WMMSolver solver, Refiner refiner) throws SolverException, InterruptedException { long nativeTime = 0; @@ -455,6 +461,7 @@ private RefinementIteration doRefinementIteration(ProverEnvironment prover, WMMS inconsistencyReasons = solverResult.getCoreReasons(); lastTime = System.currentTimeMillis(); refinementFormula = refiner.refine(inconsistencyReasons, context); + prover.writeComment("Refinement encoding"); prover.addConstraint(refinementFormula); refineTime = (System.currentTimeMillis() - lastTime); } 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 2da9f984e9..788a3b8f09 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/Assumption.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/Assumption.java @@ -1,21 +1,15 @@ package com.dat3m.dartagnan.wmm; -import com.dat3m.dartagnan.verification.Context; -import com.dat3m.dartagnan.wmm.analysis.RelationAnalysis; import com.dat3m.dartagnan.wmm.utils.EventGraph; import org.apache.logging.log4j.LogManager; import org.apache.logging.log4j.Logger; -import java.util.Map; import java.util.Set; -import static com.dat3m.dartagnan.wmm.utils.EventGraph.difference; import static com.google.common.base.Preconditions.checkNotNull; public final class Assumption implements Constraint { - private static final Logger logger = LogManager.getLogger(Assumption.class); - private final Relation rel; private final EventGraph may; private final EventGraph must; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/Constraint.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/Constraint.java index 1a674d9626..4c5ef52794 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/Constraint.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/Constraint.java @@ -3,7 +3,6 @@ import com.dat3m.dartagnan.encoding.EncodingContext; import com.dat3m.dartagnan.verification.Context; import com.dat3m.dartagnan.verification.VerificationTask; -import com.dat3m.dartagnan.wmm.analysis.RelationAnalysis; import com.dat3m.dartagnan.wmm.axiom.*; import com.dat3m.dartagnan.wmm.definition.*; import com.dat3m.dartagnan.wmm.utils.EventGraph; diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/c/AbstractCTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/c/AbstractCTest.java index 8593902783..39d4ef879d 100644 --- a/dartagnan/src/test/java/com/dat3m/dartagnan/c/AbstractCTest.java +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/c/AbstractCTest.java @@ -3,6 +3,7 @@ import com.dat3m.dartagnan.configuration.Arch; import com.dat3m.dartagnan.configuration.OptionNames; import com.dat3m.dartagnan.configuration.Property; +import com.dat3m.dartagnan.encoding.ProverWithTracker; import com.dat3m.dartagnan.program.Program; import com.dat3m.dartagnan.utils.Result; import com.dat3m.dartagnan.utils.rules.Provider; @@ -17,7 +18,6 @@ import org.sosy_lab.common.configuration.Configuration; import org.sosy_lab.common.configuration.InvalidConfigurationException; import org.sosy_lab.java_smt.SolverContextFactory.Solvers; -import org.sosy_lab.java_smt.api.ProverEnvironment; import org.sosy_lab.java_smt.api.SolverContext; import java.util.EnumSet; @@ -84,7 +84,7 @@ protected Provider getConfigurationProvider() { protected final Provider configurationProvider = getConfigurationProvider(); protected final Provider taskProvider = Providers.createTask(programProvider, wmmProvider, propertyProvider, targetProvider, boundProvider, configurationProvider); protected final Provider contextProvider = Providers.createSolverContextFromManager(shutdownManagerProvider, solverProvider); - protected final Provider proverProvider = Providers.createProverWithFixedOptions(contextProvider, SolverContext.ProverOptions.GENERATE_MODELS); + protected final Provider proverProvider = Providers.createProverWithFixedOptions(contextProvider, SolverContext.ProverOptions.GENERATE_MODELS); // Special rules protected final Timeout timeout = Timeout.millis(getTimeout()); diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/compilation/AbstractCompilationTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/compilation/AbstractCompilationTest.java index b92e1209f5..f0d6f31d2a 100644 --- a/dartagnan/src/test/java/com/dat3m/dartagnan/compilation/AbstractCompilationTest.java +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/compilation/AbstractCompilationTest.java @@ -2,6 +2,7 @@ import com.dat3m.dartagnan.configuration.Arch; import com.dat3m.dartagnan.configuration.Property; +import com.dat3m.dartagnan.encoding.ProverWithTracker; import com.dat3m.dartagnan.program.Program; import com.dat3m.dartagnan.program.event.Event; import com.dat3m.dartagnan.program.event.Tag; @@ -19,7 +20,6 @@ import org.sosy_lab.common.ShutdownManager; import org.sosy_lab.common.configuration.Configuration; import org.sosy_lab.java_smt.SolverContextFactory.Solvers; -import org.sosy_lab.java_smt.api.ProverEnvironment; import org.sosy_lab.java_smt.api.SolverContext; import org.sosy_lab.java_smt.api.SolverContext.ProverOptions; @@ -99,8 +99,8 @@ protected Provider getConfigurationProvider() { protected final Provider task2Provider = Providers.createTask(program2Provider, wmm2Provider, propertyProvider, targetProvider, () -> 1, configProvider); protected final Provider context1Provider = Providers.createSolverContextFromManager(shutdownManagerProvider, () -> Solvers.Z3); protected final Provider context2Provider = Providers.createSolverContextFromManager(shutdownManagerProvider, () -> Solvers.Z3); - protected final Provider prover1Provider = Providers.createProverWithFixedOptions(context1Provider, ProverOptions.GENERATE_MODELS); - protected final Provider prover2Provider = Providers.createProverWithFixedOptions(context2Provider, ProverOptions.GENERATE_MODELS); + protected final Provider prover1Provider = Providers.createProverWithFixedOptions(context1Provider, ProverOptions.GENERATE_MODELS); + protected final Provider prover2Provider = Providers.createProverWithFixedOptions(context2Provider, ProverOptions.GENERATE_MODELS); private final Timeout timeout = Timeout.millis(getTimeout()); private final RequestShutdownOnError shutdownOnError = RequestShutdownOnError.create(shutdownManagerProvider); diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/litmus/AbstractLitmusTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/litmus/AbstractLitmusTest.java index 1e86058312..3316d114eb 100644 --- a/dartagnan/src/test/java/com/dat3m/dartagnan/litmus/AbstractLitmusTest.java +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/litmus/AbstractLitmusTest.java @@ -2,6 +2,7 @@ import com.dat3m.dartagnan.configuration.Arch; import com.dat3m.dartagnan.configuration.Property; +import com.dat3m.dartagnan.encoding.ProverWithTracker; import com.dat3m.dartagnan.program.Program; import com.dat3m.dartagnan.utils.ResourceHelper; import com.dat3m.dartagnan.utils.Result; @@ -19,7 +20,6 @@ import org.sosy_lab.common.ShutdownManager; import org.sosy_lab.common.configuration.Configuration; import org.sosy_lab.java_smt.SolverContextFactory.Solvers; -import org.sosy_lab.java_smt.api.ProverEnvironment; import org.sosy_lab.java_smt.api.SolverContext; import org.sosy_lab.java_smt.api.SolverContext.ProverOptions; @@ -110,8 +110,8 @@ protected long getTimeout() { protected final Provider configProvider = getConfigurationProvider(); protected final Provider taskProvider = Providers.createTask(programProvider, wmmProvider, propertyProvider, targetProvider, boundProvider, configProvider); protected final Provider contextProvider = Providers.createSolverContextFromManager(shutdownManagerProvider, () -> Solvers.Z3); - protected final Provider proverProvider = Providers.createProverWithFixedOptions(contextProvider, ProverOptions.GENERATE_MODELS); - protected final Provider prover2Provider = Providers.createProverWithFixedOptions(contextProvider, ProverOptions.GENERATE_MODELS); + protected final Provider proverProvider = Providers.createProverWithFixedOptions(contextProvider, ProverOptions.GENERATE_MODELS); + protected final Provider prover2Provider = Providers.createProverWithFixedOptions(contextProvider, ProverOptions.GENERATE_MODELS); private final Timeout timeout = Timeout.millis(getTimeout()); private final RequestShutdownOnError shutdownOnError = RequestShutdownOnError.create(shutdownManagerProvider); diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/miscellaneous/ArrayValidTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/miscellaneous/ArrayValidTest.java index fa2d573259..e8ba520d5c 100644 --- a/dartagnan/src/test/java/com/dat3m/dartagnan/miscellaneous/ArrayValidTest.java +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/miscellaneous/ArrayValidTest.java @@ -2,6 +2,7 @@ import com.dat3m.dartagnan.configuration.Arch; import com.dat3m.dartagnan.configuration.Property; +import com.dat3m.dartagnan.encoding.ProverWithTracker; import com.dat3m.dartagnan.parsers.cat.ParserCat; import com.dat3m.dartagnan.parsers.program.ProgramParser; import com.dat3m.dartagnan.program.Program; @@ -12,7 +13,6 @@ import org.junit.Test; import org.junit.runner.RunWith; import org.junit.runners.Parameterized; -import org.sosy_lab.java_smt.api.ProverEnvironment; import org.sosy_lab.java_smt.api.SolverContext; import org.sosy_lab.java_smt.api.SolverContext.ProverOptions; @@ -56,7 +56,7 @@ public ArrayValidTest(String path, Wmm wmm) { @Test public void test() { try (SolverContext ctx = TestHelper.createContext(); - ProverEnvironment prover = ctx.newProverEnvironment(ProverOptions.GENERATE_MODELS)) { + ProverWithTracker prover = new ProverWithTracker(ctx, "", ProverOptions.GENERATE_MODELS)) { Program program = new ProgramParser().parse(new File(path)); VerificationTask task = VerificationTask.builder() .withSolverTimeout(60) diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/miscellaneous/BranchTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/miscellaneous/BranchTest.java index 05d84eb465..588dc3cdb0 100644 --- a/dartagnan/src/test/java/com/dat3m/dartagnan/miscellaneous/BranchTest.java +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/miscellaneous/BranchTest.java @@ -2,6 +2,7 @@ import com.dat3m.dartagnan.configuration.Arch; import com.dat3m.dartagnan.configuration.Property; +import com.dat3m.dartagnan.encoding.ProverWithTracker; import com.dat3m.dartagnan.parsers.cat.ParserCat; import com.dat3m.dartagnan.parsers.program.ProgramParser; import com.dat3m.dartagnan.program.Program; @@ -14,7 +15,6 @@ import org.junit.Test; import org.junit.runner.RunWith; import org.junit.runners.Parameterized; -import org.sosy_lab.java_smt.api.ProverEnvironment; import org.sosy_lab.java_smt.api.SolverContext; import org.sosy_lab.java_smt.api.SolverContext.ProverOptions; @@ -95,7 +95,7 @@ public BranchTest(String path, Result expected, Wmm wmm) { @Test public void test() { try (SolverContext ctx = TestHelper.createContext(); - ProverEnvironment prover = ctx.newProverEnvironment(ProverOptions.GENERATE_MODELS)) { + ProverWithTracker prover = new ProverWithTracker(ctx, "", ProverOptions.GENERATE_MODELS)) { Program program = new ProgramParser().parse(new File(path)); VerificationTask task = VerificationTask.builder() .withSolverTimeout(60) diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/basic/SpirvAssertionsTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/basic/SpirvAssertionsTest.java index e86077b009..24fa6af270 100644 --- a/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/basic/SpirvAssertionsTest.java +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/basic/SpirvAssertionsTest.java @@ -1,6 +1,7 @@ package com.dat3m.dartagnan.spirv.basic; import com.dat3m.dartagnan.configuration.Arch; +import com.dat3m.dartagnan.encoding.ProverWithTracker; import com.dat3m.dartagnan.parsers.cat.ParserCat; import com.dat3m.dartagnan.parsers.program.ProgramParser; import com.dat3m.dartagnan.program.Program; @@ -17,7 +18,6 @@ import org.sosy_lab.common.configuration.InvalidConfigurationException; import org.sosy_lab.common.log.BasicLogManager; import org.sosy_lab.java_smt.SolverContextFactory; -import org.sosy_lab.java_smt.api.ProverEnvironment; import org.sosy_lab.java_smt.api.SolverContext; import java.io.File; @@ -113,10 +113,10 @@ public static Iterable data() throws IOException { @Test public void testAllSolvers() throws Exception { - try (SolverContext ctx = mkCtx(); ProverEnvironment prover = mkProver(ctx)) { - assertEquals(expected, RefinementSolver.run(ctx, prover, mkTask()).getResult()); + try (SolverContext ctx = mkCtx(); ProverWithTracker prover = mkProver(ctx)) { + assertEquals(expected, RefinementSolver.run(ctx, prover, mkTask()).getResult()); } - try (SolverContext ctx = mkCtx(); ProverEnvironment prover = mkProver(ctx)) { + try (SolverContext ctx = mkCtx(); ProverWithTracker prover = mkProver(ctx)) { assertEquals(expected, AssumeSolver.run(ctx, prover, mkTask()).getResult()); } } @@ -130,8 +130,8 @@ private SolverContext mkCtx() throws InvalidConfigurationException { SolverContextFactory.Solvers.Z3); } - private ProverEnvironment mkProver(SolverContext ctx) { - return ctx.newProverEnvironment(SolverContext.ProverOptions.GENERATE_MODELS); + private ProverWithTracker mkProver(SolverContext ctx) { + return new ProverWithTracker(ctx, "", SolverContext.ProverOptions.GENERATE_MODELS); } private VerificationTask mkTask() throws Exception { diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/benchmarks/SpirvAssertionsTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/benchmarks/SpirvAssertionsTest.java index 9006c1b99f..6625246101 100644 --- a/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/benchmarks/SpirvAssertionsTest.java +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/benchmarks/SpirvAssertionsTest.java @@ -1,6 +1,7 @@ package com.dat3m.dartagnan.spirv.benchmarks; import com.dat3m.dartagnan.configuration.Arch; +import com.dat3m.dartagnan.encoding.ProverWithTracker; import com.dat3m.dartagnan.parsers.cat.ParserCat; import com.dat3m.dartagnan.parsers.program.ProgramParser; import com.dat3m.dartagnan.program.Program; @@ -17,7 +18,6 @@ import org.sosy_lab.common.configuration.InvalidConfigurationException; import org.sosy_lab.common.log.BasicLogManager; import org.sosy_lab.java_smt.SolverContextFactory; -import org.sosy_lab.java_smt.api.ProverEnvironment; import org.sosy_lab.java_smt.api.SolverContext; import java.io.File; @@ -114,10 +114,10 @@ public static Iterable data() throws IOException { @Test public void testAllSolvers() throws Exception { - try (SolverContext ctx = mkCtx(); ProverEnvironment prover = mkProver(ctx)) { + try (SolverContext ctx = mkCtx(); ProverWithTracker prover = mkProver(ctx)) { assertEquals(expected, RefinementSolver.run(ctx, prover, mkTask()).getResult()); } - try (SolverContext ctx = mkCtx(); ProverEnvironment prover = mkProver(ctx)) { + try (SolverContext ctx = mkCtx(); ProverWithTracker prover = mkProver(ctx)) { assertEquals(expected, AssumeSolver.run(ctx, prover, mkTask()).getResult()); } } @@ -131,8 +131,8 @@ private SolverContext mkCtx() throws InvalidConfigurationException { SolverContextFactory.Solvers.Z3); } - private ProverEnvironment mkProver(SolverContext ctx) { - return ctx.newProverEnvironment(SolverContext.ProverOptions.GENERATE_MODELS); + private ProverWithTracker mkProver(SolverContext ctx) { + return new ProverWithTracker(ctx, "", SolverContext.ProverOptions.GENERATE_MODELS); } private VerificationTask mkTask() throws Exception { diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/benchmarks/SpirvChecksTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/benchmarks/SpirvChecksTest.java index c217abd6f7..0efe8060ed 100644 --- a/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/benchmarks/SpirvChecksTest.java +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/benchmarks/SpirvChecksTest.java @@ -1,6 +1,7 @@ package com.dat3m.dartagnan.spirv.benchmarks; import com.dat3m.dartagnan.configuration.Arch; +import com.dat3m.dartagnan.encoding.ProverWithTracker; import com.dat3m.dartagnan.parsers.cat.ParserCat; import com.dat3m.dartagnan.parsers.program.ProgramParser; import com.dat3m.dartagnan.program.Program; @@ -17,7 +18,6 @@ import org.sosy_lab.common.configuration.InvalidConfigurationException; import org.sosy_lab.common.log.BasicLogManager; import org.sosy_lab.java_smt.SolverContextFactory; -import org.sosy_lab.java_smt.api.ProverEnvironment; import org.sosy_lab.java_smt.api.SolverContext; import java.io.File; @@ -118,10 +118,10 @@ public static Iterable data() throws IOException { @Test public void testAllSolvers() throws Exception { - try (SolverContext ctx = mkCtx(); ProverEnvironment prover = mkProver(ctx)) { - assertEquals(expected, RefinementSolver.run(ctx, prover, mkTask()).getResult()); + try (SolverContext ctx = mkCtx(); ProverWithTracker prover = mkProver(ctx)) { + assertEquals(expected, RefinementSolver.run(ctx, prover, mkTask()).getResult()); } - try (SolverContext ctx = mkCtx(); ProverEnvironment prover = mkProver(ctx)) { + try (SolverContext ctx = mkCtx(); ProverWithTracker prover = mkProver(ctx)) { assertEquals(expected, AssumeSolver.run(ctx, prover, mkTask()).getResult()); } } @@ -135,8 +135,8 @@ private SolverContext mkCtx() throws InvalidConfigurationException { SolverContextFactory.Solvers.Z3); } - private ProverEnvironment mkProver(SolverContext ctx) { - return ctx.newProverEnvironment(SolverContext.ProverOptions.GENERATE_MODELS); + private ProverWithTracker mkProver(SolverContext ctx) { + return new ProverWithTracker(ctx, "", SolverContext.ProverOptions.GENERATE_MODELS); } private VerificationTask mkTask() throws Exception { diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/benchmarks/SpirvRacesTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/benchmarks/SpirvRacesTest.java index a5c88e5f77..b6ee1d618c 100644 --- a/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/benchmarks/SpirvRacesTest.java +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/benchmarks/SpirvRacesTest.java @@ -1,6 +1,7 @@ package com.dat3m.dartagnan.spirv.benchmarks; import com.dat3m.dartagnan.configuration.Arch; +import com.dat3m.dartagnan.encoding.ProverWithTracker; import com.dat3m.dartagnan.parsers.cat.ParserCat; import com.dat3m.dartagnan.parsers.program.ProgramParser; import com.dat3m.dartagnan.program.Program; @@ -17,7 +18,6 @@ import org.sosy_lab.common.configuration.InvalidConfigurationException; import org.sosy_lab.common.log.BasicLogManager; import org.sosy_lab.java_smt.SolverContextFactory; -import org.sosy_lab.java_smt.api.ProverEnvironment; import org.sosy_lab.java_smt.api.SolverContext; import java.io.File; @@ -119,10 +119,10 @@ public static Iterable data() throws IOException { @Test public void testAllSolvers() throws Exception { - try (SolverContext ctx = mkCtx(); ProverEnvironment prover = mkProver(ctx)) { - assertEquals(expected, RefinementSolver.run(ctx, prover, mkTask()).getResult()); + try (SolverContext ctx = mkCtx(); ProverWithTracker prover = mkProver(ctx)) { + assertEquals(expected, RefinementSolver.run(ctx, prover, mkTask()).getResult()); } - try (SolverContext ctx = mkCtx(); ProverEnvironment prover = mkProver(ctx)) { + try (SolverContext ctx = mkCtx(); ProverWithTracker prover = mkProver(ctx)) { assertEquals(expected, AssumeSolver.run(ctx, prover, mkTask()).getResult()); } } @@ -136,8 +136,8 @@ private SolverContext mkCtx() throws InvalidConfigurationException { SolverContextFactory.Solvers.Z3); } - private ProverEnvironment mkProver(SolverContext ctx) { - return ctx.newProverEnvironment(SolverContext.ProverOptions.GENERATE_MODELS); + private ProverWithTracker mkProver(SolverContext ctx) { + return new ProverWithTracker(ctx, "", SolverContext.ProverOptions.GENERATE_MODELS); } private VerificationTask mkTask() throws Exception { diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/gpuverify/SpirvChecksTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/gpuverify/SpirvChecksTest.java index b682b3505e..0cbb610e7d 100644 --- a/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/gpuverify/SpirvChecksTest.java +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/gpuverify/SpirvChecksTest.java @@ -1,6 +1,7 @@ package com.dat3m.dartagnan.spirv.gpuverify; import com.dat3m.dartagnan.configuration.Arch; +import com.dat3m.dartagnan.encoding.ProverWithTracker; import com.dat3m.dartagnan.parsers.cat.ParserCat; import com.dat3m.dartagnan.parsers.program.ProgramParser; import com.dat3m.dartagnan.program.Program; @@ -17,7 +18,6 @@ import org.sosy_lab.common.configuration.InvalidConfigurationException; import org.sosy_lab.common.log.BasicLogManager; import org.sosy_lab.java_smt.SolverContextFactory; -import org.sosy_lab.java_smt.api.ProverEnvironment; import org.sosy_lab.java_smt.api.SolverContext; import java.io.File; @@ -346,10 +346,10 @@ public static Iterable data() throws IOException { @Test public void testAllSolvers() throws Exception { - try (SolverContext ctx = mkCtx(); ProverEnvironment prover = mkProver(ctx)) { - assertEquals(expected, RefinementSolver.run(ctx, prover, mkTask()).getResult()); + try (SolverContext ctx = mkCtx(); ProverWithTracker prover = mkProver(ctx)) { + assertEquals(expected, RefinementSolver.run(ctx, prover, mkTask()).getResult()); } - try (SolverContext ctx = mkCtx(); ProverEnvironment prover = mkProver(ctx)) { + try (SolverContext ctx = mkCtx(); ProverWithTracker prover = mkProver(ctx)) { assertEquals(expected, AssumeSolver.run(ctx, prover, mkTask()).getResult()); } } @@ -363,8 +363,8 @@ private SolverContext mkCtx() throws InvalidConfigurationException { SolverContextFactory.Solvers.Z3); } - private ProverEnvironment mkProver(SolverContext ctx) { - return ctx.newProverEnvironment(SolverContext.ProverOptions.GENERATE_MODELS); + private ProverWithTracker mkProver(SolverContext ctx) { + return new ProverWithTracker(ctx, "", SolverContext.ProverOptions.GENERATE_MODELS); } private VerificationTask mkTask() throws Exception { diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/gpuverify/SpirvRacesTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/gpuverify/SpirvRacesTest.java index da21d9fb30..2493d31e92 100644 --- a/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/gpuverify/SpirvRacesTest.java +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/gpuverify/SpirvRacesTest.java @@ -1,6 +1,7 @@ package com.dat3m.dartagnan.spirv.gpuverify; import com.dat3m.dartagnan.configuration.Arch; +import com.dat3m.dartagnan.encoding.ProverWithTracker; import com.dat3m.dartagnan.parsers.cat.ParserCat; import com.dat3m.dartagnan.parsers.program.ProgramParser; import com.dat3m.dartagnan.program.Program; @@ -17,7 +18,6 @@ import org.sosy_lab.common.configuration.InvalidConfigurationException; import org.sosy_lab.common.log.BasicLogManager; import org.sosy_lab.java_smt.SolverContextFactory; -import org.sosy_lab.java_smt.api.ProverEnvironment; import org.sosy_lab.java_smt.api.SolverContext; import java.io.File; @@ -346,10 +346,10 @@ public static Iterable data() throws IOException { @Test public void testAllSolvers() throws Exception { - try (SolverContext ctx = mkCtx(); ProverEnvironment prover = mkProver(ctx)) { - assertEquals(expected, RefinementSolver.run(ctx, prover, mkTask()).getResult()); + try (SolverContext ctx = mkCtx(); ProverWithTracker prover = mkProver(ctx)) { + assertEquals(expected, RefinementSolver.run(ctx, prover, mkTask()).getResult()); } - try (SolverContext ctx = mkCtx(); ProverEnvironment prover = mkProver(ctx)) { + try (SolverContext ctx = mkCtx(); ProverWithTracker prover = mkProver(ctx)) { assertEquals(expected, AssumeSolver.run(ctx, prover, mkTask()).getResult()); } } @@ -363,8 +363,8 @@ private SolverContext mkCtx() throws InvalidConfigurationException { SolverContextFactory.Solvers.Z3); } - private ProverEnvironment mkProver(SolverContext ctx) { - return ctx.newProverEnvironment(SolverContext.ProverOptions.GENERATE_MODELS); + private ProverWithTracker mkProver(SolverContext ctx) { + return new ProverWithTracker(ctx, "", SolverContext.ProverOptions.GENERATE_MODELS); } private VerificationTask mkTask() throws Exception { diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/utils/rules/Providers.java b/dartagnan/src/test/java/com/dat3m/dartagnan/utils/rules/Providers.java index 0b8c06b449..f31db39a13 100644 --- a/dartagnan/src/test/java/com/dat3m/dartagnan/utils/rules/Providers.java +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/utils/rules/Providers.java @@ -8,12 +8,12 @@ import com.dat3m.dartagnan.wmm.Wmm; import com.dat3m.dartagnan.configuration.Arch; import com.dat3m.dartagnan.configuration.Property; +import com.dat3m.dartagnan.encoding.ProverWithTracker; import org.sosy_lab.common.ShutdownManager; import org.sosy_lab.common.ShutdownNotifier; import org.sosy_lab.common.configuration.Configuration; import org.sosy_lab.java_smt.SolverContextFactory.Solvers; -import org.sosy_lab.java_smt.api.ProverEnvironment; import org.sosy_lab.java_smt.api.SolverContext; import java.io.File; @@ -81,11 +81,11 @@ public static Provider createSolverContextFromManager(Supplier TestHelper.createContextWithShutdownNotifier(shutdownManagerSupplier.get().getNotifier(), solverSupplier.get())); } - public static Provider createProver(Supplier contextSupplier, Supplier optionsSupplier) { - return Provider.fromSupplier(() -> contextSupplier.get().newProverEnvironment(optionsSupplier.get())); + public static Provider createProver(Supplier contextSupplier, Supplier optionsSupplier) { + return Provider.fromSupplier(() -> new ProverWithTracker(contextSupplier.get(), "", optionsSupplier.get())); } - public static Provider createProverWithFixedOptions(Supplier contextSupplier, SolverContext.ProverOptions... options) { + public static Provider createProverWithFixedOptions(Supplier contextSupplier, SolverContext.ProverOptions... options) { return createProver(contextSupplier, () -> options); } } diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/witness/BuildWitnessTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/witness/BuildWitnessTest.java index 98b1d7d9ee..7b4d135cb4 100644 --- a/dartagnan/src/test/java/com/dat3m/dartagnan/witness/BuildWitnessTest.java +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/witness/BuildWitnessTest.java @@ -1,6 +1,7 @@ package com.dat3m.dartagnan.witness; import com.dat3m.dartagnan.configuration.Property; +import com.dat3m.dartagnan.encoding.ProverWithTracker; import com.dat3m.dartagnan.parsers.cat.ParserCat; import com.dat3m.dartagnan.parsers.program.ProgramParser; import com.dat3m.dartagnan.program.Program; @@ -15,7 +16,6 @@ import org.sosy_lab.common.configuration.Configuration; import org.sosy_lab.java_smt.api.BooleanFormula; import org.sosy_lab.java_smt.api.BooleanFormulaManager; -import org.sosy_lab.java_smt.api.ProverEnvironment; import org.sosy_lab.java_smt.api.SolverContext; import org.sosy_lab.java_smt.api.SolverContext.ProverOptions; @@ -43,7 +43,7 @@ public void BuildWriteEncode() throws Exception { Wmm wmm = new ParserCat().parse(new File(getRootPath("cat/svcomp.cat"))); VerificationTask task = VerificationTask.builder().withConfig(config).build(p, wmm, Property.getDefault()); try (SolverContext ctx = TestHelper.createContext(); - ProverEnvironment prover = ctx.newProverEnvironment(ProverOptions.GENERATE_MODELS)) { + ProverWithTracker prover = new ProverWithTracker(ctx, "", ProverOptions.GENERATE_MODELS)) { AssumeSolver modelChecker = AssumeSolver.run(ctx, prover, task); Result res = modelChecker.getResult(); WitnessBuilder witnessBuilder = WitnessBuilder.of(modelChecker.getEncodingContext(), prover, res, "user assertion"); diff --git a/ui/src/main/java/com/dat3m/ui/result/ReachabilityResult.java b/ui/src/main/java/com/dat3m/ui/result/ReachabilityResult.java index 6f2f6e622b..890aa30d4b 100644 --- a/ui/src/main/java/com/dat3m/ui/result/ReachabilityResult.java +++ b/ui/src/main/java/com/dat3m/ui/result/ReachabilityResult.java @@ -10,13 +10,13 @@ import com.dat3m.dartagnan.verification.solving.RefinementSolver; import com.dat3m.dartagnan.witness.WitnessType; import com.dat3m.dartagnan.wmm.Wmm; +import com.dat3m.dartagnan.encoding.ProverWithTracker; import com.dat3m.ui.utils.UiOptions; import com.dat3m.ui.utils.Utils; import org.sosy_lab.common.ShutdownManager; import org.sosy_lab.common.configuration.Configuration; import org.sosy_lab.common.log.BasicLogManager; import org.sosy_lab.java_smt.SolverContextFactory; -import org.sosy_lab.java_smt.api.ProverEnvironment; import org.sosy_lab.java_smt.api.SolverContext; import org.sosy_lab.java_smt.api.SolverContext.ProverOptions; @@ -92,7 +92,7 @@ private void run() { BasicLogManager.create(solverConfig), sdm.getNotifier(), options.solver()); - ProverEnvironment prover = ctx.newProverEnvironment(ProverOptions.GENERATE_MODELS)) { + ProverWithTracker prover = new ProverWithTracker(ctx, "", ProverOptions.GENERATE_MODELS)) { final ModelChecker modelChecker; modelChecker = switch (options.method()) { case EAGER -> AssumeSolver.run(ctx, prover, task); From 669e83a73a14a61ce27da9c4335129af497272c6 Mon Sep 17 00:00:00 2001 From: Hernan Ponce de Leon Date: Fri, 6 Sep 2024 17:55:11 +0200 Subject: [PATCH 12/18] Use correct smtlib2 syntax for push/pop (#728) Co-authored-by: Hernan Ponce de Leon --- .../com/dat3m/dartagnan/encoding/ProverWithTracker.java | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProverWithTracker.java b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProverWithTracker.java index 24d6ad8be4..38e11fb04c 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProverWithTracker.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProverWithTracker.java @@ -88,7 +88,7 @@ public Void addConstraint(BooleanFormula f) throws InterruptedException { public boolean isUnsatWithAssumptions(Collection fs) throws SolverException, InterruptedException { if(dump()) { - write("(push)\n"); + write("(push 1)\n"); for(BooleanFormula f : fs) { write(fmgr.dumpFormula(f).toString()); } @@ -102,7 +102,7 @@ public boolean isUnsatWithAssumptions(Collection fs) throws Solv write("(set-info :status " + (result ? "unsat" : "sat") + ")\n"); write("(check-sat)\n"); writeComment("Original solving time: " + (end - start) + " ms"); - write("(pop)\n"); + write("(pop 1)\n"); } return result; @@ -134,7 +134,7 @@ public Model getModel() throws SolverException { @Override public void push() throws InterruptedException { if(dump()) { - write("(push)\n"); + write("(push 1)\n"); } prover.push(); } @@ -142,7 +142,7 @@ public void push() throws InterruptedException { @Override public void pop() { if(dump()) { - write("(pop)\n"); + write("(pop 1)\n"); } prover.pop(); } From 28bbd11cad8e3ae90dc47b501bee4f574de451dc Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ren=C3=A9=20Pascal=20Maseli?= Date: Mon, 9 Sep 2024 18:14:54 +0200 Subject: [PATCH 13/18] Add options to access previous implementations. --- .../dartagnan/configuration/OptionNames.java | 2 + .../BackwardsReachingDefinitionsAnalysis.java | 18 ++++----- .../analysis/ReachingDefinitionsAnalysis.java | 28 ++++++++++++++ .../processing/NaiveLoopBoundAnnotation.java | 18 ++++++++- .../verification/solving/ModelChecker.java | 2 +- .../dartagnan/miscellaneous/AnalysisTest.java | 37 +++++++++++-------- 6 files changed, 78 insertions(+), 27 deletions(-) diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/configuration/OptionNames.java b/dartagnan/src/main/java/com/dat3m/dartagnan/configuration/OptionNames.java index 3cec00bf75..6832187bf8 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/configuration/OptionNames.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/configuration/OptionNames.java @@ -43,8 +43,10 @@ public class OptionNames { public static final String DYNAMIC_SPINLOOP_DETECTION = "program.processing.spinloops"; public static final String PROPAGATE_COPY_ASSIGNMENTS = "program.processing.propagateCopyAssignments"; public static final String REMOVE_ASSERTION_OF_TYPE = "program.processing.skipAssertionsOfType"; + public static final String LOOP_BOUNDS_USE_DEF_METHOD = "program.processing.loopBounds.useDefAnalysis"; // Program Property Options + public static final String REACHING_DEFINITIONS_METHOD = "program.analysis.reachingDefinitions"; public static final String ALIAS_METHOD = "program.analysis.alias"; public static final String ALIAS_GRAPHVIZ = "program.analysis.generateAliasGraph"; public static final String ALIAS_GRAPHVIZ_SPLIT_BY_THREAD = "program.analysis.generateAliasGraph.splitByThread"; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/BackwardsReachingDefinitionsAnalysis.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/BackwardsReachingDefinitionsAnalysis.java index b9a5f27e51..f651b9fd58 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/BackwardsReachingDefinitionsAnalysis.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/BackwardsReachingDefinitionsAnalysis.java @@ -11,6 +11,7 @@ import com.dat3m.dartagnan.verification.Context; import com.google.common.base.Preconditions; import com.google.common.collect.Iterables; +import org.sosy_lab.common.configuration.Configuration; import java.util.ArrayList; import java.util.Collection; @@ -38,7 +39,7 @@ *

* This analysis supports loops; * that is, backward jumps cause re-evaluation of the loop body until convergence. - * This results in a squared worst-case time complexity. + * This results in a squared worst-case time complexity in terms of events being processed. */ public class BackwardsReachingDefinitionsAnalysis implements ReachingDefinitionsAnalysis { @@ -96,10 +97,14 @@ public static BackwardsReachingDefinitionsAnalysis forFunction(Function function /** * Analyzes an entire set of threads. + *

+ * Optionally queries {@link ExecutionAnalysis} for pairs of writers appearing together in an execution. * @param program Contains a set of threads to be analyzed. Additionally-defined functions are ignored. - * @param exec Optional, queried for possibility of pairs of writers appearing together in an execution. + * @param analysisContext Collection of previous analyses to be used as dependencies. + * @param config User-defined settings for this analysis. */ - public static BackwardsReachingDefinitionsAnalysis forProgram(Program program, ExecutionAnalysis exec) { + public static BackwardsReachingDefinitionsAnalysis fromConfig(Program program, Context analysisContext, Configuration config) { + final ExecutionAnalysis exec = analysisContext.get(ExecutionAnalysis.class); final var analysis = new BackwardsReachingDefinitionsAnalysis(); final Set finalRegisters = finalRegisters(program); for (Function function : program.isUnrolled() ? program.getThreads() : @@ -114,13 +119,6 @@ public static BackwardsReachingDefinitionsAnalysis forProgram(Program program, E return analysis; } - public static BackwardsReachingDefinitionsAnalysis injectForProgram(Program program, Context analysisContext) { - final ExecutionAnalysis exec = analysisContext.get(ExecutionAnalysis.class); - final BackwardsReachingDefinitionsAnalysis analysis = forProgram(program, exec); - analysisContext.register(ReachingDefinitionsAnalysis.class, analysis); - return analysis; - } - private static Set finalRegisters(Program program) { final Set finalRegisters = new HashSet<>(); if (program.getSpecification() != null) { diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/ReachingDefinitionsAnalysis.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/ReachingDefinitionsAnalysis.java index 576f59ea84..c97dfa2bdd 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/ReachingDefinitionsAnalysis.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/ReachingDefinitionsAnalysis.java @@ -1,11 +1,19 @@ package com.dat3m.dartagnan.program.analysis; +import com.dat3m.dartagnan.program.Program; import com.dat3m.dartagnan.program.Register; import com.dat3m.dartagnan.program.event.RegReader; import com.dat3m.dartagnan.program.event.RegWriter; +import com.dat3m.dartagnan.verification.Context; +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 static com.dat3m.dartagnan.configuration.OptionNames.REACHING_DEFINITIONS_METHOD; + /** * Instances of this analysis shall over-approximate the relationship between {@link RegWriter} and {@link RegReader}, * where the writer performs the latest reassignment on the register being used by the reader. @@ -66,4 +74,24 @@ interface RegisterWriters { */ List getMustWriters(); } + + static ReachingDefinitionsAnalysis fromConfig(Program program, Context analysisContext, Configuration config) throws InvalidConfigurationException { + var c = new Config(); + config.inject(c); + ReachingDefinitionsAnalysis analysis = switch (c.method) { + case BACKWARD -> BackwardsReachingDefinitionsAnalysis.fromConfig(program, analysisContext, config); + case FORWARD -> Dependency.fromConfig(program, analysisContext, config); + }; + analysisContext.register(ReachingDefinitionsAnalysis.class, analysis); + return analysis; + } + + @Options + final class Config { + + @Option(name = REACHING_DEFINITIONS_METHOD, description = "", secure = true) + private Method method = Method.BACKWARD; + } + + enum Method { BACKWARD, FORWARD} } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/NaiveLoopBoundAnnotation.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/NaiveLoopBoundAnnotation.java index f40fe4c62f..55c3083c87 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/NaiveLoopBoundAnnotation.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/NaiveLoopBoundAnnotation.java @@ -11,6 +11,7 @@ import com.dat3m.dartagnan.program.analysis.LiveRegistersAnalysis; import com.dat3m.dartagnan.program.analysis.LoopAnalysis; import com.dat3m.dartagnan.program.analysis.ReachingDefinitionsAnalysis; +import com.dat3m.dartagnan.program.analysis.UseDefAnalysis; import com.dat3m.dartagnan.program.event.Event; import com.dat3m.dartagnan.program.event.EventFactory; import com.dat3m.dartagnan.program.event.RegWriter; @@ -18,9 +19,13 @@ import com.dat3m.dartagnan.program.event.core.Label; import com.dat3m.dartagnan.program.event.core.Local; import com.dat3m.dartagnan.utils.DominatorTree; +import org.sosy_lab.common.configuration.Option; +import org.sosy_lab.common.configuration.Options; import java.util.List; +import static com.dat3m.dartagnan.configuration.OptionNames.LOOP_BOUNDS_USE_DEF_METHOD; + /* This pass adds a loop bound annotation to static loops of the form @@ -43,12 +48,20 @@ TODO: support general step increments */ +@Options public class NaiveLoopBoundAnnotation implements FunctionProcessor { + @Option(name = LOOP_BOUNDS_USE_DEF_METHOD, + description = "", + secure = true) + private Method method = Method.BACKWARD; + public static NaiveLoopBoundAnnotation newInstance() { return new NaiveLoopBoundAnnotation(); } + public enum Method { BACKWARD, FORWARD } + @Override public void run(Function function) { if (!function.hasBody()) { @@ -56,7 +69,10 @@ public void run(Function function) { } final LiveRegistersAnalysis liveAnalysis = LiveRegistersAnalysis.forFunction(function); - final ReachingDefinitionsAnalysis useDefAnalysis = BackwardsReachingDefinitionsAnalysis.forFunction(function); + final ReachingDefinitionsAnalysis useDefAnalysis = switch(method) { + case BACKWARD -> BackwardsReachingDefinitionsAnalysis.forFunction(function); + case FORWARD -> UseDefAnalysis.forFunction(function); + }; final DominatorTree preDominatorTree = DominatorAnalysis.computePreDominatorTree(function.getEntry(), function.getExit()); final List loops = LoopAnalysis.onFunction(function).getLoopsOfFunction(function); diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/ModelChecker.java b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/ModelChecker.java index 2b004a1cb8..89077dbbec 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/ModelChecker.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/ModelChecker.java @@ -83,7 +83,7 @@ public static void performStaticProgramAnalyses(VerificationTask task, Context a Program program = task.getProgram(); analysisContext.register(BranchEquivalence.class, BranchEquivalence.fromConfig(program, config)); analysisContext.register(ExecutionAnalysis.class, ExecutionAnalysis.fromConfig(program, analysisContext, config)); - BackwardsReachingDefinitionsAnalysis.injectForProgram(program, analysisContext); + analysisContext.register(ReachingDefinitionsAnalysis.class, ReachingDefinitionsAnalysis.fromConfig(program, analysisContext, config)); analysisContext.register(AliasAnalysis.class, AliasAnalysis.fromConfig(program, analysisContext, config)); analysisContext.register(ThreadSymmetry.class, ThreadSymmetry.fromConfig(program, config)); for(Thread thread : program.getThreads()) { diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/miscellaneous/AnalysisTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/miscellaneous/AnalysisTest.java index 2d3dd80f7c..f13c9e748e 100644 --- a/dartagnan/src/test/java/com/dat3m/dartagnan/miscellaneous/AnalysisTest.java +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/miscellaneous/AnalysisTest.java @@ -12,6 +12,7 @@ import com.dat3m.dartagnan.program.analysis.BackwardsReachingDefinitionsAnalysis; import com.dat3m.dartagnan.program.analysis.BranchEquivalence; import com.dat3m.dartagnan.program.analysis.ExecutionAnalysis; +import com.dat3m.dartagnan.program.analysis.ReachingDefinitionsAnalysis; import com.dat3m.dartagnan.program.analysis.alias.AliasAnalysis; import com.dat3m.dartagnan.program.event.Event; import com.dat3m.dartagnan.program.event.EventFactory; @@ -33,6 +34,7 @@ import static com.dat3m.dartagnan.configuration.Alias.*; import static com.dat3m.dartagnan.configuration.OptionNames.ALIAS_METHOD; +import static com.dat3m.dartagnan.configuration.OptionNames.REACHING_DEFINITIONS_METHOD; import static com.dat3m.dartagnan.program.event.EventFactory.*; import static org.junit.Assert.*; @@ -49,6 +51,11 @@ private enum Result {NONE, MAY, MUST} @Test public void reachingDefinitionMustOverride() throws InvalidConfigurationException { + reachingDefinitionMustOverride(ReachingDefinitionsAnalysis.Method.BACKWARD); + reachingDefinitionMustOverride(ReachingDefinitionsAnalysis.Method.FORWARD); + } + + private void reachingDefinitionMustOverride(ReachingDefinitionsAnalysis.Method method) throws InvalidConfigurationException { ProgramBuilder b = ProgramBuilder.forLanguage(SourceLanguage.LITMUS); b.newThread(0); Register r0 = b.getOrNewRegister(0, "r0"); @@ -77,29 +84,29 @@ public void reachingDefinitionMustOverride() throws InvalidConfigurationExceptio Compilation.newInstance().run(program); LoopUnrolling.newInstance().run(program); MemoryAllocation.newInstance().run(program); - Configuration config = Configuration.defaultConfiguration(); + Configuration config = Configuration.builder().setOption(REACHING_DEFINITIONS_METHOD, method.name()).build(); Context context = Context.create(); context.register(BranchEquivalence.class, BranchEquivalence.fromConfig(program, config)); context.register(ExecutionAnalysis.class, ExecutionAnalysis.fromConfig(program, context, config)); - final var dep = BackwardsReachingDefinitionsAnalysis.injectForProgram(program, context); + final ReachingDefinitionsAnalysis rd = ReachingDefinitionsAnalysis.fromConfig(program, context, config); var me0 = (RegReader) findMatchingEventAfterProcessing(program, e0); var me1 = (RegReader) findMatchingEventAfterProcessing(program, e1); var me2 = (RegReader) findMatchingEventAfterProcessing(program, e2); var me3 = (RegReader) findMatchingEventAfterProcessing(program, e3); var me4 = (RegReader) findMatchingEventAfterProcessing(program, e4); var me5 = (RegReader) findMatchingEventAfterProcessing(program, e5); - assertTrue(dep.getWriters(me1).ofRegister(r0).mustBeInitialized()); - assertList(dep.getWriters(me1).ofRegister(r0).getMayWriters(), me0); - assertList(dep.getWriters(me1).ofRegister(r0).getMustWriters(), me0); - assertFalse(dep.getWriters(me3).ofRegister(r0).mustBeInitialized()); - assertList(dep.getWriters(me3).ofRegister(r0).getMayWriters(), me0); - assertList(dep.getWriters(me3).ofRegister(r0).getMustWriters(), me0); - assertTrue(dep.getWriters(me4).ofRegister(r1).mustBeInitialized()); - assertList(dep.getWriters(me4).ofRegister(r1).getMayWriters(), me1, me2); - assertList(dep.getWriters(me4).ofRegister(r1).getMustWriters(), me1, me2); - assertTrue(dep.getWriters(me5).ofRegister(r2).mustBeInitialized()); - assertList(dep.getWriters(me5).ofRegister(r2).getMayWriters(), me4); - assertList(dep.getWriters(me5).ofRegister(r2).getMustWriters(), me4); + assertTrue(rd.getWriters(me1).ofRegister(r0).mustBeInitialized()); + assertList(rd.getWriters(me1).ofRegister(r0).getMayWriters(), me0); + assertList(rd.getWriters(me1).ofRegister(r0).getMustWriters(), me0); + assertFalse(rd.getWriters(me3).ofRegister(r0).mustBeInitialized()); + assertList(rd.getWriters(me3).ofRegister(r0).getMayWriters(), me0); + assertList(rd.getWriters(me3).ofRegister(r0).getMustWriters(), me0); + assertTrue(rd.getWriters(me4).ofRegister(r1).mustBeInitialized()); + assertList(rd.getWriters(me4).ofRegister(r1).getMayWriters(), me1, me2); + assertList(rd.getWriters(me4).ofRegister(r1).getMustWriters(), me1, me2); + assertTrue(rd.getWriters(me5).ofRegister(r2).mustBeInitialized()); + assertList(rd.getWriters(me5).ofRegister(r2).getMayWriters(), me4); + assertList(rd.getWriters(me5).ofRegister(r2).getMustWriters(), me4); } @@ -627,7 +634,7 @@ private AliasAnalysis analyze(Program program, Alias method) throws InvalidConfi Context analysisContext = Context.create(); analysisContext.register(BranchEquivalence.class, BranchEquivalence.fromConfig(program, configuration)); analysisContext.register(ExecutionAnalysis.class, ExecutionAnalysis.fromConfig(program, analysisContext, configuration)); - BackwardsReachingDefinitionsAnalysis.injectForProgram(program, analysisContext); + analysisContext.register(ReachingDefinitionsAnalysis.class, ReachingDefinitionsAnalysis.fromConfig(program, analysisContext, configuration)); return AliasAnalysis.fromConfig(program, analysisContext, configuration); } From c0d8a382c8802e4dd3dc8160796c8941a3e5ec81 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ren=C3=A9=20Pascal=20Maseli?= Date: Tue, 10 Sep 2024 12:40:19 +0200 Subject: [PATCH 14/18] Refactor --- .../BackwardsReachingDefinitionsAnalysis.java | 52 +++++++++++-------- .../analysis/ReachingDefinitionsAnalysis.java | 12 +++-- 2 files changed, 37 insertions(+), 27 deletions(-) diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/BackwardsReachingDefinitionsAnalysis.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/BackwardsReachingDefinitionsAnalysis.java index f651b9fd58..6c15de0cd5 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/BackwardsReachingDefinitionsAnalysis.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/BackwardsReachingDefinitionsAnalysis.java @@ -21,21 +21,19 @@ import java.util.HashSet; import java.util.List; import java.util.Map; +import java.util.Objects; import java.util.Set; /** * Collects all direct usage relationships between {@link RegWriter} and {@link RegReader}. *

- * In contrast to a usual Reaching-Definitions-Analysis, - * this implementation analyzes the program from back to front, - * assigning each program point the set of readers, - * who may still require a register initialization. + * In contrast to a usual Reaching-Definitions-Analysis, this implementation analyzes the program from back to front, + * assigning each program point the set of readers, who may still require a register initialization. * This means that it does not collect definitions for unused registers. * Especially, it does not collect last writers for all registers. *

* This analysis is control-flow-sensitive; - * that is, {@link Label} splits the information among the jumps to it - * and {@link CondJump} merges the information. + * that is, {@link Label} splits the information among the jumps to it and {@link CondJump} merges the information. *

* This analysis supports loops; * that is, backward jumps cause re-evaluation of the loop body until convergence. @@ -45,6 +43,8 @@ public class BackwardsReachingDefinitionsAnalysis implements ReachingDefinitions private final Map readerMap = new HashMap<>(); private final Map writerMap = new HashMap<>(); + private final RegWriter INITIAL_WRITER = null; + private final RegReader FINAL_READER = null; @Override public Writers getWriters(RegReader reader) { @@ -56,7 +56,7 @@ public Writers getWriters(RegReader reader) { @Override public Writers getFinalWriters() { - final ReaderInfo result = readerMap.get(null); + final ReaderInfo result = readerMap.get(FINAL_READER); Preconditions.checkState(result != null, "final state has not been analyzed."); return result; } @@ -77,7 +77,7 @@ public Readers getReaders(RegWriter writer) { * Lists all potential users of uninitialized registers. */ public Readers getInitialReaders() { - final Readers result = writerMap.get(null); + final Readers result = writerMap.get(INITIAL_WRITER); Preconditions.checkState(result != null, "initial state has not been analyzed."); return result; } @@ -89,8 +89,10 @@ public Readers getInitialReaders() { public static BackwardsReachingDefinitionsAnalysis forFunction(Function function) { final var analysis = new BackwardsReachingDefinitionsAnalysis(); final Set finalRegisters = new HashSet<>(); - analysis.initialize(function, finalRegisters); - analysis.run(function, finalRegisters); + final List events = function.getEvents(); + analysis.initializeWriterMap(events); + analysis.initializeReaderMap(events, finalRegisters); + analysis.run(events, finalRegisters); analysis.postProcess(); return analysis; } @@ -109,8 +111,10 @@ public static BackwardsReachingDefinitionsAnalysis fromConfig(Program program, C final Set finalRegisters = finalRegisters(program); for (Function function : program.isUnrolled() ? program.getThreads() : Iterables.concat(program.getThreads(), program.getFunctions())) { - analysis.initialize(function, finalRegisters); - analysis.run(function, finalRegisters); + final List events = function.getEvents(); + analysis.initializeWriterMap(events); + analysis.initializeReaderMap(events, finalRegisters); + analysis.run(events, finalRegisters); } analysis.postProcess(); if (exec != null && program.isUnrolled()) { @@ -209,14 +213,17 @@ public boolean mayBeFinal() { private BackwardsReachingDefinitionsAnalysis() {} - private void initialize(Function function, Set finalRegisters) { - for (Event event : function.getEvents()) { + private void initializeWriterMap(Collection events) { + for (Event event : events) { if (event instanceof RegWriter writer) { writerMap.put(writer, new Readers()); } } - writerMap.put(null, new Readers()); - for (Event event : function.getEvents()) { + writerMap.put(INITIAL_WRITER, new Readers()); + } + + private void initializeReaderMap(Collection events, Set finalRegisters) { + for (Event event : events) { if (event instanceof RegReader reader) { final Set usedRegisters = new HashSet<>(); for (Register.Read read : reader.getRegisterReads()) { @@ -225,20 +232,19 @@ private void initialize(Function function, Set finalRegisters) { readerMap.put(reader, new ReaderInfo(usedRegisters)); } } - readerMap.put(null, new ReaderInfo(finalRegisters)); + readerMap.put(FINAL_READER, new ReaderInfo(finalRegisters)); } - private void run(Function function, Set finalRegisters) { + private void run(List events, Set finalRegisters) { //For each register used after this state, all future users. final State currentState = new State(); for (Register finalRegister : finalRegisters) { final var info = new StateInfo(); - info.mayReaders.add(null); + info.mayReaders.add(FINAL_READER); currentState.put(finalRegister, info); } final Map trueStates = new HashMap<>(); final Map falseStates = new HashMap<>(); - final List events = function.getEvents(); for (int i = events.size() - 1; i >= 0; i--) { final CondJump loop = runLocal(events.get(i), currentState, trueStates, falseStates); if (loop != null) { @@ -248,7 +254,7 @@ private void run(Function function, Set finalRegisters) { } } // set the uninitialized flags - final Readers uninitialized = writerMap.get(null); + final Readers uninitialized = writerMap.get(INITIAL_WRITER); for (Map.Entry entry : currentState.entrySet()) { uninitialized.readers.addAll(entry.getValue().mayReaders); for (RegReader reader : entry.getValue().mayReaders) { @@ -260,7 +266,7 @@ private void run(Function function, Set finalRegisters) { private void postProcess() { // build the reverse association for (Map.Entry entry : writerMap.entrySet()) { - if (entry.getKey() == null) { + if (Objects.equals(entry.getKey(), INITIAL_WRITER)) { continue; } for (RegReader reader : entry.getValue().readers) { @@ -275,7 +281,7 @@ private void postProcess() { } // set the final flag for (Readers writer : writerMap.values()) { - writer.mayBeFinal = writer.readers.remove(null); + writer.mayBeFinal = writer.readers.remove(FINAL_READER); } } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/ReachingDefinitionsAnalysis.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/ReachingDefinitionsAnalysis.java index c97dfa2bdd..41caac9a2f 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/ReachingDefinitionsAnalysis.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/ReachingDefinitionsAnalysis.java @@ -51,7 +51,8 @@ interface Writers { } /** - * Instances of this class are associated with a {@link Register} and either a {@link RegReader} or the final state of the program or function. + * Instances of this class are associated with a {@link Register} + * and either a {@link RegReader} or the final state of the program or function. */ interface RegisterWriters { @@ -63,19 +64,22 @@ interface RegisterWriters { boolean mustBeInitialized(); /** - * Lists writers s.t. there may be executions, where some instance of the associated reader directly uses the result of an instance of that writer. + * Lists writers s.t. there may be executions, where some instance of the associated reader directly uses the + * result of an instance of that writer. * @return Writers in program order. */ List getMayWriters(); /** - * Lists writers s.t. all event instances of the associated reader in any execution read from all instances of that writer in that execution. + * Lists writers s.t. all event instances of the associated reader in any execution read from all instances of + * that writer in that execution. * @return Writers in program order. */ List getMustWriters(); } - static ReachingDefinitionsAnalysis fromConfig(Program program, Context analysisContext, Configuration config) throws InvalidConfigurationException { + static ReachingDefinitionsAnalysis fromConfig(Program program, Context analysisContext, Configuration config) + throws InvalidConfigurationException { var c = new Config(); config.inject(c); ReachingDefinitionsAnalysis analysis = switch (c.method) { From bf0c691bcc3dd98ff02185b786317f9e2c98d8da Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ren=C3=A9=20Pascal=20Maseli?= Date: Tue, 10 Sep 2024 14:10:55 +0200 Subject: [PATCH 15/18] Refactor --- .../BackwardsReachingDefinitionsAnalysis.java | 40 +++++++------------ 1 file changed, 15 insertions(+), 25 deletions(-) diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/BackwardsReachingDefinitionsAnalysis.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/BackwardsReachingDefinitionsAnalysis.java index 6c15de0cd5..c0eef846b7 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/BackwardsReachingDefinitionsAnalysis.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/BackwardsReachingDefinitionsAnalysis.java @@ -89,16 +89,14 @@ public Readers getInitialReaders() { public static BackwardsReachingDefinitionsAnalysis forFunction(Function function) { final var analysis = new BackwardsReachingDefinitionsAnalysis(); final Set finalRegisters = new HashSet<>(); - final List events = function.getEvents(); - analysis.initializeWriterMap(events); - analysis.initializeReaderMap(events, finalRegisters); - analysis.run(events, finalRegisters); + analysis.initialize(function, finalRegisters); + analysis.run(function, finalRegisters); analysis.postProcess(); return analysis; } /** - * Analyzes an entire set of threads. + * Analyzes the entire program (after thread creation). *

* Optionally queries {@link ExecutionAnalysis} for pairs of writers appearing together in an execution. * @param program Contains a set of threads to be analyzed. Additionally-defined functions are ignored. @@ -111,10 +109,8 @@ public static BackwardsReachingDefinitionsAnalysis fromConfig(Program program, C final Set finalRegisters = finalRegisters(program); for (Function function : program.isUnrolled() ? program.getThreads() : Iterables.concat(program.getThreads(), program.getFunctions())) { - final List events = function.getEvents(); - analysis.initializeWriterMap(events); - analysis.initializeReaderMap(events, finalRegisters); - analysis.run(events, finalRegisters); + analysis.initialize(function, finalRegisters); + analysis.run(function, finalRegisters); } analysis.postProcess(); if (exec != null && program.isUnrolled()) { @@ -213,29 +209,22 @@ public boolean mayBeFinal() { private BackwardsReachingDefinitionsAnalysis() {} - private void initializeWriterMap(Collection events) { - for (Event event : events) { - if (event instanceof RegWriter writer) { - writerMap.put(writer, new Readers()); - } + private void initialize(Function function, Set finalRegisters) { + for (RegWriter writer : function.getEvents(RegWriter.class)) { + writerMap.put(writer, new Readers()); } writerMap.put(INITIAL_WRITER, new Readers()); - } - - private void initializeReaderMap(Collection events, Set finalRegisters) { - for (Event event : events) { - if (event instanceof RegReader reader) { - final Set usedRegisters = new HashSet<>(); - for (Register.Read read : reader.getRegisterReads()) { - usedRegisters.add(read.register()); - } - readerMap.put(reader, new ReaderInfo(usedRegisters)); + for (RegReader reader : function.getEvents(RegReader.class)) { + final Set usedRegisters = new HashSet<>(); + for (Register.Read read : reader.getRegisterReads()) { + usedRegisters.add(read.register()); } + readerMap.put(reader, new ReaderInfo(usedRegisters)); } readerMap.put(FINAL_READER, new ReaderInfo(finalRegisters)); } - private void run(List events, Set finalRegisters) { + private void run(Function function, Set finalRegisters) { //For each register used after this state, all future users. final State currentState = new State(); for (Register finalRegister : finalRegisters) { @@ -245,6 +234,7 @@ private void run(List events, Set finalRegisters) { } final Map trueStates = new HashMap<>(); final Map falseStates = new HashMap<>(); + final List events = function.getEvents(); for (int i = events.size() - 1; i >= 0; i--) { final CondJump loop = runLocal(events.get(i), currentState, trueStates, falseStates); if (loop != null) { From 0db0bb7d3aa24d27c0ca2ca51b7ebbc254e19e9a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ren=C3=A9=20Pascal=20Maseli?= Date: Fri, 20 Sep 2024 17:48:31 +0200 Subject: [PATCH 16/18] fixup! Merge remote-tracking branch 'refs/remotes/origin/development' into backwards-reaching-definitions --- .../com/dat3m/dartagnan/utils/options/BaseOptions.java | 7 ------- 1 file changed, 7 deletions(-) diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/utils/options/BaseOptions.java b/dartagnan/src/main/java/com/dat3m/dartagnan/utils/options/BaseOptions.java index 70210b0e14..176c97689d 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/utils/options/BaseOptions.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/utils/options/BaseOptions.java @@ -118,11 +118,4 @@ public boolean getDumpSmtLib() { public String getCatIncludePath() { return catIncludePath; } - - @Option( - name=SMTLIB2, - description="Dump encoding to an SMTLIB2 file.") - private boolean smtlib=false; - - public boolean getDumpSmtLib() { return smtlib; } } \ No newline at end of file From b8f136feb5452831943760dd6ac99be4f6c20302 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ren=C3=A9=20Pascal=20Maseli?= Date: Fri, 20 Sep 2024 18:38:19 +0200 Subject: [PATCH 17/18] Remove option program.processing.loopBounds.useDefAnalysis Remove NaiveLoopBoundAnnotation.newInstance() Add NaiveLoopBoundAnnotation.fromConfig(Configuration) Add ReachingDefinitionsAnalysis.configure(Configuration) Set BackwardsReachingDefinitionsAnalysis package-private --- .../dartagnan/configuration/OptionNames.java | 1 - .../BackwardsReachingDefinitionsAnalysis.java | 11 +++---- .../analysis/ReachingDefinitionsAnalysis.java | 31 ++++++++++++++----- .../processing/NaiveLoopBoundAnnotation.java | 27 ++++++---------- .../program/processing/ProcessingManager.java | 2 +- .../dartagnan/miscellaneous/AnalysisTest.java | 9 ++++-- 6 files changed, 45 insertions(+), 36 deletions(-) diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/configuration/OptionNames.java b/dartagnan/src/main/java/com/dat3m/dartagnan/configuration/OptionNames.java index f0d77eb788..61831093e1 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/configuration/OptionNames.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/configuration/OptionNames.java @@ -46,7 +46,6 @@ public class OptionNames { public static final String DYNAMIC_SPINLOOP_DETECTION = "program.processing.spinloops"; public static final String PROPAGATE_COPY_ASSIGNMENTS = "program.processing.propagateCopyAssignments"; public static final String REMOVE_ASSERTION_OF_TYPE = "program.processing.skipAssertionsOfType"; - public static final String LOOP_BOUNDS_USE_DEF_METHOD = "program.processing.loopBounds.useDefAnalysis"; // Program Property Options public static final String REACHING_DEFINITIONS_METHOD = "program.analysis.reachingDefinitions"; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/BackwardsReachingDefinitionsAnalysis.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/BackwardsReachingDefinitionsAnalysis.java index c0eef846b7..255cccd3f2 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/BackwardsReachingDefinitionsAnalysis.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/BackwardsReachingDefinitionsAnalysis.java @@ -10,8 +10,8 @@ import com.dat3m.dartagnan.program.event.core.Label; import com.dat3m.dartagnan.verification.Context; import com.google.common.base.Preconditions; +import com.google.common.base.Verify; import com.google.common.collect.Iterables; -import org.sosy_lab.common.configuration.Configuration; import java.util.ArrayList; import java.util.Collection; @@ -39,7 +39,7 @@ * that is, backward jumps cause re-evaluation of the loop body until convergence. * This results in a squared worst-case time complexity in terms of events being processed. */ -public class BackwardsReachingDefinitionsAnalysis implements ReachingDefinitionsAnalysis { +class BackwardsReachingDefinitionsAnalysis implements ReachingDefinitionsAnalysis { private final Map readerMap = new HashMap<>(); private final Map writerMap = new HashMap<>(); @@ -57,7 +57,7 @@ public Writers getWriters(RegReader reader) { @Override public Writers getFinalWriters() { final ReaderInfo result = readerMap.get(FINAL_READER); - Preconditions.checkState(result != null, "final state has not been analyzed."); + Verify.verify(result != null, "final state has not been analyzed."); return result; } @@ -78,7 +78,7 @@ public Readers getReaders(RegWriter writer) { */ public Readers getInitialReaders() { final Readers result = writerMap.get(INITIAL_WRITER); - Preconditions.checkState(result != null, "initial state has not been analyzed."); + Verify.verify(result != null, "initial state has not been analyzed."); return result; } @@ -101,9 +101,8 @@ public static BackwardsReachingDefinitionsAnalysis forFunction(Function function * Optionally queries {@link ExecutionAnalysis} for pairs of writers appearing together in an execution. * @param program Contains a set of threads to be analyzed. Additionally-defined functions are ignored. * @param analysisContext Collection of previous analyses to be used as dependencies. - * @param config User-defined settings for this analysis. */ - public static BackwardsReachingDefinitionsAnalysis fromConfig(Program program, Context analysisContext, Configuration config) { + public static BackwardsReachingDefinitionsAnalysis forProgram(Program program, Context analysisContext) { final ExecutionAnalysis exec = analysisContext.get(ExecutionAnalysis.class); final var analysis = new BackwardsReachingDefinitionsAnalysis(); final Set finalRegisters = finalRegisters(program); diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/ReachingDefinitionsAnalysis.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/ReachingDefinitionsAnalysis.java index 41caac9a2f..d2997516ab 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/ReachingDefinitionsAnalysis.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/ReachingDefinitionsAnalysis.java @@ -1,5 +1,6 @@ package com.dat3m.dartagnan.program.analysis; +import com.dat3m.dartagnan.program.Function; import com.dat3m.dartagnan.program.Program; import com.dat3m.dartagnan.program.Register; import com.dat3m.dartagnan.program.event.RegReader; @@ -80,22 +81,38 @@ interface RegisterWriters { static ReachingDefinitionsAnalysis fromConfig(Program program, Context analysisContext, Configuration config) throws InvalidConfigurationException { - var c = new Config(); - config.inject(c); - ReachingDefinitionsAnalysis analysis = switch (c.method) { - case BACKWARD -> BackwardsReachingDefinitionsAnalysis.fromConfig(program, analysisContext, config); + ReachingDefinitionsAnalysis analysis = switch (configure(config).method) { + case BACKWARD -> BackwardsReachingDefinitionsAnalysis.forProgram(program, analysisContext); case FORWARD -> Dependency.fromConfig(program, analysisContext, config); }; analysisContext.register(ReachingDefinitionsAnalysis.class, analysis); return analysis; } + static Config configure(Configuration config) throws InvalidConfigurationException { + var c = new Config(); + config.inject(c); + return c; + } + + enum Method { BACKWARD, FORWARD } + @Options final class Config { - @Option(name = REACHING_DEFINITIONS_METHOD, description = "", secure = true) + @Option(name = REACHING_DEFINITIONS_METHOD, + description = "Specifies the static analysis algorithm, that collects the relationship between" + + " register writers and their direct readers.", + secure = true) private Method method = Method.BACKWARD; - } - enum Method { BACKWARD, FORWARD} + private Config() {} + + public ReachingDefinitionsAnalysis forFunction(Function function) { + return switch (method) { + case BACKWARD -> BackwardsReachingDefinitionsAnalysis.forFunction(function); + case FORWARD -> UseDefAnalysis.forFunction(function); + }; + } + } } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/NaiveLoopBoundAnnotation.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/NaiveLoopBoundAnnotation.java index 55c3083c87..4ecfc1498e 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/NaiveLoopBoundAnnotation.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/NaiveLoopBoundAnnotation.java @@ -6,12 +6,10 @@ import com.dat3m.dartagnan.expression.misc.ITEExpr; import com.dat3m.dartagnan.program.Function; import com.dat3m.dartagnan.program.Register; -import com.dat3m.dartagnan.program.analysis.BackwardsReachingDefinitionsAnalysis; import com.dat3m.dartagnan.program.analysis.DominatorAnalysis; import com.dat3m.dartagnan.program.analysis.LiveRegistersAnalysis; import com.dat3m.dartagnan.program.analysis.LoopAnalysis; import com.dat3m.dartagnan.program.analysis.ReachingDefinitionsAnalysis; -import com.dat3m.dartagnan.program.analysis.UseDefAnalysis; import com.dat3m.dartagnan.program.event.Event; import com.dat3m.dartagnan.program.event.EventFactory; import com.dat3m.dartagnan.program.event.RegWriter; @@ -19,13 +17,11 @@ import com.dat3m.dartagnan.program.event.core.Label; import com.dat3m.dartagnan.program.event.core.Local; import com.dat3m.dartagnan.utils.DominatorTree; -import org.sosy_lab.common.configuration.Option; -import org.sosy_lab.common.configuration.Options; +import org.sosy_lab.common.configuration.Configuration; +import org.sosy_lab.common.configuration.InvalidConfigurationException; import java.util.List; -import static com.dat3m.dartagnan.configuration.OptionNames.LOOP_BOUNDS_USE_DEF_METHOD; - /* This pass adds a loop bound annotation to static loops of the form @@ -48,19 +44,17 @@ TODO: support general step increments */ -@Options public class NaiveLoopBoundAnnotation implements FunctionProcessor { - @Option(name = LOOP_BOUNDS_USE_DEF_METHOD, - description = "", - secure = true) - private Method method = Method.BACKWARD; + private final ReachingDefinitionsAnalysis.Config reachingDefinitionsAnalysis; - public static NaiveLoopBoundAnnotation newInstance() { - return new NaiveLoopBoundAnnotation(); + private NaiveLoopBoundAnnotation(ReachingDefinitionsAnalysis.Config c) { + reachingDefinitionsAnalysis = c; } - public enum Method { BACKWARD, FORWARD } + public static NaiveLoopBoundAnnotation fromConfig(Configuration config) throws InvalidConfigurationException { + return new NaiveLoopBoundAnnotation(ReachingDefinitionsAnalysis.configure(config)); + } @Override public void run(Function function) { @@ -69,10 +63,7 @@ public void run(Function function) { } final LiveRegistersAnalysis liveAnalysis = LiveRegistersAnalysis.forFunction(function); - final ReachingDefinitionsAnalysis useDefAnalysis = switch(method) { - case BACKWARD -> BackwardsReachingDefinitionsAnalysis.forFunction(function); - case FORWARD -> UseDefAnalysis.forFunction(function); - }; + final ReachingDefinitionsAnalysis useDefAnalysis = reachingDefinitionsAnalysis.forFunction(function); final DominatorTree preDominatorTree = DominatorAnalysis.computePreDominatorTree(function.getEntry(), function.getExit()); final List loops = LoopAnalysis.onFunction(function).getLoopsOfFunction(function); diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/ProcessingManager.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/ProcessingManager.java index 19c24b528e..60b209d087 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/ProcessingManager.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/ProcessingManager.java @@ -108,7 +108,7 @@ private ProcessingManager(Configuration config) throws InvalidConfigurationExcep ProgramProcessor.fromFunctionProcessor(MemToReg.fromConfig(config), Target.FUNCTIONS, true), ProgramProcessor.fromFunctionProcessor(sccp, Target.FUNCTIONS, false), dynamicSpinLoopDetection ? DynamicSpinLoopDetection.fromConfig(config) : null, - ProgramProcessor.fromFunctionProcessor(NaiveLoopBoundAnnotation.newInstance(), Target.FUNCTIONS, true), + ProgramProcessor.fromFunctionProcessor(NaiveLoopBoundAnnotation.fromConfig(config), Target.FUNCTIONS, true), LoopUnrolling.fromConfig(config), // We keep unrolling global for now printAfterUnrolling ? DebugPrint.withHeader("After loop unrolling", Printer.Mode.ALL) : null, ProgramProcessor.fromFunctionProcessor( diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/miscellaneous/AnalysisTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/miscellaneous/AnalysisTest.java index 62f05b006a..fea312ebc5 100644 --- a/dartagnan/src/test/java/com/dat3m/dartagnan/miscellaneous/AnalysisTest.java +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/miscellaneous/AnalysisTest.java @@ -10,7 +10,6 @@ import com.dat3m.dartagnan.program.Program; import com.dat3m.dartagnan.program.Program.SourceLanguage; import com.dat3m.dartagnan.program.Register; -import com.dat3m.dartagnan.program.analysis.BackwardsReachingDefinitionsAnalysis; import com.dat3m.dartagnan.program.analysis.BranchEquivalence; import com.dat3m.dartagnan.program.analysis.ExecutionAnalysis; import com.dat3m.dartagnan.program.analysis.ReachingDefinitionsAnalysis; @@ -113,7 +112,7 @@ private void reachingDefinitionMustOverride(ReachingDefinitionsAnalysis.Method m @Test - public void reachingDefinitionSupportsLoops() { + public void reachingDefinitionSupportsLoops() throws InvalidConfigurationException { ProgramBuilder b = ProgramBuilder.forLanguage(SourceLanguage.LITMUS); b.newFunction("test", 0, types.getFunctionType(types.getArchType(), List.of()), List.of()); Register r0 = b.getOrNewRegister(0, "r0"); @@ -187,7 +186,11 @@ public void reachingDefinitionSupportsLoops() { b.addChild(0, ret); Program program = b.build(); - final var dep = BackwardsReachingDefinitionsAnalysis.forFunction(program.getFunctions().get(0)); + Configuration config = Configuration.builder() + .setOption(REACHING_DEFINITIONS_METHOD, ReachingDefinitionsAnalysis.Method.BACKWARD.name()) + .build(); + final ReachingDefinitionsAnalysis dep = ReachingDefinitionsAnalysis.configure(config) + .forFunction(program.getFunctions().get(0)); assertFalse(dep.getWriters(r00).ofRegister(r0).mustBeInitialized()); assertList(dep.getWriters(r00).ofRegister(r0).getMayWriters()); assertFalse(dep.getWriters(r10).ofRegister(r0).mustBeInitialized()); From e91f205ec3039ce7c8d642b2461407ce31ec9876 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ren=C3=A9=20Pascal=20Maseli?= Date: Fri, 20 Sep 2024 18:47:30 +0200 Subject: [PATCH 18/18] Small reformat --- .../dat3m/dartagnan/verification/solving/RefinementSolver.java | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/RefinementSolver.java b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/RefinementSolver.java index 4d5a8b134b..6aa6619b73 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/RefinementSolver.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/RefinementSolver.java @@ -555,8 +555,7 @@ private static void addBiases(Wmm wmm, EnumSet biases) { rf, co, fr - ) - ))); + )))); } if (biases.contains(Baseline.NO_OOTA)) { // ---- acyclic (dep | rf) ----