Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Visual output of Alias Analysis #581

Merged
merged 1 commit into from
Jan 18, 2024
Merged

Visual output of Alias Analysis #581

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
9 changes: 6 additions & 3 deletions dartagnan/src/main/java/com/dat3m/dartagnan/configuration/OptionNames.java
View file
Open in desktop
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
Open in desktop
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) {
hernanponcedeleon marked this conversation as resolved.
Show resolved Hide resolved
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