[PATCH] [Unfinished] Use modulo semantic to generate non-wrap assumptions

[Tobias Grosser]

In http://reviews.llvm.org/D9099#162193, @jdoerfert wrote:

> I commited first parts of this patch already, however there are still two problems I wanted to discuss before we move forward.


I followed this. Nice.

> 1. A few (~8) tests in lnt fail, at least one of them times out when the complement of the isl_set is computed as the set has multiple existentially quantified variables. I tried to use the domain on which both functions are equal to avoid the complement but I cannot get the constraints on the parameters that way.


You do not happen to have a (minimal?) test case that shows this behavior?

> 2. We currently assume parameters to be signed (e.g., use the signed range information about them) but this will use unsigned modulo semantic (e.g., mod bitwidth) to compute valid parameter combinations.


What do you mean by "this"?

The 'res = ((res + 2^7) mod (2 ^ 8)) - 2^7' models wrapping of signed types, which
is what we want for signed types. Can you point me to where exactly we use 'signed modulo semantic'?

> First, this makes it hard to generate tests with small bounds and it additionally makes it hard to argue about the test cases we can generate. I am currently not even sure this is safe. An example for this clash of interpretation below:

> 

>   // Let T be an integer type of width W

>   char *A = ...

>   T N = ...                   //   N    is in [-2^(W-1) : 2^(W-1) - 1]

>   for (T i = 0; i <= N; i++)  //   i    is in [     0   : 2^(W-1) - 1]

>     A[i + 43] = ...           // i + 43 is in [    43   : 2^(W-1) + 42] which is non-wrapping modulo 2^W


Should the expression i + 43 not also be modeled with signed arithmetic? Which means it is expected to be smaller than 2^(W-1)?

Best,
Tobias


http://reviews.llvm.org/D9099

EMAIL PREFERENCES
  http://reviews.llvm.org/settings/panel/emailpreferences/