[cfe-dev] How to know which edge the path is traversing?

[Ted Kremenek]

On May 16, 2008, at 7:32 AM, Zhongxing Xu wrote:

> I use GRCoreEngine to do a path sensitive analysis. For example, I  
> can get two paths for the program below:
>
> int f(int n) {
>   if (n > 0)
>     ...
>   else
>     ...
> }
>
> I can use the nodes in EndNodes to get these two paths (by  
> backtracking from endnodes).
> There are two BlockEdgeDst nodes after the block containing the  
> IfStmt "if (n>0)".
> How can I know which path is led by the condition n > 0 or n <= 0?  
> That is, how can I know which is the "true"/"false" branch edge?

Hi Zhongxing,

You will want to inspect the successors CFBBlocks of the "source" in  
the BlockEdge, and compare it against the destination.  For CFGBlock's  
whose terminator is a branch (if statements, loops, etc), the first  
successor block is the true branch, the and second successor block is  
the false branch.  For example:


ProgramPoint P = N->getLocation();  // N is an ExplodedNode<...>

if (BlockEdge* BE = dyn_cast<BlockEdge>(&P)) {

   CFGBlock* Src = BE->getSrc();
   CFGBlock* Dst = BE->getDst();

   // Test if we are at a (binary) branch.
   if (Src.hasBinaryBranchTerminator()) {

     if (*Src.succ_begin() == Dst) {
        // We took the true branch.
     }
     else {
        assert (*(Src.succ_begin()+1) == Dst);
        // We took the false branch.
     }
   }
}

Note that "hasBinaryBranchTerminator" only returns true for  
terminators that are "ForStmt", "WhileStmt", "DoStmt", "IfStmt",  
"ChooseExpr", "ConditionalOperator", and "BinaryOperator" (for '&&'  
and '||').  IndirectGotoStmt and SwitchStmt work differently.   
IndirectGotoStmt always branches to a special block where the actual  
indirect goto takes place (do a CFG dump of code with a labeled goto  
to see what I mean).  Blocks that have a SwitchStmt terminator have as  
their successor blocks the targets of the switch.  In that case, each  
successor block should have "getLabel()" return a SwitchStmt, with the  
exception of the last successor.  The last successor is always the  
"default" branch, which may be explicit (with a "default:" label) or  
implicit (in the case of fall-through to the code after the switch  
block).

BTW, "hasBinaryBranchTerminator" was a recently added predicate  
method.  Most code that inspects terminators actually uses a switch  
statement on the statement class of the terminator to handle both  
binary branches and other terminator types.

Ted