From 00390d367a4a0f1cb13cc48941119b2cccfd92e4 Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Mon, 19 Jun 2017 23:46:03 -0700 Subject: [PATCH] [inferbo] Refactor new symbol generation Summary: `Dom.Val.make_sym` takes `new_sym_num : unit -> int` as an argument instead of `sym_num : int`. Reviewed By: mbouaziz Differential Revision: D5042836 fbshipit-source-id: 955e708 --- .../src/bufferoverrun/bufferOverrunChecker.ml | 26 +++++++------------ .../src/bufferoverrun/bufferOverrunDomain.ml | 6 ++--- infer/src/bufferoverrun/itv.ml | 20 +++++++++----- 3 files changed, 25 insertions(+), 27 deletions(-) diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.ml b/infer/src/bufferoverrun/bufferOverrunChecker.ml index eff41355f..936a6f6f3 100644 --- a/infer/src/bufferoverrun/bufferOverrunChecker.ml +++ b/infer/src/bufferoverrun/bufferOverrunChecker.ml @@ -162,25 +162,21 @@ struct get_num let declare_symbolic_val - : Typ.Procname.t -> Tenv.t -> CFG.node -> Loc.t -> Typ.t -> inst_num:int - -> new_sym_num: (unit -> int) -> Domain.t -> Domain.t + : Typ.Procname.t -> Tenv.t -> CFG.node -> Loc.t -> Typ.typ + -> inst_num:int -> new_sym_num: (unit -> int) -> Domain.t -> Domain.t = fun pname tenv node loc typ ~inst_num ~new_sym_num mem -> let max_depth = 2 in let new_alloc_num = counter_gen 1 in - let rec decl_sym_fld ~depth loc typ mem = + let rec decl_sym_val ~depth loc typ mem = if depth > max_depth then mem else let depth = depth + 1 in match typ.Typ.desc with | Typ.Tint ikind -> let unsigned = Typ.ikind_is_unsigned ikind in - let sym_num = new_sym_num () in - let _ = new_sym_num () in - let v = Dom.Val.make_sym ~unsigned pname sym_num in + let v = Dom.Val.make_sym ~unsigned pname new_sym_num in Dom.Mem.add_heap loc v mem | Typ.Tfloat _ -> - let sym_num = new_sym_num () in - let _ = new_sym_num () in - let v = Dom.Val.make_sym pname sym_num in + let v = Dom.Val.make_sym pname new_sym_num in Dom.Mem.add_heap loc v mem | Typ.Tptr (typ, _) -> decl_sym_arr ~depth loc typ mem @@ -191,7 +187,7 @@ struct | Typ.Tstruct typename -> let decl_fld mem (fn, typ, _) = let loc_fld = Loc.append_field loc fn in - decl_sym_fld ~depth loc_fld typ mem + decl_sym_val ~depth loc_fld typ mem in let decl_flds str = List.fold ~f:decl_fld ~init:mem str.Typ.Struct.fields @@ -211,11 +207,7 @@ struct | Some x -> x | None -> default_f () in - let itv_make_sym () = - let sym_num = new_sym_num () in - let _ = new_sym_num () in - Itv.make_sym pname sym_num - in + let itv_make_sym () = Itv.make_sym pname new_sym_num in let offset = option_value opt_offset itv_make_sym in let size = option_value opt_size itv_make_sym in let alloc_num = new_alloc_num () in @@ -226,9 +218,9 @@ struct let deref_loc = Loc.of_allocsite (Sem.get_allocsite pname node inst_num alloc_num) in - decl_sym_fld ~depth deref_loc typ mem + decl_sym_val ~depth deref_loc typ mem in - decl_sym_fld ~depth:0 loc typ mem + decl_sym_val ~depth:0 loc typ mem let declare_symbolic_parameter : Procdesc.t -> Tenv.t -> CFG.node -> int -> Dom.Mem.astate -> Dom.Mem.astate diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml index 098113c86..fd5e63519 100644 --- a/infer/src/bufferoverrun/bufferOverrunDomain.ml +++ b/infer/src/bufferoverrun/bufferOverrunDomain.ml @@ -274,9 +274,9 @@ struct let modify_itv : Itv.t -> t -> t = fun i x -> { x with itv = i } - let make_sym : ?unsigned:bool -> Typ.Procname.t -> int -> t - = fun ?(unsigned=false) pname i -> - { bot with itv = Itv.make_sym ~unsigned pname i } + let make_sym : ?unsigned:bool -> Typ.Procname.t -> (unit -> int) -> t + = fun ?(unsigned=false) pname new_sym_num -> + { bot with itv = Itv.make_sym ~unsigned pname new_sym_num } let unknown_bit : t -> t = fun x -> { x with itv = Itv.top } diff --git a/infer/src/bufferoverrun/itv.ml b/infer/src/bufferoverrun/itv.ml index f82a3d529..de52718c5 100644 --- a/infer/src/bufferoverrun/itv.ml +++ b/infer/src/bufferoverrun/itv.ml @@ -547,21 +547,27 @@ struct let of_int n = of_bound (Bound.of_int n) + let of_int_lit : IntLit.t -> t option + = fun s -> + match IntLit.to_int s with + | size -> Some (of_int size) + | exception _ -> None + let get_new_sym : Typ.Procname.t -> t = fun pname -> let lower = Bound.of_sym (SymLinear.get_new pname) in let upper = Bound.of_sym (SymLinear.get_new pname) in (lower, upper) - let make_sym : unsigned:bool -> Typ.Procname.t -> int -> t - = fun ~unsigned pname i -> + let make_sym : unsigned:bool -> Typ.Procname.t -> (unit -> int) -> t + = fun ~unsigned pname new_sym_num -> let lower = if unsigned then - Bound.MinMax (Bound.Max, 0, Symbol.make pname i) + Bound.MinMax (Bound.Max, 0, Symbol.make pname (new_sym_num ())) else - Bound.of_sym (SymLinear.make pname i) + Bound.of_sym (SymLinear.make pname (new_sym_num ())) in - let upper = Bound.of_sym (SymLinear.make pname (i+1)) in + let upper = Bound.of_sym (SymLinear.make pname (new_sym_num ())) in (lower, upper) let m1_255 = (Bound.minus_one, Bound._255) @@ -970,8 +976,8 @@ let minus : t -> t -> t let get_new_sym : Typ.Procname.t -> t = fun pname -> NonBottom (ItvPure.get_new_sym pname) -let make_sym : ?unsigned:bool -> Typ.Procname.t -> int -> t - = fun ?(unsigned=false) pname i -> NonBottom (ItvPure.make_sym ~unsigned pname i) +let make_sym : ?unsigned:bool -> Typ.Procname.t -> (unit -> int) -> t + = fun ?(unsigned=false) pname new_sym_num -> NonBottom (ItvPure.make_sym ~unsigned pname new_sym_num) let neg : t -> t = lift1 ItvPure.neg