From eb05e7ac47e50dde1cf7eec62c93f421cfb28cc2 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Wed, 23 Feb 2022 14:36:58 +0100
Subject: [PATCH] [ivette] AST informations
---
ivette/src/frama-c/index.tsx | 12 +-
ivette/src/frama-c/kernel/ASTinfo.tsx | 335 ++++++++++++++++--
ivette/src/frama-c/kernel/ASTview.tsx | 4 +-
ivette/src/frama-c/kernel/api/ast/index.ts | 31 +-
ivette/src/frama-c/kernel/style.css | 86 ++++-
ivette/src/frama-c/{utils.ts => richtext.tsx} | 84 ++++-
src/plugins/server/kernel_ast.ml | 189 ++++++----
src/plugins/server/kernel_ast.mli | 26 ++
8 files changed, 648 insertions(+), 119 deletions(-)
rename ivette/src/frama-c/{utils.ts => richtext.tsx} (57%)
diff --git a/ivette/src/frama-c/index.tsx b/ivette/src/frama-c/index.tsx
index 9c3e42d30e1..cca6df663d7 100644
--- a/ivette/src/frama-c/index.tsx
+++ b/ivette/src/frama-c/index.tsx
@@ -55,18 +55,18 @@ Ivette.registerGroup({
Ivette.registerSidebar({ id: 'frama-c.globals', children: <Globals /> });
Ivette.registerToolbar({ id: 'frama-c.history', children: <History /> });
Ivette.registerStatusbar({ id: 'frama-c.message', children: <Status /> });
+ Ivette.registerComponent({
+ id: 'frama-c.astinfo',
+ label: 'Informations',
+ title: 'Contextual informations on current selection',
+ children: <ASTinfo />
+ });
Ivette.registerComponent({
id: 'frama-c.astview',
label: 'AST',
title: 'Normalized C/ACSL Source Code',
children: <ASTview />,
});
- Ivette.registerComponent({
- id: 'frama-c.astinfo',
- label: 'Informations',
- title: 'Informations on currently selected item',
- children: <ASTinfo />,
- });
Ivette.registerComponent({
id: 'frama-c.sourcecode',
label: 'Source Code',
diff --git a/ivette/src/frama-c/kernel/ASTinfo.tsx b/ivette/src/frama-c/kernel/ASTinfo.tsx
index 928411368bd..abf6d96d7c7 100644
--- a/ivette/src/frama-c/kernel/ASTinfo.tsx
+++ b/ivette/src/frama-c/kernel/ASTinfo.tsx
@@ -25,49 +25,322 @@
// --------------------------------------------------------------------------
import React from 'react';
+import * as Dome from 'dome';
+import { classes } from 'dome/misc/utils';
import * as States from 'frama-c/states';
-import * as Utils from 'frama-c/utils';
+import * as DATA from 'frama-c/kernel/api/data';
+import * as AST from 'frama-c/kernel/api/ast';
+import { Text } from 'frama-c/richtext';
+import { Icon } from 'dome/controls/icons';
+import { Code } from 'dome/controls/labels';
+import { IconButton } from 'dome/controls/buttons';
+import * as Boxes from 'dome/layout/boxes';
+import { TitleBar } from 'ivette';
-import { Vfill } from 'dome/layout/boxes';
-import { RichTextBuffer } from 'dome/text/buffers';
-import { Text } from 'dome/text/editors';
-import { getInfo } from 'frama-c/kernel/api/ast';
+// --------------------------------------------------------------------------
+// --- Marker Kinds
+// --------------------------------------------------------------------------
+
+interface MarkerKindProps { label: string; title: string }
+
+function MarkerKind(props: MarkerKindProps): JSX.Element {
+ const { label, title } = props;
+ return <span className="astinfo-markerkind" title={title}>{label}</span>;
+}
+
+const GMARKER =
+ <MarkerKind label="M" title="Generic Marker" />;
+
+const MARKERS = new Map<AST.markerKind, JSX.Element>();
+[
+ {
+ kind: AST.markerKind.declaration,
+ elt: <MarkerKind label="D" title="Declaration" />,
+ },
+ {
+ kind: AST.markerKind.global,
+ elt: <MarkerKind label="G" title="Global" />,
+ },
+ {
+ kind: AST.markerKind.lvalue,
+ elt: <MarkerKind label="L" title="L-value" />,
+ },
+ {
+ kind: AST.markerKind.expression,
+ elt: <MarkerKind label="E" title="Expression" />,
+ },
+ {
+ kind: AST.markerKind.statement,
+ elt: <MarkerKind label="S" title="Statement" />,
+ },
+ {
+ kind: AST.markerKind.property,
+ elt: <MarkerKind label="P" title="Property" />,
+ },
+ {
+ kind: AST.markerKind.term,
+ elt: <MarkerKind label="T" title="Term" />,
+ },
+].forEach(({ kind, elt }) => MARKERS.set(kind, elt));
// --------------------------------------------------------------------------
-// --- Information Panel
+// --- Information Details
// --------------------------------------------------------------------------
-export default function ASTinfo(): JSX.Element {
+interface InfoItemProps {
+ label: string;
+ title: string;
+ descr: DATA.text;
+}
+
+function InfoItem(props: InfoItemProps): JSX.Element {
+ return (
+ <div className="astinfo-infos">
+ <div
+ className="dome-text-label astinfo-kind"
+ title={props.title}
+ >
+ {props.label}
+ </div>
+ <div className="dome-text-cell astinfo-data">
+ <Text text={props.descr} />
+ </div>
+ </div>
+ );
+}
+
+interface ASTinfos {
+ id: string;
+ label: string;
+ title: string;
+ descr: DATA.text;
+}
+
+interface InfoSectionProps {
+ marker: AST.marker;
+ markerInfo: AST.markerInfoData;
+ filter: string;
+ selected: boolean;
+ hovered: boolean;
+ pinned: boolean;
+ onPin: () => void;
+ onHover: (hover: boolean) => void;
+ onSelect: () => void;
+ onRemove: () => void;
+}
+
+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.getInformations, marker) ?? [];
+ const highlight = classes(
+ props.selected && !props.pinned && 'transient',
+ props.hovered && 'hovered',
+ );
+ const descr = markerInfo.descr ?? markerInfo.name;
+ const kind = MARKERS.get(markerInfo.kind) ?? GMARKER;
+ const fs = props.filter.split(':');
+ const filtered = allInfos.filter((info) => !fs.some((m) => m === info.id));
+ const infos = more ? allInfos : filtered;
+ const hasMore = filtered.length < allInfos.length;
+ return (
+ <div
+ className={`astinfo-section ${highlight}`}
+ onMouseEnter={() => props.onHover(true)}
+ onMouseLeave={() => props.onHover(false)}
+ onDoubleClick={props.onSelect}
+ >
+ <div
+ key="MARKER"
+ className={`astinfo-markerbar ${highlight}`}
+ title={descr}
+ >
+ <Icon
+ className="astinfo-folderbutton"
+ style={{ visibility: infos.length ? 'visible' : 'hidden' }}
+ size={9}
+ offset={-2}
+ id={unfold ? 'TRIANGLE.DOWN' : 'TRIANGLE.RIGHT'}
+ onClick={() => setUnfold(!unfold)}
+ />
+ <Code className="astinfo-markercode">
+ {kind}{descr}
+ </Code>
+ <IconButton
+ className="astinfo-markerbutton"
+ title="Pin/unpin information in sidebar"
+ size={9}
+ offset={0}
+ icon="PIN"
+ selected={props.pinned}
+ onClick={props.onPin}
+ />
+ <IconButton
+ style={{ display: hasMore ? undefined : 'none' }}
+ className="astinfo-markerbutton"
+ title="Show all available informations"
+ size={9}
+ offset={0}
+ icon="CIRC.PLUS"
+ selected={more}
+ onClick={() => setMore(!more)}
+ />
+ <IconButton
+ className="astinfo-markerbutton"
+ title="Remove informations"
+ size={9}
+ offset={0}
+ icon="CIRC.CLOSE"
+ onClick={props.onRemove}
+ />
+ </div>
+ {unfold && infos.map((info) => <InfoItem key={info.id} {...info} />)}
+ </div>
+ );
+}
- const buffer = React.useMemo(() => new RichTextBuffer(), []);
- const [selection, updateSelection] = States.useSelection();
- const marker = selection?.current?.marker;
- const data = States.useRequest(getInfo, marker);
-
- React.useEffect(() => {
- buffer.clear();
- const style = { css: 'color: var(--text-highlighted)' };
- if (data) Utils.printTextWithTags(buffer, data, style);
- }, [buffer, data]);
-
- // Callbacks
- function onTextSelection(id: string): void {
- // For now, the only markers are functions.
- const location = { fct: id };
- updateSelection({ location });
+// --------------------------------------------------------------------------
+// --- Information Selection State
+// --------------------------------------------------------------------------
+
+type Mark = { fct: string; marker: AST.marker };
+
+const reload = new Dome.Event('frama-c.astinfo');
+
+class InfoMarkers {
+
+ private selection: Mark[] = [];
+ private pinned = new Map<string, boolean>();
+
+ setSelected(location?: States.Location, pinned = false): void {
+ const fct = location?.fct;
+ const marker = location?.marker;
+ const keep =
+ (m: Mark): boolean => m.marker === marker || this.isPinned(m.marker);
+ const self =
+ (m: Mark): boolean => m.marker === marker;
+ this.selection = this.selection.filter(keep);
+ if (fct && marker && !this.selection.some(self)) {
+ this.selection.push({ fct, marker });
+ this.pinned.set(marker, pinned);
+ }
+ reload.emit();
+ }
+
+ isPinned(marker: AST.marker | undefined): boolean {
+ return (marker !== undefined) && (this.pinned.get(marker) ?? false);
+ }
+
+ setPinned(marker: AST.marker, pinned: boolean): void {
+ this.pinned.set(marker, pinned);
+ reload.emit();
+ }
+
+ removeMarker(marker: AST.marker): void {
+ this.selection = this.selection.filter((m) => m.marker !== marker);
+ this.pinned.delete(marker);
+ reload.emit();
}
- // Component
+ getSelected(): Mark[] { return this.selection; }
+
+}
+
+// --------------------------------------------------------------------------
+// --- Context Menu Filter
+// --------------------------------------------------------------------------
+
+function openFilter(
+ infos: ASTinfos[],
+ filter: string,
+ onChange: (f: string) => void,
+): void {
+ const menuItems = infos.map((info) => {
+ const fs = filter.split(':');
+ const checked = !fs.some((m) => m === info.id);
+ const onClick = (): void => {
+ const newFs =
+ checked
+ ? fs.concat(info.id)
+ : fs.filter((m) => m !== info.id);
+ onChange(newFs.join(':'));
+ };
+ return {
+ id: info.id,
+ label: `${info.title} (${info.label})`,
+ checked,
+ onClick,
+ };
+ });
+ Dome.popupMenu(menuItems);
+ return;
+}
+
+// --------------------------------------------------------------------------
+// --- Information Panel
+// --------------------------------------------------------------------------
+
+export default function ASTinfo(): JSX.Element {
+ // Hooks
+ Dome.useUpdate(reload);
+ const markers = React.useMemo(() => new InfoMarkers(), []);
+ const markerInfos = States.useSyncArray(AST.markerInfo, false);
+ const [selection] = States.useSelection();
+ const [hoveredLoc] = States.useHovered();
+ const informations = States.useRequest(AST.getInformations, null) ?? [];
+ const [filter, setFilter] =
+ Dome.useStringSettings('frama-c.sidebar.astinfo.filter', '');
+ const location = selection?.current;
+ const selected = location?.marker;
+ const hovered = hoveredLoc?.marker;
+ React.useEffect(() => markers.setSelected(location), [markers, location]);
+ Dome.useEvent(States.MetaSelection, (loc) => {
+ if (selected) markers.setPinned(selected, true);
+ markers.setSelected(loc, true);
+ });
+ // Rendering
+ const renderMark = (mark: Mark): JSX.Element | null => {
+ const { marker } = mark;
+ const markerInfo = markerInfos.getData(marker);
+ if (!markerInfo) return null;
+ const pinned = markers.isPinned(marker);
+ const isSelected = selected === marker;
+ const isHovered = hovered === marker;
+ const onPin = () => void markers.setPinned(marker, !pinned);
+ const onRemove = () => void markers.removeMarker(marker);
+ const onSelect = () => void States.setSelection(mark);
+ const onHover =
+ (h: boolean): void => States.setHovered(h ? mark : undefined);
+ return (
+ <MarkInfos
+ key={marker}
+ marker={marker}
+ markerInfo={markerInfo}
+ pinned={pinned}
+ selected={isSelected}
+ filter={filter}
+ hovered={isHovered}
+ onPin={onPin}
+ onRemove={onRemove}
+ onHover={onHover}
+ onSelect={onSelect}
+ />
+ );
+ };
return (
<>
- <Vfill>
- <Text
- buffer={buffer}
- mode="text"
- onSelection={onTextSelection}
- readOnly
+ <TitleBar>
+ <IconButton
+ icon="CLIPBOARD"
+ onClick={() => openFilter(informations, filter, setFilter)}
+ title="Information Filters"
/>
- </Vfill>
+ </TitleBar>
+ <Boxes.Vfill>
+ {markers.getSelected().map(renderMark)}
+ </Boxes.Vfill>
</>
);
}
diff --git a/ivette/src/frama-c/kernel/ASTview.tsx b/ivette/src/frama-c/kernel/ASTview.tsx
index d54fb085d2f..53650f233aa 100644
--- a/ivette/src/frama-c/kernel/ASTview.tsx
+++ b/ivette/src/frama-c/kernel/ASTview.tsx
@@ -30,7 +30,7 @@ import React from 'react';
import _ from 'lodash';
import * as Server from 'frama-c/server';
import * as States from 'frama-c/states';
-import * as Utils from 'frama-c/utils';
+import * as RichText from 'frama-c/richtext';
import * as Dome from 'dome';
import { RichTextBuffer } from 'dome/text/buffers';
@@ -66,7 +66,7 @@ async function loadAST(
if (!data) {
buffer.log('// No code for function', theFunction);
}
- Utils.printTextWithTags(buffer, data);
+ RichText.printTextWithTags(buffer, data);
if (theMarker)
buffer.scroll(theMarker);
} catch (err) {
diff --git a/ivette/src/frama-c/kernel/api/ast/index.ts b/ivette/src/frama-c/kernel/api/ast/index.ts
index 73dad1c7216..8e2a100ffc9 100644
--- a/ivette/src/frama-c/kernel/api/ast/index.ts
+++ b/ivette/src/frama-c/kernel/api/ast/index.ts
@@ -458,15 +458,34 @@ const functions_internal: State.Array<Json.key<'#functions'>,functionsData> = {
/** AST Functions */
export const functions: State.Array<Json.key<'#functions'>,functionsData> = functions_internal;
-const getInfo_internal: Server.GetRequest<marker,text> = {
+/** Updated AST informations */
+export const getInformationsUpdate: Server.Signal = {
+ name: 'kernel.ast.getInformationsUpdate',
+};
+
+const getInformations_internal: Server.GetRequest<
+ marker |
+ undefined,
+ { id: string, label: string, title: string, descr: text }[]
+ > = {
kind: Server.RqKind.GET,
- name: 'kernel.ast.getInfo',
+ name: 'kernel.ast.getInformations',
input: jMarker,
- output: jText,
- signals: [],
+ output: Json.jList(
+ Json.jObject({
+ id: Json.jFail(Json.jString,'String expected'),
+ label: Json.jFail(Json.jString,'String expected'),
+ title: Json.jFail(Json.jString,'String expected'),
+ descr: jTextSafe,
+ })),
+ signals: [[ { name: 'kernel.ast.getInformationsUpdate' } ]],
};
-/** Get textual information about a marker */
-export const getInfo: Server.GetRequest<marker,text>= getInfo_internal;
+/** Get available informations about markers. When no marker is given, returns all kinds of informations (with empty `descr` field). */
+export const getInformations: Server.GetRequest<
+ marker |
+ undefined,
+ { id: string, label: string, title: string, descr: text }[]
+ >= getInformations_internal;
const getMarkerAt_internal: Server.GetRequest<
[ string, number, number ],
diff --git a/ivette/src/frama-c/kernel/style.css b/ivette/src/frama-c/kernel/style.css
index be30b0d1581..52e6d44c63d 100644
--- a/ivette/src/frama-c/kernel/style.css
+++ b/ivette/src/frama-c/kernel/style.css
@@ -9,6 +9,18 @@
text-overflow: ellipsis;
}
+/* -------------------------------------------------------------------------- */
+/* --- Lightweight Text Markers --- */
+/* -------------------------------------------------------------------------- */
+
+.kernel-text {
+ white-space: pre;
+}
+
+.kernel-text-marker:hover {
+ background: lightgreen;
+}
+
/* -------------------------------------------------------------------------- */
/* --- AST View --- */
/* -------------------------------------------------------------------------- */
@@ -17,6 +29,10 @@
background-color: var(--highlighted-marker);
}
+.hovered-marker {
+ background-color: lightblue;
+}
+
.dead-code {
background-color: var(--dead-code);
border-bottom: solid 0.1em var(--dead-code);
@@ -54,7 +70,75 @@
}
/* -------------------------------------------------------------------------- */
-/* --- Globals --- */
+/* --- Informations --- */
+/* -------------------------------------------------------------------------- */
+
+.astinfo-section {
+ position: relative;
+ overflow: hidden;
+ padding-top: 1px;
+ padding-bottom: 2px;
+}
+
+.astinfo-section.hovered {
+ background: #ddd;
+}
+
+.astinfo-section.transient {
+ background: #f5d69e;
+}
+
+.astinfo-folderbutton {
+ flex: 0 0 auto;
+}
+
+.astinfo-markerbar {
+ display: flex;
+ overflow: hidden;
+ padding-left: 4px;
+}
+
+.astinfo-markerkind {
+ background: #b1c6dc;
+ position: relative;
+ top: -1px;
+ border-radius: 2px;
+ font-size: 7pt;
+ padding: 2px;
+ color: black;
+ user-select: none;
+ margin-right: 3pt;
+}
+
+.astinfo-markercode {
+ flex: 1 1 auto;
+ text-overflow: ellipsis;
+ cursor: default;
+}
+
+.astinfo-markerbutton {
+ flex: 0 1 auto;
+ margin: 0px;
+ position: relative;
+}
+
+.astinfo-infos {
+ display: flex ;
+ margin-top: 1px ;
+ margin-bottom: 1px ;
+}
+
+.astinfo-kind {
+ flex: 0 1 50px;
+ text-align: center;
+ margin-top: 1px;
+ margin-left: 8px;
+ color: #999;
+ font-size: smaller;
+}
+
+/* -------------------------------------------------------------------------- */
+/* --- Messages --- */
/* -------------------------------------------------------------------------- */
.message-search {
diff --git a/ivette/src/frama-c/utils.ts b/ivette/src/frama-c/richtext.tsx
similarity index 57%
rename from ivette/src/frama-c/utils.ts
rename to ivette/src/frama-c/richtext.tsx
index 86df5df5f3d..3ce352526b6 100644
--- a/ivette/src/frama-c/utils.ts
+++ b/ivette/src/frama-c/richtext.tsx
@@ -26,12 +26,14 @@
/**
* @packageDocumentation
- * @module frama-c/utils
-*/
+ * @module frama-c/richtext
+ */
+import React from 'react';
import * as Dome from 'dome';
import * as DomeBuffers from 'dome/text/buffers';
import * as KernelData from 'frama-c/kernel/api/data';
+import { classes } from 'dome/misc/utils';
const D = new Dome.Debug('Utils');
@@ -42,33 +44,93 @@ const D = new Dome.Debug('Utils');
/**
* Print text containing tags into buffer.
* @param buffer Rich text buffer to print into.
- * @param contents Actual text containing tags.
+ * @param text Actual text containing tags.
* @param options Specify particular marker options.
*/
export function printTextWithTags(
buffer: DomeBuffers.RichTextBuffer,
- contents: KernelData.text,
+ text: KernelData.text,
options?: DomeBuffers.MarkerProps,
): void {
- if (Array.isArray(contents)) {
+ if (Array.isArray(text)) {
let marker = false;
- const tag = contents.shift();
+ const tag = text.shift();
if (tag) {
if (Array.isArray(tag)) {
- contents.unshift(tag);
+ text.unshift(tag);
} else {
buffer.openTextMarker({ id: tag, ...options ?? {} });
marker = true;
}
}
- contents.forEach((txt) => printTextWithTags(buffer, txt, options));
+ text.forEach((txt) => printTextWithTags(buffer, txt, options));
if (marker) {
marker = false;
buffer.closeTextMarker();
}
- } else if (typeof contents === 'string') {
- buffer.append(contents);
+ } else if (typeof text === 'string') {
+ buffer.append(text);
} else {
- D.error('Unexpected text', contents);
+ D.error('Unexpected text', text);
+ }
+}
+
+// --------------------------------------------------------------------------
+// --- Lightweight Text Renderer
+// --------------------------------------------------------------------------
+
+interface MarkerProps {
+ marker: string;
+ onMarker?: (marker: string) => void;
+ children?: React.ReactNode;
+}
+
+function Marker(props: MarkerProps): JSX.Element {
+ const { marker, onMarker, children } = props;
+ const onClick = (): void => { if (onMarker) onMarker(marker); };
+ return (
+ <span
+ className="kernel-text-marker"
+ onClick={onClick}
+ >
+ {children}
+ </span>
+ );
+}
+
+function makeContents(text: KernelData.text): React.ReactNode {
+ if (Array.isArray(text)) {
+ const tag = text.shift();
+ let marker: string | undefined;
+ if (tag) {
+ if (Array.isArray(tag)) {
+ text.unshift(tag);
+ } else if (typeof tag === 'string') {
+ marker = tag;
+ }
+ // otherwize, ignore tag
+ }
+ const contents = React.Children.map(text, makeContents);
+ if (marker)
+ return <Marker marker={marker}>{contents}</Marker>;
+ return <>{contents}</>;
+ } if (typeof text === 'string') {
+ return text;
}
+ D.error('Unexpected text', text);
+ return null;
+
}
+
+export interface TextProps {
+ text: KernelData.text;
+ onMarker?: (marker: string) => void;
+ className?: string;
+}
+
+export function Text(props: TextProps): JSX.Element {
+ const className = classes('kernel-text', 'dome-text-code', props.className);
+ return <div className={className}>{makeContents(props.text)}</div>;
+}
+
+// --------------------------------------------------------------------------
diff --git a/src/plugins/server/kernel_ast.ml b/src/plugins/server/kernel_ast.ml
index d8cf92f5501..bc13a83fd26 100644
--- a/src/plugins/server/kernel_ast.ml
+++ b/src/plugins/server/kernel_ast.ml
@@ -543,74 +543,139 @@ struct
end
(* -------------------------------------------------------------------------- *)
-(* --- Information --- *)
+(* --- Marker Informations --- *)
(* -------------------------------------------------------------------------- *)
-module Info = struct
- open Printer_tag
+module Informations =
+struct
+
+ type info = {
+ id: string;
+ rank: int;
+ label: string;
+ title: string;
+ pretty: Format.formatter -> Printer_tag.localizable -> unit
+ }
+
+ (* Info markers serialization *)
+
+ module S =
+ struct
+ type t = (info * Jtext.t)
+ let jtype = Package.(Jrecord[
+ "id", Jstring ;
+ "label", Jstring ;
+ "title", Jstring ;
+ "descr", Jtext.jtype ;
+ ])
+ let of_json _ = failwith "Informations.Info"
+ let to_json (info,text) = `Assoc [
+ "id", `String info.id ;
+ "label", `String info.label ;
+ "title", `String info.title ;
+ "descr", text ;
+ ]
+ end
+
+ (* Info markers registry *)
+
+ let rankId = ref 0
+ let registry : (string,info) Hashtbl.t = Hashtbl.create 0
+
+ let jtext pp marker =
+ try
+ let buffer = Jbuffer.create () in
+ let fmt = Jbuffer.formatter buffer in
+ pp fmt marker;
+ Format.pp_print_flush fmt ();
+ Jbuffer.contents buffer
+ with Not_found ->
+ `Null
+
+ let rank ({rank},_) = rank
+ let by_rank a b = Stdlib.compare (rank a) (rank b)
+
+ let get_informations tgt =
+ let infos = ref [] in
+ Hashtbl.iter
+ (fun _ info ->
+ match tgt with
+ | None -> infos := (info, `Null) :: !infos
+ | Some marker ->
+ let text = jtext info.pretty marker in
+ if not (Jbuffer.is_empty text) then
+ infos := (info, text) :: !infos
+ ) registry ;
+ List.sort by_rank !infos
+
+ let signal = Request.signal ~package
+ ~name:"getInformationsUpdate"
+ ~descr:(Md.plain "Updated AST informations")
+
+ let update () = Request.emit signal
+
+ let register ~id ~label ~title pretty =
+ let rank = incr rankId ; !rankId in
+ let info = { id ; rank ; label ; title ; pretty } in
+ if Hashtbl.mem registry id then
+ ( let msg = Format.sprintf
+ "Server.Kernel_ast.register_info: duplicate %S" id in
+ raise (Invalid_argument msg) );
+ Hashtbl.add registry id info
- let print_function fmt name =
- let stag = Format.String_tag name in
- Format.pp_open_stag fmt stag;
- Format.pp_print_string fmt name;
- Format.pp_close_stag fmt ()
-
- let print_kf fmt kf = print_function fmt (Kernel_function.get_name kf)
-
- let print_variable fmt vi =
- Format.fprintf fmt "Variable %s has type %a.@."
- vi.vname Printer.pp_typ vi.vtype;
- let kf = Kernel_function.find_defining_kf vi in
- let pp_kf fmt kf = Format.fprintf fmt " of function %a" print_kf kf in
- Format.fprintf fmt "It is a %s variable%a.@."
- (if vi.vglob then "global" else if vi.vformal then "formal" else "local")
- (Format.pp_print_option pp_kf) kf;
- if vi.vtemp then
- Format.fprintf fmt "This is a temporary variable%s.@."
- (match vi.vdescr with None -> "" | Some descr -> " for " ^ descr);
- Format.fprintf fmt "It is %sreferenced and its address is %staken."
- (if vi.vreferenced then "" else "not ")
- (if vi.vaddrof then "" else "not ")
-
- let print_varinfo fmt vi =
- if Cil.isFunctionType vi.vtype
- then
- Format.fprintf fmt "%a is a C function of type '%a'."
- print_function vi.vname Printer.pp_typ vi.vtype
- else print_variable fmt vi
-
- let print_lvalue fmt _loc = function
- | Var vi, NoOffset -> print_varinfo fmt vi
- | lval ->
- Format.fprintf fmt "This is an lvalue of type %a."
- Printer.pp_typ (Cil.typeOfLval lval)
-
- let print_localizable fmt = function
- | PExp (_, _, e) ->
- Format.fprintf fmt "This is a pure C expression of type %a."
- Printer.pp_typ (Cil.typeOf e)
- | PLval (_, _, lval) as loc -> print_lvalue fmt loc lval
- | PVDecl (_, _, vi) ->
- Format.fprintf fmt "This is the declaration of variable %a.@.@."
- Printer.pp_varinfo vi;
- print_varinfo fmt vi
- | PStmt (kf, _) | PStmtStart (kf, _) ->
- Format.fprintf fmt "This is a statement of function %a." print_kf kf
- | _ -> ()
-
- let get_marker_info loc =
- let buffer = Jbuffer.create () in
- let fmt = Jbuffer.formatter buffer in
- print_localizable fmt loc;
- Format.pp_print_flush fmt ();
- Jbuffer.contents buffer
end
let () = Request.register ~package
- ~kind:`GET ~name:"getInfo"
- ~descr:(Md.plain "Get textual information about a marker")
- ~input:(module Marker) ~output:(module Jtext)
- Info.get_marker_info
+ ~kind:`GET ~name:"getInformations"
+ ~descr:(Md.plain
+ "Get available informations about markers. \
+ When no marker is given, returns all kinds \
+ of informations (with empty `descr` field).")
+ ~input:(module Joption(Marker))
+ ~output:(module Jlist(Informations.S))
+ ~signals:[Informations.signal]
+ Informations.get_informations
+
+(* -------------------------------------------------------------------------- *)
+(* --- Default Kernel Informations --- *)
+(* -------------------------------------------------------------------------- *)
+
+let () = Informations.register
+ ~id:"kernel.ast.varinfo"
+ ~label:"Var"
+ ~title:"Variable Informations"
+ begin fun fmt loc ->
+ match loc with
+ | PLval (_ , _, (Var x,NoOffset)) | PVDecl(_,_,x) ->
+ if not x.vreferenced then Format.pp_print_string fmt "unused " ;
+ begin
+ match x.vstorage with
+ | NoStorage -> ()
+ | Extern -> Format.pp_print_string fmt "extern "
+ | Static -> Format.pp_print_string fmt "static "
+ | Register -> Format.pp_print_string fmt "register "
+ end ;
+ if x.vghost then Format.pp_print_string fmt "ghost " ;
+ if x.vaddrof then Format.pp_print_string fmt "aliased " ;
+ if x.vformal then Format.pp_print_string fmt "formal" else
+ if x.vglob then Format.pp_print_string fmt "global" else
+ if x.vtemp then Format.pp_print_string fmt "temporary" else
+ Format.pp_print_string fmt "local" ;
+ | _ -> raise Not_found
+ end
+
+let () = Informations.register
+ ~id:"kernel.ast.typeinfo"
+ ~label:"Type"
+ ~title:"Type of C/ASCL expression"
+ begin fun fmt loc ->
+ let open Printer in
+ match loc with
+ | PExp (_, _, e) -> pp_typ fmt (Cil.typeOf e)
+ | PLval (_, _, lval) -> pp_typ fmt (Cil.typeOfLval lval)
+ | PTermLval(_,_,_,lv) -> pp_logic_type fmt (Cil.typeOfTermLval lv)
+ | _ -> raise Not_found
+ end
(* -------------------------------------------------------------------------- *)
(* --- Marker at a position --- *)
diff --git a/src/plugins/server/kernel_ast.mli b/src/plugins/server/kernel_ast.mli
index 448d6f373de..3dd3868e276 100644
--- a/src/plugins/server/kernel_ast.mli
+++ b/src/plugins/server/kernel_ast.mli
@@ -62,6 +62,32 @@ module KfMarker : Data.S with type t = kernel_function * Printer_tag.localizable
module Printer : Printer_tag.S_pp
+(* -------------------------------------------------------------------------- *)
+(** Ast Informations *)
+(* -------------------------------------------------------------------------- *)
+
+module Informations :
+sig
+ (**
+ Registers a marker information printer.
+ Identifier [id] shall be unique.
+ Label [label] shall be very short.
+ Description shall succintly describe the kind of informations.
+ The printer is allowed to raise [Not_found] exception,
+ which is interpreted as there is no information of this kind for
+ the localizable.
+ *)
+ val register :
+ id:string -> label:string -> title:string ->
+ (Format.formatter -> Printer_tag.localizable -> unit) -> unit
+
+ (** Updated informations signal *)
+ val signal : Request.signal
+
+ (** Emits a signal to server clients to reload AST marker informations. *)
+ val update : unit -> unit
+end
+
(* -------------------------------------------------------------------------- *)
(** Globals *)
(* -------------------------------------------------------------------------- *)
--
GitLab