<div dir="ltr">Hi all,<div><br></div><div><div>Hi guys,</div><div><br></div><div>I'm investigating the constraints being dropped, here's what I got so far.</div><div><br></div><div>First of all, I'm using the following program:</div><div><br></div><div>void foo(unsigned width)</div><div>{</div><div> int base;</div><div> int i = 0;</div><div><br></div><div> if (!(i % width))</div><div> base = 1;</div><div><br></div><div> if(base == 1)</div><div> abort();</div><div>}</div><div><br></div><div>I started by looking at ExprEngine::processBranch, where </div><div><br></div><div>SVal X = PrevState->getSVal(Condition, PredI->getLocationContext());</div><div><br></div><div>returns Unknown for the remainder condition. The getSVal ends up looking in a map for the value result, so I found that bindExpr fills that map.</div><div><br></div><div>Going back a bit, into ExprEngine::Visit, when evaluating a Stmt::BinaryOperatorClass (regardless of the eagerly assume flag) ExprEngine::VisitBinaryOperator is called, which eventually calls evalBinOp and, since it doesn't understand remainder, it returns unknown and BindExpr is never called.</div><div><br></div><div>Back to ExprEngine::processBranch, when the symbol is unknown the following piece of code is called:</div><div><br></div><div> // If the condition is still unknown, give up.</div><div> if (X.isUnknownOrUndef()) {</div><div> builder.generateNode(PrevState, true, PredI);</div><div> builder.generateNode(PrevState, false, PredI);</div><div> continue;</div><div> }</div><div><br></div><div>and the condition is simply ignored. When the result is defined, it creates two nodes assuming the constraints.</div><div><br></div><div>~</div><div><br></div><div>My idea is when the SVal is undef or unknown, instead of generating two nodes with no knowledge about the constraints, we could create two ranged constraints, like:</div><div><br></div><div>i % width: [0,0]</div><div><br></div><div>and </div><div><br></div><div>i % width: [1,1]</div><div><br></div><div>for each path. That way we can keep the constraints with reasonable values.</div><div><br></div><div>What do you think? It feels like this will break stuff further down the line, but I'll know for sure if I implement the change.</div></div><div><br></div><div>~</div><div><br></div><div>Artem's response:</div><div><br></div><div><div>Yep, i strongly believe that any UnknownVal should be treated as a </div><div>synonym of "not implemented".</div><div><br></div><div>In *this* example you might also notice that there's no symbol for 'i', </div><div>but it's a concrete integer 0 instead. So you can evaluate the whole </div><div>remainder to 0, unless 'width' is also equal to 0 (in which case the </div><div>answer would be UndefinedVal). Also note that when enabled, DivZero </div><div>checker will refute the 'width == 0' branch.</div><div><br></div><div>In the general case you have no choice but to produce an IntSymExpr (if </div><div>'i' is a concrete integer other than 0) or a SymSymExpr (if 'i' is a </div><div>symbol).</div></div><div><br></div></div><br><div class="gmail_quote"><div dir="ltr">Em qui, 24 de mai de 2018 às 18:15, Mikhail Ramalho <<a href="mailto:mikhail.ramalho@gmail.com" target="_blank">mikhail.ramalho@gmail.com</a>> escreveu:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr">
<span></span>
<table cellspacing="0" border="0" style="font-family:"Liberation Sans";font-size:x-small">
<colgroup width="106"></colgroup>
<colgroup width="85"></colgroup>
<colgroup width="211"></colgroup>
<colgroup width="215"></colgroup>
<colgroup width="212"></colgroup>
<colgroup width="47"></colgroup>
<colgroup width="31"></colgroup>
<colgroup width="98"></colgroup>
<tbody style="font-family:"Liberation Sans";font-size:x-small"><tr style="font-family:"Liberation Sans";font-size:x-small">
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" height="17" align="left"><br></td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="left">Total Time</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="left">time.analyzer.time.sys (s) (mean)</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="left">time.analyzer.time.user (s) (mean)</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="left">time.analyzer.time.wall (s) (mean)</td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="left">Reported bugs</td>
</tr>
<tr style="font-family:"Liberation Sans";font-size:x-small">
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" height="17" align="left">Tmux</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">99.2</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">0.076</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">27.253</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">7.656</td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">32</td>
</tr>
<tr style="font-family:"Liberation Sans";font-size:x-small">
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" height="17" align="left">Tmux + z3</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">152.88</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">0.074</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">56.251</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">11.505</td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">32</td>
</tr>
<tr style="font-family:"Liberation Sans";font-size:x-small">
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" height="17" align="left">Ratio</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">154.11%</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">97.37%</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">206.40%</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">150.27%</td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="left">Diff</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">0</td>
</tr>
<tr style="font-family:"Liberation Sans";font-size:x-small">
<td height="17" align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
</tr>
<tr style="font-family:"Liberation Sans";font-size:x-small">
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" height="17" align="left">Redis</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">173.69</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">0.057</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">7.083</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">7.271</td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">146</td>
</tr>
<tr style="font-family:"Liberation Sans";font-size:x-small">
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" height="17" align="left">Redis + z3</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">193.43</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">0.057</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">7.621</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">7.728</td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">140</td>
</tr>
<tr style="font-family:"Liberation Sans";font-size:x-small">
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" height="17" align="left">Ratio</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">111.37%</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">100.00%</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">107.60%</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">106.29%</td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="left">Diff</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">6</td>
</tr>
<tr style="font-family:"Liberation Sans";font-size:x-small">
<td height="17" align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
</tr>
<tr style="font-family:"Liberation Sans";font-size:x-small">
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" height="17" align="left">OpenSSL</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">264.93</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">0.042</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">3.31</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">3.412</td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">204</td>
</tr>
<tr style="font-family:"Liberation Sans";font-size:x-small">
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" height="17" align="left">OpenSSL + z3</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">213.53</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">0.035</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">3.099</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">3.152</td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">204</td>
</tr>
<tr style="font-family:"Liberation Sans";font-size:x-small">
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" height="17" align="left">Ratio</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">80.60%</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">83.33%</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">93.63%</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">92.38%</td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="left">Diff</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">0</td>
</tr>
<tr style="font-family:"Liberation Sans";font-size:x-small">
<td height="17" align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
</tr>
<tr style="font-family:"Liberation Sans";font-size:x-small">
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" height="17" align="left">Twin</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">143.17</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">0.067</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">6.593</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">6.696</td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">138</td>
</tr>
<tr style="font-family:"Liberation Sans";font-size:x-small">
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" height="17" align="left">Twin + z3</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">133.83</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">0.06</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">6.79</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">6.882</td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">138</td>
</tr>
<tr style="font-family:"Liberation Sans";font-size:x-small">
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" height="17" align="left">Ratio</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">93.48%</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">89.55%</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">102.99%</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">102.78%</td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="left">Diff</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">0</td>
</tr>
<tr style="font-family:"Liberation Sans";font-size:x-small">
<td height="17" align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
</tr>
<tr style="font-family:"Liberation Sans";font-size:x-small">
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" height="17" align="left">Git + z3</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">333.9</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">0.075</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">8.52</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">8.67</td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">96</td>
</tr>
<tr style="font-family:"Liberation Sans";font-size:x-small">
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" height="17" align="left">Git + z3</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">289.59</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">0.062</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">7.924</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">8.023</td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">90</td>
</tr>
<tr style="font-family:"Liberation Sans";font-size:x-small">
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" height="17" align="left">Ratio</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">86.73%</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">82.67%</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">93.00%</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">92.54%</td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="left">Diff</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">6</td>
</tr>
<tr style="font-family:"Liberation Sans";font-size:x-small">
<td height="17" align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
</tr>
<tr style="font-family:"Liberation Sans";font-size:x-small">
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" height="17" align="left">Postgresql</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">889.35</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">0.079</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">8.482</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">8.631</td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">676</td>
</tr>
<tr style="font-family:"Liberation Sans";font-size:x-small">
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" height="17" align="left">Postgresql + z3</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">902.86</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">0.077</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">9.694</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">9.863</td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">676</td>
</tr>
<tr style="font-family:"Liberation Sans";font-size:x-small">
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" height="17" align="left">Ratio</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">101.52%</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">97.47%</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">114.29%</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">114.27%</td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="left">Diff</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">0</td>
</tr>
<tr style="font-family:"Liberation Sans";font-size:x-small">
<td height="17" align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
</tr>
<tr style="font-family:"Liberation Sans";font-size:x-small">
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" height="17" align="left">Sqlite3</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">1206.3</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">0.262</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">368.446</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">370.786</td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">200</td>
</tr>
<tr style="font-family:"Liberation Sans";font-size:x-small">
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" height="17" align="left">Sqlite3 + z3</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">1260.85</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">0.43</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">407.763</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">409.688</td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">199</td>
</tr>
<tr style="font-family:"Liberation Sans";font-size:x-small">
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" height="17" align="left">Ratio</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">104.52%</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">164.12%</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">110.67%</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">110.49%</td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="left">Diff</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">1</td>
</tr>
<tr style="font-family:"Liberation Sans";font-size:x-small">
<td height="17" align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
</tr>
<tr style="font-family:"Liberation Sans";font-size:x-small">
<td height="17" align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
</tr>
<tr style="font-family:"Liberation Sans";font-size:x-small">
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" height="17" align="left">Average</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">104.62%</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">102.07%</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">118.37%</td>
<td style="border-width:1px;border-style:solid;border-color:rgb(0,0,0);font-family:"Liberation Sans";font-size:x-small" align="right">109.86%</td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
<td align="left" style="font-family:"Liberation Sans";font-size:x-small"><br></td>
</tr>
</tbody></table>
<br></div><div class="gmail_extra"><br><div class="gmail_quote">2018-05-24 15:11 GMT+01:00 Mikhail Ramalho <span dir="ltr"><<a href="mailto:mikhail.ramalho@gmail.com" target="_blank">mikhail.ramalho@gmail.com</a>></span>:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr">Hi all,<div><br></div><div>This is my first report to the community, comparing the results with and without the Z3 refutation when analyzing a number of projects.</div><div><br></div><div>~</div><div><br></div><div>First of all, I'd like to thank Réka Kovács as the first version of the refutation using Z3 was created by her (<a href="https://reviews.llvm.org/D45517" target="_blank">https://reviews.llvm.org/D45517</a>)! Thank you very much!</div><div><br></div><div>After applying patch D45517, you can use the refutation check by using -analyzer-config crosscheck-with-z3=true. Obviously, you need a version of clang built with Z3.</div><div><br></div><div>~</div><div><br></div><div>I'm currently analyzing 7 C projects (unfortunately, there's a bug preventing us from analyzing FFmpeg):</div><div><br></div><div>1. Tmux</div><div>2. Redis </div><div>3. OpenSSL</div><div>4. Twin</div><div>5. Git</div><div>6. Postgresql</div><div>7. Sqlite3</div><div><br></div><div>In short, the refutation check slows down the verification by ~20%. It removed 6 FPs from Redis, 6 FPs from git and 1 FP from Sqlite3 (FP means false positive). Surprisingly enough, some analysis were faster with the crosscheck, but I'm not sure why (maybe ccache?).</div><div><br></div><div>Attached is a spreadsheet (report1.ods) with some number (total time, average time per check, # of reported bugs) and a txt with all the raw data from the analysis (raw.txt). I'll add these data to google drive for the next report.</div><div><br></div><div>In order to generate the raw data, you need to use a version of clang with assertions enabled, call scan-build.py with '-analyzer-config serialize-stats=true' and you need to apply patch <a href="https://reviews.llvm.org/D43134" target="_blank">https://reviews.llvm.org/D43134</a>.</div><div><br></div><div>Thank you very much,</div><div><br></div></div><div class="gmail_extra"><div><div class="m_-9124958404266313734m_-7789057286250042837gmail-h5"><br><div class="gmail_quote">2018-05-01 15:27 GMT+01:00 Mikhail Ramalho <span dir="ltr"><<a href="mailto:mikhail.ramalho@gmail.com" target="_blank">mikhail.ramalho@gmail.com</a>></span>:<br><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir="ltr">Hello all,<div><br></div><div>My proposal for GSoC 2018 [0] about Bug Validation in the Clang Static Analyzer using the Z3 SMT Solver was accepted.</div><div><br></div><div>I'll work with George Karpenkov to improve the bug reports that the static analyzer produces by reducing the number of false bugs.</div><div><br></div><div>Thank you,</div><div><br></div><div>[0] <a href="https://docs.google.com/document/d/1-zNSv0l4WyoxYpJUAw8LFnQq_TY4AGjIpPu1VPkmO-g" target="_blank">https://docs.google.com/document/d/1-zNSv0l4WyoxYpJUAw8LFnQq_TY4AGjIpPu1VPkmO-g</a><span class="m_-9124958404266313734m_-7789057286250042837gmail-m_5428437582812369831gmail-HOEnZb"><font color="#888888"><br clear="all"><div><br></div>-- <br><div class="m_-9124958404266313734m_-7789057286250042837gmail-m_5428437582812369831gmail-m_1835488271327190244m_-1529477061806271292gmail_signature"><div dir="ltr"><div><br></div><div>Mikhail Ramalho.</div></div></div>
</font></span></div></div>
</blockquote></div><br><br clear="all"><div><br></div></div></div><span class="m_-9124958404266313734m_-7789057286250042837gmail-HOEnZb"><font color="#888888">-- <br><div class="m_-9124958404266313734m_-7789057286250042837gmail-m_5428437582812369831gmail_signature"><div dir="ltr"><div><br></div><div>Mikhail Ramalho.</div></div></div>
</font></span></div>
</blockquote></div><br><br clear="all"><div><br></div>-- <br><div class="m_-9124958404266313734m_-7789057286250042837gmail_signature" data-smartmail="gmail_signature"><div dir="ltr"><div><br></div><div>Mikhail Ramalho.</div></div></div>
</div>
</blockquote></div><br clear="all"><div><br></div>-- <br><div dir="ltr" class="m_-9124958404266313734gmail_signature" data-smartmail="gmail_signature"><div dir="ltr"><div><br></div><div>Mikhail Ramalho.</div></div></div>