Commit f23ed837 authored by Andrei Paskevich's avatar Andrei Paskevich

alias specification: reviewed

parent 60965332
......@@ -207,6 +207,7 @@ goods examples/avl "-L examples/avl"
goods examples/verifythis_2016_matrix_multiplication "-L examples/verifythis_2016_matrix_multiplication"
goods examples/double_wp "-L examples/double_wp"
goods examples/in_progress
goods examples/in_progress/multiprecision
echo ""
echo "=== Checking valid goals ==="
......
......@@ -7,7 +7,7 @@ module Test
val c (x:t) : t
ensures { x.f = result.f }
alias { x.f ~ result.f }
alias { x.f with result.f }
let test () =
let x = { f = 42 } in
......@@ -43,7 +43,7 @@ module A
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 }
alias { p.data with result.data }
val malloc (sz:uint32) : ptr 'a
ensures { plength result = UInt32.to_int sz }
......@@ -84,4 +84,4 @@ module A
let y = get p in
assert { y = 27 }
end
\ No newline at end of file
end
This diff is collapsed.
This diff is collapsed.
......@@ -197,8 +197,8 @@ module N
let zero = Int32.of_int 0 in
let one = Int32.of_int 1 in
let i = ref zero in
let xp = ref x in
let rp = ref r in
let xp = ref (C.incr x zero) in
let rp = ref (C.incr r zero) in
while (Int32.(<) !i sz) do
variant { p2i sz - p2i !i }
invariant { 0 <= !i <= sz }
......@@ -210,8 +210,8 @@ module N
invariant { !xp.offset = x.offset + !i }
invariant { !rp.offset = r.offset + !i }
C.set !rp (C.get !xp);
rp := C.incr !rp one;
xp := C.incr !xp one;
rp.contents <- C.incr !rp one;
xp.contents <- C.incr !xp one;
i := Int32.(+) !i one;
done
......@@ -220,9 +220,7 @@ module N
let compare_same_size (x y:t) (sz:int32) : int32
requires { valid x sz }
requires { valid y sz }
ensures { result = compare_int (value x sz)
(value y sz)
}
ensures { result = compare_int (value x sz) (value y sz) }
=
let i = ref sz in
try
......@@ -1349,7 +1347,7 @@ module N
zero r sz;
let limb_zero = Limb.of_int 0 in
let one = Int32.of_int 1 in
let rp = ref r in
let rp = ref (C.incr r (Int32.of_int 0)) in
let ly = ref limb_zero in
let c = ref limb_zero in
let i = ref (Int32.of_int 0) in
......@@ -1477,7 +1475,7 @@ module N
(value y k + power radix k * !ly)
= value x sz * value y !i
};
rp := C.incr !rp one;
rp.contents <- C.incr !rp one;
done;
value_sub_lower_bound (pelts r) r.offset (r.offset + p2i sz + p2i sz);
value_sub_upper_bound (pelts x) x.offset (x.offset + p2i sz);
......@@ -1516,7 +1514,7 @@ module N
=
let limb_zero = Limb.of_int 0 in
let one = Int32.of_int 1 in
let rp = ref r in
let rp = ref (C.incr r (Int32.of_int 0)) in
let ly = ref limb_zero in
let lr = ref limb_zero in
let c = ref limb_zero in
......@@ -1684,7 +1682,7 @@ module N
= value (old r) (!i +sz)
+ value x sz * value y !i
};
rp := C.incr !rp one;
rp.contents <- C.incr !rp one;
done;
!c
......@@ -1703,7 +1701,7 @@ module N
zero r sx;
let limb_zero = Limb.of_int 0 in
let one = Int32.of_int 1 in
let rp = ref r in
let rp = ref (C.incr r (Int32.of_int 0)) in
let ly = ref limb_zero in
let c = ref limb_zero in
let i = ref (Int32.of_int 0) in
......@@ -1831,7 +1829,7 @@ module N
(value y k + power radix k * !ly)
= value x sx * value y !i
};
rp := C.incr !rp one;
rp.contents <- C.incr !rp one;
done;
value_sub_lower_bound (pelts r) r.offset (r.offset + p2i sy + p2i sx);
value_sub_upper_bound (pelts x) x.offset (x.offset + p2i sx);
......@@ -2003,7 +2001,7 @@ module N
invariant { pelts !xp = pelts x }
invariant { !high <= radix - power 2 (cnt) }
label StartLoop in
xp := C.incr !xp minus_one;
xp.contents <- C.incr !xp minus_one;
low := C.get !xp;
let l,h = lsld_ext !low cnt in
assert { !high + h < radix };
......@@ -2011,7 +2009,7 @@ module N
value_sub_update_no_change (pelts r) (!rp).offset (r.offset + 1 + p2i !i)
(r.offset + p2i sz) v;
C.set !rp (Limb.(+) !high h);
rp := C.incr !rp minus_one;
rp.contents <- C.incr !rp minus_one;
high := l;
let ghost k = p2i !i in
i := Int32.(-) !i one;
......@@ -2116,8 +2114,8 @@ module N
let zero = Int32.of_int 0 in
let one = Int32.of_int 1 in
let msb = Int32.(-) sz one in
let xp = ref x in
let rp = ref r in
let xp = ref (C.incr x zero) in
let rp = ref (C.incr r zero) in
let high = ref (C.get !xp) in
let retval, h = lsld_ext !high tnc in
let low = ref h in
......@@ -2137,7 +2135,7 @@ module N
invariant { !low < power 2 (tnc) }
label StartLoop in
let ghost k = p2i !i in
xp := C.incr !xp one;
xp.contents <- C.incr !xp one;
high := C.get !xp;
let l,h = lsld_ext !high tnc in
assert { !low + l < radix };
......@@ -2145,7 +2143,7 @@ module N
value_sub_shift_no_change (pelts r) r.offset (p2i !i) (p2i !i) v;
C.set !rp (Limb.(+) !low l);
assert { value r k = value (r at StartLoop) k };
rp := C.incr !rp one;
rp.contents <- C.incr !rp one;
low := h;
i := Int32.(+) !i one;
value_sub_tail (pelts r) r.offset (r.offset + k);
......@@ -2638,8 +2636,8 @@ let divmod_1 (q x:t) (y:limb) (sz:int32) : limb
value_sub_update_no_change (pelts q) (!qp).offset (q.offset + 1 + p2i !i)
(q.offset + p2i sz) qu;
C.set !qp qu;
xp := C.incr !xp minus_one;
qp := C.incr !qp minus_one;
xp.contents <- C.incr !xp minus_one;
qp.contents <- C.incr !qp minus_one;
i := Int32.(-) !i one;
value_sub_head (pelts x) (x.offset + k) (x.offset + p2i sz);
value_sub_head (pelts q) (q.offset + k) (q.offset + p2i sz);
......@@ -3759,7 +3757,7 @@ let divmod_1 (q x:t) (y:limb) (sz:int32) : limb
let ghost k = p2i !i in
i := Int32.(-) !i one;
let ghost s = p2i sy + p2i !i - 1 in
xp := C.incr !xp minus_one;
xp.contents <- C.incr !xp minus_one;
let xd = C.incr !xp mdn in
let nx0 = C.get_ofs !xp one in
if (Limb.(=) !x1 dh && Limb.(=) nx0 dl) (* unlikely *)
......@@ -3928,7 +3926,7 @@ let divmod_1 (q x:t) (y:limb) (sz:int32) : limb
};
value_sub_concat (pelts x) x.offset xd.offset (x.offset + s);
x1 := C.get_ofs !xp one;
qp := C.incr !qp minus_one;
qp.contents <- C.incr !qp minus_one;
value_sub_update_no_change (pelts q) (!qp).offset
((!qp).offset + 1)
((!qp).offset + p2i sx - p2i sy - p2i !i)
......@@ -4781,7 +4779,7 @@ let divmod_1 (q x:t) (y:limb) (sz:int32) : limb
= value (xd at SubProd) sy
+ power radix sy * (!x1 at StartLoop)
- !ql * vy };
qp := C.incr !qp minus_one;
qp.contents <- C.incr !qp minus_one;
value_sub_update_no_change (pelts q) (!qp).offset
((!qp).offset + 1)
((!qp).offset + p2i sx - p2i sy - p2i !i)
......@@ -5082,7 +5080,7 @@ let divmod_1 (q x:t) (y:limb) (sz:int32) : limb
};
end
else begin
qp := C.incr !qp minus_one;
qp.contents <- C.incr !qp minus_one;
value_sub_update_no_change (pelts q) (!qp).offset
((!qp).offset + 1)
((!qp).offset + p2i sx - p2i sy - p2i !i)
......@@ -5615,7 +5613,7 @@ let divmod_1 (q x:t) (y:limb) (sz:int32) : limb
invariant { !rl + radix * !rh < dl + radix * dh }
label StartLoop in
let ghost k = p2i !i in
xp := C.incr !xp minus_one;
xp.contents <- C.incr !xp minus_one;
lx := C.get !xp;
label Got in
let (qu, r0, r1) = div3by2_inv !rh !rl !lx dh dl dinv in
......
......@@ -39,7 +39,7 @@ module C
requires { p.offset + ofs <= plength p }
ensures { result.offset = p.offset + Int32.to_int ofs }
ensures { result.data = p.data }
alias { p.data ~ result.data }
alias { p.data with result.data }
val get (p:ptr 'a) : 'a
requires { 0 <= p.offset < plength p }
......
......@@ -856,15 +856,7 @@ let create_assert = to_fmla
let create_invariant pl = List.map to_fmla pl
let create_post ity ql = List.map (fun (v,f) ->
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
ity_equal_check ity v.pv_ity; Ity.create_post v.pv_vs (to_fmla f)) ql
let create_xpost xql = Mxs.mapi (fun xs ql -> create_post xs.xs_ity ql) xql
......@@ -910,38 +902,61 @@ 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 rec subst reg ity2 ity =
let handle_alias dsp ity =
let effect_of_term t =
let v, ity, fd = effect_of_term t in
v, match fd with
| Some {rs_cty={cty_args=[arg]; cty_result=res; cty_freeze=frz}} ->
ity_full_inst (ity_match frz arg.pv_ity ity) res
| _ -> ity in
let add_alias isb (t1, t2) =
let v1, ity1 = effect_of_term t1 in
let v2, ity2 = effect_of_term t2 in
let is_res1 = v1.pv_vs.vs_name.id_string = "result" in
let is_res2 = v2.pv_vs.vs_name.id_string = "result" in
if is_res1 && is_res2 then Loc.errorm ?loc:t1.t_loc
"Only one term in an `alias' clause can refer to `result'";
if not is_res1 && not is_res2 then Loc.errorm ?loc:t1.t_loc
"One term in an `alias' clause must refer to `result'";
if match ity1.ity_node with Ityreg _ -> false | _ -> true then
Loc.errorm ?loc:t1.t_loc "mutable expression expected";
if match ity2.ity_node with Ityreg _ -> false | _ -> true then
Loc.errorm ?loc:t2.t_loc "mutable expression expected";
let isb = if is_res1 then ity_match isb ity1 ity2
else ity_match isb ity2 ity1 in
let check_var v ity = match ity.ity_node with
| Ityvar (u, false) -> tv_equal u v | _ -> false in
let check_pur v ity = match ity.ity_node with
| Ityvar (u, true) -> tv_equal u v | _ -> false in
if not (Mtv.for_all check_var isb.isb_var &&
Mtv.for_all check_pur isb.isb_pur) then
Loc.errorm ?loc:t1.t_loc "illegal `alias' clause"; (* FIXME: errmsg *)
isb in
let rec subst isb ity =
let subst = subst isb in
match ity.ity_node with
| Ityreg r when reg_equal r reg -> ity2
| Ityapp (s, l, r) ->
ity_app s (List.map (subst reg ity2) l) (List.map (subst reg ity2) r)
| Ityvar _ -> ity
| Ityreg { reg_its = s; reg_args = l; reg_regs = r } -> (* FIXME ? *)
ity_app s (List.map (subst reg ity2) l) (List.map (subst reg ity2) r)
in
let add_alias (ity, regs, conflicts) (t, rt) =
match (effect_of_term t, effect_of_term rt) with
| (_, ({ity_node = Ityreg reg} as nity), _),
(v, ({ity_node = Ityreg rreg}), _) ->
if v.pv_vs.vs_name.id_string = "result"
then
if Sreg.mem rreg conflicts
then Loc.errorm ?loc:rt.t_loc "aliasing conflict" (* FIXME *)
else (subst rreg nity ity, Sreg.add reg regs, Sreg.add rreg conflicts)
else Loc.errorm ?loc:rt.t_loc "result expected" (* FIXME ? *)
| (_, {ity_node = Ityreg _}, _), _ ->
Loc.errorm ?loc:rt.t_loc "mutable expression expected"
| _ ->
Loc.errorm ?loc:t.t_loc "mutable expression expected" in
let ity, regs, _conflicts =
List.fold_left
add_alias
(ity, Sreg.empty, Sreg.empty)
dsp.ds_alias in
let regs = Sreg.fold (fun r acc -> reg_freeregs acc r) regs regs in
(* FIXME ? *)
ity, regs
| Ityreg r when Mreg.mem r isb.isb_reg ->
Mreg.find r isb.isb_reg
| Ityreg { reg_its = s; reg_args = tl; reg_regs = rl } ->
ity_app s (List.map subst tl) (List.map subst rl)
| Ityapp (s, tl, rl) ->
ity_app_pure s (List.map subst tl) (List.map subst rl)
| Ityvar _ -> ity in
let isb = List.fold_left add_alias isb_empty dsp.ds_alias in
let res = subst isb ity in
let update (v,t) =
ity_equal_check ity v.pv_ity;
let id = id_clone v.pv_vs.vs_name in
let nv = create_pvsymbol id ~ghost:v.pv_ghost res in
nv, t_subst_single v.pv_vs (t_var nv.pv_vs) t in
let post = List.map update dsp.ds_post in
let freeze _ reg frz = ity_freeze frz reg in
let frz = Mreg.fold freeze isb.isb_reg isb_empty in
{ dsp with ds_post = post }, res, frz.isb_reg
let handle_alias dsp ity =
if dsp.ds_alias = [] then dsp, ity, Mreg.empty
else handle_alias dsp ity
(* TODO: add warnings for empty postconditions (anywhere)
and empty exceptional postconditions (toplevel). *)
......@@ -1137,20 +1152,19 @@ let add_xsymbol ({xsm = xsm} as env) xs =
(** Abstract values *)
let cty_of_spec env bl mask dspl dity =
let cty_of_spec env bl mask dsp dity =
let ity = ity_of_dity dity in
let bl = binders env.ghs bl in
let env = add_binders env bl in
let preold = Mstr.find_opt old_mark env.old in
let env, old = add_label env old_mark in
let dsp = get_later env dspl ity in
let ity, regs = alias_of_dspec dsp ity in
let dsp = get_later env dspl ity in (* FIXME ? *)
let dsp = get_later env dsp ity in
let dsp, ity, frz = handle_alias dsp ity in
let _, eff = effect_of_dspec dsp in
let eff = eff_ghostify env.ghs eff in
let eff = eff_reset_overwritten eff in
let res = Sreg.diff (ity_freeregs Sreg.empty ity) regs in
let eff = eff_reset eff res in
let rst = ity_freeregs Sreg.empty ity in
let eff = eff_reset eff (Mreg.set_diff rst frz) 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
......
......@@ -217,8 +217,6 @@ rule token = parse
{ GT }
| "<>"
{ LTGT }
| "~"
{ TILDE }
| "="
{ EQUAL }
| "-"
......
......@@ -130,11 +130,11 @@
(* program keywords *)
%token ABSTRACT ABSURD ANY ASSERT ASSUME AT BEGIN BREAK CHECK
%token CONTINUE DIVERGES DO DONE DOWNTO ENSURES EXCEPTION FOR
%token FUN GHOST INVARIANT LABEL MODULE MUTABLE OLD
%token ABSTRACT ABSURD ALIAS ANY ASSERT ASSUME AT BEGIN BREAK
%token CHECK CONTINUE DIVERGES DO DONE DOWNTO ENSURES EXCEPTION
%token FOR FUN GHOST INVARIANT LABEL MODULE MUTABLE OLD
%token PRIVATE PURE RAISE RAISES READS REC REQUIRES
%token RETURN RETURNS TO TRY VAL VARIANT WHILE WRITES ALIAS
%token RETURN RETURNS TO TRY VAL VARIANT WHILE WRITES
(* symbols *)
......@@ -145,7 +145,6 @@
%token LEFTPAR LEFTPAR_STAR_RIGHTPAR LEFTSQ
%token LARROW LRARROW OR
%token RIGHTPAR RIGHTSQ
%token TILDE
%token UNDERSCORE
%token EOF
......@@ -162,7 +161,8 @@
%nonassoc prec_no_else
%nonassoc DOT ELSE RETURN
%nonassoc prec_no_spec
%nonassoc REQUIRES ENSURES RETURNS RAISES READS WRITES ALIAS DIVERGES VARIANT
%nonassoc REQUIRES ENSURES RETURNS RAISES READS
%nonassoc WRITES ALIAS DIVERGES VARIANT
%nonassoc below_LARROW
%nonassoc LARROW
%nonassoc below_COMMA
......@@ -988,7 +988,7 @@ single_spec:
| WRITES LEFTBRC comma_list0(single_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 ? *)
{ { empty_spec with sp_alias = $3; sp_checkrw = true } }
| RAISES LEFTBRC comma_list1(xsymbol) RIGHTBRC
{ { empty_spec with sp_xpost = [floc $startpos($3) $endpos($3), $3] } }
| DIVERGES
......@@ -996,7 +996,8 @@ single_spec:
| variant
{ { empty_spec with sp_variant = $1 } }
%inline alias_pair: term TILDE term { ($1,$3) }
alias_pair:
| term WITH term { $1, $3 }
ensures:
| term
......
......@@ -543,22 +543,19 @@ let dreads muc rl lvm =
let dwrites muc wl lvm =
let old _ _ = Loc.errorm
"`at' and `old' cannot be used in the `writes' clause" in
"`at' and `old' cannot be used in a `writes' clause" in
let dwrites t = type_term muc lvm old t in
List.map dwrites wl
let dalias muc al lvm ity =
let old _ _ = Loc.errorm
"`at' and `old' cannot be used in the `alias' clause" in
"`at' and `old' cannot be used in an `alias' clause" in
let dalias (t1,t2) =
(type_term muc lvm old t1,
(* result only allowed on the right *)
let v = create_pvsymbol (id_fresh "result") ity in
let lvm = Mstr.add "result" v lvm in
type_term muc lvm old t2) in
let v = create_pvsymbol (id_fresh "result") ity in
let lvm = Mstr.add "result" v lvm in
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
......@@ -721,10 +718,7 @@ let rec dexpr muc denv {expr_desc = desc; expr_loc = loc} =
DErec (rd, dexpr muc denv e1)
| Ptree.Efun (bl, pty, msk, sp, e) ->
let bl = List.map (dbinder muc) bl in
let ds = match sp.sp_alias with
| ({term_loc = loc},_)::_ ->
Loc.errorm ~loc "unexpected 'alias' clause"
| _ -> dspec_no_variant muc sp in
let ds = dspec_no_variant muc sp in
let dity = dity_of_opt muc pty in
let denv = denv_add_args denv bl in
DEfun (bl, dity, msk, ds, dexpr muc denv e)
......
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