From 5331648b91a81a1755484e19f7489f603e387137 Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Mon, 12 Aug 2019 07:03:15 -0700 Subject: [PATCH] [inferbo] Revise vector model Summary: We do not need to keep the elements type of vector in the field. Reviewed By: ezgicicek Differential Revision: D16761451 fbshipit-source-id: 6d5384662 --- .../src/bufferoverrun/bufferOverrunDomain.ml | 10 +- infer/src/bufferoverrun/bufferOverrunField.ml | 14 ++- .../src/bufferoverrun/bufferOverrunModels.ml | 101 +++++++++--------- .../bufferoverrun/bufferOverrunOndemandEnv.ml | 4 +- .../bufferoverrun/bufferOverrunTypModels.ml | 6 +- infer/src/bufferoverrun/bufferOverrunUtils.ml | 2 +- 6 files changed, 71 insertions(+), 66 deletions(-) diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml index b34319c05..c174339f2 100644 --- a/infer/src/bufferoverrun/bufferOverrunDomain.ml +++ b/infer/src/bufferoverrun/bufferOverrunDomain.ml @@ -477,12 +477,10 @@ module Val = struct let deref_path = SPath.deref ~deref_kind path in let size = Itv.of_int_lit length in ptr_to_c_array_alloc deref_path size - | Some (CppStdVector {element_typ}) -> - let deref_path = - SPath.field path (BufferOverrunField.cpp_vector_elem ~classname:typename element_typ) - in - let size = Itv.of_length_path ~is_void:false path in - ptr_to_c_array_alloc deref_path size + | Some CppStdVector -> + let l = Loc.of_path (SPath.deref ~deref_kind:Deref_CPointer path) in + let traces = traces_of_loc l in + of_loc ~traces l | Some JavaCollection -> let deref_path = SPath.deref ~deref_kind:Deref_ArrayIndex path in let l = Loc.of_path deref_path in diff --git a/infer/src/bufferoverrun/bufferOverrunField.ml b/infer/src/bufferoverrun/bufferOverrunField.ml index f6afeeff7..2dfc274dd 100644 --- a/infer/src/bufferoverrun/bufferOverrunField.ml +++ b/infer/src/bufferoverrun/bufferOverrunField.ml @@ -6,6 +6,7 @@ *) open! IStd module F = Format +module L = Logging (** If fn is empty, prints [pp_lhs_alone lhs] @@ -54,7 +55,18 @@ let c_strlen () = let cpp_vector_elem_str = "cpp.vector_elem" -let cpp_vector_elem ~classname elt_typ = +let cpp_vector_elem ~vec_typ ~elt_typ = + let classname = + match vec_typ.Typ.desc with + | Typ.Tptr (vec_typ, _) -> ( + match Typ.name vec_typ with + | None -> + L.(die InternalError) "Unknown class name of vector `%a`" (Typ.pp_full Pp.text) vec_typ + | Some t -> + t ) + | _ -> + L.(die InternalError) "First parameter of constructor should be a pointer." + in let desc = Typ.Tptr (elt_typ, Typ.Pk_pointer) in mk ~cpp_classname:classname cpp_vector_elem_str {Typ.desc; quals= Typ.mk_type_quals ()} diff --git a/infer/src/bufferoverrun/bufferOverrunModels.ml b/infer/src/bufferoverrun/bufferOverrunModels.ml index 4d52220c8..99eb838df 100644 --- a/infer/src/bufferoverrun/bufferOverrunModels.ml +++ b/infer/src/bufferoverrun/bufferOverrunModels.ml @@ -648,20 +648,17 @@ module StdBasicString = struct end module StdVector = struct - let deref_of vec_exp mem = - Dom.Val.get_all_locs (Dom.Mem.find_set (Sem.eval_locs vec_exp mem) mem) - - - let get_classname vec_typ = - match vec_typ.Typ.desc with - | Typ.Tptr (vec_typ, _) -> ( - match Typ.name vec_typ with - | None -> - L.(die InternalError) "Unknown class name of vector `%a`" (Typ.pp_full Pp.text) vec_typ - | Some t -> - t ) - | _ -> - L.(die InternalError) "First parameter of constructor should be a pointer." + let append_field loc ~vec_typ ~elt_typ = + Loc.append_field loc ~fn:(BufferOverrunField.cpp_vector_elem ~vec_typ ~elt_typ) + + + let append_fields locs ~vec_typ ~elt_typ = + PowLoc.append_field locs ~fn:(BufferOverrunField.cpp_vector_elem ~vec_typ ~elt_typ) + + + let deref_of {integer_type_widths} elt_typ (vec_exp, vec_typ) mem = + Dom.Val.get_all_locs (Sem.eval_arr integer_type_widths vec_exp mem) + |> append_fields ~vec_typ ~elt_typ (* The (3) constructor in https://en.cppreference.com/w/cpp/container/vector/vector *) @@ -671,12 +668,10 @@ module StdVector = struct mem = let mem = malloc_exec model_env ~ret mem in let vec_locs = Sem.eval_locs vec_exp mem in - let classname = get_classname vec_typ in let deref_of_vec = Allocsite.make pname ~node_hash ~inst_num:1 ~dimension:1 ~path:None ~represents_multiple_values:false |> Loc.of_allocsite - |> Loc.append_field ~fn:(BufferOverrunField.cpp_vector_elem ~classname elt_typ) in let array_v = Sem.eval integer_type_widths (Exp.Var id) mem @@ -684,7 +679,7 @@ module StdVector = struct in mem |> Dom.Mem.update_mem vec_locs (Dom.Val.of_loc deref_of_vec) - |> Dom.Mem.add_heap deref_of_vec array_v + |> Dom.Mem.add_heap (append_field deref_of_vec ~vec_typ ~elt_typ) array_v in {exec; check} @@ -694,16 +689,13 @@ module StdVector = struct (* The (5) constructor in https://en.cppreference.com/w/cpp/container/vector/vector *) let constructor_copy elt_typ (vec_exp, vec_typ) src_exp = - let exec {integer_type_widths} ~ret:_ mem = + let exec ({integer_type_widths} as model_env) ~ret:_ mem = let vec_locs, traces = let v = Sem.eval integer_type_widths vec_exp mem in (Dom.Val.get_all_locs v, Dom.Val.get_traces v) in - let deref_of_vec = - let classname = get_classname vec_typ in - PowLoc.append_field vec_locs ~fn:(BufferOverrunField.cpp_vector_elem ~classname elt_typ) - in - let deref_of_src = deref_of src_exp mem in + let deref_of_vec = append_fields vec_locs ~vec_typ ~elt_typ in + let deref_of_src = deref_of model_env elt_typ (src_exp, vec_typ) mem in mem |> Dom.Mem.update_mem vec_locs (Dom.Val.of_pow_loc ~traces deref_of_vec) |> Dom.Mem.update_mem deref_of_vec (Dom.Mem.find_set deref_of_src mem) @@ -711,17 +703,17 @@ module StdVector = struct {exec; check= no_check} - let at vec_exp index_exp = - let exec {pname; location} ~ret:(id, _) mem = + let at elt_typ vec_arg index_exp = + let exec ({pname; location} as model_env) ~ret:(id, _) mem = let array_v = - let locs = deref_of vec_exp mem in + let locs = deref_of model_env elt_typ vec_arg mem in if PowLoc.is_bot locs then Dom.Val.unknown_from ~callee_pname:(Some pname) ~location else Dom.Mem.find_set locs mem in Dom.Mem.add_stack (Loc.of_id id) array_v mem - and check {location; integer_type_widths} mem cond_set = + and check ({location; integer_type_widths} as model_env) mem cond_set = let idx = Sem.eval integer_type_widths index_exp mem in - let arr = Dom.Mem.find_set (deref_of vec_exp mem) mem in + let arr = Dom.Mem.find_set (deref_of model_env elt_typ vec_arg mem) mem in let relation = Dom.Mem.get_relation mem in let latest_prune = Dom.Mem.get_latest_prune mem in BoUtils.Check.array_access ~arr ~idx ~idx_sym_exp:None ~relation ~is_plus:true @@ -730,17 +722,14 @@ module StdVector = struct {exec; check} - let get_size vec_exp mem = eval_array_locs_length (deref_of vec_exp mem) mem - - let set_size {location} vec_exp new_size mem = - let locs = deref_of vec_exp mem in + let set_size {location} locs new_size mem = Dom.Mem.transform_mem locs mem ~f:(fun v -> Dom.Val.set_array_length location ~length:new_size v ) - let empty vec_exp = - let exec _ ~ret:(id, _) mem = - let deref_of_vec = deref_of vec_exp mem in + let empty elt_typ vec_arg = + let exec model_env ~ret:(id, _) mem = + let deref_of_vec = deref_of model_env elt_typ vec_arg mem in let array_v = Dom.Mem.find_set deref_of_vec mem in let mem = array_empty_exec id array_v mem in match PowLoc.is_singleton_or_more deref_of_vec with @@ -752,31 +741,33 @@ module StdVector = struct {exec; check= no_check} - let data vec_exp = - let exec _ ~ret:(id, _) mem = - let arr = Dom.Mem.find_set (deref_of vec_exp mem) mem in + let data elt_typ vec_arg = + let exec model_env ~ret:(id, _) mem = + let arr = Dom.Mem.find_set (deref_of model_env elt_typ vec_arg mem) mem in model_by_value arr id mem in {exec; check= no_check} - let push_back vec_exp elt_exp = + let push_back elt_typ vec_arg elt_exp = let exec model_env ~ret:_ mem = + let arr_locs = deref_of model_env elt_typ vec_arg mem in let mem = - let new_size = Dom.Val.plus_a (get_size vec_exp mem) (Dom.Val.of_int 1) in - set_size model_env vec_exp new_size mem + let new_size = Dom.Val.plus_a (eval_array_locs_length arr_locs mem) (Dom.Val.of_int 1) in + set_size model_env arr_locs new_size mem in - let elt_locs = Dom.Val.get_all_locs (Dom.Mem.find_set (deref_of vec_exp mem) mem) in + let elt_locs = Dom.Val.get_all_locs (Dom.Mem.find_set arr_locs mem) in let elt_v = Dom.Mem.find_set (Sem.eval_locs elt_exp mem) mem in Dom.Mem.update_mem elt_locs elt_v mem in {exec; check= no_check} - let size vec_exp = - let exec _ ~ret:(id, _) mem = - let mem = Dom.Mem.add_stack (Loc.of_id id) (get_size vec_exp mem) mem in - match PowLoc.is_singleton_or_more (deref_of vec_exp mem) with + let size elt_typ vec_arg = + let exec model_env ~ret:(id, _) mem = + let arr_locs = deref_of model_env elt_typ vec_arg mem in + let mem = Dom.Mem.add_stack (Loc.of_id id) (eval_array_locs_length arr_locs mem) mem in + match PowLoc.is_singleton_or_more arr_locs with | IContainer.Singleton loc -> Dom.Mem.load_size_alias id loc mem | IContainer.Empty | IContainer.More -> @@ -1149,14 +1140,18 @@ module Call = struct $ capt_arg_of_typ (-"std" &:: "vector") $+ capt_exp_of_typ (-"std" &:: "vector") $+? any_arg $--> StdVector.constructor_copy - ; -"std" &:: "vector" < any_typ &+ any_typ >:: "operator[]" $ capt_exp $+ capt_exp - $--> StdVector.at - ; -"std" &:: "vector" < any_typ &+ any_typ >:: "empty" $ capt_exp $--> StdVector.empty - ; -"std" &:: "vector" < any_typ &+ any_typ >:: "data" $ capt_exp $--> StdVector.data - ; -"std" &:: "vector" < any_typ &+ any_typ >:: "push_back" $ capt_exp $+ capt_exp - $--> StdVector.push_back + ; -"std" &:: "vector" + < capt_typ `T + &+ any_typ >:: "operator[]" + $ capt_arg_of_typ (-"std" &:: "vector") + $+ capt_exp $--> StdVector.at + ; -"std" &:: "vector" < capt_typ `T &+ any_typ >:: "empty" $ capt_arg $--> StdVector.empty + ; -"std" &:: "vector" < capt_typ `T &+ any_typ >:: "data" $ capt_arg $--> StdVector.data + ; -"std" &:: "vector" + < capt_typ `T + &+ any_typ >:: "push_back" $ capt_arg $+ capt_exp $--> StdVector.push_back ; -"std" &:: "vector" < any_typ &+ any_typ >:: "reserve" $ any_arg $+ any_arg $--> no_model - ; -"std" &:: "vector" < any_typ &+ any_typ >:: "size" $ capt_exp $--> StdVector.size + ; -"std" &:: "vector" < capt_typ `T &+ any_typ >:: "size" $ capt_arg $--> StdVector.size ; +PatternMatch.implements_collection &:: "" <>$ capt_var_exn $+ capt_exp_of_typ (+PatternMatch.implements_collection) diff --git a/infer/src/bufferoverrun/bufferOverrunOndemandEnv.ml b/infer/src/bufferoverrun/bufferOverrunOndemandEnv.ml index 2a797385f..649b2bdd4 100644 --- a/infer/src/bufferoverrun/bufferOverrunOndemandEnv.ml +++ b/infer/src/bufferoverrun/bufferOverrunOndemandEnv.ml @@ -42,8 +42,8 @@ let mk pdesc = match BufferOverrunTypModels.dispatch tenv typename with | Some (CArray {element_typ}) -> Some element_typ - | Some (CppStdVector {element_typ}) -> - Some (Typ.mk (Typ.Tptr (element_typ, Typ.Pk_pointer))) + | Some CppStdVector -> + Some (Typ.mk (Typ.Tptr (Typ.void, Typ.Pk_pointer))) | Some _ -> L.internal_error "Deref of non-array modeled type `%a`" Typ.Name.pp typename ; None diff --git a/infer/src/bufferoverrun/bufferOverrunTypModels.ml b/infer/src/bufferoverrun/bufferOverrunTypModels.ml index 5a23003bc..414b37690 100644 --- a/infer/src/bufferoverrun/bufferOverrunTypModels.ml +++ b/infer/src/bufferoverrun/bufferOverrunTypModels.ml @@ -9,7 +9,7 @@ open! IStd type typ_model = | CArray of {element_typ: Typ.t; deref_kind: Symb.SymbolPath.deref_kind; length: IntLit.t} - | CppStdVector of {element_typ: Typ.t} + | CppStdVector | JavaCollection | JavaInteger @@ -17,7 +17,7 @@ let std_array element_typ length = CArray {element_typ; deref_kind= Symb.SymbolPath.Deref_ArrayIndex; length= IntLit.of_int64 length} -let std_vector element_typ = CppStdVector {element_typ} +let std_vector = CppStdVector (* Java's Collections are represented by their size. We don't care about the elements. - when they are constructed, we set the size to 0 @@ -34,7 +34,7 @@ let dispatch : (Tenv.t, typ_model) ProcnameDispatcher.TypName.dispatcher = let open ProcnameDispatcher.TypName in make_dispatcher [ -"std" &:: "array" < capt_typ `T &+ capt_int >--> std_array - ; -"std" &:: "vector" < capt_typ `T &+ any_typ >--> std_vector + ; -"std" &:: "vector" < any_typ &+ any_typ >--> std_vector ; +PatternMatch.implements_collection &::.*--> Java.collection ; +PatternMatch.implements_iterator &::.*--> Java.collection ; +PatternMatch.implements_lang "Integer" &::.*--> Java.integer diff --git a/infer/src/bufferoverrun/bufferOverrunUtils.ml b/infer/src/bufferoverrun/bufferOverrunUtils.ml index 1545feffa..3bb37d9fb 100644 --- a/infer/src/bufferoverrun/bufferOverrunUtils.ml +++ b/infer/src/bufferoverrun/bufferOverrunUtils.ml @@ -59,7 +59,7 @@ module Exec = struct | Some (CArray {element_typ; length}) -> decl_local_array model_env loc element_typ ~length:(Some length) ~inst_num ~represents_multiple_values ~dimension mem - | Some (CppStdVector _) | Some JavaCollection | Some JavaInteger | None -> + | Some CppStdVector | Some JavaCollection | Some JavaInteger | None -> (mem, inst_num) ) | _ -> (mem, inst_num)