From 332b150be9196c697fb6a0f466d4b074f84d5895 Mon Sep 17 00:00:00 2001 From: Daiva Naudziuniene Date: Thu, 6 Dec 2018 05:32:13 -0800 Subject: [PATCH] [pulse] Model std::vector::reserve to invalidate references to elements Summary: Similarly as `std::vector::push_back`, `std::vector::reserve` can invalidate the references to elements if the new size is bigger than the existing one. More info on `std::vector::reserve`: https://en.cppreference.com/w/cpp/container/vector/reserve Reviewed By: jvillard Differential Revision: D13340324 fbshipit-source-id: bf99b6923 --- infer/src/checkers/PulseInvalidation.ml | 21 +++++++++++++------ infer/src/checkers/PulseInvalidation.mli | 4 +++- infer/src/checkers/PulseModels.ml | 19 ++++++++++------- .../tests/codetoanalyze/cpp/pulse/issues.exp | 1 + .../tests/codetoanalyze/cpp/pulse/vector.cpp | 6 ++++++ 5 files changed, 37 insertions(+), 14 deletions(-) diff --git a/infer/src/checkers/PulseInvalidation.ml b/infer/src/checkers/PulseInvalidation.ml index 2a98b9730..277fac399 100644 --- a/infer/src/checkers/PulseInvalidation.ml +++ b/infer/src/checkers/PulseInvalidation.ml @@ -7,12 +7,21 @@ open! IStd module F = Format +type std_vector_function = PushBack | Reserve [@@deriving compare] + +let std_vector_function_pp f = function + | PushBack -> + F.fprintf f "std::vector::push_back" + | Reserve -> + F.fprintf f "std::vector::reserve" + + type t = | CFree of AccessExpression.t * Location.t | CppDelete of AccessExpression.t * Location.t | CppDestructor of Typ.Procname.t * AccessExpression.t * Location.t | Nullptr - | StdVectorPushBack of AccessExpression.t * Location.t + | StdVector of std_vector_function * AccessExpression.t * Location.t [@@deriving compare] let issue_type_of_cause = function @@ -24,7 +33,7 @@ let issue_type_of_cause = function IssueType.use_after_destructor | Nullptr -> IssueType.null_dereference - | StdVectorPushBack _ -> + | StdVector _ -> IssueType.vector_invalidation @@ -32,7 +41,7 @@ let get_location = function | CFree (_, location) | CppDelete (_, location) | CppDestructor (_, _, location) - | StdVectorPushBack (_, location) -> + | StdVector (_, _, location) -> Some location | Nullptr -> None @@ -50,6 +59,6 @@ let pp f = function AccessExpression.pp access_expr Location.pp location | Nullptr -> F.fprintf f "null pointer" - | StdVectorPushBack (access_expr, location) -> - F.fprintf f "potentially invalidated by call to `std::vector::push_back(%a, ..)` at %a" - AccessExpression.pp access_expr Location.pp location + | StdVector (std_vector_f, access_expr, location) -> + F.fprintf f "potentially invalidated by call to `%a(%a, ..)` at %a" std_vector_function_pp + std_vector_f AccessExpression.pp access_expr Location.pp location diff --git a/infer/src/checkers/PulseInvalidation.mli b/infer/src/checkers/PulseInvalidation.mli index 16104d01a..4f2802cab 100644 --- a/infer/src/checkers/PulseInvalidation.mli +++ b/infer/src/checkers/PulseInvalidation.mli @@ -6,12 +6,14 @@ *) open! IStd +type std_vector_function = PushBack | Reserve [@@deriving compare] + type t = | CFree of AccessExpression.t * Location.t | CppDelete of AccessExpression.t * Location.t | CppDestructor of Typ.Procname.t * AccessExpression.t * Location.t | Nullptr - | StdVectorPushBack of AccessExpression.t * Location.t + | StdVector of std_vector_function * AccessExpression.t * Location.t [@@deriving compare] val issue_type_of_cause : t -> IssueType.t diff --git a/infer/src/checkers/PulseModels.ml b/infer/src/checkers/PulseModels.ml index 6ae43890f..6e53ad0ec 100644 --- a/infer/src/checkers/PulseModels.ml +++ b/infer/src/checkers/PulseModels.ml @@ -86,6 +86,15 @@ module StdVector = struct AccessExpression.(array_offset (dereference (to_internal_array vector)) Typ.void []) + let reallocate_internal_array vector vector_f location astate = + let array = to_internal_array vector in + (* all elements should be invalidated *) + let array_elements = deref_internal_array vector in + let invalidation = PulseInvalidation.StdVector (vector_f, vector, location) in + PulseDomain.invalidate invalidation location array_elements astate + >>= PulseDomain.havoc location array + + let at : model = fun location ~ret ~actuals astate -> match actuals with @@ -100,7 +109,8 @@ module StdVector = struct fun location ~ret:_ ~actuals astate -> match actuals with | [AccessExpression vector; _value] -> - PulseDomain.StdVector.mark_reserved location vector astate + reallocate_internal_array vector Reserve location astate + >>= PulseDomain.StdVector.mark_reserved location vector | _ -> Ok astate @@ -117,12 +127,7 @@ module StdVector = struct Ok astate else (* simulate a re-allocation of the underlying array every time an element is added *) - let array = to_internal_array vector in - (* all elements should be invalidated *) - let array_elements = deref_internal_array vector in - let invalidation = PulseInvalidation.StdVectorPushBack (vector, location) in - PulseDomain.invalidate invalidation location array_elements astate - >>= PulseDomain.havoc location array + reallocate_internal_array vector PushBack location astate | _ -> Ok astate end diff --git a/infer/tests/codetoanalyze/cpp/pulse/issues.exp b/infer/tests/codetoanalyze/cpp/pulse/issues.exp index 65d65c005..be8d6c089 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/issues.exp +++ b/infer/tests/codetoanalyze/cpp/pulse/issues.exp @@ -20,3 +20,4 @@ codetoanalyze/cpp/pulse/use_after_free.cpp, use_after_free_simple_bad, 2, USE_AF 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, 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, 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] diff --git a/infer/tests/codetoanalyze/cpp/pulse/vector.cpp b/infer/tests/codetoanalyze/cpp/pulse/vector.cpp index 061dd70ac..a07c9240c 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/vector.cpp +++ b/infer/tests/codetoanalyze/cpp/pulse/vector.cpp @@ -65,3 +65,9 @@ void FP_init_fill_then_push_back_loop_ok(std::vector& vec_other) { } std::cout << *elt << "\n"; } + +void reserve_bad(std::vector& vec) { + int* elt = &vec[1]; + vec.reserve(vec.size() + 1); + std::cout << *elt << "\n"; +}