[cfe-dev] Question on static analyzer callback: checkBranchCondition()

[Artem Dergachev via cfe-dev]

(whoops, re-added the mailing list)

Due to the short circuit nature of logical binary operators, the value 
of the expression `x && y` is equal to the value of `y` as long as `y` 
gets evaluated at all, and to `false` otherwise. You can see which 
branch is evaluated in the callback for `x` by figuring out if `x` 
evaluates to `false`, and in this case you already know that the value 
of `x && y` would be false. You can see which branch is evaluated in the 
callback for `y` - it is definitely the branch on which `y` is 
evaluated. In this callback the value of `x && y` can be computed as `y`.

P.S. If you are trying to prove that some expressions in the code are 
always false or always true, you won't be able to do it that way, 
because all computations within checker callbacks are based on the 
assumptions that allowed the program to reach the respective point in a 
certain state, and may be incorrect on other paths to the same program 
point in which the state of the program is different or different 
assumptions have been made. For example, in code

   if (a < 10) {
   }
   if (a < 10) {
   }

you would "prove" that the second branch condition is both "always true" 
(i.e., assuming you take the true branch on the first if(), the 
condition is definitely true on the second if) and "always false" (i.e., 
assuming you take the false branch on the first if(), the condition is 
definitely false on the second if).

Static Analyzer's path-sensitive engine is only useful for problems that 
consist in finding execution paths with special properties 
("may"-problems), not for proving that paths with certain properties do 
not exist ("must"-problems). The only on-by-default "must"-checker in 
the Static Analyzer is the DeadStores checker (assigned value is 
discarded or overwritten before use on all paths after the assignment), 
and it works by exploring the CFG manually and doesn't rely on the 
Static Analyzer's path-sensitive engine.

On 11/19/18 7:56 PM, illiop via cfe-dev wrote:
> Hello,
> Thanks in advance for any help!
> If I have the following code:
> void function()
> {
>        int a = 1;
>        if ( ( a<10 ) && ( a > 20 ) ) // always false
>       {
>       }
> }
> How can I evaluate the whole condition expression  '( a<10 ) && ( a > 
> 20 ) ' ?
> When I write code like:
> class MyChecker : public Checker< check::BranchCOndition >
> {
> public:
>    void checkBranchCondition(const Stmt* cond, CheckerContext& ctx) const;
> }
> I found that checkBranchCondition() only be called back 2 times, once 
> for 'a<10' , once for 'a > 20 '.  And it's done. No further call back.
> But my goal is to get the 'value' for the whole  '( a<10 ) && ( a > 20 
> ) '.
> I tried the following in vain:
> 1. in checkBranchCondition(), find the 'father' node(it is '( a<10 ) 
> && ( a > 20 ) ' ), and evaluate its 'sval', but the sval is 
> invalid/undifined
> 2. Use check::PostStmt<CompoundStmt> call back. It does NOT called 
> back at all
> 3. Use check::PostStmt<Stmt> call back, and try to find the 'father' 
> by : if(isa<IfStmt>(stmt)), useless.
> 4. Use check::PostStmt<BinaryOperator>, but it still only called back 
> 2 times:  once for 'a<10' , once for 'a > 20 '
> I am a fresh man in the static analyzer, please help, thanks!
> illiop
>
>
>
>
> _______________________________________________
> cfe-dev mailing list
> cfe-dev at lists.llvm.org
> http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev