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
