diff --git a/ivette/api/generated/plugins/eva/values/index.ts b/ivette/api/generated/plugins/eva/values/index.ts
index 75e2236ab73ece5dbd4e1d8444154b4f53643eed..bc7353fe239426e399d04330a865ab4b616facad 100644
--- a/ivette/api/generated/plugins/eva/values/index.ts
+++ b/ivette/api/generated/plugins/eva/values/index.ts
@@ -98,21 +98,25 @@ export const getStmtInfo: Server.GetRequest<
const getProbeInfo_internal: Server.GetRequest<
marker,
- { rank: number, code?: string, stmt?: Json.key<'#stmt'> }
+ { condition: boolean, effects: boolean, rank: number,
+ stmt?: Json.key<'#stmt'>, code?: string }
> = {
kind: Server.RqKind.GET,
name: 'plugins.eva.values.getProbeInfo',
input: jMarker,
output: Json.jObject({
+ condition: Json.jFail(Json.jBoolean,'Boolean expected'),
+ effects: Json.jFail(Json.jBoolean,'Boolean expected'),
rank: Json.jFail(Json.jNumber,'Number expected'),
- code: Json.jString,
stmt: Json.jKey<'#stmt'>('#stmt'),
+ code: Json.jString,
}),
};
/** Probe informations */
export const getProbeInfo: Server.GetRequest<
marker,
- { rank: number, code?: string, stmt?: Json.key<'#stmt'> }
+ { condition: boolean, effects: boolean, rank: number,
+ stmt?: Json.key<'#stmt'>, code?: string }
>= getProbeInfo_internal;
const getValues_internal: Server.GetRequest<
diff --git a/ivette/src/dome/src/renderer/frame/toolbars.tsx b/ivette/src/dome/src/renderer/frame/toolbars.tsx
index 93d5c78ccc323d1ed613fd8350d8466248e5accf..74696bf0d3f0e4d436eb316d036871a7c0781a33 100644
--- a/ivette/src/dome/src/renderer/frame/toolbars.tsx
+++ b/ivette/src/dome/src/renderer/frame/toolbars.tsx
@@ -91,6 +91,10 @@ export interface ButtonProps<A> {
title?: string;
/** Button kind. */
kind?: ButtonKind;
+ /** Button is displayed (default `true`). */
+ visible?: boolean;
+ /** Button is hidden (default `false`). */
+ hidden?: boolean;
/** Enabled State (default `true`). */
enabled?: boolean;
/** Disabled State (default `false`). */
@@ -107,8 +111,10 @@ export interface ButtonProps<A> {
/** Toolbar Button. */
export function Button<A = undefined>(props: ButtonProps<A>) {
- const { selected, value, selection, onClick } = props;
+ const { visible = true, hidden = false } = props;
+ if (!visible || hidden) return null;
const { enabled = true, disabled = false } = props;
+ const { selected, value, selection, onClick } = props;
const isSelected = selected !== undefined
? selected
: (value !== undefined && value === selection);
@@ -147,13 +153,18 @@ export interface SelectionProps<A> {
// --- ToolBar Button Group
// --------------------------------------------------------------------------
+export interface ButtonGroupProps<A> extends SelectionProps<A> {
+ className?: string;
+ style?: React.CSSProperties;
+}
+
/**
Toolbar Button Group.
Properties of the button group are passed down the buttons of the group
as appropriate defaults.
*/
-export function ButtonGroup<A>(props: SelectionProps<A>) {
+export function ButtonGroup<A>(props: ButtonGroupProps<A>) {
const { children, value, onChange, enabled, disabled } = props;
const baseProps: ButtonProps<A> = {
enabled,
@@ -161,8 +172,9 @@ export function ButtonGroup<A>(props: SelectionProps<A>) {
selection: value,
onClick: onChange,
};
+ const className = classes('dome-xToolBar-group', props.className);
return (
- <div className="dome-xToolBar-group">
+ <div className={className} style={props.style}>
{React.Children.map(children, (elt) => React.cloneElement(
elt,
{ ...baseProps, ...elt.props },
diff --git a/ivette/src/frama-c/eva/Values.tsx b/ivette/src/frama-c/eva/Values.tsx
index 316602737496e54df6107d54bf2b4ec4cb9f6075..b2293d91b2acac1dd7383f994e477253404d78a4 100644
--- a/ivette/src/frama-c/eva/Values.tsx
+++ b/ivette/src/frama-c/eva/Values.tsx
@@ -10,6 +10,7 @@ import { VariableSizeList } from 'react-window';
import { Vfill, Hpack, Filler } from 'dome/layout/boxes';
import { Label, Code } from 'dome/controls/labels';
import { IconButton } from 'dome/controls/buttons';
+import { ButtonGroup, Button } from 'dome/frame/toolbars';
// External Libs
import { AutoSizer } from 'react-virtualized';
@@ -23,7 +24,8 @@ import * as Ast from 'frama-c/api/kernel/ast';
// Locals
import { SizedArea, HSIZER, WSIZER } from './sized';
-import { sizeof } from './cells';
+import { Diff } from './diffed';
+import { sizeof, valueAt, diffAfter, diffThen, diffElse } from './cells';
import { Row } from './layout';
import { Probe } from './probes';
import { Callsite } from './stacks';
@@ -83,6 +85,8 @@ function ProbeInfos() {
const zoomed = probe?.zoomed;
const zoomable = probe?.zoomable;
const visibility = visible ? 'visible' : 'hidden';
+ const effects = probe?.effects;
+ const condition = probe?.condition;
return (
<Hpack style={{ visibility }} className="eva-probeinfo">
<Label className="eva-probeinfo-label">{label && `${label}:`}</Label>
@@ -113,6 +117,33 @@ function ProbeInfos() {
onClick={() => { if (probe) probe.setTransient(!transient); }}
/>
<Filler />
+ <ButtonGroup
+ enabled={!!probe}
+ value={probe?.vstate}
+ onChange={(s) => { if (probe) probe.setState(s); }}
+ className="eva-probeinfo-state"
+ >
+ <Button
+ visible={effects || condition}
+ label="H"
+ value="Here"
+ />
+ <Button
+ visible={condition}
+ label="T"
+ value="Then"
+ />
+ <Button
+ visible={condition}
+ label="E"
+ value="Else"
+ />
+ <Button
+ visible={effects}
+ label="A"
+ value="After"
+ />
+ </ButtonGroup>
</Hpack>
);
}
@@ -153,7 +184,7 @@ function StackInfos() {
}
// --------------------------------------------------------------------------
-// --- Table Cell Layout
+// --- Table Cell
// --------------------------------------------------------------------------
interface TableCellProps {
@@ -196,15 +227,22 @@ function TableCell(props: TableCellProps) {
case 'values':
case 'callstack':
{
- const { values } = model.values.getValues(
+ const domain = model.values.getValues(
probe.marker,
probe.stmt,
callstack,
);
- const { cols, rows } = sizeof(values);
+ const { vstate: s, effects, condition } = probe;
+ const text = valueAt(domain, s) ?? '';
+ const diff = diffAfter(domain, effects, s);
+ const diffA = diffThen(domain, condition, s);
+ const diffB = diffElse(domain, condition, s);
+ const { cols, rows } = sizeof(text);
contents = (
<SizedArea cols={cols} rows={rows}>
- {values}
+ <span className={`eva-state-${s}`}>
+ <Diff text={text} diff={diff} diffA={diffA} diffB={diffB} />
+ </span>
</SizedArea>
);
}
diff --git a/ivette/src/frama-c/eva/cells.ts b/ivette/src/frama-c/eva/cells.ts
index 33e2a5647038a0dd83a0853f957aa4877b626c0d..acb3e9ea05432b1ef0952432b9cb098a0059e90f 100644
--- a/ivette/src/frama-c/eva/cells.ts
+++ b/ivette/src/frama-c/eva/cells.ts
@@ -88,7 +88,42 @@ export function valueAt(v: EvaValues, st: EvaState): string | undefined {
case 'After': return v.v_after;
case 'Then': return v.v_then;
case 'Else': return v.v_else;
- default: return undefined;
+ }
+}
+
+export function diffAfter(
+ v: EvaValues,
+ effects: boolean,
+ st: EvaState,
+): string | undefined {
+ if (!effects) return undefined;
+ switch (st) {
+ case 'Here': return v.v_after;
+ default: return v.values;
+ }
+}
+
+export function diffThen(
+ v: EvaValues,
+ condition: boolean,
+ st: EvaState,
+): string | undefined {
+ if (!condition) return undefined;
+ switch (st) {
+ case 'Here': return v.v_then;
+ default: return v.values;
+ }
+}
+
+export function diffElse(
+ v: EvaValues,
+ condition: boolean,
+ st: EvaState,
+): string | undefined {
+ if (!condition) return undefined;
+ switch (st) {
+ case 'Here': return v.v_else;
+ default: return v.values;
}
}
diff --git a/ivette/src/frama-c/eva/diffed.tsx b/ivette/src/frama-c/eva/diffed.tsx
index cef19297cff3d89169b6505c44aca22dca08a388..9fa71d9e20ce92d88dbd53fe9f6bc92a416e2974 100644
--- a/ivette/src/frama-c/eva/diffed.tsx
+++ b/ivette/src/frama-c/eva/diffed.tsx
@@ -5,63 +5,158 @@
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 readonly contents: React.ReactNode[] = [];
private added = false;
private removed = false;
private value = '';
+ private scratch = '';
+ private contents: React.ReactNode[] = [];
constructor() {
this.push = this.push.bind(this);
}
+ clear() {
+ this.added = false;
+ this.removed = false;
+ this.value = '';
+ this.scratch = '';
+ this.contents = [];
+ }
+
push(c: Change) {
- if (!c.added && !c.removed) this.flush();
- if (c.added) this.added = true;
- if (c.removed) this.removed = true;
- if (!c.added) this.value += c.value;
+ 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;
+ }
+ }
}
- flush(): React.ReactNode[] {
- const { value, added, removed, contents } = this;
- if (value) {
- if (added && removed) {
- contents.push(<span className="eva-diff-modified">{value}</span>);
- } else if (removed) {
- contents.push(<span className="eva-diff-removed">{value}</span>);
- } else if (added) {
- contents.push(<span className="eva-diff-added" />);
- } else {
- contents.push(value);
+ private flush() {
+ 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;
}
- return this.contents;
+ this.value = '';
+ this.added = false;
+ this.removed = false;
+ }
+
+ getContents(): React.ReactNode {
+ this.flush();
+ return <>{React.Children.toArray(this.contents)}</>;
+ }
+
+ getScratch() {
+ this.flush();
+ return this.scratch;
}
}
/* --------------------------------------------------------------------------*/
-/* --- Component with memoized diff ---*/
+/* --- Diff2 Component ---*/
/* --------------------------------------------------------------------------*/
-export interface DiffedProps {
- original?: string;
- modified?: string;
+export interface Diff2Props {
+ text: string;
+ diff: string;
}
-export function Diffed(props: DiffedProps) {
- const { original = '', modified = '' } = props;
+export function Diff2(props: Diff2Props) {
+ const { text, diff } = props;
const contents = React.useMemo(() => {
- if (original === modified) return original;
+ if (text === diff) return text;
const buffer = new DiffBuffer();
- diffChars(original, modified).forEach(buffer.push);
- return buffer.flush();
- }, [original, modified]);
- return <>{contents}</>;
+ const chunks = diffChars(text, diff);
+ console.log('DIFF', text, diff, chunks);
+ 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) {
+ const { text, diffA, diffB } = props;
+ const contents = React.useMemo(() => {
+ 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;
+ diffA?: string;
+ diffB?: string;
+}
+
+export function Diff(props: DiffProps): JSX.Element {
+ const { text, diff, diffA, diffB } = props;
+ if (text === diff) return <>{text}</>;
+ if (diff !== undefined)
+ return <Diff2 text={text} diff={diff} />;
+ if (diffA === undefined) {
+ if (diffB === undefined) return <>{text}</>;
+ return <Diff2 text={text} diff={diffB} />;
+ } if (diffB === undefined) {
+ if (diffA === undefined) return <>{text}</>;
+ return <Diff2 text={text} diff={diffA} />;
+ }
+ return <Diff3 text={text} diffA={diffA} diffB={diffB} />;
+
}
// --------------------------------------------------------------------------
diff --git a/ivette/src/frama-c/eva/probes.ts b/ivette/src/frama-c/eva/probes.ts
index 77f6c695e7777508fb647df32d758bbc6b629639..c920d71d0068667623c4e98973e82a291bad2313 100644
--- a/ivette/src/frama-c/eva/probes.ts
+++ b/ivette/src/frama-c/eva/probes.ts
@@ -58,6 +58,8 @@ export class Probe {
zoomed = false;
zoomable = false;
vstate: EvaState = 'Here';
+ effects = false;
+ condition = false;
constructor(state: ModelCallbacks, fct: string, marker: Ast.marker) {
this.fct = fct;
@@ -71,10 +73,13 @@ export class Probe {
this.loading = true;
Server
.send(Values.getProbeInfo, this.marker)
- .then(({ code, stmt, rank }) => {
+ .then(({ code, stmt, rank, effects, condition }) => {
this.code = code;
this.stmt = stmt;
this.rank = rank;
+ this.effects = effects;
+ this.condition = condition;
+ this.vstate = effects ? 'After' : 'Here';
this.loading = false;
})
.catch(() => {
@@ -118,6 +123,11 @@ export class Probe {
}
}
+ setState(s: EvaState | undefined) {
+ this.vstate = s ?? 'Here';
+ this.model.forceUpdate();
+ }
+
// --------------------------------------------------------------------------
// --- Ordering
// --------------------------------------------------------------------------
diff --git a/ivette/src/frama-c/eva/style.css b/ivette/src/frama-c/eva/style.css
index e970cbd5216646b6d100883fdfd809299891d3f3..dfa4086596e359cf79979a119d09131fe637f359 100644
--- a/ivette/src/frama-c/eva/style.css
+++ b/ivette/src/frama-c/eva/style.css
@@ -19,7 +19,7 @@
/* -------------------------------------------------------------------------- */
.eva-probeinfo {
- min-height: 29px;
+ min-height: 32px;
padding-left: 6px;
padding-top: 2px;
padding-bottom: 4px;
@@ -59,6 +59,35 @@
min-width: 16px;
}
+.eva-probeinfo-state {
+ margin-top: 2px;
+ margin-bottom: 2px;
+}
+
+/* -------------------------------------------------------------------------- */
+/* --- Call Satck Info --- */
+/* -------------------------------------------------------------------------- */
+
+.eva-info {
+ width: 100%;
+ background: #ccc;
+ 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;
+}
+
+.eva-callsite {
+ cursor: default;
+}
+
/* -------------------------------------------------------------------------- */
/* --- Table Rows --- */
/* -------------------------------------------------------------------------- */
@@ -101,29 +130,19 @@
text-align: center;
}
-/* -------------------------------------------------------------------------- */
-/* --- Call Satck Info --- */
-/* -------------------------------------------------------------------------- */
-
-.eva-info {
- width: 100%;
- background: #ccc;
- padding-top: 3px;
- padding-left: 12px;
- padding-bottom: 2px;
+.eva-diff-shadow {
+ border: solid red thin;
+ position: relative;
+ z-index: -1;
}
-.eva-callsite {
- fill: #7cacbb;
- background: #eee;
- border-radius: 4px;
- border: thin solid black;
- padding-right: 7px;
-}
+.eva-diff-added { }
+.eva-diff-removed { text-decoration: strike }
-.eva-callsite {
- cursor: default;
-}
+.eva-state-Here .eva-diff { background: pink; }
+.eva-state-After .eva-diff { background: yellow; }
+.eva-state-Then .eva-diff { background: green; }
+.eva-state-Else .eva-diff { background: orange; }
/* -------------------------------------------------------------------------- */
/* --- Table Rows Background --- */
diff --git a/ivette/src/renderer/ASTview.tsx b/ivette/src/renderer/ASTview.tsx
index 3d6d82e4b316940218b02d7c3121d84b220f59c8..8583af381634c5a90bebcf4e82ac79ff56515e73 100644
--- a/ivette/src/renderer/ASTview.tsx
+++ b/ivette/src/renderer/ASTview.tsx
@@ -108,13 +108,13 @@ function getBulletColor(status: States.Tag) {
case 'invalid_under_hyp': return '#FF0000';
case 'valid':
case 'valid_under_hyp': return '#00B900';
- case 'considered_valid': return '#0000FF';
+ case 'considered_valid': return '#73bbbb';
case 'invalid_but_dead':
case 'valid_but_dead':
case 'unknown_but_dead': return '#000000';
case 'never_tried': return '#FFFFFF';
case 'inconsistent': return '#FF00FF';
- default: return '#0000FF';
+ default: return '#FF8300';
}
}
diff --git a/src/plugins/value/api/values_request.ml b/src/plugins/value/api/values_request.ml
index a5c89203fa258db1dc6bc15dd5ad42b1d256952b..035340717f3f43761da0c8aeb4d49614d572d6ab 100644
--- a/src/plugins/value/api/values_request.ml
+++ b/src/plugins/value/api/values_request.ml
@@ -46,6 +46,7 @@ type probe =
| Pexpr of exp * stmt
| Plval of lval * stmt
| Pnone
+
type callstack = Value_types.callstack
type truth = Abstract_interp.truth
type step = [ `Here | `After | `Then of exp | `Else of exp ]
@@ -314,7 +315,7 @@ struct
begin fun st vs ->
match st with
| `Here -> vs (* absurd *)
- | `After -> dnext st vs @@ dstate ~after:false stmt callstack
+ | `After -> dnext st vs @@ dstate ~after:true stmt callstack
| `Then cond -> dnext st vs @@ A.assume_cond stmt state cond true
| `Else cond -> dnext st vs @@ A.assume_cond stmt state cond false
end (next_steps stmt) []
@@ -409,28 +410,42 @@ let () =
let () =
let getProbeInfo = Request.signature ~input:(module Jmarker) () in
- let set_stmt = Request.result_opt getProbeInfo
- ~name:"stmt" ~descr:(Md.plain "Probe statement")
- (module Jstmt) in
let set_code = Request.result_opt getProbeInfo
~name:"code" ~descr:(Md.plain "Probe source code")
(module Jstring) in
+ let set_stmt = Request.result_opt getProbeInfo
+ ~name:"stmt" ~descr:(Md.plain "Probe statement")
+ (module Jstmt) in
let set_rank = Request.result getProbeInfo
~name:"rank" ~descr:(Md.plain "Probe statement rank")
~default:0 (module Jint) in
- let pp_code rq pp x = set_code rq (Some (Pretty_utils.to_string pp x)) in
- Request.register_sig ~package ~kind:`GET getProbeInfo
+ let set_effects = Request.result getProbeInfo
+ ~name:"effects" ~descr:(Md.plain "Effectfull statement")
+ ~default:false (module Jbool) in
+ let set_condition = Request.result getProbeInfo
+ ~name:"condition" ~descr:(Md.plain "Conditional statement")
+ ~default:false (module Jbool) in
+ let set_probe rq pp p s =
+ begin
+ set_code rq (Some (Pretty_utils.to_string pp p)) ;
+ set_stmt rq (Some s) ;
+ set_rank rq (Ranking.stmt s) ;
+ List.iter
+ (function
+ | `Here -> ()
+ | `Then _ | `Else _ -> set_condition rq true
+ | `After -> set_effects rq true
+ )
+ (next_steps s)
+ end
+ in Request.register_sig ~package ~kind:`GET getProbeInfo
~name:"getProbeInfo" ~descr:(Md.plain "Probe informations")
begin fun rq marker ->
match probe marker with
| Plval(l,s) ->
- pp_code rq Printer.pp_lval l ;
- set_stmt rq (Some s) ;
- set_rank rq (Ranking.stmt s) ;
+ set_probe rq Printer.pp_lval l s ;
| Pexpr(e,s) ->
- pp_code rq Printer.pp_exp e ;
- set_stmt rq (Some s) ;
- set_rank rq (Ranking.stmt s) ;
+ set_probe rq Printer.pp_exp e s ;
| Pnone -> ()
end