diff --git a/infer/src/pulse/Pulse.ml b/infer/src/pulse/Pulse.ml index 746524648..df84d785e 100644 --- a/infer/src/pulse/Pulse.ml +++ b/infer/src/pulse/Pulse.ml @@ -428,11 +428,15 @@ let with_debug_exit_node proc_desc ~f = let checker ({InterproceduralAnalysis.proc_desc; err_log; tenv} as analysis_data) = AbstractValue.State.reset () ; - let initial = [ExecutionDomain.mk_initial tenv proc_desc] in + let initial_astate = ExecutionDomain.mk_initial tenv proc_desc in + let initial = [initial_astate] in match DisjunctiveAnalyzer.compute_post analysis_data ~initial proc_desc with | Some posts -> with_debug_exit_node proc_desc ~f:(fun () -> - let summary = PulseSummary.of_posts proc_desc posts in + let updated_posts = + PulseObjectiveCSummary.update_objc_method_posts analysis_data ~initial_astate ~posts + in + let summary = PulseSummary.of_posts proc_desc updated_posts in report_topl_errors proc_desc err_log summary ; Some summary ) | None -> diff --git a/infer/src/pulse/PulseObjectiveCSummary.ml b/infer/src/pulse/PulseObjectiveCSummary.ml new file mode 100644 index 000000000..c4b37e7c2 --- /dev/null +++ b/infer/src/pulse/PulseObjectiveCSummary.ml @@ -0,0 +1,70 @@ +(* + * Copyright (c) Facebook, Inc. and its affiliates. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + *) + +open! IStd +open PulseBasicInterface +open PulseOperations.Import + +let mk_objc_self_pvar proc_desc = + let proc_name = Procdesc.get_proc_name proc_desc in + Pvar.mk Mangled.self proc_name + + +let mk_objc_method_nil_summary_aux proc_desc astate = + let location = Procdesc.get_loc proc_desc in + let self = mk_objc_self_pvar proc_desc in + let* astate, self_value = PulseOperations.eval_deref location (Lvar self) astate in + let astate = PulseArithmetic.prune_eq_zero (fst self_value) astate in + let ret_var = Procdesc.get_ret_var proc_desc in + let ret_addr = AbstractValue.mk_fresh () in + let ret_value = (ret_addr, []) in + let* astate, ret_var_addr_hist = PulseOperations.eval Write location (Lvar ret_var) astate in + let* astate = PulseOperations.write_deref location ~ref:ret_var_addr_hist ~obj:ret_value astate in + let astate = PulseArithmetic.and_eq_int ret_addr IntLit.zero astate in + let+ astate = + PulseOperations.invalidate location (ConstantDereference IntLit.zero) ret_value astate + in + [astate] + + +let mk_objc_method_nil_summary ({InterproceduralAnalysis.proc_desc} as analysis_data) initial = + let proc_name = Procdesc.get_proc_name proc_desc in + match (initial, proc_name) with + | ContinueProgram astate, Procname.ObjC_Cpp {kind= ObjCInstanceMethod} -> + let result = mk_objc_method_nil_summary_aux proc_desc astate in + Some (PulseReport.report_list_result analysis_data result) + | ContinueProgram _, _ + | ExitProgram _, _ + | AbortProgram _, _ + | LatentAbortProgram _, _ + | ISLLatentMemoryError _, _ -> + None + + +let append_objc_self_positive ({InterproceduralAnalysis.proc_desc} as analysis_data) astate = + let location = Procdesc.get_loc proc_desc in + let self = mk_objc_self_pvar proc_desc in + match astate with + | ContinueProgram astate -> + let result = + let+ astate, value = PulseOperations.eval_deref location (Lvar self) astate in + let astate = PulseArithmetic.prune_positive (fst value) astate in + [astate] + in + PulseReport.report_list_result analysis_data result + | ExitProgram _ | AbortProgram _ | LatentAbortProgram _ | ISLLatentMemoryError _ -> + [astate] + + +let update_objc_method_posts analysis_data ~initial_astate ~posts = + let nil_summary = mk_objc_method_nil_summary analysis_data initial_astate in + match nil_summary with + | None -> + posts + | Some nil_summary -> + 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 new file mode 100644 index 000000000..3d6bef57d --- /dev/null +++ b/infer/src/pulse/PulseObjectiveCSummary.mli @@ -0,0 +1,17 @@ +(* + * Copyright (c) Facebook, Inc. and its affiliates. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + *) + +open! IStd +open PulseDomainInterface + +val update_objc_method_posts : + PulseSummary.t InterproceduralAnalysis.t + -> 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 *) diff --git a/infer/tests/codetoanalyze/objcpp/pulse/NPEBasic.mm b/infer/tests/codetoanalyze/objcpp/pulse/NPEBasic.mm index b4462030b..b2bf322db 100644 --- a/infer/tests/codetoanalyze/objcpp/pulse/NPEBasic.mm +++ b/infer/tests/codetoanalyze/objcpp/pulse/NPEBasic.mm @@ -17,6 +17,8 @@ - (std::shared_ptr)returnsnonPOD; +- (int)add:(int)param1 andParam2:(int)param2; + @end @implementation SomeObject @@ -29,6 +31,10 @@ return std::shared_ptr(new int(_x)); } +- (int)add:(int)param1 andParam2:(int)param2 { + return _x + param1 + param2; +} + @end int dereferenceNilBad() { @@ -36,32 +42,58 @@ int dereferenceNilBad() { return *int_ptr; } -int FP_testCallMethodReturnsPODOk() { +int testCallMethodReturnsPODOk() { SomeObject* obj = nil; return [obj returnsPOD]; } -std::shared_ptr testCallMethodReturnsnonPODBad() { +std::shared_ptr FN_testCallMethodReturnsnonPODBad() { SomeObject* obj = nil; std::shared_ptr d = [obj returnsnonPOD]; // UB return d; } -int FP_testAccessPropertyAccessorOk() { +int testAccessPropertyAccessorOk() { SomeObject* obj = nil; return obj.x; // calls property accessor method } -std::shared_ptr testAccessPropertyAccessorBad() { +std::shared_ptr FN_testAccessPropertyAccessorBad() { SomeObject* obj = nil; return obj.ptr; // calls property accessor method, but return type is non-POD } int methodReturnsPOD(SomeObject* obj) { return [obj returnsPOD]; }; -int FP_methodReturnsPODNilOk() { return methodReturnsPOD(nil); }; +int methodReturnsPODNilOk() { return methodReturnsPOD(nil); }; int methodReturnsPODNotNilOK() { SomeObject* o = [SomeObject new]; return methodReturnsPOD(o); } + +int testFalsyReturnedValueOk() { + int x = testCallMethodReturnsPODOk(); + + if (x != 0) { + int* int_ptr = nil; + return *int_ptr; + } +} + +int testParamsRemainTheSameOk() { + SomeObject* obj = nil; + int x1 = 0; + int x2 = 5; + int x = [obj add:x1 andParam2:x2]; + + if (x1 != 0) { + int* int_ptr = nil; + return *int_ptr; + } + + if (x2 != 5) { + int* int_ptr = nil; + return *int_ptr; + } +} diff --git a/infer/tests/codetoanalyze/objcpp/pulse/issues.exp b/infer/tests/codetoanalyze/objcpp/pulse/issues.exp index ee421aef9..e79adb911 100644 --- a/infer/tests/codetoanalyze/objcpp/pulse/issues.exp +++ b/infer/tests/codetoanalyze/objcpp/pulse/issues.exp @@ -1,9 +1,4 @@ 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 call to `ABFDataCreate` (modelled),allocation part of the trace ends here,memory becomes unreachable here] -codetoanalyze/objcpp/pulse/NPEBasic.mm, FP_methodReturnsPODNilOk, 0, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,when calling `methodReturnsPOD` here,parameter `obj` of methodReturnsPOD,when calling `SomeObject.returnsPOD` here,parameter `self` of SomeObject.returnsPOD,invalid access occurs here] -codetoanalyze/objcpp/pulse/NPEBasic.mm, FP_testAccessPropertyAccessorOk, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,assigned,when calling `SomeObject.x` here,parameter `self` of SomeObject.x,invalid access occurs here] -codetoanalyze/objcpp/pulse/NPEBasic.mm, FP_testCallMethodReturnsPODOk, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,assigned,when calling `SomeObject.returnsPOD` here,parameter `self` of SomeObject.returnsPOD,invalid access occurs here] codetoanalyze/objcpp/pulse/NPEBasic.mm, dereferenceNilBad, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here] -codetoanalyze/objcpp/pulse/NPEBasic.mm, testAccessPropertyAccessorBad, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,assigned,when calling `SomeObject.ptr` here,parameter `self` of SomeObject.ptr,invalid access occurs here] -codetoanalyze/objcpp/pulse/NPEBasic.mm, testCallMethodReturnsnonPODBad, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,assigned,when calling `SomeObject.returnsnonPOD` here,parameter `self` of SomeObject.returnsnonPOD,invalid access occurs here] codetoanalyze/objcpp/pulse/use_after_delete.mm, PulseTest.deref_deleted_in_objc_method_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,passed as argument to `new` (modelled),return from call to `new` (modelled),assigned,was invalidated by `delete`,use-after-lifetime part of the trace starts here,passed as argument to `new` (modelled),return from call to `new` (modelled),assigned,when calling `Simple::Simple` here,parameter `__param_0` of Simple::Simple,invalid access occurs here] codetoanalyze/objcpp/pulse/use_after_delete.mm, deref_deleted_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,passed as argument to `new` (modelled),return from call to `new` (modelled),assigned,was invalidated by `delete`,use-after-lifetime part of the trace starts here,passed as argument to `new` (modelled),return from call to `new` (modelled),assigned,when calling `Simple::Simple` here,parameter `__param_0` of Simple::Simple,invalid access occurs here]