Skip to content

Commit

Permalink
Alias graph nodes are grouped by source location by default.
Browse files Browse the repository at this point in the history
  • Loading branch information
@xeren
xeren committed Jan 11, 2024
1 parent 85d64c6 commit 9caddfa
Show file tree
Hide file tree
Showing 2 changed files with 104 additions and 88 deletions.
104 changes: 104 additions & 0 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 @@ -4,13 +4,27 @@
import com.dat3m.dartagnan.configuration.Arch;
import com.dat3m.dartagnan.program.Program;
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 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.ALIAS_GRAPHVIZ;
import static com.dat3m.dartagnan.configuration.OptionNames.ALIAS_METHOD;

public interface AliasAnalysis {
Expand Down Expand Up @@ -51,6 +65,24 @@ 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." +
" Defaults to 'false'.")
private void setPrintOption(String argument) {
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 Config(Configuration config) throws InvalidConfigurationException {
config.inject(this);
}
Expand All @@ -77,4 +109,76 @@ 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).
// 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);
}

// Print 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();

// Print 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) {
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) + "\"";
}
assert configuration.printOption == PrintOption.SOURCE_LOCATION;
return location == null ? null : "\"" + esc(location) + "\"";
}

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

enum PrintOption {
NONE,
SOURCE_LOCATION,
THREAD_AND_SOURCE_LOCATION,
}
}
88 changes: 0 additions & 88 deletions ...gnan/src/main/java/com/dat3m/dartagnan/program/analysis/alias/FieldSensitiveAndersen.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -7,25 +7,15 @@
import com.dat3m.dartagnan.program.event.core.*;
import com.dat3m.dartagnan.program.event.core.threading.ThreadArgument;
import com.dat3m.dartagnan.program.event.core.utils.RegWriter;
import com.dat3m.dartagnan.program.event.metadata.SourceLocation;
import com.dat3m.dartagnan.program.memory.MemoryObject;
import com.dat3m.dartagnan.utils.visualization.Graphviz;
import com.google.common.collect.ImmutableSet;
import com.google.common.collect.Sets;
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 java.io.File;
import java.io.FileWriter;
import java.io.IOException;
import java.math.BigInteger;
import java.util.*;
import java.util.function.Function;

import static com.dat3m.dartagnan.GlobalSettings.getOutputDirectory;
import static com.dat3m.dartagnan.configuration.OptionNames.ALIAS_GRAPHVIZ;
import static com.dat3m.dartagnan.expression.op.IOpBin.*;
import static com.dat3m.dartagnan.expression.op.IOpUn.MINUS;
import static com.google.common.base.Preconditions.checkArgument;
Expand All @@ -45,14 +35,8 @@
* <p>
* Structures, that never occurs in any expression, are considered unreachable.
*/
@Options
public class FieldSensitiveAndersen implements AliasAnalysis {

@Option(name = ALIAS_GRAPHVIZ,
description = "If provided, the alias analysis produces a graphical representation of its initial state as a graphviz dot file." +
" If simply set to 'true', the generated files are stored in the output directory.")
private String graphPath;

///When a pointer set gains new content, it is added to this queue
private final LinkedHashSet<Object> variables = new LinkedHashSet<>();

Expand All @@ -70,9 +54,7 @@ public class FieldSensitiveAndersen implements AliasAnalysis {

public static FieldSensitiveAndersen fromConfig(Program program, Configuration config) throws InvalidConfigurationException {
var analysis = new FieldSensitiveAndersen();
config.inject(analysis);
analysis.run(program);
analysis.printGraph(program, FieldSensitiveAndersen::repr);
return analysis;
}

Expand Down Expand Up @@ -417,74 +399,4 @@ private void addAllAddresses(Object v, Collection<Location> s) {
private Set<Location> getAddresses(Object v) {
return addresses.getOrDefault(v, ImmutableSet.of());
}

private void printGraph(Program program, Function<MemoryCoreEvent, String> repr) {
if (graphPath == null) {
return;
}

// Nodes are identified by thread and source location (if missing, event id).
// A solid line marks the existence of events that must alias.
// A dashed line marks the existence of events that may alias.
final var graphviz = new Graphviz();

final Map<String, Set<String>> mayGraph = new HashMap<>();
final Map<String, Set<String>> mustGraph = new HashMap<>();
for (final MemoryCoreEvent event1 : eventAddressSpaceMap.keySet()) {
final String node1 = repr.apply(event1);
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 : eventAddressSpaceMap.keySet()) {
final String node2 = repr.apply(event2);
if (node2 != null && node1.compareTo(node2) < 0 && mayAlias(event1, event2)) {
(mustAlias(event1, event2) ? mustSet : maySet).add(node2);
}
}
maySet.removeAll(mustSet);
}

// Print the graphs
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();

// Print the .dot file and convert into the .png file.
File dotFile;
if ("true".equals(graphPath)) {
String programName = program.getName();
String programBase = programName.substring(0, programName.lastIndexOf('.'));
dotFile = new File(getOutputDirectory() + "/" + programBase + "-alias.dot");
} else {
dotFile = new File(graphPath);
}
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) {
final SourceLocation location = event.getMetadata(SourceLocation.class);
return event instanceof Init ? "\"" + event + "\"" :
"\"T" + event.getThread().getId() + (location != null ? esc(location) :
"E" + event.getGlobalId() + ": " + esc(event)) + "\"";
}

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

0 comments on commit 9caddfa

Please sign in to comment.