diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml index d72ee15a3..1955338cf 100644 --- a/infer/src/bufferoverrun/bufferOverrunDomain.ml +++ b/infer/src/bufferoverrun/bufferOverrunDomain.ml @@ -424,6 +424,12 @@ module Val = struct let trace = if Loc.is_global l then Trace.Global l else Trace.Parameter l in TraceSet.singleton location trace in + let ptr_to_c_array_alloc deref_path size = + let allocsite = Allocsite.make_symbol deref_path in + let offset = Itv.zero in + let traces = traces_of_loc (Loc.of_path deref_path) in + of_c_array_alloc allocsite ~stride:None ~offset ~size ~traces + in let is_java = Language.curr_language_is Java in L.d_printfln_escaped "Val.of_path %a : %a%s%s" SPath.pp_partial path (Typ.pp Pp.text) typ (if may_last_field then ", may_last_field" else "") @@ -457,7 +463,10 @@ module Val = struct | _ -> Itv.nat in - let offset = Itv.of_offset_path ~is_void:(Typ.is_pointer_to_void typ) path in + let offset = + if SPath.is_cpp_vector_elem path then Itv.zero + else Itv.of_offset_path ~is_void:(Typ.is_pointer_to_void typ) path + in let size = Itv.of_length_path ~is_void:(Typ.is_pointer_to_void typ) path in ArrayBlk.make_c allocsite ~stride ~offset ~size in @@ -466,12 +475,14 @@ module Val = struct match BufferOverrunTypModels.dispatch tenv typename with | Some (CArray {deref_kind; length}) -> let deref_path = SPath.deref ~deref_kind path in - let l = Loc.of_path deref_path in - let traces = traces_of_loc l in - let allocsite = Allocsite.make_symbol deref_path in - let offset = Itv.zero in let size = Itv.of_int_lit length in - of_c_array_alloc allocsite ~stride:None ~offset ~size ~traces + 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 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 b0f958357..f6afeeff7 100644 --- a/infer/src/bufferoverrun/bufferOverrunField.ml +++ b/infer/src/bufferoverrun/bufferOverrunField.ml @@ -30,9 +30,15 @@ let pp ~pp_lhs ~pp_lhs_alone ~sep f lhs fn = let mk, get_type = let classname = "__infer__" in let types = ref Typ.Fieldname.Map.empty in - let mk name typ = - let fullname = Format.sprintf "%s.%s" classname name in - let fieldname = Typ.Fieldname.Java.from_string fullname in + let mk ?cpp_classname name typ = + let fieldname = + match cpp_classname with + | None -> + let fullname = Format.sprintf "%s.%s" classname name in + Typ.Fieldname.Java.from_string fullname + | Some classname -> + Typ.Fieldname.Clang.from_class_name classname name + in types := Typ.Fieldname.Map.add fieldname typ !types ; fieldname in @@ -44,3 +50,14 @@ let java_collection_internal_array = mk "java.collection.$elements." Typ.(mk_arr let c_strlen () = if Language.curr_language_is Java then mk "length" Typ.uint else mk "c.strlen" Typ.uint + + +let cpp_vector_elem_str = "cpp.vector_elem" + +let cpp_vector_elem ~classname elt_typ = + 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 ()} + + +let is_cpp_vector_elem fn = + String.equal (Typ.Fieldname.to_simplified_string fn) cpp_vector_elem_str diff --git a/infer/src/bufferoverrun/bufferOverrunModels.ml b/infer/src/bufferoverrun/bufferOverrunModels.ml index a90e03679..8c701e8ba 100644 --- a/infer/src/bufferoverrun/bufferOverrunModels.ml +++ b/infer/src/bufferoverrun/bufferOverrunModels.ml @@ -645,16 +645,29 @@ end module StdVector = struct (* The (3) constructor in https://en.cppreference.com/w/cpp/container/vector/vector *) - let constructor vec_exp size_exp = + let constructor elt_typ (vec_exp, vec_typ) size_exp = let {exec= malloc_exec; check} = malloc ~can_be_zero:true size_exp in let exec ({pname; node_hash; integer_type_widths; location} as model_env) ~ret:((id, _) as ret) mem = let mem = malloc_exec model_env ~ret mem in let vec_locs = Sem.eval_locs vec_exp mem in + 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 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 @@ -1012,8 +1025,11 @@ module Call = struct $+ any_arg_of_typ (-"std" &:: "basic_string") $--> by_value Dom.Val.Itv.unknown_bool ; -"std" &:: "basic_string" &::.*--> no_model - ; -"std" &:: "vector" < any_typ &+ any_typ >:: "vector" $ capt_exp $+ capt_exp - $--> StdVector.constructor + ; -"std" &:: "vector" + < capt_typ `T + &+ any_typ >:: "vector" + $ capt_arg_of_typ (-"std" &:: "vector") + $+ capt_exp $--> StdVector.constructor ; -"std" &:: "vector" < any_typ &+ any_typ >:: "operator[]" $ capt_exp $+ capt_exp $--> StdVector.at ; -"std" &:: "vector" < any_typ &+ any_typ >:: "size" $ capt_exp $--> StdVector.size diff --git a/infer/src/bufferoverrun/bufferOverrunOndemandEnv.ml b/infer/src/bufferoverrun/bufferOverrunOndemandEnv.ml index d6224b287..2a797385f 100644 --- a/infer/src/bufferoverrun/bufferOverrunOndemandEnv.ml +++ b/infer/src/bufferoverrun/bufferOverrunOndemandEnv.ml @@ -42,6 +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 _ -> 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 1ab62bcdb..1d20afc16 100644 --- a/infer/src/bufferoverrun/bufferOverrunTypModels.ml +++ b/infer/src/bufferoverrun/bufferOverrunTypModels.ml @@ -9,12 +9,15 @@ 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} | JavaCollection 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} + (* 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 - each time we add an element, we increase the length of the array @@ -26,6 +29,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 ; +PatternMatch.implements_collection &::.*--> collection ; +PatternMatch.implements_iterator &::.*--> collection ; +PatternMatch.implements_org_json "JSONArray" &::.*--> collection ] diff --git a/infer/src/bufferoverrun/bufferOverrunUtils.ml b/infer/src/bufferoverrun/bufferOverrunUtils.ml index 07803ad89..e37725711 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 JavaCollection | None -> + | Some (CppStdVector _) | Some JavaCollection | None -> (mem, inst_num) ) | _ -> (mem, inst_num) diff --git a/infer/src/bufferoverrun/symb.ml b/infer/src/bufferoverrun/symb.ml index fc2df5597..fee65db24 100644 --- a/infer/src/bufferoverrun/symb.ml +++ b/infer/src/bufferoverrun/symb.ml @@ -232,6 +232,13 @@ module SymbolPath = struct is_void | Normal _ | Modeled _ -> false + + + let is_cpp_vector_elem = function + | Field (fn, _) -> + BufferOverrunField.is_cpp_vector_elem fn + | _ -> + false end module Symbol = struct diff --git a/infer/src/bufferoverrun/symb.mli b/infer/src/bufferoverrun/symb.mli index 83ca7bb2b..27d110083 100644 --- a/infer/src/bufferoverrun/symb.mli +++ b/infer/src/bufferoverrun/symb.mli @@ -87,6 +87,8 @@ module SymbolPath : sig val exists_str_partial : f:(string -> bool) -> partial -> bool val is_void_ptr_path : t -> bool + + val is_cpp_vector_elem : partial -> bool end module Symbol : sig diff --git a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp index 3c4a7bd61..a42847e83 100644 --- a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp @@ -44,8 +44,6 @@ codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp, call_condition codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp, call_conditional_minus_2_Bad, 2, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Call,,Parameter `size`,Binary operation: (0 - 1):unsigned32 by call to `conditional_minus` ] codetoanalyze/cpp/bufferoverrun/external.cpp, extern_bad, 5, BUFFER_OVERRUN_U5, no_bucket, ERROR, [,Unknown value from: lib,Assignment,Array access: Offset: [-oo, +oo] Size: [0, +oo]] codetoanalyze/cpp/bufferoverrun/external.cpp, extern_bad, 10, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 30 Size: 10] -codetoanalyze/cpp/bufferoverrun/folly_memory_UninitializedMemoryHacks.cpp, folly::resizeWithoutInitialization, 1, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here] -codetoanalyze/cpp/bufferoverrun/folly_memory_UninitializedMemoryHacks.cpp, folly::resizeWithoutInitialization, 1, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here] codetoanalyze/cpp/bufferoverrun/function_call.cpp, call_by_ref_bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Call,Assignment,,Array declaration,Array access: Offset: -1 Size: 10] codetoanalyze/cpp/bufferoverrun/function_call.cpp, call_loop_with_init_S_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Call,Parameter `length`,Assignment,,Array declaration,Array access: Offset: 10 Size: 10] codetoanalyze/cpp/bufferoverrun/realloc.cpp, realloc_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Assignment,,Array declaration,Assignment,Array access: Offset: 5 Size: 5] @@ -62,8 +60,11 @@ codetoanalyze/cpp/bufferoverrun/relation.cpp, call2_plus_params_Bad, 0, BUFFER_O codetoanalyze/cpp/bufferoverrun/remove_temps.cpp, C::foo_Bad, 1, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here] codetoanalyze/cpp/bufferoverrun/remove_temps.cpp, C::foo_Bad, 6, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 10 Size: 5] codetoanalyze/cpp/bufferoverrun/remove_temps.cpp, C::goo, 1, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here] +codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM::fB_FP, 0, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [,Parameter `*o`,Call,Parameter `*k`,Call,Parameter `*k`,Assignment,Assignment,Binary operation: ([-oo, +oo] + 1):unsigned64] codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM::lI_FP, 2, BUFFER_OVERRUN_U5, no_bucket, ERROR, [,Unknown value from: std::unique_ptr,std::default_delete>>::operator->,Array access: Offset: [-oo, +oo] Size: [0, +oo]] +codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM::lI_FP, 2, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [,Call,Parameter `*o`,Call,Parameter `*k`,Call,Parameter `*k`,Assignment,Assignment,Assignment,Assignment,Binary operation: ([-oo, +oo] - 1):signed32] codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM::uI, 0, BUFFER_OVERRUN_U5, no_bucket, ERROR, [,Unknown value from: std::unique_ptr,std::default_delete>>::operator->,Array access: Offset: [-oo, +oo] Size: [0, +oo]] +codetoanalyze/cpp/bufferoverrun/repro1.cpp, am_Good_FP, 5, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Call,Assignment,Assignment,Call,Parameter `t->bI`,Call,Assignment,Call,,Parameter `bi`,Binary operation: ([-oo, +oo] - 1):signed32 by call to `ral_good` ] codetoanalyze/cpp/bufferoverrun/simple_vector.cpp, my_vector_oob_Bad, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [Parameter `v->_size`,Call,,Parameter `i`,,Parameter `this->_size`,Array declaration,Assignment,Array access: Offset: v->_size Size: v->_size by call to `int_vector::access_at` ] codetoanalyze/cpp/bufferoverrun/std_array.cpp, array_iter1_Bad, 5, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 10 Size: 5] codetoanalyze/cpp/bufferoverrun/std_array.cpp, array_iter2_Bad, 5, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 10 Size: 5] @@ -108,13 +109,12 @@ codetoanalyze/cpp/bufferoverrun/vector.cpp, FP_assert_Good_2, 6, BUFFER_OVERRUN_ codetoanalyze/cpp/bufferoverrun/vector.cpp, FP_data_Good, 3, BUFFER_OVERRUN_U5, no_bucket, ERROR, [,Unknown value from: std::vector>::data,Assignment,Array access: Offset: [-oo, +oo] (⇐ [-oo, +oo] + 4) Size: [0, +oo]] codetoanalyze/cpp/bufferoverrun/vector.cpp, FP_push_back_Good, 3, BUFFER_OVERRUN_U5, no_bucket, ERROR, [,Unknown value from: std::vector>::operator[],Array access: Offset: [-oo, +oo] Size: [0, +oo]] codetoanalyze/cpp/bufferoverrun/vector.cpp, FP_reserve_Good, 4, BUFFER_OVERRUN_U5, no_bucket, ERROR, [,Unknown value from: std::vector>::operator[],Array access: Offset: [-oo, +oo] Size: [0, +oo]] -codetoanalyze/cpp/bufferoverrun/vector.cpp, FP_safe_access2, 6, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here] -codetoanalyze/cpp/bufferoverrun/vector.cpp, FP_safe_access2, 6, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here] codetoanalyze/cpp/bufferoverrun/vector.cpp, FP_safe_access3_Good, 3, BUFFER_OVERRUN_U5, no_bucket, ERROR, [,Unknown value from: std::vector>::operator[],Array access: Offset: [-oo, +oo] Size: [0, +oo]] codetoanalyze/cpp/bufferoverrun/vector.cpp, FP_safe_access6, 2, BUFFER_OVERRUN_U5, no_bucket, ERROR, [,Unknown value from: std::vector>::empty,,Array declaration,Assignment,Array access: Offset: [-oo, +oo] Size: 2] codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Bad, 6, BUFFER_OVERRUN_U5, no_bucket, ERROR, [,Unknown value from: std::vector>::operator[],Array access: Offset: [-oo, +oo] Size: [0, +oo]] codetoanalyze/cpp/bufferoverrun/vector.cpp, constructor_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Assignment,Array access: Offset: 3 Size: 1] codetoanalyze/cpp/bufferoverrun/vector.cpp, data_Bad, 4, BUFFER_OVERRUN_U5, no_bucket, ERROR, [,Unknown value from: std::vector>::data,Assignment,Array access: Offset: [-oo, +oo] (⇐ [-oo, +oo] + [-oo, +oo]) Size: [0, +oo]] +codetoanalyze/cpp/bufferoverrun/vector.cpp, out_of_bound_Bad, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [,Parameter `*v->vector_elem`,Assignment,,Parameter `*v->vector_elem`,Array access: Offset: v->vector_elem.length Size: v->vector_elem.length] codetoanalyze/cpp/bufferoverrun/vector.cpp, precise_subst_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array declaration,Call,Parameter `*init`,Assignment,Call,Parameter `*__param_0->a`,Assignment,Call,,Parameter `count`,Call,Parameter `idx`,Assignment,Array access: Offset: -1 Size: 10 by call to `access_minus_one` ] codetoanalyze/cpp/bufferoverrun/vector.cpp, precise_subst_Good_FP, 3, BUFFER_OVERRUN_L3, no_bucket, ERROR, [Array declaration,Call,Parameter `*init`,Assignment,Call,Parameter `*__param_0->a`,Assignment,Call,,Parameter `count`,Call,Parameter `idx`,Assignment,Array access: Offset: [-1, 0] Size: 10 by call to `access_minus_one` ] codetoanalyze/cpp/bufferoverrun/vector.cpp, push_back_Bad, 3, BUFFER_OVERRUN_U5, no_bucket, ERROR, [,Unknown value from: std::vector>::operator[],Array access: Offset: [-oo, +oo] Size: [0, +oo]] diff --git a/infer/tests/codetoanalyze/cpp/bufferoverrun/repro1.cpp b/infer/tests/codetoanalyze/cpp/bufferoverrun/repro1.cpp index bdc7b543e..36c23dad2 100644 --- a/infer/tests/codetoanalyze/cpp/bufferoverrun/repro1.cpp +++ b/infer/tests/codetoanalyze/cpp/bufferoverrun/repro1.cpp @@ -74,7 +74,7 @@ struct LM { void l(lt& t, const lo& o) { lI_FP(t, o); } void tL(lt& t, const lo& o) { lI_FP(t, o); } void u(lt& t, const lo& o) { - ASSERT(fB(o) == t.bI); + ASSERT(fB_FP(o) == t.bI); if (t.bI == kBN) { return; } @@ -83,9 +83,9 @@ struct LM { } private: - BI fB(const lo& o) { return (BI)th((const void*)&o) % b.size() + 1; } + BI fB_FP(const lo& o) { return (BI)th((const void*)&o) % b.size() + 1; } void lI_FP(lt& t, const lo& o) { - auto bi = fB(o); + auto bi = fB_FP(o); auto r = b[bi - 1]->lO(o); if (r != TLOR::S) { t.bI = kBN; @@ -133,7 +133,7 @@ struct arh { ft i1; }; -static void am_Good(im* it) { +static void am_Good_FP(im* it) { const arh* ch = (const arh*)it->gKPC(); const ai a = aft(ch->i1); lt at; diff --git a/infer/tests/codetoanalyze/cpp/bufferoverrun/vector.cpp b/infer/tests/codetoanalyze/cpp/bufferoverrun/vector.cpp index 030355a27..fc3b003ee 100644 --- a/infer/tests/codetoanalyze/cpp/bufferoverrun/vector.cpp +++ b/infer/tests/codetoanalyze/cpp/bufferoverrun/vector.cpp @@ -8,7 +8,7 @@ #include #include -void FN_out_of_bound_Bad(std::vector v) { +void out_of_bound_Bad(std::vector v) { unsigned int n = v.size(); v[n] = 1; } @@ -69,7 +69,7 @@ void call_safe_access_Good() { safe_access(v); } -void FP_safe_access2(std::vector v) { +void safe_access2(std::vector v) { if (v.empty()) { return; } @@ -82,7 +82,7 @@ void FP_safe_access2(std::vector v) { void call_safe_access2_Good() { std::vector v; - FP_safe_access2(v); + safe_access2(v); } void FP_safe_access3_Good() {