Merge branch 'feature/ivette/imprecision-graph' into 'master'

[Ivette] New componant for the data dependency graphs built by the Dive plugin

Closes #927, #926, and #925

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

headers/header_spec.txt

@@ -768,14 +768,18 @@ 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/context.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/dive/context.mli: CEA_LGPL_OR_PROPRIETARY
+src/plugins/dive/dive_graph.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/dive/dive_graph.mli: CEA_LGPL_OR_PROPRIETARY
+src/plugins/dive/dive_types.mli: 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/node_range.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/dive/node_range.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

ivette/api/kernel/ast/index.ts

@@ -227,6 +227,33 @@ export const jMarkerSafe: Json.Safe<marker> =
 /** Natural order for `marker` */
 export const byMarker: Compare.Order<marker> = Compare.structural;
 
+/** Location: function and marker */
+export interface location {
+  /** Function */
+  function: Json.key<'#fct'>;
+  /** Marker */
+  marker: marker;
+}
+
+/** Loose decoder for `location` */
+export const jLocation: Json.Loose<location> =
+  Json.jObject({
+    function: Json.jFail(Json.jKey<'#fct'>('#fct'),'#fct expected'),
+    marker: jMarkerSafe,
+  });
+
+/** Safe decoder for `location` */
+export const jLocationSafe: Json.Safe<location> =
+  Json.jFail(jLocation,'Location expected');
+
+/** Natural order for `location` */
+export const byLocation: Compare.Order<location> =
+  Compare.byFields
+    <{ function: Json.key<'#fct'>, marker: marker }>({
+    function: Compare.string,
+    marker: byMarker,
+  });
+
 const getFunctions_internal: Server.GetRequest<null,Json.key<'#fct'>[]> = {
   kind: Server.RqKind.GET,
   name:   'kernel.ast.getFunctions',

ivette/api/plugins/dive/index.ts

@@ -15,42 +15,296 @@ import * as Server from 'frama-c/server';
 //@ts-ignore
 import * as State from 'frama-c/states';
 
+//@ts-ignore
+import { byLocation } from 'api/kernel/ast';
+//@ts-ignore
+import { byMarker } from 'api/kernel/ast';
+//@ts-ignore
+import { jLocation } from 'api/kernel/ast';
+//@ts-ignore
+import { jLocationSafe } from 'api/kernel/ast';
+//@ts-ignore
+import { jMarker } from 'api/kernel/ast';
+//@ts-ignore
+import { jMarkerSafe } from 'api/kernel/ast';
+//@ts-ignore
+import { location } from 'api/kernel/ast';
+//@ts-ignore
+import { marker } from 'api/kernel/ast';
 
-/** The name of variable of the program */
-export interface variableName {
-  /** owner function for a local variable */
-  funName?: string;
-  /** variable name */
-  varName: string;
+/** Parametrization of the exploration range. */
+export interface range {
+  /** range for the write dependencies */
+  backward?: number;
+  /** range for the read dependencies */
+  forward?: number;
 }
 
-/** Loose decoder for `variableName` */
-export const jVariableName: Json.Loose<variableName> =
+/** Loose decoder for `range` */
+export const jRange: Json.Loose<range> =
+  Json.jObject({ backward: Json.jNumber, forward: Json.jNumber,});
+
+/** Safe decoder for `range` */
+export const jRangeSafe: Json.Safe<range> =
+  Json.jFail(jRange,'Range expected');
+
+/** Natural order for `range` */
+export const byRange: Compare.Order<range> =
+  Compare.byFields
+    <{ backward?: number, forward?: number }>({
+    backward: Compare.defined(Compare.number),
+    forward: Compare.defined(Compare.number),
+  });
+
+/** Global parametrization of the exploration. */
+export interface explorationWindow {
+  /** how far dive will explore from root nodes ; must be a finite range */
+  perception: range;
+  /** range beyond which the nodes must be hidden */
+  horizon: range;
+}
+
+/** Loose decoder for `explorationWindow` */
+export const jExplorationWindow: Json.Loose<explorationWindow> =
+  Json.jObject({ perception: jRangeSafe, horizon: jRangeSafe,});
+
+/** Safe decoder for `explorationWindow` */
+export const jExplorationWindowSafe: Json.Safe<explorationWindow> =
+  Json.jFail(jExplorationWindow,'ExplorationWindow expected');
+
+/** Natural order for `explorationWindow` */
+export const byExplorationWindow: Compare.Order<explorationWindow> =
+  Compare.byFields
+    <{ perception: range, horizon: range }>({
+    perception: byRange,
+    horizon: byRange,
+  });
+
+/** A node identifier in the graph */
+export type nodeId = number;
+
+/** Loose decoder for `nodeId` */
+export const jNodeId: Json.Loose<nodeId> = Json.jNumber;
+
+/** Safe decoder for `nodeId` */
+export const jNodeIdSafe: Json.Safe<nodeId> =
+  Json.jFail(Json.jNumber,'Number expected');
+
+/** Natural order for `nodeId` */
+export const byNodeId: Compare.Order<nodeId> = Compare.number;
+
+/** A callsite */
+export type callsite = { fun: string, instr: number | string };
+
+/** Loose decoder for `callsite` */
+export const jCallsite: Json.Loose<callsite> =
+  Json.jObject({
+    fun: Json.jFail(Json.jString,'String expected'),
+    instr: Json.jFail(
+             Json.jUnion<number | string>( Json.jNumber, Json.jString,),
+             'Union expected'),
+  });
+
+/** Safe decoder for `callsite` */
+export const jCallsiteSafe: Json.Safe<callsite> =
+  Json.jFail(jCallsite,'Callsite expected');
+
+/** Natural order for `callsite` */
+export const byCallsite: Compare.Order<callsite> =
+  Compare.byFields
+    <{ fun: string, instr: number | string }>({
+    fun: Compare.string,
+    instr: Compare.structural,
+  });
+
+/** The callstack context for a node */
+export type callstack = callsite[];
+
+/** Safe decoder for `callstack` */
+export const jCallstackSafe: Json.Safe<callstack> =
+  Json.jArray(jCallsiteSafe);
+
+/** Loose decoder for `callstack` */
+export const jCallstack: Json.Loose<callstack> = Json.jTry(jCallstackSafe);
+
+/** Natural order for `callstack` */
+export const byCallstack: Compare.Order<callstack> =
+  Compare.array(byCallsite);
+
+/** The description of a node locality */
+export type nodeLocality = { file: string, callstack?: callstack };
+
+/** Loose decoder for `nodeLocality` */
+export const jNodeLocality: Json.Loose<nodeLocality> =
   Json.jObject({
-    funName: Json.jString,
-    varName: Json.jFail(Json.jString,'String expected'),
+    file: Json.jFail(Json.jString,'String expected'),
+    callstack: jCallstack,
   });
 
-/** Safe decoder for `variableName` */
-export const jVariableNameSafe: Json.Safe<variableName> =
-  Json.jFail(jVariableName,'VariableName expected');
+/** Safe decoder for `nodeLocality` */
+export const jNodeLocalitySafe: Json.Safe<nodeLocality> =
+  Json.jFail(jNodeLocality,'NodeLocality expected');
 
-/** Natural order for `variableName` */
-export const byVariableName: Compare.Order<variableName> =
+/** Natural order for `nodeLocality` */
+export const byNodeLocality: Compare.Order<nodeLocality> =
   Compare.byFields
-    <{ funName?: string, varName: string }>({
-    funName: Compare.defined(Compare.alpha),
-    varName: Compare.alpha,
+    <{ file: string, callstack?: callstack }>({
+    file: Compare.string,
+    callstack: Compare.defined(byCallstack),
   });
 
-const graph_internal: Server.GetRequest<null,Json.json> = {
+/** A graph node */
+export type node =
+  { id: nodeId, label: string, kind: string, locality: nodeLocality,
+    is_root: boolean, backward_explored: string, forward_explored: string,
+    writes: location[], values?: string, range: number | string,
+    type?: string };
+
+/** Loose decoder for `node` */
+export const jNode: Json.Loose<node> =
+  Json.jObject({
+    id: jNodeIdSafe,
+    label: Json.jFail(Json.jString,'String expected'),
+    kind: Json.jFail(Json.jString,'String expected'),
+    locality: jNodeLocalitySafe,
+    is_root: Json.jFail(Json.jBoolean,'Boolean expected'),
+    backward_explored: Json.jFail(Json.jString,'String expected'),
+    forward_explored: Json.jFail(Json.jString,'String expected'),
+    writes: Json.jArray(jLocationSafe),
+    values: Json.jString,
+    range: Json.jFail(
+             Json.jUnion<number | string>( Json.jNumber, Json.jString,),
+             'Union expected'),
+    type: Json.jString,
+  });
+
+/** Safe decoder for `node` */
+export const jNodeSafe: Json.Safe<node> = Json.jFail(jNode,'Node expected');
+
+/** Natural order for `node` */
+export const byNode: Compare.Order<node> =
+  Compare.byFields
+    <{ id: nodeId, label: string, kind: string, locality: nodeLocality,
+       is_root: boolean, backward_explored: string, forward_explored: string,
+       writes: location[], values?: string, range: number | string,
+       type?: string }>({
+    id: byNodeId,
+    label: Compare.string,
+    kind: Compare.string,
+    locality: byNodeLocality,
+    is_root: Compare.boolean,
+    backward_explored: Compare.string,
+    forward_explored: Compare.string,
+    writes: Compare.array(byLocation),
+    values: Compare.defined(Compare.string),
+    range: Compare.structural,
+    type: Compare.defined(Compare.string),
+  });
+
+/** The dependency between two nodes */
+export type dependency =
+  { id: number, src: nodeId, dst: nodeId, kind: string, origins: location[] };
+
+/** Loose decoder for `dependency` */
+export const jDependency: Json.Loose<dependency> =
+  Json.jObject({
+    id: Json.jFail(Json.jNumber,'Number expected'),
+    src: jNodeIdSafe,
+    dst: jNodeIdSafe,
+    kind: Json.jFail(Json.jString,'String expected'),
+    origins: Json.jArray(jLocationSafe),
+  });
+
+/** Safe decoder for `dependency` */
+export const jDependencySafe: Json.Safe<dependency> =
+  Json.jFail(jDependency,'Dependency expected');
+
+/** Natural order for `dependency` */
+export const byDependency: Compare.Order<dependency> =
+  Compare.byFields
+    <{ id: number, src: nodeId, dst: nodeId, kind: string,
+       origins: location[] }>({
+    id: Compare.number,
+    src: byNodeId,
+    dst: byNodeId,
+    kind: Compare.string,
+    origins: Compare.array(byLocation),
+  });
+
+/** The whole graph being built */
+export type graphData = { nodes: node[], deps: dependency[] };
+
+/** Loose decoder for `graphData` */
+export const jGraphData: Json.Loose<graphData> =
+  Json.jObject({
+    nodes: Json.jArray(jNodeSafe),
+    deps: Json.jArray(jDependencySafe),
+  });
+
+/** Safe decoder for `graphData` */
+export const jGraphDataSafe: Json.Safe<graphData> =
+  Json.jFail(jGraphData,'GraphData expected');
+
+/** Natural order for `graphData` */
+export const byGraphData: Compare.Order<graphData> =
+  Compare.byFields
+    <{ nodes: node[], deps: dependency[] }>({
+    nodes: Compare.array(byNode),
+    deps: Compare.array(byDependency),
+  });
+
+/** Graph differences from the last action. */
+export type diffData =
+  { root?: nodeId, add: { nodes: node[], deps: dependency[] }, sub: nodeId[]
+    };
+
+/** Loose decoder for `diffData` */
+export const jDiffData: Json.Loose<diffData> =
+  Json.jObject({
+    root: jNodeId,
+    add: Json.jFail(
+           Json.jObject({
+             nodes: Json.jArray(jNodeSafe),
+             deps: Json.jArray(jDependencySafe),
+           }),'Record expected'),
+    sub: Json.jArray(jNodeIdSafe),
+  });
+
+/** Safe decoder for `diffData` */
+export const jDiffDataSafe: Json.Safe<diffData> =
+  Json.jFail(jDiffData,'DiffData expected');
+
+/** Natural order for `diffData` */
+export const byDiffData: Compare.Order<diffData> =
+  Compare.byFields
+    <{ root?: nodeId, add: { nodes: node[], deps: dependency[] },
+       sub: nodeId[] }>({
+    root: Compare.defined(byNodeId),
+    add: Compare.byFields
+           <{ nodes: node[], deps: dependency[] }>({
+           nodes: Compare.array(byNode),
+           deps: Compare.array(byDependency),
+         }),
+    sub: Compare.array(byNodeId),
+  });
+
+const window_internal: Server.SetRequest<explorationWindow,null> = {
+  kind: Server.RqKind.SET,
+  name:   'plugins.dive.window',
+  input:  jExplorationWindow,
+  output: Json.jNull,
+};
+/** Set the exploration window */
+export const window: Server.SetRequest<explorationWindow,null>= window_internal;
+
+const graph_internal: Server.GetRequest<null,graphData> = {
   kind: Server.RqKind.GET,
   name:   'plugins.dive.graph',
   input:  Json.jNull,
-  output: Json.jAny,
+  output: jGraphData,
 };
 /** Retrieve the whole graph */
-export const graph: Server.GetRequest<null,Json.json>= graph_internal;
+export const graph: Server.GetRequest<null,graphData>= graph_internal;
 
 const clear_internal: Server.ExecRequest<null,null> = {
   kind: Server.RqKind.EXEC,
@@ -61,58 +315,40 @@ const clear_internal: Server.ExecRequest<null,null> = {
 /** Erase the graph and start over with an empty one */
 export const clear: Server.ExecRequest<null,null>= clear_internal;
 
-const addVar_internal: Server.ExecRequest<variableName,Json.json> = {
+const add_internal: Server.ExecRequest<marker,diffData> = {
   kind: Server.RqKind.EXEC,
-  name:   'plugins.dive.addVar',
-  input:  jVariableName,
-  output: Json.jAny,
+  name:   'plugins.dive.add',
+  input:  jMarker,
+  output: jDiffData,
 };
-/** Add a variable to the graph */
-export const addVar: Server.ExecRequest<variableName,Json.json>= addVar_internal;
+/** Add a node to the graph */
+export const add: Server.ExecRequest<marker,diffData>= add_internal;
 
-const addFunctionAlarms_internal: Server.ExecRequest<
-  Json.key<'#fct'>,
-  Json.json
-  > = {
-  kind: Server.RqKind.EXEC,
-  name:   'plugins.dive.addFunctionAlarms',
-  input:  Json.jKey<'#fct'>('#fct'),
-  output: Json.jAny,
-};
-/** Add all alarms of the given function */
-export const addFunctionAlarms: Server.ExecRequest<
-  Json.key<'#fct'>,
-  Json.json
-  >= addFunctionAlarms_internal;
-
-const explore_internal: Server.ExecRequest<
-  Json.index<'#dive-node'>,
-  Json.json
-  > = {
+const explore_internal: Server.ExecRequest<nodeId,diffData> = {
   kind: Server.RqKind.EXEC,
   name:   'plugins.dive.explore',
-  input:  Json.jIndex<'#dive-node'>('#dive-node'),
-  output: Json.jAny,
+  input:  jNodeId,
+  output: jDiffData,
 };
 /** Explore the graph starting from an existing vertex */
-export const explore: Server.ExecRequest<Json.index<'#dive-node'>,Json.json>= explore_internal;
+export const explore: Server.ExecRequest<nodeId,diffData>= explore_internal;
 
-const show_internal: Server.ExecRequest<Json.index<'#dive-node'>,Json.json> = {
+const show_internal: Server.ExecRequest<nodeId,diffData> = {
   kind: Server.RqKind.EXEC,
   name:   'plugins.dive.show',
-  input:  Json.jIndex<'#dive-node'>('#dive-node'),
-  output: Json.jAny,
+  input:  jNodeId,
+  output: jDiffData,
 };
 /** Show the dependencies of an existing vertex */
-export const show: Server.ExecRequest<Json.index<'#dive-node'>,Json.json>= show_internal;
+export const show: Server.ExecRequest<nodeId,diffData>= show_internal;
 
-const hide_internal: Server.ExecRequest<Json.index<'#dive-node'>,Json.json> = {
+const hide_internal: Server.ExecRequest<nodeId,diffData> = {
   kind: Server.RqKind.EXEC,
   name:   'plugins.dive.hide',
-  input:  Json.jIndex<'#dive-node'>('#dive-node'),
-  output: Json.jAny,
+  input:  jNodeId,
+  output: jDiffData,
 };
 /** Hide the dependencies of an existing vertex */
-export const hide: Server.ExecRequest<Json.index<'#dive-node'>,Json.json>= hide_internal;
+export const hide: Server.ExecRequest<nodeId,diffData>= hide_internal;
 
 /* ------------------------------------- */

ivette/api/server_tsc.ml

@@ -167,7 +167,7 @@ let rec makeDecoder ~safe ?self ~names fmt js =
   | Jboolean -> jsafe ~safe "Boolean" jprim fmt "jBoolean"
   | Jnumber -> jsafe ~safe "Number" jprim fmt "jNumber"
   | Jstring | Jalpha -> jsafe ~safe "String" jprim fmt "jString"
-  | Jtag a -> Format.fprintf fmt "jTag(\"%s\")" a
+  | Jtag a -> Format.fprintf fmt "Json.jTag(\"%s\")" a
   | Jkey kd -> jsafe ~safe ("#" ^ kd) jkey fmt kd
   | Jindex kd -> jsafe ~safe ("#" ^ kd) jindex fmt kd
   | Jdata id -> jcall names fmt (Pkg.Derived.decode ~safe id)
@@ -188,6 +188,10 @@ let rec makeDecoder ~safe ?self ~names fmt js =
   | Jrecord jfs -> jsafe ~safe "Record" (jrecord ~makeSafe) fmt jfs
   | Jtuple jts -> jtry ~safe (jtuple ~makeSafe) fmt jts
 
+let makeLooseNeedSafe = function
+  | Pkg.Jtuple _ | Pkg.Jarray _ -> true
+  | _ -> false
+
 let makeRootDecoder ~safe ~self ~names fmt js =
   let open Pkg in
   match js with
@@ -414,12 +418,13 @@ let makeDeclaration fmt names d =
 type ranking = {
   mutable rank : int ;
   mutable mark : int Pkg.IdMap.t ;
+  index : Pkg.declInfo Pkg.IdMap.t ;
 }
 
 let depends d =
   match d.Pkg.d_kind with
-  | D_loose(id,(Jtuple _ | Jarray _)) -> [Pkg.Derived.safe id]
-  | D_safe(id,_) -> [Pkg.Derived.loose id]
+  | D_loose(id,t) when makeLooseNeedSafe t -> [Pkg.Derived.safe id]
+  | D_safe(id,t) when not (makeLooseNeedSafe t) -> [Pkg.Derived.loose id]
   | D_array _ ->
     let id = d.d_ident in
     let data = Pkg.Derived.data id in
@@ -439,13 +444,20 @@ let next m id =
   m.mark <- Pkg.IdMap.add id r m.mark ;
   m.rank <- succ r
 
-let mark m d =
+let rec mark m d =
   let id = d.Pkg.d_ident in
   if not (Pkg.IdMap.mem id m.mark) then
-    ( List.iter (next m) (depends d) ; next m id )
+    ( List.iter (mark_id m) (depends d) ; next m id )
+
+and mark_id m id =
+  try mark m (Pkg.IdMap.find id m.index)
+  with Not_found -> ()
 
 let ranking ds =
-  let m = { rank = 0 ; mark = Pkg.IdMap.empty } in
+  let index = List.fold_left
+      (fun m d -> Pkg.IdMap.add d.Pkg.d_ident d m)
+      Pkg.IdMap.empty ds in
+  let m = { rank = 0 ; mark = Pkg.IdMap.empty ; index } in
   List.iter (mark m) ds ;
   let rk = m.mark in
   let getRank a = try Pkg.IdMap.find a.Pkg.d_ident rk with Not_found -> 0 in

ivette/package.json

@@ -22,6 +22,7 @@
     "@babel/preset-typescript": "^7.9.0",
     "@hot-loader/react-dom": "^16.13.0",
     "@types/codemirror": "^0.0.89",
+    "@types/cytoscape": "^3.14.5",
     "@types/lodash": "^4.14.149",
     "@types/node": "12.12.21",
     "@types/react": "^16.9.17",
@@ -53,15 +54,25 @@
   },
   "dependencies": {
     "@babel/runtime": "^7.9.2",
+    "@fortawesome/fontawesome-free": "^5.13.1",
     "codemirror": "^5.52.2",
+    "cytoscape": "^3.15.1",
+    "cytoscape-cola": "^2.3.1",
+    "cytoscape-cose-bilkent": "^4.1.0",
+    "cytoscape-cxtmenu": "^3.1.2",
+    "cytoscape-dagre": "^2.2.2",
+    "cytoscape-klay": "^3.1.3",
+    "cytoscape-popper": "^1.0.7",
     "immutable": "^4.0.0-rc.12",
     "lodash": "^4.17.15",
     "react": "^16.8",
+    "react-cytoscapejs": "^1.2.1",
     "react-dom": "^16.13.1",
     "react-draggable": "^4.2.0",
     "react-fast-compare": "^3.2.0",
     "react-virtualized": "^9.21.2",
     "source-map-support": "^0.5.16",
+    "tippy.js": "5.2.1",
     "zeromq": "^6.0.0-beta.5"
   }
 }

ivette/src/dome/src/renderer/data/json.ts

@@ -188,7 +188,7 @@ export function jCatch<A>(fn: Loose<A>, fallBack: A): Safe<A> {
     try {
       return fn(js) ?? fallBack;
     } catch (err) {
-      if (DEVEL) console.error('[Dome.json]', err);
+      if (DEVEL) console.warn('[Dome.json]', err);
       return fallBack;
     }
   };
@@ -202,7 +202,8 @@ export function jTry<A>(fn: Loose<A>, defaultValue?: A): Loose<A> {
   return (js: json) => {
     try {
       return fn(js) ?? defaultValue;
-    } catch (_err) {
+    } catch (err) {
+      if (DEVEL) console.warn('[Dome.json]', err);
       return defaultValue;
     }
   };

ivette/src/frama-c/dive/Dive.tsx

+import React, { useState, useEffect } from 'react';
+import _ from 'lodash';
+import { renderToString } from 'react-dom/server';
+import * as Dome from 'dome';
+import * as Server from 'frama-c/server';
+import * as States from 'frama-c/states';
+
+import * as API from 'api/plugins/dive';
+
+import Cytoscape from 'cytoscape';
+import CytoscapeComponent from 'react-cytoscapejs';
+import './cytoscape_libs';
+
+import tippy, * as Tippy from 'tippy.js';
+import 'tippy.js/dist/tippy.css';
+import 'tippy.js/themes/light-border.css';
+import 'tippy.js/animations/shift-away.css';
+import './tippy.css';