Mm... ignore this for now please, I think I messed up the analysis by
hand. I will try again. Thanks!
On Wed, 17 Mar 2021 at 16:16, Erick Ochoa <eoc...@gcc.gnu.org> wrote:
>
> Hi Richard, I think I misunderstood yesterday's answer and deviated a
> little bit. But now I want to focus on this:
>
> > > * the process in GCC that generates the constraints for NULL works
> > > fine (i.e., feeding the constraints generated by GCC to an external
> > > solver should yield a conservatively correct answer) but the process
> > > that solves the constraints relaxes the solutions for the NULL
> > > constraint variable (i.e., GCC has deviated from the constraint
> > > solving algorithm somehow)
> >
> > No, that part should work OK.
> >
>
> So, let's ignore the other solver for now and instead focus on the
> concrete example I presented on the previous email. If GCC is solving
> these constraints:
>
> ```
> ANYTHING = &ANYTHING
> ESCAPED = *ESCAPED
> ESCAPED = ESCAPED + UNKNOWN
> *ESCAPED = NONLOCAL
> NONLOCAL = &NONLOCAL
> NONLOCAL = &ESCAPED
> INTEGER = &ANYTHING
> ISRA.4 = &NONLOCAL
> derefaddrtmp(9) = &NULL
> *ISRA.4 = derefaddrtmp(9)
> i = NONLOCAL
> i = &NONLOCAL
> ESCAPED = &NONLOCAL
> _2 = *ISRA.4
> ```
>
> What would a hand calculated solution gives us vs what was the
> solution given by GCC?
>
> I am following the algorithm stated on Section 3.3 of Structure
> Aliasing in GCC, and I will be ignoring the ESCAPED = ESCAPED +
> UNKNOWN constraint since there isn't any other field offset that needs
> to be calculated.
>
> First, I want to make some adjustments. I am going to be using "=" to
> signify the \supseteq symbol and I will be adding curly braces to
> specify the element in a set as opposed to the whole set. Therefore
> the constraints will now become (ordered slightly differently):
>
> ```
> ====direct contraints========
> ANYTHING = { ANYTHING }
> ESCAPED = { NONLOCAL }
> NONLOCAL = { NONLOCAL }
> NONLOCAL = { ESCAPED }
> INTEGER = { ANYTHING }
> ISRA.4 = { NONLOCAL }
> derefaddrtmp(9) = { NULL }
> i = { NONLOCAL }
>
> ====complex constraints======
> ESCAPED = *ESCAPED
> *ESCAPED = NONLOCAL
> *ISRA.4 = derefaddrtmp(9)
> _2 = *ISRA.4
>
> ===== copy-constraints======
> ESCAPED = ESCAPED // again ignoring the + UNKNOWN since I don't think
> it will matter...
> i = NONLOCAL
> ```
>
> Solution sets are basically the direct constraints at the moment.
>
> Let's now create the graph
>
> 1. node ESCAPED has an edge going to itself (due to the copy constraint)
> 2. node ISRA.4 has no outgoing copy edges
> 3. node derefaddrtmp(9) has no outgoing edges
> 4. node _2 has no outgoing edges
> 5. node i has an outgoing edge to NONLOCAL (due to the copy constraint)
> 6. node NONLOCAL has no outgoing edge
>
> Now, we can iterate over this set of nodes
>
> 1. Walking over node ESCAPED. Sol(ESCAPED) = {NONLOCAL}. There are no
> edges, but it has complex-constraints. Let's modify the graph.
> 1. Looking at ESCAPED = *ESCAPED we note that we need to add a copy
> edge from ESCAPED to NONLOCAL.
> 2. Looking at *ESCAPED = NONLOCAL we note that we need to add a copy
> edge from NONLOCAL to NONLOCAL
>
> The graph is now transformed to
>
> 1. node ESCAPED has an edge going to ESCAPED and NONLOCAL
> 2. node ISRA.4 has no outgoing copy edges
> 3. node derefaddrtmp(9) has no outgoing edges
> 4. node _2 has no outgoing edges
> 5. node i has an outgoing edge to NONLOCAL (due to the copy constraint)
> 6. node NONLOCAL has an edge going to NONLOCAL
>
> The solution set of escaped is now Sol(ESCAPED) = Sol(ESCAPED) U
> Sol(NONLOCAL) = {NONLOCAL, ESCAPED}
>
> Now we continue walking
>
> 2. Walking over node ISRA.4. It has the solution set { NONLOCAL }.
> There are no edges, but it has complex-constraints. Let's modify the
> graph.
> 1. Looking at *ISRA.4 = derefaddrtmp(9), we note that we need to add
> a copy edge from NONLOCAL to derefaddrtmp(9).
>
> The graph is now transformed to
>
> 1. node ESCAPED has an edge going to ESCAPED and NONLOCAL
> 2. node ISRA.4 has no outgoing copy edges
> 3. node derefaddrtmp(9) has no outgoing edges
> 4. node _2 has no outgoing edges
> 5. node i has an outgoing edge to NONLOCAL (due to the copy constraint)
> 6. node NONLOCAL has an edge going to NONLOCAL, derefaddrtmp(9)
>
> The Sol(NONLOCAL) = Sol(NONLOCAL) U Sol(derefaddrtmp(9)) = {NONLOCAL,
> ESCAPED, NULL}.
>
> Now I could continue, but here is already something that is not shown
> in the points-to sets in the dump. It shows that
>
> NONLOCAL = {NONLOCAL, ESCAPED, NULL}
>
> Looking at the data that I showed yesterday:
>
> ```
> NONLOCAL = { ESCAPED NONLOCAL } same as i
> ```
>
> we see that NULL is not in the solution set of NONLOCAL.
>
> Now, yesterday you said that NULL is not conservatively correctly
> represented in the constraints. You also said today the points-to
> analysis should be solving the constraints fine. What I now understand
> from this is that while NULL may be pointed to by some constraints, it
> doesn't mean that not being on the set means that a pointer will not
> point to NULL. However, it should still be shown in the dumps where
> the points-to sets are shown for the constraint variables since it is
> solved using the same analysis? Is this correct? Am I doing the points
> to analysis by hand wrong somehow? Why would NULL not be in
> Sol(NONLOCAL) if it is solving the same constraints that I am solving
> by hand?
