[sledge] Remove Exp.size_of and Term.size_of

Summary:
Having `val size_of : Typ.t -> t` in the signature of `Term` and `val
size_of : t -> t` in the signature of `Exp` gives the impression that
`Term` and `Exp` know something about `Typ`. But they don't, those
functions are only trivial convenience wrappers, and only have a few
uses, so just inline them to clarify that it is `Typ` that knows about
the sizes of types.

Reviewed By: jvillard

Differential Revision: D21441535

fbshipit-source-id: 09b135a8c

sledge/bin/frontend.ml

@@ -864,6 +864,9 @@ let rec xlate_func_name x llv =
 
 let ignored_callees = Hash_set.create (module String)
 
+let exp_size_of exp =
+  Exp.integer Typ.siz (Z.of_int (Typ.size_of (Exp.typ exp)))
+
 let xlate_instr :
        pop_thunk
     -> x
@@ -902,12 +905,12 @@ let xlate_instr :
   match opcode with
   | Load ->
       let reg = xlate_name x instr in
-      let len = Exp.size_of (Exp.reg reg) in
+      let len = exp_size_of (Exp.reg reg) in
       let ptr = xlate_value x (Llvm.operand instr 0) in
       emit_inst (Llair.Inst.load ~reg ~ptr ~len ~loc)
   | Store ->
       let exp = xlate_value x (Llvm.operand instr 0) in
-      let len = Exp.size_of exp in
+      let len = exp_size_of exp in
       let ptr = xlate_value x (Llvm.operand instr 1) in
       emit_inst (Llair.Inst.store ~ptr ~exp ~len ~loc)
   | Alloca ->
@@ -919,7 +922,7 @@ let xlate_instr :
           (xlate_value x rand)
       in
       assert (Poly.(Llvm.classify_type (Llvm.type_of instr) = Pointer)) ;
-      let len = Exp.size_of (Exp.reg reg) in
+      let len = exp_size_of (Exp.reg reg) in
       emit_inst (Llair.Inst.alloc ~reg ~num ~len ~loc)
   | Call -> (
       let maybe_llfunc = Llvm.operand instr (Llvm.num_operands instr - 1) in
@@ -970,7 +973,7 @@ let xlate_instr :
             (* operator new(unsigned long, std::align_val_t) *) ] ->
             let reg = xlate_name x instr in
             let num = xlate_value x (Llvm.operand instr 0) in
-            let len = Exp.size_of (Exp.reg reg) in
+            let len = exp_size_of (Exp.reg reg) in
             emit_inst (Llair.Inst.alloc ~reg ~num ~len ~loc)
         | ["_ZdlPv" (* operator delete(void* ptr) *)]
          |[ "_ZdlPvSt11align_val_t"
@@ -1086,7 +1089,7 @@ let xlate_instr :
         when num_actuals > 0 ->
           let reg = xlate_name x instr in
           let num = xlate_value x (Llvm.operand instr 0) in
-          let len = Exp.size_of (Exp.reg reg) in
+          let len = exp_size_of (Exp.reg reg) in
           let dst, blocks = xlate_jump x instr return_blk loc [] in
           emit_term
             ~prefix:[Llair.Inst.alloc ~reg ~num ~len ~loc]

sledge/src/domain_sh.ml

@@ -20,7 +20,7 @@ let init globals =
   IArray.fold globals ~init:Sh.emp ~f:(fun q -> function
     | {Global.reg; init= Some arr} ->
         let loc = Term.var (Reg.var reg) in
-        let len = Term.size_of (Exp.typ arr) in
+        let len = Term.integer (Z.of_int (Typ.size_of (Exp.typ arr))) in
         let arr = arr.term in
         Sh.star q (Sh.seg {loc; bas= loc; len; siz= len; arr})
     | _ -> q )

sledge/src/exec.ml

@@ -315,7 +315,7 @@ let calloc_spec us reg num len =
   let post = Sh.or_ (null_eq (Term.var reg)) (Sh.seg seg) in
   {xs; foot; sub; ms; post}
 
-let size_of_ptr = Term.size_of Typ.ptr
+let size_of_ptr = Term.integer (Z.of_int (Typ.size_of Typ.ptr))
 
 (* { p-[_;_)->⟨W,_⟩ }
  *   posix_memalign r p s
@@ -487,7 +487,8 @@ let nallocx_spec us reg siz =
   let post = Sh.or_ (null_eq loc) (Sh.pure (Term.eq loc siz)) in
   {xs; foot; sub; ms; post}
 
-let size_of_int_mul = Term.mul (Term.size_of Typ.siz)
+let size_of_int_mul =
+  Term.mul (Term.integer (Z.of_int (Typ.size_of Typ.siz)))
 
 (* { r-[_;_)->⟨m,_⟩ * i-[_;_)->⟨_,m⟩ * w=0 * n=0 }
  *   mallctl r i w n

sledge/src/exp.ml

@@ -497,8 +497,6 @@ let struct_rec key =
          forcing the recursive thunks also updates this value. *)
       {desc= ApN (Struct_rec, typ, elts); term= rec_app ~id IArray.empty}
 
-let size_of exp = integer Typ.siz (Z.of_int (Typ.size_of (typ exp)))
-
 (** Traverse *)
 
 let fold_exps e ~init ~f =

sledge/src/exp.mli

@@ -200,8 +200,6 @@ val struct_rec :
     one point on each cycle. Failure to obey these requirements will lead to
     stack overflow. *)
 
-val size_of : t -> t
-
 (** Traverse *)
 
 val fold_regs : t -> init:'a -> f:('a -> Reg.t -> 'a) -> 'a

sledge/src/term.ml

@@ -1124,7 +1124,6 @@ let concat xs = normN Concat (IArray.of_array xs)
 let record elts = normN Record elts
 let select ~rcd ~idx = norm1 (Select idx) rcd
 let update ~rcd ~idx ~elt = norm2 (Update idx) rcd elt
-let size_of t = integer (Z.of_int (Typ.size_of t))
 
 let eq_concat (siz, arr) ms =
   eq (memory ~siz ~arr)

sledge/src/term.mli

@@ -248,8 +248,6 @@ val rec_app :
      (module Hashtbl.Key_plain with type t = 'id)
   -> (id:'id -> recN -> t lazy_t iarray -> t) Staged.t
 
-val size_of : Typ.t -> t
-
 (** Transform *)
 
 val map : t -> f:(t -> t) -> t