Skip to content

GitLab

why3
why3
Commit fcb44a61 authored by MARCHE Claude's avatar MARCHE Claude
Browse files
Options

trans compute: more robust protection against non termination

parent e3447b63
Hide whitespace changes
Inline Side-by-side
Showing with 237 additions and 395 deletions
src/transform/compute.ml
View file @ fcb44a61
......@@ -14,338 +14,8 @@ open Decl
open Task
open Theory
(* obsolete
type env = {
tknown : Decl.known_map;
vsenv : term Mvs.t;
}
let bind_vs v t env =
{ env with vsenv = Mvs.add v t env.vsenv }
let multibind_vs l tl env =
try
List.fold_right2 bind_vs l tl env
with Invalid_argument _ -> assert false
let get_vs env vs =
try Mvs.find vs env.vsenv
with Not_found ->
Format.eprintf "[Compute] logic variable %s not found in env@." vs.vs_name.Ident.id_string;
raise Not_found
exception NoMatch
exception Undetermined
exception CannotCompute
let rec matching env t p =
match p.pat_node with
| Pwild -> env
| Pvar v -> bind_vs v t env
| Por(p1,p2) ->
begin
try matching env t p1
with NoMatch -> matching env t p2
end
| Pas(p,v) -> matching (bind_vs v t env) t p
| Papp(ls1,pl) ->
match t.t_node with
| Tapp(ls2,tl) ->
if ls_equal ls1 ls2 then
List.fold_left2 matching env tl pl
else
if ls2.ls_constr > 0 then raise NoMatch
else raise Undetermined
| _ -> raise Undetermined
(* builtin symbols *)
let builtins = Hls.create 17
let ls_minus = ref ps_equ (* temporary *)
(* all builtin functions *)
let const_equality c1 c2 =
match c1,c2 with
| Number.ConstInt i1, Number.ConstInt i2 ->
BigInt.eq (Number.compute_int i1) (Number.compute_int i2)
| _ -> raise Undetermined
let value_equality t1 t2 =
match (t1.t_node,t2.t_node) with
| Tconst c1, Tconst c2 -> const_equality c1 c2
| _ -> raise Undetermined
let to_bool b = if b then t_true else t_false
let eval_equ _ls l _ty =
match l with
| [t1;t2] ->
begin
try to_bool (value_equality t1 t2)
with Undetermined -> t_equ t1 t2
end
| _ -> assert false
let eval_true _ls _l _ty = t_true
let eval_false _ls _l _ty = t_false
exception NotNum
let big_int_of_const c =
match c with
| Number.ConstInt i -> Number.compute_int i
| _ -> raise NotNum
let const_of_big_int n =
t_const (Number.ConstInt (Number.int_const_dec (BigInt.to_string n)))
let eval_int_op op ls l ty =
match l with
| [{t_node = Tconst c1};{t_node = Tconst c2}] ->
begin
try const_of_big_int (op (big_int_of_const c1) (big_int_of_const c2))
with NotNum | Division_by_zero ->
t_app ls l ty
end
| _ -> t_app ls l ty
let built_in_theories =
[ ["bool"],"Bool", [],
[ "True", None, eval_true ;
"False", None, eval_false ;
] ;
["int"],"Int", [],
[ "infix +", None, eval_int_op BigInt.add;
"infix -", None, eval_int_op BigInt.sub;
"infix *", None, eval_int_op BigInt.mul;
(*
"prefix -", Some ls_minus, eval_int_uop BigInt.minus;
"infix <", None, eval_int_rel BigInt.lt;
"infix <=", None, eval_int_rel BigInt.le;
"infix >", None, eval_int_rel BigInt.gt;
"infix >=", None, eval_int_rel BigInt.ge;
*)
] ;
(*
["int"],"MinMax", [],
[ "min", None, eval_int_op BigInt.min;
"max", None, eval_int_op BigInt.max;
] ;
["int"],"ComputerDivision", [],
[ "div", None, eval_int_op BigInt.computer_div;
"mod", None, eval_int_op BigInt.computer_mod;
] ;
["int"],"EuclideanDivision", [],
[ "div", None, eval_int_op BigInt.euclidean_div;
"mod", None, eval_int_op BigInt.euclidean_mod;
] ;
["map"],"Map", ["map", builtin_map_type],
[ "const", Some ls_map_const, eval_map_const;
"get", Some ls_map_get, eval_map_get;
"set", Some ls_map_set, eval_map_set;
] ;
*)
]
let add_builtin_th env (l,n,t,d) =
try
let th = Env.find_theory env l n in
List.iter
(fun (id,r) ->
let ts = Theory.ns_find_ts th.Theory.th_export [id] in
r ts)
t;
List.iter
(fun (id,r,f) ->
let ls = Theory.ns_find_ls th.Theory.th_export [id] in
Hls.add builtins ls f;
match r with
| None -> ()
| Some r -> r := ls)
d
with Not_found ->
Format.eprintf "[Compute] theory %s not found@." n
let get_builtins env =
Hls.clear builtins;
Hls.add builtins ps_equ eval_equ;
List.iter (add_builtin_th env) built_in_theories
(* computation in terms *)
let rec compute_in_term env t =
let eval_rec = compute_in_term env in
match t.t_node with
| Ttrue | Tfalse | Tconst _ -> t
| Tbinop(Tand,t1,t2) ->
t_and_simp (eval_rec t1) (eval_rec t2)
| Tbinop(Tor,t1,t2) ->
t_or_simp (eval_rec t1) (eval_rec t2)
| Tbinop(Timplies,t1,t2) ->
t_implies_simp (eval_rec t1) (eval_rec t2)
| Tbinop(Tiff,t1,t2) ->
t_iff_simp (eval_rec t1) (eval_rec t2)
| Tnot(t1) -> t_not_simp (eval_rec t1)
| Tvar vs ->
begin
try get_vs env vs
with Not_found -> t
end
| Tapp(ls,tl) ->
compute_app env ls (List.map eval_rec tl) t.t_ty
| Tif(t1,t2,t3) ->
let u1 = eval_rec t1 in
begin match u1.t_node with
| Ttrue -> eval_rec t2
| Tfalse -> eval_rec t3
| _ -> t_if u1 t2 t3
end
| Tlet(t1,tb) ->
let u1 = eval_rec t1 in
let v,t2 = t_open_bound tb in
let u2 = compute_in_term (bind_vs v u1 env) t2 in
t_let_close_simp v u1 u2
| Tcase(t1,tbl) ->
let u1 = eval_rec t1 in
compute_match env u1 tbl
| Teps _ -> t
| Tquant _ -> t
and compute_match env u tbl =
let rec iter tbl =
match tbl with
| [] ->
Format.eprintf "[Compute] fatal error: pattern matching not exhaustive in evaluation.@.";
assert false
| b::rem ->
let p,t = t_open_branch b in
try
let env' = matching env u p in
compute_in_term env' t
with NoMatch -> iter rem
in
try iter tbl with Undetermined ->
t_case u tbl
and compute_app env ls tl ty =
try
let f = Hls.find builtins ls in
f ls tl ty
with Not_found ->
try
let d = Ident.Mid.find ls.ls_name env.tknown in
match d.Decl.d_node with
| Decl.Dtype _ | Decl.Dprop _ -> assert false
| Decl.Dlogic dl ->
(* regular definition *)
let d = List.assq ls dl in
let l,t = Decl.open_ls_defn d in
let env' = multibind_vs l tl env in
compute_in_term env' t
| Decl.Dparam _ | Decl.Dind _ ->
t_app ls tl ty
| Decl.Ddata dl ->
(* constructor or projection *)
match tl with
| [ { t_node = Tapp(ls1,tl1) } ] ->
(* if ls is a projection and ls1 is a constructor,
we should compute that projection *)
let rec iter dl =
match dl with
| [] -> t_app ls tl ty
| (_,csl) :: rem ->
let rec iter2 csl =
match csl with
| [] -> iter rem
| (cs,prs) :: rem2 ->
if ls_equal cs ls1
then
(* we found the right constructor *)
let rec iter3 prs tl1 =
match prs,tl1 with
| (Some pr)::prs, t::tl1 ->
if ls_equal ls pr
then (* projection found! *) t
else
iter3 prs tl1
| None::prs, _::tl1 ->
iter3 prs tl1
| _ -> t_app ls tl ty
in iter3 prs tl1
else iter2 rem2
in iter2 csl
in iter dl
| _ -> t_app ls tl ty
with Not_found ->
Format.eprintf "[Compute] definition of logic symbol %s not found@."
ls.ls_name.Ident.id_string;
t_app ls tl ty
let compute_in_decl km d =
match d.d_node with
| Dprop(k,pr,f) ->
let t = compute_in_term { tknown = km; vsenv = Mvs.empty } f in
create_prop_decl k pr t
| _ -> d
let compute_in_tdecl km d =
match d.td_node with
| Decl d -> create_decl (compute_in_decl km d)
| _ -> d
let rec compute_in_task task =
match task with
| Some d ->
add_tdecl
(compute_in_task d.task_prev)
(compute_in_tdecl d.task_known d.task_decl)
| None -> None
let compute env task =
let task = compute_in_task task in
match task with
| Some
{ task_decl =
{ td_node = Decl { d_node = Dprop (Pgoal, _, f) }}
} ->
get_builtins env;
begin match f.t_node with
| Ttrue -> []
| _ -> [task]
end
| _ -> assert false
let () =
Trans.register_env_transform_l "compute"
(fun env -> Trans.store (compute env))
~desc:"Compute@ as@ much@ as@ possible"
*)
(* compute with rewrite rules *)
let meta = Theory.register_meta "rewrite" [Theory.MTprsymbol]
~desc:"Declares@ the@ given@ proposition@ as@ a@ rewrite@ rule."
let collect_rule_decl prs e d =
match d.Decl.d_node with
......@@ -356,7 +26,7 @@ let collect_rule_decl prs e d =
try
Reduction_engine.add_rule t e
with Reduction_engine.NotARewriteRule msg ->
Warning.emit "prop %a cannot be turned into a rewrite rule: %s"
Warning.emit "proposition %a cannot be turned into a rewrite rule: %s"
Pretty.print_pr pr msg;
e
else e
......@@ -387,9 +57,6 @@ let normalize_goal env (prs : Decl.Spr.t) task =
| _ -> assert false
let meta = Theory.register_meta "rewrite" [Theory.MTprsymbol]
~desc:"Declares@ the@ given@ prop@ as@ a@ rewrite@ rule."
let normalize_transf env =
Trans.on_tagged_pr meta (fun prs -> Trans.store (normalize_goal env prs))
......
src/transform/reduction_engine.ml
View file @ fcb44a61
......@@ -379,6 +379,12 @@ let rec matching ((mt,mv) as sigma) t p =
| _ -> raise Undetermined
let rec extract_first n acc l =
if n = 0 then acc,l else
match l with
| x :: r ->
extract_first (n-1) (x::acc) r
| [] -> assert false
let rec reduce engine c =
......@@ -477,10 +483,7 @@ and reduce_match st u tbl sigma cont =
with NoMatch -> iter rem
in
try iter tbl with Undetermined ->
{ (* value_stack = Term (t_case u tbl) :: st; *)
(* FIXME: apply (t_subst sigma) on each branch of tbl !! *)
value_stack = Term (t_subst sigma (t_case u tbl)) :: st;
(* DONE? *)
{ value_stack = Term (t_subst sigma (t_case u tbl)) :: st;
cont_stack = cont;
}
......@@ -549,13 +552,6 @@ and reduce_app engine st ls ty rem_cont =
| t2 :: t1 :: rem_st -> reduce_equ rem_st t1 t2 rem_cont
| _ -> assert false
else
let rec extract_first n acc l =
if n = 0 then acc,l else
match l with
| x :: r ->
extract_first (n-1) (x::acc) r
| [] -> assert false
in
let arity = List.length ls.ls_args in
let args,rem_st = extract_first arity [] st in
try
......@@ -736,20 +732,90 @@ and reduce_term_equ st t1 t2 cont =
let rec many_steps engine c n =
let rec reconstruct c =
match c.value_stack, c.cont_stack with
| [Term t], [] -> t
| _, [] -> assert false
| _ -> if n = 0 then assert false else
let c = reduce engine c in
many_steps engine c (n-1)
| st, Keval (t,sigma) :: rem ->
reconstruct {
value_stack = (Term (t_subst sigma t)) :: st;
cont_stack = rem;
}
| [], Kif _ :: _ -> assert false
| v :: st, Kif(t2,t3,sigma) :: rem ->
reconstruct {
value_stack =
Term (t_if (term_of_value v) (t_subst sigma t2) (t_subst sigma t3)) :: st;
cont_stack = rem ;
}
| [], Klet _ :: _ -> assert false
| t1 :: st, Klet(v,t2,sigma) :: rem ->
reconstruct {
value_stack = Term(t_let_close v (term_of_value t1) (t_subst sigma t2)) :: st;
cont_stack = rem;
}
| [], Kcase _ :: _ -> assert false
| v :: st, Kcase(tbl,sigma) :: rem ->
reconstruct {
value_stack = Term (t_subst sigma (t_case (term_of_value v) tbl)) :: st;
cont_stack = rem;
}
| ([] | [_]), Kbinop _ :: _ -> assert false
| t1 :: t2 :: st, Kbinop op :: rem ->
reconstruct {
value_stack = Term (t_binary_simp op (term_of_value t1) (term_of_value t2)) :: st;
cont_stack = rem;
}
| [], Knot :: _ -> assert false
| t :: st, Knot :: rem ->
reconstruct {
value_stack = Term (t_not (term_of_value t)) :: st;
cont_stack = rem;
}
| st, Kapp(ls,ty) :: rem ->
let args,rem_st = extract_first (List.length ls.ls_args) [] st in
let args = List.map term_of_value args in
reconstruct {
value_stack = Term (t_app ls args ty) :: rem_st;
cont_stack = rem;
}
| [], Keps _ :: _ -> assert false
| t :: st, Keps v :: rem ->
reconstruct {
value_stack = Term (t_eps_close v (term_of_value t)) :: st;
cont_stack = rem;
}
| [], Kquant _ :: _ -> assert false
| t :: st, Kquant(q,vl,tr) :: rem ->
reconstruct {
value_stack = Term (t_quant_close q vl tr (term_of_value t)) :: st;
cont_stack = rem;
}
let normalize engine t =
(** iterated reductions *)
let normalize ?(limit=1000) engine t0 =
let rec many_steps c n =
match c.value_stack, c.cont_stack with
| [Term t], [] -> t
| _, [] -> assert false
| _ ->
if n = limit then
begin
Warning.emit "reduction of term %a takes more than %d steps, aborted.@."
Pretty.print_term t0 limit;
reconstruct c
end
else
let c = reduce engine c in
many_steps c (n+1)
in
let c = { value_stack = [];
cont_stack = [Keval(t,Mvs.empty)] ;
cont_stack = [Keval(t0,Mvs.empty)] ;
}
in
many_steps engine c 1000
many_steps c 0
......
src/transform/reduction_engine.mli
View file @ fcb44a61
......@@ -10,11 +10,7 @@
(********************************************************************)
(*********************
{1 A reduction engine for Why3 terms}
*************************)
(** A reduction engine for Why3 terms *)
(*
terms are normalized with respect to
......@@ -98,10 +94,11 @@ val add_rule : Term.term -> engine -> engine
*)
val normalize : engine -> Term.term -> Term.term
val normalize : ?limit:int -> engine -> Term.term -> Term.term
(** [normalize e t] normalizes the term [t] with respect to the engine
[e]
TODO: specify the behavior when non-termination...
Optional parameter [limit] provides a maximum number of steps for execution.
(default 1000). When limit is reached, the partially reduced term is returned.
*)
tests/test_compute.why
View file @ fcb44a61
......@@ -198,6 +198,50 @@ theory Rgroup
end
theory NonTerm
type t
constant c : t
function f t : t
axiom a: f c = f (f c)
meta "rewrite" prop a
goal g: f c = f c
use import int.Int
type nat = O | S nat
function plus (n m:nat) : nat =
match n with
| O -> m
| S k -> S (plus k m)
end
function fib (n:nat) : nat =
match n with
| O -> O
| S O -> S O
| S (S n as m) -> plus (fib n) (fib m)
end
constant x : nat
goal g3 : fib (S (S (S O))) = x
goal g4 : fib (S (S (S (S O)))) = x
goal g5 : fib (S (S (S (S (S O))))) = x
goal g6 : fib (S (S (S (S (S (S O)))))) = x
goal g7 : fib (S (S (S (S (S (S (S O))))))) = x
goal g8 : fib (S (S (S (S (S (S (S (S O)))))))) = x
goal g9 : fib (S (S (S (S (S (S (S (S (S O))))))))) = x
goal g10 : fib (S (S (S (S (S (S (S (S (S (S O)))))))))) = x
end
theory Rinteger
use export int.Int
......
tests/test_compute/why3session.xml
View file @ fcb44a61
......@@ -57,7 +57,7 @@
</transf>
</goal>
</theory>
<theory name="TestList" expanded="true">
<theory name="TestList">
<goal name="g1" sum="0ddd0eeb3a391ca74d03f68832a092a6">
<transf name="compute_in_goal">
</transf>
......@@ -70,18 +70,18 @@
<transf name="compute_in_goal">
</transf>
</goal>
<goal name="h1" sum="e2022f7025813c0922b8d8d9143180b9" expanded="true">
<transf name="compute_in_goal" expanded="true">
<goal name="h1" sum="e2022f7025813c0922b8d8d9143180b9">
<transf name="compute_in_goal">
<goal name="h1.1" expl="1." sum="d8bcddc97984d451ccfe8ca384a80ccb">
</goal>
</transf>
</goal>
<goal name="h2" sum="23bc457ed3671d19bf68aacaceb560ac" expanded="true">
<goal name="h2" sum="23bc457ed3671d19bf68aacaceb560ac">
<transf name="compute_in_goal">
</transf>
</goal>
<goal name="h3" sum="554dc390f63c85050856d58aeb5c9928" expanded="true">
<transf name="compute_in_goal" expanded="true">
<goal name="h3" sum="554dc390f63c85050856d58aeb5c9928">
<transf name="compute_in_goal">
<goal name="h3.1" expl="1." sum="16656d9cb10c34b8dfa06a7f65f5004a">
</goal>
</transf>
......@@ -89,55 +89,55 @@
</theory>
<theory name="Rstandard" expanded="true">
</theory>
<theory name="TestStandard" expanded="true">
<goal name="g00" sum="0ceddda03e7e96cda00c67eebccb8ce2" expanded="true">
<transf name="compute_in_goal" expanded="true">
<theory name="TestStandard">
<goal name="g00" sum="0ceddda03e7e96cda00c67eebccb8ce2">
<transf name="compute_in_goal">
<goal name="g00.1" expl="1." sum="72e859206601f617bc9e8d202f1736c7">
</goal>
</transf>
</goal>
<goal name="g01" sum="033e36efdc75e7ebee7089bb79aae621" expanded="true">
<transf name="compute_in_goal" expanded="true">
<goal name="g01" sum="033e36efdc75e7ebee7089bb79aae621">
<transf name="compute_in_goal">
<goal name="g01.1" expl="1." sum="d6d954e45cea3cfb507006372f300730">
</goal>
</transf>
</goal>
<goal name="g02" sum="e9fe9f1ccbd8b3e9306f10125f9884fe" expanded="true">
<transf name="compute_in_goal" expanded="true">
<goal name="g02" sum="e9fe9f1ccbd8b3e9306f10125f9884fe">
<transf name="compute_in_goal">
<goal name="g02.1" expl="1." sum="bf81b44246d2030307c2cbbc6036407a">
</goal>
</transf>
</goal>
<goal name="g03" sum="0d4620924ddd3999e33c97573f5b78e0" expanded="true">
<transf name="compute_in_goal" expanded="true">
<goal name="g03" sum="0d4620924ddd3999e33c97573f5b78e0">
<transf name="compute_in_goal">
<goal name="g03.1" expl="1." sum="4f95c487067aa0d0dee0ac82ede93e99">
</goal>
</transf>
</goal>
<goal name="g04" sum="e37cdc4814159dbd3887a5880f33246c" expanded="true">
<transf name="compute_in_goal" expanded="true">
<goal name="g04" sum="e37cdc4814159dbd3887a5880f33246c">
<transf name="compute_in_goal">
<goal name="g04.1" expl="1." sum="15d82520ff40518ce3e75cf46bb5c135">
</goal>
</transf>
</goal>
<goal name="g05" sum="4e7c955211deed29770e221db4c89bca" expanded="true">
<transf name="compute_in_goal" expanded="true">
<goal name="g05" sum="4e7c955211deed29770e221db4c89bca">
<transf name="compute_in_goal">
<goal name="g05.1" expl="1." sum="6f9cf28d8e4785900d38fff421f2260d">
</goal>
</transf>
</goal>
<goal name="g06" sum="447bada60ec36071cd53b698cbf73823" expanded="true">
<goal name="g06" sum="447bada60ec36071cd53b698cbf73823">
</goal>
<goal name="g07" sum="9f175ea63c4a17c0a01aadffe9cf5e9f" expanded="true">
<transf name="compute_in_goal" expanded="true">
<goal name="g07" sum="9f175ea63c4a17c0a01aadffe9cf5e9f">
<transf name="compute_in_goal">
<goal name="g07.1" expl="1." sum="ffa418ac5ab3f343a3554872c65c8bd9">
</goal>
</transf>
</goal>
</theory>
<theory name="Rgroup" expanded="true">
<goal name="g0" sum="1e4b57ee823bf83fde917bdd0b03d14a" expanded="true">
<transf name="compute_in_goal" expanded="true">
<theory name="Rgroup">
<goal name="g0" sum="1e4b57ee823bf83fde917bdd0b03d14a">
<transf name="compute_in_goal">
<goal name="g0.1" expl="1." sum="143d0d6addcac455f08acfb659827668">
</goal>
</transf>
......@@ -148,8 +148,8 @@
</goal>
</transf>
</goal>
<goal name="g1" sum="825053ebfb5449346b8ed12490cc9354" expanded="true">
<transf name="compute_in_goal" expanded="true">
<goal name="g1" sum="825053ebfb5449346b8ed12490cc9354">
<transf name="compute_in_goal">
<goal name="g1.1" expl="1." sum="992aa1eb1a8bf3883d4100848222a45e">
</goal>
</transf>
......@@ -161,30 +161,98 @@
</transf>
</goal>
</theory>
<theory name="NonTerm" expanded="true">
<goal name="g" sum="440373155c791eedfdbcd9785975a319" expanded="true">
<transf name="compute_in_goal" expanded="true">
<goal name="g.1" expl="1." sum="ca724c1f318987fce7ceabe6e2557be7" expanded="true">
<transf name="compute_in_goal" expanded="true">