[inferbo] Clean up exit state from unreachable locations

Summary: Remove from inferbo summary locations that are unreachable from callers

Reviewed By: ezgicicek

Differential Revision: D15064518

fbshipit-source-id: 734e79b4a

infer/src/bufferoverrun/absLoc.ml

@@ -117,6 +117,13 @@ module Allocsite = struct
         || Option.value_map path ~default:false ~f:Symb.SymbolPath.represents_multiple_values
     | LiteralString _ ->
         true
+
+
+  let exists_pvar ~f = function
+    | Unknown | LiteralString _ | Known {path= None} ->
+        false
+    | Symbol path | Known {path= Some path} ->
+        Symb.SymbolPath.exists_pvar_partial ~f path
 end
 
 module Loc = struct
@@ -258,12 +265,6 @@ module Loc = struct
         Option.map (get_param_path l) ~f:(fun p -> Symb.SymbolPath.field p fn)
 
 
-  let has_param_path formals x =
-    Option.value_map (get_path x) ~default:false ~f:(fun x ->
-        Option.value_map (Symb.SymbolPath.get_pvar x) ~default:false ~f:(fun x ->
-            List.exists formals ~f:(fun (formal, _) -> Pvar.equal x formal) ) )
-
-
   let rec represents_multiple_values = function
     | Var _ ->
         false
@@ -273,6 +274,17 @@ module Loc = struct
         represents_multiple_values l
 
 
+  let rec exists_pvar ~f = function
+    | Var (LogicalVar _) ->
+        false
+    | Var (ProgramVar pvar) ->
+        f pvar
+    | Allocsite allocsite ->
+        Allocsite.exists_pvar ~f allocsite
+    | Field (l, _) ->
+        exists_pvar ~f l
+
+
   let exists_str ~f l =
     Option.exists (get_path l) ~f:(fun path -> Symb.SymbolPath.exists_str_partial ~f path)
 end

infer/src/bufferoverrun/bufferOverrunAnalysis.ml

@@ -354,12 +354,16 @@ let cached_compute_invariant_map =
         inv_map
 
 
-let compute_summary : local_decls -> CFG.t -> invariant_map -> memory_summary =
+let compute_summary :
- fun locals cfg inv_map ->
+    local_decls -> (Pvar.t * Typ.t) list -> CFG.t -> invariant_map -> memory_summary =
+ fun locals formals cfg inv_map ->
   let exit_node_id = CFG.exit_node cfg |> CFG.Node.id in
   match extract_post exit_node_id inv_map with
   | Some exit_mem ->
-      exit_mem |> Dom.Mem.relation_forget_locs locals |> Dom.Mem.unset_oenv
+      exit_mem
+      |> Dom.Mem.forget_unreachable_locs ~formals
+      |> Dom.Mem.relation_forget_locs locals
+      |> Dom.Mem.unset_oenv
   | None ->
       Bottom
 
@@ -368,6 +372,7 @@ let do_analysis : Callbacks.proc_callback_args -> Summary.t =
  fun {proc_desc; tenv; integer_type_widths; summary} ->
   let inv_map = cached_compute_invariant_map proc_desc tenv integer_type_widths in
   let locals = get_local_decls proc_desc in
+  let formals = Procdesc.get_pvar_formals proc_desc in
   let cfg = CFG.from_pdesc proc_desc in
-  let payload = compute_summary locals cfg inv_map in
+  let payload = compute_summary locals formals cfg inv_map in
   Payload.update_summary payload summary

infer/src/bufferoverrun/bufferOverrunDomain.ml

@@ -1460,7 +1460,7 @@ module MemReach = struct
 
   let set_latest_prune : LatestPrune.t -> t -> t = fun latest_prune x -> {x with latest_prune}
 
-  let get_reachable_locs_from : (Pvar.t * Typ.t) list -> PowLoc.t -> _ t0 -> PowLoc.t =
+  let get_reachable_locs_from_aux : f:(Pvar.t -> bool) -> PowLoc.t -> _ t0 -> PowLoc.t =
     let add_reachable1 ~root loc v acc =
       if Loc.equal root loc then PowLoc.union acc (Val.get_all_locs v)
       else if Loc.is_field_of ~loc:root ~field_loc:loc then PowLoc.add loc acc
@@ -1473,15 +1473,21 @@ module MemReach = struct
         let reachable_locs = MemPure.fold (add_reachable1 ~root:loc) heap PowLoc.empty in
         add_from_locs heap reachable_locs (PowLoc.add loc acc)
     in
-    let add_param_locs formals mem acc =
+    let add_param_locs ~f mem acc =
-      let add_loc loc _ acc = if Loc.has_param_path formals loc then PowLoc.add loc acc else acc in
+      let add_loc loc _ acc = if Loc.exists_pvar ~f loc then PowLoc.add loc acc else acc in
       MemPure.fold add_loc mem acc
     in
-    fun formals locs m ->
+    fun ~f locs m ->
-      let locs = add_param_locs formals m.mem_pure locs in
+      let locs = add_param_locs ~f m.mem_pure locs in
       add_from_locs m.mem_pure locs PowLoc.empty
 
 
+  let get_reachable_locs_from : (Pvar.t * Typ.t) list -> PowLoc.t -> _ t0 -> PowLoc.t =
+   fun formals locs m ->
+    let is_formal pvar = List.exists formals ~f:(fun (formal, _) -> Pvar.equal pvar formal) in
+    get_reachable_locs_from_aux ~f:is_formal locs m
+
+
   let range :
       filter_loc:(Loc.t -> LoopHeadLoc.t option) -> t -> Polynomials.NonNegativePolynomial.t =
    fun ~filter_loc {mem_pure} -> MemPure.range ~filter_loc mem_pure
@@ -1511,6 +1517,23 @@ module MemReach = struct
    fun locs -> lift_relation (Relation.forget_locs locs)
 
 
+  let forget_unreachable_locs : formals:(Pvar.t * Typ.t) list -> t -> t =
+   fun ~formals m ->
+    let is_reachable =
+      let reachable_locs =
+        let f pvar =
+          Pvar.is_return pvar || Pvar.is_global pvar
+          || List.exists formals ~f:(fun (formal, _) -> Pvar.equal formal pvar)
+        in
+        get_reachable_locs_from_aux ~f PowLoc.empty m
+      in
+      fun l -> PowLoc.mem l reachable_locs
+    in
+    let stack_locs = StackLocs.filter is_reachable m.stack_locs in
+    let mem_pure = MemPure.filter (fun l _ -> is_reachable l) m.mem_pure in
+    {m with stack_locs; mem_pure}
+
+
   let init_param_relation : Loc.t -> t -> t = fun loc -> lift_relation (Relation.init_param loc)
 
   let init_array_relation :
@@ -1692,6 +1715,10 @@ module Mem = struct
    fun locs -> map ~f:(MemReach.relation_forget_locs locs)
 
 
+  let forget_unreachable_locs : formals:(Pvar.t * Typ.t) list -> t -> t =
+   fun ~formals -> map ~f:(MemReach.forget_unreachable_locs ~formals)
+
+
   let[@warning "-32"] init_param_relation : Loc.t -> t -> t =
    fun loc -> map ~f:(MemReach.init_param_relation loc)
 

infer/src/bufferoverrun/symb.ml

@@ -140,6 +140,15 @@ module SymbolPath = struct
         represents_callsite_sound_partial p
 
 
+  let rec exists_pvar_partial ~f = function
+    | Pvar pvar ->
+        f pvar
+    | Deref (_, p) | Field (_, p) ->
+        exists_pvar_partial ~f p
+    | Callsite _ ->
+        false
+
+
   let rec exists_str_partial ~f = function
     | Pvar pvar ->
         f (Pvar.to_string pvar)

infer/src/bufferoverrun/symb.mli

@@ -67,6 +67,8 @@ module SymbolPath : sig
 
   val represents_callsite_sound_partial : partial -> bool
 
+  val exists_pvar_partial : f:(Pvar.t -> bool) -> partial -> bool
+
   val exists_str_partial : f:(string -> bool) -> partial -> bool
 end