[retain cycles] Improve the filtering of retain cycles reporting

Summary:
Before we were a bit inconsistent when filtering the objects that can make the cycle that we report: we were checking only some of the objects in the cycle, now we check the properties in all the objects.

The properties are:
1. Non nil
2. Not part of a cycle previously reported
3. Known (We have a decompiler value for it)
4. We only take into account ObjC classes or blocks

This means that we can be sure that we won't report on cycles that include structs or C++ classes.

Reviewed By: skcho

Differential Revision: D56636988

fbshipit-source-id: 6c5bb8ce17c10b1f79b905139917e4e76b0593ff

infer/src/pulse/PulseRetainCycleChecker.ml

@@ -9,7 +9,7 @@ open PulseBasicInterface
 open PulseDomainInterface
 open PulseOperationResult.Import
 
-let is_ref_counted_or_block addr astate =
+let is_ref_counted_or_block astate addr =
  AddressAttributes.get_static_type addr astate
  |> Option.exists ~f:(fun typ_name -> Typ.Name.is_objc_class typ_name)
  ||
@@ -24,7 +24,7 @@ let rec crop_seen_to_cycle seen_list addr =
  match seen_list with
  | [] ->
  []
- | (value, _) :: rest ->
+ | (value, _, _) :: rest ->
  if AbstractValue.equal value addr then seen_list else crop_seen_to_cycle rest addr
 
 
@@ -38,20 +38,20 @@ let remove_non_objc_objects cycle astate =
 
 
 let add_missing_objects path loc cycle astate =
- let add_missing_object (astate, cycle) addr_hist =
- if has_static_dynamic_type astate (fst addr_hist) then
+ let add_missing_object (astate, cycle) (addr, hist, _) =
+ if has_static_dynamic_type astate addr then
  match
- PulseOperations.eval_access path NoAccess loc addr_hist MemoryAccess.TakeAddress astate
+ PulseOperations.eval_access path NoAccess loc (addr, hist) MemoryAccess.TakeAddress astate
  with
  | Ok (astate, (value, hist)) | Recoverable ((astate, (value, hist)), _) ->
  if
  not
- (List.mem cycle (value, hist) ~equal:(fun (value1, _) (value2, _) ->
+ (List.exists cycle ~f:(fun (value1, _, _) ->
  let expr1 = Decompiler.find value1 astate in
- let expr2 = Decompiler.find value2 astate in
- AbstractValue.equal value1 value2
- || DecompilerExpr.decomp_source_expr_equal expr1 expr2 ) )
- then (astate, (value, hist) :: cycle)
+ let expr = Decompiler.find value astate in
+ AbstractValue.equal value1 value
+ || DecompilerExpr.decomp_source_expr_equal expr1 expr ) )
+ then (astate, (value, hist, MemoryAccess.Dereference) :: cycle)
  else (astate, cycle)
  | _ ->
  (astate, cycle)
@@ -94,6 +94,25 @@ let create_values astate cycle =
  sorted_values
 
 
+let should_report_cycle astate cycle =
+ let addr_in_retain_cycle (addr, _, access) =
+ let not_previously_reported = not (AddressAttributes.is_in_reported_retain_cycle addr astate) in
+ let path_condition = astate.AbductiveDomain.path_condition in
+ let is_not_null = not (PulseFormula.is_known_zero path_condition addr) in
+ let value = Decompiler.find addr astate in
+ let is_known = not (DecompilerExpr.is_unknown value) in
+ let is_objc_or_block =
+ match access with
+ | MemoryAccess.FieldAccess _ ->
+ is_ref_counted_or_block astate addr
+ | _ ->
+ true
+ in
+ not_previously_reported && is_not_null && is_known && is_objc_or_block
+ in
+ List.for_all ~f:addr_in_retain_cycle cycle
+
+
 (* A retain cycle is a memory path from an address to itself, following only
  strong references. From that definition, detecting them can be made
  trivial:
@@ -114,40 +133,27 @@ let create_values astate cycle =
 let check_retain_cycles path tenv location addresses orig_astate =
  (* remember explored adresses to avoid reexploring path without retain cycles *)
  let checked = ref AbstractValue.Set.empty in
+ let is_seen l addr = List.exists ~f:(fun (value, _, _) -> AbstractValue.equal value addr) l in
  let check_retain_cycle src_addr =
- let rec contains_cycle ~seen (addr, hist) astate =
- (* [seen] tracks addresses met in the current path
- [addr] is the address to explore
- *)
+ let rec contains_cycle ~rev_seen (addr, hist) astate =
  if AbstractValue.Set.mem addr !checked then Ok astate
- else
- let value = Decompiler.find addr astate in
- let is_known = not (DecompilerExpr.is_unknown value) in
- let is_seen =
- List.mem
- ~equal:(fun (value1, _) (value2, _) -> AbstractValue.equal value1 value2)
- seen (addr, hist)
- in
- let is_ref_counted_or_block = is_ref_counted_or_block addr astate in
- let not_previously_reported =
- not (AddressAttributes.is_in_reported_retain_cycle addr astate)
- in
- let path_condition = astate.AbductiveDomain.path_condition in
- let is_not_null = not (PulseFormula.is_known_zero path_condition addr) in
- if is_known && is_seen && is_ref_counted_or_block && not_previously_reported && is_not_null
- then
- let seen = List.rev seen in
- let cycle = crop_seen_to_cycle seen addr in
+ else if is_seen rev_seen addr then
+ let seen = List.rev rev_seen in
+ let cycle = crop_seen_to_cycle seen addr in
+ if should_report_cycle astate cycle then (
  let astate, cycle = add_missing_objects path location cycle astate in
- let cycle = List.map ~f:fst cycle in
+ Logging.d_printfln "Found cycle %a"
+ (Pp.seq ~sep:"->" AbstractValue.pp)
+ (List.map ~f:(fun (addr, _, _) -> addr) cycle) ;
+ let cycle = List.map ~f:(fun (addr, _, _) -> addr) cycle in
  let cycle = remove_non_objc_objects cycle astate in
  let values = create_values astate cycle in
  if List.exists ~f:(fun {Diagnostic.trace} -> Option.is_some trace) values then
  match List.rev values with
  | {Diagnostic.trace} :: _ ->
  let astate =
  List.fold ~init:astate
- ~f:(fun astate (addr, _) ->
+ ~f:(fun astate (addr, _, _) ->
  AddressAttributes.in_reported_retain_cycle addr astate )
  seen
  in
@@ -160,46 +166,40 @@ let check_retain_cycles path tenv location addresses orig_astate =
  Recoverable (astate, [ReportableError {astate; diagnostic}])
  | [] ->
  Ok astate
- else Ok astate
- else (
- if is_seen && ((not is_known) || not is_ref_counted_or_block) then
- (* add the `UNKNOWN` address at which we have found a cycle to the [checked]
- list in case we would have a cycle of `UNKNOWN` addresses, to avoid
- looping forever. Also add the not ref_counted addresses to checked, since
- we could loop forever otherwise *)
- checked := AbstractValue.Set.add addr !checked ;
- let res =
- AbductiveDomain.Memory.fold_edges ~init:(Ok astate) addr astate
- ~f:(fun acc (access, (accessed_addr, accessed_hist)) ->
- match acc with
- | Recoverable _ | FatalError _ ->
- acc
- | Ok astate ->
- if PulseRefCounting.is_strong_access tenv access then
- (* This is needed to update the decompiler and be able to get good values when printing the path (above).
- We don't want to return those changes in the decompiler to the rest of the analysis though, that was
- changing some tests. So this checker only returns errors, but not the changes to the state. *)
- let astate =
- if not is_known then Memory.eval_edge (addr, hist) access astate |> fst
- else astate
- in
- let seen = (addr, hist) :: seen in
- contains_cycle ~seen (accessed_addr, accessed_hist) astate
- else Ok astate )
- in
- (* all paths down [addr] have been explored *)
- checked := AbstractValue.Set.add addr !checked ;
- res )
+ else Ok astate )
+ else Ok astate
+ else
+ let res =
+ AbductiveDomain.Memory.fold_edges ~init:(Ok astate) addr astate
+ ~f:(fun acc (access, (accessed_addr, accessed_hist)) ->
+ match acc with
+ | Recoverable _ | FatalError _ ->
+ acc
+ | Ok astate ->
+ if PulseRefCounting.is_strong_access tenv access then
+ (* This is needed to update the decompiler and be able to get good values when printing the path (above).
+ We don't want to return those changes in the decompiler to the rest of the analysis though, that was
+ changing some tests. So this checker only returns errors, but not the changes to the state. *)
+ let astate =
+ let value = Decompiler.find addr astate in
+ if DecompilerExpr.is_unknown value then
+ Memory.eval_edge (addr, hist) access astate |> fst
+ else astate
+ in
+ let rev_seen = (addr, hist, access) :: rev_seen in
+ contains_cycle ~rev_seen (accessed_addr, accessed_hist) astate
+ else Ok astate )
+ in
+ (* all paths down [addr] have been explored *)
+ checked := AbstractValue.Set.add addr !checked ;
+ res
  in
- contains_cycle ~seen:[] src_addr orig_astate
+ contains_cycle ~rev_seen:[] src_addr orig_astate
  in
+ Logging.d_printfln "checking retain cycles, addresses to check are %a"
+ (Pp.comma_seq AbstractValue.pp) (List.map ~f:fst addresses) ;
  List.fold addresses ~init:(Ok orig_astate) ~f:(fun acc (addr, hist) ->
- match acc with
- | Recoverable _ | FatalError _ ->
- acc
- | Ok astate ->
- if is_ref_counted_or_block addr orig_astate then check_retain_cycle (addr, hist)
- else Ok astate )
+ match acc with Recoverable _ | FatalError _ -> acc | Ok _ -> check_retain_cycle (addr, hist) )
 
 
 let check_retain_cycles_call path tenv location func_args ret_opt astate =

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

@@ -146,7 +146,6 @@ codetoanalyze/objc/pulse/retain_cycles/BlockInHeap.m, BlockInHeap.assign_strong_
 codetoanalyze/objc/pulse/retain_cycles/BrokenCycles.m, broken_strong_cycle_good_FP, 5, RETAIN_CYCLE, no_bucket, ERROR, [assignment of a_obj->_b part of the trace starts here,allocated by call to `alloc` (modelled),assigned,when calling `ClassA.setB:` here,parameter `self` of ClassA.setB:,assigned,assignment of b_obj->_a part of the trace starts here,allocated by call to `alloc` (modelled),in call to `ClassBStrong.init`,parameter `self` of ClassBStrong.init,in call to `NSObject.init` (modelled),assigned,returned,return from call to `ClassBStrong.init`,assigned,when calling `ClassBStrong.setA:` here,parameter `self` of ClassBStrong.setA:,assigned,retain cycle here]
 codetoanalyze/objc/pulse/retain_cycles/BrokenCycles.m, broken_inner_cycle_good_FP, 5, RETAIN_CYCLE, no_bucket, ERROR, [assignment of b_obj->_a part of the trace starts here,allocated by call to `alloc` (modelled),in call to `ClassBStrong.init`,parameter `self` of ClassBStrong.init,in call to `NSObject.init` (modelled),assigned,returned,return from call to `ClassBStrong.init`,assigned,when calling `ClassBStrong.setA:` here,parameter `self` of ClassBStrong.setA:,assigned,assignment of c_obj.a._b part of the trace starts here,allocated by call to `alloc` (modelled),assigned,allocated by call to `alloc` (modelled),in call to `ClassC.setA:`,parameter `a` of ClassC.setA:,parameter `self` of ClassC.setA:,assigned,return from call to `ClassC.setA:`,in call to `ClassC.a`,parameter `self` of ClassC.a,returned,return from call to `ClassC.a`,when calling `ClassA.setB:` here,parameter `self` of ClassA.setB:,assigned,retain cycle here]
 codetoanalyze/objc/pulse/retain_cycles/BrokenCycles.m, broken_self_strong_cycle_good_FP, 2, RETAIN_CYCLE, no_bucket, ERROR, [assignment of obj->_s part of the trace starts here,allocated by call to `alloc` (modelled),in call to `SelfReferencing.init`,parameter `self` of SelfReferencing.init,in call to `NSObject.init` (modelled),assigned,returned,return from call to `SelfReferencing.init`,assigned,when calling `SelfReferencing.setS:` here,parameter `self` of SelfReferencing.setS:,assigned,retain cycle here]
-codetoanalyze/objc/pulse/retain_cycles/CycleStructExample.m, test_no_retain_cycle_good_FP, 4, RETAIN_CYCLE, no_bucket, ERROR, [assignment of &person part of the trace starts here,when calling `BridgingDelegate.newWithPerson:` here,allocated by call to `alloc` (modelled),in call to `NSObject.init` (modelled),assigned,assigned,assignment of person->_responderBridgingDelegate part of the trace starts here,struct field address `_responderBridgingDelegate` created,assigned,retain cycle here]
 codetoanalyze/objc/pulse/retain_cycles/IvarInheritanceRetainCycle.m, field_superclass_main, 3, RETAIN_CYCLE, no_bucket, ERROR, [assignment of b->a part of the trace starts here,allocated by call to `alloc` (modelled),in call to `NSObject.init` (modelled),assigned,assigned,retain cycle here]
 codetoanalyze/objc/pulse/retain_cycles/RetainCycleBlockAsParameter.m, FBSomeDataManager.fetchNewData_bad, 2, RETAIN_CYCLE, no_bucket, ERROR, [assignment of self->_fetcher part of the trace starts here,parameter `self` of FBSomeDataManager.fetchNewData_bad,assigned,assignment of &block defined in RetainCycleBlockAsParameter.m:46 part of the trace starts here,allocated by call to `alloc` (modelled),when calling `Fetcher.initWithCompletionBlock:` here,parameter `self` of Fetcher.initWithCompletionBlock:,assigned,self captured by block defined in RetainCycleBlockAsParameter.m:46 here,retain cycle here]
 codetoanalyze/objc/pulse/retain_cycles/RetainCycleBlockCapturedVar.m, LinkResolver.test, 3, RETAIN_CYCLE, no_bucket, ERROR, [retainedListener captured by block defined in RetainCycleBlockCapturedVar.m:32 here,assignment of listener->_didFinishLoad part of the trace starts here,allocated by call to `alloc` (modelled),in call to `NSObject.init` (modelled),assigned,when calling `Listener.setDidFinishLoad:` here,parameter `self` of Listener.setDidFinishLoad:,assigned,retainedListener captured by block defined in RetainCycleBlockCapturedVar.m:32 here,retain cycle here]

infer/tests/codetoanalyze/objc/pulse/retain_cycles/CycleStructExample.m

@@ -31,7 +31,7 @@ + (instancetype)newWithPerson:(struct Person*)person {
 
 @end
 
-void test_no_retain_cycle_good_FP() {
+void test_no_retain_cycle_good() {
  struct Person* person = (struct Person*)malloc(sizeof(struct Person));
  BridgingDelegate* responderBridgingDelegate =
  [BridgingDelegate newWithPerson:person];

infer/tests/codetoanalyze/objcpp/retain-cycles/ObjCPPStruct.mm

@@ -24,7 +24,8 @@ - (instancetype)aFnGood {
  return self;
 }
 
-- (instancetype)aFnBad {
+// we only report retain cycles between ObjC objects and blocks
+- (instancetype)aFnGood2 {
  _weakHolder = new WeakHolder();
  _weakHolder->ref = self;
  return self;

infer/tests/codetoanalyze/objcpp/retain-cycles/issues.exp

@@ -1 +0,0 @@
-codetoanalyze/objcpp/retain-cycles/ObjCPPStruct.mm, A.aFnBad, 2, RETAIN_CYCLE, no_bucket, ERROR, [assignment of self->_weakHolder part of the trace starts here,parameter `self` of A.aFnBad,assigned,assignment of self->_weakHolder->ref part of the trace starts here,allocated by call to `new` (modelled),in call to `WeakHolder::WeakHolder`,parameter `this` of WeakHolder::WeakHolder,return from call to `WeakHolder::WeakHolder`,assigned,retain cycle here]