From 492ff29e49f3571f461384cb99ec813104d6ec57 Mon Sep 17 00:00:00 2001 From: Maxime Jacquemin <maxime2.jacquemin@gmail.com> Date: Wed, 16 Mar 2022 15:51:46 +0100 Subject: [PATCH] [ivette] Removing the old Eva component --- ivette/Makefile.distrib | 9 - ivette/headers/header_spec.txt | 11 +- ivette/src/frama-c/plugins/eva/cells.ts | 236 ---- ivette/src/frama-c/plugins/eva/diffed.tsx | 182 --- ivette/src/frama-c/plugins/eva/index.tsx | 2 +- ivette/src/frama-c/plugins/eva/layout.ts | 237 ---- ivette/src/frama-c/plugins/eva/model.ts | 316 ----- ivette/src/frama-c/plugins/eva/probeinfos.tsx | 172 --- ivette/src/frama-c/plugins/eva/probes.ts | 114 -- ivette/src/frama-c/plugins/eva/sized.tsx | 141 --- ivette/src/frama-c/plugins/eva/stacks.ts | 141 --- ivette/src/frama-c/plugins/eva/state.tsx | 820 ------------- ivette/src/frama-c/plugins/eva/valueinfos.tsx | 148 --- ivette/src/frama-c/plugins/eva/valuetable.tsx | 1065 ++++++++++++----- 14 files changed, 737 insertions(+), 2857 deletions(-) delete mode 100644 ivette/src/frama-c/plugins/eva/cells.ts delete mode 100644 ivette/src/frama-c/plugins/eva/diffed.tsx delete mode 100644 ivette/src/frama-c/plugins/eva/layout.ts delete mode 100644 ivette/src/frama-c/plugins/eva/model.ts delete mode 100644 ivette/src/frama-c/plugins/eva/probeinfos.tsx delete mode 100644 ivette/src/frama-c/plugins/eva/probes.ts delete mode 100644 ivette/src/frama-c/plugins/eva/sized.tsx delete mode 100644 ivette/src/frama-c/plugins/eva/stacks.ts delete mode 100644 ivette/src/frama-c/plugins/eva/state.tsx delete mode 100644 ivette/src/frama-c/plugins/eva/valueinfos.tsx diff --git a/ivette/Makefile.distrib b/ivette/Makefile.distrib index 87068f0322f..5a9f51b860b 100644 --- a/ivette/Makefile.distrib +++ b/ivette/Makefile.distrib @@ -175,19 +175,10 @@ DISTRIB_FILES += ivette/src/frama-c/plugins/eva/CoverageMeter.tsx DISTRIB_FILES += ivette/src/frama-c/plugins/eva/Summary.tsx DISTRIB_FILES += ivette/src/frama-c/plugins/eva/api/general/index.ts DISTRIB_FILES += ivette/src/frama-c/plugins/eva/api/values/index.ts -DISTRIB_FILES += ivette/src/frama-c/plugins/eva/cells.ts -DISTRIB_FILES += ivette/src/frama-c/plugins/eva/diffed.tsx DISTRIB_FILES += ivette/src/frama-c/plugins/eva/index.tsx -DISTRIB_FILES += ivette/src/frama-c/plugins/eva/layout.ts -DISTRIB_FILES += ivette/src/frama-c/plugins/eva/model.ts DISTRIB_FILES += ivette/src/frama-c/plugins/eva/pkg.json -DISTRIB_FILES += ivette/src/frama-c/plugins/eva/probeinfos.tsx -DISTRIB_FILES += ivette/src/frama-c/plugins/eva/probes.ts -DISTRIB_FILES += ivette/src/frama-c/plugins/eva/sized.tsx -DISTRIB_FILES += ivette/src/frama-c/plugins/eva/stacks.ts DISTRIB_FILES += ivette/src/frama-c/plugins/eva/style.css DISTRIB_FILES += ivette/src/frama-c/plugins/eva/summary.css -DISTRIB_FILES += ivette/src/frama-c/plugins/eva/valueinfos.tsx DISTRIB_FILES += ivette/src/frama-c/plugins/eva/valuetable.tsx DISTRIB_FILES += ivette/src/frama-c/plugins/pivot/api/general/index.ts DISTRIB_FILES += ivette/src/frama-c/plugins/studia/api/studia/index.ts diff --git a/ivette/headers/header_spec.txt b/ivette/headers/header_spec.txt index 75e97fe5eb7..1bc4d665822 100644 --- a/ivette/headers/header_spec.txt +++ b/ivette/headers/header_spec.txt @@ -173,22 +173,13 @@ src/frama-c/plugins/dive/tippy.css: .ignore src/frama-c/plugins/eva/Coverage.tsx: CEA_LGPL src/frama-c/plugins/eva/CoverageMeter.tsx: CEA_LGPL src/frama-c/plugins/eva/Summary.tsx: CEA_LGPL +src/frama-c/plugins/eva/valuetable.tsx: CEA_LGPL src/frama-c/plugins/eva/api/general/index.ts: CEA_LGPL src/frama-c/plugins/eva/api/values/index.ts: CEA_LGPL -src/frama-c/plugins/eva/cells.ts: CEA_LGPL -src/frama-c/plugins/eva/diffed.tsx: CEA_LGPL src/frama-c/plugins/eva/index.tsx: CEA_LGPL -src/frama-c/plugins/eva/layout.ts: CEA_LGPL -src/frama-c/plugins/eva/model.ts: CEA_LGPL src/frama-c/plugins/eva/pkg.json: .ignore -src/frama-c/plugins/eva/probeinfos.tsx: CEA_LGPL -src/frama-c/plugins/eva/probes.ts: CEA_LGPL -src/frama-c/plugins/eva/sized.tsx: CEA_LGPL -src/frama-c/plugins/eva/stacks.ts: CEA_LGPL src/frama-c/plugins/eva/style.css: .ignore src/frama-c/plugins/eva/summary.css: .ignore -src/frama-c/plugins/eva/valueinfos.tsx: CEA_LGPL -src/frama-c/plugins/eva/valuetable.tsx: CEA_LGPL src/frama-c/plugins/pivot/api/general/index.ts: CEA_LGPL src/frama-c/plugins/studia/api/studia/index.ts: CEA_LGPL src/frama-c/react-pivottable.d.ts: CEA_LGPL diff --git a/ivette/src/frama-c/plugins/eva/cells.ts b/ivette/src/frama-c/plugins/eva/cells.ts deleted file mode 100644 index 02e3ef3ffdc..00000000000 --- a/ivette/src/frama-c/plugins/eva/cells.ts +++ /dev/null @@ -1,236 +0,0 @@ -/* ************************************************************************ */ -/* */ -/* This file is part of Frama-C. */ -/* */ -/* Copyright (C) 2007-2022 */ -/* CEA (Commissariat à l'énergie atomique et aux énergies */ -/* alternatives) */ -/* */ -/* you can redistribute it and/or modify it under the terms of the GNU */ -/* Lesser General Public License as published by the Free Software */ -/* Foundation, version 2.1. */ -/* */ -/* It is distributed in the hope that it will be useful, */ -/* but WITHOUT ANY WARRANTY; without even the implied warranty of */ -/* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the */ -/* GNU Lesser General Public License for more details. */ -/* */ -/* See the GNU Lesser General Public License version 2.1 */ -/* for more details (enclosed in the file licenses/LGPLv2.1). */ -/* */ -/* ************************************************************************ */ - -// -------------------------------------------------------------------------- -// --- Cells -// -------------------------------------------------------------------------- - -// Frama-C -import * as Server from 'frama-c/server'; -import * as Ast from 'frama-c/kernel/api/ast'; -import * as Values from 'frama-c/plugins/eva/api/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 === undefined) 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 EvaPointedVar = [string, Ast.marker]; -export type Evaluation = Values.evaluation; - -const emptyEvaluation: Values.evaluation = { - value: '', - alarms: [], - pointedVars: [], -}; - -export interface EvaValues { - errors?: string; - vBefore: Evaluation; - vAfter?: Evaluation; - vThen?: Evaluation; - vElse?: Evaluation; - size: Size; -} - -// -------------------------------------------------------------------------- -// --- Value Cache -// -------------------------------------------------------------------------- - -export interface Probe { - fct: string | undefined; - marker: Ast.marker; -} - -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(): void { - this.smax = EMPTY; - this.probes.clear(); - this.stacks.clear(); - this.vcache.clear(); - this.state.forceLayout(); - } - - // --- Cached Measures - - getMaxSize(): Size { return this.smax; } - - getProbeSize(target: Ast.marker): Size { - return this.probes.get(target) ?? EMPTY; - } - - private static stackKey(fct: string, callstack: Values.callstack): string { - return `${fct}::${callstack}`; - } - - getStackSize(fct: string, callstack: Values.callstack): Size { - const key = ValueCache.stackKey(fct, callstack); - return this.stacks.get(key) ?? EMPTY; - } - - // --- Cached Values & Request Update - - getValues( - { fct, marker }: Probe, - callstack: Values.callstack | undefined, - ): EvaValues { - const key = callstack !== undefined ? `${marker}@${callstack}` : marker; - const cache = this.vcache; - const cached = cache.get(key); - if (cached) return cached; - const newValue: EvaValues = { vBefore: emptyEvaluation, size: EMPTY }; - if (callstack !== undefined && fct === undefined) - return newValue; - // callstack !== undefined ==> fct !== undefined) - cache.set(key, newValue); - Server - .send(Values.getValues, { target: marker, callstack }) - .then((r) => { - newValue.errors = undefined; - if (r.vBefore) newValue.vBefore = r.vBefore; - newValue.vAfter = r.vAfter; - newValue.vThen = r.vThen; - newValue.vElse = r.vElse; - if (this.updateLayout(marker, fct, 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, - fct: string | undefined, - callstack: Values.callstack | undefined, - v: EvaValues, - ): boolean { - // measuring cell - let s = sizeof(v.vBefore.value); - s = addS(s, v.vAfter?.value); - s = addS(s, v.vThen?.value); - s = addS(s, v.vElse?.value); - 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 (fct === undefined) small = false; - else { - const key = ValueCache.stackKey(fct, 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/plugins/eva/diffed.tsx b/ivette/src/frama-c/plugins/eva/diffed.tsx deleted file mode 100644 index 5859784ad91..00000000000 --- a/ivette/src/frama-c/plugins/eva/diffed.tsx +++ /dev/null @@ -1,182 +0,0 @@ -/* ************************************************************************ */ -/* */ -/* This file is part of Frama-C. */ -/* */ -/* Copyright (C) 2007-2022 */ -/* CEA (Commissariat à l'énergie atomique et aux énergies */ -/* alternatives) */ -/* */ -/* you can redistribute it and/or modify it under the terms of the GNU */ -/* Lesser General Public License as published by the Free Software */ -/* Foundation, version 2.1. */ -/* */ -/* It is distributed in the hope that it will be useful, */ -/* but WITHOUT ANY WARRANTY; without even the implied warranty of */ -/* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the */ -/* GNU Lesser General Public License for more details. */ -/* */ -/* See the GNU Lesser General Public License version 2.1 */ -/* for more details (enclosed in the file licenses/LGPLv2.1). */ -/* */ -/* ************************************************************************ */ - -// -------------------------------------------------------------------------- -// --- 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(): void { - this.added = false; - this.removed = false; - this.value = ''; - this.scratch = ''; - this.contents = []; - } - - push(c: Change): void { - 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(): void { - 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(): string { - 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<React.ReactNode>(() => { - if (text === diff) return text; - const buffer = new DiffBuffer(); - const chunks = diffChars(text, diff); - chunks.forEach(buffer.push); - return buffer.getContents(); - }, [text, diff]); - return <>{contents}</>; -} - -/* --------------------------------------------------------------------------*/ -/* --- 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<React.ReactNode>(() => { - 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}</>; -} - -/* --------------------------------------------------------------------------*/ -/* --- Diff Component ---*/ -/* --------------------------------------------------------------------------*/ - -export interface DiffProps { - text?: string; - diff?: string; - diff2?: string; -} - - -export function Diff(props: DiffProps): JSX.Element | null { - const { text, diff, diff2 } = props; - if (text === undefined) - return null; - if (diff !== undefined && diff2 !== undefined) - return <Diff3 text={text} diffA={diff} diffB={diff2} />; - if (diff !== undefined) { - if (diff === text) return <>{text}</>; - return <Diff2 text={text} diff={diff} />; - } - if (diff2 !== undefined) { - if (diff2 === text) return <>{text}</>; - return <Diff2 text={text} diff={diff2} />; - } - return <>{text}</>; -} - -// -------------------------------------------------------------------------- diff --git a/ivette/src/frama-c/plugins/eva/index.tsx b/ivette/src/frama-c/plugins/eva/index.tsx index e88ef8411b0..2df245b2abe 100644 --- a/ivette/src/frama-c/plugins/eva/index.tsx +++ b/ivette/src/frama-c/plugins/eva/index.tsx @@ -25,7 +25,7 @@ // -------------------------------------------------------------------------- import * as Ivette from 'ivette'; -import { } from 'frama-c/plugins/eva/state'; +import { } from 'frama-c/plugins/eva/valuetable'; import { } from './Summary'; import { } from './Coverage'; import './style.css'; diff --git a/ivette/src/frama-c/plugins/eva/layout.ts b/ivette/src/frama-c/plugins/eva/layout.ts deleted file mode 100644 index b8e4c1e27eb..00000000000 --- a/ivette/src/frama-c/plugins/eva/layout.ts +++ /dev/null @@ -1,237 +0,0 @@ -/* ************************************************************************ */ -/* */ -/* This file is part of Frama-C. */ -/* */ -/* Copyright (C) 2007-2022 */ -/* CEA (Commissariat à l'énergie atomique et aux énergies */ -/* alternatives) */ -/* */ -/* you can redistribute it and/or modify it under the terms of the GNU */ -/* Lesser General Public License as published by the Free Software */ -/* Foundation, version 2.1. */ -/* */ -/* It is distributed in the hope that it will be useful, */ -/* but WITHOUT ANY WARRANTY; without even the implied warranty of */ -/* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the */ -/* GNU Lesser General Public License for more details. */ -/* */ -/* See the GNU Lesser General Public License version 2.1 */ -/* for more details (enclosed in the file licenses/LGPLv2.1). */ -/* */ -/* ************************************************************************ */ - -/* --------------------------------------------------------------------------*/ -/* --- Layout ---*/ -/* --------------------------------------------------------------------------*/ - -import { callstack } from 'frama-c/plugins/eva/api/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 = 'section' | 'probes' | 'values' | 'callstack'; - -export interface Row { - key: string; - fct: string; - kind: RowKind; - probes: Probe[]; - headstack?: string; - stackIndex?: number; - stackCount?: number; - callstack?: callstack; - hlines: number; -} - -/* --------------------------------------------------------------------------*/ -/* --- Layout Enfine ---*/ -/* --------------------------------------------------------------------------*/ - -const HEAD_PADDING = 4; // Left margin -const CELL_PADDING = 4; // Inter cell padding -const TEXT_PADDING = 2; // Intra cell padding -const HCROP = 18; -const VCROP = 1; - -export class LayoutEngine { - - // --- Setup - - private readonly folded: (fct: string) => boolean; - 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, - folded: (fct: string) => boolean, - ) { - this.values = values; - this.stacks = stacks; - this.folded = folded; - const zoom = Math.max(0, props?.zoom ?? 0); - this.vcrop = VCROP + 3 * zoom; - this.hcrop = HCROP + zoom; - this.margin = (props?.margin ?? 80) - HEAD_PADDING; - this.push = this.push.bind(this); - } - - // --- Probe Buffer - private byFct?: string; // current function - private byStk = new Map<string, boolean>(); // callstack probes - private skip?: boolean; // skip current function - private rowSize: Size = EMPTY; - private buffer: Probe[] = []; - private rows: Row[] = []; - private chained?: Probe; - - crop(zoomed: boolean, s: Size): Size { - const s$cols = s.cols + TEXT_PADDING; - const cols = zoomed ? s$cols : Math.min(s$cols, this.hcrop); - const rows = zoomed ? s.rows : Math.min(s.rows, this.vcrop); - return { - cols: Math.max(HCROP, cols), - rows: Math.max(VCROP, rows), - }; - } - - layout(ps: Probe[], byCallstacks: Map<string, boolean>): Row[] { - this.chained = undefined; - this.byStk = byCallstacks; - ps.sort(LayoutEngine.order).forEach(this.push); - return this.flush(); - } - - private static order(p: Probe, q: Probe): number { - const fp = p.fct; - const fq = q.fct; - if (fp === fq) { - const rp = p.rank ?? 0; - const rq = q.rank ?? 0; - if (rp < rq) return (-1); - if (rp > rq) return (+1); - if (p.marker < q.marker) return (-1); - if (p.marker > q.marker) return (+1); - } - return 0; - } - - private push(p: Probe): void { - // --- sectionning - const { fct } = p; - if (fct !== this.byFct) { - this.flush(); - this.rows.push({ - key: `S:${fct}`, - kind: 'section', - fct, - probes: [], - hlines: 1, - }); - this.byFct = fct; - this.csRowsCounter = 1; - this.skip = this.folded(fct); - } - if (this.skip) return; - // --- chaining - const q = this.chained; - if (q) q.next = p; - p.prev = q; - this.chained = p; - // --- sizing - const probeSize = this.values.getProbeSize(p.marker); - const s = this.crop(p.zoomed, probeSize); - p.zoomable = p.zoomed || !leq(probeSize, s); - p.minCols = s.cols; - p.maxCols = Math.max(p.minCols, probeSize.cols); - // --- queueing - if (s.cols + this.rowSize.cols > this.margin) - this.flush(); - this.rowSize = addH(this.rowSize, s); - this.rowSize.cols += CELL_PADDING; - this.buffer.push(p); - } - - // --- Flush Rows - - private csRowsCounter = 1; - - private flush(): Row[] { - const ps = this.buffer; - const rs = this.rows; - const fct = this.byFct; - if (fct && ps.length > 0) { - const stk = this.byStk.get(fct); - const hlines = this.rowSize.rows; - if (stk) { - // --- by callstacks - const markers = ps.map((p) => p.marker); - const stacks = this.stacks.getStacks(...markers); - const summary = fct ? this.stacks.getSummary(fct) : false; - const callstacks = stacks.length; - const { csRowsCounter } = this; - rs.push({ - key: `P:${fct}:${csRowsCounter}`, - kind: 'probes', - probes: ps, - stackCount: callstacks, - fct, - hlines: 1, - }); - if (summary && callstacks > 1) rs.push({ - key: `V:${fct}:${csRowsCounter}`, - kind: 'values', - probes: ps, - stackIndex: -1, - stackCount: stacks.length, - fct, - hlines, - }); - stacks.forEach((cs, k) => { - rs.push({ - key: `C:${fct}:${csRowsCounter}:${cs}`, - kind: 'callstack', - probes: ps, - stackIndex: k, - stackCount: callstacks, - callstack: cs, - fct, - hlines, - }); - }); - } else { - // --- not by callstacks - const n = rs.length; - rs.push({ - key: `P#${n}`, - kind: 'probes', - probes: ps, - fct, - hlines: 1, - }, { - key: `V#${n}`, - kind: 'values', - probes: ps, - fct, - hlines, - }); - } - } - this.buffer = []; - this.rowSize = EMPTY; - this.csRowsCounter++; - return rs; - } - -} - -/* --------------------------------------------------------------------------*/ diff --git a/ivette/src/frama-c/plugins/eva/model.ts b/ivette/src/frama-c/plugins/eva/model.ts deleted file mode 100644 index 01e3d14334b..00000000000 --- a/ivette/src/frama-c/plugins/eva/model.ts +++ /dev/null @@ -1,316 +0,0 @@ -/* ************************************************************************ */ -/* */ -/* This file is part of Frama-C. */ -/* */ -/* Copyright (C) 2007-2022 */ -/* CEA (Commissariat à l'énergie atomique et aux énergies */ -/* alternatives) */ -/* */ -/* you can redistribute it and/or modify it under the terms of the GNU */ -/* Lesser General Public License as published by the Free Software */ -/* Foundation, version 2.1. */ -/* */ -/* It is distributed in the hope that it will be useful, */ -/* but WITHOUT ANY WARRANTY; without even the implied warranty of */ -/* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the */ -/* GNU Lesser General Public License for more details. */ -/* */ -/* See the GNU Lesser General Public License version 2.1 */ -/* for more details (enclosed in the file licenses/LGPLv2.1). */ -/* */ -/* ************************************************************************ */ - -/* eslint-disable @typescript-eslint/explicit-function-return-type */ - -// -------------------------------------------------------------------------- -// --- 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 States from 'frama-c/states'; -import * as Values from 'frama-c/plugins/eva/api/values'; - -// 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 { - location?: States.Location; -} - -export type EvalStmt = 'Before' | 'After'; -export type EvalCond = 'Cond' | 'Then' | 'Else'; - -/* --------------------------------------------------------------------------*/ -/* --- 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.metaSelection = this.metaSelection.bind(this); - this.getRowKey = this.getRowKey.bind(this); - this.getRowCount = this.getRowCount.bind(this); - this.getRowLines = this.getRowLines.bind(this); - this.isFolded = this.isFolded.bind(this); - } - - // --- Probes - - private vstmt: EvalStmt = 'Before'; - private vcond: EvalCond = 'Cond'; - private selected?: Probe; - private focused?: Probe; - private callstack?: Values.callstack; - private remanent?: Probe; // last transient - private probes = new Map<string, Probe>(); - private folded = new Map<string, boolean>(); // folded functions - private byCallstacks = new Map<string, boolean>(); - - getFocused() { return this.focused; } - isFocused(p: Probe | undefined) { return this.focused === p; } - - getProbe(location: States.Location | undefined): Probe | undefined { - if (!location) return undefined; - const { fct, marker } = location; - if (fct && marker) { - let p = this.probes.get(marker); - if (!p) { - p = new Probe(this, fct, marker); - this.probes.set(marker, p); - p.requestProbeInfo(); - } - return p; - } - return undefined; - } - - addProbe(location: States.Location) { - const { fct, marker } = location; - if (fct && marker) { - const probe = new Probe(this, fct, marker); - probe.setPersistent(); - probe.requestProbeInfo(); - this.probes.set(marker, probe); - this.forceLayout(); - } - } - - removeProbe(probe: Probe) { - probe.setTransient(); - if (this.selected === probe) - this.clearSelection(); - } - - getStacks(p: Probe | undefined): Values.callstack[] { - return p ? this.stacks.getStacks(p.marker) : []; - } - - getVstmt(): EvalStmt { return this.vstmt; } - getVcond(): EvalCond { return this.vcond; } - setVstmt(s: EvalStmt) { this.vstmt = s; this.forceUpdate(); } - setVcond(s: EvalCond) { this.vcond = s; this.forceUpdate(); } - - isFolded(fct: string): boolean { - return (this.focused?.fct !== fct) && (this.folded.get(fct) ?? false); - } - - isFoldable(fct: string): boolean { - return this.focused?.fct !== fct; - } - - setFolded(fct: string, folded: boolean) { - this.folded.set(fct, folded); - this.forceLayout(); - } - - isByCallstacks(fct: string): boolean { - return this.byCallstacks.get(fct) ?? false; - } - - setByCallstacks(fct: string, b: boolean) { - this.byCallstacks.set(fct, b); - this.forceLayout(); - } - - clearFunction(fct: string) { - let selected = false; - this.probes.forEach((p) => { - if (p.fct === fct) { - p.setTransient(); - if (this.selected === p) - selected = true; - } - }); - if (selected) - this.clearSelection(); - } - - // --- 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 { - if (!this.byCallstacks) return false; - const cs = this.callstack; - return cs !== undefined && cs === row.callstack; - } - - isAlignedRow(row: Row): boolean { - const cs = this.callstack; - const cr = row.callstack; - return cs !== undefined && cr !== undefined && this.stacks.aligned(cs, cr); - } - - 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; - this.selected = this.getProbe(ly.location); - this.forceLayout(); - } - } - - metaSelection(location: States.Location) { - const p = this.getProbe(location); - if (p && p.transient) - p.setPersistent(); - } - - clearSelection() { - this.focused = undefined; - this.selected = undefined; - this.remanent = undefined; - this.forceLayout(); - } - - // --- Recompute Layout - - private computeLayout() { - if (this.lock) return; - this.lock = true; - const s = this.selected; - if (!s) { - this.focused = undefined; - this.remanent = undefined; - } else if (!s.loading) { - this.focused = s; - 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, - this.isFolded, - ); - this.rows = engine.layout(toLayout, this.byCallstacks); - 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(); } - - // --- Global Signals - - mount() { - States.MetaSelection.on(this.metaSelection); - Server.onSignal(Values.changed, this.forceReload); - } - - unmount() { - States.MetaSelection.off(this.metaSelection); - Server.offSignal(Values.changed, this.forceReload); - } - -} - -export interface ModelProp { - model: Model; -} diff --git a/ivette/src/frama-c/plugins/eva/probeinfos.tsx b/ivette/src/frama-c/plugins/eva/probeinfos.tsx deleted file mode 100644 index 9baa4c9acdb..00000000000 --- a/ivette/src/frama-c/plugins/eva/probeinfos.tsx +++ /dev/null @@ -1,172 +0,0 @@ -/* ************************************************************************ */ -/* */ -/* This file is part of Frama-C. */ -/* */ -/* Copyright (C) 2007-2022 */ -/* CEA (Commissariat à l'énergie atomique et aux énergies */ -/* alternatives) */ -/* */ -/* you can redistribute it and/or modify it under the terms of the GNU */ -/* Lesser General Public License as published by the Free Software */ -/* Foundation, version 2.1. */ -/* */ -/* It is distributed in the hope that it will be useful, */ -/* but WITHOUT ANY WARRANTY; without even the implied warranty of */ -/* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the */ -/* GNU Lesser General Public License for more details. */ -/* */ -/* See the GNU Lesser General Public License version 2.1 */ -/* for more details (enclosed in the file licenses/LGPLv2.1). */ -/* */ -/* ************************************************************************ */ - -// -------------------------------------------------------------------------- -// --- Eva Values -// -------------------------------------------------------------------------- - -// React & Dome -import React from 'react'; -import { Hpack, Filler } from 'dome/layout/boxes'; -import { Code } from 'dome/controls/labels'; -import { IconButton } from 'dome/controls/buttons'; -import { ButtonGroup, Button } from 'dome/frame/toolbars'; - -// Frama-C -import * as States from 'frama-c/states'; - -// Locals -import { SizedArea } from './sized'; -import { sizeof } from './cells'; -import { ModelProp } from './model'; -import { Stmt } from './valueinfos'; - -// -------------------------------------------------------------------------- -// --- Probe Editor -// -------------------------------------------------------------------------- - -function ProbeEditor(props: ModelProp): JSX.Element | null { - const { model } = props; - const probe = model.getFocused(); - if (!probe || !probe.code) return null; - const { code } = probe; - const { stmt, marker } = probe; - const { cols, rows } = sizeof(code); - const { transient } = probe; - const { zoomed } = probe; - const { zoomable } = probe; - return ( - <> - <div className="eva-probeinfo-code"> - <SizedArea cols={cols} rows={rows}>{code}</SizedArea> - </div> - <Code><Stmt stmt={stmt} marker={marker} /></Code> - <IconButton - icon="SEARCH" - className="eva-probeinfo-button" - display={zoomable} - selected={zoomed} - title="Resize cells to fit values" - onClick={() => { if (probe) probe.setZoomed(!zoomed); }} - /> - <IconButton - icon="PIN" - className="eva-probeinfo-button" - selected={!transient} - title={transient ? 'Make the probe persistent' : 'Release the probe'} - onClick={() => { - if (probe) { - if (transient) probe.setPersistent(); - else probe.setTransient(); - } - }} - /> - <IconButton - icon="CIRC.CLOSE" - className="eva-probeinfo-button" - display={!transient} - title="Discard the probe" - onClick={() => { - if (probe) { - probe.setTransient(); - const p = probe.next ?? probe.prev; - if (p) setImmediate(() => { - States.setSelection({ fct: p.fct, marker: p.marker }); - }); - else model.clearSelection(); - } - }} - /> - </> - ); -} - -// -------------------------------------------------------------------------- -// --- Probe Panel -// -------------------------------------------------------------------------- - -export function ProbeInfos(props: ModelProp): JSX.Element { - const { model } = props; - const probe = model.getFocused(); - const fct = probe?.fct; - const byCS = fct ? model.isByCallstacks(fct) : false; - const effects = probe ? probe.effects : false; - const condition = probe ? probe.condition : false; - const summary = fct ? model.stacks.getSummary(fct) : false; - const vcond = model.getVcond(); - const vstmt = model.getVstmt(); - return ( - <Hpack className="eva-probeinfo"> - <ProbeEditor model={model} /> - <Filler /> - <ButtonGroup - enabled={!!probe} - className="eva-probeinfo-state" - > - <Button - label={'\u2211'} - title="Show Callstacks Summary" - selected={summary} - visible={byCS} - onClick={() => { if (fct) model.stacks.setSummary(fct, !summary); }} - /> - <Button - visible={condition} - label="C" - selected={vcond === 'Cond'} - title="Show values in all conditions" - onClick={() => model.setVcond('Cond')} - /> - <Button - visible={condition || vcond === 'Then'} - selected={vcond === 'Then'} - enabled={condition} - label="T" - value="Then" - title="Show reduced values when condition holds (Then)" - onClick={() => model.setVcond('Then')} - /> - <Button - visible={condition || vcond === 'Else'} - selected={vcond === 'Else'} - enabled={condition} - label="E" - value="Else" - title="Show reduced values when condition does not hold (Else)" - onClick={() => model.setVcond('Else')} - /> - <Button - visible={condition || effects} - selected={vstmt === 'After'} - label="A" - value="After" - title="Show values after/before statement effects" - onClick={() => { - model.setVstmt(vstmt === 'After' ? 'Before' : 'After'); - }} - /> - </ButtonGroup> - </Hpack> - ); -} - -// -------------------------------------------------------------------------- diff --git a/ivette/src/frama-c/plugins/eva/probes.ts b/ivette/src/frama-c/plugins/eva/probes.ts deleted file mode 100644 index e9bdb0da9ca..00000000000 --- a/ivette/src/frama-c/plugins/eva/probes.ts +++ /dev/null @@ -1,114 +0,0 @@ -/* ************************************************************************ */ -/* */ -/* This file is part of Frama-C. */ -/* */ -/* Copyright (C) 2007-2022 */ -/* CEA (Commissariat à l'énergie atomique et aux énergies */ -/* alternatives) */ -/* */ -/* you can redistribute it and/or modify it under the terms of the GNU */ -/* Lesser General Public License as published by the Free Software */ -/* Foundation, version 2.1. */ -/* */ -/* It is distributed in the hope that it will be useful, */ -/* but WITHOUT ANY WARRANTY; without even the implied warranty of */ -/* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the */ -/* GNU Lesser General Public License for more details. */ -/* */ -/* See the GNU Lesser General Public License version 2.1 */ -/* for more details (enclosed in the file licenses/LGPLv2.1). */ -/* */ -/* ************************************************************************ */ - -/* --------------------------------------------------------------------------*/ -/* --- Probes ---*/ -/* --------------------------------------------------------------------------*/ - -// Frama-C -import * as Server from 'frama-c/server'; -import * as Values from 'frama-c/plugins/eva/api/values'; -import * as Ast from 'frama-c/kernel/api/ast'; - -// Model -import { ModelCallbacks } from './cells'; - -/* --------------------------------------------------------------------------*/ -/* --- Probe State ---*/ -/* --------------------------------------------------------------------------*/ - -const LabelSize = 12; - -export class Probe { - - // properties - readonly fct: string; - readonly marker: Ast.marker; - readonly model: ModelCallbacks; - next?: Probe; - prev?: Probe; - transient = true; - loading = true; - code?: string; - stmt?: Ast.marker; - rank?: number; - minCols: number = LabelSize; - maxCols: number = LabelSize; - zoomed = true; - zoomable = false; - 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); - } - - requestProbeInfo(): void { - 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.loading = false; - }) - .catch(() => { - this.code = '(error)'; - this.stmt = undefined; - this.rank = undefined; - this.effects = false; - this.condition = false; - this.loading = false; - }) - .finally(this.model.forceLayout); - } - - // -------------------------------------------------------------------------- - // --- Internal State - // -------------------------------------------------------------------------- - - setPersistent(): void { this.updateTransient(false); } - setTransient(): void { this.updateTransient(true); } - - private updateTransient(tr: boolean): void { - if (this.transient !== tr) { - this.transient = tr; - this.model.forceLayout(); - } - } - - setZoomed(zoomed: boolean): void { - if (zoomed !== this.zoomed) { - this.zoomed = zoomed; - this.model.forceLayout(); - } - } - -} - -/* --------------------------------------------------------------------------*/ diff --git a/ivette/src/frama-c/plugins/eva/sized.tsx b/ivette/src/frama-c/plugins/eva/sized.tsx deleted file mode 100644 index 95496201039..00000000000 --- a/ivette/src/frama-c/plugins/eva/sized.tsx +++ /dev/null @@ -1,141 +0,0 @@ -/* ************************************************************************ */ -/* */ -/* This file is part of Frama-C. */ -/* */ -/* Copyright (C) 2007-2022 */ -/* CEA (Commissariat à l'énergie atomique et aux énergies */ -/* alternatives) */ -/* */ -/* you can redistribute it and/or modify it under the terms of the GNU */ -/* Lesser General Public License as published by the Free Software */ -/* Foundation, version 2.1. */ -/* */ -/* It is distributed in the hope that it will be useful, */ -/* but WITHOUT ANY WARRANTY; without even the implied warranty of */ -/* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the */ -/* GNU Lesser General Public License for more details. */ -/* */ -/* See the GNU Lesser General Public License version 2.1 */ -/* for more details (enclosed in the file licenses/LGPLv2.1). */ -/* */ -/* ************************************************************************ */ - -// -------------------------------------------------------------------------- -// --- 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): void { - 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): void { - 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): number { - const k = this.k.mean(); - const p = this.p.mean(); - return Math.round(0.5 + (y - p) / k); - } - - dimension(n: number): number { - const k = this.k.mean(); - const p = this.p.mean(); - return p + n * k; - } - - dump(x: string): string { - const k = this.k.mean(); - const p = this.p.mean(); - return `${k}.${x}+${p}`; - } - -} - -/* --------------------------------------------------------------------------*/ -/* --- Sizing Component ---*/ -/* --------------------------------------------------------------------------*/ - -export const WSIZER = new FontSizer(7, 6); -export const HSIZER = new FontSizer(15, 6); - -export interface SizedAreaProps { - cols: number; - rows: number; - children?: React.ReactNode; -} - -export function SizedArea(props: SizedAreaProps): JSX.Element { - 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-cell" - > - {children} - </div> - ); -} - -/* --------------------------------------------------------------------------*/ diff --git a/ivette/src/frama-c/plugins/eva/stacks.ts b/ivette/src/frama-c/plugins/eva/stacks.ts deleted file mode 100644 index 447890eef2d..00000000000 --- a/ivette/src/frama-c/plugins/eva/stacks.ts +++ /dev/null @@ -1,141 +0,0 @@ -/* ************************************************************************ */ -/* */ -/* This file is part of Frama-C. */ -/* */ -/* Copyright (C) 2007-2022 */ -/* CEA (Commissariat à l'énergie atomique et aux énergies */ -/* alternatives) */ -/* */ -/* you can redistribute it and/or modify it under the terms of the GNU */ -/* Lesser General Public License as published by the Free Software */ -/* Foundation, version 2.1. */ -/* */ -/* It is distributed in the hope that it will be useful, */ -/* but WITHOUT ANY WARRANTY; without even the implied warranty of */ -/* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the */ -/* GNU Lesser General Public License for more details. */ -/* */ -/* See the GNU Lesser General Public License version 2.1 */ -/* for more details (enclosed in the file licenses/LGPLv2.1). */ -/* */ -/* ************************************************************************ */ - -// -------------------------------------------------------------------------- -// --- CallStacks -// -------------------------------------------------------------------------- - -import * as Server from 'frama-c/server'; -import * as Ast from 'frama-c/kernel/api/ast'; -import * as Values from 'frama-c/plugins/eva/api/values'; - -import { ModelCallbacks } from './cells'; - -// -------------------------------------------------------------------------- -// --- Callstack infos -// -------------------------------------------------------------------------- - -export type callstacks = Values.callstack[]; -export interface Callsite { - callee: string; - caller?: string; - stmt?: Ast.marker; -} - -function equalSite(a: Callsite, b: Callsite): boolean { - return a.stmt === b.stmt && a.callee === b.callee; -} - -// -------------------------------------------------------------------------- -// --- CallStacks Cache -// -------------------------------------------------------------------------- - -export class StacksCache { - - private readonly model: ModelCallbacks; - private readonly stacks = new Map<string, callstacks>(); - private readonly summary = new Map<string, boolean>(); - private readonly calls = new Map<Values.callstack, Callsite[]>(); - - // -------------------------------------------------------------------------- - // --- LifeCycle - // -------------------------------------------------------------------------- - - constructor(state: ModelCallbacks) { - this.model = state; - } - - clear(): void { - this.stacks.clear(); - this.calls.clear(); - } - - // -------------------------------------------------------------------------- - // --- Getters - // -------------------------------------------------------------------------- - - getSummary(fct: string): boolean { - return this.summary.get(fct) ?? true; - } - - setSummary(fct: string, s: boolean): void { - this.summary.set(fct, s); - this.model.forceLayout(); - } - - getStacks(...markers: Ast.marker[]): callstacks { - if (markers.length === 0) return []; - const key = markers.join('$'); - const cs = this.stacks.get(key); - if (cs !== undefined) return cs; - this.stacks.set(key, []); - this.requestStacks(key, markers); - 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 []; - } - - aligned(a: Values.callstack, b: Values.callstack): boolean { - if (a === b) return true; - const ca = this.getCalls(a); - const cb = this.getCalls(b); - let ka = ca.length - 1; - let kb = cb.length - 1; - while (ka >= 0 && kb >= 0 && equalSite(ca[ka], cb[kb])) { - --ka; - --kb; - } - return ka < 0 || kb < 0; - } - - // -------------------------------------------------------------------------- - // --- Fetchers - // -------------------------------------------------------------------------- - - private requestStacks(key: string, markers: Ast.marker[]): void { - Server - .send(Values.getCallstacks, markers) - .then((stacks: callstacks) => { - this.stacks.set(key, stacks); - this.model.forceLayout(); - this.model.forceUpdate(); - }); - } - - private requestCalls(cs: Values.callstack): void { - Server - .send(Values.getCallstackInfo, cs) - .then((calls) => { - this.calls.set(cs, calls); - this.model.forceUpdate(); - }); - } - -} - -// -------------------------------------------------------------------------- diff --git a/ivette/src/frama-c/plugins/eva/state.tsx b/ivette/src/frama-c/plugins/eva/state.tsx deleted file mode 100644 index 2ec22a8465a..00000000000 --- a/ivette/src/frama-c/plugins/eva/state.tsx +++ /dev/null @@ -1,820 +0,0 @@ -/* ************************************************************************ */ -/* */ -/* This file is part of Frama-C. */ -/* */ -/* Copyright (C) 2007-2022 */ -/* CEA (Commissariat à l'énergie atomique et aux énergies */ -/* alternatives) */ -/* */ -/* you can redistribute it and/or modify it under the terms of the GNU */ -/* Lesser General Public License as published by the Free Software */ -/* Foundation, version 2.1. */ -/* */ -/* It is distributed in the hope that it will be useful, */ -/* but WITHOUT ANY WARRANTY; without even the implied warranty of */ -/* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the */ -/* GNU Lesser General Public License for more details. */ -/* */ -/* See the GNU Lesser General Public License version 2.1 */ -/* for more details (enclosed in the file licenses/LGPLv2.1). */ -/* */ -/* ************************************************************************ */ - -import React from 'react'; -import * as Ivette from 'ivette'; -import * as Dome from 'dome/dome'; -import * as States from 'frama-c/states'; -import * as Server from 'frama-c/server'; -import * as Ast from 'frama-c/kernel/api/ast'; -import * as Values from 'frama-c/plugins/eva/api/values'; - -import { classes } from 'dome/misc/utils'; -import { Icon } from 'dome/controls/icons'; -import { Cell, Code } from 'dome/controls/labels'; -import { IconButton } from 'dome/controls/buttons'; -import { Filler, Hpack, Vpack, Vfill } from 'dome/layout/boxes'; -import { Inset, Button, ButtonGroup } from 'dome/frame/toolbars'; - - - -type Request<A, B> = (a: A) => Promise<B>; -type StateToDisplay = 'Before' | 'After' | 'Both' | 'None' -type callstack = 'Summary' | Values.callstack - -function useCallstacksCache(): Request<Ast.marker[], callstack[]> { - const get = React.useCallback((markers) => { - return Server.send(Values.getCallstacks, markers); - }, []); - const toString = React.useCallback((markers: Ast.marker[]) => { - return markers.map((m) => `${m}`).join('|'); - }, []); - return Dome.useCache(get, toString); -} - -type Alarm = [ 'True' | 'False' | 'Unknown', string ] -function getAlarmStatus(alarms: Alarm[]): string { - if (alarms.length === 0) return 'none'; - if (alarms.find(([st, _]) => st === 'False')) return 'False'; - else return 'Unknown'; -} - -type MarkerTracked = [ 'Tracked', boolean ] -type MarkerPinned = [ 'Pinned' , boolean ] -type MarkerStatus = MarkerTracked | MarkerPinned | 'JustFocused' - -function MarkerStatusClass(status: MarkerStatus): string { - if (status === 'JustFocused') return 'eva-header-just-focused'; - const [ kind, focused ] = status; - return 'eva-header-' + kind.toLowerCase() + (focused ? '-focused' : ''); -} - -function isPinnedMarker(status: MarkerStatus): boolean { - if (status === 'JustFocused') return false; - const [ kind ] = status; - return kind === 'Pinned'; -} - - - -interface Callsite { - callee: string; - caller?: string; - stmt?: Ast.marker; -} - -function useCallsitesCache(): Request<callstack, Callsite[]> { - const get = React.useCallback((c) => { - if (c !== 'Summary') return Server.send(Values.getCallstackInfo, c); - else return Promise.resolve([]); - }, []); - return Dome.useCache(get); -} - -interface CallsiteCellProps { - callstack: callstack | 'Header'; - getCallsites: Request<callstack, Callsite[]>; - selectedClass?: string; -} - -function makeStackTitle(calls: Callsite[]): string { - const cs = calls.slice(1); - if (cs.length > 0) - return `Callstack: ${cs.map((c) => c.callee).join(' \u2190 ')}`; - return 'Callstack Details'; -} - -async function CallsiteCell(props: CallsiteCellProps): Promise<JSX.Element> { - const { callstack: c, getCallsites, selectedClass = '' } = props; - const activeClass = 'eva-table-callsite-active'; - const callClass = classes('eva-table-callsite', activeClass, selectedClass); - const callsites = c !== 'Header' ? await getCallsites(c) : []; - const infos = - c === 'Header' ? 'Corresponding callstack' : - c === 'Summary' ? 'Summary' : makeStackTitle(callsites); - return ( - <td className={callClass} title={infos}> - {c === 'Header' ? '#' : c === 'Summary' ? '∑' : c} - </td> - ); -} - - - -interface Location { - target: Ast.marker; - fct: string; -} - -interface Evaluation { - errors?: string; - vBefore?: Values.evaluation; - vAfter?: Values.evaluation; - vThen?: Values.evaluation; - vElse?: Values.evaluation; -} - -interface Probe extends Location { - code?: string; - stmt?: Ast.marker; - rank?: number; - effects?: boolean; - condition?: boolean; - evaluate: Request<callstack, Evaluation> -} - -function useProbeCache(): Request<Location, Probe> { - const toString = React.useCallback((l) => `${l.fct}:${l.target}`, []); - const get = React.useCallback(async (loc: Location): Promise<Probe> => { - const infos = await Server.send(Values.getProbeInfo, loc.target); - const evaluate: Request<callstack, Evaluation> = (c) => { - const callstack = c === 'Summary' ? undefined : c as Values.callstack; - return Server.send(Values.getValues, { ...loc, callstack }); - }; - return { ...loc, ...infos, evaluate }; - }, []); - return Dome.useCache(get, toString); -} - - - -interface StmtProps { - stmt?: Ast.marker; - marker?: Ast.marker; - short?: boolean; -} - -function Stmt(props: StmtProps): JSX.Element { - const markersInfo = States.useSyncArray(Ast.markerInfo); - const { stmt, marker, short } = props; - if (!stmt || !marker) return <></>; - const line = markersInfo.getData(marker)?.sloc?.line; - const filename = markersInfo.getData(marker)?.sloc?.base; - const title = markersInfo.getData(stmt)?.descr; - const text = short ? `@L${line}` : `@${filename}:${line}`; - const className = 'dome-text-cell eva-stmt'; - return <span className={className} title={title}>{text}</span>; -} - - - -function AlarmsInfos(probe?: Probe): Request<callstack, JSX.Element> { - return async (c: callstack): Promise<JSX.Element> => { - const evaluation = await probe?.evaluate(c); - const alarms = evaluation?.vBefore?.alarms ?? []; - if (alarms.length <= 0) return <></>; - const renderAlarm = ([status, alarm]: Alarm): JSX.Element => { - const className = `eva-alarm-info eva-alarm-${status}`; - return <Code className={className} icon="WARNING">{alarm}</Code>; - }; - const children = React.Children.toArray(alarms.map(renderAlarm)); - return <Vpack className="eva-info">{children}</Vpack>; - }; -} - - - -interface StackInfosProps { - callsites: Callsite[]; - isSelected: boolean; - setSelection: (a: States.SelectionActions) => void; -} - -async function StackInfos(props: StackInfosProps): Promise<JSX.Element> { - const { callsites, setSelection, isSelected } = props; - const selectedClass = isSelected ? 'eva-table-selected-row' : ''; - const className = classes('eva-callsite', selectedClass); - if (callsites.length <= 1) return <></>; - const makeCallsite = ({ caller, stmt }: Callsite): JSX.Element => { - if (!caller || !stmt) return <></>; - const key = `${caller}@${stmt}`; - const location = { fct: caller, marker: stmt }; - const select = (meta: boolean): void => { - setSelection({ location }); - if (meta) States.MetaSelection.emit(location); - }; - const onClick = (evt: React.MouseEvent): void => { select(evt.altKey); }; - const onDoubleClick = (evt: React.MouseEvent): void => { - evt.preventDefault(); - select(true); - }; - return ( - <Cell - key={key} - icon='TRIANGLE.LEFT' - className={className} - onClick={onClick} - onDoubleClick={onDoubleClick} - > - {caller} - <Stmt stmt={stmt} marker={stmt} /> - </Cell> - ); - }; - const children = React.Children.toArray(callsites.map(makeCallsite)); - return <Hpack className="eva-info">{children}</Hpack>; -} - - - -interface ProbeInfosProps { - probe?: Probe; - status?: MarkerStatus; - removeProbe: (probe: Probe) => void; - setLocPin: (loc: Location, pin: boolean) => void; - state: StateToDisplay; - setState: (state: StateToDisplay) => void; -} - -function SelectedProbeInfos(props: ProbeInfosProps): JSX.Element { - const { probe, status, setLocPin, removeProbe, state, setState } = props; - const code = probe?.code; - const stmt = probe?.stmt; - const target = probe?.target; - const visible = code !== undefined; - const pinned = status ? isPinnedMarker(status) : false; - return ( - <Hpack className="eva-probeinfo"> - <div - className="eva-probeinfo-code" - style={{ visibility: visible ? 'visible' : 'hidden' }} - > - <div className='eva-sized-area dome-text-cell'>{code}</div> - </div> - <Code><Stmt stmt={stmt} marker={target} /></Code> - <IconButton - icon='PIN' - className="eva-probeinfo-button" - title='Pin the probe' - selected={pinned} - visible={visible} - onClick={() => { if (probe) setLocPin(probe, !pinned); }} - /> - <IconButton - icon="CIRC.CLOSE" - className="eva-probeinfo-button" - title="Discard the probe" - onClick={() => { if (probe) removeProbe(probe); }} - visible={visible} - /> - <Filler /> - <ButtonGroup className='eva-probeinfo-state'> - <Button - label='B' - value='Before' - selected={state === 'Before' || state === 'Both'} - title='Show values before statement effects' - visible={visible} - onClick={() => { - if (state === 'Before') setState('None'); - else if (state === 'After') setState('Both'); - else if (state === 'None') setState('Before'); - else if (state === 'Both') setState('After'); - }} - /> - <Button - label='A' - value='After' - selected={state === 'After' || state === 'Both'} - title='Show values after statement effects' - visible={visible} - onClick={() => { - if (state === 'Before') setState('Both'); - else if (state === 'After') setState('None'); - else if (state === 'None') setState('After'); - else if (state === 'Both') setState('Before'); - }} - /> - </ButtonGroup> - </Hpack> - ); -} - - - -interface ProbeHeaderProps { - probe: Probe; - status: MarkerStatus; - state: StateToDisplay; - pinProbe: (pin: boolean) => void; - selectProbe: () => void; - removeProbe: () => void; - setSelection: (a: States.SelectionActions) => void; -} - -async function ProbeHeader(props: ProbeHeaderProps): Promise<JSX.Element> { - const { probe, status, state, setSelection } = props; - const { code = '(error)', stmt, target, fct } = probe; - const color = MarkerStatusClass(status); - const { selectProbe, removeProbe, pinProbe } = props; - - // Computing the number of columns. By design, either vAfter or vThen and - // vElse are empty. Also by design (hypothesis), it is not function of the - // considered callstacks, so we check on the consolidated. - const evaluation = await probe.evaluate('Summary'); - const { vBefore, vAfter, vThen, vElse } = evaluation; - let span = 0; - if ((state === 'Before' || state === 'Both') && vBefore) span += 1; - if ((state === 'After' || state === 'Both') && vAfter) span += 1; - if ((state === 'After' || state === 'Both') && vThen && vElse) span += 2; - if (span === 0) return <></>; - - const loc: States.SelectionActions = { location: { fct, marker: target} }; - const onClick = (): void => { setSelection(loc); selectProbe(); }; - const onDoubleClick = (): void => pinProbe(!isPinnedMarker(status)); - const onContextMenu = (): void => { - const items: Dome.PopupMenuItem[] = []; - const removeLabel = `Remove column for ${code}`; - items.push({ label: removeLabel, onClick: removeProbe }); - Dome.popupMenu(items); - }; - - return ( - <th - className={color} - colSpan={span} - onClick={onClick} - onDoubleClick={onDoubleClick} - onContextMenu={onContextMenu} - > - <span className='dome-text-cell'>{code}</span> - <Stmt stmt={stmt} marker={target} short={true}/> - </th> - ); -} - - - -interface ProbeValuesProps { - probe: Probe; - status: MarkerStatus; - state: StateToDisplay; - addLoc: (loc: Location) => void; - selectedClass?: string; -} - -function ProbeValues(props: ProbeValuesProps): Request<callstack, JSX.Element> { - const { probe, state, selectedClass = '', addLoc } = props; - const className = classes('eva-table-values', selectedClass); - - // Building common parts - const onContextMenu = (evaluation: Values.evaluation) => (): void => { - const { value, pointedVars } = evaluation; - const items: Dome.PopupMenuItem[] = []; - const copy = (): void => { navigator.clipboard.writeText(value); }; - if (value !== '') items.push({ label: 'Copy to clipboard', onClick: copy }); - if (items.length > 0 && pointedVars.length > 0) items.push('separator'); - pointedVars.forEach((lval) => { - const [text, lvalMarker] = lval; - const label = `Display values for ${text}`; - const location = { fct: probe.fct, target: lvalMarker }; - const onItemClick = (): void => addLoc(location); - items.push({ label, onClick: onItemClick }); - }); - if (items.length > 0) Dome.popupMenu(items); - }; - - return async (callstack: callstack): Promise<JSX.Element> => { - const evaluation = await probe.evaluate(callstack); - const { vBefore, vAfter, vThen, vElse } = evaluation; - function td(e: Values.evaluation, state: string): JSX.Element { - const status = getAlarmStatus(e.alarms); - const alarmClass = `eva-alarms eva-alarm-${status}`; - const kind = callstack === 'Summary' ? 'one' : 'this'; - const title = `At least one alarm is raised in ${kind} callstack`; - return ( - <td - className={className} - onContextMenu={onContextMenu(e)} - > - <div style={{ position: 'relative' }}> - <span className={`eva-state-${state}`}>{e.value}</span> - <Icon className={alarmClass} size={10} title={title} id="WARNING" /> - </div> - </td> - ); - } - if (state === 'Before' && vBefore) return td(vBefore, 'Before'); - if (state === 'After' && vAfter) return td(vAfter, 'After'); - if (state === 'After' && vThen && vElse) - return <>{td(vThen, 'Then')}{td(vElse, 'Else')}</>; - if (state === 'Both' && vBefore && vAfter) - return <>{td(vBefore, 'Before')}{td(vAfter, 'After')}</>; - if (state === 'Both' && vBefore && vThen && vElse) - return <>{td(vBefore, 'Before')}{td(vThen, 'Then')}{td(vElse, 'Else')}</>; - return <></>; - }; -} - - - -interface FunctionProps { - fct: string; - markers: Map<Ast.marker, MarkerStatus>; - state: StateToDisplay; - close: () => void; - getProbe: Request<Location, Probe>; - pinProbe: (probe: Probe, pin: boolean) => void; - selectProbe: (probe: Probe) => void; - removeProbe: (probe: Probe) => void; - addLoc: (loc: Location) => void; - folded: boolean; - setFolded: (folded: boolean) => void; - getCallsites: Request<callstack, Callsite[]>; - byCallstacks: boolean; - getCallstacks: Request<Ast.marker[], callstack[]>; - setByCallstacks: (byCallstack: boolean) => void; - selectCallstack: (callstack: callstack) => void; - isSelectedCallstack: (c: callstack) => boolean; - setSelection: (a: States.SelectionActions) => void; -} - -async function FunctionSection(props: FunctionProps): Promise<JSX.Element> { - const { fct, state, folded, isSelectedCallstack } = props; - const { byCallstacks, setSelection, getCallsites } = props; - const { addLoc, getCallstacks: getCS } = props; - const { setFolded, setByCallstacks, close } = props; - const displayTable = folded ? 'none' : 'table'; - const headerCall = await CallsiteCell({ getCallsites, callstack: 'Header' }); - - /* Compute relevant callstacks */ - const markers: Ast.marker[] = []; - props.markers.forEach((_, m) => markers.push(m)); - const computedCallstacks = byCallstacks ? (await getCS(markers) ?? []) : []; - const callstacks = [ 'Summary' as callstack ].concat(computedCallstacks); - - const probes: [ Promise<Probe>, MarkerStatus ][] = []; - props.markers.forEach(async (status, target) => { - const probe = props.getProbe({ target, fct }); - probes.push([ probe, status ]); - }); - - const headers = await Promise.all(probes.map(async ([ promise, status ]) => { - const probe = await promise; - const pinProbe = (pin: boolean): void => props.pinProbe(probe, pin); - const selectProbe = (): void => props.selectProbe(probe); - const removeProbe = (): void => props.removeProbe(probe); - const fcts = { selectProbe, pinProbe, removeProbe, setSelection }; - return ProbeHeader({ probe, status, state, ...fcts }); - })); - - const values = await Promise.all(callstacks.map(async (callstack) => { - const isSelected = isSelectedCallstack(callstack); - const selector = isSelected && callstack !== 'Summary'; - const selectedClass = selector ? 'eva-table-selected-row' : ''; - const call = await CallsiteCell({ selectedClass, getCallsites, callstack }); - const onClick = (): void => props.selectCallstack(callstack); - const vs = await Promise.all(probes.map(async ([ promise, status ]) => { - const probe = await promise; - const fcts = { addLoc, selectedClass }; - return ProbeValues({ probe, status, state, ...fcts })(callstack); - })); - return ( - <tr key={callstack} onClick={onClick}>{call} - {React.Children.toArray(vs)} - </tr> - ); - })); - - return ( - <div key={fct}> - <Hpack className="eva-function"> - <IconButton - className="eva-fct-fold" - icon={folded ? 'ANGLE.RIGHT' : 'ANGLE.DOWN'} - onClick={() => setFolded(!folded)} - /> - <Cell className="eva-fct-name">{fct}</Cell> - <Filler /> - <IconButton - icon="ITEMS.LIST" - className="eva-probeinfo-button" - selected={byCallstacks} - title="Details by callstack" - onClick={() => setByCallstacks(!byCallstacks)} - /> - <Inset /> - <IconButton - icon="CROSS" - className="eva-probeinfo-button" - title="Close" - onClick={close} - /> - </Hpack> - <div style={{ overflowX: 'auto' }}> - <table className='eva-table' style={{ display: displayTable }}> - <tbody> - <tr> - {headerCall} - {React.Children.toArray(headers)} - </tr> - {React.Children.toArray(values)} - </tbody> - </table> - </div> - </div> - ); -} - - - -class FunctionInfos { - - readonly fct: string; - readonly pinned = new Set<Ast.marker>(); - readonly tracked = new Set<Ast.marker>(); - byCallstacks = false; - folded = false; - - constructor(fct: string) { - this.fct = fct; - } - - has(marker: Ast.marker): boolean { - const pinned = this.pinned.has(marker); - const tracked = this.tracked.has(marker); - return pinned || tracked; - } - - pin(marker: Ast.marker): void { - this.pinned.add(marker); - this.tracked.delete(marker); - } - - track(marker: Ast.marker): void { - this.tracked.add(marker); - this.pinned.delete(marker); - } - - delete(marker: Ast.marker): void { - this.pinned.delete(marker); - this.tracked.delete(marker); - } - - isEmpty(): boolean { - return this.pinned.size === 0 && this.tracked.size === 0; - } - - markers(focusedLoc?: Location): Map<Ast.marker, MarkerStatus> { - const focused = focusedLoc?.target; - const fct = focusedLoc?.fct; - const { pinned, tracked } = this; - const markers = new Map<Ast.marker, MarkerStatus>(); - if (focused && fct && fct === this.fct) { - if (pinned.has(focused)) - markers.set(focused, [ 'Pinned', true ]); - else if (tracked.has(focused)) - markers.set(focused, [ 'Tracked', true ]); - else - markers.set(focused, 'JustFocused'); - } - const add = (marker: Ast.marker, kind: 'Pinned' | 'Tracked'): void => { - if (marker !== focused) markers.set(marker, [ kind, false ]); - }; - pinned.forEach((p) => add(p, 'Pinned')); - tracked.forEach((t) => add(t, 'Tracked')); - return markers; - } - -} - - - -class FunctionsManager { - - private readonly cache = new Map<string, FunctionInfos>(); - - constructor() { - this.newFunction = this.newFunction.bind(this); - this.getInfos = this.getInfos.bind(this); - this.setByCallstacks = this.setByCallstacks.bind(this); - this.setFolded = this.setFolded.bind(this); - this.pin = this.pin.bind(this); - this.track = this.track.bind(this); - this.removeLocation = this.removeLocation.bind(this); - this.delete = this.delete.bind(this); - this.clear = this.clear.bind(this); - this.map = this.map.bind(this); - } - - newFunction(fct: string): void { - if (!this.cache.has(fct)) this.cache.set(fct, new FunctionInfos(fct)); - } - - private getInfos(fct: string): FunctionInfos { - const { cache } = this; - if (cache.has(fct)) return cache.get(fct) as FunctionInfos; - const infos = new FunctionInfos(fct); - this.cache.set(fct, infos); - return infos; - } - - setByCallstacks(fct: string, byCallstacks: boolean): void { - const infos = this.cache.get(fct); - if (!infos) return; - infos.byCallstacks = byCallstacks; - } - - setFolded(fct: string, folded: boolean): void { - const infos = this.cache.get(fct); - if (!infos) return; - infos.folded = folded; - } - - pin(loc: Location): void { - const { target, fct } = loc; - this.getInfos(fct).pin(target); - } - - unpin(loc: Location): void { - const { target, fct } = loc; - this.cache.get(fct)?.pinned.delete(target); - } - - track(loc: Location): void { - const { target, fct } = loc; - this.getInfos(fct).track(target); - } - - status(loc?: Location): MarkerStatus | undefined { - if (!loc) return undefined; - const infos = this.cache.get(loc.fct); - if (infos?.pinned.has(loc.target)) - return [ 'Pinned', true ]; - else if (infos?.tracked.has(loc.target)) - return [ 'Tracked', true ]; - return 'JustFocused'; - } - - removeLocation(loc: Location): void { - const { target, fct } = loc; - const infos = this.cache.get(fct); - if (!infos) return; - infos.delete(target); - } - - delete(fct: string): void { - this.cache.delete(fct); - } - - clear(): void { - this.cache.clear(); - } - - clean(focused?: Location): void { - const focusedFct = focused?.fct; - this.cache.forEach((infos) => { - if (focusedFct !== infos.fct && infos.isEmpty()) - this.cache.delete(infos.fct); - }); - } - - map<A>(func: (infos: FunctionInfos, fct: string) => A): A[] { - const acc: A[] = []; - this.cache.forEach((infos, fct) => acc.push(func(infos, fct))); - return acc; - } - -} - - - -function EvaTable(): JSX.Element { - const [ selection, select ] = States.useSelection(); - const [ state, setState ] = React.useState<StateToDisplay>('Before'); - const [ cs, setCS ] = React.useState<callstack>('Summary'); - const [ fcts ] = React.useState(new FunctionsManager()); - const [ tac, setTic ] = React.useState(false); - - const getProbe = useProbeCache(); - const getCallsites = useCallsitesCache(); - const getCallstacks = useCallstacksCache(); - - const [ focus, setFocus ] = React.useState<Probe | undefined>(undefined); - React.useEffect(() => { - const target = selection?.current?.marker; - const fct = selection?.current?.fct; - const loc = (target && fct) ? { target, fct } : undefined; - const f = (p: Probe): void => { if (fct && p.code) fcts.newFunction(fct); }; - const doUpdate = (p: Probe): void => { f(p) ; setFocus(p); }; - fcts.clean(loc); - if (loc) getProbe(loc).then(doUpdate); - else setFocus(undefined); - }, [ fcts, selection, getProbe, setFocus ]); - - const setLocPin = React.useCallback((loc: Location, pin: boolean): void => { - if (pin) fcts.pin(loc); - else fcts.unpin(loc); - setTic(!tac); - }, [fcts, setTic, tac]); - - const remove = React.useCallback((probe: Probe): void => { - fcts.removeLocation(probe); - if (probe.target === focus?.target) - setFocus(undefined); - fcts.clean(undefined); - setTic(!tac); - }, [ fcts, focus, setFocus, tac ]); - - const functionsPromise = React.useMemo(() => { - const ps = fcts.map((infos, fct) => { - const { byCallstacks, folded } = infos; - const isSelectedCallstack = (c: callstack): boolean => c === cs; - const setFolded = (folded: boolean): void => { - fcts.setFolded(fct, folded); - setTic(!tac); - }; - const setByCS = (byCS: boolean): void => { - fcts.setByCallstacks(fct, byCS); - setTic(!tac); - }; - return { - fct, - markers: infos.markers(focus), - state, - close: () => { fcts.delete(fct); setTic(!tac); }, - pinProbe: setLocPin, - getProbe, - selectProbe: setFocus, - removeProbe: remove, - addLoc: (loc: Location) => { fcts.pin(loc); setTic(!tac); }, - folded, - setFolded, - getCallsites, - byCallstacks, - getCallstacks, - setByCallstacks: setByCS, - selectCallstack: (c: callstack) => { setCS(c); setTic(!tac); }, - isSelectedCallstack, - setSelection: select, - }; - }); - return Promise.all(ps.map(FunctionSection)); - }, - [ cs, fcts, focus, tac, getCallsites, setLocPin, - getCallstacks, getProbe, remove, select, state - ]); - const { result: functions } = Dome.usePromise(functionsPromise); - - const alarmsProm = React.useMemo(() => AlarmsInfos(focus)(cs), [ focus, cs ]); - const { result: alarmsInfos } = Dome.usePromise(alarmsProm); - - const stackInfosPromise = React.useMemo(async () => { - const callsites = await getCallsites(cs); - const tgt = selection.current?.marker; - const p = (c: Callsite): boolean => c.stmt !== undefined && c.stmt === tgt; - const isSelected = callsites.find(p) !== undefined; - return StackInfos({ callsites, isSelected, setSelection: select }); - }, [ cs, select, getCallsites, selection ]); - const { result: stackInfos } = Dome.usePromise(stackInfosPromise); - - return ( - <> - <Ivette.TitleBar /> - <SelectedProbeInfos - probe={focus} - status={fcts.status(focus)} - setLocPin={setLocPin} - removeProbe={remove} - state={state} - setState={setState} - /> - <Vfill style={{ overflowY: 'auto' }}> - {React.Children.toArray(functions)} - </Vfill> - {alarmsInfos} - {stackInfos} - </> - ); -} - - - -Ivette.registerComponent({ - id: 'frama-c.plugins.values', - group: 'frama-c.plugins', - rank: 1, - label: 'Eva Values', - title: 'Values inferred by the Eva analysis', - children: <EvaTable />, -}); - diff --git a/ivette/src/frama-c/plugins/eva/valueinfos.tsx b/ivette/src/frama-c/plugins/eva/valueinfos.tsx deleted file mode 100644 index 28fb0a30249..00000000000 --- a/ivette/src/frama-c/plugins/eva/valueinfos.tsx +++ /dev/null @@ -1,148 +0,0 @@ -/* ************************************************************************ */ -/* */ -/* This file is part of Frama-C. */ -/* */ -/* Copyright (C) 2007-2022 */ -/* CEA (Commissariat à l'énergie atomique et aux énergies */ -/* alternatives) */ -/* */ -/* you can redistribute it and/or modify it under the terms of the GNU */ -/* Lesser General Public License as published by the Free Software */ -/* Foundation, version 2.1. */ -/* */ -/* It is distributed in the hope that it will be useful, */ -/* but WITHOUT ANY WARRANTY; without even the implied warranty of */ -/* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the */ -/* GNU Lesser General Public License for more details. */ -/* */ -/* See the GNU Lesser General Public License version 2.1 */ -/* for more details (enclosed in the file licenses/LGPLv2.1). */ -/* */ -/* ************************************************************************ */ - -/* eslint-disable @typescript-eslint/explicit-function-return-type */ - -// -------------------------------------------------------------------------- -// --- Info Components -// -------------------------------------------------------------------------- - -// React & Dome -import React from 'react'; -import { classes } from 'dome/misc/utils'; -import { Hpack, Vpack } from 'dome/layout/boxes'; -import { Code, Cell } from 'dome/controls/labels'; -import * as States from 'frama-c/states'; -import * as Ast from 'frama-c/kernel/api/ast'; -import { ModelProp } from 'frama-c/plugins/eva/model'; - -// Locals -import { EvaAlarm } from './cells'; -import { Callsite } from './stacks'; - -// -------------------------------------------------------------------------- -// --- Stmt Printer -// -------------------------------------------------------------------------- - -interface StmtProps { - stmt?: Ast.marker; - marker: Ast.marker; - short?: boolean; -} - -export function Stmt(props: StmtProps) { - const markersInfo = States.useSyncArray(Ast.markerInfo); - - const { stmt, marker, short } = props; - if (!stmt) return null; - const line = markersInfo.getData(marker)?.sloc?.line; - const filename = markersInfo.getData(marker)?.sloc?.base; - const title = markersInfo.getData(stmt)?.descr; - const text = short ? `@L${line}` : `@${filename}:${line}`; - return ( - <span className="dome-text-cell eva-stmt" title={title}> - {text} - </span> - ); -} - -// -------------------------------------------------------------------------- -// --- Alarms Panel -// -------------------------------------------------------------------------- - -export function AlarmsInfos(props: ModelProp) { - const { model } = props; - const probe = model.getFocused(); - if (probe) { - const callstack = model.getCallstack(); - const domain = model.values.getValues(probe, callstack); - const alarms = domain?.vBefore.alarms ?? []; - if (alarms.length > 0) { - const renderAlarm = ([status, alarm]: EvaAlarm) => { - const className = `eva-alarm-info eva-alarm-${status}`; - return ( - <Code className={className} icon="WARNING">{alarm}</Code> - ); - }; - return ( - <Vpack className="eva-info"> - {React.Children.toArray(alarms.map(renderAlarm))} - </Vpack> - ); - } - } - return null; -} - -// -------------------------------------------------------------------------- -// --- Stack Panel -// -------------------------------------------------------------------------- - -export function StackInfos(props: ModelProp) { - const { model } = props; - const [, setSelection] = States.useSelection(); - const focused = model.getFocused(); - const callstack = model.getCalls(); - if (callstack.length <= 1) return null; - const makeCallsite = ({ caller, stmt }: Callsite) => { - if (!caller || !stmt) return null; - const key = `${caller}@${stmt}`; - const isFocused = focused?.marker === stmt; - const isTransient = focused?.transient; - const className = classes( - 'eva-callsite', - isFocused && 'eva-focused', - isTransient && 'eva-transient', - ); - const select = (meta: boolean) => { - const location = { fct: caller, marker: stmt }; - setSelection({ location }); - if (meta) States.MetaSelection.emit(location); - }; - const onClick = (evt: React.MouseEvent) => { - select(evt.altKey); - }; - const onDoubleClick = (evt: React.MouseEvent) => { - evt.preventDefault(); - select(true); - }; - return ( - <Cell - key={key} - icon="TRIANGLE.LEFT" - className={className} - onClick={onClick} - onDoubleClick={onDoubleClick} - > - {caller} - <Stmt stmt={stmt} marker={stmt} /> - </Cell> - ); - }; - return ( - <Hpack className="eva-info"> - {callstack.map(makeCallsite)} - </Hpack> - ); -} - -// -------------------------------------------------------------------------- diff --git a/ivette/src/frama-c/plugins/eva/valuetable.tsx b/ivette/src/frama-c/plugins/eva/valuetable.tsx index 3e09f9d2c54..2ec22a8465a 100644 --- a/ivette/src/frama-c/plugins/eva/valuetable.tsx +++ b/ivette/src/frama-c/plugins/eva/valuetable.tsx @@ -20,396 +20,801 @@ /* */ /* ************************************************************************ */ -/* eslint-disable @typescript-eslint/explicit-function-return-type */ - -// -------------------------------------------------------------------------- -// --- Eva Values -// -------------------------------------------------------------------------- - -// React & Dome import React from 'react'; -import * as Dome from 'dome'; +import * as Ivette from 'ivette'; +import * as Dome from 'dome/dome'; +import * as States from 'frama-c/states'; +import * as Server from 'frama-c/server'; +import * as Ast from 'frama-c/kernel/api/ast'; +import * as Values from 'frama-c/plugins/eva/api/values'; + import { classes } from 'dome/misc/utils'; -import { VariableSizeList } from 'react-window'; -import { Hpack, Filler } from 'dome/layout/boxes'; -import { Inset } from 'dome/frame/toolbars'; import { Icon } from 'dome/controls/icons'; -import { Cell } from 'dome/controls/labels'; +import { Cell, Code } from 'dome/controls/labels'; import { IconButton } from 'dome/controls/buttons'; -import { ModelProp, EvalStmt, EvalCond } from 'frama-c/plugins/eva/model'; +import { Filler, Hpack, Vpack, Vfill } from 'dome/layout/boxes'; +import { Inset, Button, ButtonGroup } from 'dome/frame/toolbars'; -// Frama-C -import * as States from 'frama-c/states'; -// Locals -import { SizedArea, HSIZER, WSIZER } from './sized'; -import { Diff } from './diffed'; -import { sizeof, EvaValues, EvaPointedVar, Evaluation } from './cells'; -import { Probe } from './probes'; -import { Row } from './layout'; -import { Callsite } from './stacks'; -import { Stmt } from './valueinfos'; -import './style.css'; - -// -------------------------------------------------------------------------- -// --- Cell Diffs -// -------------------------------------------------------------------------- - -function computeValueDiffs(v: EvaValues, vstate: EvalStmt | EvalCond) { - let here = v.vBefore; - let diff: undefined | Evaluation; - let diff2: undefined | Evaluation; - function setValue(e?: Evaluation) { if (e) { here = e; diff = v.vBefore; } } - switch (vstate) { - case 'Before': diff = v.vAfter; break; - case 'After': setValue(v.vAfter); break; - case 'Then': setValue(v.vThen); break; - case 'Else': setValue(v.vElse); break; - case 'Cond': diff = v.vThen; diff2 = v.vElse; break; - } - const vdiffs = { text: here.value, diff: diff?.value, diff2: diff2?.value }; - return { value: here, vdiffs }; + +type Request<A, B> = (a: A) => Promise<B>; +type StateToDisplay = 'Before' | 'After' | 'Both' | 'None' +type callstack = 'Summary' | Values.callstack + +function useCallstacksCache(): Request<Ast.marker[], callstack[]> { + const get = React.useCallback((markers) => { + return Server.send(Values.getCallstacks, markers); + }, []); + const toString = React.useCallback((markers: Ast.marker[]) => { + return markers.map((m) => `${m}`).join('|'); + }, []); + return Dome.useCache(get, toString); } -// -------------------------------------------------------------------------- -// --- Table Cell -// -------------------------------------------------------------------------- +type Alarm = [ 'True' | 'False' | 'Unknown', string ] +function getAlarmStatus(alarms: Alarm[]): string { + if (alarms.length === 0) return 'none'; + if (alarms.find(([st, _]) => st === 'False')) return 'False'; + else return 'Unknown'; +} -interface TableCellProps extends ModelProp { - probe: Probe; - row: Row; +type MarkerTracked = [ 'Tracked', boolean ] +type MarkerPinned = [ 'Pinned' , boolean ] +type MarkerStatus = MarkerTracked | MarkerPinned | 'JustFocused' + +function MarkerStatusClass(status: MarkerStatus): string { + if (status === 'JustFocused') return 'eva-header-just-focused'; + const [ kind, focused ] = status; + return 'eva-header-' + kind.toLowerCase() + (focused ? '-focused' : ''); } -const CELLPADDING = 12; - -function TableCell(props: TableCellProps) { - const { probe, row, model } = props; - const [, setSelection] = States.useSelection(); - 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; - let valueText = ''; - let pointedVars: EvaPointedVar[] = []; - const { transient, marker } = probe; - const focused = model.getFocused(); - const isFocused = focused === probe; - - switch (kind) { - - // ---- Probe Contents - case 'probes': - { - const { stmt, code } = probe; - contents = ( - <> - <span className='dome-text-cell'>{code}</span> - <Stmt stmt={stmt} marker={marker} short /> - </> - ); - } - break; - - // ---- Values Contents - case 'values': - case 'callstack': - { - const domain = model.values.getValues(probe, callstack); - const { condition } = probe; - const vstate = condition ? model.getVcond() : model.getVstmt(); - const { value, vdiffs } = computeValueDiffs(domain, vstate); - valueText = value.value; - const text = vdiffs.text ?? vdiffs.diff; - const { cols, rows } = sizeof(text); - let status = 'none'; - if (value.alarms.length > 0) { - if (value.alarms.find(([st, _]) => st === 'False')) status = 'False'; - else status = 'Unknown'; - } - if (value.pointedVars.length > 0) - pointedVars = value.pointedVars; - const alarmClass = `eva-cell-alarms eva-alarm-${status}`; - const title = 'At least one alarm is raised in one callstack'; - contents = ( - <> - <Icon className={alarmClass} size={10} title={title} id="WARNING" /> - <SizedArea cols={cols} rows={rows}> - <span className={`eva-state-${vstate}`}> - <Diff {...vdiffs} /> - </span> - </SizedArea> - </> - ); - } - break; +function isPinnedMarker(status: MarkerStatus): boolean { + if (status === 'JustFocused') return false; + const [ kind ] = status; + return kind === 'Pinned'; +} - } - // --- Cell Packing - const className = classes( - 'eva-cell', - transient && 'eva-transient', - isFocused && 'eva-focused', - ); - const onClick = () => { - const location = { fct: probe.fct, marker: probe.marker }; - setSelection({ location }); - model.setSelectedRow(row); - }; - const onDoubleClick = () => { - probe.setPersistent(); - if (probe.zoomable) probe.setZoomed(!probe.zoomed); - }; - async function onContextMenu() { - const items: Dome.PopupMenuItem[] = []; - const copyValue = () => navigator.clipboard.writeText(valueText); - if (valueText !== '') - items.push({ label: 'Copy to clipboard', onClick: copyValue }); - if (items.length > 0 && pointedVars.length > 0) - items.push('separator'); - pointedVars.forEach((lval) => { - const [text, lvalMarker] = lval; - const label = `Display values for ${text}`; - const location = { fct: probe.fct, marker: lvalMarker }; - const onItemClick = () => model.addProbe(location); - items.push({ label, onClick: onItemClick }); - }); - if (items.length > 0) - items.push('separator'); - const remove = () => model.removeProbe(probe); - const removeLabel = `Remove column for ${probe.code}`; - items.push({ label: removeLabel, onClick: remove }); - if (items.length > 0) Dome.popupMenu(items); - } +interface Callsite { + callee: string; + caller?: string; + stmt?: Ast.marker; +} +function useCallsitesCache(): Request<callstack, Callsite[]> { + const get = React.useCallback((c) => { + if (c !== 'Summary') return Server.send(Values.getCallstackInfo, c); + else return Promise.resolve([]); + }, []); + return Dome.useCache(get); +} + +interface CallsiteCellProps { + callstack: callstack | 'Header'; + getCallsites: Request<callstack, Callsite[]>; + selectedClass?: string; +} + +function makeStackTitle(calls: Callsite[]): string { + const cs = calls.slice(1); + if (cs.length > 0) + return `Callstack: ${cs.map((c) => c.callee).join(' \u2190 ')}`; + return 'Callstack Details'; +} + +async function CallsiteCell(props: CallsiteCellProps): Promise<JSX.Element> { + const { callstack: c, getCallsites, selectedClass = '' } = props; + const activeClass = 'eva-table-callsite-active'; + const callClass = classes('eva-table-callsite', activeClass, selectedClass); + const callsites = c !== 'Header' ? await getCallsites(c) : []; + const infos = + c === 'Header' ? 'Corresponding callstack' : + c === 'Summary' ? 'Summary' : makeStackTitle(callsites); return ( - <div - className={className} - style={style} - onClick={onClick} - onDoubleClick={onDoubleClick} - onContextMenu={onContextMenu} - > - {contents} - </div> + <td className={callClass} title={infos}> + {c === 'Header' ? '#' : c === 'Summary' ? '∑' : c} + </td> ); } -// -------------------------------------------------------------------------- -// --- Table Section -// -------------------------------------------------------------------------- -interface TableSectionProps { + +interface Location { + target: Ast.marker; fct: string; - folded: boolean; - foldable: boolean; - onClick: () => void; - byCallstacks: boolean; - onCallstackClick: () => void; - close: () => void; } -function TableSection(props: TableSectionProps) { - const { fct, foldable, folded, onClick } = props; - const icon = folded ? 'ANGLE.RIGHT' : - foldable ? 'ANGLE.DOWN' : 'TRIANGLE.RIGHT'; - return ( - <> - <IconButton - className="eva-fct-fold" - size={10} - offset={-1} - icon={icon} - enabled={foldable} +interface Evaluation { + errors?: string; + vBefore?: Values.evaluation; + vAfter?: Values.evaluation; + vThen?: Values.evaluation; + vElse?: Values.evaluation; +} + +interface Probe extends Location { + code?: string; + stmt?: Ast.marker; + rank?: number; + effects?: boolean; + condition?: boolean; + evaluate: Request<callstack, Evaluation> +} + +function useProbeCache(): Request<Location, Probe> { + const toString = React.useCallback((l) => `${l.fct}:${l.target}`, []); + const get = React.useCallback(async (loc: Location): Promise<Probe> => { + const infos = await Server.send(Values.getProbeInfo, loc.target); + const evaluate: Request<callstack, Evaluation> = (c) => { + const callstack = c === 'Summary' ? undefined : c as Values.callstack; + return Server.send(Values.getValues, { ...loc, callstack }); + }; + return { ...loc, ...infos, evaluate }; + }, []); + return Dome.useCache(get, toString); +} + + + +interface StmtProps { + stmt?: Ast.marker; + marker?: Ast.marker; + short?: boolean; +} + +function Stmt(props: StmtProps): JSX.Element { + const markersInfo = States.useSyncArray(Ast.markerInfo); + const { stmt, marker, short } = props; + if (!stmt || !marker) return <></>; + const line = markersInfo.getData(marker)?.sloc?.line; + const filename = markersInfo.getData(marker)?.sloc?.base; + const title = markersInfo.getData(stmt)?.descr; + const text = short ? `@L${line}` : `@${filename}:${line}`; + const className = 'dome-text-cell eva-stmt'; + return <span className={className} title={title}>{text}</span>; +} + + + +function AlarmsInfos(probe?: Probe): Request<callstack, JSX.Element> { + return async (c: callstack): Promise<JSX.Element> => { + const evaluation = await probe?.evaluate(c); + const alarms = evaluation?.vBefore?.alarms ?? []; + if (alarms.length <= 0) return <></>; + const renderAlarm = ([status, alarm]: Alarm): JSX.Element => { + const className = `eva-alarm-info eva-alarm-${status}`; + return <Code className={className} icon="WARNING">{alarm}</Code>; + }; + const children = React.Children.toArray(alarms.map(renderAlarm)); + return <Vpack className="eva-info">{children}</Vpack>; + }; +} + + + +interface StackInfosProps { + callsites: Callsite[]; + isSelected: boolean; + setSelection: (a: States.SelectionActions) => void; +} + +async function StackInfos(props: StackInfosProps): Promise<JSX.Element> { + const { callsites, setSelection, isSelected } = props; + const selectedClass = isSelected ? 'eva-table-selected-row' : ''; + const className = classes('eva-callsite', selectedClass); + if (callsites.length <= 1) return <></>; + const makeCallsite = ({ caller, stmt }: Callsite): JSX.Element => { + if (!caller || !stmt) return <></>; + const key = `${caller}@${stmt}`; + const location = { fct: caller, marker: stmt }; + const select = (meta: boolean): void => { + setSelection({ location }); + if (meta) States.MetaSelection.emit(location); + }; + const onClick = (evt: React.MouseEvent): void => { select(evt.altKey); }; + const onDoubleClick = (evt: React.MouseEvent): void => { + evt.preventDefault(); + select(true); + }; + return ( + <Cell + key={key} + icon='TRIANGLE.LEFT' + className={className} onClick={onClick} - /> - <Cell className="eva-fct-name">{fct}</Cell> - <Filler /> + onDoubleClick={onDoubleClick} + > + {caller} + <Stmt stmt={stmt} marker={stmt} /> + </Cell> + ); + }; + const children = React.Children.toArray(callsites.map(makeCallsite)); + return <Hpack className="eva-info">{children}</Hpack>; +} + + + +interface ProbeInfosProps { + probe?: Probe; + status?: MarkerStatus; + removeProbe: (probe: Probe) => void; + setLocPin: (loc: Location, pin: boolean) => void; + state: StateToDisplay; + setState: (state: StateToDisplay) => void; +} + +function SelectedProbeInfos(props: ProbeInfosProps): JSX.Element { + const { probe, status, setLocPin, removeProbe, state, setState } = props; + const code = probe?.code; + const stmt = probe?.stmt; + const target = probe?.target; + const visible = code !== undefined; + const pinned = status ? isPinnedMarker(status) : false; + return ( + <Hpack className="eva-probeinfo"> + <div + className="eva-probeinfo-code" + style={{ visibility: visible ? 'visible' : 'hidden' }} + > + <div className='eva-sized-area dome-text-cell'>{code}</div> + </div> + <Code><Stmt stmt={stmt} marker={target} /></Code> <IconButton - icon="ITEMS.LIST" + icon='PIN' className="eva-probeinfo-button" - selected={props.byCallstacks} - title="Details by callstack" - onClick={props.onCallstackClick} + title='Pin the probe' + selected={pinned} + visible={visible} + onClick={() => { if (probe) setLocPin(probe, !pinned); }} /> - <Inset /> <IconButton - icon="CROSS" + icon="CIRC.CLOSE" className="eva-probeinfo-button" - title="Close" - onClick={props.close} + title="Discard the probe" + onClick={() => { if (probe) removeProbe(probe); }} + visible={visible} /> - </> + <Filler /> + <ButtonGroup className='eva-probeinfo-state'> + <Button + label='B' + value='Before' + selected={state === 'Before' || state === 'Both'} + title='Show values before statement effects' + visible={visible} + onClick={() => { + if (state === 'Before') setState('None'); + else if (state === 'After') setState('Both'); + else if (state === 'None') setState('Before'); + else if (state === 'Both') setState('After'); + }} + /> + <Button + label='A' + value='After' + selected={state === 'After' || state === 'Both'} + title='Show values after statement effects' + visible={visible} + onClick={() => { + if (state === 'Before') setState('Both'); + else if (state === 'After') setState('None'); + else if (state === 'None') setState('After'); + else if (state === 'Both') setState('Before'); + }} + /> + </ButtonGroup> + </Hpack> ); } -// -------------------------------------------------------------------------- -// --- Table Row Header -// -------------------------------------------------------------------------- -interface TableHeadProps { - stackCalls: Callsite[]; - stackIndex: number | undefined; - stackCount: number | undefined; - onClick: () => void; -} -function makeStackTitle(calls: Callsite[]) { - const cs = calls.slice(1); - if (cs.length > 0) - return `Callstack: ${cs.map((c) => c.callee).join(' \u2190 ')}`; - return 'Callstack Details'; +interface ProbeHeaderProps { + probe: Probe; + status: MarkerStatus; + state: StateToDisplay; + pinProbe: (pin: boolean) => void; + selectProbe: () => void; + removeProbe: () => void; + setSelection: (a: States.SelectionActions) => void; } -function TableHead(props: TableHeadProps) { - const sk = props.stackIndex; - const sc = props.stackCount; - const hdClass = classes('eva-head', sc ? undefined : 'dome-hidden'); - const hdHeader = sk === undefined; - const hdSummary = sk !== undefined && sk < 0; - const hdNumber = sk === undefined ? 0 : 1 + sk; - const hdTitle = - hdHeader ? 'Callstack / Summary' : - hdSummary ? 'Summary' : makeStackTitle(props.stackCalls); +async function ProbeHeader(props: ProbeHeaderProps): Promise<JSX.Element> { + const { probe, status, state, setSelection } = props; + const { code = '(error)', stmt, target, fct } = probe; + const color = MarkerStatusClass(status); + const { selectProbe, removeProbe, pinProbe } = props; + + // Computing the number of columns. By design, either vAfter or vThen and + // vElse are empty. Also by design (hypothesis), it is not function of the + // considered callstacks, so we check on the consolidated. + const evaluation = await probe.evaluate('Summary'); + const { vBefore, vAfter, vThen, vElse } = evaluation; + let span = 0; + if ((state === 'Before' || state === 'Both') && vBefore) span += 1; + if ((state === 'After' || state === 'Both') && vAfter) span += 1; + if ((state === 'After' || state === 'Both') && vThen && vElse) span += 2; + if (span === 0) return <></>; + + const loc: States.SelectionActions = { location: { fct, marker: target} }; + const onClick = (): void => { setSelection(loc); selectProbe(); }; + const onDoubleClick = (): void => pinProbe(!isPinnedMarker(status)); + const onContextMenu = (): void => { + const items: Dome.PopupMenuItem[] = []; + const removeLabel = `Remove column for ${code}`; + items.push({ label: removeLabel, onClick: removeProbe }); + Dome.popupMenu(items); + }; + return ( - <div - className={hdClass} - title={hdTitle} - onClick={props.onClick} + <th + className={color} + colSpan={span} + onClick={onClick} + onDoubleClick={onDoubleClick} + onContextMenu={onContextMenu} > - <div className="eva-phantom">{'\u2211'}{sc ?? '#'}</div> - {hdHeader ? '#' : hdSummary ? '\u2211' : `${hdNumber}`} - </div> + <span className='dome-text-cell'>{code}</span> + <Stmt stmt={stmt} marker={target} short={true}/> + </th> ); } -// -------------------------------------------------------------------------- -// --- Table Row -// -------------------------------------------------------------------------- -interface TableRowProps { - style: React.CSSProperties; - index: number; - data: ModelProp; + +interface ProbeValuesProps { + probe: Probe; + status: MarkerStatus; + state: StateToDisplay; + addLoc: (loc: Location) => void; + selectedClass?: string; } -function TableRow(props: TableRowProps) { - const { model } = props.data; - const row = model.getRow(props.index); - if (!row) return null; - const { kind, probes } = row; - if (kind === 'section') { - const { fct } = row; - if (!fct) return null; - const folded = model.isFolded(fct); - const foldable = model.isFoldable(fct); - const byCallstacks = model.isByCallstacks(fct); +function ProbeValues(props: ProbeValuesProps): Request<callstack, JSX.Element> { + const { probe, state, selectedClass = '', addLoc } = props; + const className = classes('eva-table-values', selectedClass); + + // Building common parts + const onContextMenu = (evaluation: Values.evaluation) => (): void => { + const { value, pointedVars } = evaluation; + const items: Dome.PopupMenuItem[] = []; + const copy = (): void => { navigator.clipboard.writeText(value); }; + if (value !== '') items.push({ label: 'Copy to clipboard', onClick: copy }); + if (items.length > 0 && pointedVars.length > 0) items.push('separator'); + pointedVars.forEach((lval) => { + const [text, lvalMarker] = lval; + const label = `Display values for ${text}`; + const location = { fct: probe.fct, target: lvalMarker }; + const onItemClick = (): void => addLoc(location); + items.push({ label, onClick: onItemClick }); + }); + if (items.length > 0) Dome.popupMenu(items); + }; + + return async (callstack: callstack): Promise<JSX.Element> => { + const evaluation = await probe.evaluate(callstack); + const { vBefore, vAfter, vThen, vElse } = evaluation; + function td(e: Values.evaluation, state: string): JSX.Element { + const status = getAlarmStatus(e.alarms); + const alarmClass = `eva-alarms eva-alarm-${status}`; + const kind = callstack === 'Summary' ? 'one' : 'this'; + const title = `At least one alarm is raised in ${kind} callstack`; + return ( + <td + className={className} + onContextMenu={onContextMenu(e)} + > + <div style={{ position: 'relative' }}> + <span className={`eva-state-${state}`}>{e.value}</span> + <Icon className={alarmClass} size={10} title={title} id="WARNING" /> + </div> + </td> + ); + } + if (state === 'Before' && vBefore) return td(vBefore, 'Before'); + if (state === 'After' && vAfter) return td(vAfter, 'After'); + if (state === 'After' && vThen && vElse) + return <>{td(vThen, 'Then')}{td(vElse, 'Else')}</>; + if (state === 'Both' && vBefore && vAfter) + return <>{td(vBefore, 'Before')}{td(vAfter, 'After')}</>; + if (state === 'Both' && vBefore && vThen && vElse) + return <>{td(vBefore, 'Before')}{td(vThen, 'Then')}{td(vElse, 'Else')}</>; + return <></>; + }; +} + + + +interface FunctionProps { + fct: string; + markers: Map<Ast.marker, MarkerStatus>; + state: StateToDisplay; + close: () => void; + getProbe: Request<Location, Probe>; + pinProbe: (probe: Probe, pin: boolean) => void; + selectProbe: (probe: Probe) => void; + removeProbe: (probe: Probe) => void; + addLoc: (loc: Location) => void; + folded: boolean; + setFolded: (folded: boolean) => void; + getCallsites: Request<callstack, Callsite[]>; + byCallstacks: boolean; + getCallstacks: Request<Ast.marker[], callstack[]>; + setByCallstacks: (byCallstack: boolean) => void; + selectCallstack: (callstack: callstack) => void; + isSelectedCallstack: (c: callstack) => boolean; + setSelection: (a: States.SelectionActions) => void; +} + +async function FunctionSection(props: FunctionProps): Promise<JSX.Element> { + const { fct, state, folded, isSelectedCallstack } = props; + const { byCallstacks, setSelection, getCallsites } = props; + const { addLoc, getCallstacks: getCS } = props; + const { setFolded, setByCallstacks, close } = props; + const displayTable = folded ? 'none' : 'table'; + const headerCall = await CallsiteCell({ getCallsites, callstack: 'Header' }); + + /* Compute relevant callstacks */ + const markers: Ast.marker[] = []; + props.markers.forEach((_, m) => markers.push(m)); + const computedCallstacks = byCallstacks ? (await getCS(markers) ?? []) : []; + const callstacks = [ 'Summary' as callstack ].concat(computedCallstacks); + + const probes: [ Promise<Probe>, MarkerStatus ][] = []; + props.markers.forEach(async (status, target) => { + const probe = props.getProbe({ target, fct }); + probes.push([ probe, status ]); + }); + + const headers = await Promise.all(probes.map(async ([ promise, status ]) => { + const probe = await promise; + const pinProbe = (pin: boolean): void => props.pinProbe(probe, pin); + const selectProbe = (): void => props.selectProbe(probe); + const removeProbe = (): void => props.removeProbe(probe); + const fcts = { selectProbe, pinProbe, removeProbe, setSelection }; + return ProbeHeader({ probe, status, state, ...fcts }); + })); + + const values = await Promise.all(callstacks.map(async (callstack) => { + const isSelected = isSelectedCallstack(callstack); + const selector = isSelected && callstack !== 'Summary'; + const selectedClass = selector ? 'eva-table-selected-row' : ''; + const call = await CallsiteCell({ selectedClass, getCallsites, callstack }); + const onClick = (): void => props.selectCallstack(callstack); + const vs = await Promise.all(probes.map(async ([ promise, status ]) => { + const probe = await promise; + const fcts = { addLoc, selectedClass }; + return ProbeValues({ probe, status, state, ...fcts })(callstack); + })); return ( - <Hpack className="eva-function" style={props.style}> - <TableSection - fct={fct} - folded={folded} - foldable={foldable} - onClick={() => model.setFolded(fct, !folded)} - byCallstacks={byCallstacks} - onCallstackClick={() => model.setByCallstacks(fct, !byCallstacks)} - close={() => model.clearFunction(fct)} - /> - </Hpack> + <tr key={callstack} onClick={onClick}>{call} + {React.Children.toArray(vs)} + </tr> ); - } - const sk = row.stackIndex; - const sc = row.stackCount; - const cs = row.callstack; - const calls = cs ? model.stacks.getCalls(cs) : []; - const rowKind = `eva-${kind}`; - const rowParity = sk !== undefined && sk % 2 === 1; - const rowIndexKind = - model.isSelectedRow(row) ? 'eva-row-selected' : - model.isAlignedRow(row) ? 'eva-row-aligned' : - rowParity ? 'eva-row-odd' : 'eva-row-even'; - const rowClass = classes('eva-row', rowKind, rowIndexKind); - const onHeaderClick = () => model.setSelectedRow(row); - const makeCell = (probe: Probe) => ( - <TableCell - key={probe.marker} - probe={probe} - row={row} - model={model} - /> - ); + })); + return ( - <Hpack style={props.style}> - <div className={rowClass}> - <TableHead - stackIndex={sk} - stackCount={sc} - stackCalls={calls} - onClick={onHeaderClick} + <div key={fct}> + <Hpack className="eva-function"> + <IconButton + className="eva-fct-fold" + icon={folded ? 'ANGLE.RIGHT' : 'ANGLE.DOWN'} + onClick={() => setFolded(!folded)} + /> + <Cell className="eva-fct-name">{fct}</Cell> + <Filler /> + <IconButton + icon="ITEMS.LIST" + className="eva-probeinfo-button" + selected={byCallstacks} + title="Details by callstack" + onClick={() => setByCallstacks(!byCallstacks)} + /> + <Inset /> + <IconButton + icon="CROSS" + className="eva-probeinfo-button" + title="Close" + onClick={close} /> - {probes.map(makeCell)} + </Hpack> + <div style={{ overflowX: 'auto' }}> + <table className='eva-table' style={{ display: displayTable }}> + <tbody> + <tr> + {headerCall} + {React.Children.toArray(headers)} + </tr> + {React.Children.toArray(values)} + </tbody> + </table> </div> - <Filler /> - </Hpack> + </div> ); } -// -------------------------------------------------------------------------- -// --- Values Panel -// -------------------------------------------------------------------------- -export interface Dimension { - width: number; - height: number; -} -export interface ValuesPanelProps extends Dimension, ModelProp { - zoom: number; +class FunctionInfos { + + readonly fct: string; + readonly pinned = new Set<Ast.marker>(); + readonly tracked = new Set<Ast.marker>(); + byCallstacks = false; + folded = false; + + constructor(fct: string) { + this.fct = fct; + } + + has(marker: Ast.marker): boolean { + const pinned = this.pinned.has(marker); + const tracked = this.tracked.has(marker); + return pinned || tracked; + } + + pin(marker: Ast.marker): void { + this.pinned.add(marker); + this.tracked.delete(marker); + } + + track(marker: Ast.marker): void { + this.tracked.add(marker); + this.pinned.delete(marker); + } + + delete(marker: Ast.marker): void { + this.pinned.delete(marker); + this.tracked.delete(marker); + } + + isEmpty(): boolean { + return this.pinned.size === 0 && this.tracked.size === 0; + } + + markers(focusedLoc?: Location): Map<Ast.marker, MarkerStatus> { + const focused = focusedLoc?.target; + const fct = focusedLoc?.fct; + const { pinned, tracked } = this; + const markers = new Map<Ast.marker, MarkerStatus>(); + if (focused && fct && fct === this.fct) { + if (pinned.has(focused)) + markers.set(focused, [ 'Pinned', true ]); + else if (tracked.has(focused)) + markers.set(focused, [ 'Tracked', true ]); + else + markers.set(focused, 'JustFocused'); + } + const add = (marker: Ast.marker, kind: 'Pinned' | 'Tracked'): void => { + if (marker !== focused) markers.set(marker, [ kind, false ]); + }; + pinned.forEach((p) => add(p, 'Pinned')); + tracked.forEach((t) => add(t, 'Tracked')); + return markers; + } + } -export function ValuesPanel(props: ValuesPanelProps) { - const { zoom, width, height, model } = props; - // --- reset line cache - const listRef = React.useRef<VariableSizeList>(null); - const [rowCount, setRowCount] = React.useState(model.getRowCount()); - Dome.useEvent(model.laidout, () => { - // The layout has changed, so the number of rows may also have changed. - setRowCount(model.getRowCount()); - setImmediate(() => { - const vlist = listRef.current; - if (vlist) vlist.resetAfterIndex(0, true); + + +class FunctionsManager { + + private readonly cache = new Map<string, FunctionInfos>(); + + constructor() { + this.newFunction = this.newFunction.bind(this); + this.getInfos = this.getInfos.bind(this); + this.setByCallstacks = this.setByCallstacks.bind(this); + this.setFolded = this.setFolded.bind(this); + this.pin = this.pin.bind(this); + this.track = this.track.bind(this); + this.removeLocation = this.removeLocation.bind(this); + this.delete = this.delete.bind(this); + this.clear = this.clear.bind(this); + this.map = this.map.bind(this); + } + + newFunction(fct: string): void { + if (!this.cache.has(fct)) this.cache.set(fct, new FunctionInfos(fct)); + } + + private getInfos(fct: string): FunctionInfos { + const { cache } = this; + if (cache.has(fct)) return cache.get(fct) as FunctionInfos; + const infos = new FunctionInfos(fct); + this.cache.set(fct, infos); + return infos; + } + + setByCallstacks(fct: string, byCallstacks: boolean): void { + const infos = this.cache.get(fct); + if (!infos) return; + infos.byCallstacks = byCallstacks; + } + + setFolded(fct: string, folded: boolean): void { + const infos = this.cache.get(fct); + if (!infos) return; + infos.folded = folded; + } + + pin(loc: Location): void { + const { target, fct } = loc; + this.getInfos(fct).pin(target); + } + + unpin(loc: Location): void { + const { target, fct } = loc; + this.cache.get(fct)?.pinned.delete(target); + } + + track(loc: Location): void { + const { target, fct } = loc; + this.getInfos(fct).track(target); + } + + status(loc?: Location): MarkerStatus | undefined { + if (!loc) return undefined; + const infos = this.cache.get(loc.fct); + if (infos?.pinned.has(loc.target)) + return [ 'Pinned', true ]; + else if (infos?.tracked.has(loc.target)) + return [ 'Tracked', true ]; + return 'JustFocused'; + } + + removeLocation(loc: Location): void { + const { target, fct } = loc; + const infos = this.cache.get(fct); + if (!infos) return; + infos.delete(target); + } + + delete(fct: string): void { + this.cache.delete(fct); + } + + clear(): void { + this.cache.clear(); + } + + clean(focused?: Location): void { + const focusedFct = focused?.fct; + this.cache.forEach((infos) => { + if (focusedFct !== infos.fct && infos.isEmpty()) + this.cache.delete(infos.fct); }); - }); - // --- compute line height - const getRowHeight = React.useCallback( - (k: number) => HSIZER.dimension(model.getRowLines(k)), - [model], - ); - // --- compute layout - const margin = WSIZER.capacity(width); - const estimatedHeight = HSIZER.dimension(1); - const [selection] = States.useSelection(); + } + + map<A>(func: (infos: FunctionInfos, fct: string) => A): A[] { + const acc: A[] = []; + this.cache.forEach((infos, fct) => acc.push(func(infos, fct))); + return acc; + } + +} + + + +function EvaTable(): JSX.Element { + const [ selection, select ] = States.useSelection(); + const [ state, setState ] = React.useState<StateToDisplay>('Before'); + const [ cs, setCS ] = React.useState<callstack>('Summary'); + const [ fcts ] = React.useState(new FunctionsManager()); + const [ tac, setTic ] = React.useState(false); + + const getProbe = useProbeCache(); + const getCallsites = useCallsitesCache(); + const getCallstacks = useCallstacksCache(); + + const [ focus, setFocus ] = React.useState<Probe | undefined>(undefined); React.useEffect(() => { - const location = selection?.current; - model.setLayout({ zoom, margin, location }); - }); - // --- render list + const target = selection?.current?.marker; + const fct = selection?.current?.fct; + const loc = (target && fct) ? { target, fct } : undefined; + const f = (p: Probe): void => { if (fct && p.code) fcts.newFunction(fct); }; + const doUpdate = (p: Probe): void => { f(p) ; setFocus(p); }; + fcts.clean(loc); + if (loc) getProbe(loc).then(doUpdate); + else setFocus(undefined); + }, [ fcts, selection, getProbe, setFocus ]); + + const setLocPin = React.useCallback((loc: Location, pin: boolean): void => { + if (pin) fcts.pin(loc); + else fcts.unpin(loc); + setTic(!tac); + }, [fcts, setTic, tac]); + + const remove = React.useCallback((probe: Probe): void => { + fcts.removeLocation(probe); + if (probe.target === focus?.target) + setFocus(undefined); + fcts.clean(undefined); + setTic(!tac); + }, [ fcts, focus, setFocus, tac ]); + + const functionsPromise = React.useMemo(() => { + const ps = fcts.map((infos, fct) => { + const { byCallstacks, folded } = infos; + const isSelectedCallstack = (c: callstack): boolean => c === cs; + const setFolded = (folded: boolean): void => { + fcts.setFolded(fct, folded); + setTic(!tac); + }; + const setByCS = (byCS: boolean): void => { + fcts.setByCallstacks(fct, byCS); + setTic(!tac); + }; + return { + fct, + markers: infos.markers(focus), + state, + close: () => { fcts.delete(fct); setTic(!tac); }, + pinProbe: setLocPin, + getProbe, + selectProbe: setFocus, + removeProbe: remove, + addLoc: (loc: Location) => { fcts.pin(loc); setTic(!tac); }, + folded, + setFolded, + getCallsites, + byCallstacks, + getCallstacks, + setByCallstacks: setByCS, + selectCallstack: (c: callstack) => { setCS(c); setTic(!tac); }, + isSelectedCallstack, + setSelection: select, + }; + }); + return Promise.all(ps.map(FunctionSection)); + }, + [ cs, fcts, focus, tac, getCallsites, setLocPin, + getCallstacks, getProbe, remove, select, state + ]); + const { result: functions } = Dome.usePromise(functionsPromise); + + const alarmsProm = React.useMemo(() => AlarmsInfos(focus)(cs), [ focus, cs ]); + const { result: alarmsInfos } = Dome.usePromise(alarmsProm); + + const stackInfosPromise = React.useMemo(async () => { + const callsites = await getCallsites(cs); + const tgt = selection.current?.marker; + const p = (c: Callsite): boolean => c.stmt !== undefined && c.stmt === tgt; + const isSelected = callsites.find(p) !== undefined; + return StackInfos({ callsites, isSelected, setSelection: select }); + }, [ cs, select, getCallsites, selection ]); + const { result: stackInfos } = Dome.usePromise(stackInfosPromise); + return ( - <VariableSizeList - ref={listRef} - itemCount={rowCount} - itemKey={model.getRowKey} - itemSize={getRowHeight} - estimatedItemSize={estimatedHeight} - width={width} - height={height} - itemData={{ model }} - > - {TableRow} - </VariableSizeList> + <> + <Ivette.TitleBar /> + <SelectedProbeInfos + probe={focus} + status={fcts.status(focus)} + setLocPin={setLocPin} + removeProbe={remove} + state={state} + setState={setState} + /> + <Vfill style={{ overflowY: 'auto' }}> + {React.Children.toArray(functions)} + </Vfill> + {alarmsInfos} + {stackInfos} + </> ); } -// -------------------------------------------------------------------------- + + +Ivette.registerComponent({ + id: 'frama-c.plugins.values', + group: 'frama-c.plugins', + rank: 1, + label: 'Eva Values', + title: 'Values inferred by the Eva analysis', + children: <EvaTable />, +}); + -- GitLab