[infer] remove the field `nodes` in the summary definition

Summary:
This field was always empty.

depends on D6351097

Reviewed By: sblackshear, jvillard

Differential Revision: D6351243

fbshipit-source-id: 4a74bea

infer/src/backend/InferPrint.ml

@@ -133,8 +133,6 @@ type summary_val =
   ; vflags: ProcAttributes.proc_flags
   ; vline: int
   ; vsignature: string
-  ; vweight: int
-  ; vproof_coverage: string
   ; vproof_trace: string }
 
 (** compute values from summary data to export to csv format *)
@@ -144,9 +142,8 @@ let summary_values summary =
   let err_log = Specs.get_err_log summary in
   let proc_name = Specs.get_proc_name summary in
   let signature = Specs.get_signature summary in
-  let nodes_nr = List.length summary.Specs.nodes in
   let specs = Specs.get_specs_from_payload summary in
-  let nr_nodes_visited, lines_visited =
+  let lines_visited =
     let visited = ref Specs.Visitedset.empty in
     let do_spec spec = visited := Specs.Visitedset.union spec.Specs.visited !visited in
     List.iter ~f:do_spec specs ;
@@ -154,16 +151,13 @@ let summary_values summary =
     Specs.Visitedset.iter
       (fun (_, ls) -> List.iter ~f:(fun l -> visited_lines := Int.Set.add !visited_lines l) ls)
       !visited ;
-    (Specs.Visitedset.cardinal !visited, Int.Set.elements !visited_lines)
+    Int.Set.elements !visited_lines
   in
   let proof_trace =
     let pp_line fmt l = F.fprintf fmt "%d" l in
     let pp fmt = F.fprintf fmt "%a" (Pp.seq pp_line) lines_visited in
     F.asprintf "%t" pp
   in
-  let node_coverage =
-    if Int.equal nodes_nr 0 then 0.0 else float_of_int nr_nodes_visited /. float_of_int nodes_nr
-  in
   let pp_failure failure = F.asprintf "%a" SymOp.pp_failure_kind failure in
   { vname= Typ.Procname.to_string proc_name
   ; vname_id= Typ.Procname.to_filename proc_name
@@ -179,8 +173,6 @@ let summary_values summary =
   ; vfile= SourceFile.to_string attributes.ProcAttributes.loc.Location.file
   ; vline= attributes.ProcAttributes.loc.Location.line
   ; vsignature= signature
-  ; vweight= nodes_nr
-  ; vproof_coverage= Printf.sprintf "%2.2f" node_coverage
   ; vproof_trace= proof_trace }
 
 
@@ -208,8 +200,6 @@ module ProcsCsv = struct
     pp "%s," sv.vfile ;
     pp "%d," sv.vline ;
     pp "\"%s\"," (Escape.escape_csv sv.vsignature) ;
-    pp "%d," sv.vweight ;
-    pp "%s," sv.vproof_coverage ;
     pp "%s@\n" sv.vproof_trace
 
 end
@@ -1241,4 +1231,3 @@ let main ~report_csv ~report_json =
       pp_json_report_by_report_kind formats_by_report_kind fname
   | None ->
       pp_summary_and_issues formats_by_report_kind issue_formats
-

infer/src/backend/specs.ml

@@ -356,8 +356,7 @@ type payload =
   ; uninit: UninitDomain.summary option }
 
 type summary =
-  { nodes: Procdesc.Node.id list  (** ids of cfg nodes of the procedure *)
+  { phase: phase  (** in FOOTPRINT phase or in RE_EXECUTION PHASE *)
-  ; phase: phase  (** in FOOTPRINT phase or in RE_EXECUTION PHASE *)
   ; payload: payload  (** payload containing the result of some analysis *)
   ; sessions: int ref  (** Session number: how many nodes went trough symbolic execution *)
   ; stats: stats  (** statistics: execution time and list of errors *)
@@ -756,8 +755,7 @@ let empty_payload =
     initializes the summary for [proc_name] given dependent procs in list [depend_list]. *)
 let init_summary proc_desc =
   let summary =
-    { nodes= [] (* TODO(T23648322): remove this information from the summary *)
+    { phase= FOOTPRINT
-    ; phase= FOOTPRINT
     ; sessions= ref 0
     ; payload= empty_payload
     ; stats= empty_stats

infer/src/backend/specs.mli

@@ -142,8 +142,7 @@ type payload =
 
 (** Procedure summary *)
 type summary =
-  { nodes: Procdesc.Node.id list  (** ids of cfg nodes of the procedure *)
+  { phase: phase  (** in FOOTPRINT phase or in RE_EXECUTION PHASE *)
-  ; phase: phase  (** in FOOTPRINT phase or in RE_EXECUTION PHASE *)
   ; payload: payload  (** payload containing the result of some analysis *)
   ; sessions: int ref  (** Session number: how many nodes went trough symbolic execution *)
   ; stats: stats  (** statistics: execution time and list of errors *)

infer/src/eradicate/eradicate.ml

@@ -41,14 +41,12 @@ end
 (** Create a module with the toplevel callback. *)
 module MkCallback (Extension : ExtensionT) : CallBackT = struct
   (** Update the summary with stats from the checker. *)
-  let update_summary proc_name proc_desc final_typestate_opt =
+  let update_summary proc_name final_typestate_opt =
     match Specs.get_summary proc_name with
     | Some old_summ ->
-        let nodes = List.map ~f:(fun n -> Procdesc.Node.get_id n) (Procdesc.get_nodes proc_desc) in
         let new_summ =
           { old_summ with
-            Specs.nodes
+            Specs.payload= Extension.update_payload final_typestate_opt old_summ.Specs.payload }
-          ; Specs.payload= Extension.update_payload final_typestate_opt old_summ.Specs.payload }
         in
         Specs.add_summary proc_name new_summ
     | None ->
@@ -323,7 +321,7 @@ module MkCallback (Extension : ExtensionT) : CallBackT = struct
       EradicateChecks.check_overridden_annotations find_canonical_duplicate tenv curr_pname
         curr_pdesc annotated_signature ;
     TypeErr.report_forall_checks_and_reset tenv (Checkers.ST.report_error tenv) curr_pdesc ;
-    update_summary curr_pname curr_pdesc final_typestate_opt
+    update_summary curr_pname final_typestate_opt
 
 
   (** Entry point for the eradicate-based checker infrastructure. *)
@@ -392,3 +390,4 @@ let callback_check_return_type check_return_type callback_args =
     {TypeCheck.eradicate= false; check_extension= false; check_ret_type= [check_return_type]}
   in
   Main.callback checks callback_args
+