@@ -543,6 +543,9 @@ module GoCfg {
543543 implicitFieldSelection ( n , i , implicitField ) and
544544 tag = "implicit-field:" + i .toString ( )
545545 )
546+ or
547+ // Deferred-call invocation node, placed at function exit by `deferExitStep`
548+ n = any ( Go:: DeferStmt s ) .getCall ( ) and tag = "defer-invoke"
546549 )
547550 }
548551
@@ -721,6 +724,7 @@ module GoCfg {
721724 or
722725 exists ( Go:: FuncDef fd |
723726 ast = fd .getBody ( ) and
727+ not funcHasDefer ( fd ) and
724728 c .getSuccessorType ( ) instanceof ReturnSuccessor and
725729 (
726730 // If the function has result variables, route the return completion
@@ -745,7 +749,11 @@ module GoCfg {
745749 // `return` straight to the normal exit node is suppressed so that the
746750 // return is instead caught by `endAbruptCompletion` above and routed
747751 // through the result-read epilogue.
748- exists ( c .( Go:: FuncDef ) .getResultVar ( 0 ) ) and
752+ //
753+ // For functions containing `defer` statements, the default routing is
754+ // likewise suppressed so that returns are routed through the deferred-call
755+ // epilogue (see `deferExitStep`) instead.
756+ ( exists ( c .( Go:: FuncDef ) .getResultVar ( 0 ) ) or funcHasDefer ( c .( Go:: FuncDef ) ) ) and
749757 completion .getSuccessorType ( ) instanceof ReturnSuccessor
750758 }
751759
@@ -759,6 +767,145 @@ module GoCfg {
759767 )
760768 }
761769
770+ /** Holds if `fd` contains at least one `defer` statement. */
771+ private predicate funcHasDefer ( Go:: FuncDef fd ) {
772+ exists ( Go:: DeferStmt s | s .getEnclosingFunction ( ) = fd )
773+ }
774+
775+ /**
776+ * Holds if `n` is the registration node of `defer` statement `s` (the
777+ * post-order node of the statement, reached once its call's arguments have
778+ * been evaluated).
779+ *
780+ * This uses the reachability-free `isInOrderNode` rather than `n.isIn(s)`
781+ * because it is referenced under negation by `notDeferSucc`, and must
782+ * therefore not depend on `reachable`.
783+ */
784+ private predicate deferRegistration ( PreControlFlowNode n , Go:: DeferStmt s ) {
785+ isInOrderNode ( n , s )
786+ }
787+
788+ /**
789+ * Holds if `n` is the deferred-invocation node for `defer` statement `s`,
790+ * which models the deferred call running at function exit.
791+ */
792+ private predicate deferInvoke ( PreControlFlowNode n , Go:: DeferStmt s ) {
793+ n .isAdditional ( s .getCall ( ) , "defer-invoke" )
794+ }
795+
796+ /**
797+ * Gets a defer-free successor of `n` that is not a `defer` registration
798+ * node. Walking this relation from a node stops at the next registration
799+ * node, which is how the reachability gate for deferred calls is computed.
800+ *
801+ * This is typed over `PreControlFlowNode` and uses `succIgnoringDeferExit`
802+ * so that it does not depend on `reachable` (which would otherwise create a
803+ * non-monotonic cycle through `deferExitStep`).
804+ */
805+ private PreControlFlowNode notDeferSucc ( PreControlFlowNode n ) {
806+ succIgnoringDeferExit ( n , result , _) and
807+ not deferRegistration ( result , _)
808+ }
809+
810+ /** Gets a node reachable from `start` over `notDeferSucc`, reflexively. */
811+ private PreControlFlowNode notDeferReach ( PreControlFlowNode start ) {
812+ result = start
813+ or
814+ result = notDeferSucc ( notDeferReach ( start ) )
815+ }
816+
817+ /** Gets the entry node of `fd`. */
818+ private PreControlFlowNode funcEntry ( Go:: FuncDef fd ) {
819+ result .( EntryNodeImpl ) .getEnclosingCallable ( ) = fd
820+ }
821+
822+ /**
823+ * Holds if `s` can be the first `defer` statement registered in `fd`, and
824+ * hence the last to run: its registration node is reachable from the entry
825+ * node without passing through another registration node.
826+ */
827+ private predicate firstDefer ( Go:: DeferStmt s , Go:: FuncDef fd ) {
828+ s .getEnclosingFunction ( ) = fd and
829+ exists ( PreControlFlowNode reg , PreControlFlowNode m |
830+ deferRegistration ( reg , s ) and
831+ m = notDeferReach ( funcEntry ( fd ) ) and
832+ succIgnoringDeferExit ( m , reg , _)
833+ )
834+ }
835+
836+ /**
837+ * Holds if the registration node of `predD` is the next registration node
838+ * reachable from the registration node of `succD`. Then `predD` is
839+ * registered immediately after `succD` and therefore runs immediately
840+ * before it (deferred calls run in last-in-first-out order).
841+ */
842+ private predicate nextDefer ( Go:: DeferStmt predD , Go:: DeferStmt succD ) {
843+ exists ( PreControlFlowNode regPred , PreControlFlowNode regSucc , PreControlFlowNode m |
844+ deferRegistration ( regPred , predD ) and
845+ deferRegistration ( regSucc , succD ) and
846+ m = notDeferReach ( regSucc ) and
847+ succIgnoringDeferExit ( m , regPred , _)
848+ )
849+ }
850+
851+ /**
852+ * Holds if `n` is a normal-exit predecessor of `fd`: a `return` statement
853+ * node, or the fall-through node after the body.
854+ */
855+ private predicate normalExitPred ( PreControlFlowNode n , Go:: FuncDef fd ) {
856+ exists ( Go:: ReturnStmt ret | ret .getEnclosingFunction ( ) = fd and n .isIn ( ret ) )
857+ or
858+ n .isAfter ( fd .getBody ( ) )
859+ }
860+
861+ /**
862+ * Holds if, after running its deferred calls, `fd` should continue at
863+ * `target` on a normal exit. For functions with result variables this is
864+ * the start of the result-read epilogue; otherwise it is the normal exit
865+ * node directly.
866+ */
867+ private predicate deferChainExitTarget ( Go:: FuncDef fd , PreControlFlowNode target ) {
868+ exists ( fd .getResultVar ( 0 ) ) and target .isAdditional ( fd .getBody ( ) , "result-read:0" )
869+ or
870+ not exists ( fd .getResultVar ( _) ) and
871+ target .( NormalExitNodeImpl ) .getEnclosingCallable ( ) = fd
872+ }
873+
874+ predicate deferExitStep ( PreControlFlowNode n1 , PreControlFlowNode n2 ) {
875+ exists ( Go:: FuncDef fd | funcHasDefer ( fd ) |
876+ // (a) an exit predecessor with no active defer flows straight to the exit target
877+ normalExitPred ( n1 , fd ) and
878+ n1 = notDeferReach ( funcEntry ( fd ) ) and
879+ deferChainExitTarget ( fd , n2 )
880+ or
881+ // (b) an exit predecessor flows to the invocation of the last-registered active defer
882+ exists ( Go:: DeferStmt d , PreControlFlowNode reg |
883+ deferRegistration ( reg , d ) and
884+ d .getEnclosingFunction ( ) = fd and
885+ normalExitPred ( n1 , fd ) and
886+ n1 = notDeferReach ( reg ) and
887+ deferInvoke ( n2 , d )
888+ )
889+ or
890+ // (c) deferred invocations chain in last-in-first-out order
891+ exists ( Go:: DeferStmt predD , Go:: DeferStmt succD |
892+ predD .getEnclosingFunction ( ) = fd and
893+ nextDefer ( predD , succD ) and
894+ deferInvoke ( n1 , predD ) and
895+ deferInvoke ( n2 , succD )
896+ )
897+ or
898+ // (d) the invocation of the first-registered (last to run) defer flows to the exit target
899+ exists ( Go:: DeferStmt firstD |
900+ firstDefer ( firstD , fd ) and
901+ deferInvoke ( n1 , firstD ) and
902+ deferChainExitTarget ( fd , n2 )
903+ )
904+ )
905+ }
906+
907+ predicate overridesCallableBodyExit ( Ast:: Callable c ) { funcHasDefer ( c .( Go:: FuncDef ) ) }
908+
762909 predicate step ( PreControlFlowNode n1 , PreControlFlowNode n2 ) {
763910 rangeLoop ( n1 , n2 ) or
764911 switchStmt ( n1 , n2 ) or
0 commit comments