@@ -63,35 +63,82 @@ class StmtCfgNode extends AstCfgNode {
6363}
6464
6565pragma [ nomagic]
66- private BasicBlock getARelevantBasicBlock ( Ast a ) { result .getANode ( ) .getAstNode ( ) = a }
66+ private BasicBlock getBasicBlock ( Ast a ) { result .getANode ( ) .getAstNode ( ) = a }
6767
6868/**
6969 * A class for mapping parent-child AST nodes to parent-child CFG nodes.
7070 */
7171abstract private class ChildMapping extends Ast {
72+ /** Holds if `child` is evaluated before its parent in the CFG. */
73+ abstract predicate precedesParent ( Ast child ) ;
74+
75+ private CfgNode getRelevantChildCfgNode ( Ast child ) {
76+ this .relevantChild ( child ) and
77+ result .getAstNode ( ) = child
78+ }
79+
7280 /**
7381 * Holds if `child` is a (possibly nested) child of this expression
7482 * for which we would like to find a matching CFG child.
7583 */
7684 abstract predicate relevantChild ( Ast child ) ;
7785
7886 /**
79- * Holds if `child` appears before its parent in the control-flow graph.
80- * This always holds for expressions, and _almost_ never for statements .
87+ * Gets a basic block that contains a CFG node for this AST node or
88+ * any relevant child of this AST node .
8189 */
82- abstract predicate precedesParent ( Ast child ) ;
90+ pragma [ nomagic]
91+ private BasicBlock getARelevantBasicBlock ( ) {
92+ getBasicBlock ( this ) = result
93+ or
94+ exists ( Ast child |
95+ this .relevantChild ( child ) and
96+ getBasicBlock ( child ) = result
97+ )
98+ }
8399
100+ /**
101+ * Holds if CFG node `cfnChild` can reach basic block `bb`, without going
102+ * through an intermediate block that contains a CFG node for this AST node
103+ * or any other relevant child of this AST node.
104+ */
84105 pragma [ nomagic]
85- final predicate reachesBasicBlock ( Ast child , CfgNode cfn , BasicBlock bb ) {
86- this .relevantChild ( child ) and
87- cfn .getAstNode ( ) = this and
88- bb .getANode ( ) = cfn
106+ private predicate childNodeReachesBasicBlock ( Ast child , CfgNode cfnChild , BasicBlock bb ) {
107+ exists ( BasicBlock bb0 |
108+ cfnChild = this .getRelevantChildCfgNode ( child ) and
109+ bb0 .getANode ( ) = cfnChild
110+ |
111+ bb = bb0
112+ or
113+ not getBasicBlock ( this ) = bb0 and
114+ if this .precedesParent ( child ) then bb = bb0 .getASuccessor ( ) else bb = bb0 .getAPredecessor ( )
115+ )
89116 or
90117 exists ( BasicBlock mid |
91- this .reachesBasicBlock ( child , cfn , mid ) and
92- not mid = getARelevantBasicBlock ( child )
93- |
94- if this .precedesParent ( child ) then bb = mid .getAPredecessor ( ) else bb = mid .getASuccessor ( )
118+ this .childNodeReachesBasicBlock ( child , cfnChild , mid ) and
119+ not mid = this .getARelevantBasicBlock ( ) and
120+ if this .precedesParent ( child ) then bb = mid .getASuccessor ( ) else bb = mid .getAPredecessor ( )
121+ )
122+ }
123+
124+ /**
125+ * Holds if CFG node `cfnChild` can reach CFG node `cfnParent`, without going
126+ * through an intermediate block that contains a CFG node for this AST node.
127+ */
128+ pragma [ nomagic]
129+ private predicate childNodeReachesParentNode ( CfgNode cfnParent , Ast child , CfgNode cfnChild ) {
130+ exists ( BasicBlock bb | this .childNodeReachesBasicBlock ( child , cfnChild , bb ) |
131+ cfnParent .getAstNode ( ) = this and
132+ (
133+ cfnParent = bb .getANode ( )
134+ or
135+ if this .precedesParent ( child )
136+ then cfnParent = bb .getASuccessor ( ) .getANode ( )
137+ else cfnParent = bb .getAPredecessor ( ) .getANode ( )
138+ )
139+ or
140+ // `cfnChild` can reach `cfnParent` by going via another relevant child
141+ this .childNodeReachesParentNode ( cfnParent , _, bb .getANode ( ) )
95142 )
96143 }
97144
@@ -104,8 +151,7 @@ abstract private class ChildMapping extends Ast {
104151 */
105152 cached
106153 predicate hasCfgChild ( Ast child , CfgNode cfn , CfgNode cfnChild ) {
107- this .reachesBasicBlock ( child , cfn , cfnChild .getBasicBlock ( ) ) and
108- cfnChild .getAstNode ( ) = child
154+ this .childNodeReachesParentNode ( cfn , child , cfnChild )
109155 }
110156}
111157
0 commit comments