Re: Constraints and branching in -fanalyzer
To be clear, I only solved the lesser problem if(idx-- > 0) __analyzer_eval(idx >= 0); which is a stepping stone problem. I correctly surmised that this was failing (with the prefix operator and -= operator working as expected) because the condition that is constrainted in the postfix problem is the old value for idx while the condition being evaluated is the new value. I can send you a patch, but the short version is the initial value of idx is constrained, then a binop_svalue is stored and eventually ends up in __analyzer_eval. Adding a case in constraint_manager::eval_condition to take apart binop svalues and recur the way you are imagining would be necessary is basically all that is needed to solve that one. Currently, the constraint_manager is just looking at that binop_svalue and determining it does not know any rules for it, because the rule it knows about is actually for one of its arguments. I was hoping this would be it for the original loop problem, but like I said, it goes from saying "UNKNOWN" twice to saying "TRUE UNKNOWN" which I found out happens for the other operators in a for loop as well. The first true is my binop_svalue handler, but the second UNKNOWN is the merging of the bottom of the loop back with the entry point. Since that is fairly abstract, when I found the case I told you about, I decided to see if I could fix it, because merging >0 with =0 into >=0 for a linear CFG should not be too hard. Sent with ProtonMail Secure Email. ‐‐‐ Original Message ‐‐‐ On Saturday, February 20, 2021 12:42 PM, David Malcolm wrote: > [Moving this discussion from offlist to the GCC mailing list (with > permission) and tweaking the subject] > > On Sat, 2021-02-20 at 02:57 +, brian.sobulefsky wrote: > > > Yeah, its a lot to take in. For the last one, it was just about > > storing and retrieving data and I ignored everything else about the > > analyzer, and that was hard enough. > > Well done on making it this far; I'm impressed that you're diving into > some of the more difficult aspects of this code, and seem to be coping. > > > I am working on PR94362, which originates from a false positive found > > compiling openssl. It effectivly amounted to not knowing that idx >= > > 0 within the loop for(; idx-- >0 ;). > > It turns out there are two problems here. One has to do with the > > postfix operator, and yes, the analyzer currently does not know that > > i >= 0 within an if block like if(idx-- > 0). That problem was easy > > and I got it to work within a few days with a relatively simple > > patch. I thought I was going to be submitting again. > > The second part is hard. It has to do with state merging and has > > nothing to do with the postfix operator. It fails for all sorts of > > operators when looping. In fact, the following fails: > > if(idx < 0) > > idx = 0; > > __analyzer_eval(idx >= 0); > > which is devastating if you are hoping the analyzer can "understand" > > a loop. Even with my first fix (which gives one TRUE when run on a > > for loop), there is the second "iterated" pass, which ends up with a > > widening_svalue (I'm still trying to wrap my head around that one > > too), that gives an UNKNOWN > > FWIW "widening" in this context is taken from abstract interpretation; > see e.g. the early papers by Patrick and Radhia Cousot; the idea is to > jump ahead of an infinitely descending chain of values to instead go > directly to a fixed point in a (small) finite number of steps. (I've > not attempted the narrowing approach, which refines it further to get a > tighter approximation). > > > So I am trying to follow how states are merged, but that means I need > > to at least sort of understand the graphs. I do know that the actual > > merging follows in the PK_AFTER_SUPERNODE branch, with the call to > > node->on_edge, which eventually gets you to maybe_update_for_edge and > > the for_each_fact iterator. > > I have spent far too many hours poring over graph dumps from the > analyzer, and yes, grokking the state merging is painful, and I'm sure > there are many bugs. > > Are you familiar with the various dump formats for the graph? In > particular the .dot ones? FWIW I use xdot.py for viewing them: > https://github.com/jrfonseca/xdot.py > (and indeed am the maintainer of the Fedora package for it); it has a > relatively quick and scalable UI for navigating graphs, but at some > point even it can't cope. > I started writing a dedicated visualizer that uses some of xdot.py's > classes: > https://github.com/davidmalcolm/gcc-analyzer-viewer > but it's early days for that. > > > I watched a merge in the debugger yesterday for the if example above > > and watched the unknown_svalues be made for the merged state, but it > > was still too much to take in all at once for me to know where the > > solution is. > > One other nasty problem with the state merging code is that any time I > touch it, there are knock-on effects where other things break (e.g. > loop analysis stops conve
Re: Constraints and branching in -fanalyzer
I can post it to the patches list with an explanation that it is not a full solution to the PR. I actually put the logic directly into constraint_manager::eval_condition when I was experimenting but I think I will make a new subroutine for you for "folding" constraints. It is not overly complicated, but there are a lot of cases based on whether the binop_svalue is on the right or left of the eval operator, and whether the value we recur on is on the left or right in the binop. A new subroutine can be a place for folding other svalues, such as unaryop or widening. As of now, for example, if we have a constraint on an svalue s, and ask about the same constraint on a unaryop svalue u_s with operator NOP, there is no reason to expect the right answer from the constraint manager. Sent with ProtonMail Secure Email. ‐‐‐ Original Message ‐‐‐ On Monday, February 22, 2021 5:57 PM, David Malcolm wrote: > On Sun, 2021-02-21 at 05:27 +, brian.sobulefsky wrote: > > > To be clear, I only solved the lesser problem > > if(idx-- > 0) > > __analyzer_eval(idx >= 0); > > which is a stepping stone problem. I correctly surmised that this was > > failing > > (with the prefix operator and -= operator working as expected) > > because the > > condition that is constrainted in the postfix problem is the old > > value for idx > > while the condition being evaluated is the new value. I can send you > > a patch, > > but the short version is the initial value of idx is constrained, > > then a binop_svalue > > is stored and eventually ends up in __analyzer_eval. Adding a case in > > constraint_manager::eval_condition to take apart binop svalues and > > recur > > the way you are imagining would be necessary is basically all that is > > needed > > to solve that one. Currently, the constraint_manager is just looking > > at > > that binop_svalue and determining it does not know any rules for it, > > because > > the rule it knows about is actually for one of its arguments. > > I was hoping this would be it for the original loop problem, but like > > I said, > > it goes from saying "UNKNOWN" twice to saying "TRUE UNKNOWN" which I > > found out happens for the other operators in a for loop as well. The > > first > > true is my binop_svalue handler, but the second UNKNOWN is the > > merging of > > the bottom of the loop back with the entry point. > > Since that is fairly abstract, when I found the case I told you > > about, > > I decided to see if I could fix it, because merging >0 with =0 into > > > > > =0 > > > for a linear CFG should not be too hard. > > I think it's probably best if you post the patch that you have so far > (which as I understand it fixes the non-looping case), since it sounds > like a useful base to work from. > > Thanks > Dave > > > ‐‐‐ Original Message ‐‐‐ > > On Saturday, February 20, 2021 12:42 PM, David Malcolm < > > dmalc...@redhat.com> wrote: > > > > > [Moving this discussion from offlist to the GCC mailing list (with > > > permission) and tweaking the subject] > > > On Sat, 2021-02-20 at 02:57 +, brian.sobulefsky wrote: > > > > > > > Yeah, its a lot to take in. For the last one, it was just about > > > > storing and retrieving data and I ignored everything else about > > > > the > > > > analyzer, and that was hard enough. > > > > > > Well done on making it this far; I'm impressed that you're diving > > > into > > > some of the more difficult aspects of this code, and seem to be > > > coping. > > > > > > > I am working on PR94362, which originates from a false positive > > > > found > > > > compiling openssl. It effectivly amounted to not knowing that idx > > > > > > > > > = > > > > > 0 within the loop for(; idx-- >0 ;). > > > > > It turns out there are two problems here. One has to do with the > > > > > postfix operator, and yes, the analyzer currently does not know > > > > > that > > > > > i >= 0 within an if block like if(idx-- > 0). That problem was > > > > > easy > > > > > and I got it to work within a few days with a relatively simple > > > > > patch. I thought I was going to be submitting again. > > > > > The second part is hard. It has to do with state merging and has > > > > > nothing to do with the postfix operator. It fails for all sorts > > > > > of > > > > > operators when looping. In fact, the following fails: > > > > > if(idx < 0) > > > > > idx = 0; > > > > > __analyzer_eval(idx >= 0); > > > > > which is devastating if you are hoping the analyzer can > > > > > "understand" > > > > > a loop. Even with my first fix (which gives one TRUE when run on > > > > > a > > > > > for loop), there is the second "iterated" pass, which ends up > > > > > with a > > > > > widening_svalue (I'm still trying to wrap my head around that one > > > > > too), that gives an UNKNOWN > > > > > > FWIW "widening" in this context is taken from abstract > > > interpretation; > > > see e.g. the early papers by Patrick and Radhia Cousot; the idea is > > > to > > > jump ahead of an infinitely descen
Re: Constraints and branching in -fanalyzer
Hi, I have implemented the discussed change, bootstrapped, and run the testsuite. I would be submitting except to my disappointment I saw failures increase by 4. As it turns out, these "failures" are actually passes that had been marked "xfail" and "TRUE" "desired" in the testsuite. The items in question are in testsuite files gcc.dg/analyzer/operations.c and params.c. In particular operations.c is only partially fixed because, as I have described, I thus far have only added cases for PLUS and MINUS. As you can see in that test file, you have some tests involving multiplication and division. My question is, before bothering to submit would you like me to just add handlers for these? I guess it will save us a patch cycle. Also, your comment regarding overflows is well taken, but I think we should fix the overall problem first, then worry about the overflow corner case. Brian
Re: Constraints and branching in -fanalyzer
I'll send it. It is not too slow. I just figured I would try to fix the others but I get that it is easier for you to see changes in steps. Brian Sent with ProtonMail Secure Email. ‐‐‐ Original Message ‐‐‐ On Friday, February 26, 2021 8:36 AM, David Malcolm wrote: > On Fri, 2021-02-26 at 04:23 +, brian.sobulefsky wrote: > > > Hi, > > I have implemented the discussed change, bootstrapped, and run the > > testsuite. I > > would be submitting except to my disappointment I saw failures > > increase by 4. As > > it turns out, these "failures" are actually passes that had been > > marked "xfail" > > and "TRUE" "desired" in the testsuite. The items in question are in > > testsuite > > files gcc.dg/analyzer/operations.c and params.c. In particular > > operations.c > > is only partially fixed because, as I have described, I thus far have > > only added > > cases for PLUS and MINUS. As you can see in that test file, you have > > some tests > > involving multiplication and division. My question is, before > > bothering to > > submit would you like me to just add handlers for these? I guess it > > will save us > > a patch cycle. > > Can you post what you have so far? > > It's easier for me to understand a patch by looking at the patch, > rather than a description of a patch, if that makes sense. > > Is the issue that doing a full bootstrap&test cycle is too slow? If so > I'm fine with you posting preliminary patches for discussion if you're > upfront about the ones that haven't been through a full bootstrap&test > run. Also, would it help if you had access to the GCC compiler farm? > There are some very fast machines there. > > (that said, I'm meant to be taking a day off today so I ought to sign > off for now) > > Dave > > > Also, your comment regarding overflows is well taken, but I think we > > should fix > > the overall problem first, then worry about the overflow corner case. > > Brian
