[backend] Add missing fields to the tenv in the bi-abduction

Reviewed By: sblackshear

Differential Revision: D7197980

fbshipit-source-id: 56759ff

infer/src/backend/tabulation.ml

@@ -1064,6 +1064,29 @@ let check_uninitialize_dangling_deref caller_pname tenv callee_pname actual_pre
     props
 
 
+let add_missing_field_to_tenv tenv callee_pname hpreds =
+  match Ondemand.get_proc_desc callee_pname with
+  | Some pdesc ->
+      let attrs = Procdesc.get_attributes pdesc in
+      let source_file = attrs.ProcAttributes.loc.Location.file in
+      let callee_tenv_opt = Tenv.load source_file in
+      let add_field_in_hpred hpred =
+        match (callee_tenv_opt, hpred) with
+        | ( Some callee_tenv
+          , Sil.Hpointsto (_, Sil.Estruct (_, _), Exp.Sizeof {typ= {desc= Typ.Tstruct name}}) ) -> (
+          match Tenv.lookup callee_tenv name with
+          | Some {fields} ->
+              List.iter ~f:(fun field -> Tenv.add_field tenv name field) fields
+          | None ->
+              () )
+        | _ ->
+            ()
+      in
+      List.iter ~f:add_field_in_hpred hpreds
+  | None ->
+      ()
+
+
 (** Perform symbolic execution for a single spec *)
 let exe_spec tenv ret_id_opt (n, nspecs) caller_pdesc callee_pname loc prop path_pre
     (spec: Prop.exposed Specs.spec) actual_params formal_params : abduction_res =
@@ -1156,10 +1179,12 @@ let exe_spec tenv ret_id_opt (n, nspecs) caller_pdesc callee_pname loc prop path
             | _ ->
                 false
           in
-          (* missing fields minus hidden fields *)
+          let missing_fld_objc_class, missing_fld_not_objc_class =
-          let missing_fld_not_objc_class =
+            List.partition_tf ~f:(fun hp -> hpred_missing_objc_class hp) missing_fld
-            List.filter ~f:(fun hp -> not (hpred_missing_objc_class hp)) missing_fld
           in
+          if missing_fld_objc_class <> [] then (
+            L.d_strln "Objective-C missing_fld not empty: adding it to current tenv..." ;
+            add_missing_field_to_tenv tenv callee_pname missing_fld_objc_class ) ;
           if not !Config.footprint && split.missing_sigma <> [] then (
             L.d_strln "Implication error: missing_sigma not empty in re-execution" ;
             Invalid_res Missing_sigma_not_empty )

infer/tests/build_systems/codetoanalyze/objc_retain_cycles_weak/AnalyticsTimeSpent.h

@@ -0,0 +1,21 @@
+/*
+ * Copyright (c) 2018 - present Facebook, Inc.
+ * All rights reserved.
+ *
+ * This source code is licensed under the BSD style license found in the
+ * LICENSE file in the root directory of this source tree. An additional grant
+ * of patent rights can be found in the PATENTS file in the same directory.
+ */
+#import <Foundation/NSObject.h>
+
+@interface AnalyticsTimeSpent : NSObject
+
+@property(nonatomic, weak) id delegate;
+
+@property(nonatomic, strong) id strong_delegate;
+
+- (instancetype)initWithDelegate:(id)delegateObject;
+
+- (instancetype)initWithStrongDelegate:(id)delegateObject;
+
+@end

infer/tests/build_systems/codetoanalyze/objc_retain_cycles_weak/AnalyticsTimeSpent.m

@@ -0,0 +1,26 @@
+/*
+ * Copyright (c) 2018 - present Facebook, Inc.
+ * All rights reserved.
+ *
+ * This source code is licensed under the BSD style license found in the
+ * LICENSE file in the root directory of this source tree. An additional grant
+ * of patent rights can be found in the PATENTS file in the same directory.
+ */
+#import "AnalyticsTimeSpent.h"
+#import "TimeSpent.h"
+
+@implementation AnalyticsTimeSpent
+
+@synthesize delegate;
+
+- (instancetype)initWithDelegate:(id)delegateObject {
+  [self setDelegate:delegateObject];
+  return self;
+}
+
+- (instancetype)initWithStrongDelegate:(id)delegateObject {
+  _strong_delegate = delegateObject;
+  return self;
+}
+
+@end

infer/tests/build_systems/codetoanalyze/objc_retain_cycles_weak/TimeSpent.h

@@ -0,0 +1,14 @@
+/*
+ * Copyright (c) 2018 - present Facebook, Inc.
+ * All rights reserved.
+ *
+ * This source code is licensed under the BSD style license found in the
+ * LICENSE file in the root directory of this source tree. An additional grant
+ * of patent rights can be found in the PATENTS file in the same directory.
+ */
+#import <Foundation/NSObject.h>
+#import "AnalyticsTimeSpent.h"
+
+@interface TimeSpent : NSObject
+- (instancetype)init;
+@end

infer/tests/build_systems/codetoanalyze/objc_retain_cycles_weak/TimeSpent.m

@@ -0,0 +1,39 @@
+/*
+ * Copyright (c) 2018 - present Facebook, Inc.
+ * All rights reserved.
+ *
+ * This source code is licensed under the BSD style license found in the
+ * LICENSE file in the root directory of this source tree. An additional grant
+ * of patent rights can be found in the PATENTS file in the same directory.
+ */
+#import "TimeSpent.h"
+#import "AnalyticsTimeSpent.h"
+
+@interface TimeSpent () {
+  AnalyticsTimeSpent* _timeSpent;
+}
+@end
+
+@implementation TimeSpent
+- (instancetype)init {
+  _timeSpent = [[AnalyticsTimeSpent alloc] initWithDelegate:self];
+  return self;
+}
+
+- (void)setAnalyticsTimeSpent:(AnalyticsTimeSpent*)timeSpent {
+  _timeSpent = timeSpent;
+}
+@end
+
+int retain_cycle_weak_good() {
+  TimeSpent* ts = [TimeSpent new];
+  return 0;
+}
+
+int retain_cycle_weak_bad() {
+  TimeSpent* ts = [[TimeSpent alloc] init];
+  AnalyticsTimeSpent* ats =
+      [[AnalyticsTimeSpent alloc] initWithStrongDelegate:ts];
+  [ts setAnalyticsTimeSpent:ats];
+  return 0;
+}

infer/tests/build_systems/objc_retain_cycles_weak/Makefile

@@ -0,0 +1,23 @@
+# Copyright (c) 2017 - present Facebook, Inc.
+# All rights reserved.
+#
+# This source code is licensed under the BSD style license found in the
+# LICENSE file in the root directory of this source tree. An additional grant
+# of patent rights can be found in the PATENTS file in the same directory.
+
+TESTS_DIR = ../..
+ROOT_DIR = $(TESTS_DIR)/../..
+CODETOANALYZE_DIR = ../codetoanalyze/objc_retain_cycles_weak
+
+ANALYZER = checkers
+SOURCES = $(CODETOANALYZE_DIR)/TimeSpent.m $(CODETOANALYZE_DIR)/AnalyticsTimeSpent.m
+OBJECTS = $(CODETOANALYZE_DIR)/TimeSpent.o $(CODETOANALYZE_DIR)/AnalyticsTimeSpent.o
+INFER_OPTIONS = --biabduction-only --report-custom-error --developer-mode --project-root $(TESTS_DIR)
+INFERPRINT_OPTIONS = --project-root $(TESTS_DIR) --issues-tests
+
+include $(TESTS_DIR)/infer.make
+
+infer-out/report.json: $(CLANG_DEPS) $(SOURCES) $(MAKEFILE_LIST)
+	$(QUIET)$(REMOVE_DIR) buck-out && \
+	$(call silent_on_success,Testing analysis with Objective-C retain cycles on weak properties,\
+	$(INFER_BIN) $(INFER_OPTIONS) --results-dir $(CURDIR)/infer-out -- clang -c  -fobjc-arc $(SOURCES))

infer/tests/build_systems/objc_retain_cycles_weak/issues.exp

@@ -0,0 +1 @@
+build_systems/codetoanalyze/objc_retain_cycles_weak/TimeSpent.m, retain_cycle_weak_bad, 4, RETAIN_CYCLE, [start of procedure retain_cycle_weak_bad(),start of procedure init,start of procedure initWithDelegate:,return from a call to AnalyticsTimeSpent_initWithDelegate:,return from a call to TimeSpent_init,start of procedure initWithStrongDelegate:,return from a call to AnalyticsTimeSpent_initWithStrongDelegate:,start of procedure setAnalyticsTimeSpent:,return from a call to TimeSpent_setAnalyticsTimeSpent:]