[Dive] Add an output to json format

src/plugins/dive/imprecision_graph.ml

@@ -175,3 +175,64 @@ let ouptput_to_dot out_channel g =
     end)
   in
   Dot.output_graph out_channel g
+
+let ouptput_to_json out_channel g =
+  let output_node_kind kind =
+    let s = match kind with
+      | Scalar _ -> "scalar"
+      | Composite _ -> "composite"
+      | Scattered _ -> "scattered"
+      | Alarm _ -> "alarm"
+      | File -> "dummy"
+    in
+    Json.of_string s
+  and output_node_locality { loc_file ; loc_function } =
+    let f1 = ("file", Json.of_string loc_file) in
+    let fields = match loc_function with
+      | None -> [f1]
+      | Some kf -> [f1 ; ("fun", Json.of_string (Kernel_function.get_name kf))]
+    in
+    Json.of_fields fields
+  and output_node_precision precision =
+    let s = match precision with
+      | Unevaluated -> "unevaluated"
+      | Singleton -> "singleton"
+      | Normal -> "normal"
+      | Wide -> "wide"
+      | Critical -> "critical"
+    in
+    Json.of_string s
+  and output_dep_kind kind =
+    let s = match kind with
+      | Callee -> "callee"
+      | Data -> "data"
+      | Address -> "addr"
+      | Control -> "ctrl"
+    in
+    Json.of_string s
+  in
+  let output_node node acc =
+    if node.node_kind = File then acc
+    else
+      let label = Pretty_utils.to_string Node_kind.pretty node.node_kind in
+      Json.of_fields [
+        ("id", Json.of_int node.node_key) ;
+        ("label", Json.of_string label) ;
+        ("kind", output_node_kind node.node_kind) ;
+        ("locality", output_node_locality node.node_locality) ;
+        ("precision", output_node_precision node.node_precision) ;
+        ("explored", Json.of_bool node.node_deps_computed)
+      ] :: acc
+  and output_dep (n1,dep,n2) acc =
+    Json.of_fields [
+      ("id", Json.of_int dep.dependency_key) ;
+      ("src", Json.of_int n1.node_key) ;
+      ("dst", Json.of_int n2.node_key) ;
+      ("kind", output_dep_kind dep.dependency_kind) ;
+      ("multiple", Json.of_bool dep.dependency_multiple)
+    ] :: acc
+  in
+  let nodes = Json.of_list (fold_vertex output_node g [])
+  and deps = Json.of_list (fold_edges_e output_dep g []) in
+  let json = Json.of_fields [("nodes", nodes) ; ("deps", deps)] in
+  Json.save_channel ~pretty:true out_channel json
\ No newline at end of file

src/plugins/dive/imprecision_graph.mli

@@ -37,3 +37,4 @@ val create_dependency : allow_folding:bool -> t -> node -> dependency_kind ->
   node -> unit
 
 val ouptput_to_dot : out_channel -> t -> unit
+val ouptput_to_json : out_channel -> t -> unit

src/plugins/dive/main.ml

@@ -20,6 +20,18 @@
 (*                                                                        *)
 (**************************************************************************)
 
+type format = Dot | Json
+
+let output format context basename =
+  let filename, output_function = match format with
+    | Dot -> basename ^ ".dot", Imprecision_graph.ouptput_to_dot
+    | Json -> basename ^ ".json", Imprecision_graph.ouptput_to_json
+  in
+  Self.result "output to %s" filename;
+  let out_channel = open_out filename in
+  output_function out_channel (Build.get_graph context);
+  close_out out_channel
+
 let main () =
   if not (Self.FromBases.is_empty () &&
           Self.FromFunctionAlarms.is_empty ()) then begin
@@ -39,14 +51,10 @@ let main () =
     if not (Self.FromFunctionAlarms.is_empty ()) then
       Alarms.iter add_alarm;
     (* Output it *)
-    let output_basename = Self.OutputBasename.get () in
-    if output_basename <> "" then begin
-      let filename = output_basename ^ ".dot" in
-      Self.result "output to %s" filename;
-      let out_channel = open_out filename in
-      Imprecision_graph.ouptput_to_dot out_channel (Build.get_graph context);
-      close_out out_channel
-    end;
+    if Self.OutputDot.get () <> "" then
+      output Dot context (Self.OutputDot.get ());
+    if Self.OutputJson.get () <> "" then
+      output Json context (Self.OutputJson.get ());
   end
 
 let () =

src/plugins/dive/self.ml

@@ -29,10 +29,17 @@ include Plugin.Register
       let help = "An interactive imprecision graph generator."
     end)
 
-module OutputBasename = Empty_string
+module OutputDot = Empty_string
     (struct
-      let option_name = "-dive-output"
-      let help = "Outputs the built graph into a file with this basename."
+      let option_name = "-dive-output-dot"
+      let help = "Outputs the built graph into a dot file with this basename."
+      let arg_name = "basename"
+    end)
+
+module OutputJson = Empty_string
+    (struct
+      let option_name = "-dive-output-json"
+      let help = "Outputs the built graph into a json file with this basename."
       let arg_name = "basename"
     end)
 

src/plugins/dive/self.mli

@@ -26,7 +26,8 @@ module type Varinfo_set = Parameter_sig.Set
   with type elt = Cil_types.varinfo
    and type t = Cil_datatype.Varinfo.Set.t
 
-module OutputBasename : Parameter_sig.String
+module OutputDot : Parameter_sig.String
+module OutputJson : Parameter_sig.String
 module DepthLimit : Parameter_sig.Int
 module FromFunctionAlarms : Parameter_sig.Kernel_function_set
 module FromBases : Varinfo_set