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

SymExec free of SummaryReporting

Browse Source 
Summary: progress

Reviewed By: dulmarod

Differential Revision: D21261637

fbshipit-source-id: 132375f66
master
Jules Villard 5 years ago committed by Facebook GitHub Bot
parent a0b237fe06
commit eb336fc4b7
3 changed files with 104 additions and 116 deletions
Show Stats Download Patch File Download Diff File

130
infer/src/biabduction/BuiltinDefn.ml
Unescape View File

@ -53,9 +53,8 @@ let return_result tenv e prop (ret_id, _) = Prop.conjoin_eq tenv e (Exp.Var ret_
(* Add an array of typ pointed to by lexp to prop_ if it doesn't already exist *) (* Add an array of typ pointed to by lexp to prop_ if it doesn't already exist *)
(* Return the new prop and the array length *) (* Return the new prop and the array length *)
(* Return None if it fails to add the array *) (* Return None if it fails to add the array *)
let add_array_to_prop tenv pdesc prop_ lexp typ = let add_array_to_prop ({InterproceduralAnalysis.tenv; _} as analysis_data) prop_ lexp typ =
let pname = Procdesc.get_proc_name pdesc in let n_lexp, prop = check_arith_norm_exp analysis_data lexp prop_ in
let n_lexp, prop = check_arith_norm_exp tenv pname lexp prop_ in
let hpred_opt = let hpred_opt =
List.find List.find
~f:(function Predicates.Hpointsto (e, _, _) -> Exp.equal e n_lexp | _ -> false) ~f:(function Predicates.Hpointsto (e, _, _) -> Exp.equal e n_lexp | _ -> false)
@ -85,11 +84,10 @@ let add_array_to_prop tenv pdesc prop_ lexp typ =
(* Add an array in prop if it is not allocated.*) (* Add an array in prop if it is not allocated.*)
let execute___require_allocated_array {Builtin.analysis_data= {proc_desc; tenv}; prop_; path; args} let execute___require_allocated_array {Builtin.analysis_data; prop_; path; args} : Builtin.ret_typ =
: Builtin.ret_typ =
match args with match args with
| [(lexp, typ)] -> ( | [(lexp, typ)] -> (
match add_array_to_prop tenv proc_desc prop_ lexp typ with match add_array_to_prop analysis_data prop_ lexp typ with
| None -> | None ->
[] []
| Some (_, prop) -> | Some (_, prop) ->
@ -99,10 +97,11 @@ let execute___require_allocated_array {Builtin.analysis_data= {proc_desc; tenv};
let execute___get_array_length let execute___get_array_length
{Builtin.analysis_data= {proc_desc; tenv}; prop_; path; ret_id_typ; args} : Builtin.ret_typ = {Builtin.analysis_data= {tenv; _} as analysis_data; prop_; path; ret_id_typ; args} :
Builtin.ret_typ =
match args with match args with
| [(lexp, typ)] -> ( | [(lexp, typ)] -> (
match add_array_to_prop tenv proc_desc prop_ lexp typ with match add_array_to_prop analysis_data prop_ lexp typ with
| None -> | None ->
[] []
| Some (len, prop) -> | Some (len, prop) ->
@ -111,18 +110,17 @@ let execute___get_array_length
raise (Exceptions.Wrong_argument_number __POS__) raise (Exceptions.Wrong_argument_number __POS__)
let execute___set_array_length {Builtin.analysis_data= {proc_desc; tenv}; prop_; path; args} : let execute___set_array_length {Builtin.analysis_data= {tenv; _} as analysis_data; prop_; path; args}
Builtin.ret_typ = : Builtin.ret_typ =
match args with match args with
| [(lexp, typ); (len, _)] -> ( | [(lexp, typ); (len, _)] -> (
match add_array_to_prop tenv proc_desc prop_ lexp typ with match add_array_to_prop analysis_data prop_ lexp typ with
| None -> | None ->
[] []
| Some (_, prop_a) -> ( | Some (_, prop_a) -> (
(* Invariant: prop_a has an array pointed to by lexp *) (* Invariant: prop_a has an array pointed to by lexp *)
let pname = Procdesc.get_proc_name proc_desc in let n_lexp, prop__ = check_arith_norm_exp analysis_data lexp prop_a in
let n_lexp, prop__ = check_arith_norm_exp tenv pname lexp prop_a in let n_len, prop = check_arith_norm_exp analysis_data len prop__ in
let n_len, prop = check_arith_norm_exp tenv pname len prop__ in
let hpred, sigma' = let hpred, sigma' =
List.partition_tf List.partition_tf
~f:(function Predicates.Hpointsto (e, _, _) -> Exp.equal e n_lexp | _ -> false) ~f:(function Predicates.Hpointsto (e, _, _) -> Exp.equal e n_lexp | _ -> false)
@ -140,12 +138,10 @@ let execute___set_array_length {Builtin.analysis_data= {proc_desc; tenv}; prop_;
raise (Exceptions.Wrong_argument_number __POS__) raise (Exceptions.Wrong_argument_number __POS__)
let execute___print_value {Builtin.analysis_data= {proc_desc; tenv}; prop_; path; args} : let execute___print_value {Builtin.analysis_data; prop_; path; args} : Builtin.ret_typ =
Builtin.ret_typ =
L.(debug Analysis Medium) "__print_value: " ; L.(debug Analysis Medium) "__print_value: " ;
let pname = Procdesc.get_proc_name proc_desc in
let do_arg (lexp, _) = let do_arg (lexp, _) =
let n_lexp, _ = check_arith_norm_exp tenv pname lexp prop_ in let n_lexp, _ = check_arith_norm_exp analysis_data lexp prop_ in
L.(debug Analysis Medium) "%a " Exp.pp n_lexp L.(debug Analysis Medium) "%a " Exp.pp n_lexp
in in
List.iter ~f:do_arg args ; List.iter ~f:do_arg args ;
@ -213,12 +209,12 @@ let create_type tenv n_lexp typ prop =
else null_case @ non_null_case else null_case @ non_null_case
let execute___get_type_of {Builtin.analysis_data= {proc_desc; tenv}; prop_; path; ret_id_typ; args} let execute___get_type_of
: Builtin.ret_typ = {Builtin.analysis_data= {tenv; _} as analysis_data; prop_; path; ret_id_typ; args} :
Builtin.ret_typ =
match args with match args with
| [(lexp, typ)] -> | [(lexp, typ)] ->
let pname = Procdesc.get_proc_name proc_desc in let n_lexp, prop = check_arith_norm_exp analysis_data lexp prop_ in
let n_lexp, prop = check_arith_norm_exp tenv pname lexp prop_ 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 =
let hpred_opt = let hpred_opt =
@ -261,12 +257,12 @@ let replace_ptsto_texp tenv prop root_e texp =
let execute___instanceof_cast ~instof let execute___instanceof_cast ~instof
{Builtin.analysis_data= {proc_desc; tenv}; prop_; path; ret_id_typ; args} : Builtin.ret_typ = {Builtin.analysis_data= {tenv; _} as analysis_data; prop_; path; ret_id_typ; args} :
Builtin.ret_typ =
match args with match args with
| [(val1_, typ1); (texp2_, _)] -> | [(val1_, typ1); (texp2_, _)] ->
let pname = Procdesc.get_proc_name proc_desc in let val1, prop__ = check_arith_norm_exp analysis_data val1_ prop_ in
let val1, prop__ = check_arith_norm_exp tenv pname val1_ prop_ in let texp2, prop = check_arith_norm_exp analysis_data texp2_ prop__ in
let texp2, prop = check_arith_norm_exp tenv pname texp2_ prop__ in
let is_cast_to_reference = let is_cast_to_reference =
match typ1.desc with Typ.Tptr (_, Typ.Pk_reference) -> true | _ -> false match typ1.desc with Typ.Tptr (_, Typ.Pk_reference) -> true | _ -> false
in in
@ -363,12 +359,11 @@ let set_resource_attribute tenv prop path n_lexp loc ra_res =
(** Set the attibute of the value as file *) (** Set the attibute of the value as file *)
let execute___set_file_attribute {Builtin.analysis_data= {proc_desc; tenv}; prop_; path; args; loc} let execute___set_file_attribute
: Builtin.ret_typ = {Builtin.analysis_data= {tenv; _} as analysis_data; prop_; path; args; loc} : Builtin.ret_typ =
match args with match args with
| [(lexp, _)] -> | [(lexp, _)] ->
let pname = Procdesc.get_proc_name proc_desc in let n_lexp, prop = check_arith_norm_exp analysis_data lexp prop_ in
let n_lexp, prop = check_arith_norm_exp tenv pname lexp prop_ in
set_resource_attribute tenv prop path n_lexp loc PredSymb.Rfile set_resource_attribute tenv prop path n_lexp loc PredSymb.Rfile
| _ -> | _ ->
raise (Exceptions.Wrong_argument_number __POS__) raise (Exceptions.Wrong_argument_number __POS__)
@ -377,56 +372,50 @@ let execute___set_file_attribute {Builtin.analysis_data= {proc_desc; tenv}; prop
(** Set the resource attribute of the first real argument of method as ignore, the first argument is (** Set the resource attribute of the first real argument of method as ignore, the first argument is
assumed to be "this" *) assumed to be "this" *)
let execute___method_set_ignore_attribute let execute___method_set_ignore_attribute
{Builtin.analysis_data= {proc_desc; tenv}; prop_; path; args; loc} : Builtin.ret_typ = {Builtin.analysis_data= {tenv; _} as analysis_data; prop_; path; args; loc} : Builtin.ret_typ =
match args with match args with
| [_; (lexp, _)] -> | [_; (lexp, _)] ->
let pname = Procdesc.get_proc_name proc_desc in let n_lexp, prop = check_arith_norm_exp analysis_data lexp prop_ in
let n_lexp, prop = check_arith_norm_exp tenv pname lexp prop_ in
set_resource_attribute tenv prop path n_lexp loc PredSymb.Rignore set_resource_attribute tenv prop path n_lexp loc PredSymb.Rignore
| _ -> | _ ->
raise (Exceptions.Wrong_argument_number __POS__) raise (Exceptions.Wrong_argument_number __POS__)
(** Set the attibute of the value as memory *) (** Set the attibute of the value as memory *)
let execute___set_mem_attribute {Builtin.analysis_data= {proc_desc; tenv}; prop_; path; args; loc} : let execute___set_mem_attribute
Builtin.ret_typ = {Builtin.analysis_data= {tenv; _} as analysis_data; prop_; path; args; loc} : Builtin.ret_typ =
match args with match args with
| [(lexp, _)] -> | [(lexp, _)] ->
let pname = Procdesc.get_proc_name proc_desc in let n_lexp, prop = check_arith_norm_exp analysis_data lexp prop_ in
let n_lexp, prop = check_arith_norm_exp tenv pname lexp prop_ in
set_resource_attribute tenv prop path n_lexp loc (PredSymb.Rmemory PredSymb.Mnew) set_resource_attribute tenv prop path n_lexp loc (PredSymb.Rmemory PredSymb.Mnew)
| _ -> | _ ->
raise (Exceptions.Wrong_argument_number __POS__) raise (Exceptions.Wrong_argument_number __POS__)
let set_attr tenv pdesc prop path exp attr = let set_attr ({InterproceduralAnalysis.tenv; _} as analysis_data) prop path exp attr =
let pname = Procdesc.get_proc_name pdesc in let n_lexp, prop = check_arith_norm_exp analysis_data exp prop in
let n_lexp, prop = check_arith_norm_exp tenv pname exp prop in
[(Attribute.add_or_replace tenv prop (Apred (attr, [n_lexp])), path)] [(Attribute.add_or_replace tenv prop (Apred (attr, [n_lexp])), path)]
let delete_attr tenv pdesc prop path exp attr = let delete_attr ({InterproceduralAnalysis.tenv; _} as analysis_data) prop path exp attr =
let pname = Procdesc.get_proc_name pdesc in let n_lexp, prop = check_arith_norm_exp analysis_data exp prop in
let n_lexp, prop = check_arith_norm_exp tenv pname exp prop in
[(Attribute.remove tenv prop (Apred (attr, [n_lexp])), path)] [(Attribute.remove tenv prop (Apred (attr, [n_lexp])), path)]
(** Set attibute att *) (** Set attibute att *)
let execute___set_attr attr {Builtin.analysis_data= {proc_desc; tenv}; prop_; path; args} : let execute___set_attr attr {Builtin.analysis_data; prop_; path; args} : Builtin.ret_typ =
Builtin.ret_typ =
match args with match args with
| [(lexp, _)] -> | [(lexp, _)] ->
set_attr tenv proc_desc prop_ path lexp attr set_attr analysis_data prop_ path lexp attr
| _ -> | _ ->
raise (Exceptions.Wrong_argument_number __POS__) raise (Exceptions.Wrong_argument_number __POS__)
(** Delete the locked attibute of the value*) (** Delete the locked attibute of the value*)
let execute___delete_locked_attribute {Builtin.analysis_data= {proc_desc; tenv}; prop_; path; args} let execute___delete_locked_attribute {Builtin.analysis_data; prop_; path; args} : Builtin.ret_typ =
: Builtin.ret_typ =
match args with match args with
| [(lexp, _)] -> | [(lexp, _)] ->
delete_attr tenv proc_desc prop_ path lexp PredSymb.Alocked delete_attr analysis_data prop_ path lexp PredSymb.Alocked
| _ -> | _ ->
raise (Exceptions.Wrong_argument_number __POS__) raise (Exceptions.Wrong_argument_number __POS__)
@ -500,12 +489,11 @@ let execute_free_nonzero_ mk ?(mark_as_freed = true)
let execute_free mk ?(mark_as_freed = true) let execute_free mk ?(mark_as_freed = true)
{Builtin.analysis_data= {proc_desc; tenv} as analysis_data; instr; prop_; path; args; loc} : {Builtin.analysis_data= {tenv; _} as analysis_data; instr; prop_; path; args; loc} :
Builtin.ret_typ = Builtin.ret_typ =
match args with match args with
| [(lexp, typ)] -> | [(lexp, typ)] ->
let pname = Procdesc.get_proc_name proc_desc in let n_lexp, prop = check_arith_norm_exp analysis_data lexp prop_ in
let n_lexp, prop = check_arith_norm_exp tenv pname lexp prop_ in
let prop_nonzero = let prop_nonzero =
(* case n_lexp!=0 *) (* case n_lexp!=0 *)
Propset.to_proplist (prune tenv ~positive:true n_lexp prop) Propset.to_proplist (prune tenv ~positive:true n_lexp prop)
@ -537,9 +525,8 @@ let execute_free mk ?(mark_as_freed = true)
let execute_free_cf mk = execute_free mk ~mark_as_freed:false let execute_free_cf mk = execute_free mk ~mark_as_freed:false
let execute_alloc mk can_return_null let execute_alloc mk can_return_null
{Builtin.analysis_data= {proc_desc; tenv}; prop_; path; ret_id_typ; args; loc} : Builtin.ret_typ {Builtin.analysis_data= {tenv; _} as analysis_data; prop_; path; ret_id_typ; args; loc} :
= Builtin.ret_typ =
let pname = Procdesc.get_proc_name proc_desc in
let rec evaluate_char_sizeof e = let rec evaluate_char_sizeof e =
match e with match e with
| Exp.Var _ -> | Exp.Var _ ->
@ -578,7 +565,7 @@ let execute_alloc mk can_return_null
in in
let ret_id = fst ret_id_typ in let ret_id = fst ret_id_typ in
let size_exp', prop = let size_exp', prop =
let n_size_exp, prop = check_arith_norm_exp tenv pname size_exp prop_ in let n_size_exp, prop = check_arith_norm_exp analysis_data size_exp prop_ 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 tenv prop n_size_exp', prop) (Prop.exp_normalize_prop tenv prop n_size_exp', prop)
in in
@ -611,16 +598,13 @@ let execute_alloc mk can_return_null
else [(prop_alloc, path)] else [(prop_alloc, path)]
let execute___cxx_typeid let execute___cxx_typeid ({Builtin.analysis_data; prop_; args; loc} as r) : Builtin.ret_typ =
({Builtin.analysis_data= {proc_desc; tenv} as analysis_data; prop_; args; loc} as r) :
Builtin.ret_typ =
match args with match args with
| type_info_exp :: rest -> ( | type_info_exp :: rest -> (
let res = execute_alloc PredSymb.Mnew false {r with args= [type_info_exp]} in let res = execute_alloc PredSymb.Mnew false {r with args= [type_info_exp]} in
match rest with match rest with
| [(field_exp, _); (lexp, typ_)] -> | [(field_exp, _); (lexp, typ_)] ->
let pname = Procdesc.get_proc_name proc_desc in let n_lexp, prop = check_arith_norm_exp analysis_data lexp prop_ in
let n_lexp, prop = check_arith_norm_exp tenv pname lexp prop_ in
let typ = let typ =
List.find List.find
~f:(function Predicates.Hpointsto (e, _, _) -> Exp.equal e n_lexp | _ -> false) ~f:(function Predicates.Hpointsto (e, _, _) -> Exp.equal e n_lexp | _ -> false)
@ -697,11 +681,11 @@ let execute_scan_function skip_n_arguments ({Builtin.args; ret_id_typ} as call_a
let execute__unwrap_exception let execute__unwrap_exception
{Builtin.analysis_data= {proc_desc; tenv}; prop_; path; ret_id_typ; args} : Builtin.ret_typ = {Builtin.analysis_data= {tenv; _} as analysis_data; prop_; path; ret_id_typ; args} :
Builtin.ret_typ =
match args with match args with
| [(ret_exn, _)] -> ( | [(ret_exn, _)] -> (
let pname = Procdesc.get_proc_name proc_desc in let n_ret_exn, prop = check_arith_norm_exp analysis_data ret_exn prop_ in
let n_ret_exn, prop = check_arith_norm_exp tenv pname ret_exn prop_ in
match n_ret_exn with match n_ret_exn with
| Exp.Exn exp -> | Exp.Exn exp ->
let prop_with_exn = return_result tenv exp prop ret_id_typ in let prop_with_exn = return_result tenv exp prop ret_id_typ in
@ -713,25 +697,25 @@ let execute__unwrap_exception
let execute_return_first_argument let execute_return_first_argument
{Builtin.analysis_data= {proc_desc; tenv}; prop_; path; ret_id_typ; args} : Builtin.ret_typ = {Builtin.analysis_data= {tenv; _} as analysis_data; prop_; path; ret_id_typ; args} :
Builtin.ret_typ =
match args with match args with
| (arg1_, _) :: _ -> | (arg1_, _) :: _ ->
let pname = Procdesc.get_proc_name proc_desc in let arg1, prop = check_arith_norm_exp analysis_data arg1_ prop_ in
let arg1, prop = check_arith_norm_exp tenv pname arg1_ prop_ in
let prop' = return_result tenv arg1 prop ret_id_typ in let prop' = return_result tenv arg1 prop ret_id_typ in
[(prop', path)] [(prop', path)]
| _ -> | _ ->
raise (Exceptions.Wrong_argument_number __POS__) raise (Exceptions.Wrong_argument_number __POS__)
let execute___split_get_nth {Builtin.analysis_data= {proc_desc; tenv}; prop_; path; ret_id_typ; args} let execute___split_get_nth
: Builtin.ret_typ = {Builtin.analysis_data= {tenv; _} as analysis_data; prop_; path; ret_id_typ; args} :
Builtin.ret_typ =
match args with match args with
| [(lexp1, _); (lexp2, _); (lexp3, _)] -> ( | [(lexp1, _); (lexp2, _); (lexp3, _)] -> (
let pname = Procdesc.get_proc_name proc_desc in let n_lexp1, prop__ = check_arith_norm_exp analysis_data lexp1 prop_ in
let n_lexp1, prop__ = check_arith_norm_exp tenv pname lexp1 prop_ in let n_lexp2, prop___ = check_arith_norm_exp analysis_data lexp2 prop__ in
let n_lexp2, prop___ = check_arith_norm_exp tenv pname lexp2 prop__ in let n_lexp3, prop = check_arith_norm_exp analysis_data lexp3 prop___ in
let n_lexp3, prop = check_arith_norm_exp tenv pname lexp3 prop___ in
match (n_lexp1, n_lexp2, n_lexp3) with match (n_lexp1, n_lexp2, n_lexp3) with
| Exp.Const (Const.Cstr str1), Exp.Const (Const.Cstr str2), Exp.Const (Const.Cint n_sil) -> ( | Exp.Const (Const.Cstr str1), Exp.Const (Const.Cstr str2), Exp.Const (Const.Cint n_sil) -> (
let n = IntLit.to_int_exn n_sil in let n = IntLit.to_int_exn n_sil in

85
infer/src/biabduction/SymExec.ml
Unescape View File

@ -402,7 +402,7 @@ let check_constant_string_dereference lexp =
(** Normalize an expression and check for arithmetic problems *) (** Normalize an expression and check for arithmetic problems *)
let check_arith_norm_exp tenv pname exp prop = let check_arith_norm_exp {InterproceduralAnalysis.proc_desc; err_log; tenv} exp prop =
match Attribute.find_arithmetic_problem tenv (State.get_path_pos ()) prop exp with match Attribute.find_arithmetic_problem tenv (State.get_path_pos ()) prop exp with
| Some (Attribute.Div0 div), prop' -> | Some (Attribute.Div0 div), prop' ->
let desc = let desc =
@ -410,7 +410,8 @@ let check_arith_norm_exp tenv pname exp prop =
(AnalysisState.get_loc_exn ()) (AnalysisState.get_loc_exn ())
in in
let exn = Exceptions.Divide_by_zero (desc, __POS__) in let exn = Exceptions.Divide_by_zero (desc, __POS__) in
SummaryReporting.log_issue_deprecated_using_state Exceptions.Warning pname exn ; let attrs = Procdesc.get_attributes proc_desc in
BiabductionReporting.log_issue_deprecated_using_state attrs err_log Exceptions.Warning exn ;
(Prop.exp_normalize_prop tenv prop exp, prop') (Prop.exp_normalize_prop tenv prop exp, prop')
| Some (Attribute.UminusUnsigned (e, typ)), prop' -> | Some (Attribute.UminusUnsigned (e, typ)), prop' ->
let desc = let desc =
@ -418,14 +419,15 @@ let check_arith_norm_exp tenv pname exp prop =
(AnalysisState.get_node_exn ()) (AnalysisState.get_loc_exn ()) (AnalysisState.get_node_exn ()) (AnalysisState.get_loc_exn ())
in in
let exn = Exceptions.Unary_minus_applied_to_unsigned_expression (desc, __POS__) in let exn = Exceptions.Unary_minus_applied_to_unsigned_expression (desc, __POS__) in
SummaryReporting.log_issue_deprecated_using_state Exceptions.Warning pname exn ; let attrs = Procdesc.get_attributes proc_desc in
BiabductionReporting.log_issue_deprecated_using_state attrs err_log Exceptions.Warning exn ;
(Prop.exp_normalize_prop tenv prop exp, prop') (Prop.exp_normalize_prop tenv prop exp, prop')
| None, prop' -> | None, prop' ->
(Prop.exp_normalize_prop tenv prop exp, prop') (Prop.exp_normalize_prop tenv prop exp, prop')
(** Check if [cond] is testing for NULL a pointer already dereferenced *) (** Check if [cond] is testing for NULL a pointer already dereferenced *)
let check_already_dereferenced tenv pname cond prop = let check_already_dereferenced {InterproceduralAnalysis.proc_desc; err_log; tenv} cond prop =
let find_hpred lhs = let find_hpred lhs =
List.find List.find
~f:(function Predicates.Hpointsto (e, _, _) -> Exp.equal e lhs | _ -> false) ~f:(function Predicates.Hpointsto (e, _, _) -> Exp.equal e lhs | _ -> false)
@ -476,7 +478,8 @@ let check_already_dereferenced tenv pname cond prop =
(AnalysisState.get_node_exn ()) n (AnalysisState.get_loc_exn ()) (AnalysisState.get_node_exn ()) n (AnalysisState.get_loc_exn ())
in in
let exn = Exceptions.Null_test_after_dereference (desc, __POS__) in let exn = Exceptions.Null_test_after_dereference (desc, __POS__) in
SummaryReporting.log_issue_deprecated_using_state Exceptions.Warning pname exn let attrs = Procdesc.get_attributes proc_desc in
BiabductionReporting.log_issue_deprecated_using_state attrs err_log Exceptions.Warning exn
| None -> | None ->
() ()
@ -860,9 +863,9 @@ let handle_objc_instance_method_call actual_pars pre tenv ret_id pdesc callee_pn
handle_objc_instance_method_call_or_skip pdesc tenv actual_pars path callee_pname pre ret_id res handle_objc_instance_method_call_or_skip pdesc tenv actual_pars path callee_pname pre ret_id res
let normalize_params tenv pdesc prop actual_params = let normalize_params analysis_data prop actual_params =
let norm_arg (p, args) (e, t) = let norm_arg (p, args) (e, t) =
let e', p' = check_arith_norm_exp tenv pdesc e p in let e', p' = check_arith_norm_exp analysis_data e p in
(p', (e', t) :: args) (p', (e', t) :: args)
in in
let prop, args = List.fold ~f:norm_arg ~init:(prop, []) actual_params in let prop, args = List.fold ~f:norm_arg ~init:(prop, []) actual_params in
@ -958,16 +961,15 @@ let add_constraints_on_retval tenv pdesc prop ret_exp ~has_nonnull_annot typ cal
else add_ret_non_null ret_exp typ prop else add_ret_non_null ret_exp typ prop
let execute_load ?(report_deref_errors = true) pname let execute_load ?(report_deref_errors = true) ({InterproceduralAnalysis.tenv; _} as analysis_data)
({InterproceduralAnalysis.proc_desc= pdesc; tenv; _} as analysis_data) id rhs_exp typ loc prop_ id rhs_exp typ loc prop_ =
=
let execute_load_ acc_in iter = let execute_load_ acc_in iter =
let iter_ren = Prop.prop_iter_make_id_primed tenv id iter in let iter_ren = Prop.prop_iter_make_id_primed tenv id iter in
let prop_ren = Prop.prop_iter_to_prop tenv iter_ren in let prop_ren = Prop.prop_iter_to_prop tenv iter_ren in
match Prop.prop_iter_current tenv iter_ren with match Prop.prop_iter_current tenv iter_ren with
| Predicates.Hpointsto (lexp, strexp, Exp.Sizeof sizeof_data), offlist -> ( | Predicates.Hpointsto (lexp, strexp, Exp.Sizeof sizeof_data), offlist -> (
let contents, new_ptsto, pred_insts_op, lookup_uninitialized = let contents, new_ptsto, pred_insts_op, lookup_uninitialized =
ptsto_lookup pdesc tenv prop_ren (lexp, strexp, sizeof_data) offlist id ptsto_lookup analysis_data tenv prop_ren (lexp, strexp, sizeof_data) offlist id
in in
let is_union_field = let is_union_field =
match rhs_exp with match rhs_exp with
@ -1005,7 +1007,7 @@ let execute_load ?(report_deref_errors = true) pname
assert false assert false
in in
try try
let n_rhs_exp, prop = check_arith_norm_exp tenv pname rhs_exp prop_ in let n_rhs_exp, prop = check_arith_norm_exp analysis_data rhs_exp prop_ in
let n_rhs_exp' = Prop.exp_collapse_consecutive_indices_prop typ n_rhs_exp in let n_rhs_exp' = Prop.exp_collapse_consecutive_indices_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 ->
@ -1036,8 +1038,8 @@ let load_ret_annots pname =
Annot.Item.empty Annot.Item.empty
let execute_store ?(report_deref_errors = true) pname let execute_store ?(report_deref_errors = true) ({InterproceduralAnalysis.tenv; _} as analysis_data)
({InterproceduralAnalysis.tenv; _} as analysis_data) lhs_exp typ rhs_exp loc prop_ = lhs_exp typ rhs_exp loc prop_ =
let execute_store_ analysis_data tenv rhs_exp acc_in iter = let execute_store_ analysis_data tenv rhs_exp acc_in iter =
let lexp, strexp, sizeof, offlist = let lexp, strexp, sizeof, offlist =
match Prop.prop_iter_current tenv iter with match Prop.prop_iter_current tenv iter with
@ -1063,8 +1065,8 @@ let execute_store ?(report_deref_errors = true) pname
List.fold ~f:update ~init:acc_in pred_insts List.fold ~f:update ~init:acc_in pred_insts
in in
try try
let n_lhs_exp, prop_' = check_arith_norm_exp tenv pname lhs_exp prop_ in let n_lhs_exp, prop_' = check_arith_norm_exp analysis_data lhs_exp prop_ in
let n_rhs_exp, prop = check_arith_norm_exp tenv pname rhs_exp prop_' in let n_rhs_exp, prop = check_arith_norm_exp analysis_data rhs_exp prop_' in
let prop = Attribute.replace_objc_null tenv prop n_lhs_exp n_rhs_exp in let prop = Attribute.replace_objc_null tenv prop n_lhs_exp n_rhs_exp in
let n_lhs_exp' = Prop.exp_collapse_consecutive_indices_prop typ n_lhs_exp in let n_lhs_exp' = Prop.exp_collapse_consecutive_indices_prop typ n_lhs_exp in
let iter_list = let iter_list =
@ -1171,8 +1173,9 @@ let declare_locals_and_ret tenv pdesc (prop_ : Prop.normal Prop.t) =
(** Execute [instr] with a symbolic heap [prop].*) (** Execute [instr] with a symbolic heap [prop].*)
let rec sym_exec let rec sym_exec
({InterproceduralAnalysis.proc_desc= current_pdesc; analyze_dependency; tenv} as analysis_data) ( {InterproceduralAnalysis.proc_desc= current_pdesc; analyze_dependency; err_log; tenv} as
instr_ (prop_ : Prop.normal Prop.t) path : (Prop.normal Prop.t * Paths.Path.t) list = analysis_data ) instr_ (prop_ : Prop.normal Prop.t) path :
(Prop.normal Prop.t * Paths.Path.t) list =
let current_pname = Procdesc.get_proc_name current_pdesc in let current_pname = Procdesc.get_proc_name current_pdesc in
AnalysisState.set_instr instr_ ; AnalysisState.set_instr instr_ ;
(* mark instruction last seen *) (* mark instruction last seen *)
@ -1206,7 +1209,8 @@ let rec sym_exec
ret_id_typ ret_typ actual_args = ret_id_typ ret_typ actual_args =
let skip_res () = let skip_res () =
let exn = Exceptions.Skip_function (Localise.desc_skip_function callee_pname) in let exn = Exceptions.Skip_function (Localise.desc_skip_function callee_pname) in
SummaryReporting.log_issue_deprecated_using_state Exceptions.Info current_pname exn ; let attrs = Procdesc.get_attributes current_pdesc in
BiabductionReporting.log_issue_deprecated_using_state attrs err_log Exceptions.Info exn ;
L.d_printfln "Skipping function '%a': %s" Procname.pp callee_pname reason ; L.d_printfln "Skipping function '%a': %s" Procname.pp callee_pname reason ;
unknown_or_scan_call ~is_scan:false ~reason ret_typ ret_annots unknown_or_scan_call ~is_scan:false ~reason ret_typ ret_annots
{ Builtin.instr { Builtin.instr
@ -1228,9 +1232,9 @@ let rec sym_exec
in in
match instr with match instr with
| Sil.Load {id; e= rhs_exp; root_typ= typ; loc} -> | Sil.Load {id; e= rhs_exp; root_typ= typ; loc} ->
execute_load current_pname analysis_data id rhs_exp typ loc prop_ |> ret_old_path execute_load analysis_data id rhs_exp typ loc prop_ |> ret_old_path
| Sil.Store {e1= lhs_exp; root_typ= typ; e2= rhs_exp; loc} -> | Sil.Store {e1= lhs_exp; root_typ= typ; e2= rhs_exp; loc} ->
execute_store current_pname analysis_data lhs_exp typ rhs_exp loc prop_ |> ret_old_path execute_store analysis_data lhs_exp typ rhs_exp loc prop_ |> ret_old_path
| Sil.Prune (cond, loc, true_branch, ik) -> | Sil.Prune (cond, loc, true_branch, ik) ->
let prop__ = Attribute.nullify_exp_with_objc_null tenv prop_ cond in let prop__ = Attribute.nullify_exp_with_objc_null tenv prop_ cond in
let check_condition_always_true_false () = let check_condition_always_true_false () =
@ -1257,14 +1261,16 @@ let rec sym_exec
let exn = let exn =
Exceptions.Condition_always_true_false (desc, not (IntLit.iszero i), __POS__) Exceptions.Condition_always_true_false (desc, not (IntLit.iszero i), __POS__)
in in
SummaryReporting.log_issue_deprecated_using_state Exceptions.Warning current_pname exn let attrs = Procdesc.get_attributes current_pdesc in
BiabductionReporting.log_issue_deprecated_using_state attrs err_log Exceptions.Warning
exn
| _ -> | _ ->
() ()
in in
if not (Procname.is_java current_pname) then if not (Procname.is_java current_pname) then
check_already_dereferenced tenv current_pname cond prop__ ; check_already_dereferenced analysis_data cond prop__ ;
check_condition_always_true_false () ; check_condition_always_true_false () ;
let n_cond, prop = check_arith_norm_exp tenv current_pname cond prop__ in let n_cond, prop = check_arith_norm_exp analysis_data cond prop__ in
ret_old_path (Propset.to_proplist (prune tenv ~positive:true n_cond prop)) ret_old_path (Propset.to_proplist (prune tenv ~positive:true n_cond prop))
| Sil.Call (ret_id_typ, Exp.Const (Const.Cfun callee_pname), actual_params, loc, call_flags) -> ( | Sil.Call (ret_id_typ, Exp.Const (Const.Cfun callee_pname), actual_params, loc, call_flags) -> (
match Builtin.get callee_pname with match Builtin.get callee_pname with
@ -1273,7 +1279,7 @@ let rec sym_exec
| None -> ( | None -> (
match callee_pname with match callee_pname with
| Java callee_pname_java when Config.dynamic_dispatch -> ( | Java callee_pname_java when Config.dynamic_dispatch -> (
let norm_prop, norm_args' = normalize_params tenv current_pname prop_ actual_params in let norm_prop, norm_args' = normalize_params analysis_data prop_ actual_params in
let norm_args = call_constructor_url_update_args callee_pname norm_args' in let norm_args = call_constructor_url_update_args callee_pname norm_args' in
let exec_skip_call ~reason skipped_pname ret_annots ret_type = let exec_skip_call ~reason skipped_pname ret_annots ret_type =
skip_call ~reason norm_prop path skipped_pname ret_annots loc ret_id_typ ret_type skip_call ~reason norm_prop path skipped_pname ret_annots loc ret_id_typ ret_type
@ -1298,7 +1304,7 @@ let rec sym_exec
exec_skip_call ~reason resolved_pname ret_annots proc_attrs.ProcAttributes.ret_type exec_skip_call ~reason resolved_pname ret_annots proc_attrs.ProcAttributes.ret_type
) ) ) )
| Java callee_pname_java -> | Java callee_pname_java ->
let norm_prop, norm_args = normalize_params tenv current_pname prop_ actual_params in let norm_prop, norm_args = normalize_params analysis_data prop_ actual_params in
let url_handled_args = call_constructor_url_update_args callee_pname norm_args in let url_handled_args = call_constructor_url_update_args callee_pname norm_args in
let resolved_pnames = let resolved_pnames =
resolve_virtual_pname tenv norm_prop url_handled_args callee_pname call_flags resolve_virtual_pname tenv norm_prop url_handled_args callee_pname call_flags
@ -1326,7 +1332,7 @@ let rec sym_exec
List.fold ~f:(fun acc pname -> exec_one_pname pname @ acc) ~init:[] resolved_pnames List.fold ~f:(fun acc pname -> exec_one_pname pname @ acc) ~init:[] resolved_pnames
| _ -> ( | _ -> (
(* Generic fun call with known name *) (* Generic fun call with known name *)
let prop_r, n_actual_params = normalize_params tenv current_pname prop_ actual_params in let prop_r, n_actual_params = normalize_params analysis_data prop_ actual_params in
(* method with block parameters *) (* method with block parameters *)
let with_block_parameters_summary_opt = let with_block_parameters_summary_opt =
if call_flags.CallFlags.cf_with_block_parameters then if call_flags.CallFlags.cf_with_block_parameters then
@ -1337,7 +1343,7 @@ let rec sym_exec
match with_block_parameters_summary_opt with match with_block_parameters_summary_opt with
| Some (resolved_summary, extended_actual_params) -> | Some (resolved_summary, extended_actual_params) ->
let prop_r, n_extended_actual_params = let prop_r, n_extended_actual_params =
normalize_params tenv current_pname prop_r extended_actual_params normalize_params analysis_data prop_r extended_actual_params
in in
Logging.d_strln "Calling method specialized with blocks... " ; Logging.d_strln "Calling method specialized with blocks... " ;
proc_call resolved_summary proc_call resolved_summary
@ -1416,7 +1422,7 @@ let rec sym_exec
List.concat_map ~f:do_call sentinel_result ) ) ) List.concat_map ~f:do_call sentinel_result ) ) )
| Sil.Call (ret_id_typ, fun_exp, actual_params, loc, call_flags) -> | Sil.Call (ret_id_typ, fun_exp, actual_params, loc, call_flags) ->
(* Call via function pointer *) (* Call via function pointer *)
let prop_r, n_actual_params = normalize_params tenv current_pname prop_ actual_params in let prop_r, n_actual_params = normalize_params analysis_data prop_ actual_params in
if if
call_flags.CallFlags.cf_is_objc_block call_flags.CallFlags.cf_is_objc_block
&& not (Rearrange.is_only_pt_by_fld_or_param_nonnull current_pdesc tenv prop_r fun_exp) && not (Rearrange.is_only_pt_by_fld_or_param_nonnull current_pdesc tenv prop_r fun_exp)
@ -1730,7 +1736,7 @@ and check_variadic_sentinel_if_present ({Builtin.prop_; path; proc_name} as buil
and sym_exec_objc_getter field ret_typ ret_id ({InterproceduralAnalysis.tenv; _} as analysis_data) and sym_exec_objc_getter field ret_typ ret_id ({InterproceduralAnalysis.tenv; _} as analysis_data)
pname loc args prop = loc args prop =
let field_name, _, _ = field in let field_name, _, _ = field in
L.d_printfln "No custom getter found. Executing the ObjC builtin getter with ivar %a." L.d_printfln "No custom getter found. Executing the ObjC builtin getter with ivar %a."
Fieldname.pp field_name ; Fieldname.pp field_name ;
@ -1740,14 +1746,13 @@ and sym_exec_objc_getter field ret_typ ret_id ({InterproceduralAnalysis.tenv; _}
| {desc= Tptr (({desc= Tstruct struct_name} as typ), _)} ) ) ] -> | {desc= Tptr (({desc= Tstruct struct_name} as typ), _)} ) ) ] ->
Tenv.add_field tenv struct_name field ; Tenv.add_field tenv struct_name field ;
let field_access_exp = Exp.Lfield (lexp, field_name, typ) in let field_access_exp = Exp.Lfield (lexp, field_name, typ) in
execute_load ~report_deref_errors:false pname analysis_data ret_id field_access_exp ret_typ execute_load ~report_deref_errors:false analysis_data ret_id field_access_exp ret_typ loc prop
loc prop
| _ -> | _ ->
raise (Exceptions.Wrong_argument_number __POS__) raise (Exceptions.Wrong_argument_number __POS__)
and sym_exec_objc_setter field _ _ ({InterproceduralAnalysis.tenv; _} as analysis_data) pname loc and sym_exec_objc_setter field _ _ ({InterproceduralAnalysis.tenv; _} as analysis_data) loc args
args prop = prop =
let field_name, _, _ = field in let field_name, _, _ = field in
L.d_printfln "No custom setter found. Executing the ObjC builtin setter with ivar %a." L.d_printfln "No custom setter found. Executing the ObjC builtin setter with ivar %a."
Fieldname.pp field_name ; Fieldname.pp field_name ;
@ -1758,15 +1763,13 @@ and sym_exec_objc_setter field _ _ ({InterproceduralAnalysis.tenv; _} as analysi
:: (lexp2, typ2) :: _ -> :: (lexp2, typ2) :: _ ->
Tenv.add_field tenv struct_name field ; Tenv.add_field tenv struct_name field ;
let field_access_exp = Exp.Lfield (lexp1, field_name, typ1) in let field_access_exp = Exp.Lfield (lexp1, field_name, typ1) in
execute_store ~report_deref_errors:false pname analysis_data field_access_exp typ2 lexp2 loc execute_store ~report_deref_errors:false analysis_data field_access_exp typ2 lexp2 loc prop
prop
| _ -> | _ ->
raise (Exceptions.Wrong_argument_number __POS__) raise (Exceptions.Wrong_argument_number __POS__)
and sym_exec_objc_accessor callee_pname property_accesor ret_typ ret_id and sym_exec_objc_accessor callee_pname property_accesor ret_typ ret_id analysis_data _ loc args
({InterproceduralAnalysis.proc_desc= pdesc} as analysis_data) _ loc args prop path : prop path : Builtin.ret_typ =
Builtin.ret_typ =
let f_accessor = let f_accessor =
match property_accesor with match property_accesor with
| ProcAttributes.Objc_getter field -> | ProcAttributes.Objc_getter field ->
@ -1776,15 +1779,13 @@ and sym_exec_objc_accessor callee_pname property_accesor ret_typ ret_id
in in
(* we want to execute in the context of the current procedure, not in the context of callee_pname, (* we want to execute in the context of the current procedure, not in the context of callee_pname,
since this is the procname of the setter/getter method *) since this is the procname of the setter/getter method *)
let cur_pname = Procdesc.get_proc_name pdesc in
let path_description = let path_description =
F.sprintf "Executing synthesized %s %s" F.sprintf "Executing synthesized %s %s"
(ProcAttributes.kind_of_objc_accessor_type property_accesor) (ProcAttributes.kind_of_objc_accessor_type property_accesor)
(Procname.to_simplified_string callee_pname) (Procname.to_simplified_string callee_pname)
in in
let path = Paths.Path.add_description path path_description in let path = Paths.Path.add_description path path_description in
f_accessor ret_typ ret_id analysis_data cur_pname loc args prop f_accessor ret_typ ret_id analysis_data loc args prop |> List.map ~f:(fun p -> (p, path))
|> List.map ~f:(fun p -> (p, path))
and sym_exec_alloc_model analysis_data pname ret_typ ret_id_typ loc prop path : Builtin.ret_typ = and sym_exec_alloc_model analysis_data pname ret_typ ret_id_typ loc prop path : Builtin.ret_typ =

5
infer/src/biabduction/SymExec.mli
Unescape View File

@ -41,7 +41,10 @@ val unknown_or_scan_call : is_scan:bool -> reason:string -> Typ.t -> Annot.Item.
val check_variadic_sentinel : ?fails_on_nil:bool -> int -> int * int -> Builtin.t val check_variadic_sentinel : ?fails_on_nil:bool -> int -> int * int -> Builtin.t
val check_arith_norm_exp : val check_arith_norm_exp :
Tenv.t -> Procname.t -> Exp.t -> Prop.normal Prop.t -> Exp.t * Prop.normal Prop.t BiabductionSummary.t InterproceduralAnalysis.t
-> Exp.t
-> Prop.normal Prop.t
-> Exp.t * Prop.normal Prop.t
(** Check for arithmetic problems and normalize an expression. *) (** Check for arithmetic problems and normalize an expression. *)
val prune : Tenv.t -> positive:bool -> Exp.t -> Prop.normal Prop.t -> Propset.t val prune : Tenv.t -> positive:bool -> Exp.t -> Prop.normal Prop.t -> Propset.t

Write Preview
Loading…
Cancel
Save