Question on static analyzer callback: checkBranchCondition()

classic Classic list List threaded Threaded
3 messages Options
Reply | Threaded
Open this post in threaded view
|

Question on static analyzer callback: checkBranchCondition()

Oleg Smolsky via cfe-dev
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
[hidden email]
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev
Reply | Threaded
Open this post in threaded view
|

Re: Question on static analyzer callback: checkBranchCondition()

Oleg Smolsky 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
> [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
Reply | Threaded
Open this post in threaded view
|

Re: Question on static analyzer callback: checkBranchCondition()

Oleg Smolsky 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" <[hidden email]> 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 >> [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