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

[Johannes Doerfert]

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

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


http://reviews.llvm.org/D9099

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