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

[Pierrick Philippe <pierrick.philippe@irisa.fr>]

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