From 90b5600c8f77dfcf322e6201a79870bee6e2842b Mon Sep 17 00:00:00 2001 From: Mehdi Bouaziz Date: Mon, 26 Mar 2018 05:49:04 -0700 Subject: [PATCH] [inferbo] Refactoring 2/8: abstract type for counter Reviewed By: jvillard Differential Revision: D7397118 fbshipit-source-id: aa5e625 --- .../src/bufferoverrun/bufferOverrunChecker.ml | 6 ++--- .../src/bufferoverrun/bufferOverrunDomain.ml | 2 +- .../src/bufferoverrun/bufferOverrunModels.ml | 3 +-- infer/src/bufferoverrun/bufferOverrunUtils.ml | 24 +++++------------- infer/src/bufferoverrun/itv.ml | 25 ++++++++++++++++--- infer/src/bufferoverrun/itv.mli | 10 +++++++- 6 files changed, 41 insertions(+), 29 deletions(-) diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.ml b/infer/src/bufferoverrun/bufferOverrunChecker.ml index 7b045a085..5a27c1c4c 100644 --- a/infer/src/bufferoverrun/bufferOverrunChecker.ml +++ b/infer/src/bufferoverrun/bufferOverrunChecker.ml @@ -39,10 +39,10 @@ module TransferFunctions (CFG : ProcCfg.S) = struct let declare_symbolic_val : Typ.Procname.t -> Tenv.t -> CFG.node -> Location.t -> Loc.t -> Typ.typ -> inst_num:int - -> new_sym_num:(unit -> int) -> Domain.t -> Domain.t = + -> new_sym_num:Itv.Counter.t -> Domain.t -> Domain.t = fun pname tenv node location loc typ ~inst_num ~new_sym_num mem -> let max_depth = 2 in - let new_alloc_num = BoUtils.counter_gen 1 in + let new_alloc_num = Itv.Counter.make 1 in let rec decl_sym_val pname tenv node location ~depth ~may_last_field loc typ mem = if depth > max_depth then mem else @@ -108,7 +108,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct : Typ.Procname.t -> Tenv.t -> CFG.node -> Location.t -> inst_num:int -> (Pvar.t * Typ.t) list -> Dom.Mem.astate -> Dom.Mem.astate = fun pname tenv node location ~inst_num formals mem -> - let new_sym_num = BoUtils.counter_gen 0 in + let new_sym_num = Itv.Counter.make 0 in let add_formal (mem, inst_num) (pvar, typ) = let loc = Loc.of_pvar pvar in let mem = declare_symbolic_val pname tenv node location loc typ ~inst_num ~new_sym_num mem in diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml index e29d276c7..5b9f40c5d 100644 --- a/infer/src/bufferoverrun/bufferOverrunDomain.ml +++ b/infer/src/bufferoverrun/bufferOverrunDomain.ml @@ -106,7 +106,7 @@ module Val = struct let modify_itv : Itv.t -> t -> t = fun i x -> {x with itv= i} - let make_sym : ?unsigned:bool -> Typ.Procname.t -> (unit -> int) -> t = + let make_sym : ?unsigned:bool -> Typ.Procname.t -> Itv.Counter.t -> t = fun ?(unsigned= false) pname new_sym_num -> {bot with itv= Itv.make_sym ~unsigned pname new_sym_num} diff --git a/infer/src/bufferoverrun/bufferOverrunModels.ml b/infer/src/bufferoverrun/bufferOverrunModels.ml index a1cd1151f..7cbb5a060 100644 --- a/infer/src/bufferoverrun/bufferOverrunModels.ml +++ b/infer/src/bufferoverrun/bufferOverrunModels.ml @@ -41,8 +41,7 @@ module Make (BoUtils : BufferOverrunUtils.S) = struct type declare_symbolic_fun = decl_sym_val:BoUtils.Exec.decl_sym_val -> model_env -> depth:int -> Loc.t -> inst_num:int - -> new_sym_num:BoUtils.counter -> new_alloc_num:BoUtils.counter -> Dom.Mem.astate - -> Dom.Mem.astate + -> new_sym_num:Itv.Counter.t -> new_alloc_num:Itv.Counter.t -> Dom.Mem.astate -> Dom.Mem.astate type typ_model = {declare_local: declare_local_fun; declare_symbolic: declare_symbolic_fun} diff --git a/infer/src/bufferoverrun/bufferOverrunUtils.ml b/infer/src/bufferoverrun/bufferOverrunUtils.ml index 498cc512b..ba2b3a72d 100644 --- a/infer/src/bufferoverrun/bufferOverrunUtils.ml +++ b/infer/src/bufferoverrun/bufferOverrunUtils.ml @@ -21,8 +21,6 @@ module type S = sig module Sem : module type of BufferOverrunSemantics.Make (CFG) - type counter = unit -> int - module Exec : sig val load_val : Ident.t -> Dom.Val.astate -> Dom.Mem.astate -> Dom.Mem.astate @@ -41,8 +39,9 @@ module type S = sig val decl_sym_arr : decl_sym_val:decl_sym_val -> Typ.Procname.t -> Tenv.t -> CFG.node -> Location.t -> depth:int - -> Loc.t -> Typ.t -> ?offset:Itv.t -> ?size:Itv.t -> inst_num:int -> new_sym_num:counter - -> new_alloc_num:counter -> Dom.Mem.astate -> Dom.Mem.astate + -> Loc.t -> Typ.t -> ?offset:Itv.t -> ?size:Itv.t -> inst_num:int + -> new_sym_num:Itv.Counter.t -> new_alloc_num:Itv.Counter.t -> Dom.Mem.astate + -> Dom.Mem.astate val init_array_fields : Tenv.t -> Typ.Procname.t -> CFG.node -> Typ.t -> PowLoc.t -> ?dyn_length:Exp.t @@ -62,18 +61,6 @@ module Make (CFG : ProcCfg.S) = struct module CFG = CFG module Sem = BufferOverrunSemantics.Make (CFG) - type counter = unit -> int - - let counter_gen init : counter = - let num_ref = ref init in - let get_num () = - let v = !num_ref in - num_ref := v + 1 ; - v - in - get_num - - module Exec = struct let load_val id val_ mem = let locs = val_ |> Dom.Val.get_all_locs in @@ -115,14 +102,15 @@ module Make (CFG : ProcCfg.S) = struct let decl_sym_arr : decl_sym_val:decl_sym_val -> Typ.Procname.t -> Tenv.t -> CFG.node -> Location.t -> depth:int -> Loc.t -> Typ.t -> ?offset:Itv.t -> ?size:Itv.t -> inst_num:int - -> new_sym_num:counter -> new_alloc_num:counter -> Dom.Mem.astate -> Dom.Mem.astate = + -> new_sym_num:Itv.Counter.t -> new_alloc_num:Itv.Counter.t -> Dom.Mem.astate + -> Dom.Mem.astate = fun ~decl_sym_val pname tenv node location ~depth loc typ ?offset ?size ~inst_num ~new_sym_num ~new_alloc_num mem -> let option_value opt_x default_f = match opt_x with Some x -> x | None -> default_f () in let itv_make_sym () = Itv.make_sym pname new_sym_num in let offset = option_value offset itv_make_sym in let size = option_value size itv_make_sym in - let alloc_num = new_alloc_num () in + let alloc_num = Itv.Counter.next new_alloc_num in let elem = Trace.SymAssign (loc, location) in let arr = Sem.eval_array_alloc pname node typ offset size inst_num alloc_num diff --git a/infer/src/bufferoverrun/itv.ml b/infer/src/bufferoverrun/itv.ml index 88c63c193..5bb9dfb9f 100644 --- a/infer/src/bufferoverrun/itv.ml +++ b/infer/src/bufferoverrun/itv.ml @@ -15,6 +15,23 @@ open! AbstractDomain.Types module F = Format module L = Logging +module Counter = struct + type t = unit -> int + + let make : int -> t = + fun init -> + let num_ref = ref init in + let get_num () = + let v = !num_ref in + num_ref := v + 1 ; + v + in + get_num + + + let next : t -> int = fun counter -> counter () +end + exception Not_one_symbol module Symbol = struct @@ -925,10 +942,10 @@ module ItvPure = struct let of_int n = of_bound (Bound.of_int n) - let make_sym : unsigned:bool -> Typ.Procname.t -> (unit -> int) -> t = + let make_sym : unsigned:bool -> Typ.Procname.t -> Counter.t -> t = fun ~unsigned pname new_sym_num -> - let lower = Bound.of_sym (SymLinear.make ~unsigned pname (new_sym_num ())) in - let upper = Bound.of_sym (SymLinear.make ~unsigned pname (new_sym_num ())) in + let lower = Bound.of_sym (SymLinear.make ~unsigned pname (Counter.next new_sym_num)) in + let upper = Bound.of_sym (SymLinear.make ~unsigned pname (Counter.next new_sym_num)) in (lower, upper) @@ -1345,7 +1362,7 @@ let plus : t -> t -> t = lift2 ItvPure.plus let minus : t -> t -> t = lift2 ItvPure.minus -let make_sym : ?unsigned:bool -> Typ.Procname.t -> (unit -> int) -> t = +let make_sym : ?unsigned:bool -> Typ.Procname.t -> Counter.t -> t = fun ?(unsigned= false) pname new_sym_num -> NonBottom (ItvPure.make_sym ~unsigned pname new_sym_num) diff --git a/infer/src/bufferoverrun/itv.mli b/infer/src/bufferoverrun/itv.mli index 97abd72e1..885ed79c7 100644 --- a/infer/src/bufferoverrun/itv.mli +++ b/infer/src/bufferoverrun/itv.mli @@ -11,6 +11,14 @@ open! IStd open! AbstractDomain.Types module F = Format +module Counter : sig + type t + + val make : int -> t + + val next : t -> int +end + module Symbol : sig type t end @@ -165,7 +173,7 @@ val of_int_lit : IntLit.t -> t val of_int64 : Int64.t -> t -val make_sym : ?unsigned:bool -> Typ.Procname.t -> (unit -> int) -> t +val make_sym : ?unsigned:bool -> Typ.Procname.t -> Counter.t -> t val lb : t -> Bound.t