Commit c4a8d097 authored by Raphaël Rieu-Helft's avatar Raphaël Rieu-Helft

WIP add alias keyword

parent bdec33a5
module C
use import mach.int.Int32
type ptr 'a = private {
mutable data : 'a;
offset : int ;
}
val incr (p:ptr 'a) (ofs:int32) : ptr 'a
ensures { result.offset = p.offset + Int32.to_int ofs }
ensures { result.data = p.data }
alias { p.data ~ result.data }
end
\ No newline at end of file
......@@ -378,6 +378,7 @@ type dspec_final = {
ds_xpost : (pvsymbol * term) list Mxs.t;
ds_reads : pvsymbol list;
ds_writes : term list;
ds_alias : (term * term) list;
ds_diverge : bool;
ds_checkrw : bool;
}
......@@ -773,7 +774,15 @@ let create_assert = to_fmla
let create_invariant pl = List.map to_fmla pl
let create_post ity ql = List.map (fun (v,f) ->
ity_equal_check ity v.pv_ity; Ity.create_post v.pv_vs (to_fmla f)) ql
try
ity_equal_check ity v.pv_ity;
Ity.create_post v.pv_vs (to_fmla f)
with TypeMismatch _ ->
let ty = ty_of_ity ity in
ty_equal_check ty (ty_of_ity v.pv_ity);
let preid = Ident.id_clone v.pv_vs.vs_name in
Ity.create_post (create_vsymbol preid ty) (to_fmla f)
) ql
let create_xpost xql = Mxs.mapi (fun xs ql -> create_post xs.xs_ity ql) xql
......@@ -819,6 +828,22 @@ let effect_of_dspec dsp =
let eff = if dsp.ds_diverge then eff_diverge eff else eff in
wl, eff
let alias_of_dspec dsp ity =
let add_alias (sbs, regs) (t, rt) = (* FIXME conflicts + result on right *)
match (effect_of_term t, effect_of_term rt) with
| (_, ({ity_node = Ityreg reg} as ity), _),
(_, ({ity_node = Ityreg _} as rity), _) ->
(ity_match sbs rity ity, Sreg.add reg regs)
| (_, {ity_node = Ityreg _}, _), _ ->
Loc.errorm ?loc:rt.t_loc "mutable expression expected"
| _ ->
Loc.errorm ?loc:t.t_loc "mutable expression expected" in
let sbs, regs =
List.fold_left add_alias (isb_empty, Sreg.empty) dsp.ds_alias in
let ity = ity_full_inst sbs ity in
let regs = Sreg.fold (fun r acc -> reg_freeregs acc r) regs regs in (* FIXME ? *)
ity, regs
(* TODO: add warnings for empty postconditions (anywhere)
and empty exceptional postconditions (toplevel). *)
let check_spec inr dsp ecty ({e_loc = loc} as e) =
......@@ -1002,9 +1027,11 @@ let cty_of_spec env bl mask dsp dity =
let env, old = add_label env "0" in
let dsp = get_later env dsp ity in
let _, eff = effect_of_dspec dsp in
let ity, regs = alias_of_dspec dsp ity in
let eff = eff_ghostify env.ghs eff in
let eff = eff_reset_overwritten eff in
let eff = eff_reset eff (ity_freeregs Sreg.empty ity) in
let res = Sreg.diff (ity_freeregs Sreg.empty ity) regs in
let eff = eff_reset eff res in
let p = rebase_pre env preold old dsp.ds_pre in
let q = create_post ity dsp.ds_post in
let xq = create_xpost dsp.ds_xpost in
......
......@@ -67,6 +67,7 @@ type dspec_final = {
ds_xpost : (pvsymbol * term) list Mxs.t;
ds_reads : pvsymbol list;
ds_writes : term list;
ds_alias : (term * term) list;
ds_diverge : bool;
ds_checkrw : bool;
}
......
......@@ -60,6 +60,7 @@
(* programs *)
"abstract", ABSTRACT;
"absurd", ABSURD;
"alias", ALIAS;
"any", ANY;
"assert", ASSERT;
"assume", ASSUME;
......@@ -199,6 +200,8 @@ rule token = parse
{ EQUAL }
| "<>"
{ LTGT }
| "~"
{ TILDE }
| "["
{ LEFTSQ }
| "]"
......
......@@ -72,6 +72,7 @@
sp_xpost = [];
sp_reads = [];
sp_writes = [];
sp_alias = [];
sp_variant = [];
sp_checkrw = false;
sp_diverge = false;
......@@ -83,6 +84,7 @@
sp_xpost = s1.sp_xpost @ s2.sp_xpost;
sp_reads = s1.sp_reads @ s2.sp_reads;
sp_writes = s1.sp_writes @ s2.sp_writes;
sp_alias = s1.sp_alias @ s2.sp_alias;
sp_variant = variant_union s1.sp_variant s2.sp_variant;
sp_checkrw = s1.sp_checkrw || s2.sp_checkrw;
sp_diverge = s1.sp_diverge || s2.sp_diverge;
......@@ -136,7 +138,7 @@
%token DIVERGES DO DONE DOWNTO ENSURES EXCEPTION FOR
%token FUN GHOST INVARIANT LABEL MODULE MUTABLE OLD
%token PRIVATE RAISE RAISES READS REC REQUIRES RETURNS
%token TO TRY VAL VARIANT WHILE WRITES
%token TO TRY VAL VARIANT WHILE WRITES ALIAS
(* symbols *)
......@@ -147,6 +149,7 @@
%token LEFTPAR LEFTPAR_STAR_RIGHTPAR LEFTSQ
%token LARROW LRARROW OR
%token RIGHTPAR RIGHTSQ
%token TILDE
%token UNDERSCORE
%token EOF
......@@ -855,6 +858,8 @@ single_spec:
{ { empty_spec with sp_reads = $3; sp_checkrw = true } }
| WRITES LEFTBRC comma_list0(term) RIGHTBRC
{ { empty_spec with sp_writes = $3; sp_checkrw = true } }
| ALIAS LEFTBRC comma_list0(alias_pair) RIGHTBRC
{ { empty_spec with sp_alias = $3 } } (* FIXME checkrw ? *)
| RAISES LEFTBRC comma_list1(xsymbol) RIGHTBRC
{ { empty_spec with sp_xpost = [floc $startpos($3) $endpos($3), $3] } }
| DIVERGES
......@@ -862,6 +867,8 @@ single_spec:
| variant
{ { empty_spec with sp_variant = $1 } }
%inline alias_pair: term TILDE term { ($1,$3) }
ensures:
| term
{ let id = mk_id "result" $startpos $endpos in
......
......@@ -102,6 +102,7 @@ type spec = {
sp_xpost : xpost list;
sp_reads : qualid list;
sp_writes : term list;
sp_alias : (term * term) list;
sp_variant : variant;
sp_checkrw : bool;
sp_diverge : bool;
......
......@@ -505,6 +505,14 @@ let dwrites muc wl lvm =
let dwrites t = type_term muc lvm old t in
List.map dwrites wl
let dalias muc al lvm =
let old _ _ = Loc.errorm
"`at' and `old' cannot be used in the `alias' clause" in
let dalias (t1,t2) =
(type_term muc lvm old t1, type_term muc lvm old t2) in
List.map dalias al
let find_variant_ls muc q = match find_lsymbol muc.muc_theory q with
| { ls_args = [u;v]; ls_value = None } as ls when ty_equal u v -> ls
| s -> Loc.errorm ~loc:(qloc q) "Not an order relation: %a" Pretty.print_ls s
......@@ -520,6 +528,7 @@ let dspec muc sp lvm old ity = {
ds_xpost = dxpost muc sp.sp_xpost lvm old;
ds_reads = dreads muc sp.sp_reads lvm;
ds_writes = dwrites muc sp.sp_writes lvm;
ds_alias = dalias muc sp.sp_alias lvm;
ds_checkrw = sp.sp_checkrw;
ds_diverge = sp.sp_diverge; }
......@@ -648,9 +657,11 @@ let rec dexpr muc denv {expr_desc = desc; expr_loc = loc} =
let e = match pty with
| Some pty -> { e with expr_desc = Ecast (e, pty) }
| None -> e in
let ds = match sp.sp_variant with
| ({term_loc = loc},_)::_ ->
Loc.errorm ~loc "unexpected 'variant' clause"
let ds = match (sp.sp_variant, sp.sp_alias) with
| (({term_loc = loc},_)::_,_) ->
Loc.errorm ~loc "unexpected 'variant' clause"
| (_,({term_loc = loc},_)::_) ->
Loc.errorm ~loc "unexpected 'alias' clause"
| _ -> dspec muc sp in
DEfun (bl, msk, ds, dexpr muc (denv_add_args denv bl) e)
| Ptree.Eany (pl, kind, pty, msk, sp) ->
......
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