Simplify code in SymExec: cleanup and look up cfg.

Reviewed By: jeremydubreil

Differential Revision: D3011360

fb-gh-sync-id: b2fb8fc
shipit-source-id: b2fb8fc

infer/src/backend/callbacks.ml

@@ -12,6 +12,7 @@ module L = Logging
 (** Module to register and invoke callbacks *)
 
 type proc_callback_args = {
+  get_cfg : Procname.t -> Cfg.cfg option;
   get_proc_desc : Procname.t -> Cfg.Procdesc.t option;
   get_procs_in_file : Procname.t -> Procname.t list;
   idenv : Idenv.t;
@@ -61,6 +62,8 @@ let iterate_procedure_callbacks exe_env proc_name =
   Config.curr_language := procedure_language;
 
   let cfg = Exe_env.get_cfg exe_env proc_name in
+  let get_cfg pname =
+    Some (Exe_env.get_cfg exe_env pname) in
   let get_proc_desc proc_name =
     let cfg = try Exe_env.get_cfg exe_env proc_name with Not_found -> cfg in
     Cfg.Procdesc.find_from_name cfg proc_name in
@@ -90,6 +93,7 @@ let iterate_procedure_callbacks exe_env proc_name =
                 let init_time = Unix.gettimeofday () in
                 proc_callback
                   {
+                    get_cfg;
                     get_proc_desc;
                     get_procs_in_file;
                     idenv;

infer/src/backend/callbacks.mli

@@ -10,6 +10,7 @@
 (** Module to register and invoke callbacks *)
 
 type proc_callback_args = {
+  get_cfg : Procname.t -> Cfg.cfg option;
   get_proc_desc : Procname.t -> Cfg.Procdesc.t option;
   get_procs_in_file : Procname.t -> Procname.t list;
   idenv : Idenv.t;

infer/src/backend/cfg.ml

@@ -984,17 +984,6 @@ let check_cfg_connectedness cfg =
   let pdescs = get_all_procs cfg in
   IList.iter do_pdesc pdescs
 
-(** Given a mangled name of a block return its procdesc if exists*)
-let get_block_pdesc cfg block =
-  let pdescs = get_defined_procs cfg in
-  let is_block_pdesc pd =
-    let name = Procdesc.get_proc_name pd in
-    (Procname.to_string name) = (Mangled.to_string block) in
-  try
-    let block_pdesc = IList.find is_block_pdesc pdescs in
-    Some block_pdesc
-  with Not_found -> None
-
 (** Removes seeds variables from a prop corresponding to captured variables in an objc block *)
 let remove_seed_captured_vars_block captured_vars prop =
   let is_captured pname vn = Mangled.equal pname vn in
@@ -1158,14 +1147,14 @@ let store_cfg_to_file (filename : DB.filename) (save_sources : bool) (cfg : cfg)
     (name, typ) where name is a parameter. The resulting procedure CFG is isomorphic but
     all the type of the parameters are replaced in the instructions according to the list.
     The virtual calls are also replaced to match the parameter types *)
-let specialize_types cfg callee_proc_name resolved_proc_name args =
-  (* TODO (#9333890): This currently only works when the callee is defined in the same file.
+let specialize_types caller_cfg callee_proc_name resolved_proc_name args =
+  (** TODO (#9333890): This currently only works when the callee is defined in the same file.
       Add support to search for the callee procedure description in the execution environment *)
-  match Procdesc.find_from_name cfg resolved_proc_name with
+  match Procdesc.find_from_name caller_cfg resolved_proc_name with
   | Some _ -> ()
   | None ->
       begin
-        match Procdesc.find_from_name cfg callee_proc_name with
+        match Procdesc.find_from_name caller_cfg callee_proc_name with
         | None -> ()
         | Some callee_proc_desc ->
             let callee_attributes = Procdesc.get_attributes callee_proc_desc in
@@ -1179,12 +1168,13 @@ let specialize_types cfg callee_proc_name resolved_proc_name args =
                 proc_name = resolved_proc_name;
               } in
             AttributesTable.store_attributes resolved_attributes;
-            Procdesc.specialize_types cfg callee_proc_desc resolved_attributes resolved_formals;
+            Procdesc.specialize_types
+              caller_cfg callee_proc_desc resolved_attributes resolved_formals;
             begin
               let source_file = resolved_attributes.ProcAttributes.loc.Location.file in
               let source_dir = DB.source_dir_from_source_file source_file in
               let cfg_file = DB.source_dir_get_internal_file source_dir ".cfg" in
               let save_sources = false in
-              store_cfg_to_file cfg_file save_sources cfg
+              store_cfg_to_file cfg_file save_sources caller_cfg
             end
       end

infer/src/backend/cfg.mli

@@ -310,9 +310,6 @@ val remove_seed_vars : 'a Prop.t -> Prop.normal Prop.t
 (** checks whether a cfg is connected or not *)
 val check_cfg_connectedness : cfg -> unit
 
-(** Given a mangled name of a block return its procdesc if exists*)
-val get_block_pdesc : cfg -> Mangled.t -> Procdesc.t option
-
 (** Removes seeds variables from a prop corresponding to captured variables in an objc block *)
 val remove_seed_captured_vars_block : Mangled.t list -> Prop.normal Prop.t -> Prop.normal Prop.t
 

infer/src/backend/config.ml

@@ -291,9 +291,6 @@ let smt_output = ref false
 (** flag: if true performs taint analysis *)
 let taint_analysis = ref true
 
-(** set to true to printing tracing information for the analysis *)
-let trace_anal = ref false
-
 (** Flag for turning on the optimization based on locality
     0 = no
     1 = based on reachability

infer/src/backend/interproc.ml

@@ -160,7 +160,7 @@ let path_set_checkout_todo (wl : Worklist.t) (node: Cfg.node) : Paths.PathSet.t
 let collect_do_abstract_pre pname tenv (pset : Propset.t) : Propset.t =
   if !Config.footprint
   then
-    run_with_footprint_false
+    run_in_re_execution_mode
       (Abs.lifted_abstract pname tenv)
       pset
   else
@@ -172,7 +172,7 @@ let collect_do_abstract_post pname tenv (pathset : Paths.PathSet.t) : Paths.Path
     else Some (Abs.abstract pname tenv p) in
   if !Config.footprint
   then
-    run_with_footprint_false
+    run_in_re_execution_mode
       (Paths.PathSet.map_option abs_option)
       pathset
   else
@@ -198,7 +198,7 @@ let collect_preconditions pname tenv proc_name : Prop.normal Specs.Jprop.t list
   let collect_do_abstract_one tenv prop =
     if !Config.footprint
     then
-      run_with_footprint_false
+      run_in_re_execution_mode
         (Abs.abstract_no_symop tenv)
         prop
     else
@@ -443,7 +443,7 @@ let check_assignement_guard node =
     ) else ()
 
 (** Perform symbolic execution for a node starting from an initial prop *)
-let do_symbolic_execution handle_exn cfg tenv
+let do_symbolic_execution handle_exn tenv
     (node : Cfg.node) (prop: Prop.normal Prop.t) (path : Paths.Path.t) =
   let pdesc = Cfg.Node.get_proc_desc node in
   State.mark_execution_start node;
@@ -452,7 +452,7 @@ let do_symbolic_execution handle_exn cfg tenv
   let instrs = Cfg.Node.get_instrs node in
   Ident.update_name_generator (instrs_get_normal_vars instrs); (* fresh normal vars must be fresh w.r.t. instructions *)
   let pset =
-    SymExec.lifted_sym_exec handle_exn cfg tenv pdesc
+    SymExec.lifted_sym_exec handle_exn tenv pdesc
       (Paths.PathSet.from_renamed_list [(prop, path)]) node instrs in
   L.d_strln ".... After Symbolic Execution ....";
   Propset.d prop (Paths.PathSet.to_propset pset);
@@ -469,7 +469,7 @@ let mark_visited summary node =
   else
     stats.Specs.nodes_visited_re <- IntSet.add node_id stats.Specs.nodes_visited_re
 
-let forward_tabulate cfg tenv wl =
+let forward_tabulate tenv wl =
   let handled_some_exception = ref false in
   let handle_exn curr_node exn =
     let curr_pdesc = Cfg.Node.get_proc_desc curr_node in
@@ -550,7 +550,7 @@ let forward_tabulate cfg tenv wl =
                  L.d_increase_indent 1;
                  State.reset_diverging_states_goto_node ();
                  let pset =
-                   do_symbolic_execution (handle_exn curr_node) cfg tenv curr_node prop path in
+                   do_symbolic_execution (handle_exn curr_node) tenv curr_node prop path in
                  L.d_decrease_indent 1; L.d_ln();
                  propagate_nodes_divergence tenv proc_desc pset succ_nodes exn_nodes wl;
                with
@@ -793,7 +793,7 @@ let initial_prop_from_pre tenv curr_f pre =
     initial_prop tenv curr_f pre false
 
 (** Re-execute one precondition and return some spec if there was no re-execution error. *)
-let execute_filter_prop wl cfg tenv pdesc init_node (precondition : Prop.normal Specs.Jprop.t)
+let execute_filter_prop wl tenv pdesc init_node (precondition : Prop.normal Specs.Jprop.t)
   : Prop.normal Specs.spec option =
   let proc_name = Cfg.Procdesc.get_proc_name pdesc in
   do_before_node 0 init_node;
@@ -807,7 +807,7 @@ let execute_filter_prop wl cfg tenv pdesc init_node (precondition : Prop.normal
   try
     Worklist.add wl init_node;
     ignore (path_set_put_todo wl init_node init_edgeset);
-    forward_tabulate cfg tenv wl;
+    forward_tabulate tenv wl;
     do_before_node 0 init_node;
     L.d_strln_color Green ("#### Finished: RE-execution for " ^ Procname.to_string proc_name ^ " ####");
     L.d_increase_indent 1;
@@ -855,7 +855,7 @@ let pp_intra_stats wl proc_desc fmt _ =
     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 cfg tenv (pname : Procname.t) (pdesc : Cfg.Procdesc.t)
+let perform_analysis_phase tenv (pname : Procname.t) (pdesc : Cfg.Procdesc.t)
   : (unit -> unit) * (unit -> Prop.normal Specs.spec list * Specs.phase) =
   let start_node = Cfg.Procdesc.get_start_node pdesc in
 
@@ -890,8 +890,7 @@ let perform_analysis_phase cfg tenv (pname : Procname.t) (pdesc : Cfg.Procdesc.t
       Worklist.add wl start_node;
       Config.arc_mode := Hashtbl.mem (Cfg.Procdesc.get_flags pdesc) Mleak_buckets.objc_arc_flag;
       ignore (path_set_put_todo wl start_node init_edgeset);
-      forward_tabulate cfg tenv wl
-    in
+      forward_tabulate tenv wl in
     let get_results (wl : Worklist.t) () =
       State.process_execution_failures Reporting.log_warning pname;
       let results = collect_analysis_result wl pdesc in
@@ -923,7 +922,7 @@ let perform_analysis_phase cfg tenv (pname : Procname.t) (pdesc : Cfg.Procdesc.t
       check_recursion_level ();
       let filter p =
         let wl = path_set_create_worklist pdesc in
-        let speco = execute_filter_prop wl cfg tenv pdesc start_node p in
+        let speco = execute_filter_prop wl tenv pdesc start_node p in
         let is_valid = match speco with
           | None -> false
           | Some spec ->
@@ -1166,19 +1165,13 @@ let update_summary prev_summary specs phase proc_name elapsed res =
   }
 
 
-(** Analyze [proc_name] and return the updated summary. Use module
-    [Timeout] to call [perform_analysis_phase] with a time limit, and
-    then return the updated summary. Executed as a child process. *)
-let analyze_proc exe_env (proc_name: Procname.t) : Specs.summary =
-  if !Config.trace_anal then L.err "===analyze_proc@.";
+(** Analyze the procedure and return the resulting summary. *)
+let analyze_proc exe_env proc_desc : Specs.summary =
+  let proc_name = Cfg.Procdesc.get_proc_name proc_desc in
   let init_time = Unix.gettimeofday () in
   let tenv = Exe_env.get_tenv exe_env proc_name in
-  let cfg = Exe_env.get_cfg exe_env proc_name in
-  let proc_desc = match Cfg.Procdesc.find_from_name cfg proc_name with
-    | Some proc_desc -> proc_desc
-    | None -> assert false in
   reset_global_values proc_desc;
-  let go, get_results = perform_analysis_phase cfg tenv proc_name proc_desc in
+  let go, get_results = perform_analysis_phase tenv proc_name proc_desc in
   let res = Timeout.exe_timeout go () in
   let specs, phase = get_results () in
   let elapsed = Unix.gettimeofday () -. init_time in
@@ -1256,18 +1249,6 @@ let perform_transition exe_env proc_name =
   if Specs.get_phase proc_name == Specs.FOOTPRINT
   then transition proc_name
 
-let analyze_proc_for_ondemand exe_env proc_name =
-  let saved_footprint = !Config.footprint in
-  Config.footprint := true;
-  let summaryfp = analyze_proc exe_env proc_name in
-  Specs.add_summary proc_name summaryfp;
-  let cg = Cg.create () in
-  Cg.add_defined_node cg proc_name;
-  perform_transition exe_env proc_name;
-  Config.footprint := false;
-  let summaryre = analyze_proc exe_env proc_name in
-  Specs.add_summary proc_name summaryre;
-  Config.footprint := saved_footprint
 
 let interprocedural_algorithm exe_env : unit =
   let call_graph = Exe_env.get_cg exe_env in
@@ -1306,7 +1287,6 @@ let interprocedural_algorithm exe_env : unit =
 
 (** Perform the analysis of an exe_env *)
 let do_analysis exe_env =
-  if !Config.trace_anal then L.err "do_analysis@.";
   let cg = Exe_env.get_cg exe_env in
   let procs_and_defined_children = get_procs_and_defined_children cg in
   let get_calls caller_pdesc =
@@ -1338,12 +1318,30 @@ let do_analysis exe_env =
     procs_and_defined_children;
 
   let callbacks =
+    let get_cfg proc_name =
+      Some (Exe_env.get_cfg exe_env proc_name) in
     let get_proc_desc proc_name =
       let callee_cfg = Exe_env.get_cfg exe_env proc_name in
       Cfg.Procdesc.find_from_name callee_cfg proc_name in
     let analyze_ondemand proc_name =
-      analyze_proc_for_ondemand exe_env proc_name in
-    { Ondemand.analyze_ondemand; get_proc_desc; } in
+      match get_proc_desc proc_name with
+      | Some proc_desc ->
+          let summaryfp =
+            run_in_footprint_mode (analyze_proc exe_env) proc_desc in
+          Specs.add_summary proc_name summaryfp;
+
+          perform_transition exe_env proc_name;
+
+          let summaryre =
+            run_in_re_execution_mode (analyze_proc exe_env) proc_desc in
+          Specs.add_summary proc_name summaryre
+      | None ->
+          () in
+    {
+      Ondemand.analyze_ondemand;
+      get_cfg;
+      get_proc_desc;
+    } in
 
   Ondemand.set_callbacks callbacks;
   interprocedural_algorithm exe_env;

infer/src/backend/ondemand.ml

@@ -35,11 +35,14 @@ let read_dirs_to_analyze () =
 
 type analyze_ondemand = Procname.t -> unit
 
+type get_cfg = Procname.t -> Cfg.cfg option
+
 type get_proc_desc = Procname.t -> Cfg.Procdesc.t option
 
 type callbacks =
   {
     analyze_ondemand : analyze_ondemand;
+    get_cfg : get_cfg;
     get_proc_desc : get_proc_desc;
   }
 
@@ -108,6 +111,9 @@ let restore_global_state st =
   State.restore_state st.symexec_state;
   Timeout.resume_previous_timeout ()
 
+(** do_analysis curr_pdesc proc_name
+    performs an on-demand analysis of proc_name
+    triggered during the analysis of curr_pname. *)
 let do_analysis ~propagate_exceptions curr_pdesc callee_pname =
   let curr_pname = Cfg.Procdesc.get_proc_name curr_pdesc in
 
@@ -193,3 +199,11 @@ let do_analysis ~propagate_exceptions curr_pdesc callee_pname =
       end
   | _ ->
       () (* skipping *)
+
+(** Find a cfg for the procedure, perhaps loading it from disk. *)
+let get_cfg callee_pname =
+  match !callbacks_ref with
+  | Some callbacks ->
+      callbacks.get_cfg callee_pname
+  | None ->
+      None

infer/src/backend/ondemand.mli

@@ -14,14 +14,20 @@ val read_dirs_to_analyze : unit -> StringSet.t option
 
 type analyze_ondemand = Procname.t -> unit
 
+type get_cfg = Procname.t -> Cfg.cfg option
+
 type get_proc_desc = Procname.t -> Cfg.Procdesc.t option
 
 type callbacks =
   {
     analyze_ondemand : analyze_ondemand;
+    get_cfg : get_cfg;
     get_proc_desc : get_proc_desc;
   }
 
+(** Find a cfg for the procedure, perhaps loading it from disk. *)
+val get_cfg : get_cfg
+
 (** do_analysis curr_pdesc proc_name
     performs an on-demand analysis of proc_name
     triggered during the analysis of curr_pname. *)

infer/src/backend/procAttributes.ml

@@ -42,31 +42,6 @@ type t =
     ret_type : Sil.typ; (** return type *)
   }
 
-let copy pa =
-  {
-    access = pa.access;
-    captured = pa.captured;
-    changed = pa.changed;
-    err_log = pa.err_log;
-    exceptions = pa.exceptions;
-    formals = pa.formals;
-    func_attributes = pa.func_attributes;
-    is_abstract = pa.is_abstract;
-    is_bridge_method = pa.is_bridge_method;
-    is_cpp_instance_method = pa.is_cpp_instance_method;
-    is_defined = pa.is_defined;
-    is_objc_instance_method = pa.is_objc_instance_method;
-    is_synthetic_method = pa.is_synthetic_method;
-    language = pa.language;
-    loc = pa.loc;
-    locals = pa.locals;
-    method_annotation = pa.method_annotation;
-    objc_accessor = pa.objc_accessor;
-    proc_flags = pa.proc_flags;
-    proc_name = pa.proc_name;
-    ret_type = pa.ret_type;
-  }
-
 let default proc_name language = {
   access = Sil.Default;
   captured = [];

infer/src/backend/procAttributes.mli

@@ -38,8 +38,5 @@ type t =
     ret_type : Sil.typ; (** return type *)
   }
 
-(** Create a copy of a proc_attributes *)
-val copy : t -> t
-
 (** Create a proc_attributes with default values. *)
 val default : Procname.t -> Config.language -> t

infer/src/backend/symExec.mli

@@ -17,7 +17,7 @@ val print_builtins : unit -> unit
 val function_is_builtin : Procname.t -> bool
 
 (** symbolic execution on the level of sets of propositions *)
-val lifted_sym_exec : (exn -> unit) -> Cfg.cfg -> Sil.tenv -> Cfg.Procdesc.t ->
+val lifted_sym_exec : (exn -> unit) -> Sil.tenv -> Cfg.Procdesc.t ->
   Paths.PathSet.t -> Cfg.Node.t -> Sil.instr list -> Paths.PathSet.t
 
 (** OO method resolution: given a class name and a method name, climb the class hierarchy to find

infer/src/backend/utils.ml

@@ -1001,7 +1001,7 @@ let string_append_crc_cutoff ?(cutoff=100) ?(key="") name =
     string_crc_hex32 name_for_crc in
   name_up_to_cutoff ^ "." ^ crc_str
 
-let run_with_val reference value f x =
+let set_reference_and_call_function reference value f x =
   let saved = !reference in
   let restore () =
     reference := saved in
@@ -1015,8 +1015,11 @@ let run_with_val reference value f x =
       restore ();
       raise exn
 
-let run_with_footprint_false f x =
-  run_with_val Config.footprint false f x
+let run_in_re_execution_mode f x =
+  set_reference_and_call_function Config.footprint false f x
+
+let run_in_footprint_mode f x =
+  set_reference_and_call_function Config.footprint true f x
 
 let run_with_abs_val_equal_zero f x =
-  run_with_val Config.abs_val 0 f x
+  set_reference_and_call_function Config.abs_val 0 f x

infer/src/backend/utils.mli

@@ -371,10 +371,18 @@ val string_of_analyzer: analyzer -> string
 
 val analyzer_of_string: string -> analyzer
 
+(** Call f x with Config.abs_val set to zero.
+    Restore the initial value also in case of exception. *)
+val run_with_abs_val_equal_zero : ('a -> 'b) -> 'a -> 'b
+
+(** Call f x with Config.footprint set to true.
+    Restore the initial value of footprint also in case of exception. *)
+val run_in_footprint_mode : ('a -> 'b) -> 'a -> 'b
+
 (** Call f x with Config.footprint set to false.
     Restore the initial value of footprint also in case of exception. *)
-val run_with_footprint_false : ('a -> 'b) -> 'a -> 'b
+val run_in_re_execution_mode : ('a -> 'b) -> 'a -> 'b
 
-(** Call f x with Config.abs_val set to zero.
+(** [set_reference_and_call_function ref val f x] calls f x with ref set to val.
     Restore the initial value also in case of exception. *)
-val run_with_abs_val_equal_zero : ('a -> 'b) -> 'a -> 'b
+val set_reference_and_call_function : 'a ref -> 'a -> ('b -> 'c) -> 'b -> 'c

infer/src/checkers/performanceCritical.ml

@@ -314,13 +314,18 @@ let check_one_procedure tenv pname pdesc =
     report_allocations tenv pname pdesc loc call_summary.Specs.allocations
 
 
-let callback_performance_checker { Callbacks.proc_desc; proc_name; get_proc_desc; tenv } =
+let callback_performance_checker
+    { Callbacks.get_cfg; get_proc_desc; proc_desc; proc_name; tenv } =
   let callbacks =
     let analyze_ondemand pn =
       match get_proc_desc pn with
       | None -> ()
       | Some pd -> check_one_procedure tenv pn pd in
-    { Ondemand.analyze_ondemand; get_proc_desc; } in
+    {
+      Ondemand.analyze_ondemand;
+      get_cfg;
+      get_proc_desc;
+    } in
   if Ondemand.procedure_should_be_analyzed proc_name
   then
     begin

infer/src/eradicate/eradicate.ml

@@ -385,7 +385,8 @@ module Main =
   Build(EmptyExtension)
 
 (** Eradicate checker for Java @Nullable annotations. *)
-let callback_eradicate ({ Callbacks.get_proc_desc; idenv; proc_name } as callback_args) =
+let callback_eradicate
+    ({ Callbacks.get_cfg; get_proc_desc; idenv; proc_name } as callback_args) =
   let checks =
     {
       TypeCheck.eradicate = true;
@@ -403,7 +404,11 @@ let callback_eradicate ({ Callbacks.get_proc_desc; idenv; proc_name } as callbac
               Callbacks.idenv = idenv_pname;
               proc_name = pname;
               proc_desc = pdesc; } in
-    { Ondemand.analyze_ondemand; get_proc_desc; } in
+    {
+      Ondemand.analyze_ondemand;
+      get_cfg;
+      get_proc_desc;
+    } in
 
   if Ondemand.procedure_should_be_analyzed proc_name
   then