Lower statically unreachable code to unreachable ()

src/main.rs

@@ -162,6 +162,8 @@ fn main() {
     }
 
     // Run passes
+    pass::builtins::builtins(&mut combined_tu);
+
     let t = Instant::now();
     pass::prune::prune(&mut combined_tu);
     if cli.time_passes {

src/pass/builtins.rs

@@ -0,0 +1,82 @@
+//! Model the C builtins PAL understands.
+//!
+//! `__builtin_unreachable()` is a claim that control never reaches this point.
+//! It is how a `noreturn` abort is spelled to the C compiler, and code that
+//! ends a switch's default arm with one relies on it: without it the compiler
+//! reports the fall-through as a use of an uninitialized variable.
+//!
+//! Pulse spells the same claim `unreachable ()`, which PAL already emits for
+//! `_assert(false)`, so the builtin is rewritten to exactly that. The claim is
+//! discharged, not assumed: an arm PAL cannot show is dead is an error.
+
+use std::rc::Rc;
+
+use crate::ir::*;
+
+const UNREACHABLE: &str = "__builtin_unreachable";
+
+fn is_unreachable_call(stmt: &Stmt) -> bool {
+    let StmtT::Call(expr) = &stmt.val else {
+        return false;
+    };
+    let ExprT::FnCall(name, args) = &expr.val else {
+        return false;
+    };
+    &*name.val == UNREACHABLE && args.is_empty()
+}
+
+fn rewrite_stmts(stmts: &mut Stmts) {
+    for stmt in stmts.iter_mut() {
+        rewrite_stmt(stmt);
+    }
+}
+
+fn rewrite_shared_stmts(stmts: &mut Rc<Stmts>) {
+    rewrite_stmts(Rc::make_mut(stmts));
+}
+
+fn rewrite_stmt(stmt: &mut Rc<Stmt>) {
+    if is_unreachable_call(stmt) {
+        let loc = stmt.loc.clone();
+        let f = Rc::new(Ast {
+            val: ExprT::BoolLit(false),
+            loc: loc.clone(),
+        });
+        *stmt = Rc::new(Ast {
+            val: StmtT::Assert(f),
+            loc,
+        });
+        return;
+    }
+    match &mut Rc::make_mut(stmt).val {
+        StmtT::If {
+            then_branch,
+            else_branch,
+            ..
+        } => {
+            rewrite_shared_stmts(then_branch);
+            rewrite_shared_stmts(else_branch);
+        }
+        StmtT::Match {
+            branches,
+            default_branch,
+            ..
+        } => {
+            for branch in Rc::make_mut(branches).iter_mut() {
+                rewrite_shared_stmts(&mut Rc::make_mut(branch).body);
+            }
+            rewrite_shared_stmts(default_branch);
+        }
+        StmtT::While { body, .. } => rewrite_shared_stmts(body),
+        StmtT::GotoBlock { body, .. } => rewrite_shared_stmts(body),
+        _ => {}
+    }
+}
+
+pub fn builtins(tu: &mut TranslationUnit) {
+    for decl in tu.decls.iter_mut() {
+        if let DeclT::FnDefn(FnDefn { body, .. }) = &mut decl.val {
+            rewrite_stmts(body);
+        }
+    }
+}

src/pass/emit.rs

@@ -4303,6 +4303,14 @@ impl<'a> Emitter<'a> {
                     .group()
                     .nest(2),
                 StmtT::Return(None) => Doc::text("return;"),
+                // `_assert(false)` is a claim that control never reaches this
+                // point, not a proposition to carry forward. Pulse spells that
+                // `unreachable ()`, whose postcondition is `pure False`, so the
+                // branch absorbs whatever the join needs instead of having to
+                // agree with its siblings' resources. Asserting `with_pure
+                // False` would instead leave the branch's own footprint in the
+                // join and make an unreachable arm the reason a proof fails.
+                StmtT::Assert(v) if is_statically_false(v) => Doc::text("unreachable ();"),
                 StmtT::Assert(v) => Doc::text("assert")
                     .append(Doc::line())
                     .append(self.emit_rvalue(env, v))
@@ -4636,6 +4644,21 @@ fn mk_attrs(attrs: Vec<Doc>) -> Doc {
         .append(Doc::line())
 }
 
+/// Recognize an assertion condition that is syntactically the constant false.
+///
+/// `_assert` bodies are C-preprocessed, so a source-level `false` reaches us as
+/// the integer literal `0` once `<stdbool.h>` has had its way, and it may be
+/// wrapped in whatever casts the surrounding macro applied. Look through casts
+/// and accept either spelling.
+fn is_statically_false(e: &Rc<Expr>) -> bool {
+    match &e.val {
+        ExprT::BoolLit(b) => !b,
+        ExprT::IntLit(n, _) => **n == BigInt::from(0),
+        ExprT::Cast(inner, _) => is_statically_false(inner),
+        _ => false,
+    }
+}
+
 fn mk_assume_val(attrs: Vec<Doc>, n: Doc, args: &[Doc], ty: Doc) -> Doc {
     mk_attrs(attrs)
         .append(

src/pass/mod.rs

@@ -1,3 +1,4 @@
+pub mod builtins;
 pub mod check;
 pub mod decay;
 pub mod elab;

test/builtin_unreachable/Makefile

@@ -0,0 +1 @@
+../_templates/Makefile

test/builtin_unreachable/builtin_unreachable.c

@@ -0,0 +1,42 @@
+// `__builtin_unreachable()` is how a `noreturn` abort is spelled to the C
+// compiler. A switch whose default arm can only be reached by a caller that
+// broke a precondition ends with one, and without it the compiler reports the
+// fall-through as a use of an uninitialized variable.
+//
+// PAL models it as the claim it is: `unreachable ()`, discharged rather than
+// assumed. The preconditions below are what make the dead arms dead; dropping
+// either makes this file fail to verify.
+#include "pal.h"
+#include <stdint.h>
+
+uint32_t
+pick(uint32_t version) _requires(version == 1 || version == 2)
+{
+    uint32_t result = 0;
+
+    switch (version)
+    {
+    case 1:
+        result = 10;
+        break;
+    case 2:
+        result = 20;
+        break;
+    default:
+        __builtin_unreachable();
+    }
+
+    return result;
+}
+
+// The same shape without a switch: a tail the caller's precondition rules out.
+uint32_t
+halve(uint32_t n) _requires(n % 2 == 0)
+{
+    if (n % 2 != 0)
+    {
+        __builtin_unreachable();
+    }
+
+    return n / 2;
+}

test/builtin_unreachable/fstar.fst.config.json

@@ -0,0 +1 @@
+../_templates/fstar.fst.config.json

test/builtin_unreachable/pal.config.json

@@ -0,0 +1 @@
+../_templates/pal.config.json

test/builtin_unreachable/pal.h

@@ -0,0 +1 @@
+../pal.h