diff --git a/backend/cn/compile.ml b/backend/cn/compile.ml index 56ac3f4c4..f395e5b07 100644 --- a/backend/cn/compile.ml +++ b/backend/cn/compile.ml @@ -636,8 +636,7 @@ module EffectfulTranslation = struct mk_translate_binop loc bop (e1, e2) | CNExpr_sizeof ct -> let scty = Sctypes.of_ctype_unsafe loc ct in - let n = Memory.size_of_ctype scty in - return (IT (Const (Z (Z.of_int n)), SBT.Integer)) + return (IT (SizeOf scty, SBT.Integer)) | CNExpr_offsetof (tag, member) -> let@ _ = lookup_struct loc tag env in return (IT ((MemberOffset (tag, member)), SBT.Integer)) diff --git a/backend/cn/indexTerms.ml b/backend/cn/indexTerms.ml index 27537efc6..ea2ba9550 100644 --- a/backend/cn/indexTerms.ml +++ b/backend/cn/indexTerms.ml @@ -65,6 +65,7 @@ let rec free_vars_ = function | Cast (_cbt, t) -> free_vars t | MemberOffset (_tag, _id) -> SymSet.empty | ArrayOffset (_sct, t) -> free_vars t + | SizeOf _t -> SymSet.empty | Nil _bt -> SymSet.empty | Cons (t1, t2) -> free_vars_list [t1; t2] | Head t -> free_vars t @@ -124,6 +125,7 @@ let rec fold_ f binders acc = function | Cast (_cbt, t) -> fold f binders acc t | MemberOffset (_tag, _id) -> acc | ArrayOffset (_sct, t) -> fold f binders acc t + | SizeOf _ct -> acc | Nil _bt -> acc | Cons (t1, t2) -> fold_list f binders acc [t1; t2] | Head t -> fold f binders acc t @@ -256,6 +258,8 @@ let rec subst (su : typed subst) (IT (it, bt)) = IT (MemberOffset (tag, member), bt) | ArrayOffset (tag, t) -> IT (ArrayOffset (tag, subst su t), bt) + | SizeOf t -> + IT (SizeOf t, bt) | Aligned t -> IT (Aligned {t= subst su t.t; align= subst su t.align}, bt) | Representable (rt, t) -> diff --git a/backend/cn/simplify.ml b/backend/cn/simplify.ml index d21c4ac92..e8b597ec0 100644 --- a/backend/cn/simplify.ml +++ b/backend/cn/simplify.ml @@ -541,6 +541,8 @@ module IndexTerms = struct | _ -> mul_ (int_ (Memory.size_of_ctype ct), t) (* IT (Pointer_op (ArrayOffset (ct, t)), bt) *) end + | SizeOf ct -> + int_ (Memory.size_of_ctype ct) | Representable (ct, t) -> IT (Representable (ct, aux t), the_bt) | Good (ct, t) -> diff --git a/backend/cn/solver.ml b/backend/cn/solver.ml index f294ca2ae..0a19fca26 100644 --- a/backend/cn/solver.ml +++ b/backend/cn/solver.ml @@ -614,6 +614,8 @@ module Translate = struct term (int_ (Option.get (Memory.member_offset decl member))) | ArrayOffset (ct, t) -> term (mul_ (int_ (Memory.size_of_ctype ct), t)) + | SizeOf ct -> + term (int_ (Memory.size_of_ctype ct)) | Nil ibt -> make_uf (plain (!^"nil_uf"^^angles(BT.pp ibt))) (List ibt) [] | Cons (t1, t2) -> diff --git a/backend/cn/terms.ml b/backend/cn/terms.ml index a4c9f9e88..be2017f0a 100644 --- a/backend/cn/terms.ml +++ b/backend/cn/terms.ml @@ -87,6 +87,7 @@ type 'bt term_ = | Constructor of Sym.t * (Id.t * 'bt term) list | MemberOffset of Sym.t * Id.t | ArrayOffset of Sctypes.t (*element ct*) * 'bt term (*index*) + | SizeOf of Sctypes.t | Nil of BaseTypes.t | Cons of 'bt term * 'bt term | Head of 'bt term @@ -285,43 +286,45 @@ let pp : 'bt 'a. ?atomic:bool -> ?f:('bt term -> Pp.doc -> Pp.doc) -> 'bt term - mparens (c_app !^"offsetof" [Sym.pp tag; Id.pp member]) | ArrayOffset (ct, t) -> mparens (c_app !^"arrayOffset" [Sctypes.pp ct; aux false t]) + | SizeOf t -> + mparens (c_app !^"sizeof" [Sctypes.pp t]) (* end *) (* | CT_pred ct_pred -> *) (* begin match ct_pred with *) | Aligned t -> - c_app !^"aligned" [aux false t.t; aux false t.align] + mparens (c_app !^"aligned" [aux false t.t; aux false t.align]) | Representable (rt, t) -> - c_app (!^"repr" ^^ angles (CT.pp rt)) [aux false t] + mparens (c_app (!^"repr" ^^ angles (CT.pp rt)) [aux false t]) | Good (rt, t) -> - c_app (!^"good" ^^ angles (CT.pp rt)) [aux false t] + mparens (c_app (!^"good" ^^ angles (CT.pp rt)) [aux false t]) | WrapI (ity, t) -> - c_app (!^"wrapI" ^^ angles (CT.pp (Integer ity))) [aux false t] + mparens (c_app (!^"wrapI" ^^ angles (CT.pp (Integer ity))) [aux false t]) (* end *) (* | List_op list_op -> *) (* begin match list_op with *) | Head (o1) -> - c_app !^"hd" [aux false o1] + mparens (c_app !^"hd" [aux false o1]) | Tail (o1) -> - c_app !^"tl" [aux false o1] + mparens (c_app !^"tl" [aux false o1]) | Nil bt -> !^"nil" ^^ angles (BaseTypes.pp bt) | Cons (t1,t2) -> mparens (aux true t1 ^^ colon ^^ colon ^^ aux true t2) | NthList (n, xs, d) -> - c_app !^"nth_list" [aux false n; aux false xs; aux false d] + mparens (c_app !^"nth_list" [aux false n; aux false xs; aux false d]) | ArrayToList (arr, i, len) -> - c_app !^"array_to_list" [aux false arr; aux false i; aux false len] + mparens (c_app !^"array_to_list" [aux false arr; aux false i; aux false len]) (* end *) (* | Set_op set_op -> *) (* begin match set_op with *) (* end *) | MapConst (_bt, t) -> - c_app !^"const" [aux false t] + mparens (c_app !^"const" [aux false t]) | MapGet (t1, t2) -> - aux true t1 ^^ brackets (aux false t2) + mparens (aux true t1 ^^ brackets (aux false t2)) | MapSet (t1, t2, t3) -> - aux true t1 ^^ - brackets (aux false t2 ^^^ equals ^^^ aux false t3) + mparens (aux true t1 ^^ + brackets (aux false t2 ^^^ equals ^^^ aux false t3)) | MapDef ((s,_), t) -> brackets (Sym.pp s ^^^ !^"->" ^^^ aux false t) (* | Map_op map_op -> *) @@ -347,8 +350,9 @@ let pp : 'bt 'a. ?atomic:bool -> ?f:('bt term -> Pp.doc -> Pp.doc) -> 'bt term - (* prefix 2 0 root_pp @@ align (flow_map (break 0) pp_op ops) *) | Apply (name, args) -> c_app (Sym.pp name) (List.map (aux false) args) - | Let ((name, x1), x2) -> parens (!^ "let" ^^^ Sym.pp name ^^^ Pp.equals ^^^ - aux false x1 ^^^ !^ "in" ^^^ aux false x2) + | Let ((name, x1), x2) -> + parens (!^ "let" ^^^ Sym.pp name ^^^ Pp.equals ^^^ + aux false x1 ^^^ !^ "in" ^^^ aux false x2) | Match (e, cases) -> !^"match" ^^^ aux false e ^^^ braces ( (* copying from mparens *) diff --git a/backend/cn/wellTyped.ml b/backend/cn/wellTyped.ml index f00072e72..a6a8f9d44 100644 --- a/backend/cn/wellTyped.ml +++ b/backend/cn/wellTyped.ml @@ -541,6 +541,9 @@ module WIT = struct let@ () = WCT.is_ct loc ct in let@ t = check loc Integer t in return (IT (ArrayOffset (ct, t), Integer)) + | SizeOf ct -> + let@ () = WCT.is_ct loc ct in + return (IT (SizeOf ct, Integer)) | Aligned t -> let@ t_t = check loc Loc t.t in let@ t_align = check loc Integer t.align in