diff --git a/ivette/package.json b/ivette/package.json
index 5c000eebf185db31c6cb64f668ae09dad48fbd1d..bedf12a40ddbf6d65752f15353aec760bfbebc31 100644
--- a/ivette/package.json
+++ b/ivette/package.json
@@ -58,6 +58,11 @@
"@types/diff": "",
"@types/react-window": "",
"codemirror": "^5.65.2",
+ "@codemirror/view": "6.2.3",
+ "@codemirror/state": "6.1.1",
+ "@codemirror/language": "6.2.1",
+ "@codemirror/commands": "6.1.0",
+ "@codemirror/lang-cpp": "6.0.1",
"cytoscape": "",
"cytoscape-cola": "",
"cytoscape-cose-bilkent": "",
diff --git a/ivette/src/dome/renderer/dark.css b/ivette/src/dome/renderer/dark.css
index f53d8d9120eeed3dc74c02d0e7761f13c7cdea87..0660868825afc53f7e051a476f593e2d9c4d15f6 100644
--- a/ivette/src/dome/renderer/dark.css
+++ b/ivette/src/dome/renderer/dark.css
@@ -100,5 +100,11 @@
--eva-alarms-true: green;
--eva-alarms-false: #fb4e4a;
--eva-alarms-unknown: darkorange;
+
+ --codemirror-comment: #748a8d;
+ --codemirror-type: #bacd5f;
+ --codemirror-number: #d3869b;
+ --codemirror-keyword: #d84954;
+ --codemirror-def: #94aadd;
}
}
diff --git a/ivette/src/dome/renderer/data/arrays.ts b/ivette/src/dome/renderer/data/arrays.ts
index adc862f8913c006a9b968afe6d69b17a5b7fd750..26076398cc91fa72ea59b797abe627eef7e896e5 100644
--- a/ivette/src/dome/renderer/data/arrays.ts
+++ b/ivette/src/dome/renderer/data/arrays.ts
@@ -64,3 +64,11 @@ export function mergeArraysByKey<A, B>(
): (A | A & B)[] {
return mergeArrays(a1, a2, (x1, x2) => x1.key === x2.key);
}
+
+/** Maps a function through an array and returns the first computed value that
+ is not undefined. */
+export type Maybe<A> = A | undefined;
+export function first<X, R>(xs: X[], fn: (x: X) => Maybe<R>): Maybe<R> {
+ for (const x of xs) { const r = fn(x); if (r) return r; }
+ return undefined;
+}
diff --git a/ivette/src/dome/renderer/light.css b/ivette/src/dome/renderer/light.css
index eead3201596027ab0934dc20d9f447e90b89dce9..0caf3fb0e549257228f9e19d34c17a8b73f51b34 100644
--- a/ivette/src/dome/renderer/light.css
+++ b/ivette/src/dome/renderer/light.css
@@ -100,5 +100,11 @@
--eva-alarms-true: green;
--eva-alarms-false: #fb4e4a;
--eva-alarms-unknown: darkorange;
+
+ --codemirror-comment: #aa5500;
+ --codemirror-type: #008855;
+ --codemirror-number: #116644;
+ --codemirror-keyword: #770088;
+ --codemirror-def: #0000ff;
}
}
diff --git a/ivette/src/dome/renderer/text/editor.tsx b/ivette/src/dome/renderer/text/editor.tsx
new file mode 100644
index 0000000000000000000000000000000000000000..6f0438512f5f3702932e122c44c7cbe4dcea7a48
--- /dev/null
+++ b/ivette/src/dome/renderer/text/editor.tsx
@@ -0,0 +1,456 @@
+/* ************************************************************************ */
+/* */
+/* 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 { EditorState, StateField, Facet, Extension } from '@codemirror/state';
+import { Annotation, Transaction, RangeSet } from '@codemirror/state';
+import { EditorSelection, Text } from '@codemirror/state';
+
+import { EditorView, ViewPlugin, ViewUpdate } from '@codemirror/view';
+import { Decoration, DecorationSet } from '@codemirror/view';
+import { DOMEventMap as EventMap } from '@codemirror/view';
+import { GutterMarker, gutter } from '@codemirror/view';
+import { Tooltip, showTooltip } from '@codemirror/view';
+import { lineNumbers } from '@codemirror/view';
+
+import { parser } from '@lezer/cpp';
+import { tags } from '@lezer/highlight';
+import { SyntaxNode } from '@lezer/common';
+import * as Language from '@codemirror/language';
+
+import './style.css';
+
+export type { Extension } from '@codemirror/state';
+export { GutterMarker } from '@codemirror/view';
+export { Decoration } from '@codemirror/view';
+export { RangeSet } from '@codemirror/state';
+
+
+
+// -----------------------------------------------------------------------------
+// CodeMirror state's extensions types definitions
+// -----------------------------------------------------------------------------
+
+// Helper types definitions.
+export type View = EditorView | null;
+export type Range = { from: number, to: number };
+export type Set<A> = (view: View, value: A) => void;
+export type Get<A> = (state: EditorState | undefined) => A;
+export type IsUpdated = (update: ViewUpdate) => boolean;
+export interface Struct<S> { structure: S, extension: Extension }
+export interface Value<A> { init: A, get: Get<A> }
+export interface Data<A, S> extends Value<A>, Struct<S> { isUpdated: IsUpdated }
+
+// Event handlers type definition.
+export type Handler<I, E> = (i: I, v: EditorView, e: E) => void;
+export type Handlers<I> = { [e in keyof EventMap]?: Handler<I, EventMap[e]> };
+
+// A Field is a data added to the CodeMirror internal state that can be
+// modified by the outside world and used by plugins. The typical use case is
+// when one needs to inject information from the server into the CodeMirror
+// component. A Field exposes a getter and a setter that handles all React's
+// hooks shenanigans. It also exposes a StateField, a CodeMirror data structure
+// representing the internal state's part responsible of the data. This
+// structure is exposed for two reasons. The first one is that it contains the
+// extension that must be added to the CodeMirror instanciation. The second one
+// is that it is needed during the Aspects creation's process.
+export interface Field<A> extends Data<A, StateField<A>> { set: Set<A> }
+
+// An Aspect is a data associated with an editor state and computed by combining
+// data from several fields. A typical use case is if one needs a data that
+// relies on a server side information (like a synchronized array) which must be
+// recomputed each time the selection (which is a field but is also an internal
+// information of CodeMirror) is changed. An Aspect exposes a getter that
+// handles all React's hooks shenanigans and an extension that must be added to
+// the CodeMirror initial configuration.
+export type Aspect<A> = Data<A, Facet<A, A>>;
+
+// State extensions and Aspects have to declare their dependencies, i.e. the
+// Field and Aspects they rely on to perform their computations. Dependencies
+// are declared as a record mapping names to either a Field or an Aspect. This
+// is needed to be able to give the dependencies values to the computing
+// functions in a typed manner. However, an important point to take into
+// consideration is that the extensions constructors defined below cannot
+// actually typecheck without relying on type assertions. It means that if you
+// declare an extension's dependencies after creating the extension, it will
+// crash at execution time. So please, check that every dependency is declared
+// before being used.
+export type Dict = Record<string, unknown>;
+export type Dependency<A> = Field<A> | Aspect<A>;
+export type Dependencies<I extends Dict> = { [K in keyof I]: Dependency<I[K]> };
+
+// -----------------------------------------------------------------------------
+
+
+
+// -----------------------------------------------------------------------------
+// Internal types and helpers
+// -----------------------------------------------------------------------------
+
+// Type aliases to shorten internal definitions.
+type Dep<A> = Dependency<A>;
+type Deps<I extends Dict> = Dependencies<I>;
+type Combine<Output> = (l: readonly Output[]) => Output;
+type Pred<I extends Dict> = (d: Dep<I[typeof k]>, k: string) => boolean;
+type Mapper<I extends Dict, A> = (d: Dep<I[typeof k]>, k: string) => A;
+type Transform<I extends Dict> = Mapper<I, unknown>;
+
+// Helper function used to map a function over Dependencies.
+function mapDeps<I extends Dict, A>(deps: Deps<I>, fn: Mapper<I, A>): A[] {
+ return Object.keys(deps).map((k) => fn(deps[k], k));
+}
+
+// Helper function used to check if at least one depencency satisfied a
+// given predicate.
+function existsDeps<I extends Dict>(deps: Deps<I>, fn: Pred<I>): boolean {
+ return Object.keys(deps).find((k) => fn(deps[k], k)) !== undefined;
+}
+
+// Helper function used to transfrom a Dependencies will keeping its structure.
+function transformDeps<I extends Dict>(deps: Deps<I>, tr: Transform<I>): Dict {
+ return Object.fromEntries(Object.keys(deps).map(k => [k, tr(deps[k], k)]));
+}
+
+// Helper function retrieving the current values associated to each dependencies
+// in a given editor state. They are returned as a Dict instead of the precise
+// type because of TypeScript subtyping shenanigans that prevent us to correctly
+// type the returned record. Thus, a type assertion has to be used.
+function inputs<I extends Dict>(ds: Deps<I>, s: EditorState | undefined): Dict {
+ return transformDeps(ds, (d) => d.get(s));
+}
+
+// -----------------------------------------------------------------------------
+
+
+
+// -----------------------------------------------------------------------------
+// CodeMirror state's extensions
+// -----------------------------------------------------------------------------
+
+// Several extensions constructors are provided. Each one of them encapsulates
+// its dependencies if needed. This means that adding an extension to the
+// CodeMirror's initial configuration will also add all its dependencies'
+// extensions, and thus recursively. However, for now, there is no systemic way
+// to check that the fields at the root of the dependencies tree are updated by
+// a component. This means you have to verify, by hands, that every field is
+// updated when needed by your component. It may be possible to compute a
+// function that asks for a value for each fields in the dependencies tree and
+// does the update for you, thus forcing you to actually update every fields.
+// But it seems hard to define and harder to type.
+
+// A Field is simply declared using an initial value. However, to be able to
+// use it, you must add its extension (obtained through <field.extension>) to
+// the CodeMirror initial configuration. If determining equality between
+// values of the given type cannot be done using (===), an equality test can be
+// provided through the optional parameters <equal>. Providing an equality test
+// for complex types can help improve performances by avoiding recomputing
+// extensions depending on the field.
+export function createField<A>(init: A): Field<A> {
+ const annot = Annotation.define<A>();
+ const create = (): A => init;
+ type Update<A> = (current: A, transaction: Transaction) => A;
+ const update: Update<A> = (current, tr) => tr.annotation(annot) ?? current;
+ const field = StateField.define<A>({ create, update });
+ const get: Get<A> = (state) => state?.field(field) ?? init;
+ const set: Set<A> = (v, a) => v?.dispatch({ annotations: annot.of(a) });
+ const isUpdated: IsUpdated = (update) =>
+ update.transactions.find((tr) => tr.annotation(annot)) !== undefined;
+ return { init, get, set, structure: field, extension: field, isUpdated };
+}
+
+// An Aspect is declared using its dependencies and a function. This function's
+// input is a record containing, for each key of the dependencies record, a
+// value of the type of the corresponding field. The function's output is a
+// value of the aspect's type.
+export function createAspect<I extends Dict, O>(
+ deps: Dependencies<I>,
+ fn: (input: I) => O,
+): Aspect<O> {
+ const enables = mapDeps(deps, (d) => d.extension);
+ const init = fn(transformDeps(deps, (d) => d.init) as I);
+ const combine: Combine<O> = (l) => l.length > 0 ? l[l.length - 1] : init;
+ const facet = Facet.define<O, O>({ combine, enables });
+ const get: Get<O> = (state) => state?.facet(facet) ?? init;
+ const convertedDeps = mapDeps(deps, (d) => d.structure);
+ const compute: Get<O> = (s) => fn(inputs(deps, s) as I);
+ const extension = facet.compute(convertedDeps, compute);
+ const isUpdated: IsUpdated = (update) =>
+ existsDeps(deps, (d) => d.isUpdated(update));
+ return { init, get, structure: facet, extension, isUpdated };
+}
+
+// A Decorator is an extension that adds decorations to the CodeMirror's
+// document, i.e. it tags subpart of the document with CSS classes. See the
+// CodeMirror's documentation on Decoration for further details.
+export function createDecorator<I extends Dict>(
+ deps: Dependencies<I>,
+ fn: (inputs: I, state: EditorState) => DecorationSet
+): Extension {
+ const enables = mapDeps(deps, (d) => d.extension);
+ const get = (s: EditorState): DecorationSet => fn(inputs(deps, s) as I, s);
+ class S { s: DecorationSet = RangeSet.empty; }
+ class D extends S { update(u: ViewUpdate): void { this.s = get(u.state); } }
+ const decorations = (d: D): DecorationSet => d.s;
+ return enables.concat(ViewPlugin.fromClass(D, { decorations }));
+}
+
+// A Gutter is an extension that adds decorations (bullets or any kind of
+// symbol) in a gutter in front of document's lines. See the CodeMirror's
+// documentation on GutterMarker for further details.
+export function createGutter<I extends Dict>(
+ deps: Dependencies<I>,
+ className: string,
+ line: (inputs: I, block: Range, view: EditorView) => GutterMarker | null
+): Extension {
+ const enables = mapDeps(deps, (d) => d.extension);
+ const extension = gutter({
+ class: className,
+ lineMarkerChange: (u) => existsDeps(deps, (d) => d.isUpdated(u)),
+ lineMarker: (view, block) => {
+ return line(inputs(deps, view.state) as I, block, view);
+ }
+ });
+ return enables.concat(extension);
+}
+
+// A Tooltip is an extension that adds decorations as a floating DOM element
+// above or below some text. See the CodeMirror's documentation on Tooltip
+// for further details.
+export function createTooltip<I extends Dict>(
+ deps: Dependencies<I>,
+ fn: (input: I) => Tooltip | Tooltip[] | undefined,
+): Extension {
+ const { structure, extension } = createAspect(deps, fn);
+ const show = showTooltip.computeN([structure], st => {
+ const tip = st.facet(structure);
+ if (tip === undefined) return [null];
+ if ('length' in tip) return tip;
+ return [tip];
+ });
+ return [extension, show];
+}
+
+// An Event Handler is an extention responsible of performing a computation each
+// time a DOM event (like <mouseup> or <contextmenu>) happens.
+export function createEventHandler<I extends Dict>(
+ deps: Dependencies<I>,
+ handlers: Handlers<I>,
+): Extension {
+ const enables = mapDeps(deps, (d) => d.extension);
+ const domEventHandlers = Object.fromEntries(Object.keys(handlers).map((k) => {
+ const h = handlers[k] as Handler<I, typeof k>;
+ const fn = (e: typeof k, v: EditorView): void =>
+ h(inputs(deps, v.state) as I, v, e);
+ return [k, fn];
+ }));
+ return enables.concat(EditorView.domEventHandlers(domEventHandlers));
+}
+
+// A View updater is an extension that allows to modify the view each time a
+// depencency is updated. For example, one could use this to change the cursor
+// position when a Data is updated by the outside world.
+export function createViewUpdater<I extends Dict>(
+ deps: Dependencies<I>,
+ fn: (input: I, view: View) => void,
+): Extension {
+ const enables = mapDeps(deps, (d) => d.extension);
+ const listener = EditorView.updateListener.of((u) => {
+ if(!existsDeps(deps, (d) => d.isUpdated(u))) return;
+ const get = (b: boolean): EditorState => b ? u.state : u.startState;
+ const state: <X>(d: Dep<X>) => EditorState = (d) => get(d.isUpdated(u));
+ const inputs = transformDeps(deps, (d) => d.get(state(d))) as I;
+ fn(inputs, u.view);
+ });
+ return enables.concat(listener);
+}
+
+// -----------------------------------------------------------------------------
+
+
+
+// -----------------------------------------------------------------------------
+// Code highlighting and parsing
+// -----------------------------------------------------------------------------
+
+// Plugin specifying how to highlight the code. The theme is handled by the CSS.
+const Highlight = Language.syntaxHighlighting(Language.HighlightStyle.define([
+ { tag: tags.comment, class: 'cm-comment' },
+ { tag: tags.typeName, class: 'cm-type' },
+ { tag: tags.number, class: 'cm-number' },
+ { tag: tags.controlKeyword, class: 'cm-keyword' },
+ { tag: tags.definition(tags.variableName) , class: 'cm-def' },
+]));
+
+// A language provider based on the [Lezer C++ parser], extended with
+// highlighting and folding information. Only comments can be folded.
+// (Source: https://github.com/lezer-parser/cpp)
+const comment = (t: SyntaxNode): Range => ({ from: t.from + 2, to: t.to - 2});
+const folder = Language.foldNodeProp.add({ BlockComment: comment });
+const stringPrefixes = [ "L", "u", "U", "u8", "LR", "UR", "uR", "u8R", "R" ];
+const cppLanguage = Language.LRLanguage.define({
+ parser: parser.configure({ props: [ folder ] }),
+ languageData: {
+ commentTokens: { line: "//", block: { open: "/*", close: "*/" } },
+ indentOnInput: /^\s*(?:case |default:|\{|\})$/,
+ closeBrackets: { stringPrefixes },
+ }
+});
+
+// This extension enables all the language highlighting features.
+export const LanguageHighlighter: Extension =
+ [Highlight, new Language.LanguageSupport(cppLanguage)];
+
+// -----------------------------------------------------------------------------
+
+
+
+// -----------------------------------------------------------------------------
+// Standard extensions and commands
+// -----------------------------------------------------------------------------
+
+export const Selection = createSelectionField();
+function createSelectionField(): Field<EditorSelection> {
+ const cursor = EditorSelection.cursor(0);
+ const field = createField<EditorSelection>(EditorSelection.create([cursor]));
+ const set: Set<EditorSelection> = (view, selection) => {
+ view?.dispatch({ selection });
+ field.set(view, selection);
+ };
+ const updater = EditorView.updateListener.of((update) => {
+ if (update.selectionSet) field.set(update.view, update.state.selection);
+ });
+ return { ...field, set, extension: [field.extension, updater] };
+}
+
+export const Document = createDocumentField();
+function createDocumentField(): Field<Text> {
+ const field = createField<Text>(Text.empty);
+ const set: Set<Text> = (view, text) => {
+ const selection = { anchor: 0 };
+ const length = view?.state.doc.length;
+ const changes = { from: 0, to: length, insert: text };
+ view?.dispatch({ changes, selection });
+ field.set(view, text);
+ };
+ const updater = EditorView.updateListener.of((update) => {
+ if (update.docChanged) field.set(update.view, update.state.doc);
+ });
+ return { ...field, set, extension: [field.extension, updater] };
+}
+
+// Create a text field that updates the CodeMirror document when set.
+export type ToString<A> = (text: A) => string;
+export function createTextField<A>(init: A, toString: ToString<A>): Field<A> {
+ const field = createField<A>(init);
+ const set: Set<A> = (view, text) => {
+ const selection = { anchor: 0 };
+ const length = view?.state.doc.length;
+ const changes = { from: 0, to: length, insert: toString(text) };
+ view?.dispatch({ changes, selection });
+ field.set(view, text);
+ };
+ return { ...field, set };
+}
+
+// An extension displaying line numbers in a gutter. Does not display anything
+// if the document is empty.
+export const LineNumbers = createLineNumbers();
+function createLineNumbers(): Extension {
+ return lineNumbers({
+ formatNumber: (lineNo, state) => {
+ if (state.doc.length === 0) return '';
+ return lineNo.toString();
+ }
+ });
+}
+
+// An extension highlighting the active line.
+export const HighlightActiveLine = createHighlightActiveLine();
+function createHighlightActiveLine(): Extension {
+ const highlight = Decoration.line({ class: 'cm-active-line' });
+ return createDecorator({}, (_, state) => {
+ if (state.doc.length === 0) return RangeSet.empty;
+ const { from } = state.doc.lineAt(state.selection.main.from);
+ const deco = highlight.range(from, from);
+ return RangeSet.of(deco);
+ });
+}
+
+// An extension handling the folding of foldable nodes. For exemple, If used
+// with the language highlighter defined above, it will provides interactions
+// to fold comments only.
+export const FoldGutter = createFoldGutter();
+function createFoldGutter(): Extension {
+ return Language.foldGutter();
+}
+
+// Folds all the foldable nodes of the given view.
+export function foldAll(view: View): void {
+ if (view !== null) Language.foldAll(view);
+}
+
+// Unfolds all the foldable nodes of the given view.
+export function unfoldAll(view: View): void {
+ if (view !== null) Language.unfoldAll(view);
+}
+
+// Move to the given line. The indexation starts at 1.
+export function selectLine(view: View, line: number, atTop: boolean): void {
+ if (!view || view.state.doc.lines < line) return;
+ const doc = view.state.doc;
+ const { from: here } = doc.lineAt(view.state.selection.main.from);
+ const { from: goto } = doc.line(Math.max(line, 1));
+ if (here === goto) return;
+ view.dispatch({ selection: { anchor: goto }, scrollIntoView: true });
+ if (!atTop) return;
+ const effects = EditorView.scrollIntoView(goto, { y: 'start', yMargin: 0 });
+ view.dispatch({ effects });
+}
+
+// -----------------------------------------------------------------------------
+
+
+
+// -----------------------------------------------------------------------------
+// Editor component
+// -----------------------------------------------------------------------------
+
+export interface EditorComponentProps { style?: React.CSSProperties }
+export type EditorComponent = (props: EditorComponentProps) => JSX.Element;
+export interface Editor { view: View; Component: EditorComponent }
+
+export function Editor(extensions: Extension[]): Editor {
+ const parent = React.useRef(null);
+ const editor = React.useRef<View>(null);
+ const Component: EditorComponent = React.useCallback((props) => {
+ return <div className='cm-global-box' style={props.style} ref={parent} />;
+ }, [parent]);
+ React.useEffect(() => {
+ if (!parent.current) return;
+ const state = EditorState.create({ extensions });
+ editor.current = new EditorView({ state, parent: parent.current });
+ }, [parent, extensions]);
+ return { view: editor.current, Component };
+}
+
+// -----------------------------------------------------------------------------
diff --git a/ivette/src/dome/renderer/text/style.css b/ivette/src/dome/renderer/text/style.css
index 3dd0c7e07f48e46a4a51589d0fbbfa012e3617ad..d936197776803018537a588dc925c0d07239a09e 100644
--- a/ivette/src/dome/renderer/text/style.css
+++ b/ivette/src/dome/renderer/text/style.css
@@ -106,3 +106,87 @@
}
/* -------------------------------------------------------------------------- */
+/* --- Styling CodeMirror 6 editor --- */
+/* -------------------------------------------------------------------------- */
+
+.cm-global-box {
+ height: 100%;
+ overflow: auto;
+}
+
+.cm-editor {
+ background-color: var(--background-report);
+ color: var(--text);
+ height: 100%;
+ width: 100%;
+ overflow: hidden;
+}
+
+.cm-editor .cm-gutters {
+ border-right: 0px;
+ width: 2.15em;
+ background: var(--background-report);
+}
+
+.cm-editor .cm-gutters .cm-lineNumbers {
+ color: var(--disabled-text);
+}
+
+.cm-property-gutter {
+ width: 1.3em;
+ background: var(--code-bullet);
+}
+
+.cm-hovered-code {
+ background-color: var(--code-hover);
+}
+
+.cm-selected-code {
+ background-color: var(--code-select);
+}
+
+.cm-selected-code:hover {
+ background-color: var(--code-select-hover);
+}
+
+.cm-dead-code {
+ font-style: italic;
+ filter: opacity(0.7);
+}
+
+.cm-non-term-code {
+ font-style: italic;
+ filter: opacity(0.7);
+}
+
+.cm-tainted {
+ text-decoration: underline var(--warning) solid 1px;
+ text-decoration-skip-ink: none;
+ text-underline-position: under;
+}
+
+.cm-tooltip.cm-tainted-tooltip {
+ background-color: var(--background-softer);
+ color: var(--text-highlighted);
+ border: 1px solid var(--background-profound);
+ padding: 2px 7px;
+ border-radius: 4px;
+}
+
+.cm-tooltip-above.cm-tainted-tooltip .cm-tooltip-arrow:before {
+ border-top-color: var(--background-profound);
+}
+
+.cm-tooltip-above.cm-tainted-tooltip .cm-tooltip-arrow:after {
+ border-top-color: var(--background-softer);
+}
+
+.cm-def { color: var(--codemirror-def); }
+.cm-comment { color: var(--codemirror-comment); }
+.cm-type { color: var(--codemirror-type); }
+.cm-number { color: var(--codemirror-number); }
+.cm-keyword { color: var(--codemirror-keyword); }
+
+.cm-active-line { background-color: var(--background); }
+
+/* -------------------------------------------------------------------------- */
diff --git a/ivette/src/frama-c/kernel/ASTinfo.tsx b/ivette/src/frama-c/kernel/ASTinfo.tsx
index 65f9243ea26e3bf825dea2738676bc7f9507ab00..2c3ea9a4b7cf4c769e9682690cc9106c00a1da9d 100644
--- a/ivette/src/frama-c/kernel/ASTinfo.tsx
+++ b/ivette/src/frama-c/kernel/ASTinfo.tsx
@@ -27,6 +27,7 @@
import React from 'react';
import * as Dome from 'dome';
import { classes } from 'dome/misc/utils';
+import * as Server from 'frama-c/server';
import * as States from 'frama-c/states';
import * as DATA from 'frama-c/kernel/api/data';
import * as AST from 'frama-c/kernel/api/ast';
@@ -120,9 +121,9 @@ interface InfoSectionProps {
function MarkInfos(props: InfoSectionProps): JSX.Element {
const [unfold, setUnfold] = React.useState(true);
const [more, setMore] = React.useState(false);
- const { marker, markerInfo } = props;
- const allInfos: ASTinfos[] =
- States.useRequest(AST.getInformation, marker) ?? [];
+ const { marker: m, markerInfo } = props;
+ const req = React.useMemo(() => Server.send(AST.getInformation, m), [m]);
+ const { result: allInfos = [] } = Dome.usePromise(req);
const highlight = classes(
props.selected && 'selected',
props.hovered && 'hovered',
diff --git a/ivette/src/frama-c/kernel/ASTview.tsx b/ivette/src/frama-c/kernel/ASTview.tsx
index 6b6da1e69c78a49b32bdac5293eb5d663be07106..ed3deae15c9816ae754209387501b17526d59f6c 100644
--- a/ivette/src/frama-c/kernel/ASTview.tsx
+++ b/ivette/src/frama-c/kernel/ASTview.tsx
@@ -20,123 +20,341 @@
/* */
/* ************************************************************************ */
-// --------------------------------------------------------------------------
-// --- AST Source Code
-// --------------------------------------------------------------------------
-
import React from 'react';
-import _ from 'lodash';
-import CodeMirror from 'codemirror/lib/codemirror';
+import Lodash from 'lodash';
import * as Dome from 'dome';
-import * as Json from 'dome/data/json';
+import * as Editor from 'dome/text/editor';
+import * as Utils from 'dome/data/arrays';
+import * as Server from 'frama-c/server';
+import * as States from 'frama-c/states';
+import { key } from 'dome/data/json';
import * as Settings from 'dome/data/settings';
-import { TitleBar } from 'ivette';
import { IconButton } from 'dome/controls/buttons';
-import type { key } from 'dome/data/json';
-import { RichTextBuffer } from 'dome/text/buffers';
-import { Text } from 'dome/text/editors';
import { Filler, Inset } from 'dome/frame/toolbars';
-
-import * as Preferences from 'ivette/prefs';
-
-import * as Server from 'frama-c/server';
-import * as States from 'frama-c/states';
-import * as RichText from 'frama-c/richtext';
import * as Ast from 'frama-c/kernel/api/ast';
+import { text } from 'frama-c/kernel/api/data';
+import * as Eva from 'frama-c/plugins/eva/api/general';
import * as Properties from 'frama-c/kernel/api/properties';
-import { getCallers, getDeadCode } from 'frama-c/plugins/eva/api/general';
import { getWritesLval, getReadsLval } from 'frama-c/plugins/studia/api/studia';
-// --------------------------------------------------------------------------
-// --- Pretty Printing (Browser Console)
-// --------------------------------------------------------------------------
-
-const D = new Dome.Debug('AST View');
-
-// --------------------------------------------------------------------------
-// --- Rich Text Printer
-// --------------------------------------------------------------------------
-
-async function loadAST(
- buffer: RichTextBuffer, theFunction?: string, theMarker?: string,
-): Promise<void> {
- buffer.clear();
- if (theFunction) {
- buffer.log('// Loading', theFunction, '…');
- (async () => {
- try {
- const data = await Server.send(Ast.printFunction, theFunction);
- buffer.clear();
- if (!data) {
- buffer.log('// No code for function', theFunction);
- }
- RichText.printTextWithTags(buffer, data);
- if (theMarker)
- buffer.scroll(theMarker);
- } catch (err) {
- D.error(
- `Fail to retrieve the AST of function '${theFunction}' ` +
- `and marker '${theMarker}':`, err,
- );
- }
- })();
- }
+import { TitleBar } from 'ivette';
+import * as Preferences from 'ivette/prefs';
+
+
+
+// -----------------------------------------------------------------------------
+// Utilitary types and functions
+// -----------------------------------------------------------------------------
+
+// An alias type for functions and locations.
+type Fct = string | undefined;
+type Marker = string | undefined;
+
+// A range is just a pair of position in the code.
+type Range = Editor.Range;
+
+// Type checking that an input is defined.
+function isDef<A>(a: A | undefined): a is A { return a !== undefined; }
+
+// Map a function over a list, removing all inputs that returned undefined.
+function mapFilter<A, B>(xs: readonly A[], fn: (x: A) => B | undefined): B[] {
+ return xs.map(fn).filter(isDef);
}
-/* --------------------------------------------------------------------------*/
-/* --- Function Callers ---*/
-/* --------------------------------------------------------------------------*/
+// -----------------------------------------------------------------------------
+
+
-type Caller = { fct: key<'#fct'>, marker: key<'#stmt'> };
+// -----------------------------------------------------------------------------
+// Tree datatype definition and utiliary functions
+// -----------------------------------------------------------------------------
-async function functionCallers(functionName: string): Promise<Caller[]> {
- try {
- const data = await Server.send(getCallers, functionName);
- const locations = data.map(([fct, marker]) => ({ fct, marker }));
- return locations;
- } catch (err) {
- D.error(`Fail to retrieve callers of function '${functionName}':`, err);
- return [];
+// The code is given by the server has a tree but implemented with arrays and
+// without information on the ranges of each element. It will be converted in a
+// good old tree that carry those information.
+interface Leaf extends Range { text: string }
+interface Node extends Range { id: string, children: Tree[] }
+type Tree = Leaf | Node;
+
+// Utility functions on trees.
+function isLeaf (t: Tree): t is Leaf { return 'text' in t; }
+function isNode (t: Tree): t is Node { return 'id' in t && 'children' in t; }
+const empty: Tree = { text: '', from: 0, to: 0 };
+
+// Convert an Ivette text (i.e a function's code) into a Tree, adding range
+// information to each construction.
+function textToTree(t: text): Tree | undefined {
+ function aux(t: text, from: number): [Tree | undefined, number] {
+ if (t === null) return [undefined, from];
+ if (typeof t === 'string') {
+ const to = from + t.length;
+ return [{ text: t, from, to }, to];
+ }
+ if (t.length < 2 || typeof t[0] !== 'string') return [undefined, from];
+ const children: Tree[] = []; let acc = from;
+ for (const child of t.slice(1)) {
+ const [node, to] = aux(child, acc);
+ if (node) children.push(node);
+ acc = to;
+ }
+ return [{ id: t[0], from, to: acc, children }, acc];
}
+ const [res] = aux(t, 0);
+ return res;
}
-/* --------------------------------------------------------------------------*/
-/* --- Studia Access ---*/
-/* --------------------------------------------------------------------------*/
+// Convert an Ivette text into a string to be displayed.
+function textToString(text: text): string {
+ if (Array.isArray(text)) return text.slice(1).map(textToString).join('');
+ else if (typeof text === 'string') return text;
+ else return '';
+}
-type access = 'Reads' | 'Writes';
-interface StudiaInfos {
- name: string,
- title: string,
- locations: { fct: key<'#fct'>, marker: Ast.marker }[],
- index: number,
+// Computes, for each markers of a tree, its range. Returns the map containing
+// all those bindings.
+function markersRanges(tree: Tree): Map<string, Range[]>{
+ const ranges: Map<string, Range[]> = new Map();
+ const toRanges = (tree: Tree): void => {
+ if (!isNode(tree)) return;
+ const trees = ranges.get(tree.id) ?? [];
+ trees.push(tree);
+ ranges.set(tree.id, trees);
+ for (const child of tree.children) toRanges(child);
+ };
+ toRanges(tree);
+ return ranges;
}
-async function studia(
- marker: string,
- info: Ast.markerInfoData,
- kind: access,
-): Promise<StudiaInfos> {
- const request = kind === 'Reads' ? getReadsLval : getWritesLval;
- const data = await Server.send(request, marker);
- const locations = data.direct.map(([f, m]) => ({ fct: f, marker: m }));
- const lval = info.name;
- if (locations.length > 0) {
- const name = `${kind} of ${lval}`;
- const acc = (kind === 'Reads') ? 'accessing' : 'modifying';
- const title =
- `List of statements ${acc} the memory location pointed by ${lval}.`;
- return { name, title, locations, index: 0 };
- }
- const name = `No ${kind.toLowerCase()} of ${lval}`;
- return { name, title: '', locations: [], index: 0 };
+function uniqueRange(m: string, rs: Map<string, Range[]>): Range | undefined {
+ const ranges = rs.get(m);
+ return (ranges && ranges.length > 0) ? ranges[0] : undefined;
+}
+
+// Find the closest covering tagged node of a given position. Returns
+// undefined if there is not relevant covering node.
+function coveringNode(tree: Tree, pos: number): Node | undefined {
+ if (isLeaf(tree)) return undefined;
+ if (pos < tree.from || pos > tree.to) return undefined;
+ const child = Utils.first(tree.children, (c) => coveringNode(c, pos));
+ if (child && isNode(child)) return child;
+ if (tree.from <= pos && pos < tree.to) return tree;
+ return undefined;
+}
+
+// -----------------------------------------------------------------------------
+
+
+
+// -----------------------------------------------------------------------------
+// Function code representation
+// -----------------------------------------------------------------------------
+
+// This field contains the current function's code as represented by Ivette.
+// Its set function takes care to update the CodeMirror displayed document.
+const Text = Editor.createTextField<text>(null, textToString);
+
+// This aspect computes the tree representing the currently displayed function's
+// code, represented by the <Text> field.
+const Tree = Editor.createAspect({ t: Text }, ({t}) => textToTree(t) ?? empty);
+
+// This aspect computes the markers ranges of the currently displayed function's
+// tree, represented by the <Tree> aspect.
+const Ranges = Editor.createAspect({ t: Tree }, ({ t }) => markersRanges(t));
+
+// -----------------------------------------------------------------------------
+
+
+
+// -----------------------------------------------------------------------------
+// Selected marker representation
+// -----------------------------------------------------------------------------
+
+// This field contains the currently selected function.
+const Fct = Editor.createField<Fct>(undefined);
+
+// This field contains the currently selected marker.
+const Marker = Editor.createField<Marker>(undefined);
+
+// The Ivette selection must be updated by CodeMirror plugins. This input
+// add the callback in the CodeMirror internal state.
+type UpdateSelection = (a: States.SelectionActions) => void;
+const UpdateSelection = Editor.createField<UpdateSelection>(() => { return; });
+
+// The marker field is considered as the ground truth on what is selected in the
+// CodeMirror document. To do so, we catch the mouseup event (so when the user
+// select a new part of the document) and update the Ivette selection
+// accordingly. This will update the Marker field during the next Editor
+// component's render and thus update everything else.
+const MarkerUpdater = createMarkerUpdater();
+function createMarkerUpdater(): Editor.Extension {
+ const deps = { fct: Fct, tree: Tree, update: UpdateSelection };
+ return Editor.createEventHandler(deps, {
+ mouseup: ({ fct, tree, update }, view, event) => {
+ const main = view.state.selection.main;
+ const id = coveringNode(tree, main.from)?.id;
+ const location = { fct, marker: Ast.jMarker(id) };
+ update({ location });
+ if (event.altKey) States.MetaSelection.emit(location);
+ }
+ });
+}
+
+// A View updater that scrolls the selected marker into view. It is needed to
+// handle Marker's updates from the outside world, as they do not change the
+// cursor position inside CodeMirror.
+const MarkerScroller = createMarkerScroller();
+function createMarkerScroller(): Editor.Extension {
+ const deps = { marker: Marker, ranges: Ranges };
+ return Editor.createViewUpdater(deps, ({ marker, ranges }, view) => {
+ if (!view || !marker) return;
+ const markerRanges = ranges.get(marker) ?? [];
+ if (markerRanges.length !== 1) return;
+ const { from: anchor } = markerRanges[0];
+ view.dispatch({ selection: { anchor }, scrollIntoView: true });
+ });
+}
+
+// -----------------------------------------------------------------------------
+
+
+
+// -----------------------------------------------------------------------------
+// Hovered marker representation
+// -----------------------------------------------------------------------------
+
+// This field contains the currently hovered marker.
+const Hovered = Editor.createField<Marker>(undefined);
+
+// The Ivette hovered element must be updated by CodeMirror plugins. This
+// field add the callback in the CodeMirror internal state.
+type UpdateHovered = (h: States.Hovered) => void;
+const UpdateHovered = Editor.createField<UpdateHovered>(() => { return ; });
+
+// The Hovered field is updated each time the mouse moves through the CodeMirror
+// document. The handlers updates the Ivette hovered information, which is then
+// reflected on the Hovered field by the Editor component itself.
+const HoveredUpdater = createHoveredUpdater();
+function createHoveredUpdater(): Editor.Extension {
+ const deps = { fct: Fct, tree: Tree, update: UpdateHovered };
+ return Editor.createEventHandler(deps, {
+ mousemove: (inputs, view, event) => {
+ const { fct, tree, update: updateHovered } = inputs;
+ const coords = { x: event.clientX, y: event.clientY };
+ const reset = (): void => updateHovered(undefined);
+ const pos = view.posAtCoords(coords);
+ if (!pos) { reset(); return; }
+ const hov = coveringNode(tree, pos);
+ if (!hov) { reset(); return; }
+ const from = view.coordsAtPos(hov.from);
+ if (!from) { reset(); return; }
+ const to = view.coordsAtPos(hov.to);
+ if (!to) { reset(); return; }
+ const left = Math.min(from.left, to.left);
+ const right = Math.max(from.left, to.left);
+ const top = Math.min(from.top, to.top);
+ const bottom = Math.max(from.bottom, to.bottom);
+ const horizontallyOk = left <= coords.x && coords.x <= right;
+ const verticallyOk = top <= coords.y && coords.y <= bottom;
+ if (!horizontallyOk || !verticallyOk) { reset(); return; }
+ const marker = Ast.jMarker(hov.id);
+ updateHovered(marker ? { fct, marker } : undefined);
+ }
+ });
}
-/* --------------------------------------------------------------------------*/
-/* --- Property Bullets ---*/
-/* --------------------------------------------------------------------------*/
+// -----------------------------------------------------------------------------
+
+
+
+// -----------------------------------------------------------------------------
+// Plugin decorating hovered and selected elements
+// -----------------------------------------------------------------------------
+
+const CodeDecorator = createCodeDecorator();
+function createCodeDecorator(): Editor.Extension {
+ const hoveredClass = Editor.Decoration.mark({ class: 'cm-hovered-code' });
+ const selectedClass = Editor.Decoration.mark({ class: 'cm-selected-code' });
+ const deps = { ranges: Ranges, marker: Marker, hovered: Hovered };
+ return Editor.createDecorator(deps, ({ ranges, marker: m, hovered: h }) => {
+ const hoveredRanges = h ? (ranges.get(h) ?? []) : [];
+ const selectedRanges = m ? (ranges.get(m) ?? []) : [];
+ const hovered = hoveredRanges.map(r => hoveredClass.range(r.from, r.to));
+ const selected = selectedRanges.map(r => selectedClass.range(r.from, r.to));
+ return Editor.RangeSet.of(selected.concat(hovered), true);
+ });
+}
+
+// -----------------------------------------------------------------------------
+
+
+
+// -----------------------------------------------------------------------------
+// Dead code decorations plugin
+// -----------------------------------------------------------------------------
+
+// This field contains the dead code information as inferred by Eva.
+const emptyDeadCode = { unreachable: [], nonTerminating: [] };
+const Dead = Editor.createField<Eva.deadCode>(emptyDeadCode);
+
+const DeadCodeDecorator = createDeadCodeDecorator();
+function createDeadCodeDecorator(): Editor.Extension {
+ const uClass = Editor.Decoration.mark({ class: 'cm-dead-code' });
+ const tClass = Editor.Decoration.mark({ class: 'cm-non-term-code' });
+ const deps = { dead: Dead, ranges: Ranges };
+ return Editor.createDecorator(deps, ({ dead, ranges }) => {
+ const range = (m: string): Range[] | undefined => ranges.get(m);
+ const unreachableRanges = mapFilter(dead.unreachable, range).flat();
+ const unreachable = unreachableRanges.map(r => uClass.range(r.from, r.to));
+ const nonTermRanges = mapFilter(dead.nonTerminating, range).flat();
+ const nonTerm = nonTermRanges.map(r => tClass.range(r.from, r.to));
+ return Editor.RangeSet.of(unreachable.concat(nonTerm), true);
+ });
+}
+// -----------------------------------------------------------------------------
+
+
+
+// -----------------------------------------------------------------------------
+// Property bullets extension
+// -----------------------------------------------------------------------------
+
+// This field contains information on properties' tags.
+type Tags = Map<string, States.Tag>;
+const Tags = Editor.createField<Tags>(new Map());
+
+// The component needs information on markers' status data.
+const PropertiesStatuses = Editor.createField<Properties.statusData[]>([]);
+
+// This aspect filters all properties that does not have a valid range, and
+// stores the remaining properties with their ranges.
+const PropertiesRanges = createPropertiesRange();
+interface PropertyRange extends Properties.statusData { range: Range }
+function createPropertiesRange(): Editor.Aspect<PropertyRange[]> {
+ const deps = { properties: PropertiesStatuses, ranges: Ranges };
+ return Editor.createAspect(deps, ({ properties, ranges }) => {
+ const get = (p: Properties.statusData): Range[] => ranges.get(p.key) ?? [];
+ return properties.map(p => get(p).map(r => ({ ...p, range: r }))).flat();
+ });
+}
+
+// This aspect computes the tag associated to each property.
+const PropertiesTags = createPropertiesTags();
+function createPropertiesTags(): Editor.Aspect<Map<string, States.Tag>> {
+ const deps = { statuses: PropertiesStatuses, tags: Tags };
+ return Editor.createAspect(deps, ({ statuses, tags }) => {
+ const res = new Map<string, States.Tag>();
+ for (const p of statuses) {
+ if (!p.status) continue;
+ const tag = tags.get(p.status);
+ if (tag) res.set(p.key, tag);
+ }
+ return res;
+ });
+}
+
+// Bullet colors.
function getBulletColor(status: States.Tag): string {
switch (status.name) {
case 'unknown': return '#FF8300';
@@ -154,187 +372,302 @@ function getBulletColor(status: States.Tag): string {
}
}
-function makeBullet(status: States.Tag): HTMLDivElement {
- const marker = document.createElement('div');
- marker.style.color = getBulletColor(status);
- marker.style.textAlign = 'center';
- if (status.descr)
- marker.title = status.descr;
- marker.innerHTML = 'â—‰';
- return marker;
+// Property bullet gutter marker.
+class PropertyBullet extends Editor.GutterMarker {
+ readonly bullet: HTMLDivElement;
+ toDOM(): HTMLDivElement { return this.bullet; }
+ constructor(status?: States.Tag) {
+ super();
+ this.bullet = document.createElement('div');
+ this.bullet.innerHTML = 'â—‰';
+ if (status) {
+ this.bullet.style.color = getBulletColor(status);
+ this.bullet.style.textAlign = 'center';
+ if (status.descr) this.bullet.title = status.descr;
+ }
+ }
}
-// --------------------------------------------------------------------------
-// --- AST Printer
-// --------------------------------------------------------------------------
+const PropertiesGutter = createPropertiesGutter();
+function createPropertiesGutter(): Editor.Extension {
+ const deps = { ranges: PropertiesRanges, propTags: PropertiesTags };
+ const cls = 'cm-property-gutter';
+ return Editor.createGutter(deps, cls, (inputs, block, view) => {
+ const { ranges, propTags } = inputs;
+ const line = view.state.doc.lineAt(block.from);
+ const start = line.from; const end = line.to;
+ const inLine = (r: Range): boolean => start <= r.from && r.to <= end;
+ function isHeader(r: Range): boolean {
+ if (!line.text.includes('requires')) return false;
+ const next = view.state.doc.line(line.number + 1);
+ return r.from <= next.from && next.to <= r.to;
+ }
+ const prop = ranges.find((r) => inLine(r.range) || isHeader(r.range));
+ if (!prop) return null;
+ const statusTag = propTags.get(prop.key);
+ return statusTag ? new PropertyBullet(statusTag) : null;
+ });
+}
-export default function ASTview(): JSX.Element {
+// -----------------------------------------------------------------------------
- // Hooks
- const buffer = React.useMemo(() => new RichTextBuffer(), []);
- const printed = React.useRef<string | undefined>();
- const [selection, updateSelection] = States.useSelection();
- const [hoveredLoc] = States.useHovered();
- const multipleSelections = selection?.multiple.allSelections;
- const theFunction = selection?.current?.fct;
- const theMarker = selection?.current?.marker;
- const hovered = hoveredLoc?.marker;
- const [fontSize] = Settings.useGlobalSettings(Preferences.EditorFontSize);
- const markersInfo = States.useSyncArray(Ast.markerInfo);
- const deadCode = States.useRequest(getDeadCode, theFunction);
- const propertyStatus = States.useSyncArray(Properties.status).getArray();
- const statusDict = States.useTags(Properties.propStatusTags);
-
- const setBullets = React.useCallback(() => {
- propertyStatus.forEach((prop) => {
- const status = statusDict.get(prop.status);
- if (theFunction && prop.fct === theFunction && status) {
- const bullet = makeBullet(status);
- const markers = buffer.findTextMarker(prop.key);
- buffer.forEach((cm) => {
- markers.forEach((marker) => {
- const line = marker.find()?.from.line;
- if (line !== undefined) cm.setGutterMarker(line, 'bullet', bullet);
- });
- });
- }
- });
- }, [buffer, theFunction, propertyStatus, statusDict]);
-
- React.useEffect(() => {
- setBullets();
- buffer.on('change', setBullets);
- return () => { buffer.off('change', setBullets); };
- }, [buffer, setBullets]);
-
- const reload = React.useCallback(async () => {
- printed.current = theFunction;
- loadAST(buffer, theFunction, theMarker);
- }, [buffer, theFunction, theMarker]);
-
- // Hook: async loading
- React.useEffect(() => { if (printed.current !== theFunction) reload(); });
-
- // Also reload the buffer when the AST is recomputed.
- React.useEffect(() => {
- Server.onSignal(Ast.changed, reload);
- return () => { Server.offSignal(Ast.changed, reload); };
- });
- React.useEffect(() => {
- const decorator = (marker: string): string | undefined => {
- if (multipleSelections?.some((location) => location?.marker === marker))
- return 'highlighted-marker';
- if (deadCode?.unreachable?.some((m) => m === marker))
- return 'dead-code';
- if (deadCode?.nonTerminating?.some((m) => m === marker))
- return 'non-terminating';
- if (marker === hovered)
- return 'hovered-marker';
- return undefined;
- };
- buffer.setDecorator(decorator);
- }, [buffer, multipleSelections, hovered, deadCode]);
-
- // Hook: marker scrolling
- React.useEffect(() => {
- if (theMarker) buffer.scroll(theMarker);
- }, [buffer, theMarker]);
-
- function onHover(markerId?: string): void {
- const marker = Json.jOption(Ast.jMarker)(markerId);
- const fct = selection?.current?.fct;
- States.setHovered(marker ? { fct, marker } : undefined);
- }
+// -----------------------------------------------------------------------------
+// Studia access
+// -----------------------------------------------------------------------------
+
+type access = 'Reads' | 'Writes';
+
+interface StudiaProps {
+ marker: string,
+ info: Ast.markerInfoData,
+ kind: access,
+}
- function onSelection(markerId: string, meta = false): void {
- const fct = selection?.current?.fct;
- const location = { fct, marker: Ast.jMarker(markerId) };
- updateSelection({ location });
- if (meta) States.MetaSelection.emit(location);
+interface StudiaInfos {
+ name: string,
+ title: string,
+ locations: { fct: key<'#fct'>, marker: Ast.marker }[],
+ index: number,
+}
+
+async function studia(props: StudiaProps): Promise<StudiaInfos> {
+ const { marker, info, kind } = props;
+ const request = kind === 'Reads' ? getReadsLval : getWritesLval;
+ const data = await Server.send(request, marker);
+ const locations = data.direct.map(([f, m]) => ({ fct: f, marker: m }));
+ const lval = info.name;
+ if (locations.length > 0) {
+ const name = `${kind} of ${lval}`;
+ const acc = (kind === 'Reads') ? 'accessing' : 'modifying';
+ const title =
+ `List of statements ${acc} the memory location pointed by ${lval}.`;
+ return { name, title, locations, index: 0 };
}
+ const name = `No ${kind.toLowerCase()} of ${lval}`;
+ return { name, title: '', locations: [], index: 0 };
+}
- async function onContextMenu(markerId: string): Promise<void> {
- const items = [];
- const selectedMarkerInfo = markersInfo.getData(markerId);
- if (selectedMarkerInfo?.var === 'function') {
- if (selectedMarkerInfo.kind === 'declaration') {
- const name = selectedMarkerInfo?.name;
- if (name) {
- const locations = await functionCallers(name);
- const locationsByFunction = _.groupBy(locations, (e) => e.fct);
- _.forEach(locationsByFunction,
- (e) => {
- const callerName = e[0].fct;
- items.push({
- label:
- `Go to caller ${callerName} ` +
- `${e.length > 1 ? `(${e.length} call sites)` : ''}`,
- onClick: () => updateSelection({
- name: `Call sites of function ${name}`,
- locations,
- index: locations.findIndex((l) => l.fct === callerName),
- }),
- });
+// -----------------------------------------------------------------------------
+
+
+
+// -----------------------------------------------------------------------------
+// Context menu
+// -----------------------------------------------------------------------------
+
+// This field contains all the current function's callers, as inferred by Eva.
+const Callers = Editor.createField<Eva.CallSite[]>([]);
+
+// This field contains information on markers.
+type GetMarkerData = (key: string) => Ast.markerInfoData | undefined;
+const GetMarkerData = Editor.createField<GetMarkerData>(() => undefined);
+
+const ContextMenuHandler = createContextMenuHandler();
+function createContextMenuHandler(): Editor.Extension {
+ const data = { tree: Tree, callers: Callers };
+ const deps = { ...data, update: UpdateSelection, getData: GetMarkerData };
+ return Editor.createEventHandler(deps, {
+ contextmenu: (inputs, view, event) => {
+ const { tree, callers, update, getData } = inputs;
+ const coords = { x: event.clientX, y: event.clientY };
+ const position = view.posAtCoords(coords); if (!position) return;
+ const node = coveringNode(tree, position);
+ if (!node || !node.id) return;
+ const items: Dome.PopupMenuItem[] = [];
+ const info = getData(node.id);
+ if (info?.var === 'function') {
+ if (info.kind === 'declaration') {
+ const groupedCallers = Lodash.groupBy(callers, e => e.kf);
+ const locations = callers.map((l) => ({ fct: l.kf, marker: l.stmt }));
+ Lodash.forEach(groupedCallers, (e) => {
+ const callerName = e[0].kf;
+ const callSites = e.length > 1 ? `(${e.length} call sites)` : '';
+ items.push({
+ label: `Go to caller ${callerName} ` + callSites,
+ onClick: () => update({
+ name: `Call sites of function ${info.name}`,
+ locations: locations,
+ index: locations.findIndex(l => l.fct === callerName)
+ })
});
+ });
+ } else {
+ const location = { fct: info.name };
+ const onClick = (): void => update({ location });
+ const label = `Go to definition of ${info.name}`;
+ items.push({ label, onClick });
}
- } else {
- items.push({
- label: `Go to definition of ${selectedMarkerInfo.name}`,
- onClick: () => {
- const location = { fct: selectedMarkerInfo.name };
- updateSelection({ location });
- },
- });
}
+ const enabled = info?.kind === 'lvalue' || info?.var === 'variable';
+ const onClick = (kind: access): void => {
+ if (info && node.id)
+ studia({ marker: node.id, info, kind }).then(update);
+ };
+ const reads = 'Studia: select reads';
+ const writes = 'Studia: select writes';
+ items.push({ label: reads, enabled, onClick: () => onClick('Reads') });
+ items.push({ label: writes, enabled, onClick: () => onClick('Writes') });
+ if (items.length > 0) Dome.popupMenu(items);
+ return;
}
- const enabled = selectedMarkerInfo?.kind === 'lvalue'
- || selectedMarkerInfo?.var === 'variable';
- function onClick(kind: access): void {
- if (selectedMarkerInfo)
- studia(
- markerId,
- selectedMarkerInfo,
- kind,
- ).then(updateSelection);
- }
- items.push({
- label: 'Studia: select writes',
- enabled,
- onClick: () => onClick('Writes'),
- });
- items.push({
- label: 'Studia: select reads',
- enabled,
- onClick: () => onClick('Reads'),
- });
- if (items.length > 0)
- Dome.popupMenu(items);
- }
+ });
+}
+
+// -----------------------------------------------------------------------------
- const foldAll = (): void => buffer.forEach(CodeMirror.commands.foldAll);
- const unfoldAll = (): void => buffer.forEach(CodeMirror.commands.unfoldAll);
- const defaultFold = React.useCallback((): void => {
- buffer.forEach((cm) => { CodeMirror.commands.unfoldAll(cm); });
- }, [buffer]);
- React.useEffect(() => {
- buffer.on('change', defaultFold);
- return () => { buffer.off('change', defaultFold); };
+// -----------------------------------------------------------------------------
+// Tainted lvalues
+// -----------------------------------------------------------------------------
+
+type Taints = Eva.LvalueTaints;
+const TaintedLvalues = Editor.createField<Taints[] | undefined>(undefined);
+
+function textOfTaint(taint: Eva.taintStatus): string {
+ switch (taint) {
+ case 'not_computed': return 'The taint has not been computed';
+ case 'error': return 'There was an error during the taint computation';
+ case 'not_applicable': return 'No taint for this lvalue';
+ case 'direct_taint': return 'This lvalue can be affected by an attacker';
+ case 'indirect_taint':
+ return 'This lvalue depends on path conditions that can \
+ be affected by an attacker';
+ case 'not_tainted': return 'This lvalue is safe';
+ }
+ return '';
+}
+
+const TaintedLvaluesDecorator = createTaintedLvaluesDecorator();
+function createTaintedLvaluesDecorator(): Editor.Extension {
+ const mark = Editor.Decoration.mark({ class: 'cm-tainted' });
+ const deps = { ranges: Ranges, tainted: TaintedLvalues };
+ return Editor.createDecorator(deps, ({ ranges, tainted = [] }) => {
+ const find = (t: Taints): Range[] | undefined => ranges.get(t.lval);
+ const taintedRanges = mapFilter(tainted, find).flat();
+ const marks = taintedRanges.map(r => mark.range(r.from, r.to));
+ return Editor.RangeSet.of(marks, true);
});
+}
- const foldOptions: CodeMirror.FoldOptions = {
- rangeFinder: (cm, pos) => {
- const range = CodeMirror.fold.comment(cm, pos);
- /* Allows folding multi-line comments only. */
- if (!range || range.from.line === range.to.line) return undefined;
- return range;
- }
- };
+const TaintTooltip = createTaintTooltip();
+function createTaintTooltip(): Editor.Extension {
+ const deps = { hovered: Hovered, ranges: Ranges, tainted: TaintedLvalues };
+ return Editor.createTooltip(deps, ({ hovered, ranges, tainted }) => {
+ const hoveredTaint = tainted?.find(t => t.lval === hovered);
+ const hoveredNode = hovered && uniqueRange(hovered, ranges);
+ if (!hoveredTaint || !hoveredNode) return undefined;
+ return {
+ pos: hoveredNode.from,
+ above: true,
+ strictSide: true,
+ arrow: true,
+ create: () => {
+ const dom = document.createElement('div');
+ dom.className = 'cm-tainted-tooltip';
+ dom.textContent = textOfTaint(hoveredTaint.taint);
+ return { dom };
+ }
+ };
+ });
+}
+
+// -----------------------------------------------------------------------------
+
+
+
+// -----------------------------------------------------------------------------
+// Server requests
+// -----------------------------------------------------------------------------
+
+// Server request handler returning the given function's text.
+function useFctText(fct: Fct): text {
+ return States.useRequest(Ast.printFunction, fct) ?? null;
+}
+
+// Server request handler returning the given function's dead code information.
+function useFctDead(fct: Fct): Eva.deadCode {
+ const empty = { unreachable: [], nonTerminating: [] };
+ return States.useRequest(Eva.getDeadCode, fct) ?? empty;
+}
+
+// Server request handler returning the given function's callers.
+function useFctCallers(fct: Fct): Eva.CallSite[] {
+ return States.useRequest(Eva.getCallers, fct) ?? [];
+}
+
+// Server request handler returning the tainted lvalues.
+function useFctTaints(fct: Fct): Eva.LvalueTaints[] {
+ return States.useRequest(Eva.taintedLvalues, fct, { onError: [] }) ?? [];
+}
+
+// -----------------------------------------------------------------------------
+
+
+
+// -----------------------------------------------------------------------------
+// AST View component
+// -----------------------------------------------------------------------------
+
+// Necessary extensions for our needs.
+const extensions: Editor.Extension[] = [
+ MarkerUpdater,
+ MarkerScroller,
+ HoveredUpdater,
+ CodeDecorator,
+ DeadCodeDecorator,
+ ContextMenuHandler,
+ PropertiesGutter,
+ TaintedLvaluesDecorator,
+ TaintTooltip,
+ Editor.FoldGutter,
+ Editor.LanguageHighlighter,
+];
+
+// The component in itself.
+export default function ASTview(): JSX.Element {
+ const [fontSize] = Settings.useGlobalSettings(Preferences.EditorFontSize);
+ const { view, Component } = Editor.Editor(extensions);
+
+ // Updating CodeMirror when the selection or its callback are changed.
+ const [selection, setSel] = States.useSelection();
+ React.useEffect(() => UpdateSelection.set(view, setSel), [view, setSel]);
+ const fct = selection?.current?.fct;
+ React.useEffect(() => Fct.set(view, fct), [view, fct]);
+ const marker = selection?.current?.marker;
+ React.useEffect(() => Marker.set(view, marker), [view, marker]);
+
+ // Updating CodeMirror when the <updateHovered> callback is changed.
+ const [hov, setHov] = States.useHovered();
+ React.useEffect(() => UpdateHovered.set(view, setHov), [view, setHov]);
+ React.useEffect(() => Hovered.set(view, hov?.marker ?? ''), [view, hov]);
+
+ // Updating CodeMirror when the <properties> synchronized array is changed.
+ const props = States.useSyncArray(Properties.status).getArray();
+ React.useEffect(() => PropertiesStatuses.set(view, props), [view, props]);
+
+ // Updating CodeMirror when the <propStatusTags> map is changed.
+ const tags = States.useTags(Properties.propStatusTags);
+ React.useEffect(() => Tags.set(view, tags), [view, tags]);
+
+ // Updating CodeMirror when the <markersInfo> synchronized array is changed.
+ const info = States.useSyncArray(Ast.markerInfo);
+ const getData = React.useCallback((key) => info.getData(key), [info]);
+ React.useEffect(() => GetMarkerData.set(view, getData), [view, getData]);
+
+ // Retrieving data on currently selected function and updating CodeMirror when
+ // they have changed.
+ const text = useFctText(fct);
+ React.useEffect(() => Text.set(view, text), [view, text]);
+ const dead = useFctDead(fct);
+ React.useEffect(() => Dead.set(view, dead), [view, dead]);
+ const callers = useFctCallers(fct);
+ React.useEffect(() => Callers.set(view, callers), [view, callers]);
+ const taints = useFctTaints(fct);
+ React.useEffect(() => TaintedLvalues.set(view, taints), [view, taints]);
- // Component
return (
<>
<TitleBar>
@@ -342,35 +675,22 @@ export default function ASTview(): JSX.Element {
<IconButton
icon='CHEVRON.CONTRACT'
visible={true}
- onClick={foldAll}
+ onClick={() => Editor.foldAll(view)}
title='Collapse all multi-line ACSL properties'
className="titlebar-thin-icon"
/>
<IconButton
icon='CHEVRON.EXPAND'
visible={true}
- onClick={unfoldAll}
+ onClick={() => Editor.unfoldAll(view)}
title='Expand all multi-line ACSL properties'
className="titlebar-thin-icon"
/>
<Inset />
</TitleBar>
- <Text
- buffer={buffer}
- mode="text/x-csrc"
- fontSize={fontSize}
- selection={theMarker}
- onHover={onHover}
- onSelection={onSelection}
- onContextMenu={onContextMenu}
- foldGutter={true}
- foldOptions={foldOptions}
- gutters={['bullet', 'CodeMirror-foldgutter']}
- readOnly
- />
+ <Component style={{ fontSize: `${fontSize}px`}} />
</>
);
-
}
-// --------------------------------------------------------------------------
+// -----------------------------------------------------------------------------
diff --git a/ivette/src/frama-c/kernel/SourceCode.tsx b/ivette/src/frama-c/kernel/SourceCode.tsx
index fb932f8c0192ad9bfc62941c940f9c713da12dc8..1d06325a0be9f5a492d2c8da59ee91d9e52d24c9 100644
--- a/ivette/src/frama-c/kernel/SourceCode.tsx
+++ b/ivette/src/frama-c/kernel/SourceCode.tsx
@@ -20,195 +20,268 @@
/* */
/* ************************************************************************ */
-// --------------------------------------------------------------------------
-// --- Source Code
-// --------------------------------------------------------------------------
-
import React from 'react';
-import * as Server from 'frama-c/server';
-import * as States from 'frama-c/states';
+import * as Path from 'path';
import * as Dome from 'dome';
import * as System from 'dome/system';
-import { RichTextBuffer } from 'dome/text/buffers';
-import { Text } from 'dome/text/editors';
-import { TitleBar } from 'ivette';
-import * as Preferences from 'ivette/prefs';
-import { functions, markerInfo, getMarkerAt } from 'frama-c/kernel/api/ast';
-import { Code } from 'dome/controls/labels';
-import { Hfill } from 'dome/layout/boxes';
-import { IconButton } from 'dome/controls/buttons';
-import * as Path from 'path';
+import * as Boxes from 'dome/layout/boxes';
+import * as Editor from 'dome/text/editor';
+import * as Labels from 'dome/controls/labels';
import * as Settings from 'dome/data/settings';
+import * as Buttons from 'dome/controls/buttons';
+
+import { Selection, Document } from 'dome/text/editor';
+
+import * as Server from 'frama-c/server';
+import * as States from 'frama-c/states';
import * as Status from 'frama-c/kernel/Status';
+import * as Ast from 'frama-c/kernel/api/ast';
-import CodeMirror from 'codemirror/lib/codemirror';
-import 'codemirror/addon/selection/active-line';
-import 'codemirror/addon/dialog/dialog.css';
-import 'codemirror/addon/search/search';
-import 'codemirror/addon/search/searchcursor';
+import * as Ivette from 'ivette';
+import * as Preferences from 'ivette/prefs';
-// --------------------------------------------------------------------------
-// --- Pretty Printing (Browser Console)
-// --------------------------------------------------------------------------
-const D = new Dome.Debug('Source Code');
-// --------------------------------------------------------------------------
-// --- Source Code Printer
-// --------------------------------------------------------------------------
+// -----------------------------------------------------------------------------
+// Utilitary types and functions
+// -----------------------------------------------------------------------------
-// The SourceCode component, producing the GUI part showing the source code
-// corresponding to the selected function.
-export default function SourceCode(): JSX.Element {
+// Recovering the cursor position as a line and a column.
+interface Position { line: number, column: number }
+function getCursorPosition(view: Editor.View): Position {
+ const pos = view?.state.selection.main;
+ if (!view || !pos) return { line: 1, column: 1 };
+ const line = view.state.doc.lineAt(pos.from).number;
+ const column = (pos.goalColumn ?? 0) + 1;
+ return { line, column };
+}
+
+// Error messages.
+function setError(text: string): void {
+ Status.setMessage({ text, kind: 'error' });
+}
+
+// Function launching the external editor at the currently selected position.
+async function edit(file: string, pos: Position, cmd: string): Promise<void> {
+ if (file === '') return;
+ const args = cmd
+ .replace('%s', file)
+ .replace('%n', pos.line.toString())
+ .replace('%c', pos.column.toString())
+ .split(' ');
+ const prog = args.shift(); if (!prog) return;
+ const text = `An error has occured when opening the external editor ${prog}`;
+ System.spawn(prog, args).catch(() => setError(text));
+}
+
+// -----------------------------------------------------------------------------
+
+
+
+// -----------------------------------------------------------------------------
+// Fields declarations
+// -----------------------------------------------------------------------------
+
+// The Ivette selection must be updated by the CodeMirror plugin. This field
+// adds the callback in the CodeMirror internal state.
+type UpdateSelection = (a: States.SelectionActions) => void;
+const UpdateSelection = Editor.createField<UpdateSelection>(() => { return; });
+
+// Those fields contain the source code and the file name.
+const Source = Editor.createTextField<string>('', (s) => s);
+const File = Editor.createField<string>('');
+
+// This field contains the command use to start the external editor.
+const Command = Editor.createField<string>('');
+
+// These field contains a callback that returns the source of a location.
+type GetSource = (loc: States.Location) => Ast.source | undefined;
+const GetSource = Editor.createField<GetSource>(() => undefined);
+
+// We keep track of the cursor location (i.e the location that is under the
+// current CodeMirror cursor) and the ivette location (i.e the locations as
+// seen by the outside world). Keeping track of both of them together force
+// their update in one dispatch, which prevents strange bugs.
+interface Locations { cursor?: States.Location, ivette: States.Location }
+
+// The Locations field. When given Locations, it will update the cursor field if
+// and only if the new cursor location is not undefined. It simplifies the
+// update in the SourceCode component itself.
+const Locations = createLocationsField();
+function createLocationsField(): Editor.Field<Locations> {
+ const noField = { cursor: undefined, ivette: {} };
+ const field = Editor.createField<Locations>(noField);
+ const set: Editor.Set<Locations> = (view, toBe) => {
+ const hasBeen = field.get(view?.state);
+ const cursor = toBe.cursor ?? hasBeen.cursor;
+ field.set(view, { cursor, ivette: toBe.ivette });
+ };
+ return { ...field, set };
+}
+
+// -----------------------------------------------------------------------------
- // Hooks
- const [buffer] = React.useState(() => new RichTextBuffer());
- const [selection, updateSelection] = States.useSelection();
- const theFunction = selection?.current?.fct;
- const theMarker = selection?.current?.marker;
- const markersInfo = States.useSyncArray(markerInfo);
- const functionsData = States.useSyncArray(functions).getArray();
-
- // Retrieving the file name and the line number from the selection and the
- // synchronized tables.
- const sloc =
- (theMarker && markersInfo.getData(theMarker)?.sloc) ??
- (theFunction && functionsData.find((e) => e.name === theFunction)?.sloc);
- const file = sloc ? sloc.file : '';
- const line = sloc ? sloc.line : 0;
- const filename = Path.parse(file).base;
- // Global Font Size
- const [fontSize] = Settings.useGlobalSettings(Preferences.EditorFontSize);
- // Updating the buffer content.
- const text = React.useMemo(async () => {
- const onError = (): string => {
- if (file)
- D.error(`Fail to load source code file ${file}`);
- return '';
- };
- return System.readFile(file).catch(onError);
- }, [file]);
- const { result } = Dome.usePromise(text);
- React.useEffect(() => buffer.setValue(result), [buffer, result]);
-
- /* Last location selected by a click in the source code. */
- const selected: React.MutableRefObject<undefined | States.Location> =
- React.useRef();
-
- /* Updates the cursor position according to the current [selection], except
- when the [selection] is changed according to a click in the source code,
- in which case the cursor should stay exactly where the user clicked. */
- React.useEffect(() => {
- if (selected.current && selected?.current === selection?.current)
- selected.current = undefined;
- else
- buffer.setCursorOnTop(line);
- }, [buffer, selection, line, result]);
-
- /* CodeMirror types used to bind callbacks to extraKeys. */
- type position = CodeMirror.Position;
- type editor = CodeMirror.Editor;
-
- const selectCallback = React.useCallback(
- async function select(editor: editor, event: MouseEvent) {
- const pos = editor.coordsChar({ left: event.x, top: event.y });
- if (file === '' || !pos) return;
- const arg = [file, pos.line + 1, pos.ch + 1];
- Server
- .send(getMarkerAt, arg)
- .then(([fct, marker]) => {
- if (fct || marker) {
- const location = { fct, marker } as States.Location;
- selected.current = location;
- updateSelection({ location });
- }
- })
- .catch((err) => {
- D.error(`Failed to get marker from source file position: ${err}`);
- Status.setMessage({
- text: 'Failed request to Frama-C server',
- kind: 'error',
- });
- });
+// -----------------------------------------------------------------------------
+// Synchronisation with the outside world
+// -----------------------------------------------------------------------------
+
+// Update the outside world when the user click somewhere in the source code.
+const SyncOnUserSelection = createSyncOnUserSelection();
+function createSyncOnUserSelection(): Editor.Extension {
+ const actions = { cmd: Command, update: UpdateSelection };
+ const deps = { file: File, selection: Selection, doc: Document, ...actions };
+ return Editor.createEventHandler(deps, {
+ mouseup: async ({ file, cmd, update }, view, event) => {
+ if (!view || file === '') return;
+ const pos = getCursorPosition(view);
+ const cursor = [file, pos.line, pos.column];
+ try {
+ const [fct, marker] = await Server.send(Ast.getMarkerAt, cursor);
+ if (fct || marker) {
+ // The forced reload should NOT be necessary but... It is...
+ await Server.send(Ast.reloadMarkerInfo, null);
+ const location = { fct, marker };
+ update({ location });
+ Locations.set(view, { cursor: location, ivette: location });
+ }
+ } catch {
+ setError('Failure');
+ }
+ if (event.ctrlKey) edit(file, pos, cmd);
+ }
+ });
+}
+
+// Update the cursor position when the outside world changes the selected
+// location.
+const SyncOnOutsideSelection = createSyncOnOutsideSelection();
+function createSyncOnOutsideSelection(): Editor.Extension {
+ const deps = { locations: Locations, get: GetSource };
+ return Editor.createViewUpdater(deps, ({ locations, get }, view) => {
+ const { cursor, ivette } = locations;
+ if (ivette === undefined || ivette === cursor) return;
+ const source = get(ivette); if (!source) return;
+ const newFct = ivette.fct !== cursor?.fct && ivette.marker === undefined;
+ const onTop = cursor === undefined || newFct;
+ Locations.set(view, { cursor: ivette, ivette });
+ Editor.selectLine(view, source.line, onTop);
+ });
+}
+
+// -----------------------------------------------------------------------------
+
+
+
+// -----------------------------------------------------------------------------
+// Context menu
+// -----------------------------------------------------------------------------
+
+// This events handler takes care of the context menu.
+const ContextMenu = createContextMenu();
+function createContextMenu(): Editor.Extension {
+ const deps = { file: File, command: Command, update: UpdateSelection };
+ return Editor.createEventHandler(deps, {
+ contextmenu: ({ file, command }, view) => {
+ if (file === '') return;
+ const label = 'Open file in an external editor';
+ const pos = getCursorPosition(view);
+ Dome.popupMenu([ { label, onClick: () => edit(file, pos, command) } ]);
},
- [file, updateSelection],
- );
+ });
+}
- React.useEffect(() => {
- buffer.forEach((cm) => cm.on('mousedown', selectCallback));
- return () => buffer.forEach((cm) => cm.off('mousedown', selectCallback));
- }, [buffer, selectCallback]);
+// -----------------------------------------------------------------------------
+
+
+// -----------------------------------------------------------------------------
+// Server requests
+// -----------------------------------------------------------------------------
+
+// Server request handler returning the source code.
+function useFctSource(file: string): string {
+ const req = React.useMemo(() => System.readFile(file), [file]);
+ const { result } = Dome.usePromise(req);
+ return result ?? '';
+}
+
+// Build a callback that retrieves a location's source information.
+function useSourceGetter(): GetSource {
+ const markersInfo = States.useSyncArray(Ast.markerInfo);
+ const functionsData = States.useSyncArray(Ast.functions).getArray();
+ return React.useCallback(({ fct, marker }) => {
+ const markerSloc = (marker !== undefined && marker !== '') ?
+ markersInfo.getData(marker)?.sloc : undefined;
+ const fctSloc = (fct !== undefined && fct !== '') ?
+ functionsData.find((e) => e.name === fct)?.sloc : undefined;
+ return markerSloc ?? fctSloc;
+ }, [markersInfo, functionsData]);
+}
+
+// -----------------------------------------------------------------------------
+
+
+
+// -----------------------------------------------------------------------------
+// Source Code component
+// -----------------------------------------------------------------------------
+
+// Necessary extensions.
+const extensions: Editor.Extension[] = [
+ Source,
+ Editor.Selection,
+ Editor.LineNumbers,
+ Editor.LanguageHighlighter,
+ Editor.HighlightActiveLine,
+ SyncOnUserSelection,
+ SyncOnOutsideSelection,
+ ContextMenu,
+ Locations.structure,
+];
+
+// The component in itself.
+export default function SourceCode(): JSX.Element {
+ const [fontSize] = Settings.useGlobalSettings(Preferences.EditorFontSize);
const [command] = Settings.useGlobalSettings(Preferences.EditorCommand);
- async function launchEditor(_?: editor, pos?: position): Promise<void> {
- if (file !== '') {
- const selectedLine = pos ? (pos.line + 1).toString() : '1';
- const selectedChar = pos ? (pos.ch + 1).toString() : '1';
- const cmd = command
- .replace('%s', file)
- .replace('%n', selectedLine)
- .replace('%c', selectedChar);
- const args = cmd.split(' ');
- const prog = args.shift();
- if (prog) System.spawn(prog, args).catch(() => {
- Status.setMessage({
- text: `An error has occured when opening the external editor ${prog}`,
- kind: 'error',
- });
- });
- }
- }
-
- async function contextMenu(editor?: editor, pos?: position): Promise<void> {
- if (file !== '') {
- const items = [
- {
- label: 'Open file in an external editor',
- onClick: () => launchEditor(editor, pos),
- },
- ];
- Dome.popupMenu(items);
- }
- }
+ const { view, Component } = Editor.Editor(extensions);
+ const [selection, update] = States.useSelection();
+ const loc = React.useMemo(() => selection?.current ?? {}, [selection]);
+ const getSource = useSourceGetter();
+ const file = getSource(loc)?.file ?? '';
+ const filename = Path.parse(file).base;
+ const pos = getCursorPosition(view);
+ const source = useFctSource(file);
+
+ React.useEffect(() => UpdateSelection.set(view, update), [view, update]);
+ React.useEffect(() => GetSource.set(view, getSource), [view, getSource]);
+ React.useEffect(() => File.set(view, file), [view, file]);
+ React.useEffect(() => Source.set(view, source), [view, source]);
+ React.useEffect(() => Command.set(view, command), [view, command]);
+ React.useEffect(() => Locations.set(view, { ivette: loc }), [view, loc]);
const externalEditorTitle =
'Open the source file in an external editor.\nA Ctrl-click '
+ 'in the source code opens the editor at the selected location.'
+ '\nThe editor used can be configured in Ivette settings.';
- // Building the React component.
return (
<>
- <TitleBar>
- <IconButton
+ <Ivette.TitleBar>
+ <Buttons.IconButton
icon="DUPLICATE"
visible={file !== ''}
- onClick={launchEditor}
+ onClick={() => edit(file, pos, command)}
title={externalEditorTitle}
/>
- <Code title={file}>{filename}</Code>
- <Hfill />
- </TitleBar>
- <Text
- buffer={buffer}
- mode="text/x-csrc"
- fontSize={fontSize}
- selection={theMarker}
- lineNumbers={!!theFunction}
- styleActiveLine={!!theFunction}
- extraKeys={{
- 'Alt-F': 'findPersistent',
- 'Ctrl-LeftClick': launchEditor as (_: CodeMirror.Editor) => void,
- RightClick: contextMenu as (_: CodeMirror.Editor) => void,
- }}
- readOnly
- />
+ <Labels.Code title={file}>{filename}</Labels.Code>
+ <Boxes.Hfill />
+ </Ivette.TitleBar>
+ <Component style={{ fontSize: `${fontSize}px` }} />
</>
);
-
}
-// --------------------------------------------------------------------------
+// -----------------------------------------------------------------------------
diff --git a/ivette/src/frama-c/plugins/eva/api/general/index.ts b/ivette/src/frama-c/plugins/eva/api/general/index.ts
index 7bb38314aadfb773fab25c3cdf94d51abc488ffb..85c3985681b3c6821a2e683ada03a648b4a860a8 100644
--- a/ivette/src/frama-c/plugins/eva/api/general/index.ts
+++ b/ivette/src/frama-c/plugins/eva/api/general/index.ts
@@ -94,25 +94,38 @@ const computationState_internal: State.Value<computationStateType> = {
/** The current computation state of the analysis. */
export const computationState: State.Value<computationStateType> = computationState_internal;
-const getCallers_internal: Server.GetRequest<
- Json.key<'#fct'>,
- [ Json.key<'#fct'>, Json.key<'#stmt'> ][]
- > = {
+/** CallSite */
+export interface CallSite {
+ /** Function */
+ kf: Json.key<'#fct'>;
+ /** Statement */
+ stmt: Json.key<'#stmt'>;
+}
+
+/** Decoder for `CallSite` */
+export const jCallSite: Json.Decoder<CallSite> =
+ Json.jObject({
+ kf: Json.jKey<'#fct'>('#fct'),
+ stmt: Json.jKey<'#stmt'>('#stmt'),
+ });
+
+/** Natural order for `CallSite` */
+export const byCallSite: Compare.Order<CallSite> =
+ Compare.byFields
+ <{ kf: Json.key<'#fct'>, stmt: Json.key<'#stmt'> }>({
+ kf: Compare.string,
+ stmt: Compare.string,
+ });
+
+const getCallers_internal: Server.GetRequest<Json.key<'#fct'>,CallSite[]> = {
kind: Server.RqKind.GET,
name: 'plugins.eva.general.getCallers',
input: Json.jKey<'#fct'>('#fct'),
- output: Json.jArray(
- Json.jPair(
- Json.jKey<'#fct'>('#fct'),
- Json.jKey<'#stmt'>('#stmt'),
- )),
+ output: Json.jArray(jCallSite),
signals: [],
};
/** Get the list of call site of a function */
-export const getCallers: Server.GetRequest<
- Json.key<'#fct'>,
- [ Json.key<'#fct'>, Json.key<'#stmt'> ][]
- >= getCallers_internal;
+export const getCallers: Server.GetRequest<Json.key<'#fct'>,CallSite[]>= getCallers_internal;
/** Data for array rows [`functions`](#functions) */
export interface functionsData {
@@ -257,6 +270,42 @@ const taintStatusTags_internal: Server.GetRequest<null,tag[]> = {
/** Registered tags for the above type. */
export const taintStatusTags: Server.GetRequest<null,tag[]>= taintStatusTags_internal;
+/** Lvalue taint status */
+export interface LvalueTaints {
+ /** tainted lvalue */
+ lval: Json.key<'#lval'>;
+ /** taint status */
+ taint: taintStatus;
+}
+
+/** Decoder for `LvalueTaints` */
+export const jLvalueTaints: Json.Decoder<LvalueTaints> =
+ Json.jObject({ lval: Json.jKey<'#lval'>('#lval'), taint: jTaintStatus,});
+
+/** Natural order for `LvalueTaints` */
+export const byLvalueTaints: Compare.Order<LvalueTaints> =
+ Compare.byFields
+ <{ lval: Json.key<'#lval'>, taint: taintStatus }>({
+ lval: Compare.string,
+ taint: byTaintStatus,
+ });
+
+const taintedLvalues_internal: Server.GetRequest<
+ Json.key<'#fundec'>,
+ LvalueTaints[]
+ > = {
+ kind: Server.RqKind.GET,
+ name: 'plugins.eva.general.taintedLvalues',
+ input: Json.jKey<'#fundec'>('#fundec'),
+ output: Json.jArray(jLvalueTaints),
+ signals: [],
+};
+/** Get the tainted lvalues of a given function */
+export const taintedLvalues: Server.GetRequest<
+ Json.key<'#fundec'>,
+ LvalueTaints[]
+ >= taintedLvalues_internal;
+
/** Data for array rows [`properties`](#properties) */
export interface propertiesData {
/** Entry identifier. */
diff --git a/ivette/yarn.lock b/ivette/yarn.lock
index 68c29c52e021ed01caa40b93413da412b2c14ff5..aa98dbadf52cd4824088c375fd06493f2cb58f29 100644
--- a/ivette/yarn.lock
+++ b/ivette/yarn.lock
@@ -1786,6 +1786,50 @@
"@babel/helper-validator-identifier" "^7.16.7"
to-fast-properties "^2.0.0"
+"@codemirror/commands@6.1.0":
+ version "6.1.0"
+ resolved "https://registry.yarnpkg.com/@codemirror/commands/-/commands-6.1.0.tgz#c9da851f419f25dae400d7cd94f80b80ef060696"
+ integrity sha512-qCj2YqmbBjj0P1iumnlL5lBqZvJPzT+t2UvgjcaXErp5ZvMqFRVgQyrEfdXX6SX5UcvcHKBjXqno+MkUp0aYvQ==
+ dependencies:
+ "@codemirror/language" "^6.0.0"
+ "@codemirror/state" "^6.0.0"
+ "@codemirror/view" "^6.0.0"
+ "@lezer/common" "^1.0.0"
+
+"@codemirror/lang-cpp@6.0.1":
+ version "6.0.1"
+ resolved "https://registry.yarnpkg.com/@codemirror/lang-cpp/-/lang-cpp-6.0.1.tgz#7e91d193cedc3cac5135c04b1aac881d957b2c8a"
+ integrity sha512-46p3ohfhjzkLWJ3VwvzX0aqlXh8UkEqX1xo2Eds9l6Ql3uDoxI2IZEjR9cgJaGOZTXCkDzQuQH7sfYAxMvzLjA==
+ dependencies:
+ "@codemirror/language" "^6.0.0"
+ "@lezer/cpp" "^1.0.0"
+
+"@codemirror/language@6.2.1", "@codemirror/language@^6.0.0":
+ version "6.2.1"
+ resolved "https://registry.yarnpkg.com/@codemirror/language/-/language-6.2.1.tgz#cb10cd785a76e50ecd2fe2dc59ff66af8a41b87a"
+ integrity sha512-MC3svxuvIj0MRpFlGHxLS6vPyIdbTr2KKPEW46kCoCXw2ktb4NTkpkPBI/lSP/FoNXLCBJ0mrnUi1OoZxtpW1Q==
+ dependencies:
+ "@codemirror/state" "^6.0.0"
+ "@codemirror/view" "^6.0.0"
+ "@lezer/common" "^1.0.0"
+ "@lezer/highlight" "^1.0.0"
+ "@lezer/lr" "^1.0.0"
+ style-mod "^4.0.0"
+
+"@codemirror/state@6.1.1", "@codemirror/state@^6.0.0":
+ version "6.1.1"
+ resolved "https://registry.yarnpkg.com/@codemirror/state/-/state-6.1.1.tgz#4f512e5e34ea23a5e10b2c1fe43f6195e90417bb"
+ integrity sha512-2s+aXsxmAwnR3Rd+JDHPG/1lw0YsA9PEwl7Re88gHJHGfxyfEzKBmsN4rr53RyPIR4lzbbhJX0DCq0WlqlBIRw==
+
+"@codemirror/view@6.2.3", "@codemirror/view@^6.0.0":
+ version "6.2.3"
+ resolved "https://registry.yarnpkg.com/@codemirror/view/-/view-6.2.3.tgz#ba6e70037b1deee5e2d9e94541305aa50ede4715"
+ integrity sha512-cgN9gWS9+kv9+eOgVJWMrGUk4EwYKBZpuFYvxIlu4CmMye3+U+gMzuZhBgtPDOCbCp30hxFIOO0MENhGfnaC/g==
+ dependencies:
+ "@codemirror/state" "^6.0.0"
+ style-mod "^4.0.0"
+ w3c-keyname "^2.2.4"
+
"@develar/schema-utils@~2.6.5":
version "2.6.5"
resolved "https://registry.yarnpkg.com/@develar/schema-utils/-/schema-utils-2.6.5.tgz#3ece22c5838402419a6e0425f85742b961d9b6c6"
@@ -1883,6 +1927,33 @@
"@jridgewell/resolve-uri" "^3.0.3"
"@jridgewell/sourcemap-codec" "^1.4.10"
+"@lezer/common@^1.0.0":
+ version "1.0.1"
+ resolved "https://registry.yarnpkg.com/@lezer/common/-/common-1.0.1.tgz#d014fda6d582c24336fadf2715e76f02f73c8908"
+ integrity sha512-8TR5++Q/F//tpDsLd5zkrvEX5xxeemafEaek7mUp7Y+bI8cKQXdSqhzTOBaOogETcMOVr0pT3BBPXp13477ciw==
+
+"@lezer/cpp@^1.0.0":
+ version "1.0.0"
+ resolved "https://registry.yarnpkg.com/@lezer/cpp/-/cpp-1.0.0.tgz#3293fd88aaf16a6d4f18188602b4d931be8f0915"
+ integrity sha512-Klk3/AIEKoptmm6cNm7xTulNXjdTKkD+hVOEcz/NeRg8tIestP5hsGHJeFDR/XtyDTxsjoPjKZRIGohht7zbKw==
+ dependencies:
+ "@lezer/highlight" "^1.0.0"
+ "@lezer/lr" "^1.0.0"
+
+"@lezer/highlight@^1.0.0":
+ version "1.0.0"
+ resolved "https://registry.yarnpkg.com/@lezer/highlight/-/highlight-1.0.0.tgz#1dc82300f5d39fbd67ae1194b5519b4c381878d3"
+ integrity sha512-nsCnNtim90UKsB5YxoX65v3GEIw3iCHw9RM2DtdgkiqAbKh9pCdvi8AWNwkYf10Lu6fxNhXPpkpHbW6mihhvJA==
+ dependencies:
+ "@lezer/common" "^1.0.0"
+
+"@lezer/lr@^1.0.0":
+ version "1.2.3"
+ resolved "https://registry.yarnpkg.com/@lezer/lr/-/lr-1.2.3.tgz#f44ca844f15f6762fde4eab877d110567e34ffa1"
+ integrity sha512-qpB7rBzH8f6Mzjv2AVZRahcm+2Cf7nbIH++uXbvVOL1yIRvVWQ3HAM/saeBLCyz/togB7LGo76qdJYL1uKQlqA==
+ dependencies:
+ "@lezer/common" "^1.0.0"
+
"@malept/cross-spawn-promise@^1.1.0":
version "1.1.1"
resolved "https://registry.yarnpkg.com/@malept/cross-spawn-promise/-/cross-spawn-promise-1.1.1.tgz#504af200af6b98e198bce768bc1730c6936ae01d"
@@ -9152,6 +9223,11 @@ style-loader@^1.1.3:
loader-utils "^2.0.0"
schema-utils "^2.7.0"
+style-mod@^4.0.0:
+ version "4.0.0"
+ resolved "https://registry.yarnpkg.com/style-mod/-/style-mod-4.0.0.tgz#97e7c2d68b592975f2ca7a63d0dd6fcacfe35a01"
+ integrity sha512-OPhtyEjyyN9x3nhPsu76f52yUGXiZcgvsrFVtvTkyGRQJ0XK+GPc6ov1z+lRpbeabka+MYEQxOYRnt5nF30aMw==
+
sumchecker@^3.0.1:
version "3.0.1"
resolved "https://registry.yarnpkg.com/sumchecker/-/sumchecker-3.0.1.tgz#6377e996795abb0b6d348e9b3e1dfb24345a8e42"
@@ -9706,6 +9782,11 @@ vscode-textmate@5.2.0:
resolved "https://registry.yarnpkg.com/vscode-textmate/-/vscode-textmate-5.2.0.tgz#01f01760a391e8222fe4f33fbccbd1ad71aed74e"
integrity sha512-Uw5ooOQxRASHgu6C7GVvUxisKXfSgW4oFlO+aa+PAkgmH89O3CXxEEzNRNtHSqtXFTl0nAC1uYj0GMSH27uwtQ==
+w3c-keyname@^2.2.4:
+ version "2.2.6"
+ resolved "https://registry.yarnpkg.com/w3c-keyname/-/w3c-keyname-2.2.6.tgz#8412046116bc16c5d73d4e612053ea10a189c85f"
+ integrity sha512-f+fciywl1SJEniZHD6H+kUO8gOnwIr7f4ijKA6+ZvJFjeGi1r4PDLl53Ayud9O/rk64RqgoQine0feoeOU0kXg==
+
watchpack-chokidar2@^2.0.1:
version "2.0.1"
resolved "https://registry.yarnpkg.com/watchpack-chokidar2/-/watchpack-chokidar2-2.0.1.tgz#38500072ee6ece66f3769936950ea1771be1c957"
diff --git a/src/plugins/eva/api/general_requests.ml b/src/plugins/eva/api/general_requests.ml
index 2d185dc0db970e9d89e1df9c6e1bc8234568e2d5..216313063866d220a8376240db8ee9fdf02153a7 100644
--- a/src/plugins/eva/api/general_requests.ml
+++ b/src/plugins/eva/api/general_requests.ml
@@ -57,17 +57,39 @@ let _computation_signal =
~add_hook:Analysis.register_computation_hook
()
-module CallSite = Data.Jpair (Kernel_ast.Kf) (Kernel_ast.Stmt)
-let callers kf =
- let list = Results.callsites kf in
- List.concat (List.map (fun (kf, l) -> List.map (fun s -> kf, s) l) list)
-let () = Request.register ~package
- ~kind:`GET ~name:"getCallers"
- ~descr:(Markdown.plain "Get the list of call site of a function")
- ~input:(module Kernel_ast.Kf) ~output:(module Data.Jlist (CallSite))
- callers
+(* ----- Callsites ---------------------------------------------------------- *)
+
+module CallSite = struct
+ open Data
+ type callsite
+ let record: callsite Record.signature = Record.signature ()
+
+ let kf_field = Record.field record ~name:"kf"
+ ~descr:(Markdown.plain "Function") (module Kernel_ast.Kf)
+
+ let stmt_field = Record.field record ~name:"stmt"
+ ~descr:(Markdown.plain "Statement") (module Kernel_ast.Stmt)
+
+ let data = Record.publish ~package ~name:"CallSite"
+ ~descr:(Markdown.plain "CallSite") record
+
+ module R : Record.S with type r = callsite = (val data)
+
+ let convert (kf, stmts) = stmts |> List.map @@ fun stmt ->
+ R.default |> R.set kf_field kf |> R.set stmt_field stmt
+
+ let callers kf = Results.callsites kf |> List.map convert |> List.concat
+
+ let () = Request.register ~package
+ ~kind:`GET ~name:"getCallers"
+ ~descr:(Markdown.plain "Get the list of call site of a function")
+ ~input:(module Kernel_ast.Kf) ~output:(module Data.Jlist (R))
+ callers
+end
+
+
(* ----- Functions ---------------------------------------------------------- *)
@@ -93,6 +115,8 @@ struct
Analysis.register_computation_hook (fun _ -> f () ))
end
+
+
(* ----- Dead code: unreachable and non-terminating statements -------------- *)
type dead_code =
@@ -109,6 +133,7 @@ module DeadCode = struct
let unreachable = Record.field record ~name:"unreachable"
~descr:(Markdown.plain "List of unreachable statements.")
(module Data.Jlist (Kernel_ast.Marker))
+
let non_terminating = Record.field record ~name:"nonTerminating"
~descr:(Markdown.plain "List of reachable but non terminating statements.")
(module Data.Jlist (Kernel_ast.Marker))
@@ -159,7 +184,9 @@ let () = Request.register ~package
~output:(module DeadCode)
dead_code
-(* ----- Register Eva information ------------------------------------------- *)
+
+
+(* ----- Register Eva values information ------------------------------------ *)
let term_lval_to_lval tlval =
try Logic_to_c.term_lval_to_lval tlval
@@ -199,64 +226,79 @@ let () =
~enable:Analysis.is_computed
print_value
-let print_taint fmt marker =
- let loc = Cil_datatype.Location.unknown in
- let expr, stmt =
- match marker with
- | Printer_tag.PLval (_kf, Kstmt stmt, lval) ->
- Cil.new_exp ~loc (Lval lval), stmt
- | Printer_tag.PExp (_kf, Kstmt stmt, expr) -> expr, stmt
- | PVDecl (_kf, Kstmt stmt, vi) ->
- Cil.new_exp ~loc (Lval (Var vi, NoOffset)), stmt
- | PTermLval (_kf, Kstmt stmt, _ip, tlval) ->
- let lval = term_lval_to_lval tlval in
- Cil.new_exp ~loc (Lval lval), stmt
- | _ -> raise Not_found
- in
- let evaluate_taint request =
- let deps = Results.expr_dependencies expr request in
- Result.get_ok (Results.is_tainted deps.data request),
- Result.get_ok (Results.is_tainted deps.indirect request)
- in
- let before = evaluate_taint Results.(before stmt) in
- let after = evaluate_taint Results.(after stmt) in
- let str_taint = function
- | Results.Untainted -> "untainted"
+
+
+(* ----- Register Eva taints information ------------------------------------ *)
+
+let expr_of_lval v = Cil.new_exp ~loc:Cil_datatype.Location.unknown (Lval v)
+
+module EvaTaints = struct
+ open Results
+
+ let evaluate expr request =
+ let (let+) = Option.bind in
+ let { data ; indirect } = expr_dependencies expr request in
+ let+ data = is_tainted data request |> Result.to_option in
+ let+ indirect = is_tainted indirect request |> Result.to_option in
+ Some (data, indirect)
+
+ let expr_of_marker = let open Printer_tag in function
+ | PLval (_, Kstmt stmt, lval) -> Some (expr_of_lval lval, stmt)
+ | PExp (_, Kstmt stmt, expr) -> Some (expr, stmt)
+ | PVDecl (_, Kstmt stmt, vi) -> Some (expr_of_lval (Var vi, NoOffset), stmt)
+ | PTermLval (_, Kstmt stmt, _, tlval) ->
+ Some (term_lval_to_lval tlval |> expr_of_lval, stmt)
+ | _ -> None
+
+ let of_marker marker =
+ let (let+) = Option.bind in
+ let+ expr, stmt = expr_of_marker marker in
+ let+ before = evaluate expr (before stmt) in
+ let+ after = evaluate expr (after stmt) in
+ Some (before, after)
+
+ let to_string = function
+ | Untainted -> "untainted"
| Direct -> "direct taint"
| Indirect -> "indirect taint"
- in
- let pretty fmt = let open Results in function
- | taint, Untainted -> Format.fprintf fmt "%s" (str_taint taint)
- | t1, t2 ->
- Format.fprintf fmt
- "%s to the value, %s %s to values used to compute lvalues addresses"
- (str_taint t1) (if t1 = Untainted then "but" else "and") (str_taint t2)
- in
- if before = after
- then Format.fprintf fmt "%a" pretty before
- else Format.fprintf fmt "Before: %a@\nAfter: %a" pretty before pretty after
-let () =
- let enable () = Analysis.is_computed () && Taint_domain.Store.is_computed () in
- let title =
+ let pretty fmt = function
+ | taint, Untainted -> Format.fprintf fmt "%s" (to_string taint)
+ | data, indirect ->
+ let sep = match data with Untainted -> "but" | _ -> "and" in
+ Format.fprintf fmt
+ "%s to the value, %s %s to values used to compute lvalues adresses"
+ (to_string data) sep (to_string indirect)
+
+ let print_taint fmt marker =
+ let before, after = of_marker marker |> Option.get in
+ if before = after then Format.fprintf fmt "%a" pretty before
+ else Format.fprintf fmt "Before: %a@\nAfter: %a" pretty before pretty after
+
+ let eva_taints_title =
"Taint status:\n\
- Direct taint: data dependency from values provided by the attacker, \
meaning that the attacker may be able to alter this value\n\
- Indirect taint: the attacker cannot directly alter this value, but he \
may be able to impact the path by which its value is computed.\n\
- Untainted: cannot be modified by the attacker."
- in
- Server.Kernel_ast.Information.register
- ~id:"eva.taint" ~label:"Taint" ~descr: "Taint status according to Eva"
- ~title ~enable print_taint
-let () =
- Analysis.register_computation_hook
- (fun _ -> Server.Kernel_ast.Information.update ())
+ let () =
+ let taint_computed = Taint_domain.Store.is_computed in
+ let enable () = Analysis.is_computed () && taint_computed () in
+ Server.Kernel_ast.Information.register
+ ~id:"eva.taint" ~label:"Taint" ~descr: "Taint status according to Eva"
+ ~title:eva_taints_title ~enable print_taint
-(* ----- Red and tainted alarms --------------------------------------------- *)
+ let update = Server.Kernel_ast.Information.update
+ let () = Analysis.register_computation_hook (fun _ -> update ())
+end
+
+
+
+(* ----- Taint statuses ----------------------------------------------------- *)
-module Taint = struct
+module TaintStatus = struct
open Server.Data
type taint = Results.taint = Direct | Indirect | Untainted
@@ -271,49 +313,98 @@ module Taint = struct
~value dictionary
let tag_not_computed =
- tag (Error NotComputed) "not_computed" ""
- "Not computed" "the Eva taint domain has not been enabled, \
- or the Eva analysis has not been run"
+ tag (Error NotComputed) "not_computed" "" "Not computed"
+ "the Eva taint domain has not been enabled, \
+ or the Eva analysis has not been run"
let tag_error =
- tag (Error LogicError) "error" "Error"
- "Error" "the memory zone on which this property depends \
- could not be computed"
+ tag (Error LogicError) "error" "Error" "Error"
+ "the memory zone on which this property depends could not be computed"
let tag_not_applicable =
- tag (Error Irrelevant) "not_applicable" "—"
- "Not applicable" "no taint for this kind of property"
+ tag (Error Irrelevant) "not_applicable" "—" "Not applicable"
+ "no taint for this kind of property"
let tag_direct_taint =
- tag (Ok Direct) "direct_taint" "Tainted (direct)"
- "Direct taint"
+ tag (Ok Direct) "direct_taint" "Tainted (direct)" "Direct taint"
"this property is related to a memory location that can be affected \
by an attacker"
let tag_indirect_taint =
- tag (Ok Indirect) "indirect_taint" "Tainted (indirect)"
- "Indirect taint"
+ tag (Ok Indirect) "indirect_taint" "Tainted (indirect)" "Indirect taint"
"this property is related to a memory location whose assignment depends \
on path conditions that can be affected by an attacker"
let tag_untainted =
- tag (Ok Untainted) "not_tainted" "Untainted"
- "Untainted property" "this property is safe"
-
- let () = Enum.set_lookup dictionary
- begin function
- | Error NotComputed -> tag_not_computed
- | Error Irrelevant -> tag_not_applicable
- | Error LogicError -> tag_error
- | Ok Direct -> tag_direct_taint
- | Ok Indirect -> tag_indirect_taint
- | Ok Untainted -> tag_untainted
- end
+ tag (Ok Untainted) "not_tainted" "Untainted" "Untainted property"
+ "this property is safe"
+
+ let () = Enum.set_lookup dictionary @@ function
+ | Error NotComputed -> tag_not_computed
+ | Error Irrelevant -> tag_not_applicable
+ | Error LogicError -> tag_error
+ | Ok Direct -> tag_direct_taint
+ | Ok Indirect -> tag_indirect_taint
+ | Ok Untainted -> tag_untainted
let data = Request.dictionary ~package ~name:"taintStatus"
~descr:(Markdown.plain "Taint status of logical properties") dictionary
include (val data : S with type t = (taint, error) result)
+end
+
+
+
+(* ----- Tainted lvalues ---------------------------------------------------- *)
+
+module LvalueTaints = struct
+ module Table = Cil_datatype.Lval.Hashtbl
+
+ module Status = struct
+ type record
+ let record: record Data.Record.signature = Data.Record.signature ()
+ let field name d = Data.Record.field record ~name ~descr:(Markdown.plain d)
+ let lval_field = field "lval" "tainted lvalue" (module Kernel_ast.Lval)
+ let taint_field = field "taint" "taint status" (module TaintStatus)
+ let name, descr = "LvalueTaints", Markdown.plain "Lvalue taint status"
+ let publication = Data.Record.publish record ~package ~name ~descr
+ include (val publication: Data.Record.S with type r = record)
+ let create lval taint = set lval_field lval @@ set taint_field taint default
+ end
+
+ let current_project () = Visitor_behavior.inplace ()
+ class tainted_lvalues taints = object (self)
+ inherit Visitor.generic_frama_c_visitor (current_project ())
+ method! vlval lval =
+ let expr = expr_of_lval lval in
+ match self#current_stmt with
+ | None -> DoChildren
+ | Some stmt ->
+ match Results.after stmt |> EvaTaints.evaluate expr with
+ | Some (Results.Untainted, _) -> DoChildren
+ | Some (t, _) -> Table.add taints lval (Kstmt stmt, t) ; DoChildren
+ | None -> DoChildren
+ end
+
+ let get_tainted_lvals fundec =
+ let taints = Table.create 17 in
+ Visitor.visitFramacFunction (new tainted_lvalues taints) fundec |> ignore ;
+ let fn lval (ki, taint) acc = Status.create (ki, lval) (Ok taint) :: acc in
+ Table.fold fn taints [] |> List.rev
+
+ let () = Request.register ~package ~kind:`GET ~name:"taintedLvalues"
+ ~descr:(Markdown.plain "Get the tainted lvalues of a given function")
+ ~input:(module (Kernel_ast.Fundec))
+ ~output:(module (Data.Jlist (Status)))
+ get_tainted_lvals
+end
+
+
+
+(* ----- Red and tainted alarms --------------------------------------------- *)
+
+module PropertiesData = struct
+ open TaintStatus
let zone_of_predicate kinstr predicate =
let state = Results.(before_kinstr kinstr |> get_cvalue_model) in
@@ -336,40 +427,39 @@ module Taint = struct
| _ -> Error Irrelevant
let is_tainted_property ip =
- if not (Analysis.is_computed () && Taint_domain.Store.is_computed ())
- then Error NotComputed
- else
+ if Analysis.is_computed () && Taint_domain.Store.is_computed () then
let (let+) = Result.bind in
let kinstr = Property.get_kinstr ip in
let+ predicate = get_predicate ip in
let+ zone = zone_of_predicate kinstr predicate in
let result = Results.(before_kinstr kinstr |> is_tainted zone) in
Result.map_error (fun _ -> NotComputed) result
-end
+ else Error NotComputed
-let model = States.model ()
-
-let () = States.column model ~name:"priority"
- ~descr:(Markdown.plain "Is the property invalid in some context \
- of the analysis?")
- ~data:(module Data.Jbool)
- ~get:(fun ip -> Red_statuses.is_red ip)
-
-let () = States.column model ~name:"taint"
- ~descr:(Markdown.plain "Is the property tainted according to \
- the Eva taint domain?")
- ~data:(module Taint)
- ~get:(fun ip -> Taint.is_tainted_property ip)
+ let () =
+ let model = States.model () in
+ let descr = "Is the property invalid in some context of the analysis?" in
+ States.column model
+ ~name:"priority"
+ ~descr:(Markdown.plain descr)
+ ~data:(module Data.Jbool)
+ ~get:Red_statuses.is_red ;
+ let descr = "Is the property tainted according to the Eva taint domain?" in
+ States.column model
+ ~name:"taint"
+ ~descr:(Markdown.plain descr)
+ ~data:(module TaintStatus)
+ ~get:is_tainted_property ;
+ ignore @@ States.register_array
+ ~package
+ ~name:"properties"
+ ~descr:(Markdown.plain "Status of Registered Properties")
+ ~key:(fun ip -> Kernel_ast.Marker.create (PIP ip))
+ ~keyType:Kernel_ast.Marker.jproperty
+ ~iter:Property_status.iter
+ model
+end
-let _array =
- States.register_array
- ~package
- ~name:"properties"
- ~descr:(Markdown.plain "Status of Registered Properties")
- ~key:(fun ip -> Kernel_ast.Marker.create (PIP ip))
- ~keyType:Kernel_ast.Marker.jproperty
- ~iter:Property_status.iter
- model
(* ----- Analysis statistics ------------------------------------------------ *)
@@ -581,6 +671,7 @@ let _array =
model
+
(* ----- Domains states ----------------------------------------------------- *)
let compute_lval_deps request lval =