diff --git a/ivette/Makefile b/ivette/Makefile
index 29010215b7bddf4c90c1036b10c4c090a1818e0f..a30dcad4c5f3265efb03fb9bdf283e93d0243a8f 100644
--- a/ivette/Makefile
+++ b/ivette/Makefile
@@ -35,7 +35,7 @@ tsc: dome-pkg dome-templ
api:
@echo "[Ivette] Generating TypeScript API"
- @find api -name "*.ts" -exec rm -f {} \;
+ @rm -fr api/generated
../bin/frama-c.byte -load-module api/server_tsc.ml -server-tsc
@find api -name "*.ts" -exec chmod a-w {} \;
diff --git a/ivette/api/generated/kernel/ast/index.ts b/ivette/api/generated/kernel/ast/index.ts
index 2a910fb94ae5a99b0f515c71fca9aff3bfa3da03..9ae32c6bf691af3a416da8b033a070e337f6c38a 100644
--- a/ivette/api/generated/kernel/ast/index.ts
+++ b/ivette/api/generated/kernel/ast/index.ts
@@ -120,7 +120,7 @@ export const markerVarTags: Server.GetRequest<null,tag[]>= markerVarTags_interna
/** Data for array rows [`markerInfo`](#markerinfo) */
export interface markerInfoData {
/** Entry identifier. */
- key: Json.key<'#markerInfo'>;
+ key: string;
/** Marker kind */
kind: markerKind;
/** Marker variable */
@@ -136,8 +136,7 @@ export interface markerInfoData {
/** Loose decoder for `markerInfoData` */
export const jMarkerInfoData: Json.Loose<markerInfoData> =
Json.jObject({
- key: Json.jFail(Json.jKey<'#markerInfo'>('#markerInfo'),
- '#markerInfo expected'),
+ key: Json.jFail(Json.jString,'String expected'),
kind: jMarkerKindSafe,
var: jMarkerVarSafe,
name: Json.jFail(Json.jString,'String expected'),
@@ -152,8 +151,8 @@ export const jMarkerInfoDataSafe: Json.Safe<markerInfoData> =
/** Natural order for `markerInfoData` */
export const byMarkerInfoData: Compare.Order<markerInfoData> =
Compare.byFields
- <{ key: Json.key<'#markerInfo'>, kind: markerKind, var: markerVar,
- name: string, descr: string, sloc: source }>({
+ <{ key: string, kind: markerKind, var: markerVar, name: string,
+ descr: string, sloc: source }>({
key: Compare.string,
kind: byMarkerKind,
var: byMarkerVar,
@@ -178,8 +177,8 @@ export const reloadMarkerInfo: Server.GetRequest<null,null>= reloadMarkerInfo_in
const fetchMarkerInfo_internal: Server.GetRequest<
number,
- { pending: number, updated: markerInfoData[],
- removed: Json.key<'#markerInfo'>[], reload: boolean }
+ { pending: number, updated: markerInfoData[], removed: string[],
+ reload: boolean }
> = {
kind: Server.RqKind.GET,
name: 'kernel.ast.fetchMarkerInfo',
@@ -187,21 +186,18 @@ const fetchMarkerInfo_internal: Server.GetRequest<
output: Json.jObject({
pending: Json.jFail(Json.jNumber,'Number expected'),
updated: Json.jList(jMarkerInfoData),
- removed: Json.jList(Json.jKey<'#markerInfo'>('#markerInfo')),
+ removed: Json.jList(Json.jString),
reload: Json.jFail(Json.jBoolean,'Boolean expected'),
}),
};
/** Data fetcher for array [`markerInfo`](#markerinfo) */
export const fetchMarkerInfo: Server.GetRequest<
number,
- { pending: number, updated: markerInfoData[],
- removed: Json.key<'#markerInfo'>[], reload: boolean }
+ { pending: number, updated: markerInfoData[], removed: string[],
+ reload: boolean }
>= fetchMarkerInfo_internal;
-const markerInfo_internal: State.Array<
- Json.key<'#markerInfo'>,
- markerInfoData
- > = {
+const markerInfo_internal: State.Array<string,markerInfoData> = {
name: 'kernel.ast.markerInfo',
getkey: ((d:markerInfoData) => d.key),
signal: signalMarkerInfo,
@@ -210,7 +206,7 @@ const markerInfo_internal: State.Array<
order: byMarkerInfoData,
};
/** Marker informations */
-export const markerInfo: State.Array<Json.key<'#markerInfo'>,markerInfoData> = markerInfo_internal;
+export const markerInfo: State.Array<string,markerInfoData> = markerInfo_internal;
/** Localizable AST markers */
export type marker =
@@ -242,7 +238,7 @@ export const byMarker: Compare.Order<marker> = Compare.structural;
/** Location: function and marker */
export interface location {
/** Function */
- function: Json.key<'#fct'>;
+ fct: Json.key<'#fct'>;
/** Marker */
marker: marker;
}
@@ -250,7 +246,7 @@ export interface location {
/** Loose decoder for `location` */
export const jLocation: Json.Loose<location> =
Json.jObject({
- function: Json.jFail(Json.jKey<'#fct'>('#fct'),'#fct expected'),
+ fct: Json.jFail(Json.jKey<'#fct'>('#fct'),'#fct expected'),
marker: jMarkerSafe,
});
@@ -261,8 +257,8 @@ export const jLocationSafe: Json.Safe<location> =
/** Natural order for `location` */
export const byLocation: Compare.Order<location> =
Compare.byFields
- <{ function: Json.key<'#fct'>, marker: marker }>({
- function: Compare.string,
+ <{ fct: Json.key<'#fct'>, marker: marker }>({
+ fct: Compare.string,
marker: byMarker,
});
diff --git a/ivette/api/generated/kernel/properties/index.ts b/ivette/api/generated/kernel/properties/index.ts
index 7ca5ce68b252ecb5308fe822caec7a05ef680773..dcba1484d490140e593cacd56ab49052929aed4e 100644
--- a/ivette/api/generated/kernel/properties/index.ts
+++ b/ivette/api/generated/kernel/properties/index.ts
@@ -225,7 +225,7 @@ export const alarmsTags: Server.GetRequest<null,tag[]>= alarmsTags_internal;
/** Data for array rows [`status`](#status) */
export interface statusData {
/** Entry identifier. */
- key: Json.key<'#status'>;
+ key: Json.key<'#property'>;
/** Full description */
descr: string;
/** Kind */
@@ -235,7 +235,7 @@ export interface statusData {
/** Status */
status: propStatus;
/** Function */
- function?: Json.key<'#fct'>;
+ fct?: Json.key<'#fct'>;
/** Instruction */
kinstr?: Json.key<'#stmt'>;
/** Position */
@@ -251,12 +251,12 @@ export interface statusData {
/** Loose decoder for `statusData` */
export const jStatusData: Json.Loose<statusData> =
Json.jObject({
- key: Json.jFail(Json.jKey<'#status'>('#status'),'#status expected'),
+ key: Json.jFail(Json.jKey<'#property'>('#property'),'#property expected'),
descr: Json.jFail(Json.jString,'String expected'),
kind: jPropKindSafe,
names: Json.jList(Json.jString),
status: jPropStatusSafe,
- function: Json.jKey<'#fct'>('#fct'),
+ fct: Json.jKey<'#fct'>('#fct'),
kinstr: Json.jKey<'#stmt'>('#stmt'),
source: jSourceSafe,
alarm: Json.jString,
@@ -271,8 +271,8 @@ export const jStatusDataSafe: Json.Safe<statusData> =
/** Natural order for `statusData` */
export const byStatusData: Compare.Order<statusData> =
Compare.byFields
- <{ key: Json.key<'#status'>, descr: string, kind: propKind,
- names: string[], status: propStatus, function?: Json.key<'#fct'>,
+ <{ 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,
@@ -280,7 +280,7 @@ export const byStatusData: Compare.Order<statusData> =
kind: byPropKind,
names: Compare.array(Compare.string),
status: byPropStatus,
- function: Compare.defined(Compare.string),
+ fct: Compare.defined(Compare.string),
kinstr: Compare.defined(Compare.string),
source: bySource,
alarm: Compare.defined(Compare.string),
@@ -304,7 +304,7 @@ export const reloadStatus: Server.GetRequest<null,null>= reloadStatus_internal;
const fetchStatus_internal: Server.GetRequest<
number,
- { pending: number, updated: statusData[], removed: Json.key<'#status'>[],
+ { pending: number, updated: statusData[], removed: Json.key<'#property'>[],
reload: boolean }
> = {
kind: Server.RqKind.GET,
@@ -313,18 +313,18 @@ const fetchStatus_internal: Server.GetRequest<
output: Json.jObject({
pending: Json.jFail(Json.jNumber,'Number expected'),
updated: Json.jList(jStatusData),
- removed: Json.jList(Json.jKey<'#status'>('#status')),
+ removed: Json.jList(Json.jKey<'#property'>('#property')),
reload: Json.jFail(Json.jBoolean,'Boolean expected'),
}),
};
/** Data fetcher for array [`status`](#status) */
export const fetchStatus: Server.GetRequest<
number,
- { pending: number, updated: statusData[], removed: Json.key<'#status'>[],
+ { pending: number, updated: statusData[], removed: Json.key<'#property'>[],
reload: boolean }
>= fetchStatus_internal;
-const status_internal: State.Array<Json.key<'#status'>,statusData> = {
+const status_internal: State.Array<Json.key<'#property'>,statusData> = {
name: 'kernel.properties.status',
getkey: ((d:statusData) => d.key),
signal: signalStatus,
@@ -333,6 +333,6 @@ const status_internal: State.Array<Json.key<'#status'>,statusData> = {
order: byStatusData,
};
/** Status of Registered Properties */
-export const status: State.Array<Json.key<'#status'>,statusData> = status_internal;
+export const status: State.Array<Json.key<'#property'>,statusData> = status_internal;
/* ------------------------------------- */
diff --git a/ivette/api/generated/plugins/eva/values/index.ts b/ivette/api/generated/plugins/eva/values/index.ts
index bc7353fe239426e399d04330a865ab4b616facad..b08b8540d749cde916fd0650a73acd73c4c6dac2 100644
--- a/ivette/api/generated/plugins/eva/values/index.ts
+++ b/ivette/api/generated/plugins/eva/values/index.ts
@@ -43,17 +43,14 @@ export const jCallstackSafe: Json.Safe<callstack> =
/** Natural order for `callstack` */
export const byCallstack: Compare.Order<callstack> = Compare.number;
-const getCallstacks_internal: Server.GetRequest<
- Json.key<'#stmt'>,
- callstack[]
- > = {
+const getCallstacks_internal: Server.GetRequest<marker[],callstack[]> = {
kind: Server.RqKind.GET,
name: 'plugins.eva.values.getCallstacks',
- input: Json.jKey<'#stmt'>('#stmt'),
+ input: Json.jList(jMarker),
output: Json.jList(jCallstack),
};
/** Callstacks for markers */
-export const getCallstacks: Server.GetRequest<Json.key<'#stmt'>,callstack[]>= getCallstacks_internal;
+export const getCallstacks: Server.GetRequest<marker[],callstack[]>= getCallstacks_internal;
const getCallstackInfo_internal: Server.GetRequest<
callstack,
diff --git a/ivette/api/server_tsc.ml b/ivette/api/server_tsc.ml
index d190a3b3e19a78816c2a97fe4adef1be20f3a98b..669d83168c2cd58d3536c88a00742bbf9864f187 100644
--- a/ivette/api/server_tsc.ml
+++ b/ivette/api/server_tsc.ml
@@ -375,10 +375,9 @@ let makeDeclaration fmt names d =
self.name jtype js self.name;
- | D_array { arr_key ; arr_kind } ->
+ | D_array { arr_key ; arr_kind = jkey } ->
let data = Pkg.Derived.data self in
- let jkey = (Pkg.Jkey arr_kind) in
- let jrow = (Pkg.Jdata data) in
+ let jrow = Pkg.Jdata data in
Format.fprintf fmt
"@[<hv 2>const %s_internal: State.Array<@,%a,@,%a@,>@] = {@\n"
self.name jtype jkey jtype jrow ;
diff --git a/ivette/src/dome/src/renderer/controls/gallery.json b/ivette/src/dome/src/renderer/controls/gallery.json
index 93fb175304006f611729775c94b76890ae82d8dc..62fe91ead33c03e2bd5b866519ffd02dfc3574a8 100644
--- a/ivette/src/dome/src/renderer/controls/gallery.json
+++ b/ivette/src/dome/src/renderer/controls/gallery.json
@@ -17,6 +17,18 @@
"viewBox": "0 0 15 16",
"path": "M9.143 7.143v0.571q0 0.116-0.085 0.201t-0.201 0.085h-5.143q-0.116 0-0.201-0.085t-0.085-0.201v-0.571q0-0.116 0.085-0.201t0.201-0.085h5.143q0.116 0 0.201 0.085t0.085 0.201zM10.286 7.429q0-1.652-1.174-2.826t-2.826-1.174-2.826 1.174-1.174 2.826 1.174 2.826 2.826 1.174 2.826-1.174 1.174-2.826zM14.857 14.857q0 0.473-0.335 0.808t-0.808 0.335q-0.482 0-0.804-0.339l-3.063-3.054q-1.598 1.107-3.563 1.107-1.277 0-2.442-0.496t-2.009-1.339-1.339-2.009-0.496-2.442 0.496-2.442 1.339-2.009 2.009-1.339 2.442-0.496 2.442 0.496 2.009 1.339 1.339 2.009 0.496 2.442q0 1.964-1.107 3.563l3.063 3.063q0.33 0.33 0.33 0.804z"
},
+ "CURSOR": {
+ "section": "Tools",
+ "viewBox": "0 0 32 32",
+ "title": "Mouse Pointer",
+ "path": "M16.689 17.655l5.311 12.345-4 2-4.646-12.678-7.354 6.678v-26l20 16-9.311 1.655z"
+ },
+ "PIN": {
+ "section": "Tools",
+ "title": "Push Pin",
+ "viewBox": "0 0 16 16",
+ "path": "M8.5 0l-1.5 1.5 1.5 1.5-3.5 4h-3.5l2.75 2.75-4.25 5.635v0.615h0.615l5.635-4.25 2.75 2.75v-3.5l4-3.5 1.5 1.5 1.5-1.5-7.5-7.5zM7 8.5l-1-1 3.5-3.5 1 1-3.5 3.5z"
+ },
"PAINTBRUSH": {
"section": "Tools",
"title": "Paint Brush",
diff --git a/ivette/src/dome/src/renderer/controls/labels.tsx b/ivette/src/dome/src/renderer/controls/labels.tsx
index a9250344cc81c7cf3a1f2e374fc259e711c3df64..ca1630fc302230e8ff3c11f447b030ce131c9e72 100644
--- a/ivette/src/dome/src/renderer/controls/labels.tsx
+++ b/ivette/src/dome/src/renderer/controls/labels.tsx
@@ -34,6 +34,8 @@ export interface LabelProps {
children?: React.ReactNode;
/** Click event callback. */
onClick?: (evt: React.MouseEvent) => void;
+ /** Click event callback. */
+ onDoubleClick?: (evt: React.MouseEvent) => void;
/** Right-click event callback. */
onContextMenu?: (evt: React.MouseEvent) => void;
}
@@ -52,6 +54,7 @@ const makeLabel = (className: string) => (props: LabelProps, ref: any) => {
title={props.title}
style={props.style}
onClick={props.onClick}
+ onDoubleClick={props.onDoubleClick}
onContextMenu={props.onContextMenu}
>
{props.icon && <Icon title={props.title} id={props.icon} />}
@@ -70,6 +73,7 @@ const TITLE = 'dome-xLabel dome-text-title';
const DESCR = 'dome-xLabel dome-text-descr';
const TDATA = 'dome-xLabel dome-text-data';
const TCODE = 'dome-xLabel dome-text-code';
+const TCELL = 'dome-xLabel dome-text-cell';
// --------------------------------------------------------------------------
// --- Components
@@ -90,4 +94,7 @@ export const Data = React.forwardRef(makeLabel(TDATA));
/** Selectable inlined source-code content. */
export const Code = React.forwardRef(makeLabel(TCODE));
+/** Selectable inlined source-code content with default cursor. */
+export const Cell = React.forwardRef(makeLabel(TCELL));
+
// --------------------------------------------------------------------------
diff --git a/ivette/src/dome/src/renderer/frame/style.css b/ivette/src/dome/src/renderer/frame/style.css
index 9cdc1f5d44786efe4f31587d3c8cd593fe7ae051..4f7d144cae66f93d3117171f781da10a11fe86b4 100644
--- a/ivette/src/dome/src/renderer/frame/style.css
+++ b/ivette/src/dome/src/renderer/frame/style.css
@@ -384,7 +384,7 @@
background-image: none ;
}
-.dome-window-inactive .dome-xToolBar-control.dome-selected {
+.dome-window-inactive .dome-xToolBar-control.dome-selected:not(:disabled) {
fill: #eee;
color: #eee;
background-color: #ccc ;
@@ -396,14 +396,14 @@
fill: #ccc ;
color: #ccc ;
border: 1px solid #bbb ;
- background-color: #eee ;
+ background-color: #ddd ;
}
.dome-window-inactive .dome-xToolBar-control.dome-selected:disabled {
fill: #ccc ;
color: #ccc ;
border-color: #ddd ;
- background-color: #eee ;
+ background-color: #ddd ;
}
/* -------------------------------------------------------------------------- */
@@ -435,6 +435,10 @@
border-bottom-left-radius: 0 ;
}
+.dome-xToolBar-group > .dome-xToolBar-control:first-child:last-child {
+ border-radius: 4px ;
+}
+
.dome-xToolBar-group > .dome-xToolBar-control:not(:first-child):not(:last-child) {
border-radius: 0 ;
}
diff --git a/ivette/src/dome/src/renderer/style.css b/ivette/src/dome/src/renderer/style.css
index 99cb9265aaf25c94f992f721246303c6797b0af6..2ace504d516cd976248542ca513371028b5d394c 100644
--- a/ivette/src/dome/src/renderer/style.css
+++ b/ivette/src/dome/src/renderer/style.css
@@ -31,6 +31,10 @@ body {
/* --- Frame Colors --- */
/* -------------------------------------------------------------------------- */
+.dome-hidden {
+ visibility: hidden;
+}
+
.dome-window-active .dome-color-frame {
fill: #606060 ;
color: #606060 ;
@@ -128,4 +132,13 @@ div.dome-dragged {
text-overflow: clip ;
}
+.dome-text-cell {
+ cursor: default ;
+ user-select: text ;
+ font-family: 'Andale mono', monospace ;
+ font-size: 9pt ;
+ white-space: nowrap ;
+ text-overflow: clip ;
+}
+
/* -------------------------------------------------------------------------- */
diff --git a/ivette/src/dome/src/renderer/text/editors.tsx b/ivette/src/dome/src/renderer/text/editors.tsx
index a1592f1e971258232eb176afff4ba55d6b33a040..17fc74f263eb3c955d32ba2f30ff9904cd7665aa 100644
--- a/ivette/src/dome/src/renderer/text/editors.tsx
+++ b/ivette/src/dome/src/renderer/text/editors.tsx
@@ -25,7 +25,7 @@ const CSS_SELECTED = 'dome-xText-select';
/* --------------------------------------------------------------------------*/
export interface MarkerCallback {
- (id: string): void;
+ (id: string, meta?: boolean): void;
}
/**
@@ -329,10 +329,12 @@ class CodeMirrorWrapper extends React.Component<TextProps> {
onMouseClick(evt: MouseEvt, callback: MarkerCallback | undefined) {
// No need for throttling
- const { target } = evt;
- if (target instanceof Element && callback) {
- const marker = this._findMarker(target);
- if (marker && marker.id) callback(marker.id);
+ if (callback) {
+ const { target } = evt;
+ if (target instanceof Element) {
+ const marker = this._findMarker(target);
+ if (marker && marker.id) callback(marker.id, evt.altKey);
+ }
}
this.props.buffer?.setFocused(true);
}
diff --git a/ivette/src/frama-c/eva/Values.tsx b/ivette/src/frama-c/eva/Values.tsx
index 6bdf15345c8728ade58b0881b2e451cca04f9264..6a2c28e4f063dd2197198b340fc3fe71d0cb1a4c 100644
--- a/ivette/src/frama-c/eva/Values.tsx
+++ b/ivette/src/frama-c/eva/Values.tsx
@@ -5,425 +5,21 @@
// React & Dome
import React from 'react';
import * as Dome from 'dome';
-import { classes } from 'dome/misc/utils';
-import { VariableSizeList } from 'react-window';
-import { Vfill, Hpack, Vpack, Filler } from 'dome/layout/boxes';
-import { Icon } from 'dome/controls/icons';
-import { Label, Code } from 'dome/controls/labels';
+import { Vfill } from 'dome/layout/boxes';
import { IconButton } from 'dome/controls/buttons';
-import { ButtonGroup, Button } from 'dome/frame/toolbars';
// External Libs
import { AutoSizer } from 'react-virtualized';
// Frama-C
import { Component, TitleBar } from 'frama-c/LabViews';
-import * as States from 'frama-c/states';
-
-// Plugins
-import * as Ast from 'frama-c/api/kernel/ast';
// Locals
-import { SizedArea, HSIZER, WSIZER } from './sized';
-import { Diff } from './diffed';
-import { sizeof, valueAt, diffAfter, diffThen, diffElse, EvaAlarm }
- from './cells';
-import { Row } from './layout';
-import { Probe } from './probes';
-import { Callsite } from './stacks';
-import { Model, getModelInstance } from './model';
+import { ProbeInfos } from './probeinfos';
+import { Dimension, ValuesPanel } from './valuetable';
+import { AlarmsInfos, StackInfos } from './valueinfos';
import './style.css';
-// --------------------------------------------------------------------------
-// --- Use Model
-// --------------------------------------------------------------------------
-
-function useModel(): Model {
- const model = getModelInstance();
- Dome.useUpdate(model.changed, model.laidout);
- return model;
-}
-
-// --------------------------------------------------------------------------
-// --- Stmt Printer
-// --------------------------------------------------------------------------
-
-interface StmtProps {
- stmt?: string;
- rank?: number;
-}
-
-function Stmt(props: StmtProps) {
- const { rank, stmt } = props;
- if (rank === undefined || !stmt) return null;
- const title = `Stmt id ${stmt} at rank ${rank}`;
- return (
- <span className="dome-text-code eva-stmt" title={title}>
- @S{rank}
- </span>
- );
-}
-
-// --------------------------------------------------------------------------
-// --- Probe Panel
-// --------------------------------------------------------------------------
-
-function ProbeInfos() {
- const model = useModel();
- const probe = model.getFocused();
- const transient = probe?.transient ?? false;
- const label = probe?.label;
- const fct = probe?.fct;
- const code = probe?.code;
- const stmt = probe?.stmt;
- const rank = probe?.rank;
- const byCS = probe?.byCallstacks;
- const stacks = model.getStacks(probe).length;
- const stackable = byCS || stacks > 1;
- const { cols, rows } = sizeof(code);
- const width = WSIZER.dimension(cols) + 4;
- const height = HSIZER.dimension(rows) + 3;
- const visible = !!code;
- const zoomed = probe?.zoomed;
- const zoomable = probe?.zoomable;
- const visibility = visible ? 'visible' : 'hidden';
- const effects = probe?.effects;
- const condition = probe?.condition;
- return (
- <Hpack style={{ visibility }} className="eva-probeinfo">
- <Label className="eva-probeinfo-label">{label && `${label}:`}</Label>
- <div style={{ minWidth: width, height }} className="eva-probeinfo-code">
- <SizedArea cols={cols} rows={rows}>{code}</SizedArea>
- </div>
- <Code>{fct}<Stmt stmt={stmt} rank={rank} /></Code>
- <IconButton
- className="eva-probeinfo-button"
- display={stackable}
- selected={byCS}
- icon="ITEMS.LIST"
- title={`Details by callstack (${stacks})`}
- onClick={() => { if (probe) probe.setByCallstacks(!byCS); }}
- />
- <IconButton
- className="eva-probeinfo-button"
- display={zoomable}
- selected={zoomed}
- icon="SEARCH"
- onClick={() => { if (probe) probe.setZoomed(!zoomed); }}
- />
- <IconButton
- className="eva-probeinfo-button"
- kind={transient ? 'selected' : 'warning'}
- icon={transient ? 'CIRC.CHECK' : 'CIRC.CLOSE'}
- title={transient ? 'Make the probe persistent' : 'Release the probe'}
- onClick={() => { if (probe) probe.setTransient(!transient); }}
- />
- <Filler />
- <ButtonGroup
- enabled={!!probe}
- value={probe?.vstate}
- onChange={(s) => { if (probe) probe.setState(s); }}
- className="eva-probeinfo-state"
- >
- <Button
- visible={effects || condition}
- label="H"
- value="Here"
- />
- <Button
- visible={condition}
- label="T"
- value="Then"
- />
- <Button
- visible={condition}
- label="E"
- value="Else"
- />
- <Button
- visible={effects}
- label="A"
- value="After"
- />
- </ButtonGroup>
- </Hpack>
- );
-}
-
-// --------------------------------------------------------------------------
-// --- Alarms Panel
-// --------------------------------------------------------------------------
-
-function AlarmsInfo() {
- const model = useModel();
- const probe = model.getFocused();
- if (probe) {
- const callstack = model.getCallstack();
- const domain =
- model.values.getValues(probe.marker, probe.stmt, callstack);
- const alarms = domain?.alarms ?? [];
- if (alarms.length > 0) {
- // console.log('ALARMS', alarms);
- const renderAlarm = ([status, alarm]: EvaAlarm) => {
- const className = `eva-alarm-info eva-alarm-${status}`;
- return (
- <Code className={className} icon="WARNING">{alarm}</Code>
- );
- };
- return (
- <Vpack className="eva-info">
- {alarms.map(renderAlarm)}
- </Vpack>
- );
- }
- }
- return null;
-}
-
-// --------------------------------------------------------------------------
-// --- Stack Panel
-// --------------------------------------------------------------------------
-
-function StackInfo() {
- const model = useModel();
- const [, setSelection] = States.useSelection();
- const callstack = model.getCalls();
- if (callstack.length <= 1) return null;
- const makeCallsite = ({ caller, stmt, rank }: Callsite) => {
- if (!caller || !stmt) return null;
- const key = `${caller}@${stmt}`;
- const onClick = () => {
- const location = { function: caller, marker: stmt };
- setSelection({ location });
- };
- return (
- <Code
- key={key}
- icon="TRIANGLE.LEFT"
- className="eva-callsite"
- onClick={onClick}
- >
- {caller}
- <Stmt stmt={stmt} rank={rank} />
- </Code>
- );
- };
- return (
- <Hpack className="eva-info">
- {callstack.map(makeCallsite)}
- </Hpack>
- );
-}
-
-// --------------------------------------------------------------------------
-// --- Table Cell
-// --------------------------------------------------------------------------
-
-interface TableCellProps {
- probe: Probe;
- row: Row;
-}
-
-const CELLPADDING = 12;
-
-function TableCell(props: TableCellProps) {
- const model = useModel();
- const [, setSelection] = States.useSelection();
- const { probe, row } = props;
- const { kind, callstack } = row;
- const minWidth = CELLPADDING + WSIZER.dimension(probe.minCols);
- const maxWidth = CELLPADDING + WSIZER.dimension(probe.maxCols);
- const style = { width: minWidth, maxWidth };
- let contents: React.ReactNode = props.probe.marker;
- const { transient } = probe;
-
- switch (kind) {
-
- // ---- Probe Contents
- case 'probes':
- if (transient) {
- contents = <span className="dome-text-label">« Probe »</span>;
- } else {
- const { stmt, rank, code, label } = probe;
- const textClass = label ? 'dome-text-label' : 'dome-text-code';
- contents = (
- <>
- <span className={textClass}>{label ?? code}</span>
- <Stmt stmt={stmt} rank={rank} />
- </>
- );
- }
- break;
-
- // ---- Values Contents
- case 'values':
- case 'callstack':
- {
- const domain = model.values.getValues(
- probe.marker,
- probe.stmt,
- callstack,
- );
- const { alarms = [] } = domain;
- const { vstate: s, effects, condition } = probe;
- const text = valueAt(domain, s) ?? '';
- const diff = diffAfter(domain, effects, s);
- const diffA = diffThen(domain, condition, s);
- const diffB = diffElse(domain, condition, s);
- const { cols, rows } = sizeof(text);
- contents = (
- <>
- {alarms.length > 0 && (
- <Icon className="eva-cell-alarms" size={10} id="WARNING" />
- )}
- <SizedArea cols={cols} rows={rows}>
- <span className={`eva-state-${s}`}>
- <Diff text={text} diff={diff} diffA={diffA} diffB={diffB} />
- </span>
- </SizedArea>
- </>
- );
- }
- break;
-
- }
-
- // --- Cell Packing
- const isFocused = model.getFocused() === probe;
- const className = classes(
- 'eva-cell',
- transient && 'eva-transient',
- isFocused && 'eva-focused',
- );
- const onClick = () => {
- if (probe) {
- const location = { function: probe.fct, marker: probe.marker };
- setSelection({ location });
- model.setSelectedRow(row);
- }
- };
- const onDoubleClick = () => {
- if (probe) {
- if (probe.transient) probe.setTransient(false);
- if (probe.zoomable) probe.setZoomed(!probe.zoomed);
- }
- };
- return (
- <div
- className={className}
- style={style}
- onClick={onClick}
- onDoubleClick={onDoubleClick}
- >
- {contents}
- </div>
- );
-}
-
-// --------------------------------------------------------------------------
-// --- Table Row
-// --------------------------------------------------------------------------
-
-interface TableRowProps {
- style: React.CSSProperties;
- index: number;
-}
-
-function TableRow(props: TableRowProps) {
- const model = useModel();
- const row = model.getRow(props.index);
- if (!row) return null;
- const { kind, probes } = row;
- const sk = row.stackIndex;
- const rowKind = `eva-${kind}`;
- const rowParity = sk !== undefined && (sk % 2 === 0);
- const rowStyle =
- model.isSelectedRow(row) ? 'eva-row-selected' :
- rowParity ? 'eva-row-odd' : 'eva-row-even';
- const className = classes(
- rowKind,
- rowStyle,
- );
- const header = row.stacks && (
- <div className="eva-cell eva-stack">
- {sk === undefined ? '#' : `${1 + sk}`}
- </div>
- );
- const style: React.CSSProperties = { left: row.stacks ? 0 : 12 };
- const contents = probes.map((probe) => (
- <TableCell
- key={probe.marker}
- probe={probe}
- row={row}
- />
- ));
- return (
- <Hpack className={className} style={props.style}>
- <div style={style} className="eva-row">
- {header}
- {contents}
- </div>
- <Filler />
- </Hpack>
- );
-}
-
-// --------------------------------------------------------------------------
-// --- Values Panel
-// --------------------------------------------------------------------------
-
-interface Dimension {
- width: number;
- height: number;
-}
-
-interface ValuesPanelProps extends Dimension {
- zoom: number;
-}
-
-function ValuesPanel(props: ValuesPanelProps) {
- const model = useModel();
- const { zoom, width, height } = props;
- // --- reset line cache
- const listRef = React.useRef<VariableSizeList>(null);
- Dome.useEvent(model.laidout, () => {
- setImmediate(() => {
- const vlist = listRef.current;
- if (vlist) vlist.resetAfterIndex(0, true);
- });
- });
- // --- compute line height
- const getRowHeight = React.useCallback(
- (k: number) => HSIZER.dimension(model.getRowLines(k)),
- [model],
- );
- // --- compute layout
- const margin = WSIZER.capacity(width);
- const rowHeight = HSIZER.dimension(1);
- const [selection] = States.useSelection();
- React.useEffect(() => {
- const curr = selection?.current;
- const fct = curr?.function;
- const marker = Ast.jMarker(curr?.marker);
- model.setLayout({ zoom, margin, fct, marker });
- });
- // --- render list
- return (
- <VariableSizeList
- ref={listRef}
- itemCount={model.getRowCount()}
- itemKey={model.getRowKey}
- itemSize={getRowHeight}
- estimatedItemSize={rowHeight}
- width={width}
- height={height}
- itemData={model}
- >
- {TableRow}
- </VariableSizeList>
- );
-}
-
// --------------------------------------------------------------------------
// --- Values Component
// --------------------------------------------------------------------------
@@ -456,8 +52,8 @@ function ValuesComponent() {
)}
</AutoSizer>
</Vfill>
- <AlarmsInfo />
- <StackInfo />
+ <AlarmsInfos />
+ <StackInfos />
</Vfill>
</>
);
diff --git a/ivette/src/frama-c/eva/cells.ts b/ivette/src/frama-c/eva/cells.ts
index acb3e9ea05432b1ef0952432b9cb098a0059e90f..b4242c27b06880a8e119bf6a74f5d6b572d8332f 100644
--- a/ivette/src/frama-c/eva/cells.ts
+++ b/ivette/src/frama-c/eva/cells.ts
@@ -23,7 +23,7 @@ export interface Size { cols: number; rows: number }
export const EMPTY: Size = { cols: 0, rows: 0 };
export function sizeof(text?: string): Size {
- if (!text) return EMPTY;
+ if (text === undefined) return EMPTY;
const lines = text.split('\n');
return {
rows: lines.length,
@@ -82,55 +82,15 @@ export interface EvaValues {
size: Size;
}
-export function valueAt(v: EvaValues, st: EvaState): string | undefined {
- switch (st) {
- case 'Here': return v.values;
- case 'After': return v.v_after;
- case 'Then': return v.v_then;
- case 'Else': return v.v_else;
- }
-}
-
-export function diffAfter(
- v: EvaValues,
- effects: boolean,
- st: EvaState,
-): string | undefined {
- if (!effects) return undefined;
- switch (st) {
- case 'Here': return v.v_after;
- default: return v.values;
- }
-}
-
-export function diffThen(
- v: EvaValues,
- condition: boolean,
- st: EvaState,
-): string | undefined {
- if (!condition) return undefined;
- switch (st) {
- case 'Here': return v.v_then;
- default: return v.values;
- }
-}
-
-export function diffElse(
- v: EvaValues,
- condition: boolean,
- st: EvaState,
-): string | undefined {
- if (!condition) return undefined;
- switch (st) {
- case 'Here': return v.v_else;
- default: return v.values;
- }
-}
-
// --------------------------------------------------------------------------
// --- Value Cache
// --------------------------------------------------------------------------
+export interface Probe {
+ fct: string | undefined;
+ marker: Ast.marker;
+}
+
export class ValueCache {
private readonly state: ModelCallbacks;
@@ -159,33 +119,32 @@ export class ValueCache {
return this.probes.get(target) ?? EMPTY;
}
- private static stackKey(stmt: string, callstack: Values.callstack) {
- return `${stmt}::${callstack}`;
+ private static stackKey(fct: string, callstack: Values.callstack) {
+ return `${fct}::${callstack}`;
}
- getStackSize(stmt: string, callstack: Values.callstack) {
- const key = ValueCache.stackKey(stmt, callstack);
+ getStackSize(fct: string, callstack: Values.callstack) {
+ const key = ValueCache.stackKey(fct, callstack);
return this.stacks.get(key) ?? EMPTY;
}
// --- Cached Values & Request Update
getValues(
- target: Ast.marker,
- stmt: string | undefined,
+ { fct, marker }: Probe,
callstack: Values.callstack | undefined,
): EvaValues {
- const key = callstack !== undefined ? `${target}@${callstack}` : target;
+ const key = callstack !== undefined ? `${marker}@${callstack}` : marker;
const cache = this.vcache;
const cached = cache.get(key);
if (cached) return cached;
const newValue: EvaValues = { values: '', size: EMPTY };
- if (callstack !== undefined && stmt === undefined)
+ if (callstack !== undefined && fct === undefined)
return newValue;
- // callstack !== undefined ==> stmt !== undefined)
+ // callstack !== undefined ==> fct !== undefined)
cache.set(key, newValue);
Server
- .send(Values.getValues, { target, callstack })
+ .send(Values.getValues, { target: marker, callstack })
.then((r) => {
newValue.errors = undefined;
newValue.values = r.values;
@@ -193,7 +152,7 @@ export class ValueCache {
newValue.v_then = r.v_then;
newValue.v_else = r.v_else;
newValue.alarms = r.alarms;
- if (this.updateLayout(target, stmt, callstack, newValue))
+ if (this.updateLayout(marker, fct, callstack, newValue))
this.state.forceLayout();
else
this.state.forceUpdate();
@@ -209,7 +168,7 @@ export class ValueCache {
private updateLayout(
target: Ast.marker,
- stmt: string | undefined,
+ fct: string | undefined,
callstack: Values.callstack | undefined,
v: EvaValues,
): boolean {
@@ -231,9 +190,9 @@ export class ValueCache {
}
// max size for stack row
if (callstack !== undefined) {
- if (stmt === undefined) small = false;
+ if (fct === undefined) small = false;
else {
- const key = ValueCache.stackKey(stmt, callstack);
+ const key = ValueCache.stackKey(fct, callstack);
const cs = this.stacks.get(key) ?? EMPTY;
if (!leq(s, cs)) {
this.stacks.set(key, merge(cs, s));
diff --git a/ivette/src/frama-c/eva/diffed.tsx b/ivette/src/frama-c/eva/diffed.tsx
index 9edf57ee95f6edd03c49de4f3935ad4dbb70156a..19dd3b913268add01e6b2623a54dda1879b5232b 100644
--- a/ivette/src/frama-c/eva/diffed.tsx
+++ b/ivette/src/frama-c/eva/diffed.tsx
@@ -50,7 +50,7 @@ export class DiffBuffer {
if (value) {
this.scratch += '\0'.repeat(value.length);
this.contents.push(
- <span className={MODIFIED} title="Modified"> {value}</span>,
+ <span className={MODIFIED} title="Modified">{value}</span>,
);
}
} else if (removed) {
@@ -74,7 +74,7 @@ export class DiffBuffer {
getContents(): React.ReactNode {
this.flush();
- return <>{React.Children.toArray(this.contents)}</>;
+ return React.Children.toArray(this.contents);
}
getScratch() {
@@ -93,17 +93,16 @@ export interface Diff2Props {
diff: string;
}
-export function Diff2(props: Diff2Props): JSX.Element {
+export function Diff2(props: Diff2Props) {
const { text, diff } = props;
- const contents = React.useMemo(() => {
+ const contents = React.useMemo<React.ReactNode>(() => {
if (text === diff) return text;
const buffer = new DiffBuffer();
const chunks = diffChars(text, diff);
- // console.log('DIFF', text, diff, chunks);
chunks.forEach(buffer.push);
return buffer.getContents();
}, [text, diff]);
- return contents as JSX.Element;
+ return <>{contents}</>;
}
/* --------------------------------------------------------------------------*/
@@ -116,9 +115,9 @@ export interface Diff3Props {
diffB: string;
}
-export function Diff3(props: Diff3Props): JSX.Element {
+export function Diff3(props: Diff3Props) {
const { text, diffA, diffB } = props;
- const contents = React.useMemo(() => {
+ const contents = React.useMemo<React.ReactNode>(() => {
if (text === diffA && text === diffB) return text;
const buffer = new DiffBuffer();
diffChars(diffA, diffB).forEach(buffer.push);
@@ -127,7 +126,7 @@ export function Diff3(props: Diff3Props): JSX.Element {
diffChars(text, scratch).forEach(buffer.push);
return buffer.getContents();
}, [text, diffA, diffB]);
- return contents as JSX.Element;
+ return <>{contents}</>;
}
/* --------------------------------------------------------------------------*/
@@ -135,17 +134,20 @@ export function Diff3(props: Diff3Props): JSX.Element {
/* --------------------------------------------------------------------------*/
export interface DiffProps {
- text: string;
+ text?: string;
diff?: string;
diffA?: string;
diffB?: string;
}
-export function Diff(props: DiffProps): JSX.Element {
+export function Diff(props: DiffProps) {
const { text, diff, diffA, diffB } = props;
- if (text === diff) return <>{text}</>;
- if (diff !== undefined)
+ if (text === undefined)
+ return diff ? <>{diff}</> : null;
+ if (diff !== undefined) {
+ if (diff === text) return <>{text}</>;
return <Diff2 text={text} diff={diff} />;
+ }
if (diffA === undefined) {
if (diffB === undefined) return <>{text}</>;
return <Diff2 text={text} diff={diffB} />;
@@ -154,7 +156,6 @@ export function Diff(props: DiffProps): JSX.Element {
return <Diff2 text={text} diff={diffA} />;
}
return <Diff3 text={text} diffA={diffA} diffB={diffB} />;
-
}
// --------------------------------------------------------------------------
diff --git a/ivette/src/frama-c/eva/layout.ts b/ivette/src/frama-c/eva/layout.ts
index c416fa7c8945753a5ac0ff2490a9618ac73bc430..c116ca319731b62b3b5cc456d666b07528931f2f 100644
--- a/ivette/src/frama-c/eva/layout.ts
+++ b/ivette/src/frama-c/eva/layout.ts
@@ -12,15 +12,16 @@ export interface LayoutProps {
margin: number;
}
-export type RowKind = 'probes' | 'values' | 'callstack';
+export type RowKind = 'section' | 'probes' | 'values' | 'callstack';
export interface Row {
key: string;
+ fct: string;
kind: RowKind;
probes: Probe[];
headstack?: string;
- stacks?: number;
stackIndex?: number;
+ stackCount?: number;
callstack?: callstack;
hlines: number;
}
@@ -29,8 +30,9 @@ export interface Row {
/* --- Layout Enfine ---*/
/* --------------------------------------------------------------------------*/
-const PADDING = 2;
-const INSET = 1;
+const HEAD_PADDING = 4; // Left margin
+const CELL_PADDING = 4; // Inter cell padding
+const TEXT_PADDING = 2; // Intra cell padding
const HCROP = 18;
const VCROP = 1;
@@ -38,6 +40,7 @@ export class LayoutEngine {
// --- Setup
+ private readonly folded: (fct: string) => boolean;
private readonly values: ValueCache;
private readonly stacks: StacksCache;
private readonly hcrop: number;
@@ -48,25 +51,30 @@ export class LayoutEngine {
props: undefined | LayoutProps,
values: ValueCache,
stacks: StacksCache,
+ folded: (fct: string) => boolean,
) {
this.values = values;
this.stacks = stacks;
+ this.folded = folded;
const zoom = Math.max(0, props?.zoom ?? 0);
- this.vcrop = VCROP + 2 * zoom;
+ this.vcrop = VCROP + 3 * zoom;
this.hcrop = HCROP + zoom;
- this.margin = props?.margin ?? 80;
+ this.margin = (props?.margin ?? 80) - HEAD_PADDING;
this.push = this.push.bind(this);
}
// --- Probe Buffer
- private byStacks?: string; // stmt
+ private byFct?: string; // current function
+ private byStk?: boolean; // callstack probes
+ private skip?: boolean; // skip current function
private rowSize: Size = EMPTY;
private buffer: Probe[] = [];
private rows: Row[] = [];
+ private chained?: Probe;
crop(zoomed: boolean, s: Size): Size {
- const sCols = s.cols + INSET;
- const cols = zoomed ? sCols : Math.min(sCols, this.hcrop);
+ const s$cols = s.cols + TEXT_PADDING;
+ const cols = zoomed ? s$cols : Math.min(s$cols, this.hcrop);
const rows = zoomed ? s.rows : Math.min(s.rows, this.vcrop);
return {
cols: Math.max(HCROP, cols),
@@ -74,65 +82,128 @@ export class LayoutEngine {
};
}
- push(p: Probe) {
+ layout(ps: Probe[]): Row[] {
+ this.chained = undefined;
+ ps.sort(LayoutEngine.order).forEach(this.push);
+ return this.flush();
+ }
+
+ private static order(p: Probe, q: Probe): number {
+ const fp = p.fct;
+ const fq = q.fct;
+ if (fp === fq) {
+ const cp = p.byCallstacks;
+ const cq = q.byCallstacks;
+ if (!cp && cq) return (-1);
+ if (cp && !cq) return (+1);
+ }
+ const rp = p.rank ?? 0;
+ const rq = q.rank ?? 0;
+ if (rp < rq) return (-1);
+ if (rp > rq) return (+1);
+ if (p.marker < q.marker) return (-1);
+ if (p.marker > q.marker) return (+1);
+ return 0;
+ }
+
+ private push(p: Probe) {
+ // --- sectionning
+ const { fct, byCallstacks: stk } = p;
+ if (fct !== this.byFct) {
+ this.flush();
+ this.rows.push({
+ key: `S:${fct}`,
+ kind: 'section',
+ fct,
+ probes: [],
+ hlines: 1,
+ });
+ this.byFct = fct;
+ this.byStk = stk;
+ this.skip = this.folded(fct);
+ } else if (stk !== this.byStk) {
+ this.flush();
+ this.byStk = stk;
+ }
+ if (this.skip) return;
+ // --- chaining
+ const q = this.chained;
+ if (q) q.next = p;
+ p.prev = q;
+ this.chained = p;
+ // --- sizing
const probeSize = this.values.getProbeSize(p.marker);
const s = this.crop(p.zoomed, probeSize);
p.zoomable = p.zoomed || !leq(probeSize, s);
p.minCols = s.cols;
p.maxCols = Math.max(p.minCols, probeSize.cols);
- const stmt = p.byCallstacks ? p.stmt : undefined;
- if (stmt !== this.byStacks) {
- this.flush();
- this.byStacks = stmt;
- }
- if (!stmt && s.cols + this.rowSize.cols > this.margin)
+ // --- queueing
+ if (!stk && s.cols + this.rowSize.cols > this.margin)
this.flush();
this.rowSize = addH(this.rowSize, s);
- this.rowSize.cols += PADDING;
+ this.rowSize.cols += CELL_PADDING;
this.buffer.push(p);
}
// --- Flush Rows
- flush(): Row[] {
+ private flush(): Row[] {
const ps = this.buffer;
const rs = this.rows;
- if (ps.length > 0) {
- const stmt = this.byStacks;
- if (stmt) {
+ const fct = this.byFct;
+ if (fct && ps.length > 0) {
+ const stk = this.byStk;
+ const hlines = this.rowSize.rows;
+ if (stk) {
// --- by callstacks
- const wcs = this.stacks.getStacks(stmt);
+ const markers = ps.map((p) => p.marker);
+ const stacks = this.stacks.getStacks(...markers);
+ const summary = fct ? this.stacks.getSummary(fct) : false;
+ const callstacks = stacks.length;
rs.push({
- key: `P${stmt}`,
+ key: `P:${fct}`,
kind: 'probes',
probes: ps,
- stacks: wcs.length,
+ stackCount: callstacks,
+ fct,
hlines: 1,
});
- wcs.forEach((cs, k) => {
+ if (summary) rs.push({
+ key: `V:${fct}`,
+ kind: 'values',
+ probes: ps,
+ stackIndex: -1,
+ stackCount: stacks.length,
+ fct,
+ hlines: 1,
+ });
+ stacks.forEach((cs, k) => {
rs.push({
- key: `C${stmt}::${cs}`,
+ key: `C:${fct}:${cs}`,
kind: 'callstack',
probes: ps,
stackIndex: k,
- stacks: wcs.length,
+ stackCount: callstacks,
callstack: cs,
- hlines: this.values.getStackSize(stmt, cs).rows,
+ fct,
+ hlines,
});
});
} else {
- // --- by callstacks
+ // --- not by callstacks
const n = rs.length;
rs.push({
- key: `P${n}`,
+ key: `P#${n}`,
kind: 'probes',
probes: ps,
+ fct,
hlines: 1,
}, {
- key: `V${n}`,
+ key: `V#${n}`,
kind: 'values',
probes: ps,
- hlines: this.rowSize.rows,
+ fct,
+ hlines,
});
}
}
diff --git a/ivette/src/frama-c/eva/model.ts b/ivette/src/frama-c/eva/model.ts
index 6f24c809c84d2360cc6a461d60e7c09ef7dcd0d0..0c5f7c2bfe107e58f0d396178f448f2958979b29 100644
--- a/ivette/src/frama-c/eva/model.ts
+++ b/ivette/src/frama-c/eva/model.ts
@@ -8,18 +8,17 @@ import equal from 'react-fast-compare';
import * as Dome from 'dome';
import * as Server from 'frama-c/server';
+import * as States from 'frama-c/states';
import * as Values from 'frama-c/api/plugins/eva/values';
-import * as Ast from 'frama-c/api/kernel/ast';
// Model
import { Probe } from './probes';
import { StacksCache, Callsite } from './stacks';
-import { ModelCallbacks, ValueCache } from './cells';
+import { ModelCallbacks, ValueCache, EvaState } from './cells';
import { LayoutProps, LayoutEngine, Row } from './layout';
export interface ModelLayout extends LayoutProps {
- fct?: string;
- marker?: Ast.marker;
+ location?: States.Location;
}
/* --------------------------------------------------------------------------*/
@@ -34,37 +33,62 @@ export class Model implements ModelCallbacks {
this.forceReload = this.forceReload.bind(this);
this.computeLayout = this.computeLayout.bind(this);
this.setLayout = throttle(this.setLayout.bind(this), 300);
+ this.metaSelection = this.metaSelection.bind(this);
this.getRowKey = this.getRowKey.bind(this);
this.getRowCount = this.getRowCount.bind(this);
this.getRowLines = this.getRowLines.bind(this);
- Server.onSignal(Values.changed, this.forceReload);
+ this.isFolded = this.isFolded.bind(this);
}
// --- Probes
+ private vstmt: EvaState = 'After';
+ private vcond: EvaState = 'Here';
private selected?: Probe;
private focused?: Probe;
private callstack?: Values.callstack;
private remanent?: Probe; // last transient
private probes = new Map<string, Probe>();
+ private folded = new Map<string, boolean>(); // folded functions
getFocused() { return this.focused; }
isFocused(p: Probe | undefined) { return this.focused === p; }
- isRemanent(p: Probe | undefined) { return this.remanent === p; }
-
- getProbe(fct: string, m: Ast.marker): Probe {
- let p = this.probes.get(m);
- if (!p) {
- p = new Probe(this, fct, m);
- this.probes.set(m, p);
- p.requestProbeInfo();
+
+ getProbe(location: States.Location | undefined): Probe | undefined {
+ if (!location) return undefined;
+ const { fct, marker } = location;
+ if (fct && marker) {
+ let p = this.probes.get(marker);
+ if (!p) {
+ p = new Probe(this, fct, marker);
+ this.probes.set(marker, p);
+ p.requestProbeInfo();
+ }
+ return p;
}
- return p;
+ return undefined;
}
getStacks(p: Probe | undefined): Values.callstack[] {
- const stmt = p?.stmt;
- return stmt ? this.stacks.getStacks(stmt) : [];
+ return p ? this.stacks.getStacks(p.marker) : [];
+ }
+
+ getVstmt(): EvaState { return this.vstmt; }
+ getVcond(): EvaState { return this.vcond; }
+ setVstmt(s: EvaState) { this.vstmt = s; this.forceUpdate(); }
+ setVcond(s: EvaState) { this.vcond = s; this.forceUpdate(); }
+
+ isFolded(fct: string): boolean {
+ return (this.focused?.fct !== fct) && (this.folded.get(fct) ?? false);
+ }
+
+ isFoldable(fct: string): boolean {
+ return this.focused?.fct !== fct;
+ }
+
+ setFolded(fct: string, folded: boolean) {
+ this.folded.set(fct, folded);
+ this.forceLayout();
}
// --- Caches
@@ -105,8 +129,15 @@ export class Model implements ModelCallbacks {
}
isSelectedRow(row: Row): boolean {
+ if (!this.focused?.byCallstacks) return false;
+ const cs = this.callstack;
+ return cs !== undefined && cs === row.callstack;
+ }
+
+ isAlignedRow(row: Row): boolean {
const cs = this.callstack;
- return cs !== undefined ? cs === row.callstack : false;
+ const cr = row.callstack;
+ return cs !== undefined && cr !== undefined && this.stacks.aligned(cs, cr);
}
getCallstack(): Values.callstack | undefined {
@@ -122,13 +153,30 @@ export class Model implements ModelCallbacks {
setLayout(ly: ModelLayout) {
if (!equal(this.layout, ly)) {
this.layout = ly;
- const { fct, marker } = ly;
- this.selected =
- fct && marker ? this.getProbe(fct, marker) : undefined;
+ this.selected = this.getProbe(ly.location);
this.forceLayout();
}
}
+ metaSelection(location: States.Location) {
+ const p = this.getProbe(location);
+ if (p) {
+ if (p.transient) {
+ if (this.focused?.byCallstacks)
+ p.setByCallstacks(true);
+ else
+ p.setPersistent();
+ }
+ }
+ }
+
+ clearSelection() {
+ this.focused = undefined;
+ this.selected = undefined;
+ this.remanent = undefined;
+ this.forceLayout();
+ }
+
// --- Recompute Layout
private computeLayout() {
@@ -137,17 +185,9 @@ export class Model implements ModelCallbacks {
const s = this.selected;
if (!s) {
this.focused = undefined;
- this.callstack = undefined;
this.remanent = undefined;
} else if (!s.loading) {
this.focused = s;
- const stacks = this.getStacks(s);
- if (s.byCallstacks) {
- const cs0 = this.callstack;
- if (cs0) this.callstack = stacks.find((cs) => cs === cs0);
- } else {
- this.callstack = stacks.length === 1 ? stacks[0] : undefined;
- }
if (s.code && s.transient) {
this.remanent = s;
} else {
@@ -164,9 +204,9 @@ export class Model implements ModelCallbacks {
this.layout,
this.values,
this.stacks,
+ this.isFolded,
);
- toLayout.sort(Probe.order).forEach(engine.push);
- this.rows = engine.flush();
+ this.rows = engine.layout(toLayout);
this.laidout.emit();
this.lock = false;
}
@@ -196,16 +236,39 @@ export class Model implements ModelCallbacks {
// --- Foce Update
forceUpdate() { this.changed.emit(); }
+ // --- Global Signals
+
+ mount() {
+ States.MetaSelection.on(this.metaSelection);
+ Server.onSignal(Values.changed, this.forceReload);
+ }
+
+ unmount() {
+ States.MetaSelection.off(this.metaSelection);
+ Server.offSignal(Values.changed, this.forceReload);
+ }
+
}
// --------------------------------------------------------------------------
-// --- EVA Model
+// --- EVA Model Hook
// --------------------------------------------------------------------------
let MODEL: Model | undefined;
-export function getModelInstance(): Model {
- if (!MODEL) MODEL = new Model();
+Server.onShutdown(() => {
+ if (MODEL) {
+ MODEL.unmount();
+ MODEL = undefined;
+ }
+});
+
+export function useModel(): Model {
+ if (!MODEL) {
+ MODEL = new Model();
+ MODEL.mount();
+ }
+ Dome.useUpdate(MODEL.changed, MODEL.laidout);
return MODEL;
}
diff --git a/ivette/src/frama-c/eva/probeinfos.tsx b/ivette/src/frama-c/eva/probeinfos.tsx
new file mode 100644
index 0000000000000000000000000000000000000000..7f8d1da41fcd27494b5905f9e234b811ee2277b2
--- /dev/null
+++ b/ivette/src/frama-c/eva/probeinfos.tsx
@@ -0,0 +1,163 @@
+// --------------------------------------------------------------------------
+// --- Eva Values
+// --------------------------------------------------------------------------
+
+// React & Dome
+import React from 'react';
+import { Hpack, Filler } from 'dome/layout/boxes';
+import { Label, Code } from 'dome/controls/labels';
+import { IconButton } from 'dome/controls/buttons';
+import { ButtonGroup, Button } from 'dome/frame/toolbars';
+
+// Frama-C
+import * as States from 'frama-c/states';
+
+// Locals
+import { SizedArea } from './sized';
+import { sizeof } from './cells';
+import { useModel } from './model';
+import { Stmt } from './valueinfos';
+
+// --------------------------------------------------------------------------
+// --- Probe Editor
+// --------------------------------------------------------------------------
+
+function ProbeEditor() {
+ const model = useModel();
+ const probe = model.getFocused();
+ if (!probe || !probe.code) return null;
+ const { label } = probe;
+ const { code } = probe;
+ const { stmt } = probe;
+ const { rank } = probe;
+ const byCS = probe.byCallstacks;
+ const stacks = model.getStacks(probe);
+ const stackable = byCS || stacks.length > 1;
+ const { cols, rows } = sizeof(code);
+ const { transient } = probe;
+ const { zoomed } = probe;
+ const { zoomable } = probe;
+ return (
+ <>
+ <Label className="eva-probeinfo-label">{label}</Label>
+ <div className="eva-probeinfo-code">
+ <SizedArea cols={cols} rows={rows}>{code}</SizedArea>
+ </div>
+ <Code><Stmt stmt={stmt} rank={rank} /></Code>
+ <IconButton
+ icon="ITEMS.LIST"
+ className="eva-probeinfo-button"
+ display={stackable}
+ selected={byCS}
+ title={`Details by callstack (${stacks})`}
+ onClick={() => { if (probe) probe.setByCallstacks(!byCS); }}
+ />
+ <IconButton
+ icon="SEARCH"
+ className="eva-probeinfo-button"
+ display={zoomable}
+ selected={zoomed}
+ onClick={() => { if (probe) probe.setZoomed(!zoomed); }}
+ />
+ <IconButton
+ icon="PIN"
+ className="eva-probeinfo-button"
+ selected={!transient}
+ title={transient ? 'Make the probe persistent' : 'Release the probe'}
+ onClick={() => {
+ if (probe) {
+ if (transient) probe.setPersistent();
+ else probe.setTransient();
+ }
+ }}
+ />
+ <IconButton
+ icon="CIRC.CLOSE"
+ className="eva-probeinfo-button"
+ display={!transient}
+ title="Discard the probe"
+ onClick={() => {
+ if (probe) {
+ probe.setTransient();
+ const p = probe.next ?? probe.prev;
+ if (p) setImmediate(() => {
+ States.setSelection({ fct: p.fct, marker: p.marker });
+ });
+ else model.clearSelection();
+ }
+ }}
+ />
+ </>
+ );
+}
+
+// --------------------------------------------------------------------------
+// --- Probe Panel
+// --------------------------------------------------------------------------
+
+export function ProbeInfos() {
+ const model = useModel();
+ const probe = model.getFocused();
+ const fct = probe?.fct;
+ const byCS = probe?.byCallstacks;
+ const effects = probe ? probe.effects : false;
+ const condition = probe ? probe.condition : false;
+ const summary = fct ? model.stacks.getSummary(fct) : false;
+ const vcond = model.getVcond();
+ const vstmt = model.getVstmt();
+ return (
+ <Hpack className="eva-probeinfo">
+ <ProbeEditor />
+ <Filler />
+ <ButtonGroup
+ enabled={!!probe}
+ className="eva-probeinfo-state"
+ >
+ <Button
+ label={'\u2211'}
+ title="Show Callstacks Summary"
+ selected={summary}
+ visible={byCS}
+ onClick={() => { if (fct) model.stacks.setSummary(fct, !summary); }}
+ />
+ <Button
+ visible={condition}
+ label="C"
+ selected={vcond === 'Here'}
+ title="Show values in all conditions"
+ onClick={() => model.setVcond('Here')}
+ />
+ <Button
+ visible={condition || vcond === 'Then'}
+ selected={vcond === 'Then'}
+ enabled={condition}
+ label="T"
+ value="Then"
+ title="Show reduced values when condition holds (Then)"
+ onClick={() => model.setVcond('Then')}
+ />
+ <Button
+ visible={condition || vcond === 'Else'}
+ selected={vcond === 'Else'}
+ enabled={condition}
+ label="E"
+ value="Else"
+ title="Show reduced values when condition does not hold (Else)"
+ onClick={() => model.setVcond('Else')}
+ />
+ <Button
+ visible={condition || effects}
+ selected={vstmt === 'After'}
+ label="A"
+ value="After"
+ title="Show values after/before statement effects"
+ onClick={() => {
+ model.setVstmt(vstmt === 'After' ? 'Here' : 'After');
+ }}
+ />
+ </ButtonGroup>
+ </Hpack>
+ );
+}
+
+// --------------------------------------------------------------------------
diff --git a/ivette/src/frama-c/eva/probes.ts b/ivette/src/frama-c/eva/probes.ts
index c920d71d0068667623c4e98973e82a291bad2313..e301c9f6439052a0f86f958b488d3ede1a467508 100644
--- a/ivette/src/frama-c/eva/probes.ts
+++ b/ivette/src/frama-c/eva/probes.ts
@@ -8,7 +8,7 @@ import * as Values from 'frama-c/api/plugins/eva/values';
import * as Ast from 'frama-c/api/kernel/ast';
// Model
-import { ModelCallbacks, EvaState } from './cells';
+import { ModelCallbacks } from './cells';
/* --------------------------------------------------------------------------*/
/* --- Probe Labelling ---*/
@@ -46,6 +46,8 @@ export class Probe {
readonly fct: string;
readonly marker: Ast.marker;
readonly model: ModelCallbacks;
+ next?: Probe;
+ prev?: Probe;
transient = true;
loading = true;
label?: string;
@@ -57,7 +59,6 @@ export class Probe {
byCallstacks = false;
zoomed = false;
zoomable = false;
- vstate: EvaState = 'Here';
effects = false;
condition = false;
@@ -66,26 +67,30 @@ export class Probe {
this.marker = marker;
this.model = state;
this.requestProbeInfo = this.requestProbeInfo.bind(this);
- this.setTransient = this.setTransient.bind(this);
}
requestProbeInfo() {
this.loading = true;
+ this.label = '…';
Server
.send(Values.getProbeInfo, this.marker)
.then(({ code, stmt, rank, effects, condition }) => {
this.code = code;
this.stmt = stmt;
this.rank = rank;
+ this.label = undefined;
this.effects = effects;
this.condition = condition;
- this.vstate = effects ? 'After' : 'Here';
this.loading = false;
+ this.updateLabel();
})
.catch(() => {
this.code = '(error)';
this.stmt = undefined;
this.rank = undefined;
+ this.label = undefined;
+ this.effects = false;
+ this.condition = false;
this.loading = false;
})
.finally(this.model.forceLayout);
@@ -95,16 +100,23 @@ export class Probe {
// --- Internal State
// --------------------------------------------------------------------------
- setTransient(tr: boolean) {
+ setPersistent() { this.updateTransient(false); }
+ setTransient() { this.updateTransient(true); }
+
+ private updateLabel() {
+ const { transient, label, code } = this;
+ if (transient && label) {
+ LabelRing.push(label);
+ this.label = undefined;
+ }
+ if (!transient && !label && code && code.length > LabelSize)
+ this.label = newLabel();
+ }
+
+ private updateTransient(tr: boolean) {
if (this.transient !== tr) {
this.transient = tr;
- if (tr && this.label) {
- LabelRing.push(this.label);
- this.label = undefined;
- }
- if (!tr && !this.label && this.code && this.code.length > LabelSize) {
- this.label = newLabel();
- }
+ this.updateLabel();
this.model.forceLayout();
}
}
@@ -112,6 +124,7 @@ export class Probe {
setByCallstacks(byCS: boolean) {
if (byCS !== this.byCallstacks) {
this.byCallstacks = byCS;
+ if (byCS) this.setPersistent();
this.model.forceLayout();
}
}
@@ -123,29 +136,6 @@ export class Probe {
}
}
- setState(s: EvaState | undefined) {
- this.vstate = s ?? 'Here';
- this.model.forceUpdate();
- }
-
- // --------------------------------------------------------------------------
- // --- Ordering
- // --------------------------------------------------------------------------
-
- static order(p: Probe, q: Probe): number {
- const rp = p.rank ?? 0;
- const rq = q.rank ?? 0;
- if (rp < rq) return (-1);
- if (rp > rq) return (+1);
- const cp = p.byCallstacks;
- const cq = q.byCallstacks;
- if (!cp && cq) return (-1);
- if (cp && !cq) return (+1);
- if (p.marker < q.marker) return (-1);
- if (p.marker > q.marker) return (+1);
- return 0;
- }
-
}
/* --------------------------------------------------------------------------*/
diff --git a/ivette/src/frama-c/eva/sized.tsx b/ivette/src/frama-c/eva/sized.tsx
index e092f088c71ab39547c1d626951aa93648049807..bb4b564a1740f236f4d79965a22db56e9b9987ed 100644
--- a/ivette/src/frama-c/eva/sized.tsx
+++ b/ivette/src/frama-c/eva/sized.tsx
@@ -35,6 +35,7 @@ export class Streamer {
}
return this.v;
}
+
}
export class FontSizer {
@@ -73,6 +74,12 @@ export class FontSizer {
return p + n * k;
}
+ dump(x: string) {
+ const k = this.k.mean();
+ const p = this.p.mean();
+ return `${k}.${x}+${p}`;
+ }
+
}
/* --------------------------------------------------------------------------*/
@@ -102,7 +109,7 @@ export function SizedArea(props: SizedAreaProps) {
return (
<div
ref={refSizer}
- className="eva-sized-area dome-text-code"
+ className="eva-sized-area dome-text-cell"
>
{children}
</div>
diff --git a/ivette/src/frama-c/eva/stacks.ts b/ivette/src/frama-c/eva/stacks.ts
index 013638a1630db36810df46b65f3b8cc011226801..891d90fea51c93ca5e28fd5493ba85538cb5ca0c 100644
--- a/ivette/src/frama-c/eva/stacks.ts
+++ b/ivette/src/frama-c/eva/stacks.ts
@@ -3,6 +3,7 @@
// --------------------------------------------------------------------------
import * as Server from 'frama-c/server';
+import * as Ast from 'frama-c/api/kernel/ast';
import * as Values from 'frama-c/api/plugins/eva/values';
import { ModelCallbacks } from './cells';
@@ -15,10 +16,14 @@ export type callstacks = Values.callstack[];
export interface Callsite {
callee: string;
caller?: string;
- stmt?: string;
+ stmt?: Ast.marker;
rank?: number;
}
+function equalSite(a: Callsite, b: Callsite): boolean {
+ return a.stmt === b.stmt && a.callee === b.callee;
+}
+
// --------------------------------------------------------------------------
// --- CallStacks Cache
// --------------------------------------------------------------------------
@@ -27,6 +32,7 @@ export class StacksCache {
private readonly model: ModelCallbacks;
private readonly stacks = new Map<string, callstacks>();
+ private readonly summary = new Map<string, boolean>();
private readonly calls = new Map<Values.callstack, Callsite[]>();
// --------------------------------------------------------------------------
@@ -39,17 +45,29 @@ export class StacksCache {
clear() {
this.stacks.clear();
+ this.calls.clear();
}
// --------------------------------------------------------------------------
// --- Getters
// --------------------------------------------------------------------------
- getStacks(stmt: string): callstacks {
- const cs = this.stacks.get(stmt);
+ getSummary(fct: string): boolean {
+ return this.summary.get(fct) ?? true;
+ }
+
+ setSummary(fct: string, s: boolean) {
+ this.summary.set(fct, s);
+ this.model.forceLayout();
+ }
+
+ getStacks(...markers: Ast.marker[]): callstacks {
+ if (markers.length === 0) return [];
+ const key = markers.join('$');
+ const cs = this.stacks.get(key);
if (cs !== undefined) return cs;
- this.stacks.set(stmt, []);
- this.requestCallstacks(stmt);
+ this.stacks.set(key, []);
+ this.requestStacks(key, markers);
return [];
}
@@ -61,16 +79,30 @@ export class StacksCache {
return [];
}
+ aligned(a: Values.callstack, b: Values.callstack): boolean {
+ if (a === b) return true;
+ const ca = this.getCalls(a);
+ const cb = this.getCalls(b);
+ let ka = ca.length - 1;
+ let kb = cb.length - 1;
+ while (ka >= 0 && kb >= 0 && equalSite(ca[ka], cb[kb])) {
+ --ka;
+ --kb;
+ }
+ return ka < 0 || kb < 0;
+ }
+
// --------------------------------------------------------------------------
// --- Fetchers
// --------------------------------------------------------------------------
- private requestCallstacks(stmt: string) {
+ private requestStacks(key: string, markers: Ast.marker[]) {
Server
- .send(Values.getCallstacks, stmt)
- .then((cs: callstacks) => {
- this.stacks.set(stmt, cs);
+ .send(Values.getCallstacks, markers)
+ .then((stacks: callstacks) => {
+ this.stacks.set(key, stacks);
this.model.forceLayout();
+ this.model.forceUpdate();
});
}
diff --git a/ivette/src/frama-c/eva/style.css b/ivette/src/frama-c/eva/style.css
index 12ff6e4916e8c18aff58de792b27a599606f26d2..e578ea782ba99cb6cf9866b99429f404c0233191 100644
--- a/ivette/src/frama-c/eva/style.css
+++ b/ivette/src/frama-c/eva/style.css
@@ -1,19 +1,3 @@
-/* -------------------------------------------------------------------------- */
-/* --- Styling Values --- */
-/* -------------------------------------------------------------------------- */
-
-.eva-sized-area {
- padding: 3px;
- white-space: pre;
- overflow: hidden;
- text-overflow: ellipsis;
-}
-
-.eva-stmt {
- cursor: default;
- color: grey;
-}
-
/* -------------------------------------------------------------------------- */
/* --- Probe Panel --- */
/* -------------------------------------------------------------------------- */
@@ -36,6 +20,7 @@
.eva-probeinfo-code {
flex: 0 1 auto;
+ height: fit-content;
background: lightgrey;
min-width: 120px;
width: auto;
@@ -70,6 +55,7 @@
.eva-info {
width: 100%;
+ flex-wrap: wrap;
background: #ccc;
padding-top: 3px;
padding-left: 12px;
@@ -77,6 +63,7 @@
}
.eva-callsite {
+ flex: 0 0 auto;
fill: #7cacbb;
background: #eee;
border-radius: 4px;
@@ -84,8 +71,51 @@
padding-right: 7px;
}
-.eva-callsite {
- cursor: default;
+.eva-callsite.eva-focused {
+ background: #cbe4cb;
+}
+
+.eva-callsite.eva-focused.eva-transient {
+ background: #f9dca6;
+}
+
+/* -------------------------------------------------------------------------- */
+/* --- Alarms --- */
+/* -------------------------------------------------------------------------- */
+
+.eva-cell-alarms {
+ fill: orange;
+ position: absolute;
+ top: -1px;
+ right: 3px;
+ z-index: 1;
+}
+
+.eva-alarm-info {
+ font-size: x-small;
+ padding: 0px;
+ margin: 1px;
+}
+
+.eva-alarm-none { display: none; }
+.eva-alarm-True { fill: green; }
+.eva-alarm-False { fill: #fb4e4a; }
+.eva-alarm-Unknown { fill: darkorange; }
+
+/* -------------------------------------------------------------------------- */
+/* --- Styling Values --- */
+/* -------------------------------------------------------------------------- */
+
+.eva-stmt {
+ color: grey;
+ text-select: none;
+}
+
+.eva-sized-area {
+ padding: 3px;
+ white-space: pre;
+ overflow: hidden;
+ text-overflow: ellipsis;
}
/* -------------------------------------------------------------------------- */
@@ -97,41 +127,71 @@
position: relative;
flex: 0 1 auto;
height: 100%;
- border-bottom: thin solid black;
+}
+
+/* -------------------------------------------------------------------------- */
+/* --- Table Heads --- */
+/* -------------------------------------------------------------------------- */
+
+.eva-function {
+ padding-top: 0px;
+ background: #ccc;
+}
+
+.eva-head {
+ padding-top: 2px;
+ color: #777;
+ text-align: center;
border-left: thin solid black;
+ border-bottom: thin solid black;
}
-.eva-probes .eva-row {
+.eva-probes .eva-head {
border-top: thin solid black;
}
+.eva-phantom {
+ visibility: hidden;
+ height: 0;
+}
+
/* -------------------------------------------------------------------------- */
/* --- Table Cells --- */
/* -------------------------------------------------------------------------- */
-.eva-stack {
- width: 12px;
- padding-top: 1px;
- color: #777;
- text-align: center;
+.eva-fct-fold {
+ margin-left: 4px;
+ margin-right: 8px;
+ padding: 0px;
+}
+
+.eva-fct-name {
+ padding: 0px;
+ font-weight: bold;
}
.eva-cell {
flex: 1 1 auto;
border-right: thin solid black;
+ border-bottom: thin solid black;
}
-.eva-cell:nth-child(last) {
- border-right: none;
+.eva-cell:nth-child(2) {
+ border-left: thin solid black;
}
.eva-probes .eva-cell {
padding: 2px;
text-align: center;
+ border-top: thin solid black;
}
+/* -------------------------------------------------------------------------- */
+/* --- Cell Diffs --- */
+/* -------------------------------------------------------------------------- */
+
.eva-diff-shadow {
- border: solid red thin;
+ border: solid transparent 2px;
position: relative;
z-index: -1;
}
@@ -139,87 +199,62 @@
.eva-diff-added { }
.eva-diff-removed { text-decoration: strike }
-.eva-state-Here .eva-diff { background: pink; }
-.eva-state-After .eva-diff { background: yellow; }
-.eva-state-Then .eva-diff { background: green; }
-.eva-state-Else .eva-diff { background: orange; }
-
-/* -------------------------------------------------------------------------- */
-/* --- Alarms --- */
-/* -------------------------------------------------------------------------- */
-
-.eva-cell-alarms {
- fill: orange;
- position: absolute;
- top: -1px;
- right: 3px;
- z-index: 1;
-}
-
-.eva-alarm-info {
- font-size: x-small;
- padding: 0px;
- margin: 1px;
-}
-
-.eva-alarm-True { fill: green; }
-.eva-alarm-False { fill: red; }
-.eva-alarm-Unknown { fill: darkorange; }
+.eva-state-Here .eva-diff { background: #95f5ff; }
+.eva-state-After .eva-diff { background: #fff819; }
+.eva-state-Then .eva-diff { background: #c8e06e; }
+.eva-state-Else .eva-diff { background: #ff834e; }
/* -------------------------------------------------------------------------- */
/* --- Table Rows Background --- */
/* -------------------------------------------------------------------------- */
-.eva-probes .eva-row {
- background: #cbe4cb;
-}
+/* --- Probes --- */
-.eva-values .eva-row {
- background: #eee;
-}
-
-.eva-callstack.eva-row-odd .eva-row {
- background: #eee;
+.eva-probes .eva-cell {
+ background: #cbe4cb;
}
-.eva-callstack.eva-row-even .eva-row {
- background: #e2e8e8;
+.eva-probes .eva-focused {
+ background: #02da02;
}
-.eva-callstack.eva-row-odd .eva-row .eva-transient {
+.eva-probes .eva-transient {
background: #fff0d5;
}
-.eva-callstack.eva-row-even .eva-row .eva-transient {
- background: #fff0d5;
+.eva-probes .eva-transient.eva-focused {
+ background: orange;
}
-.eva-callstack.eva-row-selected .eva-row .eva-transient {
- background: lightblue;
-}
-.eva-callstack.eva-row-selected .eva-row {
- background: lightblue;
+/* --- Values / Callstacks --- */
+
+.eva-values .eva-cell {
+ background: #eee;
}
-.eva-probes .eva-focused {
- background: #02da02;
+.eva-values .eva-focused {
+ background: #e1e8f7;
}
-.eva-probes .eva-transient {
+.eva-values .eva-transient.eva-focused {
background: #fff0d5;
}
-.eva-probes .eva-transient.eva-focused {
- background: orange;
+.eva-callstack.eva-row-odd .eva-cell {
+ background: #eee;
}
-.eva-stack {
- background: #eee;
+.eva-callstack.eva-row-even .eva-cell {
+ background: #e2e8e8;
}
-.eva-callstack.eva-row-selected .eva-stack {
+.eva-callstack.eva-row-aligned {
background: lightblue;
}
+.eva-callstack.eva-row-selected {
+ background: #f9dca6;
+}
+
/* -------------------------------------------------------------------------- */
diff --git a/ivette/src/frama-c/eva/valueinfos.tsx b/ivette/src/frama-c/eva/valueinfos.tsx
new file mode 100644
index 0000000000000000000000000000000000000000..72271f07b54b58aa5f8f0cb486e5a892ae205286
--- /dev/null
+++ b/ivette/src/frama-c/eva/valueinfos.tsx
@@ -0,0 +1,117 @@
+// --------------------------------------------------------------------------
+// --- Info Components
+// --------------------------------------------------------------------------
+
+// React & Dome
+import React from 'react';
+import { classes } from 'dome/misc/utils';
+import { Hpack, Vpack } from 'dome/layout/boxes';
+import { Code, Cell } from 'dome/controls/labels';
+import * as States from 'frama-c/states';
+
+// Locals
+import { EvaAlarm } from './cells';
+import { Callsite } from './stacks';
+import { useModel } from './model';
+
+// --------------------------------------------------------------------------
+// --- Stmt Printer
+// --------------------------------------------------------------------------
+
+interface StmtProps {
+ stmt?: string;
+ rank?: number;
+}
+
+export function Stmt(props: StmtProps) {
+ const { rank, stmt } = props;
+ if (rank === undefined || !stmt) return null;
+ const title = `Stmt at global rank ${rank} (internal id: ${stmt})`;
+ return (
+ <span className="dome-text-cell eva-stmt" title={title}>
+ @S{rank}
+ </span>
+ );
+}
+
+// --------------------------------------------------------------------------
+// --- Alarms Panel
+// --------------------------------------------------------------------------
+
+export function AlarmsInfos() {
+ const model = useModel();
+ const probe = model.getFocused();
+ if (probe) {
+ const callstack = model.getCallstack();
+ const domain = model.values.getValues(probe, callstack);
+ const alarms = domain?.alarms ?? [];
+ if (alarms.length > 0) {
+ const renderAlarm = ([status, alarm]: EvaAlarm) => {
+ const className = `eva-alarm-info eva-alarm-${status}`;
+ return (
+ <Code className={className} icon="WARNING">{alarm}</Code>
+ );
+ };
+ return (
+ <Vpack className="eva-info">
+ {React.Children.toArray(alarms.map(renderAlarm))}
+ </Vpack>
+ );
+ }
+ }
+ return null;
+}
+
+// --------------------------------------------------------------------------
+// --- Stack Panel
+// --------------------------------------------------------------------------
+
+export function StackInfos() {
+ const model = useModel();
+ const [, setSelection] = States.useSelection();
+ const focused = model.getFocused();
+ const callstack = model.getCalls();
+ if (callstack.length <= 1) return null;
+ const makeCallsite = ({ caller, stmt, rank }: Callsite) => {
+ if (!caller || !stmt) return null;
+ const key = `${caller}@${stmt}`;
+ const isFocused = focused?.marker === stmt;
+ const isTransient = focused?.transient;
+ const className = classes(
+ 'eva-callsite',
+ isFocused && 'eva-focused',
+ isTransient && 'eva-transient',
+ );
+ const select = (meta: boolean) => {
+ const location = { fct: caller, marker: stmt };
+ setSelection({ location });
+ if (meta) States.MetaSelection.emit(location);
+ };
+ const onClick = (evt: React.MouseEvent) => {
+ select(evt.altKey);
+ };
+ const onDoubleClick = (evt: React.MouseEvent) => {
+ evt.preventDefault();
+ select(true);
+ };
+ return (
+ <Cell
+ key={key}
+ icon="TRIANGLE.LEFT"
+ className={className}
+ onClick={onClick}
+ onDoubleClick={onDoubleClick}
+ >
+ {caller}
+ <Stmt stmt={stmt} rank={rank} />
+ </Cell>
+ );
+ };
+ return (
+ <Hpack className="eva-info">
+ {callstack.map(makeCallsite)}
+ </Hpack>
+ );
+}
+
+// --------------------------------------------------------------------------
diff --git a/ivette/src/frama-c/eva/valuetable.tsx b/ivette/src/frama-c/eva/valuetable.tsx
new file mode 100644
index 0000000000000000000000000000000000000000..8a4dff4bac16f75bca3f4f18390d08df12333490
--- /dev/null
+++ b/ivette/src/frama-c/eva/valuetable.tsx
@@ -0,0 +1,358 @@
+// --------------------------------------------------------------------------
+// --- Eva Values
+// --------------------------------------------------------------------------
+
+// React & Dome
+import React from 'react';
+import * as Dome from 'dome';
+import { classes } from 'dome/misc/utils';
+import { VariableSizeList } from 'react-window';
+import { Hpack, Filler } from 'dome/layout/boxes';
+import { Icon } from 'dome/controls/icons';
+import { Cell } from 'dome/controls/labels';
+import { IconButton } from 'dome/controls/buttons';
+
+// Frama-C
+import * as States from 'frama-c/states';
+
+// Locals
+import { SizedArea, HSIZER, WSIZER } from './sized';
+import { Diff, DiffProps } from './diffed';
+import { sizeof, EvaValues, EvaState } from './cells';
+import { Probe } from './probes';
+import { Row } from './layout';
+import { Callsite } from './stacks';
+import { useModel } from './model';
+import { Stmt } from './valueinfos';
+import './style.css';
+
+// --------------------------------------------------------------------------
+// --- Cell Diffs
+// --------------------------------------------------------------------------
+
+function isTrivial(v: EvaValues) {
+ return v.values === '{0; 1}' &&
+ v.v_then === '{1}' &&
+ v.v_else === '{0}';
+}
+
+function computeDiffs(
+ condition: boolean,
+ v: EvaValues,
+ vstate: EvaState,
+): DiffProps {
+ if (condition) {
+ const trv = isTrivial(v);
+ switch (vstate) {
+ case 'Here':
+ case 'After':
+ return trv ? { text: v.values } :
+ { text: v.values, diffA: v.v_then, diffB: v.v_else };
+ case 'Then':
+ return { text: v.v_then, diff: !trv ? v.values : undefined };
+ case 'Else':
+ return { text: v.v_else, diff: !trv ? v.values : undefined };
+ }
+ } else {
+ switch (vstate) {
+ case 'Here':
+ case 'Then':
+ case 'Else':
+ return { text: v.values, diff: v.v_after };
+ case 'After':
+ return { text: v.v_after, diff: v.values };
+ }
+ }
+}
+
+// --------------------------------------------------------------------------
+// --- Table Cell
+// --------------------------------------------------------------------------
+
+interface TableCellProps {
+ probe: Probe;
+ row: Row;
+}
+
+const CELLPADDING = 12;
+
+function TableCell(props: TableCellProps) {
+ const model = useModel();
+ const [, setSelection] = States.useSelection();
+ const { probe, row } = props;
+ const { kind, callstack } = row;
+ const minWidth = CELLPADDING + WSIZER.dimension(probe.minCols);
+ const maxWidth = CELLPADDING + WSIZER.dimension(probe.maxCols);
+ const style = { width: minWidth, maxWidth };
+ let contents: React.ReactNode = props.probe.marker;
+ const { transient } = probe;
+ const focused = model.getFocused();
+ const isFocused = focused === probe;
+
+ switch (kind) {
+
+ // ---- Probe Contents
+ case 'probes':
+ if (transient) {
+ contents = <span className="dome-text-label">« Probe »</span>;
+ } else {
+ const { stmt, rank, code, label } = probe;
+ const textClass = label ? 'dome-text-label' : 'dome-text-cell';
+ contents = (
+ <>
+ <span className={textClass}>{label ?? code}</span>
+ <Stmt stmt={stmt} rank={rank} />
+ </>
+ );
+ }
+ break;
+
+ // ---- Values Contents
+ case 'values':
+ case 'callstack':
+ {
+ const domain = model.values.getValues(probe, callstack);
+ const { alarms = [] } = domain;
+ const { condition } = probe;
+ const vstate = condition ? model.getVcond() : model.getVstmt();
+ const vdiffs = computeDiffs(condition, domain, vstate);
+ const text = vdiffs.text ?? vdiffs.diff;
+ const { cols, rows } = sizeof(text);
+ let status = 'none';
+ if (alarms.length > 0) {
+ if (alarms.find(([st, _]) => st === 'False')) status = 'False';
+ else status = 'Unknown';
+ }
+ const alarmClass = `eva-cell-alarms eva-alarm-${status}`;
+ contents = (
+ <>
+ <Icon className={alarmClass} size={10} id="WARNING" />
+ <SizedArea cols={cols} rows={rows}>
+ <span className={`eva-state-${vstate}`}>
+ <Diff {...vdiffs} />
+ </span>
+ </SizedArea>
+ </>
+ );
+ }
+ break;
+
+ }
+
+ // --- Cell Packing
+ const className = classes(
+ 'eva-cell',
+ transient && 'eva-transient',
+ isFocused && 'eva-focused',
+ );
+ const onClick = () => {
+ const location = { fct: probe.fct, marker: probe.marker };
+ setSelection({ location });
+ model.setSelectedRow(row);
+ };
+ const onDoubleClick = () => {
+ probe.setPersistent();
+ if (probe.zoomable) probe.setZoomed(!probe.zoomed);
+ };
+ return (
+ <div
+ className={className}
+ style={style}
+ onClick={onClick}
+ onDoubleClick={onDoubleClick}
+ >
+ {contents}
+ </div>
+ );
+}
+
+// --------------------------------------------------------------------------
+// --- Table Section
+// --------------------------------------------------------------------------
+
+interface TableSectionProps {
+ fct: string;
+ folded: boolean;
+ foldable: boolean;
+ onClick: () => void;
+}
+
+function TableSection(props: TableSectionProps) {
+ const { fct, foldable, folded, onClick } = props;
+ const icon = folded ? 'ANGLE.RIGHT' :
+ foldable ? 'ANGLE.DOWN' : 'TRIANGLE.RIGHT';
+ return (
+ <>
+ <IconButton
+ className="eva-fct-fold"
+ size={10}
+ offset={-1}
+ icon={icon}
+ enabled={foldable}
+ onClick={onClick}
+ />
+ <Cell className="eva-fct-name">{fct}</Cell>
+ </>
+ );
+}
+
+// --------------------------------------------------------------------------
+// --- Table Row Header
+// --------------------------------------------------------------------------
+
+interface TableHeadProps {
+ stackCalls: Callsite[];
+ stackIndex: number | undefined;
+ stackCount: number | undefined;
+ onClick: () => void;
+}
+
+function makeStackTitle(calls: Callsite[]) {
+ const cs = calls.slice(1);
+ if (cs.length > 0)
+ return `Callstack: ${cs.map((c) => c.callee).join(' \u2190 ')}`;
+ return 'Callstack Details';
+}
+
+function TableHead(props: TableHeadProps) {
+ const sk = props.stackIndex;
+ const sc = props.stackCount;
+ const hdClass = classes('eva-head', sc ? undefined : 'dome-hidden');
+ const hdHeader = sk === undefined;
+ const hdSummary = sk !== undefined && sk < 0;
+ const hdNumber = sk === undefined ? 0 : 1 + sk;
+ const hdTitle =
+ hdHeader ? 'Callstack / Summary' :
+ hdSummary ? 'Summary' : makeStackTitle(props.stackCalls);
+ return (
+ <div
+ className={hdClass}
+ title={hdTitle}
+ onClick={props.onClick}
+ >
+ <div className="eva-phantom">{'\u2211'}{sc ?? '#'}</div>
+ {hdHeader ? '#' : hdSummary ? '\u2211' : `${hdNumber}`}
+ </div>
+ );
+}
+
+// --------------------------------------------------------------------------
+// --- Table Row
+// --------------------------------------------------------------------------
+
+interface TableRowProps {
+ style: React.CSSProperties;
+ index: number;
+}
+
+function TableRow(props: TableRowProps) {
+ const model = useModel();
+ const row = model.getRow(props.index);
+ if (!row) return null;
+ const { kind, probes } = row;
+ if (kind === 'section') {
+ const { fct } = row;
+ if (!fct) return null;
+ const folded = model.isFolded(fct);
+ const foldable = model.isFoldable(fct);
+ return (
+ <Hpack className="eva-function" style={props.style}>
+ <TableSection
+ fct={fct}
+ folded={folded}
+ foldable={foldable}
+ onClick={() => model.setFolded(fct, !folded)}
+ />
+ </Hpack>
+ );
+ }
+ const sk = row.stackIndex;
+ const sc = row.stackCount;
+ const cs = row.callstack;
+ const calls = cs ? model.stacks.getCalls(cs) : [];
+ const rowKind = `eva-${kind}`;
+ const rowParity = sk !== undefined && sk % 2 === 1;
+ const rowIndexKind =
+ model.isSelectedRow(row) ? 'eva-row-selected' :
+ model.isAlignedRow(row) ? 'eva-row-aligned' :
+ rowParity ? 'eva-row-odd' : 'eva-row-even';
+ const rowClass = classes('eva-row', rowKind, rowIndexKind);
+ const onHeaderClick = () => model.setSelectedRow(row);
+ const makeCell = (probe: Probe) => (
+ <TableCell
+ key={probe.marker}
+ probe={probe}
+ row={row}
+ />
+ );
+ return (
+ <Hpack style={props.style}>
+ <div className={rowClass}>
+ <TableHead
+ stackIndex={sk}
+ stackCount={sc}
+ stackCalls={calls}
+ onClick={onHeaderClick}
+ />
+ {probes.map(makeCell)}
+ </div>
+ <Filler />
+ </Hpack>
+ );
+}
+
+// --------------------------------------------------------------------------
+// --- Values Panel
+// --------------------------------------------------------------------------
+
+export interface Dimension {
+ width: number;
+ height: number;
+}
+
+export interface ValuesPanelProps extends Dimension {
+ zoom: number;
+}
+
+export function ValuesPanel(props: ValuesPanelProps) {
+ const model = useModel();
+ const { zoom, width, height } = props;
+ // --- reset line cache
+ const listRef = React.useRef<VariableSizeList>(null);
+ Dome.useEvent(model.laidout, () => {
+ setImmediate(() => {
+ const vlist = listRef.current;
+ if (vlist) vlist.resetAfterIndex(0, true);
+ });
+ });
+ // --- compute line height
+ const getRowHeight = React.useCallback(
+ (k: number) => HSIZER.dimension(model.getRowLines(k)),
+ [model],
+ );
+ // --- compute layout
+ const margin = WSIZER.capacity(width);
+ const estimatedHeight = HSIZER.dimension(1);
+ const [selection] = States.useSelection();
+ React.useEffect(() => {
+ const location = selection?.current;
+ model.setLayout({ zoom, margin, location });
+ });
+ // --- render list
+ return (
+ <VariableSizeList
+ ref={listRef}
+ itemCount={model.getRowCount()}
+ itemKey={model.getRowKey}
+ itemSize={getRowHeight}
+ estimatedItemSize={estimatedHeight}
+ width={width}
+ height={height}
+ itemData={model}
+ >
+ {TableRow}
+ </VariableSizeList>
+ );
+}
+
+// --------------------------------------------------------------------------
diff --git a/ivette/src/frama-c/states.ts b/ivette/src/frama-c/states.ts
index 3895ee4978f75af68bed38a3677e579510941174..1feb79a7c847cd568d0ca8be8f36cd29288f9ebf 100644
--- a/ivette/src/frama-c/states.ts
+++ b/ivette/src/frama-c/states.ts
@@ -15,6 +15,7 @@ import { Order } from 'dome/data/compare';
import { GlobalState, useGlobalState } from 'dome/data/states';
import { useModel } from 'dome/table/models';
import { CompactModel } from 'dome/table/arrays';
+import * as Ast from 'frama-c/api/kernel/ast';
import * as Server from './server';
const PROJECT = new Dome.Event('frama-c.project');
@@ -445,22 +446,15 @@ export function useSyncArray<K, A>(
// --- Selection
// --------------------------------------------------------------------------
-type AtLeastOne<T, U = { [K in keyof T]: Pick<T, K> }> =
- Partial<T> & U[keyof U];
-
-export interface FullLocation {
- /** Function name. */
- readonly function: string;
- /** Marker identifier. */
- readonly marker: string;
-}
-
/** An AST location.
*
* Properties [[function]] and [[marker]] are optional,
* but at least one of the two must be set.
*/
-export type Location = AtLeastOne<FullLocation>;
+export type Location = {
+ fct?: string;
+ marker?: Ast.marker;
+};
export interface HistorySelection {
/** Previous locations with respect to the [[current]] one. */
@@ -554,7 +548,7 @@ function isNthSelect(a: SelectionActions): a is NthSelect {
/** Update selection to the given location. */
function selectLocation(s: Selection, location: Location): Selection {
const [prevSelections, nextSelections] =
- s.current && s.current.function !== location.function ?
+ s.current && s.current.fct !== location.fct ?
[[s.current, ...s.history.prevSelections], []] :
[s.history.prevSelections, s.history.nextSelections];
return {
@@ -603,19 +597,18 @@ function fromHistory(s: Selection, action: HistorySelectActions): Selection {
*/
function fromMultipleSelections(
s: Selection,
- action: 'MULTIPLE_PREV' | 'MULTIPLE_NEXT' | 'MULTIPLE_CYCLE'
- | 'MULTIPLE_CLEAR',
+ a: 'MULTIPLE_PREV' | 'MULTIPLE_NEXT' | 'MULTIPLE_CYCLE' | 'MULTIPLE_CLEAR',
): Selection {
- switch (action) {
+ switch (a) {
case 'MULTIPLE_PREV':
case 'MULTIPLE_NEXT':
case 'MULTIPLE_CYCLE': {
const idx =
- action === 'MULTIPLE_PREV' ?
+ a === 'MULTIPLE_PREV' ?
s.multiple.index - 1 :
s.multiple.index + 1;
const index =
- action === 'MULTIPLE_CYCLE' && idx >= s.multiple.allSelections.length ?
+ a === 'MULTIPLE_CYCLE' && idx >= s.multiple.allSelections.length ?
0 :
idx;
if (0 <= index && index < s.multiple.allSelections.length) {
@@ -701,19 +694,20 @@ const emptySelection = {
},
};
-const GlobalSelection = new GlobalState<Selection>(emptySelection);
+export const MetaSelection = new Dome.Event<Location>('frama-c-meta-selection');
+export const GlobalSelection = new GlobalState<Selection>(emptySelection);
Server.onShutdown(() => GlobalSelection.setValue(emptySelection));
+export function setSelection(location: Location, meta = false) {
+ const s = GlobalSelection.getValue();
+ GlobalSelection.setValue(reducer(s, { location }));
+ if (meta) MetaSelection.emit(location);
+}
+
/** Current selection. */
export function useSelection(): [Selection, (a: SelectionActions) => void] {
- const [selection, setSelection] = useGlobalState(GlobalSelection);
-
- function update(action: SelectionActions) {
- const nextSelection = reducer(selection, action);
- setSelection(nextSelection);
- }
-
- return [selection, update];
+ const [current, setCurrent] = useGlobalState(GlobalSelection);
+ return [current, (action) => setCurrent(reducer(current, action))];
}
// --------------------------------------------------------------------------
diff --git a/ivette/src/renderer/ASTinfo.tsx b/ivette/src/renderer/ASTinfo.tsx
index be2aa17a99d70cb07f0ab23ac1a61174ac880922..4ad40c6cfb0f6f7a11ea12881388d5a2e20da908 100644
--- a/ivette/src/renderer/ASTinfo.tsx
+++ b/ivette/src/renderer/ASTinfo.tsx
@@ -33,7 +33,7 @@ const ASTinfo = () => {
// Callbacks
function onTextSelection(id: string) {
// For now, the only markers are functions.
- const location = { function: id };
+ const location = { fct: id };
updateSelection({ location });
}
diff --git a/ivette/src/renderer/ASTview.tsx b/ivette/src/renderer/ASTview.tsx
index 8583af381634c5a90bebcf4e82ac79ff56515e73..36fe6b36ddb648b80bd617ff0c4fea518523f7e5 100644
--- a/ivette/src/renderer/ASTview.tsx
+++ b/ivette/src/renderer/ASTview.tsx
@@ -9,11 +9,10 @@ import * as States from 'frama-c/states';
import * as Utils from 'frama-c/utils';
import * as Dome from 'dome';
-import * as Json from 'dome/data/json';
import { RichTextBuffer } from 'dome/text/buffers';
import { Text } from 'dome/text/editors';
import { Component, TitleBar } from 'frama-c/LabViews';
-import * as AST from 'frama-c/api/kernel/ast';
+import * as Ast from 'frama-c/api/kernel/ast';
import * as Properties from 'frama-c/api/kernel/properties';
import { getCallers, getDeadCode } from 'frama-c/api/plugins/eva/general';
import { getWritesLval, getReadsLval } from 'frama-c/api/plugins/studia/studia';
@@ -38,7 +37,7 @@ async function loadAST(
buffer.log('// Loading', theFunction, '…');
(async () => {
try {
- const data = await Server.send(AST.printFunction, theFunction);
+ const data = await Server.send(Ast.printFunction, theFunction);
buffer.clear();
if (!data) {
buffer.log('// No code for function', theFunction);
@@ -63,7 +62,7 @@ async function loadAST(
async function functionCallers(functionName: string) {
try {
const data = await Server.send(getCallers, functionName);
- const locations = data.map(([fct, marker]) => ({ function: fct, marker }));
+ const locations = data.map(([fct, marker]) => ({ fct, marker }));
return locations;
} catch (err) {
D.error(`Fail to retrieve callers of function '${functionName}':`, err);
@@ -79,12 +78,12 @@ type access = 'Reads' | 'Writes';
async function studia(
marker: string,
- info: AST.markerInfoData,
+ info: Ast.markerInfoData,
kind: access,
) {
const request = kind === 'Reads' ? getReadsLval : getWritesLval;
const data = await Server.send(request, marker);
- const locations = data.direct.map(([f, m]) => ({ function: f, marker: m }));
+ const locations = data.direct.map(([f, m]) => ({ fct: f, marker: m }));
const lval = info.name;
if (locations.length > 0) {
const name = `${kind} of ${lval}`;
@@ -139,7 +138,7 @@ const ASTview = () => {
const printed = React.useRef<string | undefined>();
const [selection, updateSelection] = States.useSelection();
const multipleSelections = selection?.multiple.allSelections;
- const theFunction = selection?.current?.function;
+ const theFunction = selection?.current?.fct;
const theMarker = selection?.current?.marker;
const { buttons: themeButtons, theme, fontSize, wrapText } =
Preferences.useThemeButtons({
@@ -150,7 +149,7 @@ const ASTview = () => {
disabled: !theFunction,
});
- const markersInfo = States.useSyncArray(AST.markerInfo);
+ const markersInfo = States.useSyncArray(Ast.markerInfo);
const deadCode = States.useRequest(getDeadCode, theFunction);
const propertyStatus = States.useSyncArray(Properties.status).getArray();
const statusDict = States.useTags(Properties.propStatusTags);
@@ -158,7 +157,7 @@ const ASTview = () => {
const setBullets = React.useCallback(() => {
if (theFunction) {
propertyStatus.forEach((prop) => {
- if (prop.function === theFunction) {
+ if (prop.fct === theFunction) {
const status = statusDict.get(prop.status);
if (status) {
const bullet = makeBullet(status);
@@ -206,26 +205,25 @@ const ASTview = () => {
if (theMarker) buffer.scroll(theMarker);
}, [buffer, theMarker]);
- function onTextSelection(id: string) {
- if (selection.current) {
- const location = { ...selection.current, marker: id };
- updateSelection({ location });
- }
+ function onSelection(markerId: string, meta = false) {
+ const fct = selection?.current?.fct;
+ const location = { fct, marker: Ast.jMarker(markerId) };
+ updateSelection({ location });
+ if (meta) States.MetaSelection.emit(location);
}
- async function onContextMenu(id: string) {
+ async function onContextMenu(markerId: string) {
const items = [];
- const markerId = (id as Json.key<'#markerInfo'>);
const selectedMarkerInfo = markersInfo.getData(markerId);
if (selectedMarkerInfo?.var === 'function') {
if (selectedMarkerInfo.kind === 'declaration') {
const name = selectedMarkerInfo?.name;
if (name) {
const locations = await functionCallers(name);
- const locationsByFunction = _.groupBy(locations, (e) => e.function);
+ const locationsByFunction = _.groupBy(locations, (e) => e.fct);
_.forEach(locationsByFunction,
(e) => {
- const callerName = e[0].function;
+ const callerName = e[0].fct;
items.push({
label:
`Go to caller ${callerName} ` +
@@ -233,7 +231,7 @@ const ASTview = () => {
onClick: () => updateSelection({
name: `Call sites of function ${name}`,
locations,
- index: locations.findIndex((l) => l.function === callerName),
+ index: locations.findIndex((l) => l.fct === callerName),
}),
});
});
@@ -242,7 +240,7 @@ const ASTview = () => {
items.push({
label: `Go to definition of ${selectedMarkerInfo.name}`,
onClick: () => {
- const location = { function: selectedMarkerInfo.name };
+ const location = { fct: selectedMarkerInfo.name };
updateSelection({ location });
},
});
@@ -252,7 +250,11 @@ const ASTview = () => {
|| selectedMarkerInfo?.var === 'variable';
function onClick(kind: access) {
if (selectedMarkerInfo)
- studia(markerId, selectedMarkerInfo, kind).then(updateSelection);
+ studia(
+ markerId,
+ selectedMarkerInfo,
+ kind,
+ ).then(updateSelection);
}
items.push({
label: 'Studia: select writes',
@@ -281,7 +283,7 @@ const ASTview = () => {
fontSize={fontSize}
lineWrapping={wrapText}
selection={theMarker}
- onSelection={onTextSelection}
+ onSelection={onSelection}
onContextMenu={onContextMenu}
gutters={['bullet']}
readOnly
diff --git a/ivette/src/renderer/Globals.tsx b/ivette/src/renderer/Globals.tsx
index 27d21bc47181ee8f530e98abf2c209324240992b..0a4d754b4fdcfb12cd00740af485edd0ae92275e 100644
--- a/ivette/src/renderer/Globals.tsx
+++ b/ivette/src/renderer/Globals.tsx
@@ -23,7 +23,7 @@ const makeHint = (fct: functionsData): GlobalHint => ({
id: fct.key,
label: fct.name,
title: fct.signature,
- value: { function: fct.name },
+ value: { fct: fct.name },
});
export function useHints(): [GlobalHint[], (pattern: string) => void] {
@@ -101,12 +101,12 @@ export default () => {
function isSelected(fct: functionsData) {
return multipleSelection?.allSelections.some(
- (l) => fct.name === l?.function
+ (l) => fct.name === l?.fct
);
}
// Currently selected function.
- const current: undefined | string = selection?.current?.function;
+ const current: undefined | string = selection?.current?.fct;
function showFunction(fct: functionsData) {
const visible =
@@ -119,7 +119,7 @@ export default () => {
}
function onSelection(name: string) {
- updateSelection({ location: { function: name } });
+ updateSelection({ location: { fct: name } });
}
async function onContextMenu() {
diff --git a/ivette/src/renderer/Locations.tsx b/ivette/src/renderer/Locations.tsx
index b0e3f6c197ada15e1e21c12657c0a839b2dc6a07..22595c3cf9208ea6d51036380624b726333babf4 100644
--- a/ivette/src/renderer/Locations.tsx
+++ b/ivette/src/renderer/Locations.tsx
@@ -124,7 +124,7 @@ const LocationsTable = () => {
width={25}
getter={(r: { id: number }) => r.id + 1}
/>
- <Column id="function" label="Function" width={120} />
+ <Column id="fct" label="Function" width={120} />
<Column
id="marker"
label="Statement"
diff --git a/ivette/src/renderer/Properties.tsx b/ivette/src/renderer/Properties.tsx
index 89737980d9c4855cf01eed52d767aef811f418df..5c77dd726e54444108a87bf9bf74a326d297b005 100644
--- a/ivette/src/renderer/Properties.tsx
+++ b/ivette/src/renderer/Properties.tsx
@@ -235,7 +235,7 @@ const byStatus =
const byProperty: Compare.ByFields<Property> = {
status: byStatus,
- function: Compare.defined(Compare.alpha),
+ fct: Compare.defined(Compare.alpha),
source: bySource,
kind: Compare.structural,
alarm: Compare.defined(Compare.alpha),
@@ -270,7 +270,7 @@ class PropertyModel extends Arrays.CompactModel<Json.key<'#status'>, Property> {
}
filterItem(prop: Property) {
- const kf = prop.function;
+ const kf = prop.fct;
const cf = this.filterFun;
const filteringFun = cf && filter('currentFunction');
const filterFunction = filteringFun ? kf === cf : true;
@@ -424,7 +424,7 @@ const PropertyColumns = () => {
getter={(prop: Property) => prop?.source}
render={renderFile}
/>
- <ColumnCode id="function" label="Function" width={120} />
+ <ColumnCode id="fct" label="Function" width={120} />
<ColumnTag id="kind" label="Property kind" getter={getKind} width={120} />
<ColumnTag id="alarm" label="Alarms" getter={getAlarm} width={160} />
<Column
@@ -477,15 +477,14 @@ const RenderTable = () => {
model.reload();
}, [model, data]);
- const [selection, updateSelection] =
- States.useSelection();
+ const [selection, updateSelection] = States.useSelection();
const [showFilter, flipFilter] =
Dome.useFlipSettings('ivette.properties.showFilter');
// Updating the filter
Dome.useEvent(Reload, model.reload);
- const selectedFunction = selection?.current?.function;
+ const selectedFunction = selection?.current?.fct;
React.useEffect(() => {
model.setFilterFunction(selectedFunction);
}, [model, selectedFunction]);
@@ -493,8 +492,8 @@ const RenderTable = () => {
// Callbacks
const onPropertySelection = React.useCallback(
- ({ key: propKey, function: fct }: Property) => {
- const location = { function: fct, marker: propKey };
+ ({ key: marker, fct }: Property) => {
+ const location = { fct, marker };
updateSelection({ location });
}, [updateSelection],
);
diff --git a/ivette/src/renderer/SourceCode.tsx b/ivette/src/renderer/SourceCode.tsx
index 0c9f8a7dfa42d7a626938d1fe10f5d24016c76a8..aa1ca31d7984a27de13b2a886f9231e5afe1158b 100644
--- a/ivette/src/renderer/SourceCode.tsx
+++ b/ivette/src/renderer/SourceCode.tsx
@@ -7,7 +7,6 @@ import * as States from 'frama-c/states';
import * as Dome from 'dome';
import { readFile } from 'dome/system';
-import * as Json from 'dome/data/json';
import { RichTextBuffer } from 'dome/text/buffers';
import { Text } from 'dome/text/editors';
import { Component, TitleBar } from 'frama-c/LabViews';
@@ -37,7 +36,7 @@ const SourceCode = () => {
// Hooks
const buffer = React.useMemo(() => new RichTextBuffer(), []);
const [selection] = States.useSelection();
- const theFunction = selection?.current?.function;
+ const theFunction = selection?.current?.fct;
const theMarker = selection?.current?.marker;
const { buttons: themeButtons, theme, fontSize, wrapText } =
Preferences.useThemeButtons({
@@ -72,10 +71,8 @@ const SourceCode = () => {
}
// Actual source code loading upon function or marker update.
const sloc =
- /* Non-empty [selection] has defined either marker or function: we give
- precedence to marker as it provides more precise source location. */
- (theMarker &&
- markersInfo.getData(theMarker as Json.key<'#markerInfo'>)?.sloc)
+ /* markers have more precise source location */
+ (theMarker && markersInfo.getData(theMarker)?.sloc)
??
(theFunction && functionsData.find((e) => e.name === theFunction)?.sloc);
if (sloc) {
diff --git a/src/plugins/server/data.ml b/src/plugins/server/data.ml
index 0dc576f61ca97541dd4e906cac794a5827f24732..1f20d6d4c36fb901dfa0745f3250418c76edc568 100644
--- a/src/plugins/server/data.ml
+++ b/src/plugins/server/data.ml
@@ -635,8 +635,8 @@ struct
let get m a =
try M.find a m.index
with Not_found ->
- let id = m.kid in
- m.kid <- succ id ;
+ let id = succ m.kid in
+ m.kid <- id ;
m.index <- M.add a id m.index ;
Hashtbl.add m.lookup id a ; id
diff --git a/src/plugins/server/kernel_ast.ml b/src/plugins/server/kernel_ast.ml
index a8e380889208883e6e45eff039c4180a26dd898c..dfc1510305d2ee0835c65483225a72f20f85c703 100644
--- a/src/plugins/server/kernel_ast.ml
+++ b/src/plugins/server/kernel_ast.ml
@@ -206,7 +206,7 @@ struct
~package
~name:"markerInfo"
~descr:(Md.plain "Marker informations")
- ~key:snd
+ ~key:snd ~keyType:Jstring
~iter model
let create_tag = function
@@ -322,7 +322,7 @@ end
module KfMarker = struct
type record
let record : record Record.signature = Record.signature ()
- let fct = Record.field record ~name:"function"
+ let fct = Record.field record ~name:"fct"
~descr:(Md.plain "Function") (module Kf)
let marker = Record.field record ~name:"marker"
~descr:(Md.plain "Marker") (module Marker)
diff --git a/src/plugins/server/kernel_properties.ml b/src/plugins/server/kernel_properties.ml
index 511c5299a0e354b86bef51f466c5d02b060e0eef..4f09c05dab339a6a5f2f94916f04dd81cdedea4f 100644
--- a/src/plugins/server/kernel_properties.ml
+++ b/src/plugins/server/kernel_properties.ml
@@ -281,7 +281,7 @@ let () = States.column model ~name:"status"
~data:(module PropStatus)
~get:(Property_status.Feedback.get)
-let () = States.column model ~name:"function"
+let () = States.column model ~name:"fct"
~descr:(Md.plain "Function")
~data:(module Joption(Kf)) ~get:Property.get_kf
@@ -330,6 +330,7 @@ let array =
~name:"status"
~descr:(Md.plain "Status of Registered Properties")
~key:(fun ip -> Kernel_ast.Marker.create (PIP ip))
+ ~keyType:Kernel_ast.Marker.jproperty
~iter
~add_update_hook
~add_remove_hook
diff --git a/src/plugins/server/package.ml b/src/plugins/server/package.ml
index 309cae632565703288b5cc95ca1a5793215cfba5..bb87b1da3d58d915060b0455fa705ae855e78eba 100644
--- a/src/plugins/server/package.ml
+++ b/src/plugins/server/package.ml
@@ -208,7 +208,7 @@ type requestInfo = {
type arrayInfo = {
arr_key: string;
- arr_kind: string;
+ arr_kind: jtype;
}
type declKindInfo =
diff --git a/src/plugins/server/package.mli b/src/plugins/server/package.mli
index 952f0dd05659e32932bce624cb57c19fcc2e8741..30075f6243c419aca7d1e4e98ba70462c1704d1d 100644
--- a/src/plugins/server/package.mli
+++ b/src/plugins/server/package.mli
@@ -72,7 +72,7 @@ type requestInfo = {
type arrayInfo = {
arr_key: string;
- arr_kind: string;
+ arr_kind: jtype;
}
type declKindInfo =
diff --git a/src/plugins/server/states.ml b/src/plugins/server/states.ml
index f9ae51a5b8acb166d074e7b2dc88b1624e90c1b1..52a682f2bc7b854e86c8435201fa231ebcc3c4e6 100644
--- a/src/plugins/server/states.ml
+++ b/src/plugins/server/states.ml
@@ -293,9 +293,14 @@ let fetch array n =
(* --- Signature Registry --- *)
(* -------------------------------------------------------------------------- *)
+let rec is_keyType = function
+ | Package.Junion js -> List.for_all is_keyType js
+ | Jstring | Jalpha | Jkey _ | Jtag _ -> true
+ | _ -> false
+
let register_array ~package ~name ~descr ~key
?(keyName="key")
- ?(keyKind=name)
+ ?(keyType=Package.Jkey name)
~(iter : 'a callback)
?(add_update_hook : 'a callback option)
?(add_remove_hook : 'a callback option)
@@ -304,15 +309,24 @@ let register_array ~package ~name ~descr ~key
let open Markdown in
let href = link ~name () in
let columns = List.rev !model in
- if List.exists (fun (fd,_) -> fd.Package.fd_name = keyName) columns then
- raise (Invalid_argument "States.array: key name overrides column name") ;
+ begin
+ if List.exists (fun (fd,_) -> fd.Package.fd_name = keyName) columns then
+ raise (Invalid_argument (
+ Printf.sprintf "States.array(%S) : invalid key %S"
+ name keyName
+ ));
+ if not (is_keyType keyType) then
+ raise (Invalid_argument (
+ Printf.sprintf "States.array(%S): invalid key type" name
+ ));
+ end ;
let fields = Package.{
fd_name = keyName ;
- fd_type = Jkey keyKind ;
+ fd_type = keyType ;
fd_descr = plain "Entry identifier." ;
} :: List.map fst columns in
let id = Package.declare_id ~package:package ~name:name ~descr
- (D_array { arr_key = keyName ; arr_kind = keyKind }) in
+ (D_array { arr_key = keyName ; arr_kind = keyType }) in
let signal = Request.signal
~package ~name:(Package.Derived.signal id).name
~descr:(plain "Signal for array" @ href) in
@@ -331,7 +345,7 @@ let register_array ~package ~name ~descr ~key
let signature = Request.signature ~input:(module Jint) () in
let module Jkeys = Jlist(struct
include Jstring
- let jtype = Package.Jkey keyKind
+ let jtype = keyType
end) in
let module Jrows = Jlist (struct
include Jany
diff --git a/src/plugins/server/states.mli b/src/plugins/server/states.mli
index a75c6c76c8776b067e39b4544c66198d3424fe89..1f38038f83ee1d2b4ea80a1fb1704119e9bf9021 100644
--- a/src/plugins/server/states.mli
+++ b/src/plugins/server/states.mli
@@ -136,7 +136,7 @@ val register_array :
descr:Markdown.text ->
key:('a -> string) ->
?keyName:string ->
- ?keyKind:string ->
+ ?keyType:jtype ->
iter:('a callback) ->
?add_update_hook:('a callback) ->
?add_remove_hook:('a callback) ->
diff --git a/src/plugins/value/api/values_request.ml b/src/plugins/value/api/values_request.ml
index 035340717f3f43761da0c8aeb4d49614d572d6ab..e6587ea85824ad563a6d556b6d85d5c615992eda 100644
--- a/src/plugins/value/api/values_request.ml
+++ b/src/plugins/value/api/values_request.ml
@@ -27,6 +27,7 @@ open Cil_types
module Kmap = Kernel_function.Hashtbl
module Smap = Cil_datatype.Stmt.Hashtbl
module CS = Value_types.Callstack
+module CSet = CS.Set
module CSmap = CS.Hashtbl
module Md = Markdown
@@ -365,11 +366,18 @@ let proxy =
let () = Request.register ~package
~kind:`GET ~name:"getCallstacks"
~descr:(Md.plain "Callstacks for markers")
- ~input:(module Jstmt)
+ ~input:(module Jlist(Jmarker))
~output:(module Jlist(Jcallstack))
- begin fun stmt ->
+ begin fun markers ->
let module A = (val !proxy) in
- Ranking.sort (A.callstacks stmt)
+ let cset = List.fold_left
+ (fun cset marker ->
+ match probe marker with
+ | Pexpr(_,stmt) | Plval(_,stmt) ->
+ List.fold_right CSet.add (A.callstacks stmt) cset
+ | Pnone -> cset
+ ) CSet.empty markers in
+ Ranking.sort (CSet.elements cset)
end
(* -------------------------------------------------------------------------- *)