Skip to content

Commit

Permalink
Visual output of Alias Analysis (#581)
Browse files Browse the repository at this point in the history
  • Loading branch information
@xeren
xeren committed Jan 17, 2024
1 parent 83b3969 commit 6c1352a
Show file tree
Hide file tree
Showing 5 changed files with 261 additions and 124 deletions.
9 changes: 6 additions & 3 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 @@ -19,12 +19,12 @@ public class OptionNames {
// Compilation Options
public static final String USE_RC11_TO_ARCH_SCHEME = "compilation.rc11ToArch";
public static final String C_TO_POWER_SCHEME = "compilation.cToPower";

// Encoding Options
public static final String USE_INTEGERS = "encoding.integers";
public static final String ENABLE_ACTIVE_SETS = "encoding.activeSets";
public static final String REDUCE_ACYCLICITY_ENCODE_SETS = "encoding.wmm.reduceAcyclicityEncodeSets";
public static final String LOCALLY_CONSISTENT = "encoding.locallyConsistent";//TODO also influences RA
public static final String LOCALLY_CONSISTENT = "encoding.locallyConsistent";// TODO also influences RA
public static final String MERGE_CF_VARS = "encoding.mergeCFVars";
public static final String INITIALIZE_REGISTERS = "encoding.initializeRegisters";
public static final String BREAK_SYMMETRY_ON = "encoding.symmetry.breakOn";
Expand All @@ -42,6 +42,9 @@ public class OptionNames {

// Program Property Options
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";
public static final String ALIAS_GRAPHVIZ_SHOW_ALL = "program.analysis.generateAliasGraph.showAllEvents";
public static final String ALWAYS_SPLIT_ON_JUMPS = "program.analysis.cf.alwaysSplitOnJump";
public static final String MERGE_BRANCHES = "program.analysis.cf.mergeBranches";

Expand All @@ -52,7 +55,7 @@ public class OptionNames {

// Refinement Options
public static final String BASELINE = "refinement.baseline";

// SMT solver Options
public static final String PHANTOM_REFERENCES = "solver.z3.usePhantomReferences";

Expand Down
106 changes: 103 additions & 3 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 @@ -3,29 +3,44 @@
import com.dat3m.dartagnan.configuration.Alias;
import com.dat3m.dartagnan.configuration.Arch;
import com.dat3m.dartagnan.program.Program;
import com.dat3m.dartagnan.program.event.core.Init;
import com.dat3m.dartagnan.program.event.core.MemoryCoreEvent;
import com.dat3m.dartagnan.program.event.core.MemoryEvent;
import com.dat3m.dartagnan.program.event.metadata.SourceLocation;
import com.dat3m.dartagnan.utils.visualization.Graphviz;
import org.apache.logging.log4j.LogManager;
import org.apache.logging.log4j.Logger;
import org.sosy_lab.common.configuration.Configuration;
import org.sosy_lab.common.configuration.InvalidConfigurationException;
import org.sosy_lab.common.configuration.Option;
import org.sosy_lab.common.configuration.Options;

import static com.dat3m.dartagnan.configuration.OptionNames.ALIAS_METHOD;
import java.io.File;
import java.io.FileWriter;
import java.io.IOException;
import java.util.HashMap;
import java.util.HashSet;
import java.util.List;
import java.util.Map;
import java.util.Set;

import static com.dat3m.dartagnan.GlobalSettings.getOutputDirectory;
import static com.dat3m.dartagnan.configuration.OptionNames.*;

public interface AliasAnalysis {

Logger logger = LogManager.getLogger(AliasAnalysis.class);

boolean mustAlias(MemoryCoreEvent a, MemoryCoreEvent b);

boolean mayAlias(MemoryCoreEvent a, MemoryCoreEvent b);

static AliasAnalysis fromConfig(Program program, Configuration config) throws InvalidConfigurationException {
Config c = new Config(config);
logger.info("Selected alias analysis: " + c.method);
logger.info("Selected alias analysis: " + c.method);
AliasAnalysis a;
long t0 = System.currentTimeMillis();
switch (c.method) {
switch (c.method) {
case FIELD_SENSITIVE:
a = FieldSensitiveAndersen.fromConfig(program, config);
break;
Expand All @@ -39,6 +54,9 @@ static AliasAnalysis fromConfig(Program program, Configuration config) throws In
if (Arch.supportsVirtualAddressing(program.getArch())) {
a = VirtualAliasAnalysis.wrap(a);
}
if (c.graphviz) {
a.generateGraph(program, c);
}

long t1 = System.currentTimeMillis();
logger.info("Finished alias analysis in {}ms", t1 - t0);
Expand All @@ -51,6 +69,23 @@ final class Config {
description = "General type of analysis that approximates the 'loc' relationship between memory events.")
private Alias method = Alias.FIELD_SENSITIVE;

@Option(name = ALIAS_GRAPHVIZ,
description = "If 'true', stores the results of the alias analysis as a PNG image." +
" Defaults to 'false'.")
private boolean graphviz;

@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)
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)
private boolean graphvizShowAll;

private Config(Configuration config) throws InvalidConfigurationException {
config.inject(this);
}
Expand All @@ -77,4 +112,69 @@ public boolean mayAlias(MemoryCoreEvent a, MemoryCoreEvent b) {
}
}

private void generateGraph(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.
final Map<String, Set<String>> mayGraph = new HashMap<>();
final Map<String, Set<String>> mustGraph = new HashMap<>();
final List<MemoryCoreEvent> events = program.getThreadEvents(MemoryCoreEvent.class);
for (final MemoryCoreEvent event1 : events) {
final String node1 = repr(event1, configuration);
if (node1 == null) {
continue;
}
final Set<String> maySet = mayGraph.computeIfAbsent(node1, k -> new HashSet<>());
final Set<String> mustSet = mustGraph.computeIfAbsent(node1, k -> new HashSet<>());
for (final MemoryCoreEvent event2 : events) {
final String node2 = repr(event2, configuration);
if (node2 != null && node1.compareTo(node2) < 0 && mayAlias(event1, event2)) {
(mustAlias(event1, event2) ? mustSet : maySet).add(node2);
}
}
maySet.removeAll(mustSet);
}

// Generates the graphs
final var graphviz = new Graphviz();
graphviz.beginGraph("alias");
graphviz.beginSubgraph("may alias");
graphviz.setEdgeAttributes("color=mediumslateblue", "style=dashed");
graphviz.addEdges(mayGraph);
graphviz.end();
graphviz.beginSubgraph("must alias");
graphviz.setEdgeAttributes("color=mediumslateblue");
graphviz.addEdges(mustGraph);
graphviz.end();
graphviz.end();

// Generates the .dot file and convert into the .png file.
String programName = program.getName();
String programBase = programName.substring(0, programName.lastIndexOf('.'));
File dotFile = new File(getOutputDirectory() + "/" + programBase + "-alias.dot");
try (var writer = new FileWriter(dotFile)) {
graphviz.generateOutput(writer);
writer.flush();
logger.info("Alias graph written to {}.", dotFile);
Graphviz.convert(dotFile);
} catch (IOException | InterruptedException x) {
logger.warn("Could not write initial alias graph: \"{}\".", x.getMessage());
}
}

private static String repr(MemoryEvent event, Config configuration) {
if (!configuration.graphvizShowAll && event instanceof Init) {
return null;
}
final SourceLocation location = event.getMetadata(SourceLocation.class);
if (configuration.graphvizSplitByThread) {
return location != null ? "\"T" + event.getThread().getId() + esc(location) + "\"" :
"\"T" + event.getThread().getId() + "E" + event.getGlobalId() + "\"";
}
return location != null ? "\"" + esc(location) + "\"" : "\"E" + event.getGlobalId() + "\"";
}

private static String esc(Object object) {
return object.toString().replace('"', '\'');
}
}
Loading

0 comments on commit 6c1352a

Please sign in to comment.