Give each record type the size its ABI assigns it

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

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

src/pass/emit.rs

@@ -3591,11 +3591,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 {
@@ -4771,10 +4775,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<u64>) -> Option<Doc> {
+        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<Type>) -> Option<Doc> {
+        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());
@@ -4825,6 +4893,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
@@ -5780,7 +5852,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());
 
@@ -5826,6 +5906,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

src/pass/prune.rs

@@ -416,6 +416,7 @@ fn scan_translation_unit(deps: &mut Deps<DeclName>, 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<DeclName>, 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);

test/sizeof_abi/Makefile

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

test/sizeof_abi/fstar.fst.config.json

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

test/sizeof_abi/pal.config.json

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

test/sizeof_abi/pal.h

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

test/sizeof_abi/sizeof_abi.c

@@ -0,0 +1,41 @@
+#include "pal.h"
+
+#include <stdint.h>
+
+//
+// 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);
+}