programs: fixed bug in alias detection

parent b2fedb65
module M
use import module ref.Ref
val r : ref int
let foo (x : ref int) =
x := 1;
r := 2
let test () =
foo r
end
(**************************************************************************)
(* *)
(* Copyright (C) 2010-2011 *)
(* François Bobot *)
(* Jean-Christophe Filliâtre *)
(* Claude Marché *)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Library General Public *)
(* License version 2.1, with the special exception on linking *)
(* described in file LICENSE. *)
(* *)
(* This software is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *)
(* *)
(**************************************************************************)
open Why3
open Util
open Ident
open Term
type reference =
| Rlocal of Term.vsymbol
| Rglobal of Term.lsymbol
let name_of_reference = function
| Rlocal vs -> vs.vs_name
| Rglobal ls -> ls.ls_name
let type_of_reference = function
| Rlocal vs -> vs.vs_ty
| Rglobal { ls_value = Some ty } -> ty
| Rglobal { ls_value = None } -> assert false
let ref_equal r1 r2 = match r1, r2 with
| Rlocal vs1, Rlocal vs2 -> vs_equal vs1 vs2
| Rglobal ls1, Rglobal ls2 -> ls_equal ls1 ls2
| _ -> false
let reference_of_term t = match t.t_node with
| Term.Tvar vs -> Rlocal vs
| Term.Tapp (ls, []) -> Rglobal ls
| _ -> assert false
module Reference = struct
type t = reference
let compare r1 r2 = match r1, r2 with
| Rlocal v1, Rlocal v2 -> compare (vs_hash v1) (vs_hash v2)
| Rglobal l1, Rglobal l2 -> compare (ls_hash l1) (ls_hash l2)
| Rlocal _, Rglobal _ -> -1
| Rglobal _, Rlocal _ -> 1
let equal r1 r2 = compare r1 r2 = 0
end
module Sref = Set.Make(Reference)
module Mref = Map.Make(Reference)
module E = Term.Sls
type t = {
reads : Sref.t;
writes : Sref.t;
raises : E.t;
}
let empty = { reads = Sref.empty; writes = Sref.empty; raises = E.empty }
let add_read r t = { t with reads = Sref.add r t.reads }
let add_write r t = { t with writes = Sref.add r t.writes }
let add_raise e t = { t with raises = E.add e t.raises }
let remove_reference r t =
{ t with reads = Sref.remove r t.reads; writes = Sref.remove r t.writes }
let remove_raise e t = { t with raises = E.remove e t.raises }
let union t1 t2 =
{ reads = Sref.union t1.reads t2.reads;
writes = Sref.union t1.writes t2.writes;
raises = E.union t1.raises t2.raises; }
let equal t1 t2 =
Sref.equal t1.reads t2.reads &&
Sref.equal t1.writes t2.writes &&
Sls.equal t1.raises t2.raises
let no_side_effect t =
Sref.is_empty t.writes && Sls.is_empty t.raises
let subst m t =
let add1 r' s = match r' with
| Rlocal vs' -> Sref.add (try Mvs.find vs' m with Not_found -> r') s
| _ -> Sref.add r' s
in
let apply s = Sref.fold add1 s Sref.empty in
{ 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 Pp
open Pretty
let print_reference fmt = function
| Rlocal vs -> print_vs fmt vs
| Rglobal ls -> print_ls fmt ls
let print_rset fmt s = print_list comma print_reference fmt (Sref.elements s)
let print_eset fmt s = print_list comma print_ls fmt (E.elements s)
let print fmt e =
if not (Sref.is_empty e.reads) then
fprintf fmt "@ reads %a" print_rset e.reads;
if not (Sref.is_empty e.writes) then
fprintf fmt "@ writes %a" print_rset e.writes;
if not (E.is_empty e.raises) then
fprintf fmt "@ raises %a" print_eset e.raises
(**************************************************************************)
(* *)
(* Copyright (C) 2010-2011 *)
(* François Bobot *)
(* Jean-Christophe Filliâtre *)
(* Claude Marché *)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Library General Public *)
(* License version 2.1, with the special exception on linking *)
(* described in file LICENSE. *)
(* *)
(* This software is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *)
(* *)
(**************************************************************************)
open Why3
open Term
type reference =
| Rlocal of Term.vsymbol
| Rglobal of Term.lsymbol
val name_of_reference : reference -> Ident.ident
val type_of_reference : reference -> Ty.ty
val ref_equal : reference -> reference -> bool
val reference_of_term : Term.term -> reference
module Sref : Set.S with type elt = reference
module Mref : Map.S with type key = reference
type t = private {
reads : Sref.t;
writes : Sref.t;
raises : Sls.t;
}
val empty : t
val add_read : reference -> t -> t
val add_write : reference -> t -> t
val add_raise : lsymbol -> t -> t
val remove_reference : reference -> t -> t
val remove_raise : lsymbol -> t -> t
val union : t -> t -> t
val equal : t -> t -> bool
val no_side_effect : t -> bool
val subst : reference Mvs.t -> t -> t
val occur : reference -> t -> bool
val print_reference : Format.formatter -> reference -> unit
val print : Format.formatter -> t -> unit
......@@ -629,6 +629,7 @@ and E : sig
val occur : R.t -> t -> bool
val print : Format.formatter -> t -> unit
val print_rset : Format.formatter -> Sreg.t -> unit
end = struct
......
......@@ -214,6 +214,7 @@ and E : sig
val occur : R.t -> t -> bool
val print : Format.formatter -> t -> unit
val print_rset : Format.formatter -> Sreg.t -> unit
end
......
......@@ -180,6 +180,17 @@ let rec specialize_type_v ?(policy=Region_var) ~loc htv = function
| Tpure ty ->
specialize_ty ~policy ~loc htv ty
| Tarrow (bl, c) ->
(* global regions must be different from local regions *)
let globals =
List.fold_left
(fun acc pv -> Sreg.diff acc pv.pv_regions)
(Sreg.union c.c_effect.E.reads c.c_effect.E.writes) bl
in
Sreg.iter
(fun r ->
let v = create_ty_decl_var ~user:true r.R.r_tv in
push_region_var r.R.r_tv (v, loc))
globals;
dcurrying
(List.map (fun pv -> specialize_type_v ~loc htv pv.pv_tv) bl)
(specialize_type_v ~policy:Region_ret ~loc htv c.c_result_type)
......@@ -1547,11 +1558,6 @@ and expr_desc gl env loc ty = function
| IEapply_var (e1, v) ->
let e1 = expr gl env e1 in
let vs = Mvs.find v.i_impure env in
(* TODO: alias detection *)
(* printf "e1 : %a@." print_type_v e1.expr_type_v; *)
(* printf "vs = %a@." T.print_pvsymbol vs; *)
(* if Sreg.exists (fun r -> occur_type_v r e1.expr_type_v) vs.pv_regions then *)
(* errorm ~loc "this application would create an alias"; *)
let c = apply_type_v_var e1.expr_type_v vs in
(* printf "c = %a@." print_type_c c; *)
make_apply loc e1 ty c
......@@ -1829,16 +1835,6 @@ let create_ienv denv = {
globals Mstr.empty;
}
let type_expr gl e =
let denv = create_denv gl in
let e = dexpr ~ghost:false denv e in
let ienv = create_ienv denv in
let e = iexpr gl ienv e in
let e = expr gl Mvs.empty e in
check_region_vars ();
(* fresh_expr gl ~term:true Spv.empty e; *)
e
let type_type uc ty =
let denv = create_denv uc in
let dty = Typing.dty (impure_uc uc) denv.denv ty in
......@@ -2186,7 +2182,11 @@ let find_module penv lmod q id = match q with
lmod = local modules *)
let rec decl ~wp env penv ltm lmod uc = function
| Ptree.Dlet (id, e) ->
let e = type_expr uc e in
let denv = create_denv uc in
let e = dexpr ~ghost:false denv e in
let e = iexpr uc (create_ienv denv) e in
let e = expr uc Mvs.empty e in
check_region_vars ();
if Debug.test_flag debug then
eprintf "@[--typing %s-----@\n @[<hov 2>%a@]@\n@[<hov 2>: %a@]@]@."
id.id Pgm_pretty.print_expr e print_type_v e.expr_type_v;
......@@ -2199,6 +2199,7 @@ let rec decl ~wp env penv ltm lmod uc = function
let _, dl = dletrec ~ghost:false denv dl in
let _, dl = iletrec uc (create_ienv denv) dl in
let _, dl = letrec uc Mvs.empty dl in
check_region_vars ();
let one uc (v, _, _, _ as d) =
let tyv = v.pv_tv in
let loc = loc_of_id v.pv_name in
......
......@@ -15,6 +15,7 @@ module MutualRec
end
*)
(*
module PoorArrays
use import int.Int
......@@ -33,23 +34,9 @@ module PoorArrays
{ !a.length = !(old a).length && !a.elts = M.set !(old a).elts i v }
end
*)
module Alias
use import int.Int
use import module ref.Ref
val r : ref int
let deref (x: ref int) =
!x + !r
(* TODO: should be rejected *)
let test1 () =
deref r
end
(*
module M
use import int.Int
......@@ -73,22 +60,8 @@ module M
(* let test3 () = let x = ref 0 in begin foo x (); assert { !x = 0 } end *)
end
*)
(***
module TestArray
use import int.Int
use import module array.Array
(* TODO: update *)
let f (x: array int) =
{ x.length = 2 }
x[0] <- 1;
x[1] <- 2
{ x[1] = 2 and x.length = 2 }
end
***)
(*
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