<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
</head>
<body text="#000000" bgcolor="#FFFFFF">
Casts are discarded in SimpleSValBuilder::evalCastFromNonLoc(), see
the huge comment in the middle. The correct behavior would be to add
SymbolCast.<br>
<br>
Symbol-symbol relations are now discarded very rarely, usually due
to complexity limits (i.e., the symbol becomes huge and other parts
of the Analyzer explode exponentially). There are a few other
operations that get discarded, most noticeably unary minus/logical
not/bitwise not over symbols.<br>
<br>
Just re-enable everything you need under a flag and later enable
your implementation by default together with Z3 when it becomes
stable enough. Apart from false positives and false negatives caused
by poor constraint solving there are no other downsides of adding
cast support, as long as the rest of the code is ready for it. For
instance, checkers ideally wouldn't need to be updated.<br>
<br>
<div class="moz-cite-prefix">On 9/14/18 7:11 PM, Lou Wynn wrote:<br>
</div>
<blockquote type="cite"
cite="mid:2054e454-77e6-a56d-239a-dade4df22736@gmail.com">
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
<p>As for casts, can you point me to the current code in the
analyzer that ignores them? Does the following method possibly
work?</p>
<p>I introduce another method or a few methods that handle cast
operations and use them when I process integer expressions. Or
ideally using one or few default parameters to control if the
casts should be ignored (the default), so that handling casts
doesn't disturb the existing solver and checkers.</p>
<p>Also, I think that I still need to change the current solver
not to discard constraints involving multiple symbols.</p>
<p>Is this a practical investigation work? What other issues and
places should I pay attention to, and what's the best steps to
start with?</p>
<br>
<pre class="moz-signature" cols="72">Thanks,
Lou
</pre>
<div class="moz-cite-prefix">On 09/14/2018 05:17 PM, Artem
Dergachev wrote:<br>
</div>
<blockquote type="cite"
cite="mid:25ee088a-ab7c-8cd9-829c-de757bb6c354@gmail.com">
<meta http-equiv="Content-Type" content="text/html;
charset=UTF-8">
<br>
Also for integer overflows you may encounter a completely
different problem that is currently in a worse shape than
constraint solving, and it's integral cast representation.
Static analyzer currently models casts by ignoring them, so the
solver doesn't ever get a hold on this information. You'll need
to lift this restriction, but it'll immediately upset the
existing solver and a lot of other entities in the analyzer, so
you'll have to make them prepared for seeing casted symbols.
This may involve implementing the trick i mentioned above in all
checkers, because otherwise many checkers will fail to find most
of their bugs.<br>
<br>
<blockquote type="cite"
cite="mid:06c73b46-402a-66e9-313c-08c96b51867e@gmail.com">
<p><font size="+1"> I can rephrase this to taint propagation
and integer expression by saying that an expression
involving a tainted value is likely to cause integer
overflow. What is the best way to implement this checker
if I use this strategy? I've noticed that there is a taint
propagation checker but haven't figured out how to use it
in another checker. Is there any example code that uses
it?<br>
</font></p>
</blockquote>
</blockquote>
<blockquote type="cite"
cite="mid:25ee088a-ab7c-8cd9-829c-de757bb6c354@gmail.com"><br>
In other words, taint problems are "per-path" "may" problems,
while normal problems are "per-path" "must" problems. And for
that purpose the existing refutation scheme is enough to solve
all the problems. You still have problems with casts though.<br>
</blockquote>
<br>
</blockquote>
<br>
</body>
</html>