pghs975uc
/
infer_clone
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

[backend] Reorganize the resolution of procedure attributes, fixing a bug where annotations of overridden procedures via spec files were not found.

Browse Source
master
Cristiano Calcagno 9 years ago
parent a277858924
commit 76c8b6e58b
17 changed files with 268 additions and 190 deletions
Show Stats Download Patch File Download Diff File

8
infer/src/backend/callbacks.ml
Unescape View File

@ -221,11 +221,9 @@ let iterate_callbacks store_summary call_graph exe_env =
| Some cfg -> | Some cfg ->
Cfg.Procdesc.find_from_name cfg proc_name Cfg.Procdesc.find_from_name cfg proc_name
| None -> None in | None -> None in
let loc = match procdesc_opt with let attributes_opt =
| Some proc_desc -> Option.map Cfg.Procdesc.get_attributes procdesc_opt in
Cfg.Procdesc.get_loc proc_desc Specs.reset_summary call_graph proc_name attributes_opt in
| None -> Location.dummy in
Specs.reset_summary call_graph proc_name loc in
(* Make sure summaries exists. *) (* Make sure summaries exists. *)

2
infer/src/backend/inferanalyze.ml
Unescape View File

@ -207,7 +207,7 @@ let () = (* parse command-line arguments *)
module Simulator = struct (** Simulate the analysis only *) module Simulator = struct (** Simulate the analysis only *)
let reset_summaries cg = let reset_summaries cg =
list_iter list_iter
(fun (pname, in_out_calls) -> Specs.reset_summary cg pname Location.dummy) (fun (pname, in_out_calls) -> Specs.reset_summary cg pname None)
(Cg.get_nodes_and_calls cg) (Cg.get_nodes_and_calls cg)
(** Perform phase transition from [FOOTPRINT] to [RE_EXECUTION] for (** Perform phase transition from [FOOTPRINT] to [RE_EXECUTION] for

5
infer/src/backend/interproc.ml
Unescape View File

@ -1048,9 +1048,8 @@ let report_runtime_exceptions tenv cfg pdesc summary =
&& Procname.java_is_static pname && Procname.java_is_static pname
&& (Procname.java_get_method pname) = "main" in && (Procname.java_get_method pname) = "main" in
let is_annotated = let is_annotated =
let annotated_signature = let proc_attributes = Specs.pdesc_resolve_attributes pdesc in
Annotations.get_annotated_signature let annotated_signature = Annotations.get_annotated_signature proc_attributes in
Specs.proc_get_method_annotation pdesc pname in
let ret_annotation, _ = annotated_signature.Annotations.ret in let ret_annotation, _ = annotated_signature.Annotations.ret in
Annotations.ia_is_verify ret_annotation in Annotations.ia_is_verify ret_annotation in
let is_unavoidable pre = let is_unavoidable pre =

2
infer/src/backend/rearrange.ml
Unescape View File

@ -935,7 +935,7 @@ let check_dereference_error pdesc (prop : Prop.normal Prop.t) lexp loc =
let nullable_obj_str = ref None in let nullable_obj_str = ref None in
(* return true if deref_exp is only pointed to by fields/params with @Nullable annotations *) (* return true if deref_exp is only pointed to by fields/params with @Nullable annotations *)
let is_only_pt_by_nullable_fld_or_param deref_exp = let is_only_pt_by_nullable_fld_or_param deref_exp =
let ann_sig = Models.get_annotated_signature pdesc (Cfg.Procdesc.get_proc_name pdesc) in let ann_sig = Models.get_modelled_annotated_signature (Specs.pdesc_resolve_attributes pdesc) in
list_for_all list_for_all
(fun hpred -> (fun hpred ->
match hpred with match hpred with

72
infer/src/backend/specs.ml
Unescape View File

@ -617,28 +617,55 @@ let get_summary_unsafe proc_name =
| Some summary -> summary | Some summary -> summary
(** Check if the procedure is from a library: (** Check if the procedure is from a library:
It's not defined in the current proc desc, and there is no spec file for it. *) It's not defined, and there is no spec file for it. *)
let proc_is_library proc_name proc_desc = let proc_is_library proc_attributes =
let defined = Cfg.Procdesc.is_defined proc_desc in if not proc_attributes.ProcAttributes.is_defined then
if not defined then match get_summary proc_attributes.ProcAttributes.proc_name with
match get_summary proc_name with
| None -> true | None -> true
| Some _ -> false | Some _ -> false
else false else false
(** Get the attributes of a procedure, looking first in the procdesc and then in the .specs file. *) (** Try to find the attributes for a defined proc, by first looking at the procdesc
let proc_get_attributes proc_name proc_desc : ProcAttributes.t = then looking at .specs files if required.
let from_proc_desc = Cfg.Procdesc.get_attributes proc_desc in Return the attributes for an underfined procedure otherwise.
let defined = Cfg.Procdesc.is_defined proc_desc in If no attributes can be found, return None.
if not defined then *)
match get_summary proc_name with let proc_resolve_attributes get_proc_desc proc_name =
| None -> from_proc_desc let from_proc_desc () = match get_proc_desc proc_name with
| Some proc_desc ->
Some (Cfg.Procdesc.get_attributes proc_desc)
| None ->
None in
let from_specs () = match get_summary proc_name with
| Some summary -> | Some summary ->
summary.attributes (* get attributes from .specs file *) Some summary.attributes
else from_proc_desc | None -> None in
match from_proc_desc () with
let proc_get_method_annotation proc_name proc_desc = | Some attributes ->
(proc_get_attributes proc_name proc_desc).ProcAttributes.method_annotation if attributes.ProcAttributes.is_defined
then Some attributes
else begin
match from_specs () with
| Some attributes' ->
Some attributes'
| None -> Some attributes
end
| None ->
from_specs ()
(** Like proc_resolve_attributes but start from a proc_desc. *)
let pdesc_resolve_attributes proc_desc =
let proc_name = Cfg.Procdesc.get_proc_name proc_desc in
let get_proc_desc proc_name' =
if Procname.equal proc_name proc_name'
then Some proc_desc
else None in
match proc_resolve_attributes get_proc_desc proc_name with
| Some proc_attributes ->
proc_attributes
| None ->
(* this should not happen *)
assert false
let get_origin proc_name = let get_origin proc_name =
match get_summary_origin proc_name with match get_summary_origin proc_name with
@ -770,11 +797,14 @@ let init_summary
} in } in
Procname.Hash.replace spec_tbl proc_attributes.ProcAttributes.proc_name (summary, Res_dir) Procname.Hash.replace spec_tbl proc_attributes.ProcAttributes.proc_name (summary, Res_dir)
let reset_summary call_graph proc_name loc = (** Reset a summary rebuilding the dependents and preserving the proc attributes if present. *)
let reset_summary call_graph proc_name attributes_opt =
let dependents = Cg.get_defined_children call_graph proc_name in let dependents = Cg.get_defined_children call_graph proc_name in
let proc_attributes = let proc_attributes = match attributes_opt with
{ (ProcAttributes.default proc_name !Config.curr_language) with | Some attributes ->
loc; } in attributes
| None ->
ProcAttributes.default proc_name !Config.curr_language in
init_summary ( init_summary (
Procname.Set.elements dependents, Procname.Set.elements dependents,
[], [],

19
infer/src/backend/specs.mli
Unescape View File

@ -222,7 +222,8 @@ val init_summary :
ProcAttributes.t) (** attributes of the procedure *) ProcAttributes.t) (** attributes of the procedure *)
-> unit -> unit
val reset_summary : Cg.t -> Procname.t -> Location.t -> unit (** Reset a summary rebuilding the dependents and preserving the proc attributes if present. *)
val reset_summary : Cg.t -> Procname.t -> ProcAttributes.t option -> unit
(** Load procedure summary from the given file *) (** Load procedure summary from the given file *)
val load_summary : DB.filename -> summary option val load_summary : DB.filename -> summary option
@ -245,14 +246,20 @@ val pp_specs : printenv -> Format.formatter -> Prop.normal spec list -> unit
(** Print the summary, the bool indicates whether to print whole seconds only *) (** Print the summary, the bool indicates whether to print whole seconds only *)
val pp_summary : printenv -> bool -> Format.formatter -> summary -> unit val pp_summary : printenv -> bool -> Format.formatter -> summary -> unit
(** Get the attributes of a procedure, looking first in the procdesc and then in the .specs file. *) (** Like proc_resolve_attributes but start from a proc_desc. *)
val proc_get_attributes : Procname.t -> Cfg.Procdesc.t -> ProcAttributes.t val pdesc_resolve_attributes : Cfg.Procdesc.t -> ProcAttributes.t
val proc_get_method_annotation : Procname.t -> Cfg.Procdesc.t -> Sil.method_annotation (** Try to find the attributes for a defined proc, by first looking at the procdesc
then looking at .specs files if required.
Return the attributes for an underfined procedure otherwise.
If no attributes can be found, return None.
*)
val proc_resolve_attributes :
(Procname.t -> Cfg.Procdesc.t option) -> Procname.t -> ProcAttributes.t option
(** Check if the procedure is from a library: (** Check if the procedure is from a library:
It's not defined in the current proc desc, and there is no spec file for it. *) It's not defined, and there is no spec file for it. *)
val proc_is_library : Procname.t -> Cfg.Procdesc.t -> bool val proc_is_library : ProcAttributes.t -> bool
(** Re-initialize a dependency map *) (** Re-initialize a dependency map *)
val re_initialize_dependency_map : dependency_map_t -> dependency_map_t val re_initialize_dependency_map : dependency_map_t -> dependency_map_t

137
infer/src/backend/symExec.ml
Unescape View File

@ -561,8 +561,7 @@ let check_constant_string_dereference lexp =
| _ -> None | _ -> None
(** Normalize an expression and check for arithmetic problems *) (** Normalize an expression and check for arithmetic problems *)
let exp_norm_check_arith pdesc prop exp = let exp_norm_check_arith pname prop exp =
let pname = Cfg.Procdesc.get_proc_name pdesc in
match Prop.find_arithmetic_problem (State.get_path_pos ()) prop exp with match Prop.find_arithmetic_problem (State.get_path_pos ()) prop exp with
| Some (Prop.Div0 div), prop' -> | Some (Prop.Div0 div), prop' ->
let desc = Errdesc.explain_divide_by_zero div (State.get_node ()) (State.get_loc ()) in let desc = Errdesc.explain_divide_by_zero div (State.get_node ()) (State.get_loc ()) in
@ -761,9 +760,11 @@ let redirect_shared_ptr tenv cfg pname actual_params =
pname' pname'
else pname else pname
(** recognize calls to the constructor java.net.URL and splits the argument string to be only the protocol. *) (** recognize calls to the constructor java.net.URL and splits the argument string
let call_constructor_url_update_args tenv cfg pname actual_params = to be only the protocol. *)
let url_pname = Procname.mangled_java ((Some "java.net"), "URL") None "<init>" [(Some "java.lang"), "String"] Procname.Non_Static in let call_constructor_url_update_args pname actual_params =
let url_pname = Procname.mangled_java
((Some "java.net"), "URL") None "<init>" [(Some "java.lang"), "String"] Procname.Non_Static in
if (Procname.equal url_pname pname) then if (Procname.equal url_pname pname) then
(match actual_params with (match actual_params with
| [this; (Sil.Const (Sil.Cstr s), atype)] -> | [this; (Sil.Const (Sil.Cstr s), atype)] ->
@ -781,7 +782,7 @@ let call_constructor_url_update_args tenv cfg pname actual_params =
(** Handles certain method calls in a special way *) (** Handles certain method calls in a special way *)
let handle_special_cases_call tenv cfg pname actual_params = let handle_special_cases_call tenv cfg pname actual_params =
if (!Config.curr_language = Config.Java) then if (!Config.curr_language = Config.Java) then
pname, (call_constructor_url_update_args tenv cfg pname actual_params) pname, (call_constructor_url_update_args pname actual_params)
else if (!Config.curr_language = Config.C_CPP) then else if (!Config.curr_language = Config.C_CPP) then
(redirect_shared_ptr tenv cfg pname actual_params), actual_params (redirect_shared_ptr tenv cfg pname actual_params), actual_params
else pname, actual_params else pname, actual_params
@ -876,7 +877,7 @@ let rec sym_exec cfg tenv pdesc _instr (_prop: Prop.normal Prop.t) path
| Sil.Letderef (id, rhs_exp, typ, loc) -> | Sil.Letderef (id, rhs_exp, typ, loc) ->
begin begin
try try
let n_rhs_exp, prop = exp_norm_check_arith pdesc _prop rhs_exp in let n_rhs_exp, prop = exp_norm_check_arith pname _prop rhs_exp in
let n_rhs_exp' = Prop.exp_collapse_consecutive_indices_prop prop typ n_rhs_exp in let n_rhs_exp' = Prop.exp_collapse_consecutive_indices_prop prop typ n_rhs_exp in
match check_constant_string_dereference n_rhs_exp' with match check_constant_string_dereference n_rhs_exp' with
| Some value -> | Some value ->
@ -896,8 +897,8 @@ let rec sym_exec cfg tenv pdesc _instr (_prop: Prop.normal Prop.t) path
| Sil.Set (lhs_exp, typ, rhs_exp, loc) -> | Sil.Set (lhs_exp, typ, rhs_exp, loc) ->
begin begin
try try
let n_lhs_exp, _prop' = exp_norm_check_arith pdesc _prop lhs_exp in let n_lhs_exp, _prop' = exp_norm_check_arith pname _prop lhs_exp in
let n_rhs_exp, prop = exp_norm_check_arith pdesc _prop' rhs_exp in let n_rhs_exp, prop = exp_norm_check_arith pname _prop' rhs_exp in
let prop = Prop.replace_objc_null prop n_lhs_exp n_rhs_exp in let prop = Prop.replace_objc_null prop n_lhs_exp n_rhs_exp in
let n_lhs_exp' = Prop.exp_collapse_consecutive_indices_prop prop typ n_lhs_exp in let n_lhs_exp' = Prop.exp_collapse_consecutive_indices_prop prop typ n_lhs_exp in
let iter_list = Rearrange.rearrange pdesc tenv n_lhs_exp' typ prop loc in let iter_list = Rearrange.rearrange pdesc tenv n_lhs_exp' typ prop loc in
@ -927,14 +928,15 @@ let rec sym_exec cfg tenv pdesc _instr (_prop: Prop.normal Prop.t) path
| _ -> () in | _ -> () in
check_already_dereferenced pname cond _prop; check_already_dereferenced pname cond _prop;
check_condition_always_true_false (); check_condition_always_true_false ();
let n_cond, prop = exp_norm_check_arith pdesc _prop cond in let n_cond, prop = exp_norm_check_arith pname _prop cond in
ret_old_path (Propset.to_proplist (prune_prop tenv n_cond prop)) ret_old_path (Propset.to_proplist (prune_prop tenv n_cond prop))
| Sil.Call (ret_ids, Sil.Const (Sil.Cfun fn), args, loc, call_flags) when function_is_builtin fn -> | Sil.Call (ret_ids, Sil.Const (Sil.Cfun callee_pname), args, loc, call_flags)
let sym_exe_builtin = Builtin.get_sym_exe_builtin fn in when function_is_builtin callee_pname ->
sym_exe_builtin cfg pdesc instr tenv _prop path ret_ids args fn loc let sym_exe_builtin = Builtin.get_sym_exe_builtin callee_pname in
sym_exe_builtin cfg pdesc instr tenv _prop path ret_ids args callee_pname loc
| Sil.Call (ret_ids, Sil.Const (Sil.Cfun callee_pname), actual_params, loc, call_flags) -> | Sil.Call (ret_ids, Sil.Const (Sil.Cfun callee_pname), actual_params, loc, call_flags) ->
(** Generic fun call with known name *) (** Generic fun call with known name *)
let (prop_r, _n_actual_params) = normalize_params pdesc _prop actual_params in let (prop_r, _n_actual_params) = normalize_params pname _prop actual_params in
let fn, n_actual_params = handle_special_cases_call tenv cfg callee_pname _n_actual_params in let fn, n_actual_params = handle_special_cases_call tenv cfg callee_pname _n_actual_params in
let resolved_pname = let resolved_pname =
if call_flags.Sil.cf_virtual then if call_flags.Sil.cf_virtual then
@ -961,7 +963,8 @@ let rec sym_exec cfg tenv pdesc _instr (_prop: Prop.normal Prop.t) path
ret_ids ret_typ_opt n_actual_params resolved_pname loc in ret_ids ret_typ_opt n_actual_params resolved_pname loc in
let sentinel_result = let sentinel_result =
if !Config.curr_language = Config.C_CPP then if !Config.curr_language = Config.C_CPP then
sym_exe_check_variadic_sentinel_if_present cfg pdesc tenv prop_r path actual_params callee_pname loc sym_exe_check_variadic_sentinel_if_present
cfg pdesc tenv prop_r path actual_params callee_pname loc
else [(prop_r, path)] in else [(prop_r, path)] in
let do_call (prop, path) = let do_call (prop, path) =
match Specs.get_summary resolved_pname with match Specs.get_summary resolved_pname with
@ -973,7 +976,7 @@ let rec sym_exec cfg tenv pdesc _instr (_prop: Prop.normal Prop.t) path
cfg pdesc tenv prop path ret_ids n_actual_params summary loc in cfg pdesc tenv prop path ret_ids n_actual_params summary loc in
list_flatten (list_map do_call sentinel_result) list_flatten (list_map do_call sentinel_result)
| Sil.Call (ret_ids, fun_exp, actual_params, loc, call_flags) -> (** Call via function pointer *) | Sil.Call (ret_ids, fun_exp, actual_params, loc, call_flags) -> (** Call via function pointer *)
let (prop_r, n_actual_params) = normalize_params pdesc _prop actual_params in let (prop_r, n_actual_params) = normalize_params pname _prop actual_params in
if call_flags.Sil.cf_is_objc_block then if call_flags.Sil.cf_is_objc_block then
Rearrange.check_call_to_objc_block_error pdesc prop_r fun_exp loc; Rearrange.check_call_to_objc_block_error pdesc prop_r fun_exp loc;
Rearrange.check_dereference_error pdesc prop_r fun_exp loc; Rearrange.check_dereference_error pdesc prop_r fun_exp loc;
@ -1032,7 +1035,7 @@ let rec sym_exec cfg tenv pdesc _instr (_prop: Prop.normal Prop.t) path
| Sil.Stackop _ -> (* this should be handled at the propset level *) | Sil.Stackop _ -> (* this should be handled at the propset level *)
assert false assert false
| Sil.Goto_node (node_e, loc) -> | Sil.Goto_node (node_e, loc) ->
let n_node_e, prop = exp_norm_check_arith pdesc _prop node_e in let n_node_e, prop = exp_norm_check_arith pname _prop node_e in
begin begin
match n_node_e with match n_node_e with
| Sil.Const (Sil.Cint i) -> | Sil.Const (Sil.Cint i) ->
@ -1251,17 +1254,21 @@ and sym_exe_check_variadic_sentinel ?(fails_on_nil = false) cfg pdesc tenv prop
(* error on the first premature nil argument *) (* error on the first premature nil argument *)
list_fold_left check_allocated [(prop, path)] non_terminal_argsi list_fold_left check_allocated [(prop, path)] non_terminal_argsi
and sym_exe_check_variadic_sentinel_if_present cfg pdesc tenv prop path actual_params callee_pname loc = and sym_exe_check_variadic_sentinel_if_present
match Cfg.Procdesc.find_from_name cfg callee_pname with cfg pdesc tenv prop path actual_params callee_pname loc =
| None -> [(prop, path)] match Specs.proc_resolve_attributes (Cfg.Procdesc.find_from_name cfg) callee_pname with
| Some callee_pdesc -> | None ->
let proc_attributes = Cfg.Procdesc.get_attributes callee_pdesc in [(prop, path)]
| Some callee_attributes ->
match Sil.get_sentinel_func_attribute_value match Sil.get_sentinel_func_attribute_value
proc_attributes.ProcAttributes.func_attributes with callee_attributes.ProcAttributes.func_attributes with
| None -> [(prop, path)] | None -> [(prop, path)]
| Some sentinel_arg -> | Some sentinel_arg ->
let formals = Cfg.Procdesc.get_formals callee_pdesc in let formals = callee_attributes.ProcAttributes.formals in
sym_exe_check_variadic_sentinel cfg pdesc tenv prop path (list_length formals) actual_params sentinel_arg callee_pname loc sym_exe_check_variadic_sentinel
cfg pdesc tenv prop path (list_length formals)
actual_params sentinel_arg callee_pname loc
(** Perform symbolic execution for a function call *) (** Perform symbolic execution for a function call *)
and sym_exec_call cfg pdesc tenv pre path ret_ids actual_pars summary loc = and sym_exec_call cfg pdesc tenv pre path ret_ids actual_pars summary loc =
@ -1468,8 +1475,9 @@ module ModelBuiltins = struct
: Builtin.ret_typ = : Builtin.ret_typ =
match args with match args with
| [(lexp, typ)] when list_length ret_ids <= 1 -> | [(lexp, typ)] when list_length ret_ids <= 1 ->
let pname = Cfg.Procdesc.get_proc_name pdesc in
let return_result_for_array_size e prop ret_ids = return_result e prop ret_ids in let return_result_for_array_size e prop ret_ids = return_result e prop ret_ids in
let n_lexp, prop = exp_norm_check_arith pdesc _prop lexp in let n_lexp, prop = exp_norm_check_arith pname _prop lexp in
begin begin
try try
let hpred = list_find (function let hpred = list_find (function
@ -1500,8 +1508,9 @@ module ModelBuiltins = struct
: Builtin.ret_typ = : Builtin.ret_typ =
match args, ret_ids with match args, ret_ids with
| [(lexp, typ); (size, _)], [] -> | [(lexp, typ); (size, _)], [] ->
let n_lexp, _prop' = exp_norm_check_arith pdesc _prop lexp in let pname = Cfg.Procdesc.get_proc_name pdesc in
let n_size, prop = exp_norm_check_arith pdesc _prop' size in let n_lexp, _prop' = exp_norm_check_arith pname _prop lexp in
let n_size, prop = exp_norm_check_arith pname _prop' size in
begin begin
try try
let hpred, sigma' = list_partition (function let hpred, sigma' = list_partition (function
@ -1534,8 +1543,9 @@ module ModelBuiltins = struct
let execute___print_value cfg pdesc instr tenv prop path ret_ids args callee_pname loc let execute___print_value cfg pdesc instr tenv prop path ret_ids args callee_pname loc
: Builtin.ret_typ = : Builtin.ret_typ =
L.err "__print_value: "; L.err "__print_value: ";
let pname = Cfg.Procdesc.get_proc_name pdesc in
let do_arg (lexp, typ) = let do_arg (lexp, typ) =
let n_lexp, _ = exp_norm_check_arith pdesc prop lexp in let n_lexp, _ = exp_norm_check_arith pname prop lexp in
L.err "%a " (Sil.pp_exp pe_text) n_lexp in L.err "%a " (Sil.pp_exp pe_text) n_lexp in
list_iter do_arg args; list_iter do_arg args;
L.err "@."; L.err "@.";
@ -1598,7 +1608,8 @@ module ModelBuiltins = struct
: Builtin.ret_typ = : Builtin.ret_typ =
match args with match args with
| [(lexp, typ)] when list_length ret_ids <= 1 -> | [(lexp, typ)] when list_length ret_ids <= 1 ->
let n_lexp, prop = exp_norm_check_arith pdesc _prop lexp in let pname = Cfg.Procdesc.get_proc_name pdesc in
let n_lexp, prop = exp_norm_check_arith pname _prop lexp in
let props = create_type tenv n_lexp typ prop in let props = create_type tenv n_lexp typ prop in
let aux prop = let aux prop =
begin begin
@ -1636,8 +1647,9 @@ module ModelBuiltins = struct
: Builtin.ret_typ = : Builtin.ret_typ =
match args with match args with
| [(_val1, typ1); (_texp2, typ2)] when list_length ret_ids <= 1 -> | [(_val1, typ1); (_texp2, typ2)] when list_length ret_ids <= 1 ->
let val1, __prop = exp_norm_check_arith pdesc _prop _val1 in let pname = Cfg.Procdesc.get_proc_name pdesc in
let texp2, prop = exp_norm_check_arith pdesc __prop _texp2 in let val1, __prop = exp_norm_check_arith pname _prop _val1 in
let texp2, prop = exp_norm_check_arith pname __prop _texp2 in
let exe_one_prop prop = let exe_one_prop prop =
if Sil.exp_equal texp2 Sil.exp_zero then if Sil.exp_equal texp2 Sil.exp_zero then
[(return_result Sil.exp_zero prop ret_ids, path)] [(return_result Sil.exp_zero prop ret_ids, path)]
@ -1719,7 +1731,8 @@ module ModelBuiltins = struct
: Builtin.ret_typ = : Builtin.ret_typ =
match args, ret_ids with match args, ret_ids with
| [(lexp, typ)], _ -> | [(lexp, typ)], _ ->
let n_lexp, prop = exp_norm_check_arith pdesc _prop lexp in let pname = Cfg.Procdesc.get_proc_name pdesc in
let n_lexp, prop = exp_norm_check_arith pname _prop lexp in
set_resource_attribute prop path n_lexp loc Sil.Rfile set_resource_attribute prop path n_lexp loc Sil.Rfile
| _ -> raise (Exceptions.Wrong_argument_number (try assert false with Assert_failure x -> x)) | _ -> raise (Exceptions.Wrong_argument_number (try assert false with Assert_failure x -> x))
@ -1728,7 +1741,8 @@ module ModelBuiltins = struct
: Builtin.ret_typ = : Builtin.ret_typ =
match args, ret_ids with match args, ret_ids with
| [(lexp, typ)], _ -> | [(lexp, typ)], _ ->
let n_lexp, prop = exp_norm_check_arith pdesc _prop lexp in let pname = Cfg.Procdesc.get_proc_name pdesc in
let n_lexp, prop = exp_norm_check_arith pname _prop lexp in
set_resource_attribute prop path n_lexp loc Sil.Rlock set_resource_attribute prop path n_lexp loc Sil.Rlock
| _ -> raise (Exceptions.Wrong_argument_number (try assert false with Assert_failure x -> x)) | _ -> raise (Exceptions.Wrong_argument_number (try assert false with Assert_failure x -> x))
@ -1738,7 +1752,8 @@ module ModelBuiltins = struct
: Builtin.ret_typ = : Builtin.ret_typ =
match args, ret_ids with match args, ret_ids with
| [_ ; (lexp, typ)], _ -> | [_ ; (lexp, typ)], _ ->
let n_lexp, prop = exp_norm_check_arith pdesc _prop lexp in let pname = Cfg.Procdesc.get_proc_name pdesc in
let n_lexp, prop = exp_norm_check_arith pname _prop lexp in
set_resource_attribute prop path n_lexp loc Sil.Rignore set_resource_attribute prop path n_lexp loc Sil.Rignore
| _ -> raise (Exceptions.Wrong_argument_number (try assert false with Assert_failure x -> x)) | _ -> raise (Exceptions.Wrong_argument_number (try assert false with Assert_failure x -> x))
@ -1747,7 +1762,8 @@ module ModelBuiltins = struct
: Builtin.ret_typ = : Builtin.ret_typ =
match args, ret_ids with match args, ret_ids with
| [(lexp, typ)], _ -> | [(lexp, typ)], _ ->
let n_lexp, prop = exp_norm_check_arith pdesc _prop lexp in let pname = Cfg.Procdesc.get_proc_name pdesc in
let n_lexp, prop = exp_norm_check_arith pname _prop lexp in
set_resource_attribute prop path n_lexp loc (Sil.Rmemory Sil.Mnew) set_resource_attribute prop path n_lexp loc (Sil.Rmemory Sil.Mnew)
| _ -> raise (Exceptions.Wrong_argument_number (try assert false with Assert_failure x -> x)) | _ -> raise (Exceptions.Wrong_argument_number (try assert false with Assert_failure x -> x))
@ -1756,7 +1772,8 @@ module ModelBuiltins = struct
: Builtin.ret_typ = : Builtin.ret_typ =
match args, ret_ids with match args, ret_ids with
| [(lexp, typ)], _ -> | [(lexp, typ)], _ ->
let n_lexp, prop = exp_norm_check_arith pdesc _prop lexp in let pname = Cfg.Procdesc.get_proc_name pdesc in
let n_lexp, prop = exp_norm_check_arith pname _prop lexp in
let prop' = match Prop.get_taint_attribute prop n_lexp with let prop' = match Prop.get_taint_attribute prop n_lexp with
| _ -> | _ ->
let check_attr_change att_old att_new = () in let check_attr_change att_old att_new = () in
@ -1770,7 +1787,8 @@ module ModelBuiltins = struct
: Builtin.ret_typ = : Builtin.ret_typ =
match args, ret_ids with match args, ret_ids with
| [(lexp, typ)], _ -> | [(lexp, typ)], _ ->
let n_lexp, prop = exp_norm_check_arith pdesc _prop lexp in let pname = Cfg.Procdesc.get_proc_name pdesc in
let n_lexp, prop = exp_norm_check_arith pname _prop lexp in
let prop' = match Prop.get_taint_attribute prop n_lexp with let prop' = match Prop.get_taint_attribute prop n_lexp with
| _ -> | _ ->
let check_attr_change att_old att_new = () in let check_attr_change att_old att_new = () in
@ -1784,7 +1802,8 @@ module ModelBuiltins = struct
: Builtin.ret_typ = : Builtin.ret_typ =
match args with match args with
| [(lexp, typ)] -> | [(lexp, typ)] ->
let n_lexp, prop = exp_norm_check_arith pdesc _prop lexp in let pname = Cfg.Procdesc.get_proc_name pdesc in
let n_lexp, prop = exp_norm_check_arith pname _prop lexp in
let ret_val = ref None in let ret_val = ref None in
let return_val p = match !ret_val with let return_val p = match !ret_val with
| Some e -> return_result e p ret_ids | Some e -> return_result e p ret_ids
@ -1819,8 +1838,9 @@ module ModelBuiltins = struct
: Builtin.ret_typ = : Builtin.ret_typ =
match args with match args with
| [(lexp1, typ1); (lexp2, typ2)] -> | [(lexp1, typ1); (lexp2, typ2)] ->
let n_lexp1, _prop1 = exp_norm_check_arith pdesc _prop lexp1 in let pname = Cfg.Procdesc.get_proc_name pdesc in
let n_lexp2, prop = exp_norm_check_arith pdesc _prop1 lexp2 in let n_lexp1, _prop1 = exp_norm_check_arith pname _prop lexp1 in
let n_lexp2, prop = exp_norm_check_arith pname _prop1 lexp2 in
let foot_var = lazy (Sil.Var (Ident.create_fresh Ident.kfootprint)) in let foot_var = lazy (Sil.Var (Ident.create_fresh Ident.kfootprint)) in
let filter_fld_hidden (f, _ ) = Ident.fieldname_is_hidden f in let filter_fld_hidden (f, _ ) = Ident.fieldname_is_hidden f in
let has_fld_hidden fsel = list_exists filter_fld_hidden fsel in let has_fld_hidden fsel = list_exists filter_fld_hidden fsel in
@ -1846,9 +1866,10 @@ module ModelBuiltins = struct
: Builtin.ret_typ = : Builtin.ret_typ =
match args with match args with
| [(lexp, typ)] when list_length ret_ids <= 1 -> | [(lexp, typ)] when list_length ret_ids <= 1 ->
let pname = Cfg.Procdesc.get_proc_name pdesc in
(match ret_ids with (match ret_ids with
| [ret_id] -> | [ret_id] ->
let n_lexp, prop = exp_norm_check_arith pdesc _prop lexp in let n_lexp, prop = exp_norm_check_arith pname _prop lexp in
[(return_result (Sil.BinOp(Sil.Ne, n_lexp, (Sil.Const(Sil.Cattribute((Sil.Auntaint)))))) prop ret_ids, path)] [(return_result (Sil.BinOp(Sil.Ne, n_lexp, (Sil.Const(Sil.Cattribute((Sil.Auntaint)))))) prop ret_ids, path)]
| _ -> [(_prop, path)]) | _ -> [(_prop, path)])
| _ -> raise (Exceptions.Wrong_argument_number (try assert false with Assert_failure x -> x)) | _ -> raise (Exceptions.Wrong_argument_number (try assert false with Assert_failure x -> x))
@ -1928,9 +1949,10 @@ module ModelBuiltins = struct
: Builtin.ret_typ = : Builtin.ret_typ =
match args, ret_ids with match args, ret_ids with
| [(lexp, typ)], _ -> | [(lexp, typ)], _ ->
let pname = Cfg.Procdesc.get_proc_name pdesc in
let prop = return_result lexp _prop ret_ids in let prop = return_result lexp _prop ret_ids in
if !Config.objc_memory_model_on then if !Config.objc_memory_model_on then
let n_lexp, prop = exp_norm_check_arith pdesc prop lexp in let n_lexp, prop = exp_norm_check_arith pname prop lexp in
let check_attr_change att_old att_new = () in let check_attr_change att_old att_new = () in
let prop' = Prop.add_or_replace_exp_attribute check_attr_change prop n_lexp Sil.Aautorelease in let prop' = Prop.add_or_replace_exp_attribute check_attr_change prop n_lexp Sil.Aautorelease in
[(prop', path)] [(prop', path)]
@ -1967,8 +1989,9 @@ module ModelBuiltins = struct
: Builtin.ret_typ = : Builtin.ret_typ =
match args with match args with
| [(_val1, typ1); (_texp2, typ2)] when list_length ret_ids <= 1 -> | [(_val1, typ1); (_texp2, typ2)] when list_length ret_ids <= 1 ->
let val1, __prop = exp_norm_check_arith pdesc _prop _val1 in let pname = Cfg.Procdesc.get_proc_name pdesc in
let texp2, prop = exp_norm_check_arith pdesc __prop _texp2 in let val1, __prop = exp_norm_check_arith pname _prop _val1 in
let texp2, prop = exp_norm_check_arith pname __prop _texp2 in
(try (try
let hpred = list_find (function let hpred = list_find (function
| Sil.Hpointsto(e1, _, _) -> Sil.exp_equal e1 val1 | Sil.Hpointsto(e1, _, _) -> Sil.exp_equal e1 val1
@ -2028,7 +2051,8 @@ module ModelBuiltins = struct
match args with match args with
| [(lexp, typ)] -> | [(lexp, typ)] ->
begin begin
let n_lexp, prop = exp_norm_check_arith pdesc _prop lexp in let pname = Cfg.Procdesc.get_proc_name pdesc in
let n_lexp, prop = exp_norm_check_arith pname _prop lexp in
let prop_nonzero = (* case n_lexp!=0 *) let prop_nonzero = (* case n_lexp!=0 *)
Propset.to_proplist (prune_polarity tenv true n_lexp prop) in Propset.to_proplist (prune_polarity tenv true n_lexp prop) in
let prop_zero = (* case n_lexp==0 *) let prop_zero = (* case n_lexp==0 *)
@ -2044,6 +2068,7 @@ module ModelBuiltins = struct
let execute_alloc mk can_return_null cfg pdesc instr tenv _prop path ret_ids args callee_pname loc let execute_alloc mk can_return_null cfg pdesc instr tenv _prop path ret_ids args callee_pname loc
: Builtin.ret_typ = : Builtin.ret_typ =
let pname = Cfg.Procdesc.get_proc_name pdesc in
let rec evaluate_char_sizeof e = match e with let rec evaluate_char_sizeof e = match e with
| Sil.Var _ -> e | Sil.Var _ -> e
| Sil.UnOp (uop, e', typ) -> | Sil.UnOp (uop, e', typ) ->
@ -2067,7 +2092,7 @@ module ModelBuiltins = struct
| [ret_id] -> ret_id | [ret_id] -> ret_id
| _ -> Ident.create_fresh Ident.kprimed in | _ -> Ident.create_fresh Ident.kprimed in
let size_exp', prop = let size_exp', prop =
let n_size_exp, prop = exp_norm_check_arith pdesc _prop size_exp in let n_size_exp, prop = exp_norm_check_arith pname _prop size_exp in
let n_size_exp' = evaluate_char_sizeof n_size_exp in let n_size_exp' = evaluate_char_sizeof n_size_exp in
Prop.exp_normalize_prop prop n_size_exp', prop in Prop.exp_normalize_prop prop n_size_exp', prop in
let cnt_te = handle_sizeof_exp size_exp' in let cnt_te = handle_sizeof_exp size_exp' in
@ -2128,7 +2153,8 @@ module ModelBuiltins = struct
match args with match args with
| [(ret_exn, _)] -> | [(ret_exn, _)] ->
begin begin
let n_ret_exn, prop = exp_norm_check_arith pdesc _prop ret_exn in let pname = Cfg.Procdesc.get_proc_name pdesc in
let n_ret_exn, prop = exp_norm_check_arith pname _prop ret_exn in
match n_ret_exn with match n_ret_exn with
| Sil.Const (Sil.Cexn exp) -> | Sil.Const (Sil.Cexn exp) ->
let prop_with_exn = return_result exp prop ret_ids in let prop_with_exn = return_result exp prop ret_ids in
@ -2141,7 +2167,8 @@ module ModelBuiltins = struct
: Builtin.ret_typ = : Builtin.ret_typ =
match args with match args with
| (_arg1, _):: _ -> | (_arg1, _):: _ ->
let arg1, prop = exp_norm_check_arith pdesc _prop _arg1 in let pname = Cfg.Procdesc.get_proc_name pdesc in
let arg1, prop = exp_norm_check_arith pname _prop _arg1 in
let prop' = return_result arg1 prop ret_ids in let prop' = return_result arg1 prop ret_ids in
[(prop', path)] [(prop', path)]
| _ -> raise (Exceptions.Wrong_argument_number (try assert false with Assert_failure x -> x)) | _ -> raise (Exceptions.Wrong_argument_number (try assert false with Assert_failure x -> x))
@ -2150,9 +2177,10 @@ module ModelBuiltins = struct
: Builtin.ret_typ = : Builtin.ret_typ =
match args with match args with
| [(lexp1, _); (lexp2, _); (lexp3, _)] -> | [(lexp1, _); (lexp2, _); (lexp3, _)] ->
let n_lexp1, prop = exp_norm_check_arith pdesc _prop lexp1 in let pname = Cfg.Procdesc.get_proc_name pdesc in
let n_lexp2, prop = exp_norm_check_arith pdesc _prop lexp2 in let n_lexp1, prop = exp_norm_check_arith pname _prop lexp1 in
let n_lexp3, prop = exp_norm_check_arith pdesc _prop lexp3 in let n_lexp2, prop = exp_norm_check_arith pname _prop lexp2 in
let n_lexp3, prop = exp_norm_check_arith pname _prop lexp3 in
(match n_lexp1, n_lexp2, n_lexp3 with (match n_lexp1, n_lexp2, n_lexp3 with
| Sil.Const (Sil.Cstr str1), Sil.Const (Sil.Cstr str2), Sil.Const (Sil.Cint n_sil) -> | Sil.Const (Sil.Cstr str1), Sil.Const (Sil.Cstr str2), Sil.Const (Sil.Cint n_sil) ->
(let n = Sil.Int.to_int n_sil in (let n = Sil.Int.to_int n_sil in
@ -2175,8 +2203,9 @@ module ModelBuiltins = struct
: Builtin.ret_typ = : Builtin.ret_typ =
match args with match args with
| [(lexp1, _); (lexp2, _)] -> | [(lexp1, _); (lexp2, _)] ->
let n_lexp1, _prop' = exp_norm_check_arith pdesc _prop lexp1 in let pname = Cfg.Procdesc.get_proc_name pdesc in
let n_lexp2, prop = exp_norm_check_arith pdesc _prop' lexp2 in let n_lexp1, _prop' = exp_norm_check_arith pname _prop lexp1 in
let n_lexp2, prop = exp_norm_check_arith pname _prop' lexp2 in
(match n_lexp1, n_lexp2 with (match n_lexp1, n_lexp2 with
| Sil.Const (Sil.Ctuple el), Sil.Const (Sil.Cint i) -> | Sil.Const (Sil.Ctuple el), Sil.Const (Sil.Cint i) ->
let n = Sil.Int.to_int i in let n = Sil.Int.to_int i in

29
infer/src/checkers/annotations.ml
Unescape View File

@ -146,23 +146,28 @@ let ia_is ann ia = match ann with
type get_method_annotation = Procname.t -> Cfg.Procdesc.t -> Sil.method_annotation type get_method_annotation = Procname.t -> Cfg.Procdesc.t -> Sil.method_annotation
(** Get a method signature with annotations from a proc_name and proc_desc,
or search in the .specs file if it is not defined in the proc_desc. *) (** Get a method signature with annotations from a proc_attributes. *)
let get_annotated_signature get_method_annotation proc_desc proc_name : annotated_signature = let get_annotated_signature proc_attributes : annotated_signature =
let method_annotation = get_method_annotation proc_name proc_desc in let method_annotation = proc_attributes.ProcAttributes.method_annotation in
let formals = Cfg.Procdesc.get_formals proc_desc in let formals = proc_attributes.ProcAttributes.formals in
let ret_type = Cfg.Procdesc.get_ret_type proc_desc in let ret_type = proc_attributes.ProcAttributes.ret_type in
let (ia, ial) = method_annotation in let (ia, ial0) = method_annotation in
let natl = let natl =
let rec extract ial parl = match ial, parl with let rec extract ial parl = match ial, parl with
| ia :: ial', (name, typ) :: parl' -> (name, ia, typ) :: extract ial' parl' | ia :: ial', (name, typ) :: parl' ->
| [], (name, typ) :: parl' -> (name, Sil.item_annotation_empty, typ) :: extract [] parl' (name, ia, typ) :: extract ial' parl'
| [], [] -> [] | [], (name, typ) :: parl' ->
| _ :: _, [] -> assert false in (name, Sil.item_annotation_empty, typ) :: extract [] parl'
list_rev (extract (list_rev ial) (list_rev formals)) in | [], [] ->
[]
| _ :: _, [] ->
assert false in
list_rev (extract (list_rev ial0) (list_rev formals)) in
let annotated_signature = { ret = (ia, ret_type); params = natl } in let annotated_signature = { ret = (ia, ret_type); params = natl } in
annotated_signature annotated_signature
(** Check if the annotated signature is for a wrapper of an anonymous inner class method. (** Check if the annotated signature is for a wrapper of an anonymous inner class method.
These wrappers have the same name as the original method, every type is Object, and the parameters These wrappers have the same name as the original method, every type is Object, and the parameters
are called x0, x1, x2. *) are called x0, x1, x2. *)

5
infer/src/checkers/annotations.mli
Unescape View File

@ -44,9 +44,8 @@ val equal : annotated_signature -> annotated_signature -> bool
type get_method_annotation = Procname.t -> Cfg.Procdesc.t -> Sil.method_annotation type get_method_annotation = Procname.t -> Cfg.Procdesc.t -> Sil.method_annotation
(** Get the annotated signature of the procedure *) (** Get a method signature with annotations from a proc_attributes. *)
val get_annotated_signature : val get_annotated_signature : ProcAttributes.t -> annotated_signature
get_method_annotation -> Cfg.Procdesc.t -> Procname.t -> annotated_signature
(** Return the type of the field [fn] and its annotation, None if [typ] has no field named [fn] *) (** Return the type of the field [fn] and its annotation, None if [typ] has no field named [fn] *)
val get_field_type_and_annotation : val get_field_type_and_annotation :

9
infer/src/checkers/checkers.ml
Unescape View File

@ -76,6 +76,7 @@ module ST = struct
(Option.default "" advice) (Option.default "" advice)
[("always_report", string_of_bool always_report)] in [("always_report", string_of_bool always_report)] in
let exn = exception_kind kind localized_description in let exn = exception_kind kind localized_description in
let proc_attributes = Specs.pdesc_resolve_attributes proc_desc in
(* Errors can be suppressed with annotations. An error of kind CHECKER_ERROR_NAME can be (* Errors can be suppressed with annotations. An error of kind CHECKER_ERROR_NAME can be
suppressed with the following annotations: suppressed with the following annotations:
@ -101,11 +102,11 @@ module ST = struct
let is_method_suppressed = let is_method_suppressed =
Annotations.ma_has_annotation_with Annotations.ma_has_annotation_with
(Specs.proc_get_method_annotation proc_name proc_desc) proc_attributes.ProcAttributes.method_annotation
annotation_matches in annotation_matches in
let is_field_suppressed = let is_field_suppressed =
match field_name, PatternMatch.get_this_type proc_desc with match field_name, PatternMatch.get_this_type proc_attributes with
| Some field_name, Some t -> begin | Some field_name, Some t -> begin
match (Annotations.get_field_type_and_annotation field_name t) with match (Annotations.get_field_type_and_annotation field_name t) with
| Some (_, ia) -> Annotations.ia_has_annotation_with ia annotation_matches | Some (_, ia) -> Annotations.ia_has_annotation_with ia annotation_matches
@ -114,7 +115,7 @@ module ST = struct
| _ -> false in | _ -> false in
let is_class_suppressed = let is_class_suppressed =
match (PatternMatch.get_this_type proc_desc) with match PatternMatch.get_this_type proc_attributes with
| Some t -> begin | Some t -> begin
match (PatternMatch.type_get_annotation t) with match (PatternMatch.type_get_annotation t) with
| Some ia -> Annotations.ia_has_annotation_with ia annotation_matches | Some ia -> Annotations.ia_has_annotation_with ia annotation_matches
@ -338,7 +339,7 @@ let callback_test_state all_procs get_proc_desc idenv tenv proc_name proc_desc =
(** Check the uses of VisibleForTesting *) (** Check the uses of VisibleForTesting *)
let callback_checkVisibleForTesting all_procs get_proc_desc idenv tenv proc_name proc_desc = let callback_checkVisibleForTesting all_procs get_proc_desc idenv tenv proc_name proc_desc =
let ma = Specs.proc_get_method_annotation proc_name proc_desc in let ma = (Specs.pdesc_resolve_attributes proc_desc).ProcAttributes.method_annotation in
if Annotations.ma_contains ma [Annotations.visibleForTesting] then if Annotations.ma_contains ma [Annotations.visibleForTesting] then
begin begin
let loc = Cfg.Procdesc.get_loc proc_desc in let loc = Cfg.Procdesc.get_loc proc_desc in

23
infer/src/checkers/eradicate.ml
Unescape View File

@ -54,7 +54,7 @@ struct
let old_summ = Specs.get_summary_unsafe proc_name in let old_summ = Specs.get_summary_unsafe proc_name in
let nodes = list_map (fun n -> Cfg.Node.get_id n) (Cfg.Procdesc.get_nodes proc_desc) in let nodes = list_map (fun n -> Cfg.Node.get_id n) (Cfg.Procdesc.get_nodes proc_desc) in
let method_annotation = let method_annotation =
(Specs.proc_get_attributes proc_name proc_desc).ProcAttributes.method_annotation in (Specs.pdesc_resolve_attributes proc_desc).ProcAttributes.method_annotation in
let new_summ = let new_summ =
{ {
old_summ with old_summ with
@ -177,7 +177,7 @@ struct
let do_proc (init_pn, init_pd) = let do_proc (init_pn, init_pd) =
let filter callee_pn callee_pd = let filter callee_pn callee_pd =
let is_private = let is_private =
let attr = Specs.proc_get_attributes callee_pn callee_pd in let attr = Specs.pdesc_resolve_attributes callee_pd in
attr.ProcAttributes.access = Sil.Private in attr.ProcAttributes.access = Sil.Private in
let same_class = let same_class =
let get_class_opt pn = let get_class_opt pn =
@ -215,7 +215,8 @@ struct
(** Get the final typestates of all the initializers. *) (** Get the final typestates of all the initializers. *)
let final_typestates = ref [] in let final_typestates = ref [] in
let get_final_typestate (pname, pdesc) = let get_final_typestate (pname, pdesc) =
let ann_sig = Models.get_annotated_signature pdesc pname in let ann_sig =
Models.get_modelled_annotated_signature (Cfg.Procdesc.get_attributes pdesc) in
let loc = Cfg.Procdesc.get_loc pdesc in let loc = Cfg.Procdesc.get_loc pdesc in
let idenv_pn = Idenv.create_from_idenv idenv pdesc in let idenv_pn = Idenv.create_from_idenv idenv pdesc in
match typecheck_proc false idenv_pn pname pdesc ann_sig loc with match typecheck_proc false idenv_pn pname pdesc ann_sig loc with
@ -238,8 +239,10 @@ struct
let final_initializer_typestates_lazy = lazy let final_initializer_typestates_lazy = lazy
begin begin
let is_initializer pdesc pname = let is_initializer pdesc pname =
PatternMatch.method_is_initializer tenv pname pdesc || PatternMatch.method_is_initializer tenv (Cfg.Procdesc.get_attributes pdesc) ||
let ia, _ = (Models.get_annotated_signature pdesc pname).Annotations.ret in let ia, _ =
(Models.get_modelled_annotated_signature
(Cfg.Procdesc.get_attributes pdesc)).Annotations.ret in
Annotations.ia_is_initializer ia in Annotations.ia_is_initializer ia in
let initializers_current_class = let initializers_current_class =
pname_and_pdescs_with pname_and_pdescs_with
@ -306,15 +309,17 @@ struct
let filter_special_cases () = let filter_special_cases () =
if Procname.java_is_access_method proc_name || if Procname.java_is_access_method proc_name ||
(Specs.proc_get_attributes proc_name proc_desc).ProcAttributes.is_bridge_method (Specs.pdesc_resolve_attributes proc_desc).ProcAttributes.is_bridge_method
then None then None
else else
begin begin
let annotated_signature = Models.get_annotated_signature proc_desc proc_name in let annotated_signature =
if (Specs.proc_get_attributes proc_name proc_desc).ProcAttributes.is_abstract then Models.get_modelled_annotated_signature (Specs.pdesc_resolve_attributes proc_desc) in
if (Specs.pdesc_resolve_attributes proc_desc).ProcAttributes.is_abstract then
begin begin
if Models.infer_library_return && if Models.infer_library_return &&
EradicateChecks.classify_procedure proc_name proc_desc = "L" then EradicateChecks.classify_procedure (Cfg.Procdesc.get_attributes proc_desc) = "L"
then
(let ret_is_nullable = (* get the existing annotation *) (let ret_is_nullable = (* get the existing annotation *)
let ia, _ = annotated_signature.Annotations.ret in let ia, _ = annotated_signature.Annotations.ret in
Annotations.ia_is_nullable ia in Annotations.ia_is_nullable ia in

36
infer/src/checkers/eradicateChecks.ml
Unescape View File

@ -55,13 +55,14 @@ let explain_expr node e =
| None -> None | None -> None
(** Classify a procedure. *) (** Classify a procedure. *)
let classify_procedure pn pd = let classify_procedure proc_attributes =
let pn = proc_attributes.ProcAttributes.proc_name in
let unique_id = Procname.to_unique_id pn in let unique_id = Procname.to_unique_id pn in
let classification = let classification =
if Models.is_modelled_nullable pn then "M" (* modelled *) if Models.is_modelled_nullable pn then "M" (* modelled *)
else if Models.is_ret_library pn then "R" (* return library *) else if Models.is_ret_library pn then "R" (* return library *)
else if Specs.proc_is_library pn pd then "L" (* library *) else if Specs.proc_is_library proc_attributes then "L" (* library *)
else if not (Cfg.Procdesc.is_defined pd) then "S" (* skip *) else if not proc_attributes.ProcAttributes.is_defined then "S" (* skip *)
else if string_is_prefix "com.facebook" unique_id then "F" (* FB *) else if string_is_prefix "com.facebook" unique_id then "F" (* FB *)
else "?" in else "?" in
classification classification
@ -248,7 +249,7 @@ let check_constructor_initialization
State.set_node start_node; State.set_node start_node;
if Procname.is_constructor curr_pname if Procname.is_constructor curr_pname
then begin then begin
match PatternMatch.get_this_type curr_pdesc with match PatternMatch.get_this_type (Cfg.Procdesc.get_attributes curr_pdesc) with
| Some (Sil.Tptr (Sil.Tstruct (ftal, _, _, nameo, _, _, _) as ts, _)) -> | Some (Sil.Tptr (Sil.Tstruct (ftal, _, _, nameo, _, _, _) as ts, _)) ->
let do_fta (fn, ft, ia) = let do_fta (fn, ft, ia) =
let annotated_with f = match get_field_annotation fn ts with let annotated_with f = match get_field_annotation fn ts with
@ -375,7 +376,8 @@ let check_return_annotation
return_not_nullable return_not_nullable
| _ -> | _ ->
false in false in
if Models.infer_library_return && classify_procedure curr_pname curr_pdesc = "L" if Models.infer_library_return &&
classify_procedure (Cfg.Procdesc.get_attributes curr_pdesc) = "L"
then pp_inferred_return_annotation return_not_nullable curr_pname then pp_inferred_return_annotation return_not_nullable curr_pname
(** Check the receiver of a virtual call. *) (** Check the receiver of a virtual call. *)
@ -418,9 +420,10 @@ let check_call_receiver
(** Check the parameters of a call. *) (** Check the parameters of a call. *)
let check_call_parameters let check_call_parameters
find_canonical_duplicate curr_pname node typestate callee_pname find_canonical_duplicate curr_pname node typestate callee_attributes
callee_pdesc sig_params call_params loc annotated_signature sig_params call_params loc annotated_signature
instr_ref typecheck_expr print_current_state : unit = instr_ref typecheck_expr print_current_state : unit =
let callee_pname = callee_attributes.ProcAttributes.proc_name in
let has_this = is_virtual sig_params in let has_this = is_virtual sig_params in
let tot_param_num = list_length sig_params - (if has_this then 1 else 0) in let tot_param_num = list_length sig_params - (if has_this then 1 else 0) in
let rec check sparams cparams = match sparams, cparams with let rec check sparams cparams = match sparams, cparams with
@ -455,7 +458,7 @@ let check_call_parameters
let origin_descr = TypeAnnotation.descr_origin ta2 in let origin_descr = TypeAnnotation.descr_origin ta2 in
let param_num = list_length sparams' + (if has_this then 0 else 1) in let param_num = list_length sparams' + (if has_this then 0 else 1) in
let callee_loc = Cfg.Procdesc.get_loc callee_pdesc in let callee_loc = callee_attributes.ProcAttributes.loc in
report_error report_error
find_canonical_duplicate find_canonical_duplicate
node node
@ -477,7 +480,7 @@ let check_call_parameters
if check_library_calls then true if check_library_calls then true
else else
Models.is_modelled_nullable callee_pname || Models.is_modelled_nullable callee_pname ||
Cfg.Procdesc.is_defined callee_pdesc || callee_attributes.ProcAttributes.is_defined ||
Specs.get_summary callee_pname <> None in Specs.get_summary callee_pname <> None in
if should_check_parameters then if should_check_parameters then
(* left to right to avoid guessing the different lengths *) (* left to right to avoid guessing the different lengths *)
@ -530,13 +533,12 @@ let check_overridden_annotations
ignore (list_fold_left2 compare initial_pos current_params overridden_params) in ignore (list_fold_left2 compare initial_pos current_params overridden_params) in
let check overriden_proc_name = let check overriden_proc_name =
(* TODO (#5280260): investigate why proc_desc may not be found *) match Specs.proc_resolve_attributes get_proc_desc overriden_proc_name with
match get_proc_desc overriden_proc_name with | Some attributes ->
| Some overriden_proc_desc -> let overridden_signature = Models.get_modelled_annotated_signature attributes in
let overriden_signature = check_return overriden_proc_name overridden_signature;
Models.get_annotated_signature overriden_proc_desc overriden_proc_name in check_params overriden_proc_name overridden_signature
check_return overriden_proc_name overriden_signature; | None ->
check_params overriden_proc_name overriden_signature () in
| None -> () in
PatternMatch.proc_iter_overridden_methods check tenv proc_name PatternMatch.proc_iter_overridden_methods check tenv proc_name

26
infer/src/checkers/models.ml
Unescape View File

@ -114,21 +114,21 @@ let ret_library_table : table_t Lazy.t =
lazy (Marshal.from_string Eradicate_library.marshalled_library_table 0) lazy (Marshal.from_string Eradicate_library.marshalled_library_table 0)
*) *)
(** Return the annotated signature of the procedure, taking into account models. *) (** Return the annotated signature of the procedure, taking into account models. *)
let get_annotated_signature callee_pdesc callee_pname = let get_modelled_annotated_signature proc_attributes =
let annotated_signature = let proc_name = proc_attributes.ProcAttributes.proc_name in
Annotations.get_annotated_signature let annotated_signature = Annotations.get_annotated_signature proc_attributes in
Specs.proc_get_method_annotation callee_pdesc callee_pname in let proc_id = Procname.to_unique_id proc_name in
let proc_id = Procname.to_unique_id callee_pname in
let infer_parameters ann_sig = let infer_parameters ann_sig =
let mark_par = let mark_par =
if Inference.enabled then Inference.proc_parameters_marked callee_pname if Inference.enabled then Inference.proc_parameters_marked proc_name
else None in else None in
match mark_par with match mark_par with
| None -> ann_sig | None -> ann_sig
| Some bs -> | Some bs ->
let mark = (false, bs) in let mark = (false, bs) in
Annotations.annotated_signature_mark callee_pname Annotations.Nullable ann_sig mark in Annotations.annotated_signature_mark proc_name Annotations.Nullable ann_sig mark in
let infer_return ann_sig = let infer_return ann_sig =
let mark_r = let mark_r =
let from_library = let from_library =
@ -137,16 +137,17 @@ let get_annotated_signature callee_pdesc callee_pname =
Hashtbl.find (Lazy.force ret_library_table) proc_id Hashtbl.find (Lazy.force ret_library_table) proc_id
with Not_found -> false with Not_found -> false
else false in else false in
let from_inference = Inference.enabled && Inference.proc_return_is_marked callee_pname in let from_inference = Inference.enabled &&
Inference.proc_return_is_marked proc_name in
from_library || from_inference in from_library || from_inference in
if mark_r if mark_r
then Annotations.annotated_signature_mark_return callee_pname Annotations.Nullable ann_sig then Annotations.annotated_signature_mark_return proc_name Annotations.Nullable ann_sig
else ann_sig in else ann_sig in
let lookup_models_nullable ann_sig = let lookup_models_nullable ann_sig =
if use_models then if use_models then
try try
let mark = Hashtbl.find annotated_table_nullable proc_id in let mark = Hashtbl.find annotated_table_nullable proc_id in
Annotations.annotated_signature_mark callee_pname Annotations.Nullable ann_sig mark Annotations.annotated_signature_mark proc_name Annotations.Nullable ann_sig mark
with Not_found -> with Not_found ->
ann_sig ann_sig
else ann_sig in else ann_sig in
@ -154,7 +155,7 @@ let get_annotated_signature callee_pdesc callee_pname =
if use_models then if use_models then
try try
let mark = Hashtbl.find annotated_table_present proc_id in let mark = Hashtbl.find annotated_table_present proc_id in
Annotations.annotated_signature_mark callee_pname Annotations.Present ann_sig mark Annotations.annotated_signature_mark proc_name Annotations.Present ann_sig mark
with Not_found -> with Not_found ->
ann_sig ann_sig
else ann_sig in else ann_sig in
@ -162,7 +163,7 @@ let get_annotated_signature callee_pdesc callee_pname =
if use_models if use_models
&& Hashtbl.mem annotated_table_strict proc_id && Hashtbl.mem annotated_table_strict proc_id
then then
Annotations.annotated_signature_mark_return_strict callee_pname ann_sig Annotations.annotated_signature_mark_return_strict proc_name ann_sig
else else
ann_sig in ann_sig in
@ -173,6 +174,7 @@ let get_annotated_signature callee_pdesc callee_pname =
|> infer_return |> infer_return
|> infer_parameters |> infer_parameters
(** Return true when the procedure has been modelled for nullable. *) (** Return true when the procedure has been modelled for nullable. *)
let is_modelled_nullable proc_name = let is_modelled_nullable proc_name =
if use_models then if use_models then

9
infer/src/checkers/patternMatch.ml
Unescape View File

@ -32,7 +32,7 @@ let is_direct_subtype_of this_type super_type_name =
| _ -> false | _ -> false
(** The type the method is invoked on *) (** The type the method is invoked on *)
let get_this_type proc_desc = match Cfg.Procdesc.get_formals proc_desc with let get_this_type proc_attributes = match proc_attributes.ProcAttributes.formals with
| (n, t):: args -> Some t | (n, t):: args -> Some t
| _ -> None | _ -> None
@ -275,12 +275,11 @@ let type_has_initializer
(** Check if the method is one of the known initializer methods. *) (** Check if the method is one of the known initializer methods. *)
let method_is_initializer let method_is_initializer
(tenv: Sil.tenv) (tenv: Sil.tenv)
(proc_name: Procname.t) (proc_attributes: ProcAttributes.t) : bool =
(proc_desc: Cfg.Procdesc.t) : bool = match get_this_type proc_attributes with
match get_this_type proc_desc with
| Some this_type -> | Some this_type ->
if type_has_initializer tenv this_type then if type_has_initializer tenv this_type then
let mname = Procname.java_get_method proc_name in let mname = Procname.java_get_method (proc_attributes.ProcAttributes.proc_name) in
list_exists (string_equal mname) initializer_methods list_exists (string_equal mname) initializer_methods
else else
false false

4
infer/src/checkers/patternMatch.mli
Unescape View File

@ -18,7 +18,7 @@ val get_java_method_call_formal_signature :
Sil.instr -> (string * string * string list * string) option Sil.instr -> (string * string * string list * string) option
(** Get the this type of a procedure *) (** Get the this type of a procedure *)
val get_this_type : Cfg.Procdesc.t -> Sil.typ option val get_this_type : ProcAttributes.t -> Sil.typ option
(** Get the name of a type *) (** Get the name of a type *)
val get_type_name : Sil.typ -> string val get_type_name : Sil.typ -> string
@ -29,7 +29,7 @@ val get_vararg_type_names : Cfg.Node.t -> Sil.pvar -> string list
val has_formal_method_argument_type_names : Cfg.Procdesc.t -> Procname.t -> string list -> bool val has_formal_method_argument_type_names : Cfg.Procdesc.t -> Procname.t -> string list -> bool
(** Check if the method is one of the known initializer methods. *) (** Check if the method is one of the known initializer methods. *)
val method_is_initializer : Sil.tenv -> Procname.t -> Cfg.Procdesc.t -> bool val method_is_initializer : Sil.tenv -> ProcAttributes.t -> bool
(** Is this a getter proc name? *) (** Is this a getter proc name? *)
val is_getter : Procname.t -> bool val is_getter : Procname.t -> bool

18
infer/src/checkers/repeatedCallsChecker.ml
Unescape View File

@ -99,12 +99,10 @@ struct
let proc_throws pn = Dataflow.DontKnow let proc_throws pn = Dataflow.DontKnow
end) in end) in
if Cfg.Procdesc.is_defined pdesc then let transitions = DFAllocCheck.run pdesc None in
let transitions = DFAllocCheck.run pdesc None in match transitions (Cfg.Procdesc.get_exit_node pdesc) with
match transitions (Cfg.Procdesc.get_exit_node pdesc) with | DFAllocCheck.Transition (loc, _, _) -> loc
| DFAllocCheck.Transition (loc, _, _) -> loc | DFAllocCheck.Dead_state -> None
| DFAllocCheck.Dead_state -> None
else None
(** Check repeated calls to the same procedure. *) (** Check repeated calls to the same procedure. *)
let check_instr get_proc_desc curr_pname curr_pdesc node extension instr normalized_etl = let check_instr get_proc_desc curr_pname curr_pdesc node extension instr normalized_etl =
@ -127,11 +125,11 @@ struct
normalized_etl, normalized_etl,
loc, loc,
call_flags) in call_flags) in
let report callee_pdesc = let report proc_desc =
match get_old_call instr_normalized_args extension with match get_old_call instr_normalized_args extension with
| Some (Sil.Call (_, _, _, loc_old, _)) -> | Some (Sil.Call (_, _, _, loc_old, _)) ->
begin begin
match proc_performs_allocation callee_pdesc AllPaths with match proc_performs_allocation proc_desc AllPaths with
| Some alloc_loc -> | Some alloc_loc ->
let description = let description =
Printf.sprintf "call to %s seen before on line %d (may allocate at %s:%n)" Printf.sprintf "call to %s seen before on line %d (may allocate at %s:%n)"
@ -147,7 +145,9 @@ struct
let () = match get_proc_desc callee_pname with let () = match get_proc_desc callee_pname with
| None -> () | None -> ()
| Some callee_pdesc -> report callee_pdesc in | Some proc_desc ->
if Cfg.Procdesc.is_defined proc_desc
then report proc_desc in
add_call instr_normalized_args extension add_call instr_normalized_args extension
| _ -> extension | _ -> extension

54
infer/src/checkers/typeCheck.ml
Unescape View File

@ -365,9 +365,10 @@ let typecheck_instr ext calls_this checks (node: Cfg.Node.t) idenv get_proc_desc
then calls_this := true in then calls_this := true in
(* Drops hidden and synthetic parameters which we do not check in a call. *) (* Drops hidden and synthetic parameters which we do not check in a call. *)
let drop_unchecked_params calls_this pdesc pname params = let drop_unchecked_params calls_this proc_attributes params =
let pname = proc_attributes.ProcAttributes.proc_name in
if Procname.is_constructor pname then if Procname.is_constructor pname then
match PatternMatch.get_this_type pdesc with match PatternMatch.get_this_type proc_attributes with
| Some this_type -> | Some this_type ->
begin begin
constructor_check_calls_this calls_this pname; constructor_check_calls_this calls_this pname;
@ -379,11 +380,11 @@ let typecheck_instr ext calls_this checks (node: Cfg.Node.t) idenv get_proc_desc
let rec drop_n_args ntl = match ntl with let rec drop_n_args ntl = match ntl with
| fp:: tail when is_hidden_parameter fp -> 1 + drop_n_args tail | fp:: tail when is_hidden_parameter fp -> 1 + drop_n_args tail
| _ -> 0 in | _ -> 0 in
let n = drop_n_args (Cfg.Procdesc.get_formals pdesc) in let n = drop_n_args proc_attributes.ProcAttributes.formals in
let visible_params = list_drop_first n params in let visible_params = list_drop_first n params in
(* Drop the trailing hidden parameter if the constructor is synthetic. *) (* Drop the trailing hidden parameter if the constructor is synthetic. *)
if (Cfg.Procdesc.get_attributes pdesc).ProcAttributes.is_synthetic_method then if proc_attributes.ProcAttributes.is_synthetic_method then
list_drop_last 1 visible_params list_drop_last 1 visible_params
else else
visible_params visible_params
@ -393,9 +394,9 @@ let typecheck_instr ext calls_this checks (node: Cfg.Node.t) idenv get_proc_desc
params in params in
(* Drop parameters from the signature which we do not check in a call. *) (* Drop parameters from the signature which we do not check in a call. *)
let drop_unchecked_signature_params pdesc pname annotated_signature = let drop_unchecked_signature_params proc_attributes annotated_signature =
if Procname.is_constructor pname && if Procname.is_constructor (proc_attributes.ProcAttributes.proc_name) &&
(Cfg.Procdesc.get_attributes pdesc).ProcAttributes.is_synthetic_method then proc_attributes.ProcAttributes.is_synthetic_method then
list_drop_last 1 annotated_signature.Annotations.params list_drop_last 1 annotated_signature.Annotations.params
else else
annotated_signature.Annotations.params in annotated_signature.Annotations.params in
@ -532,12 +533,14 @@ let typecheck_instr ext calls_this checks (node: Cfg.Node.t) idenv get_proc_desc
typestate (* skip othe builtins *) typestate (* skip othe builtins *)
| Sil.Call (ret_ids, Sil.Const (Sil.Cfun callee_pname), _etl, loc, cflags) | Sil.Call (ret_ids, Sil.Const (Sil.Cfun callee_pname), _etl, loc, cflags)
when get_proc_desc callee_pname <> None -> when get_proc_desc callee_pname <> None ->
let callee_pdesc = match get_proc_desc callee_pname with let callee_attributes =
| Some callee_pdesc -> callee_pdesc match get_proc_desc callee_pname with
| Some pdesc ->
Specs.pdesc_resolve_attributes pdesc
| None -> assert false in | None -> assert false in
let callee_loc = Cfg.Procdesc.get_loc callee_pdesc in let callee_loc = callee_attributes.ProcAttributes.loc in
let etl = drop_unchecked_params calls_this callee_pdesc callee_pname _etl in let etl = drop_unchecked_params calls_this callee_attributes _etl in
let call_params, typestate1 = let call_params, typestate1 =
let handle_et (e1, t1) (etl1, typestate1) = let handle_et (e1, t1) (etl1, typestate1) =
typecheck_expr_for_errors typestate e1 loc; typecheck_expr_for_errors typestate e1 loc;
@ -545,11 +548,10 @@ let typecheck_instr ext calls_this checks (node: Cfg.Node.t) idenv get_proc_desc
(((e1, e2), t1) :: etl1), typestate2 in (((e1, e2), t1) :: etl1), typestate2 in
list_fold_right handle_et etl ([], typestate) in list_fold_right handle_et etl ([], typestate) in
let annotated_signature = Models.get_annotated_signature callee_pdesc callee_pname in let annotated_signature =
let signature_params = drop_unchecked_signature_params Models.get_modelled_annotated_signature callee_attributes in
callee_pdesc let signature_params =
callee_pname drop_unchecked_signature_params callee_attributes annotated_signature in
annotated_signature in
let is_anonymous_inner_class_constructor = let is_anonymous_inner_class_constructor =
Procname.java_is_anonymous_inner_class_constructor callee_pname in Procname.java_is_anonymous_inner_class_constructor callee_pname in
@ -559,7 +561,7 @@ let typecheck_instr ext calls_this checks (node: Cfg.Node.t) idenv get_proc_desc
| [] -> typestate' | [] -> typestate'
| [id] -> | [id] ->
let (ia, ret_typ) = annotated_signature.Annotations.ret in let (ia, ret_typ) = annotated_signature.Annotations.ret in
let is_library = Specs.proc_is_library callee_pname callee_pdesc in let is_library = Specs.proc_is_library callee_attributes in
let origin = TypeOrigin.Proc (callee_pname, loc', annotated_signature, is_library) in let origin = TypeOrigin.Proc (callee_pname, loc', annotated_signature, is_library) in
TypeState.add_id TypeState.add_id
id id
@ -692,7 +694,7 @@ let typecheck_instr ext calls_this checks (node: Cfg.Node.t) idenv get_proc_desc
begin begin
let unique_id = Procname.to_unique_id callee_pname in let unique_id = Procname.to_unique_id callee_pname in
let classification = let classification =
EradicateChecks.classify_procedure callee_pname callee_pdesc in EradicateChecks.classify_procedure callee_attributes in
L.stdout " %s unique id: %s@." classification unique_id L.stdout " %s unique id: %s@." classification unique_id
end; end;
if cflags.Sil.cf_virtual && checks.eradicate then if cflags.Sil.cf_virtual && checks.eradicate then
@ -714,8 +716,7 @@ let typecheck_instr ext calls_this checks (node: Cfg.Node.t) idenv get_proc_desc
curr_pname curr_pname
node node
typestate1 typestate1
callee_pname callee_attributes
callee_pdesc
signature_params signature_params
call_params call_params
loc loc
@ -943,13 +944,14 @@ let typecheck_node
let typestates_exn = ref [] in let typestates_exn = ref [] in
let handle_exceptions typestate instr = match instr with let handle_exceptions typestate instr = match instr with
| Sil.Call (_, Sil.Const (Sil.Cfun callee_pname), _, _, _) -> | Sil.Call (_, Sil.Const (Sil.Cfun callee_pname), _, _, _) ->
let callee_attributes_opt =
Specs.proc_resolve_attributes get_proc_desc callee_pname in
(* check if the call might throw an exception *) (* check if the call might throw an exception *)
let exceptions = let has_exceptions = match callee_attributes_opt with
match get_proc_desc callee_pname with | Some callee_attributes ->
| Some callee_pdesc -> callee_attributes.ProcAttributes.exceptions <> []
(Specs.proc_get_attributes callee_pname callee_pdesc).ProcAttributes.exceptions | None -> false in
| None -> [] in if has_exceptions then
if exceptions <> [] then
typestates_exn := typestate :: !typestates_exn typestates_exn := typestate :: !typestates_exn
| Sil.Set (Sil.Lvar pv, _, _, _) when | Sil.Set (Sil.Lvar pv, _, _, _) when
Sil.pvar_is_return pv && Sil.pvar_is_return pv &&

Write Preview
Loading…
Cancel
Save