From 31c2a39e8178e9a6a3365de4684c0dfa45391ef3 Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Thu, 11 Apr 2019 03:55:38 -0700 Subject: [PATCH] [pulse] tighten up summaries Summary: Only throw values to the pre if they can be followed from "abducible" variables: formals of the current method and globals. Because figuring out if a `Pvar.t` is a formal of the current procedure is actually a giant pain, hack something not too bad instead: pre-register all formals at the start of the analysis of the procedure. Then the only other variables we care about in the precondition are globals, which we can detect easily. This is mostly an optimisation (summaries won't include irrelevant "abduced" facts about the procedure's local variables anymore), but it also fixes a bug where we would sometimes overwrite things in the pre. I think that's why the tests improved. Reviewed By: ngorogiannis Differential Revision: D14753493 fbshipit-source-id: 08e73637f --- infer/src/pulse/Pulse.ml | 8 ++-- infer/src/pulse/PulseAbductiveDomain.ml | 45 +++++++++++++++---- infer/src/pulse/PulseAbductiveDomain.mli | 2 +- .../tests/codetoanalyze/cpp/pulse/issues.exp | 3 +- .../cpp/pulse/reference_wrapper.cpp | 4 +- .../tests/codetoanalyze/cpp/pulse/vector.cpp | 2 +- 6 files changed, 47 insertions(+), 17 deletions(-) diff --git a/infer/src/pulse/Pulse.ml b/infer/src/pulse/Pulse.ml index 5de1f0df5..0ee0a56f5 100644 --- a/infer/src/pulse/Pulse.ml +++ b/infer/src/pulse/Pulse.ml @@ -245,10 +245,10 @@ module DisjunctiveAnalyzer = let checker {Callbacks.proc_desc; tenv; summary} = let proc_data = ProcData.make proc_desc tenv summary in AbstractAddress.init () ; - match - DisjunctiveAnalyzer.compute_post proc_data - ~initial:(DisjunctiveTransferFunctions.Disjuncts.singleton PulseAbductiveDomain.empty) - with + let initial = + DisjunctiveTransferFunctions.Disjuncts.singleton (PulseAbductiveDomain.mk_initial proc_desc) + in + match DisjunctiveAnalyzer.compute_post proc_data ~initial with | Some posts -> Payload.update_summary (PulseSummary.of_posts (DisjunctiveTransferFunctions.Disjuncts.elements posts)) diff --git a/infer/src/pulse/PulseAbductiveDomain.ml b/infer/src/pulse/PulseAbductiveDomain.ml index a0e8a9264..3279cb38c 100644 --- a/infer/src/pulse/PulseAbductiveDomain.ml +++ b/infer/src/pulse/PulseAbductiveDomain.ml @@ -86,8 +86,9 @@ let ( <= ) ~lhs ~rhs = module Stack = struct - let is_abducible _var = - (* TODO: need to keep only formals + return variable + globals in the pre *) true + let is_abducible astate var = + (* HACK: formals are pre-registered in the initial state *) + BaseStack.mem var (astate.pre :> base_domain).stack || Var.is_global var (** [astate] with [astate.post.stack = f astate.post.stack] *) @@ -104,7 +105,9 @@ module Stack = struct let addr_loc_opt' = (AbstractAddress.mk_fresh (), None) in let post_stack = BaseStack.add var addr_loc_opt' (astate.post :> base_domain).stack in let pre = - if is_abducible var then + (* do not overwrite values of variables already in the pre *) + if (not (BaseStack.mem var (astate.pre :> base_domain).stack)) && is_abducible astate var + then let foot_stack = BaseStack.add var addr_loc_opt' (astate.pre :> base_domain).stack in let foot_heap = BaseMemory.register_address (fst addr_loc_opt') (astate.pre :> base_domain).heap @@ -120,8 +123,12 @@ module Stack = struct let remove_vars vars astate = + let vars_to_remove = + let is_in_pre var astate = BaseStack.mem var (astate.pre :> base_domain).stack in + List.filter vars ~f:(fun var -> not (is_in_pre var astate)) + in map_post_stack astate ~f:(fun stack -> - BaseStack.filter (fun var _ -> not (List.mem ~equal:Var.equal vars var)) stack ) + BaseStack.filter (fun var _ -> not (List.mem ~equal:Var.equal vars_to_remove var)) stack ) let fold f astate accum = BaseStack.fold f (astate.post :> base_domain).stack accum @@ -206,7 +213,31 @@ module Memory = struct module Edges = BaseMemory.Edges end -let empty = {post= Domain.empty; pre= InvertedDomain.empty} +let mk_initial proc_desc = + (* HACK: save the formals in the stacks of the pre and the post to remember which local variables + correspond to formals *) + let formals = + let proc_name = Procdesc.get_proc_name proc_desc in + let location = Some (Procdesc.get_loc proc_desc) in + Procdesc.get_formals proc_desc + |> List.map ~f:(fun (mangled, _) -> + let var = Var.of_pvar (Pvar.mk mangled proc_name) in + (var, (AbstractAddress.mk_fresh (), location)) ) + in + let initial_stack = + List.fold formals ~init:(InvertedDomain.empty :> PulseDomain.t).stack + ~f:(fun stack (formal, addr_loc) -> BaseStack.add formal addr_loc stack) + in + let pre = + let initial_heap = + List.fold formals ~init:(InvertedDomain.empty :> base_domain).heap + ~f:(fun heap (_, (addr, _)) -> BaseMemory.register_address addr heap) + in + InvertedDomain.make initial_stack initial_heap + in + let post = Domain.update ~stack:initial_stack Domain.empty in + {pre; post} + let discard_unreachable ({pre; post} as astate) = let pre_addresses = PulseDomain.visit (pre :> PulseDomain.t) in @@ -542,9 +573,7 @@ module PrePost = struct let record_post_for_return callee_proc_name call_loc pre_post ~ret call_state = let return_var = Var.of_pvar (Pvar.get_ret_pvar callee_proc_name) in - match - PulseDomain.Stack.find_opt return_var (pre_post.pre :> PulseDomain.t).PulseDomain.stack - with + match PulseDomain.Stack.find_opt return_var (pre_post.post :> PulseDomain.t).stack with | Some (addr_return, _) -> record_post_for_address callee_proc_name call_loc pre_post ~addr_callee:addr_return ~addr_caller:(fst ret) call_state diff --git a/infer/src/pulse/PulseAbductiveDomain.mli b/infer/src/pulse/PulseAbductiveDomain.mli index f8d9ce2f6..9b06367e4 100644 --- a/infer/src/pulse/PulseAbductiveDomain.mli +++ b/infer/src/pulse/PulseAbductiveDomain.mli @@ -16,7 +16,7 @@ module Attributes = PulseDomain.Attributes include AbstractDomain.NoJoin -val empty : t +val mk_initial : Procdesc.t -> t (** stack operations like {!PulseDomain.Stack} but that also take care of propagating facts to the precondition *) diff --git a/infer/tests/codetoanalyze/cpp/pulse/issues.exp b/infer/tests/codetoanalyze/cpp/pulse/issues.exp index b478adaf0..33b6df5b2 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/issues.exp +++ b/infer/tests/codetoanalyze/cpp/pulse/issues.exp @@ -10,6 +10,8 @@ codetoanalyze/cpp/pulse/interprocedural.cpp, delete_then_read_bad, 2, USE_AFTER_ codetoanalyze/cpp/pulse/interprocedural.cpp, delete_then_write_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [start of end of lifetime trace,invalidated by during call to `wraps_delete()` here,invalidated by during call to `wraps_delete_inner()` here,invalidated by `delete` on `x` here,start of use after lifetime trace,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, [start of end of lifetime trace,invalidated by during call to `may_return_invalid_ptr_ok()` here,invalidated by `delete` on `y` here,start of use after lifetime trace,accessed during call to `call_store()` here,accessed during call to `store()` here,accessed `y->p` here,start of value trace,assigned to `y`,assigned to `return`,returned from call to `may_return_invalid_ptr_ok()`,assigned to `y`] codetoanalyze/cpp/pulse/join.cpp, invalidate_node_alias_bad, 12, USE_AFTER_DELETE, no_bucket, ERROR, [start of end of lifetime trace,invalidated by `delete` on `result` here,start of use after lifetime trace,accessed `*(result)` here,start of value trace,assigned to `result`] +codetoanalyze/cpp/pulse/reference_wrapper.cpp, reference_wrapper_heap_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [start of end of lifetime trace,invalidated by during call to `getwrapperHeap()` here,invalidated by during call to `~WrapsB` here,invalidated by during call to `__infer_inner_destructor_~WrapsB` here,invalidated by `delete` on `this->b` here,start of use after lifetime trace,accessed `rw.b->f` here,start of value trace,assigned to `this->b`,returned from call to `ReferenceWrapperHeap::ReferenceWrapperHeap()`] +codetoanalyze/cpp/pulse/reference_wrapper.cpp, reference_wrapper_stack_bad, 2, USE_AFTER_LIFETIME, no_bucket, ERROR, [start of end of lifetime trace,invalidated by during call to `getwrapperStack()` here,invalidated by `&(b)` gone out of scope here,start of use after lifetime trace,accessed `rw.b->f` here,start of value trace,assigned to `this->b`,returned from call to `ReferenceWrapperStack::ReferenceWrapperStack()`] 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, [] @@ -31,7 +33,6 @@ 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_LIFETIME, no_bucket, ERROR, [start of end of lifetime trace,invalidated by `&(c)` gone out of scope here,start of use after lifetime trace,accessed `pc->f` here,start of value trace,variable declared,assigned to `pc`] codetoanalyze/cpp/pulse/use_after_free.cpp, double_free_simple_bad, 2, USE_AFTER_FREE, no_bucket, ERROR, [start of end of lifetime trace,invalidated by call to `free()` on `x` here,start of use after lifetime trace,accessed `x` here] codetoanalyze/cpp/pulse/use_after_free.cpp, use_after_free_simple_bad, 2, USE_AFTER_FREE, no_bucket, ERROR, [start of end of lifetime trace,invalidated by call to `free()` on `x` here,start of use after lifetime trace,accessed `*(x)` here] -codetoanalyze/cpp/pulse/vector.cpp, FP_init_fill_then_push_back_loop_ok, 6, VECTOR_INVALIDATION, no_bucket, ERROR, [start of end of lifetime trace,invalidated by potentially invalidated by call to `std::vector::push_back()` on `&(vec)` here,start of use after lifetime trace,accessed `*(elt)` here,start of value trace,returned from call to `std::vector::at(&(vec),(unsigned long) 1)`,assigned to `elt`] codetoanalyze/cpp/pulse/vector.cpp, assign_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [start of end of lifetime trace,invalidated by potentially invalidated by call to `std::vector::assign()` on `vec` here,start of use after lifetime trace,accessed `*(elt)` here,start of value trace,returned from call to `std::vector::at(vec,(unsigned long) 1)`,assigned to `elt`] codetoanalyze/cpp/pulse/vector.cpp, clear_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [start of end of lifetime trace,invalidated by potentially invalidated by call to `std::vector::clear()` on `vec` here,start of use after lifetime trace,accessed `*(elt)` here,start of value trace,returned from call to `std::vector::at(vec,(unsigned long) 1)`,assigned to `elt`] codetoanalyze/cpp/pulse/vector.cpp, deref_local_vector_element_after_push_back_bad, 4, VECTOR_INVALIDATION, no_bucket, ERROR, [start of end of lifetime trace,invalidated by potentially invalidated by call to `std::vector::push_back()` on `&(vec)` here,start of use after lifetime trace,accessed `*(elt)` here,start of value trace,returned from call to `std::vector::at(&(vec),(unsigned long) 1)`,assigned to `elt`] diff --git a/infer/tests/codetoanalyze/cpp/pulse/reference_wrapper.cpp b/infer/tests/codetoanalyze/cpp/pulse/reference_wrapper.cpp index 9b1ff26f3..acf5613f2 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/reference_wrapper.cpp +++ b/infer/tests/codetoanalyze/cpp/pulse/reference_wrapper.cpp @@ -27,7 +27,7 @@ ReferenceWrapperHeap getwrapperHeap() { // destructor of WrapsB } -int FN_reference_wrapper_heap_bad() { +int reference_wrapper_heap_bad() { ReferenceWrapperHeap rw = getwrapperHeap(); return rw.b->f; // we want to report use after lifetime bug here } @@ -42,7 +42,7 @@ ReferenceWrapperStack getwrapperStack() { return b; } -int FN_reference_wrapper_stack_bad() { +int 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/vector.cpp b/infer/tests/codetoanalyze/cpp/pulse/vector.cpp index ec6147041..fbf75dd87 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/vector.cpp +++ b/infer/tests/codetoanalyze/cpp/pulse/vector.cpp @@ -58,7 +58,7 @@ void reserve_then_push_back_loop_ok(std::vector& vec, std::cout << *elt << "\n"; } -void FP_init_fill_then_push_back_loop_ok(std::vector& vec_other) { +void 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) {