Introduce ESizeof to InputAST

lib/Ast.ml

@@ -295,6 +295,7 @@ type expr' =
   | EStandaloneComment of string
   | EAddrOf of expr
   | ETernary of expr * expr * expr
+  | ESizeof of typ_wo
 
   [@@deriving show,
     visitors { variety = "map"; ancestors = [ "map_typ_adapter" ]; name = "map_expr" },

lib/AstToCFlat.ml

@@ -1012,6 +1012,10 @@ and mk_expr (env: env) (locals: locals) (e: expr): locals * CF.expr =
       (* No need for ternary in CFlat, turn to if-then-else and recurse *)
       mk_expr env locals (with_type e.typ (EIfThenElse (e1, e2, e3)))
 
+  | ESizeof t ->
+     (* sizeof is resolved statically for Wasm — all sizes are known *)
+     locals, mk_uint32 (byte_size env t)
+
 (* See digression for [dup32] in CFlatToWasm *)
 let scratch_locals =
   [ I64; I64; I32; I32; I32 ]

lib/AstToCStar.ml

@@ -483,6 +483,9 @@ and mk_expr env in_stmt under_initializer_list e =
   | ETernary (e1, e2, e3) ->
       CStar.Ternary (mk_expr env false e1, mk_expr env false e2, mk_expr env false e3)
 
+  | ESizeof t ->
+      CStar.Sizeof (mk_type env t)
+
   | _ ->
       Warn.maybe_fatal_error (KPrint.bsprintf "%a" Loc.ploc env.location, NotLowStar e);
       CStar.Any

lib/AstToMiniRust.ml

@@ -1356,6 +1356,10 @@ and translate_expr_with_type (env: env) ?(context=`Other) (fn_t_ret: MiniRust.ty
       (* Rust has if-then-else expressions, go back to it and keep going. *)
       translate_expr_with_type env ~context fn_t_ret (Ast.with_type e.typ (Ast.EIfThenElse (e1, e2, e3))) t_ret
 
+  | ESizeof t ->
+      (* use std::mem::size_of *)
+      env, Call (Name ["std"; "mem"; "size_of"], [translate_type env t], [])
+
 and translate_pat env (p: Ast.pattern): MiniRust.pat =
   match p.node with
   | PBound v -> VarP v

lib/CStar.ml

@@ -86,6 +86,7 @@ and expr =
         contain anything as arguments, including statements. *)
   | Type of typ
   | Ternary of expr * expr * expr
+  | Sizeof of typ
   [@@deriving show]
 
 and block =

lib/CStarToC11.ml

@@ -166,6 +166,8 @@ let rec vars_of m = function
       vars_of_block m stmts
   | Ternary (e1, e2, e3) ->
       S.union (vars_of m e1) (S.union (vars_of m e2) (vars_of m e3))
+  | Sizeof _t ->
+      S.empty
 
 and vars_of_block m stmts =
   KList.reduce S.union (List.map (vars_of_stmt m) stmts)
@@ -743,7 +745,7 @@ and mk_stmt m (stmt: stmt): C.stmt list =
           | Constant _ | Var _ | Macro _ | Qualified _
           | BufRead _ | BufSub _ | BufNull
           | Op _ | Bool _  | Type _ | StringLiteral _
-          | Any ->
+          | Any | Sizeof _ ->
             true
 
           | Ternary (c, t, e) ->
@@ -1224,6 +1226,9 @@ and mk_expr m (e: expr): C.expr =
   | Ternary (c, t, e) ->
       Ternary (mk_expr m c, mk_expr m t, mk_expr m e)
 
+  | Sizeof t ->
+      Sizeof (Type (mk_type m t))
+
 and mk_compound_literal m name fields =
   let name = to_c_name m (name, Type) in
   match fields with

lib/Checker.ml

@@ -331,7 +331,8 @@ and check' env t e =
   | EFor _
   | EIgnore _
   | EStandaloneComment _
-  | EApp _ ->
+  | EApp _
+  | ESizeof _ ->
       c (infer env e)
 
   | ECast (_, t) ->
@@ -892,6 +893,9 @@ and infer' env e =
       check_eqtype env t1 t2;
       t1
 
+  | ESizeof _t ->
+     sizet
+
 and infer_and_check_eq: 'a. env -> ('a -> typ) -> 'a list -> typ =
   fun env f l ->
   let t_base = ref None in

lib/InputAst.ml

@@ -106,6 +106,7 @@ and expr =
   | EBufNull of typ
   | EBufDiff of (expr * expr)
     (** e1 - e2 *)
+  | ESizeof of typ
 
 and branches =
   branch list
@@ -165,7 +166,7 @@ let flatten_arrow =
 
 type version = int
   [@@deriving yojson]
-let current_version: version = 31
+let current_version: version = 32
 
 type file = string * program
   [@@deriving yojson]

lib/InputAstToAst.ml

@@ -292,6 +292,8 @@ and mk_expr = function
       mk (EStandaloneComment s)
   | I.EAddrOf e ->
       mk (EAddrOf (mk_expr e))
+  | I.ESizeof t ->
+      mk (ESizeof (mk_typ t))
 
 and mk_branches branches =
   List.map mk_branch branches

lib/PrintAst.ml

@@ -375,6 +375,8 @@ and print_expr env { node; typ; meta } =
           string "?" ^/^ print_expr env t ^/^
           string ":" ^/^ print_expr env e
       )
+  | ESizeof t ->
+      string "sizeof" ^^ parens (print_typ t)
 
 and print_poly_comp = function
   | PEq -> equals

lib/Simplify.ml

@@ -1379,7 +1379,8 @@ and hoist_expr tbl loc pos e =
   | EEnum _
   | EStandaloneComment _
   | EPolyComp _
-  | EOp _ ->
+  | EOp _
+  | ESizeof _ ->
       [], e
 
   | EAddrOf e ->

lib/SimplifyMerge.ml

@@ -78,6 +78,7 @@ let rec merge' (env: env) (u: S.t) (e: expr): S.t * S.t * expr =
   | EEnum _
   | EStandaloneComment _
   | EAbort _
+  | ESizeof _
   | EBufNull ->
       keys env, u, e
 

lib/Structs.ml

@@ -608,7 +608,8 @@ let to_addr is_struct =
     | EPushFrame
     | EPopFrame
     | EStandaloneComment _
-    | EEnum _ ->
+    | EEnum _
+    | ESizeof _ ->
         not_struct ();
         e