diff --git a/infer/src/pulse/Pulse.ml b/infer/src/pulse/Pulse.ml index 20d37e325..abda2f70c 100644 --- a/infer/src/pulse/Pulse.ml +++ b/infer/src/pulse/Pulse.ml @@ -166,6 +166,7 @@ module PulseTransferFunctions = struct in match model with | Some model -> + L.d_printfln "Found model for call@\n" ; model call_loc ~ret ~actuals:actuals_evaled astate | None -> ( (* do interprocedural call then destroy objects going out of scope *) diff --git a/infer/src/pulse/PulseModels.ml b/infer/src/pulse/PulseModels.ml index 8c46f779f..9145897bd 100644 --- a/infer/src/pulse/PulseModels.ml +++ b/infer/src/pulse/PulseModels.ml @@ -17,6 +17,24 @@ type exec_fun = type model = exec_fun module Misc = struct + let shallow_copy model_desc : model = + fun location ~ret:(ret_id, _) ~actuals astate -> + let event = PulseDomain.ValueHistory.Call {f= `Model model_desc; location} in + ( match actuals with + | [(dest_pointer_hist, _); (src_pointer_hist, _)] -> + PulseOperations.eval_access location src_pointer_hist Dereference astate + >>= fun (astate, obj) -> + PulseOperations.shallow_copy location obj astate + >>= fun (astate, obj_copy) -> + let obj_hist = snd obj in + PulseOperations.write_deref location ~ref:dest_pointer_hist + ~obj:(obj_copy, event :: obj_hist) + astate + | _ -> + Ok astate ) + >>| fun astate -> [PulseOperations.havoc_id ret_id [event] astate] + + let early_exit : model = fun _ ~ret:_ ~actuals:_ _ -> Ok [] let skip : model = fun _ ~ret:_ ~actuals:_ astate -> Ok [astate] @@ -48,28 +66,31 @@ module Cplusplus = struct Ok [astate] + let placement_new : model = + fun location ~ret:(ret_id, _) ~actuals astate -> + let event = PulseDomain.ValueHistory.Call {f= `Model ""; location} in + match List.rev actuals with + | ((address, _), _) :: _ -> + Ok [PulseOperations.write_id ret_id (address, [event]) astate] + | _ -> + Ok [PulseOperations.havoc_id ret_id [event] astate] +end + +module StdFunction = struct let operator_call : model = fun location ~ret:(ret_id, _) ~actuals astate -> ( match actuals with - | (lambda, _) :: _ -> + | (lambda_ptr_hist, _) :: _ -> + PulseOperations.eval_access location lambda_ptr_hist Dereference astate + >>= fun (astate, (lambda, _)) -> PulseOperations.Closures.check_captured_addresses (PulseDomain.InterprocAction.Immediate {imm= (); location}) - (fst lambda) astate + lambda astate | _ -> Ok astate ) >>| fun astate -> let event = PulseDomain.ValueHistory.Call {f= `Model ""; location} in [PulseOperations.havoc_id ret_id [event] astate] - - - let placement_new : model = - fun location ~ret:(ret_id, _) ~actuals astate -> - let event = PulseDomain.ValueHistory.Call {f= `Model ""; location} in - match List.rev actuals with - | ((address, _), _) :: _ -> - Ok [PulseOperations.write_id ret_id (address, [event]) astate] - | _ -> - Ok [PulseOperations.havoc_id ret_id [event] astate] end module StdVector = struct @@ -164,7 +185,8 @@ module ProcNameDispatcher = struct make_dispatcher [ -"folly" &:: "DelayedDestruction" &:: "destroy" &--> Misc.skip ; -"folly" &:: "SocketAddress" &:: "~SocketAddress" &--> Misc.skip - ; -"std" &:: "function" &:: "operator()" &--> Cplusplus.operator_call + ; -"std" &:: "function" &:: "operator()" &--> StdFunction.operator_call + ; -"std" &:: "function" &:: "operator=" &--> Misc.shallow_copy "std::function::operator=" ; -"std" &:: "vector" &:: "assign" &--> StdVector.invalidate_references Assign ; -"std" &:: "vector" &:: "clear" &--> StdVector.invalidate_references Clear ; -"std" &:: "vector" &:: "emplace" &--> StdVector.invalidate_references Emplace diff --git a/infer/src/pulse/PulseOperations.ml b/infer/src/pulse/PulseOperations.ml index d4580ca34..b17050b53 100644 --- a/infer/src/pulse/PulseOperations.ml +++ b/infer/src/pulse/PulseOperations.ml @@ -215,6 +215,21 @@ let invalidate_array_elements location cause addr_trace astate = edges astate +let shallow_copy location addr_hist astate = + let action = action_of_address location in + check_addr_access action addr_hist astate + >>| fun astate -> + let cell = + match Memory.find_opt (fst addr_hist) astate with + | None -> + (Memory.Edges.empty, Attributes.empty) + | Some cell -> + cell + in + let copy = AbstractAddress.mk_fresh () in + (Memory.set_cell copy cell astate, copy) + + let check_address_escape escape_location proc_desc address history astate = let is_assigned_to_global address astate = let points_to_address pointer address astate = diff --git a/infer/src/pulse/PulseOperations.mli b/infer/src/pulse/PulseOperations.mli index a69fdfb1a..314de8787 100644 --- a/infer/src/pulse/PulseOperations.mli +++ b/infer/src/pulse/PulseOperations.mli @@ -86,6 +86,10 @@ val invalidate_array_elements : -> t access_result (** record that all the array elements that address points to is invalid *) +val shallow_copy : + Location.t -> PulseDomain.AddrTracePair.t -> t -> (t * AbstractAddress.t) access_result +(** returns the address of a new cell with the same edges as the original *) + val remove_vars : Var.t list -> t -> t val check_address_escape : diff --git a/infer/tests/codetoanalyze/cpp/pulse/closures.cpp b/infer/tests/codetoanalyze/cpp/pulse/closures.cpp index dd9456178..6265d52d3 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/closures.cpp +++ b/infer/tests/codetoanalyze/cpp/pulse/closures.cpp @@ -13,7 +13,7 @@ struct S { ~S() {} }; -int FN_ref_capture_destroy_invoke_bad() { +int ref_capture_destroy_invoke_bad() { std::function f; { S s; @@ -22,7 +22,7 @@ int FN_ref_capture_destroy_invoke_bad() { return f(); // s used here } -int FN_implicit_ref_capture_destroy_invoke_bad() { +int implicit_ref_capture_destroy_invoke_bad() { std::function f; { auto s = S(); @@ -44,7 +44,7 @@ int FN_reassign_lambda_capture_destroy_invoke_bad() { // frontend doesn't understand difference between capture-by-value and // capture-by-ref, need to fix -int value_capture_destroy_invoke_ok() { +int FP_value_capture_destroy_invoke_ok() { std::function f; { S s; @@ -54,7 +54,7 @@ int value_capture_destroy_invoke_ok() { } // same thing here -int implicit_value_capture_destroy_invoke_ok() { +int FP_implicit_value_capture_destroy_invoke_ok() { std::function f; { S s; diff --git a/infer/tests/codetoanalyze/cpp/pulse/issues.exp b/infer/tests/codetoanalyze/cpp/pulse/issues.exp index 4e38d1651..65a32c9e3 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/issues.exp +++ b/infer/tests/codetoanalyze/cpp/pulse/issues.exp @@ -1,5 +1,9 @@ codetoanalyze/cpp/pulse/basics.cpp, multiple_invalidations_branch_bad, 6, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,invalid access occurs here here] codetoanalyze/cpp/pulse/basics.cpp, multiple_invalidations_loop_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,invalid access occurs here here] +codetoanalyze/cpp/pulse/closures.cpp, FP_implicit_value_capture_destroy_invoke_ok, 6, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidation part of the trace starts here,variable declared,memory is the address of a stack variable `s` whose lifetime has ended here,use-after-lifetime part of the trace starts here,value captured as `&s`,invalid access occurs here here] +codetoanalyze/cpp/pulse/closures.cpp, FP_value_capture_destroy_invoke_ok, 6, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidation part of the trace starts here,variable declared,memory is the address of a stack variable `s` whose lifetime has ended here,use-after-lifetime part of the trace starts here,value captured as `&s`,invalid access occurs here here] +codetoanalyze/cpp/pulse/closures.cpp, implicit_ref_capture_destroy_invoke_bad, 6, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidation part of the trace starts here,variable declared,memory is the address of a stack variable `s` whose lifetime has ended here,use-after-lifetime part of the trace starts here,variable declared,value captured as `&s`,invalid access occurs here here] +codetoanalyze/cpp/pulse/closures.cpp, ref_capture_destroy_invoke_bad, 6, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidation part of the trace starts here,variable declared,memory is the address of a stack variable `s` whose lifetime has ended here,use-after-lifetime part of the trace starts here,variable declared,value captured as `&s`,invalid access occurs here here] codetoanalyze/cpp/pulse/deduplication.cpp, deduplication::SomeTemplatedClass::lifetime_error_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `templated_wrapper_delete_ok` here,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,when calling `templated_wrapper_access_ok` here,invalid access occurs here here] codetoanalyze/cpp/pulse/deduplication.cpp, deduplication::SomeTemplatedClass::lifetime_error_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `templated_wrapper_delete_ok` here,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,when calling `templated_wrapper_access_ok` here,invalid access occurs here here] codetoanalyze/cpp/pulse/deduplication.cpp, deduplication::templated_function_bad<_Bool>, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `deduplication::templated_delete_function` here,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,assigned,when calling `deduplication::templated_access_function` here,invalid access occurs here here]