From f49ba50d29e661530aecec64e17e440be2cb093b Mon Sep 17 00:00:00 2001
From: Valentin Perrelle <valentin.perrelle@cea.fr>
Date: Fri, 8 Mar 2019 16:32:09 +0100
Subject: [PATCH] [Dive] Add an output to json format
---
src/plugins/dive/imprecision_graph.ml | 61 ++++++++++++++++++++++++++
src/plugins/dive/imprecision_graph.mli | 1 +
src/plugins/dive/main.ml | 24 ++++++----
src/plugins/dive/self.ml | 13 ++++--
src/plugins/dive/self.mli | 3 +-
5 files changed, 90 insertions(+), 12 deletions(-)
diff --git a/src/plugins/dive/imprecision_graph.ml b/src/plugins/dive/imprecision_graph.ml
index 3f0979ffefd..ebb0ce5808c 100644
--- a/src/plugins/dive/imprecision_graph.ml
+++ b/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
diff --git a/src/plugins/dive/imprecision_graph.mli b/src/plugins/dive/imprecision_graph.mli
index 9598baf375d..46a60f58d55 100644
--- a/src/plugins/dive/imprecision_graph.mli
+++ b/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
diff --git a/src/plugins/dive/main.ml b/src/plugins/dive/main.ml
index 1f7419db4e3..20949175f5e 100644
--- a/src/plugins/dive/main.ml
+++ b/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 () =
diff --git a/src/plugins/dive/self.ml b/src/plugins/dive/self.ml
index 73639f3d05f..e4666b27580 100644
--- a/src/plugins/dive/self.ml
+++ b/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)
diff --git a/src/plugins/dive/self.mli b/src/plugins/dive/self.mli
index 77fdb5a3f8f..9adf345bcc7 100644
--- a/src/plugins/dive/self.mli
+++ b/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
--
GitLab