[cfe-dev] static analyzer status?

[Artem Dergachev via cfe-dev]

Casts are discarded in SimpleSValBuilder::evalCastFromNonLoc(), see the 
huge comment in the middle. The correct behavior would be to add SymbolCast.

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.

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.

On 9/14/18 7:11 PM, Lou Wynn wrote:
>
> As for casts, can you point me to the current code in the analyzer 
> that ignores them? Does the following method possibly work?
>
> 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.
>
> Also, I think that I still need to change the current solver not to 
> discard constraints involving multiple symbols.
>
> 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?
>
>
> Thanks,
> Lou
>   
> On 09/14/2018 05:17 PM, Artem Dergachev wrote:
>>
>> 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.
>>
>>> 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?
>>>
>>
>> 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.
>

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.llvm.org/pipermail/cfe-dev/attachments/20180917/47658a4b/attachment.html>