[ivette/eva] EVA value cache & sizing

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;

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} />
   );

ivette/src/frama-c/eva/cells.ts

 // --------------------------------------------------------------------------
-// --- 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;
+  }
+
+}
+
 // --------------------------------------------------------------------------

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);
   }

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();

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);

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")