Skip to content

GitLab

why3
why3
Commit fa17cfa0 authored by Andrei Paskevich's avatar Andrei Paskevich
Browse files
Options

Mlw: eval_match 

We only destruct n-tuples, unit types, and singleton records
without invariants. We only inline projection-like functions
for these types.
parent 3714d05b
Hide whitespace changes
Inline Side-by-side
Showing with 94 additions and 120 deletions
Makefile.in
View file @ fa17cfa0
......@@ -164,7 +164,7 @@ LIB_DRIVER = call_provers driver_ast driver_parser driver_lexer driver \
whyconf autodetection \
parse_smtv2_model_parser parse_smtv2_model_lexer parse_smtv2_model
LIB_MLW = ity expr dexpr pdecl vc pmodule
LIB_MLW = ity expr dexpr pdecl eval_match vc pmodule
LIB_PARSER = ptree glob typing parser lexer
......@@ -179,7 +179,7 @@ LIB_TRANSFORM = simplify_formula inlining split_goal induction \
introduction abstraction close_epsilon lift_epsilon \
eliminate_epsilon intro_projections_counterexmp \
prepare_for_counterexmp \
eval_match instantiate_predicate smoke_detector \
instantiate_predicate smoke_detector \
reduction_engine compute induction_pr prop_curry
LIB_PRINTER = alt_ergo why3printer smtv1 smtv2 coq pvs isabelle \
......
src/transform/eval_match.ml → src/mlw/eval_match.ml
View file @ fa17cfa0
......@@ -13,27 +13,26 @@ open Ident
open Ty
open Term
open Decl
open Pdecl
type inline = known_map -> lsymbol -> ty list -> ty option -> bool
let unfold def tl ty =
let vl, e = open_ls_defn def in
let add (mt,mv) x y = ty_match mt x.vs_ty (t_type y), Mvs.add x y mv in
let (mt,mv) = List.fold_left2 add (Mtv.empty, Mvs.empty) vl tl in
let mt = oty_match mt e.t_ty ty in
t_ty_subst mt mv e
let is_constructor kn ls = match Mid.find ls.ls_name kn with
| { d_node = Ddata dl } ->
let constr (_,csl) = List.exists (fun (cs,_) -> ls_equal cs ls) csl in
List.exists constr dl
let is_projection kn ls = ls.ls_constr = 0 &&
match Mid.find ls.ls_name kn with
| { pd_node = PDtype _ } -> true
| _ -> false
let is_projection kn ls = match Mid.find ls.ls_name kn with
| { d_node = Ddata dl } ->
let constr (_,csl) = List.exists (fun (cs,_) -> ls_equal cs ls) csl in
not (List.exists constr dl)
| _ -> false
let find_constructors kn ({ts_name = id} as ts) =
let rec find = function
| {d_news = s}::dl when not (Mid.mem id s) -> find dl
| {d_node = Ddata dl}::_ -> List.assq ts dl
| _ -> [] in
find (Mid.find id kn).pd_pure
let find_logic_definition kn ({ls_name = id} as ls) =
let rec find = function
| {d_news = s}::dl when not (Mid.mem id s) -> find dl
| {d_node = Dlogic dl}::_ -> Some (List.assq ls dl)
| _ -> None in
find (Mid.find id kn).pd_pure
let apply_projection kn ls t = match t.t_node with
| Tapp (cs,tl) ->
......@@ -54,14 +53,45 @@ let flat_case t bl =
let mk_case = t_case_close and mk_let = t_let_close_simp in
Pattern.compile_bare ~mk_case ~mk_let [t] (List.map mk_b bl)
let rec add_quant kn (vl,tl,f) v =
let ty = v.vs_ty in
(* we destruct tuples, units, and singleton records *)
let destructible kn ty =
let cl = match ty.ty_node with
| Tyapp (ts, _) -> find_constructors kn ts
| _ -> []
in
| _ -> [] in
match cl with
| [ls,_] ->
| [ls,_] when is_fs_tuple ls -> Some ls
| [{ls_args = [_]} as ls, _] -> Some ls
| [{ls_args = []} as ls, _] -> Some ls
| _ -> None
(* we inline projections of destructed types *)
let find_inlineable kn ls = match ls.ls_args with
| [arg] when destructible kn arg <> None ->
begin match find_logic_definition kn ls with
| Some def ->
let res = open_ls_defn def in
begin match (snd res).t_node with
| Tvar _ | Tconst _
| Tapp (_, [{t_node = Tvar _}]) -> Some res
| Tcase ({t_node = Tvar _}, [bt]) ->
begin match t_open_branch bt with
| _, {t_node = Tvar _} -> Some res
| _ -> None end
| _ -> None end
| _ -> None end
| _ -> None
let unfold_inlineable kn ls tl ty = match find_inlineable kn ls with
| Some (vl, e) ->
let mt = List.fold_left2 (fun mt x y ->
ty_match mt x.vs_ty (t_type y)) Mtv.empty vl tl in
let mv = List.fold_right2 Mvs.add vl tl Mvs.empty in
Some (t_ty_subst (oty_match mt e.t_ty ty) mv e)
| None -> None
let rec add_quant kn (vl,tl,f) ({vs_ty = ty} as v) =
match destructible kn ty with
| Some ls ->
let s = ty_match Mtv.empty (Opt.get ls.ls_value) ty in
let mk_v ty = create_vsymbol (id_clone v.vs_name) (ty_inst s ty) in
let nvl = List.map mk_v ls.ls_args in
......@@ -69,7 +99,7 @@ let rec add_quant kn (vl,tl,f) v =
let f = t_let_close_simp v t f in
let tl = tr_map (t_subst_single v t) tl in
List.fold_left (add_quant kn) (vl,tl,f) nvl
| _ ->
| None ->
(v::vl, tl, f)
let let_map fn env t1 tb =
......@@ -82,50 +112,49 @@ let branch_map fn env t1 bl =
let p,t2,close = t_open_branch_cb b in close p (fn env t2) in
t_case t1 (List.map mk_b bl)
let dive_to_constructor kn fn env t =
let dive_to_constructor fn env t =
let rec dive env t = t_label_copy t (match t.t_node with
| Tvar x -> dive env (Mvs.find_exn Exit x env)
| Tlet (t1,tb) -> let_map dive env t1 tb
| Tcase (t1,bl) -> branch_map dive env t1 bl
| Tif (f,t1,t2) -> t_if_simp f (dive env t1) (dive env t2)
| Tapp (ls,_) when is_constructor kn ls -> fn env t
| Tapp (ls,_) when ls.ls_constr > 0 -> fn env t
| _ -> raise Exit)
in
dive env t
let rec cs_equ kn env t1 t2 =
let rec cs_equ env t1 t2 =
if t_equal t1 t2 then t_true
else match t1,t2 with
| { t_node = Tapp (cs,tl) }, t
| t, { t_node = Tapp (cs,tl) } when is_constructor kn cs ->
let fn = apply_cs_equ kn cs tl in
begin try dive_to_constructor kn fn env t
| t, { t_node = Tapp (cs,tl) } when cs.ls_constr > 0 ->
let fn = apply_cs_equ cs tl in
begin try dive_to_constructor fn env t
with Exit -> t_equ t1 t2 end
| _ -> t_equ t1 t2
and apply_cs_equ kn cs1 tl1 env t = match t.t_node with
and apply_cs_equ cs1 tl1 env t = match t.t_node with
| Tapp (cs2,tl2) when ls_equal cs1 cs2 ->
let merge t1 t2 f = t_and_simp (cs_equ kn env t1 t2) f in
let merge t1 t2 f = t_and_simp (cs_equ env t1 t2) f in
List.fold_right2 merge tl1 tl2 t_true
| Tapp _ -> t_false
| _ -> assert false
let eval_match ~inline kn t =
let rec eval stop env t =
let stop = stop || Slab.mem Term.stop_split t.t_label in
let eval = eval stop in
t_label_copy t (match t.t_node with
let rec eval_match kn stop env t =
let stop = stop || Slab.mem Term.stop_split t.t_label in
let eval env t = eval_match kn stop env t in
t_label_copy t (match t.t_node with
| Tapp (ls, [t1;t2]) when ls_equal ls ps_equ ->
cs_equ kn env (eval env t1) (eval env t2)
cs_equ env (eval env t1) (eval env t2)
| Tapp (ls, [t1]) when is_projection kn ls ->
let t1 = eval env t1 in
let fn _env t = apply_projection kn ls t in
begin try dive_to_constructor kn fn env t1
begin try dive_to_constructor fn env t1
with Exit -> t_app ls [t1] t.t_ty end
| Tapp (ls, tl) when inline kn ls (List.map t_type tl) t.t_ty ->
begin match find_logic_definition kn ls with
| None -> t_map (eval env) t
| Some def -> eval env (unfold def tl t.t_ty)
| Tapp (ls, tl) ->
begin match unfold_inlineable kn ls tl t.t_ty with
| Some t -> eval env t
| None -> t_map (eval env) t
end
| Tlet (t1, tb2) ->
let t1 = eval env t1 in
......@@ -133,54 +162,14 @@ let eval_match ~inline kn t =
| Tcase (t1, bl1) ->
let t1 = eval env t1 in
let fn env t2 = eval env (Loc.try2 ?loc:t.t_loc flat_case t2 bl1) in
begin try dive_to_constructor kn fn env t1
begin try dive_to_constructor fn env t1
with Exit -> branch_map eval env t1 bl1 end
| Tquant (q, qf) ->
let vl,tl,f,close = t_open_quant_cb qf in
let vl,tl,f = if stop
then (List.rev vl,tl,f)
else List.fold_left (add_quant kn) ([],tl,f) vl in
let vl,tl,f = if stop then List.rev vl,tl,f else
List.fold_left (add_quant kn) ([],tl,f) vl in
t_quant_simp q (close (List.rev vl) tl (eval env f))
| _ ->
t_map_simp (eval env) t)
in
eval false Mvs.empty t
let rec linear vars t = match t.t_node with
| Tvar x -> Svs.add_new Exit x vars
| Tif _ | Teps _ -> raise Exit
| _ -> t_fold linear vars t
let linear t =
try ignore (linear Svs.empty t); true with Exit -> false
let is_algebraic_type kn ty = match ty.ty_node with
| Tyapp (ts, _) -> find_constructors kn ts <> []
| Tyvar _ -> false
(* The following memoization by function definition is unsafe,
since the same definition can be used in different contexts.
If we could produce the record updates {| x with field = v |}
that were linear (by eliminating occurrences of x.field in v),
inline_nonrec_linear might not call eval_match at all and so
be independent of the context. FIXME/TODO *)
let inline_cache = Wdecl.create 17
let rec inline_nonrec_linear kn ls tyl ty =
(* at least one actual parameter (or the result) has an algebraic type *)
List.exists (is_algebraic_type kn) (oty_cons tyl ty) &&
(* and ls is not recursively defined and is linear *)
let d = Mid.find ls.ls_name kn in
if Mid.mem ls.ls_name d.d_syms then false else
match d.d_node with
| Dlogic [_,def] ->
begin try Wdecl.find inline_cache d with Not_found ->
let vl,t = open_ls_defn def in
let _,_,t = List.fold_left (add_quant kn) ([],[],t) vl in
let t = eval_match ~inline:inline_nonrec_linear kn t in
let res = linear t in
Wdecl.set inline_cache d res;
res
end
| _ -> false
t_map (eval env) t)
let eval_match kn t = eval_match kn false Mvs.empty t
src/transform/eval_match.mli → src/mlw/eval_match.mli
View file @ fa17cfa0
......@@ -9,13 +9,4 @@
(* *)
(********************************************************************)
open Ty
open Term
open Decl
type inline = known_map -> lsymbol -> ty list -> ty option -> bool
val eval_match: inline:inline -> known_map -> term -> term
val inline_nonrec_linear : inline
val eval_match : Pdecl.known_map -> Term.term -> Term.term
src/mlw/vc.ml
View file @ fa17cfa0
......@@ -19,12 +19,15 @@ open Pdecl
(* basic tools *)
let debug = Debug.register_info_flag "vc"
let debug = Debug.register_info_flag "vc_debug"
~desc:"Print@ details@ of@ verification@ conditions@ generation."
let debug_sp = Debug.register_info_flag "vc_sp"
let debug_sp = Debug.register_flag "vc_sp"
~desc:"Use@ 'Efficient@ Weakest@ Preconditions'@ for@ verification."
let no_eval = Debug.register_flag "vc_no_eval"
~desc:"Do@ not@ simplify@ pattern@ matching@ on@ record@ datatypes@ in@ VCs."
let ls_of_rs s = match s.rs_logic with RLls ls -> ls | _ -> assert false
let clone_vs v = create_vsymbol (id_clone v.vs_name) v.vs_ty
......@@ -314,20 +317,9 @@ let adjustment dst dst' =
(* combine postconditions with preconditions *)
let extract_defn v sp =
let rec extract h = match h.t_node with
| Tapp (ps, [{t_node = Tvar u}; t])
when ls_equal ps ps_equ && vs_equal u v && t_v_occurs v t = 0 ->
t, t_true
| Tbinop (Tand,f,g) ->
let t, f = extract f in
t, t_label_copy h (sp_and f g)
| _ -> raise Exit in
try Some (extract sp) with Exit -> None
let wp_close lab v ql wp =
let sp = sp_of_post lab v ql in
match extract_defn v sp with
match term_of_post ~prop:false v sp with
| Some (t, sp) -> wp_let v t (sp_implies sp wp)
| None -> wp_forall [v] (sp_implies sp wp)
......@@ -340,13 +332,13 @@ let sp_wp_close v sp adv wp =
let fvs = Mvs.filter (fun v _ -> is_fresh v) fvs in
let fvs = Mvs.fold (fun _ t s -> t_freevars s t) adv fvs in
let vl = List.rev (Mvs.keys (Mvs.remove v fvs)) in
match extract_defn v sp with
match term_of_post ~prop:false v sp with
| Some (t, sp) -> wp_forall vl (wp_let v t (sp_implies sp wp))
| None -> wp_forall (v :: vl) (sp_implies sp wp)
let sp_sp_close v sp adv sp' =
let sp' = t_subst adv sp' in
match extract_defn v sp with
match term_of_post ~prop:false v sp with
| Some (t, sp) -> wp_let v t (sp_and sp sp')
| None when is_fresh v -> sp_and sp sp'
| None -> t_subst_single v (t_var (clone_vs v)) (sp_and sp sp')
......@@ -1043,21 +1035,23 @@ and vc_rec ({letrec_ps = lps} as env) vc_wp rdl =
vc_fun env ~o2n vc_wp c.c_cty e in
List.map vc_rd rdl
let mk_vc_decl id f =
let mk_vc_decl kn id f =
let {id_string = nm; id_label = label; id_loc = loc} = id in
let label = if lab_has_expl label then label else
Slab.add (Ident.create_label ("expl:VC for " ^ nm)) label in
let pr = create_prsymbol (id_fresh ~label ?loc ("VC " ^ nm)) in
let f = wp_forall (Mvs.keys (t_freevars Mvs.empty f)) f in
let f = if Debug.test_flag no_eval then f else
Eval_match.eval_match kn f in
create_pure_decl (create_prop_decl Pgoal pr f)
let vc env kn d = match d.pd_node with
| PDlet (LDsym (s, {c_node = Cfun e; c_cty = cty})) ->
let env = mk_env env kn in
let f = vc_fun env (Debug.test_noflag debug_sp) cty e in
[mk_vc_decl s.rs_name f]
[mk_vc_decl kn s.rs_name f]
| PDlet (LDrec rdl) ->
let env = mk_env env kn in
let fl = vc_rec env (Debug.test_noflag debug_sp) rdl in
List.map2 (fun rd f -> mk_vc_decl rd.rec_sym.rs_name f) rdl fl
List.map2 (fun rd f -> mk_vc_decl kn rd.rec_sym.rs_name f) rdl fl
| _ -> []
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