From dae7f36339d487836b09c740bda139b54c62657c Mon Sep 17 00:00:00 2001 From: Daiva Naudziuniene Date: Mon, 20 Apr 2020 02:36:04 -0700 Subject: [PATCH] [pulse] Vector iterator model Summary: Modeling vector iterator with two internal fields: an internal array and an internal pointer. The internal array field points to the internal array field of a vector; the internal pointer field represents the current element of the array. For now `operator++` creates a fresh element inside the array. Reviewed By: ezgicicek Differential Revision: D21043304 fbshipit-source-id: db3be49ce --- infer/src/pulse/PulseModels.ml | 122 ++++++++++++++++-- infer/src/pulse/PulseOperations.ml | 4 +- infer/src/pulse/PulseOperations.mli | 9 ++ .../codetoanalyze/cpp/impurity/issues.exp | 6 +- .../tests/codetoanalyze/cpp/pulse/issues.exp | 4 + .../cpp/pulse/vector_iterator.cpp | 66 ++++++++++ 6 files changed, 192 insertions(+), 19 deletions(-) create mode 100644 infer/tests/codetoanalyze/cpp/pulse/vector_iterator.cpp diff --git a/infer/src/pulse/PulseModels.ml b/infer/src/pulse/PulseModels.ml index ecb0db750..6c4bc01f9 100644 --- a/infer/src/pulse/PulseModels.ml +++ b/infer/src/pulse/PulseModels.ml @@ -349,31 +349,88 @@ module StdFunction = struct ~formals_opt:None astate end -module StdVector = struct - let internal_array = +module GenericArrayBackedCollection = struct + let field = Fieldname.make - (Typ.CStruct (QualifiedCppName.of_list ["std"; "vector"])) + (Typ.CStruct (QualifiedCppName.of_list ["__infer_pulse_model"])) "__infer_model_backing_array" - let internal_array_access = HilExp.Access.FieldAccess internal_array + let access = HilExp.Access.FieldAccess field + + let eval location collection astate = + PulseOperations.eval_access location collection access astate + + + let eval_element location internal_array index astate = + PulseOperations.eval_access location internal_array (ArrayAccess (Typ.void, index)) astate + + + let element location collection index astate = + let* astate, internal_array = eval location collection astate in + eval_element location internal_array index astate +end + +module GenericArrayBackedCollectionIterator = struct + let internal_pointer = + Fieldname.make + (Typ.CStruct (QualifiedCppName.of_list ["__infer_pulse_model"])) + "__infer_model_backing_pointer" + - let to_internal_array location vector astate = - PulseOperations.eval_access location vector internal_array_access astate + let internal_pointer_access = HilExp.Access.FieldAccess internal_pointer + let to_internal_pointer location iterator astate = + PulseOperations.eval_access location iterator internal_pointer_access astate - let element_of_internal_array location vector index astate = - let* astate, vector_internal_array = to_internal_array location vector astate in - PulseOperations.eval_access location vector_internal_array - (ArrayAccess (Typ.void, index)) + + let constructor ~desc this init : model = + fun ~caller_summary:_ ~callee_procname:_ location ~ret:_ astate -> + let event = ValueHistory.Call {f= Model desc; location; in_call= []} in + let* astate, (arr_addr, arr_hist) = GenericArrayBackedCollection.eval location init astate in + let* astate = + PulseOperations.write_field location ~ref:this GenericArrayBackedCollection.field + ~obj:(arr_addr, event :: arr_hist) + astate + in + let* astate, (p_addr, p_hist) = to_internal_pointer location init astate in + PulseOperations.write_field location ~ref:this internal_pointer + ~obj:(p_addr, event :: p_hist) astate + >>| ExecutionDomain.continue >>| List.return + let operator_star ~desc iter ~caller_summary:_ ~callee_procname:_ location ~ret astate = + let event = ValueHistory.Call {f= Model desc; location; in_call= []} in + let* astate, iter_index = to_internal_pointer location iter astate in + let+ astate, (elem_val, elem_hist) = + GenericArrayBackedCollection.element location iter (fst iter_index) astate + in + let astate = PulseOperations.write_id (fst ret) (elem_val, event :: elem_hist) astate in + [ExecutionDomain.ContinueProgram astate] + + + let operator_plus_plus ~desc iter ~caller_summary:_ ~callee_procname:_ location ~ret:_ astate = + let event = ValueHistory.Call {f= Model desc; location; in_call= []} in + let index_next = AbstractValue.mk_fresh () in + let* astate, current_index = to_internal_pointer location iter astate in + let* astate, element = + GenericArrayBackedCollection.element location iter (fst current_index) astate + in + (* Iterator is invalid if the value it points to is invalid *) + let* astate, _ = PulseOperations.eval_access location element Dereference astate in + PulseOperations.write_field location ~ref:iter internal_pointer + ~obj:(index_next, [event]) + astate + >>| ExecutionDomain.continue >>| List.return +end + +module StdVector = struct let reallocate_internal_array trace vector vector_f location astate = - let* astate, array_address = to_internal_array location vector astate in + let* astate, array_address = GenericArrayBackedCollection.eval location vector astate in PulseOperations.invalidate_array_elements location (StdVector vector_f) array_address astate >>= PulseOperations.invalidate_deref location (StdVector vector_f) array_address - >>= PulseOperations.havoc_field location vector internal_array trace + >>= PulseOperations.havoc_field location vector GenericArrayBackedCollection.field trace let invalidate_references vector_f vector : model = @@ -391,11 +448,33 @@ module StdVector = struct let at ~desc vector index : model = fun ~caller_summary:_ ~callee_procname:_ location ~ret astate -> let event = ValueHistory.Call {f= Model desc; location; in_call= []} in - let+ astate, (addr, hist) = element_of_internal_array location vector (fst index) astate in + let+ astate, (addr, hist) = + GenericArrayBackedCollection.element location vector (fst index) astate + in let astate = PulseOperations.write_id (fst ret) (addr, event :: hist) astate in [ExecutionDomain.ContinueProgram astate] + let vector_begin vector iter : model = + fun ~caller_summary:_ ~callee_procname:_ location ~ret:_ astate -> + let event = ValueHistory.Call {f= Model "std::vector::begin()"; location; in_call= []} in + let index_zero = AbstractValue.mk_fresh () in + let astate = + PulseArithmetic.and_eq_int (Immediate {location; history= []}) index_zero IntLit.zero astate + in + let* astate, ((arr_addr, hist) as arr) = + GenericArrayBackedCollection.eval location vector astate + in + let* astate, _ = GenericArrayBackedCollection.eval_element location arr index_zero astate in + PulseOperations.write_field location ~ref:iter GenericArrayBackedCollection.field + ~obj:(arr_addr, event :: hist) + astate + >>= PulseOperations.write_field location ~ref:iter + GenericArrayBackedCollectionIterator.internal_pointer + ~obj:(index_zero, [event]) + >>| ExecutionDomain.continue >>| List.return + + let reserve vector : model = fun ~caller_summary:_ ~callee_procname:_ location ~ret:_ astate -> let crumb = ValueHistory.Call {f= Model "std::vector::reserve()"; location; in_call= []} in @@ -422,7 +501,7 @@ module JavaCollection = struct fun ~caller_summary:_ ~callee_procname:_ location ~ret astate -> let event = ValueHistory.Call {f= Model "Collection.set"; location; in_call= []} in let* astate, ((old_addr, old_hist) as old_elem) = - StdVector.element_of_internal_array location coll (fst index) astate + GenericArrayBackedCollection.element location coll (fst index) astate in let+ astate = PulseOperations.write_deref location ~ref:new_elem @@ -497,10 +576,25 @@ module ProcNameDispatcher = struct ; -"std" &:: "integral_constant" < any_typ &+ capt_int >::+ (fun _ name -> String.is_prefix ~prefix:"operator_" name) <>--> Misc.return_int + ; -"std" &:: "__wrap_iter" &:: "__wrap_iter" <>$ capt_arg_payload $+ capt_arg_payload + $+...$--> GenericArrayBackedCollectionIterator.constructor ~desc:"iterator constructor" + ; -"std" &:: "__wrap_iter" &:: "operator*" <>$ capt_arg_payload + $--> GenericArrayBackedCollectionIterator.operator_star ~desc:"iterator operator*" + ; -"std" &:: "__wrap_iter" &:: "operator++" <>$ capt_arg_payload + $--> GenericArrayBackedCollectionIterator.operator_plus_plus ~desc:"iterator operator++" + ; -"__gnu_cxx" &:: "__normal_iterator" &:: "__normal_iterator" <>$ capt_arg_payload + $+ capt_arg_payload + $+...$--> GenericArrayBackedCollectionIterator.constructor ~desc:"iterator constructor" + ; -"__gnu_cxx" &:: "__normal_iterator" &:: "operator*" <>$ capt_arg_payload + $--> GenericArrayBackedCollectionIterator.operator_star ~desc:"iterator operator*" + ; -"__gnu_cxx" &:: "__normal_iterator" &:: "operator++" <>$ capt_arg_payload + $--> GenericArrayBackedCollectionIterator.operator_plus_plus ~desc:"iterator operator++" ; -"std" &:: "vector" &:: "assign" <>$ capt_arg_payload $+...$--> StdVector.invalidate_references Assign ; -"std" &:: "vector" &:: "at" <>$ capt_arg_payload $+ capt_arg_payload $--> StdVector.at ~desc:"std::vector::at()" + ; -"std" &:: "vector" &:: "begin" <>$ capt_arg_payload $+ capt_arg_payload + $--> StdVector.vector_begin ; -"std" &:: "vector" &:: "clear" <>$ capt_arg_payload $--> StdVector.invalidate_references Clear ; -"std" &:: "vector" &:: "emplace" $ capt_arg_payload diff --git a/infer/src/pulse/PulseOperations.ml b/infer/src/pulse/PulseOperations.ml index b1282e879..9ed11e3f7 100644 --- a/infer/src/pulse/PulseOperations.ml +++ b/infer/src/pulse/PulseOperations.ml @@ -214,12 +214,12 @@ let write_deref location ~ref:addr_trace_ref ~obj:addr_trace_obj astate = write_access location addr_trace_ref Dereference addr_trace_obj astate -let write_field location addr_trace_ref field addr_trace_obj astate = +let write_field location ~ref:addr_trace_ref field ~obj:addr_trace_obj astate = write_access location addr_trace_ref (FieldAccess field) addr_trace_obj astate let havoc_field location addr_trace field trace_obj astate = - write_field location addr_trace field (AbstractValue.mk_fresh (), trace_obj) astate + write_field location ~ref:addr_trace field ~obj:(AbstractValue.mk_fresh (), trace_obj) astate let allocate procname location addr_trace astate = diff --git a/infer/src/pulse/PulseOperations.mli b/infer/src/pulse/PulseOperations.mli index da8607069..e6ce46abe 100644 --- a/infer/src/pulse/PulseOperations.mli +++ b/infer/src/pulse/PulseOperations.mli @@ -61,6 +61,15 @@ val realloc_pvar : Pvar.t -> Location.t -> t -> t val write_id : Ident.t -> AbstractValue.t * ValueHistory.t -> t -> t +val write_field : + Location.t + -> ref:AbstractValue.t * ValueHistory.t + -> Fieldname.t + -> obj:AbstractValue.t * ValueHistory.t + -> t + -> t access_result +(** write the edge [ref --.field--> obj] *) + val write_deref : Location.t -> ref:AbstractValue.t * ValueHistory.t diff --git a/infer/tests/codetoanalyze/cpp/impurity/issues.exp b/infer/tests/codetoanalyze/cpp/impurity/issues.exp index 8650093bc..b1f7885a8 100644 --- a/infer/tests/codetoanalyze/cpp/impurity/issues.exp +++ b/infer/tests/codetoanalyze/cpp/impurity/issues.exp @@ -30,7 +30,7 @@ codetoanalyze/cpp/impurity/unmodeled.cpp, output_stream_impure, 0, IMPURE_FUNCTI codetoanalyze/cpp/impurity/unmodeled.cpp, random_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function random_impure,call to skipped function rand occurs here] codetoanalyze/cpp/impurity/vector.cpp, assign_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function assign_impure,parameter `vec` modified here] codetoanalyze/cpp/impurity/vector.cpp, clear_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function clear_impure,parameter `vec` modified here] -codetoanalyze/cpp/impurity/vector.cpp, insert_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function insert_impure,parameter `vec` modified here,call to skipped function std::vector>::begin occurs here] +codetoanalyze/cpp/impurity/vector.cpp, insert_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function insert_impure,parameter `vec` modified here] codetoanalyze/cpp/impurity/vector.cpp, push_back_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function push_back_impure,parameter `vec` modified here] -codetoanalyze/cpp/impurity/vector.cpp, push_back_in_loop_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function push_back_in_loop_impure,parameter `vec_other` modified here,parameter `vec` modified here,call to skipped function std::vector>::begin occurs here,call to skipped function std::vector>::end occurs here] -codetoanalyze/cpp/impurity/vector.cpp, set_zero_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function set_zero_impure,parameter `numbers` modified here,call to skipped function std::vector>::begin occurs here,call to skipped function std::vector>::end occurs here] +codetoanalyze/cpp/impurity/vector.cpp, push_back_in_loop_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function push_back_in_loop_impure,parameter `vec_other` modified here,parameter `vec` modified here,call to skipped function std::vector>::end occurs here] +codetoanalyze/cpp/impurity/vector.cpp, set_zero_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function set_zero_impure,parameter `numbers` modified here,call to skipped function std::vector>::end occurs here] diff --git a/infer/tests/codetoanalyze/cpp/pulse/issues.exp b/infer/tests/codetoanalyze/cpp/pulse/issues.exp index fd949627e..64fecf6f1 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/issues.exp +++ b/infer/tests/codetoanalyze/cpp/pulse/issues.exp @@ -87,3 +87,7 @@ codetoanalyze/cpp/pulse/vector.cpp, insert_bad, 3, VECTOR_INVALIDATION, no_bucke codetoanalyze/cpp/pulse/vector.cpp, push_back_loop_bad, 6, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,variable `vec` declared here,was potentially invalidated by `std::vector::push_back()`,use-after-lifetime part of the trace starts here,variable `vec` declared here,passed as argument to `std::vector::at()` (modelled),return from call to `std::vector::at()` (modelled),assigned,invalid access occurs here] codetoanalyze/cpp/pulse/vector.cpp, reserve_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `vec` of reserve_bad,was potentially invalidated by `std::vector::reserve()`,use-after-lifetime part of the trace starts here,parameter `vec` of reserve_bad,passed as argument to `std::vector::at()` (modelled),return from call to `std::vector::at()` (modelled),assigned,invalid access occurs here] codetoanalyze/cpp/pulse/vector.cpp, shrink_to_fit_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `vec` of shrink_to_fit_bad,was potentially invalidated by `std::vector::shrink_to_fit()`,use-after-lifetime part of the trace starts here,parameter `vec` of shrink_to_fit_bad,passed as argument to `std::vector::at()` (modelled),return from call to `std::vector::at()` (modelled),assigned,invalid access occurs here] +codetoanalyze/cpp/pulse/vector_iterator.cpp, iterator_after_push_back_loop_bad, 9, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,variable `vec` declared here,was potentially invalidated by `std::vector::push_back()`,use-after-lifetime part of the trace starts here,variable `vec` declared here,passed as argument to `iterator operator*` (modelled),return from call to `iterator operator*` (modelled),invalid access occurs here] +codetoanalyze/cpp/pulse/vector_iterator.cpp, iterator_next_after_emplace_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `vec` of iterator_next_after_emplace_bad,was potentially invalidated by `std::vector::emplace()`,use-after-lifetime part of the trace starts here,parameter `vec` of iterator_next_after_emplace_bad,invalid access occurs here] +codetoanalyze/cpp/pulse/vector_iterator.cpp, iterator_next_after_emplace_loop_bad, 2, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `vec` of iterator_next_after_emplace_loop_bad,was potentially invalidated by `std::vector::emplace()`,use-after-lifetime part of the trace starts here,parameter `vec` of iterator_next_after_emplace_loop_bad,invalid access occurs here] +codetoanalyze/cpp/pulse/vector_iterator.cpp, iterator_read_after_emplace_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `vec` of iterator_read_after_emplace_bad,was potentially invalidated by `std::vector::emplace()`,use-after-lifetime part of the trace starts here,parameter `vec` of iterator_read_after_emplace_bad,passed as argument to `iterator operator*` (modelled),return from call to `iterator operator*` (modelled),invalid access occurs here] diff --git a/infer/tests/codetoanalyze/cpp/pulse/vector_iterator.cpp b/infer/tests/codetoanalyze/cpp/pulse/vector_iterator.cpp new file mode 100644 index 000000000..3138b0a1d --- /dev/null +++ b/infer/tests/codetoanalyze/cpp/pulse/vector_iterator.cpp @@ -0,0 +1,66 @@ +/* + * Copyright (c) Facebook, Inc. and its affiliates. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + */ +#include +#include + +void iterator_read_after_emplace_bad(std::vector& vec) { + auto iter = vec.begin(); + vec.emplace(iter, 4); + std::cout << *iter << '\n'; +} + +void iterator_next_after_emplace_bad(std::vector& vec) { + auto iter = vec.begin(); + vec.emplace(iter, 4); + ++iter; + std::cout << *iter << '\n'; +} + +void another_iterator_ok(std::vector& vec) { + auto iter = vec.begin(); + vec.emplace(iter, 4); + auto another_iter = vec.begin(); + std::cout << *another_iter << '\n'; + ++another_iter; + std::cout << *another_iter << '\n'; +} + +void read_iterator_loop_ok(std::vector& vec) { + int sum = 0; + for (auto iter = vec.begin(); iter != vec.end(); ++iter) { + sum += *iter; + } +} + +void iterator_next_after_emplace_loop_bad(std::vector& vec) { + int sum = 0; + for (auto iter = vec.begin(); iter != vec.end(); ++iter) { + int elem = *iter; + sum += elem; + if (elem < 0) + vec.emplace(iter, -elem); + } +} + +void iterator_after_push_back_loop_bad(std::vector& vec_other) { + std::vector vec(2); + auto iter_begin = vec.begin(); + auto iter_end = vec.end(); + for (const auto& i : vec_other) { + vec.push_back(i); + } + int sum = 0; + for (auto iter = iter_begin; iter != iter_end; ++iter) { + sum += *iter; + } +} + +void FN_iterator_empty_vector_read_bad() { + std::vector vec = {}; + auto iter = vec.begin(); + std::cout << *iter << '\n'; +}