From d5baac56b86aba4de9f28d52c5f6a4e885332878 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Tue, 17 Jan 2023 19:47:49 +0100
Subject: [PATCH] [kernel] nenamed printer-tag api
---
ivette/src/frama-c/kernel/ASTinfo.tsx | 54 +--
ivette/src/frama-c/kernel/ASTview.tsx | 73 +--
ivette/src/frama-c/kernel/Locations.tsx | 4 +-
ivette/src/frama-c/kernel/Properties.tsx | 4 +-
ivette/src/frama-c/kernel/SourceCode.tsx | 10 +-
ivette/src/frama-c/kernel/api/ast/index.ts | 258 ++++------
.../frama-c/kernel/api/properties/index.ts | 36 +-
.../frama-c/plugins/eva/api/general/index.ts | 44 +-
.../frama-c/plugins/eva/api/values/index.ts | 26 +-
ivette/src/frama-c/plugins/eva/valuetable.tsx | 91 ++--
.../plugins/studia/api/studia/index.ts | 12 +-
ivette/src/frama-c/states.ts | 31 ++
src/kernel_services/ast_data/globals.ml | 5 +
src/kernel_services/ast_data/globals.mli | 3 +
.../ast_printing/printer_tag.ml | 59 +--
.../ast_printing/printer_tag.mli | 2 +-
src/plugins/eva/api/general_requests.ml | 4 +-
src/plugins/gui/pretty_source.ml | 6 +-
src/plugins/server/kernel_ast.ml | 456 +++++++++---------
src/plugins/server/kernel_ast.mli | 31 +-
src/plugins/server/kernel_properties.ml | 4 +-
21 files changed, 555 insertions(+), 658 deletions(-)
diff --git a/ivette/src/frama-c/kernel/ASTinfo.tsx b/ivette/src/frama-c/kernel/ASTinfo.tsx
index 332a656b245..72adb6eedde 100644
--- a/ivette/src/frama-c/kernel/ASTinfo.tsx
+++ b/ivette/src/frama-c/kernel/ASTinfo.tsx
@@ -57,38 +57,6 @@ function makeFilter(filter: string): string[] {
return filter.split(':').filter((s) => s.length > 0).sort();
}
-// --------------------------------------------------------------------------
-// --- Marker Kinds
-// --------------------------------------------------------------------------
-
-import Kind = AST.markerKind;
-import Var = AST.markerVar
-
-function getMarkerKind(props: AST.markerInfoData): [string, string] {
- switch (props.kind) {
- case Kind.declaration:
- switch (props.var) {
- case Var.function: return ["Declaration", "Function declaration"];
- case Var.variable: return ["Declaration", "Variable declaration"];
- case Var.none: return ["Declaration", "Declaration"];
- }
- break;
- case Kind.global: return ["Global", "Global declaration or definition"];
- case Kind.lvalue:
- switch (props.var) {
- case Var.function: return ["Function", "Function"];
- case Var.variable: return ["Variable", "C variable"];
- case Var.none: return ["Lvalue", "C lvalue"];
- }
- break;
- case Kind.expression: return ["Expression", "C expression"];
- case Kind.statement: return ["Statement", "C statement"];
- case Kind.property: return ["Property", "ACSL property"];
- case Kind.term: return ["Term", "ACSL term"];
- case Kind.type: return ["Type", "C type"];
- }
-}
-
// --------------------------------------------------------------------------
// --- Information Details
// --------------------------------------------------------------------------
@@ -159,7 +127,7 @@ interface InfoSectionProps {
fct: string | undefined;
scroll: React.RefObject<HTMLDivElement> | undefined;
marker: AST.marker;
- markerInfos: AST.markerInfoData;
+ attrs: AST.markerAttributesData;
scrolled: AST.marker | undefined;
selected: AST.marker | undefined;
hovered: AST.marker | undefined;
@@ -170,9 +138,9 @@ interface InfoSectionProps {
}
function MarkInfos(props: InfoSectionProps): JSX.Element {
- const { marker, markerInfos } = props;
+ const { marker, attrs } = props;
const { fct, scrolled, selected, hovered, excluded } = props;
- const scope = markerInfos.scope ?? fct;
+ const scope = attrs.scope ?? fct;
const foreign = !!scope && fct !== scope;
const [unfold, setUnfold] = React.useState(true);
const [expand, setExpand] = React.useState(false);
@@ -186,9 +154,7 @@ function MarkInfos(props: InfoSectionProps): JSX.Element {
isSelected && 'selected',
isHovered && 'hovered',
);
- const [label, title] = getMarkerKind(markerInfos);
- const name = markerInfos.name;
- const descr = markerInfos.descr ?? `${label} ${name}`;
+ const { labelKind, titleKind, name, descr } = attrs;
const filtered = markerFields.filter((fd) => !excluded.includes(fd.id));
const hasMore = filtered.length < markerFields.length;
const displayed = expand ? markerFields : filtered;
@@ -241,8 +207,8 @@ function MarkInfos(props: InfoSectionProps): JSX.Element {
onClick={onFoldUnfold}
/>
<Code key="NAME" className="astinfo-markercode">
- <span className="astinfo-markerkind" title={title}>
- {label}
+ <span className="astinfo-markerkind" title={titleKind}>
+ {labelKind}
</span> {name}
</Code>
<Code key="SCOPE" className="" display={foreign}>
@@ -317,7 +283,7 @@ export default function ASTinfo(): JSX.Element {
const [setting, setSetting] = Dome.useStringSettings(filterSettings, '');
const [selection] = States.useSelection();
const [hovering] = States.useHovered();
- const allInfos = States.useSyncArray(AST.markerInfo);
+ const attributes = States.useSyncArray(AST.markerAttributes);
const allFields = States.useRequest(AST.getInformation, null) ?? [];
const excluded = React.useMemo(() => makeFilter(setting), [setting]);
Dome.useEvent(States.MetaSelection, (loc: States.Location) => {
@@ -345,15 +311,15 @@ export default function ASTinfo(): JSX.Element {
setMarkers(toggleMarker(markers, marker));
// Mark Rendering
const renderMark = (marker: AST.marker): JSX.Element | null => {
- const markerInfos = allInfos.getData(marker);
- if (!markerInfos) return null;
+ const attrs = attributes.getData(marker);
+ if (!attrs) return null;
return (
<MarkInfos
key={marker}
fct={fct}
scroll={scroll}
marker={marker}
- markerInfos={markerInfos}
+ attrs={attrs}
scrolled={scrolled}
hovered={hovered}
selected={selected}
diff --git a/ivette/src/frama-c/kernel/ASTview.tsx b/ivette/src/frama-c/kernel/ASTview.tsx
index ed3deae15c9..acf1959aabd 100644
--- a/ivette/src/frama-c/kernel/ASTview.tsx
+++ b/ivette/src/frama-c/kernel/ASTview.tsx
@@ -78,8 +78,8 @@ 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; }
+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
@@ -104,6 +104,9 @@ function textToTree(t: text): Tree | undefined {
return res;
}
+// Convert an Ivette text to defined Tree.
+function rootText(t: text): Tree { return textToTree(t) ?? empty; }
+
// 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('');
@@ -113,7 +116,7 @@ function textToString(text: text): string {
// Computes, for each markers of a tree, its range. Returns the map containing
// all those bindings.
-function markersRanges(tree: Tree): Map<string, Range[]>{
+function markersRanges(tree: Tree): Map<string, Range[]> {
const ranges: Map<string, Range[]> = new Map();
const toRanges = (tree: Tree): void => {
if (!isNode(tree)) return;
@@ -156,7 +159,7 @@ 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);
+const Tree = Editor.createAspect({ t: Text }, ({ t }) => rootText(t));
// This aspect computes the markers ranges of the currently displayed function's
// tree, represented by the <Tree> aspect.
@@ -229,7 +232,7 @@ 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 ; });
+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
@@ -421,7 +424,7 @@ type access = 'Reads' | 'Writes';
interface StudiaProps {
marker: string,
- info: Ast.markerInfoData,
+ attrs: Ast.markerAttributesData,
kind: access,
}
@@ -433,11 +436,11 @@ interface StudiaInfos {
}
async function studia(props: StudiaProps): Promise<StudiaInfos> {
- const { marker, info, kind } = props;
+ const { marker, attrs, 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;
+ const lval = attrs.name;
if (locations.length > 0) {
const name = `${kind} of ${lval}`;
const acc = (kind === 'Reads') ? 'accessing' : 'modifying';
@@ -461,7 +464,7 @@ async function studia(props: StudiaProps): Promise<StudiaInfos> {
const Callers = Editor.createField<Eva.CallSite[]>([]);
// This field contains information on markers.
-type GetMarkerData = (key: string) => Ast.markerInfoData | undefined;
+type GetMarkerData = (key: string) => Ast.markerAttributesData | undefined;
const GetMarkerData = Editor.createField<GetMarkerData>(() => undefined);
const ContextMenuHandler = createContextMenuHandler();
@@ -476,34 +479,32 @@ function createContextMenuHandler(): Editor.Extension {
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)
- })
- });
+ const attrs = getData(node.id);
+ if (attrs?.isFunDecl) {
+ 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 ${attrs.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 if (attrs?.isFun) {
+ const location = { fct: attrs.name };
+ const onClick = (): void => update({ location });
+ const label = `Go to definition of ${attrs.name}`;
+ items.push({ label, onClick });
}
- const enabled = info?.kind === 'lvalue' || info?.var === 'variable';
+ const enabled = attrs?.isLval;
const onClick = (kind: access): void => {
- if (info && node.id)
- studia({ marker: node.id, info, kind }).then(update);
+ if (attrs && node.id)
+ studia({ marker: node.id, attrs, kind }).then(update);
};
const reads = 'Studia: select reads';
const writes = 'Studia: select writes';
@@ -653,7 +654,7 @@ export default function ASTview(): JSX.Element {
React.useEffect(() => Tags.set(view, tags), [view, tags]);
// Updating CodeMirror when the <markersInfo> synchronized array is changed.
- const info = States.useSyncArray(Ast.markerInfo);
+ const info = States.useSyncArray(Ast.markerAttributes);
const getData = React.useCallback((key) => info.getData(key), [info]);
React.useEffect(() => GetMarkerData.set(view, getData), [view, getData]);
@@ -688,7 +689,7 @@ export default function ASTview(): JSX.Element {
/>
<Inset />
</TitleBar>
- <Component style={{ fontSize: `${fontSize}px`}} />
+ <Component style={{ fontSize: `${fontSize}px` }} />
</>
);
}
diff --git a/ivette/src/frama-c/kernel/Locations.tsx b/ivette/src/frama-c/kernel/Locations.tsx
index ba048e57111..7f955a475a6 100644
--- a/ivette/src/frama-c/kernel/Locations.tsx
+++ b/ivette/src/frama-c/kernel/Locations.tsx
@@ -34,7 +34,7 @@ import { Label } from 'dome/controls/labels';
import { IconButton } from 'dome/controls/buttons';
import { Space } from 'dome/frame/toolbars';
import { TitleBar } from 'ivette';
-import { markerInfo } from 'frama-c/kernel/api/ast';
+import { markerAttributes } from 'frama-c/kernel/api/ast';
// --------------------------------------------------------------------------
// --- Locations Panel
@@ -51,7 +51,7 @@ export default function LocationsTable(): JSX.Element {
), []);
const multipleSelections = selection?.multiple;
const numberOfSelections = multipleSelections?.allSelections?.length;
- const markersInfo = States.useSyncArray(markerInfo);
+ const markersInfo = States.useSyncArray(markerAttributes);
// Renderer for statement markers.
const renderMarker: Renderer<string> =
diff --git a/ivette/src/frama-c/kernel/Properties.tsx b/ivette/src/frama-c/kernel/Properties.tsx
index 5034f8671cc..546732eb09f 100644
--- a/ivette/src/frama-c/kernel/Properties.tsx
+++ b/ivette/src/frama-c/kernel/Properties.tsx
@@ -206,7 +206,7 @@ function filterEva(p: Property): boolean {
case 'not_tainted':
case 'not_applicable':
return !filter('eva.data_tainted_only') &&
- !filter('eva.ctrl_tainted_only');
+ !filter('eva.ctrl_tainted_only');
case 'direct_taint':
return !(filter('eva.ctrl_tainted_only'));
case 'indirect_taint':
@@ -333,7 +333,7 @@ const byColumn: Arrays.ByColumns<Property> = {
};
class PropertyModel
- extends Arrays.CompactModel<Json.key<'#property'>, Property> {
+ extends Arrays.CompactModel<Json.key<'#marker'>, Property> {
private filterFun?: string;
diff --git a/ivette/src/frama-c/kernel/SourceCode.tsx b/ivette/src/frama-c/kernel/SourceCode.tsx
index cc059c919a4..cf2eed18e59 100644
--- a/ivette/src/frama-c/kernel/SourceCode.tsx
+++ b/ivette/src/frama-c/kernel/SourceCode.tsx
@@ -142,7 +142,7 @@ function createSyncOnUserSelection(): Editor.Extension {
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);
+ await Server.send(Ast.reloadMarkerAttributes, null);
const location = { fct, marker };
update({ location });
Locations.set(view, { cursor: location, ivette: location });
@@ -188,7 +188,7 @@ function createContextMenu(): Editor.Extension {
if (file === '') return;
const label = 'Open file in an external editor';
const pos = getCursorPosition(view);
- Dome.popupMenu([ { label, onClick: () => edit(file, pos, command) } ]);
+ Dome.popupMenu([{ label, onClick: () => edit(file, pos, command) }]);
},
});
}
@@ -210,15 +210,15 @@ function useFctSource(file: string): string {
// Build a callback that retrieves a location's source information.
function useSourceGetter(): GetSource {
- const markersInfo = States.useSyncArray(Ast.markerInfo);
+ const attributes = States.useSyncArray(Ast.markerAttributes);
const functionsData = States.useSyncArray(Ast.functions).getArray();
return React.useCallback(({ fct, marker }) => {
const markerSloc = (marker !== undefined && marker !== '') ?
- markersInfo.getData(marker)?.sloc : undefined;
+ attributes.getData(marker)?.sloc : undefined;
const fctSloc = (fct !== undefined && fct !== '') ?
functionsData.find((e) => e.name === fct)?.sloc : undefined;
return markerSloc ?? fctSloc;
- }, [markersInfo, functionsData]);
+ }, [attributes, functionsData]);
}
// -----------------------------------------------------------------------------
diff --git a/ivette/src/frama-c/kernel/api/ast/index.ts b/ivette/src/frama-c/kernel/api/ast/index.ts
index 093da142747..7cbd4af0072 100644
--- a/ivette/src/frama-c/kernel/api/ast/index.ts
+++ b/ivette/src/frama-c/kernel/api/ast/index.ts
@@ -37,17 +37,11 @@ import * as Server from 'frama-c/server';
//@ts-ignore
import * as State from 'frama-c/states';
-//@ts-ignore
-import { byTag } from 'frama-c/kernel/api/data';
//@ts-ignore
import { byText } from 'frama-c/kernel/api/data';
//@ts-ignore
-import { jTag } from 'frama-c/kernel/api/data';
-//@ts-ignore
import { jText } from 'frama-c/kernel/api/data';
//@ts-ignore
-import { tag } from 'frama-c/kernel/api/data';
-//@ts-ignore
import { text } from 'frama-c/kernel/api/data';
const compute_internal: Server.ExecRequest<null,null> = {
@@ -88,206 +82,140 @@ export const bySource: Compare.Order<source> =
line: Compare.number,
});
-/** Marker kind */
-export enum markerKind {
- /** Expression */
- expression = 'expression',
- /** Lvalue */
- lvalue = 'lvalue',
- /** Declaration */
- declaration = 'declaration',
- /** Statement */
- statement = 'statement',
- /** Global */
- global = 'global',
- /** Term */
- term = 'term',
- /** Property */
- property = 'property',
- /** Type */
- type = 'type',
-}
+/** Localizable AST markers */
+export type marker = Json.key<'#marker'>;
-/** Decoder for `markerKind` */
-export const jMarkerKind: Json.Decoder<markerKind> = Json.jEnum(markerKind);
+/** Decoder for `marker` */
+export const jMarker: Json.Decoder<marker> = Json.jKey<'#marker'>('#marker');
-/** Natural order for `markerKind` */
-export const byMarkerKind: Compare.Order<markerKind> =
- Compare.byEnum(markerKind);
+/** Natural order for `marker` */
+export const byMarker: Compare.Order<marker> = Compare.string;
-const markerKindTags_internal: Server.GetRequest<null,tag[]> = {
- kind: Server.RqKind.GET,
- name: 'kernel.ast.markerKindTags',
- input: Json.jNull,
- output: Json.jArray(jTag),
- signals: [],
-};
-/** Registered tags for the above type. */
-export const markerKindTags: Server.GetRequest<null,tag[]>= markerKindTags_internal;
-
-/** Marker variable */
-export enum markerVar {
- /** None */
- none = 'none',
- /** Variable */
- variable = 'variable',
+/** Location: function and marker */
+export interface location {
/** Function */
- function = 'function',
+ fct: Json.key<'#fct'>;
+ /** Marker */
+ marker: marker;
}
-/** Decoder for `markerVar` */
-export const jMarkerVar: Json.Decoder<markerVar> = Json.jEnum(markerVar);
-
-/** Natural order for `markerVar` */
-export const byMarkerVar: Compare.Order<markerVar> =
- Compare.byEnum(markerVar);
+/** Decoder for `location` */
+export const jLocation: Json.Decoder<location> =
+ Json.jObject({ fct: Json.jKey<'#fct'>('#fct'), marker: jMarker,});
-const markerVarTags_internal: Server.GetRequest<null,tag[]> = {
- kind: Server.RqKind.GET,
- name: 'kernel.ast.markerVarTags',
- input: Json.jNull,
- output: Json.jArray(jTag),
- signals: [],
-};
-/** Registered tags for the above type. */
-export const markerVarTags: Server.GetRequest<null,tag[]>= markerVarTags_internal;
+/** Natural order for `location` */
+export const byLocation: Compare.Order<location> =
+ Compare.byFields
+ <{ fct: Json.key<'#fct'>, marker: marker }>({
+ fct: Compare.string,
+ marker: byMarker,
+ });
-/** Data for array rows [`markerInfo`](#markerinfo) */
-export interface markerInfoData {
+/** Data for array rows [`markerAttributes`](#markerattributes) */
+export interface markerAttributesData {
/** Entry identifier. */
key: string;
- /** Marker kind */
- kind: markerKind;
- /** Marker variable */
- var: markerVar;
+ /** Marker kind (short) */
+ labelKind: string;
+ /** Marker kind (long) */
+ titleKind: string;
/** Marker short name */
name: string;
/** Marker declaration or description */
descr: string;
+ /** Whether it is an l-value */
+ isLval: boolean;
+ /** Whether it is a function declaration or definition */
+ isFunDecl: boolean;
+ /** Whether it is a function symbol */
+ isFun: boolean;
/** Function scope of the marker, if applicable */
scope?: string;
/** Source location */
sloc: source;
}
-/** Decoder for `markerInfoData` */
-export const jMarkerInfoData: Json.Decoder<markerInfoData> =
+/** Decoder for `markerAttributesData` */
+export const jMarkerAttributesData: Json.Decoder<markerAttributesData> =
Json.jObject({
key: Json.jString,
- kind: jMarkerKind,
- var: jMarkerVar,
+ labelKind: Json.jString,
+ titleKind: Json.jString,
name: Json.jString,
descr: Json.jString,
+ isLval: Json.jBoolean,
+ isFunDecl: Json.jBoolean,
+ isFun: Json.jBoolean,
scope: Json.jOption(Json.jString),
sloc: jSource,
});
-/** Natural order for `markerInfoData` */
-export const byMarkerInfoData: Compare.Order<markerInfoData> =
+/** Natural order for `markerAttributesData` */
+export const byMarkerAttributesData: Compare.Order<markerAttributesData> =
Compare.byFields
- <{ key: string, kind: markerKind, var: markerVar, name: string,
- descr: string, scope?: string, sloc: source }>({
+ <{ key: string, labelKind: string, titleKind: string, name: string,
+ descr: string, isLval: boolean, isFunDecl: boolean, isFun: boolean,
+ scope?: string, sloc: source }>({
key: Compare.string,
- kind: byMarkerKind,
- var: byMarkerVar,
+ labelKind: Compare.alpha,
+ titleKind: Compare.alpha,
name: Compare.alpha,
descr: Compare.string,
+ isLval: Compare.boolean,
+ isFunDecl: Compare.boolean,
+ isFun: Compare.boolean,
scope: Compare.defined(Compare.string),
sloc: bySource,
});
-/** Signal for array [`markerInfo`](#markerinfo) */
-export const signalMarkerInfo: Server.Signal = {
- name: 'kernel.ast.signalMarkerInfo',
+/** Signal for array [`markerAttributes`](#markerattributes) */
+export const signalMarkerAttributes: Server.Signal = {
+ name: 'kernel.ast.signalMarkerAttributes',
};
-const reloadMarkerInfo_internal: Server.GetRequest<null,null> = {
+const reloadMarkerAttributes_internal: Server.GetRequest<null,null> = {
kind: Server.RqKind.GET,
- name: 'kernel.ast.reloadMarkerInfo',
+ name: 'kernel.ast.reloadMarkerAttributes',
input: Json.jNull,
output: Json.jNull,
signals: [],
};
-/** Force full reload for array [`markerInfo`](#markerinfo) */
-export const reloadMarkerInfo: Server.GetRequest<null,null>= reloadMarkerInfo_internal;
+/** Force full reload for array [`markerAttributes`](#markerattributes) */
+export const reloadMarkerAttributes: Server.GetRequest<null,null>= reloadMarkerAttributes_internal;
-const fetchMarkerInfo_internal: Server.GetRequest<
+const fetchMarkerAttributes_internal: Server.GetRequest<
number,
- { pending: number, updated: markerInfoData[], removed: string[],
+ { pending: number, updated: markerAttributesData[], removed: string[],
reload: boolean }
> = {
kind: Server.RqKind.GET,
- name: 'kernel.ast.fetchMarkerInfo',
+ name: 'kernel.ast.fetchMarkerAttributes',
input: Json.jNumber,
output: Json.jObject({
pending: Json.jNumber,
- updated: Json.jArray(jMarkerInfoData),
+ updated: Json.jArray(jMarkerAttributesData),
removed: Json.jArray(Json.jString),
reload: Json.jBoolean,
}),
signals: [],
};
-/** Data fetcher for array [`markerInfo`](#markerinfo) */
-export const fetchMarkerInfo: Server.GetRequest<
+/** Data fetcher for array [`markerAttributes`](#markerattributes) */
+export const fetchMarkerAttributes: Server.GetRequest<
number,
- { pending: number, updated: markerInfoData[], removed: string[],
+ { pending: number, updated: markerAttributesData[], removed: string[],
reload: boolean }
- >= fetchMarkerInfo_internal;
-
-const markerInfo_internal: State.Array<string,markerInfoData> = {
- name: 'kernel.ast.markerInfo',
- getkey: ((d:markerInfoData) => d.key),
- signal: signalMarkerInfo,
- fetch: fetchMarkerInfo,
- reload: reloadMarkerInfo,
- order: byMarkerInfoData,
+ >= fetchMarkerAttributes_internal;
+
+const markerAttributes_internal: State.Array<string,markerAttributesData> = {
+ name: 'kernel.ast.markerAttributes',
+ getkey: ((d:markerAttributesData) => d.key),
+ signal: signalMarkerAttributes,
+ fetch: fetchMarkerAttributes,
+ reload: reloadMarkerAttributes,
+ order: byMarkerAttributesData,
};
-/** Marker information */
-export const markerInfo: State.Array<string,markerInfoData> = markerInfo_internal;
-
-/** Localizable AST markers */
-export type marker =
- Json.key<'#stmt'> | Json.key<'#decl'> | Json.key<'#lval'> |
- Json.key<'#expr'> | Json.key<'#term'> | Json.key<'#global'> |
- Json.key<'#property'> | Json.key<'#type'>;
-
-/** Decoder for `marker` */
-export const jMarker: Json.Decoder<marker> =
- Json.jUnion<Json.key<'#stmt'> | Json.key<'#decl'> | Json.key<'#lval'> |
- Json.key<'#expr'> | Json.key<'#term'> | Json.key<'#global'> |
- Json.key<'#property'> | Json.key<'#type'>>(
- Json.jKey<'#stmt'>('#stmt'),
- Json.jKey<'#decl'>('#decl'),
- Json.jKey<'#lval'>('#lval'),
- Json.jKey<'#expr'>('#expr'),
- Json.jKey<'#term'>('#term'),
- Json.jKey<'#global'>('#global'),
- Json.jKey<'#property'>('#property'),
- Json.jKey<'#type'>('#type'),
- );
-
-/** Natural order for `marker` */
-export const byMarker: Compare.Order<marker> = Compare.structural;
-
-/** Location: function and marker */
-export interface location {
- /** Function */
- fct: Json.key<'#fct'>;
- /** Marker */
- marker: marker;
-}
-
-/** Decoder for `location` */
-export const jLocation: Json.Decoder<location> =
- Json.jObject({ fct: Json.jKey<'#fct'>('#fct'), marker: jMarker,});
-
-/** Natural order for `location` */
-export const byLocation: Compare.Order<location> =
- Compare.byFields
- <{ fct: Json.key<'#fct'>, marker: marker }>({
- fct: Compare.string,
- marker: byMarker,
- });
+/** Marker attributes */
+export const markerAttributes: State.Array<string,markerAttributesData> = markerAttributes_internal;
const getMainFunction_internal: Server.GetRequest<
null,
@@ -494,42 +422,22 @@ const setFiles_internal: Server.SetRequest<string[],null> = {
/** Set the source file names to analyze. */
export const setFiles: Server.SetRequest<string[],null>= setFiles_internal;
-/** <markerFromTerm> input */
-export interface markerFromTermInput {
- /** The statement at which we will build the marker. */
- atStmt: marker;
- /** The ACSL term. */
- term: string;
-}
-
-/** Decoder for `markerFromTermInput` */
-export const jMarkerFromTermInput: Json.Decoder<markerFromTermInput> =
- Json.jObject({ atStmt: jMarker, term: Json.jString,});
-
-/** Natural order for `markerFromTermInput` */
-export const byMarkerFromTermInput: Compare.Order<markerFromTermInput> =
- Compare.byFields
- <{ atStmt: marker, term: string }>({
- atStmt: byMarker,
- term: Compare.string,
- });
-
-const markerFromTerm_internal: Server.GetRequest<
- markerFromTermInput,
+const parseTerm_internal: Server.GetRequest<
+ { term: string, stmt: marker },
marker |
undefined
> = {
kind: Server.RqKind.GET,
- name: 'kernel.ast.markerFromTerm',
- input: jMarkerFromTermInput,
+ name: 'kernel.ast.parseTerm',
+ input: Json.jObject({ term: Json.jString, stmt: jMarker,}),
output: Json.jOption(jMarker),
signals: [],
};
-/** Build a marker from an ACSL term. */
-export const markerFromTerm: Server.GetRequest<
- markerFromTermInput,
+/** Parse an ACSL Term and returns the associated marker */
+export const parseTerm: Server.GetRequest<
+ { term: string, stmt: marker },
marker |
undefined
- >= markerFromTerm_internal;
+ >= parseTerm_internal;
/* ------------------------------------- */
diff --git a/ivette/src/frama-c/kernel/api/properties/index.ts b/ivette/src/frama-c/kernel/api/properties/index.ts
index fbbd717805e..ab774d1f222 100644
--- a/ivette/src/frama-c/kernel/api/properties/index.ts
+++ b/ivette/src/frama-c/kernel/api/properties/index.ts
@@ -37,11 +37,17 @@ import * as Server from 'frama-c/server';
//@ts-ignore
import * as State from 'frama-c/states';
+//@ts-ignore
+import { byMarker } from 'frama-c/kernel/api/ast';
//@ts-ignore
import { bySource } from 'frama-c/kernel/api/ast';
//@ts-ignore
+import { jMarker } from 'frama-c/kernel/api/ast';
+//@ts-ignore
import { jSource } from 'frama-c/kernel/api/ast';
//@ts-ignore
+import { marker } from 'frama-c/kernel/api/ast';
+//@ts-ignore
import { source } from 'frama-c/kernel/api/ast';
//@ts-ignore
import { byTag } from 'frama-c/kernel/api/data';
@@ -238,7 +244,7 @@ export const alarmsTags: Server.GetRequest<null,tag[]>= alarmsTags_internal;
/** Data for array rows [`status`](#status) */
export interface statusData {
/** Entry identifier. */
- key: Json.key<'#property'>;
+ key: marker;
/** Full description */
descr: string;
/** Kind */
@@ -250,7 +256,7 @@ export interface statusData {
/** Function */
fct?: Json.key<'#fct'>;
/** Instruction */
- kinstr?: Json.key<'#stmt'>;
+ kinstr?: marker;
/** Position */
source: source;
/** Alarm name (if the property is an alarm) */
@@ -264,13 +270,13 @@ export interface statusData {
/** Decoder for `statusData` */
export const jStatusData: Json.Decoder<statusData> =
Json.jObject({
- key: Json.jKey<'#property'>('#property'),
+ key: jMarker,
descr: Json.jString,
kind: jPropKind,
names: Json.jArray(Json.jString),
status: jPropStatus,
fct: Json.jOption(Json.jKey<'#fct'>('#fct')),
- kinstr: Json.jOption(Json.jKey<'#stmt'>('#stmt')),
+ kinstr: Json.jOption(jMarker),
source: jSource,
alarm: Json.jOption(Json.jString),
alarm_descr: Json.jOption(Json.jString),
@@ -280,17 +286,17 @@ export const jStatusData: Json.Decoder<statusData> =
/** Natural order for `statusData` */
export const byStatusData: Compare.Order<statusData> =
Compare.byFields
- <{ key: Json.key<'#property'>, descr: string, kind: propKind,
- names: string[], status: propStatus, fct?: Json.key<'#fct'>,
- kinstr?: Json.key<'#stmt'>, source: source, alarm?: string,
- alarm_descr?: string, predicate?: string }>({
- key: Compare.string,
+ <{ key: marker, descr: string, kind: propKind, names: string[],
+ status: propStatus, fct?: Json.key<'#fct'>, kinstr?: marker,
+ source: source, alarm?: string, alarm_descr?: string,
+ predicate?: string }>({
+ key: byMarker,
descr: Compare.string,
kind: byPropKind,
names: Compare.array(Compare.string),
status: byPropStatus,
fct: Compare.defined(Compare.string),
- kinstr: Compare.defined(Compare.string),
+ kinstr: Compare.defined(byMarker),
source: bySource,
alarm: Compare.defined(Compare.string),
alarm_descr: Compare.defined(Compare.string),
@@ -314,7 +320,7 @@ export const reloadStatus: Server.GetRequest<null,null>= reloadStatus_internal;
const fetchStatus_internal: Server.GetRequest<
number,
- { pending: number, updated: statusData[], removed: Json.key<'#property'>[],
+ { pending: number, updated: statusData[], removed: marker[],
reload: boolean }
> = {
kind: Server.RqKind.GET,
@@ -323,7 +329,7 @@ const fetchStatus_internal: Server.GetRequest<
output: Json.jObject({
pending: Json.jNumber,
updated: Json.jArray(jStatusData),
- removed: Json.jArray(Json.jKey<'#property'>('#property')),
+ removed: Json.jArray(jMarker),
reload: Json.jBoolean,
}),
signals: [],
@@ -331,11 +337,11 @@ const fetchStatus_internal: Server.GetRequest<
/** Data fetcher for array [`status`](#status) */
export const fetchStatus: Server.GetRequest<
number,
- { pending: number, updated: statusData[], removed: Json.key<'#property'>[],
+ { pending: number, updated: statusData[], removed: marker[],
reload: boolean }
>= fetchStatus_internal;
-const status_internal: State.Array<Json.key<'#property'>,statusData> = {
+const status_internal: State.Array<marker,statusData> = {
name: 'kernel.properties.status',
getkey: ((d:statusData) => d.key),
signal: signalStatus,
@@ -344,6 +350,6 @@ const status_internal: State.Array<Json.key<'#property'>,statusData> = {
order: byStatusData,
};
/** Status of Registered Properties */
-export const status: State.Array<Json.key<'#property'>,statusData> = status_internal;
+export const status: State.Array<marker,statusData> = status_internal;
/* ------------------------------------- */
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 85c3985681b..1ccceb03887 100644
--- a/ivette/src/frama-c/plugins/eva/api/general/index.ts
+++ b/ivette/src/frama-c/plugins/eva/api/general/index.ts
@@ -99,22 +99,19 @@ export interface CallSite {
/** Function */
kf: Json.key<'#fct'>;
/** Statement */
- stmt: Json.key<'#stmt'>;
+ stmt: marker;
}
/** Decoder for `CallSite` */
export const jCallSite: Json.Decoder<CallSite> =
- Json.jObject({
- kf: Json.jKey<'#fct'>('#fct'),
- stmt: Json.jKey<'#stmt'>('#stmt'),
- });
+ Json.jObject({ kf: Json.jKey<'#fct'>('#fct'), stmt: jMarker,});
/** Natural order for `CallSite` */
export const byCallSite: Compare.Order<CallSite> =
Compare.byFields
- <{ kf: Json.key<'#fct'>, stmt: Json.key<'#stmt'> }>({
+ <{ kf: Json.key<'#fct'>, stmt: marker }>({
kf: Compare.string,
- stmt: Compare.string,
+ stmt: byMarker,
});
const getCallers_internal: Server.GetRequest<Json.key<'#fct'>,CallSite[]> = {
@@ -273,20 +270,20 @@ export const taintStatusTags: Server.GetRequest<null,tag[]>= taintStatusTags_int
/** Lvalue taint status */
export interface LvalueTaints {
/** tainted lvalue */
- lval: Json.key<'#lval'>;
+ lval: marker;
/** taint status */
taint: taintStatus;
}
/** Decoder for `LvalueTaints` */
export const jLvalueTaints: Json.Decoder<LvalueTaints> =
- Json.jObject({ lval: Json.jKey<'#lval'>('#lval'), taint: jTaintStatus,});
+ Json.jObject({ lval: jMarker, taint: jTaintStatus,});
/** Natural order for `LvalueTaints` */
export const byLvalueTaints: Compare.Order<LvalueTaints> =
Compare.byFields
- <{ lval: Json.key<'#lval'>, taint: taintStatus }>({
- lval: Compare.string,
+ <{ lval: marker, taint: taintStatus }>({
+ lval: byMarker,
taint: byTaintStatus,
});
@@ -309,7 +306,7 @@ export const taintedLvalues: Server.GetRequest<
/** Data for array rows [`properties`](#properties) */
export interface propertiesData {
/** Entry identifier. */
- key: Json.key<'#property'>;
+ key: marker;
/** Is the property invalid in some context of the analysis? */
priority: boolean;
/** Is the property tainted according to the Eva taint domain? */
@@ -318,17 +315,14 @@ export interface propertiesData {
/** Decoder for `propertiesData` */
export const jPropertiesData: Json.Decoder<propertiesData> =
- Json.jObject({
- key: Json.jKey<'#property'>('#property'),
- priority: Json.jBoolean,
- taint: jTaintStatus,
+ Json.jObject({ key: jMarker, priority: Json.jBoolean, taint: jTaintStatus,
});
/** Natural order for `propertiesData` */
export const byPropertiesData: Compare.Order<propertiesData> =
Compare.byFields
- <{ key: Json.key<'#property'>, priority: boolean, taint: taintStatus }>({
- key: Compare.string,
+ <{ key: marker, priority: boolean, taint: taintStatus }>({
+ key: byMarker,
priority: Compare.boolean,
taint: byTaintStatus,
});
@@ -350,8 +344,8 @@ export const reloadProperties: Server.GetRequest<null,null>= reloadProperties_in
const fetchProperties_internal: Server.GetRequest<
number,
- { pending: number, updated: propertiesData[],
- removed: Json.key<'#property'>[], reload: boolean }
+ { pending: number, updated: propertiesData[], removed: marker[],
+ reload: boolean }
> = {
kind: Server.RqKind.GET,
name: 'plugins.eva.general.fetchProperties',
@@ -359,7 +353,7 @@ const fetchProperties_internal: Server.GetRequest<
output: Json.jObject({
pending: Json.jNumber,
updated: Json.jArray(jPropertiesData),
- removed: Json.jArray(Json.jKey<'#property'>('#property')),
+ removed: Json.jArray(jMarker),
reload: Json.jBoolean,
}),
signals: [],
@@ -367,11 +361,11 @@ const fetchProperties_internal: Server.GetRequest<
/** Data fetcher for array [`properties`](#properties) */
export const fetchProperties: Server.GetRequest<
number,
- { pending: number, updated: propertiesData[],
- removed: Json.key<'#property'>[], reload: boolean }
+ { pending: number, updated: propertiesData[], removed: marker[],
+ reload: boolean }
>= fetchProperties_internal;
-const properties_internal: State.Array<Json.key<'#property'>,propertiesData> = {
+const properties_internal: State.Array<marker,propertiesData> = {
name: 'plugins.eva.general.properties',
getkey: ((d:propertiesData) => d.key),
signal: signalProperties,
@@ -380,7 +374,7 @@ const properties_internal: State.Array<Json.key<'#property'>,propertiesData> = {
order: byPropertiesData,
};
/** Status of Registered Properties */
-export const properties: State.Array<Json.key<'#property'>,propertiesData> = properties_internal;
+export const properties: State.Array<marker,propertiesData> = properties_internal;
/** The alarms are counted after being grouped by these categories */
export enum alarmCategory {
diff --git a/ivette/src/frama-c/plugins/eva/api/values/index.ts b/ivette/src/frama-c/plugins/eva/api/values/index.ts
index 2519fa6327d..fdb7cf5397b 100644
--- a/ivette/src/frama-c/plugins/eva/api/values/index.ts
+++ b/ivette/src/frama-c/plugins/eva/api/values/index.ts
@@ -70,8 +70,8 @@ export const getCallstacks: Server.GetRequest<marker[],callstack[]>= getCallstac
const getCallstackInfo_internal: Server.GetRequest<
callstack,
- { callee: Json.key<'#fct'>, caller?: Json.key<'#fct'>,
- stmt?: Json.key<'#stmt'>, rank?: number }[]
+ { callee: Json.key<'#fct'>, caller?: Json.key<'#fct'>, stmt?: marker,
+ rank?: number }[]
> = {
kind: Server.RqKind.GET,
name: 'plugins.eva.values.getCallstackInfo',
@@ -80,7 +80,7 @@ const getCallstackInfo_internal: Server.GetRequest<
Json.jObject({
callee: Json.jKey<'#fct'>('#fct'),
caller: Json.jOption(Json.jKey<'#fct'>('#fct')),
- stmt: Json.jOption(Json.jKey<'#stmt'>('#stmt')),
+ stmt: Json.jOption(jMarker),
rank: Json.jOption(Json.jNumber),
})),
signals: [],
@@ -88,31 +88,31 @@ const getCallstackInfo_internal: Server.GetRequest<
/** Callstack Description */
export const getCallstackInfo: Server.GetRequest<
callstack,
- { callee: Json.key<'#fct'>, caller?: Json.key<'#fct'>,
- stmt?: Json.key<'#stmt'>, rank?: number }[]
+ { callee: Json.key<'#fct'>, caller?: Json.key<'#fct'>, stmt?: marker,
+ rank?: number }[]
>= getCallstackInfo_internal;
const getStmtInfo_internal: Server.GetRequest<
- Json.key<'#stmt'>,
+ marker,
{ rank: number, fct: Json.key<'#fct'> }
> = {
kind: Server.RqKind.GET,
name: 'plugins.eva.values.getStmtInfo',
- input: Json.jKey<'#stmt'>('#stmt'),
+ input: jMarker,
output: Json.jObject({ rank: Json.jNumber, fct: Json.jKey<'#fct'>('#fct'),
}),
signals: [],
};
/** Stmt Information */
export const getStmtInfo: Server.GetRequest<
- Json.key<'#stmt'>,
+ marker,
{ rank: number, fct: Json.key<'#fct'> }
>= getStmtInfo_internal;
const getProbeInfo_internal: Server.GetRequest<
marker,
- { condition: boolean, effects: boolean, rank: number,
- stmt?: Json.key<'#stmt'>, code?: string, evaluable: boolean }
+ { condition: boolean, effects: boolean, rank: number, stmt?: marker,
+ code?: string, evaluable: boolean }
> = {
kind: Server.RqKind.GET,
name: 'plugins.eva.values.getProbeInfo',
@@ -121,7 +121,7 @@ const getProbeInfo_internal: Server.GetRequest<
condition: Json.jBoolean,
effects: Json.jBoolean,
rank: Json.jNumber,
- stmt: Json.jOption(Json.jKey<'#stmt'>('#stmt')),
+ stmt: Json.jOption(jMarker),
code: Json.jOption(Json.jString),
evaluable: Json.jBoolean,
}),
@@ -130,8 +130,8 @@ const getProbeInfo_internal: Server.GetRequest<
/** Probe informations */
export const getProbeInfo: Server.GetRequest<
marker,
- { condition: boolean, effects: boolean, rank: number,
- stmt?: Json.key<'#stmt'>, code?: string, evaluable: boolean }
+ { condition: boolean, effects: boolean, rank: number, stmt?: marker,
+ code?: string, evaluable: boolean }
>= getProbeInfo_internal;
/** Evaluation of an expression or lvalue */
diff --git a/ivette/src/frama-c/plugins/eva/valuetable.tsx b/ivette/src/frama-c/plugins/eva/valuetable.tsx
index a89b9ee1207..5e103a1f5aa 100644
--- a/ivette/src/frama-c/plugins/eva/valuetable.tsx
+++ b/ivette/src/frama-c/plugins/eva/valuetable.tsx
@@ -49,7 +49,7 @@ import { ipcRenderer } from 'electron';
type Request<A, B> = (a: A) => Promise<B>;
-type Alarm = [ 'True' | 'False' | 'Unknown', string ]
+type Alarm = ['True' | 'False' | 'Unknown', string]
function getAlarmStatus(alarms: Alarm[] | undefined): string {
if (!alarms) return 'none';
if (alarms.length === 0) return 'none';
@@ -57,19 +57,19 @@ function getAlarmStatus(alarms: Alarm[] | undefined): string {
else return 'Unknown';
}
-type MarkerTracked = [ 'Tracked', boolean ]
-type MarkerPinned = [ 'Pinned' , boolean ]
-type MarkerStatus = MarkerTracked | MarkerPinned | 'JustFocused'
+type MarkerTracked = ['Tracked', boolean]
+type MarkerPinned = ['Pinned', boolean]
+type MarkerStatus = MarkerTracked | MarkerPinned | 'JustFocused'
function MarkerStatusClass(status: MarkerStatus): string {
if (status === 'JustFocused') return 'eva-header-just-focused';
- const [ kind, focused ] = status;
+ const [kind, focused] = status;
return 'eva-header-' + kind.toLowerCase() + (focused ? '-focused' : '');
}
function isPinnedMarker(status: MarkerStatus): boolean {
if (status === 'JustFocused') return false;
- const [ kind ] = status;
+ const [kind] = status;
return kind === 'Pinned';
}
@@ -84,7 +84,7 @@ function TableCell(props: TableCellProps): JSX.Element {
const leftVisible = align === 'center' ? 'block' : 'none';
return (
<div className='eva-cell-container'>
- <div className='eva-cell-left' style={{ display: leftVisible }}/>
+ <div className='eva-cell-left' style={{ display: leftVisible }} />
<div className='eva-cell-content'>
{children}
</div>
@@ -177,12 +177,12 @@ interface Probe extends Location {
}
/* Builds a cached version of the `getValues` request */
-function useEvaluationCache(): Request<[ Location, callstack ], Evaluation> {
- type LocStack = [ Location, callstack ];
- const toString = React.useCallback(([ l, c ] : LocStack): string => {
+function useEvaluationCache(): Request<[Location, callstack], Evaluation> {
+ type LocStack = [Location, callstack];
+ const toString = React.useCallback(([l, c]: LocStack): string => {
return `${l.fct}:${l.target}:${c}`;
}, []);
- const get: Request<LocStack, Evaluation> = React.useCallback(([ l, c ]) => {
+ const get: Request<LocStack, Evaluation> = React.useCallback(([l, c]) => {
const callstack = c === 'Summary' ? undefined : c;
return Server.send(Values.getValues, { ...l, callstack });
}, []);
@@ -195,9 +195,9 @@ function useProbeCache(): Request<Location, Probe> {
const cache = useEvaluationCache();
const get = React.useCallback(async (loc: Location): Promise<Probe> => {
const infos = await Server.send(Values.getProbeInfo, loc.target);
- const evaluate: Request<callstack, Evaluation> = (c) => cache([ loc, c ]);
+ const evaluate: Request<callstack, Evaluation> = (c) => cache([loc, c]);
return { ...loc, ...infos, evaluate };
- }, [ cache ]);
+ }, [cache]);
return Dome.useCache(get, toString);
}
@@ -215,16 +215,13 @@ interface StmtProps {
short?: boolean;
}
-function Stmt(props: StmtProps): JSX.Element {
- const markersInfo = States.useSyncArray(Ast.markerInfo);
+function Stmt(props: StmtProps): JSX.Element | null {
const { stmt, marker, short } = props;
- if (!stmt || !marker) return <></>;
- const line = markersInfo.getData(marker)?.sloc?.line;
- const filename = markersInfo.getData(marker)?.sloc?.base;
- const title = markersInfo.getData(stmt)?.descr;
- const text = short ? `@L${line}` : `@${filename}:${line}`;
+ const { descr, sloc: { base, line } } = States.useMarker(marker);
+ if (!stmt || !marker) return null;
+ const label = short ? `@L${line}` : `@${base}:${line}`;
const className = 'dome-text-cell eva-stmt';
- return <span className={className} title={title}>{text}</span>;
+ return <span className={className} title={descr}>{label}</span>;
}
/* -------------------------------------------------------------------------- */
@@ -345,7 +342,7 @@ function ProbeHeader(props: ProbeHeaderProps): JSX.Element {
const isPinned = isPinnedMarker(status);
const pinText = isPinned ? 'Unpin' : 'Pin';
- const loc: States.SelectionActions = { location: { fct, marker: target} };
+ const loc: States.SelectionActions = { location: { fct, marker: target } };
const onClick = (): void => { setSelection(loc); selectProbe(); };
const onDoubleClick = (): void => pinProbe(!isPinned);
const onContextMenu = (): void => {
@@ -373,7 +370,7 @@ function ProbeHeader(props: ProbeHeaderProps): JSX.Element {
onClick={() => removeProbe()}
/>
</div>;
-
+
return (
<th
ref={ref}
@@ -387,7 +384,7 @@ function ProbeHeader(props: ProbeHeaderProps): JSX.Element {
<div className='eva-header-text-overflow'>
<span className='dome-text-cell' title={code}>{code}</span>
</div>
- <Stmt stmt={stmt} marker={target} short={true}/>
+ <Stmt stmt={stmt} marker={target} short={true} />
</TableCell>
</th>
);
@@ -621,7 +618,7 @@ async function FunctionSection(props: FunctionProps): Promise<JSX.Element> {
/* Computes the relevant data for each marker */
interface Data { probe: Probe; summary: Evaluation; status: MarkerStatus }
const entries = Array.from(props.markers.entries());
- const data = await Promise.all(entries.map(async ([ target, status ]) => {
+ const data = await Promise.all(entries.map(async ([target, status]) => {
const probe = await props.getProbe({ target, fct });
const summary = await probe.evaluate('Summary');
return { probe, summary, status } as Data;
@@ -795,8 +792,8 @@ class FunctionInfos {
const { target: tgt, fct } = focusedLoc ?? {};
const inFct = fct !== undefined && fct === this.fct;
const ms = new Map<Ast.marker, MarkerStatus>();
- this.pinned.forEach((p) => ms.set(p, [ 'Pinned', inFct && tgt === p ]));
- this.tracked.forEach((p) => ms.set(p, [ 'Tracked', inFct && tgt === p ]));
+ this.pinned.forEach((p) => ms.set(p, ['Pinned', inFct && tgt === p]));
+ this.tracked.forEach((p) => ms.set(p, ['Tracked', inFct && tgt === p]));
if (inFct && tgt && !this.has(tgt)) ms.set(tgt, 'JustFocused');
return new Map(Array.from(ms.entries()).reverse());
}
@@ -892,7 +889,7 @@ class FunctionsManager {
map<A>(func: (infos: FunctionInfos, fct: string) => A): A[] {
const entries = Array.from(this.cache.entries());
- return entries.map(([ fct, infos ]) => func(infos, fct));
+ return entries.map(([fct, infos]) => func(infos, fct));
}
}
@@ -909,7 +906,7 @@ export const evaluateEvent = new Dome.Event('dome.evaluate');
ipcRenderer.on('dome.ipc.evaluate', () => evaluateEvent.emit());
interface EvaluationModeProps {
- computationState : Eva.computationStateType | undefined;
+ computationState: Eva.computationStateType | undefined;
selection: States.Selection;
setLocPin: (loc: Location, pin: boolean) => void;
}
@@ -935,8 +932,8 @@ function useEvaluationMode(props: EvaluationModeProps): void {
const shortcut = System.platform === 'macos' ? 'Cmd+E' : 'Ctrl+E';
const onEnter = (pattern: string): void => {
const marker = selection?.current?.marker;
- const data = { atStmt: marker, term: pattern };
- Server.send(Ast.markerFromTerm, data).then(addProbe).catch(handleError);
+ const data = { stmt: marker, term: pattern };
+ Server.send(Ast.parseTerm, data).then(addProbe).catch(handleError);
};
const evalMode = {
label: 'Evaluation',
@@ -973,21 +970,21 @@ const FocusState = new GlobalState<Probe | undefined>(undefined);
function EvaTable(): JSX.Element {
/* Component state */
- const [ selection, select ] = States.useSelection();
- const [ cs, setCS ] = useGlobalState(CallstackState);
- const [ fcts ] = useGlobalState(FunctionsManagerState);
- const [ focus, setFocus ] = useGlobalState(FocusState);
+ const [selection, select] = States.useSelection();
+ const [cs, setCS] = useGlobalState(CallstackState);
+ const [fcts] = useGlobalState(FunctionsManagerState);
+ const [focus, setFocus] = useGlobalState(FocusState);
/* Used to force the component update. We cannot use the `forceUpdate` hook
* proposed by Dome as we need to be able to add dependencies on a changing
* value (here tac) explicitly. We need to force the update as modifications
* of the Function Manager internal data does NOT trigger the component
* update. */
- const [ tac, setTic ] = React.useState(0);
+ const [tac, setTic] = React.useState(0);
/* Event use to communicate when a location is selected. Used to scroll
* related column into view if needed */
- const [ locEvt ] = React.useState(new Dome.Event<Location>('eva-location'));
+ const [locEvt] = React.useState(new Dome.Event<Location>('eva-location'));
/* Build cached version of needed server's requests */
const getProbe = useProbeCache();
@@ -999,14 +996,14 @@ function EvaTable(): JSX.Element {
const selectedCSInfos = await getCallsites(cs);
if (selectedCSInfos.length === 0) return undefined;
else return selectedCSInfos[0].callee;
- }, [ cs, getCallsites ]);
+ }, [cs, getCallsites]);
const { result: csFct } = Dome.usePromise(csFctPromise);
/* Reset the selected callstack when the corresponding function is removed */
React.useEffect(() => {
if (csFct && fcts.isEmpty(csFct) && focus?.fct !== csFct)
setCS('Summary');
- }, [ csFct, setCS, fcts, focus?.fct ] );
+ }, [csFct, setCS, fcts, focus?.fct]);
/* Updated the focused Probe when the selection changes. Also emit on the
* `locEvent` event. */
@@ -1022,7 +1019,7 @@ function EvaTable(): JSX.Element {
};
if (loc) getProbe(loc).then(doUpdate);
else setFocus(undefined);
- }, [ fcts, selection, getProbe, setFocus, locEvt ]);
+ }, [fcts, selection, getProbe, setFocus, locEvt]);
/* Callback used to pin or unpin a location */
const setLocPin = React.useCallback((loc: Location, pin: boolean): void => {
@@ -1034,7 +1031,7 @@ function EvaTable(): JSX.Element {
/* On meta-selection, pin the selected location. */
React.useEffect(() => {
const pin = (loc: States.Location): void => {
- const {marker, fct} = loc;
+ const { marker, fct } = loc;
if (marker && fct) setLocPin({ target: marker, fct }, true);
};
States.MetaSelection.on(pin);
@@ -1052,7 +1049,7 @@ function EvaTable(): JSX.Element {
fcts.clean(focus);
}
setTic(tac + 1);
- }, [ fcts, focus, setFocus, tac ]);
+ }, [fcts, focus, setFocus, tac]);
/* Builds the sections for each function. As the component is built
* asynchronously, we have to use the `usePromise` hook, which forces us to
@@ -1103,13 +1100,13 @@ function EvaTable(): JSX.Element {
});
return Promise.all(ps.map(FunctionSection));
},
- [ cs, setCS, fcts, focus, setFocus, tac, getCallsites, setLocPin, csFct,
- getCallstacks, getProbe, remove, select, locEvt ]);
+ [cs, setCS, fcts, focus, setFocus, tac, getCallsites, setLocPin, csFct,
+ getCallstacks, getProbe, remove, select, locEvt]);
const { result: functions } = Dome.usePromise(functionsPromise);
/* Builds the alarms component. As for the function sections, it is an
* asynchronous process. */
- const alarmsProm = React.useMemo(() => AlarmsInfos(focus)(cs), [ focus, cs ]);
+ const alarmsProm = React.useMemo(() => AlarmsInfos(focus)(cs), [focus, cs]);
const { result: alarmsInfos } = Dome.usePromise(alarmsProm);
/* Builds the stacks component. As for the function sections, it is an
@@ -1121,7 +1118,7 @@ function EvaTable(): JSX.Element {
const isSelected = callsites.find(p) !== undefined;
const close = (): void => setCS('Summary');
return StackInfos({ callsites, isSelected, setSelection: select, close });
- }, [ cs, setCS, select, getCallsites, selection ]);
+ }, [cs, setCS, select, getCallsites, selection]);
const { result: stackInfos } = Dome.usePromise(stackInfosPromise);
/* Handle Evaluation mode */
@@ -1135,7 +1132,7 @@ function EvaTable(): JSX.Element {
<div className='eva-functions-section'>
{React.Children.toArray(functions)}
</div>
- <Vfill/>
+ <Vfill />
{alarmsInfos}
{stackInfos}
</>
diff --git a/ivette/src/frama-c/plugins/studia/api/studia/index.ts b/ivette/src/frama-c/plugins/studia/api/studia/index.ts
index a5a8fb11a1e..4d55bfa8523 100644
--- a/ivette/src/frama-c/plugins/studia/api/studia/index.ts
+++ b/ivette/src/frama-c/plugins/studia/api/studia/index.ts
@@ -68,24 +68,24 @@ export const byEffects: Compare.Order<effects> =
indirect: Compare.array(Compare.pair(Compare.string,byMarker,)),
});
-const getReadsLval_internal: Server.GetRequest<Json.key<'#lval'>,effects> = {
+const getReadsLval_internal: Server.GetRequest<marker,effects> = {
kind: Server.RqKind.GET,
name: 'plugins.studia.studia.getReadsLval',
- input: Json.jKey<'#lval'>('#lval'),
+ input: jMarker,
output: jEffects,
signals: [],
};
/** Get the list of statements that read a lval. */
-export const getReadsLval: Server.GetRequest<Json.key<'#lval'>,effects>= getReadsLval_internal;
+export const getReadsLval: Server.GetRequest<marker,effects>= getReadsLval_internal;
-const getWritesLval_internal: Server.GetRequest<Json.key<'#lval'>,effects> = {
+const getWritesLval_internal: Server.GetRequest<marker,effects> = {
kind: Server.RqKind.GET,
name: 'plugins.studia.studia.getWritesLval',
- input: Json.jKey<'#lval'>('#lval'),
+ input: jMarker,
output: jEffects,
signals: [],
};
/** Get the list of statements that write a lval. */
-export const getWritesLval: Server.GetRequest<Json.key<'#lval'>,effects>= getWritesLval_internal;
+export const getWritesLval: Server.GetRequest<marker,effects>= getWritesLval_internal;
/* ------------------------------------- */
diff --git a/ivette/src/frama-c/states.ts b/ivette/src/frama-c/states.ts
index a4287f3245a..ea4469337c9 100644
--- a/ivette/src/frama-c/states.ts
+++ b/ivette/src/frama-c/states.ts
@@ -792,6 +792,37 @@ export async function resetSelection(): Promise<void> {
}
}
+// --------------------------------------------------------------------------
+// --- Markers
+// --------------------------------------------------------------------------
+
+export type attributes = Ast.markerAttributesData;
+
+export const defaultMarker: attributes = {
+ key: '',
+ labelKind: '',
+ titleKind: '',
+ name: '',
+ descr: '',
+ isLval: false,
+ isFunDecl: false,
+ isFun: false,
+ sloc: { dir: '', base: '', file: '', line: 0 },
+};
+
+/** Access the marker attributes from AST. */
+export function useMarker(marker: Ast.marker | undefined): attributes {
+ const marks = useSyncArray(Ast.markerAttributes);
+ if (marker === undefined) return defaultMarker;
+ const attrs = marks.getData(marker);
+ if (attrs === undefined) return defaultMarker;
+ return attrs;
+}
+
+// --------------------------------------------------------------------------
+// --- General Synchro
+// --------------------------------------------------------------------------
+
Server.onReady(() => {
if (GlobalSelection.getValue() === emptySelection)
resetSelection();
diff --git a/src/kernel_services/ast_data/globals.ml b/src/kernel_services/ast_data/globals.ml
index c82ac01c137..42b251943f4 100644
--- a/src/kernel_services/ast_data/globals.ml
+++ b/src/kernel_services/ast_data/globals.ml
@@ -303,6 +303,11 @@ module Functions = struct
in
State.memo add vi
+ let mem vi =
+ vi.vglob &&
+ try let _ = get vi in true
+ with Not_found -> false
+
let get_params kf =
match kf.fundec with
| Definition(f,_loc) -> f.sformals
diff --git a/src/kernel_services/ast_data/globals.mli b/src/kernel_services/ast_data/globals.mli
index d2e0cc20be1..51ff3e98930 100644
--- a/src/kernel_services/ast_data/globals.mli
+++ b/src/kernel_services/ast_data/globals.mli
@@ -96,6 +96,9 @@ module Functions: sig
(** {2 Getters} *)
+ val mem: varinfo -> bool
+ (** Returns [true] is this variable is associated to some kernel function *)
+
val get: varinfo -> kernel_function
(** @raise Not_found if the given varinfo has no associated kernel function
and is not a built-in.
diff --git a/src/kernel_services/ast_printing/printer_tag.ml b/src/kernel_services/ast_printing/printer_tag.ml
index 9f5fe65f343..7c1e8c4aadc 100644
--- a/src/kernel_services/ast_printing/printer_tag.ml
+++ b/src/kernel_services/ast_printing/printer_tag.ml
@@ -233,10 +233,13 @@ let ki_of_localizable loc = match loc with
| PType _ -> Kglobal
let varinfo_of_localizable = function
- | PLval (_, _, (Var vi, NoOffset)) -> Some vi
- | PVDecl (_, _, vi) -> Some vi
- | PGlobal (GVar (vi, _, _) | GVarDecl (vi, _)
- | GFunDecl (_, vi, _) | GFun ({svar = vi }, _)) -> Some vi
+ | PVDecl (_, _, vi)
+ | PLval (_, _, (Var vi, NoOffset))
+ | PTermLval (_, _, _, (TVar { lv_origin = Some vi }, TNoOffset))
+ | PGlobal (
+ GVar (vi, _, _) | GVarDecl (vi, _) |
+ GFun ({svar = vi },_) | GFunDecl (_, vi, _)
+ ) -> Some vi
| _ -> None
let typ_of_localizable = function
@@ -490,16 +493,16 @@ let loc_to_localizable ?(precise_col=false) loc =
(* --- Printer API --- *)
(* -------------------------------------------------------------------------- *)
-module type TAG =
+module type INFO =
sig
- val create : localizable -> string
+ val tag : localizable -> string
val unfold : stmt -> bool
end
(* We delay the creation of the class to execution time, so that all
pretty-printer extensions get properly registered (as we want to inherit
from them). The only known solution is to use a functor *)
-module BUILD(Tag : TAG)(X: Printer.PrinterClass) : Printer.PrinterClass =
+module BUILD(Info : INFO)(X: Printer.PrinterClass) : Printer.PrinterClass =
struct
class printer : Printer.extensible_printer = object(self)
@@ -584,10 +587,10 @@ struct
method! next_stmt next fmt current =
- if Tag.unfold current
+ if Info.unfold current
then self#preconditions_at_call fmt current;
Format.fprintf fmt "@{<%s>%a@}"
- (Tag.create (PStmt (Option.get self#current_kf,current)))
+ (Info.tag (PStmt (Option.get self#current_kf,current)))
(super#next_stmt next) current
method! lval fmt lv =
@@ -596,7 +599,7 @@ struct
(* Do not highlight the lvals in initializers. *)
| Kstmt _ as ki ->
Format.fprintf fmt "@{<%s>"
- (Tag.create (PLval (self#current_kf,ki,lv)));
+ (Info.tag (PLval (self#current_kf,ki,lv)));
(match lv with
| Var vi, (Field _| Index _ as o) ->
(* Small hack to be able to click on the arrays themselves
@@ -616,7 +619,7 @@ struct
self#lval fmt lv
| _ ->
Format.fprintf fmt "@{<%s>"
- (Tag.create (PExp (self#current_kf,self#current_kinstr,e)));
+ (Info.tag (PExp (self#current_kf,self#current_kinstr,e)));
super#exp fmt e;
Format.fprintf fmt "@}"
@@ -632,7 +635,7 @@ struct
super#term_lval fmt lv
| Some ip ->
Format.fprintf fmt "@{<%s>"
- (Tag.create
+ (Info.tag
(PTermLval (self#current_kf, self#current_kinstr, ip, lv)));
(match lv with
| TVar vi, (TField _| TIndex _ as o) ->
@@ -645,12 +648,12 @@ struct
method! vdecl fmt vi =
Format.fprintf fmt "@{<%s>%a@}"
- (Tag.create (PVDecl (self#current_kf, self#current_kinstr, vi)))
+ (Info.tag (PVDecl (self#current_kf, self#current_kinstr, vi)))
super#vdecl vi
method private tag_property p =
current_property <- Some p;
- Tag.create (PIP p)
+ Info.tag (PIP p)
method! code_annotation fmt ca =
match ca.annot_content with
@@ -688,7 +691,7 @@ struct
| GType _ ->
super#global fmt g
| GAsm _ | GPragma _ | GText _ | GAnnot _ ->
- Format.fprintf fmt "@{<%s>%a@}" (Tag.create (PGlobal g)) super#global g
+ Format.fprintf fmt "@{<%s>%a@}" (Info.tag (PGlobal g)) super#global g
method! extended fmt ext =
let loc =
@@ -793,14 +796,14 @@ struct
self#current_behavior_or_loop from)
in
Format.fprintf fmt "@{<%s>%a@}"
- (Tag.create (PIP ip)) (super#from s) from
+ (Info.tag (PIP ip)) (super#from s) from
method! global_annotation fmt a =
match Property.ip_of_global_annotation_single a with
| None -> super#global_annotation fmt a
| Some ip ->
Format.fprintf fmt "@{<%s>%a@}"
- (Tag.create (PIP ip)) super#global_annotation a
+ (Info.tag (PIP ip)) super#global_annotation a
method! allocation ~isloop fmt a =
match
@@ -810,39 +813,39 @@ struct
None -> super#allocation ~isloop fmt a
| Some ip ->
Format.fprintf fmt "@{<%s>%a@}"
- (Tag.create (PIP ip)) (super#allocation ~isloop) a;
+ (Info.tag (PIP ip)) (super#allocation ~isloop) a;
method! stmtkind sattr next fmt sk =
(* Special tag denoting the start of the statement, WITHOUT any ACSL
assertion/statement contract, etc. *)
let s = Option.get self#current_stmt in
let f = Option.get self#current_kf in
- let tag = Tag.create (PStmtStart(f,s)) in
+ let tag = Info.tag (PStmtStart(f,s)) in
Format.fprintf fmt "@{<%s>%a@}" tag (super#stmtkind sattr next) sk
method! ikind fmt c =
Format.fprintf fmt "@{<%s>%a@}"
- (Tag.create (PType(TInt(c,[]))))
+ (Info.tag (PType(TInt(c,[]))))
super#ikind c
method! fkind fmt c =
Format.fprintf fmt "@{<%s>%a@}"
- (Tag.create (PType(TFloat(c,[]))))
+ (Info.tag (PType(TFloat(c,[]))))
super#fkind c
method! compname fmt comp =
Format.fprintf fmt "@{<%s>%a@}"
- (Tag.create (PGlobal(Globals.Types.global Struct comp.cname)))
+ (Info.tag (PGlobal(Globals.Types.global Struct comp.cname)))
super#compname comp
method! enuminfo fmt enum =
Format.fprintf fmt "@{<%s>%a@}"
- (Tag.create (PGlobal(Globals.Types.global Enum enum.ename)))
+ (Info.tag (PGlobal(Globals.Types.global Enum enum.ename)))
super#enuminfo enum
method! typeinfo fmt tinfo =
Format.fprintf fmt "@{<%s>%a@}"
- (Tag.create (PGlobal(Globals.Types.global Typedef tinfo.tname)))
+ (Info.tag (PGlobal(Globals.Types.global Typedef tinfo.tname)))
super#typeinfo tinfo
initializer force_brace <- true
@@ -852,7 +855,7 @@ end
module type Tag =
sig
- val create : localizable -> string
+ val tag : localizable -> string
end
module type S_pp =
@@ -871,11 +874,11 @@ struct
let printer () =
let pp = Printer.current_printer () in
let module PP = (val pp: Printer.PrinterClass) in
- let module TAG = struct
- let create = T.create
+ let module INFO = struct
+ let tag = T.tag
let unfold s = !unfold s
end in
- let module TagPrinterClass = BUILD(TAG)(PP) in
+ let module TagPrinterClass = BUILD(INFO)(PP) in
new TagPrinterClass.printer
let with_unfold_precond unfolder f fmt x =
diff --git a/src/kernel_services/ast_printing/printer_tag.mli b/src/kernel_services/ast_printing/printer_tag.mli
index 57de33aaba6..9da67df17c2 100644
--- a/src/kernel_services/ast_printing/printer_tag.mli
+++ b/src/kernel_services/ast_printing/printer_tag.mli
@@ -74,7 +74,7 @@ val loc_to_localizable: ?precise_col:bool -> Filepath.position -> localizable op
module type Tag =
sig
- val create : localizable -> string
+ val tag : localizable -> string
end
module type S_pp =
diff --git a/src/plugins/eva/api/general_requests.ml b/src/plugins/eva/api/general_requests.ml
index 37a7c0daaec..fdb4c9cb1f3 100644
--- a/src/plugins/eva/api/general_requests.ml
+++ b/src/plugins/eva/api/general_requests.ml
@@ -457,8 +457,8 @@ module PropertiesData = struct
~package
~name:"properties"
~descr:(Markdown.plain "Status of Registered Properties")
- ~key:(fun ip -> Kernel_ast.Marker.create (PIP ip))
- ~keyType:Kernel_ast.Marker.jproperty
+ ~key:(fun ip -> Kernel_ast.Marker.tag (PIP ip))
+ ~keyType:Kernel_ast.Marker.jtype
~iter:Property_status.iter
model
end
diff --git a/src/plugins/gui/pretty_source.ml b/src/plugins/gui/pretty_source.ml
index e68c355f644..b2d1ddff1c5 100644
--- a/src/plugins/gui/pretty_source.ml
+++ b/src/plugins/gui/pretty_source.ml
@@ -203,12 +203,12 @@ struct
| PIP _ -> 'i'
| PType _ -> 'y'
- let create loc =
+ let tag loc =
incr current ;
let tag = Printf.sprintf "guitag:%c%x" (charcode loc) !current in
Hashtbl.replace hashtbl tag loc ; tag
- let get = Hashtbl.find hashtbl
+ let find = Hashtbl.find hashtbl
end
@@ -261,7 +261,7 @@ let buffer_formatter state source =
let s = Extlib.format_string_of_stag s in
(* Ignore tags that are not ours *)
if Extlib.string_prefix "guitag:" s then
- Stack.push (source#end_iter#offset, Tag.get s) starts ;
+ Stack.push (source#end_iter#offset, Tag.find s) starts ;
""
in
let emit_close_tag s =
diff --git a/src/plugins/server/kernel_ast.ml b/src/plugins/server/kernel_ast.ml
index 6864cbb2b69..f21cc6e95b8 100644
--- a/src/plugins/server/kernel_ast.ml
+++ b/src/plugins/server/kernel_ast.ml
@@ -96,90 +96,6 @@ end
(* --- Printers --- *)
(* -------------------------------------------------------------------------- *)
-(* The kind of a marker. *)
-module MarkerKind = struct
-
- let kinds = Enum.dictionary ()
-
- let kind name =
- Enum.tag
- ~name
- ~descr:(Md.plain (String.capitalize_ascii name))
- kinds
-
- let expr = kind "expression"
- let lval = kind "lvalue"
- let decl = kind "declaration"
- let stmt = kind "statement"
- let glob = kind "global"
- let term = kind "term"
- let prop = kind "property"
- let typ = kind "type"
-
- let () =
- Enum.set_lookup
- kinds
- (fun localizable ->
- let open Printer_tag in
- match localizable with
- | PStmt _ -> stmt
- | PStmtStart _ -> stmt
- | PVDecl _ -> decl
- | PLval _ -> lval
- | PExp _ -> expr
- | PTermLval _ -> term
- | PGlobal _ -> glob
- | PIP _ -> prop
- | PType _ -> typ)
-
- let data =
- Request.dictionary
- ~package
- ~name:"markerKind"
- ~descr:(Md.plain "Marker kind")
- kinds
-
- include (val data : S with type t = Printer_tag.localizable)
-end
-
-module MarkerVar = struct
-
- let vars = Enum.dictionary ()
-
- let kind name =
- Enum.tag
- ~name
- ~descr:(Md.plain (String.capitalize_ascii name))
- vars
-
- let none = kind "none"
- let var = kind "variable"
- let fct = kind "function"
-
- let () =
- Enum.set_lookup
- vars
- (fun localizable ->
- let open Printer_tag in
- match localizable with
- | PLval (_, _, (Var vi, NoOffset))
- | PVDecl (_, _, vi)
- | PGlobal (GVar (vi, _, _) | GVarDecl (vi, _)) ->
- if Cil.isFunctionType vi.vtype then fct else var
- | PGlobal (GFun _ | GFunDecl _) -> fct
- | PLval _ | PStmt _ | PStmtStart _
- | PExp _ | PTermLval _ | PGlobal _ | PIP _ | PType _ -> none)
-
- let data =
- Request.dictionary
- ~package
- ~name:"markerVar"
- ~descr:(Md.plain "Marker variable")
- vars
-
- include (val data : S with type t = Printer_tag.localizable)
-end
-
module Marker =
struct
@@ -217,66 +133,6 @@ struct
let iter f =
Localizable.Hashtbl.iter (fun key str -> f (key, str)) (STATE.get ()).tags
- let array =
- let model = States.model () in
- let () =
- States.column
- ~name:"kind"
- ~descr:(Md.plain "Marker kind")
- ~data:(module MarkerKind)
- ~get:fst
- model
- in
- let () =
- States.column
- ~name:"var"
- ~descr:(Md.plain "Marker variable")
- ~data:(module MarkerVar)
- ~get:fst
- model
- in
- let () =
- States.column
- ~name:"name"
- ~descr:(Md.plain "Marker short name")
- ~data:(module Jalpha)
- ~get:(fun (tag, _) -> Printer_tag.label tag)
- model
- in
- let () =
- States.column
- ~name:"descr"
- ~descr:(Md.plain "Marker declaration or description")
- ~data:(module Jstring)
- ~get:(fun (tag, _) -> Rich_text.to_string Printer_tag.pretty tag)
- model
- in
- let () =
- States.option
- ~name:"scope"
- ~descr:(Md.plain "Function scope of the marker, if applicable")
- ~data:(module Jstring)
- ~get:(fun (tag, _) ->
- Option.map Kernel_function.get_name @@
- Printer_tag.kf_of_localizable tag)
- model
- in
- let () =
- States.column
- ~name:"sloc"
- ~descr:(Md.plain "Source location")
- ~data:(module Position)
- ~get:(fun (tag, _) -> fst (Printer_tag.loc_of_localizable tag))
- model
- in
- States.register_array
- ~package
- ~name:"markerInfo"
- ~descr:(Md.plain "Marker information")
- ~key:snd ~keyType:Jstring
- ~iter ~add_reload_hook:ast_update_hook
- model
-
let create_tag = function
| PStmt(_,s) -> Printf.sprintf "#s%d" s.sid
| PStmtStart(_,s) -> Printf.sprintf "#k%d" s.sid
@@ -288,40 +144,29 @@ struct
| PIP _ -> Printf.sprintf "#p%d" (incr kid ; !kid)
| PType _ -> Printf.sprintf "#y%d" (incr kid ; !kid)
- let create loc =
+ let hooks = ref []
+ let hook f = hooks := !hooks @ [f]
+
+ let tag loc =
let { tags ; locs } = STATE.get () in
try Localizable.Hashtbl.find tags loc
with Not_found ->
let tag = create_tag loc in
Localizable.Hashtbl.add tags loc tag ;
Hashtbl.add locs tag loc ;
- States.update array (loc, tag);
- tag
+ List.iter (fun fn -> fn (loc,tag)) !hooks ; tag
- let lookup tag = Hashtbl.find (STATE.get()).locs tag
+ let find tag = Hashtbl.find (STATE.get()).locs tag
type t = localizable
- let markers = ref []
- let jmarker kd =
- let jt = Pkg.Jkey kd in markers := jt :: !markers ; jt
-
- let jstmt = jmarker "stmt"
- let jdecl = jmarker "decl"
- let jlval = jmarker "lval"
- let jexpr = jmarker "expr"
- let jterm = jmarker "term"
- let jglobal = jmarker "global"
- let jproperty = jmarker "property"
- let jtyp = jmarker "type"
-
let jtype = Data.declare ~package ~name:"marker"
~descr:(Md.plain "Localizable AST markers")
- Pkg.(Junion (List.rev !markers))
+ (Pkg.Jkey "marker")
- let to_json loc = `String (create loc)
+ let to_json loc = `String (tag loc)
let of_json js =
- try lookup (Js.to_string js)
+ try find (Js.to_string js)
with Not_found -> Data.failure "not a localizable marker"
end
@@ -334,27 +179,36 @@ module Printer = Printer_tag.Make(Marker)
module Lval =
struct
+ open Printer_tag
+
type t = kinstr * lval
- let jtype = Marker.jlval
+ let jtype = Marker.jtype
+
let to_json (kinstr, lval) =
let kf = match kinstr with
| Kglobal -> None
| Kstmt stmt -> Some (Kernel_function.find_englobing_kf stmt)
in
Marker.to_json (PLval (kf, kinstr, lval))
- let of_json js =
- let open Printer_tag in
- match Marker.of_json js with
+
+ let find = function
| PLval (_, kinstr, lval) -> kinstr, lval
| PVDecl (_, kinstr, vi) -> kinstr, Cil.var vi
| PGlobal (GVar (vi, _, _) | GVarDecl (vi, _)) -> Kglobal, Cil.var vi
- | _ -> Data.failure "not a lval marker"
+ | _ -> raise Not_found
+
+ let mem tag = try let _ = find tag in true with Not_found -> false
+
+ let of_json js =
+ try find (Marker.of_json js)
+ with Not_found -> Data.failure "not a lval marker"
+
end
module Stmt =
struct
type t = stmt
- let jtype = Marker.jstmt
+ let jtype = Marker.jtype
let to_json st =
let kf = Kernel_function.find_englobing_kf st in
Marker.to_json (PStmt(kf,st))
@@ -368,7 +222,7 @@ end
module Ki =
struct
type t = kinstr
- let jtype = Pkg.Joption Marker.jstmt
+ let jtype = Pkg.Joption Marker.jtype
let to_json = function
| Kglobal -> `Null
| Kstmt st -> Stmt.to_json st
@@ -430,6 +284,138 @@ module KfMarker = struct
R.get fct r, R.get marker r
end
+(* -------------------------------------------------------------------------- *)
+(* --- Marker Attributes --- *)
+(* -------------------------------------------------------------------------- *)
+
+module Attributes =
+struct
+ open Printer_tag
+
+ let descr ~short m =
+ match varinfo_of_localizable m with
+ | Some vi ->
+ if Globals.Functions.mem vi then "Function" else
+ if vi.vglob then
+ if short then "Global" else "Global Variable"
+ else if vi.vformal then
+ if short then "Formal" else "Formal Parameter"
+ else if vi.vtemp then
+ if short then "Temp" else "Temporary Variable (generated)"
+ else
+ if short then "Local" else "Local Variable"
+ | None ->
+ match m with
+ | PStmt _ | PStmtStart _ -> if short then "Stmt" else "Statement"
+ | PLval _ -> if short then "Lval" else "L-value"
+ | PTermLval _ -> if short then "Lval" else "ACSL L-value"
+ | PVDecl _ -> assert false
+ | PExp _ -> if short then "Expr" else "Expression"
+ | PIP _ -> if short then "Prop" else "Property"
+ | PGlobal _ -> if short then "Decl" else "Declaration"
+ | PType _ -> "Type"
+
+ let kf tag =
+ match varinfo_of_localizable tag with
+ | Some vi -> Globals.Functions.get vi
+ | None -> raise Not_found
+
+ let fundecl = function
+ | PGlobal (GVar (vi, _, _) | GVarDecl (vi, _)) -> Globals.Functions.get vi
+ | _ -> raise Not_found
+
+ let is_kf tag = try let _ = kf tag in true with Not_found -> false
+ let is_fundecl tag = try let _ = fundecl tag in true with Not_found -> false
+
+ let scope tag =
+ Option.map Kernel_function.get_name @@ Printer_tag.kf_of_localizable tag
+
+ let model = States.model ()
+
+ let () =
+ States.column
+ ~name:"labelKind"
+ ~descr:(Md.plain "Marker kind (short)")
+ ~data:(module Jalpha)
+ ~get:(fun (tag,_) -> descr ~short:true tag)
+ model
+
+ let () =
+ States.column
+ ~name:"titleKind"
+ ~descr:(Md.plain "Marker kind (long)")
+ ~data:(module Jalpha)
+ ~get:(fun (tag,_) -> descr ~short:false tag)
+ model
+
+ let () =
+ States.column
+ ~name:"name"
+ ~descr:(Md.plain "Marker short name")
+ ~data:(module Jalpha)
+ ~get:(fun (tag, _) -> Printer_tag.label tag)
+ model
+
+ let () =
+ States.column
+ ~name:"descr"
+ ~descr:(Md.plain "Marker declaration or description")
+ ~data:(module Jstring)
+ ~get:(fun (tag, _) -> Rich_text.to_string Printer_tag.pretty tag)
+ model
+
+ let () =
+ States.column
+ ~name:"isLval"
+ ~descr:(Md.plain "Whether it is an l-value")
+ ~data:(module Jbool)
+ ~get:(fun (tag, _) -> Lval.mem tag)
+ model
+ let () =
+ States.column
+ ~name:"isFunDecl"
+ ~descr:(Md.plain "Whether it is a function declaration or definition")
+ ~data:(module Jbool)
+ ~get:(fun (tag, _) -> is_fundecl tag)
+ model
+
+ let () =
+ States.column
+ ~name:"isFun"
+ ~descr:(Md.plain "Whether it is a function symbol")
+ ~data:(module Jbool)
+ ~get:(fun (tag, _) -> is_kf tag)
+ model
+
+ let () =
+ States.option
+ ~name:"scope"
+ ~descr:(Md.plain "Function scope of the marker, if applicable")
+ ~data:(module Jstring)
+ ~get:(fun (tag, _) -> scope tag)
+ model
+
+ let () =
+ States.column
+ ~name:"sloc"
+ ~descr:(Md.plain "Source location")
+ ~data:(module Position)
+ ~get:(fun (tag, _) -> fst (Printer_tag.loc_of_localizable tag))
+ model
+
+ let array = States.register_array
+ ~package
+ ~name:"markerAttributes"
+ ~descr:(Md.plain "Marker attributes")
+ ~key:snd ~keyType:Jstring
+ ~iter:Marker.iter
+ ~add_reload_hook:ast_update_hook
+ model
+
+ let () = Marker.hook (States.update array)
+
+end
+
(* -------------------------------------------------------------------------- *)
(* --- Functions --- *)
(* -------------------------------------------------------------------------- *)
@@ -805,68 +791,74 @@ let () =
set_files
(* -------------------------------------------------------------------------- *)
-(* ----- Build a marker from an ACSL term ----------------------------------- *)
+(* --- Build a marker from an ACSL term --- *)
(* -------------------------------------------------------------------------- *)
-type marker_term_input = { atStmt : stmt ; term : string }
-
-module MarkerTermInput = struct
- type record
- let record : record Record.signature = Record.signature ()
-
- let atStmt =
- let descr = "The statement at which we will build the marker." in
- Record.field record ~name:"atStmt" ~descr:(Markdown.plain descr)
- (module Marker)
-
- let term =
- let descr = "The ACSL term." in
- Record.field record ~name:"term" ~descr:(Markdown.plain descr)
- (module Data.Jstring)
-
- let data =
- Record.publish record ~package ~name:"markerFromTermInput"
- ~descr:(Markdown.plain "<markerFromTerm> input")
-
- module R : Record.S with type r = record = (val data)
- type t = marker_term_input option
- let jtype = R.jtype
-
- let of_json js =
- let record = R.of_json js in
- match R.get atStmt record with
- | PStmt (_, s) | PStmtStart (_, s)
- | PLval (_, Kstmt s, _) | PExp (_, Kstmt s, _)
- | PTermLval (_, Kstmt s, _, _)
- | PVDecl (_, Kstmt s, _) ->
- let term = R.get term record in
- Some { atStmt = s ; term }
- | _ -> None
-
-end
-
-module MarkerTermOutput = Data.Joption (Marker)
-
-let build_marker input =
- let env =
- let open Logic_typing in
- Lenv.empty () |> append_pre_label |> append_init_label |> append_here_label
- in
- try
- let kf = Kernel_function.find_englobing_kf input.atStmt in
- let term = Logic_parse_string.term ~env kf input.term in
- let exp = Logic_to_c.term_to_exp term in
- Some (Printer_tag.PExp (Some kf, Kstmt input.atStmt, exp))
- with Not_found
- | Logic_parse_string.Error _
- | Logic_parse_string.Unbound _
- | Logic_to_c.No_conversion -> None (* TODO: return an error message. *)
-
-let descr = "Build a marker from an ACSL term."
+let logic_environment () =
+ let open Logic_typing in
+ Lenv.empty () |> append_pre_label |> append_init_label |> append_here_label
+
+module StmtTerm = Datatype.Pair(Cil_datatype.Stmt)(Cil_datatype.Term)
+module Cache = Hashtbl.Make(StmtTerm)
+
+let cache : Printer_tag.localizable Cache.t = Cache.create 0
+
+let reparse_term kf stmt text =
+ let env = logic_environment () in
+ try Some (stmt,Logic_parse_string.term ~env kf text)
+ with Logic_parse_string.Error _ | Parsing.Parse_error -> None
+
+let parseable_marker =
+ let open Printer_tag in
+ function
+ | PStmt _ | PStmtStart _ | PTermLval _ | PVDecl _ | PGlobal _ | PIP _
+ | PLval (None, _, _) | PExp (None, _, _)
+ | PLval (_, Kglobal, _) | PExp (_, Kglobal, _)
+ | PType _
+ -> None
+ | PLval (Some kf, Kstmt stmt, lval) ->
+ reparse_term kf stmt @@ Format.asprintf "%a" Cil_datatype.Lval.pretty lval
+ | PExp (Some kf, Kstmt stmt, exp) ->
+ reparse_term kf stmt @@ Format.asprintf "%a" Cil_datatype.Exp.pretty exp
+
+(* pre-fill the cache with known markers *)
+let () =
+ Marker.hook
+ begin fun (loc,_) ->
+ match parseable_marker loc with
+ | None -> ()
+ | Some entry -> Cache.add cache entry loc
+ end
-let () = Request.register ~package
- ~kind:`GET ~name:"markerFromTerm" ~descr:(Markdown.plain descr)
- ~input:(module MarkerTermInput) ~output:(module MarkerTermOutput)
- (fun input -> Option.bind input build_marker)
+(* request to parse a new marker from ACSL term *)
+let () =
+ let module Md = Markdown in
+ let s = Request.signature ~output:(module Data.Joption(Marker)) () in
+ let get_marker = Request.param s ~name:"stmt"
+ ~descr:(Md.plain "Marker position from where to localize the term")
+ (module Marker) in
+ let get_term = Request.param s ~name:"term"
+ ~descr:(Md.plain "ACSL term to parse")
+ (module Data.Jstring) in
+ Request.register_sig ~package s
+ ~kind:`GET ~name:"parseTerm"
+ ~descr:(Md.plain "Parse an ACSL Term and returns the associated marker")
+ begin fun rq () ->
+ match Printer_tag.ki_of_localizable @@ get_marker rq with
+ | Kglobal -> None
+ | Kstmt stmt ->
+ let kf = Kernel_function.find_englobing_kf stmt in
+ let env = logic_environment () in
+ let term = Logic_parse_string.term ~env kf @@ get_term rq in
+ let entry = (stmt, term) in
+ try Some (Cache.find cache entry) with Not_found ->
+ let tag =
+ match Logic_to_c.term_to_exp term with
+ | { enode = Lval lv } ->
+ Printer_tag.PLval(Some kf, Kstmt stmt, lv)
+ | exp ->
+ Printer_tag.PExp(Some kf, Kstmt stmt, exp)
+ in Cache.add cache entry tag ; Some tag
+ end
-(**************************************************************************)
+(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/server/kernel_ast.mli b/src/plugins/server/kernel_ast.mli
index 938b968119c..50702ec1922 100644
--- a/src/plugins/server/kernel_ast.mli
+++ b/src/plugins/server/kernel_ast.mli
@@ -24,37 +24,28 @@
(** Ast Data *)
(* -------------------------------------------------------------------------- *)
-open Package
open Cil_types
-module Position : Data.S with type t = Filepath.position
-
-module Kf : Data.S with type t = kernel_function
-module Fundec : Data.S with type t = fundec
-module Ki : Data.S with type t = kinstr
-module Stmt : Data.S with type t = stmt
-module Lval : Data.S with type t = kinstr * lval
module Marker :
sig
include Data.S with type t = Printer_tag.localizable
- val jstmt : jtype
- val jdecl : jtype
- val jlval : jtype
- val jexpr : jtype
- val jterm : jtype
- val jglobal : jtype
- val jproperty : jtype
- val jtyp : jtype
-
- val create : t -> string
+ val tag : t -> string
(** Memoized unique identifier. *)
- val lookup : string -> t
- (** Get back the localizable, if any. *)
+ val find : string -> t
+ (** Get back the localizable, if any.
+ @raises Not_found if marker is not defined yet *)
+
end
+module Position : Data.S with type t = Filepath.position
+module Kf : Data.S with type t = kernel_function
+module Fundec : Data.S with type t = fundec
+module Ki : Data.S with type t = kinstr
+module Stmt : Data.S with type t = stmt
+module Lval : Data.S with type t = kinstr * lval
module KfMarker : Data.S with type t = kernel_function * Printer_tag.localizable
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/server/kernel_properties.ml b/src/plugins/server/kernel_properties.ml
index a130f3d5634..7d54d4144eb 100644
--- a/src/plugins/server/kernel_properties.ml
+++ b/src/plugins/server/kernel_properties.ml
@@ -338,8 +338,8 @@ let array =
~package
~name:"status"
~descr:(Md.plain "Status of Registered Properties")
- ~key:(fun ip -> Kernel_ast.Marker.create (PIP ip))
- ~keyType:Kernel_ast.Marker.jproperty
+ ~key:(fun ip -> Kernel_ast.Marker.tag (PIP ip))
+ ~keyType:Kernel_ast.Marker.jtype
~iter
~add_update_hook
~add_remove_hook
--
GitLab