Skip to content
Snippets Groups Projects
Commit bfca79bb authored by Loïc Correnson's avatar Loïc Correnson
Browse files

[wp/cache] moving scripts in <session>/script

parent 4fc5be8a
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 123 additions and 55 deletions
src/plugins/wp/GuiProof.ml
+ 2
− 2
View file @ bfca79bb
......@@ -194,10 +194,10 @@ class printer (text : Wtext.text) =
| `Proof ->
text#printf "@{<it>Existing Script (navigate to explore)@}@."
| `Script ->
text#printf "[File '%s']@." (ProofSession.filename wpo) ;
text#printf "[%a]@." ProofSession.pp_goal wpo ;
text#printf "@{<it>Existing Script (replay to explore)@}@."
| `Saved ->
text#printf "[File '%s']@." (ProofSession.filename wpo) ;
text#printf "[%a]@." ProofSession.pp_goal wpo ;
text#printf "@{<it>Saved Script (replay to load)@}@."
| `None ->
text#printf "@{<it>No Script@}@."
......
src/plugins/wp/ProofSession.ml
+ 25
− 11
View file @ bfca79bb
......@@ -29,12 +29,17 @@ type status =
let files : (string,status) Hashtbl.t = Hashtbl.create 32
let filename ?(legacy=false) wpo =
let filename wpo =
let d = Wp_parameters.get_session_dir "script" in
Printf.sprintf "%s/%s.json" d wpo.po_gid
let legacies wpo =
let m = WpContext.MODEL.id wpo.po_model in
let d = Wp_parameters.get_session_dir m in
Printf.sprintf "%s/%s.json" d (if legacy then wpo.po_leg else wpo.po_gid)
let pretty fmt wpo = Format.pp_print_string fmt (filename wpo)
List.map (Printf.sprintf "%s/%s.json" d) [
wpo.po_gid ;
wpo.po_leg ;
]
let status wpo =
let f = filename wpo in
......@@ -42,13 +47,22 @@ let status wpo =
with Not_found ->
let status =
if Sys.file_exists f then Script f else
let f' = filename ~legacy:true wpo in
if Sys.file_exists f' then
( Wp_parameters.warning ~current:false
"Deprecated script for '%s'" wpo.po_sid ;
Deprecated f' )
else NoScript in
Hashtbl.add files f status ; status
try
let f' = List.find Sys.file_exists (legacies wpo) in
Wp_parameters.warning ~current:false
"Deprecated script for '%s'" wpo.po_sid ;
Deprecated f'
with Not_found -> NoScript
in Hashtbl.add files f status ; status
let pp_file fmt s = Filepath.Normalized.(pretty fmt (of_string s))
let pp_status fmt = function
| NoScript -> Format.pp_print_string fmt "no script file"
| Script f -> Format.fprintf fmt "script '%a'" pp_file f
| Deprecated f -> Format.fprintf fmt "script '%a' (deprecated)" pp_file f
let pp_goal fmt wpo = pp_status fmt (status wpo)
let exists wpo =
match status wpo with NoScript -> false | Script _ | Deprecated _ -> true
......
src/plugins/wp/ProofSession.mli
+ 10
− 2
View file @ bfca79bb
......@@ -20,8 +20,16 @@
(* *)
(**************************************************************************)
val pretty : Format.formatter -> Wpo.t -> unit
val filename : ?legacy:bool -> Wpo.t -> string
type status =
| NoScript
| Script of string
| Deprecated of string
val pp_status : Format.formatter -> status -> unit
val pp_goal : Format.formatter -> Wpo.t -> unit
val status : Wpo.t -> status
val exists : Wpo.t -> bool
val save : Wpo.t -> Json.t -> unit
val load : Wpo.t -> Json.t
......
src/plugins/wp/tests/wp_plugin/oracle_qualif/unroll.0.session/script/typed_unrolled_loop_ensures_zero.json 0 → 100644
+ 54
− 0
View file @ bfca79bb
[ { "header": "Definition", "tactic": "Wp.unfold", "params": {},
"select": { "select": "clause-goal",
"target": "(P_zeroed\n Mint_37[(shift_uint32 t_2 0)->0][(shift_uint32 t_2 1)->0]\n [(shift_uint32 t_2 2)->0][(shift_uint32 t_2 3)->0][(shift_uint32 t_2 4)\n ->0][(shift_uint32 t_2 5)->0][(shift_uint32 t_2 6)->0]\n [(shift_uint32 t_2 7)->0][(shift_uint32 t_2 8)->0][(shift_uint32 t_2 9)\n ->0][(shift_uint32 t_2 10)->0][(shift_uint32 t_2 11)->0]\n [(shift_uint32 t_2 12)->0][(shift_uint32 t_2 13)->0]\n [(shift_uint32 t_2 14)->0][(shift_uint32 t_2 15)->0] t_2 0 15)",
"pattern": "P_zeroed[=]$t015[=]shift_uint320" },
"children": { "Unfold 'P_zeroed'": [ { "header": "Range",
"tactic": "Wp.range",
"params": { "inf": 0, "sup": 15 },
"select": { "select": "inside-goal",
"occur": 0,
"target": "i_0",
"pattern": "$i" },
"children": { "Lower 0": [ { "prover": "qed",
"verdict": "valid" } ],
"Value 0": [ { "prover": "qed",
"verdict": "valid" } ],
"Value 1": [ { "prover": "qed",
"verdict": "valid" } ],
"Value 2": [ { "prover": "qed",
"verdict": "valid" } ],
"Value 3": [ { "prover": "qed",
"verdict": "valid" } ],
"Value 4": [ { "prover": "qed",
"verdict": "valid" } ],
"Value 5": [ { "prover": "qed",
"verdict": "valid" } ],
"Value 6": [ { "prover": "qed",
"verdict": "valid" } ],
"Value 7": [ { "prover": "qed",
"verdict": "valid" } ],
"Value 8": [ { "prover": "qed",
"verdict": "valid" } ],
"Value 9": [ { "prover": "qed",
"verdict": "valid" } ],
"Value 10":
[ { "prover": "qed",
"verdict": "valid" } ],
"Value 11":
[ { "prover": "qed",
"verdict": "valid" } ],
"Value 12":
[ { "prover": "qed",
"verdict": "valid" } ],
"Value 13":
[ { "prover": "qed",
"verdict": "valid" } ],
"Value 14":
[ { "prover": "qed",
"verdict": "valid" } ],
"Value 15":
[ { "prover": "qed",
"verdict": "valid" } ],
"Upper 15":
[ { "prover": "qed",
"verdict": "valid" } ] } } ] } } ]
src/plugins/wp/tests/wp_plugin/oracle_qualif/unroll.0.session/typed/typed_unrolled_loop_ensures_zero.json deleted 100644 → 0
+ 0
− 12
View file @ 4fc5be8a
[ { "header": "Definition", "tactic": "Wp.unfold", "params": {},
"select": { "select": "clause-goal",
"target": "(P_zeroed\n Mint_37[(shift_uint32 t_2 0)->0][(shift_uint32 t_2 1)->0]\n [(shift_uint32 t_2 2)->0][(shift_uint32 t_2 3)->0][(shift_uint32 t_2 4)\n ->0][(shift_uint32 t_2 5)->0][(shift_uint32 t_2 6)->0]\n [(shift_uint32 t_2 7)->0][(shift_uint32 t_2 8)->0][(shift_uint32 t_2 9)\n ->0][(shift_uint32 t_2 10)->0][(shift_uint32 t_2 11)->0]\n [(shift_uint32 t_2 12)->0][(shift_uint32 t_2 13)->0]\n [(shift_uint32 t_2 14)->0][(shift_uint32 t_2 15)->0] t_2 0 15)",
"pattern": "P_zeroed[=]$t015[=]shift_uint320" },
"children": { "Unfold 'P_zeroed'": [ { "header": "Range",
"tactic": "Wp.range",
"params": { "inf": 0, "sup": 15 },
"select": { "select": "inside-goal",
"occur": 0,
"target": "i_0",
"pattern": "$i" },
"children": {} } ] } } ]
\ No newline at end of file
src/plugins/wp/tests/wp_plugin/oracle_qualif/unsigned.0.session/typed/typed_lemma_U32.json → src/plugins/wp/tests/wp_plugin/oracle_qualif/unsigned.0.session/script/typed_lemma_U32.json
+ 14
− 10
View file @ bfca79bb
......@@ -8,21 +8,25 @@
"select": { "select": "clause-goal",
"target": "(0<=x_0) /\\ (0<=(land 4294967295 x_0)) /\\ (x_0<=4294967295)",
"pattern": "&<=<=<=0$x0land$x42949672954294967295" },
"children": { "Goal 1/3": [ { "prover": "alt-ergo",
"children": { "Goal 1/3": [ { "prover": "why3:Alt-Ergo,2.0.0",
"verdict": "valid",
"time": 0.0087,
"steps": 7 } ],
"time": 0.0103,
"steps": 10 } ],
"Goal 2/3": [ { "header": "Bit Range",
"tactic": "Wp.bitrange",
"params": {},
"params":
{ "positive-land": true,
"positive-lor": true },
"select":
{ "select": "clause-goal",
"target": "0<=(land 4294967295 x_0)",
"pattern": "<=0land4294967295$x" },
"children": {} } ],
"Goal 3/3": [ { "prover": "alt-ergo",
"children":
{ "bit-range":
[ { "prover": "qed",
"verdict": "valid" } ] } } ],
"Goal 3/3": [ { "prover": "why3:Alt-Ergo,2.0.0",
"verdict": "valid",
"time": 0.0073,
"steps": 7 } ] } } ],
"bitwise": [ { "prover": "alt-ergo", "verdict": "valid",
"time": 0.0167, "steps": 10 } ] } } ]
\ No newline at end of file
"time": 0.0105,
"steps": 10 } ] } } ],
"bitwise": [ { "prover": "qed", "verdict": "valid" } ] } } ]
src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/typed/typed_init_t2_bis_v2_assigns_exit_part2.json → src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/typed_init_t2_bis_v2_assigns_exit_part2.json
+ 2
− 2
View file @ bfca79bb
......@@ -3,8 +3,8 @@
"target": "exists i_0,i_1:int.\n(i_0<=i_102) /\\ (i_1<=i_103) /\\ (0<=i_0) /\\ (i_102<=i_0) /\\ (i_103<=i_1)\n/\\ (i_0<=9)",
"pattern": "\\E\\E&<=<=<=<=<=<=#1$i#0$i0#1$i#1" },
"children": { "Goal 1/2": [ { "prover": "why3:Alt-Ergo,2.0.0",
"verdict": "valid", "time": 0.0174,
"verdict": "valid", "time": 0.0117,
"steps": 12 } ],
"Goal 2/2": [ { "prover": "why3:Alt-Ergo,2.0.0",
"verdict": "valid", "time": 0.0186,
"verdict": "valid", "time": 0.0125,
"steps": 16 } ] } } ]
src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/typed/typed_init_t2_bis_v2_assigns_normal_part2.json → src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/typed_init_t2_bis_v2_assigns_normal_part2.json
+ 2
− 2
View file @ bfca79bb
......@@ -3,8 +3,8 @@
"target": "exists i_0,i_1:int.\n(i_0<=i_102) /\\ (i_1<=i_103) /\\ (0<=i_0) /\\ (i_102<=i_0) /\\ (i_103<=i_1)\n/\\ (i_0<=9)",
"pattern": "\\E\\E&<=<=<=<=<=<=#1$i#0$i0#1$i#1" },
"children": { "Goal 1/2": [ { "prover": "why3:Alt-Ergo,2.0.0",
"verdict": "valid", "time": 0.0183,
"verdict": "valid", "time": 0.0107,
"steps": 12 } ],
"Goal 2/2": [ { "prover": "why3:Alt-Ergo,2.0.0",
"verdict": "valid", "time": 0.0199,
"verdict": "valid", "time": 0.0125,
"steps": 16 } ] } } ]
src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/typed/typed_init_t2_bis_v2_loop_assigns_part2.json → src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/typed_init_t2_bis_v2_loop_assigns_part2.json
+ 2
− 2
View file @ bfca79bb
......@@ -3,8 +3,8 @@
"target": "exists i_0,i_1:int.\n(i_0<=i_9) /\\ (i_1<=i_10) /\\ (0<=i_0) /\\ (i_9<=i_0) /\\ (i_10<=i_1)\n/\\ (i_0<=9)",
"pattern": "\\E\\E&<=<=<=<=<=<=#1$i#0$i0#1$i#1" },
"children": { "Goal 1/2": [ { "prover": "why3:Alt-Ergo,2.0.0",
"verdict": "valid", "time": 0.0242,
"verdict": "valid", "time": 0.015,
"steps": 22 } ],
"Goal 2/2": [ { "prover": "why3:Alt-Ergo,2.0.0",
"verdict": "valid", "time": 0.0275,
"verdict": "valid", "time": 0.0175,
"steps": 28 } ] } } ]
src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/typed/typed_init_t2_bis_v2_loop_assigns_part3.json → src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/typed_init_t2_bis_v2_loop_assigns_part3.json
+ 2
− 2
View file @ bfca79bb
......@@ -3,8 +3,8 @@
"target": "exists i_1,i_2:int.\n(i_1<=i_0) /\\ (i_2<=i_3) /\\ (0<=i_1) /\\ (i_0<=i_1) /\\ (i_3<=i_2) /\\ (i_1<=9)",
"pattern": "\\E\\E&<=<=<=<=<=<=#1$i#0$i0#1$i#1" },
"children": { "Goal 1/2": [ { "prover": "why3:Alt-Ergo,2.0.0",
"verdict": "valid", "time": 0.0244,
"verdict": "valid", "time": 0.0183,
"steps": 16 } ],
"Goal 2/2": [ { "prover": "why3:Alt-Ergo,2.0.0",
"verdict": "valid", "time": 0.0246,
"verdict": "valid", "time": 0.0203,
"steps": 22 } ] } } ]
src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/typed/typed_init_t2_v2_assigns_part2.json → src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/typed_init_t2_v2_assigns_part2.json
+ 2
− 2
View file @ bfca79bb
......@@ -3,8 +3,8 @@
"target": "exists i_0,i_1:int.\n(i_0<=i_156) /\\ (i_1<=i_157) /\\ (0<=i_0) /\\ (i_156<=i_0) /\\ (i_157<=i_1)\n/\\ (i_0<=9)",
"pattern": "\\E\\E&<=<=<=<=<=<=#1$i#0$i0#1$i#1" },
"children": { "Goal 1/2": [ { "prover": "why3:Alt-Ergo,2.0.0",
"verdict": "valid", "time": 0.0083,
"verdict": "valid", "time": 0.0068,
"steps": 9 } ],
"Goal 2/2": [ { "prover": "why3:Alt-Ergo,2.0.0",
"verdict": "valid", "time": 0.0075,
"verdict": "valid", "time": 0.0069,
"steps": 11 } ] } } ]
src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/typed/typed_init_t2_v2_loop_assigns_2_part2.json → src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/typed_init_t2_v2_loop_assigns_2_part2.json
+ 2
− 2
View file @ bfca79bb
......@@ -3,8 +3,8 @@
"target": "exists i_0,i_1:int.\n(i_0<=i_13) /\\ (i_1<=i_14) /\\ (0<=i_0) /\\ (i_13<=i_0) /\\ (i_14<=i_1)\n/\\ (i_0<=9)",
"pattern": "\\E\\E&<=<=<=<=<=<=#1$i#0$i0#1$i#1" },
"children": { "Goal 1/2": [ { "prover": "why3:Alt-Ergo,2.0.0",
"verdict": "valid", "time": 0.0113,
"verdict": "valid", "time": 0.0097,
"steps": 22 } ],
"Goal 2/2": [ { "prover": "why3:Alt-Ergo,2.0.0",
"verdict": "valid", "time": 0.0127,
"verdict": "valid", "time": 0.0112,
"steps": 24 } ] } } ]
src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/typed/typed_init_t2_v2_loop_assigns_2_part3.json → src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/typed_init_t2_v2_loop_assigns_2_part3.json
+ 2
− 2
View file @ bfca79bb
......@@ -3,8 +3,8 @@
"target": "exists i_0,i_2:int.\n(i_0<=i_1) /\\ (0<=i_0) /\\ (i_1<=i_0) /\\ (j_0<=i_2) /\\ (i_2<=j_0) /\\ (i_0<=9)",
"pattern": "\\E\\E&<=<=<=<=<=<=#1$i0#1$i#1$j#0" },
"children": { "Goal 1/2": [ { "prover": "why3:Alt-Ergo,2.0.0",
"verdict": "valid", "time": 0.0106,
"verdict": "valid", "time": 0.0099,
"steps": 14 } ],
"Goal 2/2": [ { "prover": "why3:Alt-Ergo,2.0.0",
"verdict": "valid", "time": 0.0108,
"verdict": "valid", "time": 0.0131,
"steps": 16 } ] } } ]
src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/typed/typed_init_t2_v2_loop_assigns_part2.json → src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/typed_init_t2_v2_loop_assigns_part2.json
+ 2
− 2
View file @ bfca79bb
......@@ -3,8 +3,8 @@
"target": "exists i_0,i_1:int.\n(i_0<=i_21) /\\ (i_1<=i_22) /\\ (0<=i_0) /\\ (i_21<=i_0) /\\ (i_22<=i_1)\n/\\ (i_0<=9)",
"pattern": "\\E\\E&<=<=<=<=<=<=#1$i#0$i0#1$i#1" },
"children": { "Goal 1/2": [ { "prover": "why3:Alt-Ergo,2.0.0",
"verdict": "valid", "time": 0.0175,
"verdict": "valid", "time": 0.0121,
"steps": 18 } ],
"Goal 2/2": [ { "prover": "why3:Alt-Ergo,2.0.0",
"verdict": "valid", "time": 0.0191,
"verdict": "valid", "time": 0.0146,
"steps": 20 } ] } } ]
src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/typed/typed_init_t2_v2_loop_assigns_part3.json → src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/typed_init_t2_v2_loop_assigns_part3.json
+ 2
− 2
View file @ bfca79bb
......@@ -3,8 +3,8 @@
"target": "exists i_0,i_1:int.\n(i_0<=i_8) /\\ (i_1<=i_9) /\\ (0<=i_0) /\\ (i_8<=i_0) /\\ (i_9<=i_1) /\\ (i_0<=9)",
"pattern": "\\E\\E&<=<=<=<=<=<=#1$i#0$i0#1$i#1" },
"children": { "Goal 1/2": [ { "prover": "why3:Alt-Ergo,2.0.0",
"verdict": "valid", "time": 0.0191,
"verdict": "valid", "time": 0.0092,
"steps": 18 } ],
"Goal 2/2": [ { "prover": "why3:Alt-Ergo,2.0.0",
"verdict": "valid", "time": 0.021,
"verdict": "valid", "time": 0.0103,
"steps": 20 } ] } } ]
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment