[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

@@ -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
+  let initial =
-    DisjunctiveAnalyzer.compute_post proc_data
+    DisjunctiveTransferFunctions.Disjuncts.singleton (PulseAbductiveDomain.mk_initial proc_desc)
-      ~initial:(DisjunctiveTransferFunctions.Disjuncts.singleton PulseAbductiveDomain.empty)
+  in
-  with
+  match DisjunctiveAnalyzer.compute_post proc_data ~initial with
   | Some posts ->
       Payload.update_summary
         (PulseSummary.of_posts (DisjunctiveTransferFunctions.Disjuncts.elements posts))

infer/src/pulse/PulseAbductiveDomain.ml

@@ -86,8 +86,9 @@ let ( <= ) ~lhs ~rhs =
 
 
 module Stack = struct
-  let is_abducible _var =
+  let is_abducible astate var =
-    (* TODO: need to keep only formals + return variable + globals in the pre *) true
+    (* 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
+    match PulseDomain.Stack.find_opt return_var (pre_post.post :> PulseDomain.t).stack with
-      PulseDomain.Stack.find_opt return_var (pre_post.pre :> PulseDomain.t).PulseDomain.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

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 *)

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`]

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
 }

infer/tests/codetoanalyze/cpp/pulse/vector.cpp

@@ -58,7 +58,7 @@ void reserve_then_push_back_loop_ok(std::vector<int>& vec,
   std::cout << *elt << "\n";
 }
 
-void FP_init_fill_then_push_back_loop_ok(std::vector<int>& vec_other) {
+void init_fill_then_push_back_loop_ok(std::vector<int>& vec_other) {
   std::vector<int> vec(vec_other.size());
   int* elt = &vec[1];
   for (const auto& i : vec_other) {