From 923a15fa609faa1fb4417be4dcbe620a29167550 Mon Sep 17 00:00:00 2001 From: Jeremy Dubreil Date: Wed, 11 Oct 2017 13:37:31 -0700 Subject: [PATCH] [infer][clang] initial version of a nullable checker for Clang languages Reviewed By: sblackshear Differential Revision: D5970391 fbshipit-source-id: 6148094 --- infer/src/base/Config.ml | 13 +- infer/src/base/Config.mli | 6 +- infer/src/base/IssueType.ml | 2 + infer/src/base/IssueType.mli | 2 + infer/src/checkers/NullabilityCheck.ml | 121 ++++++++++++++++++ infer/src/checkers/NullabilityCheck.mli | 10 ++ infer/src/checkers/registerCheckers.ml | 1 + .../tests/codetoanalyze/cpp/nullable/Makefile | 2 +- .../codetoanalyze/cpp/nullable/issues.exp | 6 + .../codetoanalyze/cpp/nullable/method.cpp | 55 ++++++++ .../codetoanalyze/objc/checkers/Makefile | 2 +- .../codetoanalyze/objc/checkers/Nullable.m | 21 +++ .../codetoanalyze/objc/checkers/issues.exp | 2 + 13 files changed, 236 insertions(+), 7 deletions(-) create mode 100644 infer/src/checkers/NullabilityCheck.ml create mode 100644 infer/src/checkers/NullabilityCheck.mli create mode 100644 infer/tests/codetoanalyze/cpp/nullable/method.cpp diff --git a/infer/src/base/Config.ml b/infer/src/base/Config.ml index 2fe05d6ac..495f3957c 100644 --- a/infer/src/base/Config.ml +++ b/infer/src/base/Config.ml @@ -586,6 +586,7 @@ and android_harness = and ( annotation_reachability , biabduction , bufferoverrun + , check_nullable , crashcontext , eradicate , fragment_retains_view @@ -612,6 +613,9 @@ and ( annotation_reachability mk_checker ~long:"biabduction" "the separation logic based bi-abduction analysis using the checkers framework" and bufferoverrun = mk_checker ~long:"bufferoverrun" "the buffer overrun analysis" + and check_nullable = + mk_checker ~long:"check-nullable" + "checks that values annotated with nullable are always checked for null before dereference" and crashcontext = mk_checker ~long:"crashcontext" "the crashcontext checker for Java stack trace context reconstruction" @@ -665,6 +669,7 @@ and ( annotation_reachability ( annotation_reachability , biabduction , bufferoverrun + , check_nullable , crashcontext , eradicate , fragment_retains_view @@ -1974,11 +1979,11 @@ and buck_out = !buck_out and bufferoverrun = !bufferoverrun -and changed_files_index = !changed_files_index - and calls_csv = !calls_csv -and dump_duplicate_symbols = !dump_duplicate_symbols +and changed_files_index = !changed_files_index + +and check_nullable = !check_nullable and clang_biniou_file = !clang_biniou_file @@ -2026,6 +2031,8 @@ and differential_filter_set = !differential_filter_set and dotty_cfg_libs = !dotty_cfg_libs +and dump_duplicate_symbols = !dump_duplicate_symbols + and eradicate = !eradicate and eradicate_condition_redundant = !eradicate_condition_redundant diff --git a/infer/src/base/Config.mli b/infer/src/base/Config.mli index 8d08ca974..abd0ed76f 100644 --- a/infer/src/base/Config.mli +++ b/infer/src/base/Config.mli @@ -297,13 +297,15 @@ val buck_out : string option val bufferoverrun : bool -val changed_files_index : string option - val calls_csv : string option val captured_dir : string (** directory where the results of the capture phase are stored *) +val changed_files_index : string option + +val check_nullable : bool + val clang_biniou_file : string option val clang_frontend_action_string : string diff --git a/infer/src/base/IssueType.ml b/infer/src/base/IssueType.ml index 46c349998..6805f291e 100644 --- a/infer/src/base/IssueType.ml +++ b/infer/src/base/IssueType.ml @@ -228,6 +228,8 @@ let null_dereference = from_string "NULL_DEREFERENCE" let null_test_after_dereference = from_string ~enabled:false "NULL_TEST_AFTER_DEREFERENCE" +let nullable_dereference = from_string "NULLABLE_DEREFERENCE" + let parameter_not_null_checked = from_string "PARAMETER_NOT_NULL_CHECKED" let pointer_size_mismatch = from_string "POINTER_SIZE_MISMATCH" diff --git a/infer/src/base/IssueType.mli b/infer/src/base/IssueType.mli index ea8ede275..f8d1cc777 100644 --- a/infer/src/base/IssueType.mli +++ b/infer/src/base/IssueType.mli @@ -159,6 +159,8 @@ val null_dereference : t val null_test_after_dereference : t +val nullable_dereference : t + val parameter_not_null_checked : t val pointer_size_mismatch : t diff --git a/infer/src/checkers/NullabilityCheck.ml b/infer/src/checkers/NullabilityCheck.ml new file mode 100644 index 000000000..9eb2c0805 --- /dev/null +++ b/infer/src/checkers/NullabilityCheck.ml @@ -0,0 +1,121 @@ +(* + * 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. + *) + +module L = Logging +module MF = MarkupFormatter +module CallSites = AbstractDomain.FiniteSet (CallSite) +module Domain = AbstractDomain.Map (AccessPath) (CallSites) + +module TransferFunctions (CFG : ProcCfg.S) = struct + module CFG = CFG + module Domain = Domain + + type extras = Specs.summary + + let is_instance_method callee_pname = + if Typ.Procname.is_java callee_pname then not (Typ.Procname.java_is_static callee_pname) + else + Option.exists + ~f:(fun attributes -> + attributes.ProcAttributes.is_objc_instance_method + || attributes.ProcAttributes.is_cpp_instance_method) + (Specs.proc_resolve_attributes callee_pname) + + let report_nullable_dereference ap call_sites {ProcData.pdesc; extras} loc = + let pname = Procdesc.get_proc_name pdesc in + let annotation = Localise.nullable_annotation_name pname in + let issue_kind = IssueType.nullable_dereference.unique_id in + let call_site = + try CallSites.min_elt call_sites + with Not_found -> + L.(die InternalError) + "Expecting a least one element in the set of call sites when analyzing %a" + Typ.Procname.pp pname + in + let message = + Format.asprintf + "Variable %a is indirectly annotated with %a (source %a) and is dereferenced without being checked for null" + (MF.wrap_monospaced AccessPath.pp) ap MF.pp_monospaced annotation + (MF.wrap_monospaced CallSite.pp) call_site + in + let exn = Exceptions.Checkers (issue_kind, Localise.verbatim_desc message) in + let summary = extras in + let trace = + let with_origin_site = + let callee_pname = CallSite.pname call_site in + match Specs.proc_resolve_attributes callee_pname with + | None + -> [] + | Some attributes + -> let description = + Format.asprintf "definition of %s" (Typ.Procname.get_method callee_pname) + in + let trace_element = + Errlog.make_trace_element 1 attributes.ProcAttributes.loc description [] + in + [trace_element] + in + let with_assignment_site = + let call_site_loc = CallSite.loc call_site in + if Location.equal call_site_loc loc then with_origin_site + else + let trace_element = + Errlog.make_trace_element 0 call_site_loc "assignment of the nullable value" [] + in + trace_element :: with_origin_site + in + let dereference_site = + let description = Format.asprintf "deference of %a" AccessPath.pp ap in + Errlog.make_trace_element 0 loc description [] + in + dereference_site :: with_assignment_site + in + Reporting.log_error summary ~loc ~ltr:trace exn + + let exec_instr (astate: Domain.astate) proc_data _ (instr: HilInstr.t) : Domain.astate = + match instr with + | Call (Some ret_var, Direct callee_pname, _, _, loc) + when Annotations.pname_has_return_annot callee_pname + ~attrs_of_pname:Specs.proc_resolve_attributes Annotations.ia_is_nullable + -> let call_site = CallSite.make callee_pname loc in + Domain.add (ret_var, []) (CallSites.singleton call_site) astate + | Call (_, Direct callee_pname, (HilExp.AccessPath receiver) :: _, _, loc) + when is_instance_method callee_pname -> ( + match Domain.find_opt receiver astate with + | None + -> astate + | Some call_sites + -> report_nullable_dereference receiver call_sites proc_data loc ; + Domain.remove receiver astate ) + | Call (Some ret_var, _, _, _, _) + -> Domain.remove (ret_var, []) astate + | Assign (lhs, _, loc) when Domain.mem lhs astate + -> report_nullable_dereference lhs (Domain.find lhs astate) proc_data loc ; + Domain.remove lhs astate + | Assign (lhs, HilExp.AccessPath rhs, _) when Domain.mem rhs astate + -> Domain.add lhs (Domain.find rhs astate) astate + | Assign (lhs, _, _) + -> Domain.remove lhs astate + | Assume (HilExp.AccessPath ap, _, _, _) + -> Domain.remove ap astate + | Assume (HilExp.BinaryOperator (Binop.Ne, HilExp.AccessPath ap, exp), _, _, _) + when HilExp.is_null_literal exp + -> Domain.remove ap astate + | _ + -> astate +end + +module Analyzer = + AbstractInterpreter.Make (ProcCfg.Exceptional) (LowerHil.MakeDefault (TransferFunctions)) + +let checker {Callbacks.summary; proc_desc; tenv} = + let initial = (Domain.empty, IdAccessPathMapDomain.empty) in + let proc_data = ProcData.make proc_desc tenv summary in + ignore (Analyzer.compute_post proc_data ~initial ~debug:false) ; + summary diff --git a/infer/src/checkers/NullabilityCheck.mli b/infer/src/checkers/NullabilityCheck.mli new file mode 100644 index 000000000..d6c90bc25 --- /dev/null +++ b/infer/src/checkers/NullabilityCheck.mli @@ -0,0 +1,10 @@ +(* + * 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. + *) + +val checker : Callbacks.proc_callback_t diff --git a/infer/src/checkers/registerCheckers.ml b/infer/src/checkers/registerCheckers.ml index 1b90ae5b8..68ea3031d 100644 --- a/infer/src/checkers/registerCheckers.ml +++ b/infer/src/checkers/registerCheckers.ml @@ -45,6 +45,7 @@ let checkers = , Config.suggest_nullable , [ (Procedure NullabilitySuggest.checker, Config.Java) ; (Procedure NullabilitySuggest.checker, Config.Clang) ] ) + ; ("nullable checks", Config.check_nullable, [(Procedure NullabilityCheck.checker, Config.Clang)]) ; ( "quandary" , Config.quandary , [ (Procedure JavaTaintAnalysis.checker, Config.Java) diff --git a/infer/tests/codetoanalyze/cpp/nullable/Makefile b/infer/tests/codetoanalyze/cpp/nullable/Makefile index 2739f1b77..a5c6d8c78 100644 --- a/infer/tests/codetoanalyze/cpp/nullable/Makefile +++ b/infer/tests/codetoanalyze/cpp/nullable/Makefile @@ -10,7 +10,7 @@ TESTS_DIR = ../../.. ANALYZER = checkers # see explanations in cpp/errors/Makefile for the custom isystem CLANG_OPTIONS = -x c++ -std=c++11 -nostdinc++ -isystem$(ROOT_DIR) -isystem$(CLANG_INCLUDES)/c++/v1/ -c -INFER_OPTIONS = --biabduction --suggest-nullable --debug-exceptions --project-root $(TESTS_DIR) +INFER_OPTIONS = --biabduction --suggest-nullable --check-nullable --debug-exceptions --project-root $(TESTS_DIR) INFERPRINT_OPTIONS = --issues-tests SOURCES = $(wildcard *.cpp) diff --git a/infer/tests/codetoanalyze/cpp/nullable/issues.exp b/infer/tests/codetoanalyze/cpp/nullable/issues.exp index 9e56ea0ef..a31dc2f58 100644 --- a/infer/tests/codetoanalyze/cpp/nullable/issues.exp +++ b/infer/tests/codetoanalyze/cpp/nullable/issues.exp @@ -7,3 +7,9 @@ codetoanalyze/cpp/nullable/example.cpp, T_dereference_unnanotated_field_after_te codetoanalyze/cpp/nullable/example.cpp, T_dereference_unnanotated_field_after_test_for_null_bad, 2, NULL_DEREFERENCE, [start of procedure dereference_unnanotated_field_after_test_for_null_bad,Condition is true] codetoanalyze/cpp/nullable/example.cpp, T_test_nonnull_field_for_null_bad, 1, FIELD_SHOULD_BE_NULLABLE, [Field nonnull_field is compared to null here] codetoanalyze/cpp/nullable/example.cpp, T_test_unnanotated_field_for_null_bad, 1, FIELD_SHOULD_BE_NULLABLE, [Field unnanotated_field is compared to null here] +codetoanalyze/cpp/nullable/method.cpp, FP_reAssigningNullableValueOk, 2, NULLABLE_DEREFERENCE, [deference of &p,assignment of the nullable value,definition of mayReturnNullPointer] +codetoanalyze/cpp/nullable/method.cpp, assignNullableValueBad, 2, NULLABLE_DEREFERENCE, [deference of &p,assignment of the nullable value,definition of mayReturnNullPointer] +codetoanalyze/cpp/nullable/method.cpp, assignNullableValueBad, 2, NULL_DEREFERENCE, [start of procedure assignNullableValueBad(),start of procedure mayReturnNullPointer,Condition is true,return from a call to T_mayReturnNullPointer] +codetoanalyze/cpp/nullable/method.cpp, callMethodOnNullableObjectBad, 1, NULLABLE_DEREFERENCE, [deference of n$2,definition of mayReturnNullObject] +codetoanalyze/cpp/nullable/method.cpp, callMethodOnNullableObjectBad, 1, NULL_DEREFERENCE, [start of procedure callMethodOnNullableObjectBad(),start of procedure mayReturnNullObject,Condition is false,return from a call to T_mayReturnNullObject] +codetoanalyze/cpp/nullable/method.cpp, callMethodOnNullableObjectOk, 2, NULL_TEST_AFTER_DEREFERENCE, [start of procedure callMethodOnNullableObjectOk(),start of procedure mayReturnNullObject,Condition is false,return from a call to T_mayReturnNullObject,Condition is false] diff --git a/infer/tests/codetoanalyze/cpp/nullable/method.cpp b/infer/tests/codetoanalyze/cpp/nullable/method.cpp new file mode 100644 index 000000000..636e28802 --- /dev/null +++ b/infer/tests/codetoanalyze/cpp/nullable/method.cpp @@ -0,0 +1,55 @@ +/* + * 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. + */ +bool star(); + +class T { + + public: + int* _Nullable mayReturnNullPointer() { + if (star()) { + return nullptr; + } else { + return new int; + } + } + + public: + T* _Nullable mayReturnNullObject() { + if (star()) { + return nullptr; + } else { + return this; + } + } + + public: + void doSomething() {} +}; + +void assignNullableValueBad(T* t) { + int* p = t->mayReturnNullPointer(); + *p = 42; +} + +void FP_reAssigningNullableValueOk(T* t) { + int* p = t->mayReturnNullPointer(); + p = new int; + *p = 42; +} + +void callMethodOnNullableObjectBad(T* t) { + t->mayReturnNullObject()->doSomething(); +} + +void callMethodOnNullableObjectOk(T* t) { + T* p = t->mayReturnNullObject(); + if (p != nullptr) { + p->doSomething(); + } +} diff --git a/infer/tests/codetoanalyze/objc/checkers/Makefile b/infer/tests/codetoanalyze/objc/checkers/Makefile index ebe9279c1..a835fec46 100644 --- a/infer/tests/codetoanalyze/objc/checkers/Makefile +++ b/infer/tests/codetoanalyze/objc/checkers/Makefile @@ -9,7 +9,7 @@ TESTS_DIR = ../../.. ANALYZER = checkers CLANG_OPTIONS = -c -INFER_OPTIONS = --biabduction --suggest-nullable --debug-exceptions --project-root $(TESTS_DIR) +INFER_OPTIONS = --biabduction --suggest-nullable --check-nullable --debug-exceptions --project-root $(TESTS_DIR) INFERPRINT_OPTIONS = --issues-tests SOURCES = $(wildcard *.m) diff --git a/infer/tests/codetoanalyze/objc/checkers/Nullable.m b/infer/tests/codetoanalyze/objc/checkers/Nullable.m index 7c7a0da3e..0aa88fd1b 100644 --- a/infer/tests/codetoanalyze/objc/checkers/Nullable.m +++ b/infer/tests/codetoanalyze/objc/checkers/Nullable.m @@ -8,6 +8,8 @@ */ #import +int* __nullable returnsNull(); + @interface T : NSObject - (void)assignUnnanotatedFieldToNullBad; @end @@ -81,4 +83,23 @@ } } +- (void)dereferenceNullableMethodBad { + int* p = returnsNull(); + *p = 42; +} + +- (void)dereferenceNullableMethod1Ok { + int* p = returnsNull(); + if (p) { + *p = 42; + } +} + +- (void)dereferenceNullableMethod2Ok { + int* p = returnsNull(); + if (p != nil) { + *p = 42; + } +} + @end diff --git a/infer/tests/codetoanalyze/objc/checkers/issues.exp b/infer/tests/codetoanalyze/objc/checkers/issues.exp index cab882921..731694438 100644 --- a/infer/tests/codetoanalyze/objc/checkers/issues.exp +++ b/infer/tests/codetoanalyze/objc/checkers/issues.exp @@ -3,6 +3,8 @@ codetoanalyze/objc/checkers/Nullable.m, T_FP_dereferenceNonnullFieldAfterTestFor codetoanalyze/objc/checkers/Nullable.m, T_assignNonnullFieldToNullBad, 1, FIELD_SHOULD_BE_NULLABLE, [Field nonnullField is assigned null here] codetoanalyze/objc/checkers/Nullable.m, T_assignUnnanotatedFieldToNullBad, 1, FIELD_SHOULD_BE_NULLABLE, [Field unnanotatedField is assigned null here] codetoanalyze/objc/checkers/Nullable.m, T_dereferenceNullableFieldBad, 1, NULL_DEREFERENCE, [start of procedure dereferenceNullableFieldBad] +codetoanalyze/objc/checkers/Nullable.m, T_dereferenceNullableMethodBad, 2, NULLABLE_DEREFERENCE, [deference of &p,assignment of the nullable value,definition of returnsNull] +codetoanalyze/objc/checkers/Nullable.m, T_dereferenceNullableMethodBad, 2, NULL_DEREFERENCE, [start of procedure dereferenceNullableMethodBad,Skipping returnsNull(): function or method not found] codetoanalyze/objc/checkers/Nullable.m, T_dereferenceUnnanotatedFieldAfterTestForNullBad, 1, FIELD_SHOULD_BE_NULLABLE, [Field unnanotatedField is compared to null here] codetoanalyze/objc/checkers/Nullable.m, T_dereferenceUnnanotatedFieldAfterTestForNullBad, 2, NULL_DEREFERENCE, [start of procedure dereferenceUnnanotatedFieldAfterTestForNullBad,Condition is true] codetoanalyze/objc/checkers/Nullable.m, T_testNonnullFieldForNullBad, 1, FIELD_SHOULD_BE_NULLABLE, [Field nonnullField is compared to null here]