From fcfb6cc361f275bb675e45b459c634e7106dec2b Mon Sep 17 00:00:00 2001 From: Daiva Naudziuniene Date: Tue, 11 Dec 2018 05:23:06 -0800 Subject: [PATCH] [pulse] Model more std::vector functions that can invalid references to elements Summary: Model more `std::vector` functions that can potentially invalidate references to vector's elements (https://en.cppreference.com/w/cpp/container/vector). Reviewed By: mbouaziz Differential Revision: D13399161 fbshipit-source-id: 95cf2cae6 --- infer/src/checkers/PulseInvalidation.ml | 23 ++++++++++- infer/src/checkers/PulseInvalidation.mli | 11 +++++- infer/src/checkers/PulseModels.ml | 19 +++++++++- .../tests/codetoanalyze/cpp/pulse/issues.exp | 4 ++ .../tests/codetoanalyze/cpp/pulse/vector.cpp | 38 +++++++++++++++++++ 5 files changed, 91 insertions(+), 4 deletions(-) diff --git a/infer/src/checkers/PulseInvalidation.ml b/infer/src/checkers/PulseInvalidation.ml index 358a50873..0759cb67a 100644 --- a/infer/src/checkers/PulseInvalidation.ml +++ b/infer/src/checkers/PulseInvalidation.ml @@ -7,13 +7,34 @@ open! IStd module F = Format -type std_vector_function = PushBack | Reserve [@@deriving compare] +type std_vector_function = + | Assign + | Clear + | Emplace + | EmplaceBack + | Insert + | PushBack + | Reserve + | ShrinkToFit +[@@deriving compare] let std_vector_function_pp f = function + | Assign -> + F.fprintf f "std::vector::assign" + | Clear -> + F.fprintf f "std::vector::clear" + | Emplace -> + F.fprintf f "std::vector::emplace" + | EmplaceBack -> + F.fprintf f "std::vector::emplace_back" + | Insert -> + F.fprintf f "std::vector::insert" | PushBack -> F.fprintf f "std::vector::push_back" | Reserve -> F.fprintf f "std::vector::reserve" + | ShrinkToFit -> + F.fprintf f "std::vector::shrink_to_fit" type t = diff --git a/infer/src/checkers/PulseInvalidation.mli b/infer/src/checkers/PulseInvalidation.mli index 2247c1357..65235de51 100644 --- a/infer/src/checkers/PulseInvalidation.mli +++ b/infer/src/checkers/PulseInvalidation.mli @@ -6,7 +6,16 @@ *) open! IStd -type std_vector_function = PushBack | Reserve [@@deriving compare] +type std_vector_function = + | Assign + | Clear + | Emplace + | EmplaceBack + | Insert + | PushBack + | Reserve + | ShrinkToFit +[@@deriving compare] type t = | CFree of HilExp.AccessExpression.t * Location.t diff --git a/infer/src/checkers/PulseModels.ml b/infer/src/checkers/PulseModels.ml index a77c120ea..ce3ef10f2 100644 --- a/infer/src/checkers/PulseModels.ml +++ b/infer/src/checkers/PulseModels.ml @@ -95,6 +95,15 @@ module StdVector = struct >>= PulseDomain.havoc location array + let invalidate_references invalidation : model = + fun location ~ret:_ ~actuals astate -> + match actuals with + | AccessExpression vector :: _ -> + reallocate_internal_array vector invalidation location astate + | _ -> + Ok astate + + let at : model = fun location ~ret ~actuals astate -> match actuals with @@ -137,9 +146,15 @@ module ProcNameDispatcher = struct let dispatch : (unit, model) ProcnameDispatcher.ProcName.dispatcher = let open ProcnameDispatcher.ProcName in make_dispatcher - [ -"std" &:: "vector" &:: "operator[]" &--> StdVector.at + [ -"std" &:: "vector" &:: "assign" &--> StdVector.invalidate_references Assign + ; -"std" &:: "vector" &:: "clear" &--> StdVector.invalidate_references Clear + ; -"std" &:: "vector" &:: "emplace" &--> StdVector.invalidate_references Emplace + ; -"std" &:: "vector" &:: "emplace_back" &--> StdVector.invalidate_references EmplaceBack + ; -"std" &:: "vector" &:: "insert" &--> StdVector.invalidate_references Insert + ; -"std" &:: "vector" &:: "operator[]" &--> StdVector.at ; -"std" &:: "vector" &:: "push_back" &--> StdVector.push_back - ; -"std" &:: "vector" &:: "reserve" &--> StdVector.reserve ] + ; -"std" &:: "vector" &:: "reserve" &--> StdVector.reserve + ; -"std" &:: "vector" &:: "shrink_to_fit" &--> StdVector.invalidate_references ShrinkToFit ] end let builtins_dispatcher = diff --git a/infer/tests/codetoanalyze/cpp/pulse/issues.exp b/infer/tests/codetoanalyze/cpp/pulse/issues.exp index be8d6c089..baae52f9d 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/issues.exp +++ b/infer/tests/codetoanalyze/cpp/pulse/issues.exp @@ -18,6 +18,10 @@ codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::use_afte codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::use_after_scope4_bad, 6, USE_AFTER_DESTRUCTOR, no_bucket, ERROR, [invalidated by destructor call `use_after_destructor::C_~C(c)` at line 204, column 3 here,accessed `pc->f` here] codetoanalyze/cpp/pulse/use_after_free.cpp, use_after_free_simple_bad, 2, USE_AFTER_FREE, no_bucket, ERROR, [invalidated by call to `free(x)` at line 10, column 3 here,accessed `*(x)` here] codetoanalyze/cpp/pulse/vector.cpp, FP_init_fill_then_push_back_loop_ok, 6, VECTOR_INVALIDATION, no_bucket, ERROR, [potentially invalidated by call to `std::vector::push_back(&(vec), ..)` at line 64, column 5 here,accessed `*(elt)` here] +codetoanalyze/cpp/pulse/vector.cpp, assign_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [potentially invalidated by call to `std::vector::assign(vec, ..)` at line 83, column 3 here,accessed `*(elt)` here] +codetoanalyze/cpp/pulse/vector.cpp, clear_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [potentially invalidated by call to `std::vector::clear(vec, ..)` at line 77, column 3 here,accessed `*(elt)` here] codetoanalyze/cpp/pulse/vector.cpp, deref_local_vector_element_after_push_back_bad, 4, VECTOR_INVALIDATION, no_bucket, ERROR, [potentially invalidated by call to `std::vector::push_back(&(vec), ..)` at line 19, column 3 here,accessed `*(elt)` here] codetoanalyze/cpp/pulse/vector.cpp, deref_vector_element_after_push_back_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [potentially invalidated by call to `std::vector::push_back(vec, ..)` at line 12, column 3 here,accessed `*(elt)` here] +codetoanalyze/cpp/pulse/vector.cpp, insert_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [potentially invalidated by call to `std::vector::insert(vec, ..)` at line 95, column 3 here,accessed `*(elt)` here] codetoanalyze/cpp/pulse/vector.cpp, reserve_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [potentially invalidated by call to `std::vector::reserve(vec, ..)` at line 71, column 3 here,accessed `*(elt)` here] +codetoanalyze/cpp/pulse/vector.cpp, shrink_to_fit_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [potentially invalidated by call to `std::vector::shrink_to_fit(vec, ..)` at line 89, column 3 here,accessed `*(elt)` here] diff --git a/infer/tests/codetoanalyze/cpp/pulse/vector.cpp b/infer/tests/codetoanalyze/cpp/pulse/vector.cpp index a07c9240c..e000d5e0f 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/vector.cpp +++ b/infer/tests/codetoanalyze/cpp/pulse/vector.cpp @@ -71,3 +71,41 @@ void reserve_bad(std::vector& vec) { vec.reserve(vec.size() + 1); std::cout << *elt << "\n"; } + +void clear_bad(std::vector& vec) { + int* elt = &vec[1]; + vec.clear(); + std::cout << *elt << "\n"; +} + +void assign_bad(std::vector& vec) { + int* elt = &vec[1]; + vec.assign(11, 7); + std::cout << *elt << "\n"; +} + +void shrink_to_fit_bad(std::vector& vec) { + int* elt = &vec[1]; + vec.shrink_to_fit(); + std::cout << *elt << "\n"; +} + +void insert_bad(std::vector& vec) { + int* elt = &vec[1]; + vec.insert(vec.begin(), 7); + std::cout << *elt << "\n"; +} + +void FN_emplace_bad(std::vector& vec) { + int* elt = &vec[1]; + vec.emplace(vec.begin(), + 7); // procname matcher does not match emplace (T37883260) + std::cout << *elt << "\n"; +} + +void FN_emplace_back_bad(std::vector& vec) { + int* elt = &vec[1]; + vec.emplace_back(7); // procname matcher does not match emplace_back + // (T37883260) + std::cout << *elt << "\n"; +}