From eb336fc4b725c8d6da2d6fcdceee374c72cf9ce7 Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Wed, 29 Apr 2020 02:59:53 -0700 Subject: [PATCH] SymExec free of SummaryReporting Summary: progress Reviewed By: dulmarod Differential Revision: D21261637 fbshipit-source-id: 132375f66 --- infer/src/biabduction/BuiltinDefn.ml | 130 ++++++++++++--------------- infer/src/biabduction/SymExec.ml | 85 +++++++++--------- infer/src/biabduction/SymExec.mli | 5 +- 3 files changed, 104 insertions(+), 116 deletions(-) diff --git a/infer/src/biabduction/BuiltinDefn.ml b/infer/src/biabduction/BuiltinDefn.ml index d2d1b2f61..3c5f683aa 100644 --- a/infer/src/biabduction/BuiltinDefn.ml +++ b/infer/src/biabduction/BuiltinDefn.ml @@ -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 *) (* Return the new prop and the array length *) (* Return None if it fails to add the array *) -let add_array_to_prop tenv pdesc prop_ lexp typ = - let pname = Procdesc.get_proc_name pdesc in - let n_lexp, prop = check_arith_norm_exp tenv pname lexp prop_ in +let add_array_to_prop ({InterproceduralAnalysis.tenv; _} as analysis_data) prop_ lexp typ = + let n_lexp, prop = check_arith_norm_exp analysis_data lexp prop_ in let hpred_opt = List.find ~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.*) -let execute___require_allocated_array {Builtin.analysis_data= {proc_desc; tenv}; prop_; path; args} - : Builtin.ret_typ = +let execute___require_allocated_array {Builtin.analysis_data; prop_; path; args} : Builtin.ret_typ = match args with | [(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 -> [] | Some (_, prop) -> @@ -99,10 +97,11 @@ let execute___require_allocated_array {Builtin.analysis_data= {proc_desc; tenv}; 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 | [(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 -> [] | Some (len, prop) -> @@ -111,18 +110,17 @@ let execute___get_array_length raise (Exceptions.Wrong_argument_number __POS__) -let execute___set_array_length {Builtin.analysis_data= {proc_desc; tenv}; prop_; path; args} : - Builtin.ret_typ = +let execute___set_array_length {Builtin.analysis_data= {tenv; _} as analysis_data; prop_; path; args} + : Builtin.ret_typ = match args with | [(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 -> [] | Some (_, prop_a) -> ( (* 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 tenv pname lexp prop_a in - let n_len, prop = check_arith_norm_exp tenv pname len prop__ in + let n_lexp, prop__ = check_arith_norm_exp analysis_data lexp prop_a in + let n_len, prop = check_arith_norm_exp analysis_data len prop__ in let hpred, sigma' = List.partition_tf ~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__) -let execute___print_value {Builtin.analysis_data= {proc_desc; tenv}; prop_; path; args} : - Builtin.ret_typ = +let execute___print_value {Builtin.analysis_data; prop_; path; args} : Builtin.ret_typ = L.(debug Analysis Medium) "__print_value: " ; - let pname = Procdesc.get_proc_name proc_desc in 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 in List.iter ~f:do_arg args ; @@ -213,12 +209,12 @@ let create_type tenv n_lexp typ prop = else null_case @ non_null_case -let execute___get_type_of {Builtin.analysis_data= {proc_desc; tenv}; prop_; path; ret_id_typ; args} - : Builtin.ret_typ = +let execute___get_type_of + {Builtin.analysis_data= {tenv; _} as analysis_data; prop_; path; ret_id_typ; args} : + Builtin.ret_typ = match args with | [(lexp, typ)] -> - let pname = Procdesc.get_proc_name proc_desc in - let n_lexp, prop = check_arith_norm_exp tenv pname lexp prop_ in + let n_lexp, prop = check_arith_norm_exp analysis_data lexp prop_ in let props = create_type tenv n_lexp typ prop in let aux prop = let hpred_opt = @@ -261,12 +257,12 @@ let replace_ptsto_texp tenv prop root_e texp = 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 | [(val1_, typ1); (texp2_, _)] -> - let pname = Procdesc.get_proc_name proc_desc in - let val1, prop__ = check_arith_norm_exp tenv pname val1_ prop_ in - let texp2, prop = check_arith_norm_exp tenv pname texp2_ prop__ in + let val1, prop__ = check_arith_norm_exp analysis_data val1_ prop_ in + let texp2, prop = check_arith_norm_exp analysis_data texp2_ prop__ in let is_cast_to_reference = match typ1.desc with Typ.Tptr (_, Typ.Pk_reference) -> true | _ -> false 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 *) -let execute___set_file_attribute {Builtin.analysis_data= {proc_desc; tenv}; prop_; path; args; loc} - : Builtin.ret_typ = +let execute___set_file_attribute + {Builtin.analysis_data= {tenv; _} as analysis_data; prop_; path; args; loc} : Builtin.ret_typ = match args with | [(lexp, _)] -> - let pname = Procdesc.get_proc_name proc_desc in - let n_lexp, prop = check_arith_norm_exp tenv pname lexp prop_ in + let n_lexp, prop = check_arith_norm_exp analysis_data lexp prop_ in set_resource_attribute tenv prop path n_lexp loc PredSymb.Rfile | _ -> 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 assumed to be "this" *) 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 | [_; (lexp, _)] -> - let pname = Procdesc.get_proc_name proc_desc in - let n_lexp, prop = check_arith_norm_exp tenv pname lexp prop_ in + let n_lexp, prop = check_arith_norm_exp analysis_data lexp prop_ in set_resource_attribute tenv prop path n_lexp loc PredSymb.Rignore | _ -> raise (Exceptions.Wrong_argument_number __POS__) (** Set the attibute of the value as memory *) -let execute___set_mem_attribute {Builtin.analysis_data= {proc_desc; tenv}; prop_; path; args; loc} : - Builtin.ret_typ = +let execute___set_mem_attribute + {Builtin.analysis_data= {tenv; _} as analysis_data; prop_; path; args; loc} : Builtin.ret_typ = match args with | [(lexp, _)] -> - let pname = Procdesc.get_proc_name proc_desc in - let n_lexp, prop = check_arith_norm_exp tenv pname lexp prop_ in + let n_lexp, prop = check_arith_norm_exp analysis_data lexp prop_ in set_resource_attribute tenv prop path n_lexp loc (PredSymb.Rmemory PredSymb.Mnew) | _ -> raise (Exceptions.Wrong_argument_number __POS__) -let set_attr tenv pdesc prop path exp attr = - let pname = Procdesc.get_proc_name pdesc in - let n_lexp, prop = check_arith_norm_exp tenv pname exp prop in +let set_attr ({InterproceduralAnalysis.tenv; _} as analysis_data) prop path exp attr = + let n_lexp, prop = check_arith_norm_exp analysis_data exp prop in [(Attribute.add_or_replace tenv prop (Apred (attr, [n_lexp])), path)] -let delete_attr tenv pdesc prop path exp attr = - let pname = Procdesc.get_proc_name pdesc in - let n_lexp, prop = check_arith_norm_exp tenv pname exp prop in +let delete_attr ({InterproceduralAnalysis.tenv; _} as analysis_data) prop path exp attr = + let n_lexp, prop = check_arith_norm_exp analysis_data exp prop in [(Attribute.remove tenv prop (Apred (attr, [n_lexp])), path)] (** Set attibute att *) -let execute___set_attr attr {Builtin.analysis_data= {proc_desc; tenv}; prop_; path; args} : - Builtin.ret_typ = +let execute___set_attr attr {Builtin.analysis_data; prop_; path; args} : Builtin.ret_typ = match args with | [(lexp, _)] -> - set_attr tenv proc_desc prop_ path lexp attr + set_attr analysis_data prop_ path lexp attr | _ -> raise (Exceptions.Wrong_argument_number __POS__) (** Delete the locked attibute of the value*) -let execute___delete_locked_attribute {Builtin.analysis_data= {proc_desc; tenv}; prop_; path; args} - : Builtin.ret_typ = +let execute___delete_locked_attribute {Builtin.analysis_data; prop_; path; args} : Builtin.ret_typ = match args with | [(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__) @@ -500,12 +489,11 @@ let execute_free_nonzero_ 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 = match args with | [(lexp, typ)] -> - let pname = Procdesc.get_proc_name proc_desc in - let n_lexp, prop = check_arith_norm_exp tenv pname lexp prop_ in + let n_lexp, prop = check_arith_norm_exp analysis_data lexp prop_ in let prop_nonzero = (* case n_lexp!=0 *) 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_alloc mk can_return_null - {Builtin.analysis_data= {proc_desc; tenv}; prop_; path; ret_id_typ; args; loc} : Builtin.ret_typ - = - let pname = Procdesc.get_proc_name proc_desc in + {Builtin.analysis_data= {tenv; _} as analysis_data; prop_; path; ret_id_typ; args; loc} : + Builtin.ret_typ = let rec evaluate_char_sizeof e = match e with | Exp.Var _ -> @@ -578,7 +565,7 @@ let execute_alloc mk can_return_null in let ret_id = fst ret_id_typ in 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 (Prop.exp_normalize_prop tenv prop n_size_exp', prop) in @@ -611,16 +598,13 @@ let execute_alloc mk can_return_null else [(prop_alloc, path)] -let execute___cxx_typeid - ({Builtin.analysis_data= {proc_desc; tenv} as analysis_data; prop_; args; loc} as r) : - Builtin.ret_typ = +let execute___cxx_typeid ({Builtin.analysis_data; prop_; args; loc} as r) : Builtin.ret_typ = match args with | type_info_exp :: rest -> ( let res = execute_alloc PredSymb.Mnew false {r with args= [type_info_exp]} in match rest with | [(field_exp, _); (lexp, typ_)] -> - let pname = Procdesc.get_proc_name proc_desc in - let n_lexp, prop = check_arith_norm_exp tenv pname lexp prop_ in + let n_lexp, prop = check_arith_norm_exp analysis_data lexp prop_ in let typ = List.find ~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 - {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 | [(ret_exn, _)] -> ( - let pname = Procdesc.get_proc_name proc_desc in - let n_ret_exn, prop = check_arith_norm_exp tenv pname ret_exn prop_ in + let n_ret_exn, prop = check_arith_norm_exp analysis_data ret_exn prop_ in match n_ret_exn with | Exp.Exn exp -> 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 - {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 | (arg1_, _) :: _ -> - let pname = Procdesc.get_proc_name proc_desc in - let arg1, prop = check_arith_norm_exp tenv pname arg1_ prop_ in + let arg1, prop = check_arith_norm_exp analysis_data arg1_ prop_ in let prop' = return_result tenv arg1 prop ret_id_typ in [(prop', path)] | _ -> raise (Exceptions.Wrong_argument_number __POS__) -let execute___split_get_nth {Builtin.analysis_data= {proc_desc; tenv}; prop_; path; ret_id_typ; args} - : Builtin.ret_typ = +let execute___split_get_nth + {Builtin.analysis_data= {tenv; _} as analysis_data; prop_; path; ret_id_typ; args} : + Builtin.ret_typ = match args with | [(lexp1, _); (lexp2, _); (lexp3, _)] -> ( - let pname = Procdesc.get_proc_name proc_desc in - let n_lexp1, prop__ = check_arith_norm_exp tenv pname lexp1 prop_ in - let n_lexp2, prop___ = check_arith_norm_exp tenv pname lexp2 prop__ in - let n_lexp3, prop = check_arith_norm_exp tenv pname lexp3 prop___ in + let n_lexp1, prop__ = check_arith_norm_exp analysis_data lexp1 prop_ in + let n_lexp2, prop___ = check_arith_norm_exp analysis_data lexp2 prop__ in + let n_lexp3, prop = check_arith_norm_exp analysis_data lexp3 prop___ in match (n_lexp1, n_lexp2, n_lexp3) with | 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 diff --git a/infer/src/biabduction/SymExec.ml b/infer/src/biabduction/SymExec.ml index dbb7763b6..6164cf6a5 100644 --- a/infer/src/biabduction/SymExec.ml +++ b/infer/src/biabduction/SymExec.ml @@ -402,7 +402,7 @@ let check_constant_string_dereference lexp = (** 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 | Some (Attribute.Div0 div), prop' -> let desc = @@ -410,7 +410,8 @@ let check_arith_norm_exp tenv pname exp prop = (AnalysisState.get_loc_exn ()) 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') | Some (Attribute.UminusUnsigned (e, typ)), prop' -> let desc = @@ -418,14 +419,15 @@ let check_arith_norm_exp tenv pname exp prop = (AnalysisState.get_node_exn ()) (AnalysisState.get_loc_exn ()) 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') | None, prop' -> (Prop.exp_normalize_prop tenv prop exp, prop') (** 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 = List.find ~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 ()) 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 -> () @@ -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 -let normalize_params tenv pdesc prop actual_params = +let normalize_params analysis_data prop actual_params = 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) 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 -let execute_load ?(report_deref_errors = true) pname - ({InterproceduralAnalysis.proc_desc= pdesc; tenv; _} as analysis_data) id rhs_exp typ loc prop_ - = +let execute_load ?(report_deref_errors = true) ({InterproceduralAnalysis.tenv; _} as analysis_data) + id rhs_exp typ loc prop_ = let execute_load_ acc_in iter = 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 match Prop.prop_iter_current tenv iter_ren with | Predicates.Hpointsto (lexp, strexp, Exp.Sizeof sizeof_data), offlist -> ( 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 let is_union_field = match rhs_exp with @@ -1005,7 +1007,7 @@ let execute_load ?(report_deref_errors = true) pname assert false in 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 match check_constant_string_dereference n_rhs_exp' with | Some value -> @@ -1036,8 +1038,8 @@ let load_ret_annots pname = Annot.Item.empty -let execute_store ?(report_deref_errors = true) pname - ({InterproceduralAnalysis.tenv; _} as analysis_data) lhs_exp typ rhs_exp loc prop_ = +let execute_store ?(report_deref_errors = true) ({InterproceduralAnalysis.tenv; _} as analysis_data) + lhs_exp typ rhs_exp loc prop_ = let execute_store_ analysis_data tenv rhs_exp acc_in iter = let lexp, strexp, sizeof, offlist = 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 in try - let n_lhs_exp, prop_' = check_arith_norm_exp tenv pname lhs_exp prop_ in - let n_rhs_exp, prop = check_arith_norm_exp tenv pname rhs_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 analysis_data rhs_exp prop_' 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 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].*) let rec sym_exec - ({InterproceduralAnalysis.proc_desc= current_pdesc; analyze_dependency; tenv} as analysis_data) - instr_ (prop_ : Prop.normal Prop.t) path : (Prop.normal Prop.t * Paths.Path.t) list = + ( {InterproceduralAnalysis.proc_desc= current_pdesc; analyze_dependency; err_log; tenv} as + 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 AnalysisState.set_instr instr_ ; (* mark instruction last seen *) @@ -1206,7 +1209,8 @@ let rec sym_exec ret_id_typ ret_typ actual_args = let skip_res () = 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 ; unknown_or_scan_call ~is_scan:false ~reason ret_typ ret_annots { Builtin.instr @@ -1228,9 +1232,9 @@ let rec sym_exec in match instr with | 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} -> - 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) -> let prop__ = Attribute.nullify_exp_with_objc_null tenv prop_ cond in let check_condition_always_true_false () = @@ -1257,14 +1261,16 @@ let rec sym_exec let exn = Exceptions.Condition_always_true_false (desc, not (IntLit.iszero i), __POS__) 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 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 () ; - 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)) | Sil.Call (ret_id_typ, Exp.Const (Const.Cfun callee_pname), actual_params, loc, call_flags) -> ( match Builtin.get callee_pname with @@ -1273,7 +1279,7 @@ let rec sym_exec | None -> ( match callee_pname with | 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 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 @@ -1298,7 +1304,7 @@ let rec sym_exec exec_skip_call ~reason resolved_pname ret_annots proc_attrs.ProcAttributes.ret_type ) ) | 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 resolved_pnames = 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 | _ -> ( (* 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 *) let with_block_parameters_summary_opt = if call_flags.CallFlags.cf_with_block_parameters then @@ -1337,7 +1343,7 @@ let rec sym_exec match with_block_parameters_summary_opt with | Some (resolved_summary, 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 Logging.d_strln "Calling method specialized with blocks... " ; proc_call resolved_summary @@ -1416,7 +1422,7 @@ let rec sym_exec List.concat_map ~f:do_call sentinel_result ) ) ) | Sil.Call (ret_id_typ, fun_exp, actual_params, loc, call_flags) -> (* 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 call_flags.CallFlags.cf_is_objc_block && 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) - pname loc args prop = + loc args prop = let field_name, _, _ = field in L.d_printfln "No custom getter found. Executing the ObjC builtin getter with ivar %a." 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), _)} ) ) ] -> Tenv.add_field tenv struct_name field ; 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 - loc prop + execute_load ~report_deref_errors:false analysis_data ret_id field_access_exp ret_typ loc prop | _ -> raise (Exceptions.Wrong_argument_number __POS__) -and sym_exec_objc_setter field _ _ ({InterproceduralAnalysis.tenv; _} as analysis_data) pname loc - args prop = +and sym_exec_objc_setter field _ _ ({InterproceduralAnalysis.tenv; _} as analysis_data) loc args + prop = let field_name, _, _ = field in L.d_printfln "No custom setter found. Executing the ObjC builtin setter with ivar %a." Fieldname.pp field_name ; @@ -1758,15 +1763,13 @@ and sym_exec_objc_setter field _ _ ({InterproceduralAnalysis.tenv; _} as analysi :: (lexp2, typ2) :: _ -> Tenv.add_field tenv struct_name field ; 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 - prop + execute_store ~report_deref_errors:false analysis_data field_access_exp typ2 lexp2 loc prop | _ -> raise (Exceptions.Wrong_argument_number __POS__) -and sym_exec_objc_accessor callee_pname property_accesor ret_typ ret_id - ({InterproceduralAnalysis.proc_desc= pdesc} as analysis_data) _ loc args prop path : - Builtin.ret_typ = +and sym_exec_objc_accessor callee_pname property_accesor ret_typ ret_id analysis_data _ loc args + prop path : Builtin.ret_typ = let f_accessor = match property_accesor with | ProcAttributes.Objc_getter field -> @@ -1776,15 +1779,13 @@ and sym_exec_objc_accessor callee_pname property_accesor ret_typ ret_id in (* 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 *) - let cur_pname = Procdesc.get_proc_name pdesc in let path_description = F.sprintf "Executing synthesized %s %s" (ProcAttributes.kind_of_objc_accessor_type property_accesor) (Procname.to_simplified_string callee_pname) in let path = Paths.Path.add_description path path_description in - f_accessor ret_typ ret_id analysis_data cur_pname loc args prop - |> List.map ~f:(fun p -> (p, path)) + f_accessor ret_typ ret_id analysis_data loc args prop |> 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 = diff --git a/infer/src/biabduction/SymExec.mli b/infer/src/biabduction/SymExec.mli index 518766f60..58b5150a2 100644 --- a/infer/src/biabduction/SymExec.mli +++ b/infer/src/biabduction/SymExec.mli @@ -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_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. *) val prune : Tenv.t -> positive:bool -> Exp.t -> Prop.normal Prop.t -> Propset.t