https://gcc.gnu.org/bugzilla/show_bug.cgi?id=105346
--- Comment #14 from Aldy Hernandez <aldyh at gcc dot gnu.org> ---
(In reply to Richard Biener from comment #13)
> (In reply to Andrew Macleod from comment #11)
> > (In reply to Richard Biener from comment #6)
> >
> > >
> > > <bb 2> :
> > > bufp_2 = &buf;
> > > if (&buf != bufp_2)
> > > goto <bb 3>; [INV]
> > > else
> > > goto <bb 4>; [INV]
> > >
> > > <bb 3> :
> > > __builtin_free (bufp_2);
> > >
> > > and for the stmt __builtin_free (bufp_2) I'd like to ask if we know
> > > that bufp_2 is != &buf (I'd expect a 'true' answer). I think the
> > > relation oracle should be able to answer this but I can't find the
> > > appropriate API to use for this?
> >
> > - The relation oracle currently only works with ssa-names.
> > - Ranger also doesn't currently track that sort of symbolic equivalence with
> > irange.
> > - the VRP passes have a pointer tracking mechanism as part of the dom walk,
> > and the call to rvrp_folder::value_of_expr (bufp_2) would give us &buf. I
> > also think we also would fold the stmt in VRP. This could in theory be
> > extended to any pass doing a dom walk. however:
> > - I believe the upcoming prange extension for pointer ranges in stage 1 will
> > make this happen naturally with rangers query system. range_of_stmt ( if
> > <..>) would then produce bool [0, 0]. I would also expect that prange will
> > have an easy way to ask what its base/equivalence(s) are.
>
> OK, I was hoping I can so sth like
>
> range_simplify_expr (NE_EXPR, bufp_2, &buf, at_free_stmt);
>
> and then by means of the dominating if condition get a 'true'. Note the
> diagnostic pass is not within a DOM walk so all I can use is an ad-hoc
> query. I'm not looking to simplify the conditional itself as that won't
> help me with the current pass structure.
Hmmm, I suppose we could track inequality as well as equality in prange. In
which case, we'd have:
=========== BB 2 ============
Imports: bufp_2
Exports: bufp_2
<bb 2> :
bufp_2 = &buf;
if (&buf != bufp_2)
goto <bb 3>; [INV]
else
goto <bb 4>; [INV]
bufp_2 : [prange] char[20] * [1B, +INF] [PT &buf]
2->3 (T) bufp_2 : [prange] char[20] * [1B, +INF] [PT !&buf]
2->4 (F) bufp_2 : [prange] char[20] * [1B, +INF] [PT &buf]
=========== BB 3 ============
bufp_2 [prange] char[20] * [1B, +INF] [PT !&buf]
<bb 3> :
free (bufp_2);
Notice that the range of bufp_2 at free() is:
bufp_2 [prange] char[20] * [1B, +INF] [PT !&buf]
Whereas range_of_expr of &buf (anywhere) would be:
[prange] char[20] * [1B, +INF] [PT &buf]
The intersection of both is the empty set / UNDEFINED, and should be able to
get that without dominance info.
Would that help?
Right now we're tracking equality, but it should be trivial to track
non-equality by adjusting the op1_range range-op entries.
