From d06e50c205780c5cbe2238243c3dba1df6b89faf Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Tue, 5 Jan 2021 09:32:23 +0100
Subject: [PATCH] [ivette/eva] group callstacks by function
---
.../api/generated/plugins/eva/values/index.ts | 9 +--
ivette/src/frama-c/eva/Values.tsx | 12 +---
ivette/src/frama-c/eva/cells.ts | 33 +++++-----
ivette/src/frama-c/eva/layout.ts | 47 ++++++++++-----
ivette/src/frama-c/eva/model.ts | 12 ++--
ivette/src/frama-c/eva/probes.ts | 6 +-
ivette/src/frama-c/eva/stacks.ts | 60 ++++++++++++++-----
src/plugins/value/api/values_request.ml | 14 ++++-
8 files changed, 124 insertions(+), 69 deletions(-)
diff --git a/ivette/api/generated/plugins/eva/values/index.ts b/ivette/api/generated/plugins/eva/values/index.ts
index bc7353fe239..b08b8540d74 100644
--- a/ivette/api/generated/plugins/eva/values/index.ts
+++ b/ivette/api/generated/plugins/eva/values/index.ts
@@ -43,17 +43,14 @@ export const jCallstackSafe: Json.Safe<callstack> =
/** Natural order for `callstack` */
export const byCallstack: Compare.Order<callstack> = Compare.number;
-const getCallstacks_internal: Server.GetRequest<
- Json.key<'#stmt'>,
- callstack[]
- > = {
+const getCallstacks_internal: Server.GetRequest<marker[],callstack[]> = {
kind: Server.RqKind.GET,
name: 'plugins.eva.values.getCallstacks',
- input: Json.jKey<'#stmt'>('#stmt'),
+ input: Json.jList(jMarker),
output: Json.jList(jCallstack),
};
/** Callstacks for markers */
-export const getCallstacks: Server.GetRequest<Json.key<'#stmt'>,callstack[]>= getCallstacks_internal;
+export const getCallstacks: Server.GetRequest<marker[],callstack[]>= getCallstacks_internal;
const getCallstackInfo_internal: Server.GetRequest<
callstack,
diff --git a/ivette/src/frama-c/eva/Values.tsx b/ivette/src/frama-c/eva/Values.tsx
index 6bdf15345c8..5a10fc807c9 100644
--- a/ivette/src/frama-c/eva/Values.tsx
+++ b/ivette/src/frama-c/eva/Values.tsx
@@ -159,11 +159,9 @@ function AlarmsInfo() {
const probe = model.getFocused();
if (probe) {
const callstack = model.getCallstack();
- const domain =
- model.values.getValues(probe.marker, probe.stmt, callstack);
+ const domain = model.values.getValues(probe, callstack);
const alarms = domain?.alarms ?? [];
if (alarms.length > 0) {
- // console.log('ALARMS', alarms);
const renderAlarm = ([status, alarm]: EvaAlarm) => {
const className = `eva-alarm-info eva-alarm-${status}`;
return (
@@ -172,7 +170,7 @@ function AlarmsInfo() {
};
return (
<Vpack className="eva-info">
- {alarms.map(renderAlarm)}
+ {React.Children.toArray(alarms.map(renderAlarm))}
</Vpack>
);
}
@@ -259,11 +257,7 @@ function TableCell(props: TableCellProps) {
case 'values':
case 'callstack':
{
- const domain = model.values.getValues(
- probe.marker,
- probe.stmt,
- callstack,
- );
+ const domain = model.values.getValues(probe, callstack);
const { alarms = [] } = domain;
const { vstate: s, effects, condition } = probe;
const text = valueAt(domain, s) ?? '';
diff --git a/ivette/src/frama-c/eva/cells.ts b/ivette/src/frama-c/eva/cells.ts
index acb3e9ea054..5c4b29066bf 100644
--- a/ivette/src/frama-c/eva/cells.ts
+++ b/ivette/src/frama-c/eva/cells.ts
@@ -16,6 +16,7 @@ export type callback = () => void;
export interface ModelCallbacks {
forceUpdate: callback;
forceLayout: callback;
+ mergeStacks: (fct: string) => void;
}
export interface Size { cols: number; rows: number }
@@ -131,6 +132,11 @@ export function diffElse(
// --- Value Cache
// --------------------------------------------------------------------------
+export interface Probe {
+ fct: string | undefined;
+ marker: Ast.marker;
+}
+
export class ValueCache {
private readonly state: ModelCallbacks;
@@ -159,33 +165,32 @@ export class ValueCache {
return this.probes.get(target) ?? EMPTY;
}
- private static stackKey(stmt: string, callstack: Values.callstack) {
- return `${stmt}::${callstack}`;
+ private static stackKey(fct: string, callstack: Values.callstack) {
+ return `${fct}::${callstack}`;
}
- getStackSize(stmt: string, callstack: Values.callstack) {
- const key = ValueCache.stackKey(stmt, callstack);
+ getStackSize(fct: string, callstack: Values.callstack) {
+ const key = ValueCache.stackKey(fct, callstack);
return this.stacks.get(key) ?? EMPTY;
}
// --- Cached Values & Request Update
getValues(
- target: Ast.marker,
- stmt: string | undefined,
+ { fct, marker }: Probe,
callstack: Values.callstack | undefined,
): EvaValues {
- const key = callstack !== undefined ? `${target}@${callstack}` : target;
+ const key = callstack !== undefined ? `${marker}@${callstack}` : marker;
const cache = this.vcache;
const cached = cache.get(key);
if (cached) return cached;
const newValue: EvaValues = { values: '', size: EMPTY };
- if (callstack !== undefined && stmt === undefined)
+ if (callstack !== undefined && fct === undefined)
return newValue;
- // callstack !== undefined ==> stmt !== undefined)
+ // callstack !== undefined ==> fct !== undefined)
cache.set(key, newValue);
Server
- .send(Values.getValues, { target, callstack })
+ .send(Values.getValues, { target: marker, callstack })
.then((r) => {
newValue.errors = undefined;
newValue.values = r.values;
@@ -193,7 +198,7 @@ export class ValueCache {
newValue.v_then = r.v_then;
newValue.v_else = r.v_else;
newValue.alarms = r.alarms;
- if (this.updateLayout(target, stmt, callstack, newValue))
+ if (this.updateLayout(marker, fct, callstack, newValue))
this.state.forceLayout();
else
this.state.forceUpdate();
@@ -209,7 +214,7 @@ export class ValueCache {
private updateLayout(
target: Ast.marker,
- stmt: string | undefined,
+ fct: string | undefined,
callstack: Values.callstack | undefined,
v: EvaValues,
): boolean {
@@ -231,9 +236,9 @@ export class ValueCache {
}
// max size for stack row
if (callstack !== undefined) {
- if (stmt === undefined) small = false;
+ if (fct === undefined) small = false;
else {
- const key = ValueCache.stackKey(stmt, callstack);
+ const key = ValueCache.stackKey(fct, callstack);
const cs = this.stacks.get(key) ?? EMPTY;
if (!leq(s, cs)) {
this.stacks.set(key, merge(cs, s));
diff --git a/ivette/src/frama-c/eva/layout.ts b/ivette/src/frama-c/eva/layout.ts
index c416fa7c894..58ae0f0b1cd 100644
--- a/ivette/src/frama-c/eva/layout.ts
+++ b/ivette/src/frama-c/eva/layout.ts
@@ -59,7 +59,7 @@ export class LayoutEngine {
}
// --- Probe Buffer
- private byStacks?: string; // stmt
+ private byFctStacks?: string; // function
private rowSize: Size = EMPTY;
private buffer: Probe[] = [];
private rows: Row[] = [];
@@ -74,18 +74,35 @@ export class LayoutEngine {
};
}
- push(p: Probe) {
+ layout(ps: Probe[]): Row[] {
+ 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) return -1;
+ if (fp > fq) return +1;
+ const cp = p.byCallstacks;
+ const cq = q.byCallstacks;
+ if (!cp && cq) return (-1);
+ if (cp && !cq) return (+1);
+ return Probe.order(p, q);
+ }
+
+ private push(p: Probe) {
const probeSize = this.values.getProbeSize(p.marker);
const s = this.crop(p.zoomed, probeSize);
p.zoomable = p.zoomed || !leq(probeSize, s);
p.minCols = s.cols;
p.maxCols = Math.max(p.minCols, probeSize.cols);
- const stmt = p.byCallstacks ? p.stmt : undefined;
- if (stmt !== this.byStacks) {
+ const fct = p.byCallstacks ? p.fct : undefined;
+ if (fct !== this.byFctStacks) {
this.flush();
- this.byStacks = stmt;
+ this.byFctStacks = fct;
}
- if (!stmt && s.cols + this.rowSize.cols > this.margin)
+ if (!fct && s.cols + this.rowSize.cols > this.margin)
this.flush();
this.rowSize = addH(this.rowSize, s);
this.rowSize.cols += PADDING;
@@ -94,16 +111,18 @@ export class LayoutEngine {
// --- Flush Rows
- flush(): Row[] {
+ private flush(): Row[] {
const ps = this.buffer;
const rs = this.rows;
if (ps.length > 0) {
- const stmt = this.byStacks;
- if (stmt) {
+ const fct = this.byFctStacks;
+ const hlines = this.rowSize.rows;
+ if (fct) {
// --- by callstacks
- const wcs = this.stacks.getStacks(stmt);
+ const markers = ps.map((p) => p.marker);
+ const wcs = this.stacks.getStacksForFunction(fct, markers);
rs.push({
- key: `P${stmt}`,
+ key: `F${fct}`,
kind: 'probes',
probes: ps,
stacks: wcs.length,
@@ -111,13 +130,13 @@ export class LayoutEngine {
});
wcs.forEach((cs, k) => {
rs.push({
- key: `C${stmt}::${cs}`,
+ key: `C${fct}::${cs}`,
kind: 'callstack',
probes: ps,
stackIndex: k,
stacks: wcs.length,
callstack: cs,
- hlines: this.values.getStackSize(stmt, cs).rows,
+ hlines,
});
});
} else {
@@ -132,7 +151,7 @@ export class LayoutEngine {
key: `V${n}`,
kind: 'values',
probes: ps,
- hlines: this.rowSize.rows,
+ hlines,
});
}
}
diff --git a/ivette/src/frama-c/eva/model.ts b/ivette/src/frama-c/eva/model.ts
index 6f24c809c84..ce2d7b30c1f 100644
--- a/ivette/src/frama-c/eva/model.ts
+++ b/ivette/src/frama-c/eva/model.ts
@@ -32,6 +32,7 @@ export class Model implements ModelCallbacks {
this.forceUpdate = this.forceUpdate.bind(this);
this.forceLayout = this.forceLayout.bind(this);
this.forceReload = this.forceReload.bind(this);
+ this.mergeStacks = this.mergeStacks.bind(this);
this.computeLayout = this.computeLayout.bind(this);
this.setLayout = throttle(this.setLayout.bind(this), 300);
this.getRowKey = this.getRowKey.bind(this);
@@ -63,8 +64,7 @@ export class Model implements ModelCallbacks {
}
getStacks(p: Probe | undefined): Values.callstack[] {
- const stmt = p?.stmt;
- return stmt ? this.stacks.getStacks(stmt) : [];
+ return p ? this.stacks.getStacksForProbe(p) : [];
}
// --- Caches
@@ -165,8 +165,7 @@ export class Model implements ModelCallbacks {
this.values,
this.stacks,
);
- toLayout.sort(Probe.order).forEach(engine.push);
- this.rows = engine.flush();
+ this.rows = engine.layout(toLayout);
this.laidout.emit();
this.lock = false;
}
@@ -196,6 +195,11 @@ export class Model implements ModelCallbacks {
// --- Foce Update
forceUpdate() { this.changed.emit(); }
+ // --- Force Stacks Reload
+ mergeStacks(fct: string) {
+ this.stacks.mergeStacksForFunction(fct);
+ this.forceLayout();
+ }
}
// --------------------------------------------------------------------------
diff --git a/ivette/src/frama-c/eva/probes.ts b/ivette/src/frama-c/eva/probes.ts
index c920d71d006..aaa3f86cc52 100644
--- a/ivette/src/frama-c/eva/probes.ts
+++ b/ivette/src/frama-c/eva/probes.ts
@@ -112,7 +112,7 @@ export class Probe {
setByCallstacks(byCS: boolean) {
if (byCS !== this.byCallstacks) {
this.byCallstacks = byCS;
- this.model.forceLayout();
+ this.model.mergeStacks(this.fct);
}
}
@@ -137,10 +137,6 @@ export class Probe {
const rq = q.rank ?? 0;
if (rp < rq) return (-1);
if (rp > rq) return (+1);
- const cp = p.byCallstacks;
- const cq = q.byCallstacks;
- if (!cp && cq) return (-1);
- if (cp && !cq) return (+1);
if (p.marker < q.marker) return (-1);
if (p.marker > q.marker) return (+1);
return 0;
diff --git a/ivette/src/frama-c/eva/stacks.ts b/ivette/src/frama-c/eva/stacks.ts
index 013638a1630..84e5f98b290 100644
--- a/ivette/src/frama-c/eva/stacks.ts
+++ b/ivette/src/frama-c/eva/stacks.ts
@@ -3,6 +3,7 @@
// --------------------------------------------------------------------------
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';
import { ModelCallbacks } from './cells';
@@ -19,6 +20,20 @@ export interface Callsite {
rank?: number;
}
+// --------------------------------------------------------------------------
+// --- CallStacks by Function
+// --------------------------------------------------------------------------
+
+interface StacksByFct {
+ dirty: boolean;
+ stacks: callstacks;
+}
+
+interface ProbeFct {
+ fct: string;
+ marker: Ast.marker;
+}
+
// --------------------------------------------------------------------------
// --- CallStacks Cache
// --------------------------------------------------------------------------
@@ -26,7 +41,7 @@ export interface Callsite {
export class StacksCache {
private readonly model: ModelCallbacks;
- private readonly stacks = new Map<string, callstacks>();
+ private readonly byFct = new Map<string, StacksByFct>();
private readonly calls = new Map<Values.callstack, Callsite[]>();
// --------------------------------------------------------------------------
@@ -38,24 +53,40 @@ export class StacksCache {
}
clear() {
- this.stacks.clear();
+ this.byFct.clear();
}
// --------------------------------------------------------------------------
// --- Getters
// --------------------------------------------------------------------------
- getStacks(stmt: string): callstacks {
- const cs = this.stacks.get(stmt);
- if (cs !== undefined) return cs;
- this.stacks.set(stmt, []);
- this.requestCallstacks(stmt);
- return [];
+ mergeStacksForFunction(fct: string) {
+ const buffer = this.byFct.get(fct);
+ if (buffer) buffer.dirty = true;
+ }
+
+ getStacksForProbe({ fct, marker }: ProbeFct): callstacks {
+ const fs = this.byFct.get(fct);
+ if (!fs) {
+ this.byFct.set(fct, { dirty: true, stacks: [] });
+ this.requestCallstacks(fct, [marker]);
+ }
+ return fs ? fs.stacks : [];
+ }
+
+ getStacksForFunction(fct: string, probes?: Ast.marker[]): callstacks {
+ const fs = this.byFct.get(fct);
+ if (!fs) this.byFct.set(fct, { dirty: false, stacks: [] });
+ if (probes) {
+ if (!fs || fs.dirty) this.requestCallstacks(fct, probes);
+ if (fs && fs.dirty) fs.dirty = false;
+ }
+ return fs ? fs.stacks : [];
}
getCalls(cs: Values.callstack): Callsite[] {
- const fs = this.calls.get(cs);
- if (fs !== undefined) return fs;
+ const fcs = this.calls.get(cs);
+ if (fcs !== undefined) return fcs;
this.calls.set(cs, []);
this.requestCalls(cs);
return [];
@@ -65,12 +96,13 @@ export class StacksCache {
// --- Fetchers
// --------------------------------------------------------------------------
- private requestCallstacks(stmt: string) {
+ private requestCallstacks(fct: string, probes: Ast.marker[]) {
Server
- .send(Values.getCallstacks, stmt)
- .then((cs: callstacks) => {
- this.stacks.set(stmt, cs);
+ .send(Values.getCallstacks, probes)
+ .then((stacks: callstacks) => {
+ this.byFct.set(fct, { dirty: false, stacks });
this.model.forceLayout();
+ this.model.forceUpdate();
});
}
diff --git a/src/plugins/value/api/values_request.ml b/src/plugins/value/api/values_request.ml
index 035340717f3..e6587ea8582 100644
--- a/src/plugins/value/api/values_request.ml
+++ b/src/plugins/value/api/values_request.ml
@@ -27,6 +27,7 @@ open Cil_types
module Kmap = Kernel_function.Hashtbl
module Smap = Cil_datatype.Stmt.Hashtbl
module CS = Value_types.Callstack
+module CSet = CS.Set
module CSmap = CS.Hashtbl
module Md = Markdown
@@ -365,11 +366,18 @@ let proxy =
let () = Request.register ~package
~kind:`GET ~name:"getCallstacks"
~descr:(Md.plain "Callstacks for markers")
- ~input:(module Jstmt)
+ ~input:(module Jlist(Jmarker))
~output:(module Jlist(Jcallstack))
- begin fun stmt ->
+ begin fun markers ->
let module A = (val !proxy) in
- Ranking.sort (A.callstacks stmt)
+ let cset = List.fold_left
+ (fun cset marker ->
+ match probe marker with
+ | Pexpr(_,stmt) | Plval(_,stmt) ->
+ List.fold_right CSet.add (A.callstacks stmt) cset
+ | Pnone -> cset
+ ) CSet.empty markers in
+ Ranking.sort (CSet.elements cset)
end
(* -------------------------------------------------------------------------- *)
--
GitLab