[LLVMdev] SimplifyIndVar looses nsw flags

[Jonas Wagner]

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>