Model non-returning functions in CFG

go/ql/lib/semmle/go/Concepts.qll

@@ -431,7 +431,7 @@ private class HeuristicLoggerFunction extends Method {
     )
   }
 
-  override predicate mayReturnNormally() { logFunctionPrefix != "Fatal" }
+  override predicate mustNotReturnNormally() { logFunctionPrefix = "Fatal" }
 
   override predicate mustPanic() { logFunctionPrefix = "Panic" }
 }

go/ql/lib/semmle/go/Scopes.qll

@@ -437,11 +437,12 @@ class Function extends ValueEntity, @functionobject {
    * This predicate is an over-approximation: it may hold for functions that can never
    * return normally, but it never fails to hold for functions that can.
    *
-   * Note this is declared here and not in `DeclaredFunction` so that library models can override this
-   * by extending `Function` rather than having to remember to extend `DeclaredFunction`.
+   * Library models should not override this predicate; override `mustNotReturnNormally`
+   * instead, so that the control-flow graph construction can take the model into account.
    */
   predicate mayReturnNormally() {
     not this.mustPanic() and
+    not this.mustNotReturnNormally() and
     (ControlFlow::mayReturnNormally(this.getFuncDecl()) or not exists(this.getBody()))
   }
 
@@ -461,6 +462,16 @@ class Function extends ValueEntity, @functionobject {
    */
   predicate mustPanic() { none() }
 
+  /**
+   * Holds if calling this function never returns normally (for example because it
+   * always panics, exits the process, or loops forever).
+   *
+   * Unlike `mayReturnNormally`, this predicate must be defined without reference to
+   * the control-flow graph, so that it can be used during CFG construction to
+   * suppress normal-flow successors of calls to this function.
+   */
+  predicate mustNotReturnNormally() { none() }
+
   /** Gets the number of parameters of this function. */
   int getNumParameter() { result = this.getType().(SignatureType).getNumParameter() }
 

go/ql/lib/semmle/go/controlflow/ControlFlowGraphShared.qll

@@ -642,6 +642,18 @@ module GoCfg {
       c.asSimpleAbruptCompletion() instanceof ExceptionSuccessor and
       always = false
       or
+      // Calls to functions that never return normally (e.g. `os.Exit`, `log.Fatal`,
+      // `panic`) must suppress normal flow past the call site. We emit an `always`
+      // exception completion so that the shared library's default In->After step
+      // is suppressed.
+      ast instanceof Go::CallExpr and
+      exists(Go::Function target | target = ast.(Go::CallExpr).getTarget() |
+        target.mustPanic() or target.mustNotReturnNormally()
+      ) and
+      n.isIn(ast) and
+      c.asSimpleAbruptCompletion() instanceof ExceptionSuccessor and
+      always = true
+      or
       ast instanceof Go::DivExpr and
       not ast.(Go::Expr).isConst() and
       n.isIn(ast) and

go/ql/lib/semmle/go/frameworks/Glog.qll

@@ -59,7 +59,7 @@ module Glog {
     /** Holds if this function takes a format string. */
     predicate formatter() { format = "f" }
 
-    override predicate mayReturnNormally() { level != "Fatal" and level != "Exit" }
+    override predicate mustNotReturnNormally() { level = "Fatal" or level = "Exit" }
   }
 
   private class StringFormatter extends StringOps::Formatting::Range instanceof GlogFunction {

go/ql/lib/semmle/go/frameworks/Logrus.qll

@@ -29,8 +29,8 @@ module Logrus {
       )
     }
 
-    override predicate mayReturnNormally() {
-      not exists(string level, string suffix | level = ["Fatal", "Panic"] |
+    override predicate mustNotReturnNormally() {
+      exists(string level, string suffix | level = ["Fatal", "Panic"] |
         this.getName() = level + suffix
       )
     }

go/ql/lib/semmle/go/frameworks/Zap.qll

@@ -54,7 +54,7 @@ module Zap {
       this.hasQualifiedName(packagePath(), "SugaredLogger", "Fatal" + getSuffix())
     }
 
-    override predicate mayReturnNormally() { none() }
+    override predicate mustNotReturnNormally() { any() }
   }
 
   /** A Zap logging function which always panics. */

go/ql/lib/semmle/go/frameworks/stdlib/Log.qll

@@ -44,7 +44,7 @@ module Log {
       )
     }
 
-    override predicate mayReturnNormally() { none() }
+    override predicate mustNotReturnNormally() { any() }
   }
 
   /** A log function which must panic. */

go/ql/lib/semmle/go/frameworks/stdlib/Os.qll

@@ -12,7 +12,7 @@ module Os {
   private class Exit extends Function {
     Exit() { this.hasQualifiedName("os", "Exit") }
 
-    override predicate mayReturnNormally() { none() }
+    override predicate mustNotReturnNormally() { any() }
   }
 
   // These models are not implemented using Models-as-Data because they represent reverse flow.