From c9dcc47db22fb0fb6bf4be7ccdae450a631e8d0b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Mon, 11 Sep 2023 22:01:15 +0200
Subject: [PATCH] [wp/ivette] goals filter
---
ivette/src/frama-c/plugins/wp/api/index.ts | 10 +++--
ivette/src/frama-c/plugins/wp/goals.tsx | 48 ++++++++++++++--------
ivette/src/frama-c/plugins/wp/index.tsx | 45 ++++++++++++++++++--
src/plugins/wp/wpApi.ml | 4 ++
4 files changed, 83 insertions(+), 24 deletions(-)
diff --git a/ivette/src/frama-c/plugins/wp/api/index.ts b/ivette/src/frama-c/plugins/wp/api/index.ts
index e8bd3107906..583cfa27486 100644
--- a/ivette/src/frama-c/plugins/wp/api/index.ts
+++ b/ivette/src/frama-c/plugins/wp/api/index.ts
@@ -193,6 +193,8 @@ export interface goalsData {
name: string;
/** Smoking (or not) goal */
smoke: boolean;
+ /** Valid or Passed goal */
+ passed: boolean;
/** Verdict, Status */
status: status;
/** Prover Stats Summary */
@@ -213,6 +215,7 @@ export const jGoalsData: Json.Decoder<goalsData> =
thy: Json.jOption(Json.jString),
name: Json.jString,
smoke: Json.jBoolean,
+ passed: Json.jBoolean,
status: jStatus,
stats: jStats,
script: Json.jOption(Json.jString),
@@ -223,8 +226,8 @@ export const jGoalsData: Json.Decoder<goalsData> =
export const byGoalsData: Compare.Order<goalsData> =
Compare.byFields
<{ wpo: goal, property: marker, fct?: fct, bhv?: string, thy?: string,
- name: string, smoke: boolean, status: status, stats: stats,
- script?: string, saved: boolean }>({
+ name: string, smoke: boolean, passed: boolean, status: status,
+ stats: stats, script?: string, saved: boolean }>({
wpo: byGoal,
property: byMarker,
fct: Compare.defined(byFct),
@@ -232,6 +235,7 @@ export const byGoalsData: Compare.Order<goalsData> =
thy: Compare.defined(Compare.string),
name: Compare.string,
smoke: Compare.boolean,
+ passed: Compare.boolean,
status: byStatus,
stats: byStats,
script: Compare.defined(Compare.string),
@@ -288,7 +292,7 @@ export const goals: State.Array<goal,goalsData> = goals_internal;
/** Default value for `goalsData` */
export const goalsDataDefault: goalsData =
{ wpo: goalDefault, property: markerDefault, fct: undefined,
- bhv: undefined, thy: undefined, name: '', smoke: false,
+ bhv: undefined, thy: undefined, name: '', smoke: false, passed: false,
status: statusDefault, stats: statsDefault, script: undefined,
saved: false };
diff --git a/ivette/src/frama-c/plugins/wp/goals.tsx b/ivette/src/frama-c/plugins/wp/goals.tsx
index a02b4300db2..45d135b2773 100644
--- a/ivette/src/frama-c/plugins/wp/goals.tsx
+++ b/ivette/src/frama-c/plugins/wp/goals.tsx
@@ -22,8 +22,8 @@
import React from 'react';
import { IconKind, Cell } from 'dome/controls/labels';
+import { Filter } from 'dome/table/models';
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';
@@ -62,14 +62,33 @@ function renderStatus(s : Status): JSX.Element {
return <Cell {...s} />;
}
+/* -------------------------------------------------------------------------- */
+/* --- Goals Filter --- */
+/* -------------------------------------------------------------------------- */
+
+function filterGoal(
+ failed: boolean,
+ scope: string | undefined,
+): Filter<WP.goal, WP.goalsData> {
+ return (goal: WP.goalsData): boolean => {
+ if (failed && goal.passed) return false;
+ if (scope && scope && goal.fct !== scope) return false;
+ return true;
+ };
+}
+
/* -------------------------------------------------------------------------- */
/* --- Goals Table --- */
/* -------------------------------------------------------------------------- */
-function WPGoals(): JSX.Element {
- const model = States.useSyncArrayModel(WP.goals);
+export interface GoalTableProps {
+ scope: string | undefined;
+ failed: boolean;
+}
- // TODO: from AST selection, find WPO
+export function GoalTable(props: GoalTableProps): JSX.Element {
+ const { scope, failed } = props;
+ const model = States.useSyncArrayModel(WP.goals);
const [_, updateAstSelection] = States.useSelection();
const [wpoSelection, setWpoSelection] = React.useState(WP.goalDefault);
@@ -81,6 +100,14 @@ function WPGoals(): JSX.Element {
}, [updateAstSelection],
);
+ React.useEffect(() => {
+ if (failed || !!scope) {
+ model.setFilter(filterGoal(failed, scope));
+ } else {
+ model.setFilter();
+ }
+ }, [model, scope, failed]);
+
return (
<Table
model={model}
@@ -96,16 +123,3 @@ function WPGoals(): JSX.Element {
}
/* -------------------------------------------------------------------------- */
-/* --- Goals Component --- */
-/* -------------------------------------------------------------------------- */
-
-Ivette.registerComponent({
- id: 'frama-c.plugins.wp.goals',
- group: 'frama-c.plugins',
- rank: 10,
- label: 'WP Goals',
- title: 'WP Generated Verification Conditions',
- children: <WPGoals />,
-});
-
-/* -------------------------------------------------------------------------- */
diff --git a/ivette/src/frama-c/plugins/wp/index.tsx b/ivette/src/frama-c/plugins/wp/index.tsx
index aa17e7478a6..9b6fd0efcde 100644
--- a/ivette/src/frama-c/plugins/wp/index.tsx
+++ b/ivette/src/frama-c/plugins/wp/index.tsx
@@ -24,13 +24,50 @@
// --- Eva Values
// --------------------------------------------------------------------------
+import React from 'react';
+import * as Dome from 'dome';
+import { IconButton } from 'dome/controls/buttons';
import * as Ivette from 'ivette';
-import './goals';
+import * as States from 'frama-c/states';
+import { GoalTable } from './goals';
import './style.css';
-// --------------------------------------------------------------------------
-// --- Export Component
-// --------------------------------------------------------------------------
+/* -------------------------------------------------------------------------- */
+/* --- Goal Component --- */
+/* -------------------------------------------------------------------------- */
+
+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 [selection] = States.useSelection();
+ const fct = selection?.current?.fct;
+ const scope = scoped ? fct : undefined;
+ return (
+ <>
+ <Ivette.TitleBar>
+ <IconButton icon='COMPONENT' title='Current Scope Only'
+ enabled={!!fct}
+ selected={scoped} onClick={flipScoped} />
+ <IconButton icon='CIRC.QUESTION' title='Unresolved Goals Only'
+ selected={failed} onClick={flipFailed} />
+ </Ivette.TitleBar>
+ <GoalTable scope={scope} failed={failed} />
+ </>
+ );
+}
+
+Ivette.registerComponent({
+ id: 'frama-c.plugins.wp.goals',
+ group: 'frama-c.plugins',
+ rank: 10,
+ label: 'WP Goals',
+ title: 'WP Generated Verification Conditions',
+ children: <WPGoals />,
+});
+
+/* -------------------------------------------------------------------------- */
+/* --- WP View --- */
+/* -------------------------------------------------------------------------- */
Ivette.registerView({
id: 'wp.main',
diff --git a/src/plugins/wp/wpApi.ml b/src/plugins/wp/wpApi.ml
index 95f1c92875a..7f63a336980 100644
--- a/src/plugins/wp/wpApi.ml
+++ b/src/plugins/wp/wpApi.ml
@@ -213,6 +213,10 @@ 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:"passed"
+ ~descr:(Md.plain "Valid or Passed goal")
+ ~data:(module D.Jbool) ~get:Wpo.is_passed
+
let () = S.column gmodel ~name:"status"
~descr:(Md.plain "Verdict, Status")
~data:(module STATUS) ~get:get_status
--
GitLab