From bba61bda772b3e1d24cc61c8a26aadce50f945f9 Mon Sep 17 00:00:00 2001
From: Valentin Perrelle <valentin.perrelle@cea.fr>
Date: Wed, 28 Aug 2019 17:30:51 +0200
Subject: [PATCH] [Dive] More input checks and use of Yojson
---
src/plugins/dive/build.ml | 19 ++++---
src/plugins/dive/build.mli | 9 ++-
src/plugins/dive/imprecision_graph.ml | 76 ++++++++++++-------------
src/plugins/dive/server_interface.ml | 82 +++++++++++++++++++++------
4 files changed, 122 insertions(+), 64 deletions(-)
diff --git a/src/plugins/dive/build.ml b/src/plugins/dive/build.ml
index ba98a800bf7..d7bdb9f1076 100644
--- a/src/plugins/dive/build.ml
+++ b/src/plugins/dive/build.ml
@@ -252,7 +252,7 @@ let is_hidden context node_kind =
| Some vi when BaseSet.mem vi context.hidden_bases -> true
| _ -> false
-let get_node context node_key =
+let find_node context node_key =
Index.find context.vertex_table node_key
let update_node context node =
@@ -601,16 +601,21 @@ let add_alarm ?(depth=1) context stmt alarm =
let node = build_alarm context callstack stmt alarm in
complete_in_depth ~depth context node
-let explore_from_vertex ~depth context node_key =
- explore ~depth context (get_node context node_key)
+let add_function_alarms ?(depth=1) context kf =
+ let add_one_alarm _emitter kf' stmt ~rank:_ alarm _code_annot =
+ if Kernel_function.equal kf' kf then
+ add_alarm ~depth context stmt alarm
+ in
+ Alarms.iter add_one_alarm
+
+let explore_from_node ~depth context node =
+ explore ~depth context node
-let show ?(depth=1) context node_key =
- let node = get_node context node_key in
+let show ?(depth=1) context node =
node.node_hidden <- false;
explore ~depth context node
-let hide context node_key =
- let node = get_node context node_key in
+let hide context node =
if not node.node_hidden then
begin
let g = get_graph context in
diff --git a/src/plugins/dive/build.mli b/src/plugins/dive/build.mli
index e3e345a3e82..7bd5f3af5ad 100644
--- a/src/plugins/dive/build.mli
+++ b/src/plugins/dive/build.mli
@@ -34,12 +34,15 @@ val fold_base : t -> Cil_types.varinfo -> unit
val hide_base : t -> Cil_types.varinfo -> unit
val unhide_base : t -> Cil_types.varinfo -> unit
+val find_node : t -> int -> Graph_types.node
+
val add_lval : ?depth:int -> t -> Cil_types.kinstr -> Cil_types.lval -> unit
val add_var : ?depth:int -> t -> Cil_types.varinfo -> unit
val add_alarm : ?depth:int -> t -> Cil_types.stmt -> Alarms.alarm -> unit
-val explore_from_vertex : depth:int -> t -> int -> unit
+val add_function_alarms : ?depth:int -> t -> Cil_types.kernel_function -> unit
+val explore_from_node : depth:int -> t -> Graph_types.node -> unit
-val show : ?depth:int -> t -> int -> unit
-val hide : t -> int -> unit
+val show : ?depth:int -> t -> Graph_types.node -> unit
+val hide : t -> Graph_types.node -> unit
val take_last_differences : t -> Graph_types.graph_diff
diff --git a/src/plugins/dive/imprecision_graph.ml b/src/plugins/dive/imprecision_graph.ml
index 86edf4c918c..9efa403a971 100644
--- a/src/plugins/dive/imprecision_graph.ml
+++ b/src/plugins/dive/imprecision_graph.ml
@@ -248,17 +248,17 @@ let ouptput_to_dot out_channel g =
module JsonPrinter =
struct
let output_kinstr = function
- | Cil_types.Kglobal -> Json.of_string "global"
- | Cil_types.Kstmt stmt -> Json.of_int stmt.Cil_types.sid
+ | Cil_types.Kglobal -> `String "global"
+ | Cil_types.Kstmt stmt -> `Int stmt.Cil_types.sid
let output_callsite (kf,kinstr) =
- Json.of_fields [
- ("fun", Json.of_string (Kernel_function.get_name kf)) ;
+ `Assoc [
+ ("fun", `String (Kernel_function.get_name kf)) ;
("instr", output_kinstr kinstr) ;
]
let output_callstack cs =
- Json.of_list (List.map output_callsite cs)
+ `List (List.map output_callsite cs)
let output_node_kind kind =
let s = match kind with
@@ -267,15 +267,15 @@ struct
| Scattered _ -> "scattered"
| Alarm _ -> "alarm"
in
- Json.of_string s
+ `String s
let output_node_locality { loc_file ; loc_callstack } =
- let f1 = ("file", Json.of_string loc_file) in
+ let f1 = ("file", `String loc_file) in
let fields = match loc_callstack with
| [] -> [f1]
| cs -> [f1 ; ("callstack", output_callstack cs)]
in
- Json.of_fields fields
+ `Assoc fields
let output_node_precision_grade grade =
let s = match grade with
@@ -283,7 +283,7 @@ struct
| Normal -> "normal"
| Wide -> "wide"
in
- Json.of_string s
+ `String s
let output_dep_kind kind =
let s = match kind with
@@ -293,30 +293,30 @@ struct
| Control -> "ctrl"
| Composition -> "comp"
in
- Json.of_string s
+ `String s
let output_int_interval interval =
(* TODO: handle overflow *)
- Json.of_fields [
- ("min", Json.of_int (Integer.to_int interval.min)) ;
- ("max", Json.of_int (Integer.to_int interval.max)) ;
+ `Assoc [
+ ("min", `Int (Integer.to_int interval.min)) ;
+ ("max", `Int (Integer.to_int interval.max)) ;
]
let output_float_interval interval =
- Json.of_fields [
- ("min", Json.of_float interval.min) ;
- ("max", Json.of_float interval.max) ;
+ `Assoc [
+ ("min", `Float interval.min) ;
+ ("max", `Float interval.max) ;
]
let output_node_int_values values =
- Json.of_fields [
+ `Assoc [
("computed", output_int_interval values.values_interval) ;
("limits", output_int_interval values.values_limits) ;
("grade", output_node_precision_grade values.values_grade) ;
]
let output_node_float_values values =
- Json.of_fields [
+ `Assoc [
("computed", output_float_interval values.values_interval) ;
("limits", output_float_interval values.values_limits) ;
("grade", output_node_precision_grade values.values_grade) ;
@@ -324,12 +324,12 @@ struct
let output_node node =
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) ;
+ `Assoc ([
+ ("id", `Int node.node_key) ;
+ ("label", `String label) ;
("kind", output_node_kind node.node_kind) ;
("locality", output_node_locality node.node_locality) ;
- ("explored", Json.of_bool node.node_deps_computed) ;
+ ("explored", `Bool node.node_deps_computed) ;
] @
begin match node.node_int_values with
| None -> []
@@ -346,22 +346,22 @@ struct
| Some lval ->
let typ = Cil.typeOfLval lval in
let str = Pretty_utils.to_string Cil_printer.pp_typ typ in
- [("type", Json.of_string str)]
+ [("type", `String str)]
end)
let output_dep (n1,dep,n2) =
- Json.of_fields [
- ("id", Json.of_int dep.dependency_key) ;
- ("src", Json.of_int n1.node_key) ;
- ("dst", Json.of_int n2.node_key) ;
+ `Assoc [
+ ("id", `Int dep.dependency_key) ;
+ ("src", `Int n1.node_key) ;
+ ("dst", `Int n2.node_key) ;
("kind", output_dep_kind dep.dependency_kind) ;
- ("multiple", Json.of_bool dep.dependency_multiple)
+ ("multiple", `Bool dep.dependency_multiple)
]
let output_graph g =
- Json.of_fields [
- ("nodes", Json.of_list (List.map output_node (vertices g))) ;
- ("deps", Json.of_list (List.map output_dep (edges g)))
+ `Assoc [
+ ("nodes", `List (List.map output_node (vertices g))) ;
+ ("deps", `List (List.map output_dep (edges g)))
]
let output_diff g diff =
@@ -380,19 +380,19 @@ struct
let set = List.fold_left collect_deps Set.empty diff.added_nodes in
List.map output_dep (Set.elements set)
and removed_nodes =
- List.map (fun node -> Json.of_int node.node_key) diff.removed_nodes
+ List.map (fun node -> `Int node.node_key) diff.removed_nodes
in
- Json.of_fields [
- ("add", Json.of_fields [
- ("nodes", Json.of_list added_nodes) ;
- ("deps", Json.of_list added_deps)
+ `Assoc [
+ ("add", `Assoc [
+ ("nodes", `List added_nodes) ;
+ ("deps", `List added_deps)
]) ;
- ("sub", Json.of_list removed_nodes)]
+ ("sub", `List removed_nodes)]
end
let ouptput_to_json out_channel g =
let json = JsonPrinter.output_graph g in
- Json.save_channel ~pretty:true out_channel json
+ Yojson.Basic.to_channel out_channel json
let to_json g =
JsonPrinter.output_graph g
diff --git a/src/plugins/dive/server_interface.ml b/src/plugins/dive/server_interface.ml
index 23cebe7468d..d1d8dfd9d22 100644
--- a/src/plugins/dive/server_interface.ml
+++ b/src/plugins/dive/server_interface.ml
@@ -34,8 +34,8 @@ let get_graph =
g
-let page = Doc.page (`Plugin "Dive")
- ~title:"Dive into dependency graph"
+let page = Doc.page (`Plugin "dive")
+ ~title:"Dive Services"
~filename:"dive.md"
module Graph =
@@ -55,8 +55,8 @@ end
module Variable = Data.Collection (struct
module Info = struct
let page = page
- let name = "variable"
- let descr = Markdown.rm "Variable from the program"
+ let name = "dive-variable-name"
+ let descr = Markdown.rm "The name of variable of the program"
end
module R = Data.Record (Info)
@@ -75,7 +75,7 @@ module Variable = Data.Collection (struct
let to_json v =
let varname = v.Cil_types.vname in
- let fields = [ "var" , `String varname ] in
+ let fields = [ "var", `String varname ] in
let fields = match Kernel_function.find_defining_kf v with
| Some kf -> ("fun", `String (Kernel_function.get_name kf)) :: fields
| None -> fields
@@ -83,11 +83,12 @@ module Variable = Data.Collection (struct
`Assoc fields
let of_json json =
+ let open Yojson.Basic.Util in
try
let funname =
- try Some (Json.(string (field "fun" json)))
+ try Some (json |> member "fun" |> to_string)
with Not_found -> None
- and varname = Json.(string (field "var" json)) in
+ and varname = json |> member "var" |> to_string in
match funname with
| Some name ->
let kf =
@@ -116,6 +117,44 @@ module Variable = Data.Collection (struct
Data.failure json "Invalid source format"
end)
+module Function = Data.Collection (struct
+ type t = Cil_types.kernel_function
+
+ let syntax = Syntax.publish ~page ~name:"dive-function-name"
+ ~synopsis:Syntax.string
+ ~descr:(Markdown.rm "The name of a function of the program") ()
+
+ let to_json kf =
+ `String (Kernel_function.get_name kf)
+
+ let of_json json =
+ let open Yojson.Basic.Util in
+ let name = to_string json in
+ try
+ Globals.Functions.find_by_name name
+ with Not_found ->
+ Data.failure json "no function '%s'" name
+ end)
+
+module Node = Data.Collection (struct
+ type t = Graph_types.node
+
+ let syntax = Syntax.publish ~page ~name:"dive-node"
+ ~synopsis:Syntax.int
+ ~descr:(Markdown.rm "A node identifier in the graph") ()
+
+ let to_json node =
+ `Int node.Graph_types.node_key
+
+ let of_json json =
+ let open Yojson.Basic.Util in
+ let node_key = to_int json in
+ try
+ Build.find_node (get_graph ()) node_key
+ with Not_found ->
+ Data.failure json "no node '%d' in the current graph" node_key
+ end)
+
let () = Request.register ~page
~kind:`GET ~name:"dive.graph"
@@ -140,34 +179,45 @@ let () = Request.register ~page
Build.get_graph g, Build.take_last_differences g
end
+let () = Request.register ~page
+ ~kind:`EXEC ~name:"dive.add_function_alarms"
+ ~descr:(Markdown.rm "Add all alarms of the given function")
+ ~input:(module Function) ~output:(module GraphDiff)
+ begin fun kf ->
+ let depth = Self.DepthLimit.get () in
+ let g = get_graph () in
+ Build.add_function_alarms ~depth g kf;
+ Build.get_graph g, Build.take_last_differences g
+ end
+
let () = Request.register ~page
~kind:`EXEC ~name:"dive.explore"
~descr:(Markdown.rm "Explore the graph starting from an existing vertex")
- ~input:(module Data.Jint) ~output:(module GraphDiff)
- begin fun node_key ->
+ ~input:(module Node) ~output:(module GraphDiff)
+ begin fun node ->
let depth = Self.DepthLimit.get () in
let g = get_graph () in
- Build.explore_from_vertex ~depth g node_key;
+ Build.explore_from_node ~depth g node;
Build.get_graph g, Build.take_last_differences g
end
let () = Request.register ~page
~kind:`EXEC ~name:"dive.show"
~descr:(Markdown.rm "Show the dependencies of an existing vertex")
- ~input:(module Data.Jint) ~output:(module GraphDiff)
- begin fun node_key ->
+ ~input:(module Node) ~output:(module GraphDiff)
+ begin fun node ->
let depth = Self.DepthLimit.get () in
let g = get_graph () in
- Build.show ~depth g node_key;
+ Build.show ~depth g node;
Build.get_graph g, Build.take_last_differences g
end
let () = Request.register ~page
~kind:`EXEC ~name:"dive.hide"
~descr:(Markdown.rm "Hide the dependencies of an existing vertex")
- ~input:(module Data.Jint) ~output:(module GraphDiff)
- begin fun node_key ->
+ ~input:(module Node) ~output:(module GraphDiff)
+ begin fun node ->
let g = get_graph () in
- Build.hide g node_key;
+ Build.hide g node;
Build.get_graph g, Build.take_last_differences g
end
\ No newline at end of file
--
GitLab