From 0086c3436482d958af6fec3132432889b326daab Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Tue, 27 Nov 2018 18:41:13 -0800 Subject: [PATCH] [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 | 17 +++++-- .../src/bufferoverrun/bufferOverrunChecker.ml | 47 ++++++++----------- .../src/bufferoverrun/bufferOverrunModels.ml | 14 ++---- infer/src/bufferoverrun/bufferOverrunUtils.ml | 28 +++-------- .../src/bufferoverrun/bufferOverrunUtils.mli | 7 --- infer/src/bufferoverrun/symb.ml | 2 + infer/src/bufferoverrun/symb.mli | 2 + 7 files changed, 49 insertions(+), 68 deletions(-) diff --git a/infer/src/bufferoverrun/absLoc.ml b/infer/src/bufferoverrun/absLoc.ml index 0d0aee49a..2d8ee62cd 100644 --- a/infer/src/bufferoverrun/absLoc.ml +++ b/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 _} -> - (* Known with a path are parameters, parameters may alias *) Boolean.Top + | Param _, Param _ -> + (* 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 diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.ml b/infer/src/bufferoverrun/bufferOverrunChecker.ml index e882b0eec..93d68d60e 100644 --- a/infer/src/bufferoverrun/bufferOverrunChecker.ml +++ b/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 - ~new_sym_num mem -> + fun pname symbol_table path tenv integer_type_widths ~node_hash location loc typ ~new_sym_num + mem -> let max_depth = 2 in - let new_alloc_num = Counter.make 1 in - let rec decl_sym_val pname path tenv ~node_hash location ~depth ~may_last_field loc typ mem = + let rec decl_sym_val pname path tenv 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 - ~depth loc elt ~inst_num ~new_sym_num ~new_alloc_num mem + Symb.SymbolPath.Deref_ArrayIndex pname symbol_table path tenv location ~depth loc + 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 - ~depth loc typ ~inst_num ~new_sym_num ~new_alloc_num mem + Symb.SymbolPath.Deref_CPointer pname symbol_table path tenv location ~depth loc typ + ~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 - ~depth loc elt ~offset ?size ?stride ~inst_num ~new_sym_num ~new_alloc_num mem + Symb.SymbolPath.Deref_ArrayIndex pname symbol_table path tenv location ~depth loc elt + ~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 - mem + decl_sym_val pname path tenv location ~depth loc_fld typ ~may_last_field 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 typ ~inst_num ~new_sym_num mem - in - (mem, inst_num + 1) + declare_symbolic_val pname symbol_table path tenv integer_type_widths ~node_hash location loc + typ ~new_sym_num mem 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 diff --git a/infer/src/bufferoverrun/bufferOverrunModels.ml b/infer/src/bufferoverrun/bufferOverrunModels.ml index 33029a00e..7f2abbf72 100644 --- a/infer/src/bufferoverrun/bufferOverrunModels.ml +++ b/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 - loc ~inst_num ~new_sym_num ~new_alloc_num mem = + let declare_symbolic ~decl_sym_val path {pname; tenv; location; symbol_table} ~depth loc + ~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 - ~new_alloc_num mem + path tenv location ~depth loc typ ~offset ~size ~new_sym_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:_ - ~new_sym_num:_ ~new_alloc_num:_ mem = + let declare_symbolic ~decl_sym_val:_ _path {pname; location} ~depth:_ _loc ~new_sym_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} diff --git a/infer/src/bufferoverrun/bufferOverrunUtils.ml b/infer/src/bufferoverrun/bufferOverrunUtils.ml index cfe2fc01e..9e092c572 100644 --- a/infer/src/bufferoverrun/bufferOverrunUtils.ml +++ b/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 - ?offset ?size ?stride ~inst_num ~new_sym_num ~new_alloc_num mem -> + fun ~decl_sym_val deref_kind pname symbol_table path tenv location ~depth loc typ ?offset ?size + ?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 alloc_num = Counter.next new_alloc_num in - Allocsite.make pname ~node_hash ~inst_num ~dimension:alloc_num ~path:(Some deref_path) - in + let allocsite = Allocsite.make_param 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 - mem -> - 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 + fun ~decl_sym_val pname path tenv location ~depth loc typ mem -> + let allocsite = Allocsite.make_param 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 : diff --git a/infer/src/bufferoverrun/bufferOverrunUtils.mli b/infer/src/bufferoverrun/bufferOverrunUtils.mli index e300dde79..fcf515e70 100644 --- a/infer/src/bufferoverrun/bufferOverrunUtils.mli +++ b/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 diff --git a/infer/src/bufferoverrun/symb.ml b/infer/src/bufferoverrun/symb.ml index 9e3c882de..5df9a81b9 100644 --- a/infer/src/bufferoverrun/symb.ml +++ b/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) diff --git a/infer/src/bufferoverrun/symb.mli b/infer/src/bufferoverrun/symb.mli index 92e6f1ba7..904beab8a 100644 --- a/infer/src/bufferoverrun/symb.mli +++ b/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