From 6d8e39e99adc3cf3f5d377233e5765a5a3ea7379 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Mon, 6 Feb 2023 16:59:22 +0100
Subject: [PATCH] [wp/server] proof node & proof tree
---
ivette/src/frama-c/plugins/wp/api/index.ts | 69 ++++++++++++++--
src/plugins/wp/ProofEngine.ml | 14 ++++
src/plugins/wp/ProofEngine.mli | 10 +++
src/plugins/wp/wpApi.ml | 93 ++++++++++++++++++++--
4 files changed, 173 insertions(+), 13 deletions(-)
diff --git a/ivette/src/frama-c/plugins/wp/api/index.ts b/ivette/src/frama-c/plugins/wp/api/index.ts
index 4e945ba0c77..bd48d1e056b 100644
--- a/ivette/src/frama-c/plugins/wp/api/index.ts
+++ b/ivette/src/frama-c/plugins/wp/api/index.ts
@@ -144,8 +144,6 @@ export interface goalsData {
passed: boolean;
/** Verdict Details */
stats: stats;
- /** Prover Results */
- results: [ prover, result ][];
}
/** Decoder for `goalsData` */
@@ -160,7 +158,6 @@ export const jGoalsData: Json.Decoder<goalsData> =
smoke: Json.jBoolean,
passed: Json.jBoolean,
stats: jStats,
- results: Json.jArray(Json.jPair( jProver, jResult,)),
});
/** Natural order for `goalsData` */
@@ -168,7 +165,7 @@ export const byGoalsData: Compare.Order<goalsData> =
Compare.byFields
<{ wpo: Json.key<'#wpo'>, property: marker, name: string,
fct?: Json.key<'#fct'>, bhv?: string, thy?: string, smoke: boolean,
- passed: boolean, stats: stats, results: [ prover, result ][] }>({
+ passed: boolean, stats: stats }>({
wpo: Compare.string,
property: byMarker,
name: Compare.string,
@@ -178,7 +175,6 @@ export const byGoalsData: Compare.Order<goalsData> =
smoke: Compare.boolean,
passed: Compare.boolean,
stats: byStats,
- results: Compare.array(Compare.pair(byProver,byResult,)),
});
/** Signal for array [`goals`](#goals) */
@@ -266,4 +262,67 @@ const cancelProofTasks_internal: Server.SetRequest<null,null> = {
/** Cancel all scheduled proof tasks. */
export const cancelProofTasks: Server.SetRequest<null,null>= cancelProofTasks_internal;
+/** Proof Status has changed */
+export const proofStatus: Server.Signal = {
+ name: 'plugins.wp.proofStatus',
+};
+
+const getNodeInfos_internal: Server.GetRequest<
+ Json.index<'#node'>,
+ { stats: string, size: number, pending: number, proved: boolean,
+ result: string }
+ > = {
+ kind: Server.RqKind.GET,
+ name: 'plugins.wp.getNodeInfos',
+ input: Json.jIndex<'#node'>('#node'),
+ output: Json.jObject({
+ stats: Json.jString,
+ size: Json.jNumber,
+ pending: Json.jNumber,
+ proved: Json.jBoolean,
+ result: Json.jString,
+ }),
+ signals: [ { name: 'plugins.wp.proofStatus' },
+ { name: 'plugins.wp.signalGoals' } ],
+};
+/** Proof node information */
+export const getNodeInfos: Server.GetRequest<
+ Json.index<'#node'>,
+ { stats: string, size: number, pending: number, proved: boolean,
+ result: string }
+ >= getNodeInfos_internal;
+
+const getProofState_internal: Server.GetRequest<
+ goal,
+ { children: [ string, Json.index<'#node'> ][], tactic: string,
+ results: [ prover, result ][], index: number, pending: number,
+ parents: Json.index<'#node'>[], current: Json.index<'#node'> }
+ > = {
+ kind: Server.RqKind.GET,
+ name: 'plugins.wp.getProofState',
+ input: jGoal,
+ output: Json.jObject({
+ children: Json.jArray(
+ Json.jPair(
+ Json.jString,
+ Json.jIndex<'#node'>('#node'),
+ )),
+ tactic: Json.jString,
+ results: Json.jArray(Json.jPair( jProver, jResult,)),
+ index: Json.jNumber,
+ pending: Json.jNumber,
+ parents: Json.jArray(Json.jIndex<'#node'>('#node')),
+ current: Json.jIndex<'#node'>('#node'),
+ }),
+ signals: [ { name: 'plugins.wp.proofStatus' },
+ { name: 'plugins.wp.signalGoals' } ],
+};
+/** Current Proof Status of a Goal */
+export const getProofState: Server.GetRequest<
+ goal,
+ { children: [ string, Json.index<'#node'> ][], tactic: string,
+ results: [ prover, result ][], index: number, pending: number,
+ parents: Json.index<'#node'>[], current: Json.index<'#node'> }
+ >= getProofState_internal;
+
/* ------------------------------------- */
diff --git a/src/plugins/wp/ProofEngine.ml b/src/plugins/wp/ProofEngine.ml
index bb9af717ec9..18afa7f14d7 100644
--- a/src/plugins/wp/ProofEngine.ml
+++ b/src/plugins/wp/ProofEngine.ml
@@ -39,6 +39,15 @@ and script =
| Script of ProofScript.jscript (* to replay *)
| Tactic of ProofScript.jtactic * (string * node) list (* played *)
+module Node =
+struct
+ type t = node
+ let hash t = Wpo.S.hash t.goal
+ let equal a b = Wpo.S.equal a.goal b.goal
+ let compare a b = Wpo.S.compare a.goal b.goal
+ let pretty fmt a = Wpo.S.pretty fmt a.goal
+end
+
type tree = {
main : Wpo.t ; (* Main goal to be proved. *)
mutable pool : Lang.F.pool option ; (* Global pool variable *)
@@ -344,6 +353,11 @@ let mk_root ~tree =
tree.head <- root ;
node
+let root tree =
+ match tree.root with
+ | Some node -> node
+ | None -> mk_root ~tree
+
(* -------------------------------------------------------------------------- *)
(* --- Forking --- *)
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/ProofEngine.mli b/src/plugins/wp/ProofEngine.mli
index f009fd7c28e..eb17cd87687 100644
--- a/src/plugins/wp/ProofEngine.mli
+++ b/src/plugins/wp/ProofEngine.mli
@@ -30,6 +30,15 @@ type tree
(** A proof node *)
type node
+module Node :
+sig
+ type t = node
+ val hash : t -> int
+ val equal : t -> t -> bool
+ val compare : t -> t -> int
+ val pretty : Format.formatter -> t -> unit
+end
+
val get : Wpo.t -> [ `Script | `Proof | `Saved | `None ]
val proof : main:Wpo.t -> tree
val reset : tree -> unit
@@ -62,6 +71,7 @@ val status : tree -> status
val current : tree -> current
val goto : tree -> position -> unit
+val root : tree -> node
val main : tree -> Wpo.t
val head : tree -> Wpo.t
val goal : node -> Wpo.t
diff --git a/src/plugins/wp/wpApi.ml b/src/plugins/wp/wpApi.ml
index 879866c429b..1288c3437da 100644
--- a/src/plugins/wp/wpApi.ml
+++ b/src/plugins/wp/wpApi.ml
@@ -47,7 +47,7 @@ module INDEX = State_builder.Ref
let mem_project = Datatype.never_any_project
end))
(struct
- let name = "WpAPpi.INDEX"
+ let name = "WpApi.INDEX"
let dependencies = [ Ast.self ]
let default () = Hashtbl.create 0
end)
@@ -198,13 +198,7 @@ let () = S.column gmodel ~name:"stats"
~descr:(Md.plain "Verdict Details")
~data:(module STATS) ~get:get_stats
-(*TODO: remove this field! *)
-let () = S.column gmodel ~name:"results"
- ~descr:(Md.plain "Prover Results")
- ~data:(module D.Jlist(D.Jpair(PROVER)(RESULT)))
- ~get:Wpo.get_results
-
-let _garray = S.register_array ~package ~name:"goals"
+let garray = S.register_array ~package ~name:"goals"
~descr:(Md.plain "Generated Goals")
~key:(fun g -> g.Wpo.po_gid)
~keyName:"wpo"
@@ -261,3 +255,86 @@ let () = R.register ~package ~kind:`SET ~name:"cancelProofTasks"
(fun () -> let server = ProverTask.server () in Task.cancel_all server)
(* -------------------------------------------------------------------------- *)
+(* --- Proof Node --- *)
+(* -------------------------------------------------------------------------- *)
+
+let proofStatus = R.signal ~package ~name:"proofStatus"
+ ~descr:(Md.plain "Proof Status has changed")
+
+module NODE = D.Index(Map.Make(ProofEngine.Node))(struct let name = "node" end)
+
+let () =
+ let snode = R.signature ~input:(module NODE) () in
+ let set_title = R.result snode ~name:"result"
+ ~descr:(Md.plain "Proof node title") (module D.Jstring) in
+ let set_proved = R.result snode ~name:"proved"
+ ~descr:(Md.plain "Proof node complete") (module D.Jbool) in
+ let set_pending = R.result snode ~name:"pending"
+ ~descr:(Md.plain "Pending children") (module D.Jint) in
+ let set_size = R.result snode ~name:"size"
+ ~descr:(Md.plain "Proof size") (module D.Jint) in
+ let set_stats = R.result snode ~name:"stats"
+ ~descr:(Md.plain "Node statistics") (module D.Jstring) in
+ R.register_sig ~package ~kind:`GET ~name:"getNodeInfos"
+ ~descr:(Md.plain "Proof node information") snode
+ ~signals:[proofStatus;S.signal garray]
+ begin fun rq node ->
+ set_title rq (ProofEngine.title node) ;
+ set_proved rq (ProofEngine.proved node) ;
+ set_pending rq (ProofEngine.pending node) ;
+ let s = ProofEngine.stats node in
+ set_size rq (Stats.proofs s) ;
+ set_stats rq (Pretty_utils.to_string Stats.pretty s) ;
+ end
+
+(* -------------------------------------------------------------------------- *)
+(* --- Proof Tree --- *)
+(* -------------------------------------------------------------------------- *)
+
+let () =
+ let state = R.signature ~input:(module WPO) () in
+ let set_current = R.result state ~name:"current"
+ ~descr:(Md.plain "Current proof node.") (module NODE) in
+ let set_parents = R.result state ~name:"parents"
+ ~descr:(Md.plain "Proof node parents.") (module D.Jlist(NODE)) in
+ let set_pending = R.result state ~name:"pending"
+ ~descr:(Md.plain "Pending proof nodes.") (module D.Jint) in
+ let set_index = R.result state ~name:"index"
+ ~descr:(Md.plain "Current node index among pending nodes (else -1)")
+ (module D.Jint) in
+ let set_results = R.result state ~name:"results"
+ ~descr:(Md.plain "Prover results for current node")
+ (module D.Jlist(D.Jpair(PROVER)(RESULT))) in
+ let set_tactic = R.result state ~name:"tactic"
+ ~descr:(Md.plain "Proof node tactic header (if any)")
+ (module D.Jstring) in
+ let set_children = R.result state ~name:"children"
+ ~descr:(Md.plain "Proof node tactic children (id any)")
+ (module D.Jlist(D.Jpair(D.Jstring)(NODE))) in
+ R.register_sig ~package
+ ~kind:`GET ~name:"getProofState"
+ ~descr:(Md.plain "Current Proof Status of a Goal") state
+ ~signals:[proofStatus;S.signal garray]
+ begin fun rq wpo ->
+ let tree = ProofEngine.proof ~main:wpo in
+ let current,index =
+ match ProofEngine.current tree with
+ | `Main -> ProofEngine.root tree,-1
+ | `Internal node -> node,-1
+ | `Leaf(idx,node) -> node,idx in
+ let rec parents node = match ProofEngine.parent node with
+ | None -> []
+ | Some p -> p::parents p in
+ let tactic = match ProofEngine.tactical current with
+ | None -> ""
+ | Some { header } -> header in
+ set_current rq current ;
+ set_parents rq (parents current) ;
+ set_index rq index ;
+ set_pending rq (ProofEngine.pending current) ;
+ set_results rq (Wpo.get_results (ProofEngine.goal current)) ;
+ set_tactic rq tactic ;
+ set_children rq (ProofEngine.children current) ;
+ end
+
+(* -------------------------------------------------------------------------- *)
--
GitLab