fix 'sizeof' issue

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

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

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

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

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

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