@@ -14,9 +14,11 @@ module CfgImpl {
1414
1515 private module Cfg0 = CfgLib:: Make0< Go:: Location , Ast > ;
1616
17- private module Cfg1 = Cfg0:: Make1< Input > ;
17+ private module Cfg1 = Cfg0:: Make1< Input1 > ;
1818
19- private module Cfg2 = Cfg1:: Make2< Input > ;
19+ private module EarlyCfg2 = Cfg1:: Make2< EarlyInput2 > ;
20+
21+ private module Cfg2 = Cfg1:: Make2< FinalInput2 > ;
2022
2123 private import Cfg0
2224 private import Cfg1
@@ -27,7 +29,7 @@ module CfgImpl {
2729
2830 /** Holds if `e` has an implicit field selection at `index` for `implicitField`. */
2931 predicate implicitFieldSelection ( Go:: AstNode e , int index , Go:: Field implicitField ) {
30- Input :: implicitFieldSelection ( e , index , implicitField )
32+ Input1 :: implicitFieldSelection ( e , index , implicitField )
3133 }
3234
3335 /**
@@ -411,8 +413,8 @@ module CfgImpl {
411413 }
412414 }
413415
414- /** The Input module implementing InputSig1 and InputSig2 for Go . */
415- private module Input implements Cfg0:: InputSig1 , Cfg1 :: InputSig2 {
416+ /** Predicates shared by the two stages of Go CFG construction . */
417+ private module Input1 implements Cfg0:: InputSig1 {
416418 predicate cfgCachedStageRef ( ) { CfgCachedStage:: ref ( ) }
417419
418420 class CallableContext = Void ;
@@ -702,7 +704,7 @@ module CfgImpl {
702704 )
703705 }
704706
705- predicate beginAbruptCompletion (
707+ additional predicate beginAbruptCompletion (
706708 Ast:: AstNode ast , PreControlFlowNode n , AbruptCompletion c , boolean always
707709 ) {
708710 ast instanceof Go:: CallExpr and
@@ -759,7 +761,9 @@ module CfgImpl {
759761 always = false
760762 }
761763
762- predicate endAbruptCompletion ( Ast:: AstNode ast , PreControlFlowNode n , AbruptCompletion c ) {
764+ additional predicate endAbruptCompletion (
765+ Ast:: AstNode ast , PreControlFlowNode n , AbruptCompletion c
766+ ) {
763767 exists ( Go:: LabeledStmt lbl |
764768 ast = lbl .getStmt ( ) and
765769 n .isAfter ( lbl ) and
@@ -798,7 +802,9 @@ module CfgImpl {
798802 )
799803 }
800804
801- predicate overridesCallableEndAbruptCompletion ( Ast:: Callable c , AbruptCompletion completion ) {
805+ additional predicate overridesCallableEndAbruptCompletion (
806+ Ast:: Callable c , AbruptCompletion completion
807+ ) {
802808 // For functions with result variables, the library's default routing of a
803809 // `return` straight to the normal exit node is suppressed so that the
804810 // return is instead caught by `endAbruptCompletion` above and routed
@@ -811,7 +817,7 @@ module CfgImpl {
811817 completion .getSuccessorType ( ) instanceof ReturnSuccessor
812818 }
813819
814- predicate overridesAbruptCompletionEdge (
820+ additional predicate overridesAbruptCompletionEdge (
815821 PreControlFlowNode source , PreControlFlowNode target , AbruptCompletion completion
816822 ) {
817823 completion .getSuccessorType ( ) instanceof ExceptionSuccessor and
@@ -821,7 +827,7 @@ module CfgImpl {
821827 )
822828 }
823829
824- predicate callableExitStep ( PreControlFlowNode n , Ast:: Callable c , boolean normal ) {
830+ additional predicate callableExitStep ( PreControlFlowNode n , Ast:: Callable c , boolean normal ) {
825831 // The last result-read node of the epilogue steps to the normal exit node.
826832 exists ( Go:: FuncDef fd , int j | fd = c |
827833 normal = true and
@@ -870,15 +876,19 @@ module CfgImpl {
870876 * node. Walking this relation from a node stops at the next registration
871877 * node, which is how the reachability gate for deferred calls is computed.
872878 *
873- * This is typed over `PreControlFlowNode` and uses `succIgnoringDeferExit`
874- * so that it does not depend on `reachable` (which would otherwise create a
875- * non-monotonic cycle through `deferExitStep`).
879+ * This is computed over the early CFG, before deferred-invocation edges are
880+ * added to the final CFG.
876881 */
877882 private PreControlFlowNode succBeforeNextDeferRegistration ( PreControlFlowNode n ) {
878- succIgnoringDeferExit ( n , result , _ ) and
883+ earlySuccessor ( n ) = result and
879884 not deferRegistration ( result , _)
880885 }
881886
887+ /** Gets a successor of `n` in the early CFG, before deferred invocations are added. */
888+ private PreControlFlowNode earlySuccessor ( PreControlFlowNode n ) {
889+ exists ( EarlyCfg2:: ControlFlowNode early | early = n and result = early .getASuccessor ( ) )
890+ }
891+
882892 /** Gets a node reachable from `start` over `succBeforeNextDeferRegistration`, reflexively. */
883893 private PreControlFlowNode reachableBeforeNextDeferRegistration ( PreControlFlowNode start ) {
884894 result = start
@@ -901,7 +911,7 @@ module CfgImpl {
901911 exists ( PreControlFlowNode reg , PreControlFlowNode m |
902912 deferRegistration ( reg , s ) and
903913 m = reachableBeforeNextDeferRegistration ( funcEntry ( fd ) ) and
904- succIgnoringDeferExit ( m , reg , _ )
914+ earlySuccessor ( m ) = reg
905915 )
906916 }
907917
@@ -921,7 +931,7 @@ module CfgImpl {
921931 deferRegistration ( laterRegistration , laterRegistered ) and
922932 deferRegistration ( earlierRegistration , earlierRegistered ) and
923933 m = reachableBeforeNextDeferRegistration ( earlierRegistration ) and
924- succIgnoringDeferExit ( m , laterRegistration , _ )
934+ earlySuccessor ( m ) = laterRegistration
925935 )
926936 }
927937
@@ -968,7 +978,7 @@ module CfgImpl {
968978 target .( NormalExitNodeImpl ) .getEnclosingCallable ( ) = fd
969979 }
970980
971- predicate deferExitStep (
981+ additional predicate deferExitStep (
972982 PreControlFlowNode n1 , PreControlFlowNode n2 , SuccessorType successorType
973983 ) {
974984 exists ( Go:: FuncDef fd | funcHasDefer ( fd ) |
@@ -1018,9 +1028,11 @@ module CfgImpl {
10181028 )
10191029 }
10201030
1021- predicate overridesCallableBodyExit ( Ast:: Callable c ) { funcHasDefer ( c .( Go:: FuncDef ) ) }
1031+ additional predicate overridesCallableBodyExit ( Ast:: Callable c ) {
1032+ funcHasDefer ( c .( Go:: FuncDef ) )
1033+ }
10221034
1023- predicate overridesDefaultControlFlow ( Ast:: AstNode ast ) {
1035+ additional predicate overridesDefaultControlFlow ( Ast:: AstNode ast ) {
10241036 exists ( Go:: SelectStmt sel , Go:: RecvStmt recv |
10251037 recv = sel .getACommClause ( ) .getComm ( ) and
10261038 ( ast = recv or ast = recv .getExpr ( ) )
@@ -1031,13 +1043,13 @@ module CfgImpl {
10311043 )
10321044 }
10331045
1034- predicate preservesDefaultControlFlow ( Ast:: AstNode ast ) {
1046+ additional predicate preservesDefaultControlFlow ( Ast:: AstNode ast ) {
10351047 ast = any ( Go:: FuncDef fd | hasFuncDefPrologue ( fd ) ) .getBody ( )
10361048 or
10371049 exists ( getFirstEpilogueTag ( ast ) )
10381050 }
10391051
1040- predicate overridesDefaultControlFlowStep (
1052+ additional predicate overridesDefaultControlFlowStep (
10411053 Ast:: AstNode ast , PreControlFlowNode source , PreControlFlowNode target
10421054 ) {
10431055 ast = any ( Go:: FuncDef fd | hasFuncDefPrologue ( fd ) ) .getBody ( ) and source .isBefore ( ast )
@@ -1051,7 +1063,7 @@ module CfgImpl {
10511063 ( target .isIn ( ast ) or target .isAfter ( ast ) )
10521064 }
10531065
1054- predicate step ( PreControlFlowNode n1 , PreControlFlowNode n2 ) {
1066+ additional predicate step ( PreControlFlowNode n1 , PreControlFlowNode n2 ) {
10551067 rangeStmtStep ( n1 , n2 ) or
10561068 selectStmtStep ( n1 , n2 ) or
10571069 deferStmtStep ( n1 , n2 ) or
@@ -1734,4 +1746,100 @@ module CfgImpl {
17341746 )
17351747 }
17361748 }
1749+
1750+ /** Builds the CFG used to determine which `defer` statements have been registered. */
1751+ private module EarlyInput2 implements Cfg1:: InputSig2 {
1752+ predicate beginAbruptCompletion (
1753+ Ast:: AstNode ast , PreControlFlowNode n , AbruptCompletion c , boolean always
1754+ ) {
1755+ Input1:: beginAbruptCompletion ( ast , n , c , always )
1756+ }
1757+
1758+ predicate endAbruptCompletion ( Ast:: AstNode ast , PreControlFlowNode n , AbruptCompletion c ) {
1759+ Input1:: endAbruptCompletion ( ast , n , c )
1760+ or
1761+ exists ( Go:: FuncDef fd |
1762+ ast = fd .getBody ( ) and
1763+ c .getSuccessorType ( ) instanceof ReturnSuccessor and
1764+ exists ( fd .getResultVar ( 0 ) ) and
1765+ n .isAdditional ( fd .getBody ( ) , "result-read:0" )
1766+ )
1767+ }
1768+
1769+ predicate overridesCallableEndAbruptCompletion ( Ast:: Callable c , AbruptCompletion completion ) {
1770+ exists ( c .( Go:: FuncDef ) .getResultVar ( 0 ) ) and
1771+ completion .getSuccessorType ( ) instanceof ReturnSuccessor
1772+ }
1773+
1774+ predicate callableExitStep ( PreControlFlowNode n , Ast:: Callable c , boolean normal ) {
1775+ Input1:: callableExitStep ( n , c , normal )
1776+ }
1777+
1778+ predicate overridesDefaultControlFlow ( Ast:: AstNode ast ) {
1779+ Input1:: overridesDefaultControlFlow ( ast )
1780+ }
1781+
1782+ predicate preservesDefaultControlFlow ( Ast:: AstNode ast ) {
1783+ Input1:: preservesDefaultControlFlow ( ast )
1784+ }
1785+
1786+ predicate overridesDefaultControlFlowStep (
1787+ Ast:: AstNode ast , PreControlFlowNode source , PreControlFlowNode target
1788+ ) {
1789+ Input1:: overridesDefaultControlFlowStep ( ast , source , target )
1790+ }
1791+
1792+ predicate step ( PreControlFlowNode n1 , PreControlFlowNode n2 ) { Input1:: step ( n1 , n2 ) }
1793+ }
1794+
1795+ /** Builds the final Go CFG, including deferred invocations. */
1796+ private module FinalInput2 implements Cfg1:: InputSig2 {
1797+ predicate beginAbruptCompletion (
1798+ Ast:: AstNode ast , PreControlFlowNode n , AbruptCompletion c , boolean always
1799+ ) {
1800+ Input1:: beginAbruptCompletion ( ast , n , c , always )
1801+ }
1802+
1803+ predicate endAbruptCompletion ( Ast:: AstNode ast , PreControlFlowNode n , AbruptCompletion c ) {
1804+ Input1:: endAbruptCompletion ( ast , n , c )
1805+ }
1806+
1807+ predicate overridesCallableEndAbruptCompletion ( Ast:: Callable c , AbruptCompletion completion ) {
1808+ Input1:: overridesCallableEndAbruptCompletion ( c , completion )
1809+ }
1810+
1811+ predicate overridesAbruptCompletionEdge (
1812+ PreControlFlowNode source , PreControlFlowNode target , AbruptCompletion completion
1813+ ) {
1814+ Input1:: overridesAbruptCompletionEdge ( source , target , completion )
1815+ }
1816+
1817+ predicate callableExitStep ( PreControlFlowNode n , Ast:: Callable c , boolean normal ) {
1818+ Input1:: callableExitStep ( n , c , normal )
1819+ }
1820+
1821+ predicate deferExitStep (
1822+ PreControlFlowNode n1 , PreControlFlowNode n2 , SuccessorType successorType
1823+ ) {
1824+ Input1:: deferExitStep ( n1 , n2 , successorType )
1825+ }
1826+
1827+ predicate overridesCallableBodyExit ( Ast:: Callable c ) { Input1:: overridesCallableBodyExit ( c ) }
1828+
1829+ predicate overridesDefaultControlFlow ( Ast:: AstNode ast ) {
1830+ Input1:: overridesDefaultControlFlow ( ast )
1831+ }
1832+
1833+ predicate preservesDefaultControlFlow ( Ast:: AstNode ast ) {
1834+ Input1:: preservesDefaultControlFlow ( ast )
1835+ }
1836+
1837+ predicate overridesDefaultControlFlowStep (
1838+ Ast:: AstNode ast , PreControlFlowNode source , PreControlFlowNode target
1839+ ) {
1840+ Input1:: overridesDefaultControlFlowStep ( ast , source , target )
1841+ }
1842+
1843+ predicate step ( PreControlFlowNode n1 , PreControlFlowNode n2 ) { Input1:: step ( n1 , n2 ) }
1844+ }
17371845}
0 commit comments