Commit b023e8fe authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files

programs: typing now rejects aliases

parent 0c8ac354
let foo (x : ref int) (y : ref int) =
x := 1;
y := 2
parameter r : ref int
let test () =
foo r r
let foo (x : ref int) (y : ref int) =
x := 1;
y := 2
let test (x : ref int) =
foo x x
let foo (x : ref int) (y : ref int) =
x := 1;
y := 2
let test () =
let x = ref 0 in
foo x x
...@@ -112,6 +112,9 @@ let subst vs r t = ...@@ -112,6 +112,9 @@ let subst vs r t =
let apply s = Sref.fold add1 s Sref.empty in let apply s = Sref.fold add1 s Sref.empty in
{ reads = apply t.reads; writes = apply t.writes; raises = t.raises } { reads = apply t.reads; writes = apply t.writes; raises = t.raises }
let occur r t =
Sref.mem r t.reads || Sref.mem r t.writes
open Format open Format
open Pp open Pp
open Pretty open Pretty
......
...@@ -56,5 +56,7 @@ val no_side_effect : t -> bool ...@@ -56,5 +56,7 @@ val no_side_effect : t -> bool
val subst : vsymbol -> reference -> t -> t val subst : vsymbol -> reference -> t -> t
val occur : reference -> t -> bool
val print_reference : Format.formatter -> reference -> unit val print_reference : Format.formatter -> reference -> unit
val print : Format.formatter -> t -> unit val print : Format.formatter -> t -> unit
...@@ -251,6 +251,33 @@ let apply_type_v_ref env v r = match r, v with ...@@ -251,6 +251,33 @@ let apply_type_v_ref env v r = match r, v with
| _ -> | _ ->
assert false assert false
let occur_formula r f = match r with
| E.Rlocal vs -> f_occurs_single vs f
| E.Rglobal ls -> f_s_any (fun _ -> false) (ls_equal ls) f
let rec occur_type_v r = function
| Tpure _ ->
false
| Tarrow (bl, c) ->
occur_arrow r bl c
and occur_arrow r bl c = match bl with
| [] ->
occur_type_c r c
| (vs, v) :: bl ->
occur_type_v r v ||
not (E.ref_equal r (E.Rlocal vs)) && occur_arrow r bl c
and occur_type_c r c =
occur_type_v r c.c_result_type ||
occur_formula r c.c_pre ||
E.occur r c.c_effect ||
occur_post r c.c_post
and occur_post r ((_, q), ql) =
occur_formula r q ||
List.exists (fun (_, (_, qe)) -> occur_formula r qe) ql
let rec eq_type_v v1 v2 = match v1, v2 with let rec eq_type_v v1 v2 = match v1, v2 with
| Tpure ty1, Tpure ty2 -> | Tpure ty1, Tpure ty2 ->
ty_equal ty1 ty2 ty_equal ty1 ty2
......
...@@ -71,6 +71,8 @@ val purify : env -> type_v -> ty ...@@ -71,6 +71,8 @@ val purify : env -> type_v -> ty
val apply_type_v : env -> type_v -> vsymbol -> type_c val apply_type_v : env -> type_v -> vsymbol -> type_c
val apply_type_v_ref : env -> type_v -> reference -> type_c val apply_type_v_ref : env -> type_v -> reference -> type_c
val occur_type_v : reference -> type_v -> bool
val v_result : ty -> vsymbol val v_result : ty -> vsymbol
val post_map : (fmla -> fmla) -> post -> post val post_map : (fmla -> fmla) -> post -> post
......
...@@ -903,6 +903,8 @@ and expr_desc gl env loc ty = function ...@@ -903,6 +903,8 @@ and expr_desc gl env loc ty = function
make_apply loc e1 ty c make_apply loc e1 ty c
| IEapply_ref (e1, r) -> | IEapply_ref (e1, r) ->
let e1 = expr gl env e1 in let e1 = expr gl env e1 in
if occur_type_v r e1.expr_type_v then
errorm ~loc "this application would create an alias";
let c = apply_type_v_ref gl e1.expr_type_v r in let c = apply_type_v_ref gl e1.expr_type_v r in
make_apply loc e1 ty c make_apply loc e1 ty c
| IEfun (bl, t) -> | IEfun (bl, t) ->
......
let foo () = let foo (x : ref int) (y : ref int) =
{} x := 1;
any {} int {result=2} + 1 y := 2
{result=3}
let test () =
let rec div x y variant {x} = let x = ref 0 in
{ 0 <= x and 0 < y } let y = x in
if y < x then foo x y
(0, x)
else
let (q,r) = div (x-y) y in (q+1, r)
{ let (q,r) = result in x = q*y + r and 0 <= r < x }
{
type tree 'a =
| Empty
| Node (tree 'a) 'a (tree 'a)
}
let rec mem x t = match t : tree int with
| Empty -> False
| Node l y r -> x=y || mem x (if x < y then l else r)
end
let root t : 'a =
{ t <> Empty }
match t with
| Empty -> absurd
| Node _ x _ -> x
end
{ }
(* (*
Local Variables: Local Variables:
......
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