[retain cycles] Removing code for finding retain cycles on blocks that is now unused.

Reviewed By: mbouaziz

Differential Revision: D7041598

fbshipit-source-id: 65ca070

infer/src/backend/prop.ml

@@ -2284,31 +2284,6 @@ let from_pi pi = set prop_emp ~pi
 
 let from_sigma sigma = set prop_emp ~sigma
 
-(** Rename free variables in a prop replacing them with existentially quantified vars *)
-let prop_rename_fav_with_existentials tenv (p: normal t) : normal t =
-  let fav = Sil.fav_new () in
-  prop_fav_add fav p ;
-  let ids = Sil.fav_to_list fav in
-  let ids' = List.map ~f:(fun i -> (i, Ident.create_fresh Ident.kprimed)) ids in
-  let ren_sub = Sil.subst_of_list (List.map ~f:(fun (i, i') -> (i, Exp.Var i')) ids') in
-  let p' = prop_sub ren_sub p in
-  (*L.d_strln "Prop after renaming:"; d_prop p'; L.d_strln "";*)
-  Normalize.normalize tenv p'
-
-
-(** Removes seeds variables from a prop corresponding to captured variables in an objc block *)
-let remove_seed_captured_vars_block tenv captured_vars prop =
-  let hpred_seed_captured = function
-    | Sil.Hpointsto (Exp.Lvar pv, _, _) ->
-        let pname = Pvar.get_name pv in
-        Pvar.is_seed pv && List.mem ~equal:Mangled.equal captured_vars pname
-    | _ ->
-        false
-  in
-  let sigma = prop.sigma in
-  let sigma' = List.filter ~f:(fun hpred -> not (hpred_seed_captured hpred)) sigma in
-  Normalize.normalize tenv (set prop ~sigma:sigma')
-
 
 (** {2 Prop iterators} *)
 

infer/src/backend/prop.mli

@@ -285,12 +285,6 @@ val set :
   ?sub:Sil.exp_subst -> ?pi:pi -> ?sigma:sigma -> ?pi_fp:pi -> ?sigma_fp:sigma -> 'a t -> exposed t
 (** Set individual fields of the prop. *)
 
-val prop_rename_fav_with_existentials : Tenv.t -> normal t -> normal t
-(** Rename free variables in a prop replacing them with existentially quantified vars *)
-
-val remove_seed_captured_vars_block : Tenv.t -> Mangled.t list -> normal t -> normal t
-(** Removes seeds variables from a prop corresponding to captured variables in an objc block *)
-
 (** {2 Prop iterators} *)
 
 (** Iterator over the sigma part. Each iterator has a current [hpred]. *)

infer/src/backend/symExec.ml

@@ -48,35 +48,6 @@ let unroll_type tenv (typ: Typ.t) (off: Sil.offset) =
       fail Sil.offset_to_string off
 
 
-(** Given a node, returns a list of pvar of blocks that have been nullified in the block. *)
-let get_blocks_nullified node =
-  let null_blocks =
-    List.concat_map
-      ~f:(fun i ->
-        match i with Sil.Nullify (pvar, _) when Sil.is_block_pvar pvar -> [pvar] | _ -> [] )
-      (ProcCfg.Exceptional.instrs node)
-  in
-  null_blocks
-
-
-(** Given a proposition and an objc block checks whether by existentially quantifying
-    captured variables in the block we obtain a leak. *)
-let check_block_retain_cycle tenv caller_pname prop block_nullified =
-  let mblock = Pvar.get_name block_nullified in
-  let block_pname = Typ.Procname.mangled_objc_block (Mangled.to_string mblock) in
-  let block_captured =
-    match Attributes.load block_pname with
-    | Some attributes ->
-        fst (List.unzip attributes.ProcAttributes.captured)
-    | None ->
-        []
-  in
-  let prop' = Prop.remove_seed_captured_vars_block tenv block_captured prop in
-  let prop'' = Prop.prop_rename_fav_with_existentials tenv prop' in
-  let _ : Prop.normal Prop.t = Abs.abstract_junk ~original_prop:prop caller_pname tenv prop'' in
-  ()
-
-
 (** Apply function [f] to the expression at position [offlist] in [strexp].
     If not found, expand [strexp] and apply [f] to [None].
     The routine should maintain the invariant that strexp and typ correspond to
@@ -1367,9 +1338,6 @@ let rec sym_exec tenv current_pdesc instr_ (prop_: Prop.normal Prop.t) path
             pvar ;
           assert false )
   | Sil.Abstract _ ->
-      let node = State.get_node () in
-      let blocks_nullified = get_blocks_nullified node in
-      List.iter ~f:(check_block_retain_cycle tenv current_pname prop_) blocks_nullified ;
       if Prover.check_inconsistency tenv prop_ then ret_old_path []
       else
         ret_old_path