diff --git a/ivette/src/frama-c/eva/Values.tsx b/ivette/src/frama-c/eva/Values.tsx index c2580b783143d1e705fc3d1f7a0143c7015db590..986e41886b35118410be3bc7cab50a4a535b8b4a 100644 --- a/ivette/src/frama-c/eva/Values.tsx +++ b/ivette/src/frama-c/eva/Values.tsx @@ -50,23 +50,35 @@ function ProbeEditor() { const label = probe?.label; const code = probe?.code; const rank = probe?.rank; + const byCS = probe?.byCallstacks; const stmt = rank ? `@S${rank}` : undefined; + const stacks = model.getStacks(probe).length; const { cols, rows } = sizeof(code); + const width = WSIZER.dimension(cols) + 4; + const height = HSIZER.dimension(rows) + 3; const visible = probe ? !!code : model.getRowCount() > 0; const visibility = visible ? 'visible' : 'hidden'; return ( <Hpack style={{ visibility }} className="eva-probe"> <Label className="eva-probe-label">{label && `${label}:`}</Label> - <div className="eva-probe-code"> + <div style={{ width, height }} className="eva-probe-code"> <SizedArea cols={cols} rows={rows}>{code}</SizedArea> </div> <Code className="eva-probe-stmt">{stmt}</Code> + <IconButton + className="eva-probe-button" + visible={byCS || stacks > 0} + selected={byCS} + icon="ITEMS.LIST" + title={`Details by callstack (${stacks})`} + onClick={() => { if (probe) probe.setByCallstacks(!byCS); }} + /> <IconButton className="eva-probe-button" kind={transient ? 'selected' : 'warning'} icon={transient ? 'CIRC.CHECK' : 'CIRC.CLOSE'} - onClick={() => { if (probe) probe.setTransient(!transient); }} title={transient ? 'Make the probe persistent' : 'Release the probe'} + onClick={() => { if (probe) probe.setTransient(!transient); }} /> <Filler /> </Hpack> @@ -93,22 +105,26 @@ function TableCell(props: TableCellProps) { const style = { width: minWidth, maxWidth }; let styling = 'dome-text-code'; let contents: React.ReactNode = props.probe.marker; - const { transient, label, code } = probe; + const { transient } = probe; switch (kind) { case 'probes': if (transient) { styling = 'dome-text-label'; contents = '« Probe »'; - } else if (label) { - styling = 'dome-text-label'; - contents = label; } else { - contents = <>{code}</>; + const { rank, code, label } = probe; + const atpoint = rank && ( + <span className='dome-text-code eva-probe-stmt'>@S{probe.rank}</span> + ); + styling = 'dome-text-label'; + contents = ( + <>{label ?? code}{atpoint}</> + ); } break; case 'values': { - const { values } = model.cache.getValues(probe.marker); + const { values } = model.values.getValues(probe.marker); const { cols, rows } = sizeof(values); contents = ( <SizedArea cols={cols} rows={rows}> diff --git a/ivette/src/frama-c/eva/cells.ts b/ivette/src/frama-c/eva/cells.ts index 95a2dd5e3c242f2d0685ddfd148c4bc2d62f7435..eb3b2b8e225d681ed0e02b8b691ad960901b0816 100644 --- a/ivette/src/frama-c/eva/cells.ts +++ b/ivette/src/frama-c/eva/cells.ts @@ -65,7 +65,7 @@ export function leq(a: Size, b: Size): boolean { } // -------------------------------------------------------------------------- -// --- Value Cache +// --- Data // -------------------------------------------------------------------------- export type EvaStatus = 'True' | 'False' | 'Unknown'; @@ -81,6 +81,10 @@ export interface EvaValues { size: Size; } +// -------------------------------------------------------------------------- +// --- Value Cache +// -------------------------------------------------------------------------- + export class ValueCache { private readonly state: StateCallbacks; diff --git a/ivette/src/frama-c/eva/model.ts b/ivette/src/frama-c/eva/model.ts index a376ea82fac05c4652733b3bc8d5e1d6047dbaeb..7f749f28ed4e22cc0b3a1cd93504444c63224e72 100644 --- a/ivette/src/frama-c/eva/model.ts +++ b/ivette/src/frama-c/eva/model.ts @@ -13,6 +13,7 @@ import * as Ast from 'frama-c/api/kernel/ast'; // Model import { Probe } from './probes'; +import { StacksCache } from './stacks'; import { callback, StateCallbacks, ValueCache } from './cells'; import { LayoutProps, LayoutEngine, Row } from './layout'; @@ -59,9 +60,15 @@ export class Model implements StateCallbacks { return p; } - // --- Values + getStacks(p: Probe | undefined): Values.callstack[] { + const stmt = p?.stmt; + return stmt ? this.stacks.getStacks(stmt) : []; + } + + // --- Caches - readonly cache = new ValueCache(this); + readonly stacks = new StacksCache(this); + readonly values = new ValueCache(this); // --- Rows @@ -91,7 +98,7 @@ export class Model implements StateCallbacks { toLayout.push(p); } }); - const engine = new LayoutEngine(this.cache, this.layout); + const engine = new LayoutEngine(this.values, this.layout); toLayout.sort(Probe.order).forEach(engine.push); this.rows = engine.flush(); this.forceUpdate(); @@ -128,14 +135,12 @@ export class Model implements StateCallbacks { // --- Force Reload (empty caches) forceReload() { - this.probes.forEach((p) => { - if (p.transient && p !== this.focused) { - this.probes.delete(p.marker); - } else { - p.requestProbeInfo(); - } - }); - this.cache.clear(); + this.focused = undefined; + this.remanent = undefined; + this.selected = undefined; + this.probes.clear(); + this.stacks.clear(); + this.values.clear(); this.forceLayout(); } diff --git a/ivette/src/frama-c/eva/probes.ts b/ivette/src/frama-c/eva/probes.ts index 3b121c23f0f55b64dc9cfa4b82b045b21ddd25a9..be73a91aa1285c5dad7b6a4ee152565347189fd4 100644 --- a/ivette/src/frama-c/eva/probes.ts +++ b/ivette/src/frama-c/eva/probes.ts @@ -53,6 +53,7 @@ export class Probe { rank?: number; minCols: number = LabelSize; maxCols: number = LabelSize; + byCallstacks = false; constructor(state: StateCallbacks, marker: Ast.marker) { this.marker = marker; @@ -98,6 +99,13 @@ export class Probe { } } + setByCallstacks(byCS: boolean) { + if (byCS !== this.byCallstacks) { + this.byCallstacks = byCS; + this.state.forceLayout(); + } + } + // -------------------------------------------------------------------------- // --- Ordering // -------------------------------------------------------------------------- diff --git a/ivette/src/frama-c/eva/stacks.ts b/ivette/src/frama-c/eva/stacks.ts new file mode 100644 index 0000000000000000000000000000000000000000..adbf6bd605bd1fc6c8caab4aa07bd00f06f4406c --- /dev/null +++ b/ivette/src/frama-c/eva/stacks.ts @@ -0,0 +1,64 @@ +// -------------------------------------------------------------------------- +// --- CallStacks +// -------------------------------------------------------------------------- + +import * as Server from 'frama-c/server'; +import * as Values from 'frama-c/api/plugins/eva/values'; + +import { StateCallbacks } from './cells'; + +// -------------------------------------------------------------------------- +// --- Callstack infos +// -------------------------------------------------------------------------- + +export type callstacks = Values.callstack[]; + +// -------------------------------------------------------------------------- +// --- CallStacks Cache +// -------------------------------------------------------------------------- + +export class StacksCache { + + private readonly state: StateCallbacks; + private readonly stacks = new Map<string, callstacks>(); + + // -------------------------------------------------------------------------- + // --- LifeCycle + // -------------------------------------------------------------------------- + + constructor(state: StateCallbacks) { + this.state = 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 []; + } + + // -------------------------------------------------------------------------- + // --- Fetchers + // -------------------------------------------------------------------------- + + private requestCallstacks(stmt: string) { + Server + .send(Values.getCallstacks, stmt) + .then((cs: callstacks) => { + this.stacks.set(stmt, cs); + this.state.forceLayout(); + }); + } + +} + +// -------------------------------------------------------------------------- diff --git a/ivette/src/frama-c/eva/style.css b/ivette/src/frama-c/eva/style.css index 24226a9b2e210e3d002ae88a40ed3f3ac5d30580..7afd3a1d6c70105441970cdcde4c6d46ad0f3e28 100644 --- a/ivette/src/frama-c/eva/style.css +++ b/ivette/src/frama-c/eva/style.css @@ -14,7 +14,7 @@ /* -------------------------------------------------------------------------- */ .eva-probe { - margin: 4px; + margin: 8px; width: 100%; display: flex; } @@ -40,13 +40,14 @@ .eva-probe-stmt { flex: 0 0 auto; color: grey; - margin-left: 3px; - margin-right: 3px; - margin-top: 3px; + margin-left: 2px; + margin-right: 0px; + margin-top: 2px; } .eva-probe-button { flex: 0 0 auto; + margin: 1px; min-width: 16px; }