SimplifyIndVar looses nsw flags

Project Infrastructure LLVM Dev List Archives
1

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

simplify_ind_var.c (1.34 KB)

2

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

3

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