Skip to content

GitLab

Commit 6411d618 authored by Allan Blanchard's avatar Allan Blanchard
Browse files

Merge branch 'fix/wp/robustify-script-engine' into 'master' 

[wp] robustify script engine

See merge request frama-c/frama-c!2888
parents 37f8ca70 c8a80909
Hide whitespace changes
Inline Side-by-side
src/libraries/utils/command.ml
View file @ 6411d618
......@@ -111,21 +111,23 @@ let print_file file job =
(* -------------------------------------------------------------------------- *)
type timer = float ref
type 'a result = Result of 'a | Error of exn
let dt_max tm dt = match tm with Some r when dt > !r -> r := dt | _ -> ()
let dt_add tm dt = match tm with Some r -> r := !r +. dt | _ -> ()
let return = function Result x -> x | Error e -> raise e
let catch f x = try Result(f x) with e -> Error e
let time ?rmax ?radd job data =
begin
let t0 = Sys.time () in
let re = catch job data in
let t0 = Sys.time () in
try
let result = job data in
let t1 = Sys.time () in
let dt = t1 -. t0 in
dt_max rmax dt ;
dt_add radd dt ;
return re ;
end
result
with exn ->
let t1 = Sys.time () in
let dt = t1 -. t0 in
dt_max rmax dt ;
dt_add radd dt ;
raise exn
(* -------------------------------------------------------------------------- *)
(* --- Process --- *)
......
src/libraries/utils/command.mli
View file @ 6411d618
......@@ -62,9 +62,7 @@ val print_file : string -> (Format.formatter -> 'a) -> 'a
(* ************************************************************************* *)
type timer = float ref
type 'a result = Result of 'a | Error of exn
val catch : ('a -> 'b) -> 'a -> 'b result
val return : 'a result -> 'a
val time : ?rmax:timer -> ?radd:timer -> ('a -> 'b) -> 'a -> 'b
(** Compute the elapsed time with [Sys.time].
The [rmax] timer is maximized and the [radd] timer is cumulated.
......
src/libraries/utils/task.ml
View file @ 6411d618
......@@ -469,7 +469,7 @@ let schedule server q =
done
with Queue.Empty -> ()
let rec run_server server () =
let server_progress server () =
begin
server.running <- List.filter
(fun task ->
......@@ -479,30 +479,29 @@ let rec run_server server () =
server.terminated <- succ server.terminated ; false )
) server.running ;
Array.iter (schedule server) server.queue ;
try
Db.yield ();
fire server.activity ;
if server.running <> [] then
begin
if not server.waiting && is_empty server then
begin
fire server.wait ;
server.waiting <- true ;
end ;
true
end
else
begin
fire server.stop ;
server.scheduled <- 0 ;
server.terminated <- 0 ;
false
end
with _ -> (* Db.Cancel ... *)
cancel_all server ;
run_server server ()
let () =
try Db.yield ()
with Db.Cancel -> cancel_all server
in
fire server.activity ;
if server.running <> [] then
begin
if not server.waiting && is_empty server then
begin
fire server.wait ;
server.waiting <- true ;
end ;
true
end
else
begin
fire server.stop ;
server.scheduled <- 0 ;
server.terminated <- 0 ;
false
end
end
let launch server =
if server.scheduled > server.terminated
then ( fire server.start ; !on_idle (run_server server) )
then ( fire server.start ; !on_idle (server_progress server) )
src/plugins/qed/term.ml
View file @ 6411d618
......@@ -2239,8 +2239,10 @@ struct
let fresh sigma t = fresh sigma.pool t
let call f e =
let v = f e in
validate "Qed.Subst.add_fun" v ; v
if lc_closed e then
let v = f e in
validate "Qed.Subst.add_fun" v ; v
else raise Not_found
let rec compute e = function
| EMPTY -> raise Not_found
......
src/plugins/wp/Footprint.ml
View file @ 6411d618
......@@ -31,7 +31,8 @@ let iter f e =
Queue.add e q ;
while not (Queue.is_empty q) do
let e = Queue.pop q in
f e ; F.lc_iter (fun e -> Queue.push e q) e
if F.lc_closed e then f e ;
F.lc_iter (fun e -> Queue.push e q) e
done
let once f e =
......@@ -42,7 +43,8 @@ let once f e =
Queue.add e q ;
while not (Queue.is_empty q) do
let e = Queue.pop q in
f e ; F.lc_iter (fun e -> if once m e then Queue.push e q) e
if F.lc_closed e then f e ;
F.lc_iter (fun e -> if once m e then Queue.push e q) e
done
(* -------------------------------------------------------------------------- *)
......@@ -151,3 +153,5 @@ let lookup ~occur ~inside =
) inside ;
raise Not_found
with Found e -> e
(* -------------------------------------------------------------------------- *)
src/plugins/wp/Footprint.mli
View file @ 6411d618
......@@ -49,3 +49,5 @@ val locate : select:term -> inside:term -> occurrence
(** Retrieve back the [k]-th occurrence of a footprint inside a term. *)
val lookup : occur:occurrence -> inside:term -> term
(* -------------------------------------------------------------------------- *)
src/plugins/wp/ProverScript.ml
View file @ 6411d618
......@@ -312,6 +312,20 @@ and autofork env ~depth fork =
else
( Env.validate env ; Task.return true )
(* -------------------------------------------------------------------------- *)
(* --- Apply Script Tactic --- *)
(* -------------------------------------------------------------------------- *)
let apply env node jtactic subscripts =
match jfork (Env.tree env) ?node jtactic with
| None -> failwith "Selector not found"
| Some fork ->
let _,children = ProofEngine.commit fork in
reconcile children subscripts ; (*TODO: saveback forgiven script ? *)
List.filter
(fun (_,node) -> not (ProofEngine.proved node))
children
(* -------------------------------------------------------------------------- *)
(* --- Script Crawling --- *)
(* -------------------------------------------------------------------------- *)
......@@ -348,30 +362,26 @@ let rec crawl env on_child node = function
| Tactic( _ , jtactic , subscripts ) :: alternative ->
begin
match jfork (Env.tree env) ?node jtactic with
| None ->
Wp_parameters.warning
"Script Error: on goal %a@\n\
can not apply '%s'@\n\
@[<hov 2>Params: %a@]@\n\
@[<hov 2>Select: %a@]@."
WpPropId.pretty (Env.goal env node).po_pid
jtactic.tactic
Json.pp jtactic.params
Json.pp jtactic.select ;
crawl env on_child node alternative
| Some fork ->
(*TODO: saveback forgiven script *)
let _,children = ProofEngine.commit fork in
reconcile children subscripts ;
let residual = List.filter
(fun (_,node) -> not (ProofEngine.proved node))
children in
if residual = [] then
Env.validate env
else
List.iter (fun (_,n) -> on_child n) children ;
Task.return ()
try
let residual = apply env node jtactic subscripts in
if residual = [] then
Env.validate env
else
List.iter (fun (_,n) -> on_child n) residual ;
Task.return ()
with exn when Wp_parameters.protect exn ->
Wp_parameters.warning
"Script Error: on goal %a@\n\
can not apply '%s'@\n\
exception %S@\n\
@[<hov 2>Params: %a@]@\n\
@[<hov 2>Select: %a@]@."
WpPropId.pretty (Env.goal env node).po_pid
jtactic.tactic
(Printexc.to_string exn)
Json.pp jtactic.params
Json.pp jtactic.select ;
crawl env on_child node alternative
end
(* -------------------------------------------------------------------------- *)
......
src/plugins/wp/prover.ml
View file @ 6411d618
......@@ -121,7 +121,15 @@ let spawn wpo ~delayed
prover , task
) provers)
else
let process = simplify ?start ?result wpo in
let process = simplify ?start ?result wpo >>= fun ok ->
begin
match success with
| None -> ()
| Some on_success ->
on_success wpo (if ok then Some VCS.Qed else None) ;
end ;
Task.return ()
in
let thread = Task.thread process in
let server = ProverTask.server () in
Task.spawn server ?pool thread
......
src/plugins/wp/tests/wp_tip/oracle_qualif/tac_split_quantifiers.0.session/script/split_ensures_Goal_Exist_And.json
View file @ 6411d618
[ { "header": "Split", "tactic": "Wp.split", "params": {},
[ { "prover": "script", "verdict": "unknown" },
{ "header": "Split", "tactic": "Wp.split", "params": {},
"select": { "select": "clause-goal",
"target": "exists i_0,i_1,i_2:int.\n(P_P1 i_0) /\\ (P_Q1 i_2) /\\ (P_P2 i_1 i_2)\n/\\ (exists i_3:int.\n (P_Q2 i_0 i_3))",
"pattern": "\\E\\E\\E&P_P1P_Q1P_P2\\E#3#1#2#1P_Q2" },
"children": { "Goal 1/2": [ { "prover": "alt-ergo", "verdict": "unknown",
"time": 0.0511159896851 },
{ "header": "NOP", "tactic": "Wp.Test.NOP",
"params": {},
"select": { "select": "clause-goal",
"target": "exists i_0,i_1:int. (P_Q1 i_0) /\\ (P_P2 i_1 i_0)",
"pattern": "\\E\\E&P_Q1P_P2#1#0#1" },
"children": { "Nop": [ { "prover": "alt-ergo",
"verdict": "unknown",
"time": 0.0514709949493 } ] } } ],
"Goal 2/2": [ { "prover": "alt-ergo", "verdict": "unknown",
"time": 0.0521941184998 },
{ "header": "NOP", "tactic": "Wp.Test.NOP",
"params": {},
"select": { "select": "clause-goal",
"target": "exists i_0:int. (P_P1 i_0) /\\ (exists i_1:int.\n (P_Q2 i_0 i_1))",
"pattern": "\\E&P_P1\\E#1P_Q2#1#0" },
"children": { "Nop": [ { "prover": "alt-ergo",
"verdict": "unknown",
"time": 0.0515058040619 } ] } } ] } } ]
"pattern": "\\E" },
"children": { "Goal 1/2": [], "Goal 2/2": [] } } ]
src/plugins/wp/tests/wp_tip/oracle_qualif/tac_split_quantifiers.0.session/script/split_ensures_Goal_Exist_And_bis.json
View file @ 6411d618
[ { "header": "Split", "tactic": "Wp.split", "params": {},
[ { "prover": "script", "verdict": "unknown" },
{ "header": "Split", "tactic": "Wp.split", "params": {},
"select": { "select": "clause-goal",
"target": "exists i_0,i_1,i_2,i_3:int.\n(P_Q1 1) /\\ (P_P2 i_0 i_1) /\\ (P_R2 i_1 i_2)\n/\\ (exists i_4:int.\n (P_Q2 i_3 i_4))",
"pattern": "\\E\\E\\E\\E&P_Q1P_P2P_R2\\E1#4#3#3#2" },
"children": { "Goal 1/3": [ { "prover": "alt-ergo", "verdict": "unknown",
"time": 0.0512578487396 },
{ "header": "NOP", "tactic": "Wp.Test.NOP",
"params": {},
"select": { "select": "clause-goal",
"target": "exists i_0,i_1:int. (P_Q2 i_0 i_1)",
"pattern": "\\E\\EP_Q2#1#0" },
"children": { "Nop": [ { "prover": "alt-ergo",
"verdict": "unknown",
"time": 0.0515179634094 } ] } } ],
"Goal 2/3": [ { "prover": "alt-ergo", "verdict": "unknown",
"time": 0.0517938137054 },
{ "header": "NOP", "tactic": "Wp.Test.NOP",
"params": {},
"select": { "select": "clause-goal",
"target": "exists i_0,i_1,i_2:int. (P_P2 i_2 i_1) /\\ (P_R2 i_1 i_0)",
"pattern": "\\E\\E\\E&P_P2P_R2#0#1#1#2" },
"children": { "Nop": [ { "prover": "alt-ergo",
"verdict": "unknown",
"time": 0.0515098571777 } ] } } ],
"Goal 3/3": [ { "prover": "alt-ergo", "verdict": "unknown",
"time": 0.0528788566589 },
{ "header": "NOP", "tactic": "Wp.Test.NOP",
"params": {},
"select": { "select": "clause-goal",
"target": "(P_Q1 1)",
"pattern": "P_Q11" },
"children": { "Nop": [ { "prover": "alt-ergo",
"verdict": "unknown",
"time": 0.0515050888062 } ] } } ] } } ]
"pattern": "\\EP_Q11" },
"children": { "Goal 1/3": [], "Goal 2/3": [], "Goal 3/3": [] } } ]
src/plugins/wp/tests/wp_tip/oracle_qualif/tac_split_quantifiers.0.session/script/split_ensures_Goal_Exist_Or.json
View file @ 6411d618
[ { "header": "Split", "tactic": "Wp.split", "params": {},
"select": { "select": "clause-goal",
"target": "exists i_0,i_1,i_2:int.\n(P_Q1 1) \\/ (P_P1 i_0) \\/ (P_P2 i_1 i_2) \\/ (exists i_3:int.\n (P_Q2 i_0 i_3))",
"pattern": "\\E\\E\\E|P_Q1P_P1P_P2\\E1#3#2#1P_Q2" },
"children": { "Distrib (exists or)": [ { "prover": "alt-ergo",
"verdict": "unknown",
"time": 0.0515348911285 },
{ "header": "NOP",
"tactic": "Wp.Test.NOP",
"params": {},
"select": { "select": "clause-goal",
"target": "(P_Q1 1) \\/ (exists i_0:int.\n (P_P1 i_0)) \\/ (exists i_0,i_1:int.\n (P_P2 i_1 i_0))\n\\/ (exists i_0,i_1:int.\n (P_Q2 i_0 i_1))",
"pattern": "|P_Q1\\E\\E\\E1P_P1\\E\\E#0P_P2P_Q2#0" },
"children": { "Nop": [ { "prover": "alt-ergo",
"verdict": "unknown",
"time": 0.0513439178467 } ] } } ] } } ]
"pattern": "\\EP_Q11" },
"children": { "Split": [ { "prover": "Alt-Ergo:2.2.0",
"verdict": "unknown" } ] } } ]
src/plugins/wp/tests/wp_tip/oracle_qualif/tac_split_quantifiers.0.session/script/split_ensures_Hyp_Forall_And.json
View file @ 6411d618
[ { "header": "Split", "tactic": "Wp.split", "params": {},
[ { "prover": "script", "verdict": "unknown" },
{ "header": "Split", "tactic": "Wp.split", "params": {},
"select": { "select": "clause-step", "at": 0, "kind": "have",
"target": "forall i_0,i_1,i_2:int.\n(P_Q1 1) /\\ (P_P1 i_0) /\\ (P_P2 i_1 i_2) /\\ (forall i_3:int.\n (P_Q2 i_0 i_3))",
"pattern": "\\F\\F\\F&P_Q1P_P1P_P2\\F1#3#2#1P_Q2" },
"children": { "Distrib (forall and)": [ { "prover": "alt-ergo",
"verdict": "unknown",
"time": 0.051558971405 },
{ "header": "NOP",
"tactic": "Wp.Test.NOP",
"params": {},
"select": { "select": "clause-step",
"at": 0,
"kind": "have",
"target": "(P_Q1 1) /\\ (forall i_0:int.\n (P_P1 i_0)) /\\ (forall i_0,i_1:int.\n (P_P2 i_1 i_0))\n/\\ (forall i_0,i_1:int.\n (P_Q2 i_0 i_1))",
"pattern": "&P_Q1\\F\\F\\F1P_P1\\F\\F#0P_P2P_Q2#0" },
"children": { "Nop": [ { "prover": "alt-ergo",
"verdict": "unknown",
"time": 0.0513830184937 } ] } } ] } } ]
"pattern": "\\FP_Q11" },
"children": { "Split (distrib forall and)": [] } } ]
src/plugins/wp/tests/wp_tip/oracle_qualif/tac_split_quantifiers.0.session/script/split_ensures_Hyp_Forall_Or_bis.json
View file @ 6411d618
[ { "header": "Split", "tactic": "Wp.split", "params": {},
[ { "prover": "script", "verdict": "unknown" },
{ "header": "Split", "tactic": "Wp.split", "params": {},
"select": { "select": "clause-step", "at": 0, "kind": "have",
"target": "forall i_0,i_1,i_2,i_3:int.\n(P_Q1 1) \\/ (P_P2 i_0 i_1) \\/ (P_R2 i_1 i_2)\n\\/ (forall i_4:int.\n (P_Q2 i_3 i_4))",
"pattern": "\\F\\F\\F\\F|P_Q1P_P2P_R2\\F1#4#3#3#2" },
"children": { "Goal 1/3": [ { "prover": "alt-ergo", "verdict": "unknown",
"time": 0.0511250495911 },
{ "header": "NOP", "tactic": "Wp.Test.NOP",
"params": {},
"select": { "select": "clause-step",
"at": 0, "kind": "have",
"target": "forall i_0,i_1:int. (P_Q2 i_0 i_1)",
"pattern": "\\F\\FP_Q2#1#0" },
"children": { "Nop": [ { "prover": "alt-ergo",
"verdict": "unknown",
"time": 0.0515208244324 } ] } } ],
"Goal 2/3": [ { "prover": "alt-ergo", "verdict": "unknown",
"time": 0.0517539978027 },
{ "header": "NOP", "tactic": "Wp.Test.NOP",
"params": {},
"select": { "select": "clause-step",
"at": 0, "kind": "have",
"target": "forall i_0,i_1,i_2:int. (P_P2 i_2 i_1) \\/ (P_R2 i_1 i_0)",
"pattern": "\\F\\F\\F|P_P2P_R2#0#1#1#2" },
"children": { "Nop": [ { "prover": "alt-ergo",
"verdict": "unknown",
"time": 0.0515398979187 } ] } } ],
"Goal 3/3": [ { "prover": "alt-ergo", "verdict": "unknown",
"time": 0.0528609752655 },
{ "header": "NOP", "tactic": "Wp.Test.NOP",
"params": {},
"select": { "select": "clause-step",
"at": 0, "kind": "have",
"target": "(P_Q1 1)",
"pattern": "P_Q11" },
"children": { "Nop": [ { "prover": "alt-ergo",
"verdict": "unknown",
"time": 0.051561832428 } ] } } ] } } ]
"pattern": "\\FP_Q11" },
"children": { "Goal 1/3": [], "Goal 2/3": [], "Goal 3/3": [] } } ]
src/plugins/wp/tests/wp_tip/tac_split_quantifiers.i
View file @ 6411d618
......@@ -17,7 +17,7 @@
predicate R2(integer a1, integer a2) reads \nothing ;
} */
/*@ ensures Goal_Exist_Or:
/*@ ensures Goal_Exist_Or:
(\exists integer a, b, c ;
P1(a) || P2(b, c) || Q1(1) || \exists integer d ; Q2(a,d)) ;
......@@ -29,7 +29,7 @@
(\exists integer a, b, c, d ;
P2(a, b) && R2(b, c) && Q1(1) && \exists integer e ; Q2(d,e)) ;
@ ensures Hyp_Forall_And:
@ ensures Hyp_Forall_And:
(\forall integer a, b, c ;
P1(a) && P2(b, c) && Q1(1) && \forall integer d ; Q2(a,d)
) ==>
......
src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_assigns_exit_part2.json
View file @ 6411d618
[ { "header": "Split", "tactic": "Wp.split", "params": {},
"select": { "select": "clause-goal",
"target": "exists i_0,i_1:int.\n(i_0<=i_136) /\\ (i_1<=i_137) /\\ (0<=i_0) /\\ (i_136<=i_0) /\\ (i_137<=i_1)\n/\\ (i_0<=9)",
"pattern": "\\E\\E&<=<=<=<=<=<=#1$i#0$i0#1$i#1" },
"pattern": "\\E$i$i0$i$i9" },
"children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.2.0",
"verdict": "valid", "time": 0.017,
"steps": 22 } ],
......
src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_assigns_normal_part2.json
View file @ 6411d618
[ { "header": "Split", "tactic": "Wp.split", "params": {},
"select": { "select": "clause-goal",
"target": "exists i_0,i_1:int.\n(i_0<=i_136) /\\ (i_1<=i_137) /\\ (0<=i_0) /\\ (i_136<=i_0) /\\ (i_137<=i_1)\n/\\ (i_0<=9)",
"pattern": "\\E\\E&<=<=<=<=<=<=#1$i#0$i0#1$i#1" },
"pattern": "\\E$i$i0$i$i9" },
"children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.2.0",
"verdict": "valid", "time": 0.017,
"steps": 22 } ],
......
src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_loop_assigns_part2.json
View file @ 6411d618
[ { "header": "Split", "tactic": "Wp.split", "params": {},
"select": { "select": "clause-goal",
"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" },
"pattern": "\\E$i$i0$i$i9" },
"children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.2.0",
"verdict": "valid", "time": 0.0236,
"steps": 41 } ],
......
src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_loop_assigns_part3.json
View file @ 6411d618
[ { "header": "Split", "tactic": "Wp.split", "params": {},
"select": { "select": "clause-goal",
"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" },
"pattern": "\\E$i$i0$i$i9" },
"children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.2.0",
"verdict": "valid", "time": 0.018,
"steps": 29 } ],
......
src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_assigns_part2.json
View file @ 6411d618
[ { "header": "Split", "tactic": "Wp.split", "params": {},
"select": { "select": "clause-goal",
"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" },
"pattern": "\\E$i$i0$i$i9" },
"children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.2.0",
"verdict": "valid", "time": 0.011,
"steps": 16 } ],
......
src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_2_part2.json
View file @ 6411d618
[ { "header": "Split", "tactic": "Wp.split", "params": {},
"select": { "select": "clause-goal",
"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" },
"pattern": "\\E$i$i0$i$i9" },
"children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.2.0",
"verdict": "valid", "time": 0.0177,
"steps": 40 } ],
......
Markdown is supported
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