[cfe-dev] Evaluation of Symbolic Expressions?

[Ádám Balogh 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

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