diff --git a/ivette/src/frama-c/plugins/dive/dive.css b/ivette/src/frama-c/plugins/dive/dive.css
new file mode 100644
index 0000000000000000000000000000000000000000..9cf41c0888e3f71613cd848124a0377f56710ae4
--- /dev/null
+++ b/ivette/src/frama-c/plugins/dive/dive.css
@@ -0,0 +1,55 @@
+.legend {
+ position: absolute;
+ z-index: 4;
+ right: 10px;
+ top: 30px;
+ width: 170px;
+ height: 420px;
+ box-shadow: 3px 3px 2px rgba(0, 0, 0, .4);
+ background-color: var(--background-profound);
+}
+
+.diveTree {
+ overflow: auto;
+}
+
+.diveTree ul {
+ list-style: none;
+ border-left: 1px dotted black;
+ margin-left: 8px;
+ padding-left: 12px;
+}
+
+.diveTree .folder {
+ width: 16px;
+ height: 16px;
+ cursor: pointer;
+ /* border: 1px solid var(--text); */
+}
+
+.diveTree .exploration {
+ width: 20px;
+ height: 20px;
+ vertical-align: middle;
+}
+
+.diveTree .marker > .label {
+ text-overflow: ellipsis;
+ width: 240px;
+ white-space: nowrap;
+ display: inline-block;
+ overflow: hidden;
+ vertical-align: middle;
+}
+
+.diveTree .selected {
+ background: var(--code-select);
+}
+
+.diveTree .hovered {
+ background: var(--code-hover);
+}
+
+.diveTree .marker {
+ cursor: pointer;
+}
diff --git a/ivette/src/frama-c/plugins/dive/graph.tsx b/ivette/src/frama-c/plugins/dive/graph.tsx
new file mode 100644
index 0000000000000000000000000000000000000000..160e228eba10f4257be125ce5e143d71a6d3a71b
--- /dev/null
+++ b/ivette/src/frama-c/plugins/dive/graph.tsx
@@ -0,0 +1,762 @@
+/* ************************************************************************ */
+/* */
+/* This file is part of Frama-C. */
+/* */
+/* Copyright (C) 2007-2023 */
+/* 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). */
+/* */
+/* ************************************************************************ */
+
+import React, { useState, useEffect, useImperativeHandle, useRef } from 'react';
+import _ from 'lodash';
+import { renderToString } from 'react-dom/server';
+import * as Dome from 'dome';
+import * as Ivette from 'ivette';
+import * as Server from 'frama-c/server';
+import * as States from 'frama-c/states';
+
+import * as API from './api';
+
+import Cytoscape from 'cytoscape';
+import CytoscapeComponent from 'react-cytoscapejs';
+import './cytoscape_libs';
+import 'cytoscape-panzoom/cytoscape.js-panzoom.css';
+
+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';
+
+import { IconButton } from 'dome/controls/buttons';
+import { Space } from 'dome/frame/toolbars';
+
+import '@fortawesome/fontawesome-free/js/all';
+
+import EvaReady from 'frama-c/plugins/eva/EvaReady';
+import Legend from './legend';
+import style from './style.json';
+import layouts from './layouts.json';
+import './dive.css';
+
+const Debug = new Dome.Debug('dive');
+
+interface Cxtcommand {
+ content: string;
+ select: () => void;
+ enabled: boolean;
+}
+
+interface CytoscapeExtended extends Cytoscape.Core {
+ cxtmenu(options: unknown): void;
+ panzoom(options: unknown): void;
+}
+
+type Identified = { id: string }
+type NodeData = Cytoscape.NodeDataDefinition & Identified
+type EdgeData = { id: string;[key: string]: unknown }
+type NodeOrId = string | Cytoscape.NodeSingular
+
+function callstackToString(callstack: API.callstack): string {
+ return callstack.map((cs) => `${cs.fun}:${cs.instr}`).join('/');
+}
+
+function buildCxtMenu(
+ commands: Cxtcommand[],
+ content?: JSX.Element,
+ action?: () => void,
+): void {
+ commands.push({
+ content: content ? renderToString(content) : '',
+ select: action || (() => { /* Do nothing */ }),
+ enabled: !!action,
+ });
+}
+
+/* double click events for Cytoscape */
+
+function enableDoubleClickEvents(cy: Cytoscape.Core, delay = 350): void {
+ let last: Cytoscape.EventObject | undefined;
+ cy.on('click', (e) => {
+ if (last && last.target === e.target &&
+ e.timeStamp - last.timeStamp < delay) {
+ e.target.trigger('double-click', e);
+ }
+ last = e;
+ });
+}
+
+/* The Dive class handles the selection of nodes according to user actions.
+ To prevent cytoscape to automatically select (and unselect) nodes wrongly,
+ we make some nodes unselectable. We then use the functions below to make
+ the nodes selectable before (un)selecting them. */
+
+function select(node: Cytoscape.NodeSingular): void {
+ node.selectify();
+ node.select();
+}
+
+function unselect(node: Cytoscape.NodeSingular): void {
+ node.selectify();
+ node.unselect();
+}
+
+export type mode = 'explore' | 'overview';
+
+class Dive {
+ headless: boolean;
+ cy: Cytoscape.Core;
+ mode: mode = 'explore';
+ _layout = '';
+ layoutOptions: Cytoscape.LayoutOptions | undefined;
+ currentSelection: string | null = null;
+ onSelect: ((_: States.Location[]) => void) | null = null;
+ selectedLocation: (States.Location | undefined) = undefined;
+
+ constructor(cy: Cytoscape.Core | null = null) {
+ this.cy = cy || Cytoscape();
+ this.headless = this.cy.container() === null;
+ this.cy.elements().remove();
+
+ this.cy.minZoom(1e-1);
+ this.cy.maxZoom(1.0);
+
+ // Remove previous listeners
+ this.cy.off('click');
+ this.cy.off('double-click');
+
+ // Add new listeners
+ enableDoubleClickEvents(this.cy);
+ this.cy.on('click', 'node', (event) => this.clickNode(event.target));
+ this.cy.on('click', 'edge', (event) => this.clickEdge(event.target));
+ this.cy.on('double-click', '$node > node', // compound nodes
+ (event) => this.doubleClickNode(event.target));
+
+ // Set zoom limits
+ const panzoomDefaults = {
+ minZoom: this.cy.minZoom(),
+ maxZoom: this.cy.maxZoom(),
+ };
+ (this.cy as CytoscapeExtended).panzoom(panzoomDefaults);
+
+ // Default layout
+ this.layout = 'dagre';
+
+ // Contextual menu
+ if (!this.headless) {
+ this.cy.scratch('cxtmenu')?.destroy?.(); // Remove previous menu
+ this.cy.scratch('cxtmenu', (this.cy as CytoscapeExtended).cxtmenu({
+ selector: 'node',
+ commands: (node: Cytoscape.NodeSingular) => this.onCxtMenu(node),
+ }));
+ }
+
+ // Node width hack
+ const padding = 10;
+ const min = 50;
+ /* eslint-disable @typescript-eslint/no-explicit-any */
+ if (this.cy.style() && !this.headless) {
+ const canvas = document.querySelector('canvas[data-id="layer2-node"]');
+ if (canvas instanceof HTMLCanvasElement) {
+ const context = canvas.getContext('2d');
+ if (context) {
+ (this.cy.style() as any).selector('node').style('width',
+ (node: any) => {
+ const fStyle = node.pstyle('font-style').strValue;
+ const weight = node.pstyle('font-weight').strValue;
+ const size = node.pstyle('font-size').pfValue;
+ const family = node.pstyle('font-family').strValue;
+ context.font = `${fStyle} ${weight} ${size}px ${family}`;
+ const width = context.measureText(node.data('label')).width;
+ return `${Math.max(min, width + padding)}px`;
+ });
+ }
+ }
+ }
+ /* eslint-enable @typescript-eslint/no-explicit-any */
+ }
+
+ onCxtMenu(node: Cytoscape.NodeSingular): Cxtcommand[] {
+ const data = node.data();
+ const commands = [] as Cxtcommand[];
+ buildCxtMenu(commands,
+ <><div className="fas fa-binoculars fa-2x" />Explore</>,
+ () => { this.explore(node); });
+ if (data.nkind === 'composite')
+ buildCxtMenu(commands,
+ <><div className="fa fa-expand-arrows-alt fa-2x" />Unfold</>);
+ else
+ buildCxtMenu(commands);
+ if (data.backward_explored === 'no')
+ buildCxtMenu(commands,
+ <div><div className="fa fa-eye fa-2x" />Show</div>,
+ () => this.show(node));
+ else
+ buildCxtMenu(commands,
+ <><div className="fa fa-eye-slash fa-2x" />Hide</>,
+ () => this.hide(node));
+ return commands;
+ }
+
+ remove(node: Cytoscape.NodeSingular): void {
+ const parent = node.parent();
+ node.remove();
+ this.cy.$id(`${node.id()}-more`).remove();
+ if (parent.nonempty() && parent.children().empty())
+ this.remove(parent as Cytoscape.NodeSingular); // Recursively remove parents
+ }
+
+ referenceFile(fileName: string): Cytoscape.NodeSingular {
+ const id = `file_${fileName}`;
+ const node = this.cy.$id(id);
+ if (node.nonempty()) {
+ return node;
+ }
+
+ const nodeDefinition = {
+ data: { id, label: fileName },
+ classes: 'file',
+ pannable: true,
+ };
+ // cytoscape.add type declaration is missing the 'pannable' field
+ // eslint-disable-next-line @typescript-eslint/ban-ts-comment
+ // @ts-ignore
+ return this.cy.add(nodeDefinition);
+ }
+
+ referenceCallstack(callstack: API.callstack): Cytoscape.NodeSingular | null {
+ const name = callstackToString(callstack);
+ const elt = callstack.shift();
+
+ if (!elt)
+ return null;
+
+ const id = `callstack_${name}`;
+ const node = this.cy.$id(id);
+ if (node.nonempty()) {
+ return node;
+ }
+
+ const parentNode = this.referenceCallstack(callstack);
+ const nodeDefinition = {
+ data: { id, label: elt.fun, parent: parentNode?.id() },
+ classes: 'function',
+ pannable: true
+ };
+ // cytoscape.add type declaration is missing the 'pannable' field
+ // eslint-disable-next-line @typescript-eslint/ban-ts-comment
+ // @ts-ignore
+ return this.cy.add(nodeDefinition);
+ }
+
+ createTips(node: Cytoscape.NodeSingular): Tippy.Instance[] {
+ const container = this.cy.container();
+ if (!container)
+ return [];
+
+ // eslint-disable-next-line @typescript-eslint/no-explicit-any
+ const ref = (node as any).popperRef();
+ const common = {
+ getReferenceClientRect: ref.getBoundingClientRect,
+ interactive: true,
+ animation: 'shift-away',
+ duration: 500,
+ trigger: 'manual',
+ appendTo: document.body,
+ };
+
+ const tips = [];
+
+ if (node.data().values) {
+ tips.push(tippy(container, {
+ ...common,
+ content: node.data().values,
+ placement: 'top',
+ offset: [0, 20],
+ arrow: true,
+ }));
+ }
+
+ if (node.data().type) {
+ tips.push(tippy(container, {
+ ...common,
+ content: node.data().type,
+ placement: 'bottom',
+ offset: [0, 20],
+ theme: 'light-border',
+ arrow: false,
+ }));
+ }
+
+ return tips;
+ }
+
+ addTips(node: Cytoscape.NodeSingular): void {
+ let timeout: NodeJS.Timeout;
+ let tips: Tippy.Instance[] | null = null;
+
+ node.on('mouseover', () => {
+ if (tips === null) {
+ tips = this.createTips(node);
+ tips.forEach((tip) => tip.props.onHidden = (() => tip.destroy()));
+ }
+ clearTimeout(timeout);
+ timeout = setTimeout(() => tips?.forEach((tip) => {
+ tip.show();
+ }), 200);
+ });
+
+ node.on('mouseout', () => {
+ clearTimeout(timeout);
+ timeout = setTimeout(() => {
+ tips?.forEach((tip) => tip.hide());
+ tips = null; // Force rebuilding tips in case they changed
+ }, 0);
+ });
+ }
+
+ updateElement(group: Cytoscape.ElementGroup, data: NodeData | EdgeData):
+ Cytoscape.CollectionReturnValue {
+ let element = this.cy.$id(data.id);
+ if (element.nonempty()) {
+ element.removeData();
+ element.data(data);
+ }
+ else {
+ element = this.cy.add({ group, data });
+ element.addClass("new");
+ }
+ element.removeClass("stale");
+ return element;
+ }
+
+ updateNode(data: NodeData):
+ Cytoscape.NodeSingular {
+ const element = this.updateElement("nodes", data);
+ element.addClass('node');
+ return element;
+ }
+
+ updateEdge(src: NodeOrId, dst: NodeOrId, data: EdgeData):
+ Cytoscape.EdgeSingular {
+ const source = typeof src === "string" ? src : src.id();
+ const target = typeof dst === "string" ? dst : dst.id();
+ data = { ...data, source, target };
+ const element = this.updateElement("edges", data);
+ element.addClass('dependency');
+ return element;
+ }
+
+ updateNodeData(node: API.node): void {
+ const data = { ...node, id: `${node.id}` } as NodeData;
+
+ // Interval range visualization (see cytoscape stops style property)
+ if (typeof node.range === 'number')
+ data.stops = `0% ${node.range}% ${node.range}% 100%`;
+
+ // Build clusters for this node if needed
+ if (node.locality.callstack)
+ data.parent = this.referenceCallstack(node.locality.callstack)?.id();
+ else
+ data.parent = this.referenceFile(node.locality.file).id();
+
+ // Add new node or update existing node
+ const ele = this.updateNode(data);
+ if (ele.hasClass("new"))
+ this.addTips(ele);
+
+ // Add a node for the user to ask for more dependencies
+ const idmore = `${node.id}-more`;
+ if (node.backward_explored === 'partial') {
+ const elemore = this.updateNode({ id: idmore, parent: data.parent });
+ elemore.addClass("more");
+ this.updateEdge(elemore, ele, { id: `e${node.id}-more` });
+ }
+ else {
+ this.cy.$id(idmore).remove();
+ }
+ }
+
+ updateEdgeData(edge: API.dependency): void {
+ const data = { ...edge, id: `e${edge.id}` } as EdgeData;
+ this.updateEdge(`${edge.src}`, `${edge.dst}`, data);
+ }
+
+ updateGraph(data: API.graphData[]): void {
+ this.cy.startBatch();
+ this.cy.$('.node, .dependency').addClass('stale');
+
+ // Update vertices
+ for (const d of data) {
+ if ('nkind' in d.element) // Node
+ this.updateNodeData(d.element);
+ }
+
+ // Edges must be updated after vertices since their sources and destination
+ // must have been created beforhand
+ for (const d of data) {
+ if ('dkind' in d.element) // Dependency
+ this.updateEdgeData(d.element);
+ }
+
+ // Remove nodes that are not present anymore
+ this.cy.$('.stale').forEach(n => this.remove(n));
+
+ this.cy.endBatch();
+
+ this.recomputeLayout(this.cy.$('node.new'));
+ }
+
+ get layout(): string {
+ return this._layout;
+ }
+
+ set layout(layout: string) {
+ if (layout === this._layout)
+ return;
+ let extendedOptions = {};
+ if (layout in layouts)
+ extendedOptions = (layouts as { [key: string]: object })[layout];
+ this._layout = layout;
+ this.layoutOptions = {
+ name: layout,
+ fit: true,
+ animate: true,
+ randomize: false, /* Keep previous positions if layout supports it */
+ ...extendedOptions,
+ };
+
+ this.recomputeLayout();
+ }
+
+ recomputeLayout(newNodes?: Cytoscape.Collection): void {
+ if (this.layoutOptions && this.cy.container() &&
+ (newNodes === undefined || !newNodes.empty())) {
+ this.cy.layout({
+ animationEasing: 'ease-in-out-quad',
+ /* Do not move new nodes */
+ animateFilter: (node: Cytoscape.Singular) => newNodes === undefined ||
+ !newNodes.contains(node),
+ stop: () => {
+ this.cy.$('.new').addClass('old').removeClass('new');
+ },
+ ...this.layoutOptions,
+ } as unknown as Cytoscape.LayoutOptions).run();
+ }
+ }
+
+ async exec<In>(
+ request: Server.ExecRequest<In, number | undefined | null>,
+ param: In): Promise<Cytoscape.NodeSingular | undefined> {
+ try {
+ if (Server.isRunning()) {
+ await this.setMode();
+ const r = await Server.send(request, param);
+ if (r) {
+ return undefined;
+ }
+ }
+ }
+ catch (err) {
+ Debug.error(err);
+ }
+
+ return undefined;
+ }
+
+ static async setWindow(window: API.explorationWindow): Promise<void> {
+ if (Server.isRunning())
+ await Server.send(API.window, window);
+ }
+
+ async setMode(): Promise<void> {
+ switch (this.mode) {
+ case 'explore':
+ await Dive.setWindow({
+ perception: { backward: 3, forward: 1 },
+ horizon: { backward: 3, forward: 1 },
+ });
+ break;
+ case 'overview':
+ await Dive.setWindow({
+ perception: { backward: 4, forward: 1 },
+ horizon: { backward: undefined, forward: undefined },
+ });
+ break;
+ default: /* This is useless and impossible if the program is correctly
+ typed, but the linter wants it */
+ }
+ }
+
+ clear(): void {
+ this.cy.elements().remove();
+ this.exec(API.clear, null);
+ }
+
+ async add(marker: string): Promise<void> {
+ const node = await this.exec(API.add, marker);
+ if (node)
+ this.updateNodeSelection(node);
+ }
+
+ async explore(node: Cytoscape.NodeSingular): Promise<void> {
+ const id = parseInt(node.id(), 10);
+ if (id)
+ await this.exec(API.explore, id);
+ }
+
+ show(node: Cytoscape.NodeSingular): void {
+ const id = parseInt(node.id(), 10);
+ if (id)
+ this.exec(API.show, id);
+ }
+
+ hide(node: Cytoscape.NodeSingular): void {
+ const id = parseInt(node.id(), 10);
+ if (id)
+ this.exec(API.hide, id);
+ }
+
+ async clickNode(node: Cytoscape.NodeSingular): Promise<void> {
+ this.updateNodeSelection(node);
+ await this.explore(node);
+
+ const writes = node.data()?.writes;
+ if (writes && writes.length)
+ this.onSelect?.(writes);
+
+ /* Cytoscape automatically selects the node clicked, and unselects all other
+ nodes and edges. As we want some incoming edges to remain selected, we
+ make the node unselectable, preventing cytoscape to select it. */
+ node.unselectify();
+ }
+
+ async clickEdge(edge: Cytoscape.EdgeSingular): Promise<void> {
+ // Unselect everything
+ this.cy.$(':selected').forEach(unselect);
+ this.cy.$('.multiple-selection').removeClass('multiple-selection');
+ this.cy.$('.selection').removeClass('selection');
+
+ // Update Ivette selection
+ const origins = edge.data()?.origins;
+ if (origins && origins.length)
+ this.onSelect?.(origins);
+ }
+
+ doubleClickNode(node: Cytoscape.NodeSingular): void {
+ this.cy.animate({ fit: { eles: node, padding: 10 } });
+ }
+
+ selectLocation(
+ location: States.Location | undefined,
+ doExplore: boolean): void {
+ if (!location) {
+ // Reset whole graph if no location is selected.
+ this.clear();
+ } else if (location !== this.selectedLocation) {
+ this.selectedLocation = location;
+ const selectNode = this.cy.$('node:selected');
+ const writes = selectNode?.data()?.writes;
+ if (doExplore && location.marker && !_.some(writes, location)) {
+ this.add(location.marker);
+ }
+ else {
+ this.updateNodeSelection(selectNode);
+ }
+ }
+ }
+
+ updateNodeSelection(node: Cytoscape.NodeSingular): void {
+ const hasOrigin = (ele: Cytoscape.NodeSingular): boolean => (
+ _.some(ele.data().origins, this.selectedLocation)
+ );
+ this.cy.$(':selected').forEach(unselect);
+ this.cy.$('.multiple-selection').removeClass('multiple-selection');
+ this.cy.$('.selection').removeClass('selection');
+ select(node);
+ const edges = node.incomers('edge');
+ const relevantEdges = edges.filter(hasOrigin);
+ edges.addClass('multiple-selection');
+ relevantEdges.addClass('selection');
+ }
+}
+
+
+type GraphViewProps = {
+ addSelection: boolean;
+ grabbable: boolean;
+ layout: string;
+ selectionMode: string;
+}
+
+type GraphViewRef = {
+ clear: () => void;
+}
+
+const GraphView = React.forwardRef<GraphViewRef | undefined, GraphViewProps>(
+ (props: GraphViewProps, ref) => {
+ const { addSelection, grabbable, layout, selectionMode } = props;
+
+ const [dive, setDive] = useState(() => new Dive());
+ const [selection, updateSelection] = States.useSelection();
+ const graph = States.useSyncArrayData(API.graph);
+
+ function setCy(cy: Cytoscape.Core): void {
+ if (cy !== dive.cy)
+ setDive(new Dive(cy));
+ }
+
+ useImperativeHandle(ref, () => ({ clear: () => dive.clear() }));
+
+ useEffect(() => {
+ setDive(new Dive(dive.cy)); // On hot reload, setup a new instance
+ }, [Dive]); // eslint-disable-line react-hooks/exhaustive-deps
+
+ useEffect(() => {
+ dive.layout = layout;
+ }, [dive, layout]);
+
+ useEffect(() => {
+ dive.updateGraph(graph);
+ }, [dive, graph]);
+
+ // Follow mode
+ useEffect(() => {
+ dive.mode = selectionMode === 'follow' ? 'explore' : 'overview';
+ }, [dive, selectionMode]);
+
+ useEffect(() => {
+ /* When clicking on a node, select its writes locations as a multiple
+ selection. If these locations were already selected, select the next
+ location in the multiple selection. */
+ dive.onSelect = (locations) => {
+ if (_.isEqual(locations, selection?.multiple?.allSelections))
+ updateSelection('MULTIPLE_CYCLE');
+ else {
+ const name = "Dive graph";
+ updateSelection({ name, locations, index: 0 });
+ }
+ };
+
+ // Updates the graph according to the selected marker.
+ dive.selectLocation(selection?.current, addSelection);
+ }, [dive, addSelection, selection, updateSelection]);
+
+ return (
+ <CytoscapeComponent
+ stylesheet={style}
+ cy={setCy}
+ autoungrabify={!grabbable}
+ style={{ width: '100%', height: '100%' }}
+ />);
+});
+
+GraphView.displayName = "GraphView";
+
+
+export default function GraphComponent(): JSX.Element {
+ const graph = useRef<GraphViewRef>();
+ const [addSelection, flipAddSelection] =
+ Dome.useFlipSettings('dive.addSelection', true);
+ const [grabbable, flipGrabbable] =
+ Dome.useFlipSettings('dive.grabbable', true);
+ const [selectionMode, setSelectionMode] =
+ Dome.useStringSettings('dive.selectionMode', 'follow');
+ const [layout, setLayout] =
+ Dome.useStringSettings('dive.layout', 'dagre');
+ const [showLegend, flipShowLegend] =
+ Dome.useFlipSettings('dive.legend', true);
+
+ // Selection mode
+ const selectMode = (id?: string) => void (id && setSelectionMode(id));
+ const modes = [
+ { id: 'follow', label: 'Follow selection' },
+ { id: 'add', label: 'Add selection to the graph' },
+ ];
+ const checkMode =
+ (item: { id: string; label: string }): Dome.PopupMenuItem => (
+ { checked: item.id === selectionMode, ...item }
+ );
+ const modeMenu = (): void => {
+ Dome.popupMenu(modes.map(checkMode), selectMode);
+ };
+
+ // Layout selection
+ const selectLayout = (layout?: string) => void (layout && setLayout(layout));
+ const layoutsNames = ['cose-bilkent', 'dagre', 'cola', 'klay'];
+ const layoutItem = (id: string): Dome.PopupMenuItem =>
+ ({ id, label: id, checked: (id === layout) });
+ const layoutMenu = () =>
+ void Dome.popupMenu(layoutsNames.map(layoutItem), selectLayout);
+
+ // Component
+ return (
+ <>
+ <Ivette.TitleBar>
+ <IconButton
+ icon="PIN"
+ onClick={flipAddSelection}
+ kind={addSelection ? 'positive' : 'negative'}
+ title={addSelection ?
+ 'Do not add selected AST elements into the graph' :
+ 'Add selected AST elements into the graph'}
+ />
+ <IconButton
+ icon="LOCK"
+ onClick={flipGrabbable}
+ kind={grabbable ? 'positive' : 'negative'}
+ title={grabbable ?
+ 'Disallow nodes to be moved' :
+ 'Allow nodes to be moved'}
+ />
+ <IconButton
+ icon="SETTINGS"
+ onClick={modeMenu}
+ title="Choose the selection mode"
+ />
+ <IconButton
+ icon="DISPLAY"
+ onClick={layoutMenu}
+ title="Choose the graph layout"
+ />
+ <Space />
+ <IconButton
+ icon="HELP"
+ onClick={flipShowLegend}
+ kind={showLegend ? 'positive' : 'default'}
+ title={showLegend ?
+ 'Hide legend' :
+ 'Show legend'}
+ />
+ <Space />
+ <IconButton
+ icon="TRASH"
+ onClick={() => graph.current?.clear()}
+ title="Clear the graph"
+ />
+ </Ivette.TitleBar>
+ <EvaReady>
+ <GraphView
+ addSelection={addSelection}
+ grabbable={grabbable}
+ layout={layout}
+ selectionMode={selectionMode}
+ ref={graph}/>
+ { showLegend ? <Legend /> : null }
+ </EvaReady>
+ </>
+ );
+}
diff --git a/ivette/src/frama-c/plugins/dive/index.tsx b/ivette/src/frama-c/plugins/dive/index.tsx
index 77dd2a9f9aa1316c467648d7493450d287645c96..26df8fda493b559391bcbf21b8a98cf6fec5fb6d 100644
--- a/ivette/src/frama-c/plugins/dive/index.tsx
+++ b/ivette/src/frama-c/plugins/dive/index.tsx
@@ -20,715 +20,38 @@
/* */
/* ************************************************************************ */
-import React, { useState, useEffect, useImperativeHandle, useRef } from 'react';
-import _ from 'lodash';
-import { renderToString } from 'react-dom/server';
-import * as Dome from 'dome';
+import React from 'react';
import * as Ivette from 'ivette';
-import * as Server from 'frama-c/server';
-import * as States from 'frama-c/states';
-import * as API from './api';
+import GraphComponent from './graph';
+import TreeComponent from './tree';
-import Cytoscape from 'cytoscape';
-import CytoscapeComponent from 'react-cytoscapejs';
-import './cytoscape_libs';
-import 'cytoscape-panzoom/cytoscape.js-panzoom.css';
-
-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';
-
-import { IconButton } from 'dome/controls/buttons';
-import { Space } from 'dome/frame/toolbars';
-
-import '@fortawesome/fontawesome-free/js/all';
-
-import EvaReady from 'frama-c/plugins/eva/EvaReady';
-import style from './style.json';
-import layouts from './layouts.json';
-
-const Debug = new Dome.Debug('dive');
-
-interface Cxtcommand {
- content: string;
- select: () => void;
- enabled: boolean;
-}
-
-interface CytoscapeExtended extends Cytoscape.Core {
- cxtmenu(options: unknown): void;
- panzoom(options: unknown): void;
-}
-
-type Identified = { id: string }
-type NodeData = Cytoscape.NodeDataDefinition & Identified
-type EdgeData = { id: string;[key: string]: unknown }
-type NodeOrId = string | Cytoscape.NodeSingular
-
-function callstackToString(callstack: API.callstack): string {
- return callstack.map((cs) => `${cs.fun}:${cs.instr}`).join('/');
-}
-
-function buildCxtMenu(
- commands: Cxtcommand[],
- content?: JSX.Element,
- action?: () => void,
-): void {
- commands.push({
- content: content ? renderToString(content) : '',
- select: action || (() => { /* Do nothing */ }),
- enabled: !!action,
- });
-}
-
-/* double click events for Cytoscape */
-
-function enableDoubleClickEvents(cy: Cytoscape.Core, delay = 350): void {
- let last: Cytoscape.EventObject | undefined;
- cy.on('click', (e) => {
- if (last && last.target === e.target &&
- e.timeStamp - last.timeStamp < delay) {
- e.target.trigger('double-click', e);
- }
- last = e;
+Ivette.registerComponent({
+ id: 'frama-c.plugins.dive.graph',
+ label: 'Dive Dataflow Graph',
+ group: 'frama-c.plugins',
+ rank: 2,
+ title:
+ 'Data dependency graph according to an Eva analysis.',
+ children: <GraphComponent />,
});
-}
-
-/* The Dive class handles the selection of nodes according to user actions.
- To prevent cytoscape to automatically select (and unselect) nodes wrongly,
- we make some nodes unselectable. We then use the functions below to make
- the nodes selectable before (un)selecting them. */
-
-function select(node: Cytoscape.NodeSingular): void {
- node.selectify();
- node.select();
-}
-
-function unselect(node: Cytoscape.NodeSingular): void {
- node.selectify();
- node.unselect();
-}
-
-export type mode = 'explore' | 'overview';
-
-class Dive {
- headless: boolean;
- cy: Cytoscape.Core;
- mode: mode = 'explore';
- _layout = '';
- layoutOptions: Cytoscape.LayoutOptions | undefined;
- currentSelection: string | null = null;
- onSelect: ((_: States.Location[]) => void) | null = null;
- selectedLocation: (States.Location | undefined) = undefined;
-
- constructor(cy: Cytoscape.Core | null = null) {
- this.cy = cy || Cytoscape();
- this.headless = this.cy.container() === null;
- this.cy.elements().remove();
-
- this.cy.minZoom(1e-1);
- this.cy.maxZoom(1.0);
-
- // Remove previous listeners
- this.cy.off('click');
- this.cy.off('double-click');
-
- // Add new listeners
- enableDoubleClickEvents(this.cy);
- this.cy.on('click', 'node', (event) => this.clickNode(event.target));
- this.cy.on('double-click', '$node > node', // compound nodes
- (event) => this.doubleClickNode(event.target));
-
- // Set zoom limits
- const panzoomDefaults = {
- minZoom: this.cy.minZoom(),
- maxZoom: this.cy.maxZoom(),
- };
- (this.cy as CytoscapeExtended).panzoom(panzoomDefaults);
-
- // Default layout
- this.layout = 'dagre';
-
- // Contextual menu
- if (!this.headless) {
- this.cy.scratch('cxtmenu')?.destroy?.(); // Remove previous menu
- this.cy.scratch('cxtmenu', (this.cy as CytoscapeExtended).cxtmenu({
- selector: 'node',
- commands: (node: Cytoscape.NodeSingular) => this.onCxtMenu(node),
- }));
- }
-
- // Node width hack
- const padding = 10;
- const min = 50;
- /* eslint-disable @typescript-eslint/no-explicit-any */
- if (this.cy.style() && !this.headless) {
- const canvas = document.querySelector('canvas[data-id="layer2-node"]');
- if (canvas instanceof HTMLCanvasElement) {
- const context = canvas.getContext('2d');
- if (context) {
- (this.cy.style() as any).selector('node').style('width',
- (node: any) => {
- const fStyle = node.pstyle('font-style').strValue;
- const weight = node.pstyle('font-weight').strValue;
- const size = node.pstyle('font-size').pfValue;
- const family = node.pstyle('font-family').strValue;
- context.font = `${fStyle} ${weight} ${size}px ${family}`;
- const width = context.measureText(node.data('label')).width;
- return `${Math.max(min, width + padding)}px`;
- });
- }
- }
- }
- /* eslint-enable @typescript-eslint/no-explicit-any */
- }
-
- onCxtMenu(node: Cytoscape.NodeSingular): Cxtcommand[] {
- const data = node.data();
- const commands = [] as Cxtcommand[];
- buildCxtMenu(commands,
- <><div className="fas fa-binoculars fa-2x" />Explore</>,
- () => { this.explore(node); });
- if (data.nkind === 'composite')
- buildCxtMenu(commands,
- <><div className="fa fa-expand-arrows-alt fa-2x" />Unfold</>);
- else
- buildCxtMenu(commands);
- if (data.backward_explored === 'no')
- buildCxtMenu(commands,
- <div><div className="fa fa-eye fa-2x" />Show</div>,
- () => this.show(node));
- else
- buildCxtMenu(commands,
- <><div className="fa fa-eye-slash fa-2x" />Hide</>,
- () => this.hide(node));
- return commands;
- }
-
- remove(node: Cytoscape.NodeSingular): void {
- const parent = node.parent();
- node.remove();
- this.cy.$id(`${node.id()}-more`).remove();
- if (parent.nonempty() && parent.children().empty())
- this.remove(parent as Cytoscape.NodeSingular); // Recursively remove parents
- }
-
- referenceFile(fileName: string): Cytoscape.NodeSingular {
- const id = `file_${fileName}`;
- const node = this.cy.$id(id);
- if (node.nonempty()) {
- return node;
- }
-
- return this.cy.add({ data: { id, label: fileName }, classes: 'file' });
- }
-
- referenceCallstack(callstack: API.callstack): Cytoscape.NodeSingular | null {
- const name = callstackToString(callstack);
- const elt = callstack.shift();
-
- if (!elt)
- return null;
-
- const id = `callstack_${name}`;
- const node = this.cy.$id(id);
- if (node.nonempty()) {
- return node;
- }
-
- const parentNode = this.referenceCallstack(callstack);
- const parent = parentNode?.id();
- const label = elt.fun;
- return this.cy.add({ data: { id, label, parent }, classes: 'function' });
- }
-
- createTips(node: Cytoscape.NodeSingular): Tippy.Instance[] {
- const container = this.cy.container();
- if (!container)
- return [];
-
- // eslint-disable-next-line @typescript-eslint/no-explicit-any
- const ref = (node as any).popperRef();
- const common = {
- getReferenceClientRect: ref.getBoundingClientRect,
- interactive: true,
- animation: 'shift-away',
- duration: 500,
- trigger: 'manual',
- appendTo: document.body,
- };
-
- const tips = [];
-
- if (node.data().values) {
- tips.push(tippy(container, {
- ...common,
- content: node.data().values,
- placement: 'top',
- offset: [0, 20],
- arrow: true,
- }));
- }
-
- if (node.data().type) {
- tips.push(tippy(container, {
- ...common,
- content: node.data().type,
- placement: 'bottom',
- offset: [0, 20],
- theme: 'light-border',
- arrow: false,
- }));
- }
-
- return tips;
- }
-
- addTips(node: Cytoscape.NodeSingular): void {
- let timeout: NodeJS.Timeout;
- let tips: Tippy.Instance[] | null = null;
-
- node.on('mouseover', () => {
- if (tips === null) {
- tips = this.createTips(node);
- tips.forEach((tip) => tip.props.onHidden = (() => tip.destroy()));
- }
- clearTimeout(timeout);
- timeout = setTimeout(() => tips?.forEach((tip) => {
- tip.show();
- }), 200);
- });
-
- node.on('mouseout', () => {
- clearTimeout(timeout);
- timeout = setTimeout(() => {
- tips?.forEach((tip) => tip.hide());
- tips = null; // Force rebuilding tips in case they changed
- }, 0);
- });
- }
-
- updateElement(group: Cytoscape.ElementGroup, data: NodeData | EdgeData):
- Cytoscape.CollectionReturnValue {
- let element = this.cy.$id(data.id);
- if (element.nonempty()) {
- element.removeData();
- element.data(data);
- }
- else {
- element = this.cy.add({ group, data });
- element.addClass("new");
- }
- element.removeClass("stale");
- return element;
- }
-
- updateNode(data: NodeData):
- Cytoscape.NodeSingular {
- const element = this.updateElement("nodes", data);
- element.addClass('node');
- return element;
- }
-
- updateEdge(src: NodeOrId, dst: NodeOrId, data: EdgeData):
- Cytoscape.EdgeSingular {
- const source = typeof src === "string" ? src : src.id();
- const target = typeof dst === "string" ? dst : dst.id();
- data = { ...data, source, target };
- const element = this.updateElement("edges", data);
- element.addClass('dependency');
- return element;
- }
-
- updateNodeData(node: API.node): void {
- const data = { ...node, id: `${node.id}` } as NodeData;
-
- // Interval range visualization (see cytoscape stops style property)
- if (typeof node.range === 'number')
- data.stops = `0% ${node.range}% ${node.range}% 100%`;
-
- // Build clusters for this node if needed
- if (node.locality.callstack)
- data.parent = this.referenceCallstack(node.locality.callstack)?.id();
- else
- data.parent = this.referenceFile(node.locality.file).id();
-
- // Add new node or update existing node
- const ele = this.updateNode(data);
- if (ele.hasClass("new"))
- this.addTips(ele);
-
- // Add a node for the user to ask for more dependencies
- const idmore = `${node.id}-more`;
- if (node.backward_explored === 'partial') {
- const elemore = this.updateNode({ id: idmore, parent: data.parent });
- elemore.addClass("more");
- this.updateEdge(elemore, ele, { id: `e${node.id}-more` });
- }
- else {
- this.cy.$id(idmore).remove();
- }
- }
-
- updateEdgeData(edge: API.dependency): void {
- const data = { ...edge, id: `e${edge.id}` } as EdgeData;
- this.updateEdge(`${edge.src}`, `${edge.dst}`, data);
- }
-
- updateGraph(data: API.graphData[]): void {
- this.cy.startBatch();
- this.cy.$('.node, .dependency').addClass('stale');
-
- // Update vertices
- for (const d of data) {
- if ('nkind' in d.element) // Node
- this.updateNodeData(d.element);
- }
-
- // Edges must be updated after vertices since their sources and destination
- // must have been created beforhand
- for (const d of data) {
- if ('dkind' in d.element) // Dependency
- this.updateEdgeData(d.element);
- }
-
- // Remove nodes that are not present anymore
- this.cy.$('.stale').forEach(n => this.remove(n));
-
- this.cy.endBatch();
-
- this.recomputeLayout(this.cy.$('node.new'));
- }
-
- get layout(): string {
- return this._layout;
- }
-
- set layout(layout: string) {
- if (layout === this._layout)
- return;
- let extendedOptions = {};
- if (layout in layouts)
- extendedOptions = (layouts as { [key: string]: object })[layout];
- this._layout = layout;
- this.layoutOptions = {
- name: layout,
- fit: true,
- animate: true,
- randomize: false, /* Keep previous positions if layout supports it */
- ...extendedOptions,
- };
-
- this.recomputeLayout();
- }
-
- recomputeLayout(newNodes?: Cytoscape.Collection): void {
- if (this.layoutOptions && this.cy.container() &&
- (newNodes === undefined || !newNodes.empty())) {
- this.cy.layout({
- animationEasing: 'ease-in-out-quad',
- /* Do not move new nodes */
- animateFilter: (node: Cytoscape.Singular) => newNodes === undefined ||
- !newNodes.contains(node),
- stop: () => {
- this.cy.$('.new').addClass('old').removeClass('new');
- },
- ...this.layoutOptions,
- } as unknown as Cytoscape.LayoutOptions).run();
- }
- }
-
- async exec<In>(
- request: Server.ExecRequest<In, number | undefined | null>,
- param: In): Promise<Cytoscape.NodeSingular | undefined> {
- try {
- if (Server.isRunning()) {
- await this.setMode();
- const r = await Server.send(request, param);
- if (r) {
- return undefined;
- }
- }
- }
- catch (err) {
- Debug.error(err);
- }
-
- return undefined;
- }
-
- static async setWindow(window: API.explorationWindow): Promise<void> {
- if (Server.isRunning())
- await Server.send(API.window, window);
- }
-
- async setMode(): Promise<void> {
- switch (this.mode) {
- case 'explore':
- await Dive.setWindow({
- perception: { backward: 3, forward: 1 },
- horizon: { backward: 3, forward: 1 },
- });
- break;
- case 'overview':
- await Dive.setWindow({
- perception: { backward: 4, forward: 1 },
- horizon: { backward: undefined, forward: undefined },
- });
- break;
- default: /* This is useless and impossible if the program is correctly
- typed, but the linter wants it */
- }
- }
-
- clear(): void {
- this.cy.elements().remove();
- this.exec(API.clear, null);
- }
-
- async add(marker: string): Promise<void> {
- const node = await this.exec(API.add, marker);
- if (node)
- this.updateNodeSelection(node);
- }
-
- async explore(node: Cytoscape.NodeSingular): Promise<void> {
- const id = parseInt(node.id(), 10);
- if (id)
- await this.exec(API.explore, id);
- }
-
- show(node: Cytoscape.NodeSingular): void {
- const id = parseInt(node.id(), 10);
- if (id)
- this.exec(API.show, id);
- }
-
- hide(node: Cytoscape.NodeSingular): void {
- const id = parseInt(node.id(), 10);
- if (id)
- this.exec(API.hide, id);
- }
-
- async clickNode(node: Cytoscape.NodeSingular): Promise<void> {
- this.updateNodeSelection(node);
- await this.explore(node);
-
- const writes = node.data()?.writes;
- if (writes && writes.length)
- this.onSelect?.(writes);
-
- /* Cytoscape automatically selects the node clicked, and unselects all other
- nodes and edges. As we want some incoming edges to remain selected, we
- make the node unselectable, preventing cytoscape to select it. */
- node.unselectify();
- }
-
- doubleClickNode(node: Cytoscape.NodeSingular): void {
- this.cy.animate({ fit: { eles: node, padding: 10 } });
- }
-
- selectLocation(
- location: States.Location | undefined,
- doExplore: boolean): void {
- if (!location) {
- // Reset whole graph if no location is selected.
- this.clear();
- } else if (location !== this.selectedLocation) {
- this.selectedLocation = location;
- const selectNode = this.cy.$('node:selected');
- const writes = selectNode?.data()?.writes;
- if (doExplore && location.marker && !_.some(writes, location)) {
- this.add(location.marker);
- }
- else {
- this.updateNodeSelection(selectNode);
- }
- }
- }
-
- updateNodeSelection(node: Cytoscape.NodeSingular): void {
- const hasOrigin = (ele: Cytoscape.NodeSingular): boolean => (
- _.some(ele.data().origins, this.selectedLocation)
- );
- this.cy.$(':selected').forEach(unselect);
- this.cy.$('.multiple-selection').removeClass('multiple-selection');
- this.cy.$('.selection').removeClass('selection');
- select(node);
- const edges = node.incomers('edge');
- const relevantEdges = edges.filter(hasOrigin);
- edges.addClass('multiple-selection');
- relevantEdges.addClass('selection');
- }
-}
-
-
-type GraphViewProps = {
- lock: boolean;
- layout: string;
- selectionMode: string;
-}
-
-type GraphViewRef = {
- clear: () => void;
-}
-
-const GraphView = React.forwardRef<GraphViewRef | undefined, GraphViewProps>(
- (props: GraphViewProps, ref) => {
- const { lock, layout, selectionMode } = props;
-
- const [dive, setDive] = useState(() => new Dive());
- const [selection, updateSelection] = States.useSelection();
- const graph = States.useSyncArrayData(API.graph);
-
- function setCy(cy: Cytoscape.Core): void {
- if (cy !== dive.cy)
- setDive(new Dive(cy));
- }
-
- useImperativeHandle(ref, () => ({ clear: () => dive.clear() }));
-
- useEffect(() => {
- setDive(new Dive(dive.cy)); // On hot reload, setup a new instance
- }, [Dive]); // eslint-disable-line react-hooks/exhaustive-deps
-
- useEffect(() => {
- dive.layout = layout;
- }, [dive, layout]);
-
- useEffect(() => {
- dive.updateGraph(graph);
- }, [dive, graph]);
-
- // Follow mode
- useEffect(() => {
- dive.mode = selectionMode === 'follow' ? 'explore' : 'overview';
- }, [dive, selectionMode]);
-
- useEffect(() => {
- /* When clicking on a node, select its writes locations as a multiple
- selection. If these locations were already selected, select the next
- location in the multiple selection. */
- dive.onSelect = (locations) => {
- if (_.isEqual(locations, selection?.multiple?.allSelections))
- updateSelection('MULTIPLE_CYCLE');
- else
- updateSelection({ locations, index: 0 });
- };
-
- // Updates the graph according to the selected marker.
- dive.selectLocation(selection?.current, !lock);
- }, [dive, lock, selection, updateSelection]);
-
- return (
- <CytoscapeComponent
- stylesheet={style}
- cy={setCy}
- style={{ width: '100%', height: '100%' }}
- />);
-});
-
-GraphView.displayName = "GraphView";
-
-
-function DiveView(): JSX.Element {
- const graph = useRef<GraphViewRef>();
- const [lock, flipLock] =
- Dome.useFlipSettings('dive.lock');
- const [selectionMode, setSelectionMode] =
- Dome.useStringSettings('dive.selectionMode', 'follow');
- const [layout, setLayout] =
- Dome.useStringSettings('dive.layout', 'dagre');
-
- // Selection mode
- const selectMode = (id?: string) => void (id && setSelectionMode(id));
- const modes = [
- { id: 'follow', label: 'Follow selection' },
- { id: 'add', label: 'Add selection to the graph' },
- ];
- const checkMode =
- (item: { id: string; label: string }): Dome.PopupMenuItem => (
- { checked: item.id === selectionMode, ...item }
- );
- const modeMenu = (): void => {
- Dome.popupMenu(modes.map(checkMode), selectMode);
- };
-
- // Layout selection
- const selectLayout = (layout?: string) => void (layout && setLayout(layout));
- const layoutsNames = ['cose-bilkent', 'dagre', 'cola', 'klay'];
- const layoutItem = (id: string): Dome.PopupMenuItem =>
- ({ id, label: id, checked: (id === layout) });
- const layoutMenu = () =>
- void Dome.popupMenu(layoutsNames.map(layoutItem), selectLayout);
-
- // Component
- return (
- <>
- <Ivette.TitleBar>
- <IconButton
- icon="LOCK"
- onClick={flipLock}
- kind={lock ? 'negative' : 'positive'}
- title={lock ?
- 'Unlock the graph: update the graph with the selection' :
- 'Lock the graph: do not update the graph with the selection'}
- />
- <IconButton
- icon="SETTINGS"
- onClick={modeMenu}
- title="Choose the selection mode"
- />
- <IconButton
- icon="DISPLAY"
- onClick={layoutMenu}
- title="Choose the graph layout"
- />
- <Space />
- <IconButton
- icon="TRASH"
- onClick={() => graph.current?.clear()}
- title="Clear the graph"
- />
- </Ivette.TitleBar>
- <EvaReady>
- <GraphView
- lock={lock}
- layout={layout}
- selectionMode={selectionMode}
- ref={graph}/>
- </EvaReady>
- </>
- );
-
-}
-
-// --------------------------------------------------------------------------
-// --- Export Component
-// --------------------------------------------------------------------------
Ivette.registerComponent({
- id: 'frama-c.plugins.dive',
- label: 'Dive Dataflow',
- group: 'frama-c.plugins',
- rank: 2,
- title:
- 'Data dependency graph according to an Eva analysis.\nNodes color ' +
- 'represents the precision of the values inferred by Eva.',
- children: <DiveView />,
-});
+ id: 'frama-c.plugins.dive.tree',
+ label: 'Dive Dataflow Tree',
+ group: 'frama-c.plugins',
+ rank: 3,
+ title:
+ 'Data dependency tree according to an Eva analysis.',
+ children: <TreeComponent />,
+ });
Ivette.registerView({
- id: 'dive',
- label: 'Dive Dataflow',
- rank: 5,
- layout: [
- ['frama-c.astview', 'frama-c.plugins.dive'],
- ['frama-c.properties', 'frama-c.locations'],
- ],
-});
-
-// --------------------------------------------------------------------------
+ id: 'dive',
+ label: 'Dive Dataflow',
+ rank: 5,
+ layout: [
+ ['frama-c.astview', 'frama-c.plugins.dive.graph'],
+ ['frama-c.properties', 'frama-c.locations'],
+ ],
+ });
diff --git a/ivette/src/frama-c/plugins/dive/legend.tsx b/ivette/src/frama-c/plugins/dive/legend.tsx
new file mode 100644
index 0000000000000000000000000000000000000000..ff8918adeb7633a407c426d0dd4fc956850dee6e
--- /dev/null
+++ b/ivette/src/frama-c/plugins/dive/legend.tsx
@@ -0,0 +1,187 @@
+/* ************************************************************************ */
+/* */
+/* This file is part of Frama-C. */
+/* */
+/* Copyright (C) 2007-2023 */
+/* 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). */
+/* */
+/* ************************************************************************ */
+
+import React from 'react';
+import _ from 'lodash';
+
+import CytoscapeComponent from 'react-cytoscapejs';
+import stylesheet from './style.json';
+
+const elements = [
+ {
+ data: {
+ id: "shape",
+ label: "Node shape: memory"
+ },
+ classes: ["group"],
+ },
+ {
+ data: {
+ parent: "shape",
+ label: "constant",
+ nkind: 'const'
+ },
+ position: { x: 0, y: 0 }
+ },
+ {
+ data: {
+ parent: "shape",
+ label: "scalar type"
+ },
+ position: { x: 0, y: 40 }
+ },
+ {
+ data: {
+ parent: "shape",
+ label: "aggregate type",
+ nkind: 'composite'
+ },
+ position: { x: 0, y: 80 }
+ },
+ {
+ data: {
+ parent: "shape",
+ label: "set of addresses",
+ nkind: 'scattered'
+ },
+ position: { x: 0, y: 120 }
+ },
+ {
+ data: {
+ parent: "shape",
+ label: "analysis alarm",
+ nkind: 'alarm'
+ },
+ position: { x: 0, y: 160 }
+ },
+ {
+ data: {
+ id: "color",
+ label: "Node color: value cardinality"
+ },
+ classes: ["group"]
+ },
+ {
+ data: {
+ parent: "color",
+ label: "unique value",
+ range: 'singleton'
+ },
+ position: { x: 0, y: 230 }
+ },
+ {
+ data: {
+ parent: "color",
+ label: "small range of values",
+ stops: '0% 20% 20% 100%'
+ },
+ position: { x: 0, y: 270 }
+ },
+ {
+ data: {
+ parent: "color",
+ label: "large range of values",
+ stops: '0% 80% 80% 100%'
+ },
+ position: { x: 0, y: 310 }
+ },
+ {
+ data: {
+ parent: "color",
+ label: "extreme range of values",
+ range: 'wide'
+ },
+ position: { x: 0, y: 350 }
+ },
+ {
+ data: {
+ id: "outline",
+ label: "Node outline color: taint analysis",
+ },
+ classes: ["group"]
+ },
+ {
+ data: {
+ parent: "outline",
+ label: "directly tainted",
+ taint: 'direct'
+ },
+ position: { x: 0, y: 420 }
+ },
+ {
+ data: {
+ parent: "outline",
+ label: "indirectly tainted",
+ taint: 'indirect'
+ },
+ position: { x: 0, y: 480 }
+ },
+];
+
+const layout = {
+ name: 'preset',
+ fit: true,
+ padding: 0,
+};
+
+const completeStylecheet = [
+ ...stylesheet,
+ {
+ "selector": "node",
+ "style": {
+ "width": '140',
+ "height": '20',
+ "font-size": "14px",
+ }
+ },
+ {
+ "selector": ".group",
+ "style": {
+ "shape": "rectangle",
+ "background-opacity": 0.0,
+ "text-valign": "top",
+ "text-halign": "center",
+ "padding": "4px",
+ "border-width": 0,
+ }
+ },
+ {
+ "selector": "#outline",
+ "style": { "padding": "10px", }
+ },
+];
+
+function Legend() : JSX.Element {
+ return (
+ <CytoscapeComponent
+ elements={elements}
+ layout={layout}
+ className="legend"
+ stylesheet={completeStylecheet}
+ userPanningEnabled={false} /* No panning */
+ userZoomingEnabled={false} /* No zoom */
+ autounselectify={true} /* No node selection */
+ autoungrabify={true} /* No node grab */
+ />);
+}
+
+export default Legend;
diff --git a/ivette/src/frama-c/plugins/dive/style.json b/ivette/src/frama-c/plugins/dive/style.json
index 79a9907c1e06fd4d0f2841f0d5a4e2fd8e17f16a..331ea3a2bc361ac636420453cacbe4fd6b8863e0 100644
--- a/ivette/src/frama-c/plugins/dive/style.json
+++ b/ivette/src/frama-c/plugins/dive/style.json
@@ -168,17 +168,15 @@
{
"selector": "node[nkind='composite']",
"style": {
- "ghost": "yes",
- "ghost-offset-x": "6px",
- "ghost-offset-y": "6px",
- "ghost-opacity": "0.7"
+ "border-style": "double",
+ "border-width": "5px"
}
},
{
"selector": "node[taint='direct']",
"style": {
"underlay-color": "#882288",
- "underlay-padding": "14px",
+ "underlay-padding": "12px",
"underlay-opacity": 0.4
}
},
@@ -186,7 +184,7 @@
"selector": "node[taint='indirect']",
"style": {
"underlay-color": "#73BBBB",
- "underlay-padding": "14px",
+ "underlay-padding": "12px",
"underlay-opacity": 0.8
}
},
diff --git a/ivette/src/frama-c/plugins/dive/tree.tsx b/ivette/src/frama-c/plugins/dive/tree.tsx
new file mode 100644
index 0000000000000000000000000000000000000000..78be7a54daa2d52fbac8e53b2f69abdfe046d1e9
--- /dev/null
+++ b/ivette/src/frama-c/plugins/dive/tree.tsx
@@ -0,0 +1,232 @@
+/* ************************************************************************ */
+/* */
+/* This file is part of Frama-C. */
+/* */
+/* Copyright (C) 2007-2023 */
+/* 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). */
+/* */
+/* ************************************************************************ */
+
+import React, { useEffect } from 'react';
+
+import { classes } from 'dome/misc/utils';
+import { IconButton } from 'dome/controls/buttons';
+import * as Ivette from 'ivette';
+
+import * as Server from 'frama-c/server';
+import * as States from 'frama-c/states';
+
+import EvaReady from 'frama-c/plugins/eva/EvaReady';
+import * as API from './api';
+import type { marker, location } from 'frama-c/kernel/api/ast';
+import gearsIcon from '../eva/images/gears.svg';
+
+import './dive.css';
+
+const window = {
+ perception: { backward: 3, forward: 0 },
+ horizon: { backward: undefined, forward: undefined },
+};
+
+async function exec<I, O>(rq: Server.ExecRequest<I, O>, i: I):
+ Promise<O | undefined> {
+ if (Server.isRunning()) {
+ await Server.send(API.window, window);
+ return await Server.send(rq, i);
+ }
+
+ return undefined;
+}
+
+async function requestLocation(location: States.Location):
+ Promise<number | undefined> {
+ return await exec(API.add, location.marker);
+}
+
+async function explore(node: API.node): Promise<null | undefined> {
+ return await exec(API.explore, node.id);
+}
+
+function isDependency(el: API.element): el is API.dependency {
+ return 'dst' in el;
+}
+
+function Folder(props: {unfolded: boolean, onclick?: () => void}): JSX.Element {
+ return <IconButton
+ icon={props.unfolded ? 'MINUS' : 'PLUS'}
+ title="Fold / Unfold the dependencies"
+ className="folder"
+ onClick={props.onclick}
+ />;
+}
+
+function Exploring(): JSX.Element {
+ return <><img src={gearsIcon} className="exploration" />Exploring...</>;
+}
+
+function Marker(props: {location: location}): JSX.Element {
+ const location = props.location;
+ const marker = location.marker;
+ const { descr } = States.useMarker(marker);
+ const [selection, updateSelection] = States.useSelection();
+ const [hovering, updateHovered] = States.useHovered();
+ const classeName = classes(
+ 'marker',
+ selection.current?.marker === marker && 'selected',
+ hovering?.marker === marker && 'hovered'
+ );
+
+ return <span
+ className={classeName}
+ onClick={() => updateSelection({ location: location })}
+ onMouseEnter={() => updateHovered(location)}
+ onMouseLeave={() => updateHovered(undefined)}>
+ {descr}
+ </span>;
+}
+
+
+type WithKey<P> = P & {key: string | number | null}
+
+type WithItemChildren<P> =
+ P & {
+ children?: WithKey<React.ReactElement> | WithKey<React.ReactElement>[]
+ }
+
+type TreeNodeProps = {
+ label: React.ReactNode,
+ className?: string,
+ unfolded?: boolean,
+ onunfold?: () => void,
+}
+
+function TreeNode(props: WithItemChildren<TreeNodeProps>): JSX.Element {
+ const [unfolded, setUnfolded] = React.useState(props.unfolded === true);
+ const children =
+ props.children ?
+ (Array.isArray(props.children) ? props.children : [props.children]) :
+ [];
+
+ const toggle = (): void => {
+ unfolded === false && props.onunfold && props.onunfold();
+ setUnfolded(!unfolded);
+ };
+
+ return <div className={props.className}>
+ <span className="label">
+ {children.length > 0 ?
+ <Folder unfolded={unfolded} onclick={toggle} /> : <></>
+ }
+ {props.label}
+ </span>
+ {unfolded ?
+ <ul>
+ {children.map((element) => <li key={element.key}>{element}</li>)}
+ </ul> :
+ null
+ }
+ </div>;
+}
+
+function MarkerNode(props: WithItemChildren<{location: location}>):
+ JSX.Element {
+ return <TreeNode
+ unfolded={true}
+ label={<Marker location={props.location} />}
+ className="marker">
+ {props.children}
+ </TreeNode>;
+}
+
+function GraphNode(props: {nodeId: number, unfolded?: boolean}): JSX.Element {
+ const graphData = States.useSyncArrayElt(API.graph, `n${props.nodeId}`);
+ const graph = States.useSyncArrayData(API.graph);
+
+ if (graphData && 'label' in graphData.element) {
+ const node = graphData.element;
+ const deps = graph
+ .map((data) => data.element)
+ .filter(isDependency)
+ .filter((d) => d.dst === node.id);
+
+ // Transform dependencies into a map 'statement' -> 'memory location read
+ // at this statement'
+ const map = new Map<marker, [location, Set<API.nodeId>]>();
+ deps.forEach((d) => {
+ d.origins.forEach((loc) => {
+ let entry = map.get(loc.marker);
+ if (entry === undefined) {
+ entry = [loc, new Set()];
+ map.set(loc.marker, entry);
+ }
+ entry[1].add(d.src);
+ });
+ });
+
+ return <TreeNode
+ unfolded={props.unfolded}
+ onunfold={() => explore(node)}
+ label={node.label}>
+ {node.backward_explored ?
+ Array.from(map.entries()).map(([m, [loc, sources]]) =>
+ <MarkerNode location={loc} key={m}>
+ {Array.from(sources.values()).map((src) =>
+ <GraphNode nodeId={src} key={src} />
+ ) }
+ </MarkerNode>
+ ) :
+ <Exploring key={null} />
+ }
+ </TreeNode>;
+ }
+
+ return <>Error while building the tree</>;
+}
+
+export default function TreeComponent(): JSX.Element {
+ const [root, setRoot] = React.useState<number | null>(null);
+ const [selection] = States.useSelection();
+
+ useEffect(() => {
+ const update = async (): Promise<void> => {
+ if (selection.current) {
+ const node = await requestLocation(selection.current);
+ root === null && node !== null && node !== undefined && setRoot(node);
+ }
+ };
+ update();
+ }, [selection, root]);
+
+ return <>
+ <Ivette.TitleBar>
+ <IconButton
+ icon="TRASH"
+ onClick={() => setRoot(null)}
+ title="Clear the graph"
+ />
+ </Ivette.TitleBar>
+ <EvaReady>
+ {
+ root === null ?
+ <>Select an expression to investigate</>
+ :
+ <div className="diveTree">
+ <GraphNode nodeId={root} unfolded={true} />
+ </div>
+ }
+ </EvaReady>
+ </>;
+}