<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>Hi, Anders. RecursiveASTVisitor isn't going to handle what you want here: you need something at least flow-sensitive (to know that the if-check actually follows the division) if not path-sensitive (to know that the value hasn't changed since you divided). The thing is, the analyzer's not actually good at answering questions of the form "does X occur on all paths through a function?". There are two reasons for this: first, the analyzer's model of C/C++ is known to be incomplete (e.g. we don't model catching exceptions), and second, we have a performance optimization that says if a function is called and we decide to inline it, we won't analyze it again as top level, which means we're usually not seeing the fully general case.</div><div><br></div><div>The next problem is that this can contribute to state explosion: where before we might have been able to merge two paths where a division only happens on one, we'd now be forced to treat them as separate because the denominator is marked along one path.</div><div><br></div><div>Ted, Anna, and I have actually talked about this kind of check, not so much for divide-by-zero as for null dereferences. (I forget what we were calling this; something like an "inverted null check", because the check and the dereference are backwards.) This is actually a real security issue a lot of the time; see John Regehr's blog post at <a href="http://blog.regehr.org/archives/970">http://blog.regehr.org/archives/970</a>.</div><div><br></div><div>(It's fun to see Xi Wang cited; he was an LLVM contributor for a while several years ago.)</div><div><br></div><div>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.</div><div><br></div><div>Let me know if you have any more questions!</div><div>Jordan</div><div><br></div><br><div><div>On Jan 22, 2014, at 7:18 , 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"><div lang="SV" link="blue" vlink="purple" style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant: normal; font-weight: normal; letter-spacing: normal; line-height: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;"><div class="WordSection1" style="page: WordSection1;"><div style="margin: 0cm 0cm 0.0001pt; font-size: 11pt; font-family: Calibri, sans-serif;"><span lang="EN-US" style="">Hi,</span><span style=""><o:p></o:p></span></div><div style="margin: 0cm 0cm 0.0001pt; font-size: 11pt; font-family: Calibri, sans-serif;"><span lang="EN-US" style=""> </span><span style=""><o:p></o:p></span></div><div style="margin: 0cm 0cm 0.0001pt; font-size: 11pt; font-family: Calibri, sans-serif;"><span lang="EN-US" style="">There is a division by zero check where the denominator value is already known. I would like some feedback on a new static check for division by zero I intend to write where the value isn’t known yet.<o:p></o:p></span></div><div style="margin: 0cm 0cm 0.0001pt; font-size: 11pt; font-family: Calibri, sans-serif;"><span lang="EN-US" style=""> <o:p></o:p></span></div><div style="margin: 0cm 0cm 0.0001pt; font-size: 11pt; font-family: Calibri, sans-serif;"><span lang="EN-US" style="">It shall catch scenarios where the division is made before checking it against a value. To start with it will have to be directly after the division.<o:p></o:p></span></div><div style="margin: 0cm 0cm 0.0001pt; font-size: 11pt; font-family: Calibri, sans-serif;"><span lang="EN-US" style=""> <o:p></o:p></span></div><div style="margin: 0cm 0cm 0.0001pt; font-size: 11pt; font-family: Calibri, sans-serif;"><span lang="EN-US" style="">e.g<o:p></o:p></span></div><div style="margin: 0cm 0cm 0.0001pt; font-size: 11pt; font-family: Calibri, sans-serif;"><span lang="EN-US" style="">x = 100 / y;<o:p></o:p></span></div><div style="margin: 0cm 0cm 0.0001pt; font-size: 11pt; font-family: Calibri, sans-serif;"><span lang="EN-US" style="">if (y == 0)<o:p></o:p></span></div><div style="margin: 0cm 0cm 0.0001pt; font-size: 11pt; font-family: Calibri, sans-serif;"><span lang="EN-US" style=""> <o:p></o:p></span></div><div style="margin: 0cm 0cm 0.0001pt; font-size: 11pt; font-family: Calibri, sans-serif;"><span lang="EN-US" style="">I plan to do it by:<o:p></o:p></span></div><div style="margin: 0cm 0cm 0.0001pt; font-size: 11pt; font-family: Calibri, sans-serif;"><span lang="EN-US" style=""> <o:p></o:p></span></div><div style="margin: 0cm 0cm 0.0001pt; font-size: 11pt; font-family: Calibri, sans-serif;"><span lang="EN-US" style="font-size: 11.5pt;">1. When a division is reached where the denominator is a variable with unknown value, “mark” the denominator variable.</span><span lang="EN-US" style=""><o:p></o:p></span></div><div style="margin: 0cm 0cm 0.0001pt; font-size: 11pt; font-family: Calibri, sans-serif;"><span lang="EN-US" style="font-size: 11.5pt;">2. When reaching a condition that checks if a variable is 0, check if the variable in the condition is “marked”.</span><span lang="EN-US" style=""><o:p></o:p></span></div><div style="margin: 0cm 0cm 0.0001pt; font-size: 11pt; font-family: Calibri, sans-serif;"><span lang="EN-US" style="font-size: 10pt; font-family: Tahoma, sans-serif;">3. Report bug</span><span lang="EN-US" style=""><o:p></o:p></span></div><div style="margin: 0cm 0cm 0.0001pt; font-size: 11pt; font-family: Calibri, sans-serif;"><span lang="EN-US" style=""> <o:p></o:p></span></div><div style="margin: 0cm 0cm 0.0001pt; font-size: 11pt; font-family: Calibri, sans-serif;"><span lang="EN-US" style="">I guess RecursiveASTVisitor is best for this?<o:p></o:p></span></div><div style="margin: 0cm 0cm 0.0001pt; font-size: 11pt; font-family: Calibri, sans-serif;"><span lang="EN-US" style="">Is there perhaps a better way to do this that would allow me to follow the variable from division to check so that it doesn't have to be directly after?<o:p></o:p></span></div><div style="margin: 0cm 0cm 0.0001pt; font-size: 11pt; font-family: Calibri, sans-serif;"><span lang="EN-US"> </span></div><div style="margin: 0cm 0cm 0.0001pt; font-size: 11pt; font-family: Calibri, sans-serif;"><span lang="EN-US">//Anders</span><span style="font-size: 8pt; font-family: 'Courier New';"><o:p></o:p></span></div><div style="margin: 0cm 0cm 0.0001pt; font-size: 11pt; font-family: Calibri, sans-serif;"><o:p> </o:p></div></div>_______________________________________________<br>cfe-dev mailing list<br><a href="mailto:cfe-dev@cs.uiuc.edu" style="color: purple; text-decoration: underline;">cfe-dev@cs.uiuc.edu</a><br><a href="http://lists.cs.uiuc.edu/mailman/listinfo/cfe-dev" style="color: purple; text-decoration: underline;">http://lists.cs.uiuc.edu/mailman/listinfo/cfe-dev</a></div></blockquote></div><br></body></html>