Skip to content

Commit

Permalink
Split option program.analysis.printAliasGraph
Browse files Browse the repository at this point in the history 
Add option program.analysis.generateAliasGraph
Add option program.analysis.generateAliasGraph.showAllEvents
Add option program.analysis.generateAliasGraph.splitByThread
  • Loading branch information
@xeren
xeren committed Jan 16, 2024
1 parent 872cf57 commit d213871
Show file tree
Hide file tree
Showing 3 changed files with 40 additions and 42 deletions.
6 changes: 4 additions & 2 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 @@ -42,8 +42,10 @@ public class OptionNames {

// Program Property Options
public static final String ALIAS_METHOD = "program.analysis.alias";
public static final String ALIAS_GRAPHVIZ = "program.analysis.printAliasGraph";
public static final String ALWAYS_SPLIT_ON_JUMPS = "program.analysis.cf.alwaysSplitOnJump";
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";

// Memory Model Options
Expand Down
70 changes: 33 additions & 37 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,6 +3,7 @@
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;
Expand All @@ -24,8 +25,7 @@
import java.util.Set;

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

public interface AliasAnalysis {

Expand Down Expand Up @@ -53,7 +53,9 @@ static AliasAnalysis fromConfig(Program program, Configuration config) throws In
if (Arch.supportsVirtualAddressing(program.getArch())) {
a = VirtualAliasAnalysis.wrap(a);
}
a.printGraph(program, c);
if (c.graphviz) {
a.generateGraph(program, c);
}

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

private PrintOption printOption = PrintOption.NONE;

@Option(name = ALIAS_GRAPHVIZ,
description = "If 'true', prints the results of the alias analysis as a graphviz dot file." +
description = "If 'true', store the results of the alias analysis as a PNG image." +
" Defaults to 'false'.")
private void setPrintOption(String argument) {
if (argument == null) {
return;
}
printOption = switch (argument.toLowerCase()) {
case "true", "source_location" -> PrintOption.SOURCE_LOCATION;
case "false", "none" -> PrintOption.NONE;
case "thread,source_location" -> PrintOption.THREAD_AND_SOURCE_LOCATION;
default -> null;
};
if (printOption == null) {
printOption = PrintOption.SOURCE_LOCATION;
logger.warn("Unknown option '{}={}', set to {}", ALIAS_GRAPHVIZ, argument, printOption);
}
}
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 Down Expand Up @@ -113,12 +115,8 @@ public boolean mayAlias(MemoryCoreEvent a, MemoryCoreEvent b) {
}
}

private void printGraph(Program program, Config configuration) {
if (configuration.printOption == PrintOption.NONE) {
return;
}

// Nodes are identified by thread and source location (if missing, event id).
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<>();
Expand Down Expand Up @@ -168,21 +166,19 @@ private void printGraph(Program program, Config configuration) {
}

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.printOption == PrintOption.THREAD_AND_SOURCE_LOCATION) {
return location == null ? null : "\"T" + event.getThread().getId() + esc(location) + "\"";
if (configuration.graphvizSplitByThread) {
return location != null ? "\"T" + event.getThread().getId() + esc(location) + "\"" :
"\"T" + event.getThread().getId() + "E" + event.getGlobalId() + "\"";
}
assert configuration.printOption == PrintOption.SOURCE_LOCATION;
return location == null ? null : "\"" + esc(location) + "\"";
return location != null ? "\"" + esc(location) + "\"" :
"\"E" + event.getGlobalId() + "\"";
}

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

enum PrintOption {
NONE,
SOURCE_LOCATION,
THREAD_AND_SOURCE_LOCATION,
}
}
6 changes: 3 additions & 3 deletions dartagnan/src/main/java/com/dat3m/dartagnan/utils/visualization/Graphviz.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -67,11 +67,11 @@ public Graphviz appendLine(String text) {
}

public Graphviz addEdge(String node1, String node2, String... options) {
String op = directed ? "->" : "--";
String edge = directed ? "->" : "--";
if (options == null) {
text.append(String.format("%s %s %s\n", node1, op, node2));
text.append(String.format("%s %s %s\n", node1, edge, node2));
} else {
text.append(String.format("%s %s %s [%s]\n", node1, op, node2, String.join(", ", options)));
text.append(String.format("%s %s %s [%s]\n", node1, edge, node2, String.join(", ", options)));
}
return this;
}
Expand Down

0 comments on commit d213871

Please sign in to comment.