@@ -342,7 +342,7 @@ private predicate succExitSplits(
342342 ControlFlowElement pred , Splits predSplits , CfgScope succ , SuccessorType t
343343) {
344344 exists ( Reachability:: SameSplitsBlock b , Completion c | pred = b .getAnElement ( ) |
345- b .isReachable ( predSplits ) and
345+ b .isReachable ( succ , predSplits ) and
346346 t = getAMatchingSuccessorType ( c ) and
347347 scopeLast ( succ , pred , c ) and
348348 forall ( SplitImpl predSplit | predSplit = predSplits .getASplit ( ) |
@@ -399,7 +399,7 @@ private module SuccSplits {
399399 ControlFlowElement succ , Completion c
400400 ) {
401401 pred = b .getAnElement ( ) and
402- b .isReachable ( predSplits ) and
402+ b .isReachable ( _ , predSplits ) and
403403 succ ( pred , succ , c )
404404 }
405405
@@ -728,12 +728,12 @@ private module Reachability {
728728 * Holds if the elements of this block are reachable from a callable entry
729729 * point, with the splits `splits`.
730730 */
731- predicate isReachable ( Splits splits ) {
731+ predicate isReachable ( CfgScope scope , Splits splits ) {
732732 // Base case
733- succEntrySplits ( _ , this , splits , _)
733+ succEntrySplits ( scope , this , splits , _)
734734 or
735735 // Recursive case
736- exists ( SameSplitsBlock pred , Splits predSplits | pred .isReachable ( predSplits ) |
736+ exists ( SameSplitsBlock pred , Splits predSplits | pred .isReachable ( scope , predSplits ) |
737737 this = pred .getASuccessor ( predSplits , splits )
738738 )
739739 }
@@ -791,43 +791,45 @@ private module Cached {
791791 newtype TCfgNode =
792792 TEntryNode ( CfgScope scope ) { succEntrySplits ( scope , _, _, _) } or
793793 TAnnotatedExitNode ( CfgScope scope , boolean normal ) {
794- exists ( Reachability:: SameSplitsBlock b , SuccessorType t | b .isReachable ( _) |
794+ exists ( Reachability:: SameSplitsBlock b , SuccessorType t | b .isReachable ( scope , _) |
795795 succExitSplits ( b .getAnElement ( ) , _, scope , t ) and
796796 if isAbnormalExitType ( t ) then normal = false else normal = true
797797 )
798798 } or
799799 TExitNode ( CfgScope scope ) {
800- exists ( Reachability:: SameSplitsBlock b | b .isReachable ( _) |
800+ exists ( Reachability:: SameSplitsBlock b | b .isReachable ( scope , _) |
801801 succExitSplits ( b .getAnElement ( ) , _, scope , _)
802802 )
803803 } 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+ )
806808 }
807809
808810 /** Gets a successor node of a given flow type, if any. */
809811 cached
810812 TCfgNode getASuccessor ( TCfgNode pred , SuccessorType t ) {
811813 // Callable entry node -> callable body
812814 exists ( ControlFlowElement succElement , Splits succSplits , CfgScope scope |
813- result = TElementNode ( succElement , succSplits ) and
815+ result = TElementNode ( scope , succElement , succSplits ) and
814816 pred = TEntryNode ( scope ) and
815817 succEntrySplits ( scope , succElement , succSplits , t )
816818 )
817819 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 )
820822 |
821823 // 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
824826 succExitSplits ( predElement , predSplits , scope , t ) and
825827 if isAbnormalExitType ( t ) then normal = false else normal = true
826828 )
827829 or
828830 // Element node -> element node
829831 exists ( ControlFlowElement succElement , Splits succSplits , Completion c |
830- result = TElementNode ( succElement , succSplits )
832+ result = TElementNode ( pragma [ only_bind_into ] ( scope ) , succElement , succSplits )
831833 |
832834 succSplits ( predElement , predSplits , succElement , succSplits , c ) and
833835 t = getAMatchingSuccessorType ( c )
@@ -853,6 +855,23 @@ private module Cached {
853855 */
854856 cached
855857 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+ }
856875}
857876
858877import Cached
0 commit comments