@@ -740,6 +740,25 @@ module GoCfg {
740740 )
741741 }
742742
743+ predicate overridesCallableEndAbruptCompletion ( Ast:: Callable c , AbruptCompletion completion ) {
744+ // For functions with result variables, the library's default routing of a
745+ // `return` straight to the normal exit node is suppressed so that the
746+ // return is instead caught by `endAbruptCompletion` above and routed
747+ // through the result-read epilogue.
748+ exists ( c .( Go:: FuncDef ) .getResultVar ( 0 ) ) and
749+ completion .getSuccessorType ( ) instanceof ReturnSuccessor
750+ }
751+
752+ predicate callableExitStep ( PreControlFlowNode n , Ast:: Callable c , boolean normal ) {
753+ // The last result-read node of the epilogue steps to the normal exit node.
754+ exists ( Go:: FuncDef fd , int j | fd = c |
755+ normal = true and
756+ exists ( fd .getResultVar ( j ) ) and
757+ not exists ( fd .getResultVar ( j + 1 ) ) and
758+ n .isAdditional ( fd .getBody ( ) , "result-read:" + j .toString ( ) )
759+ )
760+ }
761+
743762 predicate step ( PreControlFlowNode n1 , PreControlFlowNode n2 ) {
744763 rangeLoop ( n1 , n2 ) or
745764 switchStmt ( n1 , n2 ) or
@@ -1566,9 +1585,10 @@ module GoCfg {
15661585 * - Prologue: Before(body) → arg:-1 → param-init:-1 → arg:0 → param-init:0 → ...
15671586 * when a receiver exists; otherwise it starts at arg:0. Then
15681587 * result-zero-init:0 → result-init:0 → ... → first statement
1569- * - Epilogue: return → result-read:0 → result-read:1 → ... → After(body)
1588+ * - Epilogue: return → result-read:0 → result-read:1 → ... → result-read:last
15701589 *
1571- * `After(body)` goes to `NormalExit(fd)` via the shared library's built-in step.
1590+ * The last result-read node goes to `NormalExit(fd)` via the shared
1591+ * library's `callableExitStep` hook.
15721592 */
15731593 private predicate hasFuncDefPrologue ( Go:: FuncDef fd ) {
15741594 exists ( fd .getParameter ( _) ) or exists ( fd .getResultVar ( _) )
@@ -1667,15 +1687,11 @@ module GoCfg {
16671687 or
16681688 funcDefBodyStep ( fd , n1 , n2 )
16691689 or
1670- // result-read:j → result-read:(j+1) or After(body)
1671- exists ( int j | exists ( fd .getResultVar ( j ) ) |
1690+ // result-read:j → result-read:(j+1); the last result-read node steps to
1691+ // the normal exit node via the `callableExitStep` hook.
1692+ exists ( int j | exists ( fd .getResultVar ( j + 1 ) ) |
16721693 n1 .isAdditional ( fd .getBody ( ) , "result-read:" + j .toString ( ) ) and
1673- (
1674- exists ( fd .getResultVar ( j + 1 ) ) and
1675- n2 .isAdditional ( fd .getBody ( ) , "result-read:" + ( j + 1 ) .toString ( ) )
1676- or
1677- not exists ( fd .getResultVar ( j + 1 ) ) and n2 .isAfter ( fd .getBody ( ) )
1678- )
1694+ n2 .isAdditional ( fd .getBody ( ) , "result-read:" + ( j + 1 ) .toString ( ) )
16791695 )
16801696 )
16811697 }
0 commit comments