diff --git a/infer/src/IR/ProcnameDispatcher.ml b/infer/src/IR/ProcnameDispatcher.ml index dc369688d..c2137b1ff 100644 --- a/infer/src/IR/ProcnameDispatcher.ml +++ b/infer/src/IR/ProcnameDispatcher.ml @@ -729,6 +729,10 @@ module Call = struct let capt_arg_of_typ m = {one_arg_matcher= match_typ (m <...>! ()); capture= capture_arg} + let capt_arg_payload_of_typ m = + {one_arg_matcher= match_typ (m <...>! ()); capture= capture_arg_val} + + let capt_exp_of_typ m = {one_arg_matcher= match_typ (m <...>! ()); capture= capture_arg_exp} let one_arg_matcher_of_prim_typ typ = diff --git a/infer/src/IR/ProcnameDispatcher.mli b/infer/src/IR/ProcnameDispatcher.mli index 6c27e0d33..76b2d9dde 100644 --- a/infer/src/IR/ProcnameDispatcher.mli +++ b/infer/src/IR/ProcnameDispatcher.mli @@ -199,6 +199,11 @@ module Call : sig one_arg (** Captures one arg of the given type *) + val capt_arg_payload_of_typ : + ('context, unit, _, 'arg_payload) name_matcher + -> ('context, 'arg_payload, 'wrapped_arg, 'wrapped_arg -> 'f, 'f, 'arg_payload) one_arg + (** Captures the payload of one arg of the given type *) + val capt_exp_of_typ : ('context, unit, _, 'arg_payload) name_matcher -> ('context, Exp.t, 'wrapped_arg, 'wrapped_arg -> 'f, 'f, 'arg_payload) one_arg diff --git a/infer/src/pulse/PulseModels.ml b/infer/src/pulse/PulseModels.ml index 4dbf4cd00..ac402d74d 100644 --- a/infer/src/pulse/PulseModels.ml +++ b/infer/src/pulse/PulseModels.ml @@ -435,6 +435,18 @@ module StdVector = struct >>= PulseOperations.havoc_field location vector GenericArrayBackedCollection.field trace + let init_list_constructor this init_list ~caller_summary:_ ~callee_procname:_ location ~ret:_ + astate = + let event = ValueHistory.Call {f= Model "std::vector::vector()"; location; in_call= []} in + let* astate, init_copy = PulseOperations.shallow_copy location init_list astate in + let+ astate = + PulseOperations.write_field location ~ref:this GenericArrayBackedCollection.field + ~obj:(fst init_copy, event :: snd init_copy) + astate + in + [ExecutionDomain.ContinueProgram astate] + + let invalidate_references vector_f vector : model = fun ~caller_summary:_ ~callee_procname:_ location ~ret:_ astate -> let crumb = @@ -534,6 +546,8 @@ module ProcNameDispatcher = struct ; +match_builtin BuiltinDecl.__cast <>$ capt_arg_payload $+...$--> Misc.id_first_arg ; +match_builtin BuiltinDecl.abort <>--> Misc.early_exit ; +match_builtin BuiltinDecl.exit <>--> Misc.early_exit + ; +match_builtin BuiltinDecl.__infer_initializer_list + <>$ capt_arg_payload $+...$--> Misc.id_first_arg ; +PatternMatch.implements_lang "System" &:: "exit" <>--> Misc.early_exit ; +match_builtin BuiltinDecl.__get_array_length <>--> Misc.return_unknown_size ; (* consider that all fbstrings are small strings to avoid false positives due to manual @@ -578,6 +592,9 @@ module ProcNameDispatcher = struct ; -"std" &:: "integral_constant" < any_typ &+ capt_int >::+ (fun _ name -> String.is_prefix ~prefix:"operator_" name) <>--> Misc.return_int + ; -"std" &:: "vector" &:: "vector" <>$ capt_arg_payload + $+ capt_arg_payload_of_typ (-"std" &:: "initializer_list") + $+...$--> StdVector.init_list_constructor ; -"std" &:: "__wrap_iter" &:: "__wrap_iter" <>$ capt_arg_payload $+ capt_arg_payload $+...$--> GenericArrayBackedCollectionIterator.constructor ~desc:"iterator constructor" ; -"std" &:: "__wrap_iter" &:: "operator*" <>$ capt_arg_payload diff --git a/infer/tests/codetoanalyze/cpp/pulse/issues.exp b/infer/tests/codetoanalyze/cpp/pulse/issues.exp index 6b4c8e350..a17a07420 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/issues.exp +++ b/infer/tests/codetoanalyze/cpp/pulse/issues.exp @@ -77,7 +77,8 @@ codetoanalyze/cpp/pulse/values.cpp, free_if_deref_bad, 2, USE_AFTER_FREE, no_buc codetoanalyze/cpp/pulse/vector.cpp, FP_init_fill_then_push_back_loop_ok, 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, assign_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `vec` of assign_bad,was potentially invalidated by `std::vector::assign()`,use-after-lifetime part of the trace starts here,parameter `vec` of assign_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, clear_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `vec` of clear_bad,was potentially invalidated by `std::vector::clear()`,use-after-lifetime part of the trace starts here,parameter `vec` of clear_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, deref_local_vector_element_after_push_back_bad, 4, 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, deref_local_vector_element_after_push_back_bad, 4, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,variable `C++ temporary` declared here,was potentially invalidated by `std::vector::push_back()`,use-after-lifetime part of the trace starts here,variable `C++ temporary` 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, deref_null_local_vector_element_bad, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here] codetoanalyze/cpp/pulse/vector.cpp, deref_vector_element_after_push_back_bad, 4, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `vec` of deref_vector_element_after_push_back_bad,was potentially invalidated by `std::vector::push_back()`,use-after-lifetime part of the trace starts here,parameter `vec` of deref_vector_element_after_push_back_bad,passed as argument to `std::vector::at()` (modelled),return from call to `std::vector::at()` (modelled),assigned,assigned,invalid access occurs here] codetoanalyze/cpp/pulse/vector.cpp, deref_vector_pointer_element_after_push_back_bad, 4, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `vec` of deref_vector_pointer_element_after_push_back_bad,was potentially invalidated by `std::vector::push_back()`,use-after-lifetime part of the trace starts here,parameter `vec` of deref_vector_pointer_element_after_push_back_bad,passed as argument to `std::vector::at()` (modelled),return from call to `std::vector::at()` (modelled),assigned,assigned,invalid access occurs here] codetoanalyze/cpp/pulse/vector.cpp, emplace_back_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `vec` of emplace_back_bad,was potentially invalidated by `std::vector::emplace_back()`,use-after-lifetime part of the trace starts here,parameter `vec` of emplace_back_bad,passed as argument to `std::vector::at()` (modelled),return from call to `std::vector::at()` (modelled),assigned,invalid access occurs here] diff --git a/infer/tests/codetoanalyze/cpp/pulse/vector.cpp b/infer/tests/codetoanalyze/cpp/pulse/vector.cpp index 9467690c4..ce2a95785 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/vector.cpp +++ b/infer/tests/codetoanalyze/cpp/pulse/vector.cpp @@ -29,6 +29,11 @@ void deref_local_vector_element_after_push_back_bad() { std::cout << *elt << "\n"; } +void deref_null_local_vector_element_bad() { + std::vector vec = {nullptr}; + std::cout << *vec[0] << "\n"; +} + void two_push_back_ok(std::vector& vec) { vec.push_back(32); vec.push_back(52);