From bb114688855ef8d1e5181bfab6d933a2feab9b3b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Lo=C3=AFc=20Correnson?= <loic.correnson@cea.fr>
Date: Fri, 7 Jun 2024 14:49:41 +0200
Subject: [PATCH] [regions] on-demand computing
---
.../src/frama-c/plugins/region/api/index.ts | 9 ++-
ivette/src/frama-c/plugins/region/index.tsx | 65 ++++++++++++++++++-
ivette/src/frama-c/plugins/region/memory.tsx | 15 +++--
ivette/src/frama-c/plugins/region/style.css | 9 +++
src/plugins/region/analysis.ml | 2 +
src/plugins/region/analysis.mli | 3 +
src/plugins/region/services.ml | 7 ++
7 files changed, 99 insertions(+), 11 deletions(-)
create mode 100644 ivette/src/frama-c/plugins/region/style.css
diff --git a/ivette/src/frama-c/plugins/region/api/index.ts b/ivette/src/frama-c/plugins/region/api/index.ts
index cc0b4835c5e..942053971ed 100644
--- a/ivette/src/frama-c/plugins/region/api/index.ts
+++ b/ivette/src/frama-c/plugins/region/api/index.ts
@@ -137,6 +137,11 @@ export const regionDefault: region =
pointed: undefined, reads: false, writes: false, bytes: false, label: '',
title: '' };
+/** Region Analysis Updated */
+export const updated: Server.Signal = {
+ name: 'plugins.region.updated',
+};
+
const compute_internal: Server.ExecRequest<decl,null> = {
kind: Server.RqKind.EXEC,
name: 'plugins.region.compute',
@@ -152,7 +157,7 @@ const regions_internal: Server.GetRequest<decl,region[]> = {
name: 'plugins.region.regions',
input: jDecl,
output: Json.jArray(jRegion),
- signals: [],
+ signals: [ { name: 'plugins.region.updated' } ],
};
/** Compute regions for the given declaration */
export const regions: Server.GetRequest<decl,region[]>= regions_internal;
@@ -162,7 +167,7 @@ const regionsAt_internal: Server.GetRequest<marker,region[]> = {
name: 'plugins.region.regionsAt',
input: jMarker,
output: Json.jArray(jRegion),
- signals: [],
+ signals: [ { name: 'plugins.region.updated' } ],
};
/** Compute regions at the given marker position */
export const regionsAt: Server.GetRequest<marker,region[]>= regionsAt_internal;
diff --git a/ivette/src/frama-c/plugins/region/index.tsx b/ivette/src/frama-c/plugins/region/index.tsx
index 5cebfb451ff..3bf4a449f4d 100644
--- a/ivette/src/frama-c/plugins/region/index.tsx
+++ b/ivette/src/frama-c/plugins/region/index.tsx
@@ -25,14 +25,75 @@
// --------------------------------------------------------------------------
import React from 'react';
+import { Label } from 'dome/controls/labels';
+import { LCD } from 'dome/controls/displays';
+import { IconButton } from 'dome/controls/buttons';
+import * as Dome from 'dome';
+import * as Tools from 'dome/frame/toolbars';
import * as Ivette from 'ivette';
+import * as Server from 'frama-c/server';
+import * as States from 'frama-c/states';
+import * as Region from './api';
import { MemoryView } from './memory';
+import './style.css';
+
+function RegionAnalys(): JSX.Element {
+ const [kf, setKf] = React.useState<States.Scope>();
+ const [kfName, setName] = React.useState<string>();
+ const [pinned, setPinned] = React.useState(false);
+ const [running, setRunning] = React.useState(false);
+ const setComputing = Dome.useProtected(setRunning);
+ const scope = States.useCurrentScope();
+ const { kind, name } = States.useDeclaration(scope);
+ const regions = States.useRequest(Region.regions, kf) ?? [];
+ React.useEffect(() => {
+ if (!pinned && kind === 'FUNCTION' && scope !== kf) {
+ setKf(scope);
+ setName(name);
+ } else if (!Server.isRunning()) {
+ setKf(undefined);
+ setName(undefined);
+ setPinned(false);
+ }
+ }, [pinned, kind, name, scope, kf]);
+ async function compute(): Promise<void> {
+ try {
+ setComputing(true);
+ await Server.send(Region.compute, kf);
+ } finally {
+ setComputing(false);
+ }
+ }
+ return (
+ <>
+ <Tools.ToolBar>
+ <Label label='Function' />
+ <LCD className='region-lcd' label={kfName ?? '---'} />
+ <Tools.Button
+ icon={running ? 'EXECUTE' : 'MEDIA.PLAY'}
+ title='Run region analysis on the selected function'
+ disabled={running}
+ visible={kf !== undefined && regions.length === 0}
+ onClick={compute}
+ />
+ <IconButton
+ icon='PIN'
+ display={kf !== undefined}
+ title='Keep focus on current function'
+ selected={pinned}
+ onClick={() => setPinned(!pinned)}
+ />
+ </Tools.ToolBar>
+ <MemoryView regions={regions} />
+ </>
+ );
+}
Ivette.registerComponent({
id: 'fc.region.main',
label: 'Region Analysis',
- preferredPosition: 'B',
- children: <MemoryView />,
+ preferredPosition: 'BD',
+ children: <RegionAnalys />,
});
// --------------------------------------------------------------------------
diff --git a/ivette/src/frama-c/plugins/region/memory.tsx b/ivette/src/frama-c/plugins/region/memory.tsx
index bc84a8dc5e4..81c4fd55d9f 100644
--- a/ivette/src/frama-c/plugins/region/memory.tsx
+++ b/ivette/src/frama-c/plugins/region/memory.tsx
@@ -26,10 +26,9 @@
import React from 'react';
import * as Dot from 'dome/graph/diagram';
-import * as States from 'frama-c/states';
import * as Region from './api';
-function makeDiagram(regions: Region.region[]): Dot.DiagramProps {
+function makeDiagram(regions: readonly Region.region[]): Dot.DiagramProps {
const nodes: Dot.Node[] = [];
const edges: Dot.Edge[] = [];
regions.forEach(r => {
@@ -65,10 +64,12 @@ function makeDiagram(regions: Region.region[]): Dot.DiagramProps {
return { nodes, edges };
}
-export function MemoryView(): JSX.Element {
- const scope = States.useCurrentScope();
- // eslint-disable-next-line react-hooks/exhaustive-deps
- const regions = States.useRequest(Region.regions, scope) ?? [];
+export interface MemoryViewProps {
+ regions: readonly Region.region[];
+}
+
+export function MemoryView(props: MemoryViewProps): JSX.Element {
+ const { regions } = props;
const diagram = React.useMemo(() => makeDiagram(regions), [regions]);
- return <Dot.Diagram display={regions.length > 0} {...diagram} />;
+ return <Dot.Diagram {...diagram} />;
}
diff --git a/ivette/src/frama-c/plugins/region/style.css b/ivette/src/frama-c/plugins/region/style.css
new file mode 100644
index 00000000000..0076926a052
--- /dev/null
+++ b/ivette/src/frama-c/plugins/region/style.css
@@ -0,0 +1,9 @@
+/* -------------------------------------------------------------------------- */
+/* --- CSS for Region Views --- */
+/* -------------------------------------------------------------------------- */
+
+.region-lcd {
+ margin-top: 4px;
+ min-width: 160px;
+ text-align: center;
+}
diff --git a/src/plugins/region/analysis.ml b/src/plugins/region/analysis.ml
index ae65c3fdca9..b64c6571bc8 100644
--- a/src/plugins/region/analysis.ml
+++ b/src/plugins/region/analysis.ml
@@ -69,4 +69,6 @@ let get kf =
let compute kf = ignore @@ get kf
+let add_hook f = STATE.add_hook_on_change (fun _ -> f())
+
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/region/analysis.mli b/src/plugins/region/analysis.mli
index a28624691b5..e9279b47420 100644
--- a/src/plugins/region/analysis.mli
+++ b/src/plugins/region/analysis.mli
@@ -30,3 +30,6 @@ val get : kernel_function -> Code.domain
(** Memoized *)
val compute : kernel_function -> unit
+
+(** Hook on update *)
+val add_hook : (unit -> unit) -> unit
diff --git a/src/plugins/region/services.ml b/src/plugins/region/services.ml
index 7b93f23d8f7..990424bbe4d 100644
--- a/src/plugins/region/services.ml
+++ b/src/plugins/region/services.ml
@@ -192,6 +192,11 @@ let map_of_declaration (decl : Printer_tag.declaration) =
| SFunction kf -> (Analysis.find kf).map
| _ -> raise Not_found
+let signal = Request.signal ~package ~name:"updated"
+ ~descr:(Md.plain "Region Analysis Updated")
+
+let () = Analysis.add_hook (fun () -> Request.emit signal)
+
let () =
Request.register
~package ~kind:`EXEC ~name:"compute"
@@ -206,6 +211,7 @@ let () =
~descr:(Md.plain "Compute regions for the given declaration")
~input:(module Kernel_ast.Decl)
~output:(module Regions)
+ ~signals:[signal]
begin fun decl ->
try regions @@ map_of_declaration decl
with Not_found -> []
@@ -217,6 +223,7 @@ let () =
~descr:(Md.plain "Compute regions at the given marker position")
~input:(module Kernel_ast.Marker)
~output:(module Regions)
+ ~signals:[signal]
begin fun loc ->
try regions @@ map_of_localizable loc
with Not_found -> []
--
GitLab