diff --git a/infer/src/checkers/PulseDomain.ml b/infer/src/checkers/PulseDomain.ml index 9c79a94d2..9179173c0 100644 --- a/infer/src/checkers/PulseDomain.ml +++ b/infer/src/checkers/PulseDomain.ml @@ -548,28 +548,38 @@ module Operations = struct and return [new_addr] if [overwrite_last] is [Some new_addr], or go until the end of the path if it is [None]. Create more addresses into the heap as needed to follow the [path]. Check that each address reached is valid. *) - let rec walk actor ~on_last addr path astate = + let rec walk ~dereference_to_ignore actor ~on_last addr path astate = + let check_addr_access_optional actor addr astate = + match dereference_to_ignore with + | Some 0 -> + Ok astate + | _ -> + check_addr_access actor addr astate + in match (path, on_last) with | [], `Access -> Ok (astate, addr) | [], `Overwrite _ -> L.die InternalError "Cannot overwrite last address in empty path" | [a], `Overwrite new_addr -> - check_addr_access actor addr astate + check_addr_access_optional actor addr astate >>| fun astate -> let heap = Memory.add_edge_and_back_edge addr a new_addr astate.heap in ({astate with heap}, new_addr) | a :: path, _ -> ( - check_addr_access actor addr astate + check_addr_access_optional actor addr astate >>= fun astate -> + let dereference_to_ignore = + Option.map ~f:(fun index -> max 0 (index - 1)) dereference_to_ignore + in match Memory.find_edge_opt addr a astate.heap with | None -> let addr' = AbstractAddress.mk_fresh () in let heap = Memory.add_edge_and_back_edge addr a addr' astate.heap in let astate = {astate with heap} in - walk actor ~on_last addr' path astate + walk ~dereference_to_ignore actor ~on_last addr' path astate | Some addr' -> - walk actor ~on_last addr' path astate ) + walk ~dereference_to_ignore actor ~on_last addr' path astate ) let write_var var new_addr astate = @@ -587,6 +597,21 @@ module Operations = struct {astate with heap} + let ends_with_addressof = function HilExp.AccessExpression.AddressOf _ -> true | _ -> false + + let last_dereference access_list = + let rec last_dereference_inner access_list index result = + match access_list with + | [] -> + result + | HilExp.Access.Dereference :: rest -> + last_dereference_inner rest (index + 1) (Some index) + | _ :: rest -> + last_dereference_inner rest (index + 1) result + in + last_dereference_inner access_list 0 None + + let rec to_accesses location access_expr astate = let exception Failed_fold of Diagnostic.t in try @@ -609,6 +634,9 @@ module Operations = struct and walk_access_expr ~on_last astate access_expr location = to_accesses location access_expr astate >>= fun (astate, (access_var, _), access_list) -> + let dereference_to_ignore = + if ends_with_addressof access_expr then last_dereference access_list else None + in if Config.write_html then L.d_printfln "Accessing %a -> [%a]" Var.pp access_var (Pp.seq ~sep:"," Memory.Access.pp) @@ -631,7 +659,9 @@ module Operations = struct Ok (astate, base_addr) | _ -> let actor = {access_expr; location} in - walk actor ~on_last base_addr (HilExp.Access.Dereference :: access_list) astate ) + walk ~dereference_to_ignore actor ~on_last base_addr + (HilExp.Access.Dereference :: access_list) + astate ) (** Use the stack and heap to walk the access path represented by the given expression down to an diff --git a/infer/tests/codetoanalyze/cpp/pulse/issues.exp b/infer/tests/codetoanalyze/cpp/pulse/issues.exp index 1b765a7e5..3dd35038b 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/issues.exp +++ b/infer/tests/codetoanalyze/cpp/pulse/issues.exp @@ -13,11 +13,11 @@ codetoanalyze/cpp/pulse/use_after_delete.cpp, return_deleted_bad, 3, USE_AFTER_D codetoanalyze/cpp/pulse/use_after_delete.cpp, use_in_branch_bad, 4, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete s` at line 73, column 3 here,accessed `s` here] codetoanalyze/cpp/pulse/use_after_delete.cpp, use_in_loop_bad, 4, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete s` at line 102, column 3 here,accessed `s->f` here] codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::double_destructor_bad, 5, USE_AFTER_DESTRUCTOR, no_bucket, ERROR, [invalidated by destructor call `use_after_destructor::S_~S(s)` at line 64, column 3 here,accessed `s` here] -codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::placement_new_aliasing1_bad, 5, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete alias` at line 142, column 3 here,accessed `s` here] -codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::placement_new_aliasing2_bad, 5, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete s` at line 150, column 3 here,accessed `alias` here] -codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::placement_new_aliasing3_bad, 6, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete s` at line 159, column 3 here,accessed `alias` here] +codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::placement_new_aliasing1_bad, 5, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete alias` at line 148, column 3 here,accessed `s` here] +codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::placement_new_aliasing2_bad, 5, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete s` at line 156, column 3 here,accessed `alias` here] +codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::placement_new_aliasing3_bad, 6, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete s` at line 165, column 3 here,accessed `alias` here] codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::use_after_destructor_bad, 3, USE_AFTER_DESTRUCTOR, no_bucket, ERROR, [invalidated by destructor call `use_after_destructor::S_~S(s)` at line 71, column 3 here,accessed `*(s.f)` here] -codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::use_after_scope4_bad, 6, USE_AFTER_DESTRUCTOR, no_bucket, ERROR, [invalidated by destructor call `use_after_destructor::C_~C(c)` at line 204, column 3 here,accessed `pc->f` here] +codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::use_after_scope4_bad, 6, USE_AFTER_DESTRUCTOR, no_bucket, ERROR, [invalidated by destructor call `use_after_destructor::C_~C(c)` at line 210, column 3 here,accessed `pc->f` here] codetoanalyze/cpp/pulse/use_after_free.cpp, use_after_free_simple_bad, 2, USE_AFTER_FREE, no_bucket, ERROR, [invalidated by call to `free(x)` at line 10, column 3 here,accessed `*(x)` here] 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, VectorA_FP_push_back_value_field_ok, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [potentially invalidated by call to `std::vector::push_back(vec, ..)` at line 126, column 5 here,accessed `&(this->x)` here] diff --git a/infer/tests/codetoanalyze/cpp/pulse/use_after_destructor.cpp b/infer/tests/codetoanalyze/cpp/pulse/use_after_destructor.cpp index 35b6ca1fa..85ecdbd88 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/use_after_destructor.cpp +++ b/infer/tests/codetoanalyze/cpp/pulse/use_after_destructor.cpp @@ -135,6 +135,12 @@ S* destruct_pointer_contents_then_placement_new1_ok(S* s) { return s; } +S* destruct_pointer_contents_then_placement_new2_ok(S* s) { + s->~S(); + new (&(s->f)) S(1); + return s; +} + S* placement_new_aliasing1_bad() { S* s = new S(1); s->~S();