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

[David Malcolm <dmalcolm@redhat.com>]

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