[Static Analyzer] Loop handling - False positive for malloc-sm

[Static Analyzer] Loop handling - False positive for malloc-sm

[Pierrick Philippe]

[-- Attachment #1: Type: text/plain, Size: 2868 bytes --]

Hi everyone,

I'm still playing around with the analyzer, and wanted to have a look at 
loop handling.
I'm using a build from /trunk/ branch (/20230309/).

Here is my analyzed code:

'''
1| #include <stdlib.h>
2| int main(void) {
3|    void * ptr = malloc(sizeof(int));
4|    for (int i = 0; i < 10; i++) {
5|        if (i == 5) free(ptr);
6|    }
7|}
'''

And here, the malloc-sm is reporting a double-free on line 5 with a 
quite confusing output:

'''
./test.c: In function ‘main’:
./test.c:5:21: warning: double-‘free’ of ‘ptr’ [CWE-415] 
[-Wanalyzer-double-free]
     5 |         if (i == 5) free(ptr);
        |                         ^~~~~~~~~
   ‘main’: events 1-13
     |
     |   3 |     void * ptr = malloc(sizeof(int));
     |      |                        ^~~~~~~~~~~~~~~~~~~
     |      |                        |
     |      |                        (1) allocated here
     |   4 |     for (int i = 0; i < 10; i++) {
     |      |                         ~~~~  ~~~
     |      |                         |            |
     |      |                         |            (5) ...to here
     |      |                         (2) following ‘true’ branch (when 
‘i <= 9’)...
     |      |                         (6) following ‘true’ branch (when 
‘i <= 9’)...
     |      |                         (9) following ‘true’ branch (when 
‘i <= 9’)...
     |   5 |         if (i == 5) free(ptr);
     |      |            ~           ~~~~~
     |      |            |             |
     |      |            |             (8) first ‘free’ here
     |      |            |             (12) ...to here
     |      |            |             (13) second ‘free’ here; first 
‘free’ was at (8)
     |      |            (3) ...to here
     |      |            (4) following ‘false’ branch (when ‘i != 5’)...
     |      |            (7) ...to here
     |      |            (10) ...to here
     |      |            (11) following ‘true’ branch (when ‘i == 5’)...
     |
'''

So, I'm guessing that this false positive is due to how the analyzer is 
handling loops.
Which lead to my question: how are loops handled by the analyzer?

Thanks for your time,

Pierrick

Re: [Static Analyzer] Loop handling - False positive for malloc-sm

[David Malcolm]

On Mon, 2023-03-20 at 13:28 +0100, Pierrick Philippe wrote:
> Hi everyone,
> 
> I'm still playing around with the analyzer, and wanted to have a look
> at 
> loop handling.
> I'm using a build from /trunk/ branch (/20230309/).
> 
> Here is my analyzed code:
> 
> '''
> 1| #include <stdlib.h>
> 2| int main(void) {
> 3|    void * ptr = malloc(sizeof(int));
> 4|    for (int i = 0; i < 10; i++) {
> 5|        if (i == 5) free(ptr);
> 6|    }
> 7|}
> '''
> 
> And here, the malloc-sm is reporting a double-free on line 5 with a 
> quite confusing output:
> 
> '''
> ./test.c: In function ‘main’:
> ./test.c:5:21: warning: double-‘free’ of ‘ptr’ [CWE-415] 
> [-Wanalyzer-double-free]
>      5 |         if (i == 5) free(ptr);
>         |                         ^~~~~~~~~
>    ‘main’: events 1-13
>      |
>      |   3 |     void * ptr = malloc(sizeof(int));
>      |      |                        ^~~~~~~~~~~~~~~~~~~
>      |      |                        |
>      |      |                        (1) allocated here
>      |   4 |     for (int i = 0; i < 10; i++) {
>      |      |                         ~~~~  ~~~
>      |      |                         |            |
>      |      |                         |            (5) ...to here
>      |      |                         (2) following ‘true’ branch
> (when 
> ‘i <= 9’)...
>      |      |                         (6) following ‘true’ branch
> (when 
> ‘i <= 9’)...
>      |      |                         (9) following ‘true’ branch
> (when 
> ‘i <= 9’)...
>      |   5 |         if (i == 5) free(ptr);
>      |      |            ~           ~~~~~
>      |      |            |             |
>      |      |            |             (8) first ‘free’ here
>      |      |            |             (12) ...to here
>      |      |            |             (13) second ‘free’ here; first
> ‘free’ was at (8)
>      |      |            (3) ...to here
>      |      |            (4) following ‘false’ branch (when ‘i !=
> 5’)...
>      |      |            (7) ...to here
>      |      |            (10) ...to here
>      |      |            (11) following ‘true’ branch (when ‘i ==
> 5’)...
>      |
> '''
> 
> So, I'm guessing that this false positive is due to how the analyzer
> is 
> handling loops.
> Which lead to my question: how are loops handled by the analyzer?

Sadly, the answer is currently "not very well" :/

I implemented my own approach, with a "widening_svalue" subclass of
symbolic value.  This is widening in the Abstract Interpretation sense,
(as opposed to the bitwise operations sense): if I see multiple values
on successive iterations, the widening_svalue tries to simulate that we
know the start value and the direction the variable is moving in.

This doesn't work well; arguably I should rewrite it, perhaps with an
iterator_svalue, though I'm not sure how it ought to work.  Some ideas:

* reuse gcc's existing SSA-based loop analysis, which I believe can
identify SSA names that are iterator variables, figure out their
bounds, and their per-iteration increments, etc.

* rework the program_point or supergraph code to have a notion of "1st
iteration of loop", "2nd iteration of loop", "subsequent iterations",
or similar, so that the analyzer can explore those cases differently
(on the assumption that such iterations hopefully catch the most
interesting bugs)

Dave

Re: [Static Analyzer] Loop handling - False positive for malloc-sm

[Pierrick Philippe]

On 21/03/2023 00:30, David Malcolm wrote:
> On Mon, 2023-03-20 at 13:28 +0100, Pierrick Philippe wrote:
>> Hi everyone,
>>
>> I'm still playing around with the analyzer, and wanted to have a look
>> at
>> loop handling.
>> I'm using a build from /trunk/ branch (/20230309/).
>>
>> Here is my analyzed code:
>>
>> '''
>> 1| #include <stdlib.h>
>> 2| int main(void) {
>> 3|    void * ptr = malloc(sizeof(int));
>> 4|    for (int i = 0; i < 10; i++) {
>> 5|        if (i == 5) free(ptr);
>> 6|    }
>> 7|}
>> '''
[stripping]
>> So, I'm guessing that this false positive is due to how the analyzer
>> is
>> handling loops.
>> Which lead to my question: how are loops handled by the analyzer?
> Sadly, the answer is currently "not very well" :/
>
> I implemented my own approach, with a "widening_svalue" subclass of
> symbolic value.  This is widening in the Abstract Interpretation sense,
> (as opposed to the bitwise operations sense): if I see multiple values
> on successive iterations, the widening_svalue tries to simulate that we
> know the start value and the direction the variable is moving in.
>
> This doesn't work well; arguably I should rewrite it, perhaps with an
> iterator_svalue, though I'm not sure how it ought to work.  Some ideas:
>
> * reuse gcc's existing SSA-based loop analysis, which I believe can
> identify SSA names that are iterator variables, figure out their
> bounds, and their per-iteration increments, etc.
>
> * rework the program_point or supergraph code to have a notion of "1st
> iteration of loop", "2nd iteration of loop", "subsequent iterations",
> or similar, so that the analyzer can explore those cases differently
> (on the assumption that such iterations hopefully catch the most
> interesting bugs)

I see, I don't know if you ever considered allowing state machines to 
deal with loops on their own.
Such as having an API to allow to register a callback to handle loops, 
but not in a mandatory way.
Or having a set of APIs to optionally implement for the analyzer to call.

It would allow state machines to analyze loops with the meaning of their 
inner analysis.

Which could allow them to try to find a fixed point in the loop 
execution which doesn't have
any impact on the program state for that state machine. Kind of like a 
custom loop invariant.
Because depending of the analysis goal of the state machine, you might 
need to symbolically execute the loop
only a few times before reentering the loop and having the entry state 
being the same as the end-of-loop state.

In fact, this could be done directly by the analyzer, and only calling 
state machine APIs for loop handling which still has not reached
such a fixed point in their program state for the analyzed loop, with a 
maximum number of execution fixed by the analyzer to limit execution time.

Does what I'm saying make sense?

In terms of implementation, loop detection can be done by looking for 
strongly connected components (SCCs)
in a function graph having more than one node.
I don't know if this is how it is already done within the analyzer or not?

Thank you for your time,

Pierrick

Re: [Static Analyzer] Loop handling - False positive for malloc-sm

[David Malcolm]

On Tue, 2023-03-21 at 09:21 +0100, Pierrick Philippe wrote:
> On 21/03/2023 00:30, David Malcolm wrote:
> > On Mon, 2023-03-20 at 13:28 +0100, Pierrick Philippe wrote:
> > > Hi everyone,
> > > 
> > > I'm still playing around with the analyzer, and wanted to have a
> > > look
> > > at
> > > loop handling.
> > > I'm using a build from /trunk/ branch (/20230309/).
> > > 
> > > Here is my analyzed code:
> > > 
> > > '''
> > > 1| #include <stdlib.h>
> > > 2| int main(void) {
> > > 3|    void * ptr = malloc(sizeof(int));
> > > 4|    for (int i = 0; i < 10; i++) {
> > > 5|        if (i == 5) free(ptr);
> > > 6|    }
> > > 7|}
> > > '''
> [stripping]
> > > So, I'm guessing that this false positive is due to how the
> > > analyzer
> > > is
> > > handling loops.
> > > Which lead to my question: how are loops handled by the analyzer?
> > Sadly, the answer is currently "not very well" :/
> > 
> > I implemented my own approach, with a "widening_svalue" subclass of
> > symbolic value.  This is widening in the Abstract Interpretation
> > sense,
> > (as opposed to the bitwise operations sense): if I see multiple
> > values
> > on successive iterations, the widening_svalue tries to simulate
> > that we
> > know the start value and the direction the variable is moving in.
> > 
> > This doesn't work well; arguably I should rewrite it, perhaps with
> > an
> > iterator_svalue, though I'm not sure how it ought to work.  Some
> > ideas:
> > 
> > * reuse gcc's existing SSA-based loop analysis, which I believe can
> > identify SSA names that are iterator variables, figure out their
> > bounds, and their per-iteration increments, etc.
> > 
> > * rework the program_point or supergraph code to have a notion of
> > "1st
> > iteration of loop", "2nd iteration of loop", "subsequent
> > iterations",
> > or similar, so that the analyzer can explore those cases
> > differently
> > (on the assumption that such iterations hopefully catch the most
> > interesting bugs)


I've filed an RFE discussing some of the problems with -fanalyzer's
loop-handling here:

  https://gcc.gnu.org/bugzilla/show_bug.cgi?id=109252

including the idea of making use of GCC's existing SSA-based loop
analysis (which discovers a tree of loops within each function's CFG).

> 
> I see, I don't know if you ever considered allowing state machines to
> deal with loops on their own.
> Such as having an API to allow to register a callback to handle
> loops, 
> but not in a mandatory way.
> Or having a set of APIs to optionally implement for the analyzer to
> call.

I hadn't thought of that, but it sounds like a reasonable idea.

> 
> It would allow state machines to analyze loops with the meaning of
> their 
> inner analysis.
> 
> Which could allow them to try to find a fixed point in the loop 
> execution which doesn't have
> any impact on the program state for that state machine. Kind of like
> a 
> custom loop invariant.
> Because depending of the analysis goal of the state machine, you
> might 
> need to symbolically execute the loop
> only a few times before reentering the loop and having the entry
> state 
> being the same as the end-of-loop state.

The analyzer performs symbolic execution; it tries to achieve a
reasonable balance between:
* precision of state tracking versus
* achieving decent coverage of code and data flow
* ensuring termination
via various heuristics.

Its current loop implementation uses widening_svalue and the complexity
limits on svalues/regions to attempt to have the symbolic execution
terminate due to hitting already-visited nodes in the exploded_graph,
or else hit per-program-point limits.  Unfortuately this often doesn't
work well.

GCC's optimization code has both GIMPLE and RTL loop analysis code. 
The RTL code runs too late for the analyzer, but the GIMPLE loop
analysis code is in cfgloop.{h,cc} and thus we would have access to
information about loops, at least for well-behaved cases - though
possibly only when optimization is enabled.

> 
> In fact, this could be done directly by the analyzer, and only
> calling 
> state machine APIs for loop handling which still has not reached
> such a fixed point in their program state for the analyzed loop, with
> a 
> maximum number of execution fixed by the analyzer to limit execution
> time.
> 
> Does what I'm saying make sense?

I think so, though I'm not sure how it would work in practice. 
Consider e.g. 

  for (int i = 0; i < n; i++)
     head = prepend_node (head, i);

which builds a chain of N dynamically-allocated nodes in a linked list.

> 
> In terms of implementation, loop detection can be done by looking for
> strongly connected components (SCCs)
> in a function graph having more than one node.
> I don't know if this is how it is already done within the analyzer or
> not?

It isn't yet done in the analyzer, but as noted above there is code in
GCC that already does that (in cfgloop.{h,cc}).

Dave

Re: [Static Analyzer] Loop handling - False positive for malloc-sm

[Pierrick Philippe]

On 22/03/2023 19:19, David Malcolm wrote:
> On Tue, 2023-03-21 at 09:21 +0100, Pierrick Philippe wrote:
[stripping]
>> In fact, this could be done directly by the analyzer, and only
>> calling
>> state machine APIs for loop handling which still has not reached
>> such a fixed point in their program state for the analyzed loop, with
>> a
>> maximum number of execution fixed by the analyzer to limit execution
>> time.
>>
>> Does what I'm saying make sense?
> I think so, though I'm not sure how it would work in practice.
> Consider e.g.
>
>    for (int i = 0; i < n; i++)
>       head = prepend_node (head, i);
>
> which builds a chain of N dynamically-allocated nodes in a linked list.

Well, that would be a case where the loop's analysis will depend of the 
state machine.
If we consider the malloc-sm, it would allow it to track as different 
pointers each allocated pointers, until the limit of symbolic execution 
imposed by the analyzer is reached, are the svalue of N if it is a known 
integer at the current analysis point.

For other, such as a the file-sm, it would only be needed to 
symbolically execute it once, assuming prepend_node() is not opening any 
files.
So this state machine would not have to be executed more than once on 
the loop at this program point by the analyzer.

I think the different steps for such a different cases of loop analysis, 
is somehow using the second point of the RFE you shared above.

The "algorithm" I came with when thinking about it looks like this.
Of course, I'm definitely not an expert on the analyzer, so it is 
possibly not feasible.

* Detect loop, and try to get the termination constraint (possibly 
reduced if possible).
* Iterate on the loops' node N:
     * If N is the loop's first node:
         * Check if the actual program state is in a sufficient state to 
satisfy the loop's termination constraint,
             If so, stop analyzing the loop
         * Otherwise, check if the maximum number of symbolic execution 
fixed by the analyzer is reached,
             If so, stop analyzing the loop
         * Otherwise, keep going
     * Call every sm still impacting their program state map on node N

This should work for loops iterating on integer, for other kind of 
loops, it might be trickier though.

>> In terms of implementation, loop detection can be done by looking for
>> strongly connected components (SCCs)
>> in a function graph having more than one node.
>> I don't know if this is how it is already done within the analyzer or
>> not?
> It isn't yet done in the analyzer, but as noted above there is code in
> GCC that already does that (in cfgloop.{h,cc}).

I definitely have to look at this files.

Thank you for your time,

Pierrick

Re: [Static Analyzer] Loop handling - False positive for malloc-sm

[Shengyu Huang]

[-- Attachment #1: Type: text/plain, Size: 2113 bytes --]

Hi Dave,

> I implemented my own approach, with a "widening_svalue" subclass of
> symbolic value.  This is widening in the Abstract Interpretation sense,
> (as opposed to the bitwise operations sense): if I see multiple values
> on successive iterations, the widening_svalue tries to simulate that we
> know the start value and the direction the variable is moving in.

I guess you are using interval domain? I haven’t played with abstract interpretation a lot, but I think the polyhedra domain is the more popular domain used (but more difficult to implement ofc). In a course project I did before, I remember switching to polyhedra domain from the interval domain allowed me to prove the properties I wanted to prove.

Also, are you using the same approach maybe to detect nontermination of loops? Maybe when you find out you have to widen the variable range to (minus) infinity?

> 
> This doesn't work well; arguably I should rewrite it, perhaps with an
> iterator_svalue, though I'm not sure how it ought to work.  Some ideas:
> 
> * reuse gcc's existing SSA-based loop analysis, which I believe can
> identify SSA names that are iterator variables, figure out their
> bounds, and their per-iteration increments, etc.
> 
> * rework the program_point or supergraph code to have a notion of "1st
> iteration of loop", "2nd iteration of loop", "subsequent iterations",
> or similar, so that the analyzer can explore those cases differently
> (on the assumption that such iterations hopefully catch the most
> interesting bugs)

I haven’t thought about how to do this properly in gcc, but maybe we can infer loop invariants (or even allow users to annotate loop invariants…but I guess it would change a lot of things outside the scope of current analyzer) that can help us do multiple checks for a loop. I have only seen this strategy used on the source level before, and I don’t know how difficult it will be to implement it on gimple…There is a paper I haven’t had the time to read but maybe you will find interesting: https://arxiv.org/pdf/1407.5286.pdf

Best,
Shengyu

Re: [Static Analyzer] Loop handling - False positive for malloc-sm

[David Malcolm]

On Tue, 2023-03-21 at 11:01 +0100, Shengyu Huang wrote:
> Hi Dave,
> 
> > I implemented my own approach, with a "widening_svalue" subclass of
> > symbolic value.  This is widening in the Abstract Interpretation
> > sense,
> > (as opposed to the bitwise operations sense): if I see multiple
> > values
> > on successive iterations, the widening_svalue tries to simulate
> > that we
> > know the start value and the direction the variable is moving in.
> 
> I guess you are using interval domain? I haven’t played with abstract
> interpretation a lot, but I think the polyhedra domain is the more
> popular domain used (but more difficult to implement ofc). In a
> course project I did before, I remember switching to polyhedra domain
> from the interval domain allowed me to prove the properties I wanted
> to prove.

Sorry if what I wrote was misleading: I'm not using abstract
interpretation per se; the analyzer is doing symbolic execution.  It
uses a worklist to explore the exploded_graph of (point, state) pairs,
but I have quite complicated state objects.

What I mean is that the widening_svalue is an abstraction, and the hope
is that it will get reused within the program_state object for
representing the state of the loop variant the next time through the
loop, and thus the program_state is the same as the previous iteration,
and thus we effectively have a cache hit within the exploded_graph (and
can terminate the analysis).  I see this as somewhat analogous to the
convergence that happens in an abstract interpretation approach, in
that we go from the:
  - initial value
  - widened to cover range from initial value up to +infinity
and thus (hopefully) terminate in two steps.

But it doesn't work very well, alas.

As noted in another thread, I've just filed:
  https://gcc.gnu.org/bugzilla/show_bug.cgi?id=109252
with some ideas on better ways of handling loops in the analyzer.

> 
> Also, are you using the same approach maybe to detect nontermination
> of loops? Maybe when you find out you have to widen the variable
> range to (minus) infinity?

For GCC 13 I've added a warning: -Wanalyzer-infinite-recursion
implemented in gcc/analyzer/infinite-recursion.cc which attempts to
detect infinite *recursions* based on states being too similar when
recursing: if nothing can have effectively changed, it's an infinite
recursion (for some definition of "effectively).

I'd hoped to implement something similar for *loop* detection, but it
didn't make feature freeze for GCC 13; see:
  https://gcc.gnu.org/bugzilla/show_bug.cgi?id=106147
The half-finished prototype I have works in a similar way to the
recursion detection: find loops such as:

for (int i = 0; i < 10; i++)
  for (int j = 0; j < 10; i++)
    {
    }

where due to the copy-and-paste error of reusing "i++", "j" never
changes after entering the inner loop, and we never leave it.

> 
> > 
> > This doesn't work well; arguably I should rewrite it, perhaps with
> > an
> > iterator_svalue, though I'm not sure how it ought to work.  Some
> > ideas:
> > 
> > * reuse gcc's existing SSA-based loop analysis, which I believe can
> > identify SSA names that are iterator variables, figure out their
> > bounds, and their per-iteration increments, etc.
> > 
> > * rework the program_point or supergraph code to have a notion of
> > "1st
> > iteration of loop", "2nd iteration of loop", "subsequent
> > iterations",
> > or similar, so that the analyzer can explore those cases
> > differently
> > (on the assumption that such iterations hopefully catch the most
> > interesting bugs)
> 
> I haven’t thought about how to do this properly in gcc, but maybe we
> can infer loop invariants (or even allow users to annotate loop
> invariants…but I guess it would change a lot of things outside the
> scope of current analyzer) that can help us do multiple checks for a
> loop. I have only seen this strategy used on the source level before,
> and I don’t know how difficult it will be to implement it on
> gimple…There is a paper I haven’t had the time to read but maybe you
> will find interesting: https://arxiv.org/pdf/1407.5286.pdf

Thanks!
Dave

Re: [Static Analyzer] Loop handling - False positive for malloc-sm

[Shengyu Huang]

[-- Attachment #1: Type: text/plain, Size: 626 bytes --]

Hi Dave,

> On 21 Mar 2023, at 00:30, David Malcolm via Gcc <gcc@gcc.gnu.org> wrote:
> 
> I implemented my own approach, with a "widening_svalue" subclass of
> symbolic value.  This is widening in the Abstract Interpretation sense,
> (as opposed to the bitwise operations sense): if I see multiple values
> on successive iterations, the widening_svalue tries to simulate that we
> know the start value and the direction the variable is moving in.

I forgot to mention there is a relevant section “path selection” in the paper I mentioned several times (https://users.ece.cmu.edu/~aavgerin/papers/Oakland10.pdf).