From 3c5680cae9f18433152d072cf3dac3b7b34f617a Mon Sep 17 00:00:00 2001
From: Valentin Perrelle <valentin.perrelle@cea.fr>
Date: Fri, 31 Mar 2023 11:18:16 +0200
Subject: [PATCH] [Callgraph] Add an Ivette component to display service graphs
---
.../frama-c/plugins/callgraph/api/index.ts | 221 ++++++++++++++++++
.../frama-c/plugins/callgraph/callgraph.css | 6 +
.../plugins/callgraph/graph-style.json | 34 +++
.../src/frama-c/plugins/callgraph/index.tsx | 138 +++++++++++
ivette/src/frama-c/plugins/callgraph/pkg.json | 3 +
src/plugins/callgraph/callgraph_api.ml | 1 +
src/plugins/callgraph/requests.ml | 169 ++++++++++++++
src/plugins/callgraph/requests.mli | 23 ++
src/plugins/callgraph/services.ml | 4 +
9 files changed, 599 insertions(+)
create mode 100644 ivette/src/frama-c/plugins/callgraph/api/index.ts
create mode 100644 ivette/src/frama-c/plugins/callgraph/callgraph.css
create mode 100644 ivette/src/frama-c/plugins/callgraph/graph-style.json
create mode 100644 ivette/src/frama-c/plugins/callgraph/index.tsx
create mode 100644 ivette/src/frama-c/plugins/callgraph/pkg.json
create mode 100644 src/plugins/callgraph/requests.ml
create mode 100644 src/plugins/callgraph/requests.mli
diff --git a/ivette/src/frama-c/plugins/callgraph/api/index.ts b/ivette/src/frama-c/plugins/callgraph/api/index.ts
new file mode 100644
index 00000000000..af0fd6b1f54
--- /dev/null
+++ b/ivette/src/frama-c/plugins/callgraph/api/index.ts
@@ -0,0 +1,221 @@
+/* ************************************************************************ */
+/* */
+/* 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). */
+/* */
+/* ************************************************************************ */
+
+/* --- Generated Frama-C Server API --- */
+
+/**
+ Callgraph
+ @packageDocumentation
+ @module frama-c/plugins/callgraph/api
+*/
+
+//@ts-ignore
+import * as Json from 'dome/data/json';
+//@ts-ignore
+import * as Compare from 'dome/data/compare';
+//@ts-ignore
+import * as Server from 'frama-c/server';
+//@ts-ignore
+import * as State from 'frama-c/states';
+
+//@ts-ignore
+import { byFct } from 'frama-c/kernel/api/ast';
+//@ts-ignore
+import { fct } from 'frama-c/kernel/api/ast';
+//@ts-ignore
+import { fctDefault } from 'frama-c/kernel/api/ast';
+//@ts-ignore
+import { jFct } from 'frama-c/kernel/api/ast';
+//@ts-ignore
+import { byTag } from 'frama-c/kernel/api/data';
+//@ts-ignore
+import { jTag } from 'frama-c/kernel/api/data';
+//@ts-ignore
+import { tag } from 'frama-c/kernel/api/data';
+//@ts-ignore
+import { tagDefault } from 'frama-c/kernel/api/data';
+
+export interface vertex {
+ /** kf */
+ kf: fct;
+ /** is_root */
+ is_root: boolean;
+}
+
+/** Decoder for `vertex` */
+export const jVertex: Json.Decoder<vertex> =
+ Json.jObject({ kf: jFct, is_root: Json.jBoolean,});
+
+/** Natural order for `vertex` */
+export const byVertex: Compare.Order<vertex> =
+ Compare.byFields
+ <{ kf: fct, is_root: boolean }>({
+ kf: byFct,
+ is_root: Compare.boolean,
+ });
+
+/** Default value for `vertex` */
+export const vertexDefault: vertex = { kf: fctDefault, is_root: false };
+
+/** Whether The nature of a node */
+export enum edgeKind {
+ /** */
+ inter_services = 'inter_services',
+ /** */
+ inter_functions = 'inter_functions',
+ /** */
+ both = 'both',
+}
+
+/** Decoder for `edgeKind` */
+export const jEdgeKind: Json.Decoder<edgeKind> = Json.jEnum(edgeKind);
+
+/** Natural order for `edgeKind` */
+export const byEdgeKind: Compare.Order<edgeKind> = Compare.byEnum(edgeKind);
+
+/** Default value for `edgeKind` */
+export const edgeKindDefault: edgeKind = edgeKind.inter_services;
+
+const edgeKindTags_internal: Server.GetRequest<null,tag[]> = {
+ kind: Server.RqKind.GET,
+ name: 'plugins.callgraph.edgeKindTags',
+ input: Json.jNull,
+ output: Json.jArray(jTag),
+ signals: [],
+};
+/** Registered tags for the above type. */
+export const edgeKindTags: Server.GetRequest<null,tag[]>= edgeKindTags_internal;
+
+export interface edge {
+ /** src */
+ src: fct;
+ /** dst */
+ dst: fct;
+ /** kind */
+ kind: edgeKind;
+}
+
+/** Decoder for `edge` */
+export const jEdge: Json.Decoder<edge> =
+ Json.jObject({ src: jFct, dst: jFct, kind: jEdgeKind,});
+
+/** Natural order for `edge` */
+export const byEdge: Compare.Order<edge> =
+ Compare.byFields
+ <{ src: fct, dst: fct, kind: edgeKind }>({
+ src: byFct,
+ dst: byFct,
+ kind: byEdgeKind,
+ });
+
+/** Default value for `edge` */
+export const edgeDefault: edge =
+ { src: fctDefault, dst: fctDefault, kind: edgeKindDefault };
+
+/** The callgraph of the current project */
+export interface graph {
+ /** vertices */
+ vertices: vertex[];
+ /** edges */
+ edges: edge[];
+ /** entry_point */
+ entry_point?: fct;
+}
+
+/** Decoder for `graph` */
+export const jGraph: Json.Decoder<graph> =
+ Json.jObject({
+ vertices: Json.jArray(jVertex),
+ edges: Json.jArray(jEdge),
+ entry_point: Json.jOption(jFct),
+ });
+
+/** Natural order for `graph` */
+export const byGraph: Compare.Order<graph> =
+ Compare.byFields
+ <{ vertices: vertex[], edges: edge[], entry_point?: fct }>({
+ vertices: Compare.array(byVertex),
+ edges: Compare.array(byEdge),
+ entry_point: Compare.defined(byFct),
+ });
+
+/** Default value for `graph` */
+export const graphDefault: graph =
+ { vertices: [], edges: [], entry_point: undefined };
+
+/** Signal for state [`callgraph`](#callgraph) */
+export const signalCallgraph: Server.Signal = {
+ name: 'plugins.callgraph.signalCallgraph',
+};
+
+const getCallgraph_internal: Server.GetRequest<null,graph | undefined> = {
+ kind: Server.RqKind.GET,
+ name: 'plugins.callgraph.getCallgraph',
+ input: Json.jNull,
+ output: Json.jOption(jGraph),
+ signals: [],
+};
+/** Getter for state [`callgraph`](#callgraph) */
+export const getCallgraph: Server.GetRequest<null,graph | undefined>= getCallgraph_internal;
+
+const callgraph_internal: State.Value<graph | undefined> = {
+ name: 'plugins.callgraph.callgraph',
+ signal: signalCallgraph,
+ getter: getCallgraph,
+};
+/** The current callgraph or an empty graph if it has not been computed yet */
+export const callgraph: State.Value<graph | undefined> = callgraph_internal;
+
+/** Signal for state [`isComputed`](#iscomputed) */
+export const signalIsComputed: Server.Signal = {
+ name: 'plugins.callgraph.signalIsComputed',
+};
+
+const getIsComputed_internal: Server.GetRequest<null,boolean> = {
+ kind: Server.RqKind.GET,
+ name: 'plugins.callgraph.getIsComputed',
+ input: Json.jNull,
+ output: Json.jBoolean,
+ signals: [],
+};
+/** Getter for state [`isComputed`](#iscomputed) */
+export const getIsComputed: Server.GetRequest<null,boolean>= getIsComputed_internal;
+
+const isComputed_internal: State.Value<boolean> = {
+ name: 'plugins.callgraph.isComputed',
+ signal: signalIsComputed,
+ getter: getIsComputed,
+};
+/** This boolean is true if the graph has been computed */
+export const isComputed: State.Value<boolean> = isComputed_internal;
+
+const compute_internal: Server.ExecRequest<null,null> = {
+ kind: Server.RqKind.EXEC,
+ name: 'plugins.callgraph.compute',
+ input: Json.jNull,
+ output: Json.jNull,
+ signals: [],
+};
+/** Compute the callgraph for the current project */
+export const compute: Server.ExecRequest<null,null>= compute_internal;
+
+/* ------------------------------------- */
diff --git a/ivette/src/frama-c/plugins/callgraph/callgraph.css b/ivette/src/frama-c/plugins/callgraph/callgraph.css
new file mode 100644
index 00000000000..4360e1461c2
--- /dev/null
+++ b/ivette/src/frama-c/plugins/callgraph/callgraph.css
@@ -0,0 +1,6 @@
+.callgraph-computing {
+ max-width: 90%;
+ max-height: 200px;
+ fill: var(--info-text-discrete);
+ margin: auto;
+}
diff --git a/ivette/src/frama-c/plugins/callgraph/graph-style.json b/ivette/src/frama-c/plugins/callgraph/graph-style.json
new file mode 100644
index 00000000000..6a10b6d0882
--- /dev/null
+++ b/ivette/src/frama-c/plugins/callgraph/graph-style.json
@@ -0,0 +1,34 @@
+[
+ {
+ "selector": "node",
+ "style": {
+ "shape": "round-rectangle",
+ "background-color": "#666",
+ "label": "data(id)",
+ "color": "white",
+ "text-outline-width": 2,
+ "text-outline-color": "#666",
+ "text-valign" : "center",
+ "padding" : "6px",
+ "border-width": 1,
+ "text-wrap" : "wrap"
+ }
+ },
+ {
+ "selector": "node[?is_root]",
+ "style": {
+ "border-width": "2px"
+ }
+ },
+ {
+ "selector": "edge",
+ "style": {
+ "width": 2,
+ "line-color": "#888",
+ "curve-style": "bezier",
+ "target-arrow-shape": "vee",
+ "target-arrow-color": "#888",
+ "arrow-scale": 2.0
+ }
+ }
+]
diff --git a/ivette/src/frama-c/plugins/callgraph/index.tsx b/ivette/src/frama-c/plugins/callgraph/index.tsx
new file mode 100644
index 00000000000..e5c8ccfc9d9
--- /dev/null
+++ b/ivette/src/frama-c/plugins/callgraph/index.tsx
@@ -0,0 +1,138 @@
+/* ************************************************************************ */
+/* */
+/* 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 } from 'react';
+import _ from 'lodash';
+import * as Ivette from 'ivette';
+import * as Server from 'frama-c/server';
+
+import * as API from './api';
+
+import Cytoscape from 'cytoscape';
+import CytoscapeComponent from 'react-cytoscapejs';
+import 'frama-c/plugins/dive/cytoscape_libs';
+import 'cytoscape-panzoom/cytoscape.js-panzoom.css';
+
+import style from './graph-style.json';
+import { useSyncValue } from 'frama-c/states';
+
+import gearsIcon from 'frama-c/plugins/eva/images/gears.svg';
+import './callgraph.css';
+
+
+// --------------------------------------------------------------------------
+// --- Nodes label measurement
+// --------------------------------------------------------------------------
+
+/* eslint-disable @typescript-eslint/no-explicit-any */
+function getWidth(node: any): string {
+ const padding = 10;
+ const min = 50;
+ const canvas = document.querySelector('canvas[data-id="layer2-node"]');
+ if (canvas instanceof HTMLCanvasElement) {
+ const context = canvas.getContext('2d');
+ if (context) {
+ 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('id')).width;
+ return `${Math.max(min, width + padding)}px`;
+ }
+ }
+ return `${min}px`;
+}
+
+(style as unknown[]).push({
+ selector: 'node',
+ style: {width: getWidth}
+ });
+
+
+// --------------------------------------------------------------------------
+// --- Graph
+// --------------------------------------------------------------------------
+
+function convertGraph(graph: API.graph): object[] {
+ const elements = [];
+ for (const v of graph.vertices) {
+ elements.push({data: {...v, id:v.kf}});
+ }
+ for (const e of graph.edges) {
+ elements.push({data: {source: e.src, target: e.dst}});
+ }
+ console.log(elements);
+ return elements;
+}
+
+
+function Callgraph() : JSX.Element {
+ const isComputed = useSyncValue(API.isComputed);
+ const graph = useSyncValue(API.callgraph);
+ const [cy, setCy] = useState<Cytoscape.Core>();
+ const layout = {name: 'cola', nodeSpacing: 32};
+
+ if (isComputed === false) {
+ Server.send(API.compute, null);
+ return (<img src={gearsIcon} className="callgraph-computing" />);
+ }
+ else if (graph !== undefined) {
+ return (
+ <CytoscapeComponent
+ elements={convertGraph(graph)}
+ stylesheet={style}
+ cy={setCy}
+ layout={layout}
+ style={{width: '100%', height: '100%'}}
+ />);
+ }
+ else {
+ return (<></>);
+ }
+}
+
+
+// --------------------------------------------------------------------------
+// --- Ivette Component
+// --------------------------------------------------------------------------
+
+function CallgraphComponent(): JSX.Element {
+ // Component
+ return (
+ <>
+ <Ivette.TitleBar />
+ <Callgraph />
+ </>
+ );
+}
+
+
+Ivette.registerComponent({
+ id: 'frama-c.plugins.callgraph',
+ label: 'Call Graph',
+ group: 'frama-c.plugins',
+ rank: 3,
+ title:
+ 'Display a graph showing calls between functions.',
+ children: <CallgraphComponent />,
+});
diff --git a/ivette/src/frama-c/plugins/callgraph/pkg.json b/ivette/src/frama-c/plugins/callgraph/pkg.json
new file mode 100644
index 00000000000..01be594c9ee
--- /dev/null
+++ b/ivette/src/frama-c/plugins/callgraph/pkg.json
@@ -0,0 +1,3 @@
+{
+ "name": "Frama-C/Callgraph"
+}
diff --git a/src/plugins/callgraph/callgraph_api.ml b/src/plugins/callgraph/callgraph_api.ml
index 712ccd11aed..a2d67c27747 100644
--- a/src/plugins/callgraph/callgraph_api.ml
+++ b/src/plugins/callgraph/callgraph_api.ml
@@ -61,6 +61,7 @@ module type Services = sig
val entry_point: unit -> G.V.t option
val is_root: Kernel_function.t -> bool
+ val add_hook: (G.t -> unit) -> unit
end
(*
diff --git a/src/plugins/callgraph/requests.ml b/src/plugins/callgraph/requests.ml
new file mode 100644
index 00000000000..42db7a20ad8
--- /dev/null
+++ b/src/plugins/callgraph/requests.ml
@@ -0,0 +1,169 @@
+(**************************************************************************)
+(* *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+open Server
+
+let package = Package.package ~plugin:"callgraph" ~title:"Callgraph" ()
+
+module Record () =
+struct
+ module Record = Data.Record
+ type record
+ let record : record Record.signature = Record.signature ()
+ let field name ?(descr = name) =
+ Record.field record ~name ~descr:(Markdown.plain descr)
+ let option name ?(descr = name) =
+ Record.option record ~name ~descr:(Markdown.plain descr)
+ let publish ?descr name =
+ let descr = Option.map Markdown.plain descr in
+ Record.publish record ~package ~name ?descr
+end
+
+
+module Enum (X: sig type t end) =
+struct
+ module Enum = Data.Enum
+ let dictionary: X.t Enum.dictionary = Enum.dictionary ()
+ let tag name descr = Enum.tag ~name ~descr:(Markdown.plain descr) dictionary
+ let publish lookup name descr =
+ Enum.set_lookup dictionary lookup;
+ Request.dictionary ~package ~name ~descr:(Markdown.plain descr) dictionary
+end
+
+module Vertex =
+struct
+ include Record ()
+
+ let kf = field "kf" (module Kernel_ast.Function)
+ let is_root = field "is_root" Data.jbool
+
+ include (val publish "vertex")
+ type t = Cil_types.kernel_function Service_graph.vertex
+
+ let to_json (v : Cil_types.kernel_function Service_graph.vertex) =
+ default |>
+ set kf v.node |>
+ set is_root v.is_root |>
+ to_json
+
+ let of_json _js = Data.failure "Vertex.of_json not implemented"
+end
+
+module EdgeKind =
+struct
+ include Enum (struct type t = Service_graph.edge end)
+
+ let inter_services = tag "inter_services" ""
+ let inter_functions = tag "inter_functions" ""
+ let both = tag "both" ""
+
+ let lookup = function
+ | Service_graph.Inter_services -> inter_services
+ | Inter_functions -> inter_functions
+ | Both -> both
+
+ include (val publish lookup "edgeKind" "Whether The nature of a node")
+end
+
+module Edge =
+struct
+ include Record ()
+
+ let src = field "src" (module Kernel_ast.Function)
+ let dst = field "dst" (module Kernel_ast.Function)
+ let kind = field "kind" (module EdgeKind)
+
+ include (val publish "edge")
+ type t = Services.G.E.t
+
+ let to_json (e : t) =
+ default |>
+ set src (Services.G.E.src e).node |>
+ set dst (Services.G.E.dst e).node |>
+ set kind (Services.G.E.label e) |>
+ to_json
+
+ let of_json _js = Data.failure "Edge.of_json not implemented"
+end
+
+module Graph =
+struct
+ include Record ()
+
+ let vertices = field "vertices" (module Data.Jlist (Vertex))
+ let edges = field "edges" (module Data.Jlist (Edge))
+ let entry_point = option "entry_point" (module Kernel_ast.Function)
+
+ include (val publish "graph" ~descr:"The callgraph of the current project")
+ type t = Services.G.t
+
+ let get_vertices (g : t) =
+ Services.G.fold_vertex (fun v acc -> v :: acc ) g []
+
+ let get_edges (g : t) =
+ Services.G.fold_edges_e (fun v acc -> v :: acc ) g []
+
+ let get_entry_point () =
+ Services.entry_point () |>
+ Option.map (fun v -> v.Service_graph.node)
+
+ let to_json (g : t) =
+ default |>
+ set vertices (get_vertices g) |>
+ set edges (get_edges g) |>
+ set entry_point (get_entry_point ()) |>
+ to_json
+
+ let of_json _js = Data.failure "Graph.of_json not implemented"
+end
+
+let _signal =
+ States.register_value
+ ~package ~name:"callgraph"
+ ~descr:(Markdown.plain
+ "The current callgraph or an empty graph if it has not been computed yet")
+ ~output:(module Data.Joption (Graph))
+ ~add_hook:Services.add_hook
+ ~get:
+ begin fun () ->
+ if Services.is_computed () then
+ Some (Services.get ())
+ else
+ None
+ end
+ ()
+
+let _signal =
+ States.register_value
+ ~package ~name:"isComputed"
+ ~descr:(Markdown.plain
+ "This boolean is true if the graph has been computed")
+ ~output:(module Data.Jbool)
+ ~add_hook:Services.add_hook
+ ~get:Services.is_computed
+ ()
+
+let () = Request.register ~package
+ ~kind:`EXEC ~name:"compute"
+ ~descr:(Markdown.plain "Compute the callgraph for the current project")
+ ~input:(module Data.Junit) ~output:(module Data.Junit)
+ (fun () -> ignore (Services.get ()))
diff --git a/src/plugins/callgraph/requests.mli b/src/plugins/callgraph/requests.mli
new file mode 100644
index 00000000000..d68abd32119
--- /dev/null
+++ b/src/plugins/callgraph/requests.mli
@@ -0,0 +1,23 @@
+(**************************************************************************)
+(* *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+(* This module only register requests for Frama-C Server. Nothing is exported *)
diff --git a/src/plugins/callgraph/services.ml b/src/plugins/callgraph/services.ml
index b2d3f2893fb..1345b6fcdf9 100644
--- a/src/plugins/callgraph/services.ml
+++ b/src/plugins/callgraph/services.ml
@@ -77,9 +77,12 @@ module State =
let dependencies = [ Cg.self; Kernel.MainFunction.self ]
end)
+module StateHook = Hook.Build (S.Service_graph.Datatype)
+
(* eta-expansion required to mask optional argument [?project] *)
let is_computed () = State.is_computed ()
let self = State.self
+let add_hook = StateHook.extend
let compute () =
let cg = Cg.get () in
@@ -92,6 +95,7 @@ let compute () =
in
let sg = S.compute cg isr_names in
State.mark_as_computed ();
+ StateHook.apply sg;
sg
let get () = State.memo compute
--
GitLab