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

[Shengyu Huang <kumom.huang@gmail.com>]

[-- 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