From b2788456496e0d39640a86800d1b07a429106283 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Wed, 27 Mar 2024 15:15:00 +0100
Subject: [PATCH] [ivette/wp] marker menu for running proofs
---
ivette/src/frama-c/kernel/ASTview.tsx | 2 ++
ivette/src/frama-c/plugins/wp/api/index.ts | 10 ++++++
ivette/src/frama-c/plugins/wp/index.tsx | 23 ++++++++++++++
src/plugins/wp/wpApi.ml | 36 ++++++++++++++++++++++
4 files changed, 71 insertions(+)
diff --git a/ivette/src/frama-c/kernel/ASTview.tsx b/ivette/src/frama-c/kernel/ASTview.tsx
index 54583eb3d7b..1219c382ae2 100644
--- a/ivette/src/frama-c/kernel/ASTview.tsx
+++ b/ivette/src/frama-c/kernel/ASTview.tsx
@@ -30,6 +30,7 @@ import * as States from 'frama-c/states';
import * as Settings from 'dome/data/settings';
import { IconButton } from 'dome/controls/buttons';
import * as Studia from 'frama-c/plugins/studia';
+import * as Wp from 'frama-c/plugins/wp';
import * as Ast from 'frama-c/kernel/api/ast';
import { text } from 'frama-c/kernel/api/data';
import * as Eva from 'frama-c/plugins/eva/api/general';
@@ -546,6 +547,7 @@ function createContextMenuHandler(): Editor.Extension {
});
}
Studia.buildMenu(items, attributes);
+ Wp.buildMenu(items, attributes);
items.push({
label: 'Copy to clipboard',
onClick: () => {
diff --git a/ivette/src/frama-c/plugins/wp/api/index.ts b/ivette/src/frama-c/plugins/wp/api/index.ts
index 031e5b95806..a8d5905b164 100644
--- a/ivette/src/frama-c/plugins/wp/api/index.ts
+++ b/ivette/src/frama-c/plugins/wp/api/index.ts
@@ -485,6 +485,16 @@ export const goalsDataDefault: goalsData =
name: '', smoke: false, passed: false, status: statusDefault,
stats: statsDefault, proof: false, script: undefined, saved: false };
+const startProofs_internal: Server.ExecRequest<marker,null> = {
+ kind: Server.RqKind.EXEC,
+ name: 'plugins.wp.startProofs',
+ input: jMarker,
+ output: Json.jNull,
+ signals: [],
+};
+/** Generate goals and run provers */
+export const startProofs: Server.ExecRequest<marker,null>= startProofs_internal;
+
/** Proof Server Activity */
export const serverActivity: Server.Signal = {
name: 'plugins.wp.serverActivity',
diff --git a/ivette/src/frama-c/plugins/wp/index.tsx b/ivette/src/frama-c/plugins/wp/index.tsx
index 98868917fde..f774d664d49 100644
--- a/ivette/src/frama-c/plugins/wp/index.tsx
+++ b/ivette/src/frama-c/plugins/wp/index.tsx
@@ -33,11 +33,34 @@ import { Group, Inset } from 'dome/frame/toolbars';
import * as Ivette from 'ivette';
import * as Server from 'frama-c/server';
import * as States from 'frama-c/states';
+import * as Ast from 'frama-c/kernel/api/ast';
import { GoalTable } from './goals';
import { TIPView } from './tip';
import * as WP from 'frama-c/plugins/wp/api';
import './style.css';
+/* -------------------------------------------------------------------------- */
+/* --- Generate Goals --- */
+/* -------------------------------------------------------------------------- */
+
+export function buildMenu(
+ menu: Dome.PopupMenuItem[],
+ attr: Ast.markerAttributesData,
+): void {
+ const { marker, kind } = attr;
+ switch (kind) {
+ case 'STMT':
+ case 'LFUN':
+ case 'DFUN':
+ case 'PROPERTY':
+ menu.push({
+ label: `Generate WP Goals`,
+ onClick: () => Server.send(WP.startProofs, marker)
+ });
+ return;
+ }
+}
+
/* -------------------------------------------------------------------------- */
/* --- Goal Component --- */
/* -------------------------------------------------------------------------- */
diff --git a/src/plugins/wp/wpApi.ml b/src/plugins/wp/wpApi.ml
index 71e7be36bbf..bfa4b231fbc 100644
--- a/src/plugins/wp/wpApi.ml
+++ b/src/plugins/wp/wpApi.ml
@@ -381,6 +381,42 @@ let goals =
~add_reload_hook
gmodel
+(* -------------------------------------------------------------------------- *)
+(* --- Generate goals --- *)
+(* -------------------------------------------------------------------------- *)
+
+let is_call stmt =
+ match stmt.Cil_types.skind with
+ | Instr (Call _) | Instr (Local_init (_, ConsInit _, _)) -> true
+ | _ -> false
+
+let () =
+ R.register ~package ~kind:`EXEC ~name:"startProofs"
+ ~descr:(Md.plain "Generate goals and run provers")
+ ~input:(module AST.Marker)
+ ~output:(module D.Junit)
+ begin function
+ | PExp _ | PTermLval _ | PLval _
+ | PGlobal _ | PType _ | PVDecl (None, _, _) ->
+ (* We cannot run anything here *) ()
+ | PStmtStart (_, stmt) | PStmt (_, stmt) when is_call stmt ->
+ VC.command @@ VC.generate_call stmt
+ | PStmtStart (kf, stmt) | PStmt (kf, stmt) ->
+ let fold_ips _ ca bag =
+ let ids = WpPropId.mk_code_annot_ids kf stmt ca in
+ let props = Bag.ulist @@
+ List.map VC.generate_ip @@
+ List.map WpPropId.property_of_id ids
+ in
+ Bag.concat bag props
+ in
+ VC.command @@ Annotations.fold_code_annot fold_ips stmt Bag.empty
+ | PVDecl (Some kf, _, _) ->
+ VC.command @@ VC.generate_kf kf
+ | PIP property ->
+ VC.command @@ VC.generate_ip property
+ end
+
(* -------------------------------------------------------------------------- *)
(* --- Proof Server --- *)
(* -------------------------------------------------------------------------- *)
--
GitLab