From 849c61221ddb5a961c9179f9069e5a7bc44b0b74 Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Thu, 7 May 2020 16:53:57 -0700 Subject: [PATCH] [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 | 13 ++++++++----- sledge/src/domain_sh.ml | 2 +- sledge/src/exec.ml | 5 +++-- sledge/src/exp.ml | 2 -- sledge/src/exp.mli | 2 -- sledge/src/term.ml | 1 - sledge/src/term.mli | 2 -- 7 files changed, 12 insertions(+), 15 deletions(-) diff --git a/sledge/bin/frontend.ml b/sledge/bin/frontend.ml index ab9a5e0c5..f7ad93b23 100644 --- a/sledge/bin/frontend.ml +++ b/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] diff --git a/sledge/src/domain_sh.ml b/sledge/src/domain_sh.ml index 327b6ec61..7ca98248a 100644 --- a/sledge/src/domain_sh.ml +++ b/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 ) diff --git a/sledge/src/exec.ml b/sledge/src/exec.ml index 58b2d32b8..453525f58 100644 --- a/sledge/src/exec.ml +++ b/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 diff --git a/sledge/src/exp.ml b/sledge/src/exp.ml index df1364bdc..3f8ba7d49 100644 --- a/sledge/src/exp.ml +++ b/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 = diff --git a/sledge/src/exp.mli b/sledge/src/exp.mli index 9e387d664..34eba21e3 100644 --- a/sledge/src/exp.mli +++ b/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 diff --git a/sledge/src/term.ml b/sledge/src/term.ml index 54541a8bf..98788d883 100644 --- a/sledge/src/term.ml +++ b/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) diff --git a/sledge/src/term.mli b/sledge/src/term.mli index 253067d48..60f14e8cb 100644 --- a/sledge/src/term.mli +++ b/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