Re: [PATCH] Keep lattice abstract in the SSA propagator, substitue lattice values at defs

[Richard Guenther <rguenther@suse.de>]

On Wed, 4 Aug 2010, Arnaud Charlet wrote:

> > > > Bootstrapped and tested on x86_64-unknown-linux-gnu.  c52102b
> > > > and c52102d now fail, because they rely on undefined signed integer
> > > > overflow.
> > > 
> > > Ada ACATS tests do not rely on signed integer overflow: Ada has built-in
> > > overflow checks as part of the language, but this capability requires the
> > > -gnato switch.
> > > 
> > > If these tests are failing, it means the -gnato switch is missing on these
> > > tests.
> > > 
> > > Can you please fix that by updating
> > > gcc/testsuite/ada/acats/overflow.lst ?
> > > Thanks in advance.
> > 
> > Adding -gnato doesn't fix the testcases (checked c52102b).
> 
> Well, then there's something fishy here that needs to be investigated, can you
> expand on why these tests "rely on undefined signed integer overflow" ?

I looked at the VRP dump and it derives perfectly valid assumptions.
From

  <various bounds checking concludes ident_int_2_12 is [1, 4]
   and ident_int_1_10 is [1, 4]>

<bb 15>:
  D.2465_155 = ident_int_2_12 + 1;
  L27b_156 = D.2465_155 - ident_int_1_10;
  L29b_159 = L27b_156 + 1;

<bb 16>:
  # L29b_363 = PHI <L29b_159(15), 1(14)>
...

  and we arrive with [-3, 9] for prephitmp.53_302 and [-1, 5] for L29b_363

  if (prephitmp.53_302 > L29b_363)
    goto <bb 27>;

<bb 27>:

  thus we can conclude that prephitmp.53_302 is [0, 9] here.
  The following statement then produces a range of [2147483647, overflow].
  So we happily substitute a constant value of 2147483647 for D.2544_253.

  D.2544_253 = prephitmp.53_302 + 2147483647;
  D.2553_254 = (size_type) D.2544_253;
...
  D.2554_257 = D.2553_254 + 1;


Richard.