[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

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

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 }

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