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
