[retain cycles] Report cycles after assignment and method call

Reviewed By: mbouaziz

Differential Revision: D7256076

fbshipit-source-id: f9c875a

infer/src/IR/Errlog.ml

@@ -249,7 +249,13 @@ let log_issue procname err_kind err_log loc (node_id, node_key) session ltr ?lin
     | _ ->
         false
   in
-  let exn_developer = Exceptions.equal_visibility error.visibility Exceptions.Exn_developer in
+  let report_developer_exn exn =
+    match exn with Exceptions.Dummy_exception _ -> false | _ -> true
+  in
+  let exn_developer =
+    Exceptions.equal_visibility error.visibility Exceptions.Exn_developer
+    && report_developer_exn exn
+  in
   let should_report =
     Exceptions.equal_visibility error.visibility Exceptions.Exn_user
     || Config.developer_mode && exn_developer

infer/src/IR/Exceptions.ml

@@ -67,6 +67,8 @@ exception Condition_always_true_false of Localise.error_desc * bool * L.ocaml_po
 
 exception Custom_error of string * Localise.error_desc
 
+exception Dummy_exception of Localise.error_desc
+
 exception Dangling_pointer_dereference of
   PredSymb.dangling_kind option * Localise.error_desc * L.ocaml_pos
 
@@ -115,7 +117,7 @@ exception Precondition_not_found of Localise.error_desc * L.ocaml_pos
 
 exception Precondition_not_met of Localise.error_desc * L.ocaml_pos
 
-exception Retain_cycle of Sil.hpred * Localise.error_desc * L.ocaml_pos
+exception Retain_cycle of Localise.error_desc * L.ocaml_pos
 
 exception Registered_observer_being_deallocated of Localise.error_desc * L.ocaml_pos
 
@@ -272,6 +274,14 @@ let recognize_exception exn =
       ; severity= High
       ; kind= None
       ; category= Checker }
+  | Dummy_exception desc ->
+      { name= IssueType.from_string "Analysis stops"
+      ; description= desc
+      ; ocaml_pos= None
+      ; visibility= Exn_developer
+      ; severity= Low
+      ; kind= Some Kinfo
+      ; category= Checker }
   | Dangling_pointer_dereference (dko, desc, ocaml_pos) ->
       let visibility =
         match dko with
@@ -494,7 +504,7 @@ let recognize_exception exn =
       ; kind= Some Kwarning
       ; category= Nocat }
       (* always a warning *)
-  | Retain_cycle (_, desc, ocaml_pos) ->
+  | Retain_cycle (desc, ocaml_pos) ->
       { name= IssueType.retain_cycle
       ; description= desc
       ; ocaml_pos= Some ocaml_pos

infer/src/IR/Exceptions.mli

@@ -65,6 +65,8 @@ exception Condition_always_true_false of Localise.error_desc * bool * Logging.oc
 
 exception Custom_error of string * Localise.error_desc
 
+exception Dummy_exception of Localise.error_desc
+
 exception Dangling_pointer_dereference of
   PredSymb.dangling_kind option * Localise.error_desc * Logging.ocaml_pos
 
@@ -118,7 +120,7 @@ exception Precondition_not_found of Localise.error_desc * Logging.ocaml_pos
 
 exception Precondition_not_met of Localise.error_desc * Logging.ocaml_pos
 
-exception Retain_cycle of Sil.hpred * Localise.error_desc * Logging.ocaml_pos
+exception Retain_cycle of Localise.error_desc * Logging.ocaml_pos
 
 exception Registered_observer_being_deallocated of Localise.error_desc * Logging.ocaml_pos
 

infer/src/backend/RetainCycles.ml

@@ -18,11 +18,11 @@ let desc_retain_cycle tenv (cycle: RetainCyclesType.t) =
     let index = index_ + 1 in
     let node = State.get_node () in
     let from_exp_str edge_obj =
-      match Errdesc.find_outermost_dereference tenv node edge_obj.rc_from.rc_node_exp with
+      ignore (Errdesc.find_outermost_dereference tenv node edge_obj.rc_from.rc_node_exp) ;
-      | Some de ->
+      (* | Some de ->
           DecompiledExp.to_string de
-      | None ->
+      | None -> TODO (T26707784): fix issues with DecompiledExp.to_string *)
-          Format.sprintf "(object of type %s)" (Typ.to_string edge_obj.rc_from.rc_node_typ)
+      Format.sprintf "(object of type %s)" (Typ.to_string edge_obj.rc_from.rc_node_typ)
     in
     let location_str =
       match edge with
@@ -168,26 +168,24 @@ let get_cycles found_cycles root tenv prop =
     | _ ->
         found_cycles
   in
-  L.d_strln "Looking for cycle with root expression: " ;
-  Sil.d_hpred root ;
-  L.d_strln "" ;
   match root with
-  | Sil.Hpointsto (e_root, Sil.Estruct (fl, _), Exp.Sizeof {typ= te}) ->
+  | Sil.Hpointsto (e_root, Sil.Estruct (fl, _), Exp.Sizeof {typ= te}) when Sil.is_objc_object root ->
       let se_root = {rc_node_exp= e_root; rc_node_typ= te} in
       (* start dfs with empty path and expr pointing to root *)
       dfs ~found_cycles ~root_node:se_root ~from_node:se_root ~rev_path:[] ~fields:fl ~visited:[]
   | _ ->
-      L.d_strln "Root exp is not an allocated object. No cycle found" ;
       found_cycles
 
 
-(* Find all the cycles available with root hpred, up to a limit of 10 *)
+(* Find all the cycles available in prop, up to a limit of 10 *)
-let get_retain_cycles hpred tenv prop_ =
+let get_retain_cycles tenv prop =
-  try get_cycles RetainCyclesType.Set.empty hpred tenv prop_ with Max_retain_cycles cycles ->
+  let get_retain_cycles_with_root acc_set root = get_cycles acc_set root tenv prop in
-    cycles
+  let sigma = prop.Prop.sigma in
+  try List.fold ~f:get_retain_cycles_with_root sigma ~init:RetainCyclesType.Set.empty
+  with Max_retain_cycles cycles -> cycles
 
 
-let exn_retain_cycle tenv hpred cycle =
+let exn_retain_cycle tenv cycle =
   let retain_cycle = desc_retain_cycle tenv cycle in
   let cycle_dotty = Format.asprintf "%a" RetainCyclesType.pp_dotty cycle in
   if Config.debug_mode then (
@@ -196,23 +194,24 @@ let exn_retain_cycle tenv hpred cycle =
     let rc_dotty_file = Filename.temp_file ~in_dir:rc_dotty_dir "rc" ".dot" in
     RetainCyclesType.write_dotty_to_file rc_dotty_file cycle ) ;
   let desc = Localise.desc_retain_cycle retain_cycle (State.get_loc ()) (Some cycle_dotty) in
-  Exceptions.Retain_cycle (hpred, desc, __POS__)
+  Exceptions.Retain_cycle (desc, __POS__)
 
 
-let report_cycle tenv pname hpred original_prop =
+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 remove_opt prop_ = match prop_ with Some Some p -> p | _ -> Prop.prop_emp in
+  let cycles = get_retain_cycles tenv prop in
-  let prop = remove_opt original_prop in
-  let cycles = get_retain_cycles hpred tenv prop in
   RetainCyclesType.Set.iter RetainCyclesType.print_cycle cycles ;
   match Specs.get_summary pname with
   | Some summary ->
-      RetainCyclesType.Set.iter
+      if RetainCyclesType.Set.cardinal cycles > 0 then (
-        (fun cycle ->
+        RetainCyclesType.Set.iter
-          let exn = exn_retain_cycle tenv hpred cycle in
+          (fun cycle ->
-          Reporting.log_error summary exn )
+            let exn = exn_retain_cycle tenv cycle in
-        cycles
+            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 ->
       ()

infer/src/backend/RetainCycles.mli

@@ -9,5 +9,4 @@
 
 open! IStd
 
-val report_cycle :
+val report_cycle : Tenv.t -> Typ.Procname.t -> Prop.normal Prop.t -> unit
-  Tenv.t -> Typ.Procname.t -> Sil.hpred -> Prop.normal Prop.t option option -> unit

infer/src/backend/abs.ml

@@ -1003,7 +1003,7 @@ let check_observer_is_unsubscribed_deallocation tenv prop e =
       ()
 
 
-let check_junk ?original_prop pname tenv prop =
+let check_junk pname tenv prop =
   let leaks_reported = ref [] in
   let remove_junk_once fp_part fav_root sigma =
     let id_considered_reachable =
@@ -1096,9 +1096,7 @@ let check_junk ?original_prop pname tenv prop =
               | Some PredSymb.Awont_leak, Rmemory _ ->
                   (true, exn_leak)
               | Some _, Rmemory Mobjc ->
-                  RetainCycles.report_cycle tenv pname hpred original_prop ;
                   (true, exn_leak)
-                  (* we report now inside RetainCycles, here we ignore the leak *)
               | (Some _, Rmemory Mnew | Some _, Rmemory Mnew_array)
                 when Language.curr_language_is Clang ->
                   (is_none ml_bucket_opt, exn_leak)
@@ -1112,13 +1110,6 @@ let check_junk ?original_prop pname tenv prop =
                   (false, exn_leak)
               | Some _, Rlock ->
                   (false, exn_leak)
-              | _ when Sil.is_objc_object hpred ->
-                  (* When it's a cycle and it is an Objective-C object then
-                        we have a retain cycle. Objc object may not have the
-                        Mobjc qualifier when added in footprint doing abduction *)
-                  RetainCycles.report_cycle tenv pname hpred original_prop ;
-                  (true, exn_leak)
-                  (* we report now inside RetainCycles, here we ignore the leak *)
               | _ ->
                   (Language.curr_language_is Java, exn_leak)
             in
@@ -1173,16 +1164,16 @@ let check_junk ?original_prop pname tenv prop =
 
 (** Check whether the prop contains junk.
     If it does, and [Config.allowleak] is true, remove the junk, otherwise raise a Leak exception. *)
-let abstract_junk ?original_prop pname tenv prop =
+let abstract_junk pname tenv prop =
   Absarray.array_abstraction_performed := false ;
-  check_junk ~original_prop pname tenv prop
+  check_junk pname tenv prop
 
 
 (** Remove redundant elements in an array, and check for junk afterwards *)
 let remove_redundant_array_elements pname tenv prop =
   Absarray.array_abstraction_performed := false ;
   let prop' = Absarray.remove_redundant_elements tenv prop in
-  check_junk ~original_prop:(Some prop) pname tenv prop'
+  check_junk pname tenv prop'
 
 
 let abstract_prop pname tenv ~(rename_primed: bool) ~(from_abstract_footprint: bool) p =
@@ -1197,7 +1188,7 @@ let abstract_prop pname tenv ~(rename_primed: bool) ~(from_abstract_footprint: b
   let abs_p = abs_rules_apply tenv array_abs_p in
   let abs_p = abstract_gc tenv abs_p in
   (* abstraction might enable more gc *)
-  let abs_p = check_junk ~original_prop:(Some p) pname tenv abs_p in
+  let abs_p = check_junk pname tenv abs_p in
   let ren_abs_p =
     if rename_primed then Prop.prop_rename_primed_footprint_vars tenv abs_p else abs_p
   in

infer/src/backend/abs.mli

@@ -18,9 +18,7 @@ type rules
 val abstract : Typ.Procname.t -> Tenv.t -> Prop.normal Prop.t -> Prop.normal Prop.t
 (** Abstract a proposition. *)
 
-val abstract_junk :
+val abstract_junk : Typ.Procname.t -> Tenv.t -> Prop.normal Prop.t -> Prop.normal Prop.t
-  ?original_prop:Prop.normal Prop.t -> Typ.Procname.t -> Tenv.t -> Prop.normal Prop.t
-  -> Prop.normal Prop.t
 (** Check whether the prop contains junk.
     If it does, and [Config.allowleak] is true, remove the junk,
     otherwise raise a Leak exception. *)

infer/src/backend/symExec.ml

@@ -1032,7 +1032,11 @@ let execute_store ?(report_deref_errors= true) pname pdesc tenv lhs_exp typ rhs_
     let prop = Attribute.replace_objc_null tenv prop n_lhs_exp n_rhs_exp in
     let n_lhs_exp' = Prop.exp_collapse_consecutive_indices_prop typ n_lhs_exp in
     let iter_list = Rearrange.rearrange ~report_deref_errors pdesc tenv n_lhs_exp' typ prop loc in
-    List.rev (List.fold ~f:(execute_store_ pdesc tenv n_rhs_exp) ~init:[] iter_list)
+    let prop_list =
+      List.rev (List.fold ~f:(execute_store_ pdesc tenv n_rhs_exp) ~init:[] iter_list)
+    in
+    if !Config.footprint then List.iter ~f:(RetainCycles.report_cycle tenv pname) prop_list ;
+    prop_list
   with Rearrange.ARRAY_ACCESS -> if Int.equal Config.array_level 0 then assert false else [prop_]
 
 
@@ -1791,7 +1795,7 @@ and sym_exec_wrapper handle_exn tenv proc_cfg instr ((prop: Prop.normal Prop.t),
           (* but force them into either branch *)
           p'
       | _ ->
-          check_deallocate_static_memory (Abs.abstract_junk ~original_prop:p pname tenv p')
+          check_deallocate_static_memory (Abs.abstract_junk pname tenv p')
     in
     L.d_str "Instruction " ;
     Sil.d_instr instr ;

infer/src/backend/tabulation.ml

@@ -1236,7 +1236,7 @@ let prop_pure_to_footprint tenv (p: 'a Prop.t) : Prop.normal Prop.t =
 
 
 (** post-process the raw result of a function call *)
-let exe_call_postprocess tenv ret_id trace_call callee_pname callee_attrs loc results =
+let exe_call_postprocess tenv ret_id trace_call caller_pname callee_pname callee_attrs loc results =
   let filter_valid_res = function Invalid_res _ -> false | Valid_res _ -> true in
   let valid_res0, invalid_res0 = List.partition_tf ~f:filter_valid_res results in
   let valid_res =
@@ -1366,6 +1366,10 @@ let exe_call_postprocess tenv ret_id trace_call callee_pname callee_attrs loc re
           List.iter ~f:print_pi (List.map ~f:fst cover) ;
           List.concat_map ~f:snd cover )
   in
+  if !Config.footprint then
+    List.iter
+      ~f:(fun (prop, _) -> RetainCycles.report_cycle tenv caller_pname prop)
+      res_with_path_idents ;
   trace_call CR_success ;
   let res =
     List.map
@@ -1416,4 +1420,5 @@ let exe_function_call callee_summary tenv ret_id_opt caller_pdesc callee_pname l
       formal_params
   in
   let results = List.map ~f:exe_one_spec spec_list in
-  exe_call_postprocess tenv ret_id_opt trace_call callee_pname callee_attrs loc results
+  exe_call_postprocess tenv ret_id_opt trace_call caller_pname callee_pname callee_attrs loc
+    results

infer/tests/codetoanalyze/objc/errors/issues.exp

@@ -2,8 +2,8 @@ codetoanalyze/objc/errors/field_superclass/field.c, field_superclass_main, 3, RE
 codetoanalyze/objc/errors/global_const/global_const.m, SimpleRoot_doSomethingBadWithDict:andString:, 3, NULL_DEREFERENCE, ERROR, [start of procedure doSomethingBadWithDict:andString:,Message stringByAppendingString: with receiver nil returns nil.]
 codetoanalyze/objc/errors/global_const/global_const.m, SimpleRoot_doSomethingOkWithDict:andString:, 3, NULL_DEREFERENCE, ERROR, [start of procedure doSomethingOkWithDict:andString:,Message stringByAppendingString: with receiver nil returns nil.]
 codetoanalyze/objc/errors/initialization/compound_literal.c, init_with_compound_literal, 2, DIVIDE_BY_ZERO, ERROR, [start of procedure init_with_compound_literal()]
-codetoanalyze/objc/errors/memory_leaks_benchmark/CADisplayLinkRetainCycle.m, testCycle, 3, RETAIN_CYCLE, ERROR, [start of procedure testCycle(),start of procedure init,return from a call to CADisplay_init]
+codetoanalyze/objc/errors/memory_leaks_benchmark/CADisplayLinkRetainCycle.m, CADisplay_init, 1, RETAIN_CYCLE, ERROR, [start of procedure init]
-codetoanalyze/objc/errors/memory_leaks_benchmark/RetainCycleStaticVar.m, RetainCSVycleStaticVar, 2, RETAIN_CYCLE, ERROR, [start of procedure RetainCSVycleStaticVar(),start of procedure init,return from a call to RetainCSV_init,start of procedure foo,return from a call to RetainCSV_foo]
+codetoanalyze/objc/errors/memory_leaks_benchmark/RetainCycleStaticVar.m, RetainCSV_foo, 13, RETAIN_CYCLE, ERROR, [start of procedure foo]
 codetoanalyze/objc/errors/npe/null_returned_by_method.m, NullReturnedByMethodA_test1, 1, NULL_DEREFERENCE, ERROR, [start of procedure test1,start of procedure test,return from a call to NullReturnedByMethodA_test]
 codetoanalyze/objc/errors/procdescs/main.c, ProcdescMain, 3, MEMORY_LEAK, ERROR, [start of procedure ProcdescMain(),Skipping plusX:andY:: function or method not found]
 codetoanalyze/objc/errors/procdescs/main.c, call_nslog, 3, MEMORY_LEAK, ERROR, [start of procedure call_nslog(),Skipping NSLog(): function or method not found]
@@ -30,12 +30,12 @@ codetoanalyze/objc/errors/initialization/struct_initlistexpr.c, field_set_correc
 codetoanalyze/objc/errors/initialization/struct_initlistexpr.c, implicit_expr_set_correctly, 3, DIVIDE_BY_ZERO, ERROR, [start of procedure implicit_expr_set_correctly()]
 codetoanalyze/objc/errors/initialization/struct_initlistexpr.c, point_coords_set_correctly, 2, DIVIDE_BY_ZERO, ERROR, [start of procedure point_coords_set_correctly()]
 codetoanalyze/objc/errors/memory_leaks_benchmark/RetainCycleBlockCapturedVar.m, LinkResolver_test_bad, 3, RETAIN_CYCLE, ERROR, [start of procedure test_bad]
-codetoanalyze/objc/errors/memory_leaks_benchmark/RetainCycleBlocks.m, call_retain_self_in_block_cycle, 2, RETAIN_CYCLE, ERROR, [start of procedure call_retain_self_in_block_cycle(),start of procedure retain_self_in_block,return from a call to RCBlock_retain_self_in_block]
+codetoanalyze/objc/errors/memory_leaks_benchmark/RetainCycleBlocks.m, RCBlock_retain_self_in_block, 1, RETAIN_CYCLE, ERROR, [start of procedure retain_self_in_block]
-codetoanalyze/objc/errors/memory_leaks_benchmark/RetainCycleBlocks.m, retain_a_in_block_cycle, 5, RETAIN_CYCLE, ERROR, [start of procedure retain_a_in_block_cycle()]
+codetoanalyze/objc/errors/memory_leaks_benchmark/RetainCycleBlocks.m, objc_blockretain_a_in_block_cycle_3, 1, RETAIN_CYCLE, ERROR, [start of procedure block]
-codetoanalyze/objc/errors/memory_leaks_benchmark/RetainCycleBlocks.m, retain_a_in_block_cycle, 5, RETAIN_CYCLE, ERROR, [start of procedure retain_a_in_block_cycle()]
+codetoanalyze/objc/errors/memory_leaks_benchmark/RetainCycleBlocks.m, retain_a_in_block_cycle, 4, RETAIN_CYCLE, ERROR, [start of procedure retain_a_in_block_cycle()]
-codetoanalyze/objc/errors/memory_leaks_benchmark/RetainCyclePropertyInProtocol.m, main_bad, 2, RETAIN_CYCLE, ERROR, [start of procedure main_bad(),start of procedure loadViewBad,return from a call to MyCustomViewController_loadViewBad]
+codetoanalyze/objc/errors/memory_leaks_benchmark/RetainCyclePropertyInProtocol.m, MyCustomViewController_loadViewBad, 3, RETAIN_CYCLE, ERROR, [start of procedure loadViewBad]
 codetoanalyze/objc/errors/memory_leaks_benchmark/retain_cycle.m, strongcycle, 6, RETAIN_CYCLE, ERROR, [start of procedure strongcycle()]
-codetoanalyze/objc/errors/memory_leaks_benchmark/retain_cycle2.m, strongcycle2, 4, RETAIN_CYCLE, ERROR, [start of procedure strongcycle2(),start of procedure init,return from a call to Parent_init,start of procedure init,return from a call to Child_init,start of procedure setChild:,return from a call to Parent_setChild:,start of procedure setParent:,return from a call to Child_setParent:]
+codetoanalyze/objc/errors/memory_leaks_benchmark/retain_cycle2.m, strongcycle2, 4, RETAIN_CYCLE, ERROR, [start of procedure strongcycle2(),start of procedure init,return from a call to Parent_init,start of procedure init,return from a call to Child_init,start of procedure setChild:,return from a call to Parent_setChild:]
 codetoanalyze/objc/errors/npe/UpdateDict.m, add_nil_in_dict, 10, NULL_DEREFERENCE, ERROR, [start of procedure add_nil_in_dict(),Skipping dictionaryWithObjectsAndKeys:: function or method not found]
 codetoanalyze/objc/errors/npe/UpdateDict.m, add_nil_to_array, 4, NULL_DEREFERENCE, ERROR, [start of procedure add_nil_to_array()]
 codetoanalyze/objc/errors/npe/UpdateDict.m, insert_nil_in_array, 4, NULL_DEREFERENCE, ERROR, [start of procedure insert_nil_in_array()]