Review comments

hernanponcedeleon · Oct 2, 2024 · 22084a1 · 22084a1
1 parent 8b9d3d6
commit 22084a1
Show file tree

Hide file tree

Showing 5 changed files with 10 additions and 11 deletions.
diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/analysis/LazyRelationAnalysis.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/analysis/LazyRelationAnalysis.java
@@ -202,14 +202,11 @@ public RelationAnalysis.Knowledge visitControlDependency(DirectControlDependency
             Map<Event, Set<Event>> data = new HashMap<>();
             program.getThreads().forEach(t -> t.getEvents(CondJump.class).forEach(j -> {
                 if (!j.isGoto() && !j.isDead()) {
-                    ImmutableSet<Event> range = ((j instanceof IfAsJump ifJump)
+                    data.put(j, ((j instanceof IfAsJump ifJump)
                             ? ifJump.getBranchesEvents()
                             : j.getSuccessor().getSuccessors()).stream()
                             .filter(e -> !exec.areMutuallyExclusive(j, e))
-                            .collect(ImmutableSet.toImmutableSet());
-                    if (!range.isEmpty()) {
-                        data.put(j, range);
-                    }
+                            .collect(ImmutableSet.toImmutableSet()));
                 }
             }));
             ImmutableEventGraph must = new ImmutableMapEventGraph(data);
@@ -228,6 +225,7 @@ public RelationAnalysis.Knowledge visitAddressDependency(DirectAddressDependency
         @Override
         public RelationAnalysis.Knowledge visitInternalDataDependency(DirectDataDependency definition) {
             long start = System.currentTimeMillis();
+            // FIXME: Our "internal data dependency" relation is quite odd an contains all but address dependencies.
             EventGraph must = computeInternalDependencies(EnumSet.of(DATA, CTRL, OTHER));
             time(definition, start, System.currentTimeMillis());
             return new RelationAnalysis.Knowledge(must, must);
@@ -240,6 +238,8 @@ private EventGraph computeInternalDependencies(Set<Register.UsageType> usageType
                 reader.getRegisterReads().forEach(read -> {
                     if (usageTypes.contains(read.usageType())) {
                         Register register = read.register();
+                        // TODO: Update after this is merged
+                        //  https://github.com/hernanponcedeleon/Dat3M/pull/741
                         // Register x0 is hardwired to the constant 0 in RISCV
                         // https://en.wikichip.org/wiki/risc-v/registers,
                         // and thus it generates no dependency, see

diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/analysis/NativeRelationAnalysis.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/analysis/NativeRelationAnalysis.java
@@ -915,6 +915,8 @@ private MutableKnowledge computeInternalDependencies(Set<UsageType> usageTypes)
                         continue;
                     }
                     final Register register = regRead.register();
+                    // TODO: Update after this is merged
+                    //  https://github.com/hernanponcedeleon/Dat3M/pull/741
                     // Register x0 is hardwired to the constant 0 in RISCV
                     // https://en.wikichip.org/wiki/risc-v/registers,
                     // and thus it generates no dependency, see

diff --git a/...n/src/main/java/com/dat3m/dartagnan/wmm/utils/graph/immutable/ImmutableMapEventGraph.java b/...n/src/main/java/com/dat3m/dartagnan/wmm/utils/graph/immutable/ImmutableMapEventGraph.java
@@ -28,9 +28,7 @@ private ImmutableMapEventGraph(Map<Event, Set<Event>> data, int size) {
                 .filter(e -> !e.getValue().isEmpty())
                 .collect(ImmutableMap.toImmutableMap(
                         Map.Entry::getKey,
-                        entry -> entry.getValue() instanceof ImmutableSet
-                                ? entry.getValue()
-                                : ImmutableSet.copyOf(entry.getValue())));
+                        entry -> ImmutableSet.copyOf(entry.getValue())));
         this.size = size;
     }
 

diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/utils/graph/immutable/LazyEventGraph.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/utils/graph/immutable/LazyEventGraph.java
@@ -41,7 +41,7 @@ public int size() {
         if (size == -1) {
             size = domain.stream()
                     .map(e1 -> range.stream().filter(e2 -> function.test(e1, e2)).count())
-                    .map(s -> Integer.parseInt(s.toString()))
+                    .map(Math::toIntExact)
                     .reduce(0, Integer::sum);
         }
         return size;

diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/encoding/RelationAnalysisTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/encoding/RelationAnalysisTest.java
@@ -113,8 +113,7 @@ private List<String> listFiles(Path path) throws IOException {
                     result.addAll(listFiles(file.toAbsolutePath()));
                 } else {
                     String filePath = file.toAbsolutePath().toString();
-                    if (filePath.endsWith(".litmus") || filePath.endsWith(".ll") ||
-                            filePath.endsWith(".c") || filePath.endsWith(".spv.dis")) {
+                    if (filePath.endsWith(".litmus") || filePath.endsWith(".ll") || filePath.endsWith(".spv.dis")) {
                         result.add(filePath);
                     }
                 }