From 71026bef4e58759f6fb1d63a9558e9b1ad995f9f Mon Sep 17 00:00:00 2001 From: Hernan Ponce de Leon Date: Tue, 2 Jul 2024 15:32:09 +0200 Subject: [PATCH] Add loop bound annotation (#687) Signed-off-by: Hernan Ponce de Leon Co-authored-by: Hernan Ponce de Leon Co-authored-by: Thomas Haas --- benchmarks/c/miscellaneous/staticLoops.c | 22 ++ .../expression/integers/IntCmpOp.java | 12 +- .../analysis/LiveRegistersAnalysis.java | 139 ++++++++++++ .../program/analysis/UseDefAnalysis.java | 146 ++++++++++++ .../processing/NaiveLoopBoundAnnotation.java | 208 ++++++++++++++++++ .../program/processing/ProcessingManager.java | 5 +- .../dat3m/dartagnan/c/MiscellaneousTest.java | 1 + .../resources/miscellaneous/staticLoops.ll | 181 +++++++++++++++ 8 files changed, 702 insertions(+), 12 deletions(-) create mode 100644 benchmarks/c/miscellaneous/staticLoops.c create mode 100644 dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/LiveRegistersAnalysis.java create mode 100644 dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/UseDefAnalysis.java create mode 100644 dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/NaiveLoopBoundAnnotation.java create mode 100644 dartagnan/src/test/resources/miscellaneous/staticLoops.ll diff --git a/benchmarks/c/miscellaneous/staticLoops.c b/benchmarks/c/miscellaneous/staticLoops.c new file mode 100644 index 0000000000..7e4f2591ae --- /dev/null +++ b/benchmarks/c/miscellaneous/staticLoops.c @@ -0,0 +1,22 @@ +#include +#include + +#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; +} diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/expression/integers/IntCmpOp.java b/dartagnan/src/main/java/com/dat3m/dartagnan/expression/integers/IntCmpOp.java index d1b411f903..e694717f6b 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/expression/integers/IntCmpOp.java +++ b/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; }; } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/LiveRegistersAnalysis.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/LiveRegistersAnalysis.java new file mode 100644 index 0000000000..5d3356845d --- /dev/null +++ b/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> liveRegistersMap = new HashMap<>(); + + public static LiveRegistersAnalysis forFunction(Function f) { + final LiveRegistersAnalysis analysis = new LiveRegistersAnalysis(); + analysis.computeForFunction(f); + return analysis; + } + + public Set getLiveRegistersAt(Event ev) { + return liveRegistersMap.getOrDefault(ev, Set.of()); + } + + // ====================================================================== + + private void computeForFunction(Function f) { + computeLiveRegisters(f, computeLiveRegistersAtJumps(f)); + } + + private void computeLiveRegisters(Function f, Map> liveRegsAtJump) { + + Set 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 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> computeLiveRegistersAtJumps(Function f) { + Map> liveRegsAtJumpMap = new HashMap<>(); + Set liveRegs = new HashSet<>(); + Event cur = f.getExit(); + while (cur != null) { + + updateLiveRegs(cur, liveRegs); + + if (cur instanceof CondJump jump) { + final Set 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 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 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; + + } +} diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/UseDefAnalysis.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/UseDefAnalysis.java new file mode 100644 index 0000000000..af83d85a66 --- /dev/null +++ b/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>> useDefGraph; + + private UseDefAnalysis() { } + + public static UseDefAnalysis forFunction(Function function) { + final UseDefAnalysis useDefAnalysis = new UseDefAnalysis(); + useDefAnalysis.computeForFunction(function); + return useDefAnalysis; + } + + public Map> getDefs(Event regReader) { + return useDefGraph.getOrDefault(regReader, Map.of()); + } + + public Set getDefs(Event regReader, Register register) { + return getDefs(regReader).getOrDefault(register, Set.of()); + } + + // ====================================================================== + + private void computeForFunction(Function function) { + final Map>> reachingDefinitionsMap = computeReachingDefinitionsAtLabels(function); + this.useDefGraph = computeUseDefGraph(function, reachingDefinitionsMap); + } + + private Map>> computeUseDefGraph( + Function function, Map>> reachingDefinitionsMap + ) { + final Map>> useDefGraph = new HashMap<>(); + + Map> 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> 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>> computeReachingDefinitionsAtLabels(Function function) { + final Map>> reachingDefinitionsMap = new HashMap<>(); + + Event cur = function.getEntry(); + Map> reachingDefinitions = new HashMap<>(); + while (cur != null) { + updateReachingDefinitions(cur, reachingDefinitions); + + if (cur instanceof CondJump jump && !jump.isDead()) { + final Map> 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> 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> 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> base, Map> toJoin) { + boolean changed = false; + for (Map.Entry> 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> copy(Map> source) { + final Map> copy = new HashMap<>(source.size() * 4 / 3); + source.forEach((reg, writers) -> copy.put(reg, new HashSet<>(writers))); + return copy; + } +} diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/NaiveLoopBoundAnnotation.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/NaiveLoopBoundAnnotation.java new file mode 100644 index 0000000000..a558858f51 --- /dev/null +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/NaiveLoopBoundAnnotation.java @@ -0,0 +1,208 @@ +package com.dat3m.dartagnan.program.processing; + +import com.dat3m.dartagnan.expression.Expression; +import com.dat3m.dartagnan.expression.ExpressionFactory; +import com.dat3m.dartagnan.expression.integers.*; +import com.dat3m.dartagnan.expression.misc.ITEExpr; +import com.dat3m.dartagnan.program.Function; +import com.dat3m.dartagnan.program.Register; +import com.dat3m.dartagnan.program.analysis.DominatorAnalysis; +import com.dat3m.dartagnan.program.analysis.LiveRegistersAnalysis; +import com.dat3m.dartagnan.program.analysis.LoopAnalysis; +import com.dat3m.dartagnan.program.analysis.UseDefAnalysis; +import com.dat3m.dartagnan.program.event.Event; +import com.dat3m.dartagnan.program.event.EventFactory; +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.core.Local; +import com.dat3m.dartagnan.utils.DominatorTree; + +import java.util.List; +import java.util.Set; + +/* + This pass adds a loop bound annotation to static loops of the form + + for (int i = I; i preDominatorTree = DominatorAnalysis.computePreDominatorTree(function.getEntry(), function.getExit()); + final List loops = LoopAnalysis.onFunction(function).getLoopsOfFunction(function); + + for (LoopAnalysis.LoopInfo loop : loops) { + final List loopBody = loop.iterations().get(0).computeBody(); + final Label label = (Label) loopBody.get(0); + final Event backJump = loopBody.get(loopBody.size() - 1); + + // Find candidate for loop counter register. We check for the shape: + // loopCounter <- constant + // loopHeader: + // The loop header should be dominated by the constant assignment to the counter. + if (!(label.getPredecessor() instanceof Local init && init.getExpr() instanceof IntLiteral initValExpr + && preDominatorTree.isDominatedBy(label, init))) { + continue; + } + final Register counterReg = init.getResultRegister(); + + // Validate that we indeed have found the counter register. + final boolean counterIsLive = liveAnalysis.getLiveRegistersAt(label).contains(counterReg); + final Event loopCountInc = findUniqueIncrement(loopBody, counterReg, useDefAnalysis, preDominatorTree); + final boolean counterIsAlwaysIncremented = + (loopCountInc != null) && preDominatorTree.isDominatedBy(backJump, loopCountInc); + if (!(counterIsLive && counterIsAlwaysIncremented)) { + // The candidate counter is either not the true loop counter, or + // the counter computations are too complex to analyze. + continue; + } + + // Now we look for the loop exit condition. + // (1) Find all exiting jumps + final List exitingJumps = loopBody.stream().filter(e -> e instanceof CondJump jump && + jump.getLabel().getLocalId() > backJump.getLocalId()).map(CondJump.class::cast).toList(); + + // (2) Check for each exit whether it is related to the counter variable. + // If so, try to deduce a loop bound and annotate the loop. + for (CondJump exit : exitingJumps) { + // We check for the special shape: + // if (notExit) goto L; + // goto exit; + if (!(exit.isGoto() && exit.getPredecessor() instanceof CondJump jump)) { + continue; + } + final Expression negatedGuard = jump.getGuard(); + // Now we check for the guard shape "r != 0" (i.e., we exit when r == 0 due to the inversion). + if (!(negatedGuard instanceof IntCmpExpr cond + && cond.getLeft() instanceof Register r + && cond.getKind() == IntCmpOp.NEQ + && cond.getRight() instanceof IntLiteral c && c.isZero())) { + continue; + } + // Now we need to check if r is actually related to the loop counter + // Check if there is a unique ITE defining the r from above and bounding the loop. + final Expression boundExpr = computeLoopBound(loopBody, r, counterReg, + initValExpr.getValueAsInt(), useDefAnalysis, preDominatorTree); + if (boundExpr != null) { + label.getPredecessor().insertAfter(EventFactory.Svcomp.newLoopBound(boundExpr)); + break; + } + } + } + } + + // Check if there is a single increment to the register. + // If there is, it returns the event performing the increment, otherwise it returns null. + private Event findUniqueIncrement(List events, Register register, + UseDefAnalysis useDefAnalysis, DominatorTree preDominatorTree) { + final RegWriter source = findUniqueSource(events, register, useDefAnalysis, preDominatorTree); + if (source == null) { + return null; + } + // We found the non-trivial source. Check that this is indeed the desired increment: + // (1) It is an addition operation + if (!(source instanceof Local local && local.getExpr() instanceof IntBinaryExpr add && add.getKind() == IntBinaryOp.ADD)) { + return null; + } + // (2) The addition is a positive increment of the register. + if (!(add.getLeft().equals(register) && add.getRight() instanceof IntLiteral c && c.getValue().signum() > 0)) { + return null; + } + // TODO: return also the increment + return local; + } + + private Expression computeLoopBound(List events, Register exitReg, Register counterReg, int counterRegInitVal, + UseDefAnalysis useDefAnalysis, DominatorTree preDominatorTree) { + + final RegWriter exitSource = findUniqueSource(events, exitReg, useDefAnalysis, preDominatorTree); + if (exitSource == null) { + return null; + } + + // If the non-trivial assignment has the shape exitCond <- ITE(counter <(=) C, 1, 0), we are done + if (!(exitSource instanceof Local local && local.getExpr() instanceof ITEExpr iteExpr + && iteExpr.getCondition() instanceof IntCmpExpr cond + && cond.getLeft().equals(counterReg) + && cond.getKind().isLessCategory() + && cond.getRight() instanceof IntLiteral bound + && iteExpr.getTrueCase() instanceof IntLiteral one && one.isOne() + && iteExpr.getFalseCase() instanceof IntLiteral zero && zero.isZero())) { + return null; + } + // We use C-I+1 for counter < C and C-I+2 for counter <= C + final ExpressionFactory expressions = ExpressionFactory.getInstance(); + final int loopIterations = bound.getValueAsInt() - counterRegInitVal + (cond.getKind().isStrict() ? 1 : 2); + return expressions.makeValue(loopIterations, bound.getType()); + + } + + // Finds the unique non-trivial assignment that (possibly indirectly) provides the value of + // Returns NULL, if no such unique assignment exists. + private RegWriter findUniqueSource(List events, Register register, UseDefAnalysis useDefAnalysis, DominatorTree preDominatorTree) { + final List writers = events.stream() + .filter(e -> e instanceof RegWriter writer && writer.getResultRegister().equals(register)) + .map(RegWriter.class::cast).toList(); + + if (writers.size() != 1 || !(writers.get(0) instanceof Local assignment)) { + // There is no unique writer, or the unique writer is not a simple assignment. + return null; + } + // Since the assignment may go over several trivial copy assignments, we need to traverse + // the UseDef-chain until we find a non-trivial assignment. + final RegWriter source = chaseUseDefChain(assignment, useDefAnalysis, preDominatorTree); + if (!events.contains(source)) { + // For the edge case where the source is outside the provided events. + return null; + } + return source; + } + + private RegWriter chaseUseDefChain(RegWriter assignment, UseDefAnalysis useDefAnalysis, DominatorTree preDominatorTree) { + RegWriter cur = assignment; + while (cur instanceof Local loc && loc.getExpr() instanceof Register reg) { + final Set defs = useDefAnalysis.getDefs(loc, reg); + if (defs.size() != 1) { + // Multiple assignments (or none): too complex so give up. + return null; + } + final RegWriter def = defs.iterator().next(); + if (!preDominatorTree.isDominatedBy(cur, def)) { + // Sanity check that the only def is also dominating its use. + // This might not be true if there are accesses to uninitialized registers. + return null; + } + cur = def; + } + return cur; + } +} diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/ProcessingManager.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/ProcessingManager.java index b9b6d1fd8d..3ba67f144d 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/ProcessingManager.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/ProcessingManager.java @@ -85,9 +85,7 @@ private ProcessingManager(Configuration config) throws InvalidConfigurationExcep final FunctionProcessor removeDeadJumps = RemoveDeadCondJumps.fromConfig(config); programProcessors.addAll(Arrays.asList( printBeforeProcessing ? DebugPrint.withHeader("Before processing", Printer.Mode.ALL) : null, - ProgramProcessor.fromFunctionProcessor( - NormalizeLoops.newInstance(), Target.FUNCTIONS, true - ), + ProgramProcessor.fromFunctionProcessor(NormalizeLoops.newInstance(), Target.FUNCTIONS, true), intrinsics.markIntrinsicsPass(), GEPToAddition.newInstance(), NaiveDevirtualisation.newInstance(), @@ -110,6 +108,7 @@ private ProcessingManager(Configuration config) throws InvalidConfigurationExcep ProgramProcessor.fromFunctionProcessor(MemToReg.fromConfig(config), Target.FUNCTIONS, true), ProgramProcessor.fromFunctionProcessor(sccp, Target.FUNCTIONS, false), dynamicSpinLoopDetection ? DynamicSpinLoopDetection.fromConfig(config) : null, + ProgramProcessor.fromFunctionProcessor(NaiveLoopBoundAnnotation.newInstance(), Target.FUNCTIONS, true), LoopUnrolling.fromConfig(config), // We keep unrolling global for now printAfterUnrolling ? DebugPrint.withHeader("After loop unrolling", Printer.Mode.ALL) : null, ProgramProcessor.fromFunctionProcessor( diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/c/MiscellaneousTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/c/MiscellaneousTest.java index 2b8a304440..20dc4de093 100644 --- a/dartagnan/src/test/java/com/dat3m/dartagnan/c/MiscellaneousTest.java +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/c/MiscellaneousTest.java @@ -87,6 +87,7 @@ public static Iterable data() throws IOException { {"uninitRead", IMM, FAIL, 1}, {"multipleBackJumps", IMM, UNKNOWN, 1}, {"memcpy_s", IMM, PASS, 1}, + {"staticLoops", IMM, PASS, 1}, {"offsetof", IMM, PASS, 1}, {"ctlz", IMM, PASS, 1}, {"cttz", IMM, PASS, 1} diff --git a/dartagnan/src/test/resources/miscellaneous/staticLoops.ll b/dartagnan/src/test/resources/miscellaneous/staticLoops.ll new file mode 100644 index 0000000000..8d4a6f3e08 --- /dev/null +++ b/dartagnan/src/test/resources/miscellaneous/staticLoops.ll @@ -0,0 +1,181 @@ +; ModuleID = '/home/ponce/git/Dat3M/output/staticLoops.ll' +source_filename = "/home/ponce/git/Dat3M/benchmarks/c/miscellaneous/staticLoops.c" +target datalayout = "e-m:e-p270:32:32-p271:32:32-p272:64:64-i64:64-f80:128-n8:16:32:64-S128" +target triple = "x86_64-pc-linux-gnu" + +@x = dso_local global i32 0, align 4, !dbg !0 +@.str = private unnamed_addr constant [12 x i8] c"x == 3*INCS\00", align 1 +@.str.1 = private unnamed_addr constant [63 x i8] c"/home/ponce/git/Dat3M/benchmarks/c/miscellaneous/staticLoops.c\00", align 1 +@__PRETTY_FUNCTION__.main = private unnamed_addr constant [11 x i8] c"int main()\00", align 1 + +; Function Attrs: noinline nounwind uwtable +define dso_local i32 @main() #0 !dbg !17 { + %1 = alloca i32, align 4 + %2 = alloca i32, align 4 + %3 = alloca i32, align 4 + %4 = alloca i32, align 4 + store i32 0, i32* %1, align 4 + call void @llvm.dbg.declare(metadata i32* %2, metadata !20, metadata !DIExpression()), !dbg !22 + store i32 0, i32* %2, align 4, !dbg !22 + br label %5, !dbg !23 + +5: ; preds = %11, %0 + %6 = load i32, i32* %2, align 4, !dbg !24 + %7 = icmp slt i32 %6, 3, !dbg !26 + br i1 %7, label %8, label %14, !dbg !27 + +8: ; preds = %5 + %9 = load volatile i32, i32* @x, align 4, !dbg !28 + %10 = add nsw i32 %9, 1, !dbg !28 + store volatile i32 %10, i32* @x, align 4, !dbg !28 + br label %11, !dbg !29 + +11: ; preds = %8 + %12 = load i32, i32* %2, align 4, !dbg !30 + %13 = add nsw i32 %12, 1, !dbg !30 + store i32 %13, i32* %2, align 4, !dbg !30 + br label %5, !dbg !31, !llvm.loop !32 + +14: ; preds = %5 + call void @llvm.dbg.declare(metadata i32* %3, metadata !35, metadata !DIExpression()), !dbg !37 + store i32 -1, i32* %3, align 4, !dbg !37 + br label %15, !dbg !38 + +15: ; preds = %21, %14 + %16 = load i32, i32* %3, align 4, !dbg !39 + %17 = icmp slt i32 %16, 2, !dbg !41 + br i1 %17, label %18, label %24, !dbg !42 + +18: ; preds = %15 + %19 = load volatile i32, i32* @x, align 4, !dbg !43 + %20 = add nsw i32 %19, 1, !dbg !43 + store volatile i32 %20, i32* @x, align 4, !dbg !43 + br label %21, !dbg !44 + +21: ; preds = %18 + %22 = load i32, i32* %3, align 4, !dbg !45 + %23 = add nsw i32 %22, 1, !dbg !45 + store i32 %23, i32* %3, align 4, !dbg !45 + br label %15, !dbg !46, !llvm.loop !47 + +24: ; preds = %15 + call void @llvm.dbg.declare(metadata i32* %4, metadata !49, metadata !DIExpression()), !dbg !51 + store i32 1, i32* %4, align 4, !dbg !51 + br label %25, !dbg !52 + +25: ; preds = %31, %24 + %26 = load i32, i32* %4, align 4, !dbg !53 + %27 = icmp slt i32 %26, 4, !dbg !55 + br i1 %27, label %28, label %34, !dbg !56 + +28: ; preds = %25 + %29 = load volatile i32, i32* @x, align 4, !dbg !57 + %30 = add nsw i32 %29, 1, !dbg !57 + store volatile i32 %30, i32* @x, align 4, !dbg !57 + br label %31, !dbg !58 + +31: ; preds = %28 + %32 = load i32, i32* %4, align 4, !dbg !59 + %33 = add nsw i32 %32, 1, !dbg !59 + store i32 %33, i32* %4, align 4, !dbg !59 + br label %25, !dbg !60, !llvm.loop !61 + +34: ; preds = %25 + %35 = load volatile i32, i32* @x, align 4, !dbg !63 + %36 = icmp eq i32 %35, 9, !dbg !63 + br i1 %36, label %37, label %38, !dbg !66 + +37: ; preds = %34 + br label %39, !dbg !66 + +38: ; preds = %34 + call void @__assert_fail(i8* getelementptr inbounds ([12 x i8], [12 x i8]* @.str, i64 0, i64 0), i8* getelementptr inbounds ([63 x i8], [63 x i8]* @.str.1, i64 0, i64 0), i32 19, i8* getelementptr inbounds ([11 x i8], [11 x i8]* @__PRETTY_FUNCTION__.main, i64 0, i64 0)) #3, !dbg !63 + unreachable, !dbg !63 + +39: ; preds = %37 + ret i32 0, !dbg !67 +} + +; Function Attrs: nofree nosync nounwind readnone speculatable willreturn +declare void @llvm.dbg.declare(metadata, metadata, metadata) #1 + +; Function Attrs: noreturn nounwind +declare dso_local void @__assert_fail(i8*, i8*, i32, i8*) #2 + +attributes #0 = { noinline nounwind uwtable "disable-tail-calls"="false" "frame-pointer"="all" "less-precise-fpmad"="false" "min-legal-vector-width"="0" "no-infs-fp-math"="false" "no-jump-tables"="false" "no-nans-fp-math"="false" "no-signed-zeros-fp-math"="false" "no-trapping-math"="true" "stack-protector-buffer-size"="8" "target-cpu"="x86-64" "target-features"="+cx8,+fxsr,+mmx,+sse,+sse2,+x87" "tune-cpu"="generic" "unsafe-fp-math"="false" "use-soft-float"="false" } +attributes #1 = { nofree nosync nounwind readnone speculatable willreturn } +attributes #2 = { noreturn nounwind "disable-tail-calls"="false" "frame-pointer"="all" "less-precise-fpmad"="false" "no-infs-fp-math"="false" "no-nans-fp-math"="false" "no-signed-zeros-fp-math"="false" "no-trapping-math"="true" "stack-protector-buffer-size"="8" "target-cpu"="x86-64" "target-features"="+cx8,+fxsr,+mmx,+sse,+sse2,+x87" "tune-cpu"="generic" "unsafe-fp-math"="false" "use-soft-float"="false" } +attributes #3 = { noreturn nounwind } + +!llvm.dbg.cu = !{!2} +!llvm.module.flags = !{!13, !14, !15} +!llvm.ident = !{!16} + +!0 = !DIGlobalVariableExpression(var: !1, expr: !DIExpression()) +!1 = distinct !DIGlobalVariable(name: "x", scope: !2, file: !6, line: 6, type: !7, isLocal: false, isDefinition: true) +!2 = distinct !DICompileUnit(language: DW_LANG_C99, file: !3, producer: "Ubuntu clang version 12.0.0-3ubuntu1~20.04.5", isOptimized: false, runtimeVersion: 0, emissionKind: FullDebug, enums: !4, globals: !5, splitDebugInlining: false, nameTableKind: None) +!3 = !DIFile(filename: "/home/ponce/git/Dat3M/benchmarks/c/miscellaneous/staticLoops.c", directory: "/home/ponce/git/Dat3M") +!4 = !{} +!5 = !{!0} +!6 = !DIFile(filename: "benchmarks/c/miscellaneous/staticLoops.c", directory: "/home/ponce/git/Dat3M") +!7 = !DIDerivedType(tag: DW_TAG_volatile_type, baseType: !8) +!8 = !DIDerivedType(tag: DW_TAG_typedef, name: "int32_t", file: !9, line: 26, baseType: !10) +!9 = !DIFile(filename: "/usr/include/x86_64-linux-gnu/bits/stdint-intn.h", directory: "") +!10 = !DIDerivedType(tag: DW_TAG_typedef, name: "__int32_t", file: !11, line: 41, baseType: !12) +!11 = !DIFile(filename: "/usr/include/x86_64-linux-gnu/bits/types.h", directory: "") +!12 = !DIBasicType(name: "int", size: 32, encoding: DW_ATE_signed) +!13 = !{i32 7, !"Dwarf Version", i32 4} +!14 = !{i32 2, !"Debug Info Version", i32 3} +!15 = !{i32 1, !"wchar_size", i32 4} +!16 = !{!"Ubuntu clang version 12.0.0-3ubuntu1~20.04.5"} +!17 = distinct !DISubprogram(name: "main", scope: !6, file: !6, line: 8, type: !18, scopeLine: 9, spFlags: DISPFlagDefinition, unit: !2, retainedNodes: !4) +!18 = !DISubroutineType(types: !19) +!19 = !{!12} +!20 = !DILocalVariable(name: "i", scope: !21, file: !6, line: 10, type: !12) +!21 = distinct !DILexicalBlock(scope: !17, file: !6, line: 10, column: 5) +!22 = !DILocation(line: 10, column: 14, scope: !21) +!23 = !DILocation(line: 10, column: 10, scope: !21) +!24 = !DILocation(line: 10, column: 21, scope: !25) +!25 = distinct !DILexicalBlock(scope: !21, file: !6, line: 10, column: 5) +!26 = !DILocation(line: 10, column: 23, scope: !25) +!27 = !DILocation(line: 10, column: 5, scope: !21) +!28 = !DILocation(line: 11, column: 10, scope: !25) +!29 = !DILocation(line: 11, column: 9, scope: !25) +!30 = !DILocation(line: 10, column: 32, scope: !25) +!31 = !DILocation(line: 10, column: 5, scope: !25) +!32 = distinct !{!32, !27, !33, !34} +!33 = !DILocation(line: 11, column: 10, scope: !21) +!34 = !{!"llvm.loop.mustprogress"} +!35 = !DILocalVariable(name: "i", scope: !36, file: !6, line: 13, type: !12) +!36 = distinct !DILexicalBlock(scope: !17, file: !6, line: 13, column: 5) +!37 = !DILocation(line: 13, column: 14, scope: !36) +!38 = !DILocation(line: 13, column: 10, scope: !36) +!39 = !DILocation(line: 13, column: 22, scope: !40) +!40 = distinct !DILexicalBlock(scope: !36, file: !6, line: 13, column: 5) +!41 = !DILocation(line: 13, column: 24, scope: !40) +!42 = !DILocation(line: 13, column: 5, scope: !36) +!43 = !DILocation(line: 14, column: 10, scope: !40) +!44 = !DILocation(line: 14, column: 9, scope: !40) +!45 = !DILocation(line: 13, column: 35, scope: !40) +!46 = !DILocation(line: 13, column: 5, scope: !40) +!47 = distinct !{!47, !42, !48, !34} +!48 = !DILocation(line: 14, column: 10, scope: !36) +!49 = !DILocalVariable(name: "i", scope: !50, file: !6, line: 16, type: !12) +!50 = distinct !DILexicalBlock(scope: !17, file: !6, line: 16, column: 5) +!51 = !DILocation(line: 16, column: 14, scope: !50) +!52 = !DILocation(line: 16, column: 10, scope: !50) +!53 = !DILocation(line: 16, column: 21, scope: !54) +!54 = distinct !DILexicalBlock(scope: !50, file: !6, line: 16, column: 5) +!55 = !DILocation(line: 16, column: 23, scope: !54) +!56 = !DILocation(line: 16, column: 5, scope: !50) +!57 = !DILocation(line: 17, column: 10, scope: !54) +!58 = !DILocation(line: 17, column: 9, scope: !54) +!59 = !DILocation(line: 16, column: 34, scope: !54) +!60 = !DILocation(line: 16, column: 5, scope: !54) +!61 = distinct !{!61, !56, !62, !34} +!62 = !DILocation(line: 17, column: 10, scope: !50) +!63 = !DILocation(line: 19, column: 2, scope: !64) +!64 = distinct !DILexicalBlock(scope: !65, file: !6, line: 19, column: 2) +!65 = distinct !DILexicalBlock(scope: !17, file: !6, line: 19, column: 2) +!66 = !DILocation(line: 19, column: 2, scope: !65) +!67 = !DILocation(line: 21, column: 2, scope: !17)