
<html><head><meta http-equiv="Content-Type" content="text/html charset=windows-1252"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;"><div>Sorry, this did slip my queue. Thanks for the ping.</div><br><div><div>On Mar 17, 2014, at 4:55 , Anders Rönnholm <<a href="mailto:Anders.Ronnholm@evidente.se">Anders.Ronnholm@evidente.se</a>> wrote:</div><br class="Apple-interchange-newline"><blockquote type="cite"><blockquote type="cite">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.<br><br></blockquote>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?<br></blockquote><div><br></div><div>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:</div><div><br></div><div>- The backwards walk is unbounded. It probably won't be that large, but it's not actually limited by anything.</div><div>- 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 <i>except</i> when you're joining up after a branch anyway.</div><div><br></div><div>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.</div><div><br></div><div>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?</div><div><br></div><div>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.</div><div><br></div><div>Jordan</div></div></body></html>