From 220d29766d0a17784d21f6815e6db7b268b6a7ff Mon Sep 17 00:00:00 2001 From: Daiva Naudziuniene Date: Thu, 13 Dec 2018 05:49:29 -0800 Subject: [PATCH] [pulse] Model stack as a map from addresses of variables Summary: When we create Dereference edge, we also create TakeAddress back edge. This causes false positives for stack variables. When we write to a stack variable and then take its address, the resulting address is the one from the back edge of the written value. See example `push_back_value_ok`. To solve this issue, this diff changes stack to denote a map from address of variables rather than from variables. We still have issue for fields, see example, FP_push_back_value_field_ok. To solve this, we probably need to remove back edges. Reviewed By: jvillard Differential Revision: D13432415 fbshipit-source-id: 9254a1a6d --- infer/src/checkers/PulseDomain.ml | 41 +++++++++++-------- .../tests/codetoanalyze/cpp/pulse/issues.exp | 1 + .../tests/codetoanalyze/cpp/pulse/vector.cpp | 18 ++++++++ 3 files changed, 42 insertions(+), 18 deletions(-) diff --git a/infer/src/checkers/PulseDomain.ml b/infer/src/checkers/PulseDomain.ml index a80fe0411..9c79a94d2 100644 --- a/infer/src/checkers/PulseDomain.ml +++ b/infer/src/checkers/PulseDomain.ml @@ -214,7 +214,7 @@ end = struct let fold = Graph.fold end -(** Stacks: map variables to values. +(** Stacks: map addresses of variables to values. This is defined as an abstract domain but the domain operations are mostly meaningless on their own. It so happens that the join on abstract states uses the join of stacks provided by this @@ -572,9 +572,19 @@ module Operations = struct walk actor ~on_last addr' path astate ) - let write_var var addr astate = - let stack = Stack.add var addr astate.stack in - {astate with stack} + let write_var var new_addr astate = + let astate, var_address_of = + match Stack.find_opt var astate.stack with + | Some addr -> + (astate, addr) + | None -> + let addr = AbstractAddress.mk_fresh () in + let stack = Stack.add var addr astate.stack in + ({astate with stack}, addr) + in + (* Update heap with var_address_of -*-> new_addr *) + let heap = Memory.add_edge var_address_of HilExp.Access.Dereference new_addr astate.heap in + {astate with heap} let rec to_accesses location access_expr astate = @@ -606,7 +616,7 @@ module Operations = struct match (on_last, access_list) with | `Overwrite new_addr, [] -> Ok (write_var access_var new_addr astate, new_addr) - | `Access, _ | `Overwrite _, _ :: _ -> + | `Access, _ | `Overwrite _, _ :: _ -> ( let astate, base_addr = match Stack.find_opt access_var astate.stack with | Some addr -> @@ -616,8 +626,12 @@ module Operations = struct let stack = Stack.add access_var addr astate.stack in ({astate with stack}, addr) in - let actor = {access_expr; location} in - walk actor ~on_last base_addr access_list astate + match access_list with + | [HilExp.Access.TakeAddress] -> + Ok (astate, base_addr) + | _ -> + let actor = {access_expr; location} in + walk 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 @@ -662,19 +676,10 @@ module Operations = struct {astate with heap= Memory.invalidate address actor astate.heap} - let havoc_var var astate = - {astate with stack= Stack.add var (AbstractAddress.mk_fresh ()) astate.stack} - + let havoc_var var astate = write_var var (AbstractAddress.mk_fresh ()) astate let havoc location (access_expr : HilExp.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 + overwrite_address astate access_expr (AbstractAddress.mk_fresh ()) location >>| fst let write location access_expr addr astate = diff --git a/infer/tests/codetoanalyze/cpp/pulse/issues.exp b/infer/tests/codetoanalyze/cpp/pulse/issues.exp index 7861b8ae1..1b765a7e5 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/issues.exp +++ b/infer/tests/codetoanalyze/cpp/pulse/issues.exp @@ -20,6 +20,7 @@ codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::use_afte 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_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] codetoanalyze/cpp/pulse/vector.cpp, assign_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [potentially invalidated by call to `std::vector::assign(vec, ..)` at line 83, column 3 here,accessed `*(elt)` here] codetoanalyze/cpp/pulse/vector.cpp, clear_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [potentially invalidated by call to `std::vector::clear(vec, ..)` at line 77, column 3 here,accessed `*(elt)` here] codetoanalyze/cpp/pulse/vector.cpp, deref_local_vector_element_after_push_back_bad, 4, VECTOR_INVALIDATION, no_bucket, ERROR, [potentially invalidated by call to `std::vector::push_back(&(vec), ..)` at line 19, 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 e000d5e0f..7f082884d 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/vector.cpp +++ b/infer/tests/codetoanalyze/cpp/pulse/vector.cpp @@ -109,3 +109,21 @@ void FN_emplace_back_bad(std::vector& vec) { // (T37883260) std::cout << *elt << "\n"; } + +void f(int&); + +void push_back_value_ok(std::vector& vec) { + int x = vec[0]; + vec.push_back(7); + f(x); +} + +struct VectorA { + int x; + + void FP_push_back_value_field_ok(std::vector& vec) { + x = vec[0]; + vec.push_back(7); + f(x); + } +};