[biabd] get rid of `Summary.get` in retain cycle detection

Summary:
We want to kill the cache in `Summary`, and calling `Summary.get` relies on
that cache existing for efficiency. However in this case it's not needed
because we can pass the summary from above instead.

Reviewed By: mbouaziz

Differential Revision: D9195234

fbshipit-source-id: 5b7023242

infer/src/biabduction/RetainCycles.ml

@@ -213,7 +213,7 @@ let get_cycles found_cycles root tenv prop =
       found_cycles
 
 
-(* Find all the cycles available in prop, up to a limit of 10 *)
+(** Find all the cycles available in prop, up to a limit of 10 *)
 let get_retain_cycles tenv prop =
   let get_retain_cycles_with_root acc_set root = get_cycles acc_set root tenv prop in
   let sigma = prop.Prop.sigma in
@@ -233,21 +233,16 @@ let exn_retain_cycle tenv cycle =
   Exceptions.Retain_cycle (desc, __POS__)
 
 
-let report_cycle tenv pname prop =
-  (* When there is a cycle in objc we ignore it
-        only if it's empty or it has weak or unsafe_unretained fields.
-        Otherwise we report a retain cycle. *)
+let report_cycle tenv summary prop =
+  (* When there is a cycle in objc we ignore it only if it's empty or it has weak or
+     unsafe_unretained fields.  Otherwise we report a retain cycle. *)
   let cycles = get_retain_cycles tenv prop in
   RetainCyclesType.Set.iter RetainCyclesType.print_cycle cycles ;
-  match Summary.get pname with
-  | Some summary ->
-      if RetainCyclesType.Set.cardinal cycles > 0 then (
-        RetainCyclesType.Set.iter
-          (fun cycle ->
-            let exn = exn_retain_cycle tenv cycle in
-            Reporting.log_error summary exn )
-          cycles ;
-        (* we report the retain cycles above but need to raise an exception as well to stop the analysis *)
-        raise (Exceptions.Dummy_exception (Localise.verbatim_desc "retain cycle found")) )
-  | None ->
-      ()
+  if RetainCyclesType.Set.cardinal cycles > 0 then (
+    RetainCyclesType.Set.iter
+      (fun cycle ->
+        let exn = exn_retain_cycle tenv cycle in
+        Reporting.log_error summary exn )
+      cycles ;
+    (* we report the retain cycles above but need to raise an exception as well to stop the analysis *)
+    raise (Exceptions.Dummy_exception (Localise.verbatim_desc "retain cycle found")) )

infer/src/biabduction/RetainCycles.mli

@@ -7,4 +7,4 @@
 
 open! IStd
 
-val report_cycle : Tenv.t -> Typ.Procname.t -> Prop.normal Prop.t -> unit
+val report_cycle : Tenv.t -> Summary.t -> Prop.normal Prop.t -> unit

infer/src/biabduction/RetainCyclesType.ml

@@ -94,7 +94,7 @@ let is_exp_null node =
   match node with Object obj -> Exp.is_null_literal obj.rc_from.rc_node_exp | Block _ -> false
 
 
-let _retain_cycle_node_to_string (node: retain_cycle_node) =
+let retain_cycle_node_to_string (node: retain_cycle_node) =
   Format.sprintf "%s : %s" (Exp.to_string node.rc_node_exp) (Typ.to_string node.rc_node_typ)
 
 
@@ -104,22 +104,22 @@ let retain_cycle_field_to_string (field: retain_cycle_field) =
     (Sil.inst_to_string field.rc_field_inst)
 
 
-let _retain_cycle_edge_to_string (edge: retain_cycle_edge) =
+let retain_cycle_edge_to_string (edge: retain_cycle_edge) =
   match edge with
   | Object obj ->
       Format.sprintf "%s ->{%s}"
-        (_retain_cycle_node_to_string obj.rc_from)
+        (retain_cycle_node_to_string obj.rc_from)
         (retain_cycle_field_to_string obj.rc_field)
   | Block _ ->
       Format.sprintf "a block"
 
 
-let _retain_cycle_to_string cycle =
+let retain_cycle_to_string cycle =
   "Cycle= \n\t"
-  ^ String.concat ~sep:"->" (List.map ~f:_retain_cycle_edge_to_string cycle.rc_elements)
+  ^ String.concat ~sep:"->" (List.map ~f:retain_cycle_edge_to_string cycle.rc_elements)
 
 
-let print_cycle cycle = Logging.d_strln (_retain_cycle_to_string cycle)
+let print_cycle cycle = Logging.d_strln (retain_cycle_to_string cycle)
 
 let find_minimum_element cycle =
   List.reduce_exn cycle.rc_elements ~f:(fun el1 el2 ->

infer/src/biabduction/RetainCyclesType.mli

@@ -30,9 +30,3 @@ val create_cycle : retain_cycle_edge list -> t option
 val pp_dotty : Format.formatter -> t -> unit
 
 val write_dotty_to_file : string -> t -> unit
-
-val _retain_cycle_edge_to_string : retain_cycle_edge -> string
-
-val _retain_cycle_node_to_string : retain_cycle_node -> string
-
-val _retain_cycle_to_string : t -> string

infer/src/biabduction/SymExec.ml

@@ -1908,8 +1908,8 @@ and proc_call ?dynamic_dispatch exe_env callee_summary
 
 
 (** perform symbolic execution for a single prop, and check for junk *)
-and sym_exec_wrapper exe_env handle_exn tenv proc_cfg instr ((prop: Prop.normal Prop.t), path)
-    : Paths.PathSet.t =
+and sym_exec_wrapper exe_env handle_exn tenv summary proc_cfg instr
+    ((prop: Prop.normal Prop.t), path) : Paths.PathSet.t =
   let pname = Procdesc.get_proc_name (ProcCfg.Exceptional.proc_desc proc_cfg) in
   let prop_primed_to_normal p =
     (* Rename primed vars with fresh normal vars, and return them *)
@@ -1950,7 +1950,7 @@ and sym_exec_wrapper exe_env handle_exn tenv proc_cfg instr ((prop: Prop.normal
       (* Check for retain cycles after assignments and method calls *)
       ( match instr with
       | (Sil.Store _ | Sil.Call _) when !Config.footprint ->
-          List.iter ~f:(RetainCycles.report_cycle tenv pname) [p]
+          List.iter ~f:(RetainCycles.report_cycle tenv summary) [p]
       | _ ->
           () ) ;
       let node_has_abstraction node =
@@ -2000,7 +2000,7 @@ and sym_exec_wrapper exe_env handle_exn tenv proc_cfg instr ((prop: Prop.normal
 
 (** {2 Lifted Abstract Transfer Functions} *)
 
-let node handle_exn exe_env tenv proc_cfg (node: ProcCfg.Exceptional.Node.t)
+let node handle_exn exe_env tenv summary proc_cfg (node: ProcCfg.Exceptional.Node.t)
     (pset: Paths.PathSet.t) : Paths.PathSet.t =
   let pname = Procdesc.get_proc_name (ProcCfg.Exceptional.proc_desc proc_cfg) in
   let exe_instr_prop instr p tr (pset1: Paths.PathSet.t) =
@@ -2015,7 +2015,7 @@ let node handle_exn exe_env tenv proc_cfg (node: ProcCfg.Exceptional.Node.t)
         Sil.d_instr instr ;
         L.d_strln " due to exception" ;
         Paths.PathSet.from_renamed_list [(p, tr)] )
-      else sym_exec_wrapper exe_env handle_exn tenv proc_cfg instr (p, tr)
+      else sym_exec_wrapper exe_env handle_exn tenv summary proc_cfg instr (p, tr)
     in
     Paths.PathSet.union pset2 pset1
   in

infer/src/biabduction/SymExec.mli

@@ -11,8 +11,8 @@ open! IStd
 (** Symbolic Execution *)
 
 val node :
-  (exn -> unit) -> Exe_env.t -> Tenv.t -> ProcCfg.Exceptional.t -> ProcCfg.Exceptional.Node.t
-  -> Paths.PathSet.t -> Paths.PathSet.t
+  (exn -> unit) -> Exe_env.t -> Tenv.t -> Summary.t -> ProcCfg.Exceptional.t
+  -> ProcCfg.Exceptional.Node.t -> Paths.PathSet.t -> Paths.PathSet.t
 (** Symbolic execution of the instructions of a node, lifted to sets of propositions. *)
 
 val instrs :

infer/src/biabduction/interproc.ml

@@ -376,14 +376,14 @@ let instrs_get_normal_vars instrs =
 
 
 (** Perform symbolic execution for a node starting from an initial prop *)
-let do_symbolic_execution exe_env proc_cfg handle_exn tenv (node: ProcCfg.Exceptional.Node.t)
-    (prop: Prop.normal Prop.t) (path: Paths.Path.t) =
+let do_symbolic_execution exe_env summary proc_cfg handle_exn tenv
+    (node: ProcCfg.Exceptional.Node.t) (prop: Prop.normal Prop.t) (path: Paths.Path.t) =
   State.mark_execution_start node ;
   let instrs = ProcCfg.Exceptional.instrs node in
   (* fresh normal vars must be fresh w.r.t. instructions *)
   Ident.update_name_generator (instrs_get_normal_vars instrs) ;
   let pset =
-    SymExec.node handle_exn exe_env tenv proc_cfg node
+    SymExec.node handle_exn exe_env tenv summary proc_cfg node
       (Paths.PathSet.from_renamed_list [(prop, path)])
   in
   L.d_strln ".... After Symbolic Execution ...." ;
@@ -457,7 +457,9 @@ let forward_tabulate summary exe_env tenv proc_cfg wl =
     L.d_increase_indent 1 ;
     try
       State.reset_diverging_states_node () ;
-      let pset = do_symbolic_execution exe_env proc_cfg handle_exn tenv curr_node prop path in
+      let pset =
+        do_symbolic_execution exe_env summary proc_cfg handle_exn tenv curr_node prop path
+      in
       propagate_nodes_divergence tenv proc_cfg pset curr_node wl ;
       L.d_decrease_indent 1 ;
       L.d_ln ()