[Polly][WIP] Use parameter constraints provided via llvm.assume

[jdoerfert]

Summary

• Mainly unit tests are missing --

[grosser]

Hi Johannes,

this patch looks good.

Tobias
PS: Please add next time the tests right away. This would make the review easier and more complete.

lib/Analysis/ScopInfo.cpp

1063 ↗

(On Diff #39460)

I think using a non-defined TI parameter to look for parameter constraints is rather unexpected. You should at least document this in the function header. Probably even better to understand would be to split this function into the part that creates the ConsequenceSet and the one that adds it
and then create two simple helpers, one for the parameter and one for the non parameter case.

1593 ↗

(On Diff #39460)

What about adding "ignored":

"Non-affine user assumption ignored"

polly/trunk/include/polly/ScopInfo.h

 #include "isl/ctx.h"
 
 #include <deque>
 #include <forward_list>
 
 using namespace llvm;
 
 namespace llvm {
+class AssumptionCache;
 class Loop;
 class LoopInfo;
 class PHINode;
 class ScalarEvolution;
 class SCEV;
 class SCEVAddRecExpr;
 class Type;
 }
private:
   InvariantEquivClassesTy InvariantEquivClasses;
 
   /// @brief Scop constructor; invoked from ScopInfo::buildScop.
   Scop(Region &R, AccFuncMapType &AccFuncMap, ScopDetection &SD,
        ScalarEvolution &SE, DominatorTree &DT, LoopInfo &LI, isl_ctx *ctx,
        unsigned MaxLoopDepth);
 
   /// @brief Initialize this ScopInfo .
-  void init(AliasAnalysis &AA);
+  void init(AliasAnalysis &AA, AssumptionCache &AC);
 
   /// @brief Add loop carried constraints to the header block of the loop @p L.
   ///
   /// @param L  The loop to process.
   void addLoopBoundsToHeaderDomain(Loop *L);
 
   /// @brief Compute the branching constraints for each basic block in @p R.
   ///
private:
   void addInvariantLoads(ScopStmt &Stmt, MemoryAccessList &InvMAs);
 
   /// @brief Build the Context of the Scop.
   void buildContext();
 
   /// @brief Build the BoundaryContext based on the wrapping of expressions.
   void buildBoundaryContext();
 
-  /// @brief Add user provided parameter constraints to context.
+  /// @brief Add user provided parameter constraints to context (source code).
+  void addUserAssumptions(AssumptionCache &AC);
+
+  /// @brief Add user provided parameter constraints to context (command line).
   void addUserContext();
 
   /// @brief Add the bounds of the parameters to the context.
   void addParameterBounds();
 
   /// @brief Simplify the assumed and boundary context.
   void simplifyContexts();
 
if (!scop)
       return nullptr;
     return &scop->getRegion();
   }
 
   // Clear the context.
   void clear();
 
   // Build the SCoP for Region @p R.
-  void buildScop(Region &R, DominatorTree &DT);
+  void buildScop(Region &R, DominatorTree &DT, AssumptionCache &AC);
 
   /// @brief Build an instance of MemoryAccess from the Load/Store instruction.
   ///
   /// @param Inst       The Load/Store instruction that access the memory
   /// @param L          The parent loop of the instruction
   /// @param R          The region on which to build the data access dictionary.
   /// @param BoxedLoops The set of loops that are overapproximated in @p R.
   /// @param ScopRIL    The required invariant loads equivalence classes.

polly/trunk/include/polly/Support/SCEVValidator.h

 /// region.
 ///
 /// @param S The SCEV to analyze.
 /// @param R The region in which we look for dependences.
 bool hasScalarDepsInsideRegion(const llvm::SCEV *S, const llvm::Region *R);
 bool isAffineExpr(const llvm::Region *R, const llvm::SCEV *Expression,
                   llvm::ScalarEvolution &SE, const llvm::Value *BaseAddress = 0,
                   InvariantLoadsSetTy *ILS = nullptr);
+
+/// @brief Check if @p V describes an affine parameter constraint in @p R.
+bool isAffineParamConstraint(llvm::Value *V, const llvm::Region *R,
+                             llvm::ScalarEvolution &SE,
+                             std::vector<const llvm::SCEV *> &Params,
+                             bool OrExpr = false);
+
 std::vector<const llvm::SCEV *>
 getParamsInAffineExpr(const llvm::Region *R, const llvm::SCEV *Expression,
                       llvm::ScalarEvolution &SE,
                       const llvm::Value *BaseAddress = 0);
 
 /// @brief Extract the constant factors from the multiplication @p M.
 ///
 /// @param M  A potential SCEV multiplication.
 /// @param SE The ScalarEvolution analysis to create new SCEVs.
 ///
 /// @returns The constant factor in @p M and the rest of @p M.
 std::pair<const llvm::SCEV *, const llvm::SCEV *>
 extractConstantFactor(const llvm::SCEV *M, llvm::ScalarEvolution &SE);
 }
 
 #endif

polly/trunk/lib/Analysis/ScopInfo.cpp

 #include "polly/Support/ScopHelper.h"
 #include "llvm/ADT/MapVector.h"
 #include "llvm/ADT/PostOrderIterator.h"
 #include "llvm/ADT/STLExtras.h"
 #include "llvm/ADT/SetVector.h"
 #include "llvm/ADT/Statistic.h"
 #include "llvm/ADT/StringExtras.h"
 #include "llvm/Analysis/AliasAnalysis.h"
+#include "llvm/Analysis/AssumptionCache.h"
 #include "llvm/Analysis/LoopInfo.h"
 #include "llvm/Analysis/LoopIterator.h"
 #include "llvm/Analysis/RegionIterator.h"
 #include "llvm/Analysis/ScalarEvolutionExpressions.h"
 #include "llvm/IR/DiagnosticInfo.h"
 #include "llvm/Support/Debug.h"
 #include "isl/aff.h"
 #include "isl/constraint.h"
buildConditionSets(Scop &S, SwitchInst *SI, Loop *L, __isl_keep isl_set *Domain,
   isl_pw_aff_free(LHS);
 }
 
 /// @brief Build the conditions sets for the branch condition @p Condition in
 ///        the @p Domain.
 ///
 /// This will fill @p ConditionSets with the conditions under which control
 /// will be moved from @p TI to its successors. Hence, @p ConditionSets will
-/// have as many elements as @p TI has successors.
+/// have as many elements as @p TI has successors. If @p TI is nullptr the
+/// context under which @p Condition is true/false will be returned as the
+/// new elements of @p ConditionSets.
 static void
 buildConditionSets(Scop &S, Value *Condition, TerminatorInst *TI, Loop *L,
                    __isl_keep isl_set *Domain,
                    SmallVectorImpl<__isl_give isl_set *> &ConditionSets) {
 
   isl_set *ConsequenceCondSet = nullptr;
   if (auto *CCond = dyn_cast<ConstantInt>(Condition)) {
     if (CCond->isZero())
if (auto *CCond = dyn_cast<ConstantInt>(Condition)) {
     else
       ConsequenceCondSet = isl_set_union(ConsCondPart0, ConsCondPart1);
   } else {
     auto *ICond = dyn_cast<ICmpInst>(Condition);
     assert(ICond &&
            "Condition of exiting branch was neither constant nor ICmp!");
 
     ScalarEvolution &SE = *S.getSE();
-    BasicBlock *BB = TI->getParent();
+    BasicBlock *BB = TI ? TI->getParent() : nullptr;
     isl_pw_aff *LHS, *RHS;
     LHS = S.getPwAff(SE.getSCEVAtScope(ICond->getOperand(0), L), BB);
     RHS = S.getPwAff(SE.getSCEVAtScope(ICond->getOperand(1), L), BB);
     ConsequenceCondSet =
         buildConditionSet(ICond->getPredicate(), LHS, RHS, Domain);
   }
 
+  // If no terminator was given we are only looking for parameter constraints
+  // under which @p Condition is true/false.
+  if (!TI)
+    ConsequenceCondSet = isl_set_params(ConsequenceCondSet);
+
   assert(ConsequenceCondSet);
   isl_set *AlternativeCondSet =
       isl_set_complement(isl_set_copy(ConsequenceCondSet));
 
   ConditionSets.push_back(isl_set_coalesce(
       isl_set_intersect(ConsequenceCondSet, isl_set_copy(Domain))));
   ConditionSets.push_back(isl_set_coalesce(
       isl_set_intersect(AlternativeCondSet, isl_set_copy(Domain))));
void Scop::buildBoundaryContext() {
 
   isl_options_set_on_error(getIslCtx(), ISL_ON_ERROR_ABORT);
   isl_ctx_reset_operations(getIslCtx());
   isl_ctx_set_max_operations(getIslCtx(), MaxOpsOld);
   BoundaryContext = isl_set_gist_params(BoundaryContext, getContext());
   trackAssumption(WRAPPING, BoundaryContext, DebugLoc());
 }
 
+void Scop::addUserAssumptions(AssumptionCache &AC) {
+  auto *R = &getRegion();
+  auto &F = *R->getEntry()->getParent();
+  for (auto &Assumption : AC.assumptions()) {
+    auto *CI = dyn_cast_or_null<CallInst>(Assumption);
+    if (!CI || CI->getNumArgOperands() != 1)
+      continue;
+    if (!DT.dominates(CI->getParent(), R->getEntry()))
+      continue;
+
+    auto *Val = CI->getArgOperand(0);
+    std::vector<const SCEV *> Params;
+    if (!isAffineParamConstraint(Val, R, *SE, Params)) {
+      emitOptimizationRemarkAnalysis(F.getContext(), DEBUG_TYPE, F,
+                                     CI->getDebugLoc(),
+                                     "Non-affine user assumption ignored.");
+      continue;
+    }
+
+    addParams(Params);
+
+    auto *L = LI.getLoopFor(CI->getParent());
+    SmallVector<isl_set *, 2> ConditionSets;
+    buildConditionSets(*this, Val, nullptr, L, Context, ConditionSets);
+    assert(ConditionSets.size() == 2);
+    isl_set_free(ConditionSets[1]);
+
+    auto *AssumptionCtx = ConditionSets[0];
+    emitOptimizationRemarkAnalysis(
+        F.getContext(), DEBUG_TYPE, F, CI->getDebugLoc(),
+        "Use user assumption: " + stringFromIslObj(AssumptionCtx));
+    Context = isl_set_intersect(Context, AssumptionCtx);
+  }
+}
+
 void Scop::addUserContext() {
   if (UserContextStr.empty())
     return;
 
   isl_set *UserContext = isl_set_read_from_str(IslCtx, UserContextStr.c_str());
   isl_space *Space = getParamSpace();
   if (isl_space_dim(Space, isl_dim_param) !=
       isl_set_dim(UserContext, isl_dim_param)) {
Scop::Scop(Region &R, AccFuncMapType &AccFuncMap, ScopDetection &SD,
            isl_ctx *Context, unsigned MaxLoopDepth)
     : LI(LI), DT(DT), SE(&ScalarEvolution), SD(SD), R(R),
       AccFuncMap(AccFuncMap), IsOptimized(false),
       HasSingleExitEdge(R.getExitingBlock()), HasErrorBlock(false),
       MaxLoopDepth(MaxLoopDepth), IslCtx(Context), Context(nullptr),
       Affinator(this), AssumedContext(nullptr), BoundaryContext(nullptr),
       Schedule(nullptr) {}
 
-void Scop::init(AliasAnalysis &AA) {
+void Scop::init(AliasAnalysis &AA, AssumptionCache &AC) {
   buildContext();
+  addUserAssumptions(AC);
   buildInvariantEquivalenceClasses();
 
   buildDomains(&R);
 
   // Remove empty and ignored statements.
   // Exit early in case there are no executable statements left in this scop.
   simplifySCoP(true);
   if (Stmts.empty())
addMemoryAccess(IncomingBlock, IncomingBlock->getTerminator(),
                   IsExitBlock ? MemoryAccess::SCALAR : MemoryAccess::PHI);
 }
 void ScopInfo::addPHIReadAccess(PHINode *PHI) {
   addMemoryAccess(PHI->getParent(), PHI, MemoryAccess::READ, PHI, 1, true, PHI,
                   ArrayRef<const SCEV *>(), ArrayRef<const SCEV *>(),
                   MemoryAccess::PHI);
 }
 
-void ScopInfo::buildScop(Region &R, DominatorTree &DT) {
+void ScopInfo::buildScop(Region &R, DominatorTree &DT, AssumptionCache &AC) {
   unsigned MaxLoopDepth = getMaxLoopDepthInRegion(R, *LI, *SD);
   scop = new Scop(R, AccFuncMap, *SD, *SE, DT, *LI, ctx, MaxLoopDepth);
 
   buildStmts(R);
   buildAccessFunctions(R, R);
 
   // In case the region does not have an exiting block we will later (during
   // code generation) split the exit block. This will move potential PHI nodes
   // from the current exit block into the new region exiting block. Hence, PHI
   // nodes that are at this point not part of the region will be.
   // To handle these PHI nodes later we will now model their operands as scalar
   // accesses. Note that we do not model anything in the exit block if we have
   // an exiting block in the region, as there will not be any splitting later.
   if (!R.getExitingBlock())
     buildAccessFunctions(R, *R.getExit(), nullptr, /* IsExitBlock */ true);
 
-  scop->init(*AA);
+  scop->init(*AA, AC);
 }
 
 void ScopInfo::print(raw_ostream &OS, const Module *) const {
   if (!scop) {
     OS << "Invalid Scop!\n";
     return;
   }
 

 
 void ScopInfo::getAnalysisUsage(AnalysisUsage &AU) const {
   AU.addRequired<LoopInfoWrapperPass>();
   AU.addRequired<RegionInfoPass>();
   AU.addRequired<DominatorTreeWrapperPass>();
   AU.addRequiredTransitive<ScalarEvolutionWrapperPass>();
   AU.addRequiredTransitive<ScopDetection>();
   AU.addRequired<AAResultsWrapperPass>();
+  AU.addRequired<AssumptionCacheTracker>();
   AU.setPreservesAll();
 }
 
 bool ScopInfo::runOnRegion(Region *R, RGPassManager &RGM) {
   SD = &getAnalysis<ScopDetection>();
 
   if (!SD->isMaxRegionInScop(*R))
     return false;
 
   Function *F = R->getEntry()->getParent();
   SE = &getAnalysis<ScalarEvolutionWrapperPass>().getSE();
   LI = &getAnalysis<LoopInfoWrapperPass>().getLoopInfo();
   AA = &getAnalysis<AAResultsWrapperPass>().getAAResults();
   TD = &F->getParent()->getDataLayout();
   DominatorTree &DT = getAnalysis<DominatorTreeWrapperPass>().getDomTree();
+  auto &AC = getAnalysis<AssumptionCacheTracker>().getAssumptionCache(*F);
 
   DebugLoc Beg, End;
   getDebugLocations(R, Beg, End);
   std::string Msg = "SCoP begins here.";
   emitOptimizationRemarkAnalysis(F->getContext(), DEBUG_TYPE, *F, Beg, Msg);
 
-  buildScop(*R, DT);
+  buildScop(*R, DT, AC);
 
   DEBUG(scop->print(dbgs()));
 
   if (scop->isEmpty() || !scop->hasFeasibleRuntimeContext()) {
     Msg = "SCoP ends here but was dismissed.";
     delete scop;
     scop = nullptr;
   } else {

 char ScopInfo::ID = 0;
 
 Pass *polly::createScopInfoPass() { return new ScopInfo(); }
 
 INITIALIZE_PASS_BEGIN(ScopInfo, "polly-scops",
                       "Polly - Create polyhedral description of Scops", false,
                       false);
 INITIALIZE_PASS_DEPENDENCY(AAResultsWrapperPass);
+INITIALIZE_PASS_DEPENDENCY(AssumptionCacheTracker);
 INITIALIZE_PASS_DEPENDENCY(LoopInfoWrapperPass);
 INITIALIZE_PASS_DEPENDENCY(RegionInfoPass);
 INITIALIZE_PASS_DEPENDENCY(ScalarEvolutionWrapperPass);
 INITIALIZE_PASS_DEPENDENCY(ScopDetection);
 INITIALIZE_PASS_DEPENDENCY(DominatorTreeWrapperPass);
 INITIALIZE_PASS_END(ScopInfo, "polly-scops",
                     "Polly - Create polyhedral description of Scops", false,
                     false)

polly/trunk/lib/Support/SCEVValidator.cpp

DEBUG({
     if (Result.isValid())
       dbgs() << "VALID\n";
     dbgs() << "\n";
   });
 
   return Result.isValid();
 }
 
+static bool isAffineParamExpr(Value *V, const Region *R, ScalarEvolution &SE,
+                              std::vector<const SCEV *> &Params) {
+  auto *E = SE.getSCEV(V);
+  if (isa<SCEVCouldNotCompute>(E))
+    return false;
+
+  SCEVValidator Validator(R, SE, nullptr, nullptr);
+  ValidatorResult Result = Validator.visit(E);
+  if (!Result.isConstant())
+    return false;
+
+  auto ResultParams = Result.getParameters();
+  Params.insert(Params.end(), ResultParams.begin(), ResultParams.end());
+
+  return true;
+}
+
+bool isAffineParamConstraint(Value *V, const Region *R, ScalarEvolution &SE,
+                             std::vector<const SCEV *> &Params, bool OrExpr) {
+  if (auto *ICmp = dyn_cast<ICmpInst>(V)) {
+    return isAffineParamConstraint(ICmp->getOperand(0), R, SE, Params, true) &&
+           isAffineParamConstraint(ICmp->getOperand(1), R, SE, Params, true);
+  } else if (auto *BinOp = dyn_cast<BinaryOperator>(V)) {
+    auto Opcode = BinOp->getOpcode();
+    if (Opcode == Instruction::And || Opcode == Instruction::Or)
+      return isAffineParamConstraint(BinOp->getOperand(0), R, SE, Params,
+                                     false) &&
+             isAffineParamConstraint(BinOp->getOperand(1), R, SE, Params,
+                                     false);
+    /* Fall through */
+  }
+
+  if (!OrExpr)
+    return false;
+
+  return isAffineParamExpr(V, R, SE, Params);
+}
+
 std::vector<const SCEV *> getParamsInAffineExpr(const Region *R,
                                                 const SCEV *Expr,
                                                 ScalarEvolution &SE,
                                                 const Value *BaseAddress) {
   if (isa<SCEVCouldNotCompute>(Expr))
     return std::vector<const SCEV *>();
 
   InvariantLoadsSetTy ILS;

polly/trunk/test/ScopInfo/user_provided_assumptions.ll

+; RUN: opt %loadPolly -pass-remarks-analysis="polly-scops" -polly-scops -analyze < %s 2>&1| FileCheck %s
+;
+; CHECK:      remark: <unknown>:0:0: SCoP begins here.
+; CHECK-NEXT: remark: <unknown>:0:0: Use user assumption: [M, N] -> {  : N <= 2147483647 - M }
+; CHECK-NEXT: remark: <unknown>:0:0: Use user assumption: [M, N] -> {  : N >= -2147483648 - M and N <= 2147483647 - M }
+; CHECK-NEXT: remark: <unknown>:0:0: Use user assumption: [M, N, Debug] -> {  : Debug = 0 and M <= 100 and M >= 1 and N <= 2147483647 - M and N >= -2147483648 - M }
+; CHECK-NEXT: remark: <unknown>:0:0: Use user assumption: [M, N, Debug] -> {  : Debug = 0 and N >= -2147483648 - M and N <= 2147483647 - M and M <= 100 and M >= 1 and N >= 1 }
+; CHECK-NEXT: remark: <unknown>:0:0: SCoP ends here.
+;
+; CHECK:      Context:
+; CHECK-NEXT:   [N, M, Debug] -> {  : Debug = 0 and N >= 1 and M <= 2147483647 - N and M <= 100 and M >= 1 }
+; CHECK-NEXT: Assumed Context:
+; CHECK-NEXT:   [N, M, Debug] -> {  :  }
+; CHECK-NEXT: Boundary Context:
+; CHECK-NEXT:   [N, M, Debug] -> {  :  }
+;
+;    #include <stdio.h>
+;
+;    void valid(int * restrict A, int * restrict B, int N, int M, int C[100][100], int Debug) {
+;      __builtin_assume(M <= 2147483647 - N);
+;      __builtin_assume(M >= -2147483648 - N);
+;      __builtin_assume(Debug == 0 && M <= 100 && M >= 1 && N >= 1);
+;      if (N + M == -1)
+;        C[0][0] = 0;
+;
+;      for (int i = 0; i < N; i++) {
+;        for (int j = 0; j != M; j++) {
+;          C[i][j] += A[i * M + j] + B[i + j];
+;        }
+;
+;        if (Debug)
+;          printf("Printf!");
+;      }
+;    }
+;
+target datalayout = "e-m:e-i64:64-f80:128-n8:16:32:64-S128"
+
+@.str = private unnamed_addr constant [8 x i8] c"Printf!\00", align 1
+
+define void @valid(i32* noalias %A, i32* noalias %B, i32 %N, i32 %M, [100 x i32]* %C, i32 %Debug) {
+entry:
+  %sub = sub nsw i32 2147483647, %N
+  %cmp = icmp sge i32 %sub, %M
+  call void @llvm.assume(i1 %cmp)
+  %conv = sext i32 %M to i64
+  %conv1 = sext i32 %N to i64
+  %sub2 = sub nsw i64 -2147483648, %conv1
+  %cmp3 = icmp sge i64 %conv, %sub2
+  call void @llvm.assume(i1 %cmp3)
+  %cmp5 = icmp eq i32 %Debug, 0
+  %cmp7 = icmp slt i32 %M, 101
+  %or.cond = and i1 %cmp5, %cmp7
+  %cmp10 = icmp sgt i32 %M, 0
+  %or.cond1 = and i1 %or.cond, %cmp10
+  %cmp12 = icmp sgt i32 %N, 0
+  call void @llvm.assume(i1 %or.cond1)
+  call void @llvm.assume(i1 %cmp12)
+  %add = add nsw i32 %N, %M
+  %cmp14 = icmp eq i32 %add, -1
+  br label %entry.split
+
+entry.split:
+  br i1 %cmp14, label %if.then, label %if.end
+
+if.then:                                          ; preds = %entry
+  %arrayidx16 = getelementptr inbounds [100 x i32], [100 x i32]* %C, i64 0, i64 0
+  store i32 0, i32* %arrayidx16, align 4
+  br label %if.end
+
+if.end:                                           ; preds = %if.then, %entry
+  %M64 = sext i32 %M to i64
+  %N64 = sext i32 %N to i64
+  br label %for.cond
+
+for.cond:                                         ; preds = %for.inc.36, %if.end
+  %indvars.iv3 = phi i64 [ %indvars.iv.next4, %for.inc.36 ], [ 0, %if.end ]
+  %cmp17 = icmp slt i64 %indvars.iv3, %N64
+  br i1 %cmp17, label %for.cond.19, label %for.end.38
+
+for.cond.19:                                      ; preds = %for.cond, %for.body.22
+  %indvars.iv = phi i64 [ %indvars.iv.next, %for.body.22 ], [ 0, %for.cond ]
+  %cmp20 = icmp eq i64 %indvars.iv, %M64
+  br i1 %cmp20, label %for.end, label %for.body.22
+
+for.body.22:                                      ; preds = %for.cond.19
+  %tmp9 = mul nsw i64 %indvars.iv3, %M64
+  %tmp10 = add nsw i64 %tmp9, %indvars.iv
+  %arrayidx24 = getelementptr inbounds i32, i32* %A, i64 %tmp10
+  %tmp11 = load i32, i32* %arrayidx24, align 4
+  %tmp12 = add nuw nsw i64 %indvars.iv3, %indvars.iv
+  %arrayidx27 = getelementptr inbounds i32, i32* %B, i64 %tmp12
+  %tmp13 = load i32, i32* %arrayidx27, align 4
+  %add28 = add nsw i32 %tmp11, %tmp13
+  %arrayidx32 = getelementptr inbounds [100 x i32], [100 x i32]* %C, i64 %indvars.iv3, i64 %indvars.iv
+  %tmp14 = load i32, i32* %arrayidx32, align 4
+  %add33 = add nsw i32 %tmp14, %add28
+  store i32 %add33, i32* %arrayidx32, align 4
+  %indvars.iv.next = add nuw nsw i64 %indvars.iv, 1
+  br label %for.cond.19
+
+for.end:                                          ; preds = %for.cond.19
+  %tobool = icmp eq i32 %Debug, 0
+  br i1 %tobool, label %for.inc.36, label %if.then.34
+
+if.then.34:                                       ; preds = %for.end
+  %call = call i32 (i8*, ...) @printf(i8* nonnull getelementptr inbounds ([8 x i8], [8 x i8]* @.str, i64 0, i64 0))
+  br label %for.inc.36
+
+for.inc.36:                                       ; preds = %for.end, %if.then.34
+  %indvars.iv.next4 = add nuw nsw i64 %indvars.iv3, 1
+  br label %for.cond
+
+for.end.38:                                       ; preds = %for.cond
+  ret void
+}
+
+; Function Attrs: nounwind
+declare void @llvm.assume(i1) #0
+
+declare i32 @printf(i8*, ...)
+
+attributes #0 = { nounwind }

polly/trunk/test/ScopInfo/user_provided_non_dominating_assumptions.ll

+; RUN: opt %loadPolly -pass-remarks-analysis="polly-scops" -polly-scops < %s 2>&1| FileCheck %s
+;
+; CHECK:      remark: <unknown>:0:0: SCoP begins here.
+; CHECK-NEXT: remark: <unknown>:0:0: Inbounds assumption: [i, N, p_2, M] -> {  : N <= i or (N >= 1 + i and p_2 <= 0) or (N >= 1 + i and p_2 >= 1 and M >= p_2) }
+; CHECK-NEXT: remark: <unknown>:0:0: Inbounds assumption: [i, N, p_2] -> {  : N <= i or (N >= 1 + i and p_2 <= 100) }
+; CHECK-NEXT: remark: <unknown>:0:0: SCoP ends here.
+;
+;    void f(int *restrict A, int *restrict B, int i, int N, int M, int C[100][100]) {
+;      for (; i < N; i++) {
+;        __builtin_assume(N >= 0);
+;        for (int j = 0; j != M; j++) {
+;          __builtin_assume(N >= 0);
+;          C[i][j] += A[i * M + j] + B[i + j];
+;        }
+;      }
+;    }
+;
+target datalayout = "e-m:e-i64:64-f80:128-n8:16:32:64-S128"
+
+define void @f(i32* noalias %A, i32* noalias %B, i32 %i, i32 %N, i32 %M, [100 x i32]* %C) {
+entry:
+  %tmp = zext i32 %M to i64
+  %tmp6 = sext i32 %i to i64
+  %tmp7 = sext i32 %N to i64
+  %tmp8 = sext i32 %M to i64
+  br label %for.cond
+
+for.cond:                                         ; preds = %for.inc.15, %entry
+  %indvars.iv3 = phi i64 [ %indvars.iv.next4, %for.inc.15 ], [ %tmp6, %entry ]
+  %cmp = icmp slt i64 %indvars.iv3, %tmp7
+  br i1 %cmp, label %for.body, label %for.end.17
+
+for.body:                                         ; preds = %for.cond
+  %cmp1 = icmp sgt i32 %N, -1
+  call void @llvm.assume(i1 %cmp1)
+  br label %for.cond.2
+
+for.cond.2:                                       ; preds = %for.inc, %for.body
+  %indvars.iv = phi i64 [ %indvars.iv.next, %for.inc ], [ 0, %for.body ]
+  %cmp3 = icmp eq i64 %indvars.iv, %tmp
+  br i1 %cmp3, label %for.end, label %for.body.4
+
+for.body.4:                                       ; preds = %for.cond.2
+  %tmp9 = mul nsw i64 %indvars.iv3, %tmp8
+  %tmp10 = add nsw i64 %tmp9, %indvars.iv
+  %arrayidx = getelementptr inbounds i32, i32* %A, i64 %tmp10
+  %tmp11 = load i32, i32* %arrayidx, align 4
+  %tmp12 = add nsw i64 %indvars.iv3, %indvars.iv
+  %arrayidx8 = getelementptr inbounds i32, i32* %B, i64 %tmp12
+  %tmp13 = load i32, i32* %arrayidx8, align 4
+  %add9 = add nsw i32 %tmp11, %tmp13
+  %arrayidx13 = getelementptr inbounds [100 x i32], [100 x i32]* %C, i64 %indvars.iv3, i64 %indvars.iv
+  %tmp14 = load i32, i32* %arrayidx13, align 4
+  %add14 = add nsw i32 %tmp14, %add9
+  store i32 %add14, i32* %arrayidx13, align 4
+  br label %for.inc
+
+for.inc:                                          ; preds = %for.body.4
+  %indvars.iv.next = add nuw nsw i64 %indvars.iv, 1
+  br label %for.cond.2
+
+for.end:                                          ; preds = %for.cond.2
+  br label %for.inc.15
+
+for.inc.15:                                       ; preds = %for.end
+  %indvars.iv.next4 = add nsw i64 %indvars.iv3, 1
+  br label %for.cond
+
+for.end.17:                                       ; preds = %for.cond
+  ret void
+}
+
+declare void @llvm.assume(i1) #1
+