[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

@@ -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

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

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"

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

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

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

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)

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)

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]

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();
+  }
+}

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)

infer/tests/codetoanalyze/objc/checkers/Nullable.m

@@ -8,6 +8,8 @@
  */
 #import <Foundation/NSString.h>
 
+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

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]