[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

@@ -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 *)

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
 

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
 

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
 

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.

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

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

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

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

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 *)