Translate sizeof/_Alignof to opaque c_sizeof/c_alignof

Previously, the proposed sizeof support (on the 'sizeof' branch)
constant-folded sizeof / _Alignof to integer literals using clang's
target ABI. This commits to a specific platform layout in the emitted
F* code, which we want to avoid.

This change introduces a small Pulse library 'Pulse.Lib.C.Sizeof'
that declares:

  - a reified 'c_type' inductive (Void / Bool / SizeT / PtrdiffT /
    Int / Pointer / Array / Named)
  - opaque  c_sizeof : c_type -> SizeT.t
  - opaque  c_alignof : c_type -> SizeT.t
  - axioms relating these to standard C facts (positivity, array
    decomposition, sign-independence, sizeof(intN_t) == N/8).

The translation pipeline now lowers C 'sizeof(T)' / '_Alignof(T)' to
opaque calls, with the type structure preserved as a c_type term
(e.g. sizeof(int)   -> c_sizeof (C_Int true 32)
      sizeof(T[8]) -> c_sizeof (C_Array (C_Int true 32) 8)
      sizeof(s)    -> c_sizeof (C_Named "ty_s")  for typedefs/structs).

Hauntedc (the spec mini-parser) understands sizeof(<type>) and
_Alignof(<type>) inside _ensures / _requires, so verified specs can
refer to the same opaque values as the function body.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

Author: KimayaBedarkar

cpp/iface.zng

@@ -23,6 +23,7 @@ use ::std::vec::Vec as Vec;
 use crate::ir::Ident as Ident;
 use crate::ir::SourceInfo as SourceInfo;
 use crate::ir::Type as Type;
+use crate::ir::CTypeExpr as CTypeExpr;
 use crate::ir::Stmt as Stmt;
 use crate::ir::Expr as Expr;
 use crate::ir::UnOp as UnOp;
@@ -44,6 +45,7 @@ mod crate::ir {
     type SourceInfo { #only_by_ref; }
     type Ident { wellknown_traits(?Sized); }
     type Type { #only_by_ref; }
+    type CTypeExpr { #only_by_ref; }
     type Expr { #only_by_ref; }
     type Stmt { #only_by_ref; }
 
@@ -86,6 +88,11 @@ mod crate::ir {
         fn deref(&self) -> &Type;
     }
 
+    type Rc<CTypeExpr> {
+        #layout(size=8, align=8);
+        fn deref(&self) -> &CTypeExpr;
+    }
+
     type Rc<Ident> {
         #layout(size=8, align=8);
         fn deref(&self) -> &Ident;
@@ -249,6 +256,17 @@ mod crate::clang {
     fn mk_type_arrayptr(Rc<SourceInfo>, Rc<Type>) -> Rc<Type>;
     fn mk_type_err(Rc<SourceInfo>) -> Rc<Type>;
 
+    fn mk_ctype_void(Rc<SourceInfo>) -> Rc<CTypeExpr>;
+    fn mk_ctype_bool(Rc<SourceInfo>) -> Rc<CTypeExpr>;
+    fn mk_ctype_sizet(Rc<SourceInfo>) -> Rc<CTypeExpr>;
+    fn mk_ctype_ptrdifft(Rc<SourceInfo>) -> Rc<CTypeExpr>;
+    fn mk_ctype_int(Rc<SourceInfo>, bool, u32) -> Rc<CTypeExpr>;
+    fn mk_ctype_pointer(Rc<SourceInfo>, Rc<CTypeExpr>) -> Rc<CTypeExpr>;
+    fn mk_ctype_array(Rc<SourceInfo>, Rc<CTypeExpr>, Rc<BigInt>) -> Rc<CTypeExpr>;
+    fn mk_ctype_named_typedef(Rc<SourceInfo>, Rc<Ident>) -> Rc<CTypeExpr>;
+    fn mk_ctype_named_struct(Rc<SourceInfo>, Rc<Ident>) -> Rc<CTypeExpr>;
+    fn mk_ctype_named_union(Rc<SourceInfo>, Rc<Ident>) -> Rc<CTypeExpr>;
+
     fn mk_bigint(&str) -> Rc<BigInt>;
 
     fn mk_bool_lit(Rc<SourceInfo>, bool) -> Rc<Expr>;
@@ -274,6 +292,9 @@ mod crate::clang {
     fn mk_live(Rc<SourceInfo>, Rc<Expr>) -> Rc<Expr>;
     fn mk_assign_expr(Rc<SourceInfo>, Rc<Expr>, Rc<Expr>) -> Rc<Expr>;
 
+    fn mk_sizeof(Rc<SourceInfo>, Rc<CTypeExpr>) -> Rc<Expr>;
+    fn mk_alignof(Rc<SourceInfo>, Rc<CTypeExpr>) -> Rc<Expr>;
+
     fn mk_lvalue_var(Rc<SourceInfo>, Rc<Ident>) -> Rc<Expr>;
     fn mk_lvalue_member(Rc<SourceInfo>, Rc<Expr>, Rc<Ident>) -> Rc<Expr>;
     fn mk_index(Rc<SourceInfo>, Rc<Expr>, Rc<Expr>) -> Rc<Expr>;

cpp/impl.cpp

@@ -348,6 +348,75 @@ class PALConsumer : public ASTConsumer {
     return mk_type_err(std::move(loc));
   }
 
+  /// Build a reified [CTypeExpr] for the type appearing as the operand of
+  /// `sizeof` / `_Alignof`. Mirrors [trQualType] but produces values that
+  /// are arguments to the opaque `c_sizeof` / `c_alignof` functions, and
+  /// preserves constant array lengths (which are dropped by [trQualType]).
+  Rc<ir::CTypeExpr> trCTypeFromQualType(QualType t, SourceRange range) {
+    t = t.IgnoreParens();
+    auto loc = getRange(range);
+
+    if (t.getAsString() == "size_t") {
+      return mk_ctype_sizet(std::move(loc));
+    } else if (t.getAsString() == "ptrdiff_t") {
+      return mk_ctype_ptrdifft(std::move(loc));
+    } else if (auto tydef = dyn_cast<TypedefType>(t)) {
+      auto id = ctx.mk_ident(toStr(tydef->getDecl()->getName()), loc.clone());
+      return mk_ctype_named_typedef(std::move(loc), std::move(id));
+#if LLVM_VERSION_MAJOR < 22
+    } else if (auto elab = dyn_cast<ElaboratedType>(t)) {
+      return trCTypeFromQualType(elab->desugar(), range);
+#endif
+    } else if (auto ptr = dyn_cast<PointerType>(t)) {
+      return mk_ctype_pointer(
+          std::move(loc), trCTypeFromQualType(ptr->getPointeeType(), range));
+    } else if (auto adj = dyn_cast<AdjustedType>(t)) {
+      return trCTypeFromQualType(adj->getOriginalType(), range);
+    } else if (auto carr = dyn_cast<ConstantArrayType>(t)) {
+      auto elem = trCTypeFromQualType(carr->getElementType(), range);
+      SmallString<32> nStr;
+      carr->getSize().toString(nStr, 10, /*Signed=*/false);
+      auto n = mk_bigint(toStr(StringRef(nStr)));
+      return mk_ctype_array(std::move(loc), std::move(elem), std::move(n));
+    } else if (auto rec = dyn_cast<RecordType>(t)) {
+      auto decl = rec->getDecl();
+      if (!decl->getIdentifier()) {
+        reportUnsupported(range, loc,
+                          "sizeof/_Alignof on anonymous struct/union outside "
+                          "of typedef is unsupported",
+                          "");
+        return mk_ctype_named_struct(loc.clone(),
+                                     ctx.mk_ident("__anon__"_rs, loc.clone()));
+      }
+      auto name = ctx.mk_ident(toStr(decl->getName()), loc.clone());
+      switch (decl->getTagKind()) {
+      case TagTypeKind::Struct:
+        return mk_ctype_named_struct(std::move(loc), std::move(name));
+      case TagTypeKind::Union:
+        return mk_ctype_named_union(std::move(loc), std::move(name));
+      default:
+        reportUnsupported(range, loc, "unsupported record kind in sizeof", "");
+        return mk_ctype_named_struct(std::move(loc), std::move(name));
+      }
+    }
+    if (t->isVoidType()) {
+      return mk_ctype_void(std::move(loc));
+    }
+    if (isBoolType(t)) {
+      return mk_ctype_bool(std::move(loc));
+    }
+    if (t->isSignedIntegerType() || t->isUnsignedIntegerType()) {
+      bool isSigned = t->isSignedIntegerType();
+      unsigned width = astCtx->getIntWidth(t);
+      return mk_ctype_int(std::move(loc), isSigned, width);
+    }
+
+    reportUnsupported(range, loc, "unsupported type in sizeof/_Alignof ",
+                      t->getTypeClassName());
+    return mk_ctype_named_struct(
+        loc.clone(), ctx.mk_ident("__unsupported__"_rs, loc.clone()));
+  }
+
   Rc<ir::Type> trTypeAttrs(AttrVec const &attrs, Rc<ir::Type> &&ty) {
     for (auto it = attrs.rbegin(); it != attrs.rend(); ++it) {
       if (auto ann = dyn_cast<AnnotateAttr>(*it)) {
@@ -797,6 +866,32 @@ class PALConsumer : public ASTConsumer {
       }
       // Other DeclRefExpr in rvalue context: treat as lvalue read
       return mk_rvalue_lvalue(std::move(loc), trLValue(e));
+    } else if (auto *u = dyn_cast<UnaryExprOrTypeTraitExpr>(e)) {
+      // sizeof / _Alignof: translated to opaque calls to c_sizeof /
+      // c_alignof on a reified C-type term. We deliberately do *not*
+      // commit to a specific numeric value here; the verifier sees an
+      // abstract size_t whose only known properties come from the axioms
+      // in Pulse.Lib.C.Sizeof. VLAs and other non-constant cases are
+      // unsupported.
+      if (u->getKind() == UETT_SizeOf || u->getKind() == UETT_AlignOf ||
+          u->getKind() == UETT_PreferredAlignOf) {
+        QualType argTy = u->getTypeOfArgument();
+        if (argTy->isVariableArrayType() || argTy->isDependentType() ||
+            argTy->isIncompleteType()) {
+          reportUnsupported(e->getSourceRange(), loc,
+                            "unsupported sizeof/_Alignof on incomplete, "
+                            "dependent, or variable-length type",
+                            "");
+          return mk_rvalue_err(std::move(loc),
+                               trQualType(e->getType(), e->getSourceRange()));
+        }
+        auto ctype = trCTypeFromQualType(argTy, u->getSourceRange());
+        if (u->getKind() == UETT_AlignOf ||
+            u->getKind() == UETT_PreferredAlignOf) {
+          return mk_alignof(std::move(loc), std::move(ctype));
+        }
+        return mk_sizeof(std::move(loc), std::move(ctype));
+      }
     }
 
     reportUnsupported(e->getSourceRange(), loc,

pulse/Pulse.Lib.C.Sizeof.fsti

@@ -0,0 +1,50 @@
+module Pulse.Lib.C.Sizeof
+
+open FStar.SizeT
+
+/// Reified C types used as arguments to opaque [c_sizeof] / [c_alignof].
+/// These values do not commit to any specific platform layout — they
+/// only identify the C type whose size or alignment is being asked for.
+noeq type c_type =
+  | C_Void
+  | C_Bool
+  | C_SizeT
+  | C_PtrdiffT
+  | C_Int : signed:bool -> width:nat -> c_type
+  | C_Pointer : c_type -> c_type
+  | C_Array : c_type -> nat -> c_type
+  | C_Named : string -> c_type
+
+/// Opaque size of a C type, in bytes. We commit to no specific value.
+val c_sizeof : c_type -> t
+
+/// Opaque alignment of a C type, in bytes. We commit to no specific value.
+val c_alignof : c_type -> t
+
+/// Sizes and alignments are always strictly positive on any conforming C
+/// implementation.
+val c_sizeof_pos (ty: c_type)
+  : Lemma (v (c_sizeof ty) > 0)
+    [SMTPat (v (c_sizeof ty))]
+
+val c_alignof_pos (ty: c_type)
+  : Lemma (v (c_alignof ty) > 0)
+    [SMTPat (v (c_alignof ty))]
+
+/// Array-type size decomposition: sizeof(T[n]) == n * sizeof(T).
+val c_sizeof_array (ty: c_type) (n: nat)
+  : Lemma (fits (n * v (c_sizeof ty)) /\
+           v (c_sizeof (C_Array ty n)) == n * v (c_sizeof ty))
+    [SMTPat (c_sizeof (C_Array ty n))]
+
+/// Sign of an integer type does not affect its size (C standard).
+val c_sizeof_int_sign (s1 s2: bool) (w: nat)
+  : Lemma (c_sizeof (C_Int s1 w) == c_sizeof (C_Int s2 w))
+
+/// For fixed-width integer types, the size in bytes is the width in bits
+/// divided by the bits-per-byte (8) — i.e. `sizeof(intN_t) == N/8`. This
+/// holds on any conforming C implementation where `CHAR_BIT == 8`.
+val c_sizeof_int_width (s: bool) (w: nat)
+  : Lemma (requires (w % 8 == 0))
+          (ensures (v (c_sizeof (C_Int s w)) == w / 8))
+    [SMTPat (c_sizeof (C_Int s w))]

pulse/Pulse.Lib.C.fsti

@@ -9,6 +9,7 @@ include Pulse.Class.PtsTo
 include FStar.Int.Cast
 include Pulse.Lib.C.Casts
 include Pulse.Lib.C.UnaryOps
+include Pulse.Lib.C.Sizeof
 include Pulse.Lib.WithPure
 open Pulse.Lib.Core
 let _Bool = bool

src/clang.rs

@@ -603,6 +603,37 @@ fn mk_type_err(loc: Rc<SourceInfo>) -> Rc<Type> {
     mk_ast(loc, TypeT::Error)
 }
 
+fn mk_ctype_void(loc: Rc<SourceInfo>) -> Rc<CTypeExpr> {
+    mk_ast(loc, CTypeExprT::Void)
+}
+fn mk_ctype_bool(loc: Rc<SourceInfo>) -> Rc<CTypeExpr> {
+    mk_ast(loc, CTypeExprT::Bool)
+}
+fn mk_ctype_sizet(loc: Rc<SourceInfo>) -> Rc<CTypeExpr> {
+    mk_ast(loc, CTypeExprT::SizeT)
+}
+fn mk_ctype_ptrdifft(loc: Rc<SourceInfo>) -> Rc<CTypeExpr> {
+    mk_ast(loc, CTypeExprT::PtrdiffT)
+}
+fn mk_ctype_int(loc: Rc<SourceInfo>, signed: bool, width: u32) -> Rc<CTypeExpr> {
+    mk_ast(loc, CTypeExprT::Int { signed, width })
+}
+fn mk_ctype_pointer(loc: Rc<SourceInfo>, to: Rc<CTypeExpr>) -> Rc<CTypeExpr> {
+    mk_ast(loc, CTypeExprT::Pointer(to))
+}
+fn mk_ctype_array(loc: Rc<SourceInfo>, elem: Rc<CTypeExpr>, n: Rc<BigInt>) -> Rc<CTypeExpr> {
+    mk_ast(loc, CTypeExprT::Array(elem, n))
+}
+fn mk_ctype_named_typedef(loc: Rc<SourceInfo>, name: Rc<Ident>) -> Rc<CTypeExpr> {
+    mk_ast(loc, CTypeExprT::Named(TypeRefKind::Typedef(name)))
+}
+fn mk_ctype_named_struct(loc: Rc<SourceInfo>, name: Rc<Ident>) -> Rc<CTypeExpr> {
+    mk_ast(loc, CTypeExprT::Named(TypeRefKind::Struct(name)))
+}
+fn mk_ctype_named_union(loc: Rc<SourceInfo>, name: Rc<Ident>) -> Rc<CTypeExpr> {
+    mk_ast(loc, CTypeExprT::Named(TypeRefKind::Union(name)))
+}
+
 fn mk_bigint(s: &str) -> Rc<BigInt> {
     Rc::from(BigInt::from_str(s).unwrap())
 }
@@ -681,6 +712,13 @@ fn mk_assign_expr(loc: Rc<SourceInfo>, lhs: Rc<Expr>, rhs: Rc<Expr>) -> Rc<Expr>
     mk_ast(loc, ExprT::AssignExpr(lhs, rhs))
 }
 
+fn mk_sizeof(loc: Rc<SourceInfo>, ty: Rc<CTypeExpr>) -> Rc<Expr> {
+    mk_ast(loc, ExprT::SizeOf(ty))
+}
+fn mk_alignof(loc: Rc<SourceInfo>, ty: Rc<CTypeExpr>) -> Rc<Expr> {
+    mk_ast(loc, ExprT::AlignOf(ty))
+}
+
 pub struct StructInitBuilder {
     loc: Rc<SourceInfo>,
     name: Rc<Ident>,

src/env.rs

@@ -358,6 +358,9 @@ impl Env {
             },
             ExprT::Cast(_, ty) => Ok(ty.clone().into()),
             ExprT::Error(ty) => Ok(ty.clone().into()),
+            ExprT::SizeOf(_) | ExprT::AlignOf(_) => {
+                Ok(TypeT::SizeT.with_loc_core(expr.loc.clone()).into())
+            }
             ExprT::Malloc(ty) | ExprT::Calloc(ty) => Ok(expr
                 .reuse_loc(TypeT::Pointer(ty.clone(), PointerKind::Ref))
                 .into()),

src/hauntedc.rs

@@ -354,6 +354,28 @@ fn mk_binop(binop: BinOp, lhs: Expr, rhs: Expr, loc: Rc<SourceInfo>) -> Expr {
         .into()
 }
 
+/// Convert a TypeT (as parsed by hauntedc's `type_name`) into a reified
+/// CTypeExprT for use as the argument of `sizeof` / `_Alignof`. Returns
+/// None if the type cannot be reified (e.g. SLProp, SpecInt, Refine, ...).
+fn type_t_to_ctype(ty: &TypeT) -> Option<CTypeExprT> {
+    Some(match ty {
+        TypeT::Void => CTypeExprT::Void,
+        TypeT::Bool => CTypeExprT::Bool,
+        TypeT::SizeT => CTypeExprT::SizeT,
+        TypeT::PtrdiffT => CTypeExprT::PtrdiffT,
+        TypeT::Int { signed, width } => CTypeExprT::Int {
+            signed: *signed,
+            width: *width,
+        },
+        TypeT::Pointer(inner, _) => {
+            let inner_ct = type_t_to_ctype(&inner.val)?;
+            CTypeExprT::Pointer(inner_ct.with_loc(inner.loc.clone()))
+        }
+        TypeT::TypeRef(tk) => CTypeExprT::Named(tk.clone()),
+        _ => return None,
+    })
+}
+
 type Extra<'tokens, 'src> = extra::Err<Rich<'tokens, Token<'src>, SimpleSpan>>;
 
 fn type_parser<
@@ -686,6 +708,48 @@ fn expr_parser<
                         .with_loc(loc)
                         .into()
                 }),
+            // sizeof(<type>) / sizeof(<type>[N]) and _Alignof(<type>)
+            select! {
+                Token::Ident("sizeof") => true,
+                Token::Ident("_Alignof") => false,
+                Token::Ident("__alignof__") => false,
+            }
+            .padded_by(ws())
+            .then(
+                type_name
+                    .clone()
+                    .then(
+                        select! { Token::Integer(i, _) => i }
+                            .delimited_by(punct(Punct::LBracket), punct(Punct::RBracket))
+                            .or_not(),
+                    )
+                    .delimited_by(punct(Punct::LParen), punct(Punct::RParen)),
+            )
+            .try_map(move |(is_sizeof, (ty, arr_opt)), span: SimpleSpan| {
+                let loc = sift.resolve_source_info(&span);
+                let Some(ct_inner) = type_t_to_ctype(&ty.val) else {
+                    return Err(Rich::custom(
+                        span,
+                        format!("unsupported type in sizeof/_Alignof"),
+                    ));
+                };
+                let inner_ctype = ct_inner.with_loc(ty.loc.clone());
+                let ct = match arr_opt {
+                    None => inner_ctype,
+                    Some(n_str) => {
+                        let n = BigInt::from_str(n_str)
+                            .map_err(|e| Rich::custom(span, format!("{}", e)))?;
+                        CTypeExprT::Array(inner_ctype, Rc::new(n)).with_loc(loc.clone())
+                    }
+                };
+                let expr_t = if is_sizeof {
+                    ExprT::SizeOf(ct)
+                } else {
+                    ExprT::AlignOf(ct)
+                };
+                Ok::<Expr, Rich<'_, Token<'_>, SimpleSpan>>(expr_t.with_loc(loc).into())
+            })
+            .boxed(),
             ident
                 .clone() // TODO: function should be postfix_expression
                 .then(

src/ir/mod.rs

@@ -304,9 +304,28 @@ pub enum ExprT {
     /// Assignment expression: assigns rhs to lhs, evaluates to rhs.
     /// Lowered to Assign statement + value in elab pass.
     AssignExpr(Rc<Expr>, Rc<Expr>),
+    /// `sizeof(T)` — translated to an opaque `c_sizeof` call.
+    SizeOf(Rc<CTypeExpr>),
+    /// `_Alignof(T)` / `__alignof__(T)` — translated to an opaque `c_alignof` call.
+    AlignOf(Rc<CTypeExpr>),
     Error(Rc<Type>),
 }
 
+/// Reified C type used as the argument of [ExprT::SizeOf] / [ExprT::AlignOf].
+/// Mirrors the `c_type` inductive declared in `Pulse.Lib.C.Sizeof`.
+pub type CTypeExpr = Ast<CTypeExprT>;
+#[derive(Debug, PartialEq, Eq, Hash, Clone)]
+pub enum CTypeExprT {
+    Void,
+    Bool,
+    SizeT,
+    PtrdiffT,
+    Int { signed: bool, width: u32 },
+    Pointer(Rc<CTypeExpr>),
+    Array(Rc<CTypeExpr>, Rc<BigInt>),
+    Named(TypeRefKind),
+}
+
 pub type IdentT = str;
 pub type Ident = Ast<Rc<IdentT>>;