[LLVMdev] SimplifyIndVar looses nsw flags

[Hal Finkel]

----- Original Message -----
> 
> 
> 
> 
> 
> 
> 
> Hello,
> 
> I'm using LLVM to reason about memory safety of programs. One goal is
> to prove that certain array accesses are always safe.
> 
> Currently, one of these proofs fails because of a missing
> no-signed-wrap (nsw) flag. I found that it has been "lost" during
> the SimplifyIndVar pass. Here's the example:
> 
> int foo(int a[]) {
> int sum = 0;
> for (int i = 0; i < 1000; ++i)
> sum += a[i];
> return sum;
> }
> 
> // *** IR Dump Before Induction Variable Simplification ***
> // for.body: ; preds = %entry, %for.body
> // %i.05 = phi i32 [ 0, %entry ], [ %inc, %for.body ]
> // %sum.04 = phi i32 [ 0, %entry ], [ %add, %for.body ]
> // %idxprom = sext i32 %i.05 to i64
> // %arrayidx = getelementptr inbounds i32* %a, i64 %idxprom
> // %0 = load i32* %arrayidx, align 4, !tbaa !0
> // %add = add nsw i32 %0, %sum.04
> // %inc = add nsw i32 %i.05, 1
> // %cmp = icmp slt i32 %inc, 1000
> // br i1 %cmp, label %for.body, label %for.end
> // *** IR Dump After Induction Variable Simplification ***
> // for.body: ; preds = %entry, %for.body
> // %indvars.iv = phi i64 [ 0, %entry ], [ %indvars.iv.next, %for.body
> ]
> // %sum.04 = phi i32 [ 0, %entry ], [ %add, %for.body ]
> // %arrayidx = getelementptr inbounds i32* %a, i64 %indvars.iv
> // %0 = load i32* %arrayidx, align 4, !tbaa !0
> // %add = add nsw i32 %0, %sum.04
> // %indvars.iv.next = add i64 %indvars.iv, 1
> // %lftr.wideiv = trunc i64 %indvars.iv.next to i32
> // %exitcond = icmp ne i32 %lftr.wideiv, 1000
> // br i1 %exitcond, label %for.body, label %for.end
> 
> You can see that %inc is transformed into %indvars.iv.next, and the
> nsw flag is lost in the process.
> 
> Is this behavior a problem with SimplifyIndVar or is this expected?
> How easy would it be to change this, and do you have any pointers to
> where I should have to look?

Coincidentally, we were just discussing this issue as part of the "Re: [LLVMdev] [llvm] r184698 - Add a flag to defer vectorization into a phase after the inliner and its" thread. I believe that Andy mentioned something about how he felt this should fix fixed.

 -Hal

> 
> Cheers,
> Jonas
> 
> _______________________________________________
> LLVM Developers mailing list
> LLVMdev at cs.uiuc.edu         http://llvm.cs.uiuc.edu
> http://lists.cs.uiuc.edu/mailman/listinfo/llvmdev
> 

-- 
Hal Finkel
Assistant Computational Scientist
Leadership Computing Facility
Argonne National Laboratory