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

[illiop via cfe-dev]

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<IfStmt>(parent) ){ ...... break; }
      else if( isa<WhileStmt>(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 !



At 2018-11-20 15:02:46, "Artem Dergachev" <noqnoqneo at gmail.com> wrote:
>(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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.llvm.org/pipermail/cfe-dev/attachments/20181120/d49d2e8e/attachment.html>