From 31a249b771494a7bb1f30d74131a5eff4744c7f3 Mon Sep 17 00:00:00 2001 From: Nikhil Swamy Date: Thu, 13 Aug 2026 02:03:46 -0700 Subject: [PATCH 1/4] Give each record type the size its ABI assigns it `sizeof(T)` translated to `Pulse.Lib.C.Sizeof.c_sizeof T`, which commits to no particular value. That is fine for comparing a size against itself, but it leaves any arithmetic over sizes unbounded: a proof cannot show that `sizeof(A) + n + sizeof(B)` does not overflow `size_t` when the two sizes could be anything. clang already knows what the target ABI gives every complete record type. Carry that number on the record's definition and emit it, in the record's own generated module, as a refinement-typed constant that `sizeof` sites then refer to: assume val struct__pair__c_sizeof : (n: FStar.SizeT.t{FStar.SizeT.v n == 8 /\ n == c_sizeof struct__pair}) Introducing the size once, on the type, is what keeps this sound. Stating it at each `sizeof` site instead would let two sites claim different sizes for the same type. A refinement-typed constant rather than a lemma with an `SMTPat` because the size of a specific type is a ground fact, and a trigger for it would contain no variable, which Z3 warns about and F* then rejects. Non-record types are unaffected and still size opaquely. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> Copilot-Session: 981f7d3c-6a91-47ad-84d7-7aadf747123d (cherry picked from commit 79734417766218e249b4e3e4cf5ce0e585641279) --- cpp/iface.zng | 1 + cpp/impl.cpp | 11 +++ src/clang.rs | 8 +++ src/env.rs | 1 + src/ir/mod.rs | 5 ++ src/pass/check.rs | 6 +- src/pass/elab.rs | 6 +- src/pass/elim_cis.rs | 1 + src/pass/emit.rs | 98 +++++++++++++++++++++++++-- src/pass/prune.rs | 7 +- test/sizeof_abi/Makefile | 1 + test/sizeof_abi/fstar.fst.config.json | 1 + test/sizeof_abi/pal.config.json | 1 + test/sizeof_abi/pal.h | 1 + test/sizeof_abi/sizeof_abi.c | 41 +++++++++++ 15 files changed, 179 insertions(+), 10 deletions(-) create mode 120000 test/sizeof_abi/Makefile create mode 120000 test/sizeof_abi/fstar.fst.config.json create mode 120000 test/sizeof_abi/pal.config.json create mode 120000 test/sizeof_abi/pal.h create mode 100644 test/sizeof_abi/sizeof_abi.c diff --git a/cpp/iface.zng b/cpp/iface.zng index 210d2888..9684736e 100644 --- a/cpp/iface.zng +++ b/cpp/iface.zng @@ -231,6 +231,7 @@ mod crate::clang { fn set_rec(&mut self); fn set_total(&mut self); fn set_eager_unfold_pred(&mut self); + fn set_abi_size(&mut self, u64); fn decreases(&mut self, Rc); } diff --git a/cpp/impl.cpp b/cpp/impl.cpp index 63a7b7a3..409dfe5f 100644 --- a/cpp/impl.cpp +++ b/cpp/impl.cpp @@ -329,6 +329,17 @@ class PALConsumer : public ASTConsumer { return; auto loc = getRange(decl->getSourceRange()); auto builder = DeclBuilder::new_(loc.clone(), ident.clone()); + // Record the ABI size clang computed for this record, so that the + // generated module can pin down `c_sizeof` for it. Dependent or + // incomplete types have no constant size; leave those unpinned. + { + auto recTy = decl->getASTContext().getRecordType(decl); + if (!recTy->isDependentType() && + !decl->getASTContext().getAsIncompleteArrayType(recTy)) + builder.set_abi_size((uint64_t)decl->getASTContext() + .getTypeSizeInChars(recTy) + .getQuantity()); + } if (decl->getTagKind() == TagTypeKind::Struct) { builder.refines(trTypeAttrs(decl->getAttrs(), mk_type_struct(loc.clone(), ident.clone()))); diff --git a/src/clang.rs b/src/clang.rs index dbd54f57..920657d2 100644 --- a/src/clang.rs +++ b/src/clang.rs @@ -148,6 +148,7 @@ impl<'a> Ctx<'a> { refines: builder.refines.unwrap(), fields: builder.fields, eager_unfold_pred: builder.eager_unfold_pred, + abi_size: builder.abi_size, }), }) } @@ -165,6 +166,7 @@ impl<'a> Ctx<'a> { val: DeclT::UnionDefn(UnionDefn { name: builder.name, fields: builder.fields, + abi_size: builder.abi_size, }), }) } @@ -435,6 +437,7 @@ struct DeclBuilder { is_total: bool, decreases: Option>, eager_unfold_pred: bool, + abi_size: Option, } impl DeclBuilder { @@ -454,6 +457,7 @@ impl DeclBuilder { is_total: false, decreases: None, eager_unfold_pred: false, + abi_size: None, } } @@ -521,6 +525,10 @@ impl DeclBuilder { fn set_eager_unfold_pred(&mut self) { self.eager_unfold_pred = true; } + + fn set_abi_size(&mut self, size: u64) { + self.abi_size = Some(size); + } fn decreases(&mut self, p: Rc) { self.decreases = Some(p); } diff --git a/src/env.rs b/src/env.rs index a7ad8905..bb1c6420 100644 --- a/src/env.rs +++ b/src/env.rs @@ -174,6 +174,7 @@ impl Env { .with_loc(name.loc.clone()), fields: vec![], eager_unfold_pred: false, + abi_size: None, }); } } diff --git a/src/ir/mod.rs b/src/ir/mod.rs index 4a592da7..00ed4c40 100644 --- a/src/ir/mod.rs +++ b/src/ir/mod.rs @@ -459,6 +459,9 @@ pub struct StructDefn { pub refines: Rc, pub fields: Vec, pub eager_unfold_pred: bool, + /// The size, in bytes, that the target ABI gives this type, as reported by + /// clang. `None` when the size is not a compile-time constant. + pub abi_size: Option, } impl StructDefn { @@ -483,6 +486,8 @@ impl StructDefn { pub struct UnionDefn { pub name: Rc, pub fields: Vec, + /// See `StructDefn::abi_size`. + pub abi_size: Option, } impl UnionDefn { diff --git a/src/pass/check.rs b/src/pass/check.rs index aeab9291..10da82a0 100644 --- a/src/pass/check.rs +++ b/src/pass/check.rs @@ -825,7 +825,11 @@ impl<'a> Checker<'a> { } } DeclT::StructDecl(_) => {} - DeclT::UnionDefn(UnionDefn { name: _, fields }) => { + DeclT::UnionDefn(UnionDefn { + name: _, + fields, + abi_size: _, + }) => { for f in fields { self.check_field(env, f, fields); } diff --git a/src/pass/elab.rs b/src/pass/elab.rs index e967b321..ca0d2e37 100644 --- a/src/pass/elab.rs +++ b/src/pass/elab.rs @@ -1255,7 +1255,11 @@ impl<'a> Elaborator<'a> { } } DeclT::StructDecl(_) => {} - DeclT::UnionDefn(UnionDefn { name: _, fields }) => { + DeclT::UnionDefn(UnionDefn { + name: _, + fields, + abi_size: _, + }) => { let siblings = fields.clone(); for f in fields { self.elab_field(env, f, &siblings); diff --git a/src/pass/elim_cis.rs b/src/pass/elim_cis.rs index 8491fd93..b5f21db8 100644 --- a/src/pass/elim_cis.rs +++ b/src/pass/elim_cis.rs @@ -212,6 +212,7 @@ pub fn elim_simple_cis(_diags: &mut Diagnostics, tu: &mut TranslationUnit) { .with_loc(u.name.loc.clone()), fields: vec![info.named_field.clone()], eager_unfold_pred: false, + abi_size: u.abi_size, }); } } diff --git a/src/pass/emit.rs b/src/pass/emit.rs index e3b06972..e616ef3a 100644 --- a/src/pass/emit.rs +++ b/src/pass/emit.rs @@ -3670,11 +3670,15 @@ impl<'a> Emitter<'a> { // `full_array_lspec T N`, so `sizeof(T[N])` becomes // `c_sizeof (full_array_lspec T N)` and its length // participates in the size (see the `c_sizeof_array` axiom). - // Other types size opaquely. - unaryfn( - Doc::text("Pulse.Lib.C.Sizeof.c_sizeof"), - self.emit_type(env, ty), - ) + // A record whose ABI size clang reported sizes to that + // constant; every other type sizes opaquely. + match self.record_sizeof_constant(env, ty) { + Some(c) => c, + None => unaryfn( + Doc::text("Pulse.Lib.C.Sizeof.c_sizeof"), + self.emit_type(env, ty), + ), + } } ExprT::AlignOf(ty) => { let ty_doc = match &ty.val { @@ -5349,10 +5353,74 @@ impl<'a> Emitter<'a> { ) } + /// A constant pinning `c_sizeof` for a translated record type to the size + /// clang computed for it under the target ABI. + /// + /// This is emitted into the record's own generated module, so the size of + /// a given type is introduced exactly once, for that one type. Stating it + /// at each `sizeof` site instead would be unsound: nothing would stop two + /// sites from claiming different sizes for the same type. + /// + /// It is a refinement-typed constant rather than a lemma with an `SMTPat` + /// because the size of a specific type is a ground fact: a trigger for it + /// would contain no variable, which Z3 warns about and F* then rejects. + fn emit_abi_size_constant(&mut self, type_name: &Doc, abi_size: Option) -> Option { + let size = abi_size?; + let sizeof = parens( + Doc::text("Pulse.Lib.C.Sizeof.c_sizeof") + .append(Doc::line()) + .append(type_name.clone()) + .group(), + ); + Some( + Doc::text("assume") + .append(Doc::hardline()) + .append("val ") + .append(type_name.clone()) + .append("__c_sizeof") + .append(Doc::hardline()) + .append( + Doc::text(": (n: FStar.SizeT.t{") + .append(Doc::text("FStar.SizeT.v n == ")) + .append(Doc::text(size.to_string())) + .append(Doc::text(" /\\ n == ")) + .append(sizeof) + .append("})") + .nest(2), + ), + ) + } + + /// The name of the ABI-size constant for `ty`, when `ty` resolves to a + /// record whose size clang reported. + fn record_sizeof_constant(&mut self, env: &Env, ty: &Rc) -> Option { + let whnf = env.vtype_whnf(ty.clone().into()); + let k = match &whnf.val { + TypeT::TypeRef(TypeRefKind::Struct(n)) => { + env.lookup_struct(n).filter(|d| d.abi_size.is_some())?; + TypeRefKind::Struct(n.clone()) + } + TypeT::TypeRef(TypeRefKind::Union(n)) => { + env.lookup_union(n).filter(|d| d.abi_size.is_some())?; + TypeRefKind::Union(n.clone()) + } + _ => return None, + }; + Some( + self.emit_name(Name::TypeRef((&k).into())) + .append("__c_sizeof"), + ) + } + fn emit_structdefn( &mut self, env: &Env, - decl @ StructDefn { name, fields, .. }: &StructDefn, + decl @ StructDefn { + name, + fields, + abi_size, + .. + }: &StructDefn, ) -> Doc { let env = &mut env.clone(); env.push_struct(decl.clone()); @@ -5403,6 +5471,10 @@ impl<'a> Emitter<'a> { )); } + if let Some(c) = self.emit_abi_size_constant(&struct_type_name, *abi_size) { + ses.push(c); + } + // Generate struct spec type and pred by gathering slprops from fields let env = &mut env.clone(); let this = env @@ -6359,7 +6431,15 @@ impl<'a> Emitter<'a> { Doc::intersperse(ses.into_iter().map(|se| se.group()), Doc::hardline()) } - fn emit_uniondefn(&mut self, env: &Env, decl @ UnionDefn { name, fields }: &UnionDefn) -> Doc { + fn emit_uniondefn( + &mut self, + env: &Env, + decl @ UnionDefn { + name, + fields, + abi_size, + }: &UnionDefn, + ) -> Doc { let env = &mut env.clone(); env.push_union(decl.clone()); @@ -6405,6 +6485,10 @@ impl<'a> Emitter<'a> { )); } + if let Some(c) = self.emit_abi_size_constant(&union_type_name, *abi_size) { + ses.push(c); + } + // Emit predicate (emp for MVP) let env = &mut env.clone(); let this = env diff --git a/src/pass/prune.rs b/src/pass/prune.rs index b26950f3..d586b2bd 100644 --- a/src/pass/prune.rs +++ b/src/pass/prune.rs @@ -416,6 +416,7 @@ fn scan_translation_unit(deps: &mut Deps, tu: &TranslationUnit) { refines, fields, eager_unfold_pred: _, + abi_size: _, }) => { let ds = deps.deps_for(n); scan_type(ds, refines); @@ -426,7 +427,11 @@ fn scan_translation_unit(deps: &mut Deps, tu: &TranslationUnit) { DeclT::StructDecl(_) => { deps.deps_for(n); } - DeclT::UnionDefn(UnionDefn { name: _, fields }) => { + DeclT::UnionDefn(UnionDefn { + name: _, + fields, + abi_size: _, + }) => { let ds = deps.deps_for(n); for f in fields { scan_field(ds, f); diff --git a/test/sizeof_abi/Makefile b/test/sizeof_abi/Makefile new file mode 120000 index 00000000..3febeb16 --- /dev/null +++ b/test/sizeof_abi/Makefile @@ -0,0 +1 @@ +../_templates/Makefile \ No newline at end of file diff --git a/test/sizeof_abi/fstar.fst.config.json b/test/sizeof_abi/fstar.fst.config.json new file mode 120000 index 00000000..4100b019 --- /dev/null +++ b/test/sizeof_abi/fstar.fst.config.json @@ -0,0 +1 @@ +../_templates/fstar.fst.config.json \ No newline at end of file diff --git a/test/sizeof_abi/pal.config.json b/test/sizeof_abi/pal.config.json new file mode 120000 index 00000000..d59f1cfa --- /dev/null +++ b/test/sizeof_abi/pal.config.json @@ -0,0 +1 @@ +../_templates/pal.config.json \ No newline at end of file diff --git a/test/sizeof_abi/pal.h b/test/sizeof_abi/pal.h new file mode 120000 index 00000000..05ef83f9 --- /dev/null +++ b/test/sizeof_abi/pal.h @@ -0,0 +1 @@ +../pal.h \ No newline at end of file diff --git a/test/sizeof_abi/sizeof_abi.c b/test/sizeof_abi/sizeof_abi.c new file mode 100644 index 00000000..77746605 --- /dev/null +++ b/test/sizeof_abi/sizeof_abi.c @@ -0,0 +1,41 @@ +#include "pal.h" + +#include + +// +// Every `sizeof` of a record type resolves to the size clang computed for it +// under the target ABI, so arithmetic over record sizes has known bounds. +// + +typedef struct _PAIR +{ + uint32_t First; + uint32_t Second; +} PAIR; + +typedef union _EITHER +{ + uint32_t AsWord; + uint8_t AsBytes[4]; +} EITHER; + +typedef struct _OUTER +{ + PAIR Pair; + EITHER Either; + uint64_t Tag; +} OUTER; + +void +SizesAreKnown(void) +{ + _assert(sizeof(PAIR) == 8); + _assert(sizeof(EITHER) == 4); + _assert(sizeof(OUTER) == 24); + + // + // The point of pinning the sizes: a sum of them is statically in range, + // which an opaque size would leave unprovable. + // + _assert(sizeof(PAIR) + sizeof(EITHER) + sizeof(OUTER) == 36); +} From 6c3ec4ebbacb2656ced6b3218a1dc693f7ad04e9 Mon Sep 17 00:00:00 2001 From: Nikhil Swamy Date: Tue, 11 Aug 2026 17:31:17 -0700 Subject: [PATCH 2/4] Model the cell that holds a raw pointer `ref_to_core` erases the type of a pointer value. It does not say anything about the slot that holds one, which is what an untyped out-parameter hands its callee: the same machine word, viewed at a different type. Add `core_cell` for that view, with the shifts that move ownership across it. An out-parameter goes in empty and comes back full, so the two halves are not symmetric; and the slot a caller passes has almost always just been set to NULL rather than left uninitialized, so the empty half accepts either. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> Copilot-Session: 981f7d3c-6a91-47ad-84d7-7aadf747123d (cherry picked from commit 2640b372ec577fa4ac0dc182b14045c4badc2d03) --- pulse/Pulse.Lib.C.CoreRef.fsti | 72 ++++++++++++++++++++++++++++++++++ 1 file changed, 72 insertions(+) diff --git a/pulse/Pulse.Lib.C.CoreRef.fsti b/pulse/Pulse.Lib.C.CoreRef.fsti index a0c5fbb9..8ff889c8 100644 --- a/pulse/Pulse.Lib.C.CoreRef.fsti +++ b/pulse/Pulse.Lib.C.CoreRef.fsti @@ -35,6 +35,13 @@ val core_to_ref_to_core (#a: Type u#a) (r: ref a) : Lemma (core_to_ref a (ref_to_core r) == r) [SMTPat (ref_to_core r)] +(* And the other way round: a raw pointer viewed at a type and erased again is + the pointer it started as. Both directions together say that the two views + name the same machine address, which is exactly what the C cast means. *) +val ref_to_core_to_ref (a: Type u#a) (r: core_ref) + : Lemma (ref_to_core (core_to_ref a r) == r) + [SMTPat (core_to_ref a r)] + (* Nullness is preserved by the cast. *) val ref_to_core_is_null (#a: Type u#a) (r: ref a) : Lemma (core_is_null (ref_to_core r) == is_null r) @@ -53,3 +60,68 @@ instance has_zero_default_core_ref : has_zero_default core_ref = { instance inhabited_core_ref : inhabited core_ref = { witness = core_null } + +(* ---------------------------------------------------------------------- *) +(* Raw pointer cells. *) +(* *) +(* The C idiom `f((void const ** )&typedLocal)` hands a callee the caller's *) +(* own pointer slot at an erased type, so that the callee can write a *) +(* pointer into it without knowing what it points at. It is how every *) +(* "acquire a buffer" interface is spelled. *) +(* *) +(* This is not the `ref_to_core` coercion. That one erases the type of a *) +(* pointer value; this one changes the type at which a cell holding a *) +(* pointer is viewed. A cell holds one machine word either way, so the two *) +(* views denote the same location -- but they are different F* types, so *) +(* the ownership has to be moved between them explicitly, and the value in *) +(* the cell re-read through `ref_to_core`/`core_to_ref` at the same time. *) +(* Hence a view shift rather than a coercion. *) + +val core_cell (#a: Type u#a) (r: ref (ref a)) : ref core_ref + +(* The view shift is a bijection on locations, so distinct typed cells stay + distinct when viewed raw. Without this, two acquires into two different + locals would be indistinguishable to the prover. *) +val core_cell_injective (#a: Type u#a) (r1 r2: ref (ref a)) + : Lemma (requires core_cell r1 == core_cell r2) + (ensures r1 == r2) + +ghost fn to_core_cell (#a: Type0) (r: ref (ref a)) (#p: perm) (#v: ref a) + requires pts_to r #p v + ensures pts_to (core_cell r) #p (ref_to_core v) + +ghost fn of_core_cell (#a: Type0) (r: ref (ref a)) (#p: perm) (#w: core_ref) + requires pts_to (core_cell r) #p w + ensures pts_to r #p (core_to_ref a w) + +(* An out-parameter is handed uninitialized storage, which has no value to + re-read; the shift is then just a retyping of the slot. *) +ghost fn to_core_cell_uninit (#a: Type0) (r: ref (ref a)) + requires pts_to_uninit r + ensures pts_to_uninit (core_cell r) + +(* The same shift for the way C actually reaches an empty slot. A local passed + to an out-parameter is nearly always initialized to NULL first, so what the + caller holds is a value it is about to lose rather than nothing at all. + Taking `pts_to_uninit` here would force every such call site to forget the + value by hand, and taking `pts_to` would exclude the genuinely uninitialized + local, so this takes `initialized_or_not` and covers both. *) +val initialized_or_not (#a: Type0) (r: ref a) : slprop + +[@@pulse_intro] +ghost fn intro_initialized_or_not (#a: Type0) (r: ref a) (#v: a) + requires pts_to r v + ensures initialized_or_not r + +[@@pulse_intro] +ghost fn intro_initialized_or_not_uninit (#a: Type0) (r: ref a) + requires pts_to_uninit r + ensures initialized_or_not r + +ghost fn to_core_cell_out (#a: Type0) (r: ref (ref a)) + requires initialized_or_not r + ensures pts_to_uninit (core_cell r) + +ghost fn of_core_cell_uninit (#a: Type0) (r: ref (ref a)) + requires pts_to_uninit (core_cell r) + ensures pts_to_uninit r From 3d10b6de54232d7f362fc35c23b3735cefbb4c5f Mon Sep 17 00:00:00 2001 From: Nikhil Swamy Date: Tue, 11 Aug 2026 17:31:17 -0700 Subject: [PATCH 3/4] Pass a caller's pointer slot through an untyped out-parameter `f((void const ** )&typedLocal)` is how every acquire-a-buffer interface is spelled. Until now the cast was dropped and a `ref (ref T)` reached a `ref core_ref` parameter, which is ill-typed. Emit the cell view instead, and walk the ownership across it around the call in the same way nullable arguments are already handled. Casts have to be stripped before the argument's type is inferred, or inference reports the type the cast asks for and the shift is never emitted. What the acquired buffer means is still the contract's business: only the callee's `_ensures`, written in terms of `core_to_ref`, licenses reading it at a type. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> Copilot-Session: 981f7d3c-6a91-47ad-84d7-7aadf747123d (cherry picked from commit d677cee391ce92750fb358ea7c43552051ece8ca) --- src/pass/emit.rs | 119 +++++++++++++++++++ test/core_ref_out_cell/Makefile | 1 + test/core_ref_out_cell/core_ref_out_cell.c | 49 ++++++++ test/core_ref_out_cell/fstar.fst.config.json | 1 + test/core_ref_out_cell/pal.config.json | 1 + test/core_ref_out_cell/pal.h | 1 + 6 files changed, 172 insertions(+) create mode 120000 test/core_ref_out_cell/Makefile create mode 100644 test/core_ref_out_cell/core_ref_out_cell.c create mode 120000 test/core_ref_out_cell/fstar.fst.config.json create mode 120000 test/core_ref_out_cell/pal.config.json create mode 120000 test/core_ref_out_cell/pal.h diff --git a/src/pass/emit.rs b/src/pass/emit.rs index e616ef3a..16df66d0 100644 --- a/src/pass/emit.rs +++ b/src/pass/emit.rs @@ -2971,6 +2971,29 @@ impl<'a> Emitter<'a> { self.emit_type(env, to_pointee), val_doc, ])), + // A *cell* holding a typed pointer, viewed as a cell + // holding a raw one: `(void const **)&typedLocal`, which + // is how a caller hands a callee its own pointer slot to + // write into. Unlike `ref_to_core` this does not erase a + // pointer's type, it retypes the slot that holds it, so + // the ownership is moved across by the ghost shift that + // `core_cell_arg_ghosts` emits around the call. Must be + // matched before the plain `ref T -> core_ref` rule + // below, which would otherwise erase the outer pointer + // and quietly hand the callee an unwritable address. + ( + TypeT::Pointer(from_pointee, PointerKind::Ref | PointerKind::Unknown), + TypeT::Pointer(to_pointee, PointerKind::Ref | PointerKind::Unknown), + ) if matches!( + env.vtype_whnf(from_pointee.clone().into()).val, + TypeT::Pointer(_, PointerKind::Ref | PointerKind::Unknown) + ) && matches!( + env.vtype_whnf(to_pointee.clone().into()).val, + TypeT::Pointer(_, PointerKind::Core) + ) => + { + unaryfn(Doc::text("Pulse.Lib.C.CoreRef.core_cell"), val_doc) + } // typed `ref T` → `core_ref`: erase the pointee type. ( TypeT::Pointer(_, PointerKind::Ref | PointerKind::Unknown), @@ -3746,6 +3769,101 @@ impl<'a> Emitter<'a> { } } + + /// Move a caller's pointer slot across the typed/raw view for the duration + /// of a call. + /// + /// `f((void const ** )&typedLocal)` hands the callee the caller's own slot + /// at an erased type so it can write a pointer into it without knowing the + /// pointee. `core_cell` retypes the slot as a term, but the ownership does + /// not follow on its own: `pts_to (core_cell r)` and `pts_to r` are + /// different slprops over what is nonetheless one location, so the prover + /// has to be walked across and back. Emit `to_core_cell` before the call + /// and `of_core_cell` after, which leaves the caller holding its slot at + /// the type it declared it with, now containing whatever the callee wrote. + /// + /// An `_out` parameter takes the uninitialized pair, since a slot the + /// callee is about to fill has no value to carry across. + fn core_cell_arg_ghosts( + &mut self, + env: &Env, + args: &[Rc], + fn_decl: &FnDecl, + out: &mut NullableGhosts, + ) { + for (i, arg) in args.iter().enumerate() { + let Some(param) = fn_decl.args.get(i) else { + continue; + }; + let TypeT::Pointer(param_pointee, PointerKind::Ref | PointerKind::Unknown) = + &env.vtype_whnf(param.ty.clone().into()).val + else { + continue; + }; + if !matches!( + env.vtype_whnf(param_pointee.clone().into()).val, + TypeT::Pointer(_, PointerKind::Core) + ) { + continue; + } + // Only the cell view needs the shift. An argument that is already a + // raw cell, or that is not a pointer to a typed pointer, is passed + // as it stands. + let inner = Self::strip_pointer_casts(arg); + let Ok(arg_ty) = env.infer_expr(inner) else { + continue; + }; + let TypeT::Pointer(arg_pointee, PointerKind::Ref | PointerKind::Unknown) = + &env.vtype_whnf(arg_ty.clone().into()).val + else { + continue; + }; + if !matches!( + env.vtype_whnf(arg_pointee.clone().into()).val, + TypeT::Pointer(_, PointerKind::Ref | PointerKind::Unknown) + ) { + continue; + } + let arg_doc = parens(self.emit_rvalue(env, inner)); + // An out-parameter is uninitialized going in and written by the + // time it comes back, so the two halves of the shift are not + // symmetric: hand over an empty slot, take back a full one. C + // locals passed this way are usually initialized to NULL first, so + // the empty slot is reached by forgetting that value rather than by + // never having had one; `to_core_cell_out` takes either. + let (to_shift, of_shift) = match param.mode { + ParamMode::Out => ( + "Pulse.Lib.C.CoreRef.to_core_cell_out ", + "Pulse.Lib.C.CoreRef.of_core_cell ", + ), + _ => ( + "Pulse.Lib.C.CoreRef.to_core_cell ", + "Pulse.Lib.C.CoreRef.of_core_cell ", + ), + }; + out.before.push( + Doc::text(to_shift.to_string()) + .append(arg_doc.clone()) + .append(Doc::text(";")), + ); + out.after.push( + Doc::text(of_shift.to_string()) + .append(arg_doc) + .append(Doc::text(";")), + ); + } + } + + /// The argument as written, with the pointer casts that got it to the + /// callee's type peeled off, so the shift names the caller's own slot. + fn strip_pointer_casts(e: &Rc) -> &Rc { + let mut cur = e; + while let ExprT::Cast(inner, _) = &cur.val { + cur = inner; + } + cur + } + fn nullable_arg_ghosts_expr(&mut self, env: &Env, e: &Expr, out: &mut NullableGhosts) { match &e.val { ExprT::UnOp(_, a) | ExprT::Cast(a, _) | ExprT::Deref(a) | ExprT::Ref(a) => { @@ -3762,6 +3880,7 @@ impl<'a> Emitter<'a> { let Some(fn_decl) = env.lookup_fn(f) else { return; }; + self.core_cell_arg_ghosts(env, args, &fn_decl, out); for (i, arg) in args.iter().enumerate() { let Some(param) = fn_decl.args.get(i) else { continue; diff --git a/test/core_ref_out_cell/Makefile b/test/core_ref_out_cell/Makefile new file mode 120000 index 00000000..3febeb16 --- /dev/null +++ b/test/core_ref_out_cell/Makefile @@ -0,0 +1 @@ +../_templates/Makefile \ No newline at end of file diff --git a/test/core_ref_out_cell/core_ref_out_cell.c b/test/core_ref_out_cell/core_ref_out_cell.c new file mode 100644 index 00000000..bfcb54a0 --- /dev/null +++ b/test/core_ref_out_cell/core_ref_out_cell.c @@ -0,0 +1,49 @@ +// Test: a callee writes a pointer into the caller's own slot through an +// untyped out-parameter -- the `f((void const ** )&typedLocal)` idiom that +// every "acquire a buffer" interface is spelled with. +// +// This exercises the *cell* view shift, not the pointer coercion. `_core_ref` +// on the pointee of the out-parameter makes the slot a `ref core_ref`, while +// the caller's local is a `ref (ref hdr)`. Those are the same location holding +// the same machine word, but different F* types, so PAL emits +// `core_cell` on the argument and walks the ownership across with +// `to_core_cell_out` before the call and `of_core_cell` after -- an +// out-parameter goes in empty and comes back full, so the two halves differ. +// +// What the acquired buffer *means* is not something PAL can invent: the callee +// returns an address and only its contract says what may be read there. That +// is written by hand as an `_ensures` in terms of `core_to_ref`, which is the +// slprop that licenses the cast. Without it the dereference below is rejected. + +#include "pal.h" +#include + +struct hdr { + int a; + int b; +}; + +typedef _core_ref void const* PAL_RAW_CPTR; + +/* Hands back a buffer at an erased type. The `_ensures` is the licence to read + * it as a `struct hdr`; nothing in the C types says so. */ +int acquire(unsigned n, _out PAL_RAW_CPTR* buf) + _ensures(_inline_pulse( + exists* (hv: $type(struct hdr)). + pts_to (Pulse.Lib.C.CoreRef.core_to_ref $type(struct hdr) ($(*buf))) hv)); + +/* Releases it again, taking the licence back, so nothing is left over. It + * takes the typed pointer the caller recovered: by this point the cast has + * been licensed and there is nothing left to erase. */ +void release(_consumes struct hdr const* h); + +int use(void) +{ + struct hdr const* h = NULL; + struct hdr out; + + int s = acquire(sizeof(struct hdr), (void const**)&h); + out = *h; // read through the pointer the callee wrote + release(h); + return out.a; +} diff --git a/test/core_ref_out_cell/fstar.fst.config.json b/test/core_ref_out_cell/fstar.fst.config.json new file mode 120000 index 00000000..4100b019 --- /dev/null +++ b/test/core_ref_out_cell/fstar.fst.config.json @@ -0,0 +1 @@ +../_templates/fstar.fst.config.json \ No newline at end of file diff --git a/test/core_ref_out_cell/pal.config.json b/test/core_ref_out_cell/pal.config.json new file mode 120000 index 00000000..d59f1cfa --- /dev/null +++ b/test/core_ref_out_cell/pal.config.json @@ -0,0 +1 @@ +../_templates/pal.config.json \ No newline at end of file diff --git a/test/core_ref_out_cell/pal.h b/test/core_ref_out_cell/pal.h new file mode 120000 index 00000000..05ef83f9 --- /dev/null +++ b/test/core_ref_out_cell/pal.h @@ -0,0 +1 @@ +../pal.h \ No newline at end of file From 1070a85eebc49ae92557da242a113e8b0a816c65 Mon Sep 17 00:00:00 2001 From: Nikhil Swamy Date: Tue, 11 Aug 2026 17:39:35 -0700 Subject: [PATCH 4/4] Name both directions of the raw pointer cast A caller that recovers a typed pointer from a slot the callee wrote often has to name the raw address again -- to say which loan it is holding, say. Only one direction of the round trip was stated, so that step could not be taken. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> Copilot-Session: 981f7d3c-6a91-47ad-84d7-7aadf747123d (cherry picked from commit 068411aa67ae1acc95626c4d22ec8469e775e6da) --- pulse/Pulse.Lib.C.CoreRef.fsti | 9 ++++++--- src/pass/emit.rs | 1 - 2 files changed, 6 insertions(+), 4 deletions(-) diff --git a/pulse/Pulse.Lib.C.CoreRef.fsti b/pulse/Pulse.Lib.C.CoreRef.fsti index 8ff889c8..eaee2197 100644 --- a/pulse/Pulse.Lib.C.CoreRef.fsti +++ b/pulse/Pulse.Lib.C.CoreRef.fsti @@ -35,9 +35,12 @@ val core_to_ref_to_core (#a: Type u#a) (r: ref a) : Lemma (core_to_ref a (ref_to_core r) == r) [SMTPat (ref_to_core r)] -(* And the other way round: a raw pointer viewed at a type and erased again is - the pointer it started as. Both directions together say that the two views - name the same machine address, which is exactly what the C cast means. *) +(* And the other way round: an address viewed at a type and erased again is the + address it started as. The two lemmas together say that the two views name + the same machine word, which is exactly what the C cast means -- and the + second direction is what a caller needs after it has recovered a typed + pointer from a slot and has to name the raw address again to talk about the + loan the callee gave it. *) val ref_to_core_to_ref (a: Type u#a) (r: core_ref) : Lemma (ref_to_core (core_to_ref a r) == r) [SMTPat (core_to_ref a r)] diff --git a/src/pass/emit.rs b/src/pass/emit.rs index 16df66d0..f3f91ff9 100644 --- a/src/pass/emit.rs +++ b/src/pass/emit.rs @@ -3769,7 +3769,6 @@ impl<'a> Emitter<'a> { } } - /// Move a caller's pointer slot across the typed/raw view for the duration /// of a call. ///