From 65997b6a4416e4aee834ef58c189c5fb567b317a Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Thu, 9 Aug 2018 01:21:09 -0700 Subject: [PATCH] [inferbo] Remove sizeof function Summary: It removes the sizeof function because most of the cases on static types are addressed in the clang frontend. Depends on D9193802 Reviewed By: mbouaziz Differential Revision: D9213876 fbshipit-source-id: 0ce2f3749 --- .../src/bufferoverrun/bufferOverrunModels.ml | 6 +- .../bufferoverrun/bufferOverrunSemantics.ml | 57 ++----------------- infer/src/bufferoverrun/bufferOverrunUtils.ml | 8 +-- 3 files changed, 11 insertions(+), 60 deletions(-) diff --git a/infer/src/bufferoverrun/bufferOverrunModels.ml b/infer/src/bufferoverrun/bufferOverrunModels.ml index d76203758..1c7657252 100644 --- a/infer/src/bufferoverrun/bufferOverrunModels.ml +++ b/infer/src/bufferoverrun/bufferOverrunModels.ml @@ -100,9 +100,7 @@ let malloc size_exp = let size_exp = Option.value dyn_length ~default:length0 in Relation.SymExp.of_exp ~get_sym_f:(Sem.get_sym_f mem) size_exp in - let v = - Sem.eval_array_alloc allocsite typ ~stride ~offset ~size |> Dom.Val.set_traces traces - in + let v = Sem.eval_array_alloc allocsite ~stride ~offset ~size |> Dom.Val.set_traces traces in mem |> Dom.Mem.add_stack (Loc.of_id id) v |> Dom.Mem.init_array_relation allocsite ~offset ~size ~size_exp_opt |> set_uninitialized location typ (Dom.Val.get_array_locs v) @@ -196,7 +194,7 @@ let set_array_length array length_exp = let length = Sem.eval length_exp mem |> Dom.Val.get_itv in let stride = Option.map ~f:IntLit.to_int_exn stride in let allocsite = Sem.get_allocsite pname ~node_hash ~inst_num:0 ~dimension:1 in - let v = Sem.eval_array_alloc allocsite elt ~stride ~offset:Itv.zero ~size:length in + let v = Sem.eval_array_alloc allocsite ~stride ~offset:Itv.zero ~size:length in mem |> Dom.Mem.add_stack (Loc.of_pvar array_pvar) v |> set_uninitialized location elt (Dom.Val.get_array_locs v) | _ -> diff --git a/infer/src/bufferoverrun/bufferOverrunSemantics.ml b/infer/src/bufferoverrun/bufferOverrunSemantics.ml index cc6a77e9c..46f571282 100644 --- a/infer/src/bufferoverrun/bufferOverrunSemantics.ml +++ b/infer/src/bufferoverrun/bufferOverrunSemantics.ml @@ -22,51 +22,6 @@ let eval_const : Const.t -> Val.t = function Val.Itv.top -(* TODO *) - -let sizeof_ikind : Typ.ikind -> int = function - | Typ.IChar | Typ.ISChar | Typ.IUChar | Typ.IBool -> - 1 - | Typ.IInt | Typ.IUInt -> - 4 - | Typ.IShort | Typ.IUShort -> - 2 - | Typ.ILong | Typ.IULong -> - 4 - | Typ.ILongLong | Typ.IULongLong -> - 8 - | Typ.I128 | Typ.IU128 -> - 16 - - -let sizeof_fkind : Typ.fkind -> int = function - | Typ.FFloat -> - 4 - | Typ.FDouble | Typ.FLongDouble -> - 8 - - -(* NOTE: assume 32bit machine *) -let rec sizeof (typ: Typ.t) : int = - match typ.desc with - | Typ.Tint ikind -> - sizeof_ikind ikind - | Typ.Tfloat fkind -> - sizeof_fkind fkind - | Typ.Tvoid -> - 1 - | Typ.Tptr (_, _) -> - 4 - | Typ.Tstruct _ | Typ.TVar _ -> - 4 (* TODO *) - | Typ.Tarray {length= Some length; stride= Some stride} -> - IntLit.to_int_exn stride * IntLit.to_int_exn length - | Typ.Tarray {elt; length= Some length; stride= None} -> - sizeof elt * IntLit.to_int_exn length - | _ -> - 4 - - let rec must_alias : Exp.t -> Exp.t -> Mem.astate -> bool = fun e1 e2 m -> match (e1, e2) with @@ -202,8 +157,8 @@ let rec eval : Exp.t -> Mem.astate -> Val.t = eval_lindex e1 e2 mem | Exp.Sizeof {nbytes= Some size} -> Val.of_int size - | Exp.Sizeof {typ; nbytes= None} -> - Val.of_int (sizeof typ) + | Exp.Sizeof {nbytes= None} -> + Val.Itv.nat | Exp.Exn _ | Exp.Closure _ -> Val.Itv.top @@ -323,11 +278,9 @@ let get_allocsite : Typ.Procname.t -> node_hash:int -> inst_num:int -> dimension proc_name ^ "-" ^ node_num ^ "-" ^ inst_num ^ "-" ^ dimension |> Allocsite.make -let eval_array_alloc - : Allocsite.t -> Typ.t -> stride:int option -> offset:Itv.t -> size:Itv.t -> Val.t = - fun allocsite typ ~stride ~offset ~size -> - let int_stride = match stride with None -> sizeof typ | Some stride -> stride in - let stride = Itv.of_int int_stride in +let eval_array_alloc : Allocsite.t -> stride:int option -> offset:Itv.t -> size:Itv.t -> Val.t = + fun allocsite ~stride ~offset ~size -> + let stride = Option.value_map stride ~default:Itv.nat ~f:Itv.of_int in ArrayBlk.make allocsite ~offset ~size ~stride |> Val.of_array_blk ~allocsite diff --git a/infer/src/bufferoverrun/bufferOverrunUtils.ml b/infer/src/bufferoverrun/bufferOverrunUtils.ml index 959f80a01..efa9b60a1 100644 --- a/infer/src/bufferoverrun/bufferOverrunUtils.ml +++ b/infer/src/bufferoverrun/bufferOverrunUtils.ml @@ -43,7 +43,7 @@ module Exec = struct let size = Option.value_map ~default:Itv.top ~f:Itv.of_int_lit length in let allocsite = Sem.get_allocsite pname ~node_hash ~inst_num ~dimension in let arr = - Sem.eval_array_alloc allocsite typ ~stride ~offset ~size + Sem.eval_array_alloc allocsite ~stride ~offset ~size |> Dom.Val.add_trace_elem (Trace.ArrDecl location) in let mem = @@ -100,7 +100,7 @@ module Exec = struct let elem = Trace.SymAssign (loc, location) in let allocsite = Sem.get_allocsite pname ~node_hash ~inst_num ~dimension:alloc_num in let arr = - Sem.eval_array_alloc allocsite typ ~stride:None ~offset ~size |> Dom.Val.add_trace_elem elem + Sem.eval_array_alloc allocsite ~stride:None ~offset ~size |> Dom.Val.add_trace_elem elem in let mem = mem |> Dom.Mem.add_heap loc arr |> Dom.Mem.init_param_relation loc @@ -145,7 +145,7 @@ module Exec = struct let field_loc = PowLoc.append_field locs ~fn:field_name in let mem = match field_typ.Typ.desc with - | Tarray {elt= typ; length= Some length; stride} -> + | Tarray {length= Some length; stride} -> let length = Itv.of_int_lit length in let length = Option.value_map dyn_length ~default:length ~f:(fun dyn_length -> @@ -155,7 +155,7 @@ module Exec = struct let stride = Option.map stride ~f:IntLit.to_int_exn in let allocsite = Sem.get_allocsite pname ~node_hash ~inst_num ~dimension in let offset, size = (Itv.zero, length) in - let v = Sem.eval_array_alloc allocsite typ ~stride ~offset ~size in + let v = Sem.eval_array_alloc allocsite ~stride ~offset ~size in mem |> Dom.Mem.strong_update_heap field_loc v |> Dom.Mem.init_array_relation allocsite ~offset ~size ~size_exp_opt:None | _ ->