Quantcast

Evaluation of Symbolic Expressions?

classic Classic list List threaded Threaded
2 messages Options
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

Evaluation of Symbolic Expressions?

Ivan Garramona via cfe-dev

Hello,

 

I have some trouble with symbolic expressions. Either I expect too much from the Static Analyzer, or – more probable – I use the wrong functions.

 

I have two different problems where I do not get what I expect.

 

The first problem seems very simple: I want to compare two symbolic expressions, one of them is something like {conj_1}, the other one is {conj_1} + 1. Using SValBuilder::evalBinOpNN() I get UnknownVal for comparison with e.g. BO_GE or BO_LT. I thought that these very simple expressions are easy to evaluate. I only get concrete integer result (1) if the two sides of the comparison are exactly the same (e.g. {conj_1} >= {conj_1}).

 

I also tried subtracting them from each other. Using SValBuilder::evalBinOpNN() I also get UnknownVal for subtraction, and for Symbolmanager::getSymSymExpr() I get symbolic expression ({conj_1} + 1) - {conj_1}, and then for the comparison to zero using SValBuilder::evalBinOpNN() I get symbolic expression ({conj_1} + 1) - {conj_1} > 0 instead of a concrete integer (1). This method is worse since it does not work for expressions like {conj_1} - {conj_1} >= 0 either.

 

The second problem seems also simple: I make an assumption for the state, like {conj_1} == {conj_2}. If I dump the state, I see the range of {conj_1} == {conj_2} [1 .. max]. Later, I have comparison where I check e.g. {conj_1} >= {conj_2}, but I get UnknownVal. Checking {conj_1} == {conj_2} does not help either. I also tried the subtraction here, thus to store {cont_1} – {cont_2} in the state (range was either [0..0] or [-max..-1], [1..max]), but it did not help either.

 

So, how to do it correctly? I assume that such basic symbolic calculations are part of some checkers which work for a while now. Any ideas?

 

Thanks in advance!

 

Regards,

 

Ádám

 


_______________________________________________
cfe-dev mailing list
[hidden email]
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

Re: Evaluation of Symbolic Expressions?

Ivan Garramona via cfe-dev
Hello,

The analyzer's knowledge of algebra is actually extremely minimal - it
handles "x > 1 && x < 3" pretty well, but not "x > x + 1" or "x == y".
This is because a full-featured *constraint solver* would be slow even
for a few equations, and we'd often throw thousands of equations at him
during analysis of a single file. So we have a simplified solver, called
RangeConstraintManager, which handles only simple equations, but does it
very quickly.

Currently we are discussing a patch that would provide the analyzer with
a full-featured solver (Microsoft's Z3, see
https://reviews.llvm.org/D28952), but we have very little idea of how
practical that would be.

Whenever you're seeing an UnknownVal, it indicates that we failed to
support an operation for some reason. Most checkers react to this by
skipping the analysis, deciding that the code seems to be too complex to
analyze, and it's more important to avoid false positives than to try
find a bug in a code we don't understand.

Even though a SymSymExpr of desired shape can be constructed manually,
it would not be of much use because the constraint manager would fail to
handle it properly anyway.

If you definitely need to solve complicated constraints in your checker,
you might want to cover your cases in the constraint manager, which is
easily extensible. Or you may want to maintain some extra information on
the checker side, like "this iterator object is to the left from that
iterator object" - you could terminate the analysis when an iterator is
both to the left and to the right from another iterator at the same time.

P.S. By the way, "x > x + 1" is quite possible, say for x == INT_MAX.
That's quite different from "x - (x + 1)", which may be equal to 1 with
defined overflow semantics (in C standard, signed integer overflow is
undefined behavior, but in analyzer we assume defined overflow
semantics, because a lot of people rely on them anyway on their
platforms, and we shouldn't tell them to fix code that works).


On 3/20/17 4:08 PM, Ádám Balogh via cfe-dev wrote:

>
> Hello,
>
> I have some trouble with symbolic expressions. Either I expect too
> much from the Static Analyzer, or – more probable – I use the wrong
> functions.
>
> I have two different problems where I do not get what I expect.
>
> The first problem seems very simple: I want to compare two symbolic
> expressions, one of them is something like {conj_1}, the other one is
> {conj_1} + 1. Using SValBuilder::evalBinOpNN() I get UnknownVal for
> comparison with e.g. BO_GE or BO_LT. I thought that these very simple
> expressions are easy to evaluate. I only get concrete integer result
> (1) if the two sides of the comparison are exactly the same (e.g.
> {conj_1} >= {conj_1}).
>
> I also tried subtracting them from each other. Using
> SValBuilder::evalBinOpNN() I also get UnknownVal for subtraction, and
> for Symbolmanager::getSymSymExpr() I get symbolic expression ({conj_1}
> + 1) - {conj_1}, and then for the comparison to zero using
> SValBuilder::evalBinOpNN() I get symbolic expression ({conj_1} + 1) -
> {conj_1} > 0 instead of a concrete integer (1). This method is worse
> since it does not work for expressions like {conj_1} - {conj_1} >= 0
> either.
>
> The second problem seems also simple: I make an assumption for the
> state, like {conj_1} == {conj_2}. If I dump the state, I see the range
> of {conj_1} == {conj_2} [1 .. max]. Later, I have comparison where I
> check e.g. {conj_1} >= {conj_2}, but I get UnknownVal. Checking
> {conj_1} == {conj_2} does not help either. I also tried the
> subtraction here, thus to store {cont_1} – {cont_2} in the state
> (range was either [0..0] or [-max..-1], [1..max]), but it did not help
> either.
>
> So, how to do it correctly? I assume that such basic symbolic
> calculations are part of some checkers which work for a while now. Any
> ideas?
>
> Thanks in advance!
>
> Regards,
>
> Ádám
>
>
>
> _______________________________________________
> cfe-dev mailing list
> [hidden email]
> http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev

_______________________________________________
cfe-dev mailing list
[hidden email]
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev
Loading...