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/pulse/Pulse.Lib.C.CoreRef.fsti b/pulse/Pulse.Lib.C.CoreRef.fsti index a0c5fbb9..eaee2197 100644 --- a/pulse/Pulse.Lib.C.CoreRef.fsti +++ b/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 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..f3f91ff9 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), @@ -3670,11 +3693,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 { @@ -3742,6 +3769,100 @@ 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) => { @@ -3758,6 +3879,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; @@ -5349,10 +5471,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 +5589,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 +6549,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 +6603,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/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 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); +}