Skip to content

Commit

Permalink
New Pointer Analysis (#616)
Browse files Browse the repository at this point in the history 
Signed-off-by: Hernan Ponce de Leon <[email protected]>
Co-authored-by: Hernan Ponce de Leon <[email protected]>
Co-authored-by: Thomas Haas <[email protected]>
Co-authored-by: Thomas Haas <[email protected]>
  • Loading branch information
@xeren @hernan-poncedeleon @ThomasHaas
4 people authored Apr 29, 2024
1 parent 1fe3890 commit 506ed2f
Show file tree
Hide file tree
Showing 9 changed files with 1,161 additions and 52 deletions.
6 changes: 3 additions & 3 deletions dartagnan/src/main/java/com/dat3m/dartagnan/configuration/Alias.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,15 +4,15 @@

public enum Alias implements OptionInterface {
// For comparison reasons, we might want to add a NONE method with may = true, must = false
FIELD_SENSITIVE, FIELD_INSENSITIVE;
FIELD_SENSITIVE, FIELD_INSENSITIVE, FULL;

public static Alias getDefault() {
return FIELD_SENSITIVE;
return FULL;
}

// Used to decide the order shown by the selector in the UI
public static Alias[] orderedValues() {
Alias[] order = { FIELD_SENSITIVE, FIELD_INSENSITIVE };
Alias[] order = { FIELD_SENSITIVE, FIELD_INSENSITIVE, FULL };
// Be sure no element is missing
assert(Arrays.asList(order).containsAll(Arrays.asList(values())));
return order;
Expand Down
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 @@ -47,6 +47,7 @@ public class OptionNames {
public static final String ALIAS_GRAPHVIZ = "program.analysis.generateAliasGraph";
public static final String ALIAS_GRAPHVIZ_SPLIT_BY_THREAD = "program.analysis.generateAliasGraph.splitByThread";
public static final String ALIAS_GRAPHVIZ_SHOW_ALL = "program.analysis.generateAliasGraph.showAllEvents";
public static final String ALIAS_GRAPHVIZ_INTERNAL = "program.analysis.generateAliasGraph.internal";
public static final String ALWAYS_SPLIT_ON_JUMPS = "program.analysis.cf.alwaysSplitOnJump";
public static final String MERGE_BRANCHES = "program.analysis.cf.mergeBranches";

Expand Down
6 changes: 3 additions & 3 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 @@ -265,7 +265,7 @@ public BooleanFormula encodeFinalRegisterValues() {
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<Event> writers = state.may;
final List<RegWriter> writers = state.may;
if(initializeRegisters && !state.initialized) {
List<BooleanFormula> clause = new ArrayList<>();
clause.add(context.equalZero(value));
Expand All @@ -275,9 +275,9 @@ public BooleanFormula encodeFinalRegisterValues() {
enc.add(bmgr.or(clause));
}
for(int i = 0; i < writers.size(); i++) {
final Event writer = writers.get(i);
final RegWriter writer = writers.get(i);
List<BooleanFormula> clause = new ArrayList<>();
clause.add(context.equal(value, context.result((RegWriter) writer)));
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)) {
Expand Down
18 changes: 9 additions & 9 deletions dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/Dependency.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -146,7 +146,7 @@ private void process(Thread thread, ExecutionAnalysis exec) {
if (event.cfImpliesExec()) {
state.removeIf(e -> e.register.equals(register));
}
state.add(new Writer(register, event));
state.add(new Writer(register, rw));
}
//copy state, if branching
if (event instanceof CondJump jump) {
Expand All @@ -170,18 +170,18 @@ private void process(Thread thread, ExecutionAnalysis exec) {
}

private static State process(Event reader, Set<Writer> state, Register register, ExecutionAnalysis exec) {
List<Event> candidates = state.stream()
List<RegWriter> candidates = state.stream()
.filter(e -> e.register.equals(register))
.map(e -> e.event)
.filter(e -> reader == null || !exec.areMutuallyExclusive(reader, e))
.toList();
//NOTE if candidates is empty, the reader is unreachable
List<Event> mays = candidates.stream()
List<RegWriter> mays = candidates.stream()
.filter(Objects::nonNull)
.sorted(Comparator.comparingInt(Event::getGlobalId))
.collect(Collectors.toCollection(ArrayList::new));
int end = mays.size();
List<Event> musts = range(0, end)
List<RegWriter> musts = range(0, end)
.filter(i -> mays.subList(i + 1, end).stream().allMatch(j -> exec.areMutuallyExclusive(mays.get(i), j)))
.mapToObj(mays::get)
.collect(toList());
Expand All @@ -190,9 +190,9 @@ private static State process(Event reader, Set<Writer> state, Register register,

private static final class Writer {
final Register register;
final Event event;
final RegWriter event;

Writer(Register r, Event e) {
Writer(Register r, RegWriter e) {
register = checkNotNull(r);
event = e;
}
Expand Down Expand Up @@ -226,15 +226,15 @@ public static final class State {
* 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<Event> may;
public final List<RegWriter> 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<Event> must;
public final List<RegWriter> must;

private State(boolean initialized, List<Event> may, List<Event> must) {
private State(boolean initialized, List<RegWriter> may, List<RegWriter> must) {
verify(new HashSet<>(may).containsAll(must), "Each must-writer must also be a may-writer.");
verify(may.isEmpty() || must.contains(may.get(may.size() - 1)), "The last may-writer must also be a must-writer.");
this.initialized = initialized;
Expand Down
56 changes: 37 additions & 19 deletions dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/alias/AliasAnalysis.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -9,6 +9,7 @@
import com.dat3m.dartagnan.program.event.metadata.SourceLocation;
import com.dat3m.dartagnan.utils.Utils;
import com.dat3m.dartagnan.utils.visualization.Graphviz;
import com.dat3m.dartagnan.verification.Context;
import org.apache.logging.log4j.LogManager;
import org.apache.logging.log4j.Logger;
import org.sosy_lab.common.configuration.Configuration;
Expand All @@ -32,21 +33,15 @@ public interface AliasAnalysis {

boolean mayAlias(MemoryCoreEvent a, MemoryCoreEvent b);

static AliasAnalysis fromConfig(Program program, Configuration config) throws InvalidConfigurationException {
static AliasAnalysis fromConfig(Program program, Context analysisContext, Configuration config) throws InvalidConfigurationException {
Config c = new Config(config);
logger.info("Selected alias analysis: " + c.method);
AliasAnalysis a;
logger.info("Selected alias analysis: {}", c.method);
long t0 = System.currentTimeMillis();
switch (c.method) {
case FIELD_SENSITIVE:
a = FieldSensitiveAndersen.fromConfig(program, config);
break;
case FIELD_INSENSITIVE:
a = AndersenAliasAnalysis.fromConfig(program, config);
break;
default:
throw new UnsupportedOperationException("Alias method not recognized");
}
AliasAnalysis a = switch (c.method) {
case FIELD_SENSITIVE -> FieldSensitiveAndersen.fromConfig(program, config);
case FIELD_INSENSITIVE -> AndersenAliasAnalysis.fromConfig(program, config);
case FULL -> InclusionBasedPointerAnalysis.fromConfig(program, analysisContext, c);
};
a = new CombinedAliasAnalysis(a, EqualityAliasAnalysis.fromConfig(program, config));
if (Arch.supportsVirtualAddressing(program.getArch())) {
a = VirtualAliasAnalysis.wrap(a);
Expand All @@ -64,7 +59,7 @@ static AliasAnalysis fromConfig(Program program, Configuration config) throws In
final class Config {
@Option(name = ALIAS_METHOD,
description = "General type of analysis that approximates the 'loc' relationship between memory events.")
private Alias method = Alias.FIELD_SENSITIVE;
private Alias method = Alias.getDefault();

@Option(name = ALIAS_GRAPHVIZ,
description = "If 'true', stores the results of the alias analysis as a PNG image." +
Expand All @@ -74,15 +69,23 @@ final class Config {
@Option(name = ALIAS_GRAPHVIZ_SPLIT_BY_THREAD,
description = "Controls which event sets are represented by nodes in the graph output." +
" If 'true', nodes represent events of the same thread and source location." +
" If 'false', nodes represent events of just the same source location." + " Requires '" +
ALIAS_GRAPHVIZ + "=true'." + " Defaults to 'false'.", secure = true)
" If 'false', nodes represent events of just the same source location." +
" Requires '" + ALIAS_GRAPHVIZ + "=true'." +
" Defaults to 'false'.", secure = true)
private boolean graphvizSplitByThread;

@Option(name = ALIAS_GRAPHVIZ_SHOW_ALL,
description = "If 'true', the graph representation contains even initializations." + " Requires '" +
ALIAS_GRAPHVIZ + "=true'." + " Defaults to 'false'.", secure = true)
description = "If 'true', the graph representation contains even initializations." +
" Requires '" + ALIAS_GRAPHVIZ + "=true'." +
" Defaults to 'false'.", secure = true)
private boolean graphvizShowAll;

@Option(name = ALIAS_GRAPHVIZ_INTERNAL,
description = "If 'true' and supported, the graph shows an internal representation." +
" Requires '" + ALIAS_GRAPHVIZ + "=true'." +
" Defaults to 'false'.", secure = true)
boolean graphvizInternal;

private Config(Configuration config) throws InvalidConfigurationException {
config.inject(this);
}
Expand All @@ -107,9 +110,19 @@ public boolean mustAlias(MemoryCoreEvent a, MemoryCoreEvent b) {
public boolean mayAlias(MemoryCoreEvent a, MemoryCoreEvent b) {
return a1.mayAlias(a, b) && a2.mayAlias(a, b);
}

@Override
public Graphviz getGraphVisualization() {
return a1.getGraphVisualization();
}
}

private void generateGraph(Program program, Config configuration) {
//this should be protected
default Graphviz getGraphVisualization() {
return null;
}

private Graphviz defaultGraph(Program program, Config configuration) {
// Nodes represent sets of events.
// A solid line marks the existence of events that must alias.
// A dashed line marks the existence of events that may alias.
Expand Down Expand Up @@ -144,7 +157,12 @@ private void generateGraph(Program program, Config configuration) {
graphviz.addEdges(mustGraph);
graphviz.end();
graphviz.end();
return graphviz;
}

private void generateGraph(Program program, Config configuration) {
final Graphviz internalGraph = configuration.graphvizInternal ? getGraphVisualization() : null;
final Graphviz graphviz = internalGraph != null ? internalGraph : defaultGraph(program, configuration);
// Generates the .dot file and convert into the .png file.
String programName = program.getName();
String programBase = programName.substring(0, programName.lastIndexOf('.'));
Expand Down
Loading

0 comments on commit 506ed2f

Please sign in to comment.