diff --git a/infer/src/pulse/Pulse.ml b/infer/src/pulse/Pulse.ml index 55fcfa2c6..c8a25ee64 100644 --- a/infer/src/pulse/Pulse.ml +++ b/infer/src/pulse/Pulse.ml @@ -216,10 +216,7 @@ module PulseTransferFunctions = struct [post] | Metadata (VariableLifetimeBegins (pvar, _, location)) -> let var = Var.of_pvar pvar in - let post = - PulseOperations.havoc_var [PulseTrace.VariableDeclaration location] var astate - |> PulseOperations.record_var_decl_location location var - in + let post = PulseOperations.realloc_var var location astate in [post] | Metadata (Abstract _ | Nullify _ | Skip) -> [astate] diff --git a/infer/src/pulse/PulseOperations.ml b/infer/src/pulse/PulseOperations.ml index 6c0d1f345..64ca64078 100644 --- a/infer/src/pulse/PulseOperations.ml +++ b/infer/src/pulse/PulseOperations.ml @@ -171,6 +171,10 @@ let overwrite_address astate access_expr new_addr_trace = (** Add the given address to the set of know invalid addresses. *) let mark_invalid action address astate = Memory.invalidate address action astate +let realloc_var var location astate = + Stack.add var (AbstractAddress.mk_fresh (), Some location) astate + + let havoc_var trace var astate = write_var var (AbstractAddress.mk_fresh (), trace) astate let havoc trace location (access_expr : HilExp.AccessExpression.t) astate = @@ -260,17 +264,6 @@ let remove_vars vars astate = if phys_equal astate' astate then astate else PulseAbductiveDomain.discard_unreachable astate' -let record_var_decl_location location var astate = - let addr = - match Stack.find_opt var astate with - | Some (addr, _) -> - addr - | None -> - AbstractAddress.mk_fresh () - in - Stack.add var (addr, Some location) astate - - module Closures = struct open Result.Monad_infix module Memory = PulseAbductiveDomain.Memory diff --git a/infer/src/pulse/PulseOperations.mli b/infer/src/pulse/PulseOperations.mli index 3406678c5..e455122fc 100644 --- a/infer/src/pulse/PulseOperations.mli +++ b/infer/src/pulse/PulseOperations.mli @@ -49,6 +49,8 @@ val havoc_var : PulseTrace.t -> Var.t -> t -> t val havoc : PulseTrace.t -> Location.t -> HilExp.AccessExpression.t -> t -> t access_result +val realloc_var : Var.t -> Location.t -> t -> t + val write_var : Var.t -> AbstractAddress.t * PulseTrace.t -> t -> t val write : @@ -72,8 +74,6 @@ val invalidate_array_elements : -> t -> t access_result -val record_var_decl_location : Location.t -> Var.t -> t -> t - val remove_vars : Var.t list -> t -> t (* TODO: better name and pass location to report where we returned *) diff --git a/infer/tests/codetoanalyze/cpp/pulse/issues.exp b/infer/tests/codetoanalyze/cpp/pulse/issues.exp index c894afc1e..6726ed708 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/issues.exp +++ b/infer/tests/codetoanalyze/cpp/pulse/issues.exp @@ -1,16 +1,12 @@ -codetoanalyze/cpp/pulse/basics.cpp, aggregate_reassign2_ok, 5, USE_AFTER_LIFETIME, no_bucket, ERROR, [variable declared,invalidated `&(a)` gone out of scope here,accessed `a.str` here] -codetoanalyze/cpp/pulse/basics.cpp, aggregate_reassign3_ok, 5, USE_AFTER_LIFETIME, no_bucket, ERROR, [variable declared,invalidated `&(a)` gone out of scope here,accessed `a.a.str` here] -codetoanalyze/cpp/pulse/basics.cpp, aggregate_reassign_ok, 4, USE_AFTER_LIFETIME, no_bucket, ERROR, [variable declared,invalidated `&(s)` gone out of scope here,accessed `s.i` here] codetoanalyze/cpp/pulse/basics.cpp, multiple_invalidations_branch_bad, 6, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by `delete` on `ptr` here,accessed `*(ptr)` here] codetoanalyze/cpp/pulse/basics.cpp, multiple_invalidations_loop_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by `delete` on `ptr` here,accessed `ptr` here] -codetoanalyze/cpp/pulse/closures.cpp, implicit_ref_capture_destroy_invoke_bad, 6, USE_AFTER_LIFETIME, no_bucket, ERROR, [variable declared,`&(s)` captured as `s`,invalidated `s` gone out of scope here,accessed `&(f)` here] -codetoanalyze/cpp/pulse/closures.cpp, ref_capture_destroy_invoke_bad, 6, USE_AFTER_LIFETIME, no_bucket, ERROR, [variable declared,`&(s)` captured as `s`,invalidated `s` gone out of scope here,accessed `&(f)` here] +codetoanalyze/cpp/pulse/closures.cpp, implicit_ref_capture_destroy_invoke_bad, 6, USE_AFTER_LIFETIME, no_bucket, ERROR, [`&(s)` captured as `s`,invalidated `s` gone out of scope here,accessed `&(f)` here] +codetoanalyze/cpp/pulse/closures.cpp, ref_capture_destroy_invoke_bad, 6, USE_AFTER_LIFETIME, no_bucket, ERROR, [`&(s)` captured as `s`,invalidated `s` gone out of scope here,accessed `&(f)` here] codetoanalyze/cpp/pulse/interprocedural.cpp, delete_inner_then_write_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated during call to `wraps_delete_inner` here,invalidated by `delete` on `x` here,accessed during call to `wraps_read` here,accessed during call to `wraps_read_inner` here,accessed `x->f` here] codetoanalyze/cpp/pulse/interprocedural.cpp, delete_then_read_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by `delete` on `x` here,accessed during call to `wraps_read` here,accessed during call to `wraps_read_inner` here,accessed `x->f` here] codetoanalyze/cpp/pulse/interprocedural.cpp, delete_then_write_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated during call to `wraps_delete` here,invalidated during call to `wraps_delete_inner` here,invalidated by `delete` on `x` here,accessed during call to `wraps_read` here,accessed during call to `wraps_read_inner` here,accessed `x->f` here] codetoanalyze/cpp/pulse/interprocedural.cpp, feed_invalid_into_access_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [assigned to `y`,assigned to `return`,returned from call to `may_return_invalid_ptr_ok()`,assigned to `y`,invalidated during call to `may_return_invalid_ptr_ok` here,invalidated by `delete` on `y` here,accessed during call to `call_store` here,accessed during call to `store` here,accessed `y->p` here] codetoanalyze/cpp/pulse/join.cpp, invalidate_node_alias_bad, 12, USE_AFTER_DELETE, no_bucket, ERROR, [assigned to `result`,invalidated by `delete` on `result` here,accessed `*(result)` here] -codetoanalyze/cpp/pulse/reference_wrapper.cpp, reference_wrapper_stack_bad, 2, USE_AFTER_LIFETIME, no_bucket, ERROR, [assigned to `this->b`,returned from call to `ReferenceWrapperStack::ReferenceWrapperStack()`,invalidated during call to `getwrapperStack` here,invalidated `&(b)` gone out of scope here,accessed `rw.b->f` here] codetoanalyze/cpp/pulse/returns.cpp, returns::return_literal_stack_reference_bad, 0, STACK_VARIABLE_ADDRESS_ESCAPE, no_bucket, ERROR, [] codetoanalyze/cpp/pulse/returns.cpp, returns::return_stack_pointer_bad, 1, STACK_VARIABLE_ADDRESS_ESCAPE, no_bucket, ERROR, [] codetoanalyze/cpp/pulse/returns.cpp, returns::return_variable_stack_reference1_bad, 1, STACK_VARIABLE_ADDRESS_ESCAPE, no_bucket, ERROR, [] diff --git a/infer/tests/codetoanalyze/cpp/pulse/reference_wrapper.cpp b/infer/tests/codetoanalyze/cpp/pulse/reference_wrapper.cpp index 87f4f298e..9b1ff26f3 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/reference_wrapper.cpp +++ b/infer/tests/codetoanalyze/cpp/pulse/reference_wrapper.cpp @@ -42,7 +42,7 @@ ReferenceWrapperStack getwrapperStack() { return b; } -int reference_wrapper_stack_bad() { +int FN_reference_wrapper_stack_bad() { ReferenceWrapperStack rw = getwrapperStack(); return rw.b->f; // we want to report use after lifetime bug here } diff --git a/infer/tests/codetoanalyze/cpp/pulse/use_after_destructor.cpp b/infer/tests/codetoanalyze/cpp/pulse/use_after_destructor.cpp index 3d7aad3bb..d010c42ea 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/use_after_destructor.cpp +++ b/infer/tests/codetoanalyze/cpp/pulse/use_after_destructor.cpp @@ -251,4 +251,12 @@ std::unique_ptr* allocate_in_branch_ok(bool b) { const B* read = (*a3)->f; } +std::string mk_string(); + +bool variable_init_ternary_ok(bool b) { + // this can cause issues because of the way the frontend treatment of ternary ?: interacts with + // the treatment of passing return values by reference as parameters + std::string newPath = b ? "" : mk_string(); +} + } // namespace use_after_destructor