Commit 2f7b69b5 authored by Andrei Paskevich's avatar Andrei Paskevich

Mlw: for-loops over range types

In the surface language, the loop index is always int in
the loop invariant and all annotations and pure terms inside
the loop. If you want to access the original range-typed index,
use "let copy_i = i in" in the program code before your assertion.
Of course, you cannot do that for the loop invariant, which is
what we want.
parent c8cb2b78
......@@ -157,14 +157,15 @@ let meta_float = register_meta "float_type" [MTtysymbol; MTlsymbol; MTlsymbol]
(** Theory *)
type theory = {
th_name : ident; (* theory name *)
th_path : string list; (* environment qualifiers *)
th_decls : tdecl list; (* theory declarations *)
th_crcmap : Coercion.t; (* implicit coercions *)
th_export : namespace; (* exported namespace *)
th_known : known_map; (* known identifiers *)
th_local : Sid.t; (* locally declared idents *)
th_used : Sid.t; (* used theories *)
th_name : ident; (* theory name *)
th_path : string list; (* environment qualifiers *)
th_decls : tdecl list; (* theory declarations *)
th_ranges : lsymbol Mts.t; (* range type projections *)
th_crcmap : Coercion.t; (* implicit coercions *)
th_export : namespace; (* exported namespace *)
th_known : known_map; (* known identifiers *)
th_local : Sid.t; (* locally declared idents *)
th_used : Sid.t; (* used theories *)
}
and tdecl = {
......@@ -264,6 +265,7 @@ type theory_uc = {
uc_name : ident;
uc_path : string list;
uc_decls : tdecl list;
uc_ranges : lsymbol Mts.t;
uc_crcmap : Coercion.t;
uc_prefix : string list;
uc_import : namespace list;
......@@ -280,6 +282,7 @@ let empty_theory n p = {
uc_name = id_register n;
uc_path = p;
uc_decls = [];
uc_ranges = Mts.empty;
uc_crcmap = Coercion.empty;
uc_prefix = [];
uc_import = [empty_ns];
......@@ -294,6 +297,7 @@ let close_theory uc = match uc.uc_export with
{ th_name = uc.uc_name;
th_path = uc.uc_path;
th_decls = List.rev uc.uc_decls;
th_ranges = uc.uc_ranges;
th_crcmap = uc.uc_crcmap;
th_export = e;
th_known = uc.uc_known;
......@@ -348,8 +352,11 @@ let known_meta kn al =
in
List.iter check al
(* FIXME: proper description *)
let meta_coercion = register_meta ~desc:"coercion" "coercion" [MTlsymbol]
exception RangeConflict of tysymbol
let add_tdecl uc td = match td.td_node with
| Decl d -> { uc with
uc_decls = td :: uc.uc_decls;
......@@ -362,11 +369,20 @@ let add_tdecl uc td = match td.td_node with
uc_used = Sid.union uc.uc_used (Sid.add th.th_name th.th_used) }
| Clone (_,sm) -> known_clone uc.uc_known sm;
{ uc with uc_decls = td :: uc.uc_decls }
| Meta (m,([MAts ts; MAls ls] as al)) when meta_equal m meta_range ->
known_meta uc.uc_known al;
let add b = match b with
| None -> Some ls
| Some s when ls_equal s ls -> b
| _ -> raise (RangeConflict ts) in
{ uc with uc_ranges = Mts.change add ts uc.uc_ranges;
uc_decls = td :: uc.uc_decls }
| Meta (m,([MAls ls] as al)) when meta_equal m meta_coercion ->
known_meta uc.uc_known al;
(* FIXME: shouldn't we add the meta to the theory? *)
{ uc with uc_crcmap = Coercion.add uc.uc_crcmap ls }
| Meta (_,al) -> known_meta uc.uc_known al;
{ uc with uc_crcmap = Coercion.add uc.uc_crcmap ls;
uc_decls = td :: uc.uc_decls }
| Meta (_,al) ->
known_meta uc.uc_known al;
{ uc with uc_decls = td :: uc.uc_decls }
(** Declarations *)
......@@ -487,10 +503,13 @@ let create_use th = mk_tdecl (Use th)
let use_export uc th =
let uc = add_tdecl uc (create_use th) in
let comb ts s1 s2 = if ls_equal s1 s2 then Some s1
else raise (RangeConflict ts) in
match uc.uc_import, uc.uc_export with
| i0 :: sti, e0 :: ste -> { uc with
uc_import = merge_ns false th.th_export i0 :: sti;
uc_export = merge_ns true th.th_export e0 :: ste;
uc_ranges = Mts.union comb uc.uc_ranges th.th_ranges;
uc_crcmap = Coercion.union uc.uc_crcmap th.th_crcmap }
| _ -> assert false
......@@ -942,5 +961,8 @@ let () = Exn_printer.register
Format.fprintf fmt "Metaproperty %s expects a %a argument but \
is applied to %a"
m.meta_name print_meta_arg_type t1 print_meta_arg_type t2
| RangeConflict ts ->
Format.fprintf fmt "Conflicting definitions for range type %s"
ts.ts_name.id_string
| _ -> raise exn
end
......@@ -84,14 +84,15 @@ val meta_float : meta
(** {2 Theories} *)
type theory = private {
th_name : ident; (* theory name *)
th_path : string list; (* environment qualifiers *)
th_decls : tdecl list; (* theory declarations *)
th_crcmap : Coercion.t; (* implicit coercions *)
th_export : namespace; (* exported namespace *)
th_known : known_map; (* known identifiers *)
th_local : Sid.t; (* locally declared idents *)
th_used : Sid.t; (* used theories *)
th_name : ident; (* theory name *)
th_path : string list; (* environment qualifiers *)
th_decls : tdecl list; (* theory declarations *)
th_ranges : lsymbol Mts.t; (* range type projections *)
th_crcmap : Coercion.t; (* implicit coercions *)
th_export : namespace; (* exported namespace *)
th_known : known_map; (* known identifiers *)
th_local : Sid.t; (* locally declared idents *)
th_used : Sid.t; (* used theories *)
}
and tdecl = private {
......@@ -125,6 +126,7 @@ type theory_uc = private {
uc_name : ident;
uc_path : string list;
uc_decls : tdecl list;
uc_ranges : lsymbol Mts.t;
uc_crcmap : Coercion.t;
uc_prefix : string list;
uc_import : namespace list;
......@@ -231,3 +233,5 @@ exception KnownMeta of meta
exception UnknownMeta of string
exception BadMetaArity of meta * int
exception MetaTypeMismatch of meta * meta_arg_type * meta_arg_type
exception RangeConflict of tysymbol
......@@ -499,7 +499,7 @@ let get_var denv v =
ev, is_mutable
with Not_found ->
let l =
Stdlib.Mstr.fold (fun s (_a,_b) acc -> s :: acc) (Dexpr.denv_contents denv) []
Stdlib.Sstr.fold (fun s acc -> s :: acc) (Dexpr.denv_names denv) []
in
Self.result "denv contains @[[%a]@]"
(Pp.print_list Pp.semi Format.pp_print_string) l;
......@@ -1135,7 +1135,7 @@ and lval denv (host,offset) =
get_var denv v
with e ->
let l =
Stdlib.Mstr.fold (fun s (_a,_b) acc -> s :: acc) (Dexpr.denv_contents denv) []
Stdlib.Sstr.fold (fun s acc -> s :: acc) (Dexpr.denv_names denv) []
in
Self.result "denv contains @[[%a]@]"
(Pp.print_list Pp.semi Format.pp_print_string) l;
......@@ -1474,7 +1474,7 @@ let fundecl denv_global fdec =
*)
(*
let l =
Stdlib.Mstr.fold (fun s (_a,_b) acc -> s :: acc) (Dexpr.denv_contents denv_global) []
Stdlib.Sstr.fold (fun s acc -> s :: acc) (Dexpr.denv_names denv_global) []
in
Self.result "denv_global contains @[[%a]@]"
(Pp.print_list Pp.semi Format.pp_print_string) l;
......@@ -1482,7 +1482,7 @@ let fundecl denv_global fdec =
let denv,def = Dexpr.drec_defn denv_global [predef] in
(*
let l =
Stdlib.Mstr.fold (fun s (_a,_b) acc -> s :: acc) (Dexpr.denv_contents denv) []
Stdlib.Sstr.fold (fun s acc -> s :: acc) (Dexpr.denv_names denv) []
in
Self.result "denv contains @[[%a]@]"
(Pp.print_list Pp.semi Format.pp_print_string) l;
......@@ -1558,7 +1558,7 @@ let global (theories,lemmas,denv,functions) g =
let denv = Dexpr.denv_add_let denv dlet_defn in
Self.result "global var %s done" vi.vname;
let l =
Stdlib.Mstr.fold (fun s (_a,_b) acc -> s :: acc) (Dexpr.denv_contents denv) []
Stdlib.Sstr.fold (fun s acc -> s :: acc) (Dexpr.denv_names denv) []
in
Self.result "denv contains @[[%a]@]"
(Pp.print_list Pp.semi Format.pp_print_string) l;
......
......@@ -553,10 +553,10 @@ module Translate = struct
let e1 = expr info e1 in
let e2 = expr info e2 in
ML.mk_expr (Mltree.Ewhile (e1, e2)) (Mltree.I e.e_ity) eff
| Efor (pv1, (pv2, To, pv3), _, efor) ->
| Efor (pv1, (pv2, To, pv3), _, _, efor) ->
let efor = expr info efor in
mk_for_to info pv1 pv2 pv3 efor eff
| Efor (pv1, (pv2, DownTo, pv3), _, efor) ->
| Efor (pv1, (pv2, DownTo, pv3), _, _, efor) ->
let efor = expr info efor in
mk_for_downto info pv1 pv2 pv3 efor eff
| Eghost _ -> assert false
......
......@@ -453,11 +453,11 @@ and dfun_defn = preid * ghost * rs_kind * dbinder list *
type denv = {
frozen : dity list;
locals : (Stv.t option * dvty) Mstr.t;
locals : (bool * Stv.t option * dvty) Mstr.t;
excpts : dxsymbol Mstr.t
}
let denv_contents d = d.locals
let denv_names d = Mstr.domain d.locals
let denv_empty = { frozen = []; locals = Mstr.empty; excpts = Mstr.empty }
......@@ -487,19 +487,19 @@ let denv_add_exn { frozen = fz; locals = ls; excpts = xs } id dity =
{ frozen = freeze_dvty fz ([], dity); locals = ls; excpts = xs }
let denv_add_mono { frozen = fz; locals = ls; excpts = xs } id dvty =
let ls = Mstr.add id.pre_name (None, dvty) ls in
let ls = Mstr.add id.pre_name (false, None, dvty) ls in
{ frozen = freeze_dvty fz dvty; locals = ls; excpts = xs }
let denv_add_poly { frozen = fz; locals = ls; excpts = xs } id dvty =
let ls = Mstr.add id.pre_name (Some (free_vars fz dvty), dvty) ls in
let ls = Mstr.add id.pre_name (false, Some (free_vars fz dvty), dvty) ls in
{ frozen = fz; locals = ls; excpts = xs }
let denv_add_rec_mono { frozen = fz; locals = ls; excpts = xs } id dvty =
let ls = Mstr.add id.pre_name (Some Stv.empty, dvty) ls in
let ls = Mstr.add id.pre_name (false, Some Stv.empty, dvty) ls in
{ frozen = freeze_dvty fz dvty; locals = ls; excpts = xs }
let denv_add_rec_poly { frozen = fz; locals = ls; excpts = xs } fz0 id dvty =
let ls = Mstr.add id.pre_name (Some (free_vars fz0 dvty), dvty) ls in
let ls = Mstr.add id.pre_name (false, Some (free_vars fz0 dvty), dvty) ls in
{ frozen = fz; locals = ls; excpts = xs }
let denv_add_rec denv fz0 id ((argl,res) as dvty) =
......@@ -515,6 +515,12 @@ let denv_add_rec denv fz0 id ((argl,res) as dvty) =
let denv_add_var denv id dity = denv_add_mono denv id ([], dity)
let denv_add_for_index denv id dvty =
let dvty = [], dity_of_dvty dvty in
let { frozen = fz; locals = ls; excpts = xs } = denv in
let ls = Mstr.add id.pre_name (true, None, dvty) ls in
{ frozen = freeze_dvty fz dvty; locals = ls; excpts = xs }
let denv_add_let denv (id,_,_,({de_dvty = dvty} as de)) =
if fst dvty = [] then denv_add_mono denv id dvty else
let rec is_value de = match de.de_node with
......@@ -529,19 +535,19 @@ let denv_add_args { frozen = fz; locals = ls; excpts = xs } bl =
let l = List.fold_left (fun l (_,_,t) -> t::l) fz bl in
let add s (id,_,t) = match id with
| Some {pre_name = n} ->
Mstr.add_new (Dterm.DuplicateVar n) n (None, ([],t)) s
Mstr.add_new (Dterm.DuplicateVar n) n (false, None, ([],t)) s
| None -> s in
let s = List.fold_left add Mstr.empty bl in
{ frozen = l; locals = Mstr.set_union s ls; excpts = xs }
let denv_add_pat { frozen = fz; locals = ls; excpts = xs } dp =
let l = Mstr.fold (fun _ t l -> t::l) dp.dp_vars fz in
let s = Mstr.map (fun t -> None, ([], t)) dp.dp_vars in
let s = Mstr.map (fun t -> false, None, ([], t)) dp.dp_vars in
{ frozen = l; locals = Mstr.set_union s ls; excpts = xs }
let mk_node n = function
| Some tvs, dvty -> DEvar (n, specialize_scheme tvs dvty)
| None, dvty -> DEvar (n, dvty)
| _, Some tvs, dvty -> DEvar (n, specialize_scheme tvs dvty)
| _, None, dvty -> DEvar (n, dvty)
let denv_get denv n =
mk_node n (Mstr.find_exn (Dterm.UnboundVar n) n denv.locals)
......@@ -566,9 +572,10 @@ let denv_pure denv get_dty =
let f = Dterm.dty_fresh () in Htv.add ht v (f,d); f end
| Dapp (s,dl,_) -> Dterm.dty_app s.its_ts (List.map fold dl)
| Dutv v -> Dterm.dty_var v in
let pure_denv = Mstr.mapi (fun n (_, dvty) ->
Dterm.DTvar (n, fold (dity_of_dvty dvty))) denv.locals in
let dty = get_dty pure_denv in
let add n (idx, _, dvty) =
let dity = if idx then dity_int else dity_of_dvty dvty in
Dterm.DTvar (n, fold dity) in
let dty = get_dty (Mstr.mapi add denv.locals) in
Htv.iter (fun v (f,_) ->
try Dterm.dty_match f (ty_var v) with Exit -> ()) ht;
let fnS s dl = dity_app_fresh (restore_its s) dl in
......@@ -628,8 +635,8 @@ let drec_defn denv0 prel =
"This function is expected to be polymorphic in type variable %a"
Pretty.print_tv tv in
begin match Mstr.find_opt id.pre_name denv1.locals with
| Some (Some tvs, _) -> Stv.iter check tvs
| Some (None, _) | None -> assert false
| Some (_, Some tvs, _) -> Stv.iter check tvs
| Some (_, None, _) | None -> assert false
end;
let argl = List.map (fun (_,_,t) -> t) bl in
denv_add_poly denv id (argl, res) in
......@@ -761,8 +768,9 @@ let dexpr ?loc node =
dexpr_expected_type de2 dity_unit;
dvty_unit
| DEfor (_,de_from,_,de_to,_,de) ->
dexpr_expected_type de_from dity_int;
dexpr_expected_type de_to dity_int;
let bty = dity_fresh () in
dexpr_expected_type de_from bty;
dexpr_expected_type de_to bty;
dexpr_expected_type de dity_unit;
dvty_unit
| DEtry (_,[]) ->
......@@ -970,6 +978,7 @@ type env = {
pvm : pvsymbol Mstr.t;
xsm : xsymbol Mstr.t;
old : (pvsymbol Mstr.t * (let_defn * pvsymbol) Hpv.t) Mstr.t;
idx : pvsymbol Mpv.t; (* external-to-internal loop indexes *)
ghs : bool; (* we are under DEghost or in a ghost function *)
lgh : bool; (* we are under let ghost c = <cexp> *)
cgh : bool; (* we are under DEghost in a cexp *)
......@@ -981,6 +990,7 @@ let env_empty = {
pvm = Mstr.empty;
xsm = Mstr.empty;
old = Mstr.empty;
idx = Mpv.empty;
ghs = false;
lgh = false;
cgh = false;
......@@ -1010,7 +1020,10 @@ let find_old pvm (ovm,old) v =
let register_old env v l =
find_old env.pvm (Mstr.find_exn (UnboundLabel l) l env.old) v
let get_later env later = later env.pvm env.xsm (register_old env)
let get_later env later =
let pvm = if Mpv.is_empty env.idx then env.pvm else
Mstr.map (fun v -> Mpv.find_def v v env.idx) env.pvm in
later pvm env.xsm (register_old env)
let add_label ({pvm = pvm; old = old} as env) l =
let ht = Hpv.create 3 in
......@@ -1306,9 +1319,13 @@ and try_expr uloc env ({de_dvty = argl,res} as de0) =
let e_to = expr uloc env de_to in
let v = create_pvsymbol id ity_int in
let env = add_pvsymbol env v in
let i = if ity_equal v.pv_ity ity_int then v else
create_pvsymbol id ~ghost:true ity_int in
let env = if pv_equal i v then env else
{ env with idx = Mpv.add v i env.idx } in
let e = expr uloc env de in
let inv = get_later env dinv in
e_for v e_from dir e_to (create_invariant inv) e
e_for v e_from dir e_to i (create_invariant inv) e
| DEtry (de1,bl) ->
let e1 = expr uloc env de1 in
let add_branch m (xs,dp,de) =
......
......@@ -153,6 +153,8 @@ val denv_add_args : denv -> dbinder list -> denv
val denv_add_pat : denv -> dpattern -> denv
val denv_add_for_index : denv -> preid -> dvty -> denv
val denv_add_exn : denv -> preid -> dity -> denv
val denv_get : denv -> string -> dexpr_node (** raises UnboundVar *)
......@@ -163,7 +165,7 @@ val denv_get_exn : denv -> string -> dxsymbol (** raises Not_found *)
val denv_get_exn_opt : denv -> string -> dxsymbol option
val denv_contents : denv -> (Ty.Stv.t option * dvty) Mstr.t
val denv_names : denv -> Sstr.t
val denv_pure : denv -> (Dterm.denv -> Dterm.dty) -> dity
......
......@@ -323,7 +323,7 @@ and expr_node =
| Eif of expr * expr * expr
| Ecase of expr * (prog_pattern * expr) list
| Ewhile of expr * invariant list * variant list * expr
| Efor of pvsymbol * for_bounds * invariant list * expr
| Efor of pvsymbol * for_bounds * pvsymbol * invariant list * expr
| Etry of expr * (pvsymbol list * expr) Mxs.t
| Eraise of xsymbol * expr
| Eexn of xsymbol * expr
......@@ -385,7 +385,7 @@ let c_ghost c = c.c_cty.cty_effect.eff_ghost
let e_fold fn acc e = match e.e_node with
| Evar _ | Econst _ | Eexec _ | Eassign _
| Eassert _ | Epure _ | Eabsurd -> acc
| Eraise (_,e) | Efor (_,_,_,e) | Eghost e
| Eraise (_,e) | Efor (_,_,_,_,e) | Eghost e
| Elet ((LDsym _|LDrec _), e) | Eexn (_,e) -> fn acc e
| Elet (LDvar (_,d), e) | Ewhile (d,_,_,e) -> fn (fn acc d) e
| Eif (c,d,e) -> fn (fn (fn acc c) d) e
......@@ -860,25 +860,37 @@ let e_not e = e_if e e_false e_true
(* loops *)
let e_for_raw v ((f,_,t) as bounds) inv e =
ity_equal_check v.pv_ity ity_int;
ity_equal_check f.pv_ity ity_int;
ity_equal_check t.pv_ity ity_int;
let e_for_raw v ((f,_,t) as bounds) i inv e =
ity_equal_check f.pv_ity v.pv_ity;
ity_equal_check t.pv_ity v.pv_ity;
ity_equal_check i.pv_ity ity_int;
ity_equal_check e.e_ity ity_unit;
if not (pv_equal v i) then begin
if not i.pv_ghost then Loc.errorm
"The internal for-loop index mush be ghost";
let check f = if t_v_occurs v.pv_vs f > 0 then Loc.errorm
"The external for-loop index cannot occur in the invariant" in
List.iter check inv;
match v.pv_ity.ity_node with
| Ityapp ({its_def = Range _},_,_) -> ()
| _ when ity_equal v.pv_ity ity_int -> ()
| _ -> Loc.errorm "For-loop bounds must have an integer type"
end;
let vars = List.fold_left t_freepvs Spv.empty inv in
let ghost = v.pv_ghost || f.pv_ghost || t.pv_ghost in
let eff = try_effect [e] eff_read_pre vars e.e_effect in
let eff = try_effect [e] eff_ghostify ghost eff in
ignore (try_effect [e] eff_union_seq eff eff);
let eff = eff_bind_single v eff in
let eff = eff_bind_single i eff in
let eff = eff_read_single_pre t eff in
let eff = eff_read_single_pre f eff in
mk_expr (Efor (v,bounds,inv,e)) e.e_ity MaskVisible eff
mk_expr (Efor (v,bounds,i,inv,e)) e.e_ity MaskVisible eff
let e_for v f dir t inv e =
let e_for v f dir t i inv e =
let hd, t = mk_proxy false t [] in
let hd, f = mk_proxy false f hd in
let_head hd (e_for_raw v (f,dir,t) inv e)
let_head hd (e_for_raw v (f,dir,t) i inv e)
let e_while d inv vl e =
ity_equal_check d.e_ity ity_bool;
......@@ -1011,7 +1023,7 @@ let rec e_rs_subst sm e = e_label_copy e (match e.e_node with
let sm = List.fold_left2 add sm fdl nfdl in
e_let (LDrec nfdl) (e_rs_subst sm e)
| Eif (c,d,e) -> e_if (e_rs_subst sm c) (e_rs_subst sm d) (e_rs_subst sm e)
| Efor (v,b,inv,e) -> e_for_raw v b inv (e_rs_subst sm e)
| Efor (v,b,i,inv,e) -> e_for_raw v b i inv (e_rs_subst sm e)
| Ewhile (d,inv,vl,e) -> e_while (e_rs_subst sm d) inv vl (e_rs_subst sm e)
| Eraise (xs,d) -> e_raise xs (e_rs_subst sm d) e.e_ity
| Ecase (d,bl) -> e_case (e_rs_subst sm d)
......@@ -1336,9 +1348,11 @@ and print_enode pri fmt e = match e.e_node with
| Ewhile (d,inv,varl,e) ->
fprintf fmt "@[<hov 2>while %a do%a%a@\n%a@]@\ndone"
print_expr d print_invariant inv print_variant varl print_expr e
| Efor (pv,(pvfrom,dir,pvto),inv,e) ->
fprintf fmt "@[<hov 2>for %a =@ %a@ %s@ %a@ %ado@\n%a@]@\ndone"
print_pv pv print_pv pvfrom
| Efor (pv,(pvfrom,dir,pvto),i,inv,e) ->
let print_i fmt i =
if not (pv_equal pv i) then fprintf fmt "(%a)" print_pv i in
fprintf fmt "@[<hov 2>for %a%a =@ %a@ %s@ %a@ %ado@\n%a@]@\ndone"
print_pv pv print_i i print_pv pvfrom
(if dir = To then "to" else "downto") print_pv pvto
print_invariant inv print_expr e
| Eexn (xs, e) ->
......
......@@ -131,7 +131,7 @@ and expr_node =
| Eif of expr * expr * expr
| Ecase of expr * (prog_pattern * expr) list
| Ewhile of expr * invariant list * variant list * expr
| Efor of pvsymbol * for_bounds * invariant list * expr
| Efor of pvsymbol * for_bounds * pvsymbol * invariant list * expr
| Etry of expr * (pvsymbol list * expr) Mxs.t
| Eraise of xsymbol * expr
| Eexn of xsymbol * expr
......@@ -237,8 +237,8 @@ val e_case : expr -> (prog_pattern * expr) list -> expr
val e_while : expr -> invariant list -> variant list -> expr -> expr
val e_for : pvsymbol ->
expr -> for_direction -> expr -> invariant list -> expr -> expr
val e_for : pvsymbol -> expr -> for_direction -> expr ->
pvsymbol -> invariant list -> expr -> expr
val e_assert : assertion_kind -> term -> expr
......
......@@ -218,8 +218,8 @@ let get_syms node pure =
| Eexn (xs, e) ->
let esms = syms_expr Sid.empty e in
Sid.union syms (Sid.remove xs.xs_name esms)
| Efor (i,_,invl,e) ->
syms_pv (syms_tl (syms_expr syms e) invl) i
| Efor (v,_,i,invl,e) ->
syms_pv (syms_pv (syms_tl (syms_expr syms e) invl) i) v
| Ewhile (d,invl,varl,e) ->
let syms = syms_varl (syms_expr syms e) varl in
syms_tl (syms_eity syms d) invl
......
......@@ -594,7 +594,7 @@ let rec eval_expr env (e : expr) : result =
end
| r -> r
end
| Efor(pvs,(pvs1,dir,pvs2),_inv,e1) ->
| Efor(pvs,(pvs1,dir,pvs2),_i,_inv,e1) ->
begin
try
let a = big_int_of_value (get_pvs env pvs1) in
......
......@@ -408,9 +408,11 @@ let add_use uc d = Sid.fold (fun id uc ->
| Some n -> use_export uc (tuple_module n)
| None -> uc) (Mid.set_diff d.pd_syms uc.muc_known) uc
let mk_vc uc d = Vc.vc uc.muc_env uc.muc_known uc.muc_theory d
let add_pdecl ?(warn=true) ~vc uc d =
let uc = add_use uc d in
let dl = if vc then Vc.vc uc.muc_env uc.muc_known d else [] in
let dl = if vc then mk_vc uc d else [] in
(* verification conditions must not add additional dependencies
on built-in theories like TupleN or HighOrd. Also, we expect
int.Int or any other library theory to be in the context:
......@@ -912,12 +914,14 @@ let rec clone_expr cl sm e = e_label_copy e (match e.e_node with
| Ewhile (c,invl,varl,e) ->
e_while (clone_expr cl sm c) (clone_invl cl sm invl)
(clone_varl cl sm varl) (clone_expr cl sm e)
| Efor (i, (f,dir,t), invl, e) ->
let i' = clone_pv cl i in
let ism = sm_save_pv sm i i' in
e_for i'
| Efor (v, (f,dir,t), i, invl, e) ->
let v' = clone_pv cl v in
let ism = sm_save_pv sm v v' in
let i' = if pv_equal v i then v' else clone_pv cl i in
let ism = if pv_equal v i then ism else sm_save_pv ism i i' in
e_for v'
(e_var (sm_find_pv sm f)) dir (e_var (sm_find_pv sm t))
(clone_invl cl ism invl) (clone_expr cl ism e)
i' (clone_invl cl ism invl) (clone_expr cl ism e)
| Etry (d, xl) ->
let conv_br xs (vl, e) m =
let vl' = List.map (clone_pv cl) vl in
......@@ -1032,7 +1036,7 @@ let clone_pdecl inst cl uc d = match d.pd_node with
(* FIXME check ghost status and mask of cexp/ld wrt rs *)
(* FIXME check effects of cexp/ld wrt rs *)
(* FIXME add correspondance for "let lemma" to cl.pr_table *)
let dl = Vc.vc uc.muc_env uc.muc_known (create_let_decl ld) in
let dl = mk_vc uc (create_let_decl ld) in
List.fold_left (add_pdecl_raw ~warn:false) uc dl
| PDlet ld ->
begin match ld with
......
......@@ -61,6 +61,7 @@ let vc_labels = Slab.add kp_label
type vc_env = {
known_map : Pdecl.known_map;
ts_ranges : lsymbol Mts.t;
ps_int_le : lsymbol;
ps_int_ge : lsymbol;
ps_int_lt : lsymbol;
......@@ -70,8 +71,9 @@ type vc_env = {
exn_count : int ref;
}
let mk_env {Theory.th_export = ns} kn = {
let mk_env {Theory.th_export = ns} kn tuc = {
known_map = kn;
ts_ranges = tuc.Theory.uc_ranges;
ps_int_le = Theory.ns_find_ls ns ["infix <="];
ps_int_ge = Theory.ns_find_ls ns ["infix >="];
ps_int_lt = Theory.ns_find_ls ns ["infix <"];
......@@ -89,7 +91,7 @@ let new_exn env = incr env.exn_count; !(env.exn_count)
(* FIXME: cannot verify int.why because of a cyclic dependency.
int.Int is used for the "for" loops and for integer variants.
We should be able to extract the necessary lsymbols from kn. *)
let mk_env env kn = mk_env (Env.read_theory env ["int"] "Int") kn
let mk_env env kn tuc = mk_env (Env.read_theory env ["int"] "Int") kn tuc
(* explanation labels *)
......@@ -736,9 +738,16 @@ let rec k_expr env lps ({e_loc = loc} as e) res xmap =
let k = Kseq (Kval ([], prev), 0, bind_oldies oldies k) in
let k = List.fold_right assume_inv iinv k in
Kpar (j, k_havoc e.e_effect k)
| Efor (v, ({pv_vs = a}, d, {pv_vs = b}), invl, e1) ->
let a = t_var a and b = t_var b in
let i = t_var v.pv_vs and one = t_nat_const 1 in
| Efor (vx, (a, d, b), vi, invl, e1) ->
let int_of_pv = match vx.pv_vs.vs_ty.ty_node with
| Tyapp (s,_) when ts_equal s ts_int ->
fun v -> t_var v.pv_vs
| Tyapp (s,_) ->
let s = Mts.find s env.ts_ranges in
fun v -> fs_app s [t_var v.pv_vs] ty_int
| Tyvar _ -> assert false (* never *) in
let a = int_of_pv a and i = t_var vi.pv_vs in
let b = int_of_pv b and one = t_nat_const 1 in
let init = wp_of_inv None lab expl_loop_init invl in
let prev = sp_of_inv None lab expl_loop_init invl in
let keep = wp_of_inv None lab expl_loop_keep invl in
......@@ -749,14 +758,20 @@ let rec k_expr env lps ({e_loc = loc} as e) res xmap =
let expl_bounds f = vc_expl loc lab expl_for_bound f in
let i_pl_1 = fs_app pl [i; one] ty_int in
let b_pl_1 = fs_app pl [b; one] ty_int in
let init = t_subst_single v.pv_vs a init in
let keep = t_subst_single v.pv_vs i_pl_1 keep in
let last = t_subst_single v.pv_vs b_pl_1 prev in
let init = t_subst_single vi.pv_vs a init in
let keep = t_subst_single vi.pv_vs i_pl_1 keep in
let last = t_subst_single vi.pv_vs b_pl_1 prev in
let iinv = inv_of_loop env e.e_loc invl [] in
let j = List.fold_right assert_inv iinv (Kstop init) in
let k = List.fold_right assert_inv iinv (Kstop keep) in
let k = Kseq (k_expr env lps e1 res xmap, 0, k) in
let k = Kseq (Kval ([v], sp_and bounds prev), 0, k) in
let k =
if pv_equal vx vi then
Kseq (Kval ([vx], sp_and bounds prev), 0, k)
else
Kseq (Kval ([vx], t_true), 0,
Kseq (Klet (vi, int_of_pv vx, sp_and bounds prev), 0, k))
in
let k = Kpar (k, Kval ([res], last)) in
let k = List.fold_right assume_inv iinv k in
let k = Kpar (j, k_havoc e.e_effect k) in
......@@ -1369,13 +1384,13 @@ let mk_vc_decl kn id f =
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
let vc env kn tuc d = match d.pd_node with
| PDlet (LDsym (s, {c_node = Cfun e; c_cty = cty})) ->
let env = mk_env env kn in
let env = mk_env env kn tuc in
let f = vc_fun env (Debug.test_noflag debug_sp) cty e in
[mk_vc_decl kn s.rs_name f]
| PDlet (LDrec rdl) ->
let env = mk_env env kn in
let env = mk_env env kn tuc in
let fl = vc_rec env (Debug.test_noflag debug_sp) rdl in
List.map2 (fun rd f -> mk_vc_decl kn rd.rec_sym.rs_name f) rdl fl
| _ -> []
......@@ -11,4 +11,4 @@
open Pdecl
val vc : Env.env -> known_map -> pdecl -> pdecl list
val vc : Env.env -> known_map -> Theory.theory_uc -> pdecl -> pdecl list
......@@ -730,7 +730,7 @@ let rec dexpr muc denv {expr_desc = desc; expr_loc = loc} =
let eto = dexpr muc denv eto in
let inv = dinvariant muc inv in
let id = create_user_id id in
let denv = denv_add_var denv id (dity_of_ity ity_int) in
let denv = denv_add_for_index denv id efrom.de_dvty in
DEfor (id, efrom, dir, eto, inv, dexpr muc denv e1)
| Ptree.Eassign asl ->
let mk_assign (e1,q,e2) =
......
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