From 73ba96cc45a86775abac72493b436deab020b4b7 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ren=C3=A9=20Maseli?= Date: Sat, 21 Sep 2024 08:55:09 +0200 Subject: [PATCH] Backwards reaching definitions (#726) --- .../dartagnan/configuration/OptionNames.java | 1 + .../dartagnan/encoding/ProgramEncoder.java | 46 ++- .../dat3m/dartagnan/encoding/WmmEncoder.java | 17 +- .../BackwardsReachingDefinitionsAnalysis.java | 379 ++++++++++++++++++ .../program/analysis/Dependency.java | 55 ++- .../analysis/ReachingDefinitionsAnalysis.java | 118 ++++++ .../program/analysis/UseDefAnalysis.java | 56 ++- .../alias/InclusionBasedPointerAnalysis.java | 13 +- .../processing/NaiveLoopBoundAnnotation.java | 27 +- .../program/processing/ProcessingManager.java | 2 +- .../verification/solving/ModelChecker.java | 2 +- .../wmm/analysis/CoarseRelationAnalysis.java | 4 +- .../wmm/analysis/NativeRelationAnalysis.java | 15 +- .../wmm/analysis/RelationAnalysis.java | 4 +- .../dartagnan/miscellaneous/AnalysisTest.java | 172 ++++++-- 15 files changed, 818 insertions(+), 93 deletions(-) create mode 100644 dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/BackwardsReachingDefinitionsAnalysis.java create mode 100644 dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/ReachingDefinitionsAnalysis.java 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 7fbbae45aa..61831093e1 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/configuration/OptionNames.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/configuration/OptionNames.java @@ -48,6 +48,7 @@ public class OptionNames { public static final String REMOVE_ASSERTION_OF_TYPE = "program.processing.skipAssertionsOfType"; // 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/encoding/ProgramEncoder.java b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProgramEncoder.java index 2836d3cf57..a7fbbad893 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProgramEncoder.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProgramEncoder.java @@ -8,9 +8,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; @@ -54,14 +55,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 { @@ -346,21 +347,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(RegWriter writer : reverse(state.may)) { + 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)); @@ -372,7 +373,7 @@ public BooleanFormula encodeDependencies() { 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)); @@ -398,25 +399,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 1034609ac1..b85578e9b2 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; @@ -367,16 +368,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/BackwardsReachingDefinitionsAnalysis.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/BackwardsReachingDefinitionsAnalysis.java new file mode 100644 index 0000000000..255cccd3f2 --- /dev/null +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/BackwardsReachingDefinitionsAnalysis.java @@ -0,0 +1,379 @@ +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.base.Verify; +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.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. + * 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 in terms of events being processed. + */ +class BackwardsReachingDefinitionsAnalysis implements ReachingDefinitionsAnalysis { + + 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) { + 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(FINAL_READER); + Verify.verify(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(INITIAL_WRITER); + Verify.verify(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 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. + * @param analysisContext Collection of previous analyses to be used as dependencies. + */ + 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); + for (Function function : program.isUnrolled() ? program.getThreads() : + Iterables.concat(program.getThreads(), program.getFunctions())) { + analysis.initialize(function, finalRegisters); + analysis.run(function, finalRegisters); + } + analysis.postProcess(); + if (exec != null && program.isUnrolled()) { + analysis.analyzeMust(exec); + } + 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 (RegWriter writer : function.getEvents(RegWriter.class)) { + writerMap.put(writer, new Readers()); + } + writerMap.put(INITIAL_WRITER, new Readers()); + 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(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(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) { + merge(currentState, falseStates.getOrDefault(loop, new State())); + update(currentState, loop); + i = events.indexOf(loop); + } + } + // set the uninitialized flags + 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) { + readerMap.get(reader).uninitialized.add(entry.getKey()); + } + } + } + + private void postProcess() { + // build the reverse association + for (Map.Entry entry : writerMap.entrySet()) { + if (Objects.equals(entry.getKey(), INITIAL_WRITER)) { + 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(FINAL_READER); + } + } + + 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(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()), exec)) { + reader.mustWriters.add(writer); + } + } + } + } + + private static boolean mayBeOverwritten(RegWriter earlyWriter, List lateWriters, ExecutionAnalysis exec) { + final Register resultRegister = earlyWriter.getResultRegister(); + for (RegWriter lateWriter : lateWriters) { + if (lateWriter.getResultRegister().equals(resultRegister) && + !exec.areMutuallyExclusive(earlyWriter, lateWriter)) { + return true; + } + } + return false; + } +} 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..d2997516ab --- /dev/null +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/ReachingDefinitionsAnalysis.java @@ -0,0 +1,118 @@ +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; +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. + */ +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(); + } + + static ReachingDefinitionsAnalysis fromConfig(Program program, Context analysisContext, Configuration config) + throws InvalidConfigurationException { + 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 = "Specifies the static analysis algorithm, that collects the relationship between" + + " register writers and their direct readers.", + secure = true) + private Method method = Method.BACKWARD; + + 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/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 79aef38f9b..4321914963 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/program/processing/NaiveLoopBoundAnnotation.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/NaiveLoopBoundAnnotation.java index a558858f51..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 @@ -9,7 +9,7 @@ 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; @@ -17,9 +17,10 @@ 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.Configuration; +import org.sosy_lab.common.configuration.InvalidConfigurationException; import java.util.List; -import java.util.Set; /* This pass adds a loop bound annotation to static loops of the form @@ -45,8 +46,14 @@ */ public class NaiveLoopBoundAnnotation implements FunctionProcessor { - public static NaiveLoopBoundAnnotation newInstance() { - return new NaiveLoopBoundAnnotation(); + private final ReachingDefinitionsAnalysis.Config reachingDefinitionsAnalysis; + + private NaiveLoopBoundAnnotation(ReachingDefinitionsAnalysis.Config c) { + reachingDefinitionsAnalysis = c; + } + + public static NaiveLoopBoundAnnotation fromConfig(Configuration config) throws InvalidConfigurationException { + return new NaiveLoopBoundAnnotation(ReachingDefinitionsAnalysis.configure(config)); } @Override @@ -56,7 +63,7 @@ public void run(Function function) { } final LiveRegistersAnalysis liveAnalysis = LiveRegistersAnalysis.forFunction(function); - final UseDefAnalysis useDefAnalysis = 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); @@ -123,7 +130,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 +149,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 +175,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 +194,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; 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/main/java/com/dat3m/dartagnan/verification/solving/ModelChecker.java b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/ModelChecker.java index 1452385911..ae0e11f9fe 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, task.getProgressModel(), analysisContext, config)); - analysisContext.register(Dependency.class, Dependency.fromConfig(program, analysisContext, config)); + 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/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 8ef721f364..c9c1dae705 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} *
@@ -904,6 +904,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; @@ -917,11 +918,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 6c83163eae..fea312ebc5 100644 --- a/dartagnan/src/test/java/com/dat3m/dartagnan/miscellaneous/AnalysisTest.java +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/miscellaneous/AnalysisTest.java @@ -11,12 +11,14 @@ import com.dat3m.dartagnan.program.Program.SourceLanguage; import com.dat3m.dartagnan.program.Register; 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.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; @@ -32,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.*; @@ -47,7 +50,12 @@ private enum Result {NONE, MAY, MUST} private static final ExpressionFactory expressions = ExpressionFactory.getInstance(); @Test - public void dependencyMustOverride() throws InvalidConfigurationException { + 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"); @@ -59,7 +67,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)); @@ -76,29 +84,145 @@ public void dependencyMustOverride() throws InvalidConfigurationException { 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, ProgressModel.FAIR, 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); + 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(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); + } + + + + @Test + 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"); + 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(); + 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()); + 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 @@ -514,7 +638,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, ProgressModel.FAIR, analysisContext, configuration)); - analysisContext.register(Dependency.class, Dependency.fromConfig(program, analysisContext, configuration)); + analysisContext.register(ReachingDefinitionsAnalysis.class, ReachingDefinitionsAnalysis.fromConfig(program, analysisContext, configuration)); return AliasAnalysis.fromConfig(program, analysisContext, configuration); }