[LLVMdev] Handling SMax(N, N - constInt) in Scalar Evolution pass

[Mai, Haohui]

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).

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