From 0c9f1377fb888380f0f2318b43f9bd6e9c8b0cd2 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Mon, 14 Sep 2020 15:20:50 +0200
Subject: [PATCH] [wp] goal printer debug
---
src/plugins/wp/GuiSequent.ml | 2 +-
src/plugins/wp/Pcond.ml | 21 ++++++++++++---------
src/plugins/wp/Pcond.mli | 12 +++++++-----
src/plugins/wp/cfgDump.ml | 5 ++++-
src/plugins/wp/cfgWP.ml | 9 ++++++---
src/plugins/wp/wpPropId.ml | 16 +++++++++++++---
6 files changed, 43 insertions(+), 22 deletions(-)
diff --git a/src/plugins/wp/GuiSequent.ml b/src/plugins/wp/GuiSequent.ml
index 9576660cdd5..8792a599e94 100644
--- a/src/plugins/wp/GuiSequent.ml
+++ b/src/plugins/wp/GuiSequent.ml
@@ -341,7 +341,7 @@ class pcond
(focus : step_selection)
(plang : Pcond.state) =
object(self)
- inherit Pcond.sequence plang as super
+ inherit Pcond.seqengine plang as super
(* All displayed entries *)
val mutable domain = Vars.empty
diff --git a/src/plugins/wp/Pcond.ml b/src/plugins/wp/Pcond.ml
index 76ab4ae4970..c3fe43ec6ea 100644
--- a/src/plugins/wp/Pcond.ml
+++ b/src/plugins/wp/Pcond.ml
@@ -333,7 +333,7 @@ class engine (lang : #Plang.engine) =
let is_nop = function None -> true | Some(_,upd) -> Bag.is_empty upd
-class sequence (lang : #state) =
+class seqengine (lang : #state) =
object(self)
inherit engine lang as super
@@ -440,7 +440,7 @@ class sequence (lang : #state) =
let engine () =
if Wp_parameters.has_dkey dkey_state then
- ( new sequence (new state) :> engine )
+ ( new seqengine (new state) :> engine )
else
new engine (new Plang.engine)
@@ -449,15 +449,18 @@ let pretty fmt seq =
let () = Conditions.pretty := pretty
-let sequence ?(clause="Sequence") fmt seq =
+let dump_sequence ?(clause="Sequence") ?goal fmt seq =
let plang = new Plang.engine in
let pcond = new engine plang in
plang#global
- (fun () ->
- Vars.iter (fun x -> ignore (plang#bind x)) (Conditions.vars_hyp seq) ;
- pcond#pp_sequence ~clause fmt seq)
+ begin fun () ->
+ pcond#pp_block ~clause fmt seq ;
+ match goal with
+ | None -> ()
+ | Some g -> Format.fprintf fmt "@ @[<hov 2>Prove %a@]" plang#pp_pred g
+ end
-let bundle ?clause fmt bundle =
- sequence ?clause fmt (Conditions.bundle bundle)
+let dump_bundle ?clause ?goal fmt bundle =
+ dump_sequence ?clause ?goal fmt (Conditions.bundle bundle)
-let dump = bundle ~clause:"Bundle"
+let dump = dump_bundle ?goal:None ~clause:"Bundle"
diff --git a/src/plugins/wp/Pcond.mli b/src/plugins/wp/Pcond.mli
index ece9925515e..cb7c4c44b6f 100644
--- a/src/plugins/wp/Pcond.mli
+++ b/src/plugins/wp/Pcond.mli
@@ -23,16 +23,18 @@
open Qed.Plib
open Conditions
+open Lang.F
+
(** {2 All-in-one printers} *)
-val dump : bundle printer
-val bundle : ?clause:string -> bundle printer
-val sequence : ?clause:string -> sequence printer
val pretty : sequent printer
+val dump : bundle printer
+val dump_bundle : ?clause:string -> ?goal:pred -> bundle printer
+val dump_sequence : ?clause:string -> ?goal:pred -> sequence printer
+
(** {2 Low-level API} *)
-open Lang.F
type env = Plang.Env.t
val alloc_hyp : Plang.pool -> (var -> unit) -> sequence -> unit
@@ -103,7 +105,7 @@ class state :
method pp_value : Format.formatter -> term -> unit
end
-class sequence : #state ->
+class seqengine : #state ->
object
inherit engine
method set_sequence : Conditions.sequence -> unit
diff --git a/src/plugins/wp/cfgDump.ml b/src/plugins/wp/cfgDump.ml
index 90c0924ba5d..5fbdbfb4a42 100644
--- a/src/plugins/wp/cfgDump.ml
+++ b/src/plugins/wp/cfgDump.ml
@@ -121,6 +121,7 @@ struct
let add_assigns env (pid,_) k =
let u = node () in
Format.fprintf !out " %a [ color=red , label=\"Assigns %a\" ] ;@." pretty u WpPropId.pp_propid pid ;
+ Format.fprintf !out " %a -> %a [ style=dotted ] ;@." pretty u pretty k ;
merge env u k
let use_assigns _env _stmt region d k =
@@ -215,7 +216,9 @@ struct
(fun (_,p) -> Format.fprintf fmt "\n@[<hov 2>Requires %a ;@]"
Printer.pp_predicate p) pre
end ;
- ignore pre ; merge env u k
+ ignore pre ;
+ Format.fprintf !out " %a -> %a [ style=dotted ] ;@." pretty u pretty k ;
+ merge env u k
let call env stmt _r kf _es ~pre ~post ~pexit ~assigns ~p_post ~p_exit =
let u_post = List.fold_right (add_hyp env) post p_post in
diff --git a/src/plugins/wp/cfgWP.ml b/src/plugins/wp/cfgWP.ml
index 8a35afd310f..ddf5fcd5cd1 100644
--- a/src/plugins/wp/cfgWP.ml
+++ b/src/plugins/wp/cfgWP.ml
@@ -101,6 +101,10 @@ struct
struct
type t = effect
let compare e1 e2 = P.compare e1.e_pid e2.e_pid
+ let pretty fmt e =
+ Format.fprintf fmt "@[<hov 2>EFFECT %a:@ %a@]"
+ P.pretty e.e_pid (Cvalues.pp_region M.pretty) e.e_region
+ [@@ warning "-32"]
end
module G = Qed.Collection.Make(TARGET)
@@ -140,9 +144,8 @@ struct
(* -------------------------------------------------------------------------- *)
let pp_vc fmt vc =
- Format.fprintf fmt "%a@ @[<hov 2>Prove %a@]"
- Pcond.dump vc.hyps
- F.pp_pred vc.goal
+ Format.fprintf fmt "%a"
+ (Pcond.dump_bundle ~clause:"Context" ~goal:vc.goal) vc.hyps
let pp_vcs fmt vcs =
let k = ref 0 in
diff --git a/src/plugins/wp/wpPropId.ml b/src/plugins/wp/wpPropId.ml
index ec5d88cd371..22988574935 100644
--- a/src/plugins/wp/wpPropId.ml
+++ b/src/plugins/wp/wpPropId.ml
@@ -230,7 +230,7 @@ let compare_prop_id pid1 pid2 =
else
Stdlib.compare pid1.p_part pid2.p_part
-module PropId =
+module PropIdRaw =
Datatype.Make_with_collections(
struct
type t = prop_id
@@ -356,7 +356,7 @@ end = struct
in normalize_basename basename
- module UniquifyPropId = NameUniquify(PropId)(struct
+ module UniquifyPropId = NameUniquify(PropIdRaw)(struct
let name = "WpProperty"
let basename = get_prop_id_basename
end)
@@ -435,7 +435,7 @@ struct
if n < 1000 then Printf.sprintf "%s_part%03d" basename (succ k) else
Printf.sprintf "%s_part%06d" basename (succ k)
- module Uniquify2 = NameUniquify(PropId)(struct
+ module Uniquify2 = NameUniquify(PropIdRaw)(struct
let name = "Wp.WpPropId.Names2."
let basename = get_prop_id_basename
end)
@@ -573,6 +573,16 @@ end
let pretty_local = Pretty.pp_local
+(* -------------------------------------------------------------------------- *)
+(* --- Datatype --- *)
+(* -------------------------------------------------------------------------- *)
+
+module PropId =
+struct
+ include PropIdRaw
+ let pretty = pp_propid
+end
+
(* -------------------------------------------------------------------------- *)
(* --- Hints --- *)
(* -------------------------------------------------------------------------- *)
--
GitLab