[infer] Add an option to specify the name of the nullable annotation

Reviewed By: sblackshear

Differential Revision: D5906614

fbshipit-source-id: 7130018

infer/src/IR/Localise.ml

@@ -514,7 +514,16 @@ type access =
   | Initialized_automatically
   | Returned_from_call of int
 
-let dereference_string deref_str value_str access_opt loc =
+let nullable_annotation_name proc_name =
+  match Config.nullable_annotation with
+  | Some name
+   -> name
+  | None when Typ.Procname.is_java proc_name
+   -> "@Nullable"
+  | None (* default Clang annotation name *)
+   -> "_Nullable"
+
+let dereference_string proc_name deref_str value_str access_opt loc =
   let tags = deref_str.tags in
   Tags.update tags Tags.value value_str ;
   let is_call_access = match access_opt with Some Returned_from_call _ -> true | _ -> false in
@@ -541,16 +550,13 @@ let dereference_string deref_str value_str access_opt loc =
      -> ["initialized automatically"]
   in
   let problem_desc =
-    let nullable_text =
-      MF.monospaced_to_string
-        (if Config.curr_language_is Config.Java then "@Nullable" else "__nullable")
-    in
     let problem_str =
+      let annotation_name = nullable_annotation_name proc_name in
       match (Tags.get !tags Tags.nullable_src, Tags.get !tags Tags.weak_captured_var_src) with
       | Some nullable_src, _
-       -> if String.equal nullable_src value_str then "is annotated with " ^ nullable_text
+       -> if String.equal nullable_src value_str then "is annotated with " ^ annotation_name
             ^ " and is dereferenced without a null check"
-          else "is indirectly marked " ^ nullable_text ^ " (source: "
+          else "is indirectly marked " ^ annotation_name ^ " (source: "
             ^ MF.monospaced_to_string nullable_src ^ ") and is dereferenced without a null check"
       | None, Some weak_var_str
        -> if String.equal weak_var_str value_str then

infer/src/IR/Localise.mli

@@ -134,7 +134,11 @@ type access =
   | Initialized_automatically
   | Returned_from_call of int
 
-val dereference_string : deref_str -> string -> access option -> Location.t -> error_desc
+val nullable_annotation_name : Typ.Procname.t -> string
+(** Name of the nullable annotation *)
+
+val dereference_string :
+  Typ.Procname.t -> deref_str -> string -> access option -> Location.t -> error_desc
 
 val parameter_field_not_null_checked_desc : error_desc -> Exp.t -> error_desc
 

infer/src/backend/errdesc.ml

@@ -874,7 +874,7 @@ let explain_dereference_access outermost_array is_nullable _de_opt prop =
   (value_str, access_opt)
 
 (** Create a description of a dereference operation *)
-let create_dereference_desc tenv ?(use_buckets= false) ?(outermost_array= false)
+let create_dereference_desc proc_name tenv ?(use_buckets= false) ?(outermost_array= false)
     ?(is_nullable= false) ?(is_premature_nil= false) de_opt deref_str prop loc =
   let value_str, access_opt = explain_dereference_access outermost_array is_nullable de_opt prop in
   let access_opt' =
@@ -884,7 +884,7 @@ let create_dereference_desc tenv ?(use_buckets= false) ?(outermost_array= false)
     | _
      -> access_opt
   in
-  let desc = Localise.dereference_string deref_str value_str access_opt' loc in
+  let desc = Localise.dereference_string proc_name deref_str value_str access_opt' loc in
   let desc =
     if Config.curr_language_is Config.Clang && not is_premature_nil then
       match de_opt with
@@ -917,7 +917,7 @@ let create_dereference_desc tenv ?(use_buckets= false) ?(outermost_array= false)
     if outermost_array is true, the outermost array access is removed
     if outermost_dereference is true, stop at the outermost dereference
     (skipping e.g. outermost field access) *)
-let _explain_access tenv ?(use_buckets= false) ?(outermost_array= false)
+let _explain_access proc_name tenv ?(use_buckets= false) ?(outermost_array= false)
     ?(outermost_dereference= false) ?(is_nullable= false) ?(is_premature_nil= false) deref_str prop
     loc =
   let rec find_outermost_dereference node e =
@@ -981,15 +981,15 @@ let _explain_access tenv ?(use_buckets= false) ?(outermost_array= false)
         if outermost_dereference then find_outermost_dereference node e
         else exp_lv_dexp tenv node e
       in
-      create_dereference_desc tenv ~use_buckets ~outermost_array ~is_nullable ~is_premature_nil
-        de_opt deref_str prop loc
+      create_dereference_desc proc_name tenv ~use_buckets ~outermost_array ~is_nullable
+        ~is_premature_nil de_opt deref_str prop loc
 
 (** Produce a description of which expression is dereferenced in the current instruction, if any.
     The subexpression to focus on is obtained by removing field and index accesses. *)
-let explain_dereference tenv ?(use_buckets= false) ?(is_nullable= false) ?(is_premature_nil= false)
-    deref_str prop loc =
-  _explain_access tenv ~use_buckets ~outermost_array:false ~outermost_dereference:true ~is_nullable
-    ~is_premature_nil deref_str prop loc
+let explain_dereference proc_name tenv ?(use_buckets= false) ?(is_nullable= false)
+    ?(is_premature_nil= false) deref_str prop loc =
+  _explain_access proc_name tenv ~use_buckets ~outermost_array:false ~outermost_dereference:true
+    ~is_nullable ~is_premature_nil deref_str prop loc
 
 (** Produce a description of the array access performed in the current instruction, if any.
     The subexpression to focus on is obtained by removing the outermost array access. *)
@@ -1020,7 +1020,7 @@ let dexp_apply_pvar_off dexp pvar_off =
 
 (** Produce a description of the nth parameter of the function call, if the current instruction
     is a function call with that parameter *)
-let explain_nth_function_parameter tenv use_buckets deref_str prop n pvar_off =
+let explain_nth_function_parameter proc_name tenv use_buckets deref_str prop n pvar_off =
   let node = State.get_node () in
   let loc = State.get_loc () in
   match State.get_instr () with
@@ -1031,7 +1031,7 @@ let explain_nth_function_parameter tenv use_buckets deref_str prop n pvar_off =
       let dexp_opt' =
         match dexp_opt with Some de -> Some (dexp_apply_pvar_off de pvar_off) | None -> None
       in
-      create_dereference_desc tenv ~use_buckets dexp_opt' deref_str prop loc
+      create_dereference_desc proc_name tenv ~use_buckets dexp_opt' deref_str prop loc
     with exn when SymOp.exn_not_failure exn -> Localise.no_desc )
   | _
    -> Localise.no_desc
@@ -1071,8 +1071,8 @@ let find_with_exp prop exp =
 
 (** return a description explaining value [exp] in [prop] in terms of a source expression
     using the formal parameters of the call *)
-let explain_dereference_as_caller_expression tenv ?(use_buckets= false) deref_str actual_pre
-    spec_pre exp node loc formal_params =
+let explain_dereference_as_caller_expression proc_name tenv ?(use_buckets= false) deref_str
+    actual_pre spec_pre exp node loc formal_params =
   let find_formal_param_number name =
     let rec find n = function
       | []
@@ -1088,11 +1088,12 @@ let explain_dereference_as_caller_expression tenv ?(use_buckets= false) deref_st
       let pv_name = Pvar.get_name pv in
       if Pvar.is_global pv then
         let dexp = exp_lv_dexp tenv node (Exp.Lvar pv) in
-        create_dereference_desc tenv ~use_buckets dexp deref_str actual_pre loc
+        create_dereference_desc proc_name tenv ~use_buckets dexp deref_str actual_pre loc
       else if Pvar.is_callee pv then
         let position = find_formal_param_number pv_name in
         if verbose then L.d_strln ("parameter number: " ^ string_of_int position) ;
-        explain_nth_function_parameter tenv use_buckets deref_str actual_pre position pvar_off
+        explain_nth_function_parameter proc_name tenv use_buckets deref_str actual_pre position
+          pvar_off
       else if Attribute.has_dangling_uninit tenv spec_pre exp then
         Localise.desc_uninitialized_dangling_pointer_deref deref_str (Pvar.to_string pv) loc
       else Localise.no_desc

infer/src/backend/errdesc.mli

@@ -50,7 +50,7 @@ val explain_allocation_mismatch : PredSymb.res_action -> PredSymb.res_action ->
 (** Produce a description of a mismatch between an allocation function and a deallocation function *)
 
 val explain_array_access :
-  Tenv.t -> Localise.deref_str -> 'a Prop.t -> Location.t -> Localise.error_desc
+  Typ.Procname.t -> Tenv.t -> Localise.deref_str -> 'a Prop.t -> Location.t -> Localise.error_desc
 (** Produce a description of the array access performed in the current instruction, if any. *)
 
 val explain_class_cast_exception :
@@ -65,13 +65,13 @@ val explain_deallocate_constant_string : string -> PredSymb.res_action -> Locali
 (** Explain a deallocate constant string error *)
 
 val explain_dereference :
-  Tenv.t -> ?use_buckets:bool -> ?is_nullable:bool -> ?is_premature_nil:bool -> Localise.deref_str
-  -> 'a Prop.t -> Location.t -> Localise.error_desc
+  Typ.Procname.t -> Tenv.t -> ?use_buckets:bool -> ?is_nullable:bool -> ?is_premature_nil:bool
+  -> Localise.deref_str -> 'a Prop.t -> Location.t -> Localise.error_desc
 (** Produce a description of which expression is dereferenced in the current instruction, if any. *)
 
 val explain_dereference_as_caller_expression :
-  Tenv.t -> ?use_buckets:bool -> Localise.deref_str -> 'a Prop.t -> 'b Prop.t -> Exp.t
-  -> Procdesc.Node.t -> Location.t -> Pvar.t list -> Localise.error_desc
+  Typ.Procname.t -> Tenv.t -> ?use_buckets:bool -> Localise.deref_str -> 'a Prop.t -> 'b Prop.t
+  -> Exp.t -> Procdesc.Node.t -> Location.t -> Pvar.t list -> Localise.error_desc
 (** return a description explaining value [exp] in [prop] in terms of a source expression
     using the formal parameters of the call *)
 
@@ -119,7 +119,7 @@ val explain_leak :
     If there is an alloc attribute, print the function call and line number. *)
 
 val explain_memory_access :
-  Tenv.t -> Localise.deref_str -> 'a Prop.t -> Location.t -> Localise.error_desc
+  Typ.Procname.t -> Tenv.t -> Localise.deref_str -> 'a Prop.t -> Location.t -> Localise.error_desc
 (** Produce a description of the memory access performed in the current instruction, if any. *)
 
 val explain_null_test_after_dereference :

infer/src/backend/rearrange.ml

@@ -58,12 +58,12 @@ let check_bad_index tenv pname p len index loc =
       let deref_str = Localise.deref_str_array_bound len_const_opt index_const_opt in
       let exn =
         Exceptions.Array_out_of_bounds_l1
-          (Errdesc.explain_array_access tenv deref_str p loc, __POS__)
+          (Errdesc.explain_array_access pname tenv deref_str p loc, __POS__)
       in
       Reporting.log_warning_deprecated pname exn
     else if len_is_constant then
       let deref_str = Localise.deref_str_array_bound len_const_opt index_const_opt in
-      let desc = Errdesc.explain_array_access tenv deref_str p loc in
+      let desc = Errdesc.explain_array_access pname tenv deref_str p loc in
       let exn =
         if index_has_bounds () then Exceptions.Array_out_of_bounds_l2 (desc, __POS__)
         else Exceptions.Array_out_of_bounds_l3 (desc, __POS__)
@@ -453,7 +453,9 @@ let mk_ptsto_exp_footprint pname tenv orig_prop (lexp, typ) max_stamp inst
     then (
       L.internal_error "!!!! Footprint Error, Bad Root : %a !!!! @\n" Exp.pp lexp ;
       let deref_str = Localise.deref_str_dangling None in
-      let err_desc = Errdesc.explain_dereference tenv deref_str orig_prop (State.get_loc ()) in
+      let err_desc =
+        Errdesc.explain_dereference pname tenv deref_str orig_prop (State.get_loc ())
+      in
       raise (Exceptions.Dangling_pointer_dereference (None, err_desc, __POS__)) ) ;
   let off_foot, eqs = laundry_offset_for_footprint max_stamp off in
   let subtype =
@@ -1305,7 +1307,7 @@ let check_type_size tenv pname prop texp off typ_from_instr =
         let loc = State.get_loc () in
         let exn =
           Exceptions.Pointer_size_mismatch
-            (Errdesc.explain_dereference tenv deref_str prop loc, __POS__)
+            (Errdesc.explain_dereference pname tenv deref_str prop loc, __POS__)
         in
         Reporting.log_warning_deprecated pname exn
   | None
@@ -1527,6 +1529,7 @@ let is_only_pt_by_fld_or_param_nonnull pdesc tenv prop deref_exp =
 
 (** Check for dereference errors: dereferencing 0, a freed value, or an undefined value *)
 let check_dereference_error tenv pdesc (prop: Prop.normal Prop.t) lexp loc =
+  let pname = Procdesc.get_proc_name pdesc in
   let root = Exp.root_of_lexp lexp in
   let nullable_var_opt = is_only_pt_by_fld_or_param_nullable pdesc tenv prop root in
   let is_deref_of_nullable =
@@ -1572,7 +1575,7 @@ let check_dereference_error tenv pdesc (prop: Prop.normal Prop.t) lexp loc =
         else Localise.deref_str_null None
       in
       let err_desc =
-        Errdesc.explain_dereference tenv ~use_buckets:true ~is_nullable:is_deref_of_nullable
+        Errdesc.explain_dereference pname tenv ~use_buckets:true ~is_nullable:is_deref_of_nullable
           deref_str prop loc
       in
       if Localise.is_parameter_not_null_checked_desc err_desc then
@@ -1587,23 +1590,24 @@ let check_dereference_error tenv pdesc (prop: Prop.normal Prop.t) lexp loc =
   match attribute_opt with
   | Some Apred (Adangling dk, _)
    -> let deref_str = Localise.deref_str_dangling (Some dk) in
-      let err_desc = Errdesc.explain_dereference tenv deref_str prop (State.get_loc ()) in
+      let err_desc = Errdesc.explain_dereference pname tenv deref_str prop (State.get_loc ()) in
       raise (Exceptions.Dangling_pointer_dereference (Some dk, err_desc, __POS__))
   | Some Apred (Aundef _, _)
    -> ()
   | Some Apred (Aresource ({ra_kind= Rrelease} as ra), _)
    -> let deref_str = Localise.deref_str_freed ra in
-      let err_desc = Errdesc.explain_dereference tenv ~use_buckets:true deref_str prop loc in
+      let err_desc = Errdesc.explain_dereference pname tenv ~use_buckets:true deref_str prop loc in
       raise (Exceptions.Use_after_free (err_desc, __POS__))
   | _
    -> if Prover.check_equal tenv Prop.prop_emp (Exp.root_of_lexp root) Exp.minus_one then
         let deref_str = Localise.deref_str_dangling None in
-        let err_desc = Errdesc.explain_dereference tenv deref_str prop loc in
+        let err_desc = Errdesc.explain_dereference pname tenv deref_str prop loc in
         raise (Exceptions.Dangling_pointer_dereference (None, err_desc, __POS__))
 
 (* Check that an expression representin an objc block can be null and raise a [B1] null exception.*)
 (* It's used to check that we don't call possibly null blocks *)
 let check_call_to_objc_block_error tenv pdesc prop fun_exp loc =
+  let pname = Procdesc.get_proc_name pdesc in
   let is_this = function
     | Exp.Lvar pvar
      -> let {ProcAttributes.is_objc_instance_method; is_cpp_instance_method} =
@@ -1664,7 +1668,7 @@ let check_call_to_objc_block_error tenv pdesc prop fun_exp loc =
   then
     let deref_str = Localise.deref_str_null None in
     let err_desc_nobuckets =
-      Errdesc.explain_dereference tenv ~is_nullable:true deref_str prop loc
+      Errdesc.explain_dereference pname tenv ~is_nullable:true deref_str prop loc
     in
     match fun_exp with
     | Exp.Var id when Ident.is_footprint id

infer/src/backend/symExec.ml

@@ -135,7 +135,9 @@ let rec apply_offlist pdesc tenv p fp_root nullify_struct (root_lexp, strexp, ty
               else Attribute.get_undef tenv p root_lexp
             in
             let deref_str = Localise.deref_str_uninitialized alloc_attribute_opt in
-            let err_desc = Errdesc.explain_memory_access tenv deref_str p (State.get_loc ()) in
+            let err_desc =
+              Errdesc.explain_memory_access pname tenv deref_str p (State.get_loc ())
+            in
             let exn = Exceptions.Uninitialized_value (err_desc, __POS__) in
             Reporting.log_warning_deprecated pname exn ; Sil.update_inst inst_curr inst
         | Sil.Ilookup
@@ -1607,8 +1609,8 @@ and check_variadic_sentinel ?(fails_on_nil= false) n_formals (sentinel, null_pos
       reraise_if e ~f:(fun () -> fails_on_nil) ;
       let deref_str = Localise.deref_str_nil_argument_in_variadic_method proc_name nargs i in
       let err_desc =
-        Errdesc.explain_dereference tenv ~use_buckets:true ~is_premature_nil:true deref_str prop_
-          loc
+        Errdesc.explain_dereference proc_name tenv ~use_buckets:true ~is_premature_nil:true
+          deref_str prop_ loc
       in
       raise (Exceptions.Premature_nil_termination (err_desc, __POS__))
   in

infer/src/backend/tabulation.ml

@@ -282,13 +282,13 @@ and find_dereference_without_null_check_in_sexp_list = function
 
 (** Check dereferences implicit in the spec pre.
     In case of dereference error, return [Some(deref_error, description)], otherwise [None] *)
-let check_dereferences tenv callee_pname actual_pre sub spec_pre formal_params =
+let check_dereferences caller_pname tenv callee_pname actual_pre sub spec_pre formal_params =
   let check_dereference e sexp =
     let e_sub = Sil.exp_sub sub e in
     let desc use_buckets deref_str =
       let error_desc =
-        Errdesc.explain_dereference_as_caller_expression tenv ~use_buckets deref_str actual_pre
-          spec_pre e (State.get_node ()) (State.get_loc ()) formal_params
+        Errdesc.explain_dereference_as_caller_expression caller_pname tenv ~use_buckets deref_str
+          actual_pre spec_pre e (State.get_node ()) (State.get_loc ()) formal_params
       in
       L.d_strln_color Red "found error in dereference" ;
       L.d_strln "spec_pre:" ;
@@ -980,10 +980,11 @@ let get_check_exn tenv check callee_pname loc ml_loc =
   | Prover.Class_cast_check (texp1, texp2, exp)
    -> class_cast_exn tenv (Some callee_pname) texp1 texp2 exp ml_loc
 
-let check_uninitialize_dangling_deref tenv callee_pname actual_pre sub formal_params props =
+let check_uninitialize_dangling_deref caller_pname tenv callee_pname actual_pre sub formal_params
+    props =
   List.iter
     ~f:(fun (p, _) ->
-      match check_dereferences tenv callee_pname actual_pre sub p formal_params with
+      match check_dereferences caller_pname tenv callee_pname actual_pre sub p formal_params with
       | Some (Deref_undef_exp, desc)
        -> raise (Exceptions.Dangling_pointer_dereference (Some PredSymb.DAuninit, desc, __POS__))
       | _
@@ -1041,8 +1042,8 @@ let exe_spec tenv ret_id_opt (n, nspecs) caller_pdesc callee_pname loc prop path
         | Some results
          -> (* After combining we check that we have not added
                a points-to of initialized variables.*)
-            check_uninitialize_dangling_deref tenv callee_pname actual_pre split.sub formal_params
-              results ;
+            check_uninitialize_dangling_deref caller_pname tenv callee_pname actual_pre split.sub
+              formal_params results ;
             let inconsistent_results, consistent_results =
               List.partition_tf ~f:(fun (p, _) -> Prover.check_inconsistency tenv p) results
             in
@@ -1056,7 +1057,10 @@ let exe_spec tenv ret_id_opt (n, nspecs) caller_pdesc callee_pname loc prop path
       in
       List.iter ~f:log_check_exn checks ;
       let subbed_pre = Prop.prop_sub (`Exp sub1) actual_pre in
-      match check_dereferences tenv callee_pname subbed_pre (`Exp sub2) spec_pre formal_params with
+      match
+        check_dereferences caller_pname tenv callee_pname subbed_pre (`Exp sub2) spec_pre
+          formal_params
+      with
       | Some (Deref_undef _, _)
        -> let split = do_split () in
           report_valid_res split

infer/src/base/Config.ml

@@ -1308,6 +1308,9 @@ and monitor_prop_size =
 
 and nelseg = CLOpt.mk_bool ~deprecated:["nelseg"] ~long:"nelseg" "Use only nonempty lsegs"
 
+and nullable_annotation =
+  CLOpt.mk_string_opt ~long:"nullable-annotation-name" "Specify custom nullable annotation name"
+
 (* TODO: document *)
 and objc_memory_model =
   CLOpt.mk_bool ~deprecated:["objcm"] ~long:"objc-memory-model" "Use ObjC memory model"
@@ -2151,6 +2154,8 @@ and monitor_prop_size = !monitor_prop_size
 
 and nelseg = !nelseg
 
+and nullable_annotation = !nullable_annotation
+
 and suggest_nullable = !suggest_nullable
 
 and no_translate_libs = not !headers

infer/src/base/Config.mli

@@ -516,6 +516,8 @@ val nelseg : bool
 
 val no_translate_libs : bool
 
+val nullable_annotation : string option
+
 val objc_memory_model_on : bool
 
 val only_cheap_debug : bool

infer/src/checkers/NullabilitySuggest.ml

@@ -145,9 +145,7 @@ let pretty_field_name proc_data field_name =
       Typ.Fieldname.to_string field_name
 
 let checker {Callbacks.summary; proc_desc; tenv} =
-  let nullable_annotation =
-    if Typ.Procname.is_java (Procdesc.get_proc_name proc_desc) then "@Nullable" else "_Nullable"
-  in
+  let annotation = Localise.nullable_annotation_name (Procdesc.get_proc_name proc_desc) in
   let report astate (proc_data: extras ProcData.t) =
     let report_access_path ap udchain =
       let issue_kind = IssueType.field_should_be_nullable.unique_id in
@@ -159,7 +157,7 @@ let checker {Callbacks.summary; proc_desc; tenv} =
        -> (
           let message =
             F.asprintf "Field %a should be annotated with %a" MF.pp_monospaced
-              (pretty_field_name proc_data field_name) MF.pp_monospaced nullable_annotation
+              (pretty_field_name proc_data field_name) MF.pp_monospaced annotation
           in
           let exn = Exceptions.Checkers (issue_kind, Localise.verbatim_desc message) in
           match make_error_trace astate ap udchain with