[inferbo] Refactoring 2/8: abstract type for counter

Reviewed By: jvillard

Differential Revision: D7397118

fbshipit-source-id: aa5e625

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

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}
 

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}
 

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

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)
 

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