Add support for unsigned bit-fields in structs

cpp/iface.zng

@@ -202,6 +202,7 @@ mod crate::clang {
         fn arg(&mut self, Rc<Ident>, Rc<Type>, ParamMode);
         fn arg_anon(&mut self, Rc<Type>, ParamMode);
         fn field(&mut self, Rc<Ident>, Rc<Type>);
+        fn field_bitfield(&mut self, Rc<Ident>, Rc<Type>, u32);
         fn ghost_arg(&mut self, Rc<Ident>, Rc<Type>);
         fn requires(&mut self, Rc<Expr>);
         fn ensures(&mut self, Rc<Expr>);

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<VariableArrayType>(qtPtr) || isa<IncompleteArrayType>(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<ir::Ident> 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<VariableArrayType>(qtPtr) || isa<IncompleteArrayType>(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<VariableArrayType>(qtPtr) || isa<IncompleteArrayType>(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 {

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:

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

src/clang.rs

@@ -480,6 +480,18 @@ impl DeclBuilder {
         })
     }
 
+    fn field_bitfield(&mut self, name: Rc<Ident>, ty: Rc<Type>, 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<Expr>) {
         self.requires.push(p)
     }

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<Type> },
+    /// 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<Type>,
+        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<u32> {
+        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<SourceInfo>) -> Rc<Type> {
         match self {
             FieldT::Plain { ty, .. } => ty.clone(),
+            FieldT::BitField { ty, .. } => ty.clone(),
         }
     }
 }

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

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

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