diff --git a/ivette/.eslintrc.js b/ivette/.eslintrc.js
index 9f7e0ae0e26599d4b5b578352e3047e59457669c..322375d876f3c51d95ac3358b423fc19b4f04e30 100644
--- a/ivette/.eslintrc.js
+++ b/ivette/.eslintrc.js
@@ -24,6 +24,8 @@ module.exports = {
"react/display-name": "off",
// Do not enforce component methods order
"react/sort-comp": "off",
+ // We do not use propTypes
+ "react/require-default-props": "off",
// Be more strict on usage of useMemo and useRef
"react-hooks/exhaustive-deps": "error",
// Allow type any, even if it should be avoided
diff --git a/ivette/api/generated/plugins/eva/values/index.ts b/ivette/api/generated/plugins/eva/values/index.ts
index 0484105632ff59c5958c2eac001e19b40798331e..bc7353fe239426e399d04330a865ab4b616facad 100644
--- a/ivette/api/generated/plugins/eva/values/index.ts
+++ b/ivette/api/generated/plugins/eva/values/index.ts
@@ -24,131 +24,132 @@ import { jMarkerSafe } from 'frama-c/api/kernel/ast';
//@ts-ignore
import { marker } from 'frama-c/api/kernel/ast';
-/** CallStack */
-export interface callstack {
- /** Callstack id */
- id: number;
- /** Short name for the callstack */
- short: string;
- /** Full name for the callstack */
- full: string;
-}
+/** Emitted when EVA results has changed */
+export const changed: Server.Signal = {
+ name: 'plugins.eva.values.changed',
+};
+
+export type callstack = Json.index<'#eva-callstack-id'>;
/** Loose decoder for `callstack` */
export const jCallstack: Json.Loose<callstack> =
- Json.jObject({
- id: Json.jFail(Json.jNumber,'Number expected'),
- short: Json.jFail(Json.jString,'String expected'),
- full: Json.jFail(Json.jString,'String expected'),
- });
+ Json.jIndex<'#eva-callstack-id'>('#eva-callstack-id');
/** Safe decoder for `callstack` */
export const jCallstackSafe: Json.Safe<callstack> =
- Json.jFail(jCallstack,'Callstack expected');
+ Json.jFail(Json.jIndex<'#eva-callstack-id'>('#eva-callstack-id'),
+ '#eva-callstack-id expected');
/** Natural order for `callstack` */
-export const byCallstack: Compare.Order<callstack> =
- Compare.byFields
- <{ id: number, short: string, full: string }>({
- id: Compare.number,
- short: Compare.string,
- full: Compare.string,
- });
-
-/** Data for array rows [`values`](#values) */
-export interface valuesData {
- /** Entry identifier. */
- key: Json.key<'#values'>;
- /** CallStack */
- callstack: callstack;
- /** Value inferred just before the selected point */
- value_before: string;
- /** Did the evaluation led to an alarm? */
- alarm: boolean;
- /** Value inferred just after the selected point */
- value_after?: string;
-}
-
-/** Loose decoder for `valuesData` */
-export const jValuesData: Json.Loose<valuesData> =
- Json.jObject({
- key: Json.jFail(Json.jKey<'#values'>('#values'),'#values expected'),
- callstack: jCallstackSafe,
- value_before: Json.jFail(Json.jString,'String expected'),
- alarm: Json.jFail(Json.jBoolean,'Boolean expected'),
- value_after: Json.jString,
- });
-
-/** Safe decoder for `valuesData` */
-export const jValuesDataSafe: Json.Safe<valuesData> =
- Json.jFail(jValuesData,'ValuesData expected');
-
-/** Natural order for `valuesData` */
-export const byValuesData: Compare.Order<valuesData> =
- Compare.byFields
- <{ key: Json.key<'#values'>, callstack: callstack, value_before: string,
- alarm: boolean, value_after?: string }>({
- key: Compare.string,
- callstack: byCallstack,
- value_before: Compare.string,
- alarm: Compare.boolean,
- value_after: Compare.defined(Compare.string),
- });
+export const byCallstack: Compare.Order<callstack> = Compare.number;
-/** Signal for array [`values`](#values) */
-export const signalValues: Server.Signal = {
- name: 'plugins.eva.values.signalValues',
+const getCallstacks_internal: Server.GetRequest<
+ Json.key<'#stmt'>,
+ callstack[]
+ > = {
+ kind: Server.RqKind.GET,
+ name: 'plugins.eva.values.getCallstacks',
+ input: Json.jKey<'#stmt'>('#stmt'),
+ output: Json.jList(jCallstack),
};
+/** Callstacks for markers */
+export const getCallstacks: Server.GetRequest<Json.key<'#stmt'>,callstack[]>= getCallstacks_internal;
-const reloadValues_internal: Server.GetRequest<null,null> = {
+const getCallstackInfo_internal: Server.GetRequest<
+ callstack,
+ { callee: Json.key<'#fct'>, caller?: Json.key<'#fct'>,
+ stmt?: Json.key<'#stmt'>, rank?: number }[]
+ > = {
kind: Server.RqKind.GET,
- name: 'plugins.eva.values.reloadValues',
- input: Json.jNull,
- output: Json.jNull,
+ name: 'plugins.eva.values.getCallstackInfo',
+ input: jCallstack,
+ output: Json.jList(
+ Json.jObject({
+ callee: Json.jFail(Json.jKey<'#fct'>('#fct'),'#fct expected'),
+ caller: Json.jKey<'#fct'>('#fct'),
+ stmt: Json.jKey<'#stmt'>('#stmt'),
+ rank: Json.jNumber,
+ })),
};
-/** Force full reload for array [`values`](#values) */
-export const reloadValues: Server.GetRequest<null,null>= reloadValues_internal;
-
-const fetchValues_internal: Server.GetRequest<
- number,
- { pending: number, updated: valuesData[], removed: Json.key<'#values'>[],
- reload: boolean }
+/** Callstack Description */
+export const getCallstackInfo: Server.GetRequest<
+ callstack,
+ { callee: Json.key<'#fct'>, caller?: Json.key<'#fct'>,
+ stmt?: Json.key<'#stmt'>, rank?: number }[]
+ >= getCallstackInfo_internal;
+
+const getStmtInfo_internal: Server.GetRequest<
+ Json.key<'#stmt'>,
+ { rank: number, fct: Json.key<'#fct'> }
> = {
kind: Server.RqKind.GET,
- name: 'plugins.eva.values.fetchValues',
- input: Json.jNumber,
+ name: 'plugins.eva.values.getStmtInfo',
+ input: Json.jKey<'#stmt'>('#stmt'),
output: Json.jObject({
- pending: Json.jFail(Json.jNumber,'Number expected'),
- updated: Json.jList(jValuesData),
- removed: Json.jList(Json.jKey<'#values'>('#values')),
- reload: Json.jFail(Json.jBoolean,'Boolean expected'),
+ rank: Json.jFail(Json.jNumber,'Number expected'),
+ fct: Json.jFail(Json.jKey<'#fct'>('#fct'),'#fct expected'),
}),
};
-/** Data fetcher for array [`values`](#values) */
-export const fetchValues: Server.GetRequest<
- number,
- { pending: number, updated: valuesData[], removed: Json.key<'#values'>[],
- reload: boolean }
- >= fetchValues_internal;
-
-const values_internal: State.Array<Json.key<'#values'>,valuesData> = {
- name: 'plugins.eva.values.values',
- getkey: ((d:valuesData) => d.key),
- signal: signalValues,
- fetch: fetchValues,
- reload: reloadValues,
- order: byValuesData,
+/** Stmt Information */
+export const getStmtInfo: Server.GetRequest<
+ Json.key<'#stmt'>,
+ { rank: number, fct: Json.key<'#fct'> }
+ >= getStmtInfo_internal;
+
+const getProbeInfo_internal: Server.GetRequest<
+ marker,
+ { condition: boolean, effects: boolean, rank: number,
+ stmt?: Json.key<'#stmt'>, code?: string }
+ > = {
+ kind: Server.RqKind.GET,
+ name: 'plugins.eva.values.getProbeInfo',
+ input: jMarker,
+ output: Json.jObject({
+ condition: Json.jFail(Json.jBoolean,'Boolean expected'),
+ effects: Json.jFail(Json.jBoolean,'Boolean expected'),
+ rank: Json.jFail(Json.jNumber,'Number expected'),
+ stmt: Json.jKey<'#stmt'>('#stmt'),
+ code: Json.jString,
+ }),
};
-/** Abstract values inferred by the Eva analysis */
-export const values: State.Array<Json.key<'#values'>,valuesData> = values_internal;
-
-const getValues_internal: Server.GetRequest<marker,null> = {
+/** Probe informations */
+export const getProbeInfo: Server.GetRequest<
+ marker,
+ { condition: boolean, effects: boolean, rank: number,
+ stmt?: Json.key<'#stmt'>, code?: string }
+ >= getProbeInfo_internal;
+
+const getValues_internal: Server.GetRequest<
+ { callstack?: callstack, target: marker },
+ { v_else?: string, v_then?: string, v_after?: string, values?: string,
+ alarms: [ "True" | "False" | "Unknown", string ][] }
+ > = {
kind: Server.RqKind.GET,
name: 'plugins.eva.values.getValues',
- input: jMarker,
- output: Json.jNull,
+ input: Json.jObject({ callstack: jCallstack, target: jMarkerSafe,}),
+ output: Json.jObject({
+ v_else: Json.jString,
+ v_then: Json.jString,
+ v_after: Json.jString,
+ values: Json.jString,
+ alarms: Json.jList(
+ Json.jTry(
+ Json.jPair(
+ Json.jFail(
+ Json.jUnion<"True" | "False" | "Unknown">(
+ Json.jTag("True"),
+ Json.jTag("False"),
+ Json.jTag("Unknown"),
+ ),'Union expected'),
+ Json.jFail(Json.jString,'String expected'),
+ ))),
+ }),
};
-/** Get the abstract values computed for an expression or lvalue */
-export const getValues: Server.GetRequest<marker,null>= getValues_internal;
+/** Abstract values for the given marker */
+export const getValues: Server.GetRequest<
+ { callstack?: callstack, target: marker },
+ { v_else?: string, v_then?: string, v_after?: string, values?: string,
+ alarms: [ "True" | "False" | "Unknown", string ][] }
+ >= getValues_internal;
/* ------------------------------------- */
diff --git a/ivette/package.json b/ivette/package.json
index c3e90e667c268ca1470579e8626799a9fa3d7db8..4accc25c115927804617213092dd1a8ebf2aead9 100644
--- a/ivette/package.json
+++ b/ivette/package.json
@@ -55,6 +55,8 @@
"dependencies": {
"@babel/runtime": "^7.9.2",
"@fortawesome/fontawesome-free": "^5.13.1",
+ "@types/diff": "^4.0.2",
+ "@types/react-window": "^1.8.2",
"codemirror": "^5.52.2",
"cytoscape": "^3.15.1",
"cytoscape-cola": "^2.3.1",
@@ -64,6 +66,7 @@
"cytoscape-klay": "^3.1.3",
"cytoscape-panzoom": "^2.5.3",
"cytoscape-popper": "^1.0.7",
+ "diff": "^5.0.0",
"immutable": "^4.0.0-rc.12",
"lodash": "^4.17.15",
"react": "^16.8",
@@ -72,6 +75,7 @@
"react-draggable": "^4.2.0",
"react-fast-compare": "^3.2.0",
"react-virtualized": "^9.21.2",
+ "react-window": "^1.8.6",
"source-map-support": "^0.5.16",
"tippy.js": "5.2.1",
"zeromq": "^6.0.0-beta.5"
diff --git a/ivette/src/dome/src/renderer/controls/buttons.tsx b/ivette/src/dome/src/renderer/controls/buttons.tsx
index 8404310393afa56f12408a72e708647d6593e8ac..871c37c1221660b797f502e089f64f6fe8b632e4 100644
--- a/ivette/src/dome/src/renderer/controls/buttons.tsx
+++ b/ivette/src/dome/src/renderer/controls/buttons.tsx
@@ -239,7 +239,7 @@ export const CircButton = (props: ButtonProps) => {
// --------------------------------------------------------------------------
export type IconButtonKind =
- undefined | 'default' | 'negative' | 'positive' | 'warning';
+ undefined | 'selected' | 'default' | 'negative' | 'positive' | 'warning';
export interface IconButtonProps {
/** Icon identifier. Displayed on the left side of the label. */
@@ -266,6 +266,7 @@ export interface IconButtonProps {
display?: boolean;
/** Styled bytton:
- `'default'`: normal button;
+ - `'selected'`: selection button, in blue;
- `'warning'`: warning button, in orange;
- `'positive'`: positive button, in green;
- `'negative'`: negative button, in red.
diff --git a/ivette/src/dome/src/renderer/controls/style.css b/ivette/src/dome/src/renderer/controls/style.css
index 17e54575b1f8be877d33f17a444bd07f1a1ebbfb..ffbf1cabcf280cee2b4a4a612cc1b7f35e096128 100644
--- a/ivette/src/dome/src/renderer/controls/style.css
+++ b/ivette/src/dome/src/renderer/controls/style.css
@@ -237,7 +237,7 @@
}
.dome-xButton-led-positive {
- background: radial-gradient( circle at center , #00ff0091 , #00ff00 );
+ background: radial-gradient( circle at center , #50c140, #279c16 );
}
.dome-xButton-led-negative {
@@ -288,7 +288,7 @@
.dome-xIconButton-selected:not(:hover) { fill: #449bef ; }
.dome-xIconButton-selected:hover { fill: #c54dae ; }
-.dome-xIconButton-positive { fill: #00d000 ; }
+.dome-xIconButton-positive { fill: #279c16 ; }
.dome-xIconButton-negative { fill: #fb3832 ; }
diff --git a/ivette/src/dome/src/renderer/dome.tsx b/ivette/src/dome/src/renderer/dome.tsx
index b1e1d879afc1defc21759cf0ba17a932a7f41fca..12606069a35c248072e1994daa4a1350f415bdf9 100644
--- a/ivette/src/dome/src/renderer/dome.tsx
+++ b/ivette/src/dome/src/renderer/dome.tsx
@@ -490,12 +490,10 @@ export function useForceUpdate() {
export function useUpdate(...events: Event<any>[]) {
const fn = useForceUpdate();
React.useEffect(() => {
- const trigger = () => setImmediate(fn);
- if (events.length === 0) events.push(update);
- events.forEach((evt) => evt.on(trigger));
- return () => events.forEach((evt) => evt.off(trigger));
- }, [fn, ...events]); // eslint-disable-line react-hooks/exhaustive-deps
- // The rule signals events is missing, probably because of « … »
+ const theEvents = events ? events.slice() : [update];
+ theEvents.forEach((evt) => evt.on(fn));
+ return () => theEvents.forEach((evt) => evt.off(fn));
+ });
}
// --------------------------------------------------------------------------
diff --git a/ivette/src/dome/src/renderer/frame/toolbars.tsx b/ivette/src/dome/src/renderer/frame/toolbars.tsx
index 93d5c78ccc323d1ed613fd8350d8466248e5accf..74696bf0d3f0e4d436eb316d036871a7c0781a33 100644
--- a/ivette/src/dome/src/renderer/frame/toolbars.tsx
+++ b/ivette/src/dome/src/renderer/frame/toolbars.tsx
@@ -91,6 +91,10 @@ export interface ButtonProps<A> {
title?: string;
/** Button kind. */
kind?: ButtonKind;
+ /** Button is displayed (default `true`). */
+ visible?: boolean;
+ /** Button is hidden (default `false`). */
+ hidden?: boolean;
/** Enabled State (default `true`). */
enabled?: boolean;
/** Disabled State (default `false`). */
@@ -107,8 +111,10 @@ export interface ButtonProps<A> {
/** Toolbar Button. */
export function Button<A = undefined>(props: ButtonProps<A>) {
- const { selected, value, selection, onClick } = props;
+ const { visible = true, hidden = false } = props;
+ if (!visible || hidden) return null;
const { enabled = true, disabled = false } = props;
+ const { selected, value, selection, onClick } = props;
const isSelected = selected !== undefined
? selected
: (value !== undefined && value === selection);
@@ -147,13 +153,18 @@ export interface SelectionProps<A> {
// --- ToolBar Button Group
// --------------------------------------------------------------------------
+export interface ButtonGroupProps<A> extends SelectionProps<A> {
+ className?: string;
+ style?: React.CSSProperties;
+}
+
/**
Toolbar Button Group.
Properties of the button group are passed down the buttons of the group
as appropriate defaults.
*/
-export function ButtonGroup<A>(props: SelectionProps<A>) {
+export function ButtonGroup<A>(props: ButtonGroupProps<A>) {
const { children, value, onChange, enabled, disabled } = props;
const baseProps: ButtonProps<A> = {
enabled,
@@ -161,8 +172,9 @@ export function ButtonGroup<A>(props: SelectionProps<A>) {
selection: value,
onClick: onChange,
};
+ const className = classes('dome-xToolBar-group', props.className);
return (
- <div className="dome-xToolBar-group">
+ <div className={className} style={props.style}>
{React.Children.map(children, (elt) => React.cloneElement(
elt,
{ ...baseProps, ...elt.props },
diff --git a/ivette/src/frama-c/eva/Values.tsx b/ivette/src/frama-c/eva/Values.tsx
new file mode 100644
index 0000000000000000000000000000000000000000..6bdf15345c8728ade58b0881b2e451cca04f9264
--- /dev/null
+++ b/ivette/src/frama-c/eva/Values.tsx
@@ -0,0 +1,480 @@
+// --------------------------------------------------------------------------
+// --- 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 { Vfill, Hpack, Vpack, Filler } from 'dome/layout/boxes';
+import { Icon } from 'dome/controls/icons';
+import { Label, Code } from 'dome/controls/labels';
+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 './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
+// --------------------------------------------------------------------------
+
+function ValuesComponent() {
+ const [zoom, setZoom] = Dome.useNumberSettings('eva-zoom-factor', 0);
+ return (
+ <>
+ <TitleBar>
+ <IconButton
+ enabled={zoom > 0}
+ icon="ZOOM.OUT"
+ onClick={() => setZoom(zoom - 1)}
+ />
+ <IconButton
+ enabled={zoom < 20}
+ icon="ZOOM.IN"
+ onClick={() => setZoom(zoom + 1)}
+ />
+ </TitleBar>
+ <Vfill>
+ <ProbeInfos />
+ <Vfill>
+ <AutoSizer>
+ {(dim: Dimension) => (
+ <ValuesPanel
+ zoom={zoom}
+ {...dim}
+ />
+ )}
+ </AutoSizer>
+ </Vfill>
+ <AlarmsInfo />
+ <StackInfo />
+ </Vfill>
+ </>
+ );
+}
+
+// --------------------------------------------------------------------------
+// --- Export Component
+// --------------------------------------------------------------------------
+
+export default () => (
+ <Component
+ id="frama-c.values"
+ label="Eva Values"
+ title="Values inferred by the Eva analysis"
+ >
+ <ValuesComponent />
+ </Component>
+);
+
+// --------------------------------------------------------------------------
diff --git a/ivette/src/frama-c/eva/cells.ts b/ivette/src/frama-c/eva/cells.ts
new file mode 100644
index 0000000000000000000000000000000000000000..acb3e9ea05432b1ef0952432b9cb098a0059e90f
--- /dev/null
+++ b/ivette/src/frama-c/eva/cells.ts
@@ -0,0 +1,250 @@
+// --------------------------------------------------------------------------
+// --- Cells
+// --------------------------------------------------------------------------
+
+// Frama-C
+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';
+
+// --------------------------------------------------------------------------
+// --- Cell Utilities
+// --------------------------------------------------------------------------
+
+export type callback = () => void;
+
+export interface ModelCallbacks {
+ forceUpdate: callback;
+ forceLayout: callback;
+}
+
+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;
+ const lines = text.split('\n');
+ return {
+ rows: lines.length,
+ cols: lines.reduce((w, l) => Math.max(w, l.length), 0),
+ };
+}
+
+export function merge(a: Size, b: Size): Size {
+ return {
+ cols: Math.max(a.cols, b.cols),
+ rows: Math.max(a.rows, b.rows),
+ };
+}
+
+export function addH(a: Size, b: Size, padding = 0): Size {
+ return {
+ cols: a.cols + b.cols + padding,
+ rows: Math.max(a.rows, b.rows),
+ };
+}
+
+export function addV(a: Size, b: Size, padding = 0): Size {
+ return {
+ cols: Math.max(a.cols, b.cols),
+ rows: a.rows + b.rows + padding,
+ };
+}
+
+export function addS(s: Size, t: string | undefined): Size {
+ return t ? merge(s, sizeof(t)) : s;
+}
+
+export function lt(a: Size, b: Size): boolean {
+ return a.rows < b.rows && a.cols < b.cols;
+}
+
+export function leq(a: Size, b: Size): boolean {
+ return a.rows <= b.rows && a.cols <= b.cols;
+}
+
+// --------------------------------------------------------------------------
+// --- Data
+// --------------------------------------------------------------------------
+
+export type EvaStatus = 'True' | 'False' | 'Unknown';
+export type EvaAlarm = [EvaStatus, string];
+export type EvaState = 'Here' | 'After' | 'Then' | 'Else';
+
+export interface EvaValues {
+ errors?: string;
+ values?: string;
+ v_after?: string;
+ v_then?: string;
+ v_else?: string;
+ alarms?: EvaAlarm[];
+ 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 class ValueCache {
+
+ private readonly state: ModelCallbacks;
+ private readonly probes = new Map<Ast.marker, Size>(); // Marker -> max in column
+ private readonly stacks = new Map<string, Size>(); // Callstack -> max in row
+ private readonly vcache = new Map<string, EvaValues>(); // '<Marker><@Callstack>?' -> value
+ private smax = EMPTY; // max cell size
+
+ constructor(state: ModelCallbacks) {
+ this.state = state;
+ }
+
+ clear() {
+ this.smax = EMPTY;
+ this.probes.clear();
+ this.stacks.clear();
+ this.vcache.clear();
+ this.state.forceLayout();
+ }
+
+ // --- Cached Measures
+
+ getMaxSize() { return this.smax; }
+
+ getProbeSize(target: Ast.marker) {
+ return this.probes.get(target) ?? EMPTY;
+ }
+
+ private static stackKey(stmt: string, callstack: Values.callstack) {
+ return `${stmt}::${callstack}`;
+ }
+
+ getStackSize(stmt: string, callstack: Values.callstack) {
+ const key = ValueCache.stackKey(stmt, callstack);
+ return this.stacks.get(key) ?? EMPTY;
+ }
+
+ // --- Cached Values & Request Update
+
+ getValues(
+ target: Ast.marker,
+ stmt: string | undefined,
+ callstack: Values.callstack | undefined,
+ ): EvaValues {
+ const key = callstack !== undefined ? `${target}@${callstack}` : target;
+ const cache = this.vcache;
+ const cached = cache.get(key);
+ if (cached) return cached;
+ const newValue: EvaValues = { values: '', size: EMPTY };
+ if (callstack !== undefined && stmt === undefined)
+ return newValue;
+ // callstack !== undefined ==> stmt !== undefined)
+ cache.set(key, newValue);
+ Server
+ .send(Values.getValues, { target, callstack })
+ .then((r) => {
+ newValue.errors = undefined;
+ newValue.values = r.values;
+ newValue.v_after = r.v_after;
+ newValue.v_then = r.v_then;
+ newValue.v_else = r.v_else;
+ newValue.alarms = r.alarms;
+ if (this.updateLayout(target, stmt, callstack, newValue))
+ this.state.forceLayout();
+ else
+ this.state.forceUpdate();
+ })
+ .catch((err) => {
+ newValue.errors = `$Error: ${err}`;
+ this.state.forceUpdate();
+ });
+ return newValue;
+ }
+
+ // --- Updating Measures
+
+ private updateLayout(
+ target: Ast.marker,
+ stmt: string | undefined,
+ callstack: Values.callstack | undefined,
+ v: EvaValues,
+ ): boolean {
+ // measuring cell
+ let s = sizeof(v.values);
+ s = addS(s, v.v_after);
+ s = addS(s, v.v_then);
+ s = addS(s, v.v_else);
+ v.size = s;
+ // max cell size
+ const { smax } = this;
+ let small = leq(s, smax);
+ if (!small) this.smax = merge(s, smax);
+ // max size for probe column
+ const ps = this.getProbeSize(target);
+ if (!leq(s, ps)) {
+ this.probes.set(target, merge(ps, s));
+ small = false;
+ }
+ // max size for stack row
+ if (callstack !== undefined) {
+ if (stmt === undefined) small = false;
+ else {
+ const key = ValueCache.stackKey(stmt, callstack);
+ const cs = this.stacks.get(key) ?? EMPTY;
+ if (!leq(s, cs)) {
+ this.stacks.set(key, merge(cs, s));
+ small = false;
+ }
+ }
+ }
+ // request new layout if not small enough
+ return !small;
+ }
+
+}
+
+// --------------------------------------------------------------------------
diff --git a/ivette/src/frama-c/eva/diffed.tsx b/ivette/src/frama-c/eva/diffed.tsx
new file mode 100644
index 0000000000000000000000000000000000000000..9edf57ee95f6edd03c49de4f3935ad4dbb70156a
--- /dev/null
+++ b/ivette/src/frama-c/eva/diffed.tsx
@@ -0,0 +1,160 @@
+// --------------------------------------------------------------------------
+// --- Diff Text Rendering
+// --------------------------------------------------------------------------
+
+import React from 'react';
+import { Change, diffChars } from 'diff';
+
+const MODIFIED = 'eva-diff eva-diff-modified';
+const REMOVED = 'eva-diff eva-diff-removed';
+const ADDED = 'eva-diff eva-diff-added';
+const SHADOW = 'eva-diff eva-diff-shadow';
+
+export class DiffBuffer {
+
+ private added = false;
+ private removed = false;
+ private value = '';
+ private scratch = '';
+ private contents: React.ReactNode[] = [];
+
+ constructor() {
+ this.push = this.push.bind(this);
+ }
+
+ clear() {
+ this.added = false;
+ this.removed = false;
+ this.value = '';
+ this.scratch = '';
+ this.contents = [];
+ }
+
+ push(c: Change) {
+ if (!c.added && !c.removed) {
+ this.flush();
+ this.value += c.value;
+ this.flush();
+ } else {
+ if (c.added) this.added = true;
+ if (c.removed) {
+ this.removed = true;
+ this.value += c.value;
+ }
+ }
+ }
+
+ private flush() {
+ const { value, added, removed } = this;
+ if (added && removed) {
+ if (value) {
+ this.scratch += '\0'.repeat(value.length);
+ this.contents.push(
+ <span className={MODIFIED} title="Modified"> {value}</span>,
+ );
+ }
+ } else if (removed) {
+ if (value) {
+ this.contents.push(
+ <span className={REMOVED} title="Removed">{value}</span>,
+ );
+ }
+ } else if (added) {
+ this.contents.push(
+ <span className={ADDED}><span className={SHADOW} /></span>,
+ );
+ } else if (value) {
+ this.scratch += value;
+ this.contents.push(value);
+ }
+ this.value = '';
+ this.added = false;
+ this.removed = false;
+ }
+
+ getContents(): React.ReactNode {
+ this.flush();
+ return <>{React.Children.toArray(this.contents)}</>;
+ }
+
+ getScratch() {
+ this.flush();
+ return this.scratch;
+ }
+
+}
+
+/* --------------------------------------------------------------------------*/
+/* --- Diff2 Component ---*/
+/* --------------------------------------------------------------------------*/
+
+export interface Diff2Props {
+ text: string;
+ diff: string;
+}
+
+export function Diff2(props: Diff2Props): JSX.Element {
+ const { text, diff } = props;
+ const contents = React.useMemo(() => {
+ 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;
+}
+
+/* --------------------------------------------------------------------------*/
+/* --- Diff3 Component ---*/
+/* --------------------------------------------------------------------------*/
+
+export interface Diff3Props {
+ text: string;
+ diffA: string;
+ diffB: string;
+}
+
+export function Diff3(props: Diff3Props): JSX.Element {
+ const { text, diffA, diffB } = props;
+ const contents = React.useMemo(() => {
+ if (text === diffA && text === diffB) return text;
+ const buffer = new DiffBuffer();
+ diffChars(diffA, diffB).forEach(buffer.push);
+ const scratch = buffer.getScratch();
+ buffer.clear();
+ diffChars(text, scratch).forEach(buffer.push);
+ return buffer.getContents();
+ }, [text, diffA, diffB]);
+ return contents as JSX.Element;
+}
+
+/* --------------------------------------------------------------------------*/
+/* --- Diff Component ---*/
+/* --------------------------------------------------------------------------*/
+
+export interface DiffProps {
+ text: string;
+ diff?: string;
+ diffA?: string;
+ diffB?: string;
+}
+
+export function Diff(props: DiffProps): JSX.Element {
+ const { text, diff, diffA, diffB } = props;
+ if (text === diff) return <>{text}</>;
+ if (diff !== undefined)
+ return <Diff2 text={text} diff={diff} />;
+ if (diffA === undefined) {
+ if (diffB === undefined) return <>{text}</>;
+ return <Diff2 text={text} diff={diffB} />;
+ } if (diffB === undefined) {
+ if (diffA === undefined) return <>{text}</>;
+ 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
new file mode 100644
index 0000000000000000000000000000000000000000..c416fa7c8945753a5ac0ff2490a9618ac73bc430
--- /dev/null
+++ b/ivette/src/frama-c/eva/layout.ts
@@ -0,0 +1,146 @@
+/* --------------------------------------------------------------------------*/
+/* --- Layout ---*/
+/* --------------------------------------------------------------------------*/
+
+import { callstack } from 'frama-c/api/plugins/eva/values';
+import { Probe } from './probes';
+import { StacksCache } from './stacks';
+import { Size, EMPTY, leq, addH, ValueCache } from './cells';
+
+export interface LayoutProps {
+ zoom?: number;
+ margin: number;
+}
+
+export type RowKind = 'probes' | 'values' | 'callstack';
+
+export interface Row {
+ key: string;
+ kind: RowKind;
+ probes: Probe[];
+ headstack?: string;
+ stacks?: number;
+ stackIndex?: number;
+ callstack?: callstack;
+ hlines: number;
+}
+
+/* --------------------------------------------------------------------------*/
+/* --- Layout Enfine ---*/
+/* --------------------------------------------------------------------------*/
+
+const PADDING = 2;
+const INSET = 1;
+const HCROP = 18;
+const VCROP = 1;
+
+export class LayoutEngine {
+
+ // --- Setup
+
+ private readonly values: ValueCache;
+ private readonly stacks: StacksCache;
+ private readonly hcrop: number;
+ private readonly vcrop: number;
+ private readonly margin: number;
+
+ constructor(
+ props: undefined | LayoutProps,
+ values: ValueCache,
+ stacks: StacksCache,
+ ) {
+ this.values = values;
+ this.stacks = stacks;
+ const zoom = Math.max(0, props?.zoom ?? 0);
+ this.vcrop = VCROP + 2 * zoom;
+ this.hcrop = HCROP + zoom;
+ this.margin = props?.margin ?? 80;
+ this.push = this.push.bind(this);
+ }
+
+ // --- Probe Buffer
+ private byStacks?: string; // stmt
+ private rowSize: Size = EMPTY;
+ private buffer: Probe[] = [];
+ private rows: Row[] = [];
+
+ crop(zoomed: boolean, s: Size): Size {
+ const sCols = s.cols + INSET;
+ const cols = zoomed ? sCols : Math.min(sCols, this.hcrop);
+ const rows = zoomed ? s.rows : Math.min(s.rows, this.vcrop);
+ return {
+ cols: Math.max(HCROP, cols),
+ rows: Math.max(VCROP, rows),
+ };
+ }
+
+ push(p: Probe) {
+ 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)
+ this.flush();
+ this.rowSize = addH(this.rowSize, s);
+ this.rowSize.cols += PADDING;
+ this.buffer.push(p);
+ }
+
+ // --- Flush Rows
+
+ flush(): Row[] {
+ const ps = this.buffer;
+ const rs = this.rows;
+ if (ps.length > 0) {
+ const stmt = this.byStacks;
+ if (stmt) {
+ // --- by callstacks
+ const wcs = this.stacks.getStacks(stmt);
+ rs.push({
+ key: `P${stmt}`,
+ kind: 'probes',
+ probes: ps,
+ stacks: wcs.length,
+ hlines: 1,
+ });
+ wcs.forEach((cs, k) => {
+ rs.push({
+ key: `C${stmt}::${cs}`,
+ kind: 'callstack',
+ probes: ps,
+ stackIndex: k,
+ stacks: wcs.length,
+ callstack: cs,
+ hlines: this.values.getStackSize(stmt, cs).rows,
+ });
+ });
+ } else {
+ // --- by callstacks
+ const n = rs.length;
+ rs.push({
+ key: `P${n}`,
+ kind: 'probes',
+ probes: ps,
+ hlines: 1,
+ }, {
+ key: `V${n}`,
+ kind: 'values',
+ probes: ps,
+ hlines: this.rowSize.rows,
+ });
+ }
+ }
+ this.buffer = [];
+ this.rowSize = EMPTY;
+ return rs;
+ }
+
+}
+
+/* --------------------------------------------------------------------------*/
diff --git a/ivette/src/frama-c/eva/model.ts b/ivette/src/frama-c/eva/model.ts
new file mode 100644
index 0000000000000000000000000000000000000000..6f24c809c84d2360cc6a461d60e7c09ef7dcd0d0
--- /dev/null
+++ b/ivette/src/frama-c/eva/model.ts
@@ -0,0 +1,212 @@
+// --------------------------------------------------------------------------
+// --- Eva Values
+// --------------------------------------------------------------------------
+
+// External Libs
+import { throttle } from 'lodash';
+import equal from 'react-fast-compare';
+import * as Dome from 'dome';
+
+import * as Server from 'frama-c/server';
+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 { LayoutProps, LayoutEngine, Row } from './layout';
+
+export interface ModelLayout extends LayoutProps {
+ fct?: string;
+ marker?: Ast.marker;
+}
+
+/* --------------------------------------------------------------------------*/
+/* --- EVA Values Model ---*/
+/* --------------------------------------------------------------------------*/
+
+export class Model implements ModelCallbacks {
+
+ constructor() {
+ this.forceUpdate = this.forceUpdate.bind(this);
+ this.forceLayout = this.forceLayout.bind(this);
+ this.forceReload = this.forceReload.bind(this);
+ this.computeLayout = this.computeLayout.bind(this);
+ this.setLayout = throttle(this.setLayout.bind(this), 300);
+ this.getRowKey = this.getRowKey.bind(this);
+ this.getRowCount = this.getRowCount.bind(this);
+ this.getRowLines = this.getRowLines.bind(this);
+ Server.onSignal(Values.changed, this.forceReload);
+ }
+
+ // --- Probes
+
+ private selected?: Probe;
+ private focused?: Probe;
+ private callstack?: Values.callstack;
+ private remanent?: Probe; // last transient
+ private probes = new Map<string, Probe>();
+
+ 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();
+ }
+ return p;
+ }
+
+ getStacks(p: Probe | undefined): Values.callstack[] {
+ const stmt = p?.stmt;
+ return stmt ? this.stacks.getStacks(stmt) : [];
+ }
+
+ // --- Caches
+
+ readonly stacks = new StacksCache(this);
+ readonly values = new ValueCache(this);
+
+ // --- Rows
+
+ private lock = false;
+ private layout: ModelLayout = { margin: 80 };
+ private rows: Row[] = [];
+
+ getRow(index: number): Row | undefined {
+ return this.rows[index];
+ }
+
+ getRowCount() {
+ return this.rows.length;
+ }
+
+ getRowKey(index: number): string {
+ const row = this.rows[index];
+ return row ? row.key : `#${index}`;
+ }
+
+ getRowLines(index: number): number {
+ const row = this.rows[index];
+ return row ? row.hlines : 0;
+ }
+
+ setSelectedRow(row: Row) {
+ const cs = row.callstack;
+ if (cs !== this.callstack) {
+ this.callstack = cs;
+ this.forceUpdate();
+ }
+ }
+
+ isSelectedRow(row: Row): boolean {
+ const cs = this.callstack;
+ return cs !== undefined ? cs === row.callstack : false;
+ }
+
+ getCallstack(): Values.callstack | undefined {
+ return this.callstack;
+ }
+
+ getCalls(): Callsite[] {
+ const c = this.callstack;
+ return c === undefined ? [] : this.stacks.getCalls(c);
+ }
+
+ // --- Throttled
+ 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.forceLayout();
+ }
+ }
+
+ // --- Recompute Layout
+
+ private computeLayout() {
+ if (this.lock) return;
+ this.lock = true;
+ 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 {
+ this.remanent = undefined;
+ }
+ }
+ const toLayout: Probe[] = [];
+ this.probes.forEach((p) => {
+ if (p.code && (!p.transient || p === this.remanent)) {
+ toLayout.push(p);
+ }
+ });
+ const engine = new LayoutEngine(
+ this.layout,
+ this.values,
+ this.stacks,
+ );
+ toLayout.sort(Probe.order).forEach(engine.push);
+ this.rows = engine.flush();
+ this.laidout.emit();
+ this.lock = false;
+ }
+
+ // --- Force Reload (empty caches)
+ forceReload() {
+ this.focused = undefined;
+ this.remanent = undefined;
+ this.selected = undefined;
+ this.callstack = undefined;
+ this.probes.clear();
+ this.stacks.clear();
+ this.values.clear();
+ this.forceLayout();
+ this.forceUpdate();
+ }
+
+ // --- Events
+ readonly changed = new Dome.Event('eva-changed');
+ readonly laidout = new Dome.Event('eva-laidout');
+
+ // --- Force Layout
+ forceLayout() {
+ setImmediate(this.computeLayout);
+ }
+
+ // --- Foce Update
+ forceUpdate() { this.changed.emit(); }
+
+}
+
+// --------------------------------------------------------------------------
+// --- EVA Model
+// --------------------------------------------------------------------------
+
+let MODEL: Model | undefined;
+
+export function getModelInstance(): Model {
+ if (!MODEL) MODEL = new Model();
+ return MODEL;
+}
+
+// --------------------------------------------------------------------------
diff --git a/ivette/src/frama-c/eva/probes.ts b/ivette/src/frama-c/eva/probes.ts
new file mode 100644
index 0000000000000000000000000000000000000000..c920d71d0068667623c4e98973e82a291bad2313
--- /dev/null
+++ b/ivette/src/frama-c/eva/probes.ts
@@ -0,0 +1,151 @@
+/* --------------------------------------------------------------------------*/
+/* --- Probes ---*/
+/* --------------------------------------------------------------------------*/
+
+// Frama-C
+import * as Server from 'frama-c/server';
+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';
+
+/* --------------------------------------------------------------------------*/
+/* --- Probe Labelling ---*/
+/* --------------------------------------------------------------------------*/
+
+const Ka = 'A'.charCodeAt(0);
+const Kz = 'Z'.charCodeAt(0);
+const LabelRing: string[] = [];
+const LabelSize = 12;
+let La = Ka;
+let Lk = 0;
+
+function newLabel() {
+ let lbl = LabelRing.shift();
+ if (lbl) return lbl;
+ const a = La;
+ const k = Lk;
+ lbl = String.fromCharCode(a);
+ if (a < Kz) {
+ La++;
+ } else {
+ La = Ka;
+ Lk++;
+ }
+ return k > 0 ? lbl + k : lbl;
+}
+
+/* --------------------------------------------------------------------------*/
+/* --- Probe State ---*/
+/* --------------------------------------------------------------------------*/
+
+export class Probe {
+
+ // properties
+ readonly fct: string;
+ readonly marker: Ast.marker;
+ readonly model: ModelCallbacks;
+ transient = true;
+ loading = true;
+ label?: string;
+ code?: string;
+ stmt?: string;
+ rank?: number;
+ minCols: number = LabelSize;
+ maxCols: number = LabelSize;
+ byCallstacks = false;
+ zoomed = false;
+ zoomable = false;
+ vstate: EvaState = 'Here';
+ effects = false;
+ condition = false;
+
+ constructor(state: ModelCallbacks, fct: string, marker: Ast.marker) {
+ this.fct = fct;
+ this.marker = marker;
+ this.model = state;
+ this.requestProbeInfo = this.requestProbeInfo.bind(this);
+ this.setTransient = this.setTransient.bind(this);
+ }
+
+ requestProbeInfo() {
+ this.loading = true;
+ Server
+ .send(Values.getProbeInfo, this.marker)
+ .then(({ code, stmt, rank, effects, condition }) => {
+ this.code = code;
+ this.stmt = stmt;
+ this.rank = rank;
+ this.effects = effects;
+ this.condition = condition;
+ this.vstate = effects ? 'After' : 'Here';
+ this.loading = false;
+ })
+ .catch(() => {
+ this.code = '(error)';
+ this.stmt = undefined;
+ this.rank = undefined;
+ this.loading = false;
+ })
+ .finally(this.model.forceLayout);
+ }
+
+ // --------------------------------------------------------------------------
+ // --- Internal State
+ // --------------------------------------------------------------------------
+
+ setTransient(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.model.forceLayout();
+ }
+ }
+
+ setByCallstacks(byCS: boolean) {
+ if (byCS !== this.byCallstacks) {
+ this.byCallstacks = byCS;
+ this.model.forceLayout();
+ }
+ }
+
+ setZoomed(zoomed: boolean) {
+ if (zoomed !== this.zoomed) {
+ this.zoomed = zoomed;
+ this.model.forceLayout();
+ }
+ }
+
+ 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
new file mode 100644
index 0000000000000000000000000000000000000000..e092f088c71ab39547c1d626951aa93648049807
--- /dev/null
+++ b/ivette/src/frama-c/eva/sized.tsx
@@ -0,0 +1,112 @@
+// --------------------------------------------------------------------------
+// --- Sized Cell
+// --------------------------------------------------------------------------
+
+import React from 'react';
+
+// --------------------------------------------------------------------------
+// --- Measurer
+// --------------------------------------------------------------------------
+
+export class Streamer {
+ private readonly v0: number;
+ private readonly vs: number[] = [];
+ private v?: number;
+ constructor(v0: number) {
+ this.v0 = v0;
+ }
+
+ push(v: number) {
+ const { vs } = this;
+ vs.push(Math.round(v));
+ if (vs.length > 200) vs.shift();
+ }
+
+ mean(): number {
+ if (this.v === undefined) {
+ const { vs } = this;
+ const n = vs.length;
+ if (n > 0) {
+ const m = vs.reduce((s, v) => s + v, 0) / n;
+ this.v = Math.round(m + 0.5);
+ } else {
+ this.v = this.v0;
+ }
+ }
+ return this.v;
+ }
+}
+
+export class FontSizer {
+ a = 0;
+ b = 0;
+ k: Streamer;
+ p: Streamer;
+
+ constructor(k: number, p: number) {
+ this.k = new Streamer(k);
+ this.p = new Streamer(p);
+ }
+
+ push(x: number, y: number) {
+ const a0 = this.a;
+ const b0 = this.b;
+ if (x !== a0 && a0 !== 0) {
+ const k = (y - b0) / (x - a0);
+ const p = y - k * x;
+ this.k.push(k);
+ this.p.push(p);
+ }
+ this.a = x;
+ this.b = y;
+ }
+
+ capacity(y: number) {
+ const k = this.k.mean();
+ const p = this.p.mean();
+ return Math.round(0.5 + (y - p) / k);
+ }
+
+ dimension(n: number) {
+ const k = this.k.mean();
+ const p = this.p.mean();
+ return p + n * k;
+ }
+
+}
+
+/* --------------------------------------------------------------------------*/
+/* --- Sizing Component ---*/
+/* --------------------------------------------------------------------------*/
+
+export const WSIZER = new FontSizer(7, 6);
+export const HSIZER = new FontSizer(14, 6);
+
+export interface SizedAreaProps {
+ cols: number;
+ rows: number;
+ children?: React.ReactNode;
+}
+
+export function SizedArea(props: SizedAreaProps) {
+ const { rows, cols, children } = props;
+ const refSizer = React.useCallback(
+ (ref: null | HTMLDivElement) => {
+ if (ref) {
+ const r = ref.getBoundingClientRect();
+ WSIZER.push(cols, r.width);
+ HSIZER.push(rows, r.height);
+ }
+ }, [rows, cols],
+ );
+ return (
+ <div
+ ref={refSizer}
+ className="eva-sized-area dome-text-code"
+ >
+ {children}
+ </div>
+ );
+}
+
+/* --------------------------------------------------------------------------*/
diff --git a/ivette/src/frama-c/eva/stacks.ts b/ivette/src/frama-c/eva/stacks.ts
new file mode 100644
index 0000000000000000000000000000000000000000..013638a1630db36810df46b65f3b8cc011226801
--- /dev/null
+++ b/ivette/src/frama-c/eva/stacks.ts
@@ -0,0 +1,88 @@
+// --------------------------------------------------------------------------
+// --- CallStacks
+// --------------------------------------------------------------------------
+
+import * as Server from 'frama-c/server';
+import * as Values from 'frama-c/api/plugins/eva/values';
+
+import { ModelCallbacks } from './cells';
+
+// --------------------------------------------------------------------------
+// --- Callstack infos
+// --------------------------------------------------------------------------
+
+export type callstacks = Values.callstack[];
+export interface Callsite {
+ callee: string;
+ caller?: string;
+ stmt?: string;
+ rank?: number;
+}
+
+// --------------------------------------------------------------------------
+// --- CallStacks Cache
+// --------------------------------------------------------------------------
+
+export class StacksCache {
+
+ private readonly model: ModelCallbacks;
+ private readonly stacks = new Map<string, callstacks>();
+ private readonly calls = new Map<Values.callstack, Callsite[]>();
+
+ // --------------------------------------------------------------------------
+ // --- LifeCycle
+ // --------------------------------------------------------------------------
+
+ constructor(state: ModelCallbacks) {
+ this.model = state;
+ }
+
+ clear() {
+ this.stacks.clear();
+ }
+
+ // --------------------------------------------------------------------------
+ // --- Getters
+ // --------------------------------------------------------------------------
+
+ getStacks(stmt: string): callstacks {
+ const cs = this.stacks.get(stmt);
+ if (cs !== undefined) return cs;
+ this.stacks.set(stmt, []);
+ this.requestCallstacks(stmt);
+ return [];
+ }
+
+ getCalls(cs: Values.callstack): Callsite[] {
+ const fs = this.calls.get(cs);
+ if (fs !== undefined) return fs;
+ this.calls.set(cs, []);
+ this.requestCalls(cs);
+ return [];
+ }
+
+ // --------------------------------------------------------------------------
+ // --- Fetchers
+ // --------------------------------------------------------------------------
+
+ private requestCallstacks(stmt: string) {
+ Server
+ .send(Values.getCallstacks, stmt)
+ .then((cs: callstacks) => {
+ this.stacks.set(stmt, cs);
+ this.model.forceLayout();
+ });
+ }
+
+ private requestCalls(cs: Values.callstack) {
+ Server
+ .send(Values.getCallstackInfo, cs)
+ .then((calls) => {
+ this.calls.set(cs, calls);
+ this.model.forceUpdate();
+ });
+ }
+
+}
+
+// --------------------------------------------------------------------------
diff --git a/ivette/src/frama-c/eva/style.css b/ivette/src/frama-c/eva/style.css
new file mode 100644
index 0000000000000000000000000000000000000000..12ff6e4916e8c18aff58de792b27a599606f26d2
--- /dev/null
+++ b/ivette/src/frama-c/eva/style.css
@@ -0,0 +1,225 @@
+/* -------------------------------------------------------------------------- */
+/* --- Styling Values --- */
+/* -------------------------------------------------------------------------- */
+
+.eva-sized-area {
+ padding: 3px;
+ white-space: pre;
+ overflow: hidden;
+ text-overflow: ellipsis;
+}
+
+.eva-stmt {
+ cursor: default;
+ color: grey;
+}
+
+/* -------------------------------------------------------------------------- */
+/* --- Probe Panel --- */
+/* -------------------------------------------------------------------------- */
+
+.eva-probeinfo {
+ min-height: 32px;
+ padding-left: 6px;
+ padding-top: 2px;
+ padding-bottom: 4px;
+ width: 100%;
+ background: #ccc;
+ display: flex;
+}
+
+.eva-probeinfo-label {
+ flex: 0 1 auto;
+ min-width: 22px;
+ text-align: left;
+}
+
+.eva-probeinfo-code {
+ flex: 0 1 auto;
+ background: lightgrey;
+ min-width: 120px;
+ width: auto;
+ border: thin solid black;
+ padding-left: 6px;
+ padding-right: 6px;
+ border-radius: 4px;
+ overflow: hidden;
+}
+
+.eva-probeinfo-stmt {
+ flex: 0 0 auto;
+ margin-left: 2px;
+ margin-right: 0px;
+ margin-top: 2px;
+}
+
+.eva-probeinfo-button {
+ flex: 0 0 auto;
+ margin: 1px;
+ min-width: 16px;
+}
+
+.eva-probeinfo-state {
+ margin-top: 2px;
+ margin-bottom: 2px;
+}
+
+/* -------------------------------------------------------------------------- */
+/* --- Call Satck Info --- */
+/* -------------------------------------------------------------------------- */
+
+.eva-info {
+ width: 100%;
+ background: #ccc;
+ padding-top: 3px;
+ padding-left: 12px;
+ padding-bottom: 2px;
+}
+
+.eva-callsite {
+ fill: #7cacbb;
+ background: #eee;
+ border-radius: 4px;
+ border: thin solid black;
+ padding-right: 7px;
+}
+
+.eva-callsite {
+ cursor: default;
+}
+
+/* -------------------------------------------------------------------------- */
+/* --- Table Rows --- */
+/* -------------------------------------------------------------------------- */
+
+.eva-row {
+ display: flex;
+ position: relative;
+ flex: 0 1 auto;
+ height: 100%;
+ border-bottom: thin solid black;
+ border-left: thin solid black;
+}
+
+.eva-probes .eva-row {
+ border-top: thin solid black;
+}
+
+/* -------------------------------------------------------------------------- */
+/* --- Table Cells --- */
+/* -------------------------------------------------------------------------- */
+
+.eva-stack {
+ width: 12px;
+ padding-top: 1px;
+ color: #777;
+ text-align: center;
+}
+
+.eva-cell {
+ flex: 1 1 auto;
+ border-right: thin solid black;
+}
+
+.eva-cell:nth-child(last) {
+ border-right: none;
+}
+
+.eva-probes .eva-cell {
+ padding: 2px;
+ text-align: center;
+}
+
+.eva-diff-shadow {
+ border: solid red thin;
+ position: relative;
+ z-index: -1;
+}
+
+.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; }
+
+/* -------------------------------------------------------------------------- */
+/* --- Table Rows Background --- */
+/* -------------------------------------------------------------------------- */
+
+.eva-probes .eva-row {
+ background: #cbe4cb;
+}
+
+.eva-values .eva-row {
+ background: #eee;
+}
+
+.eva-callstack.eva-row-odd .eva-row {
+ background: #eee;
+}
+
+.eva-callstack.eva-row-even .eva-row {
+ background: #e2e8e8;
+}
+
+.eva-callstack.eva-row-odd .eva-row .eva-transient {
+ background: #fff0d5;
+}
+
+.eva-callstack.eva-row-even .eva-row .eva-transient {
+ background: #fff0d5;
+}
+
+.eva-callstack.eva-row-selected .eva-row .eva-transient {
+ background: lightblue;
+}
+
+.eva-callstack.eva-row-selected .eva-row {
+ background: lightblue;
+}
+
+.eva-probes .eva-focused {
+ background: #02da02;
+}
+
+.eva-probes .eva-transient {
+ background: #fff0d5;
+}
+
+.eva-probes .eva-transient.eva-focused {
+ background: orange;
+}
+
+.eva-stack {
+ background: #eee;
+}
+
+.eva-callstack.eva-row-selected .eva-stack {
+ background: lightblue;
+}
+
+/* -------------------------------------------------------------------------- */
diff --git a/ivette/src/renderer/ASTview.tsx b/ivette/src/renderer/ASTview.tsx
index 3d6d82e4b316940218b02d7c3121d84b220f59c8..8583af381634c5a90bebcf4e82ac79ff56515e73 100644
--- a/ivette/src/renderer/ASTview.tsx
+++ b/ivette/src/renderer/ASTview.tsx
@@ -108,13 +108,13 @@ function getBulletColor(status: States.Tag) {
case 'invalid_under_hyp': return '#FF0000';
case 'valid':
case 'valid_under_hyp': return '#00B900';
- case 'considered_valid': return '#0000FF';
+ case 'considered_valid': return '#73bbbb';
case 'invalid_but_dead':
case 'valid_but_dead':
case 'unknown_but_dead': return '#000000';
case 'never_tried': return '#FFFFFF';
case 'inconsistent': return '#FF00FF';
- default: return '#0000FF';
+ default: return '#FF8300';
}
}
diff --git a/ivette/src/renderer/Application.tsx b/ivette/src/renderer/Application.tsx
index 381801a671a094310e84572fdc6867e065ff7112..494bf6008be4442b00ef445438d3e538ce08c6e4 100644
--- a/ivette/src/renderer/Application.tsx
+++ b/ivette/src/renderer/Application.tsx
@@ -2,6 +2,8 @@
// --- Main React Component rendered by './index.js'
// --------------------------------------------------------------------------
+// --- React & Dome
+
import React from 'react';
import * as Dome from 'dome';
import * as States from 'frama-c/states';
@@ -9,22 +11,26 @@ import { Vfill } from 'dome/layout/boxes';
import { LSplit } from 'dome/layout/splitters';
import * as Toolbar from 'dome/frame/toolbars';
import * as Sidebar from 'dome/frame/sidebars';
+import { GridHbox, GridItem } from 'dome/layout/grids';
-import './style.css';
+// --- Frama-C Plugins
import { LabView, View, Group } from 'frama-c/LabViews';
+import Values from 'frama-c/eva/Values';
import Dive from 'frama-c/dive/Dive';
-import { GridHbox, GridItem } from 'dome/layout/grids';
-import * as Controller from './Controller';
+// --- Ivette Main Renderers
+
+import * as Controller from './Controller';
import ASTview from './ASTview';
import ASTinfo from './ASTinfo';
import Globals, { GlobalHint, useHints } from './Globals';
import Properties from './Properties';
import Locations from './Locations';
-import Values from './Values';
import SourceCode from './SourceCode';
+import './style.css';
+
// --------------------------------------------------------------------------
// --- Selection Controls
// --------------------------------------------------------------------------
diff --git a/ivette/src/renderer/Values.tsx b/ivette/src/renderer/Values.tsx
deleted file mode 100644
index 8e34cf741ac8b9e7f296e514af2fe122d8e186e5..0000000000000000000000000000000000000000
--- a/ivette/src/renderer/Values.tsx
+++ /dev/null
@@ -1,141 +0,0 @@
-// --------------------------------------------------------------------------
-// --- Eva Values
-// --------------------------------------------------------------------------
-
-import React from 'react';
-import * as States from 'frama-c/states';
-import * as Json from 'dome/data/json';
-import * as Eva from 'frama-c/api/plugins/eva/values';
-import * as Ast from 'frama-c/api/kernel/ast';
-import * as Compare from 'dome/data/compare';
-
-import { Table, Column } from 'dome/table/views';
-import { ArrayModel } from 'dome/table/arrays';
-import { Component } from 'frama-c/LabViews';
-import { Icon } from 'dome/controls/icons';
-import { Label } from 'dome/controls/labels';
-
-// --------------------------------------------------------------------------
-// --- Columns
-// --------------------------------------------------------------------------
-
-const CallstackRenderer = (
- (cs: Eva.callstack) => <Label label={cs.short} title={cs.full} />
-);
-
-const ColumnCallstack = () => Column({
- id: 'callstack',
- label: 'Callstack',
- title: 'Context of the evaluation',
- align: 'left',
- width: 150,
- render: CallstackRenderer,
-});
-
-const AlarmRenderer = (
- (alarm: boolean) => <>{alarm && <Icon id="ATTENTION" />}</>
-);
-
-const ColumnAlarm = (props: { visible: boolean }) => Column({
- id: 'alarm',
- label: 'Alarm',
- title: 'Did the evaluation emit an alarm?',
- align: 'center',
- width: 26,
- fixed: true,
- icon: 'WARNING',
- visible: props.visible,
- render: AlarmRenderer,
-});
-
-const byValues: Compare.ByFields<Eva.valuesData> =
- { callstack: Compare.defined(Compare.byFields({ full: Compare.string })) };
-
-class ValuesModel extends ArrayModel<Json.key<'#values'>, Eva.valuesData> {
- constructor() {
- super();
- this.setOrderingByFields(byValues);
- }
-}
-
-// --------------------------------------------------------------------------
-// --- Values Panel
-// --------------------------------------------------------------------------
-
-const Values = () => {
-
- const model = React.useMemo(() => new ValuesModel(), []);
- const evaValues = States.useSyncArray(Eva.values).getArray();
- const selectMarker = States.useSelection()[0]?.current?.marker;
- const markerInfo = States.useSyncArray(Ast.markerInfo).getArray();
- const [name, setName] = React.useState<string | undefined>(undefined);
-
- States.useRequest(Eva.getValues, selectMarker);
-
- React.useEffect(() => {
- model.removeAllData();
- if (selectMarker && evaValues) {
- const selectMarkerInfo = markerInfo.find((e) => e.key === selectMarker);
- if (selectMarkerInfo && selectMarkerInfo.var !== 'function') {
- switch (selectMarkerInfo.kind) {
- case 'expression':
- case 'lvalue':
- evaValues.forEach((i) => model.setData(i.key, i));
- setName(selectMarkerInfo.descr);
- break;
- case 'declaration':
- evaValues.forEach((i) => model.setData(i.key, i));
- setName(selectMarkerInfo.name);
- break;
- default:
- setName(undefined);
- }
- }
- } else {
- setName(undefined);
- }
- model.reload();
- }, [evaValues, selectMarker, markerInfo, model]);
-
- // Component
- return (
- <>
- <Table model={model}>
- <ColumnCallstack />
- <Column
- id="value_before"
- visible={!!name}
- label={name && `${name} (before)`}
- title="Values inferred by Eva just before the selected point"
- disableSort
- width={300}
- />
- <ColumnAlarm visible={!!name} />
- <Column
- id="value_after"
- visible={!!name}
- label={name && `${name} (after)`}
- title="Values inferred by Eva just after the selected point"
- disableSort
- width={300}
- />
- </Table>
- </>
- );
-};
-
-// --------------------------------------------------------------------------
-// --- Export Component
-// --------------------------------------------------------------------------
-
-export default () => (
- <Component
- id="frama-c.values"
- label="Eva Values"
- title="Values inferred by the Eva analysis"
- >
- <Values />
- </Component>
-);
-
-// --------------------------------------------------------------------------
diff --git a/ivette/yarn.lock b/ivette/yarn.lock
index e708d53b0660333948b3107c0e6c76eb09631b01..d1b9cd89c54e0e40fff49ff63ea303bc37d47555 100644
--- a/ivette/yarn.lock
+++ b/ivette/yarn.lock
@@ -876,6 +876,13 @@
core-js-pure "^3.0.0"
regenerator-runtime "^0.13.4"
+"@babel/runtime@^7.0.0":
+ version "7.12.5"
+ resolved "https://registry.yarnpkg.com/@babel/runtime/-/runtime-7.12.5.tgz#410e7e487441e1b360c29be715d870d9b985882e"
+ integrity sha512-plcc+hbExy3McchJCEQG3knOsuh3HH+Prx1P6cLIkET/0dLuQDEnrT+s27Axgc9bqfsmNUNHfscgMUdBpC9xfg==
+ dependencies:
+ regenerator-runtime "^0.13.4"
+
"@babel/runtime@^7.10.2":
version "7.10.4"
resolved "https://registry.yarnpkg.com/@babel/runtime/-/runtime-7.10.4.tgz#a6724f1a6b8d2f6ea5236dbfe58c7d7ea9c5eb99"
@@ -1015,6 +1022,11 @@
resolved "https://registry.yarnpkg.com/@types/debug/-/debug-4.1.5.tgz#b14efa8852b7768d898906613c23f688713e02cd"
integrity sha512-Q1y515GcOdTHgagaVFhHnIFQ38ygs/kmxdNpvpou+raI9UO3YZcHDngBSYKQklcKlvA7iuQlmIKbzvmxcOE9CQ==
+"@types/diff@^4.0.2":
+ version "4.0.2"
+ resolved "https://registry.yarnpkg.com/@types/diff/-/diff-4.0.2.tgz#2e9bb89f9acc3ab0108f0f3dc4dbdcf2fff8a99c"
+ integrity sha512-mIenTfsIe586/yzsyfql69KRnA75S8SVXQbTLpDejRrjH0QSJcpu3AUOi/Vjnt9IOsXKxPhJfGpQUNMueIU1fQ==
+
"@types/eslint-visitor-keys@^1.0.0":
version "1.0.0"
resolved "https://registry.yarnpkg.com/@types/eslint-visitor-keys/-/eslint-visitor-keys-1.0.0.tgz#1ee30d79544ca84d68d4b3cdb0af4f205663dd2d"
@@ -1111,6 +1123,13 @@
"@types/prop-types" "*"
"@types/react" "*"
+"@types/react-window@^1.8.2":
+ version "1.8.2"
+ resolved "https://registry.yarnpkg.com/@types/react-window/-/react-window-1.8.2.tgz#a5a6b2762ce73ffaab7911ee1397cf645f2459fe"
+ integrity sha512-gP1xam68Wc4ZTAee++zx6pTdDAH08rAkQrWm4B4F/y6hhmlT9Mgx2q8lTCXnrPHXsr15XjRN9+K2DLKcz44qEQ==
+ dependencies:
+ "@types/react" "*"
+
"@types/react@*", "@types/react@^16.9.17":
version "16.9.32"
resolved "https://registry.yarnpkg.com/@types/react/-/react-16.9.32.tgz#f6368625b224604148d1ddf5920e4fefbd98d383"
@@ -3226,6 +3245,11 @@ detect-node@^2.0.4:
resolved "https://registry.yarnpkg.com/detect-node/-/detect-node-2.0.4.tgz#014ee8f8f669c5c58023da64b8179c083a28c46c"
integrity sha512-ZIzRpLJrOj7jjP2miAtgqIfmzbxa4ZOr5jJc601zklsfEx9oTzmmj2nVpIPRpNlRTIh8lc1kyViIY7BWSGNmKw==
+diff@^5.0.0:
+ version "5.0.0"
+ resolved "https://registry.yarnpkg.com/diff/-/diff-5.0.0.tgz#7ed6ad76d859d030787ec35855f5b1daf31d852b"
+ integrity sha512-/VTCrvm5Z0JGty/BWHljh+BAiw3IK+2j87NGMu8Nwc/f48WoDAC395uomO9ZD117ZOBaHmkX1oyLvkVM/aIT3w==
+
diffie-hellman@^5.0.0:
version "5.0.3"
resolved "https://registry.yarnpkg.com/diffie-hellman/-/diffie-hellman-5.0.3.tgz#40e8ee98f55a2149607146921c63e1ae5f3d2875"
@@ -5911,6 +5935,11 @@ mem@^4.0.0:
mimic-fn "^2.0.0"
p-is-promise "^2.0.0"
+"memoize-one@>=3.1.1 <6":
+ version "5.1.1"
+ resolved "https://registry.yarnpkg.com/memoize-one/-/memoize-one-5.1.1.tgz#047b6e3199b508eaec03504de71229b8eb1d75c0"
+ integrity sha512-HKeeBpWvqiVJD57ZUAsJNm71eHTykffzcLZVYWiVfQeI1rJtuEaS7hQiEpWfVVk18donPwJEcFKIkCmPJNOhHA==
+
memory-fs@^0.4.0, memory-fs@^0.4.1:
version "0.4.1"
resolved "https://registry.yarnpkg.com/memory-fs/-/memory-fs-0.4.1.tgz#3a9a20b8462523e447cfbc7e8bb80ed667bfc552"
@@ -7411,6 +7440,14 @@ react-virtualized@^9.21.2:
prop-types "^15.6.0"
react-lifecycles-compat "^3.0.4"
+react-window@^1.8.6:
+ version "1.8.6"
+ resolved "https://registry.yarnpkg.com/react-window/-/react-window-1.8.6.tgz#d011950ac643a994118632665aad0c6382e2a112"
+ integrity sha512-8VwEEYyjz6DCnGBsd+MgkD0KJ2/OXFULyDtorIiTz+QzwoP94tBoA7CnbtyXMm+cCeAUER5KJcPtWl9cpKbOBg==
+ dependencies:
+ "@babel/runtime" "^7.0.0"
+ memoize-one ">=3.1.1 <6"
+
react@^16.8:
version "16.13.1"
resolved "https://registry.yarnpkg.com/react/-/react-16.13.1.tgz#2e818822f1a9743122c063d6410d85c1e3afe48e"
diff --git a/src/plugins/value/api/values_request.ml b/src/plugins/value/api/values_request.ml
index 85d2df413cded868f8088cdb2d72602a095ca4ac..035340717f3f43761da0c8aeb4d49614d572d6ab 100644
--- a/src/plugins/value/api/values_request.ml
+++ b/src/plugins/value/api/values_request.ml
@@ -23,7 +23,16 @@
open Server
open Data
open Cil_types
+
+module Kmap = Kernel_function.Hashtbl
+module Smap = Cil_datatype.Stmt.Hashtbl
+module CS = Value_types.Callstack
+module CSmap = CS.Hashtbl
+
module Md = Markdown
+module Jkf = Kernel_ast.Kf
+module Jstmt = Kernel_ast.Stmt
+module Jmarker = Kernel_ast.Marker
let package =
Package.package
@@ -33,334 +42,460 @@ let package =
~readme:"eva.md"
()
-type value =
- { value: string;
- alarm: bool; }
-
-type evaluation =
- | Unreachable
- | Evaluation of value
-
-type after =
- | Unchanged
- | Reduced of evaluation
-
-type before_after =
- { before: evaluation;
- after_instr: after option;
- after_then: after option;
- after_else: after option; }
-
-type values =
- { values: before_after;
- callstack: (Value_util.callstack * before_after) list option; }
-
-let get_value = function
- | Unreachable -> "Unreachable"
- | Evaluation { value } -> value
-
-let get_alarm = function
- | Unreachable -> false
- | Evaluation { alarm } -> alarm
-
-let get_after_value =
- Extlib.opt_map
- (function Unchanged -> "unchanged" | Reduced eval -> get_value eval)
-
-module CallStackId =
- Data.Index
- (Value_types.Callstack.Map)
- (struct
- let name = "eva-callstack-id"
- end)
-
-(* This pretty-printer drops the toplevel kf, which is always the function
- in which we are pretty-printing the expression/term *)
-let pretty_callstack fmt cs =
- match cs with
- | [_, Kglobal] -> ()
- | (_kf_cur, Kstmt callsite) :: q -> begin
- let rec aux callsite = function
- | (kf, callsite') :: q -> begin
- Format.fprintf fmt "%a (%a)"
- Kernel_function.pretty kf
- Cil_datatype.Location.pretty (Cil_datatype.Stmt.loc callsite);
- match callsite' with
- | Kglobal -> ()
- | Kstmt callsite' ->
- Format.fprintf fmt " â†@ ";
- aux callsite' q
+type probe =
+ | Pexpr of exp * stmt
+ | Plval of lval * stmt
+ | Pnone
+
+type callstack = Value_types.callstack
+type truth = Abstract_interp.truth
+type step = [ `Here | `After | `Then of exp | `Else of exp ]
+
+type domain = {
+ values: ( step * string ) list ;
+ alarms: ( truth * string ) list ;
+}
+
+let signal = Request.signal ~package ~name:"changed"
+ ~descr:(Md.plain "Emitted when EVA results has changed")
+
+let () = Analysis.register_computed_hook (fun () -> Request.emit signal)
+
+(* -------------------------------------------------------------------------- *)
+(* --- Marker Utilities --- *)
+(* -------------------------------------------------------------------------- *)
+
+let next_steps s : step list =
+ match s.skind with
+ | If(cond,_,_,_) -> [ `Then cond ; `Else cond ]
+ | Instr (Set _ | Call _ | Local_init _ | Asm _ | Code_annot _)
+ | Switch _ | Loop _ | Block _ | UnspecifiedSequence _
+ | TryCatch _ | TryFinally _ | TryExcept _
+ -> [ `After ]
+ | Instr (Skip _) | Return _ | Break _ | Continue _ | Goto _ | Throw _ -> []
+
+let probe_stmt s =
+ match s.skind with
+ | Instr (Set(lv,_,_)) -> Plval(lv,s)
+ | Instr (Call(Some lr,_,_,_)) -> Plval(lr,s)
+ | Instr (Local_init(v,_,_)) -> Plval((Var v,NoOffset),s)
+ | Return (Some e,_) | If(e,_,_,_) | Switch(e,_,_,_) -> Pexpr(e,s)
+ | _ -> Pnone
+
+let probe marker =
+ let open Printer_tag in
+ match marker with
+ | PLval(_,Kstmt s,l) -> Plval(l,s)
+ | PExp(_,Kstmt s,e) -> Pexpr(e,s)
+ | PStmt(_,s) | PStmtStart(_,s) -> probe_stmt s
+ | PVDecl(_,Kstmt s,v) -> Plval((Var v,NoOffset),s)
+ | _ -> Pnone
+
+(* -------------------------------------------------------------------------- *)
+(* --- Stmt Ranking --- *)
+(* -------------------------------------------------------------------------- *)
+
+module Ranking :
+sig
+ val stmt : stmt -> int
+ val sort : callstack list -> callstack list
+end =
+struct
+
+ class ranker =
+ object(self)
+ inherit Visitor.frama_c_inplace
+ (* ranks really starts at 1 *)
+ (* rank < 0 means not computed yet *)
+ val mutable rank = (-1)
+ val rmap = Smap.create 0
+ val fmark = Kmap.create 0
+ val fqueue = Queue.create ()
+
+ method private call kf =
+ if not (Kmap.mem fmark kf) then
+ begin
+ Kmap.add fmark kf () ;
+ Queue.push kf fqueue ;
end
- | _ -> assert false
- in
- Format.fprintf fmt "@[<hv>%a" Value_types.Callstack.pretty_hash cs;
- aux callsite q;
- Format.fprintf fmt "@]"
+
+ method private newrank s =
+ let r = succ rank in
+ Smap.add rmap s r ;
+ rank <- r ; r
+
+ method! vlval lv =
+ begin
+ try match fst lv with
+ | Var vi -> self#call (Globals.Functions.get vi)
+ | _ -> ()
+ with Not_found -> ()
+ end ; Cil.DoChildren
+
+ method! vstmt_aux s =
+ ignore (self#newrank s) ;
+ Cil.DoChildren
+
+ method flush =
+ while not (Queue.is_empty fqueue) do
+ let kf = Queue.pop fqueue in
+ ignore (Visitor.(visitFramacKf (self :> frama_c_visitor) kf))
+ done
+
+ method compute =
+ match Globals.entry_point () with
+ | kf , _ -> self#call kf ; self#flush
+ | exception Globals.No_such_entry_point _ -> ()
+
+ method rank s =
+ if rank < 0 then (rank <- 0 ; self#compute) ;
+ try Smap.find rmap s
+ with Not_found ->
+ let kf = Kernel_function.find_englobing_kf s in
+ self#call kf ;
+ self#flush ;
+ try Smap.find rmap s
+ with Not_found -> self#newrank s
+
end
- | _ -> assert false
-
-(* This pretty-printer prints only the lists of the functions, not
- the locations. *)
-let pretty_callstack_short fmt cs =
- match cs with
- | [_, Kglobal] -> ()
- | (_kf_cur, Kstmt _callsite) :: q ->
- Format.fprintf fmt "%a" Value_types.Callstack.pretty_hash cs;
- Pretty_utils.pp_flowlist ~left:"@[" ~sep:" â†@ " ~right:"@]"
- (fun fmt (kf, _) -> Kernel_function.pretty fmt kf) fmt q
- | _ -> assert false
-
-module CallStack = struct
- type record
-
- let record: record Record.signature = Record.signature ()
-
- let id = Record.field record ~name:"id"
- ~descr:(Md.plain "Callstack id") (module Jint)
- let short = Record.field record ~name:"short"
- ~descr:(Md.plain "Short name for the callstack") (module Jstring)
- let full = Record.field record ~name:"full"
- ~descr:(Md.plain "Full name for the callstack") (module Jstring)
-
- module R =
- (val
- (Record.publish
- ~package
- ~name:"callstack"
- ~descr:(Md.plain "CallStack")
- record) : Record.S with type r = record)
-
- type t = Value_types.callstack option
-
- let jtype = R.jtype
-
- let pp_callstack ~short = function
- | None -> if short then "all" else ""
- | Some callstack ->
- let pp_text =
- if short
- then Pretty_utils.to_string ~margin:50 pretty_callstack_short
- else Pretty_utils.to_string pretty_callstack
- in
- (pp_text callstack)
-
- let id_callstack = function
- | None -> -1
- | Some callstack -> CallStackId.get callstack
-
- let to_json callstack =
- R.default |>
- R.set id (id_callstack callstack) |>
- R.set short (pp_callstack ~short:true callstack) |>
- R.set full (pp_callstack ~short:false callstack) |>
- R.to_json
-
- let key = function
- | None -> "all"
- | Some callstack -> string_of_int (CallStackId.get callstack)
+
+ let stmt = let rk = new ranker in rk#rank
+
+ let rec ranks (rks : int list) (cs : callstack) : int list =
+ match cs with
+ | [] -> rks
+ | (_,Kglobal)::wcs -> ranks rks wcs
+ | (_,Kstmt s)::wcs -> ranks (stmt s :: rks) wcs
+
+ let order : int list -> int list -> int = Stdlib.compare
+
+ let sort (wcs : callstack list) : callstack list =
+ List.map fst @@
+ List.sort (fun (_,rp) (_,rq) -> order rp rq) @@
+ List.map (fun cs -> cs , ranks [] cs) wcs
+
+end
+
+(* -------------------------------------------------------------------------- *)
+(* --- Domain Utilities --- *)
+(* -------------------------------------------------------------------------- *)
+
+module Jcallstack : S with type t = callstack =
+struct
+ module I = Data.Index
+ (Value_types.Callstack.Map)
+ (struct let name = "eva-callstack-id" end)
+ let jtype = Data.declare ~package ~name:"callstack" I.jtype
+ type t = I.t
+ let to_json = I.to_json
+ let of_json = I.of_json
end
+module Jcalls : Request.Output with type t = callstack =
+struct
+
+ type t = callstack
+ let jtype = Package.(Jlist (Jrecord [
+ "callee" , Jkf.jtype ;
+ "caller" , Joption Jkf.jtype ;
+ "stmt" , Joption Jstmt.jtype ;
+ "rank" , Joption Jnumber ;
+ ]))
+
+ let rec jcallstack jcallee ki cs : json list =
+ match ki , cs with
+ | Kglobal , _ | _ , [] -> [
+ `Assoc [ "callee", jcallee ]
+ ]
+ | Kstmt stmt , (called,ki) :: cs ->
+ let jcaller = Jkf.to_json called in
+ let callsite = `Assoc [
+ "callee", jcallee ;
+ "caller", jcaller ;
+ "stmt", Jstmt.to_json stmt ;
+ "rank", Jint.to_json (Ranking.stmt stmt) ;
+ ] in
+ callsite :: jcallstack jcaller ki cs
+
+ let to_json = function
+ | [] -> `List []
+ | (callee,ki)::cs -> `List (jcallstack (Jkf.to_json callee) ki cs)
-let consolidated = ref None
-let table = Hashtbl.create 100
-
-let iter f =
- if Hashtbl.length table > 1
- then Extlib.may (fun values -> f (None, values)) !consolidated;
- Hashtbl.iter (fun key data -> f (Some key, data)) table
-
-let array =
- let model = States.model () in
- let () =
- States.column
- ~name:"callstack"
- ~descr:(Md.plain "CallStack")
- ~data:(module CallStack)
- ~get:fst
- model
- in
- let () =
- States.column
- ~name:"value_before"
- ~descr:(Md.plain "Value inferred just before the selected point")
- ~data:(module Jstring)
- ~get:(fun (_, e) -> get_value e.before)
- model
- in
- let () =
- States.column
- ~name:"alarm"
- ~descr:(Md.plain "Did the evaluation led to an alarm?")
- ~data:(module Jbool)
- ~get:(fun (_, e) -> get_alarm e.before)
- model
- in
- let () =
- States.column
- ~name:"value_after"
- ~descr:(Md.plain "Value inferred just after the selected point")
- ~data:(module Joption(Jstring))
- ~get:(fun (_, e) -> get_after_value e.after_instr)
- model
- in
- States.register_array
- ~package
- ~name:"values"
- ~descr:(Md.plain "Abstract values inferred by the Eva analysis")
- ~key:(fun (cs, _) -> CallStack.key cs)
- ~iter
- model
-
-let update_values values =
- Hashtbl.clear table;
- consolidated := Some values.values;
- let () =
- match values.callstack with
- | None -> ()
- | Some by_callstack ->
- List.iter
- (fun (callstack, before_after) ->
- Hashtbl.add table callstack before_after)
- by_callstack
- in
- States.reload array
-
-module type S = sig
- val evaluate: kinstr -> exp -> values
- val lvaluate: kinstr -> lval -> values
end
-module Make (Eva: Analysis.S) : S = struct
-
- let make_before eval before =
- let before =
- match before with
- | `Bottom -> Unreachable
- | `Value state -> Evaluation (eval state)
- in
- { before; after_instr = None; after_then = None; after_else = None; }
-
- let make_callstack stmt eval =
- let before = Eva.get_stmt_state_by_callstack ~after:false stmt in
- match before with
- | (`Bottom | `Top) -> []
- | `Value before ->
- let aux callstack before acc =
- let before_after = make_before eval (`Value before) in
- (callstack, before_after) :: acc
- in
- Value_types.Callstack.Hashtbl.fold aux before []
-
- let make_before_after eval ~before ~after =
- match before with
- | `Bottom ->
- { before = Unreachable;
- after_instr = None;
- after_then = None;
- after_else = None; }
- | `Value before ->
- let before = eval before in
- let after_instr =
- match after with
- | `Bottom -> Some (Reduced Unreachable)
- | `Value after ->
- let after = eval after in
- if String.equal before.value after.value
- then Some Unchanged
- else Some (Reduced (Evaluation after))
- in
- { before = Evaluation before;
- after_instr; after_then = None; after_else = None; }
-
- let make_instr_callstack stmt eval =
- let before = Eva.get_stmt_state_by_callstack ~after:false stmt in
- let after = Eva.get_stmt_state_by_callstack ~after:true stmt in
- match before, after with
- | (`Bottom | `Top), _
- | _, (`Bottom | `Top) -> []
- | `Value before, `Value after ->
- let aux callstack before acc =
- let before = `Value before in
- let after =
- try `Value (Value_types.Callstack.Hashtbl.find after callstack)
+
+
+module Jtruth : Data.S with type t = truth =
+struct
+ type t = truth
+ let jtype =
+ Package.(Junion [ Jtag "True" ; Jtag "False" ; Jtag "Unknown" ])
+ let to_json = function
+ | Abstract_interp.Unknown -> `String "Unknown"
+ | True -> `String "True"
+ | False -> `String "False"
+ let of_json = function
+ | `String "True" -> Abstract_interp.True
+ | `String "False" -> Abstract_interp.False
+ | _ -> Abstract_interp.Unknown
+end
+
+(* -------------------------------------------------------------------------- *)
+(* --- EVA Proxy --- *)
+(* -------------------------------------------------------------------------- *)
+
+module type EvaProxy =
+sig
+ val callstacks : stmt -> callstack list
+ val domain : probe -> callstack option -> domain
+end
+
+module Proxy(A : Analysis.S) : EvaProxy =
+struct
+
+ open Eval
+ type dstate = A.Dom.state or_top_or_bottom
+
+ let callstacks stmt =
+ match A.get_stmt_state_by_callstack ~after:false stmt with
+ | `Top | `Bottom -> []
+ | `Value states ->
+ CSmap.fold_sorted (fun cs _st wcs -> cs :: wcs) states []
+
+ let dstate ~after stmt callstack =
+ match callstack with
+ | None -> (A.get_stmt_state ~after stmt :> dstate)
+ | Some cs ->
+ begin match A.get_stmt_state_by_callstack ~after stmt with
+ | `Top -> `Top
+ | `Bottom -> `Bottom
+ | `Value cmap ->
+ try `Value (CSmap.find cmap cs)
with Not_found -> `Bottom
- in
- let before_after = make_before_after eval ~before ~after in
- (callstack, before_after) :: acc
- in
- Value_types.Callstack.Hashtbl.fold aux before []
-
- let make eval kinstr =
- let before = Eva.get_kinstr_state ~after:false kinstr in
- let values, callstack =
- match kinstr with
- | Cil_types.Kglobal ->
- make_before eval before, None
- | Cil_types.Kstmt stmt ->
- match stmt.skind with
- | Instr _ ->
- let after = Eva.get_kinstr_state ~after:true kinstr in
- let values = make_before_after eval ~before ~after in
- let callstack = make_instr_callstack stmt eval in
- values, Some callstack
- | _ ->
- make_before eval before, Some (make_callstack stmt eval)
- in
- { values; callstack; }
-
-
- let evaluate kinstr expr =
- let eval state =
- let value, alarms = Eva.eval_expr state expr in
- let alarm = not (Alarmset.is_empty alarms) in
- let str = Format.asprintf "%a" (Bottom.pretty Eva.Val.pretty) value in
- { value = str; alarm }
- in
- make eval kinstr
-
- let lvaluate kinstr lval =
- let eval state =
- let value, alarms = Eva.copy_lvalue state lval in
- let alarm = not (Alarmset.is_empty alarms) in
- let flagged_value = match value with
- | `Bottom -> Eval.Flagged_Value.bottom
- | `Value v -> v
- in
- let pretty = Eval.Flagged_Value.pretty Eva.Val.pretty in
- let str = Format.asprintf "%a" pretty flagged_value in
- { value = str; alarm }
- in
- make eval kinstr
+ end
+
+ let dnone = {
+ alarms = [] ;
+ values = [] ;
+ }
+
+ let dtop = {
+ alarms = [] ;
+ values = [`Here , "Not available."] ;
+ }
+
+ let dbottom = {
+ alarms = [] ;
+ values = [`Here , "Unreachable."] ;
+ }
+
+ let dalarms alarms =
+ let pool = ref [] in
+ Alarmset.iter
+ (fun alarm status ->
+ let descr = Format.asprintf "@[<hov 2>%a@]" Alarms.pretty alarm
+ in pool := (status , descr) :: !pool
+ ) alarms ;
+ List.rev !pool
+
+ let deval (eval : A.Dom.state -> string * Alarmset.t) stmt callstack =
+ match dstate ~after:false stmt callstack with
+ | `Bottom -> dbottom
+ | `Top -> dtop
+ | `Value state ->
+ let value, alarms = eval state in
+ let dnext (step : step) vs = function
+ | `Top | `Bottom -> vs
+ | `Value state ->
+ let values =
+ try fst @@ eval state
+ with exn -> Printf.sprintf "Error (%S)" (Printexc.to_string exn)
+ in (step , values) :: vs in
+ let others = List.fold_right
+ begin fun st vs ->
+ match st with
+ | `Here -> vs (* absurd *)
+ | `After -> dnext st vs @@ dstate ~after:true stmt callstack
+ | `Then cond -> dnext st vs @@ A.assume_cond stmt state cond true
+ | `Else cond -> dnext st vs @@ A.assume_cond stmt state cond false
+ end (next_steps stmt) []
+ in {
+ values = (`Here,value) :: others ;
+ alarms = dalarms alarms ;
+ }
+
+ let e_expr expr state =
+ let value, alarms = A.eval_expr state expr in
+ begin
+ Pretty_utils.to_string (Bottom.pretty A.Val.pretty) value,
+ alarms
+ end
+
+ let e_lval lval state =
+ let value, alarms = A.copy_lvalue state lval in
+ let flagged = match value with
+ | `Bottom -> Eval.Flagged_Value.bottom
+ | `Value v -> v in
+ begin
+ Pretty_utils.to_string (Eval.Flagged_Value.pretty A.Val.pretty) flagged,
+ alarms
+ end
+
+ let domain p wcs = match p with
+ | Plval(l,s) -> deval (e_lval l) s wcs
+ | Pexpr(e,s) -> deval (e_expr e) s wcs
+ | Pnone -> dnone
+
end
+let proxy =
+ let make (a : (module Analysis.S)) = (module Proxy(val a) : EvaProxy) in
+ let current = ref (make @@ Analysis.current_analyzer ()) in
+ let () = Analysis.register_hook
+ begin fun a ->
+ current := make a ;
+ Request.emit signal ;
+ end
+ in current
+
+(* -------------------------------------------------------------------------- *)
+(* --- Request getCallstacks --- *)
+(* -------------------------------------------------------------------------- *)
+
+let () = Request.register ~package
+ ~kind:`GET ~name:"getCallstacks"
+ ~descr:(Md.plain "Callstacks for markers")
+ ~input:(module Jstmt)
+ ~output:(module Jlist(Jcallstack))
+ begin fun stmt ->
+ let module A = (val !proxy) in
+ Ranking.sort (A.callstacks stmt)
+ end
-let ref_request =
- let module Analyzer = (val Analysis.current_analyzer ()) in
- ref (module Make (Analyzer) : S)
+(* -------------------------------------------------------------------------- *)
+(* --- Request getCallstackInfo --- *)
+(* -------------------------------------------------------------------------- *)
-let hook (module Analyzer: Analysis.S) =
- ref_request := (module Make (Analyzer) : S)
+let () =
+ Request.register ~package
+ ~kind:`GET ~name:"getCallstackInfo"
+ ~descr:(Md.plain "Callstack Description")
+ ~input:(module Jcallstack)
+ ~output:(module Jcalls)
+ begin fun cs -> cs end
-let () = Analysis.register_hook hook
+(* -------------------------------------------------------------------------- *)
+(* --- Request getStmtInfo --- *)
+(* -------------------------------------------------------------------------- *)
+let () =
+ let getStmtInfo = Request.signature ~input:(module Jstmt) () in
+ let set_fct = Request.result getStmtInfo ~name:"fct"
+ ~descr:(Md.plain "Englobing function")
+ (module Jkf) in
+ let set_rank = Request.result getStmtInfo ~name:"rank"
+ ~descr:(Md.plain "Global stmt order")
+ (module Jint) in
+ Request.register_sig ~package getStmtInfo
+ ~kind:`GET ~name:"getStmtInfo"
+ ~descr:(Md.plain "Stmt Information")
+ begin fun rq s ->
+ set_fct rq (Kernel_function.find_englobing_kf s) ;
+ set_rank rq (Ranking.stmt s) ;
+ end
-let update tag =
- let module Request = (val !ref_request) in
- match tag with
- | Printer_tag.PExp (_kf, kinstr, expr) ->
- update_values (Request.evaluate kinstr expr)
- | Printer_tag.PLval (_kf, kinstr, lval) ->
- update_values (Request.lvaluate kinstr lval)
- | PVDecl (_kf, kinstr, varinfo) ->
- update_values (Request.lvaluate kinstr (Var varinfo, NoOffset))
- | _ -> ()
+(* -------------------------------------------------------------------------- *)
+(* --- Request getProbeInfo --- *)
+(* -------------------------------------------------------------------------- *)
let () =
- Server.Request.register
- ~package
- ~kind:`GET
- ~name:"getValues"
- ~descr:(Md.plain "Get the abstract values computed for an expression or lvalue")
- ~input:(module Kernel_ast.Marker)
- ~output:(module Junit)
- update
+ let getProbeInfo = Request.signature ~input:(module Jmarker) () in
+ let set_code = Request.result_opt getProbeInfo
+ ~name:"code" ~descr:(Md.plain "Probe source code")
+ (module Jstring) in
+ let set_stmt = Request.result_opt getProbeInfo
+ ~name:"stmt" ~descr:(Md.plain "Probe statement")
+ (module Jstmt) in
+ let set_rank = Request.result getProbeInfo
+ ~name:"rank" ~descr:(Md.plain "Probe statement rank")
+ ~default:0 (module Jint) in
+ let set_effects = Request.result getProbeInfo
+ ~name:"effects" ~descr:(Md.plain "Effectfull statement")
+ ~default:false (module Jbool) in
+ let set_condition = Request.result getProbeInfo
+ ~name:"condition" ~descr:(Md.plain "Conditional statement")
+ ~default:false (module Jbool) in
+ let set_probe rq pp p s =
+ begin
+ set_code rq (Some (Pretty_utils.to_string pp p)) ;
+ set_stmt rq (Some s) ;
+ set_rank rq (Ranking.stmt s) ;
+ List.iter
+ (function
+ | `Here -> ()
+ | `Then _ | `Else _ -> set_condition rq true
+ | `After -> set_effects rq true
+ )
+ (next_steps s)
+ end
+ in Request.register_sig ~package ~kind:`GET getProbeInfo
+ ~name:"getProbeInfo" ~descr:(Md.plain "Probe informations")
+ begin fun rq marker ->
+ match probe marker with
+ | Plval(l,s) ->
+ set_probe rq Printer.pp_lval l s ;
+ | Pexpr(e,s) ->
+ set_probe rq Printer.pp_exp e s ;
+ | Pnone -> ()
+ end
+
+(* -------------------------------------------------------------------------- *)
+(* --- Request getValues --- *)
+(* -------------------------------------------------------------------------- *)
+
+let () =
+ let getValues = Request.signature () in
+ let get_tgt = Request.param getValues ~name:"target"
+ ~descr:(Md.plain "Works with all markers containing an expression")
+ (module Jmarker) in
+ let get_cs = Request.param_opt getValues ~name:"callstack"
+ ~descr:(Md.plain "Callstack to collect (defaults to none)")
+ (module Jcallstack) in
+ let set_alarms = Request.result getValues ~name:"alarms"
+ ~descr:(Md.plain "Alarms raised during evaluation")
+ (module Jlist(Jpair(Jtruth)(Jstring))) in
+ let set_domain = Request.result_opt getValues ~name:"values"
+ ~descr:(Md.plain "Domain values")
+ (module Jstring) in
+ let set_after = Request.result_opt getValues ~name:"v_after"
+ ~descr:(Md.plain "Domain values after execution")
+ (module Jstring) in
+ let set_then = Request.result_opt getValues ~name:"v_then"
+ ~descr:(Md.plain "Domain values for true condition")
+ (module Jstring) in
+ let set_else = Request.result_opt getValues ~name:"v_else"
+ ~descr:(Md.plain "Domain values for false condition")
+ (module Jstring) in
+ Request.register_sig ~package getValues
+ ~kind:`GET ~name:"getValues"
+ ~descr:(Md.plain "Abstract values for the given marker")
+ begin fun rq () ->
+ let marker = get_tgt rq in
+ let callstack = get_cs rq in
+ let domain =
+ let module A : EvaProxy = (val !proxy) in
+ A.domain (probe marker) callstack in
+ set_alarms rq domain.alarms ;
+ List.iter
+ (fun (step,values) ->
+ let domain = Some values in
+ match step with
+ | `Here -> set_domain rq domain
+ | `After -> set_after rq domain
+ | `Then _ -> set_then rq domain
+ | `Else _ -> set_else rq domain
+ ) domain.values ;
+ end
+
+
+(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/value/engine/analysis.ml b/src/plugins/value/engine/analysis.ml
index 06c72bf50993d410b025682e5ee4f2ab914a45a9..d1d807098e3f571860d4221bbc4f5c2912f6e10a 100644
--- a/src/plugins/value/engine/analysis.ml
+++ b/src/plugins/value/engine/analysis.ml
@@ -40,10 +40,11 @@ module type Results = sig
val eval_lval_to_loc: state -> lval -> location evaluated
val eval_function_exp:
state -> ?args:exp list -> exp -> kernel_function list evaluated
+ val assume_cond : stmt -> state -> exp -> bool -> state or_bottom
end
module type S = sig
- include Abstractions.S
+ include Abstractions.Eva
include Results with type state := Dom.state
and type value := Val.t
and type location := Loc.location
@@ -95,6 +96,11 @@ module Make (Abstract: Abstractions.S) = struct
let eval_function_exp state ?args e =
Eval.eval_function_exp e ?args state >>=: (List.map fst)
+ let assume_cond stmt state cond positive =
+ fst (Eval.reduce state cond positive) >>- fun valuation ->
+ let dval = Eval.to_domain_valuation valuation in
+ Dom.assume stmt cond positive dval state
+
end
@@ -121,9 +127,16 @@ let current_analyzer () = (module (val (snd !ref_analyzer)): S)
Useful for the GUI parts that depend on it. *)
module Analyzer_Hook = Hook.Build (struct type t = (module S) end)
+(* Set of hooks called whenever the current Analyzer is computed.
+ Useful for the GUI parts that depend on it. *)
+module Computed_Hook = Hook.Build (struct type t = unit end)
+
(* Register a new hook. *)
let register_hook = Analyzer_Hook.extend
+(* Register a new computed hook. *)
+let register_computed_hook = Computed_Hook.extend
+
(* Sets the current Analyzer module for a given configuration.
Calls the hooks above. *)
let set_current_analyzer config (analyzer: (module Analyzer)) =
@@ -163,7 +176,8 @@ let force_compute () =
let kf, lib_entry = Globals.entry_point () in
reset_analyzer ();
let module Analyzer = (val snd !ref_analyzer) in
- Analyzer.compute_from_entry_point ~lib_entry kf
+ Analyzer.compute_from_entry_point ~lib_entry kf ;
+ Computed_Hook.apply ()
(* Resets the Analyzer when the current project is changed. *)
let () =
diff --git a/src/plugins/value/engine/analysis.mli b/src/plugins/value/engine/analysis.mli
index e96f3ed5ea11ade74b0b3a80210df1757d26e5db..50b943ccad73a30eb0d8e41ab94a60e334e471ef 100644
--- a/src/plugins/value/engine/analysis.mli
+++ b/src/plugins/value/engine/analysis.mli
@@ -40,6 +40,7 @@ module type Results = sig
val eval_lval_to_loc: state -> lval -> location evaluated
val eval_function_exp:
state -> ?args:exp list -> exp -> kernel_function list evaluated
+ val assume_cond : stmt -> state -> exp -> bool -> state or_bottom
end
@@ -55,7 +56,7 @@ end
module type S = sig
- include Abstractions.S
+ include Abstractions.Eva
include Results with type state := Dom.state
and type value := Val.t
and type location := Loc.location
@@ -69,6 +70,10 @@ val register_hook: ((module S) -> unit) -> unit
is changed. This happens when a new analysis is run with different
abstractions than before, or when the current project is changed. *)
+val register_computed_hook: (unit -> unit) -> unit
+(** Registers a hook that will be called each time the [current] analyzer
+ has been computed. *)
+
val force_compute : unit -> unit
(** Perform a full analysis, starting from the [main] function. *)
diff --git a/src/plugins/value_types/value_types.mli b/src/plugins/value_types/value_types.mli
index 99589861241eeb1e280acc5f5abee60270ee4f0e..cdd8f86c51b15e072ea718a42cf62740ba5e5143 100644
--- a/src/plugins/value_types/value_types.mli
+++ b/src/plugins/value_types/value_types.mli
@@ -27,8 +27,23 @@ open Cil_types
(* TODO: These types are already defined in Value_util. *)
type call_site = kernel_function * kinstr
+(** Value call-site.
+ A callsite [(f,p)] represents a call at function [f] invoked
+ {i from} program point [p].
+*)
+
type callstack = call_site list
-(** Value callstacks, as used e.g. in Db.Value hooks *)
+(** Value callstacks, as used e.g. in Db.Value hooks.
+
+ The head call site [(f,p)] is the most recent one,
+ where current function [f] has been called from program point [p].
+
+ Therefore, the tail call site is expected to be [(main,Kglobal)]
+ where [main] is the global entry point.
+
+ Moreover, given two consecutive call-sites […(_,p);(g,_)…] in a callstack,
+ program point [p] is then expected to live in function [g].
+ *)
module Callsite: Datatype.S_with_collections with type t = call_site
module Callstack: sig