Skip to content

Commit

Permalink
Backwards reaching definitions (#726)
Browse files Browse the repository at this point in the history
  • Loading branch information
@xeren
xeren authored Sep 21, 2024
1 parent 90c3a7b commit 73ba96c
Show file tree
Hide file tree
Showing 15 changed files with 818 additions and 93 deletions.
1 change: 1 addition & 0 deletions dartagnan/src/main/java/com/dat3m/dartagnan/configuration/OptionNames.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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";
Expand Down
46 changes: 24 additions & 22 deletions dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProgramEncoder.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down Expand Up @@ -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 {
Expand Down Expand Up @@ -346,21 +347,21 @@ public BooleanFormula encodeDependencies() {
logger.info("Encoding dependencies");
final BooleanFormulaManager bmgr = context.getBooleanFormulaManager();
List<BooleanFormula> enc = new ArrayList<>();
for(Map.Entry<Event,Map<Register, Dependency.State>> e : dep.getAll()) {
final Event reader = e.getKey();
for(Map.Entry<Register, Dependency.State> r : e.getValue().entrySet()) {
final Formula value = context.encodeExpressionAt(r.getKey(), reader);
final Dependency.State state = r.getValue();
List<BooleanFormula> 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<BooleanFormula> 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));
Expand All @@ -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));
Expand All @@ -398,25 +399,26 @@ public BooleanFormula encodeFinalRegisterValues() {

logger.info("Encoding final register values");
List<BooleanFormula> enc = new ArrayList<>();
for(Map.Entry<Register,Dependency.State> e : dep.finalWriters().entrySet()) {
final Formula value = context.encodeFinalExpression(e.getKey());
final Dependency.State state = e.getValue();
final List<RegWriter> 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<RegWriter> writers = registerWriters.getMayWriters();
if (initializeRegisters && !registerWriters.mustBeInitialized()) {
List<BooleanFormula> 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<BooleanFormula> 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));
}
}
Expand Down
17 changes: 10 additions & 7 deletions dartagnan/src/main/java/com/dat3m/dartagnan/encoding/WmmEncoder.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down Expand Up @@ -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)));
}
}
Expand Down
Loading

0 comments on commit 73ba96c

Please sign in to comment.