From f6269033e4465674f2639f523b9521a4b662d89a Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Mon, 11 Sep 2023 12:41:28 +0200
Subject: [PATCH] [wp] revisiting goal table
---
ivette/src/frama-c/plugins/wp/api/index.ts | 61 ++++++++++++----
ivette/src/frama-c/plugins/wp/goals.tsx | 34 ++++-----
src/plugins/wp/wpApi.ml | 81 ++++++++++++++--------
3 files changed, 112 insertions(+), 64 deletions(-)
diff --git a/ivette/src/frama-c/plugins/wp/api/index.ts b/ivette/src/frama-c/plugins/wp/api/index.ts
index b4f1f05f214..d3ea8c14e71 100644
--- a/ivette/src/frama-c/plugins/wp/api/index.ts
+++ b/ivette/src/frama-c/plugins/wp/api/index.ts
@@ -112,6 +112,34 @@ export const resultDefault: result =
{ descr: '', cached: false, verdict: '', solverTime: 0, proverTime: 0,
proverSteps: 0 };
+/** Test Status */
+export type status =
+ Json.key<'#NORESULT'> | Json.key<'#COMPUTING'> | Json.key<'#FAILED'> |
+ Json.key<'#STEPOUT'> | Json.key<'#UNKNOWN'> | Json.key<'#PASSED'> |
+ Json.key<'#VALID'> | Json.key<'#INVALID'>;
+
+/** Decoder for `status` */
+export const jStatus: Json.Decoder<status> =
+ Json.jUnion<Json.key<'#NORESULT'> | Json.key<'#COMPUTING'> |
+ Json.key<'#FAILED'> | Json.key<'#STEPOUT'> |
+ Json.key<'#UNKNOWN'> | Json.key<'#PASSED'> |
+ Json.key<'#VALID'> | Json.key<'#INVALID'>>(
+ Json.jKey<'#NORESULT'>('#NORESULT'),
+ Json.jKey<'#COMPUTING'>('#COMPUTING'),
+ Json.jKey<'#FAILED'>('#FAILED'),
+ Json.jKey<'#STEPOUT'>('#STEPOUT'),
+ Json.jKey<'#UNKNOWN'>('#UNKNOWN'),
+ Json.jKey<'#PASSED'>('#PASSED'),
+ Json.jKey<'#VALID'>('#VALID'),
+ Json.jKey<'#INVALID'>('#INVALID'),
+ );
+
+/** Natural order for `status` */
+export const byStatus: Compare.Order<status> = Compare.structural;
+
+/** Default value for `status` */
+export const statusDefault: status = Json.jKey<'#NORESULT'>('#NORESULT')('');
+
/** Prover Result */
export type stats =
{ summary: string, tactics: number, proved: number, total: number };
@@ -155,17 +183,19 @@ export interface goalsData {
wpo: goal;
/** Property Marker */
property: marker;
- /** Informal name */
- name: string;
/** Associated function, if any */
fct?: fct;
/** Associated behavior, if any */
bhv?: string;
/** Associated axiomatic, if any */
thy?: string;
- /** Smoking (or not) goal and result */
- result: [ boolean, boolean ];
- /** Verdict Details */
+ /** Informal Property Name */
+ name: string;
+ /** Smoking (or not) goal */
+ smoke: boolean;
+ /** Verdict, Status */
+ status: status;
+ /** Prover Stats Summary */
stats: stats;
/** Script File */
script?: string;
@@ -178,11 +208,12 @@ export const jGoalsData: Json.Decoder<goalsData> =
Json.jObject({
wpo: jGoal,
property: jMarker,
- name: Json.jString,
fct: Json.jOption(jFct),
bhv: Json.jOption(Json.jString),
thy: Json.jOption(Json.jString),
- result: Json.jPair( Json.jBoolean, Json.jBoolean,),
+ name: Json.jString,
+ smoke: Json.jBoolean,
+ status: jStatus,
stats: jStats,
script: Json.jOption(Json.jString),
saved: Json.jBoolean,
@@ -191,16 +222,17 @@ export const jGoalsData: Json.Decoder<goalsData> =
/** Natural order for `goalsData` */
export const byGoalsData: Compare.Order<goalsData> =
Compare.byFields
- <{ wpo: goal, property: marker, name: string, fct?: fct, bhv?: string,
- thy?: string, result: [ boolean, boolean ], stats: stats,
+ <{ wpo: goal, property: marker, fct?: fct, bhv?: string, thy?: string,
+ name: string, smoke: boolean, status: status, stats: stats,
script?: string, saved: boolean }>({
wpo: byGoal,
property: byMarker,
- name: Compare.string,
fct: Compare.defined(byFct),
bhv: Compare.defined(Compare.string),
thy: Compare.defined(Compare.string),
- result: Compare.pair(Compare.boolean,Compare.boolean,),
+ name: Compare.string,
+ smoke: Compare.boolean,
+ status: byStatus,
stats: byStats,
script: Compare.defined(Compare.string),
saved: Compare.boolean,
@@ -255,9 +287,10 @@ export const goals: State.Array<goal,goalsData> = goals_internal;
/** Default value for `goalsData` */
export const goalsDataDefault: goalsData =
- { wpo: goalDefault, property: markerDefault, name: '', fct: undefined,
- bhv: undefined, thy: undefined, result: [ false, false ],
- stats: statsDefault, script: undefined, saved: false };
+ { wpo: goalDefault, property: markerDefault, fct: undefined,
+ bhv: undefined, thy: undefined, name: '', smoke: false,
+ status: statusDefault, stats: statsDefault, script: undefined,
+ saved: false };
/** Proof Server Activity */
export const serverActivity: Server.Signal = {
diff --git a/ivette/src/frama-c/plugins/wp/goals.tsx b/ivette/src/frama-c/plugins/wp/goals.tsx
index 012d2a881ca..0e29a2d0ec9 100644
--- a/ivette/src/frama-c/plugins/wp/goals.tsx
+++ b/ivette/src/frama-c/plugins/wp/goals.tsx
@@ -21,30 +21,20 @@
/* ************************************************************************ */
import React from 'react';
-import { Icon } from 'dome/controls/icons';
-import { Table, Column, Renderer } from 'dome/table/views';
+import { Table, Column } from 'dome/table/views';
import * as Ivette from 'ivette';
import * as States from 'frama-c/states';
import * as WP from 'frama-c/plugins/wp/api';
-const renderResult: Renderer<[boolean, boolean]> =
- ([smoking, passed]): JSX.Element =>
- (<Icon
- id=
- {passed ? 'CIRC.CHECK' :
- (smoking ? 'CIRC.CLOSE' : 'CIRC.QUESTION')
- }
- fill=
- {passed ? `var(--positive-button-color)` :
- (smoking ? `var(--negative-button-color)` : `var(--warning-button-color)`)
- }
- />);
+/* -------------------------------------------------------------------------- */
+/* --- Goals Table --- */
+/* -------------------------------------------------------------------------- */
function WPGoals(): JSX.Element {
const model = States.useSyncArrayModel(WP.goals);
// TODO: from AST selection, find WPO
- const [_astSelection, updateAstSelection] = States.useSelection();
+ const [_, updateAstSelection] = States.useSelection();
const [wpoSelection, setWpoSelection] = React.useState(WP.goalDefault);
const onWpoSelection = React.useCallback(
@@ -62,17 +52,15 @@ function WPGoals(): JSX.Element {
onSelection={onWpoSelection}
selection={wpoSelection}
>
- <Column id='fct' label='Function' />
- <Column id='name' label='Names' />
- <Column
- id='result'
- label='Result'
- render={renderResult}
- />
+ <Column id='status' label='Status' fixed={true} width={80} />
+ <Column id='name' label='Property' />
</Table>
);
}
+/* -------------------------------------------------------------------------- */
+/* --- Goals Component --- */
+/* -------------------------------------------------------------------------- */
Ivette.registerComponent({
id: 'frama-c.plugins.wp.goals',
@@ -82,3 +70,5 @@ Ivette.registerComponent({
title: 'WP Generated Verification Conditions',
children: <WPGoals />,
});
+
+/* -------------------------------------------------------------------------- */
diff --git a/src/plugins/wp/wpApi.ml b/src/plugins/wp/wpApi.ml
index 0eec40b4198..a894d73e80f 100644
--- a/src/plugins/wp/wpApi.ml
+++ b/src/plugins/wp/wpApi.ml
@@ -105,9 +105,37 @@ struct
]
end
+module STATUS =
+struct
+ type t = { smoke : bool ; verdict : VCS.verdict }
+ let jtype = D.declare ~package ~name:"status"
+ ~descr:(Md.plain "Test Status")
+ (Junion [
+ Jkey "NORESULT" ;
+ Jkey "COMPUTING" ;
+ Jkey "FAILED" ;
+ Jkey "STEPOUT" ;
+ Jkey "UNKNOWN" ;
+ Jkey "PASSED" ;
+ Jkey "VALID" ;
+ Jkey "INVALID" ;
+ ])
+ let to_json { smoke ; verdict } =
+ `String begin
+ match verdict with
+ | VCS.Valid -> if smoke then "INVALID" else "VALID"
+ | VCS.Unknown -> if smoke then "PASSED" else "UNKNOWN"
+ | Failed -> "FAILED"
+ | NoResult -> "NORESULT"
+ | Computing _ -> "COMPUTING"
+ | Timeout -> "TIMEOUT"
+ | Stepout -> "STEPOUT"
+ end
+end
+
module STATS =
struct
- type t = bool * Stats.stats
+ type t = Stats.stats
let jtype = D.declare ~package ~name:"stats"
~descr:(Md.plain "Prover Result")
(Jrecord [
@@ -116,17 +144,8 @@ struct
"proved", Jnumber;
"total", Jnumber;
])
- let to_json (smoke,cs) : Json.t =
- let verdict = match cs.Stats.best with
- | VCS.Valid -> if smoke then "Doomed" else "Valid"
- | VCS.Unknown -> if smoke then "Passed" else "Unknown"
- | Failed -> "Failure"
- | NoResult -> "No Result"
- | Computing _ -> "Computing"
- | Timeout -> "Timeout"
- | Stepout -> "Stepout"
- in
- let summary = Format.asprintf "%s%a" verdict
+ let to_json cs : Json.t =
+ let summary = Pretty_utils.to_string
(Stats.pp_stats ~shell:false ~cache:Update) cs
in `Assoc [
"summary", `String summary ;
@@ -150,11 +169,6 @@ let () = R.register ~package ~kind:`GET ~name:"getAvailableProvers"
let gmodel : Wpo.t S.model = S.model ()
-let () = S.column gmodel ~name:"property"
- ~descr:(Md.plain "Property Marker")
- ~data:(module AST.Marker)
- ~get:(fun g -> Printer_tag.PIP (WpPropId.property_of_id g.Wpo.po_pid))
-
let get_kf g = match g.Wpo.po_idx with
| Function(kf,_) -> Some kf
| Axiomatic _ -> None
@@ -167,11 +181,16 @@ let get_thy g = match g.Wpo.po_idx with
| Function _ -> None
| Axiomatic ax -> ax
-let get_stats g = Wpo.is_smoke_test g, ProofEngine.consolidated g
+let get_status g =
+ STATUS.{
+ smoke = Wpo.is_smoke_test g ;
+ verdict = (ProofEngine.consolidated g).best ;
+ }
-let () = S.column gmodel ~name:"name"
- ~descr:(Md.plain "Informal name") ~data:(module D.Jstring)
- ~get:(fun g -> g.Wpo.po_name)
+let () = S.column gmodel ~name:"property"
+ ~descr:(Md.plain "Property Marker")
+ ~data:(module AST.Marker)
+ ~get:(fun g -> Printer_tag.PIP (WpPropId.property_of_id g.Wpo.po_pid))
let () = S.column gmodel ~name:"fct"
~descr:(Md.plain "Associated function, if any")
@@ -185,16 +204,22 @@ let () = S.option gmodel ~name:"thy"
~descr:(Md.plain "Associated axiomatic, if any")
~data:(module D.Jstring) ~get:get_thy
-let get_result g =
- Wpo.is_smoke_test g, Wpo.is_passed g
+let () = S.column gmodel ~name:"name"
+ ~descr:(Md.plain "Informal Property Name")
+ ~data:(module D.Jstring)
+ ~get:(fun g -> g.Wpo.po_name)
+
+let () = S.column gmodel ~name:"smoke"
+ ~descr:(Md.plain "Smoking (or not) goal")
+ ~data:(module D.Jbool) ~get:Wpo.is_smoke_test
-let () = S.column gmodel ~name:"result"
- ~descr:(Md.plain "Smoking (or not) goal and result")
- ~data:(module D.Jpair (D.Jbool)(D.Jbool)) ~get:get_result
+let () = S.column gmodel ~name:"status"
+ ~descr:(Md.plain "Verdict, Status")
+ ~data:(module STATUS) ~get:get_status
let () = S.column gmodel ~name:"stats"
- ~descr:(Md.plain "Verdict Details")
- ~data:(module STATS) ~get:get_stats
+ ~descr:(Md.plain "Prover Stats Summary")
+ ~data:(module STATS) ~get:ProofEngine.consolidated
let () = S.option gmodel ~name:"script"
~descr:(Md.plain "Script File")
--
GitLab