one more instance of SummaryReporting gone

Summary: Trying to be nice removing now-useless `tenv` arguments too.

Reviewed By: dulmarod

Differential Revision: D21261642

fbshipit-source-id: b95c8902a

infer/src/biabduction/Abs.ml

@@ -1199,7 +1199,7 @@ functions in Prop abstain from dropping free variables. Here, however, we can do
 atom an orphan when it contains a variable v that does not occur anywhere else in the spec. Orphans
 can be dropped. Alpha-renaming can create orphans. Thus, we will perform a best-effort fixpoint
 computation (rename, drop)*, stopping when the last drop is a no-op. *)
-let abstract_spec pname tenv spec =
+let abstract_spec ({InterproceduralAnalysis.tenv; _} as analysis_data) spec =
   let open BiabductionSummary in
   let rename spec = spec_normalize tenv spec in
   let drop spec =
@@ -1239,7 +1239,7 @@ let abstract_spec pname tenv spec =
       let toprove = AtomSet.of_list prop2.Prop.pi in
       let toprove = AtomSet.diff toprove known in
       let prop2 = Prop.set prop2 ~pi:(AtomSet.elements toprove) in
-      Prover.check_implication pname tenv prop1 prop2
+      Prover.check_implication analysis_data prop1 prop2
     in
     let rec filter kept x unseen =
       (* INV: if a is kept and b is kept or unseen then (not (implies a b)).

infer/src/biabduction/Abs.mli

@@ -18,7 +18,9 @@ val abstract :
 (** Abstract a proposition. *)
 
 val abstract_spec :
-  Procname.t -> Tenv.t -> Prop.normal BiabductionSummary.spec -> BiabductionSummary.NormSpec.t
+     BiabductionSummary.t InterproceduralAnalysis.t
+  -> Prop.normal BiabductionSummary.spec
+  -> BiabductionSummary.NormSpec.t
 (** Normalizes names and applies simplifications, soem of which require looking at both pre and
     post. *)
 

infer/src/biabduction/Dom.ml

@@ -1974,11 +1974,11 @@ let footprint_partial_join' tenv (p1 : Prop.normal Prop.t) (p2 : Prop.normal Pro
     (Prop.normalize tenv ep1', Prop.normalize tenv ep2')
 
 
-let prop_partial_join pname tenv mode p1 p2 =
+let prop_partial_join ({InterproceduralAnalysis.tenv; _} as analysis_data) mode p1 p2 =
   let res_by_implication_only =
     if !BiabductionConfig.footprint then None
-    else if Prover.check_implication pname tenv p1 (Prop.expose p2) then Some p2
-    else if Prover.check_implication pname tenv p2 (Prop.expose p1) then Some p1
+    else if Prover.check_implication analysis_data p1 (Prop.expose p2) then Some p2
+    else if Prover.check_implication analysis_data p2 (Prop.expose p1) then Some p1
     else None
   in
   match res_by_implication_only with
@@ -2092,8 +2092,8 @@ let proplist_collapse_pre tenv plist =
   List.map ~f:fst (proplist_collapse tenv JoinState.Pre plist')
 
 
-let pathset_join pname tenv (pset1 : Paths.PathSet.t) (pset2 : Paths.PathSet.t) :
-    Paths.PathSet.t * Paths.PathSet.t =
+let pathset_join ({InterproceduralAnalysis.tenv; _} as analysis_data) (pset1 : Paths.PathSet.t)
+    (pset2 : Paths.PathSet.t) : Paths.PathSet.t * Paths.PathSet.t =
   let mode = JoinState.Post in
   let rec join_proppath_plist ppalist2_acc ((p2, pa2) as ppa2) = function
     | [] ->
@@ -2107,7 +2107,7 @@ let pathset_join pname tenv (pset1 : Paths.PathSet.t) (pset2 : Paths.PathSet.t)
         Prop.d_prop p2' ;
         L.d_ln () ;
         L.d_ln () ;
-        match prop_partial_join pname tenv mode p2 p2' with
+        match prop_partial_join analysis_data mode p2 p2' with
         | None ->
             L.d_strln ~color:Red ".... JOIN FAILED ...." ;
             L.d_ln () ;

infer/src/biabduction/Dom.mli

@@ -13,7 +13,10 @@ open! IStd
 (** {2 Join Operators} *)
 
 val pathset_join :
-  Procname.t -> Tenv.t -> Paths.PathSet.t -> Paths.PathSet.t -> Paths.PathSet.t * Paths.PathSet.t
+     BiabductionSummary.t InterproceduralAnalysis.t
+  -> Paths.PathSet.t
+  -> Paths.PathSet.t
+  -> Paths.PathSet.t * Paths.PathSet.t
 (** Join two pathsets *)
 
 val proplist_collapse_pre :

infer/src/biabduction/Prover.ml

@@ -2507,7 +2507,8 @@ let check_array_bounds tenv (sub1, sub2) prop =
 
 (** [check_implication_base] returns true if [prop1|-prop2], ignoring the footprint part of the
     props *)
-let check_implication_base pname tenv check_frame_empty calc_missing prop1 prop2 =
+let check_implication_base {InterproceduralAnalysis.proc_desc; err_log; tenv} check_frame_empty
+    calc_missing prop1 prop2 =
   try
     ProverState.reset prop1 prop2 ;
     let filter (id, e) =
@@ -2573,7 +2574,8 @@ let check_implication_base pname tenv check_frame_empty calc_missing prop1 prop2
       L.d_printfln "WARNING: footprint failed to find MISSING because: %s" s ;
       None
   | Exceptions.Abduction_case_not_implemented _ as exn ->
-      SummaryReporting.log_issue_deprecated_using_state Exceptions.Error pname exn ;
+      let proc_attrs = Procdesc.get_attributes proc_desc in
+      BiabductionReporting.log_issue_deprecated_using_state proc_attrs err_log Exceptions.Error exn ;
       None
 
 
@@ -2594,10 +2596,10 @@ type implication_result =
 (** [check_implication_for_footprint p1 p2] returns [Some(sub, frame, missing)] if
     [sub(p1 * missing) |- sub(p2 * frame)] where [sub] is a substitution which instantiates the
     primed vars of [p1] and [p2], which are assumed to be disjoint. *)
-let check_implication_for_footprint pname tenv p1 (p2 : Prop.exposed Prop.t) =
+let check_implication_for_footprint analysis_data p1 (p2 : Prop.exposed Prop.t) =
   let check_frame_empty = false in
   let calc_missing = true in
-  match check_implication_base pname tenv check_frame_empty calc_missing p1 p2 with
+  match check_implication_base analysis_data check_frame_empty calc_missing p1 p2 with
   | Some ((sub1, sub2), frame) ->
       ImplOK
         ( !ProverState.checks
@@ -2615,11 +2617,11 @@ let check_implication_for_footprint pname tenv p1 (p2 : Prop.exposed Prop.t) =
 
 
 (** [check_implication p1 p2] returns true if [p1|-p2] *)
-let check_implication pname tenv p1 p2 =
+let check_implication ({InterproceduralAnalysis.tenv; _} as analysis_data) p1 p2 =
   let check p1 p2 =
     let check_frame_empty = true in
     let calc_missing = false in
-    match check_implication_base pname tenv check_frame_empty calc_missing p1 p2 with
+    match check_implication_base analysis_data check_frame_empty calc_missing p1 p2 with
     | Some _ ->
         true
     | None ->

infer/src/biabduction/Prover.mli

@@ -59,7 +59,11 @@ val get_bounds : Tenv.t -> Prop.normal Prop.t -> Exp.t -> IntLit.t option * IntL
 
 (** {2 Abduction prover} *)
 
-val check_implication : Procname.t -> Tenv.t -> Prop.normal Prop.t -> Prop.exposed Prop.t -> bool
+val check_implication :
+     BiabductionSummary.t InterproceduralAnalysis.t
+  -> Prop.normal Prop.t
+  -> Prop.exposed Prop.t
+  -> bool
 (** [check_implication p1 p2] returns true if [p1|-p2] *)
 
 type check = Bounds_check | Class_cast_check of Exp.t * Exp.t * Exp.t
@@ -81,7 +85,10 @@ type implication_result =
   | ImplFail of check list
 
 val check_implication_for_footprint :
-  Procname.t -> Tenv.t -> Prop.normal Prop.t -> Prop.exposed Prop.t -> implication_result
+     BiabductionSummary.t InterproceduralAnalysis.t
+  -> Prop.normal Prop.t
+  -> Prop.exposed Prop.t
+  -> implication_result
 (** [check_implication_for_footprint p1 p2] returns [Some(sub, frame, missing)] if
     [sub(p1 * missing) |- sub(p2 * frame)] where [sub] is a substitution which instantiates the
     primed vars of [p1] and [p2], which are assumed to be disjoint. *)

infer/src/biabduction/Tabulation.ml

@@ -1070,9 +1070,9 @@ let add_missing_field_to_tenv ~missing_sigma exe_env caller_tenv callee_pname hp
 
 
 (** Perform symbolic execution for a single spec *)
-let exe_spec exe_env tenv ret_id (n, nspecs) caller_pdesc callee_pname loc prop path_pre
-    (spec : Prop.exposed BiabductionSummary.spec) actual_params formal_params callee_summary :
-    abduction_res =
+let exe_spec ({InterproceduralAnalysis.exe_env; tenv; _} as analysis_data) ret_id (n, nspecs)
+    caller_pdesc callee_pname loc prop path_pre (spec : Prop.exposed BiabductionSummary.spec)
+    actual_params formal_params callee_summary : abduction_res =
   let caller_pname = Procdesc.get_proc_name caller_pdesc in
   let posts = mk_posts tenv prop callee_pname spec.BiabductionSummary.posts in
   let actual_pre = mk_actual_precondition tenv prop actual_params formal_params in
@@ -1090,7 +1090,7 @@ let exe_spec exe_env tenv ret_id (n, nspecs) caller_pdesc callee_pname loc prop
   L.d_ln () ;
   SymOp.pay () ;
   (* pay one symop *)
-  match Prover.check_implication_for_footprint caller_pname tenv actual_pre spec_pre with
+  match Prover.check_implication_for_footprint analysis_data actual_pre spec_pre with
   | Prover.ImplFail checks ->
       Invalid_res (Prover_checks checks)
   | Prover.ImplOK
@@ -1373,7 +1373,7 @@ let exe_call_postprocess tenv ret_id callee_pname callee_attrs loc results =
 
 
 (** Execute the function call and return the list of results with return value *)
-let exe_function_call {InterproceduralAnalysis.exe_env; proc_desc= caller_pdesc; tenv}
+let exe_function_call ({InterproceduralAnalysis.proc_desc= caller_pdesc; tenv} as analysis_data)
     ~callee_attributes ~callee_pname ~callee_summary ~ret_id loc ~actuals prop path =
   let spec_list, formal_params =
     spec_find_rename callee_attributes (BiabductionSummary.get_specs callee_summary)
@@ -1384,7 +1384,7 @@ let exe_function_call {InterproceduralAnalysis.exe_env; proc_desc= caller_pdesc;
   Prop.d_prop prop ;
   L.d_ln () ;
   let exe_one_spec (n, spec) =
-    exe_spec exe_env tenv ret_id (n, nspecs) caller_pdesc callee_pname loc prop path spec actuals
+    exe_spec analysis_data ret_id (n, nspecs) caller_pdesc callee_pname loc prop path spec actuals
       formal_params callee_attributes
   in
   let results = List.map ~f:exe_one_spec spec_list in

infer/src/biabduction/interproc.ml

@@ -309,12 +309,12 @@ let propagate_nodes_divergence ({InterproceduralAnalysis.tenv; _} as analysis_da
 (* =============== START of forward_tabulate =============== *)
 
 (** Symbolic execution for a Join node *)
-let do_symexec_join proc_cfg tenv wl curr_node (edgeset_todo : Paths.PathSet.t) =
+let do_symexec_join analysis_data proc_cfg wl curr_node (edgeset_todo : Paths.PathSet.t) =
   let pname = Procdesc.get_proc_name (ProcCfg.Exceptional.proc_desc proc_cfg) in
   let curr_node_id = ProcCfg.Exceptional.Node.id curr_node in
   let new_dset = edgeset_todo in
   let old_dset = Join_table.find wl.Worklist.join_table curr_node_id in
-  let old_dset', new_dset' = Dom.pathset_join pname tenv old_dset new_dset in
+  let old_dset', new_dset' = Dom.pathset_join analysis_data old_dset new_dset in
   Join_table.add wl.Worklist.join_table curr_node_id (Paths.PathSet.union old_dset' new_dset') ;
   Container.iter curr_node ~fold:(ProcCfg.Exceptional.fold_normal_succs proc_cfg) ~f:(fun node ->
       Paths.PathSet.iter
@@ -448,7 +448,7 @@ let forward_tabulate ({InterproceduralAnalysis.tenv; _} as analysis_data) proc_c
     print_node_preamble curr_node pathset_todo ;
     match Procdesc.Node.get_kind curr_node with
     | Join_node ->
-        do_symexec_join proc_cfg tenv wl curr_node pathset_todo
+        do_symexec_join analysis_data proc_cfg wl curr_node pathset_todo
     | Stmt_node _ | Prune_node _ | Exit_node | Skip_node _ | Start_node ->
         exe_iter (do_prop curr_node handle_exn) pathset_todo
   in
@@ -932,7 +932,7 @@ module SpecMap = Caml.Map.Make (struct
 end)
 
 (** Update the specs of the current proc after the execution of one phase *)
-let update_specs {InterproceduralAnalysis.proc_desc; tenv} prev_summary_opt phase
+let update_specs analysis_data prev_summary_opt phase
     (new_specs : BiabductionSummary.NormSpec.t list) : BiabductionSummary.NormSpec.t list * bool =
   let new_specs = BiabductionSummary.normalized_specs_to_specs new_specs in
   let old_specs = Option.value_map ~default:[] ~f:BiabductionSummary.get_specs prev_summary_opt in
@@ -986,10 +986,9 @@ let update_specs {InterproceduralAnalysis.proc_desc; tenv} prev_summary_opt phas
   in
   let res = ref [] in
   let convert pre (post_set, visited) =
-    let pname = Procdesc.get_proc_name proc_desc in
     res :=
-      Abs.abstract_spec pname tenv
-        BiabductionSummary.{pre; posts= Paths.PathSet.elements post_set; visited}
+      Abs.abstract_spec analysis_data
+        {BiabductionSummary.pre; posts= Paths.PathSet.elements post_set; visited}
       :: !res
   in
   List.iter ~f:re_exe_filter old_specs ;