From 530271319ec7aba1976db2cc0abd7df4aa8be768 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Thu, 30 Nov 2023 20:32:41 +0100
Subject: [PATCH] [ivette/wp] fix goal status details
---
ivette/src/frama-c/plugins/wp/goals.tsx | 27 +++++++++++---------
ivette/src/frama-c/plugins/wp/index.tsx | 16 +++++++-----
ivette/src/frama-c/plugins/wp/tip.tsx | 34 ++++++++++++++++++++++---
src/plugins/wp/wpApi.ml | 21 +++++++--------
4 files changed, 66 insertions(+), 32 deletions(-)
diff --git a/ivette/src/frama-c/plugins/wp/goals.tsx b/ivette/src/frama-c/plugins/wp/goals.tsx
index 1155150d55d..535c7713344 100644
--- a/ivette/src/frama-c/plugins/wp/goals.tsx
+++ b/ivette/src/frama-c/plugins/wp/goals.tsx
@@ -45,6 +45,7 @@ function getScope(g : WP.goalsData): string {
interface IconStatus {
icon: string;
+ label: string;
kind: IconKind;
title: string;
}
@@ -52,22 +53,24 @@ interface IconStatus {
interface Status extends IconStatus { label: string }
const noResult : IconStatus =
- { icon: 'MINUS', kind: 'disabled', title: 'No Result' };
+ { icon: 'MINUS', label: 'No Result', kind: 'disabled', title: 'No Result' };
+/* eslint-disable max-len */
const baseStatus : { [key:string]: IconStatus } = {
- 'VALID': { icon: 'CHECK', kind: 'positive', title: 'Valid Goal' },
- 'PASSED': { icon: 'CHECK', kind: 'positive', title: 'Passed Test' },
- 'DOOMED': { icon: 'CROSS', kind: 'negative', title: 'Doomed Test' },
- 'FAILED': { icon: 'WARNING', kind: 'negative', title: 'Prover Failure' },
- 'UNKNOWN': { icon: 'ATTENTION', kind: 'warning', title: 'Prover Stucked' },
- 'TIMEOUT': { icon: 'HELP', kind: 'warning', title: 'Prover Timeout' },
- 'STEPOUT': { icon: 'HELP', kind: 'warning', title: 'Prover Stepout' },
- 'COMPUTING': { icon: 'EXECUTE', kind: 'default', title: 'Computing…' },
+ 'VALID': { icon: 'CHECK', label: 'Valid', kind: 'positive', title: 'Valid Goal' },
+ 'PASSED': { icon: 'CHECK', label: 'Passed', kind: 'positive', title: 'Passed Test' },
+ 'DOOMED': { icon: 'CROSS', label: 'Doomed', kind: 'negative', title: 'Doomed Test' },
+ 'FAILED': { icon: 'WARNING', label: 'Failed', kind: 'negative', title: 'Prover Failure' },
+ 'UNKNOWN': { icon: 'ATTENTION', label: 'Unknown', kind: 'warning', title: 'Prover Stucked' },
+ 'TIMEOUT': { icon: 'HELP', label: 'Timeout', kind: 'warning', title: 'Prover Timeout' },
+ 'STEPOUT': { icon: 'HELP', label: 'Stepout', kind: 'warning', title: 'Prover Stepout' },
+ 'COMPUTING': { icon: 'EXECUTE', label: 'Running', kind: 'default', title: 'Prover is running' },
};
+/* eslint-enable max-len */
-function getStatus(g : WP.goalsData): Status {
- const base = baseStatus[g.status] ?? noResult;
- return { ...base, label: g.stats.summary };
+export function getStatus(g : WP.goalsData): Status {
+ const { label, ...base } = baseStatus[g.status] ?? noResult;
+ return { ...base, label: label + g.stats.summary };
}
function renderStatus(s : Status): JSX.Element {
diff --git a/ivette/src/frama-c/plugins/wp/index.tsx b/ivette/src/frama-c/plugins/wp/index.tsx
index ac06fc2a954..872aa980024 100644
--- a/ivette/src/frama-c/plugins/wp/index.tsx
+++ b/ivette/src/frama-c/plugins/wp/index.tsx
@@ -34,7 +34,7 @@ import * as Ivette from 'ivette';
import * as Server from 'frama-c/server';
import * as States from 'frama-c/states';
import { GoalTable } from './goals';
-import { TIP } from './tip';
+import { TIPView } from './tip';
import * as WP from 'frama-c/plugins/wp/api';
import './style.css';
@@ -45,15 +45,17 @@ import './style.css';
function WPGoals(): JSX.Element {
const [scoped, flipScoped] = Dome.useFlipSettings('frama-c.wp.goals.scoped');
const [failed, flipFailed] = Dome.useFlipSettings('frama-c.wp.goals.failed');
- const [tip, flipTip] = Dome.useFlipSettings('frama-c.wp.goals.tip', false);
+ const [displayTip, setTip] = React.useState(false);
const [current, setCurrent] = React.useState(WP.goalDefault);
- Server.useShutdown(() => setCurrent(WP.goalDefault));
+ Server.useShutdown(() => {
+ setTip(false);
+ setCurrent(WP.goalDefault);
+ });
const scope = States.useCurrentScope();
const [goals, setGoals] = React.useState(0);
const [total, setTotal] = React.useState(0);
const hasGoals = total > 0;
const hasSelection = current !== WP.goalDefault;
- const displayTip = tip && hasSelection;
return (
<>
<Ivette.TitleBar>
@@ -76,7 +78,7 @@ function WPGoals(): JSX.Element {
kind={displayTip ? 'warning' : 'positive'}
title='Goal Resolution'
enabled={hasSelection}
- onClick={flipTip} />
+ onClick={() => setTip(!displayTip)} />
</Ivette.TitleBar>
<GoalTable
display={!displayTip}
@@ -84,11 +86,11 @@ function WPGoals(): JSX.Element {
failed={failed}
current={current}
setCurrent={setCurrent}
- setTIP={flipTip}
+ setTIP={() => setTip(true)}
setGoals={setGoals}
setTotal={setTotal}
/>
- <TIP
+ <TIPView
display={displayTip}
goal={current} />
</>
diff --git a/ivette/src/frama-c/plugins/wp/tip.tsx b/ivette/src/frama-c/plugins/wp/tip.tsx
index af1dafa4fe8..1ed009f3313 100644
--- a/ivette/src/frama-c/plugins/wp/tip.tsx
+++ b/ivette/src/frama-c/plugins/wp/tip.tsx
@@ -21,18 +21,46 @@
/* ************************************************************************ */
import React from 'react';
-import { Vfill } from 'dome/layout/boxes';
+import { Cell } from 'dome/controls/labels';
+import { Vfill, Hbox } from 'dome/layout/boxes';
+import * as States from 'frama-c/states';
import * as WP from 'frama-c/plugins/wp/api';
+import * as TIP from 'frama-c/plugins/wp/api/tip';
+import { getStatus } from './goals';
+
+/* -------------------------------------------------------------------------- */
+/* --- TIP View --- */
+/* -------------------------------------------------------------------------- */
+
export interface TIPProps {
display: boolean;
goal: WP.goal;
}
-export function TIP(props: TIPProps): JSX.Element {
+function useTarget(target: WP.goal | undefined) : WP.goalsData {
+ const data = States.useSyncArrayElt( WP.goals, target );
+ return data ?? WP.goalsDataDefault;
+}
+
+export function TIPView(props: TIPProps): JSX.Element {
const { display, goal } = props;
+ const target = goal !== WP.goalDefault ? goal : undefined;
+ const infos: WP.goalsData = useTarget(goal);
+ const status = getStatus(infos);
+ const { index=0, pending=0 } =
+ States.useRequest( TIP.getProofState, target ) ?? {};
return (
<Vfill display={display}>
- <div>{goal}</div>
+ <Hbox>
+ <Cell
+ icon='HOME'
+ label={infos.wpo} title='Goal identifier' />
+ <Cell
+ icon='CODE'
+ display={pending > 0}
+ label={`${index+1}/${pending}`} title='Pending proof nodes'/>
+ <Cell {...status}/>
+ </Hbox>
</Vfill>
);
}
diff --git a/src/plugins/wp/wpApi.ml b/src/plugins/wp/wpApi.ml
index 41b8b9415c0..26910b42448 100644
--- a/src/plugins/wp/wpApi.ml
+++ b/src/plugins/wp/wpApi.ml
@@ -52,17 +52,18 @@ module INDEX = State_builder.Ref
let default () = Hashtbl.create 0
end)
+let indexGoal g =
+ let id = g.Wpo.po_gid in
+ let index = INDEX.get () in
+ if not (Hashtbl.mem index id) then Hashtbl.add index id g ; id
+
module Goal : D.S with type t = Wpo.t =
struct
type t = Wpo.t
let jtype = D.declare ~package ~name:"goal"
~descr:(Md.plain "Proof Obligations") (Jkey "wpo")
let of_json js = Hashtbl.find (INDEX.get ()) (Json.string js)
- let to_json g =
- let id = g.Wpo.po_gid in
- let index = INDEX.get () in
- if not (Hashtbl.mem index id) then Hashtbl.add index id g ;
- `String id
+ let to_json g = `String (indexGoal g)
end
(* -------------------------------------------------------------------------- *)
@@ -123,13 +124,13 @@ struct
let to_json { smoke ; verdict } =
`String begin
match verdict with
- | VCS.Valid -> if smoke then "DOOMED" else "VALID"
- | VCS.Unknown -> if smoke then "PASSED" else "UNKNOWN"
+ | Valid -> if smoke then "DOOMED" else "VALID"
+ | Unknown -> if smoke then "PASSED" else "UNKNOWN"
+ | Timeout -> if smoke then "PASSED" else "TIMEOUT"
+ | Stepout -> if smoke then "PASSED" else "STEPOUT"
| Failed -> "FAILED"
| NoResult -> "NORESULT"
| Computing _ -> "COMPUTING"
- | Timeout -> "TIMEOUT"
- | Stepout -> "STEPOUT"
end
end
@@ -263,7 +264,7 @@ let () = S.column gmodel ~name:"saved"
let _ = S.register_array ~package ~name:"goals"
~descr:(Md.plain "Generated Goals")
- ~key:(fun g -> g.Wpo.po_gid)
+ ~key:indexGoal
~keyName:"wpo"
~keyType:Goal.jtype
~iter:Wpo.iter_on_goals
--
GitLab