From da3b48becb0446d7c36a53bad4b79da68fd66078 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Thu, 6 Jul 2023 15:08:22 +0200
Subject: [PATCH] [ivette] Studia can be applied on arbitrary lvalues via a
dedicated search mode.
---
ivette/src/dome/renderer/dark.css | 2 +
ivette/src/dome/renderer/light.css | 2 +
ivette/src/frama-c/plugins/studia/studia.ts | 53 +++++++++++++++++++++
ivette/src/frama-c/plugins/studia/style.css | 5 ++
ivette/src/renderer/Application.tsx | 3 ++
5 files changed, 65 insertions(+)
create mode 100644 ivette/src/frama-c/plugins/studia/style.css
diff --git a/ivette/src/dome/renderer/dark.css b/ivette/src/dome/renderer/dark.css
index cbe9a2b73b5..b58523a06c7 100644
--- a/ivette/src/dome/renderer/dark.css
+++ b/ivette/src/dome/renderer/dark.css
@@ -88,6 +88,8 @@
--meter-subopti: linear-gradient(to bottom, #770 0%, #cc0 20%, #770 100%);
--meter-evenless: linear-gradient(to bottom, #710 0%, #c50 20%, #710 100%);
+ --studia-search-mode: #c2c71e;
+
--eva-evaluation-mode: #714074;
--eva-state-before: #082032;
--eva-state-after: #321428;
diff --git a/ivette/src/dome/renderer/light.css b/ivette/src/dome/renderer/light.css
index 135bd1ef348..919c24be478 100644
--- a/ivette/src/dome/renderer/light.css
+++ b/ivette/src/dome/renderer/light.css
@@ -88,6 +88,8 @@
--meter-subopti: linear-gradient(to bottom, #aa0 0%, #ff0 20%, #aa0 100%);
--meter-evenless: linear-gradient(to bottom, #a40 0%, #f80 20%, #a40 100%);
+ --studia-search-mode: #c5dc19;
+
--eva-evaluation-mode: #dc8fe1;
--eva-state-before: #95f5ff;
--eva-state-after: #fff819;
diff --git a/ivette/src/frama-c/plugins/studia/studia.ts b/ivette/src/frama-c/plugins/studia/studia.ts
index d84e1fb7e2a..a45a2b06e6e 100644
--- a/ivette/src/frama-c/plugins/studia/studia.ts
+++ b/ivette/src/frama-c/plugins/studia/studia.ts
@@ -20,11 +20,21 @@
/* */
/* ************************************************************************ */
+import React from 'react';
import * as Dome from 'dome';
import * as States from 'frama-c/states';
import * as Server from 'frama-c/server';
+import * as Toolbars from 'dome/frame/toolbars';
+import * as Status from 'frama-c/kernel/Status';
import * as Ast from 'frama-c/kernel/api/ast';
import { getWritesLval, getReadsLval } from 'frama-c/plugins/studia/api/studia';
+import { ipcRenderer } from 'electron';
+import './style.css';
+
+const studiaWritesEvent = new Dome.Event('dome.studia.writes');
+const studiaReadsEvent = new Dome.Event('dome.studia.reads');
+ipcRenderer.on('dome.ipc.studia.writes', () => studiaWritesEvent.emit());
+ipcRenderer.on('dome.ipc.studia.reads', () => studiaReadsEvent.emit());
type access = 'Reads' | 'Writes';
@@ -68,3 +78,46 @@ export function buildMenu(props: MenuProps) : void {
menu.push({ label: reads, enabled, onClick: () => onClick('Reads') });
menu.push({ label: writes, enabled, onClick: () => onClick('Writes') });
}
+
+export function useStudiaMode(): void {
+ const [selection, setSelection] = States.useSelection();
+ async function handleError(err: string): Promise<void> {
+ const msg = `Studia failure: ${err}.`;
+ Status.setMessage({ text: msg, kind: 'error' });
+ }
+ async function onEnter(label: string, kind: access): Promise<void> {
+ const stmt = selection?.current?.marker;
+ const data = { stmt, term: label };
+ const marker = await Server.send(Ast.parseLval, data).catch(handleError);
+ if (!marker) return;
+ compute(marker, label, kind).then(setSelection).catch(handleError);
+ }
+ const shared = {
+ placeholder: "lvalue",
+ icon: 'EDIT',
+ className: 'studia-search-mode',
+ hints: () => { return Promise.resolve([]); },
+ };
+ const writesMode = {
+ ...shared,
+ label: 'Studia: select writes',
+ title: `Select all statements writing the given lvalue`,
+ onEnter: (pattern:string) => onEnter(pattern, "Writes"),
+ event: studiaWritesEvent,
+ };
+ const readsMode = {
+ ...shared,
+ label: 'Studia: select reads',
+ title: `Selects all statements reading the given lvalue`,
+ onEnter: (pattern:string) => onEnter(pattern, "Reads"),
+ event: studiaReadsEvent,
+ };
+ React.useEffect(() => {
+ Toolbars.RegisterMode.emit(writesMode);
+ Toolbars.RegisterMode.emit(readsMode);
+ return () => {
+ Toolbars.UnregisterMode.emit(writesMode);
+ Toolbars.UnregisterMode.emit(readsMode);
+ };
+ });
+}
diff --git a/ivette/src/frama-c/plugins/studia/style.css b/ivette/src/frama-c/plugins/studia/style.css
new file mode 100644
index 00000000000..37090901780
--- /dev/null
+++ b/ivette/src/frama-c/plugins/studia/style.css
@@ -0,0 +1,5 @@
+
+.studia-search-mode {
+ background: var(--studia-search-mode);
+ fill: var(--text-discrete);
+}
diff --git a/ivette/src/renderer/Application.tsx b/ivette/src/renderer/Application.tsx
index c590f57fb6c..c6a1f7276e0 100644
--- a/ivette/src/renderer/Application.tsx
+++ b/ivette/src/renderer/Application.tsx
@@ -36,6 +36,7 @@ import * as Controller from './Controller';
import * as Extensions from './Extensions';
import * as Laboratory from './Laboratory';
import * as IvettePrefs from 'ivette/prefs';
+import * as Studia from 'frama-c/plugins/studia/studia';
import './loader';
import './sandbox';
@@ -49,6 +50,8 @@ export default function Application(): JSX.Element {
const [viewbar, flipViewbar] =
Dome.useFlipSettings('frama-c.viewbar.unfold', true);
+ Studia.useStudiaMode();
+
return (
<Vfill>
<Toolbar.ToolBar>
--
GitLab