diff --git a/ivette/src/dome/main/menubar.ts b/ivette/src/dome/main/menubar.ts
index a0095ce60be15ec10382a3c6638d91fcde4dd805..52f4212c96f0e09a6e8a85866acf4ac1b1e5b16e 100644
--- a/ivette/src/dome/main/menubar.ts
+++ b/ivette/src/dome/main/menubar.ts
@@ -404,7 +404,7 @@ export function setMenuItem({ id, ...options }: CustomMenuItem) {
if (entry) {
if (entry.spec) Object.assign(entry.spec, options);
if (entry.item) Object.assign(entry.item, options);
- if (options.label || options.type || options.click) requestUpdate();
+ requestUpdate ();
} else
console.warn(`[Dome] unknown menu item #${id}`);
}
diff --git a/ivette/src/dome/renderer/dark.css b/ivette/src/dome/renderer/dark.css
index 265d1d7d23c681419dac7002fb30920581eabc86..f53d8d9120eeed3dc74c02d0e7761f13c7cdea87 100644
--- a/ivette/src/dome/renderer/dark.css
+++ b/ivette/src/dome/renderer/dark.css
@@ -88,6 +88,7 @@
--meter-subopti: linear-gradient(to bottom, #770 0%, #cc0 20%, #770 100%);
--meter-evenless: linear-gradient(to bottom, #710 0%, #c50 20%, #710 100%);
+ --eva-evaluation-mode: #714074;
--eva-state-before: #082032;
--eva-state-after: #321428;
--eva-state-then: #98a02e;
diff --git a/ivette/src/dome/renderer/frame/style.css b/ivette/src/dome/renderer/frame/style.css
index f9d783ae1212313089d556f9bc563263e9a68f22..25343e43b59d10a0fd6761ceb38540c4e51a2063 100644
--- a/ivette/src/dome/renderer/frame/style.css
+++ b/ivette/src/dome/renderer/frame/style.css
@@ -480,6 +480,7 @@
width: 200px;
outline: none;
background: var(--background-softer);
+ color: var(--text);
}
.dome-xToolBar-actionComponent div.dome-xToolBar-suggestions {
diff --git a/ivette/src/dome/renderer/frame/toolbars.tsx b/ivette/src/dome/renderer/frame/toolbars.tsx
index 596a7ece181bfaeef49980544cf062a33958d779..9d7e9f196a9500a5e50299b99b956b5db906ada4 100644
--- a/ivette/src/dome/renderer/frame/toolbars.tsx
+++ b/ivette/src/dome/renderer/frame/toolbars.tsx
@@ -272,7 +272,7 @@ export function Select(props: SelectionProps<string>) {
export interface Hint {
id: string | number;
icon?: string;
- label: string | JSX.Element;
+ label: string;
title?: string;
value(): void;
rank?: number;
@@ -288,8 +288,10 @@ export type HintsEvaluator = (pattern: string) => Promise<Hint[]>;
/** Description of an action mode. */
export interface ActionMode {
- /** Mode tooltip text. */
- title: string;
+ /** Mode tooltip title. */
+ title?: string;
+ /** Mode tooltip label. */
+ label: string;
/** Mode placeholder text. */
placeholder?: string;
/** Icon displayed when the mode is selected. */
@@ -329,7 +331,8 @@ async function searchHints(pattern: string) {
}
const searchMode: ActionMode = {
- title: "Search",
+ label: "Search",
+ title: 'Search through the global definitions',
placeholder: "Search…",
icon: "SEARCH",
className: 'dome-xToolBar-searchMode',
@@ -415,7 +418,7 @@ function Suggestions(props: SuggestionsProps) {
// --------------------------------------------------------------------------
interface ActionInputProps {
- title: string;
+ title?: string;
placeholder?: string;
hints: Hint[];
onHint: (hint: Hint) => void;
@@ -529,16 +532,16 @@ export function ModalActionField() {
// Auxiliary function that build a Hint from an ActionMode.
const modeToHint = (mode: ActionMode) => {
- const { title, icon } = mode;
+ const { label, title = '', icon } = mode;
const id = 'ActionMode-' + title + '-' + icon;
const value = () => { onModeChange(mode); };
- return { id, icon, label: title, title, value, rank: -1000 };
+ return { id, icon, label, title, value, rank: -1000 };
};
// Hints provider for the mode of all modes.
const modesHints = React.useCallback((input: string) => {
const p = input.toLowerCase();
- const fit = (m: ActionMode) => m.title.toLowerCase().includes(p);
+ const fit = (m: ActionMode) => m.label.toLowerCase().includes(p);
return Promise.resolve(Array.from(allModes).filter(fit).map(modeToHint));
}, [allModes]);
@@ -546,20 +549,20 @@ export function ModalActionField() {
// on the current mode icon and allows to change the current mode, displaying
// a list of all available modes as hints.
const modesMode = React.useMemo(() => {
- const title = "Mode selection";
+ const label = "Mode selection";
const placeholder = "Search mode";
const icon = "TUNINGS";
const className = 'dome-xToolBar-modeOfModes';
- return { title, placeholder, icon, className, hints: modesHints };
+ return { label, placeholder, icon, className, hints: modesHints };
}, [modesHints]);
// Build a new search engine for the search mode, adding available modes to
// the possible search hints.
const searchModeHints = React.useCallback(async (input: string) => {
const hs = await modesMode.hints(input);
- const notCurrent = (h: Hint) => !(h.title?.includes(current.title));
+ const notCurrent = (h: Hint) => !(h.label.includes(current.label));
return hs.filter(notCurrent);
- }, [current.title, modesMode]);
+ }, [current.label, modesMode]);
// Register the new search engine.
React.useEffect(() => {
diff --git a/ivette/src/dome/renderer/light.css b/ivette/src/dome/renderer/light.css
index 1eb31da53fc00624364f9f6577ef1114ef196c60..b9563c7d155cfdada7aeaf15bc7ed7f133cd3800 100644
--- a/ivette/src/dome/renderer/light.css
+++ b/ivette/src/dome/renderer/light.css
@@ -88,6 +88,7 @@
--meter-subopti: linear-gradient(to bottom, #aa0 0%, #ff0 20%, #aa0 100%);
--meter-evenless: linear-gradient(to bottom, #a40 0%, #f80 20%, #a40 100%);
+ --eva-evaluation-mode: #dc8fe1;
--eva-state-before: #95f5ff;
--eva-state-after: #fff819;
--eva-state-then: #c8e06e;
diff --git a/ivette/src/frama-c/kernel/api/ast/index.ts b/ivette/src/frama-c/kernel/api/ast/index.ts
index 40bf034596919523dba48b67e06bb05d0d6a69d2..70b14dd814e7cb57c693dff3a5a86b5515feed05 100644
--- a/ivette/src/frama-c/kernel/api/ast/index.ts
+++ b/ivette/src/frama-c/kernel/api/ast/index.ts
@@ -528,4 +528,49 @@ const setFiles_internal: Server.SetRequest<string[],null> = {
/** Set the source file names to analyze. */
export const setFiles: Server.SetRequest<string[],null>= setFiles_internal;
+/** <markerFromTerm> input */
+export interface markerFromTermInput {
+ /** The statement at which we will build the marker. */
+ atStmt: marker;
+ /** The ACSL term. */
+ term: string;
+}
+
+/** Loose decoder for `markerFromTermInput` */
+export const jMarkerFromTermInput: Json.Loose<markerFromTermInput> =
+ Json.jObject({
+ atStmt: jMarkerSafe,
+ term: Json.jFail(Json.jString,'String expected'),
+ });
+
+/** Safe decoder for `markerFromTermInput` */
+export const jMarkerFromTermInputSafe: Json.Safe<markerFromTermInput> =
+ Json.jFail(jMarkerFromTermInput,'MarkerFromTermInput expected');
+
+/** Natural order for `markerFromTermInput` */
+export const byMarkerFromTermInput: Compare.Order<markerFromTermInput> =
+ Compare.byFields
+ <{ atStmt: marker, term: string }>({
+ atStmt: byMarker,
+ term: Compare.string,
+ });
+
+const markerFromTerm_internal: Server.GetRequest<
+ markerFromTermInput,
+ marker |
+ undefined
+ > = {
+ kind: Server.RqKind.GET,
+ name: 'kernel.ast.markerFromTerm',
+ input: jMarkerFromTermInput,
+ output: jMarker,
+ signals: [],
+};
+/** Build a marker from an ACSL term. */
+export const markerFromTerm: Server.GetRequest<
+ markerFromTermInput,
+ marker |
+ undefined
+ >= markerFromTerm_internal;
+
/* ------------------------------------- */
diff --git a/ivette/src/frama-c/plugins/eva/style.css b/ivette/src/frama-c/plugins/eva/style.css
index 34a3fce5060b1aea5442781b961a7bd06b85d05e..e4a17e65e23a5e3baf3af13f49d6f319b4c86f35 100644
--- a/ivette/src/frama-c/plugins/eva/style.css
+++ b/ivette/src/frama-c/plugins/eva/style.css
@@ -254,7 +254,7 @@ tr:first-of-type > .eva-table-callsite-box {
.eva-table-descrs {
background-color: var(--background-sidebar);
- border-right: thin solid var(--border);
+ text-align: center;
}
.eva-table-descr-sticky {
@@ -302,4 +302,18 @@ tr:first-of-type > .eva-table-callsite-box {
background: var(--code-select);
}
+.eva-evaluation-mode {
+ background: purple;
+ fill: white;
+}
+
+/* -------------------------------------------------------------------------- */
+/* --- Evaluation Mode CSS --- */
+/* -------------------------------------------------------------------------- */
+
+.eva-evaluation-mode {
+ background: var(--eva-evaluation-mode);
+ fill: var(--text-discrete);
+}
+
/* -------------------------------------------------------------------------- */
diff --git a/ivette/src/frama-c/plugins/eva/valuetable.tsx b/ivette/src/frama-c/plugins/eva/valuetable.tsx
index 63b225fd27088c3374be59051e7d0653566ff4ce..00c3b7738bac9049344c90b3addc42ce9b28d34f 100644
--- a/ivette/src/frama-c/plugins/eva/valuetable.tsx
+++ b/ivette/src/frama-c/plugins/eva/valuetable.tsx
@@ -24,18 +24,22 @@ import React from 'react';
import _ from 'lodash';
import * as Ivette from 'ivette';
import * as Dome from 'dome/dome';
+import * as System from 'dome/system';
import * as States from 'frama-c/states';
import * as Server from 'frama-c/server';
import * as Ast from 'frama-c/kernel/api/ast';
+import * as Eva from 'frama-c/plugins/eva/api/general';
import * as Values from 'frama-c/plugins/eva/api/values';
import { GlobalState, useGlobalState } from 'dome/data/states';
import { classes } from 'dome/misc/utils';
import { Icon } from 'dome/controls/icons';
import { Inset } from 'dome/frame/toolbars';
+import * as Toolbars from 'dome/frame/toolbars';
import { Cell, Code } from 'dome/controls/labels';
import { IconButton } from 'dome/controls/buttons';
import { Filler, Hpack, Hfill, Vpack, Vfill } from 'dome/layout/boxes';
+import { ipcRenderer } from 'electron';
@@ -897,6 +901,64 @@ class FunctionsManager {
+/* -------------------------------------------------------------------------- */
+/* --- Evaluation Mode Handling --- */
+/* -------------------------------------------------------------------------- */
+
+export const evaluateEvent = new Dome.Event('dome.evaluate');
+ipcRenderer.on('dome.ipc.evaluate', () => evaluateEvent.emit());
+
+interface EvaluationModeProps {
+ computationState : Eva.computationStateType | undefined;
+ selection: States.Selection;
+ setLocPin: (loc: Location, pin: boolean) => void;
+}
+
+function useEvaluationMode(props: EvaluationModeProps): void {
+ const { computationState, selection, setLocPin } = props;
+ const handleError = (): void => { return; };
+ const addProbe = (target: Ast.marker | undefined): void => {
+ const fct = selection?.current?.fct;
+ if (fct && target) setLocPin({ fct, target }, true);
+ };
+ React.useEffect(() => {
+ if (computationState !== 'computed') return () => { return; };
+ const shortcut = System.platform === 'macos' ? 'Cmd+E' : 'Ctrl+E';
+ const onEnter = (pattern: string): void => {
+ const marker = selection?.current?.marker;
+ const data = { atStmt: marker, term: pattern };
+ Server.send(Ast.markerFromTerm, data).then(addProbe).catch(handleError);
+ };
+ const evalMode = {
+ label: 'Evaluation',
+ title: `Evaluate an ACSL expression (shortcut: ${shortcut})`,
+ icon: 'TERMINAL',
+ className: 'eva-evaluation-mode',
+ hints: () => { return Promise.resolve([]); },
+ onEnter,
+ event: evaluateEvent,
+ };
+ Toolbars.RegisterMode.emit(evalMode);
+ return () => Toolbars.UnregisterMode.emit(evalMode);
+ });
+ Dome.addMenuItem({
+ menu: 'Edit',
+ id: 'EvaluateMenu',
+ type: 'normal',
+ label: 'Evaluate',
+ key: 'Cmd+E',
+ onClick: () => evaluateEvent.emit(),
+ });
+ React.useEffect(() => {
+ Dome.setMenuItem({ id: 'EvaluateMenu', enabled: true });
+ return () => Dome.setMenuItem({ id: 'EvaluateMenu', enabled: false });
+ });
+}
+
+/* -------------------------------------------------------------------------- */
+
+
+
/* -------------------------------------------------------------------------- */
/* --- Eva Table Complet Component --- */
/* -------------------------------------------------------------------------- */
@@ -1061,6 +1123,10 @@ function EvaTable(): JSX.Element {
}, [ cs, setCS, select, getCallsites, selection ]);
const { result: stackInfos } = Dome.usePromise(stackInfosPromise);
+ /* Handle Evaluation mode */
+ const computationState = States.useSyncValue(Eva.computationState);
+ useEvaluationMode({ computationState, selection, setLocPin });
+
/* Builds the component */
return (
<>
diff --git a/src/plugins/server/kernel_ast.ml b/src/plugins/server/kernel_ast.ml
index 84d21cb8a070f28a812fe2a47965b64a0191e041..61134be680a1e7fbd1fb15fddabbc0d372a4a22e 100644
--- a/src/plugins/server/kernel_ast.ml
+++ b/src/plugins/server/kernel_ast.ml
@@ -28,6 +28,36 @@ open Cil_types
let package = Pkg.package ~title:"Ast Services" ~name:"ast" ~readme:"ast.md" ()
+(* -------------------------------------------------------------------------- *)
+(* --- Marker Cache System --- *)
+(* -------------------------------------------------------------------------- *)
+
+let logic_environment () =
+ let open Logic_typing in
+ Lenv.empty () |> append_pre_label |> append_init_label |> append_here_label
+
+module Key = Datatype.Pair(Cil_datatype.Stmt)(Cil_datatype.Term)
+module Cache = Hashtbl.Make(Key)
+
+let get_term kf term =
+ let env = logic_environment () in
+ try Some (!Db.Properties.Interp.term ~env kf term)
+ with Logic_interp.Error _ | Parsing.Parse_error -> None
+
+let key_of_localizable =
+ let open Printer_tag in
+ function
+ | PStmt _ | PStmtStart _ | PTermLval _ | PVDecl _ | PGlobal _ | PIP _ -> None
+ | PLval (_, Kglobal, _) | PExp (_, Kglobal, _) -> None
+ | PLval (kf, Kstmt stmt, lval) ->
+ let str = Format.asprintf "%a" Cil_datatype.Lval.pretty lval in
+ Option.(bind kf (fun kf -> get_term kf str) |> map (fun t -> (stmt, t)))
+ | PExp (kf, Kstmt stmt, exp) ->
+ let str = Format.asprintf "%a" Cil_datatype.Exp.pretty exp in
+ Option.(bind kf (fun kf -> get_term kf str) |> map (fun t -> (stmt, t)))
+
+let cache = Cache.create 10
+
(* -------------------------------------------------------------------------- *)
(* --- Compute Ast --- *)
(* -------------------------------------------------------------------------- *)
@@ -276,6 +306,8 @@ struct
| PIP _ -> Printf.sprintf "#p%d" (incr kid ; !kid)
let create loc =
+ let add_cache key = Cache.add cache key loc in
+ key_of_localizable loc |> Option.iter add_cache;
let { tags ; locs } = STATE.get () in
try Localizable.Hashtbl.find tags loc
with Not_found ->
@@ -746,3 +778,66 @@ let () =
set_files
(* -------------------------------------------------------------------------- *)
+(* ----- Build a marker from an ACSL term ----------------------------------- *)
+(* -------------------------------------------------------------------------- *)
+
+type marker_term_input = { atStmt : stmt ; term : string }
+
+module MarkerTermInput = struct
+ type record
+ let record : record Record.signature = Record.signature ()
+
+ let atStmt =
+ let descr = "The statement at which we will build the marker." in
+ Record.field record ~name:"atStmt" ~descr:(Markdown.plain descr)
+ (module Marker)
+
+ let term =
+ let descr = "The ACSL term." in
+ Record.field record ~name:"term" ~descr:(Markdown.plain descr)
+ (module Data.Jstring)
+
+ let data =
+ Record.publish record ~package ~name:"markerFromTermInput"
+ ~descr:(Markdown.plain "<markerFromTerm> input")
+
+ module R : Record.S with type r = record = (val data)
+ type t = marker_term_input option
+ let jtype = R.jtype
+
+ let of_json js =
+ let record = R.of_json js in
+ match R.get atStmt record with
+ | PStmt (_, s) | PStmtStart (_, s)
+ | PLval (_, Kstmt s, _) | PExp (_, Kstmt s, _)
+ | PTermLval (_, Kstmt s, _, _)
+ | PVDecl (_, Kstmt s, _) ->
+ let term = R.get term record in
+ Some { atStmt = s ; term }
+ | _ -> None
+
+end
+
+module MarkerTermOutput = Data.Joption (Marker)
+
+let build_marker =
+ Option.map @@ fun input ->
+ let env = logic_environment () in
+ let kf = Kernel_function.find_englobing_kf input.atStmt in
+ let term = !Db.Properties.Interp.term ~env kf input.term in
+ let key = (input.atStmt, term) in
+ match Cache.find_opt cache key with
+ | Some tag -> tag
+ | None ->
+ let exp = !Db.Properties.Interp.term_to_exp ~result:None term in
+ let tag = Printer_tag.PExp (Some kf, Kstmt input.atStmt, exp) in
+ Cache.add cache key tag ; tag
+
+let descr = "Build a marker from an ACSL term."
+
+let () = Request.register ~package
+ ~kind:`GET ~name:"markerFromTerm" ~descr:(Markdown.plain descr)
+ ~input:(module MarkerTermInput) ~output:(module MarkerTermOutput)
+ build_marker
+
+(**************************************************************************)