From 828fa236d49ea4dc996ac75f6e97536958dc1423 Mon Sep 17 00:00:00 2001 From: Mehdi Bouaziz Date: Wed, 21 Nov 2018 15:48:33 -0800 Subject: [PATCH] [Inferbo] represents_multiple_values from path Summary: It removes the `represents_multiple_values` parameters when we can know them from `path` values. Depends on D12939124 Reviewed By: skcho Differential Revision: D12939130 fbshipit-source-id: 30ff768b2 --- .../src/bufferoverrun/bufferOverrunChecker.ml | 48 +++++++------------ .../src/bufferoverrun/bufferOverrunDomain.ml | 7 ++- .../src/bufferoverrun/bufferOverrunModels.ml | 20 ++++---- infer/src/bufferoverrun/bufferOverrunUtils.ml | 28 ++++------- .../src/bufferoverrun/bufferOverrunUtils.mli | 4 -- infer/src/bufferoverrun/symb.ml | 11 +++++ infer/src/bufferoverrun/symb.mli | 2 + 7 files changed, 52 insertions(+), 68 deletions(-) diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.ml b/infer/src/bufferoverrun/bufferOverrunChecker.ml index bc3a9f9b2..c75f7b99c 100644 --- a/infer/src/bufferoverrun/bufferOverrunChecker.ml +++ b/infer/src/bufferoverrun/bufferOverrunChecker.ml @@ -285,35 +285,27 @@ module Init = struct -> Typ.IntegerWidths.t -> node_hash:int -> Location.t - -> represents_multiple_values:bool -> 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 - ~represents_multiple_values loc typ ~inst_num ~new_sym_num mem -> + fun pname symbol_table path tenv integer_type_widths ~node_hash location loc typ ~inst_num + ~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 ~represents_multiple_values ~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 match typ.Typ.desc with | Typ.Tint ikind -> let unsigned = Typ.ikind_is_unsigned ikind in - let v = - Dom.Val.make_sym ~represents_multiple_values ~unsigned loc pname symbol_table path - new_sym_num location - in + let v = Dom.Val.make_sym ~unsigned loc pname symbol_table path new_sym_num location in mem |> Dom.Mem.add_heap loc v |> Dom.Mem.init_param_relation loc | Typ.Tfloat _ -> - let v = - Dom.Val.make_sym ~represents_multiple_values loc pname symbol_table path new_sym_num - location - in + let v = Dom.Val.make_sym loc pname symbol_table path new_sym_num location in mem |> Dom.Mem.add_heap loc v |> Dom.Mem.init_param_relation loc | Typ.Tptr (typ, _) when Language.curr_language_is Java -> ( match typ with @@ -321,17 +313,15 @@ module Init = struct BoUtils.Exec.decl_sym_arr ~decl_sym_val:(decl_sym_val ~may_last_field:false) Symb.SymbolPath.CSymArray_Array pname symbol_table path tenv ~node_hash location - ~represents_multiple_values ~depth loc elt ~inst_num ~new_sym_num ~new_alloc_num - mem + ~depth loc elt ~inst_num ~new_sym_num ~new_alloc_num mem | _ -> BoUtils.Exec.decl_sym_java_ptr ~decl_sym_val:(decl_sym_val ~may_last_field:false) - pname path tenv ~node_hash location ~represents_multiple_values ~depth loc typ - ~inst_num ~new_alloc_num mem ) + pname path tenv ~node_hash location ~depth loc typ ~inst_num ~new_alloc_num mem ) | Typ.Tptr (typ, _) -> BoUtils.Exec.decl_sym_arr ~decl_sym_val:(decl_sym_val ~may_last_field) Symb.SymbolPath.CSymArray_Pointer pname symbol_table path tenv ~node_hash location - ~represents_multiple_values ~depth loc typ ~inst_num ~new_sym_num ~new_alloc_num mem + ~depth loc typ ~inst_num ~new_sym_num ~new_alloc_num mem | Typ.Tarray {elt; length; stride} -> let size = match length with @@ -345,22 +335,21 @@ module Init = struct BoUtils.Exec.decl_sym_arr ~decl_sym_val:(decl_sym_val ~may_last_field:false) Symb.SymbolPath.CSymArray_Array pname symbol_table path tenv ~node_hash location - ~represents_multiple_values ~depth loc elt ~offset ?size ?stride ~inst_num - ~new_sym_num ~new_alloc_num mem + ~depth loc elt ~offset ?size ?stride ~inst_num ~new_sym_num ~new_alloc_num mem | Typ.Tstruct typename -> ( match Models.TypName.dispatch tenv typename with | Some {Models.declare_symbolic} -> let model_env = 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 - ~represents_multiple_values ~depth loc ~inst_num ~new_sym_num ~new_alloc_num mem + 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 | 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 ~represents_multiple_values ~depth - loc_fld typ ~may_last_field mem + decl_sym_val pname path tenv ~node_hash location ~depth loc_fld typ ~may_last_field + mem in let decl_flds str = IList.fold_last ~f:(decl_fld ~may_last_field:false) @@ -375,8 +364,7 @@ module Init = struct location ; mem in - decl_sym_val pname path tenv ~node_hash location ~represents_multiple_values ~depth:0 - ~may_last_field:true loc typ mem + decl_sym_val pname path tenv ~node_hash location ~depth:0 ~may_last_field:true loc typ mem let declare_symbolic_parameters : @@ -386,20 +374,18 @@ module Init = struct -> node_hash:int -> Location.t -> Itv.SymbolTable.t - -> represents_multiple_values:bool -> inst_num:int -> (Pvar.t * Typ.t) list -> Dom.Mem.astate -> Dom.Mem.astate = - fun pname tenv integer_type_widths ~node_hash location symbol_table ~represents_multiple_values - ~inst_num formals mem -> + fun pname tenv integer_type_widths ~node_hash location symbol_table ~inst_num formals mem -> let new_sym_num = Counter.make 0 in let add_formal (mem, inst_num) (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 - ~represents_multiple_values loc typ ~inst_num ~new_sym_num mem + loc typ ~inst_num ~new_sym_num mem in (mem, inst_num + 1) in @@ -441,7 +427,7 @@ module Init = struct let mem, inst_num = 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 - ~represents_multiple_values:false ~inst_num formals mem + ~inst_num formals mem end module Report = struct diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml index ceb9e2387..9bcf3de17 100644 --- a/infer/src/bufferoverrun/bufferOverrunDomain.ml +++ b/infer/src/bufferoverrun/bufferOverrunDomain.ml @@ -154,8 +154,7 @@ module Val = struct let modify_itv : Itv.t -> t -> t = fun i x -> {x with itv= i} let make_sym : - represents_multiple_values:bool - -> ?unsigned:bool + ?unsigned:bool -> Loc.t -> Typ.Procname.t -> Itv.SymbolTable.t @@ -163,8 +162,8 @@ module Val = struct -> Counter.t -> Location.t -> t = - fun ~represents_multiple_values ?(unsigned = false) loc pname symbol_table path new_sym_num - location -> + fun ?(unsigned = false) loc pname symbol_table path new_sym_num location -> + let represents_multiple_values = Itv.SymbolPath.represents_multiple_values path in { bot with itv= Itv.make_sym ~unsigned pname symbol_table (Itv.SymbolPath.normal path) new_sym_num ; sym= Relation.Sym.of_loc loc diff --git a/infer/src/bufferoverrun/bufferOverrunModels.ml b/infer/src/bufferoverrun/bufferOverrunModels.ml index 7fa5dd7b6..0ed5680fd 100644 --- a/infer/src/bufferoverrun/bufferOverrunModels.ml +++ b/infer/src/bufferoverrun/bufferOverrunModels.ml @@ -49,7 +49,6 @@ type declare_symbolic_fun = decl_sym_val:BoUtils.Exec.decl_sym_val -> Itv.SymbolPath.partial -> model_env - -> represents_multiple_values:bool -> depth:int -> Loc.t -> inst_num:int @@ -323,13 +322,13 @@ 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} - ~represents_multiple_values ~depth loc ~inst_num ~new_sym_num ~new_alloc_num mem = + 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 offset = Itv.zero in let size = Itv.of_int64 length in BoUtils.Exec.decl_sym_arr ~decl_sym_val Symb.SymbolPath.CSymArray_Array pname symbol_table - path tenv ~node_hash location ~represents_multiple_values ~depth loc typ ~offset ~size - ~inst_num ~new_sym_num ~new_alloc_num mem + path tenv ~node_hash location ~depth loc typ ~offset ~size ~inst_num ~new_sym_num + ~new_alloc_num mem in {declare_local; declare_symbolic} @@ -368,8 +367,8 @@ module StdArray = struct ~dimension:_ mem = (no_model "local" pname location mem, inst_num) in - let declare_symbolic ~decl_sym_val:_ _path {pname; location} ~represents_multiple_values:_ - ~depth:_ _loc ~inst_num:_ ~new_sym_num:_ ~new_alloc_num:_ mem = + let declare_symbolic ~decl_sym_val:_ _path {pname; location} ~depth:_ _loc ~inst_num:_ + ~new_sym_num:_ ~new_alloc_num:_ mem = no_model "symbolic" pname location mem in {declare_local; declare_symbolic} @@ -386,10 +385,9 @@ module Collection = struct BoUtils.Exec.decl_local_collection pname ~node_hash location loc ~inst_num ~represents_multiple_values ~dimension mem in - let declare_symbolic ~decl_sym_val:_ path {pname; location; symbol_table} - ~represents_multiple_values ~depth:_ loc ~inst_num:_ ~new_sym_num ~new_alloc_num:_ mem = - BoUtils.Exec.decl_sym_collection pname symbol_table path location ~represents_multiple_values - loc ~new_sym_num mem + let declare_symbolic ~decl_sym_val:_ path {pname; location; symbol_table} ~depth:_ loc + ~inst_num:_ ~new_sym_num ~new_alloc_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 0b0ec157b..335256a08 100644 --- a/infer/src/bufferoverrun/bufferOverrunUtils.ml +++ b/infer/src/bufferoverrun/bufferOverrunUtils.ml @@ -118,7 +118,6 @@ module Exec = struct -> Tenv.t -> node_hash:int -> Location.t - -> represents_multiple_values:bool -> depth:int -> Loc.t -> Typ.t @@ -134,7 +133,6 @@ module Exec = struct -> Tenv.t -> node_hash:int -> Location.t - -> represents_multiple_values:bool -> depth:int -> Loc.t -> Typ.t @@ -146,9 +144,8 @@ module Exec = struct -> new_alloc_num:Counter.t -> Dom.Mem.astate -> Dom.Mem.astate = - fun ~decl_sym_val array_kind pname symbol_table path tenv ~node_hash location - ~represents_multiple_values ~depth loc typ ?offset ?size ?stride ~inst_num ~new_sym_num - ~new_alloc_num mem -> + fun ~decl_sym_val array_kind pname symbol_table path tenv ~node_hash location ~depth loc typ + ?offset ?size ?stride ~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 offset = option_value offset (fun () -> @@ -167,6 +164,7 @@ module Exec = struct let mem = let arr = let elem = Trace.SymAssign (loc, location) in + let represents_multiple_values = Itv.SymbolPath.represents_multiple_values path in Dom.Val.of_array_alloc allocsite ~stride ~offset ~size |> Dom.Val.add_trace_elem elem |> Dom.Val.sets_represents_multiple_values ~represents_multiple_values @@ -175,12 +173,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 - let represents_multiple_values = - match array_kind with CSymArray_Array -> true | CSymArray_Pointer -> false - (* unsound but avoids many FPs for non-array pointers *) - in - decl_sym_val pname deref_path tenv ~node_hash location ~represents_multiple_values ~depth - deref_loc typ mem + decl_sym_val pname deref_path tenv ~node_hash location ~depth deref_loc typ mem let decl_sym_java_ptr : @@ -190,7 +183,6 @@ module Exec = struct -> Tenv.t -> node_hash:int -> Location.t - -> represents_multiple_values:bool -> depth:int -> Loc.t -> Typ.t @@ -198,8 +190,8 @@ module Exec = struct -> new_alloc_num:Counter.t -> Dom.Mem.astate -> Dom.Mem.astate = - fun ~decl_sym_val pname path tenv ~node_hash location ~represents_multiple_values ~depth loc typ - ~inst_num ~new_alloc_num mem -> + 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 elem = Trace.SymAssign (loc, location) in let allocsite = @@ -207,13 +199,13 @@ module Exec = struct in let alloc_loc = Loc.of_allocsite allocsite in let v = + let represents_multiple_values = Itv.SymbolPath.represents_multiple_values path in Dom.Val.of_pow_loc (PowLoc.singleton alloc_loc) |> Dom.Val.add_trace_elem elem |> 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 ~represents_multiple_values ~depth alloc_loc - typ mem + decl_sym_val pname path tenv ~node_hash location ~depth alloc_loc typ mem let decl_sym_collection : @@ -221,13 +213,13 @@ module Exec = struct -> Itv.SymbolTable.t -> Itv.SymbolPath.partial -> Location.t - -> represents_multiple_values:bool -> Loc.t -> new_sym_num:Counter.t -> Dom.Mem.astate -> Dom.Mem.astate = - fun pname symbol_table path location ~represents_multiple_values loc ~new_sym_num mem -> + fun pname symbol_table path location loc ~new_sym_num mem -> let size = + let represents_multiple_values = Itv.SymbolPath.represents_multiple_values path in Itv.make_sym ~unsigned:true pname symbol_table (Itv.SymbolPath.length path) new_sym_num |> Dom.Val.of_itv |> Dom.Val.add_trace_elem (Trace.SymAssign (loc, location)) diff --git a/infer/src/bufferoverrun/bufferOverrunUtils.mli b/infer/src/bufferoverrun/bufferOverrunUtils.mli index 496cbfd11..0c435a711 100644 --- a/infer/src/bufferoverrun/bufferOverrunUtils.mli +++ b/infer/src/bufferoverrun/bufferOverrunUtils.mli @@ -60,7 +60,6 @@ module Exec : sig -> Tenv.t -> node_hash:int -> Location.t - -> represents_multiple_values:bool -> depth:int -> Loc.t -> Typ.t @@ -76,7 +75,6 @@ module Exec : sig -> Tenv.t -> node_hash:int -> Location.t - -> represents_multiple_values:bool -> depth:int -> Loc.t -> Typ.t @@ -96,7 +94,6 @@ module Exec : sig -> Tenv.t -> node_hash:int -> Location.t - -> represents_multiple_values:bool -> depth:int -> Loc.t -> Typ.t @@ -110,7 +107,6 @@ module Exec : sig -> Itv.SymbolTable.t -> Itv.SymbolPath.partial -> Location.t - -> represents_multiple_values:bool -> Loc.t -> new_sym_num:Counter.t -> Dom.Mem.astate diff --git a/infer/src/bufferoverrun/symb.ml b/infer/src/bufferoverrun/symb.ml index f389da767..d2ce71f8d 100644 --- a/infer/src/bufferoverrun/symb.ml +++ b/infer/src/bufferoverrun/symb.ml @@ -56,6 +56,17 @@ module SymbolPath = struct F.fprintf fmt "%a.offset" pp_partial p | Length p -> F.fprintf fmt "%a.length" pp_partial p + + + let rec represents_multiple_values = function + | Pvar _ -> + false + | Index (CSymArray_Array, _) -> + true + | Index (CSymArray_Pointer, p) + (* unsound but avoids many FPs for non-array pointers *) + | Field (_, p) -> + represents_multiple_values p end module Symbol = struct diff --git a/infer/src/bufferoverrun/symb.mli b/infer/src/bufferoverrun/symb.mli index 579e09523..c9d176fd4 100644 --- a/infer/src/bufferoverrun/symb.mli +++ b/infer/src/bufferoverrun/symb.mli @@ -40,6 +40,8 @@ module SymbolPath : sig val offset : partial -> t val length : partial -> t + + val represents_multiple_values : partial -> bool end module Symbol : sig