Pass a caller's pointer slot through an untyped out-parameter

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<Expr>);
     }
 

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())));

pulse/Pulse.Lib.C.CoreRef.fsti

@@ -35,6 +35,16 @@ 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: 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)]
+
 (* 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 +63,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

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<Rc<Expr>>,
     eager_unfold_pred: bool,
+    abi_size: Option<u64>,
 }
 
 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<Expr>) {
         self.decreases = Some(p);
     }

src/env.rs

@@ -174,6 +174,7 @@ impl Env {
                             .with_loc(name.loc.clone()),
                         fields: vec![],
                         eager_unfold_pred: false,
+                        abi_size: None,
                     });
                 }
             }

src/ir/mod.rs

@@ -459,6 +459,9 @@ pub struct StructDefn {
     pub refines: Rc<Type>,
     pub fields: Vec<Field>,
     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<u64>,
 }
 
 impl StructDefn {
@@ -483,6 +486,8 @@ impl StructDefn {
 pub struct UnionDefn {
     pub name: Rc<Ident>,
     pub fields: Vec<Field>,
+    /// See `StructDefn::abi_size`.
+    pub abi_size: Option<u64>,
 }
 
 impl UnionDefn {

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);
                 }

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);

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,
                 });
             }
         }