<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
<meta name="Generator" content="Microsoft Word 14 (filtered medium)">
<style><!--
/* Font Definitions */
@font-face
{font-family:"Cambria Math";
panose-1:2 4 5 3 5 4 6 3 2 4;}
@font-face
{font-family:Calibri;
panose-1:2 15 5 2 2 2 4 3 2 4;}
@font-face
{font-family:Tahoma;
panose-1:2 11 6 4 3 5 4 4 2 4;}
/* Style Definitions */
p.MsoNormal, li.MsoNormal, div.MsoNormal
{margin:0cm;
margin-bottom:.0001pt;
font-size:12.0pt;
font-family:"Times New Roman","serif";}
a:link, span.MsoHyperlink
{mso-style-priority:99;
color:blue;
text-decoration:underline;}
a:visited, span.MsoHyperlinkFollowed
{mso-style-priority:99;
color:purple;
text-decoration:underline;}
p.MsoAcetate, li.MsoAcetate, div.MsoAcetate
{mso-style-priority:99;
mso-style-link:"Balloon Text Char";
margin:0cm;
margin-bottom:.0001pt;
font-size:8.0pt;
font-family:"Tahoma","sans-serif";}
span.apple-tab-span
{mso-style-name:apple-tab-span;}
span.EmailStyle18
{mso-style-type:personal-reply;
font-family:"Calibri","sans-serif";
color:#1F497D;}
span.BalloonTextChar
{mso-style-name:"Balloon Text Char";
mso-style-priority:99;
mso-style-link:"Balloon Text";
font-family:"Tahoma","sans-serif";}
.MsoChpDefault
{mso-style-type:export-only;
font-size:10.0pt;}
@page WordSection1
{size:612.0pt 792.0pt;
margin:70.85pt 70.85pt 70.85pt 70.85pt;}
div.WordSection1
{page:WordSection1;}
--></style><!--[if gte mso 9]><xml>
<o:shapedefaults v:ext="edit" spidmax="1026" />
</xml><![endif]--><!--[if gte mso 9]><xml>
<o:shapelayout v:ext="edit">
<o:idmap v:ext="edit" data="1" />
</o:shapelayout></xml><![endif]-->
</head>
<body lang="SV" link="blue" vlink="purple">
<div class="WordSection1">
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1F497D">Hi Jordan,<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1F497D"><o:p> </o:p></span></p>
<p class="MsoNormal"><span lang="EN-US" style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1F497D">I don’t know if I have the time to change division by zero right away but I can make the dereference check CFG-based. Do you have an example of
a CFG-based checker? I don’t know how to make those.<o:p></o:p></span></p>
<p class="MsoNormal"><span lang="EN-US" style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1F497D"><o:p> </o:p></span></p>
<p class="MsoNormal"><span lang="EN-US" style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1F497D">//Anders<o:p></o:p></span></p>
<p class="MsoNormal"><span lang="EN-US" style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1F497D"><o:p> </o:p></span></p>
<div style="border:none;border-left:solid blue 1.5pt;padding:0cm 0cm 0cm 4.0pt">
<div>
<div style="border:none;border-top:solid #B5C4DF 1.0pt;padding:3.0pt 0cm 0cm 0cm">
<p class="MsoNormal"><b><span lang="EN-US" style="font-size:10.0pt;font-family:"Tahoma","sans-serif"">From:</span></b><span lang="EN-US" style="font-size:10.0pt;font-family:"Tahoma","sans-serif""> Jordan Rose [mailto:jordan_rose@apple.com]
<br>
<b>Sent:</b> den 21 juli 2014 19:40<br>
<b>To:</b> Anders Rönnholm<br>
<b>Cc:</b> cfe-commits@cs.uiuc.edu; Daniel Marjamäki; Anna Zaks<br>
<b>Subject:</b> Re: [PATCH] Division by zero<o:p></o:p></span></p>
</div>
</div>
<p class="MsoNormal"><o:p> </o:p></p>
<div>
<p class="MsoNormal">So, Anna brought up that the check as implemented is very nearly path-independent, i.e. it only depends on flow-sensitive properties of the CFG. The path-sensitivity is buying us very little; it catches this case:<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<blockquote style="margin-top:5.0pt;margin-bottom:5.0pt">
<div>
<p class="MsoNormal">int y = x;<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal">int div = z / y;<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal">if (x) { ...}<o:p></o:p></p>
</div>
</blockquote>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal">But also warns here, which doesn't necessarily make sense:<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<blockquote style="margin-top:5.0pt;margin-bottom:5.0pt">
<div>
<p class="MsoNormal">int foo(int x, int y, int z) {<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><span class="apple-tab-span"> </span>int div = z / y;<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><span class="apple-tab-span"> </span>if (x) return div;<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><span class="apple-tab-span"> </span>return 0;<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal">}<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal">foo(a, a, b); // only coincidentally the same symbol<o:p></o:p></p>
</div>
</blockquote>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal">What would you think about turning this (and/or the null dereference check) into a CFG-based check instead? We lose the first example (and cases where inlining would help), but fix the second, and very possibly speed up analysis. CFG analysis
is also more capable of proving that something happens on <i>all</i> paths rather than just some, since that's just propagating information along the graph.<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal">Jordan<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<p class="MsoNormal"><o:p> </o:p></p>
<div>
<div>
<p class="MsoNormal">On Jul 10, 2014, at 9:55 , Anders Rönnholm <<a href="mailto:Anders.Ronnholm@evidente.se">Anders.Ronnholm@evidente.se</a>> wrote:<o:p></o:p></p>
</div>
<p class="MsoNormal"><br>
<br>
<o:p></o:p></p>
<p class="MsoNormal">Great, no problem. I'll move forward with my dereference then check patch now that this one is commited, which will be pretty similar.<br>
<br>
//Anders<br>
<br>
.......................................................................................................................<br>
Anders Rönnholm Senior Engineer<br>
Evidente ES East AB Warfvinges väg 34 SE-112 51 Stockholm Sweden<br>
<br>
Mobile: +46 (0)70 912 42 54<br>
E-mail: <a href="mailto:Anders.Ronnholm@evidente.se">Anders.Ronnholm@evidente.se</a><br>
<br>
<a href="http://www.evidente.se">www.evidente.se</a><br>
<br>
________________________________________<br>
Från: Jordan Rose [jordan_rose@apple.com]<br>
Skickat: den 10 juli 2014 18:20<br>
Till: Anders Rönnholm<br>
Cc: <a href="mailto:cfe-commits@cs.uiuc.edu">cfe-commits@cs.uiuc.edu</a>; Daniel Marjamäki<br>
Ämne: Re: [PATCH] Division by zero<br>
<br>
Thank you for going through so many rounds of review on this. Committed in r212731! (The one change I made was to reset the test in isZero to use assume instead of assumeDual, now that my confusion has been fixed.)<br>
<br>
Jordan<o:p></o:p></p>
</div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
</div>
</body>
</html>