[cfe-dev] New division by zero check

[Jordan Rose]

Checkers don't have direct access to the ranges, at least not currently, but you can evaluate 'x' using ProgramState::assume and see if the false-state is invalid. That means we already know x is non-zero.

Jordan


On Mar 27, 2014, at 6:56 , Anders Rönnholm <Anders.Ronnholm at evidente.se> wrote:

> One specific question, in the following example.
> 
> if (x > 3)
>  var = 77 / x;
> if (x == 0){}
> 
> When i reach the division in my check, the ProgramState knows that x is greater than 3. I can see this in the ProgramState dump. But how do i access the range in my check?
> 
> //Anders
> .......................................................................................................................
> Anders Rönnholm Senior Engineer
> Evidente ES East AB  Warfvinges väg 34  SE-112 51 Stockholm  Sweden
> 
> Mobile:                    +46 (0)70 912 42 54
> E-mail:                    Anders.Ronnholm at evidente.se
> 
> www.evidente.se
> 
> ________________________________________
> Från: Jordan Rose [jordan_rose at apple.com]
> Skickat: den 19 mars 2014 04:05
> Till: Anders Rönnholm
> Cc: cfe-dev at cs.uiuc.edu
> Ämne: Re: [cfe-dev] New division by zero check
> 
> Sorry, this did slip my queue. Thanks for the ping.
> 
> On Mar 17, 2014, at 4:55 , Anders Rönnholm <Anders.Ronnholm at evidente.se<mailto:Anders.Ronnholm at evidente.se>> wrote:
> 
> One idea we came up with is that while doing this as a fully general check is hard, it's probably worth checking this in the very simple case of straight-line code, where the division or the dereference happens in the same CFG block as the test. I still don't know if you > want to do this as a CFG walk (with lots of care taken for the variable changing in between the use and the check) or as a full analyzer checker, and we haven't really worked out any of the details, but it does seem to be more feasible than the general check while still > being immediately useful.
> 
> How do i restrict my checker to the same CFG block? No i don't intend to do a CFG walk, the variable has to be untouched between division and test. Will i have to check on each assignment that my variable isn't modified or is there an easier way? Is it SymbolRef that should be stored and matched against to follow changes on the variable?
> 
> Oh right. I didn't reply because I didn't have a good answer. :-) The best idea I can come up with is to walk backwards through the ExplodedGraph (from the predecessor node) and see what happens first: the variable is assumed non-zero because it was used in a division, or we hit a BlockEntrance program point. There are a few problems with that:
> 
> - The backwards walk is unbounded. It probably won't be that large, but it's not actually limited by anything.
> - We unique nodes in the ExplodedGraph (which is why it's a graph rather than a tree). This may not be an issue in practice: if two nodes are joined, they have the same state and the same program point, and that doesn't usually happen along two different paths except when you're joining up after a branch anyway.
> 
> The "obvious" thing to do would be to store the CFG block where a variable was assumed to be non-zero inside the state. The problem there is that then you've lost any chance of paths joining up, which means more work for the analyzer.
> 
> I'm not quite sure what the right thing is to do. It would be possible to have some kind of "per-CFG-block cache" in the ProgramState that gets cleared when we hit a transition point, either by having a special flag in the ProgramStateTrait or by adding a checker callback for BlockExit (or BlockEdge, or BlockEntrance...whatever's easiest). I haven't thought through either of these approaches, but neither of them strikes me as particularly clean. Perhaps there are other ways to solve the problem?
> 
> Anyway, I'm happy to answer specific questions, but as far as a more concrete design goes I'm not really any further along than you are.
> 
> Jordan