diff --git a/ivette/api/generated/plugins/eva/values/index.ts b/ivette/api/generated/plugins/eva/values/index.ts
index 5e4139969a3eb72faeb2da9865cdb1b5692965de..75e2236ab73ece5dbd4e1d8444154b4f53643eed 100644
--- a/ivette/api/generated/plugins/eva/values/index.ts
+++ b/ivette/api/generated/plugins/eva/values/index.ts
@@ -57,30 +57,25 @@ export const getCallstacks: Server.GetRequest<Json.key<'#stmt'>,callstack[]>= ge
const getCallstackInfo_internal: Server.GetRequest<
callstack,
- { calls:
- { fct: Json.key<'#fct'>, stmt?: Json.key<'#stmt'>, rank: number }[],
- descr: string }
+ { callee: Json.key<'#fct'>, caller?: Json.key<'#fct'>,
+ stmt?: Json.key<'#stmt'>, rank?: number }[]
> = {
kind: Server.RqKind.GET,
name: 'plugins.eva.values.getCallstackInfo',
input: jCallstack,
- output: Json.jObject({
- calls: Json.jList(
- Json.jObject({
- fct: Json.jFail(Json.jKey<'#fct'>('#fct'),
- '#fct expected'),
- stmt: Json.jKey<'#stmt'>('#stmt'),
- rank: Json.jFail(Json.jNumber,'Number expected'),
- })),
- descr: Json.jFail(Json.jString,'String expected'),
- }),
+ output: Json.jList(
+ Json.jObject({
+ callee: Json.jFail(Json.jKey<'#fct'>('#fct'),'#fct expected'),
+ caller: Json.jKey<'#fct'>('#fct'),
+ stmt: Json.jKey<'#stmt'>('#stmt'),
+ rank: Json.jNumber,
+ })),
};
/** Callstack Description */
export const getCallstackInfo: Server.GetRequest<
callstack,
- { calls:
- { fct: Json.key<'#fct'>, stmt?: Json.key<'#stmt'>, rank: number }[],
- descr: string }
+ { callee: Json.key<'#fct'>, caller?: Json.key<'#fct'>,
+ stmt?: Json.key<'#stmt'>, rank?: number }[]
>= getCallstackInfo_internal;
const getStmtInfo_internal: Server.GetRequest<
diff --git a/ivette/src/frama-c/eva/Values.tsx b/ivette/src/frama-c/eva/Values.tsx
index 408bf0b5b01dca92075ac3971c134274ee83b516..9ab06cb22a9beeb4388e84e495b4aa8775cfd332 100644
--- a/ivette/src/frama-c/eva/Values.tsx
+++ b/ivette/src/frama-c/eva/Values.tsx
@@ -7,7 +7,7 @@ import React from 'react';
import * as Dome from 'dome';
import { classes } from 'dome/misc/utils';
import { VariableSizeList } from 'react-window';
-import { Vfill, Hpack, Space, Filler } from 'dome/layout/boxes';
+import { Vfill, Hpack, Filler } from 'dome/layout/boxes';
import { Label, Code } from 'dome/controls/labels';
import { IconButton } from 'dome/controls/buttons';
@@ -26,6 +26,7 @@ import { SizedArea, HSIZER, WSIZER } from './sized';
import { sizeof } from './cells';
import { Row } from './layout';
import { Probe } from './probes';
+import { Callsite } from './stacks';
import { Model, getModelInstance } from './model';
import './style.css';
@@ -39,37 +40,57 @@ function useModel(): Model {
return model;
}
+// --------------------------------------------------------------------------
+// --- Stmt Printer
+// --------------------------------------------------------------------------
+
+interface StmtProps {
+ stmt?: string;
+ rank?: number;
+}
+
+function Stmt(props: StmtProps) {
+ const { rank, stmt } = props;
+ if (rank === undefined || !stmt) return null;
+ const title = `Stmt id ${stmt} at rank ${rank}`;
+ return (
+ <span className="dome-text-code eva-stmt" title={title}>
+ @S{rank}
+ </span>
+ );
+}
+
// --------------------------------------------------------------------------
// --- Probe Panel
// --------------------------------------------------------------------------
-function ProbeEditor() {
+function ProbeInfos() {
const model = useModel();
const probe = model.getFocused();
const transient = probe?.transient ?? false;
const label = probe?.label;
const code = probe?.code;
+ const stmt = probe?.stmt;
const rank = probe?.rank;
- const stmt = rank ? `@S${rank}` : undefined;
const byCS = probe?.byCallstacks;
const stacks = model.getStacks(probe).length;
const stackable = byCS || stacks > 1;
const { cols, rows } = sizeof(code);
const width = WSIZER.dimension(cols) + 4;
const height = HSIZER.dimension(rows) + 3;
- const visible = probe ? !!code : model.getRowCount() > 0;
+ const visible = !!code;
const zoomed = probe?.zoomed;
const zoomable = probe?.zoomable;
const visibility = visible ? 'visible' : 'hidden';
return (
- <Hpack style={{ visibility }} className="eva-probe">
- <Label className="eva-probe-label">{label && `${label}:`}</Label>
- <div style={{ minWidth: width, height }} className="eva-probe-code">
+ <Hpack style={{ visibility }} className="eva-probeinfo">
+ <Label className="eva-probeinfo-label">{label && `${label}:`}</Label>
+ <div style={{ minWidth: width, height }} className="eva-probeinfo-code">
<SizedArea cols={cols} rows={rows}>{code}</SizedArea>
</div>
- <Code className="eva-probe-stmt">{stmt}</Code>
+ <Code><Stmt stmt={stmt} rank={rank} /></Code>
<IconButton
- className="eva-probe-button"
+ className="eva-probeinfo-button"
display={stackable}
selected={byCS}
icon="ITEMS.LIST"
@@ -77,14 +98,14 @@ function ProbeEditor() {
onClick={() => { if (probe) probe.setByCallstacks(!byCS); }}
/>
<IconButton
- className="eva-probe-button"
+ className="eva-probeinfo-button"
display={zoomable}
selected={zoomed}
icon="SEARCH"
onClick={() => { if (probe) probe.setZoomed(!zoomed); }}
/>
<IconButton
- className="eva-probe-button"
+ className="eva-probeinfo-button"
kind={transient ? 'selected' : 'warning'}
icon={transient ? 'CIRC.CHECK' : 'CIRC.CLOSE'}
title={transient ? 'Make the probe persistent' : 'Release the probe'}
@@ -99,15 +120,33 @@ function ProbeEditor() {
// --- Stack Panel
// --------------------------------------------------------------------------
-function StackEditor() {
+function StackInfos() {
const model = useModel();
+ const [, setSelection] = States.useSelection();
const callstack = model.getCallstack();
- const visibility = callstack === undefined ? 'hidden' : 'visible';
- return (
- <Hpack style={{ visibility }} className="eva-callinfo">
- <Code className="eva-probe-code">
- {callstack}
+ if (callstack.length <= 1) return null;
+ const makeCallsite = ({ caller, stmt, rank }: Callsite) => {
+ if (!caller || !stmt) return null;
+ const key = `${caller}@${stmt}`;
+ const onClick = () => {
+ const location = { function: caller, marker: stmt };
+ setSelection({ location });
+ };
+ return (
+ <Code
+ key={key}
+ icon="TRIANGLE.LEFT"
+ className="eva-callsite"
+ onClick={onClick}
+ >
+ {caller}
+ <Stmt stmt={stmt} rank={rank} />
</Code>
+ );
+ };
+ return (
+ <Hpack className="eva-info">
+ {callstack.map(makeCallsite)}
</Hpack>
);
}
@@ -141,14 +180,13 @@ function TableCell(props: TableCellProps) {
if (transient) {
contents = <span className="dome-text-label">« Probe »</span>;
} else {
- const { rank, code, label } = probe;
- const atpoint = rank && (
- <span className="eva-probe-stmt">@S{rank}</span>
- );
- const text =
- label ? <span className="dome-text-label">{label}</span> : code;
+ const { stmt, rank, code, label } = probe;
+ const textClass = label ? 'dome-text-label' : 'dome-text-code';
contents = (
- <span className="dome-text-code">{text}{atpoint}</span>
+ <>
+ <span className={textClass}>{label ?? code}</span>
+ <Stmt stmt={stmt} rank={rank} />
+ </>
);
}
break;
@@ -329,7 +367,7 @@ function ValuesComponent() {
/>
</TitleBar>
<Vfill>
- <ProbeEditor />
+ <ProbeInfos />
<Vfill>
<AutoSizer>
{(dim: Dimension) => (
@@ -340,7 +378,7 @@ function ValuesComponent() {
)}
</AutoSizer>
</Vfill>
- <StackEditor />
+ <StackInfos />
</Vfill>
</>
);
diff --git a/ivette/src/frama-c/eva/model.ts b/ivette/src/frama-c/eva/model.ts
index b09992ce9b335ed02b1e356402ed3d201367c627..0b825e10ad407e29a56aae7fc99b86eb1446cc67 100644
--- a/ivette/src/frama-c/eva/model.ts
+++ b/ivette/src/frama-c/eva/model.ts
@@ -13,7 +13,7 @@ import * as Ast from 'frama-c/api/kernel/ast';
// Model
import { Probe } from './probes';
-import { StacksCache } from './stacks';
+import { StacksCache, Callsite } from './stacks';
import { StateCallbacks, ValueCache } from './cells';
import { LayoutProps, LayoutEngine, Row } from './layout';
@@ -108,12 +108,12 @@ export class Model implements StateCallbacks {
return cs !== undefined ? cs === row.callstack : false;
}
- getCallstack(): string | undefined {
- const p = this.selected;
+ getCallstack(): Callsite[] {
const c = this.callstack;
- if (p && c) return `${p.stmt}::${c}`;
- if (p) return p.stmt;
- return undefined;
+ if (c !== undefined) return this.stacks.getCalls(c);
+ const [s] = this.getStacks(this.focused);
+ if (s !== undefined) return this.stacks.getCalls(s);
+ return [];
}
// --- Throttled
diff --git a/ivette/src/frama-c/eva/stacks.ts b/ivette/src/frama-c/eva/stacks.ts
index adbf6bd605bd1fc6c8caab4aa07bd00f06f4406c..c752b2316500be0fc3f8eaba379baa82dc1f0acc 100644
--- a/ivette/src/frama-c/eva/stacks.ts
+++ b/ivette/src/frama-c/eva/stacks.ts
@@ -12,6 +12,12 @@ import { StateCallbacks } from './cells';
// --------------------------------------------------------------------------
export type callstacks = Values.callstack[];
+export interface Callsite {
+ callee: string;
+ caller?: string;
+ stmt?: string;
+ rank?: number;
+}
// --------------------------------------------------------------------------
// --- CallStacks Cache
@@ -21,6 +27,7 @@ export class StacksCache {
private readonly state: StateCallbacks;
private readonly stacks = new Map<string, callstacks>();
+ private readonly calls = new Map<Values.callstack, Callsite[]>();
// --------------------------------------------------------------------------
// --- LifeCycle
@@ -46,6 +53,14 @@ export class StacksCache {
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 [];
+ }
+
// --------------------------------------------------------------------------
// --- Fetchers
// --------------------------------------------------------------------------
@@ -59,6 +74,15 @@ export class StacksCache {
});
}
+ private requestCalls(cs: Values.callstack) {
+ Server
+ .send(Values.getCallstackInfo, cs)
+ .then((calls) => {
+ this.calls.set(cs, calls);
+ this.state.forceUpdate();
+ });
+ }
+
}
// --------------------------------------------------------------------------
diff --git a/ivette/src/frama-c/eva/style.css b/ivette/src/frama-c/eva/style.css
index 920974dce2b82ece3168752d3225d1723820370b..575b5f587f4e7e2b76d385541e49876adae1e93f 100644
--- a/ivette/src/frama-c/eva/style.css
+++ b/ivette/src/frama-c/eva/style.css
@@ -9,11 +9,17 @@
text-overflow: ellipsis;
}
+.eva-stmt {
+ cursor: default;
+ color: grey;
+}
+
/* -------------------------------------------------------------------------- */
/* --- Probe Panel --- */
/* -------------------------------------------------------------------------- */
-.eva-probe {
+.eva-probeinfo {
+ min-height: 29px;
padding-left: 6px;
padding-top: 2px;
padding-bottom: 4px;
@@ -22,13 +28,13 @@
display: flex;
}
-.eva-probe-label {
+.eva-probeinfo-label {
flex: 0 1 auto;
min-width: 22px;
text-align: left;
}
-.eva-probe-code {
+.eva-probeinfo-code {
flex: 0 1 auto;
background: lightgrey;
min-width: 120px;
@@ -40,15 +46,14 @@
overflow: hidden;
}
-.eva-probe-stmt {
+.eva-probeinfo-stmt {
flex: 0 0 auto;
- color: grey;
margin-left: 2px;
margin-right: 0px;
margin-top: 2px;
}
-.eva-probe-button {
+.eva-probeinfo-button {
flex: 0 0 auto;
margin: 1px;
min-width: 16px;
@@ -100,11 +105,20 @@
/* --- Call Satck Info --- */
/* -------------------------------------------------------------------------- */
-.eva-callinfo {
+.eva-info {
width: 100%;
background: #ccc;
- padding-top: 2px;
+ padding-top: 3px;
padding-left: 12px;
+ padding-bottom: 2px;
+}
+
+.eva-callsite {
+ fill: #7cacbb;
+ background: #eee;
+ border-radius: 4px;
+ border: thin solid black;
+ padding-right: 7px;
}
/* -------------------------------------------------------------------------- */
diff --git a/src/plugins/value/api/values_request.ml b/src/plugins/value/api/values_request.ml
index a9a456b460e3f943caf1c8b865b4fe1527cc08b5..a5c89203fa258db1dc6bc15dd5ad42b1d256952b 100644
--- a/src/plugins/value/api/values_request.ml
+++ b/src/plugins/value/api/values_request.ml
@@ -31,7 +31,6 @@ module CSmap = CS.Hashtbl
module Md = Markdown
module Jkf = Kernel_ast.Kf
-module Jki = Kernel_ast.Ki
module Jstmt = Kernel_ast.Stmt
module Jmarker = Kernel_ast.Marker
@@ -98,7 +97,6 @@ let probe marker =
module Ranking :
sig
val stmt : stmt -> int
- val kinstr : kinstr -> int
val sort : callstack list -> callstack list
end =
struct
@@ -162,10 +160,6 @@ struct
let stmt = let rk = new ranker in rk#rank
- let kinstr = function
- | Kglobal -> 0
- | Kstmt s -> stmt s
-
let rec ranks (rks : int list) (cs : callstack) : int list =
match cs with
| [] -> rks
@@ -196,27 +190,40 @@ struct
let of_json = I.of_json
end
-module Jcallsite : Data.S with type t = Value_types.call_site =
+module Jcalls : Request.Output with type t = callstack =
struct
- type t = kernel_function * kinstr
- let jtype = Package.(Jrecord [
- "fct" , Jkf.jtype ;
- "stmt" , Jki.jtype ;
- "rank" , Jnumber ;
- ])
- let to_json (kf,ki) = `Assoc [
- "fct" , Jkf.to_json kf ;
- "stmt" , Jki.to_json ki ;
- "rank" , Jint.to_json (Ranking.kinstr ki) ;
- ]
- let of_json = function
- | `Assoc fds ->
- let kf = Jkf.of_json (List.assoc "fct" fds) in
- let ki = Jki.of_json (List.assoc "stmt" fds) in
- (kf,ki)
- | _ -> failwith "Not a call-site"
+
+ type t = callstack
+ let jtype = Package.(Jlist (Jrecord [
+ "callee" , Jkf.jtype ;
+ "caller" , Joption Jkf.jtype ;
+ "stmt" , Joption Jstmt.jtype ;
+ "rank" , Joption Jnumber ;
+ ]))
+
+ let rec jcallstack jcallee ki cs : json list =
+ match ki , cs with
+ | Kglobal , _ | _ , [] -> [
+ `Assoc [ "callee", jcallee ]
+ ]
+ | Kstmt stmt , (called,ki) :: cs ->
+ let jcaller = Jkf.to_json called in
+ let callsite = `Assoc [
+ "callee", jcallee ;
+ "caller", jcaller ;
+ "stmt", Jstmt.to_json stmt ;
+ "rank", Jint.to_json (Ranking.stmt stmt) ;
+ ] in
+ callsite :: jcallstack jcaller ki cs
+
+ let to_json = function
+ | [] -> `List []
+ | (callee,ki)::cs -> `List (jcallstack (Jkf.to_json callee) ki cs)
+
end
+
+
module Jtruth : Data.S with type t = truth =
struct
type t = truth
@@ -368,30 +375,13 @@ let () = Request.register ~package
(* --- Request getCallstackInfo --- *)
(* -------------------------------------------------------------------------- *)
-let pretty fmt cs =
- match cs with
- | (_, Kstmt _) :: callers ->
- Value_types.Callstack.pretty_hash fmt cs;
- Pretty_utils.pp_flowlist ~left:"@[" ~sep:" â†@ " ~right:"@]"
- (fun fmt (kf, _) -> Kernel_function.pretty fmt kf) fmt callers
- | _ -> ()
-
let () =
- let getCallstackInfo = Request.signature
- ~input:(module Jcallstack) () in
- let set_descr = Request.result getCallstackInfo ~name:"descr"
- ~descr:(Md.plain "Description")
- (module Jstring) in
- let set_calls = Request.result getCallstackInfo ~name:"calls"
- ~descr:(Md.plain "Callers site, from last to first")
- (module Jlist(Jcallsite)) in
- Request.register_sig ~package getCallstackInfo
+ Request.register ~package
~kind:`GET ~name:"getCallstackInfo"
~descr:(Md.plain "Callstack Description")
- begin fun rq cs ->
- set_calls rq cs ;
- set_descr rq (Pretty_utils.to_string pretty cs) ;
- end
+ ~input:(module Jcallstack)
+ ~output:(module Jcalls)
+ begin fun cs -> cs end
(* -------------------------------------------------------------------------- *)
(* --- Request getStmtInfo --- *)