[inferbo] Add symbolic locations for parameters

Summary:
It adds symbolic locations for paramters, which will be used for fixing instantiations of parameters in the
following diffs.

Reviewed By: mbouaziz, jvillard

Differential Revision: D13214293

fbshipit-source-id: f016ea4c3

infer/src/bufferoverrun/absLoc.ml

@@ -13,6 +13,7 @@ module F = Format
 module Allocsite = struct
   type t =
     | Unknown
+    | Param of Symb.SymbolPath.partial
     | Known of
         { proc_name: string
         ; node_hash: int
@@ -25,17 +26,23 @@ module Allocsite = struct
     match (as1, as2) with
     | Unknown, _ | _, Unknown ->
         Boolean.Top
-    | Known {path= Some _}, Known {path= Some _} ->
+    | Param _, Param _ ->
-        (* Known with a path are parameters, parameters may alias *) Boolean.Top
+        (* parameters may alias *) Boolean.Top
+    | Known {path= Some p1}, Known {path= Some p2} ->
+        Boolean.of_bool (Symb.SymbolPath.equal_partial p1 p2)
     | Known {path= Some _}, Known {path= None} | Known {path= None}, Known {path= Some _} ->
         Boolean.False
     | Known {path= None}, Known {path= None} ->
         Boolean.of_bool ([%compare.equal: t] as1 as2)
+    | Known _, Param _ | Param _, Known _ ->
+        Boolean.False
 
 
   let pp fmt = function
     | Unknown ->
         F.fprintf fmt "Unknown"
+    | Param path ->
+        Symb.SymbolPath.pp_partial fmt path
     | Known {path= Some path} when Config.bo_debug < 1 ->
         Symb.SymbolPath.pp_partial fmt path
     | Known {proc_name; node_hash; inst_num; dimension; path} ->
@@ -43,7 +50,7 @@ module Allocsite = struct
         Option.iter path ~f:(fun path -> F.fprintf fmt "(%a)" Symb.SymbolPath.pp_partial path)
 
 
-  let is_pretty = function Known {path= Some _} -> true | _ -> false
+  let is_pretty = function Param _ | Known {path= Some _} -> true | _ -> false
 
   let to_string x = F.asprintf "%a" pp x
 
@@ -58,9 +65,11 @@ module Allocsite = struct
     Known {proc_name= Typ.Procname.to_string proc_name; node_hash; inst_num; dimension; path}
 
 
+  let make_param path = Param path
+
   let unknown = Unknown
 
-  let get_path = function Unknown -> None | Known {path} -> path
+  let get_path = function Unknown -> None | Param path -> Some path | Known {path} -> path
 end
 
 module Loc = struct

infer/src/bufferoverrun/bufferOverrunChecker.ml

@@ -279,15 +279,13 @@ module Init = struct
       -> Location.t
       -> Loc.t
       -> Typ.typ
-      -> inst_num:int
       -> new_sym_num:Counter.t
       -> Dom.Mem.t
       -> Dom.Mem.t =
-   fun pname symbol_table path tenv integer_type_widths ~node_hash location loc typ ~inst_num
+   fun pname symbol_table path tenv integer_type_widths ~node_hash location loc typ ~new_sym_num
-       ~new_sym_num mem ->
+       mem ->
     let max_depth = 2 in
-    let new_alloc_num = Counter.make 1 in
+    let rec decl_sym_val pname path tenv location ~depth ~may_last_field loc typ mem =
-    let rec decl_sym_val pname path tenv ~node_hash location ~depth ~may_last_field loc typ mem =
       if depth > max_depth then mem
       else
         let depth = depth + 1 in
@@ -304,16 +302,16 @@ module Init = struct
           | {desc= Typ.Tarray {elt}} ->
               BoUtils.Exec.decl_sym_arr
                 ~decl_sym_val:(decl_sym_val ~may_last_field:false)
-                Symb.SymbolPath.Deref_ArrayIndex pname symbol_table path tenv ~node_hash location
+                Symb.SymbolPath.Deref_ArrayIndex pname symbol_table path tenv location ~depth loc
-                ~depth loc elt ~inst_num ~new_sym_num ~new_alloc_num mem
+                elt ~new_sym_num mem
           | _ ->
               BoUtils.Exec.decl_sym_java_ptr
                 ~decl_sym_val:(decl_sym_val ~may_last_field:false)
-                pname path tenv ~node_hash location ~depth loc typ ~inst_num ~new_alloc_num mem )
+                pname path tenv location ~depth loc typ mem )
         | Typ.Tptr (typ, _) ->
             BoUtils.Exec.decl_sym_arr ~decl_sym_val:(decl_sym_val ~may_last_field)
-              Symb.SymbolPath.Deref_CPointer pname symbol_table path tenv ~node_hash location
+              Symb.SymbolPath.Deref_CPointer pname symbol_table path tenv location ~depth loc typ
-              ~depth loc typ ~inst_num ~new_sym_num ~new_alloc_num mem
+              ~new_sym_num mem
         | Typ.Tarray {elt; length; stride} ->
             let size =
               match length with
@@ -326,8 +324,8 @@ module Init = struct
             let stride = Option.map ~f:IntLit.to_int_exn stride in
             BoUtils.Exec.decl_sym_arr
               ~decl_sym_val:(decl_sym_val ~may_last_field:false)
-              Symb.SymbolPath.Deref_ArrayIndex pname symbol_table path tenv ~node_hash location
+              Symb.SymbolPath.Deref_ArrayIndex pname symbol_table path tenv location ~depth loc elt
-              ~depth loc elt ~offset ?size ?stride ~inst_num ~new_sym_num ~new_alloc_num mem
+              ~offset ?size ?stride ~new_sym_num mem
         | Typ.Tstruct typename -> (
           match Models.TypName.dispatch tenv typename with
           | Some {Models.declare_symbolic} ->
@@ -335,13 +333,12 @@ module Init = struct
                 Models.mk_model_env pname node_hash location tenv integer_type_widths symbol_table
               in
               declare_symbolic ~decl_sym_val:(decl_sym_val ~may_last_field) path model_env ~depth
-                loc ~inst_num ~new_sym_num ~new_alloc_num mem
+                loc ~new_sym_num mem
           | None ->
               let decl_fld ~may_last_field mem (fn, typ, _) =
                 let loc_fld = Loc.append_field loc ~fn in
                 let path = Itv.SymbolPath.field path fn in
-                decl_sym_val pname path tenv ~node_hash location ~depth loc_fld typ ~may_last_field
+                decl_sym_val pname path tenv location ~depth loc_fld typ ~may_last_field mem
-                  mem
               in
               let decl_flds str =
                 IList.fold_last ~f:(decl_fld ~may_last_field:false)
@@ -356,7 +353,7 @@ module Init = struct
                 location ;
             mem
     in
-    decl_sym_val pname path tenv ~node_hash location ~depth:0 ~may_last_field:true loc typ mem
+    decl_sym_val pname path tenv location ~depth:0 ~may_last_field:true loc typ mem
 
 
   let declare_symbolic_parameters :
@@ -366,22 +363,18 @@ module Init = struct
       -> node_hash:int
       -> Location.t
       -> Itv.SymbolTable.t
-      -> inst_num:int
       -> (Pvar.t * Typ.t) list
       -> Dom.Mem.t
       -> Dom.Mem.t =
-   fun pname tenv integer_type_widths ~node_hash location symbol_table ~inst_num formals mem ->
+   fun pname tenv integer_type_widths ~node_hash location symbol_table formals mem ->
     let new_sym_num = Counter.make 0 in
-    let add_formal (mem, inst_num) (pvar, typ) =
+    let add_formal mem (pvar, typ) =
       let loc = Loc.of_pvar pvar in
       let path = Itv.SymbolPath.of_pvar pvar in
-      let mem =
+      declare_symbolic_val pname symbol_table path tenv integer_type_widths ~node_hash location loc
-        declare_symbolic_val pname symbol_table path tenv integer_type_widths ~node_hash location
+        typ ~new_sym_num mem
-          loc typ ~inst_num ~new_sym_num mem
-      in
-      (mem, inst_num + 1)
     in
-    List.fold ~f:add_formal ~init:(mem, inst_num) formals |> fst
+    List.fold ~f:add_formal ~init:mem formals
 
 
   let initial_state {ProcData.pdesc; tenv; extras= {symbol_table; integer_type_widths}} start_node
@@ -416,10 +409,10 @@ module Init = struct
         ~dimension:1 mem
     in
     let mem = Dom.Mem.init in
-    let mem, inst_num = List.fold ~f:try_decl_local ~init:(mem, 1) (Procdesc.get_locals pdesc) in
+    let mem, _ = List.fold ~f:try_decl_local ~init:(mem, 1) (Procdesc.get_locals pdesc) in
     let formals = Sem.get_formals pdesc in
     declare_symbolic_parameters pname tenv integer_type_widths ~node_hash location symbol_table
-      ~inst_num formals mem
+      formals mem
 end
 
 module Report = struct

infer/src/bufferoverrun/bufferOverrunModels.ml

@@ -50,9 +50,7 @@ type declare_symbolic_fun =
   -> model_env
   -> depth:int
   -> Loc.t
-  -> inst_num:int
   -> new_sym_num:Counter.t
-  -> new_alloc_num:Counter.t
   -> Dom.Mem.t
   -> Dom.Mem.t
 
@@ -316,13 +314,12 @@ module StdArray = struct
       BoUtils.Exec.decl_local_array ~decl_local pname ~node_hash location loc typ ~length ~inst_num
         ~represents_multiple_values ~dimension mem
     in
-    let declare_symbolic ~decl_sym_val path {pname; tenv; node_hash; location; symbol_table} ~depth
+    let declare_symbolic ~decl_sym_val path {pname; tenv; location; symbol_table} ~depth loc
-        loc ~inst_num ~new_sym_num ~new_alloc_num mem =
+        ~new_sym_num mem =
       let offset = Itv.zero in
       let size = Itv.of_int64 length in
       BoUtils.Exec.decl_sym_arr ~decl_sym_val Symb.SymbolPath.Deref_ArrayIndex pname symbol_table
-        path tenv ~node_hash location ~depth loc typ ~offset ~size ~inst_num ~new_sym_num
+        path tenv location ~depth loc typ ~offset ~size ~new_sym_num mem
-        ~new_alloc_num mem
     in
     {declare_local; declare_symbolic}
 
@@ -362,8 +359,7 @@ module StdArray = struct
         ~dimension:_ mem =
       (no_model "local" pname location mem, inst_num)
     in
-    let declare_symbolic ~decl_sym_val:_ _path {pname; location} ~depth:_ _loc ~inst_num:_
+    let declare_symbolic ~decl_sym_val:_ _path {pname; location} ~depth:_ _loc ~new_sym_num:_ mem =
-        ~new_sym_num:_ ~new_alloc_num:_ mem =
       no_model "symbolic" pname location mem
     in
     {declare_local; declare_symbolic}
@@ -381,7 +377,7 @@ module Collection = struct
         ~represents_multiple_values ~dimension mem
     in
     let declare_symbolic ~decl_sym_val:_ path {pname; location; symbol_table} ~depth:_ loc
-        ~inst_num:_ ~new_sym_num ~new_alloc_num:_ mem =
+        ~new_sym_num mem =
       BoUtils.Exec.decl_sym_collection pname symbol_table path location loc ~new_sym_num mem
     in
     {declare_local; declare_symbolic}

infer/src/bufferoverrun/bufferOverrunUtils.ml

@@ -116,7 +116,6 @@ module Exec = struct
        Typ.Procname.t
     -> Itv.SymbolPath.partial
     -> Tenv.t
-    -> node_hash:int
     -> Location.t
     -> depth:int
     -> Loc.t
@@ -131,7 +130,6 @@ module Exec = struct
       -> Itv.SymbolTable.t
       -> Itv.SymbolPath.partial
       -> Tenv.t
-      -> node_hash:int
       -> Location.t
       -> depth:int
       -> Loc.t
@@ -139,13 +137,11 @@ module Exec = struct
       -> ?offset:Itv.t
       -> ?size:Itv.t
       -> ?stride:int
-      -> inst_num:int
       -> new_sym_num:Counter.t
-      -> new_alloc_num:Counter.t
       -> Dom.Mem.t
       -> Dom.Mem.t =
-   fun ~decl_sym_val deref_kind pname symbol_table path tenv ~node_hash location ~depth loc typ
+   fun ~decl_sym_val deref_kind pname symbol_table path tenv location ~depth loc typ ?offset ?size
-       ?offset ?size ?stride ~inst_num ~new_sym_num ~new_alloc_num mem ->
+       ?stride ~new_sym_num mem ->
     let offset =
       IOption.value_default_f offset ~f:(fun () ->
           Itv.make_sym pname symbol_table (Itv.SymbolPath.offset path) new_sym_num )
@@ -156,10 +152,7 @@ module Exec = struct
       )
     in
     let deref_path = Itv.SymbolPath.deref ~deref_kind path in
-    let allocsite =
+    let allocsite = Allocsite.make_param deref_path in
-      let alloc_num = Counter.next new_alloc_num in
-      Allocsite.make pname ~node_hash ~inst_num ~dimension:alloc_num ~path:(Some deref_path)
-    in
     let mem =
       let arr =
         let traces = Trace.(Set.singleton location (Parameter loc)) in
@@ -171,7 +164,7 @@ module Exec = struct
       |> Dom.Mem.init_array_relation allocsite ~offset ~size ~size_exp_opt:None
     in
     let deref_loc = Loc.of_allocsite allocsite in
-    decl_sym_val pname deref_path tenv ~node_hash location ~depth deref_loc typ mem
+    decl_sym_val pname deref_path tenv location ~depth deref_loc typ mem
 
 
   let decl_sym_java_ptr :
@@ -179,21 +172,14 @@ module Exec = struct
       -> Typ.Procname.t
       -> Itv.SymbolPath.partial
       -> Tenv.t
-      -> node_hash:int
       -> Location.t
       -> depth:int
       -> Loc.t
       -> Typ.t
-      -> inst_num:int
-      -> new_alloc_num:Counter.t
       -> Dom.Mem.t
       -> Dom.Mem.t =
-   fun ~decl_sym_val pname path tenv ~node_hash location ~depth loc typ ~inst_num ~new_alloc_num
+   fun ~decl_sym_val pname path tenv location ~depth loc typ mem ->
-       mem ->
+    let allocsite = Allocsite.make_param path in
-    let alloc_num = Counter.next new_alloc_num in
-    let allocsite =
-      Allocsite.make pname ~node_hash ~inst_num ~dimension:alloc_num ~path:(Some path)
-    in
     let alloc_loc = Loc.of_allocsite allocsite in
     let v =
       let represents_multiple_values = Itv.SymbolPath.represents_multiple_values path in
@@ -202,7 +188,7 @@ module Exec = struct
       |> Dom.Val.sets_represents_multiple_values ~represents_multiple_values
     in
     let mem = Dom.Mem.add_heap loc v mem in
-    decl_sym_val pname path tenv ~node_hash location ~depth alloc_loc typ mem
+    decl_sym_val pname path tenv location ~depth alloc_loc typ mem
 
 
   let decl_sym_collection :

infer/src/bufferoverrun/bufferOverrunUtils.mli

@@ -58,7 +58,6 @@ module Exec : sig
        Typ.Procname.t
     -> Itv.SymbolPath.partial
     -> Tenv.t
-    -> node_hash:int
     -> Location.t
     -> depth:int
     -> Loc.t
@@ -73,7 +72,6 @@ module Exec : sig
     -> Itv.SymbolTable.t
     -> Itv.SymbolPath.partial
     -> Tenv.t
-    -> node_hash:int
     -> Location.t
     -> depth:int
     -> Loc.t
@@ -81,9 +79,7 @@ module Exec : sig
     -> ?offset:Itv.t
     -> ?size:Itv.t
     -> ?stride:int
-    -> inst_num:int
     -> new_sym_num:Counter.t
-    -> new_alloc_num:Counter.t
     -> Dom.Mem.t
     -> Dom.Mem.t
 
@@ -92,13 +88,10 @@ module Exec : sig
     -> Typ.Procname.t
     -> Itv.SymbolPath.partial
     -> Tenv.t
-    -> node_hash:int
     -> Location.t
     -> depth:int
     -> Loc.t
     -> Typ.t
-    -> inst_num:int
-    -> new_alloc_num:Counter.t
     -> Dom.Mem.t
     -> Dom.Mem.t
 

infer/src/bufferoverrun/symb.ml

@@ -28,6 +28,8 @@ module SymbolPath = struct
 
   let equal = [%compare.equal: t]
 
+  let equal_partial = [%compare.equal: partial]
+
   let of_pvar pvar = Pvar pvar
 
   let field p fn = Field (fn, p)

infer/src/bufferoverrun/symb.mli

@@ -25,6 +25,8 @@ module SymbolPath : sig
 
   type t = private Normal of partial | Offset of partial | Length of partial
 
+  val equal_partial : partial -> partial -> bool
+
   val pp_mark : markup:bool -> F.formatter -> t -> unit
 
   val pp_partial : F.formatter -> partial -> unit