llvm dev - Jun 2009 - [LLVMdev] Handling SMax(N, N - constInt) in Scalar Evolution pass

On Tue, 2009-06-23 at 22:55 -0700, Nick Lewycky wrote:
> Mai, Haohui wrote:
> > Hi all,
> > 
> > I'm working on a project which tries to prove an access to an
array is
> > safe. For example,
> > 
> > int foo(int s) {
> >   int * p = malloc(s * sizeof int);
> >   ...
> >   int q = p[s - 2];
> > }
> > 
> > then the access of p[s - 2] always stays in bound.
> > 
> > I implemented a prototype using the Scalar Evolution pass. Here are
the
> > pseudo-code of the implementation:
> > 
> >   const SCEV * offset = SE->getMinusSCEV(SE->getSCEV(GEP),
GEPBase);
> >   const SCEV * bounds = SE->getSCEV(objSize);
> >  
> >   if (SE->getSMaxExpr(offset, bounds) == bounds) {
> >     ++safeGEPs;
> >   }
> > 
> > But it turns out that SCEVSMaxExpr does not handle the case of SMax(N,
> > N-2).
> 
> Consider 8-bit integers and N = -127. N-1 equals INT_MIN and N-2 then is 
> equal to INT_MAX, or 127. In that case, the SMax would equal N-2, not N.
> 
> In other cases (like N = 2) the SMax would equal N, not N-2.
> 
> Because of this, we cannot reduce this SMax any further. Your suggestion 
> that "SMax(A, B) == SMax(A-B, 0) + B" is incorrect.
> Nick
It seems that there are codes in Scalar Evolution to handle this case.
Many operations in scalar evolution only happen when SCEV can be sign
extended.
> 
> > My question is, is there a plan to support something like this, or is
it
> > possible to do some refactoring to enhance the capability of Scalar
> > Evolution? I notice that Scalar Evolution, Instruction Combining and
> > Memory Dependence Analysis require sort of evaluating symbolic
> > expression like this.
> > 
> > For this case SMax(A, B) is equivalent to SMax(A-B,0) + B, instruction
> > combining handles  sophisticated expressions like (A+B)-B pretty well.
> > It would be great if Scalar Evolution can support this.
> > 
> > Any comments are appreciated.
> > 
> > Cheers,
> > 
> > Haohui
> > 
> > _______________________________________________
> > LLVM Developers mailing list
> > LLVMdev at cs.uiuc.edu         http://llvm.cs.uiuc.edu
> > http://lists.cs.uiuc.edu/mailman/listinfo/llvmdev
> > 
> 
> _______________________________________________
> LLVM Developers mailing list
> LLVMdev at cs.uiuc.edu         http://llvm.cs.uiuc.edu
> http://lists.cs.uiuc.edu/mailman/listinfo/llvmdev

Nick,

It might be a little bit difficult to handle SMax correctly. But is it
possible to reduce A+(-A) to 0 in SAddExpr?

Haohui


On Wed, 2009-06-24 at 01:05 -0500, Mai, Haohui wrote:
> On Tue, 2009-06-23 at 22:55 -0700, Nick Lewycky wrote:
> > Mai, Haohui wrote:
> > > Hi all,
> > > 
> > > I'm working on a project which tries to prove an access to an
array is
> > > safe. For example,
> > > 
> > > int foo(int s) {
> > >   int * p = malloc(s * sizeof int);
> > >   ...
> > >   int q = p[s - 2];
> > > }
> > > 
> > > then the access of p[s - 2] always stays in bound.
> > > 
> > > I implemented a prototype using the Scalar Evolution pass. Here
are the
> > > pseudo-code of the implementation:
> > > 
> > >   const SCEV * offset = SE->getMinusSCEV(SE->getSCEV(GEP),
GEPBase);
> > >   const SCEV * bounds = SE->getSCEV(objSize);
> > >  
> > >   if (SE->getSMaxExpr(offset, bounds) == bounds) {
> > >     ++safeGEPs;
> > >   }
> > > 
> > > But it turns out that SCEVSMaxExpr does not handle the case of
SMax(N,
> > > N-2).
> > 
> > Consider 8-bit integers and N = -127. N-1 equals INT_MIN and N-2 then
is
> > equal to INT_MAX, or 127. In that case, the SMax would equal N-2, not
N.
> > 
> > In other cases (like N = 2) the SMax would equal N, not N-2.
> > 
> > Because of this, we cannot reduce this SMax any further. Your
suggestion
> > that "SMax(A, B) == SMax(A-B, 0) + B" is incorrect.
> > Nick
> 
> It seems that there are codes in Scalar Evolution to handle this case.
> Many operations in scalar evolution only happen when SCEV can be sign
> extended.
> 
> > 
> > > My question is, is there a plan to support something like this,
or is it
> > > possible to do some refactoring to enhance the capability of
Scalar
> > > Evolution? I notice that Scalar Evolution, Instruction Combining
and
> > > Memory Dependence Analysis require sort of evaluating symbolic
> > > expression like this.
> > > 
> > > For this case SMax(A, B) is equivalent to SMax(A-B,0) + B,
instruction
> > > combining handles  sophisticated expressions like (A+B)-B pretty
well.
> > > It would be great if Scalar Evolution can support this.
> > > 
> > > Any comments are appreciated.
> > > 
> > > Cheers,
> > > 
> > > Haohui
> > > 
> > > _______________________________________________
> > > LLVM Developers mailing list
> > > LLVMdev at cs.uiuc.edu         http://llvm.cs.uiuc.edu
> > > http://lists.cs.uiuc.edu/mailman/listinfo/llvmdev
> > > 
> > 
> > _______________________________________________
> > LLVM Developers mailing list
> > LLVMdev at cs.uiuc.edu         http://llvm.cs.uiuc.edu
> > http://lists.cs.uiuc.edu/mailman/listinfo/llvmdev
>

Mai, Haohui wrote:
> Nick,
> 
> It might be a little bit difficult to handle SMax correctly. But is it
> possible to reduce A+(-A) to 0 in SAddExpr?
Yes, it should already do that. Here's a quick test I wrote up:

   $ cat x.ll
   define i8 @test(i8 %x) {
     %neg = sub i8 0, %x
     %sum = add i8 %x, %neg
     ret i8 %sum
   }
   $ llvm-as < x.ll | opt -analyze -scalar-evolution -disable-output
   Printing analysis 'Scalar Evolution Analysis' for function
'test':
   Classifying expressions for: test
           %neg = sub i8 0, %x             ; <i8> [#uses=1]
     -->  (-1 * %x)
           %sum = add i8 %x, %neg          ; <i8> [#uses=1]
     -->  0
   Determining loop execution counts for: test

You'll note that %sum is deduced to be 0 and not (%x + (-1 * %x)) which 
indicates that this optimization is working correctly. If you have a 
more complicated case where it isn't, feel free to file a bug and cc me.

Nick
> On Wed, 2009-06-24 at 01:05 -0500, Mai, Haohui wrote:
>> On Tue, 2009-06-23 at 22:55 -0700, Nick Lewycky wrote:
>>> Mai, Haohui wrote:
>>>> Hi all,
>>>>
>>>> I'm working on a project which tries to prove an access to
an array is
>>>> safe. For example,
>>>>
>>>> int foo(int s) {
>>>>   int * p = malloc(s * sizeof int);
>>>>   ...
>>>>   int q = p[s - 2];
>>>> }
>>>>
>>>> then the access of p[s - 2] always stays in bound.
>>>>
>>>> I implemented a prototype using the Scalar Evolution pass. Here
are the
>>>> pseudo-code of the implementation:
>>>>
>>>>   const SCEV * offset =
SE->getMinusSCEV(SE->getSCEV(GEP), GEPBase);
>>>>   const SCEV * bounds = SE->getSCEV(objSize);
>>>>  
>>>>   if (SE->getSMaxExpr(offset, bounds) == bounds) {
>>>>     ++safeGEPs;
>>>>   }
>>>>
>>>> But it turns out that SCEVSMaxExpr does not handle the case of
SMax(N,
>>>> N-2).
>>> Consider 8-bit integers and N = -127. N-1 equals INT_MIN and N-2
then is
>>> equal to INT_MAX, or 127. In that case, the SMax would equal N-2,
not N.
>>>
>>> In other cases (like N = 2) the SMax would equal N, not N-2.
>>>
>>> Because of this, we cannot reduce this SMax any further. Your
suggestion
>>> that "SMax(A, B) == SMax(A-B, 0) + B" is incorrect.
>>> Nick
>> It seems that there are codes in Scalar Evolution to handle this case.
>> Many operations in scalar evolution only happen when SCEV can be sign
>> extended.
>>
>>>> My question is, is there a plan to support something like this,
or is it
>>>> possible to do some refactoring to enhance the capability of
Scalar
>>>> Evolution? I notice that Scalar Evolution, Instruction
Combining and
>>>> Memory Dependence Analysis require sort of evaluating symbolic
>>>> expression like this.
>>>>
>>>> For this case SMax(A, B) is equivalent to SMax(A-B,0) + B,
instruction
>>>> combining handles  sophisticated expressions like (A+B)-B
pretty well.
>>>> It would be great if Scalar Evolution can support this.
>>>>
>>>> Any comments are appreciated.
>>>>
>>>> Cheers,
>>>>
>>>> Haohui
>>>>
>>>> _______________________________________________
>>>> LLVM Developers mailing list
>>>> LLVMdev at cs.uiuc.edu         http://llvm.cs.uiuc.edu
>>>> http://lists.cs.uiuc.edu/mailman/listinfo/llvmdev
>>>>
>>> _______________________________________________
>>> LLVM Developers mailing list
>>> LLVMdev at cs.uiuc.edu         http://llvm.cs.uiuc.edu
>>> http://lists.cs.uiuc.edu/mailman/listinfo/llvmdev
> 
> _______________________________________________
> LLVM Developers mailing list
> LLVMdev at cs.uiuc.edu         http://llvm.cs.uiuc.edu
> http://lists.cs.uiuc.edu/mailman/listinfo/llvmdev
>