From 9c9519fddb683bb13347c8365371aff4be59d998 Mon Sep 17 00:00:00 2001 From: Dulma Churchill Date: Wed, 21 Mar 2018 10:35:48 -0700 Subject: [PATCH] [backend] Pass the execution environment around to use it to load tenv of callees in a more efficient way Reviewed By: jvillard Differential Revision: D7350922 fbshipit-source-id: 58e0dca --- infer/src/backend/BuiltinDefn.ml | 27 +++++++++-------- infer/src/backend/builtin.ml | 3 +- infer/src/backend/builtin.mli | 3 +- infer/src/backend/callbacks.ml | 5 +-- infer/src/backend/callbacks.mli | 3 +- infer/src/backend/interproc.ml | 35 ++++++++++----------- infer/src/backend/symExec.ml | 52 +++++++++++++++++--------------- infer/src/backend/symExec.mli | 8 ++--- infer/src/backend/tabulation.ml | 51 ++++++++++++++----------------- infer/src/backend/tabulation.mli | 4 +-- 10 files changed, 98 insertions(+), 93 deletions(-) diff --git a/infer/src/backend/BuiltinDefn.ml b/infer/src/backend/BuiltinDefn.ml index 30a722ffd..54dda96d7 100644 --- a/infer/src/backend/BuiltinDefn.ml +++ b/infer/src/backend/BuiltinDefn.ml @@ -18,12 +18,12 @@ module F = Format type t = Builtin.registered (** model va_arg as always returning 0 *) -let execute___builtin_va_arg {Builtin.pdesc; tenv; prop_; path; ret_id; args; loc} +let execute___builtin_va_arg {Builtin.pdesc; tenv; prop_; path; ret_id; args; loc; exe_env} : Builtin.ret_typ = match (args, ret_id) with | [_; _; (lexp3, typ3)], _ -> let instr' = Sil.Store (lexp3, typ3, Exp.zero, loc) in - SymExec.instrs ~mask_errors:true tenv pdesc [instr'] [(prop_, path)] + SymExec.instrs ~mask_errors:true exe_env tenv pdesc [instr'] [(prop_, path)] | _ -> raise (Exceptions.Wrong_argument_number __POS__) @@ -615,7 +615,7 @@ let execute_alloc mk can_return_null {Builtin.pdesc; tenv; prop_; path; ret_id; else [(prop_alloc, path)] -let execute___cxx_typeid ({Builtin.pdesc; tenv; prop_; args; loc} as r) : Builtin.ret_typ = +let execute___cxx_typeid ({Builtin.pdesc; tenv; prop_; args; loc; exe_env} as r) : Builtin.ret_typ = match args with | type_info_exp :: rest -> ( @@ -636,14 +636,15 @@ let execute___cxx_typeid ({Builtin.pdesc; tenv; prop_; args; loc} as r) : Builti let set_instr = Sil.Store (field_exp, Typ.mk Tvoid, Exp.Const (Const.Cstr typ_string), loc) in - SymExec.instrs ~mask_errors:true tenv pdesc [set_instr] res + SymExec.instrs ~mask_errors:true exe_env tenv pdesc [set_instr] res | _ -> res ) | _ -> raise (Exceptions.Wrong_argument_number __POS__) -let execute_pthread_create ({Builtin.tenv; prop_; path; args} as builtin_args) : Builtin.ret_typ = +let execute_pthread_create ({Builtin.tenv; prop_; path; args; exe_env} as builtin_args) + : Builtin.ret_typ = match args with | [_; _; start_routine; arg] -> ( @@ -659,7 +660,8 @@ let execute_pthread_create ({Builtin.tenv; prop_; path; args} as builtin_args) : | None -> assert false | Some callee_summary -> - SymExec.proc_call callee_summary {builtin_args with args= [(routine_arg, snd arg)]} ) + SymExec.proc_call exe_env callee_summary + {builtin_args with args= [(routine_arg, snd arg)]} ) | _ -> L.d_str "pthread_create: unknown function " ; Sil.d_exp routine_name ; @@ -747,7 +749,7 @@ let execute___infer_assume {Builtin.tenv; prop_; path; args} : Builtin.ret_typ = (* creates a named error state *) -let execute___infer_fail {Builtin.pdesc; tenv; prop_; path; args; loc} : Builtin.ret_typ = +let execute___infer_fail {Builtin.pdesc; tenv; prop_; path; args; loc; exe_env} : Builtin.ret_typ = let error_str = match args with | [(lexp_msg, _)] -> ( @@ -762,11 +764,11 @@ let execute___infer_fail {Builtin.pdesc; tenv; prop_; path; args; loc} : Builtin let set_instr = Sil.Store (Exp.Lvar Sil.custom_error, Typ.mk Tvoid, Exp.Const (Const.Cstr error_str), loc) in - SymExec.instrs ~mask_errors:true tenv pdesc [set_instr] [(prop_, path)] + SymExec.instrs ~mask_errors:true exe_env tenv pdesc [set_instr] [(prop_, path)] (* translate builtin assertion failure *) -let execute___assert_fail {Builtin.pdesc; tenv; prop_; path; args; loc} : Builtin.ret_typ = +let execute___assert_fail {Builtin.pdesc; tenv; prop_; path; args; loc; exe_env} : Builtin.ret_typ = let error_str = match List.length args with | 4 -> @@ -777,10 +779,11 @@ let execute___assert_fail {Builtin.pdesc; tenv; prop_; path; args; loc} : Builti let set_instr = Sil.Store (Exp.Lvar Sil.custom_error, Typ.mk Tvoid, Exp.Const (Const.Cstr error_str), loc) in - SymExec.instrs ~mask_errors:true tenv pdesc [set_instr] [(prop_, path)] + SymExec.instrs ~mask_errors:true exe_env tenv pdesc [set_instr] [(prop_, path)] -let execute_objc_alloc_no_fail symb_state typ alloc_fun_opt {Builtin.pdesc; tenv; ret_id; loc} = +let execute_objc_alloc_no_fail symb_state typ alloc_fun_opt + {Builtin.pdesc; tenv; ret_id; loc; exe_env} = let alloc_fun = Exp.Const (Const.Cfun BuiltinDecl.__objc_alloc_no_fail) in let ptr_typ = Typ.mk (Tptr (typ, Typ.Pk_pointer)) in let sizeof_typ = Exp.Sizeof {typ; nbytes= None; dynamic_length= None; subtype= Subtype.exact} in @@ -794,7 +797,7 @@ let execute_objc_alloc_no_fail symb_state typ alloc_fun_opt {Builtin.pdesc; tenv let alloc_instr = Sil.Call (ret_id, alloc_fun, [(sizeof_typ, ptr_typ)] @ alloc_fun_exp, loc, CallFlags.default) in - SymExec.instrs tenv pdesc [alloc_instr] symb_state + SymExec.instrs exe_env tenv pdesc [alloc_instr] symb_state (* NSArray models *) diff --git a/infer/src/backend/builtin.ml b/infer/src/backend/builtin.ml index ced25fa3a..fb1fc13c1 100644 --- a/infer/src/backend/builtin.ml +++ b/infer/src/backend/builtin.ml @@ -21,7 +21,8 @@ type args = ; ret_id: (Ident.t * Typ.t) option ; args: (Exp.t * Typ.t) list ; proc_name: Typ.Procname.t - ; loc: Location.t } + ; loc: Location.t + ; exe_env: Exe_env.t } type ret_typ = (Prop.normal Prop.t * Paths.Path.t) list diff --git a/infer/src/backend/builtin.mli b/infer/src/backend/builtin.mli index b397d9fb5..6acc72fda 100644 --- a/infer/src/backend/builtin.mli +++ b/infer/src/backend/builtin.mli @@ -20,7 +20,8 @@ type args = ; ret_id: (Ident.t * Typ.t) option ; args: (Exp.t * Typ.t) list ; proc_name: Typ.Procname.t - ; loc: Location.t } + ; loc: Location.t + ; exe_env: Exe_env.t } type ret_typ = (Prop.normal Prop.t * Paths.Path.t) list diff --git a/infer/src/backend/callbacks.ml b/infer/src/backend/callbacks.ml index 36566056b..1992146e2 100644 --- a/infer/src/backend/callbacks.ml +++ b/infer/src/backend/callbacks.ml @@ -19,7 +19,8 @@ type proc_callback_args = ; get_procs_in_file: Typ.Procname.t -> Typ.Procname.t list ; tenv: Tenv.t ; summary: Specs.summary - ; proc_desc: Procdesc.t } + ; proc_desc: Procdesc.t + ; exe_env: Exe_env.t } type proc_callback_t = proc_callback_args -> Specs.summary @@ -67,7 +68,7 @@ let iterate_procedure_callbacks get_proc_desc exe_env summary proc_desc = List.fold ~init:summary ~f:(fun summary (language, resolved, proc_callback) -> if Language.equal language procedure_language && (resolved || not is_specialized) then - proc_callback {get_proc_desc; get_procs_in_file; tenv; summary; proc_desc} + proc_callback {get_proc_desc; get_procs_in_file; tenv; summary; proc_desc; exe_env} else summary ) !procedure_callbacks diff --git a/infer/src/backend/callbacks.mli b/infer/src/backend/callbacks.mli index 74c4a5518..814258384 100644 --- a/infer/src/backend/callbacks.mli +++ b/infer/src/backend/callbacks.mli @@ -16,7 +16,8 @@ type proc_callback_args = ; get_procs_in_file: Typ.Procname.t -> Typ.Procname.t list ; tenv: Tenv.t ; summary: Specs.summary - ; proc_desc: Procdesc.t } + ; proc_desc: Procdesc.t + ; exe_env: Exe_env.t } (** Type of a procedure callback: - List of all the procedures the callback will be called on. diff --git a/infer/src/backend/interproc.ml b/infer/src/backend/interproc.ml index ebb4b0db5..c559bdc69 100644 --- a/infer/src/backend/interproc.ml +++ b/infer/src/backend/interproc.ml @@ -375,14 +375,15 @@ let instrs_get_normal_vars instrs = (** Perform symbolic execution for a node starting from an initial prop *) -let do_symbolic_execution proc_cfg handle_exn tenv (node: ProcCfg.Exceptional.node) +let do_symbolic_execution exe_env proc_cfg handle_exn tenv (node: ProcCfg.Exceptional.node) (prop: Prop.normal Prop.t) (path: Paths.Path.t) = State.mark_execution_start node ; let instrs = ProcCfg.Exceptional.instrs node in (* fresh normal vars must be fresh w.r.t. instructions *) Ident.update_name_generator (instrs_get_normal_vars instrs) ; let pset = - SymExec.node handle_exn tenv proc_cfg node (Paths.PathSet.from_renamed_list [(prop, path)]) + SymExec.node handle_exn exe_env tenv proc_cfg node + (Paths.PathSet.from_renamed_list [(prop, path)]) in L.d_strln ".... After Symbolic Execution ...." ; Propset.d prop (Paths.PathSet.to_propset tenv pset) ; @@ -400,7 +401,7 @@ let mark_visited summary node = else stats.Specs.nodes_visited_re <- IntSet.add (node_id :> int) stats.Specs.nodes_visited_re -let forward_tabulate tenv proc_cfg wl = +let forward_tabulate exe_env tenv proc_cfg wl = let pname = Procdesc.get_proc_name (ProcCfg.Exceptional.proc_desc proc_cfg) in let handle_exn_node curr_node exn = Exceptions.print_exception_html "Failure of symbolic execution: " exn ; @@ -456,7 +457,7 @@ let forward_tabulate tenv proc_cfg wl = L.d_increase_indent 1 ; try State.reset_diverging_states_node () ; - let pset = do_symbolic_execution proc_cfg handle_exn tenv curr_node prop path in + let pset = do_symbolic_execution exe_env proc_cfg handle_exn tenv curr_node prop path in let normal_succ_nodes = ProcCfg.Exceptional.normal_succs proc_cfg curr_node in let exn_succ_nodes = ProcCfg.Exceptional.exceptional_succs proc_cfg curr_node in propagate_nodes_divergence tenv proc_cfg pset normal_succ_nodes exn_succ_nodes wl ; @@ -746,8 +747,8 @@ let initial_prop_from_pre tenv curr_f pre = (** Re-execute one precondition and return some spec if there was no re-execution error. *) -let execute_filter_prop wl tenv proc_cfg init_node (precondition: Prop.normal Specs.Jprop.t) - : Prop.normal Specs.spec option = +let execute_filter_prop exe_env wl tenv proc_cfg init_node + (precondition: Prop.normal Specs.Jprop.t) : Prop.normal Specs.spec option = let pdesc = ProcCfg.Exceptional.proc_desc proc_cfg in let pname = Procdesc.get_proc_name pdesc in do_before_node 0 init_node ; @@ -765,7 +766,7 @@ let execute_filter_prop wl tenv proc_cfg init_node (precondition: Prop.normal Sp try Worklist.add wl init_node ; ignore (path_set_put_todo wl init_node init_edgeset) ; - forward_tabulate tenv proc_cfg wl ; + forward_tabulate exe_env tenv proc_cfg wl ; do_before_node 0 init_node ; L.d_strln_color Green ("#### Finished: RE-execution for " ^ Typ.Procname.to_string pname ^ " ####") ; @@ -812,7 +813,7 @@ type exe_phase = (unit -> unit) * (unit -> Prop.normal Specs.spec list * Specs.p and [get_results ()] returns the results computed. This function is architected so that [get_results ()] can be called even after [go ()] was interrupted by and exception. *) -let perform_analysis_phase tenv (summary: Specs.summary) (proc_cfg: ProcCfg.Exceptional.t) +let perform_analysis_phase exe_env tenv (summary: Specs.summary) (proc_cfg: ProcCfg.Exceptional.t) : exe_phase = let pname = Specs.get_proc_name summary in let start_node = ProcCfg.Exceptional.start_node proc_cfg in @@ -844,7 +845,7 @@ let perform_analysis_phase tenv (summary: Specs.summary) (proc_cfg: ProcCfg.Exce L.d_decrease_indent 1 ; Worklist.add wl start_node ; ignore (path_set_put_todo wl start_node init_edgeset) ; - forward_tabulate tenv proc_cfg wl + forward_tabulate exe_env tenv proc_cfg wl in let get_results (wl: Worklist.t) () = State.process_execution_failures Reporting.log_warning_deprecated pname ; @@ -872,7 +873,7 @@ let perform_analysis_phase tenv (summary: Specs.summary) (proc_cfg: ProcCfg.Exce let go () = let filter p = let wl = path_set_create_worklist proc_cfg in - let speco = execute_filter_prop wl tenv proc_cfg start_node p in + let speco = execute_filter_prop exe_env wl tenv proc_cfg start_node p in (match speco with None -> () | Some spec -> valid_specs := !valid_specs @ [spec]) ; speco in @@ -1112,12 +1113,12 @@ let update_summary tenv prev_summary specs phase res = (** Analyze the procedure and return the resulting summary. *) -let analyze_proc tenv proc_cfg : Specs.summary = +let analyze_proc exe_env tenv proc_cfg : Specs.summary = let proc_desc = ProcCfg.Exceptional.proc_desc proc_cfg in let proc_name = Procdesc.get_proc_name proc_desc in reset_global_values proc_desc ; let summary = Specs.get_summary_unsafe "analyze_proc" proc_name in - let go, get_results = perform_analysis_phase tenv summary proc_cfg in + let go, get_results = perform_analysis_phase exe_env tenv summary proc_cfg in let res = Timeout.exe_timeout go () in let specs, phase = get_results () in let updated_summary = update_summary tenv summary specs phase res in @@ -1185,22 +1186,22 @@ let perform_transition proc_cfg tenv proc_name = () -let analyze_procedure_aux tenv proc_desc = +let analyze_procedure_aux exe_env tenv proc_desc = let proc_name = Procdesc.get_proc_name proc_desc in let proc_cfg = ProcCfg.Exceptional.from_pdesc proc_desc in Preanal.do_preanalysis proc_desc tenv ; - let summaryfp = Config.run_in_footprint_mode (analyze_proc tenv) proc_cfg in + let summaryfp = Config.run_in_footprint_mode (analyze_proc exe_env tenv) proc_cfg in Specs.add_summary proc_name summaryfp ; perform_transition proc_cfg tenv proc_name ; - let summaryre = Config.run_in_re_execution_mode (analyze_proc tenv) proc_cfg in + let summaryre = Config.run_in_re_execution_mode (analyze_proc exe_env tenv) proc_cfg in Specs.add_summary proc_name summaryre ; summaryre -let analyze_procedure {Callbacks.summary; proc_desc; tenv} : Specs.summary = +let analyze_procedure {Callbacks.summary; proc_desc; tenv; exe_env} : Specs.summary = let proc_name = Procdesc.get_proc_name proc_desc in Specs.add_summary proc_name summary ; - ( try ignore (analyze_procedure_aux tenv proc_desc) with exn -> + ( try ignore (analyze_procedure_aux exe_env tenv proc_desc) with exn -> reraise_if exn ~f:(fun () -> not (Exceptions.handle_exception exn)) ; Reporting.log_error_deprecated proc_name exn ) ; Specs.get_summary_unsafe __FILE__ proc_name diff --git a/infer/src/backend/symExec.ml b/infer/src/backend/symExec.ml index a8888f988..ed7efc9ae 100644 --- a/infer/src/backend/symExec.ml +++ b/infer/src/backend/symExec.ml @@ -1041,7 +1041,7 @@ let execute_store ?(report_deref_errors= true) pname pdesc tenv lhs_exp typ rhs_ (** Execute [instr] with a symbolic heap [prop].*) -let rec sym_exec tenv current_pdesc instr_ (prop_: Prop.normal Prop.t) path +let rec sym_exec exe_env tenv current_pdesc 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 State.set_instr instr_ ; @@ -1096,7 +1096,8 @@ let rec sym_exec tenv current_pdesc instr_ (prop_: Prop.normal Prop.t) path ; ret_id ; args= actual_args ; proc_name= callee_pname - ; loc } + ; loc + ; exe_env } in if is_objc_instance_method then handle_objc_instance_method_call_or_skip current_pdesc tenv actual_args path callee_pname @@ -1104,7 +1105,7 @@ let rec sym_exec tenv current_pdesc instr_ (prop_: Prop.normal Prop.t) path else skip_res () in let call_args prop_ proc_name args ret_id loc = - {Builtin.pdesc= current_pdesc; instr; tenv; prop_; path; ret_id; args; proc_name; loc} + {Builtin.pdesc= current_pdesc; instr; tenv; prop_; path; ret_id; args; proc_name; loc; exe_env} in match instr with | Sil.Load (id, rhs_exp, typ, loc) -> @@ -1173,7 +1174,8 @@ let rec sym_exec tenv current_pdesc instr_ (prop_: Prop.normal Prop.t) path | Some resolved_summary -> match reason_to_skip resolved_summary with | None -> - proc_call resolved_summary (call_args prop_ callee_pname norm_args ret_id loc) + proc_call exe_env resolved_summary + (call_args prop_ callee_pname norm_args ret_id loc) | Some reason -> let proc_attrs = Specs.get_attributes resolved_summary in let ret_annots, _ = proc_attrs.ProcAttributes.method_annotation in @@ -1199,7 +1201,7 @@ let rec sym_exec tenv current_pdesc instr_ (prop_: Prop.normal Prop.t) path match reason_to_skip callee_summary with | None -> let handled_args = call_args norm_prop pname url_handled_args ret_id loc in - proc_call callee_summary handled_args + proc_call exe_env callee_summary handled_args | Some reason -> let proc_attrs = Specs.get_attributes callee_summary in let ret_annots, _ = proc_attrs.ProcAttributes.method_annotation in @@ -1229,7 +1231,7 @@ let rec sym_exec tenv current_pdesc instr_ (prop_: Prop.normal Prop.t) path normalize_params tenv current_pname prop_r extended_actual_params in Logging.d_strln "Calling method specialized with blocks... " ; - proc_call resolved_summary + proc_call exe_env resolved_summary (call_args prop_r resolved_pname n_extended_actual_params ret_id loc) | None -> (* Generic fun call with known name *) @@ -1273,8 +1275,8 @@ let rec sym_exec tenv current_pdesc instr_ (prop_: Prop.normal Prop.t) path (sym_exec_objc_accessor objc_accessor ret_type) | None, true -> (* If it's an alloc model, call alloc rather than skipping *) - sym_exec_alloc_model callee_pname ret_type tenv ret_id current_pdesc loc - prop path + sym_exec_alloc_model exe_env callee_pname ret_type tenv ret_id + current_pdesc loc prop path | None, false -> let is_objc_instance_method = ProcAttributes.equal_clang_method_kind @@ -1287,7 +1289,7 @@ let rec sym_exec tenv current_pdesc instr_ (prop_: Prop.normal Prop.t) path skip_call ~reason:"function or method not found" prop path resolved_pname ret_annots loc ret_id ret_typ_opt n_actual_params else - proc_call + proc_call exe_env (Option.value_exn resolved_summary_opt) (call_args prop resolved_pname n_actual_params ret_id loc) in @@ -1320,7 +1322,8 @@ let rec sym_exec tenv current_pdesc instr_ (prop_: Prop.normal Prop.t) path ; ret_id ; args= n_actual_params ; proc_name= callee_pname - ; loc } ) + ; loc + ; exe_env } ) | Sil.Nullify (pvar, _) -> ( let eprop = Prop.expose prop_ in @@ -1377,12 +1380,12 @@ and diverge prop path = (** Symbolic execution of a sequence of instructions. If errors occur and [mask_errors] is true, just treat as skip. *) -and instrs ?(mask_errors= false) tenv pdesc instrs ppl = +and instrs ?(mask_errors= false) exe_env tenv pdesc instrs ppl = let exe_instr instr (p, path) = L.d_str "Executing Generated Instruction " ; Sil.d_instr instr ; L.d_ln () ; - try sym_exec tenv pdesc instr p path with exn -> + try sym_exec exe_env tenv pdesc instr p path with exn -> reraise_if exn ~f:(fun () -> not mask_errors || not (SymOp.exn_not_failure exn)) ; let error = Exceptions.recognize_exception exn in let loc = @@ -1575,7 +1578,7 @@ and unknown_or_scan_call ~is_scan ~reason ret_type_option ret_annots and check_variadic_sentinel ?(fails_on_nil= false) n_formals (sentinel, null_pos) - {Builtin.pdesc; tenv; prop_; path; args; proc_name; loc} = + {Builtin.pdesc; tenv; prop_; path; args; proc_name; loc; exe_env} = (* from clang's lib/Sema/SemaExpr.cpp: *) (* "nullPos" is the number of formal parameters at the end which *) (* effectively count as part of the variadic arguments. This is *) @@ -1594,7 +1597,7 @@ and check_variadic_sentinel ?(fails_on_nil= false) n_formals (sentinel, null_pos (* simulate a Load for [lexp] *) let tmp_id_deref = Ident.create_fresh Ident.kprimed in let load_instr = Sil.Load (tmp_id_deref, lexp, typ, loc) in - try instrs tenv pdesc [load_instr] result with e when SymOp.exn_not_failure e -> + try instrs exe_env tenv pdesc [load_instr] result with e when SymOp.exn_not_failure e -> reraise_if e ~f:(fun () -> fails_on_nil) ; let deref_str = Localise.deref_str_nil_argument_in_variadic_method proc_name nargs i in let err_desc = @@ -1674,7 +1677,7 @@ and sym_exec_objc_accessor property_accesor ret_typ tenv ret_id pdesc _ loc args f_accessor ret_typ tenv ret_id pdesc cur_pname loc args prop |> List.map ~f:(fun p -> (p, path)) -and sym_exec_alloc_model pname ret_typ tenv ret_id pdesc loc prop path : Builtin.ret_typ = +and sym_exec_alloc_model exe_env pname ret_typ tenv ret_id pdesc loc prop path : Builtin.ret_typ = let alloc_source_function_arg = (Exp.Const (Const.Cfun pname), Typ.mk Tvoid) in let args = let sizeof_exp = @@ -1686,11 +1689,11 @@ and sym_exec_alloc_model pname ret_typ tenv ret_id pdesc loc prop path : Builtin let alloc_fun = Exp.Const (Const.Cfun BuiltinDecl.malloc_no_fail) in let alloc_instr = Sil.Call (ret_id, alloc_fun, args, loc, CallFlags.default) in L.d_strln "No spec found, method should be model as alloc, executing alloc... " ; - instrs tenv pdesc [alloc_instr] [(prop, path)] + instrs exe_env tenv pdesc [alloc_instr] [(prop, path)] (** Perform symbolic execution for a function call *) -and proc_call callee_summary +and proc_call exe_env callee_summary {Builtin.pdesc; tenv; prop_= pre; path; ret_id; args= actual_pars; loc} = let caller_pname = Procdesc.get_proc_name pdesc in let callee_attrs = Specs.get_attributes callee_summary in @@ -1737,15 +1740,15 @@ and proc_call callee_summary | Language.Clang, ProcAttributes.OBJC_INSTANCE -> handle_objc_instance_method_call actual_pars actual_params pre tenv ret_id pdesc callee_pname loc path - (Tabulation.exe_function_call callee_summary) + (Tabulation.exe_function_call exe_env callee_summary) | _ -> (* non-objective-c method call. Standard tabulation *) - Tabulation.exe_function_call callee_summary tenv ret_id pdesc callee_pname loc actual_params - pre path + Tabulation.exe_function_call exe_env callee_summary tenv ret_id pdesc callee_pname loc + actual_params pre path (** perform symbolic execution for a single prop, and check for junk *) -and sym_exec_wrapper handle_exn tenv proc_cfg instr ((prop: Prop.normal Prop.t), path) +and sym_exec_wrapper exe_env handle_exn tenv proc_cfg instr ((prop: Prop.normal Prop.t), path) : Paths.PathSet.t = let pname = Procdesc.get_proc_name (ProcCfg.Exceptional.proc_desc proc_cfg) in let prop_primed_to_normal p = @@ -1804,7 +1807,8 @@ and sym_exec_wrapper handle_exn tenv proc_cfg instr ((prop: Prop.normal Prop.t), let res_list = Config.run_with_abs_val_equal_zero (* no exp abstraction during sym exe *) - (fun () -> sym_exec tenv (ProcCfg.Exceptional.proc_desc proc_cfg) instr prop' path ) + (fun () -> + sym_exec exe_env tenv (ProcCfg.Exceptional.proc_desc proc_cfg) instr prop' path ) () in let res_list_nojunk = @@ -1829,7 +1833,7 @@ and sym_exec_wrapper handle_exn tenv proc_cfg instr ((prop: Prop.normal Prop.t), (** {2 Lifted Abstract Transfer Functions} *) -let node handle_exn tenv proc_cfg (node: ProcCfg.Exceptional.node) (pset: Paths.PathSet.t) +let node handle_exn exe_env tenv proc_cfg (node: ProcCfg.Exceptional.node) (pset: Paths.PathSet.t) : Paths.PathSet.t = let pname = Procdesc.get_proc_name (ProcCfg.Exceptional.proc_desc proc_cfg) in let exe_instr_prop instr p tr (pset1: Paths.PathSet.t) = @@ -1843,7 +1847,7 @@ let node handle_exn tenv proc_cfg (node: ProcCfg.Exceptional.node) (pset: Paths. Sil.d_instr instr ; L.d_strln " due to exception" ; Paths.PathSet.from_renamed_list [(p, tr)] ) - else sym_exec_wrapper handle_exn tenv proc_cfg instr (p, tr) + else sym_exec_wrapper exe_env handle_exn tenv proc_cfg instr (p, tr) in Paths.PathSet.union pset2 pset1 in diff --git a/infer/src/backend/symExec.mli b/infer/src/backend/symExec.mli index 93acc30af..824616524 100644 --- a/infer/src/backend/symExec.mli +++ b/infer/src/backend/symExec.mli @@ -13,12 +13,12 @@ open! IStd (** Symbolic Execution *) val node : - (exn -> unit) -> Tenv.t -> ProcCfg.Exceptional.t -> ProcCfg.Exceptional.node -> Paths.PathSet.t - -> Paths.PathSet.t + (exn -> unit) -> Exe_env.t -> Tenv.t -> ProcCfg.Exceptional.t -> ProcCfg.Exceptional.node + -> Paths.PathSet.t -> Paths.PathSet.t (** Symbolic execution of the instructions of a node, lifted to sets of propositions. *) val instrs : - ?mask_errors:bool -> Tenv.t -> Procdesc.t -> Sil.instr list + ?mask_errors:bool -> Exe_env.t -> Tenv.t -> Procdesc.t -> Sil.instr list -> (Prop.normal Prop.t * Paths.Path.t) list -> (Prop.normal Prop.t * Paths.Path.t) list (** Symbolic execution of a sequence of instructions. If errors occur and [mask_errors] is true, just treat as skip. *) @@ -26,7 +26,7 @@ val instrs : val diverge : Prop.normal Prop.t -> Paths.Path.t -> (Prop.normal Prop.t * Paths.Path.t) list (** Symbolic execution of the divergent pure computation. *) -val proc_call : Specs.summary -> Builtin.t +val proc_call : Exe_env.t -> Specs.summary -> Builtin.t val unknown_or_scan_call : is_scan:bool -> reason:string -> Typ.t option -> Annot.Item.t -> Builtin.t diff --git a/infer/src/backend/tabulation.ml b/infer/src/backend/tabulation.ml index 3fc110e97..a533522da 100644 --- a/infer/src/backend/tabulation.ml +++ b/infer/src/backend/tabulation.ml @@ -1084,37 +1084,29 @@ let missing_sigma_need_adding_to_tenv tenv hpreds = List.exists hpreds ~f:missing_hpred_need_adding_to_tenv -let add_missing_field_to_tenv ~missing_sigma caller_tenv callee_pname hpreds = +let add_missing_field_to_tenv ~missing_sigma exe_env caller_tenv callee_pname hpreds = (* if hpreds are missing_sigma, we may not need to add the fields to the tenv, so we check that first *) let add_fields = if missing_sigma then missing_sigma_need_adding_to_tenv caller_tenv hpreds else true in if add_fields then - match Ondemand.get_proc_desc callee_pname with - | Some pdesc -> - let attrs = Procdesc.get_attributes pdesc in - let source_file = attrs.ProcAttributes.loc.Location.file in - let callee_tenv_opt = Tenv.load source_file in - let add_field_in_hpred hpred = - match (callee_tenv_opt, hpred) with - | ( Some callee_tenv - , Sil.Hpointsto (_, Sil.Estruct (_, _), Exp.Sizeof {typ= {desc= Typ.Tstruct name}}) ) - -> ( - match Tenv.lookup callee_tenv name with - | Some {fields} -> - List.iter ~f:(fun field -> Tenv.add_field caller_tenv name field) fields - | None -> - () ) - | _ -> - () - in - List.iter ~f:add_field_in_hpred hpreds - | None -> - () + let callee_tenv = Exe_env.get_tenv exe_env callee_pname in + let add_field_in_hpred hpred = + match hpred with + | Sil.Hpointsto (_, Sil.Estruct (_, _), Exp.Sizeof {typ= {desc= Typ.Tstruct name}}) -> ( + match Tenv.lookup callee_tenv name with + | Some {fields} -> + List.iter ~f:(fun field -> Tenv.add_field caller_tenv name field) fields + | None -> + () ) + | _ -> + () + in + List.iter ~f:add_field_in_hpred hpreds (** Perform symbolic execution for a single spec *) -let exe_spec tenv ret_id_opt (n, nspecs) caller_pdesc callee_pname loc prop path_pre +let exe_spec exe_env tenv ret_id_opt (n, nspecs) caller_pdesc callee_pname loc prop path_pre (spec: Prop.exposed Specs.spec) actual_params formal_params : abduction_res = let caller_pname = Procdesc.get_proc_name caller_pdesc in let posts = mk_posts tenv ret_id_opt prop callee_pname spec.Specs.posts in @@ -1213,10 +1205,11 @@ let exe_spec tenv ret_id_opt (n, nspecs) caller_pdesc callee_pname loc prop path in if missing_fld_objc_class <> [] then ( L.d_strln "Objective-C missing_fld not empty: adding it to current tenv..." ; - add_missing_field_to_tenv ~missing_sigma:false tenv callee_pname missing_fld_objc_class ) ; + add_missing_field_to_tenv ~missing_sigma:false exe_env tenv callee_pname + missing_fld_objc_class ) ; if missing_sigma_objc_class <> [] then ( L.d_strln "Objective-C missing_sigma not empty: adding it to current tenv..." ; - add_missing_field_to_tenv ~missing_sigma:true tenv callee_pname + add_missing_field_to_tenv ~missing_sigma:true exe_env tenv callee_pname missing_sigma_objc_class ) ; if not !Config.footprint && split.missing_sigma <> [] then ( L.d_strln "Implication error: missing_sigma not empty in re-execution" ; @@ -1435,8 +1428,8 @@ let exe_call_postprocess tenv ret_id trace_call caller_pname callee_pname callee (** Execute the function call and return the list of results with return value *) -let exe_function_call callee_summary tenv ret_id_opt caller_pdesc callee_pname loc actual_params - prop path = +let exe_function_call exe_env callee_summary tenv ret_id_opt caller_pdesc callee_pname loc + actual_params prop path = let callee_attrs = Specs.get_attributes callee_summary in let caller_pname = Procdesc.get_proc_name caller_pdesc in let trace_call = log_call_trace caller_pname callee_pname loc in @@ -1449,8 +1442,8 @@ let exe_function_call callee_summary tenv ret_id_opt caller_pdesc callee_pname l Prop.d_prop prop ; L.d_ln () ; let exe_one_spec (n, spec) = - exe_spec tenv ret_id_opt (n, nspecs) caller_pdesc callee_pname loc prop path spec actual_params - formal_params + exe_spec exe_env tenv ret_id_opt (n, nspecs) caller_pdesc callee_pname loc prop path spec + actual_params formal_params in let results = List.map ~f:exe_one_spec spec_list in exe_call_postprocess tenv ret_id_opt trace_call caller_pname callee_pname callee_attrs loc diff --git a/infer/src/backend/tabulation.mli b/infer/src/backend/tabulation.mli index b01aa35c7..811cc338b 100644 --- a/infer/src/backend/tabulation.mli +++ b/infer/src/backend/tabulation.mli @@ -47,7 +47,7 @@ val lookup_custom_errors : 'a Prop.t -> string option (** search in prop contains an error state *) val exe_function_call : - Specs.summary -> Tenv.t -> (Ident.t * Typ.t) option -> Procdesc.t -> Typ.Procname.t -> Location.t - -> (Exp.t * Typ.t) list -> Prop.normal Prop.t -> Paths.Path.t + Exe_env.t -> Specs.summary -> Tenv.t -> (Ident.t * Typ.t) option -> Procdesc.t -> Typ.Procname.t + -> Location.t -> (Exp.t * Typ.t) list -> Prop.normal Prop.t -> Paths.Path.t -> (Prop.normal Prop.t * Paths.Path.t) list (** Execute the function call and return the list of results with return value *)