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?
Cheers,
Jonas
-------------- next part --------------
An HTML attachment was scrubbed...
URL:
<http://lists.llvm.org/pipermail/llvm-dev/attachments/20130625/a8ee1d4f/attachment.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: simplify_ind_var.c
Type: text/x-csrc
Size: 1369 bytes
Desc: not available
URL:
<http://lists.llvm.org/pipermail/llvm-dev/attachments/20130625/a8ee1d4f/attachment.c>
----- 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
> 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. >Thanks! It seems that it's indeed a complex issue... I feel I don't have the necessary knowledge of LLVM's optimizations to do something about it. But if this continues to hurt me, or if somebody has concrete ideas of how to fix it, I'll look at the code. - Jonas -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.llvm.org/pipermail/llvm-dev/attachments/20130625/6b68d77c/attachment.html>