Merge branch 'feature/dive' into 'master'

[dive] New plugin dive to generate imprecision graphs for Eva

See merge request frama-c/frama-c!2720

headers/header_spec.txt

@@ -763,6 +763,23 @@ src/plugins/constant_propagation/propagationParameters.ml: CEA_LGPL_OR_PROPRIETA
 src/plugins/constant_propagation/propagationParameters.mli: CEA_LGPL_OR_PROPRIETARY
 src/plugins/constant_propagation/api.ml: CEA_LGPL_OR_PROPRIETARY
 src/plugins/constant_propagation/api.mli: CEA_LGPL_OR_PROPRIETARY
+src/plugins/dive/build.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/dive/build.mli: CEA_LGPL_OR_PROPRIETARY
+src/plugins/dive/callstack.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/dive/callstack.mli: CEA_LGPL_OR_PROPRIETARY
+src/plugins/dive/configure.ac: CEA_LGPL_OR_PROPRIETARY
+src/plugins/dive/Dive.mli: CEA_LGPL_OR_PROPRIETARY
+src/plugins/dive/graph_types.mli: CEA_LGPL_OR_PROPRIETARY
+src/plugins/dive/imprecision_graph.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/dive/imprecision_graph.mli: CEA_LGPL_OR_PROPRIETARY
+src/plugins/dive/main.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/dive/Makefile.in: CEA_LGPL_OR_PROPRIETARY
+src/plugins/dive/node_kind.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/dive/node_kind.mli: CEA_LGPL_OR_PROPRIETARY
+src/plugins/dive/self.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/dive/self.mli: CEA_LGPL_OR_PROPRIETARY
+src/plugins/dive/server_interface.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/dive/server_interface.mli: CEA_LGPL_OR_PROPRIETARY
 src/plugins/from/From.mli: CEA_LGPL_OR_PROPRIETARY
 src/plugins/from/callwise.ml: CEA_LGPL_OR_PROPRIETARY
 src/plugins/from/callwise.mli: CEA_LGPL_OR_PROPRIETARY

src/plugins/dive/.gitignore

+/Makefile
+/tests/*/result
+/tests/ptests_config

src/plugins/dive/Dive.mli

+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of Frama-C.                                         *)
+(*                                                                        *)
+(*  Copyright (C) 2007-2020                                               *)
+(*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
+(*         alternatives)                                                  *)
+(*                                                                        *)
+(*  you can redistribute it and/or modify it under the terms of the GNU   *)
+(*  Lesser General Public License as published by the Free Software       *)
+(*  Foundation, version 2.1.                                              *)
+(*                                                                        *)
+(*  It is distributed in the hope that it will be useful,                 *)
+(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
+(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
+(*  GNU Lesser General Public License for more details.                   *)
+(*                                                                        *)
+(*  See the GNU Lesser General Public License version 2.1                 *)
+(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
+(*                                                                        *)
+(**************************************************************************)

src/plugins/dive/Makefile.in

+##########################################################################
+#                                                                        #
+#  This file is part of Frama-C.                                         #
+#                                                                        #
+#  Copyright (C) 2007-2020                                               #
+#    CEA (Commissariat à l'énergie atomique et aux énergies              #
+#         alternatives)                                                  #
+#                                                                        #
+#  you can redistribute it and/or modify it under the terms of the GNU   #
+#  Lesser General Public License as published by the Free Software       #
+#  Foundation, version 2.1.                                              #
+#                                                                        #
+#  It is distributed in the hope that it will be useful,                 #
+#  but WITHOUT ANY WARRANTY; without even the implied warranty of        #
+#  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         #
+#  GNU Lesser General Public License for more details.                   #
+#                                                                        #
+#  See the GNU Lesser General Public License version 2.1                 #
+#  for more details (enclosed in the file licenses/LGPLv2.1).            #
+#                                                                        #
+##########################################################################
+
+#######################
+# Frama-C Environment #
+#######################
+
+ifndef FRAMAC_SHARE
+FRAMAC_SHARE	:= $(shell frama-c-config -print-share-path)
+endif
+
+ifndef FRAMAC_LIBDIR
+FRAMAC_LIBDIR	:= $(shell frama-c-config -print-libpath)
+endif
+
+#########################
+# Plug-in configuration #
+#########################
+
+PLUGIN_DIR ?=.
+PLUGIN_ENABLE:=@ENABLE_DIVE@
+PLUGIN_NAME := Dive
+PLUGIN_CMO := self callstack node_kind imprecision_graph build main \
+  server_interface
+PLUGIN_CMI:= graph_types
+PLUGIN_DEPENDENCIES:= Eva Studia Server
+PLUGIN_HAS_MLI:= yes
+PLUGIN_TESTS_DIRS:=dive
+PLUGIN_GENERATED:=
+PLUGIN_DISTRIB_EXTERNAL:= Makefile.in configure.ac configure
+PLUGIN_DISTRIBUTED:=$(PLUGIN_ENABLE)
+
+################
+# Generic part #
+################
+
+include $(FRAMAC_SHARE)/Makefile.dynamic
+
+#####################################
+# Regenerating the Makefile on need #
+#####################################
+
+ifeq ("$(FRAMAC_INTERNAL)","yes")
+CONFIG_STATUS_DIR:=$(FRAMAC_SRC)
+CONFIG_STATUS_DIR_DEP:=
+else
+CONFIG_STATUS_DIR:=$(Dive_DIR)
+CONFIG_STATUS_DIR_DEP:=$(CONFIG_STATUS_DIR)/config.status
+endif
+
+$(Dive_DIR)/Makefile: $(Dive_DIR)/Makefile.in $(CONFIG_STATUS_DIR_DEP)
+	cd $(CONFIG_STATUS_DIR) && ./config.status --file $@

src/plugins/dive/README.md

+Dive is a Frama-C plugin specialized in the visualization of data dependencies.
+It is intended to help the user find the origin of an imprecision in an Eva
+analysis.
+
+
+Dependencies
+============
+
+The front-end of Dive relies on several external tools and libraries :
+
+- Node.js: a runtime environment for javascript to run programs outside a
+  browser
+- yarn: a package manager for javascript modules written for Node.js
+- electron: a javascript framework for gui applications
+- Ivette: the future Frama-C GUI
+- Cytoscape: a javascript library to display graphs and interact with them
+- Zmq: a multilanguage framework for common simple networking patterns

src/plugins/dive/build.mli

+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of Frama-C.                                         *)
+(*                                                                        *)
+(*  Copyright (C) 2007-2020                                               *)
+(*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
+(*         alternatives)                                                  *)
+(*                                                                        *)
+(*  you can redistribute it and/or modify it under the terms of the GNU   *)
+(*  Lesser General Public License as published by the Free Software       *)
+(*  Foundation, version 2.1.                                              *)
+(*                                                                        *)
+(*  It is distributed in the hope that it will be useful,                 *)
+(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
+(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
+(*  GNU Lesser General Public License for more details.                   *)
+(*                                                                        *)
+(*  See the GNU Lesser General Public License version 2.1                 *)
+(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
+(*                                                                        *)
+(**************************************************************************)
+
+type t
+
+val create : unit -> t
+val clear : t -> unit (* reset to almost an empty context,
+                         but keeps folded and hidden bases *)
+
+val get_graph : t -> Imprecision_graph.t
+val get_roots : t -> Graph_types.node list
+
+val unfold_base : t -> Cil_types.varinfo -> unit
+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 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 -> Graph_types.node -> unit
+val hide : t -> Graph_types.node -> unit
+
+val take_last_differences : t -> Graph_types.graph_diff

src/plugins/dive/callstack.ml

+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of Frama-C.                                         *)
+(*                                                                        *)
+(*  Copyright (C) 2007-2020                                               *)
+(*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
+(*         alternatives)                                                  *)
+(*                                                                        *)
+(*  you can redistribute it and/or modify it under the terms of the GNU   *)
+(*  Lesser General Public License as published by the Free Software       *)
+(*  Foundation, version 2.1.                                              *)
+(*                                                                        *)
+(*  It is distributed in the hope that it will be useful,                 *)
+(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
+(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
+(*  GNU Lesser General Public License for more details.                   *)
+(*                                                                        *)
+(*  See the GNU Lesser General Public License version 2.1                 *)
+(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
+(*                                                                        *)
+(**************************************************************************)
+
+open Cil_types
+
+include Value_types.Callstack
+
+type call_site = Value_types.call_site
+module Callsite = Value_types.Callsite
+
+let init kf = [(kf,Kglobal)]
+
+let pop cs =
+  match cs with
+  | [] | (_,Kglobal) :: _ :: _ | [(_,Kstmt _)] -> assert false (* Invariant *)
+  | [(_,Kglobal)] -> None
+  | (kf,Kstmt stmt) :: t -> Some (kf,stmt,t)
+
+let top_kf cs =
+  match cs with
+  | [] | (_,Kglobal) :: _ :: _ | [(_,Kstmt _)] -> assert false (* Invariant *)
+  | (kf,_) :: _ -> kf
+
+let rec pop_downto top_kf = function
+  | [] -> failwith "the callstack doesn't contain this function"
+  | ((kf,_kinstr) :: tail) as cs ->
+    if Kernel_function.equal kf top_kf
+    then cs
+    else pop_downto top_kf tail
+
+let push (kf,stmt) cs =
+  match cs with
+  (* When the callstack is truncated, we ignore the first callsite *)
+  | [] -> [(kf,Kglobal)]
+  | cs -> (kf,Kstmt stmt) :: cs
+
+let rec is_prefix cs1 cs2 =
+  match cs1, cs2 with
+  | [], _ -> true
+  | _, [] -> false
+  | [(kf,Kglobal)], (kf',_)::_ -> Kernel_function.equal kf kf'
+  | _, [(_,Kglobal)] -> false
+  | s1 :: t1, s2 :: t2 ->
+    if Callsite.equal s1 s2
+    then is_prefix t1 t2
+    else false
+
+let truncate_to_sub full_cs sub_cs =
+  let rec aux acc = function
+    | [] -> None
+    | (s :: t) as cs ->
+      if is_prefix sub_cs cs
+      then Some (List.rev acc @ sub_cs)
+      else aux (s :: acc) t
+  in
+  aux [] full_cs
+
+let list_filter_map f l =
+  let aux acc x =
+    match f x with
+    | None -> acc
+    | Some y -> y :: acc
+  in
+  List.rev (List.fold_left aux [] l)
+
+let filter_truncate l sub_cs =
+  list_filter_map (fun cs -> truncate_to_sub cs sub_cs) l

src/plugins/dive/callstack.mli

+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of Frama-C.                                         *)
+(*                                                                        *)
+(*  Copyright (C) 2007-2020                                               *)
+(*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
+(*         alternatives)                                                  *)
+(*                                                                        *)
+(*  you can redistribute it and/or modify it under the terms of the GNU   *)
+(*  Lesser General Public License as published by the Free Software       *)
+(*  Foundation, version 2.1.                                              *)
+(*                                                                        *)
+(*  It is distributed in the hope that it will be useful,                 *)
+(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
+(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
+(*  GNU Lesser General Public License for more details.                   *)
+(*                                                                        *)
+(*  See the GNU Lesser General Public License version 2.1                 *)
+(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
+(*                                                                        *)
+(**************************************************************************)
+
+type call_site = (Cil_types.kernel_function * Cil_types.kinstr)
+type t = call_site list
+
+include Datatype.S_with_collections with type t := t
+
+(* The callstacks manipulated here have the following invariant:
+   - the callstack is never an empty list
+   - the last item of the list has always a Kglobal
+   - all elements of the list except the last have a Kstmt *)
+
+val init : Cil_types.kernel_function -> t
+val pop : t -> (Cil_types.kernel_function * Cil_types.stmt * t) option
+val pop_downto : Cil_types.kernel_function -> t -> t
+val top_kf : t -> Cil_types.kernel_function
+val push : Cil_types.kernel_function * Cil_types.stmt -> t -> t
+val is_prefix : t -> t -> bool
+val truncate_to_sub : t -> t -> t option
+val filter_truncate : t list -> t -> t list

src/plugins/dive/configure.ac

+##########################################################################
+#                                                                        #
+#  This file is part of Frama-C.                                         #
+#                                                                        #
+#  Copyright (C) 2007-2020                                               #
+#    CEA (Commissariat à l'énergie atomique et aux énergies              #
+#         alternatives)                                                  #
+#                                                                        #
+#  you can redistribute it and/or modify it under the terms of the GNU   #
+#  Lesser General Public License as published by the Free Software       #
+#  Foundation, version 2.1.                                              #
+#                                                                        #
+#  It is distributed in the hope that it will be useful,                 #
+#  but WITHOUT ANY WARRANTY; without even the implied warranty of        #
+#  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         #
+#  GNU Lesser General Public License for more details.                   #
+#                                                                        #
+#  See the GNU Lesser General Public License version 2.1                 #
+#  for more details (enclosed in the file licenses/LGPLv2.1).            #
+#                                                                        #
+##########################################################################
+
+m4_define([plugin_file],Makefile.in)
+
+m4_define([FRAMAC_SHARE_ENV],
+          [m4_normalize(m4_esyscmd([echo $FRAMAC_SHARE]))])
+
+m4_define([FRAMAC_SHARE],
+	  [m4_ifval(FRAMAC_SHARE_ENV,[FRAMAC_SHARE_ENV],
+                                     [m4_esyscmd(frama-c -print-path)])])
+
+m4_ifndef([FRAMAC_M4_MACROS], [m4_include(FRAMAC_SHARE/configure.ac)])
+
+check_plugin(dive,PLUGIN_RELATIVE_PATH(plugin_file),
+             [support for Dive plug-in],yes)
+
+# Plug-in dependencies
+######################
+
+plugin_require(dive,eva)
+plugin_require(dive,studia)
+#plugin_use(dive,usable_plugin_but_not_mandatory)
+
+check_plugin_dependencies
+
+#######################
+# Generating Makefile #
+#######################
+
+write_plugin_config(Makefile)

src/plugins/dive/graph_types.mli

+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of Frama-C.                                         *)
+(*                                                                        *)
+(*  Copyright (C) 2007-2020                                               *)
+(*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
+(*         alternatives)                                                  *)
+(*                                                                        *)
+(*  you can redistribute it and/or modify it under the terms of the GNU   *)
+(*  Lesser General Public License as published by the Free Software       *)
+(*  Foundation, version 2.1.                                              *)
+(*                                                                        *)
+(*  It is distributed in the hope that it will be useful,                 *)
+(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
+(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
+(*  GNU Lesser General Public License for more details.                   *)
+(*                                                                        *)
+(*  See the GNU Lesser General Public License version 2.1                 *)
+(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
+(*                                                                        *)
+(**************************************************************************)
+
+type node_kind =
+  | Scalar of Cil_types.varinfo * Cil_types.typ * Cil_types.offset
+  | Composite of Cil_types.varinfo
+  | Scattered of Cil_types.lval * Cil_types.kinstr
+  | Alarm of Cil_types.stmt * Alarms.alarm
+
+type node_locality = {
+  loc_file : string;
+  loc_callstack : Callstack.t;
+}
+
+type 'a interval = {min: 'a; max: 'a}
+
+type precision_grade = Singleton | Normal | Wide
+
+type 'a node_values = {
+  values_interval : 'a interval;
+  values_limits : 'a interval;
+  values_grade : precision_grade;
+}
+
+type node = {
+  node_key : int;
+  node_kind : node_kind;
+  node_locality : node_locality;
+  mutable node_hidden : bool;
+  mutable node_int_values : (Integer.t node_values) option;
+  mutable node_float_values : (float node_values) option;
+  mutable node_deps_computed : bool;
+}
+
+type dependency_kind = Callee | Data | Address | Control | Composition
+
+type dependency = {
+  dependency_key : int;
+  dependency_kind : dependency_kind;
+  mutable dependency_multiple : bool;
+}
+
+type graph_diff = {
+  added_nodes: node list;
+  removed_nodes: node list;
+}

src/plugins/dive/imprecision_graph.ml

+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of Frama-C.                                         *)
+(*                                                                        *)
+(*  Copyright (C) 2007-2020                                               *)
+(*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
+(*         alternatives)                                                  *)
+(*                                                                        *)
+(*  you can redistribute it and/or modify it under the terms of the GNU   *)
+(*  Lesser General Public License as published by the Free Software       *)
+(*  Foundation, version 2.1.                                              *)
+(*                                                                        *)
+(*  It is distributed in the hope that it will be useful,                 *)
+(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
+(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
+(*  GNU Lesser General Public License for more details.                   *)
+(*                                                                        *)
+(*  See the GNU Lesser General Public License version 2.1                 *)
+(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
+(*                                                                        *)
+(**************************************************************************)
+
+open Graph_types
+
+module Node =
+struct
+  type t = node
+  let compare v1 v2 = v1.node_key - v2.node_key
+  let hash v = v.node_key
+  let equal v1 v2 = v1.node_key = v2.node_key
+end
+
+module Dependency =
+struct
+  type t = dependency
+  let compare e1 e2 = e1.dependency_key - e2.dependency_key
+  let hash e = e.dependency_key
+  let equal e1 e2 = e1.dependency_key = e2.dependency_key
+  let default = {
+    dependency_key = -1;
+    dependency_kind = Data;
+    dependency_multiple = false;
+  }
+end
+
+module G =
+  Graph.Imperative.Digraph.ConcreteBidirectionalLabeled (Node) (Dependency)
+include G
+
+let vertices g =
+  fold_vertex (fun n acc -> n ::acc) g []
+
+let edges g =
+  fold_edges_e (fun d acc -> d ::acc) g []
+
+let next_key = ref 0
+
+let create_node ~node_kind ~node_locality g =
+  let node = {
+    node_key = !next_key;
+    node_kind;
+    node_locality;
+    node_hidden = false;
+    node_int_values = None;
+    node_float_values = None;
+    node_deps_computed = false;
+  }
+  in
+  incr next_key;
+  add_vertex g node;
+  node
+
+let remove_node = remove_vertex
+
+let union_int_interval i1 i2 =
+  { min = Integer.min i1.min i2.min ; max = Integer.max i1.max i2.max }
+
+let union_float_interval i1 i2 =
+  { min = min i1.min i2.min ; max = max i1.max i2.max }
+
+let worst_precision_grade q1 q2 =
+  match q1, q2 with
+  | Wide, _ | _, Wide -> Wide
+  | Normal, _ | _, Normal -> Normal
+  | Singleton, Singleton -> Singleton
+
+let merge_int_values p1 p2 =
+  (* TODO: prevent assertion failure *)
+  assert (Integer.equal p1.values_limits.min p2.values_limits.min);
+  assert (Integer.equal p1.values_limits.max p2.values_limits.max);
+  {
+    values_interval = union_int_interval p1.values_interval p2.values_interval;
+    values_limits = p1.values_limits;
+    values_grade = worst_precision_grade p1.values_grade p2.values_grade;
+  }
+
+let merge_float_values p1 p2 =
+  (* TODO: prevent assertion failure *)
+  assert (p1.values_limits = p2.values_limits);
+  {
+    values_interval = union_float_interval p1.values_interval p2.values_interval;
+    values_limits = p1.values_limits;
+    values_grade = worst_precision_grade p1.values_grade p2.values_grade;
+  }
+
+let update_node_int_values node new_values =
+  node.node_int_values <-
+    Some (Extlib.opt_fold merge_int_values node.node_int_values new_values)
+
+let update_node_float_values node new_values =
+  node.node_float_values <-
+    Some (Extlib.opt_fold merge_float_values node.node_float_values new_values)
+
+
+let create_dependency ~allow_folding g v1 dependency_kind v2 =
+  let same_kind (_,e,_) =
+    e.dependency_kind = dependency_kind
+  in
+  let matching_edge =
+    try
+      if allow_folding then
+        Some (List.find same_kind (G.find_all_edges g v1 v2))
+      else
+        None
+    with Not_found -> None
+  in
+  match matching_edge with
+  | Some (_,e,_) ->
+    e.dependency_multiple <- true
+  | None ->
+    let e = {
+      dependency_key = !next_key;
+      dependency_kind;
+      dependency_multiple = false;
+    }
+    in
+    incr next_key;
+    add_edge_e g (v1,e,v2)
+
+let remove_dependency g edge =
+  remove_edge_e g edge
+
+
+let find_independant_nodes g roots =
+  let module Dfs = Graph.Traverse.Dfs (struct
+      include G
+      let iter_succ = G.iter_pred
+      let fold_succ = G.fold_pred
+    end)
+  in
+  let module Table = Hashtbl.Make (Node) in
+  let table = Table.create 13 in
+  List.iter (Dfs.prefix_component (fun n -> Table.add table n true) g) roots;
+  fold_vertex (fun n acc -> if Table.mem table n then acc else n :: acc) g []
+
+
+let ouptput_to_dot out_channel g =
+  let open Graph.Graphviz.DotAttributes in
+  (* let g = add_dummy_nodes g in *)
+
+  let build_label s = `HtmlLabel (Extlib.html_escape s) in
+
+  let module FileTable = Datatype.String.Hashtbl in
+  let module CallstackTable = Value_types.Callstack.Hashtbl in
+  let file_table = FileTable.create 13
+  and callstack_table = CallstackTable.create 13 in
+  let file_counter = ref 0 in
+  let callstack_counter = ref 0 in
+  let rec build_file_subgraph filename =
+    incr file_counter;
+    {
+      sg_name = "file_" ^ (string_of_int !file_counter);
+      sg_attributes = [build_label filename];
+      sg_parent = None;
+    }
+  and build_callstack_subgraph = function
+    | [] -> None
+    | (kf,_kinstr) :: stack ->
+      let parent = get_callstack_subgraph stack in
+      incr callstack_counter;
+      Some {
+        sg_name = "cs_" ^ (string_of_int !callstack_counter);
+        sg_attributes = [build_label (Kernel_function.get_name kf)];
+        sg_parent = Extlib.opt_map (fun sg -> sg.sg_name) parent;
+      }
+  and get_file_subgraph filename =
+    FileTable.memo file_table filename build_file_subgraph
+  and get_callstack_subgraph cs =
+    CallstackTable.memo callstack_table cs build_callstack_subgraph
+  in
+
+  let module Dot = Graph.Graphviz.Dot (
+    struct
+      include G
+      let graph_attributes _g = []
+      let default_vertex_attributes _g = []
+      let vertex_name v = "cp" ^ (string_of_int v.node_key)
+      let vertex_attributes v =
+        let grade = match v.node_int_values, v.node_float_values with
+          | Some v1, Some v2 ->
+            Some (worst_precision_grade v1.values_grade v2.values_grade)
+          | Some v, _ -> Some v.values_grade
+          | _, Some v -> Some v.values_grade
+          | None, None -> None
+        in
+        let l = ref [] in
+        let text = Pretty_utils.to_string Node_kind.pretty v.node_kind in
+        if text <> "" then
+          l := build_label text :: !l;
+        let kind = match v.node_kind with
+          | Scalar _ -> [`Shape `Box]
+          | Composite _ -> [ `Shape `Box3d ]
+          | Scattered _ -> [ `Shape `Parallelogram ]
+          | Alarm _ ->  [ `Shape `Doubleoctagon ;
+                          `Style `Bold ; `Color 0xff0000 ;
+                          `Style `Filled ; `Fillcolor 0xff0000 ]
+        and values = match grade with
+          | None -> []
+          | Some Singleton ->
+            [`Color 0x88aaff ; `Style `Filled ; `Fillcolor 0xaaccff ]
+          | Some Normal ->
+            [ `Color 0x004400 ; `Style `Filled ; `Fillcolor 0xeeffee ]
+          | Some Wide ->
+            [ `Color 0xff0000 ; `Style `Filled ; `Fillcolor 0xffbbbb ]
+        in
+        l := values @ kind @ !l;
+        if not v.node_deps_computed then
+          l := [ `Style `Dotted ] @ !l;
+        !l
+      let get_subgraph v =
+        let {loc_file ; loc_callstack} = v.node_locality in
+        match loc_callstack with
+        | [] -> Some (get_file_subgraph loc_file)
+        | cs -> get_callstack_subgraph cs
+      let default_edge_attributes _g = []
+      let edge_attributes (_v1,e,_v2) =
+        let kind_attribute = match e.dependency_kind with
+          | Callee -> [`Color 0x00ff00 ]
+          | _ -> []
+        and folding_attribute = match e.dependency_multiple with
+          | true -> [ `Style `Bold ]
+          | false -> []
+        in kind_attribute @ folding_attribute
+    end)
+  in
+  Dot.output_graph out_channel g
+
+module JsonPrinter =
+struct
+  let output_kinstr = function
+    | Cil_types.Kglobal -> `String "global"
+    | Cil_types.Kstmt stmt -> `Int stmt.Cil_types.sid
+
+  let output_callsite (kf,kinstr) =
+    `Assoc [
+      ("fun", `String (Kernel_function.get_name kf)) ;
+      ("instr", output_kinstr kinstr) ;
+    ]
+
+  let output_callstack cs =
+    `List (List.map output_callsite cs)
+
+  let output_node_kind kind =
+    let s = match kind with
+      | Scalar _ -> "scalar"
+      | Composite _ -> "composite"
+      | Scattered _ -> "scattered"
+      | Alarm _ -> "alarm"
+    in
+    `String s
+
+  let output_node_locality { loc_file ; loc_callstack } =
+    let f1 = ("file", `String loc_file) in
+    let fields = match loc_callstack with
+      | [] -> [f1]
+      | cs -> [f1 ; ("callstack", output_callstack cs)]
+    in
+    `Assoc fields
+
+  let output_node_precision_grade grade =
+    let s = match grade with
+      | Singleton -> "singleton"
+      | Normal -> "normal"
+      | Wide -> "wide"
+    in
+    `String s
+
+  let output_dep_kind kind =
+    let s = match kind with
+      | Callee -> "callee"
+      | Data -> "data"
+      | Address -> "addr"
+      | Control -> "ctrl"
+      | Composition -> "comp"
+    in
+    `String s
+
+  let output_int_interval interval =
+    (* TODO: handle overflow *)
+    `Assoc [
+      ("min", `Int (Integer.to_int interval.min)) ;
+      ("max", `Int (Integer.to_int interval.max)) ;
+    ]
+
+  let output_float_interval interval =
+    `Assoc [
+      ("min", `Float interval.min) ;
+      ("max", `Float interval.max) ;
+    ]
+
+  let output_node_int_values values =
+    `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 =
+    `Assoc [
+      ("computed", output_float_interval values.values_interval) ;
+      ("limits", output_float_interval values.values_limits) ;
+      ("grade", output_node_precision_grade values.values_grade) ;
+    ]
+
+  let output_node node =
+    let label = Pretty_utils.to_string Node_kind.pretty node.node_kind in
+    `Assoc ([
+        ("id", `Int node.node_key) ;
+        ("label", `String label) ;
+        ("kind", output_node_kind node.node_kind) ;
+        ("locality", output_node_locality node.node_locality) ;
+        ("explored", `Bool node.node_deps_computed) ;
+      ] @
+        begin match node.node_int_values with
+          | None -> []
+          | Some node_values ->
+            [("int_values", output_node_int_values node_values)]
+        end @
+        begin match node.node_float_values with
+          | None -> []
+          | Some node_values ->
+            [("float_values", output_node_float_values node_values)]
+        end @
+        begin match Node_kind.to_lval node.node_kind with
+          | None -> []
+          | Some lval ->
+            let typ = Cil.typeOfLval lval in
+            let str = Pretty_utils.to_string Cil_printer.pp_typ typ in
+            [("type", `String str)]
+        end)
+
+  let output_dep (n1,dep,n2) =
+    `Assoc [
+      ("id", `Int dep.dependency_key) ;
+      ("src", `Int n1.node_key) ;
+      ("dst", `Int n2.node_key) ;
+      ("kind", output_dep_kind dep.dependency_kind) ;
+      ("multiple", `Bool dep.dependency_multiple)
+    ]
+
+  let output_graph g =
+    `Assoc [
+      ("nodes", `List (List.map output_node (vertices g))) ;
+      ("deps", `List (List.map output_dep (edges g)))
+    ]
+
+  let output_diff g diff =
+    let added_nodes = List.map output_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
+      List.map output_dep (Set.elements set)
+    and removed_nodes =
+      List.map (fun node -> `Int node.node_key) diff.removed_nodes
+    in
+    `Assoc [
+      ("add", `Assoc [
+          ("nodes", `List added_nodes) ;
+          ("deps", `List added_deps)
+        ]) ;
+      ("sub", `List removed_nodes)]
+end
+
+let ouptput_to_json out_channel g =
+  let json = JsonPrinter.output_graph g in
+  Yojson.Basic.to_channel out_channel json
+
+let to_json g =
+  JsonPrinter.output_graph g
+
+let diff_to_json g diff =
+  JsonPrinter.output_diff g diff

src/plugins/dive/imprecision_graph.mli

+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of Frama-C.                                         *)
+(*                                                                        *)
+(*  Copyright (C) 2007-2020                                               *)
+(*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
+(*         alternatives)                                                  *)
+(*                                                                        *)
+(*  you can redistribute it and/or modify it under the terms of the GNU   *)
+(*  Lesser General Public License as published by the Free Software       *)
+(*  Foundation, version 2.1.                                              *)
+(*                                                                        *)
+(*  It is distributed in the hope that it will be useful,                 *)
+(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
+(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
+(*  GNU Lesser General Public License for more details.                   *)
+(*                                                                        *)
+(*  See the GNU Lesser General Public License version 2.1                 *)
+(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
+(*                                                                        *)
+(**************************************************************************)
+
+open Graph_types
+
+include Graph.Sig.G
+  with type V.t = node
+   and type E.t = node * dependency * node
+
+module Node : Graph.Sig.COMPARABLE with type t = node
+
+module Dependency : Graph.Sig.COMPARABLE with type t = dependency
+
+val create : ?size:int -> unit -> t
+
+val create_node :
+  node_kind:node_kind ->
+  node_locality:node_locality -> t -> node
+
+val remove_node : t -> node -> unit
+
+val update_node_int_values : node -> Integer.t node_values -> unit
+val update_node_float_values : node -> float node_values -> unit
+
+val create_dependency : allow_folding:bool -> t -> node -> dependency_kind ->
+  node -> unit
+
+val remove_dependency : t -> node * dependency * node -> unit
+
+val find_independant_nodes : t -> node list -> node list
+
+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

src/plugins/dive/main.ml

+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of Frama-C.                                         *)
+(*                                                                        *)
+(*  Copyright (C) 2007-2020                                               *)
+(*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
+(*         alternatives)                                                  *)
+(*                                                                        *)
+(*  you can redistribute it and/or modify it under the terms of the GNU   *)
+(*  Lesser General Public License as published by the Free Software       *)
+(*  Foundation, version 2.1.                                              *)
+(*                                                                        *)
+(*  It is distributed in the hope that it will be useful,                 *)
+(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
+(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
+(*  GNU Lesser General Public License for more details.                   *)
+(*                                                                        *)
+(*  See the GNU Lesser General Public License version 2.1                 *)
+(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
+(*                                                                        *)
+(**************************************************************************)
+
+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
+    (* Create the initial graph  *)
+    let context = Build.create () in
+    (* Handle parameters *)
+    Self.UnfoldedBases.iter (Build.unfold_base context);
+    Self.HiddenBases.iter (Build.hide_base context);
+    let depth = Self.DepthLimit.get () in
+    (* Add targeted vars to it *)
+    Self.FromBases.iter (Build.add_var ~depth context);
+    (* Add alarms *)
+    let add_alarm _emitter kf stmt ~rank:_ alarm _code_annot =
+      if Self.FromFunctionAlarms.mem kf then
+        Build.add_alarm ~depth context stmt alarm
+    in
+    if not (Self.FromFunctionAlarms.is_empty ()) then
+      Alarms.iter add_alarm;
+    (* Output it *)
+    if Self.OutputDot.get () <> "" then
+      output Dot context (Self.OutputDot.get ());
+    if Self.OutputJson.get () <> "" then
+      output Json context (Self.OutputJson.get ());
+  end
+
+let () =
+  Db.Main.extend main

src/plugins/dive/node_kind.ml

+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of Frama-C.                                         *)
+(*                                                                        *)
+(*  Copyright (C) 2007-2020                                               *)
+(*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
+(*         alternatives)                                                  *)
+(*                                                                        *)
+(*  you can redistribute it and/or modify it under the terms of the GNU   *)
+(*  Lesser General Public License as published by the Free Software       *)
+(*  Foundation, version 2.1.                                              *)
+(*                                                                        *)
+(*  It is distributed in the hope that it will be useful,                 *)
+(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
+(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
+(*  GNU Lesser General Public License for more details.                   *)
+(*                                                                        *)
+(*  See the GNU Lesser General Public License version 2.1                 *)
+(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
+(*                                                                        *)
+(**************************************************************************)
+
+open Graph_types
+
+module DatatypeInput =
+struct
+  include Datatype.Undefined
+
+  open Cil_datatype
+
+  type t = node_kind
+
+  let (<?>) c (cmp,x,y) =
+    if c = 0
+    then cmp x y
+    else c
+
+  let name = "Node_kind"
+
+  let reprs = [ Scalar (
+      List.hd Varinfo.reprs,
+      List.hd Typ.reprs,
+      List.hd Offset.reprs) ]
+
+  let compare k1 k2 =
+    match k1, k2 with
+    | Scalar (vi1, _, offset1), Scalar (vi2, _, offset2) ->
+      Varinfo.compare vi1 vi2 <?> (OffsetStructEq.compare, offset1, offset2)
+    | Scalar _, _ -> 1
+    | _, Scalar _ -> -1
+    | Composite vi1, Composite vi2 -> Varinfo.compare vi1 vi2
+    | Composite _, _ -> 1
+    | _, Composite _ -> -1
+    | Scattered (lv1,ki1), Scattered (lv2,ki2) ->
+      LvalStructEq.compare lv1 lv2 <?> (Kinstr.compare, ki1, ki2)
+    | Scattered _, _ -> 1
+    | _, Scattered _ -> -1
+    | Alarm (stmt1, alarm1), Alarm (stmt2, alarm2) ->
+      Stmt.compare stmt1 stmt2 <?> (Alarms.compare, alarm1, alarm2)
+
+  let equal k1 k2 =
+    match k1, k2 with
+    | Scalar (vi1, _, offset1), Scalar (vi2, _, offset2) ->
+      Varinfo.equal vi1 vi2 && OffsetStructEq.equal offset1 offset2
+    | Composite vi1, Composite vi2 -> Varinfo.equal vi1 vi2
+    | Scattered (lv1, ki1), Scattered (lv2, ki2) ->
+      LvalStructEq.equal lv1 lv2 && Kinstr.equal ki1 ki2
+    | Alarm (stmt1, alarm1), Alarm (stmt2, alarm2) ->
+      Stmt.equal stmt1 stmt2 && Alarms.equal alarm1 alarm2
+    | _ -> false
+
+  let hash k =
+    match k with
+    | Scalar (vi, _, offset) ->
+      Hashtbl.hash (1, Varinfo.hash vi, OffsetStructEq.hash offset)
+    | Composite vi -> Hashtbl.hash (2, Varinfo.hash vi)
+    | Scattered (lv, ki) ->
+      Hashtbl.hash (3, LvalStructEq.hash lv, Kinstr.hash ki)
+    | Alarm (stmt, alarm) ->
+      Hashtbl.hash (4, Stmt.hash stmt, Alarms.hash alarm)
+end
+
+include Datatype.Make (DatatypeInput)
+
+
+let get_base = function
+  | Scalar (vi,_,_) | Composite (vi) -> Some vi
+  | Scattered _ | Alarm _ -> None
+
+let to_lval = function
+  | Scalar (vi,_typ,offset) -> Some (Cil_types.Var vi, offset)
+  | Composite (vi) -> Some (Cil_types.Var vi, Cil_types.NoOffset)
+  | Scattered (lval,_) -> Some lval
+  | Alarm (_,_) -> None
+
+let pretty fmt = function
+  | (Scalar _ | Composite _ | Scattered _) as kind ->
+    Cil_printer.pp_lval fmt (Extlib.the (to_lval kind))
+  | Alarm (_stmt,alarm) ->
+    Cil_printer.pp_predicate fmt (Alarms.create_predicate alarm)

src/plugins/dive/node_kind.mli

+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of Frama-C.                                         *)
+(*                                                                        *)
+(*  Copyright (C) 2007-2020                                               *)
+(*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
+(*         alternatives)                                                  *)
+(*                                                                        *)
+(*  you can redistribute it and/or modify it under the terms of the GNU   *)
+(*  Lesser General Public License as published by the Free Software       *)
+(*  Foundation, version 2.1.                                              *)
+(*                                                                        *)
+(*  It is distributed in the hope that it will be useful,                 *)
+(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
+(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
+(*  GNU Lesser General Public License for more details.                   *)
+(*                                                                        *)
+(*  See the GNU Lesser General Public License version 2.1                 *)
+(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
+(*                                                                        *)
+(**************************************************************************)
+
+include Datatype.S with type t = Graph_types.node_kind
+
+val get_base : t -> Cil_types.varinfo option
+val to_lval : t -> Cil_types.lval option

src/plugins/dive/self.ml

+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of Frama-C.                                         *)
+(*                                                                        *)
+(*  Copyright (C) 2007-2020                                               *)
+(*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
+(*         alternatives)                                                  *)
+(*                                                                        *)
+(*  you can redistribute it and/or modify it under the terms of the GNU   *)
+(*  Lesser General Public License as published by the Free Software       *)
+(*  Foundation, version 2.1.                                              *)
+(*                                                                        *)
+(*  It is distributed in the hope that it will be useful,                 *)
+(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
+(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
+(*  GNU Lesser General Public License for more details.                   *)
+(*                                                                        *)
+(*  See the GNU Lesser General Public License version 2.1                 *)
+(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
+(*                                                                        *)
+(**************************************************************************)
+
+open Cil_types
+
+include Plugin.Register
+    (struct
+      let name = "dive"
+      let shortname = "dive"
+      let help = "An interactive imprecision graph generator for Eva."
+    end)
+
+module OutputDot = Empty_string
+    (struct
+      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)
+
+module DepthLimit = Int
+    (struct
+      let option_name = "-dive-depth-limit"
+      let help = "Build dependencies up to a depth of N."
+      let arg_name = "N"
+      let default = 2
+    end)
+
+module FromFunctionAlarms = Kernel_function_set
+    (struct
+      let option_name = "-dive-from-alarms"
+      let help = "Build the graph from the alarms emitted in the given functions."
+      let arg_name = "f1,..."
+    end)
+
+module Varinfo =
+struct
+  include Cil_datatype.Varinfo
+
+  let of_string s =
+    let regexp = Str.regexp "^\\([_a-zA-Z0-9]+\\)::\\([_a-zA-Z0-9]+\\)$" in
+    if Str.string_match regexp s 0 then
+      let function_name = Str.matched_group 1 s
+      and variable_name = Str.matched_group 2 s in
+      let kf = try Globals.Functions.find_by_name function_name
+        with Not_found ->
+          raise (Cannot_build ("no function '" ^ function_name ^ "'"))
+      in
+      try Globals.Vars.find_from_astinfo variable_name (VLocal kf)
+      with Not_found ->
+      try Globals.Vars.find_from_astinfo variable_name (VFormal kf)
+      with Not_found ->
+        raise (Cannot_build ("no variable '" ^ variable_name ^ "' in function "
+                             ^ function_name))
+    else
+      let regexp = Str.regexp "^[_a-zA-Z0-9]+$" in
+      if not (Str.string_match regexp s 0) then
+        raise (Cannot_build ("wrong syntax: '" ^ s ^ "'"));
+      match Globals.Syntactic_search.find_in_scope s Cil_types.Program with
+      | Some vi -> vi
+      | None ->
+        raise (Cannot_build ("no global variable '" ^ s ^ "'"))
+
+  let to_string vi =
+    match Kernel_function.find_defining_kf vi with
+    | None -> vi.vname
+    | Some kf -> Kernel_function.get_name kf ^ "::" ^ vi.vname
+
+  let of_singleton_string = no_element_of_string
+end
+
+module type Varinfo_set = Parameter_sig.Set
+  with type elt = Cil_types.varinfo
+   and type t = Cil_datatype.Varinfo.Set.t
+
+module Varinfo_set (X: Parameter_sig.Input_with_arg) =
+  Make_set
+    (Varinfo)
+    (struct
+      include X
+      let dependencies = []
+      let default = Cil_datatype.Varinfo.Set.empty
+    end)
+
+module FromBases = Varinfo_set
+    (struct
+      let option_name = "-dive-from-variables"
+      let help = "Build the graph from these local variables."
+      let arg_name = "f::v,..."
+    end)
+
+module UnfoldedBases = Varinfo_set
+    (struct
+      let option_name = "-dive-unfold"
+      let help = "Defines the composite variables which should be \
+                  unfolded into individual cells."
+      let arg_name = "f::v,..."
+    end)
+
+module HiddenBases = Varinfo_set
+    (struct
+      let option_name = "-dive-hide"
+      let help = "Defines the variables which must not be \
+                  displayed in the graph. The dependencies for these bases \
+                  are not computed either."
+      let arg_name = "f::v,..."
+    end)

src/plugins/dive/self.mli

+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of Frama-C.                                         *)
+(*                                                                        *)
+(*  Copyright (C) 2007-2020                                               *)
+(*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
+(*         alternatives)                                                  *)
+(*                                                                        *)
+(*  you can redistribute it and/or modify it under the terms of the GNU   *)
+(*  Lesser General Public License as published by the Free Software       *)
+(*  Foundation, version 2.1.                                              *)
+(*                                                                        *)
+(*  It is distributed in the hope that it will be useful,                 *)
+(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
+(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
+(*  GNU Lesser General Public License for more details.                   *)
+(*                                                                        *)
+(*  See the GNU Lesser General Public License version 2.1                 *)
+(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
+(*                                                                        *)
+(**************************************************************************)
+
+include Plugin.S
+
+module type Varinfo_set = Parameter_sig.Set
+  with type elt = Cil_types.varinfo
+   and type t = Cil_datatype.Varinfo.Set.t
+
+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
+module UnfoldedBases : Varinfo_set
+module HiddenBases : Varinfo_set

src/plugins/dive/server_interface.ml

+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of Frama-C.                                         *)
+(*                                                                        *)
+(*  Copyright (C) 2007-2020                                               *)
+(*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
+(*         alternatives)                                                  *)
+(*                                                                        *)
+(*  you can redistribute it and/or modify it under the terms of the GNU   *)
+(*  Lesser General Public License as published by the Free Software       *)
+(*  Foundation, version 2.1.                                              *)
+(*                                                                        *)
+(*  It is distributed in the hope that it will be useful,                 *)
+(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
+(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
+(*  GNU Lesser General Public License for more details.                   *)
+(*                                                                        *)
+(*  See the GNU Lesser General Public License version 2.1                 *)
+(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
+(*                                                                        *)
+(**************************************************************************)
+
+open Server
+
+(* TODO: state *)
+let get_graph =
+  let graph = ref None in
+  fun () ->
+    match !graph with
+    | Some g -> g
+    | None ->
+      let g = Build.create () in
+      graph := Some g;
+      g
+
+
+let page = Doc.page (`Plugin "dive")
+    ~title:"Dive Services"
+    ~filename:"dive.md"
+
+module Graph =
+struct
+  type t = Imprecision_graph.t
+  let syntax = Syntax.any
+  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
+    let name = "dive-variable-name"
+    let descr = Markdown.plain "The name of variable of the program"
+
+    let signature = Data.Record.signature ~page ~name ~descr ()
+
+    let _fun_field = Data.Record.option signature
+        ~descr:(Markdown.plain "owner function for a local variable")
+        (module Data.Jstring)
+
+    let _var_field = Data.Record.field signature
+        ~descr:(Markdown.plain "variable name")
+        (module Data.Jstring)
+
+    type t = Cil_types.varinfo
+    module R =
+      (val (Data.Record.publish signature): Data.Record.S with type r = t)
+
+    let syntax = R.syntax
+
+    let to_json v =
+      let varname = v.Cil_types.vname 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
+      in
+      `Assoc fields
+
+    let of_json json =
+      let open Yojson.Basic.Util in
+      let funname =
+        try Some (json |> member "fun" |> to_string)
+        with Not_found -> None
+      and varname = json |> member "var" |> to_string in
+      match funname with
+      | Some name ->
+        let kf =
+          try
+            Globals.Functions.find_by_name name
+          with Not_found ->
+            Data.failure "no function '%s'" name
+        in
+        let vi =
+          try Globals.Vars.find_from_astinfo varname (Cil_types.VLocal kf)
+          with Not_found ->
+          try Globals.Vars.find_from_astinfo varname (Cil_types.VFormal kf)
+          with Not_found ->
+            Data.failure "no variable '%s' in function '%s'"
+              varname name
+        in
+        vi
+      | None ->
+        match
+          Globals.Syntactic_search.find_in_scope varname Cil_types.Program
+        with
+        | Some vi -> vi
+        | None ->
+          Data.failure "no global variable '%s'" varname
+  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.plain "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 "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.plain "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 "no node '%d' in the current graph" node_key
+  end)
+
+
+let () = Request.register ~page
+    ~kind:`GET ~name:"dive.graph"
+    ~descr:(Markdown.plain "Retrieve the whole graph")
+    ~input:(module Data.Junit) ~output:(module Graph)
+    (fun () -> Build.get_graph (get_graph ()))
+
+let () = Request.register ~page
+    ~kind:`EXEC ~name:"dive.clear"
+    ~descr:(Markdown.plain "Erase the graph and start over with an empty one")
+    ~input:(module Data.Junit) ~output:(module Data.Junit)
+    (fun () -> Build.clear (get_graph ()))
+
+let () = Request.register ~page
+    ~kind:`EXEC ~name:"dive.add_var"
+    ~descr:(Markdown.plain "Add a variable to the 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.take_last_differences g
+    end
+
+let () = Request.register ~page
+    ~kind:`EXEC ~name:"dive.add_function_alarms"
+    ~descr:(Markdown.plain "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.plain "Explore the graph starting from an existing vertex")
+    ~input:(module Node) ~output:(module GraphDiff)
+    begin fun node ->
+      let depth = Self.DepthLimit.get () in
+      let g = get_graph () in
+      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.plain "Show the dependencies of an existing vertex")
+    ~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;
+      Build.get_graph g, Build.take_last_differences g
+    end
+
+let () = Request.register ~page
+    ~kind:`EXEC ~name:"dive.hide"
+    ~descr:(Markdown.plain "Hide the dependencies of an existing vertex")
+    ~input:(module Node) ~output:(module GraphDiff)
+    begin fun node ->
+      let g = get_graph () in
+      Build.hide g node;
+      Build.get_graph g, Build.take_last_differences g
+    end

src/plugins/dive/server_interface.mli

+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of Frama-C.                                         *)
+(*                                                                        *)
+(*  Copyright (C) 2007-2020                                               *)
+(*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
+(*         alternatives)                                                  *)
+(*                                                                        *)
+(*  you can redistribute it and/or modify it under the terms of the GNU   *)
+(*  Lesser General Public License as published by the Free Software       *)
+(*  Foundation, version 2.1.                                              *)
+(*                                                                        *)
+(*  It is distributed in the hope that it will be useful,                 *)
+(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
+(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
+(*  GNU Lesser General Public License for more details.                   *)
+(*                                                                        *)
+(*  See the GNU Lesser General Public License version 2.1                 *)
+(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
+(*                                                                        *)
+(**************************************************************************)
+
+module Variable : Server.Data.S_collection with type t = Cil_types.varinfo