From c3fc2b81489bfc6145d8609f5011e9e52e4bbb57 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Wed, 16 Dec 2020 12:37:17 +0100
Subject: [PATCH] [ivette/eva] EVA value cache & sizing
---
.../api/generated/plugins/eva/values/index.ts | 38 +++--
ivette/src/frama-c/eva/Values.tsx | 5 +-
ivette/src/frama-c/eva/cells.ts | 139 +++++++++++++++++-
ivette/src/frama-c/eva/layout.ts | 17 ++-
ivette/src/frama-c/eva/model.ts | 15 +-
ivette/src/frama-c/eva/probes.ts | 14 +-
src/plugins/value/api/values_request.ml | 16 +-
7 files changed, 202 insertions(+), 42 deletions(-)
diff --git a/ivette/api/generated/plugins/eva/values/index.ts b/ivette/api/generated/plugins/eva/values/index.ts
index 605a73fcd98..5e4139969a3 100644
--- a/ivette/api/generated/plugins/eva/values/index.ts
+++ b/ivette/api/generated/plugins/eva/values/index.ts
@@ -29,30 +29,41 @@ export const changed: Server.Signal = {
name: 'plugins.eva.values.changed',
};
+export type callstack = Json.index<'#eva-callstack-id'>;
+
+/** Loose decoder for `callstack` */
+export const jCallstack: Json.Loose<callstack> =
+ Json.jIndex<'#eva-callstack-id'>('#eva-callstack-id');
+
+/** Safe decoder for `callstack` */
+export const jCallstackSafe: Json.Safe<callstack> =
+ Json.jFail(Json.jIndex<'#eva-callstack-id'>('#eva-callstack-id'),
+ '#eva-callstack-id expected');
+
+/** Natural order for `callstack` */
+export const byCallstack: Compare.Order<callstack> = Compare.number;
+
const getCallstacks_internal: Server.GetRequest<
Json.key<'#stmt'>,
- Json.index<'#eva-callstack-id'>[]
+ callstack[]
> = {
kind: Server.RqKind.GET,
name: 'plugins.eva.values.getCallstacks',
input: Json.jKey<'#stmt'>('#stmt'),
- output: Json.jList(Json.jIndex<'#eva-callstack-id'>('#eva-callstack-id')),
+ output: Json.jList(jCallstack),
};
/** Callstacks for markers */
-export const getCallstacks: Server.GetRequest<
- Json.key<'#stmt'>,
- Json.index<'#eva-callstack-id'>[]
- >= getCallstacks_internal;
+export const getCallstacks: Server.GetRequest<Json.key<'#stmt'>,callstack[]>= getCallstacks_internal;
const getCallstackInfo_internal: Server.GetRequest<
- Json.index<'#eva-callstack-id'>,
+ callstack,
{ calls:
{ fct: Json.key<'#fct'>, stmt?: Json.key<'#stmt'>, rank: number }[],
descr: string }
> = {
kind: Server.RqKind.GET,
name: 'plugins.eva.values.getCallstackInfo',
- input: Json.jIndex<'#eva-callstack-id'>('#eva-callstack-id'),
+ input: jCallstack,
output: Json.jObject({
calls: Json.jList(
Json.jObject({
@@ -66,7 +77,7 @@ const getCallstackInfo_internal: Server.GetRequest<
};
/** Callstack Description */
export const getCallstackInfo: Server.GetRequest<
- Json.index<'#eva-callstack-id'>,
+ callstack,
{ calls:
{ fct: Json.key<'#fct'>, stmt?: Json.key<'#stmt'>, rank: number }[],
descr: string }
@@ -110,16 +121,13 @@ export const getProbeInfo: Server.GetRequest<
>= getProbeInfo_internal;
const getValues_internal: Server.GetRequest<
- { callstacks?: Json.index<'#eva-callstack-id'>, target: marker },
+ { callstack?: callstack, target: marker },
{ v_else?: string, v_then?: string, v_after?: string, values?: string,
alarms: [ "True" | "False" | "Unknown", string ][] }
> = {
kind: Server.RqKind.GET,
name: 'plugins.eva.values.getValues',
- input: Json.jObject({
- callstacks: Json.jIndex<'#eva-callstack-id'>('#eva-callstack-id'),
- target: jMarkerSafe,
- }),
+ input: Json.jObject({ callstack: jCallstack, target: jMarkerSafe,}),
output: Json.jObject({
v_else: Json.jString,
v_then: Json.jString,
@@ -140,7 +148,7 @@ const getValues_internal: Server.GetRequest<
};
/** Abstract values for the given marker */
export const getValues: Server.GetRequest<
- { callstacks?: Json.index<'#eva-callstack-id'>, target: marker },
+ { callstack?: callstack, target: marker },
{ v_else?: string, v_then?: string, v_after?: string, values?: string,
alarms: [ "True" | "False" | "Unknown", string ][] }
>= getValues_internal;
diff --git a/ivette/src/frama-c/eva/Values.tsx b/ivette/src/frama-c/eva/Values.tsx
index e0d331efb9d..b9a984f3f43 100644
--- a/ivette/src/frama-c/eva/Values.tsx
+++ b/ivette/src/frama-c/eva/Values.tsx
@@ -19,6 +19,7 @@ import * as Server from 'frama-c/server';
import * as States from 'frama-c/states';
// Plugins
+import * as Ast from 'frama-c/api/kernel/ast';
import * as Values from 'frama-c/api/plugins/eva/values';
// Locals
@@ -284,8 +285,8 @@ function ValuesComponent() {
Dome.useUpdate(ChangeEvent);
Server.useSignal(Values.changed, forceUpdate);
const [selection] = States.useSelection();
- const marker = selection?.current?.marker;
- const probe = vstate.focus(marker);
+ const target = Ast.jMarker(selection?.current?.marker);
+ const probe = vstate.focus(target);
const makeWindow = (size: Dimension) => (
<ValuesPanel vstate={vstate} {...size} />
);
diff --git a/ivette/src/frama-c/eva/cells.ts b/ivette/src/frama-c/eva/cells.ts
index 062da8f5924..3611997bd13 100644
--- a/ivette/src/frama-c/eva/cells.ts
+++ b/ivette/src/frama-c/eva/cells.ts
@@ -1,5 +1,14 @@
// --------------------------------------------------------------------------
-// --- Cell Utilities & Value Cache
+// --- Cells
+// --------------------------------------------------------------------------
+
+// Frama-C
+import * as Server from 'frama-c/server';
+import * as Ast from 'frama-c/api/kernel/ast';
+import * as Values from 'frama-c/api/plugins/eva/values';
+
+// --------------------------------------------------------------------------
+// --- Cell Utilities
// --------------------------------------------------------------------------
export type callback = () => void;
@@ -44,4 +53,132 @@ export function addV(a: Size, b: Size, padding = 0): Size {
};
}
+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;
+}
+
+// --------------------------------------------------------------------------
+// --- Value Cache
+// --------------------------------------------------------------------------
+
+export type EvaStatus = 'True' | 'False' | 'Unknown';
+export type EvaAlarm = [EvaStatus, string];
+
+export interface EvaValues {
+ errors?: string;
+ values?: string;
+ v_after?: string;
+ v_then?: string;
+ v_else?: string;
+ alarms?: EvaAlarm[];
+ size: Size;
+}
+
+export class ValueCache {
+
+ private readonly state: StateCallbacks;
+ private readonly probes = new Map<Ast.marker, Size>(); // Marker -> max in column
+ private readonly stacks = new Map<Values.callstack, Size>(); // Callstack -> max in row
+ private readonly vcache = new Map<string, EvaValues>(); // '<Marker><@Callstack>?' -> value
+ private smax = EMPTY; // max cell size
+
+ constructor(state: StateCallbacks) {
+ this.state = state;
+ }
+
+ clear() {
+ this.smax = EMPTY;
+ this.probes.clear();
+ this.stacks.clear();
+ this.vcache.clear();
+ this.state.forceLayout();
+ }
+
+ // --- Cached Measures
+
+ getMaxSize() { return this.smax; }
+
+ getProbeSize(target: Ast.marker) {
+ return this.probes.get(target) ?? EMPTY;
+ }
+
+ getStackSize(callstack: Values.callstack) {
+ return this.stacks.get(callstack) ?? EMPTY;
+ }
+
+ // --- Cached Values & Request Update
+
+ getValues(target: Ast.marker, callstack?: Values.callstack): EvaValues {
+ const key = `${target}@${callstack ?? '*'}`;
+ const cache = this.vcache;
+ const cached = cache.get(key);
+ if (cached) return cached;
+ const newValue: EvaValues = { values: '', size: EMPTY };
+ cache.set(key, newValue);
+ Server
+ .send(Values.getValues, { target, callstack })
+ .then((r) => {
+ newValue.errors = undefined;
+ newValue.values = r.values;
+ newValue.v_after = r.v_after;
+ newValue.v_then = r.v_then;
+ newValue.v_else = r.v_else;
+ newValue.alarms = r.alarms;
+ if (this.updateLayout(target, 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,
+ callstack: Values.callstack | undefined,
+ v: EvaValues,
+ ): boolean {
+ // measuring cell
+ let s = sizeof(v.values);
+ s = addS(s, v.v_after);
+ s = addS(s, v.v_then);
+ s = addS(s, v.v_else);
+ v.size = s;
+ // max cell size
+ const { smax } = this;
+ let small = leq(s, smax);
+ if (!small) this.smax = merge(s, smax);
+ // max size for probe column
+ const ps = this.getProbeSize(target);
+ if (!leq(s, ps)) {
+ this.probes.set(target, merge(ps, s));
+ small = false;
+ }
+ // max size for stack row
+ if (callstack) {
+ const cs = this.getStackSize(callstack);
+ if (!leq(s, cs)) {
+ this.stacks.set(callstack, merge(ps, s));
+ small = false;
+ }
+ }
+ // request new layout if not small enough
+ return !small;
+ }
+
+}
+
// --------------------------------------------------------------------------
diff --git a/ivette/src/frama-c/eva/layout.ts b/ivette/src/frama-c/eva/layout.ts
index 0b99c3cdc0a..2e54293d3e3 100644
--- a/ivette/src/frama-c/eva/layout.ts
+++ b/ivette/src/frama-c/eva/layout.ts
@@ -2,7 +2,7 @@
/* --- Layout ---*/
/* --------------------------------------------------------------------------*/
-import { Size, EMPTY, LABEL, addH } from './cells';
+import { Size, EMPTY, LABEL, addH, ValueCache } from './cells';
import { Probe } from './probes';
export interface LayoutProps {
@@ -27,14 +27,16 @@ export class LayoutEngine {
// --- Setup
- /* private */ readonly wcrop: number;
- /* private */ readonly hcrop: number;
- /* private */ readonly margin: number;
- /* private */ readonly remanent?: Probe;
+ private readonly cache: ValueCache;
+ private readonly wcrop: number;
+ private readonly hcrop: number;
+ private readonly margin: number;
constructor(
+ cache: ValueCache,
props: undefined | LayoutProps,
) {
+ this.cache = cache;
const zoom = Math.max(0, props?.zoom ?? 0);
this.hcrop = 1 + zoom;
this.wcrop = LABEL + 2 * zoom;
@@ -55,9 +57,10 @@ export class LayoutEngine {
}
push(p: Probe) {
- const s = this.crop(p.summary);
+ const probeSize = this.cache.getProbeSize(p.marker);
+ const s = this.crop(probeSize);
if (s.cols + this.rowSize.cols > this.margin) this.flush();
- p.layout = s;
+ p.colwidth = s.cols;
this.rowSize = addH(this.rowSize, s);
this.buffer.push(p);
}
diff --git a/ivette/src/frama-c/eva/model.ts b/ivette/src/frama-c/eva/model.ts
index b05b6ec8b48..908c5315c48 100644
--- a/ivette/src/frama-c/eva/model.ts
+++ b/ivette/src/frama-c/eva/model.ts
@@ -6,9 +6,11 @@
import { throttle } from 'lodash';
import equal from 'react-fast-compare';
+import type { marker } from 'frama-c/api/kernel/ast';
+
// Model
-import { StateCallbacks, callback } from './cells';
import { Probe } from './probes';
+import { callback, StateCallbacks, ValueCache } from './cells';
import { LayoutProps, LayoutEngine, Row } from './layout';
/* --------------------------------------------------------------------------*/
@@ -29,11 +31,12 @@ export class Model implements StateCallbacks {
}
// --- Probes
+
private focused?: Probe;
private remanent?: Probe; // last transient
private probes = new Map<string, Probe>();
- getProbe(m: string): Probe {
+ getProbe(m: marker): Probe {
let p = this.probes.get(m);
if (!p) {
p = new Probe(this, m);
@@ -43,7 +46,7 @@ export class Model implements StateCallbacks {
return p;
}
- focus(m: string | undefined): Probe | undefined {
+ focus(m: marker | undefined): Probe | undefined {
const r = this.remanent;
if (m) {
const p = this.getProbe(m);
@@ -62,6 +65,10 @@ export class Model implements StateCallbacks {
return this.focused;
}
+ // --- Values
+
+ private readonly cache = new ValueCache(this);
+
// --- Rows
private forcedLayout = false;
@@ -83,7 +90,7 @@ export class Model implements StateCallbacks {
toLayout.push(p);
}
});
- const engine = new LayoutEngine(this.layout);
+ const engine = new LayoutEngine(this.cache, this.layout);
toLayout.sort(Probe.order).forEach(engine.push);
this.rows = engine.flush();
this.forceUpdate();
diff --git a/ivette/src/frama-c/eva/probes.ts b/ivette/src/frama-c/eva/probes.ts
index dfb327c8aa9..28f4a4f82a0 100644
--- a/ivette/src/frama-c/eva/probes.ts
+++ b/ivette/src/frama-c/eva/probes.ts
@@ -4,12 +4,11 @@
// Frama-C
import * as Server from 'frama-c/server';
-
-// Plugins
import * as Values from 'frama-c/api/plugins/eva/values';
+import * as Ast from 'frama-c/api/kernel/ast';
// Model
-import { StateCallbacks, Size, EMPTY, LABEL } from './cells';
+import { StateCallbacks, LABEL } from './cells';
/* --------------------------------------------------------------------------*/
/* --- Probe Labelling ---*/
@@ -43,21 +42,18 @@ function newLabel() {
export class Probe {
// properties
- readonly marker: string;
+ readonly marker: Ast.marker;
readonly state: StateCallbacks;
transient = true;
label?: string;
code?: string;
stmt?: string;
rank?: number;
- layout: Size;
- summary: Size;
+ colwidth: number = LABEL;
- constructor(state: StateCallbacks, marker: string) {
+ constructor(state: StateCallbacks, marker: Ast.marker) {
this.marker = marker;
this.state = state;
- this.layout = EMPTY;
- this.summary = EMPTY;
this.requestProbeInfo = this.requestProbeInfo.bind(this);
this.setPersistent = this.setPersistent.bind(this);
this.setTransient = this.setTransient.bind(this);
diff --git a/src/plugins/value/api/values_request.ml b/src/plugins/value/api/values_request.ml
index 951a32b6d7b..a9a456b460e 100644
--- a/src/plugins/value/api/values_request.ml
+++ b/src/plugins/value/api/values_request.ml
@@ -185,8 +185,16 @@ end
(* --- Domain Utilities --- *)
(* -------------------------------------------------------------------------- *)
-module Jcallstack = Data.Index(Value_types.Callstack.Map)
- (struct let name = "eva-callstack-id" end)
+module Jcallstack : S with type t = callstack =
+struct
+ module I = Data.Index
+ (Value_types.Callstack.Map)
+ (struct let name = "eva-callstack-id" end)
+ let jtype = Data.declare ~package ~name:"callstack" I.jtype
+ type t = I.t
+ let to_json = I.to_json
+ let of_json = I.of_json
+end
module Jcallsite : Data.S with type t = Value_types.call_site =
struct
@@ -445,8 +453,8 @@ let () =
let get_tgt = Request.param getValues ~name:"target"
~descr:(Md.plain "Works with all markers containing an expression")
(module Jmarker) in
- let get_cs = Request.param_opt getValues ~name:"callstacks"
- ~descr:(Md.plain "Callstacks to collect (defaults to all)")
+ let get_cs = Request.param_opt getValues ~name:"callstack"
+ ~descr:(Md.plain "Callstack to collect (defaults to none)")
(module Jcallstack) in
let set_alarms = Request.result getValues ~name:"alarms"
~descr:(Md.plain "Alarms raised during evaluation")
--
GitLab