Lower statically unreachable code to unreachable ()

[nikswamy]

Part of the upstreaming of nswamy/pal-c-project-integration (PR18 of 35 PRs) — see PR_PLAN.md on that branch for the whole plan and the dependency graph.

Base: main. Depends on nothing; reviewable on its own.

_assert(false) in a dead default: arm is a claim that control never reaches there, not
a proposition to carry forward; emitting assert (with_pure (0 <> 0)) left the arm's own
footprint in the enclosing join, which then came out as an irreducible match on the
scrutinee — making an unreachable arm the reason a proof failed. Recognizes a statically
false condition through casts and emits unreachable (), whose postcondition pure False
absorbs whatever the join needs. __builtin_unreachable — how a noreturn abort is spelled
to the C compiler, and required for a dead default arm to compile at all — is rewritten to
the same thing. The claim is discharged, never assumed.

Commits

• Lower a statically-false assertion to unreachable ()
• Translate __builtin_unreachable

Testing

Verified: make rust lib, test/check-template.sh, cargo fmt --check, clang-format --dry-run --Werror, and F* verification of test/builtin_unreachable.

[gebner]

!diff

[github-actions]

Generated F* output diff

Effect of this pull request on the F* code pal generates for the test suite (f9d4dd2 → 4b18914).

Summary

 /dev/null => head/builtin_unreachable/Func_halve.fst         | 20 ++++++++++++++++++++
 /dev/null => head/builtin_unreachable/Func_halve.fsti        | 11 +++++++++++
 /dev/null => head/builtin_unreachable/Func_pick.fst          | 41 +++++++++++++++++++++++++++++++++++++++++
 /dev/null => head/builtin_unreachable/Func_pick.fsti         | 12 ++++++++++++
 /dev/null => head/builtin_unreachable/TranslationErrors.fst  |  1 +
 /dev/null => head/builtin_unreachable/Typedef___uint32_t.fst | 13 +++++++++++++
 /dev/null => head/builtin_unreachable/Typedef_uint32_t.fst   | 13 +++++++++++++
 /dev/null => head/builtin_unreachable/diagnostics.json       |  1 +
 8 files changed, 112 insertions(+)

Full diff: full diff artifact

Diff

diff --git head/builtin_unreachable/Func_halve.fst head/builtin_unreachable/Func_halve.fst
new file mode 100644
index 0000000..a2ba161
--- /dev/null
+++ head/builtin_unreachable/Func_halve.fst
@@ -0,0 +1,20 @@
+module Func_halve
+open Pulse
+open Pulse.Lib.C
+#lang-pulse
+
+divergent fn func_halve (var_n: Typedef_uint32_t.ty_uint32_t)
+  requires ((Typedef_uint32_t.ty_uint32_t__pred var_n 1.0R))
+  requires (with_pure (((id #int (UInt32.v var_n)) % 2) = 0))
+  returns return_1 : Typedef_uint32_t.ty_uint32_t
+  ensures ((Typedef_uint32_t.ty_uint32_t__pred var_n 1.0R))
+  ensures ((Typedef_uint32_t.ty_uint32_t__pred return_1 1.0R))
+{
+  let mut var_n = var_n;
+  if ((not
+        (((!var_n) `UInt32.rem` (id #UInt32.t (Int.Cast.int32_to_uint32 2l))) =
+          (id #UInt32.t (Int.Cast.int32_to_uint32 0l))))) {
+    unreachable ();
+  } else {};
+  return ((!var_n) `UInt32.div` (id #UInt32.t (Int.Cast.int32_to_uint32 2l)));
+}
\ No newline at end of file
diff --git head/builtin_unreachable/Func_halve.fsti head/builtin_unreachable/Func_halve.fsti
new file mode 100644
index 0000000..3453e7a
--- /dev/null
+++ head/builtin_unreachable/Func_halve.fsti
@@ -0,0 +1,11 @@
+module Func_halve
+open Pulse
+open Pulse.Lib.C
+#lang-pulse
+
+divergent fn func_halve (var_n: Typedef_uint32_t.ty_uint32_t)
+requires ((Typedef_uint32_t.ty_uint32_t__pred var_n 1.0R))
+requires (with_pure (((id #int (UInt32.v var_n)) % 2) = 0))
+returns return_1 : Typedef_uint32_t.ty_uint32_t
+ensures ((Typedef_uint32_t.ty_uint32_t__pred var_n 1.0R))
+ensures ((Typedef_uint32_t.ty_uint32_t__pred return_1 1.0R))
\ No newline at end of file
diff --git head/builtin_unreachable/Func_pick.fst head/builtin_unreachable/Func_pick.fst
new file mode 100644
index 0000000..f2fd7a3
--- /dev/null
+++ head/builtin_unreachable/Func_pick.fst
@@ -0,0 +1,41 @@
+module Func_pick
+open Pulse
+open Pulse.Lib.C
+#lang-pulse
+
+divergent fn func_pick (var_version: Typedef_uint32_t.ty_uint32_t)
+  requires ((Typedef_uint32_t.ty_uint32_t__pred var_version 1.0R))
+  requires
+    (with_pure (((id #int (UInt32.v var_version)) = 1) || ((id #int (UInt32.v var_version)) = 2)))
+  returns return_1 : Typedef_uint32_t.ty_uint32_t
+  ensures ((Typedef_uint32_t.ty_uint32_t__pred var_version 1.0R))
+  ensures ((Typedef_uint32_t.ty_uint32_t__pred return_1 1.0R))
+{
+  let mut var_version = var_version;
+  let mut var_result : Typedef_uint32_t.ty_uint32_t;
+  var_result := (id #UInt32.t (Int.Cast.int32_to_uint32 0l));
+  let var___switch_scrut_0 : Typedef_uint32_t.ty_uint32_t = (!var_version);
+  let mut var___switch_hit_0 : bool;
+  var___switch_hit_0 := false;
+  let mut var___switch_brk_0 : bool;
+  var___switch_brk_0 := false;
+  if (((not (!var___switch_brk_0)) &&
+        ((!var___switch_hit_0) ||
+          (false || (var___switch_scrut_0 = (id #UInt32.t (Int.Cast.int32_to_uint32 1l))))))) {
+    var___switch_hit_0 := true;
+    var_result := (id #UInt32.t (Int.Cast.int32_to_uint32 10l));
+    var___switch_brk_0 := true;
+  } else {};
+  if (((not (!var___switch_brk_0)) &&
+        ((!var___switch_hit_0) ||
+          (false || (var___switch_scrut_0 = (id #UInt32.t (Int.Cast.int32_to_uint32 2l))))))) {
+    var___switch_hit_0 := true;
+    var_result := (id #UInt32.t (Int.Cast.int32_to_uint32 20l));
+    var___switch_brk_0 := true;
+  } else {};
+  if ((not (!var___switch_brk_0))) {
+    var___switch_hit_0 := true;
+    unreachable ();
+  } else {};
+  return (!var_result);
+}
\ No newline at end of file
diff --git head/builtin_unreachable/Func_pick.fsti head/builtin_unreachable/Func_pick.fsti
new file mode 100644
index 0000000..dffbbae
--- /dev/null
+++ head/builtin_unreachable/Func_pick.fsti
@@ -0,0 +1,12 @@
+module Func_pick
+open Pulse
+open Pulse.Lib.C
+#lang-pulse
+
+divergent fn func_pick (var_version: Typedef_uint32_t.ty_uint32_t)
+requires ((Typedef_uint32_t.ty_uint32_t__pred var_version 1.0R))
+requires
+  (with_pure (((id #int (UInt32.v var_version)) = 1) || ((id #int (UInt32.v var_version)) = 2)))
+returns return_1 : Typedef_uint32_t.ty_uint32_t
+ensures ((Typedef_uint32_t.ty_uint32_t__pred var_version 1.0R))
+ensures ((Typedef_uint32_t.ty_uint32_t__pred return_1 1.0R))
\ No newline at end of file
diff --git head/builtin_unreachable/TranslationErrors.fst head/builtin_unreachable/TranslationErrors.fst
new file mode 100644
index 0000000..bf62561
--- /dev/null
+++ head/builtin_unreachable/TranslationErrors.fst
@@ -0,0 +1 @@
+module TranslationErrors
diff --git head/builtin_unreachable/Typedef___uint32_t.fst head/builtin_unreachable/Typedef___uint32_t.fst
new file mode 100644
index 0000000..b9a5b44
--- /dev/null
+++ head/builtin_unreachable/Typedef___uint32_t.fst
@@ -0,0 +1,13 @@
+module Typedef___uint32_t
+open Pulse
+open Pulse.Lib.C
+#lang-pulse
+
+unfold
+let ty___uint32_t : Type = UInt32.t
+[@@pulse_eager_unfold] let predicate ty___uint32_t__pred ([@@@mkey] this: ty___uint32_t) (p: perm) =
+  emp
+[@@pulse_eager_unfold] let predicate ty___uint32_t__uninit_pred ([@@@mkey] this: ty___uint32_t) =
+  emp
+instance has_zero_default_ty___uint32_t : (has_zero_default ty___uint32_t) =
+  { zero_default = (UInt32.uint_to_t 0) }
\ No newline at end of file
diff --git head/builtin_unreachable/Typedef_uint32_t.fst head/builtin_unreachable/Typedef_uint32_t.fst
new file mode 100644
index 0000000..aa0f488
--- /dev/null
+++ head/builtin_unreachable/Typedef_uint32_t.fst
@@ -0,0 +1,13 @@
+module Typedef_uint32_t
+open Pulse
+open Pulse.Lib.C
+#lang-pulse
+
+unfold
+let ty_uint32_t : Type = Typedef___uint32_t.ty___uint32_t
+[@@pulse_eager_unfold] let predicate ty_uint32_t__pred ([@@@mkey] this: ty_uint32_t) (p: perm) =
+  ((Typedef___uint32_t.ty___uint32_t__pred this p))
+[@@pulse_eager_unfold] let predicate ty_uint32_t__uninit_pred ([@@@mkey] this: ty_uint32_t) =
+  ((Typedef___uint32_t.ty___uint32_t__uninit_pred this))
+instance has_zero_default_ty_uint32_t : (has_zero_default ty_uint32_t) =
+  { zero_default = zero_default }
\ No newline at end of file
diff --git head/builtin_unreachable/diagnostics.json head/builtin_unreachable/diagnostics.json
new file mode 100644
index 0000000..9e26dfe
--- /dev/null
+++ head/builtin_unreachable/diagnostics.json
@@ -0,0 +1 @@
+{}
\ No newline at end of file