Fix inclusion updates in IBPA (#694)

dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/alias/InclusionBasedPointerAnalysis.java

@@ -473,7 +473,11 @@ private Variable newVariable(String name) {
 
     // Inserts a single inclusion relationship into the graph.
     // Any cycle closed by this edge will eventually be detected and resolved.
-    private void addInclude(Variable variable, IncludeEdge edge) {
+    private void addInclude(Variable variable, IncludeEdge includeEdge) {
+        // accelerate for self-loops.
+        // this is necessary besides lazy cycle detection, because it handles cycles of length 1.
+        // LCD uses the edge that triggered the detection, which is not always the self-loop.
+        final IncludeEdge edge = tryAccelerate(variable, includeEdge);
         if (!addInto(variable.includes, edge, true)) {
             return;
         }
@@ -488,6 +492,13 @@ private void addInclude(Variable variable, IncludeEdge edge) {
         edges.add(edge);
     }
 
+    private IncludeEdge tryAccelerate(Variable variable, IncludeEdge edge) {
+        if (edge.source != variable) {
+            return edge;
+        }
+        return new IncludeEdge(edge.source, new Modifier(0, compose(edge.modifier.alignment, edge.modifier.offset)));
+    }
+
     // Tries to detect cycles when a new edge is to be added.
     // Called when a pointer propagates from variable to successor, due to an inclusion edge.
     private List<IncludeEdge> detectCycles(Variable variable, IncludeEdge edge) {
@@ -586,15 +597,15 @@ private boolean addInto(List<IncludeEdge> list, IncludeEdge element, boolean isG
         //NOTE The Stream API is too costly here
         for (final IncludeEdge o : list) {
             if (element.source.equals(o.source) && includes(o.modifier, element.modifier)) {
-                if(isGraphModification) {
+                if (isGraphModification) {
                     addIntoGraphFails++;
                 } else {
                     addIntoCyclesFails++;
                 }
                 return false;
             }
         }
-        if(isGraphModification) {
+        if (isGraphModification) {
             addIntoGraphSucceesses++;
         } else {
             addIntoCyclesSuccesses++;
@@ -691,7 +702,7 @@ private boolean includes(Modifier left, Modifier right) {
                     return false;
                 }
             }
-            return offset % alignment == 0;
+            return offset % alignment == 0 && offset >= 0;
         }
         // Case of multiple dynamic indexes with pairwise indivisible alignments.
         final int gcd = IntMath.gcd(reduceGCD(right.alignment), Math.abs(offset));