diff --git a/src/plugins/dive/build.ml b/src/plugins/dive/build.ml
index 867ba64d01b9c47f97c7d8d801106101302d72e4..19d7f0d5832d2a752f1e02ab2fa90a9f30174607 100644
--- a/src/plugins/dive/build.ml
+++ b/src/plugins/dive/build.ml
@@ -175,6 +175,7 @@ module NodeRef = Datatype.Pair_with_collections
(struct let module_name = "Build.NodeRef" end)
module Graph = Imprecision_graph
+module VertexTable = Datatype.Int.Hashtbl
module NodeTable = FCHashtbl.Make (NodeRef)
module FileTable = Datatype.String.Hashtbl
module CallstackTable = Value_types.Callstack.Hashtbl
@@ -183,6 +184,7 @@ module FunctionMap = Kernel_function.Map
type t = {
mutable graph: Graph.t;
+ mutable vertex_table: node VertexTable.t;
mutable node_table: node NodeTable.t;
mutable file_table: node FileTable.t;
mutable callstack_table: node CallstackTable.t;
@@ -190,20 +192,41 @@ type t = {
mutable hidden_bases: BaseSet.t;
mutable focus: bool FunctionMap.t;
mutable roots: node list;
+ mutable graph_diff: graph_diff;
}
+let get_node context node_key =
+ VertexTable.find context.vertex_table node_key
+
+let add_node context ~node_kind ~node_locality =
+ let node = Graph.create_node context.graph ~node_kind ~node_locality in
+ VertexTable.add context.vertex_table node.node_key node;
+ context.graph_diff <- {
+ context.graph_diff with
+ added_nodes = node :: context.graph_diff.added_nodes
+ };
+ node
+
+let _remove_node context node =
+ Graph.remove_node context.graph node;
+ VertexTable.remove context.vertex_table node.node_key;
+ context.graph_diff <- {
+ context.graph_diff with
+ removed_nodes = node :: context.graph_diff.removed_nodes
+ }
+
let reference_node_locality context node_locality =
let { loc_file ; loc_callstack } = node_locality in
let rec add_file _ =
let node_locality = { node_locality with loc_callstack = [] } in
- Graph.create_node context.graph ~node_kind:Cluster ~node_locality
+ add_node context ~node_kind:Cluster ~node_locality
and add_callstack = function
| [] -> assert false
| _ :: t as loc_callstack ->
let node_locality = { node_locality with loc_callstack } in
if t <> [] then
ignore (CallstackTable.memo context.callstack_table t add_callstack);
- Graph.create_node context.graph ~node_kind:Cluster ~node_locality
+ add_node context ~node_kind:Cluster ~node_locality
in
match loc_callstack with
| [] ->
@@ -233,7 +256,7 @@ let build_node context callstack location lval =
let node_locality = build_node_locality callstack node_kind in
reference_node_locality context node_locality;
let build_new_node _location =
- Graph.create_node context.graph ~node_kind ~node_locality
+ add_node context ~node_kind ~node_locality
in
(* Compute the new location which might have changed after folding *)
let location' =
@@ -263,7 +286,7 @@ let build_lval context callstack kinstr lval =
let build_alarm context callstack stmt alarm =
let node_kind = Alarm (stmt,alarm) in
let node_locality = build_node_locality callstack node_kind in
- Graph.create_node context.graph ~node_kind ~node_locality
+ add_node context ~node_kind ~node_locality
exception Too_many_deps of lval
@@ -435,6 +458,7 @@ let create () =
!Db.Value.compute ();
{
graph = Graph.create ();
+ vertex_table = VertexTable.create 13;
node_table = NodeTable.create 13;
file_table = FileTable.create 13;
callstack_table = CallstackTable.create 13;
@@ -442,15 +466,18 @@ let create () =
hidden_bases = BaseSet.empty;
focus = FunctionMap.empty;
roots = [];
+ graph_diff = { added_nodes=[] ; removed_nodes=[] };
}
let clear context =
context.graph <- Graph.create ();
+ context.vertex_table <- VertexTable.create 13;
context.node_table <- NodeTable.create 13;
context.file_table <- FileTable.create 13;
context.callstack_table <- CallstackTable.create 13;
context.focus <- FunctionMap.empty;
- context.roots <- []
+ context.roots <- [];
+ context.graph_diff <- { added_nodes=[] ; removed_nodes=[] }
(* --- Accessors --- *)
@@ -481,8 +508,7 @@ let should_auto_explore node =
| Scalar _ | Composite _ | Alarm _ -> true
| Scattered _ | Cluster -> false
-let complete_in_depth ~depth context root =
- context.roots <- root :: context.roots;
+let explore ~depth context root =
(* Breadth first search *)
let queue : (node * int) Queue.t = Queue.create () in
Queue.add (root,0) queue;
@@ -502,6 +528,10 @@ let complete_in_depth ~depth context root =
end;
done
+let complete_in_depth ~depth context root =
+ context.roots <- root :: context.roots;
+ explore ~depth context root
+
let add_var ?(depth=1) context varinfo =
let callstack = [] in
let node = build_var context callstack varinfo in
@@ -519,3 +549,11 @@ let add_alarm ?(depth=1) context stmt alarm =
let callstack = Callstack.init (Kernel_function.find_englobing_kf stmt) in
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 take_last_differences context =
+ let diff = context.graph_diff in
+ context.graph_diff <- { added_nodes=[] ; removed_nodes=[] };
+ diff
diff --git a/src/plugins/dive/build.mli b/src/plugins/dive/build.mli
index c710f021829c06b0cb4849e25cac5be4b765d6a5..961dec8856363dcafaa76fa59df6e7cb591e9f05 100644
--- a/src/plugins/dive/build.mli
+++ b/src/plugins/dive/build.mli
@@ -37,3 +37,5 @@ val unhide_base : t -> Cil_types.varinfo -> unit
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 take_last_differences : t -> Graph_types.graph_diff
diff --git a/src/plugins/dive/graph_types.mli b/src/plugins/dive/graph_types.mli
index acf759d97f84382df0fe6bd1fcb5796dd595f748..515bf05c6a45be70b228ed46f2e4b41964575fd8 100644
--- a/src/plugins/dive/graph_types.mli
+++ b/src/plugins/dive/graph_types.mli
@@ -57,3 +57,8 @@ type dependency = {
dependency_kind : dependency_kind;
mutable dependency_multiple : bool;
}
+
+type graph_diff = {
+ added_nodes: node list;
+ removed_nodes: node list;
+}
diff --git a/src/plugins/dive/imprecision_graph.ml b/src/plugins/dive/imprecision_graph.ml
index 81d0ecf36c0d86e802c442895f9f0d509d373c9f..167d850effde26c8f2dca77a8c1fbad51322d83c 100644
--- a/src/plugins/dive/imprecision_graph.ml
+++ b/src/plugins/dive/imprecision_graph.ml
@@ -62,6 +62,8 @@ let create_node ?node_values ~node_kind ~node_locality g =
add_vertex g node;
node
+let remove_node = remove_vertex
+
let union_interval i1 i2 =
{ min = min i1.min i2.min ; max = max i1.max i2.max }
@@ -195,18 +197,21 @@ let ouptput_to_dot out_channel g =
in
Dot.output_graph out_channel g
-let to_json g =
- let rec output_kinstr = function
+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
- and output_callsite (kf,kinstr) =
+
+ let output_callsite (kf,kinstr) =
Json.of_fields [
("fun", Json.of_string (Kernel_function.get_name kf)) ;
("instr", output_kinstr kinstr) ;
]
- and output_callstack cs =
+
+ let output_callstack cs =
Json.of_list (List.map output_callsite cs)
- in
+
let output_node_kind kind =
let s = match kind with
| Scalar _ -> "scalar"
@@ -216,21 +221,24 @@ let to_json g =
| Cluster -> "dummy"
in
Json.of_string s
- and output_node_locality { loc_file ; loc_callstack } =
+
+ let output_node_locality { loc_file ; loc_callstack } =
let f1 = ("file", Json.of_string loc_file) in
let fields = match loc_callstack with
| [] -> [f1]
- | cs -> [f1 ; ("fun", output_callstack cs)]
+ | cs -> [f1 ; ("callstack", output_callstack cs)]
in
Json.of_fields fields
- and output_node_precision_grade grade =
+
+ let output_node_precision_grade grade =
let s = match grade with
| Singleton -> "singleton"
| Normal -> "normal"
| Wide -> "wide"
in
Json.of_string s
- and output_dep_kind kind =
+
+ let output_dep_kind kind =
let s = match kind with
| Callee -> "callee"
| Data -> "data"
@@ -238,47 +246,96 @@ let to_json g =
| Control -> "ctrl"
in
Json.of_string s
- and output_float_interval interval =
+
+ let output_float_interval interval =
Json.of_fields [
("min", Json.of_float interval.min) ;
("max", Json.of_float interval.max) ;
]
- in
+
let output_node_values values =
Json.of_fields [
- ("values", output_float_interval values.values_interval) ;
+ ("computed", output_float_interval values.values_interval) ;
("limits", output_float_interval values.values_limits) ;
("grade", output_node_precision_grade values.values_grade) ;
]
- in
- let output_node node acc =
- if node.node_kind = Cluster 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) ;
- ("explored", Json.of_bool node.node_deps_computed)
- ] @
- match node.node_values with
- | None -> []
- | Some node_values -> [("values", output_node_values node_values)]
- ) :: acc
- and output_dep (n1,dep,n2) acc =
+
+ 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) ;
+ ("kind", output_node_kind node.node_kind) ;
+ ("locality", output_node_locality node.node_locality) ;
+ ("explored", Json.of_bool node.node_deps_computed)
+ ] @
+ match node.node_values with
+ | None -> []
+ | Some node_values -> [("values", output_node_values node_values)]
+ )
+
+ 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) ;
("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
- Json.of_fields [("nodes", nodes) ; ("deps", deps)]
+ ]
+
+ let output_graph g =
+ let add_node node acc =
+ if node.node_kind = Cluster
+ then acc
+ else output_node node :: acc
+ and add_edge d acc =
+ output_dep d :: acc
+ in
+ Json.of_fields [
+ ("nodes", Json.of_list (fold_vertex add_node g [])) ;
+ ("deps", Json.of_list (fold_edges_e add_edge g []))
+ ]
+
+ let output_diff g diff =
+ let add_node acc node =
+ if node.node_kind = Cluster
+ then acc
+ else output_node node :: acc
+ and add_dep d acc =
+ output_dep d :: acc
+ in
+ let added_nodes =
+ List.fold_left add_node [] diff.added_nodes
+ and added_deps =
+ let module Set = Set.Make (struct
+ type t = edge
+ let compare (_,d1,_) (_,d2,_) = d1.dependency_key - d2.dependency_key
+ end)
+ in
+ let collect_deps set node =
+ let set = fold_pred_e Set.add g node set in
+ let set = fold_succ_e Set.add g node set in
+ set
+ in
+ let set = List.fold_left collect_deps Set.empty diff.added_nodes in
+ Set.fold add_dep set []
+ and removed_nodes =
+ List.map (fun node -> Json.of_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)
+ ]) ;
+ ("sub", Json.of_list removed_nodes)]
+end
let ouptput_to_json out_channel g =
- let json = to_json g in
+ let json = JsonPrinter.output_graph g in
Json.save_channel ~pretty:true out_channel json
+
+let to_json g =
+ JsonPrinter.output_graph g
+
+let diff_to_json g diff =
+ JsonPrinter.output_diff g diff
diff --git a/src/plugins/dive/imprecision_graph.mli b/src/plugins/dive/imprecision_graph.mli
index 17a5812872e99557bc9d7b219d4a25b4ee0eff44..3a88646f26df93877c7a140209b2530c1d64cfb1 100644
--- a/src/plugins/dive/imprecision_graph.mli
+++ b/src/plugins/dive/imprecision_graph.mli
@@ -31,11 +31,15 @@ val create_node :
node_kind:node_kind ->
node_locality:node_locality -> t -> node
+val remove_node : t -> node -> unit
+
val update_node_values : node -> node_values -> unit
val create_dependency : allow_folding:bool -> t -> node -> dependency_kind ->
node -> unit
-val to_json : t -> Json.t
val ouptput_to_dot : out_channel -> t -> unit
val ouptput_to_json : out_channel -> t -> unit
+
+val to_json : t -> Json.t
+val diff_to_json : t -> graph_diff -> Json.t
diff --git a/src/plugins/dive/server_interface.ml b/src/plugins/dive/server_interface.ml
index 510d80955cb14477551e07c9337820001c9c01c9..b8038457f16050e2bd217e3f008ec80d86fb6dac 100644
--- a/src/plugins/dive/server_interface.ml
+++ b/src/plugins/dive/server_interface.ml
@@ -45,6 +45,13 @@ struct
let to_json = Imprecision_graph.to_json
end
+module GraphDiff =
+struct
+ type t = Imprecision_graph.t * Graph_types.graph_diff
+ let syntax = Syntax.any
+ let to_json = fun (g,d) -> Imprecision_graph.diff_to_json g d
+end
+
module Variable = Data.Collection (struct
type t = Cil_types.varinfo
let syntax = Syntax.publish ~page ~name:"variable"
@@ -112,11 +119,21 @@ let () = Request.register ~page
let () = Request.register ~page
~kind:`EXEC ~name:"dive.add_var"
~descr:(Markdown.rm "Add a variable to the graph")
- ~input:(module Variable) ~output:(module Graph)
+ ~input:(module Variable) ~output:(module GraphDiff)
begin fun var ->
let depth = Self.DepthLimit.get () in
let g = get_graph () in
Build.add_var ~depth g var;
- Build.get_graph g
+ 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 ->
+ let depth = Self.DepthLimit.get () in
+ let g = get_graph () in
+ Build.explore_from_vertex ~depth g node_key;
+ Build.get_graph g, Build.take_last_differences g
+ end