From e9cf5d33b35cf57d3a44a7e6012fb51af382d587 Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Thu, 8 Aug 2019 06:24:15 -0700 Subject: [PATCH] [inferbo] Add models of vector constructors Summary: It adds models of vector constructors. Depends on D16645624 Reviewed By: ezgicicek Differential Revision: D16687167 fbshipit-source-id: eac49df6d --- .../src/bufferoverrun/bufferOverrunModels.ml | 65 +++++++++++++++---- .../cpp/bufferoverrun/folly_split.cpp | 6 +- .../cpp/bufferoverrun/issues.exp | 20 +++--- .../cpp/bufferoverrun/vector.cpp | 14 ++-- 4 files changed, 73 insertions(+), 32 deletions(-) diff --git a/infer/src/bufferoverrun/bufferOverrunModels.ml b/infer/src/bufferoverrun/bufferOverrunModels.ml index 56f8fcecb..9cd85e47e 100644 --- a/infer/src/bufferoverrun/bufferOverrunModels.ml +++ b/infer/src/bufferoverrun/bufferOverrunModels.ml @@ -644,25 +644,26 @@ module StdBasicString = struct end module StdVector = struct + 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." + + (* The (3) constructor in https://en.cppreference.com/w/cpp/container/vector/vector *) - let constructor elt_typ (vec_exp, vec_typ) size_exp = + let constructor_size 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 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 @@ -680,6 +681,30 @@ module StdVector = struct {exec; check} + (* The (1) constructor in https://en.cppreference.com/w/cpp/container/vector/vector *) + let constructor_empty elt_typ vec = constructor_size elt_typ vec Exp.zero + + (* 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 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 = + Dom.Mem.find_set (Sem.eval_locs src_exp mem) mem |> Dom.Val.get_all_locs + 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) + in + {exec; check= no_check} + + let at vec_exp index_exp = let exec {pname; location} ~ret:(id, _) mem = let deref_of_vec = Dom.Mem.find_set (Sem.eval_locs vec_exp mem) mem in @@ -1058,7 +1083,19 @@ module Call = struct < capt_typ `T &+ any_typ >:: "vector" $ capt_arg_of_typ (-"std" &:: "vector") - $+ capt_exp $--> StdVector.constructor + $--> StdVector.constructor_empty + ; -"std" &:: "vector" + < capt_typ `T + &+ any_typ >:: "vector" + $ capt_arg_of_typ (-"std" &:: "vector") + $+ capt_exp_of_prim_typ (Typ.mk (Typ.Tint Typ.size_t)) + $+? any_arg $--> StdVector.constructor_size + ; -"std" &:: "vector" + < capt_typ `T + &+ any_typ >:: "vector" + $ 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 >:: "size" $ capt_exp $--> StdVector.size diff --git a/infer/tests/codetoanalyze/cpp/bufferoverrun/folly_split.cpp b/infer/tests/codetoanalyze/cpp/bufferoverrun/folly_split.cpp index dd5cc6656..a25292ecb 100644 --- a/infer/tests/codetoanalyze/cpp/bufferoverrun/folly_split.cpp +++ b/infer/tests/codetoanalyze/cpp/bufferoverrun/folly_split.cpp @@ -42,19 +42,19 @@ void splitTo(const Delim& delimiter, } // namespace folly namespace folly_split { -std::string do_not_ignore_empty_Good(const std::string& s) { +std::string FP_do_not_ignore_empty_Good(const std::string& s) { std::vector v; folly::split("delimiter", s, v); return v[0]; } -std::string do_not_ignore_empty2_Good(const std::string& s) { +std::string FP_do_not_ignore_empty2_Good(const std::string& s) { std::vector v; folly::split("delimiter", s, v, false); return v[0]; } -std::string FN_do_not_ignore_empty_Bad(const std::string& s) { +std::string do_not_ignore_empty_Bad(const std::string& s) { std::vector v; folly::split("delimiter", s, v, true); return v[0]; diff --git a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp index a42847e83..5f86ba137 100644 --- a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp @@ -44,6 +44,9 @@ 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_split.cpp, folly_split::FP_do_not_ignore_empty2_Good, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Assignment,Array access: Offset: 0 Size: 0] +codetoanalyze/cpp/bufferoverrun/folly_split.cpp, folly_split::FP_do_not_ignore_empty_Good, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Assignment,Array access: Offset: 0 Size: 0] +codetoanalyze/cpp/bufferoverrun/folly_split.cpp, folly_split::do_not_ignore_empty_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Assignment,Array access: Offset: 0 Size: 0] 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] @@ -104,20 +107,21 @@ codetoanalyze/cpp/bufferoverrun/std_string.cpp, to_string2_Good, 6, CONDITION_AL codetoanalyze/cpp/bufferoverrun/symb_arr.cpp, symb_arr_alloc::symb_arr_access_bad, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Parameter `this->h[*]`,Array access: Offset: 10 Size: 10] codetoanalyze/cpp/bufferoverrun/this.cpp, CThis::access_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Parameter `this->n`,,Parameter `this->n`,Array declaration,Array access: Offset: this->n + 1 Size: this->n + 1] codetoanalyze/cpp/bufferoverrun/trivial.cpp, trivial, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 10 Size: 10] -codetoanalyze/cpp/bufferoverrun/vector.cpp, FP_assert_Good, 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, FP_assert_Good_2, 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, FP_call_safe_access2_Good, 2, INFERBO_ALLOC_IS_ZERO, no_bucket, ERROR, [Array declaration,Assignment,Call,Parameter `*v->vector_elem`,Allocation: Length: 0 by call to `safe_access2` ] +codetoanalyze/cpp/bufferoverrun/vector.cpp, FP_call_safe_access4_Good, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array declaration,Assignment,Call,,Parameter `*v->vector_elem`,Array access: Offset: 0 Size: 0 by call to `safe_access4` ] +codetoanalyze/cpp/bufferoverrun/vector.cpp, FP_call_safe_access5_Good, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array declaration,Assignment,Call,,Parameter `*v->vector_elem`,Array access: Offset: 0 Size: 0 by call to `safe_access5` ] +codetoanalyze/cpp/bufferoverrun/vector.cpp, FP_call_safe_access_Good, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array declaration,Assignment,Call,,Parameter `*v->vector_elem`,Array access: Offset: 9 Size: 5 by call to `safe_access` ] 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_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_push_back_Good, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Assignment,Array access: Offset: 0 Size: 0] +codetoanalyze/cpp/bufferoverrun/vector.cpp, FP_reserve_Good, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Assignment,Array access: Offset: 0 Size: 0] +codetoanalyze/cpp/bufferoverrun/vector.cpp, FP_safe_access3_Good, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Assignment,Array access: Offset: 0 Size: 0] 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]] -codetoanalyze/cpp/bufferoverrun/vector.cpp, reserve_Bad, 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, push_back_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Assignment,Array access: Offset: 1 Size: 0] +codetoanalyze/cpp/bufferoverrun/vector.cpp, reserve_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Assignment,Array access: Offset: 0 Size: 0] codetoanalyze/cpp/bufferoverrun/vector.cpp, simple_size_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Assignment,,Array declaration,Assignment,Array access: Offset: 3 Size: 3] codetoanalyze/cpp/bufferoverrun/void_ptr.cpp, FP_call_casting_void_ptr_Ok, 2, BUFFER_OVERRUN_L5, no_bucket, ERROR, [Array declaration,Call,,Parameter `*p`,Assignment,Array access: Offset: 14 Size: 2 by call to `casting_void_ptr` ] diff --git a/infer/tests/codetoanalyze/cpp/bufferoverrun/vector.cpp b/infer/tests/codetoanalyze/cpp/bufferoverrun/vector.cpp index fc3b003ee..12d0809e2 100644 --- a/infer/tests/codetoanalyze/cpp/bufferoverrun/vector.cpp +++ b/infer/tests/codetoanalyze/cpp/bufferoverrun/vector.cpp @@ -64,7 +64,7 @@ void safe_access(std::vector v) { } } -void call_safe_access_Good() { +void FP_call_safe_access_Good() { std::vector v(5, 0); safe_access(v); } @@ -80,7 +80,7 @@ void safe_access2(std::vector v) { } } -void call_safe_access2_Good() { +void FP_call_safe_access2_Good() { std::vector v; safe_access2(v); } @@ -98,7 +98,7 @@ void safe_access4(std::vector v) { } } -void call_safe_access4_Good() { +void FP_call_safe_access4_Good() { std::vector v; safe_access4(v); } @@ -110,7 +110,7 @@ void safe_access5(std::vector v) { } } -void call_safe_access5_Good() { +void FP_call_safe_access5_Good() { std::vector v; safe_access5(v); } @@ -138,7 +138,7 @@ void data_Bad() { p[v[4]] = 1; } -void FP_assert_Good() { +void assert_Good() { std::vector v; for (int i = 0; i < 5; i++) { v.push_back(1); @@ -147,7 +147,7 @@ void FP_assert_Good() { v[4] = 1; } -void FP_assert_Good_2(int x) { +void assert_Good_2(int x) { std::vector v; for (int i = 0; i < 5; i++) { v.push_back(1); @@ -156,7 +156,7 @@ void FP_assert_Good_2(int x) { v[4] = 1; } -void assert_Bad() { +void FN_assert_Bad() { std::vector v; for (int i = 0; i < 5; i++) { v.push_back(1);