Add loop bound annotation (#687)

Signed-off-by: Hernan Ponce de Leon <[email protected]>
Co-authored-by: Hernan Ponce de Leon <[email protected]>
Co-authored-by: Thomas Haas <[email protected]>

benchmarks/c/miscellaneous/staticLoops.c

@@ -0,0 +1,22 @@
+#include <stdint.h>
+#include <assert.h>
+
+#define INCS 3
+
+volatile int32_t x = 0;
+
+int main()
+{
+    for (int i = 0; i < INCS; i++)
+        x++;
+
+    for (int i = -1; i < INCS-1; i++)
+        x++;
+
+    for (int i = 1; i < INCS+1; i++)
+        x++;
+
+	assert(x == 3*INCS);
+
+	return 0;
+}

dartagnan/src/main/java/com/dat3m/dartagnan/expression/integers/IntCmpOp.java

@@ -2,8 +2,6 @@
 
 import com.dat3m.dartagnan.expression.ExpressionKind;
 
-import java.math.BigInteger;
-
 public enum IntCmpOp implements ExpressionKind {
     EQ, NEQ, GTE, LTE, GT, LT, UGTE, ULTE, UGT, ULT;
 
@@ -67,14 +65,10 @@ public boolean isStrict() {
         };
     }
 
-    public boolean combine(BigInteger a, BigInteger b){
+    public boolean isLessCategory() {
         return switch (this) {
-            case EQ -> a.compareTo(b) == 0;
-            case NEQ -> a.compareTo(b) != 0;
-            case LT, ULT -> a.compareTo(b) < 0;
-            case LTE, ULTE -> a.compareTo(b) <= 0;
-            case GT, UGT -> a.compareTo(b) > 0;
-            case GTE, UGTE -> a.compareTo(b) >= 0;
+            case LT, LTE, ULTE, ULT -> true;
+            default -> false;
         };
     }
 

dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/LiveRegistersAnalysis.java

@@ -0,0 +1,139 @@
+package com.dat3m.dartagnan.program.analysis;
+
+import com.dat3m.dartagnan.program.Function;
+import com.dat3m.dartagnan.program.IRHelper;
+import com.dat3m.dartagnan.program.Register;
+import com.dat3m.dartagnan.program.event.Event;
+import com.dat3m.dartagnan.program.event.RegReader;
+import com.dat3m.dartagnan.program.event.RegWriter;
+import com.dat3m.dartagnan.program.event.core.CondJump;
+import com.dat3m.dartagnan.program.event.core.Label;
+import com.dat3m.dartagnan.program.event.functions.AbortIf;
+import com.dat3m.dartagnan.program.event.functions.Return;
+import com.google.common.collect.ImmutableSet;
+
+import java.util.HashMap;
+import java.util.HashSet;
+import java.util.Map;
+import java.util.Set;
+
+/*
+    Computes the registers that are (potentially) live at every program point.
+    A register is live, if it is used (i.e., read from) before getting overwritten.
+    A register may be declared live even if it is not used, however, a non-live (dead) register is always guaranteed
+    to be overwritten.
+
+    This is a backwards analysis: the control-flow is traversed from exit to beginning.
+ */
+public class LiveRegistersAnalysis {
+
+    private final Map<Event, Set<Register>> liveRegistersMap = new HashMap<>();
+
+    public static LiveRegistersAnalysis forFunction(Function f) {
+        final LiveRegistersAnalysis analysis = new LiveRegistersAnalysis();
+        analysis.computeForFunction(f);
+        return analysis;
+    }
+
+    public Set<Register> getLiveRegistersAt(Event ev) {
+        return liveRegistersMap.getOrDefault(ev, Set.of());
+    }
+
+    // ======================================================================
+
+    private void computeForFunction(Function f) {
+        computeLiveRegisters(f, computeLiveRegistersAtJumps(f));
+    }
+
+    private void computeLiveRegisters(Function f, Map<CondJump, Set<Register>> liveRegsAtJump) {
+
+        Set<Register> liveRegs = new HashSet<>();
+        // The copy is an optimizations: multiple events may have the same set of live registers,
+        // so we try to reuse that set to save memory.
+        Set<Register> liveRegsCopy = ImmutableSet.copyOf(liveRegs);
+        Event cur = f.getExit();
+        while (cur != null) {
+            boolean updated;
+            if (cur instanceof CondJump jump) {
+                liveRegs = liveRegsAtJump.get(jump);
+                updated = true;
+            } else {
+                updated = updateLiveRegs(cur, liveRegs);
+            }
+
+            if (updated) {
+                liveRegsCopy = ImmutableSet.copyOf(liveRegs);
+            }
+            liveRegistersMap.put(cur, liveRegsCopy);
+
+            cur = cur.getPredecessor();
+        }
+    }
+
+    private static Map<CondJump, Set<Register>> computeLiveRegistersAtJumps(Function f) {
+        Map<CondJump, Set<Register>> liveRegsAtJumpMap = new HashMap<>();
+        Set<Register> liveRegs = new HashSet<>();
+        Event cur = f.getExit();
+        while (cur != null) {
+
+            updateLiveRegs(cur, liveRegs);
+
+            if (cur instanceof CondJump jump) {
+                final Set<Register> liveRegsAtJump = liveRegsAtJumpMap.computeIfAbsent(jump, key -> new HashSet<>());
+                if (!IRHelper.isAlwaysBranching(jump)) {
+                    liveRegsAtJump.addAll(liveRegs);
+                }
+                liveRegs = new HashSet<>(liveRegsAtJump);
+            }
+
+            if (cur instanceof Label label) {
+                // Propagate live sets to all incoming jumps. If an incoming jump is a backjump,
+                // we have a loop and may need to re-traverse the loop with the propagated values.
+                CondJump latestUpdatedBackjump = null;
+                for (CondJump jump : label.getJumpSet()) {
+                    if (jump.isDead()) {
+                        continue;
+                    }
+
+                    final Set<Register> liveRegsAtJump = liveRegsAtJumpMap.computeIfAbsent(jump, key -> new HashSet<>());
+                    if (liveRegsAtJump.addAll(liveRegs) && jump.getGlobalId() > label.getGlobalId()) {
+                        if (latestUpdatedBackjump == null || jump.getGlobalId() > latestUpdatedBackjump.getGlobalId()) {
+                            latestUpdatedBackjump = jump;
+                        }
+                    }
+                }
+
+                if (latestUpdatedBackjump != null) {
+                    cur = latestUpdatedBackjump;
+                    continue;
+                }
+            }
+
+            cur = cur.getPredecessor();
+        }
+
+        return liveRegsAtJumpMap;
+    }
+
+    // Returns true if the live registers may have updated (may return true even if no actual update happened).
+    private static boolean updateLiveRegs(Event ev, Set<Register> liveRegs) {
+        boolean changed = false;
+        if ((ev instanceof AbortIf || ev instanceof Return) && IRHelper.isAlwaysBranching(ev)) {
+            liveRegs.clear();
+            changed = true;
+        }
+
+        if (ev instanceof RegWriter writer && writer.cfImpliesExec()) {
+            changed |= liveRegs.remove(writer.getResultRegister());
+        }
+
+        if (ev instanceof RegReader reader) {
+            changed |= reader.getRegisterReads().stream()
+                    .map(read -> liveRegs.add(read.register()))
+                    .reduce(false, (res, b) -> res || b);
+        }
+
+        return changed;
+
+    }
+}

dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/UseDefAnalysis.java

@@ -0,0 +1,146 @@
+package com.dat3m.dartagnan.program.analysis;
+
+import com.dat3m.dartagnan.program.Function;
+import com.dat3m.dartagnan.program.IRHelper;
+import com.dat3m.dartagnan.program.Register;
+import com.dat3m.dartagnan.program.event.Event;
+import com.dat3m.dartagnan.program.event.RegReader;
+import com.dat3m.dartagnan.program.event.RegWriter;
+import com.dat3m.dartagnan.program.event.core.CondJump;
+import com.dat3m.dartagnan.program.event.core.Label;
+
+import java.util.HashMap;
+import java.util.HashSet;
+import java.util.Map;
+import java.util.Set;
+
+/*
+    This analysis computes the Use-Def graph of a function.
+    The Use-Def graph connects a RegReader with possible RegWriters from which it could take its value
+    (for each register read by the reader).
+
+    FIXME: The analysis currently cannot capture if a register is possibly uninitialized.
+     In particular, if the Def set consists of a single writer,
+     then it does not necessarily mean that the writer is the only one (maybe an uninitialized read is also possible).
+
+     NOTE: This analysis is essentially the same as the "Dependency" analysis we already have.
+     The main difference is that this analysis works independently of other analyses
+     (e.g., it does not depend on ExecutionAnalysis) and can be used on single functions.
+ */
+public class UseDefAnalysis {
+
+    private Map<RegReader, Map<Register, Set<RegWriter>>> useDefGraph;
+
+    private UseDefAnalysis() { }
+
+    public static UseDefAnalysis forFunction(Function function) {
+        final UseDefAnalysis useDefAnalysis = new UseDefAnalysis();
+        useDefAnalysis.computeForFunction(function);
+        return useDefAnalysis;
+    }
+
+    public Map<Register, Set<RegWriter>> getDefs(Event regReader) {
+        return useDefGraph.getOrDefault(regReader, Map.of());
+    }
+
+    public Set<RegWriter> getDefs(Event regReader, Register register) {
+        return getDefs(regReader).getOrDefault(register, Set.of());
+    }
+
+    // ======================================================================
+
+    private void computeForFunction(Function function) {
+        final Map<Label, Map<Register, Set<RegWriter>>> reachingDefinitionsMap = computeReachingDefinitionsAtLabels(function);
+        this.useDefGraph = computeUseDefGraph(function, reachingDefinitionsMap);
+    }
+
+    private Map<RegReader, Map<Register, Set<RegWriter>>> computeUseDefGraph(
+            Function function, Map<Label, Map<Register, Set<RegWriter>>> reachingDefinitionsMap
+    ) {
+        final Map<RegReader, Map<Register, Set<RegWriter>>> useDefGraph = new HashMap<>();
+
+        Map<Register, Set<RegWriter>> reachingDefinitions = new HashMap<>();
+        for (Event e : function.getEvents()) {
+            if (e instanceof RegReader reader) {
+                // Project reachable definitions down to those relevant for the RegReader
+                final Map<Register, Set<RegWriter>> readableDefinitions = new HashMap<>();
+                for (Register.Read read : reader.getRegisterReads()) {
+                    readableDefinitions.put(read.register(), reachingDefinitions.get(read.register()));
+                }
+                useDefGraph.put(reader, readableDefinitions);
+            }
+
+            updateReachingDefinitions(e, reachingDefinitions);
+
+            if (e instanceof Label label) {
+                // This will cause entries in "reachingDefinitionsMap" to get mutated,
+                // but that is fine because we do not need them anymore.
+                reachingDefinitions = reachingDefinitionsMap.get(label);
+            }
+        }
+
+        return useDefGraph;
+    }
+
+    // For efficiency reasons, we compute reaching definitions only for labels.
+    // TODO: Maybe add a cheap liveness analysis and restrict to only live definitions.
+    private Map<Label, Map<Register, Set<RegWriter>>> computeReachingDefinitionsAtLabels(Function function) {
+        final Map<Label, Map<Register, Set<RegWriter>>> reachingDefinitionsMap = new HashMap<>();
+
+        Event cur = function.getEntry();
+        Map<Register, Set<RegWriter>> reachingDefinitions = new HashMap<>();
+        while (cur != null) {
+            updateReachingDefinitions(cur, reachingDefinitions);
+
+            if (cur instanceof CondJump jump && !jump.isDead()) {
+                final Map<Register, Set<RegWriter>> reachDefAtLabel = reachingDefinitionsMap.computeIfAbsent(jump.getLabel(), k -> new HashMap<>());
+                final boolean wasUpdated = joinInto(reachDefAtLabel, reachingDefinitions);
+                final boolean isBackJump = jump.getLabel().getGlobalId() < jump.getGlobalId();
+                if (wasUpdated && isBackJump) {
+                    cur = jump.getLabel();
+                    continue;
+                }
+            }
+
+            if (cur instanceof Label label) {
+                final Map<Register, Set<RegWriter>> reachDefAtLabel = reachingDefinitionsMap.computeIfAbsent(label, k -> new HashMap<>());
+                if (!IRHelper.isAlwaysBranching(label.getPredecessor())) {
+                    joinInto(reachDefAtLabel, reachingDefinitions);
+                }
+                reachingDefinitions = copy(reachDefAtLabel);
+            }
+
+            cur = cur.getSuccessor();
+        }
+
+        return reachingDefinitionsMap;
+    }
+
+    private void updateReachingDefinitions(Event ev, Map<Register, Set<RegWriter>> reachingDefinitions) {
+        if (ev instanceof RegWriter writer) {
+            if (writer.cfImpliesExec()) {
+                reachingDefinitions.put(writer.getResultRegister(), new HashSet<>(Set.of(writer)));
+            } else {
+                reachingDefinitions.computeIfAbsent(writer.getResultRegister(), k -> new HashSet<>()).add(writer);
+            }
+        }
+    }
+
+    private boolean joinInto(Map<Register, Set<RegWriter>> base, Map<Register, Set<RegWriter>> toJoin) {
+        boolean changed = false;
+        for (Map.Entry<Register, Set<RegWriter>> entry : toJoin.entrySet()) {
+            if (!base.containsKey(entry.getKey())) {
+                changed = true;
+            }
+            changed |= base.computeIfAbsent(entry.getKey(), k -> new HashSet<>()).addAll(entry.getValue());
+        }
+
+        return changed;
+    }
+
+    private Map<Register, Set<RegWriter>> copy(Map<Register, Set<RegWriter>> source) {
+        final Map<Register, Set<RegWriter>> copy = new HashMap<>(source.size() * 4 / 3);
+        source.forEach((reg, writers) -> copy.put(reg, new HashSet<>(writers)));
+        return copy;
+    }
+}