Question on static analyzer callback: checkBranchCondition()

Clang Frontend
1

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 call back. It does NOT called back at all
  3. Use check::PostStmt call back, and try to find the ‘father’ by : if(isa(stmt)), useless.
  4. Use check::PostStmt, 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

2

(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.

3

Got your idea.

Another 2 questions:
(1) if the condition expr is a littlt complex: A&&B&&C, or (A && B) || funciont(i) , If I want to find the whole expr’s value,
I should konw what kind of the whole binary operator is(‘…&&…&&…’, ‘…&&…||…’) and which part it is now called back(‘A’, ‘B’, ‘C’, ‘function(i)’)
it’s not convenient (maybe I should do some bookkeeping by myself ? ) to do that. Am I right ?
(2)
If the codes are:
if( A && B ){}
while( A && B){}
do…while( A && B){}
for(…; A && B; …){}
Is there any Quick way to find which controll statement(IfStmt, WhileStmt, DoStmt, ForStmt) the condition expr blongs to ?
Now my method is:

void ControllStmtCondChecker::checkBranchCondition(const Stmt* cond, CheckerContext& ctx) const
{
const ParentMap& Parents = ctx.getLocationContext()->getParentMap();
const Stmt* parent = Parents.getParent(cond);
while(parent)
{
if( isa(parent) ){ … break; }
else if( isa(parent) ){ … break; }
…

else
{
cond = parent;
parent = Parents.getParent(cond);
}

// here we get the controller statement ‘parent’ and its whole condition expr ‘cond’

}

Thanks a lot !