diff --git a/infer/src/IR/Localise.ml b/infer/src/IR/Localise.ml index 2a2afbea1..5bf5aab0c 100644 --- a/infer/src/IR/Localise.ml +++ b/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 diff --git a/infer/src/IR/Localise.mli b/infer/src/IR/Localise.mli index 6e8c4efb3..dc46bc0ae 100644 --- a/infer/src/IR/Localise.mli +++ b/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 diff --git a/infer/src/backend/errdesc.ml b/infer/src/backend/errdesc.ml index 4366fcdfc..9245ba735 100644 --- a/infer/src/backend/errdesc.ml +++ b/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 diff --git a/infer/src/backend/errdesc.mli b/infer/src/backend/errdesc.mli index 14d201e1b..59cbf115e 100644 --- a/infer/src/backend/errdesc.mli +++ b/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 : diff --git a/infer/src/backend/rearrange.ml b/infer/src/backend/rearrange.ml index 9b7e94212..04de8f720 100644 --- a/infer/src/backend/rearrange.ml +++ b/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 diff --git a/infer/src/backend/symExec.ml b/infer/src/backend/symExec.ml index 1940cc958..4b1808c26 100644 --- a/infer/src/backend/symExec.ml +++ b/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 diff --git a/infer/src/backend/tabulation.ml b/infer/src/backend/tabulation.ml index 408b6a1da..9f2b1293e 100644 --- a/infer/src/backend/tabulation.ml +++ b/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 diff --git a/infer/src/base/Config.ml b/infer/src/base/Config.ml index 96e033c38..2c4eded4c 100644 --- a/infer/src/base/Config.ml +++ b/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 diff --git a/infer/src/base/Config.mli b/infer/src/base/Config.mli index 61325b491..3a5a2f7c5 100644 --- a/infer/src/base/Config.mli +++ b/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 diff --git a/infer/src/checkers/NullabilitySuggest.ml b/infer/src/checkers/NullabilitySuggest.ml index 78bad6140..7884198b8 100644 --- a/infer/src/checkers/NullabilitySuggest.ml +++ b/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