From cf66ea0afb7025451f297076889435082774dcd2 Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Fri, 26 Oct 2018 07:30:22 -0700 Subject: [PATCH] [pulse] havoc vector array on push_back Summary: Turns out once a vector array became invalid it stayed that way, instead of the vector getting a new valid internal array. Reviewed By: skcho Differential Revision: D10853532 fbshipit-source-id: f6f22407f --- infer/src/checkers/Pulse.ml | 22 ++------ infer/src/checkers/PulseDomain.ml | 47 ++++++++++------ infer/src/checkers/PulseDomain.mli | 4 +- infer/src/checkers/PulseModels.ml | 12 ++-- .../tests/codetoanalyze/cpp/pulse/issues.exp | 10 +++- .../tests/codetoanalyze/cpp/pulse/vector.cpp | 56 ++++++++++++++++--- 6 files changed, 101 insertions(+), 50 deletions(-) diff --git a/infer/src/checkers/Pulse.ml b/infer/src/checkers/Pulse.ml index 93b0c04da..cc1aec51b 100644 --- a/infer/src/checkers/Pulse.ml +++ b/infer/src/checkers/Pulse.ml @@ -66,7 +66,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct in match model with | None -> - exec_call ret call actuals _flags call_loc astate >>| PulseDomain.havoc (fst ret) + exec_call ret call actuals _flags call_loc astate >>| PulseDomain.havoc_var (fst ret) | Some model -> model call_loc ~ret ~actuals astate @@ -76,28 +76,18 @@ module TransferFunctions (CFG : ProcCfg.S) = struct match instr with | Assign (lhs_access, rhs_exp, loc) -> (* try to evaluate [rhs_exp] down to an abstract address or generate a fresh one *) - let rhs_result = + let result = match rhs_exp with | AccessExpression rhs_access -> PulseDomain.read loc rhs_access astate + >>= fun (astate, rhs_value) -> PulseDomain.write loc lhs_access rhs_value astate | Constant (Cint address) when IntLit.iszero address -> - Ok (astate, PulseDomain.AbstractAddress.nullptr) + PulseDomain.write loc lhs_access PulseDomain.AbstractAddress.nullptr astate | _ -> PulseDomain.read_all loc (HilExp.get_access_exprs rhs_exp) astate - >>= fun astate -> - Ok - ( astate - , (* TODO: we could avoid creating and recording a fresh location whenever - [lhs_access] is not already present in the state so that we keep its - evaluation lazy, which would have the same semantic result but won't make the - state grow needlessly in case we never need that value again. We would just - need to add a function {!PulseDomain.freshen access_expr} that does the lazy - refreshing and use it instead of {!PulseDomain.write} below in this case. *) - PulseDomain.AbstractAddress.mk_fresh () ) + >>= PulseDomain.havoc loc lhs_access in - Result.bind rhs_result ~f:(fun (astate, rhs_value) -> - PulseDomain.write loc lhs_access rhs_value astate ) - |> check_error summary + check_error summary result | Assume (condition, _, _, loc) -> PulseDomain.read_all loc (HilExp.get_access_exprs condition) astate |> check_error summary | Call (ret, call, actuals, flags, loc) -> diff --git a/infer/src/checkers/PulseDomain.ml b/infer/src/checkers/PulseDomain.ml index 79106df08..d3314559c 100644 --- a/infer/src/checkers/PulseDomain.ml +++ b/infer/src/checkers/PulseDomain.ml @@ -440,13 +440,13 @@ 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 ~overwrite_last addr path astate = - match (path, overwrite_last) with - | [], None -> + let rec walk actor ~on_last addr path astate = + match (path, on_last) with + | [], `Access -> Ok (astate, addr) - | [], Some _ -> + | [], `Overwrite _ -> L.die InternalError "Cannot overwrite last address in empty path" - | [a], Some new_addr -> + | [a], `Overwrite new_addr -> check_addr_access actor addr astate >>| fun astate -> let heap = Memory.add_edge_and_back_edge addr a new_addr astate.heap in @@ -459,24 +459,24 @@ module Operations = struct 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 ~overwrite_last addr' path astate + walk actor ~on_last addr' path astate | Some addr' -> - walk actor ~overwrite_last addr' path astate ) + walk actor ~on_last addr' path astate ) (** add addresses to the state to give a address to the destination of the given access path *) - let walk_access_expr ?overwrite_last astate access_expr location = + let walk_access_expr ~on_last astate access_expr location = let (access_var, _), access_list = AccessExpression.to_accesses access_expr in if Config.write_html then L.d_strln (F.asprintf "Accessing %a -> [%a]" Var.pp access_var (Pp.seq ~sep:"," AccessExpression.Access.pp) access_list) ; - match (overwrite_last, access_list) with - | Some new_addr, [] -> + match (on_last, access_list) with + | `Overwrite new_addr, [] -> let stack = AliasingDomain.add access_var new_addr astate.stack in Ok ({astate with stack}, new_addr) - | None, _ | Some _, _ :: _ -> + | `Access, _ | `Overwrite _, _ :: _ -> let astate, base_addr = match AliasingDomain.find_opt access_var astate.stack with | Some addr -> @@ -487,7 +487,7 @@ module Operations = struct ({astate with stack}, addr) in let actor = {access_expr; location} in - walk actor ~overwrite_last base_addr access_list astate + walk actor ~on_last base_addr access_list astate (** Use the stack and heap to walk the access path represented by the given expression down to an @@ -495,7 +495,7 @@ module Operations = struct Return an error state if it traverses some known invalid address or if the end destination is known to be invalid. *) - let materialize_address astate access_expr = walk_access_expr astate access_expr + let materialize_address astate access_expr = walk_access_expr ~on_last:`Access astate access_expr (** Use the stack and heap to walk the access path represented by the given expression down to an abstract address representing what the expression points to, and replace that with the given @@ -503,7 +503,7 @@ module Operations = struct Return an error state if it traverses some known invalid address. *) let overwrite_address astate access_expr new_addr = - walk_access_expr ~overwrite_last:new_addr astate access_expr + walk_access_expr ~on_last:(`Overwrite new_addr) astate access_expr (** Add the given address to the set of know invalid addresses. *) @@ -511,6 +511,23 @@ module Operations = struct {astate with invalids= InvalidAddressesDomain.add address actor astate.invalids} + let havoc_var var astate = + if AliasingDomain.mem var astate.stack then + {astate with stack= AliasingDomain.remove var astate.stack} + else astate + + + let havoc location (access_expr : AccessExpression.t) astate = + match access_expr with + | Base (access_var, _) -> + havoc_var access_var astate |> Result.return + | _ -> + walk_access_expr + ~on_last:(`Overwrite (AbstractAddress.mk_fresh ())) + astate access_expr location + >>| fst + + let read location access_expr astate = materialize_address astate access_expr location >>= fun (astate, addr) -> @@ -527,8 +544,6 @@ module Operations = struct overwrite_address astate access_expr addr location >>| fun (astate, _) -> astate - let havoc var astate = {astate with stack= AliasingDomain.remove var astate.stack} - let invalidate cause location access_expr astate = materialize_address astate access_expr location >>= fun (astate, addr) -> diff --git a/infer/src/checkers/PulseDomain.mli b/infer/src/checkers/PulseDomain.mli index b54f75e7d..78a1cbd6a 100644 --- a/infer/src/checkers/PulseDomain.mli +++ b/infer/src/checkers/PulseDomain.mli @@ -39,7 +39,9 @@ val read : Location.t -> AccessExpression.t -> t -> (t * AbstractAddress.t) acce val read_all : Location.t -> AccessExpression.t list -> t -> t access_result -val havoc : Var.t -> t -> t +val havoc_var : Var.t -> t -> t + +val havoc : Location.t -> AccessExpression.t -> t -> t access_result val write : Location.t -> AccessExpression.t -> AbstractAddress.t -> t -> t access_result diff --git a/infer/src/checkers/PulseModels.ml b/infer/src/checkers/PulseModels.ml index 4cfa63557..0196860dd 100644 --- a/infer/src/checkers/PulseModels.ml +++ b/infer/src/checkers/PulseModels.ml @@ -67,7 +67,9 @@ module StdVector = struct let deref_internal_array vector = AccessExpression.ArrayOffset - (AccessExpression.FieldOffset (vector, internal_array), Typ.void, []) + ( AccessExpression.Dereference (AccessExpression.FieldOffset (vector, internal_array)) + , Typ.void + , [] ) let at : model = @@ -77,16 +79,16 @@ module StdVector = struct PulseDomain.read location (deref_internal_array vector) astate >>= fun (astate, loc) -> PulseDomain.write location (AccessExpression.Base ret) loc astate | _ -> - Ok (PulseDomain.havoc (fst ret) astate) + Ok (PulseDomain.havoc_var (fst ret) astate) let push_back : model = fun location ~ret:_ ~actuals astate -> match actuals with | [AccessExpression vector; _value] -> - PulseDomain.invalidate - (StdVectorPushBack (vector, location)) - location (deref_internal_array vector) astate + let deref_array = deref_internal_array vector in + PulseDomain.invalidate (StdVectorPushBack (vector, location)) location deref_array astate + >>= PulseDomain.havoc location deref_array | _ -> Ok astate end diff --git a/infer/tests/codetoanalyze/cpp/pulse/issues.exp b/infer/tests/codetoanalyze/cpp/pulse/issues.exp index 3fff821a9..e79872112 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/issues.exp +++ b/infer/tests/codetoanalyze/cpp/pulse/issues.exp @@ -9,7 +9,7 @@ codetoanalyze/cpp/ownership/returns.cpp, returns::FN_return_destructed_pointer_b codetoanalyze/cpp/ownership/returns.cpp, returns::return_deleted_bad, 4, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete x` at line 112, column 3 here,accessed `x` here] codetoanalyze/cpp/ownership/use_after_delete.cpp, delete_in_branch_bad, 5, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete s` at line 57, column 5 here,accessed `s` here] codetoanalyze/cpp/ownership/use_after_delete.cpp, delete_in_loop_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete s` at line 82, column 5 here,accessed `s` here] -codetoanalyze/cpp/ownership/use_after_delete.cpp, delete_ref_in_loop_ok, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete s` at line 97, column 5 here,accessed `v.__internal_array[_]` here] +codetoanalyze/cpp/ownership/use_after_delete.cpp, delete_ref_in_loop_ok, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete s` at line 97, column 5 here,accessed `*(v.__internal_array)[_]` here] codetoanalyze/cpp/ownership/use_after_delete.cpp, deref_deleted_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete s` at line 18, column 3 here,accessed `s` here] codetoanalyze/cpp/ownership/use_after_delete.cpp, double_delete_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete s` at line 50, column 3 here,accessed `s` here] codetoanalyze/cpp/ownership/use_after_delete.cpp, gated_delete_abort_ok, 6, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete s` at line 112, column 5 here,accessed `s` here] @@ -29,5 +29,9 @@ codetoanalyze/cpp/ownership/use_after_destructor.cpp, use_after_destructor_bad, codetoanalyze/cpp/ownership/use_after_destructor.cpp, use_after_scope4_bad, 6, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated by destructor call `C_~C(&(c))` at line 186, column 3 here,accessed `pc->f` here] codetoanalyze/cpp/pulse/join.cpp, visit_list, 11, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete result` at line 21, column 5 here,accessed `*(result)` 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, deref_local_vector_element_after_lifetime_bad, 4, USE_AFTER_LIFETIME, no_bucket, ERROR, [potentially invalidated by call to `std::vector::push_back(&(x), ..)` at line 19, column 3 here,accessed `*(y)` here] -codetoanalyze/cpp/pulse/vector.cpp, deref_vector_element_after_lifetime_bad, 3, USE_AFTER_LIFETIME, no_bucket, ERROR, [potentially invalidated by call to `std::vector::push_back(x, ..)` at line 12, column 3 here,accessed `*(y)` here] +codetoanalyze/cpp/pulse/vector.cpp, FP_init_fill_then_push_back_loop_ok, 6, USE_AFTER_LIFETIME, no_bucket, ERROR, [potentially invalidated by call to `std::vector::push_back(&(vec), ..)` at line 56, column 5 here,accessed `*(elt)` here] +codetoanalyze/cpp/pulse/vector.cpp, FP_push_back_in_loop_ok, 3, USE_AFTER_LIFETIME, no_bucket, ERROR, [potentially invalidated by call to `std::vector::push_back(vec, ..)` at line 31, column 5 here,accessed `*(vec.__internal_array)[_]` here] +codetoanalyze/cpp/pulse/vector.cpp, FP_reserve_then_push_back_loop_ok, 7, USE_AFTER_LIFETIME, no_bucket, ERROR, [potentially invalidated by call to `std::vector::push_back(vec, ..)` at line 47, column 5 here,accessed `*(elt)` here] +codetoanalyze/cpp/pulse/vector.cpp, FP_reserve_then_push_back_ok, 4, USE_AFTER_LIFETIME, no_bucket, ERROR, [potentially invalidated by call to `std::vector::push_back(vec, ..)` at line 38, column 3 here,accessed `*(elt)` here] +codetoanalyze/cpp/pulse/vector.cpp, deref_local_vector_element_after_push_back_bad, 4, USE_AFTER_LIFETIME, no_bucket, ERROR, [potentially invalidated by call to `std::vector::push_back(&(vec), ..)` at line 19, column 3 here,accessed `*(elt)` here] +codetoanalyze/cpp/pulse/vector.cpp, deref_vector_element_after_push_back_bad, 3, USE_AFTER_LIFETIME, no_bucket, ERROR, [potentially invalidated by call to `std::vector::push_back(vec, ..)` at line 12, column 3 here,accessed `*(elt)` here] diff --git a/infer/tests/codetoanalyze/cpp/pulse/vector.cpp b/infer/tests/codetoanalyze/cpp/pulse/vector.cpp index 8cca254d9..4b490a092 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/vector.cpp +++ b/infer/tests/codetoanalyze/cpp/pulse/vector.cpp @@ -7,15 +7,53 @@ #include #include -void deref_vector_element_after_lifetime_bad(std::vector& x) { - int* y = &x[1]; - x.push_back(42); - std::cout << *y << "\n"; +void deref_vector_element_after_push_back_bad(std::vector& vec) { + int* elt = &vec[1]; + vec.push_back(42); + std::cout << *elt << "\n"; } -void deref_local_vector_element_after_lifetime_bad() { - std::vector x = {0, 0}; - int* y = &x[1]; - x.push_back(42); - std::cout << *y << "\n"; +void deref_local_vector_element_after_push_back_bad() { + std::vector vec = {0, 0}; + int* elt = &vec[1]; + vec.push_back(42); + std::cout << *elt << "\n"; +} + +void two_push_back_ok(std::vector& vec) { + vec.push_back(32); + vec.push_back(52); +} + +void FP_push_back_in_loop_ok(std::vector& vec, + std::vector& vec_other) { + for (const auto& i : vec_other) { + vec.push_back(i); + } +} + +void FP_reserve_then_push_back_ok(std::vector& vec) { + vec.reserve(vec.size() + 1); + int* elt = &vec[1]; + vec.push_back(42); + std::cout << *elt << "\n"; +} + +void FP_reserve_then_push_back_loop_ok(std::vector& vec, + std::vector& vec_other) { + vec.reserve(vec.size() + vec_other.size()); + int* elt = &vec[1]; + for (const auto& i : vec_other) { + vec.push_back(i); + } + std::cout << *elt << "\n"; +} + +void FP_init_fill_then_push_back_loop_ok(std::vector& vec_other) { + std::vector vec(vec_other.size()); + int* elt = &vec[1]; + for (const auto& i : vec_other) { + vec.push_back(i); + } + std::cout << *elt << "\n"; }