From 716bb1939cee4a018174c4d2f1178df804b686de Mon Sep 17 00:00:00 2001 From: Dulma Churchill Date: Tue, 13 Mar 2018 05:32:35 -0700 Subject: [PATCH] [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 | 31 +++++++++++++-- .../AnalyticsTimeSpent.h | 21 ++++++++++ .../AnalyticsTimeSpent.m | 26 +++++++++++++ .../objc_retain_cycles_weak/TimeSpent.h | 14 +++++++ .../objc_retain_cycles_weak/TimeSpent.m | 39 +++++++++++++++++++ .../objc_retain_cycles_weak/Makefile | 23 +++++++++++ .../objc_retain_cycles_weak/issues.exp | 1 + 7 files changed, 152 insertions(+), 3 deletions(-) create mode 100644 infer/tests/build_systems/codetoanalyze/objc_retain_cycles_weak/AnalyticsTimeSpent.h create mode 100644 infer/tests/build_systems/codetoanalyze/objc_retain_cycles_weak/AnalyticsTimeSpent.m create mode 100644 infer/tests/build_systems/codetoanalyze/objc_retain_cycles_weak/TimeSpent.h create mode 100644 infer/tests/build_systems/codetoanalyze/objc_retain_cycles_weak/TimeSpent.m create mode 100644 infer/tests/build_systems/objc_retain_cycles_weak/Makefile create mode 100644 infer/tests/build_systems/objc_retain_cycles_weak/issues.exp diff --git a/infer/src/backend/tabulation.ml b/infer/src/backend/tabulation.ml index 59f751df0..b2ca5aa34 100644 --- a/infer/src/backend/tabulation.ml +++ b/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_not_objc_class = - List.filter ~f:(fun hp -> not (hpred_missing_objc_class hp)) missing_fld + let missing_fld_objc_class, missing_fld_not_objc_class = + List.partition_tf ~f:(fun hp -> 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 ) diff --git a/infer/tests/build_systems/codetoanalyze/objc_retain_cycles_weak/AnalyticsTimeSpent.h b/infer/tests/build_systems/codetoanalyze/objc_retain_cycles_weak/AnalyticsTimeSpent.h new file mode 100644 index 000000000..1234f5ea5 --- /dev/null +++ b/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 + +@interface AnalyticsTimeSpent : NSObject + +@property(nonatomic, weak) id delegate; + +@property(nonatomic, strong) id strong_delegate; + +- (instancetype)initWithDelegate:(id)delegateObject; + +- (instancetype)initWithStrongDelegate:(id)delegateObject; + +@end diff --git a/infer/tests/build_systems/codetoanalyze/objc_retain_cycles_weak/AnalyticsTimeSpent.m b/infer/tests/build_systems/codetoanalyze/objc_retain_cycles_weak/AnalyticsTimeSpent.m new file mode 100644 index 000000000..73e6397a6 --- /dev/null +++ b/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 diff --git a/infer/tests/build_systems/codetoanalyze/objc_retain_cycles_weak/TimeSpent.h b/infer/tests/build_systems/codetoanalyze/objc_retain_cycles_weak/TimeSpent.h new file mode 100644 index 000000000..017d9604a --- /dev/null +++ b/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 +#import "AnalyticsTimeSpent.h" + +@interface TimeSpent : NSObject +- (instancetype)init; +@end diff --git a/infer/tests/build_systems/codetoanalyze/objc_retain_cycles_weak/TimeSpent.m b/infer/tests/build_systems/codetoanalyze/objc_retain_cycles_weak/TimeSpent.m new file mode 100644 index 000000000..51647d3ad --- /dev/null +++ b/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; +} diff --git a/infer/tests/build_systems/objc_retain_cycles_weak/Makefile b/infer/tests/build_systems/objc_retain_cycles_weak/Makefile new file mode 100644 index 000000000..9719a957f --- /dev/null +++ b/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)) diff --git a/infer/tests/build_systems/objc_retain_cycles_weak/issues.exp b/infer/tests/build_systems/objc_retain_cycles_weak/issues.exp new file mode 100644 index 000000000..2bc41937d --- /dev/null +++ b/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:]