On Fri, May 24, 2019 at 12:27 AM Eric Botcazou <ebotca...@adacore.com> wrote:
>
> > While I agree that symbolic ranges are a complication and that most
> > cases it currently handles are not "value-range" things I do not agree
> > with the idea that we can simply remove handling them and deal
> > with the fallout in some later point in the future.  Eric may also be
> > able to show you "real" symbolic value-range magic.
>
> There are a couple of testcases in the testsuite that, I believe, require a
> minimal form of support for symbolic ranges: gcc.dg/tree-ssa/vrp94.c and
> gnat.dg/opt40.adb.  They deal with the following pattern in C:

And modified a bit in the quoting

>   if (x > y)
>     return 1;
>
>   z = y - x;
     z = z - 1;
>   if (z < 0)
>     abort ();

otherwise it would be just forming a relation and then using
the relational information when deriving a range for z = y - x.

It's of course still possible to derive z = [1, +INF] from the
relation and the op...

so eventually the representation of symbolic ranges as ranges
isn't really necessary (or we need even more obscure testcases
showing that).  But tracking relations alongside VRP and using
them for deriving ranges is quite important.

Richard.

>   return z;
>
> where we want to eliminate the abort.  Of course the C version doesn't really
> make sense on its own, but it's the translation of the Ada version where the
>
>   if (z <= 0)
>     abort ();
>
> is generated by the compiler (it's a range check in Ada parlance).
>
> I also agree that symbolic ranges are a complication but I don't understand
> why they would conceptually be treated differently from literal ranges.  Of
> course things may been different practically speaking because I also agree
> that they are of lesser importance than literal ranges in most cases.
>
> > Note that symbolic ranges are already restricted to PLUS_EXPR
> > and MINUS_EXPR (and NEGATE_EXPR I think).  There are
> > also "symbolic" (non-integer constant) ranges like [&a, &a].
>
> Yes, the current implementation is restricted to additive operations.
>
> --
> Eric Botcazou

Reply via email to