From 6b67a570295a79c5bb1ddd68bed5bc08ffdab46c Mon Sep 17 00:00:00 2001 From: Daiva Naudziuniene Date: Wed, 30 Jun 2021 05:39:30 -0700 Subject: [PATCH] [pulse][objc][nil] Add constraint `self > 0` before computing spec for Objective-C instance methods Summary: Adding constraint `self > 0` after computing specs for Objective-C instance methods were causing false positives of the heuristics not to discard `self=0 /\ self|->-` (added new test testAnotherObjectUseSelfOk was FP). This diff adds constrain `self > 0` before computing Objective-C specs, discarding unsatisfiable `self > 0 /\ self =0`. Reviewed By: skcho Differential Revision: D29462462 fbshipit-source-id: 088ee447e --- infer/src/pulse/Pulse.ml | 5 +++- infer/src/pulse/PulseObjectiveCSummary.ml | 20 ++++++++------- infer/src/pulse/PulseObjectiveCSummary.mli | 9 +++++-- .../codetoanalyze/objcpp/pulse/NPEBasic.mm | 25 ++++++++++++++++++- .../codetoanalyze/objcpp/pulse/issues.exp | 1 + 5 files changed, 47 insertions(+), 13 deletions(-) diff --git a/infer/src/pulse/Pulse.ml b/infer/src/pulse/Pulse.ml index 7029e2343..124ca61f0 100644 --- a/infer/src/pulse/Pulse.ml +++ b/infer/src/pulse/Pulse.ml @@ -474,7 +474,10 @@ let with_debug_exit_node proc_desc ~f = let checker ({InterproceduralAnalysis.tenv; proc_desc; err_log} as analysis_data) = AbstractValue.State.reset () ; let initial_astate = ExecutionDomain.mk_initial tenv proc_desc in - let initial = [(initial_astate, PathContext.initial)] in + let initial_self_positive = + PulseObjectiveCSummary.append_objc_self_positive analysis_data initial_astate + in + let initial = List.map ~f:(fun initial -> (initial, PathContext.initial)) initial_self_positive in match DisjunctiveAnalyzer.compute_post analysis_data ~initial proc_desc with | Some posts -> (* forget path contexts, we don't propagate them across functions *) diff --git a/infer/src/pulse/PulseObjectiveCSummary.ml b/infer/src/pulse/PulseObjectiveCSummary.ml index 07b0dfbeb..e8a68f871 100644 --- a/infer/src/pulse/PulseObjectiveCSummary.ml +++ b/infer/src/pulse/PulseObjectiveCSummary.ml @@ -88,20 +88,23 @@ let mk_objc_method_nil_summary tenv proc_desc initial = let append_objc_self_positive {InterproceduralAnalysis.tenv; proc_desc; err_log} astate = let location = Procdesc.get_loc proc_desc in let self = mk_objc_self_pvar proc_desc in - match astate with - | ContinueProgram astate -> + let proc_name = Procdesc.get_proc_name proc_desc in + match (astate, proc_name) with + | ContinueProgram astate, Procname.ObjC_Cpp {kind= ObjCInstanceMethod} + when Procdesc.is_ret_type_pod proc_desc -> let result = let* astate, value = PulseOperations.eval_deref PathContext.initial location (Lvar self) astate in - PulseArithmetic.prune_positive (fst value) astate + PulseArithmetic.and_positive (fst value) astate in PulseReport.report_result tenv proc_desc err_log location result - | ExitProgram _ - | AbortProgram _ - | LatentAbortProgram _ - | LatentInvalidAccess _ - | ISLLatentMemoryError _ -> + | ContinueProgram _, _ + | ExitProgram _, _ + | AbortProgram _, _ + | LatentAbortProgram _, _ + | LatentInvalidAccess _, _ + | ISLLatentMemoryError _, _ -> [astate] @@ -148,5 +151,4 @@ let update_objc_method_posts ({InterproceduralAnalysis.tenv; proc_desc; err_log} | Some result -> let location = Procdesc.get_loc proc_desc in let nil_summary = PulseReport.report_result tenv proc_desc err_log location result in - let posts = List.concat_map ~f:(append_objc_self_positive analysis_data) posts in nil_summary @ posts diff --git a/infer/src/pulse/PulseObjectiveCSummary.mli b/infer/src/pulse/PulseObjectiveCSummary.mli index 552519a53..2e2b289c3 100644 --- a/infer/src/pulse/PulseObjectiveCSummary.mli +++ b/infer/src/pulse/PulseObjectiveCSummary.mli @@ -14,8 +14,8 @@ val update_objc_method_posts : -> initial_astate:ExecutionDomain.t -> posts:ExecutionDomain.t list -> ExecutionDomain.t list -(** For ObjC instance methods: adds path condition `self > 0` to given posts and appends additional - nil summary. Does nothing to posts for other kinds of methods *) +(** For ObjC instance methods: appends additional nil summary and replaces must be valid reason for + non-pod return type. Does nothing to posts for other kinds of methods *) val append_objc_actual_self_positive : Procdesc.t @@ -23,5 +23,10 @@ val append_objc_actual_self_positive : -> AbductiveDomain.t -> AbductiveDomain.t AccessResult.t +val append_objc_self_positive : + PulseSummary.t InterproceduralAnalysis.t -> ExecutionDomain.t -> ExecutionDomain.t list +(** For ObjC instance methods: adds path condition `self > 0` to a given post. Does nothing to posts + for other kinds of methods *) + val mk_objc_method_nil_summary : Tenv.t -> Procdesc.t -> ExecutionDomain.t -> AbductiveDomain.t AccessResult.t option diff --git a/infer/tests/codetoanalyze/objcpp/pulse/NPEBasic.mm b/infer/tests/codetoanalyze/objcpp/pulse/NPEBasic.mm index e96cf8b03..87df40604 100644 --- a/infer/tests/codetoanalyze/objcpp/pulse/NPEBasic.mm +++ b/infer/tests/codetoanalyze/objcpp/pulse/NPEBasic.mm @@ -8,10 +8,21 @@ #import #include +@interface AnotherObject : NSObject +- (int)someMethod:(int)param1; +@end + +@implementation AnotherObject +- (int)someMethod:(int)param1 { + return param1; +} +@end + @interface SomeObject : NSObject @property int x; @property std::shared_ptr ptr; +@property AnotherObject* anotherObject; - (int)returnsPOD; @@ -28,7 +39,6 @@ - (SomeObject*)get; + (NSString*)returnsStringNil; - @end @implementation SomeObject @@ -53,6 +63,10 @@ return nil; } +- (int)callAnotherObjectMethod { + return [_anotherObject someMethod:[self returnsPOD]]; +} + - (SomeObject*)get { SomeObject* o = [SomeObject new]; return o; @@ -74,6 +88,10 @@ return shared; } +- (int)methodNilDereferenceBad { + int* x = nil; + return *x; +} @end int dereferenceNilBad() { @@ -470,3 +488,8 @@ std::shared_ptr unknown_call_twice_FP() { } return [[SomeObject sharedInstance] returnsnonPOD]; } + +int testAnotherObjectUseSelfOk() { + auto const obj = [SomeObject returnsNil]; + return [obj callAnotherObjectMethod]; +} diff --git a/infer/tests/codetoanalyze/objcpp/pulse/issues.exp b/infer/tests/codetoanalyze/objcpp/pulse/issues.exp index a9d52d1a4..a007e05e9 100644 --- a/infer/tests/codetoanalyze/objcpp/pulse/issues.exp +++ b/infer/tests/codetoanalyze/objcpp/pulse/issues.exp @@ -1,4 +1,5 @@ codetoanalyze/objcpp/pulse/AllocPatternMemLeak.mm, A.create_no_release_leak_bad, 1, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by `ABFDataCreate` here,memory becomes unreachable here] +codetoanalyze/objcpp/pulse/NPEBasic.mm, SomeObject.methodNilDereferenceBad, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here] codetoanalyze/objcpp/pulse/NPEBasic.mm, addNilInArrayBad, 0, NIL_INSERTION_INTO_COLLECTION, no_bucket, ERROR, [is the null pointer,in call to `NSMutableArray.addObject:` (modelled),invalid access occurs here] codetoanalyze/objcpp/pulse/NPEBasic.mm, addNilInDictBad, 2, NIL_INSERTION_INTO_COLLECTION, no_bucket, ERROR, [is the null pointer,assigned,in call to `NSMutableDictionary.setObject:forKey:` (modelled),invalid access occurs here] codetoanalyze/objcpp/pulse/NPEBasic.mm, addNilKeyInDictBracketsBad, 2, NIL_INSERTION_INTO_COLLECTION, no_bucket, ERROR, [is the null pointer,assigned,in call to `mutableDictionary[someKey] = value` (modelled),invalid access occurs here]