@@ -342,7 +342,7 @@ private predicate succExitSplits(
342
342
ControlFlowElement pred , Splits predSplits , CfgScope succ , SuccessorType t
343
343
) {
344
344
exists ( Reachability:: SameSplitsBlock b , Completion c | pred = b .getAnElement ( ) |
345
- b .isReachable ( predSplits ) and
345
+ b .isReachable ( succ , predSplits ) and
346
346
t = getAMatchingSuccessorType ( c ) and
347
347
scopeLast ( succ , pred , c ) and
348
348
forall ( SplitImpl predSplit | predSplit = predSplits .getASplit ( ) |
@@ -399,7 +399,7 @@ private module SuccSplits {
399
399
ControlFlowElement succ , Completion c
400
400
) {
401
401
pred = b .getAnElement ( ) and
402
- b .isReachable ( predSplits ) and
402
+ b .isReachable ( _ , predSplits ) and
403
403
succ ( pred , succ , c )
404
404
}
405
405
@@ -728,12 +728,12 @@ private module Reachability {
728
728
* Holds if the elements of this block are reachable from a callable entry
729
729
* point, with the splits `splits`.
730
730
*/
731
- predicate isReachable ( Splits splits ) {
731
+ predicate isReachable ( CfgScope scope , Splits splits ) {
732
732
// Base case
733
- succEntrySplits ( _ , this , splits , _)
733
+ succEntrySplits ( scope , this , splits , _)
734
734
or
735
735
// Recursive case
736
- exists ( SameSplitsBlock pred , Splits predSplits | pred .isReachable ( predSplits ) |
736
+ exists ( SameSplitsBlock pred , Splits predSplits | pred .isReachable ( scope , predSplits ) |
737
737
this = pred .getASuccessor ( predSplits , splits )
738
738
)
739
739
}
@@ -791,43 +791,45 @@ private module Cached {
791
791
newtype TCfgNode =
792
792
TEntryNode ( CfgScope scope ) { succEntrySplits ( scope , _, _, _) } or
793
793
TAnnotatedExitNode ( CfgScope scope , boolean normal ) {
794
- exists ( Reachability:: SameSplitsBlock b , SuccessorType t | b .isReachable ( _) |
794
+ exists ( Reachability:: SameSplitsBlock b , SuccessorType t | b .isReachable ( scope , _) |
795
795
succExitSplits ( b .getAnElement ( ) , _, scope , t ) and
796
796
if isAbnormalExitType ( t ) then normal = false else normal = true
797
797
)
798
798
} or
799
799
TExitNode ( CfgScope scope ) {
800
- exists ( Reachability:: SameSplitsBlock b | b .isReachable ( _) |
800
+ exists ( Reachability:: SameSplitsBlock b | b .isReachable ( scope , _) |
801
801
succExitSplits ( b .getAnElement ( ) , _, scope , _)
802
802
)
803
803
} or
804
- TElementNode ( ControlFlowElement cfe , Splits splits ) {
805
- exists ( Reachability:: SameSplitsBlock b | b .isReachable ( splits ) | cfe = b .getAnElement ( ) )
804
+ TElementNode ( CfgScope scope , ControlFlowElement cfe , Splits splits ) {
805
+ exists ( Reachability:: SameSplitsBlock b | b .isReachable ( scope , splits ) |
806
+ cfe = b .getAnElement ( )
807
+ )
806
808
}
807
809
808
810
/** Gets a successor node of a given flow type, if any. */
809
811
cached
810
812
TCfgNode getASuccessor ( TCfgNode pred , SuccessorType t ) {
811
813
// Callable entry node -> callable body
812
814
exists ( ControlFlowElement succElement , Splits succSplits , CfgScope scope |
813
- result = TElementNode ( succElement , succSplits ) and
815
+ result = TElementNode ( scope , succElement , succSplits ) and
814
816
pred = TEntryNode ( scope ) and
815
817
succEntrySplits ( scope , succElement , succSplits , t )
816
818
)
817
819
or
818
- exists ( ControlFlowElement predElement , Splits predSplits |
819
- pred = TElementNode ( predElement , predSplits )
820
+ exists ( CfgScope scope , ControlFlowElement predElement , Splits predSplits |
821
+ pred = TElementNode ( pragma [ only_bind_into ] ( scope ) , predElement , predSplits )
820
822
|
821
823
// Element node -> callable exit (annotated)
822
- exists ( CfgScope scope , boolean normal |
823
- result = TAnnotatedExitNode ( scope , normal ) and
824
+ exists ( boolean normal |
825
+ result = TAnnotatedExitNode ( pragma [ only_bind_into ] ( scope ) , normal ) and
824
826
succExitSplits ( predElement , predSplits , scope , t ) and
825
827
if isAbnormalExitType ( t ) then normal = false else normal = true
826
828
)
827
829
or
828
830
// Element node -> element node
829
831
exists ( ControlFlowElement succElement , Splits succSplits , Completion c |
830
- result = TElementNode ( succElement , succSplits )
832
+ result = TElementNode ( pragma [ only_bind_into ] ( scope ) , succElement , succSplits )
831
833
|
832
834
succSplits ( predElement , predSplits , succElement , succSplits , c ) and
833
835
t = getAMatchingSuccessorType ( c )
@@ -853,6 +855,23 @@ private module Cached {
853
855
*/
854
856
cached
855
857
ControlFlowElement getAControlFlowExitNode ( ControlFlowElement cfe ) { last ( cfe , result , _) }
858
+
859
+ /**
860
+ * Gets the CFG scope of node `n`. Unlike `getCfgScope`, this predicate
861
+ * is calculated based on reachability from an entry node, and it may
862
+ * yield different results for AST elements that are split into multiple
863
+ * scopes.
864
+ */
865
+ cached
866
+ CfgScope getNodeCfgScope ( TCfgNode n ) {
867
+ n = TEntryNode ( result )
868
+ or
869
+ n = TAnnotatedExitNode ( result , _)
870
+ or
871
+ n = TExitNode ( result )
872
+ or
873
+ n = TElementNode ( result , _, _)
874
+ }
856
875
}
857
876
858
877
import Cached
0 commit comments