diff --git a/cpp/iface.zng b/cpp/iface.zng index 6bc75c1b..26ee737b 100644 --- a/cpp/iface.zng +++ b/cpp/iface.zng @@ -202,6 +202,7 @@ mod crate::clang { fn arg(&mut self, Rc, Rc, ParamMode); fn arg_anon(&mut self, Rc, ParamMode); fn field(&mut self, Rc, Rc); + fn field_bitfield(&mut self, Rc, Rc, u32); fn ghost_arg(&mut self, Rc, Rc); fn requires(&mut self, Rc); fn ensures(&mut self, Rc); diff --git a/cpp/impl.cpp b/cpp/impl.cpp index 908af68d..fc6a1f80 100644 --- a/cpp/impl.cpp +++ b/cpp/impl.cpp @@ -224,6 +224,54 @@ class PALConsumer : public ASTConsumer { ctx.report_diag(loc.clone(), true, toStr(std::string(msg) + extra)); } + // Translate a single struct/union field into the IR, pushing it onto the + // given builder. Handles plain fields and unsigned bit-fields; rejects + // signed bit-fields and skips anonymous/zero-width padding bit-fields. + void addRecordField(DeclBuilder &builder, FieldDecl *f, + AnonNameGen *liftStructs, bool inUnion) { + auto floc = getRange(f->getSourceRange()); + if (f->isBitField()) { + // Anonymous / zero-width bit-fields are pure padding with no accessible + // value; drop them entirely. + if (f->isUnnamedBitField()) + return; + // Bit-fields are only modeled inside structs; union bit-fields would need + // the same value-based encoding layered on the union variant model. + if (inUnion) { + reportUnsupported(f->getSourceRange(), floc, + "unsupported bit-field in union", ""); + return; + } + // Only unsigned (and _Bool) bit-fields are modeled. Signed bit-fields + // would need sign-extension on read and have implementation-defined + // out-of-range write semantics (C11 6.3.1.3p3), so reject them. + if (!f->getType()->isUnsignedIntegerType()) { + reportUnsupported( + f->getSourceRange(), floc, + "unsupported signed bit-field (only unsigned bit-fields are " + "supported)", + ""); + return; + } + unsigned width = f->getBitWidthValue(); + builder.field_bitfield( + ctx.mk_ident(toStr(fieldNameStr(f)), std::move(floc)), + trQualType(f->getType(), f->getSourceRange(), liftStructs), width); + return; + } + auto qt = f->getType(); + auto *qtPtr = qt.IgnoreParens().getTypePtr(); + if (isa(qtPtr) || isa(qtPtr)) { + reportUnsupported(f->getSourceRange(), floc, + "unsupported non-constant-length array field", ""); + } else { + builder.field(ctx.mk_ident(toStr(fieldNameStr(f)), std::move(floc)), + trTypeAttrs(f->getAttrs(), + trQualType(f->getType(), f->getSourceRange(), + liftStructs))); + } + } + void trRecordDecl(Rc ident, RecordDecl *decl, AnonNameGen *liftStructs) { auto key = recordKey(decl); @@ -263,19 +311,7 @@ class PALConsumer : public ASTConsumer { } } for (auto f : decl->fields()) { - auto floc = getRange(f->getSourceRange()); - auto qt = f->getType(); - auto *qtPtr = qt.IgnoreParens().getTypePtr(); - if (isa(qtPtr) || isa(qtPtr)) { - reportUnsupported(f->getSourceRange(), floc, - "unsupported non-constant-length array field", ""); - } else { - builder.field( - ctx.mk_ident(toStr(fieldNameStr(f)), std::move(floc)), - trTypeAttrs( - f->getAttrs(), - trQualType(f->getType(), f->getSourceRange(), liftStructs))); - } + addRecordField(builder, f, liftStructs, /*inUnion=*/false); } ctx.add_struct(std::move(builder)); } else if (decl->getTagKind() == TagTypeKind::Union) { @@ -292,19 +328,7 @@ class PALConsumer : public ASTConsumer { } } for (auto f : decl->fields()) { - auto floc = getRange(f->getSourceRange()); - auto qt = f->getType(); - auto *qtPtr = qt.IgnoreParens().getTypePtr(); - if (isa(qtPtr) || isa(qtPtr)) { - reportUnsupported(f->getSourceRange(), floc, - "unsupported non-constant-length array field", ""); - } else { - builder.field( - ctx.mk_ident(toStr(fieldNameStr(f)), std::move(floc)), - trTypeAttrs( - f->getAttrs(), - trQualType(f->getType(), f->getSourceRange(), liftStructs))); - } + addRecordField(builder, f, liftStructs, /*inUnion=*/true); } ctx.add_union(std::move(builder)); } else { diff --git a/doc/internals.md b/doc/internals.md index 711e8b86..33c55197 100644 --- a/doc/internals.md +++ b/doc/internals.md @@ -179,6 +179,15 @@ A `TranslationUnit` is the top-level container: a list of `main_file_names` (the input `.c` files) and a flat list of `Decl` nodes. +**Bit-fields.** An unsigned struct bit-field (`unsigned int a : N;`) is +modeled by `FieldT::BitField { name, ty, width }`. It is encoded like an +ordinary scalar field but its backing cell is range-refined to the width, +`(v:UIntW.t{UIntW.v v < pow2 N})`, and a write `s->a = e` stores +`Pulse.Lib.C.BitField.mask_uW N e` (C unsigned modular truncation), so the +stored value always satisfies the refinement. Reads need no conversion. +Anonymous and zero-width padding bit-fields are dropped; signed bit-fields +and union bit-fields are rejected with a diagnostic. + --- ## 3. Zngur FFI @@ -281,6 +290,7 @@ hand-written library code that ships with PAL. | `Pulse.Lib.C.UnaryOps` | negation, bitwise not | | `Pulse.Lib.C.Sizeof` | compile-time `sizeof` | | `Pulse.Lib.C.Inhabited` | inhabitedness proofs (needed for memory allocation) | +| `Pulse.Lib.C.BitField` | `mask_uW` truncation helpers for unsigned bit-field writes | | `Pulse.Lib.C.Assumptions` | axioms bridging C semantics and F* | The top-level module `Pulse.Lib.C` re-exports the core subset: diff --git a/pulse/Pulse.Lib.C.BitField.fst b/pulse/Pulse.Lib.C.BitField.fst new file mode 100644 index 00000000..ae9141d1 --- /dev/null +++ b/pulse/Pulse.Lib.C.BitField.fst @@ -0,0 +1,41 @@ +module Pulse.Lib.C.BitField + +/// Truncation (masking) helpers for unsigned C bit-fields. +/// +/// Assigning a value `v` to an `n`-bit unsigned bit-field stores the low `n` +/// bits of `v`, i.e. `v % pow2 n` (C unsigned modular truncation). PAL backs +/// each bit-field by a range-refined machine cell `(x:UW.t{UW.v x < pow2 n})`, +/// so the masked result must carry that bound as a refinement. +/// +/// Each `mask_uW` truncates by modular arithmetic (`rem` by `pow2 n`), mirroring +/// how `add_wrap`/`sub_wrap`/`mul_wrap` model unsigned overflow via the modular +/// primitives. The `< pow2 n` bound then holds by "mod by a positive", needing +/// no bitwise reasoning; the exact value `UW.v r == UW.v v % pow2 n` comes +/// straight from the `rem` postcondition. The `n = W` case (field as wide as its +/// storage) is the identity, since the value already fits. + +module U8 = FStar.UInt8 +module U16 = FStar.UInt16 +module U32 = FStar.UInt32 +module U64 = FStar.UInt64 +module Math = FStar.Math.Lemmas + +let mask_u8 (n: nat { 0 < n /\ n <= 8 }) (v: U8.t) + : (r:U8.t { U8.v r < pow2 n /\ U8.v r == U8.v v % pow2 n }) = + if n = 8 then (Math.small_mod (U8.v v) (pow2 8); v) + else (Math.pow2_lt_compat 8 n; U8.rem v (U8.uint_to_t (pow2 n))) + +let mask_u16 (n: nat { 0 < n /\ n <= 16 }) (v: U16.t) + : (r:U16.t { U16.v r < pow2 n /\ U16.v r == U16.v v % pow2 n }) = + if n = 16 then (Math.small_mod (U16.v v) (pow2 16); v) + else (Math.pow2_lt_compat 16 n; U16.rem v (U16.uint_to_t (pow2 n))) + +let mask_u32 (n: nat { 0 < n /\ n <= 32 }) (v: U32.t) + : (r:U32.t { U32.v r < pow2 n /\ U32.v r == U32.v v % pow2 n }) = + if n = 32 then (Math.small_mod (U32.v v) (pow2 32); v) + else (Math.pow2_lt_compat 32 n; U32.rem v (U32.uint_to_t (pow2 n))) + +let mask_u64 (n: nat { 0 < n /\ n <= 64 }) (v: U64.t) + : (r:U64.t { U64.v r < pow2 n /\ U64.v r == U64.v v % pow2 n }) = + if n = 64 then (Math.small_mod (U64.v v) (pow2 64); v) + else (Math.pow2_lt_compat 64 n; U64.rem v (U64.uint_to_t (pow2 n))) diff --git a/src/clang.rs b/src/clang.rs index 687d1dc4..b1a8bd21 100644 --- a/src/clang.rs +++ b/src/clang.rs @@ -480,6 +480,18 @@ impl DeclBuilder { }) } + fn field_bitfield(&mut self, name: Rc, ty: Rc, width: u32) { + let loc = name.loc.clone(); + self.fields.push(Ast { + loc, + val: FieldT::BitField { + name: (*name).clone(), + ty, + width, + }, + }) + } + fn requires(&mut self, p: Rc) { self.requires.push(p) } diff --git a/src/ir/mod.rs b/src/ir/mod.rs index b410a05d..3cbeb850 100644 --- a/src/ir/mod.rs +++ b/src/ir/mod.rs @@ -424,18 +424,39 @@ pub enum FieldT { /// A regular field: `T name;` /// For fixed-size C array fields (`T name[length]`), the type is `FixedArray(T, length)`. Plain { name: Ident, ty: Rc }, + /// An unsigned bit-field: `T name : width;`. `ty` is the declared underlying + /// integer type (e.g. `unsigned int`); `width` is the number of bits. The + /// value is stored directly in the struct record as a range-refined machine + /// value `(v:UIntW.t{UIntW.v v < pow2 width})` and is not separately + /// addressable (no extra `ref`/`pts_to` beyond the usual scalar cell). + BitField { + name: Ident, + ty: Rc, + width: u32, + }, } impl FieldT { pub fn name(&self) -> &Ident { match self { FieldT::Plain { name, .. } => name, + FieldT::BitField { name, .. } => name, } } pub fn is_array(&self) -> bool { match self { FieldT::Plain { ty, .. } => matches!(ty.val, TypeT::FixedArray(_, _)), + FieldT::BitField { .. } => false, + } + } + + /// For a bit-field, the number of bits in its declared width; `None` for a + /// plain field. Doubles as a "this is a bit-field" predicate. + pub fn bit_width(&self) -> Option { + match self { + FieldT::BitField { width, .. } => Some(*width), + FieldT::Plain { .. } => None, } } @@ -446,13 +467,17 @@ impl FieldT { TypeT::FixedArray(elem_ty, length) => Some((elem_ty, *length)), _ => None, }, + FieldT::BitField { .. } => None, } } - /// Returns the "logical" type of the field. + /// Returns the "logical" type of the field. For a bit-field this is the + /// declared underlying integer type (e.g. `unsigned int`), which is what a + /// member access evaluates to before integer promotion. pub fn logical_type(&self, _loc: &Rc) -> Rc { match self { FieldT::Plain { ty, .. } => ty.clone(), + FieldT::BitField { ty, .. } => ty.clone(), } } } diff --git a/src/ir/pretty.rs b/src/ir/pretty.rs index b3458f24..b61e44b6 100644 --- a/src/ir/pretty.rs +++ b/src/ir/pretty.rs @@ -561,6 +561,14 @@ impl PrettyIR for FieldT { .group() .nest(2) .append(RcDoc::hardline()), + FieldT::BitField { name, ty, width } => ty + .to_doc() + .append(RcDoc::line()) + .append(name.to_doc()) + .append(format!(" : {width};")) + .group() + .nest(2) + .append(RcDoc::hardline()), } } } diff --git a/src/pass/check.rs b/src/pass/check.rs index fbb915a2..2887d58a 100644 --- a/src/pass/check.rs +++ b/src/pass/check.rs @@ -72,6 +72,7 @@ impl<'a> Checker<'a> { fn check_field(&mut self, env: &Env, field: &Field) { match &field.val { FieldT::Plain { name: _, ty } => self.check_type(env, ty), + FieldT::BitField { name: _, ty, .. } => self.check_type(env, ty), } } diff --git a/src/pass/elab.rs b/src/pass/elab.rs index 4df5a654..44b7d52d 100644 --- a/src/pass/elab.rs +++ b/src/pass/elab.rs @@ -86,6 +86,7 @@ impl<'a> Elaborator<'a> { fn elab_field(&mut self, env: &Env, field: &mut Field) { match &mut field.val { FieldT::Plain { name: _, ty } => self.elab_type(env, Rc::make_mut(ty)), + FieldT::BitField { name: _, ty, .. } => self.elab_type(env, Rc::make_mut(ty)), } } diff --git a/src/pass/emit.rs b/src/pass/emit.rs index d5f67812..93e00a21 100644 --- a/src/pass/emit.rs +++ b/src/pass/emit.rs @@ -721,14 +721,79 @@ impl<'a> Emitter<'a> { fn emit_field_default(&mut self, env: &Env, field: &Field) -> Doc { match &field.val { FieldT::Plain { ty, .. } => self.emit_type_default(env, ty), + // A bit-field's record cell has the refined machine type, so its + // default must be a concrete machine zero (e.g. `UInt16.uint_to_t 0`, + // `0` for width `N >= 1`) that visibly satisfies the `< pow2 N` + // refinement — not the generic `zero_default`, which has no instance + // for the refined type. Resolve typedefs to reach the machine int. + FieldT::BitField { ty, .. } => { + self.emit_type_default(env, &env.vtype_whnf(ty.clone().into())) + } } } + /// Emit the range-refined machine type backing an unsigned bit-field of the + /// given declared underlying integer type and bit-width: + /// `(v:UIntW.t{UIntW.v v < pow2 N})`. The declared type may be a typedef + /// (e.g. `uint16_t`), so it is resolved to weak-head normal form to find the + /// underlying machine width for the `UIntW.v` projection in the refinement. + fn emit_bitfield_value_type(&mut self, env: &Env, ty: &Type, width: u32) -> Doc { + let base = self.emit_type(env, ty); + let modu = match &env.vtype_whnf(ty.clone().into()).val { + TypeT::Int { + signed: false, + width: w, + } => get_int_mod(&false, w), + _ => None, + }; + match modu { + Some(m) => parens( + Doc::text("v:") + .append(Doc::line()) + .append(base) + .append(Doc::line()) + .append(Doc::text(format!("{{{}.v v < pow2 {}}}", m, width))), + ), + // Should not happen for a well-formed unsigned bit-field; fall back + // to the unrefined machine type. + None => base, + } + } + + /// If `lhs` is a struct member access (`s->f` / `s.f`) whose field is an + /// unsigned bit-field, return its bit-width and the fully-qualified masking + /// helper (`Pulse.Lib.C.BitField.mask_uW`) for its underlying machine width. + /// A write to a bit-field stores `mask_uW width rhs` so the masked value + /// satisfies the cell's `< pow2 width` refinement (C unsigned truncation). + fn bitfield_member_mask(&self, env: &Env, lhs: &Expr) -> Option<(u32, &'static str)> { + let ExprT::Member(base, fld) = &lhs.val else { + return None; + }; + let base_ty = env.vtype_whnf(env.infer_expr(base).ok()?); + let struct_name = match &base_ty.val { + TypeT::TypeRef(TypeRefKind::Struct(s)) => s.clone(), + _ => return None, + }; + let sdef = env.lookup_struct(&struct_name)?; + let field = sdef.fields.iter().find(|f| f.val.name().val == fld.val)?; + let width = field.val.bit_width()?; + let underlying = env.vtype_whnf(field.val.logical_type(&field.loc).into()); + let mask_fn = match &underlying.val { + TypeT::Int { + signed: false, + width: mw, + } => get_bitfield_mask_fn(mw)?, + _ => return None, + }; + Some((width, mask_fn)) + } + /// Render the F* type appearing in a struct/union's noeq record for /// `field`. For `Plain` fields this is the stored type fn emit_field_record_type(&mut self, env: &Env, field: &Field) -> Doc { match &field.val { FieldT::Plain { name: _, ty } => self.emit_type(env, ty), + FieldT::BitField { ty, width, .. } => self.emit_bitfield_value_type(env, ty, *width), } } @@ -758,6 +823,10 @@ impl<'a> Emitter<'a> { } else { match &field.val { FieldT::Plain { name: _, ty } => unaryfn(Doc::text("ref"), self.emit_type(env, ty)), + FieldT::BitField { ty, width, .. } => unaryfn( + Doc::text("ref"), + self.emit_bitfield_value_type(env, ty, *width), + ), } } } @@ -1601,6 +1670,19 @@ fn get_uint_wrap_mod(width: &u32) -> Option<&'static str> { }) } +/// Fully-qualified bit-field truncation (masking) helper for each unsigned +/// machine width. `mask_uW n v` returns the low `n` bits of `v` as a value +/// provably `< pow2 n` (C unsigned modular truncation on a bit-field write). +fn get_bitfield_mask_fn(machine_width: &u32) -> Option<&'static str> { + Some(match machine_width { + 8 => "Pulse.Lib.C.BitField.mask_u8", + 16 => "Pulse.Lib.C.BitField.mask_u16", + 32 => "Pulse.Lib.C.BitField.mask_u32", + 64 => "Pulse.Lib.C.BitField.mask_u64", + _ => return None, + }) +} + fn get_float_mod(width: &u32) -> Option<&'static str> { Some(match width { 32 => "Pulse.Lib.C.float32", @@ -3232,13 +3314,24 @@ impl<'a> Emitter<'a> { .nest(2); } } - // Fall through to normal assignment for struct members + // Fall through to normal assignment for struct members. + // For an unsigned bit-field, mask the RHS to its width so + // the stored value satisfies the cell's `< pow2 N` + // refinement (C unsigned modular truncation on write). + let rhs = match self.bitfield_member_mask(env, x) { + Some((width, mask_fn)) => naryfn([ + Doc::text(mask_fn), + Doc::text(width.to_string()), + self.emit_rvalue(env, t), + ]), + None => self.emit_rvalue(env, t), + }; self.emit_lvalue(env, x) .append(Doc::line()) .append(":=") .group() .append(Doc::line()) - .append(self.emit_rvalue(env, t)) + .append(rhs) .append(";") .group() .nest(2) diff --git a/src/pass/prune.rs b/src/pass/prune.rs index f5549ae8..a2615492 100644 --- a/src/pass/prune.rs +++ b/src/pass/prune.rs @@ -71,6 +71,7 @@ fn in_main_file(main_files: &[Rc], loc: &SourceInfo) -> bool { fn scan_field(deps: &mut HashSet, field: &Field) { match &field.val { FieldT::Plain { name: _, ty } => scan_type(deps, ty), + FieldT::BitField { name: _, ty, .. } => scan_type(deps, ty), } } diff --git a/test/bitfields/Makefile b/test/bitfields/Makefile new file mode 120000 index 00000000..3febeb16 --- /dev/null +++ b/test/bitfields/Makefile @@ -0,0 +1 @@ +../_templates/Makefile \ No newline at end of file diff --git a/test/bitfields/bitfields.c b/test/bitfields/bitfields.c new file mode 100644 index 00000000..75a552be --- /dev/null +++ b/test/bitfields/bitfields.c @@ -0,0 +1,106 @@ +#include "pal.h" +#include + +struct flags { + unsigned int a : 3; // value in [0, 8) + unsigned int b : 5; // value in [0, 32) + unsigned int full; // ordinary (non-bit-field) member +}; + +// Read a bit-field through a pointer. +unsigned int read_a(struct flags *s) + _ensures(return == s->a) +{ + return s->a; +} + +// Read a bit-field by value. +unsigned int read_b_by_value(_plain struct flags s) + _ensures(return == s.b) +{ + return s.b; +} + +// Read an ordinary member alongside bit-fields. +unsigned int read_full(struct flags *s) + _ensures(return == s->full) +{ + return s->full; +} + +// Writing an arbitrary value to a 3-bit field: the write masks the RHS to +// 3 bits (C unsigned modular truncation), so `s->a` ends up holding `v % 8`. +// Without masking this would violate the cell's `< pow2 3` refinement. +void write_a(struct flags *s, unsigned int v) + _ensures(s->a == v % 8) +{ + s->a = v; +} + +// Writing an in-range constant stores it unchanged. +void set_a(struct flags *s) + _ensures(s->a == 5) +{ + s->a = 5; +} + +// A _Bool bit-field of width 1. `_Bool` is an unsigned type so the frontend +// accepts it, but it is modeled as a plain F* `bool` (already a 1-bit value): +// no `< pow2 n` refinement and no write masking are needed. +struct bits { + _Bool flag : 1; + unsigned char nibble : 4; +}; + +// Read a _Bool bit-field. +_Bool read_flag(struct bits *s) + _ensures(return == s->flag) +{ + return s->flag; +} + +// Write a _Bool bit-field: a `_Bool` already holds only 0/1, so the value is +// stored unchanged (no truncation). +void write_flag(struct bits *s, _Bool v) + _ensures(s->flag == v) +{ + s->flag = v; +} + +unsigned char read_nibble(struct bits *s) + _ensures(return == s->nibble) +{ + return s->nibble; +} + +void write_nibble(struct bits *s, unsigned char v) + _ensures(s->nibble == v % 16) +{ + s->nibble = v; +} + +// A bit-field whose declared type is a typedef (`uint16_t` = unsigned short). +// The typedef must be resolved to its underlying machine width so the cell +// still carries the `< pow2 n` refinement. +struct tdef { + uint16_t a : 2; // value in [0, 4) +}; + +// The refinement on the typedef'd cell lets us prove the range on read +// (regression test for the reported typedef bit-field bug). +void tdef_in_range(struct tdef *s) +{ + _assert(s->a <= 3); +} + +uint16_t read_tdef(struct tdef *s) + _ensures(return == s->a) +{ + return s->a; +} + +void write_tdef(struct tdef *s, uint16_t v) + _ensures(s->a == v % 4) +{ + s->a = v; +} diff --git a/test/bitfields/fstar.fst.config.json b/test/bitfields/fstar.fst.config.json new file mode 120000 index 00000000..4100b019 --- /dev/null +++ b/test/bitfields/fstar.fst.config.json @@ -0,0 +1 @@ +../_templates/fstar.fst.config.json \ No newline at end of file diff --git a/test/bitfields/pal.config.json b/test/bitfields/pal.config.json new file mode 120000 index 00000000..d59f1cfa --- /dev/null +++ b/test/bitfields/pal.config.json @@ -0,0 +1 @@ +../_templates/pal.config.json \ No newline at end of file diff --git a/test/bitfields/pal.h b/test/bitfields/pal.h new file mode 120000 index 00000000..05ef83f9 --- /dev/null +++ b/test/bitfields/pal.h @@ -0,0 +1 @@ +../pal.h \ No newline at end of file