[cfe-dev] [StaticAnalyzer] False positive with loop handling

[Dominic Chen via cfe-dev]

Ah, so it's an issue with the constraint manager. I couldn't find much
documentation on the internals of the static analyzer, so it wasn't
clear how the components interacted with one another.

More generally, why does the static analyzer implement its own
constraint solver? I noticed that there also used to be a
BasicConstraintManager, but was removed quite a while back for not being
useful in practice. Would replacing the internal constraint solver with
a wrapper around e.g. CVC4 or Z3 significantly increase the precision of
the analysis?

Thanks,

Dominic

On 10/20/2016 6:42 AM, Artem Dergachev wrote:
> A false positive due to a known issue.
>
> This happens because "nc = na + nb - 1" is too complicated for our
> extremely simple and fast solver (RangeConstraintManager) to handle.
> Because of that, we need to *conjure* a completely new symbol for
> "nc", and then it assumes that "nc" may be equal to 2 even when "na"
> and "nb" are equal to 1. Essentially, we can construct a correct
> SymSymExpr for "nc", but we'd need to do some bigger work to let the
> solver solve the equations.
>
> I'm all for producing more SymSymExpr objects and simplifying them
> (through an alpha-renaming-like procedure) whenever their components
> get simplified out, just need time to implement this.
>
> On 10/19/16 10:29 PM, Dominic Chen via cfe-dev wrote:
>>
>> Hello,
>>
>> I've been trying to track down a false positive with symbolic
>> execution of an array assignment within a loop, but I'm having some
>> trouble figuring out the root cause. In the attached loop.c file, the
>> analyzer identifies the LHS of the assignment equal operation on line
>> 11 to be a garbage value, but this is actually initialized on line 6.
>>
>> Initially, I thought that this was an issue with dead symbols being
>> incorrectly purged, because the trimmed ExplodedGraph shows that the
>> analyzer identifies the array "c" to be an ElementRegion "c:
>> &element{c, 0 S64b,int}" in an earlier node before
>> PreStmtPurgeDeadSymbols. But this is unchanged even after eliminating
>> calls to collectNode(), so I'm confused if the graph is representing
>> the actual symbolic execution exploration state, or just simply the
>> ordering of explored states from the worklist?
>>
>> The other place that I've been looking at is the branch condition
>> handling inside ExprEngine::processBranch(). When the symbolic
>> execution engine assumes either of the false/true branches, does that
>> also entail the body of the loop?
>>
>> Thanks,
>>
>> Dominic
>>
>>
>> _______________________________________________
>> cfe-dev mailing list
>> cfe-dev at lists.llvm.org
>> http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev
>