Skip to content

GitLab

Commit 9737c1b1 authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files
Options

WP: update for mutable fields

parent c5e93f64
Hide whitespace changes
Inline Side-by-side
Showing with 171 additions and 98 deletions
modules/array.mlw
View file @ 9737c1b1
......@@ -16,7 +16,7 @@ module Array
{ 0 <= i < length a } 'a reads a { result = a[i] }
parameter ([]<-) : a:array 'a -> i:int -> v:'a ->
{ 0 <= i < length a } unit writes a { a = (old a)[i <- v] }
{ 0 <= i < length a } unit writes a { a.elts = M.([<-]) (old a.elts) i v }
(* unsafe get/set operations with no precondition *)
exception OutOfBounds
......
src/programs/pgm_module.ml
View file @ 9737c1b1
......@@ -152,11 +152,13 @@ let add_pure_decl d uc =
let th = Typing.with_tuples Theory.add_decl uc.uc_pure d in
{ uc with uc_pure = th }
(**
let add_psymbol ps uc =
let uc = add_impure_decl (Decl.create_logic_decl [ps.ps_impure, None]) uc in
let uc = add_effect_decl (Decl.create_logic_decl [ps.ps_effect, None]) uc in
let uc = add_pure_decl (Decl.create_logic_decl [ps.ps_pure, None]) uc in
uc
**)
let ls_Exit = create_lsymbol (id_fresh "%Exit") [] (Some ty_exn)
......
src/programs/pgm_module.mli
View file @ 9737c1b1
......@@ -63,7 +63,7 @@ val use_export_theory : uc -> Theory.theory -> uc
exception ClashSymbol of string
val add_psymbol : psymbol -> uc -> uc
(* val add_psymbol : psymbol -> uc -> uc *)
val add_esymbol : esymbol -> uc -> uc
(* val add_mtsymbol : mtsymbol -> uc -> uc *)
val add_decl : Pgm_ttree.decl -> uc -> uc
......
src/programs/pgm_types.ml
View file @ 9737c1b1
......@@ -139,6 +139,48 @@ let make_arrow_type tyl ty =
module Sexn = Term.Sls
module R : sig
type t = private {
r_tv : tvsymbol;
r_ty : Ty.ty;
}
val compare : t -> t -> int
val create : tvsymbol -> Ty.ty -> t
val occurs_ty : t -> ty -> bool
val print : Format.formatter -> t -> unit
end = struct
type t = {
r_tv : tvsymbol;
r_ty : Ty.ty;
}
let compare r1 r2 =
Pervasives.compare (id_hash r1.r_tv.tv_name) (id_hash r2.r_tv.tv_name)
let create tv ty = {
r_tv = tv;
r_ty = ty;
}
(* FIXME: optimize *)
let occurs_ty r ty = Stv.mem r.r_tv (Ty.ty_freevars Stv.empty ty)
let print fmt r =
Format.fprintf fmt "%a(%a)" Pretty.print_tv r.r_tv Pretty.print_ty r.r_ty
end
module Mreg = Stdlib.Map.Make(R)
module Sreg = Mreg.Set
module rec T : sig
type pre = Term.term
......@@ -186,17 +228,17 @@ module rec T : sig
| PSlogic
type psymbol = {
ps_impure : lsymbol;
(* ps_impure : lsymbol; *)
ps_effect : lsymbol;
ps_pure : lsymbol;
ps_kind : psymbol_kind;
}
val create_psymbol:
impure:lsymbol -> effect:lsymbol -> pure:lsymbol -> kind:psymbol_kind ->
?impure:lsymbol -> effect:lsymbol -> pure:lsymbol -> kind:psymbol_kind ->
psymbol
val create_psymbol_fun: preid -> type_v -> psymbol
val create_psymbol_var: pvsymbol -> psymbol
val create_psymbol_fun: preid -> type_v -> lsymbol * psymbol
val create_psymbol_var: pvsymbol -> lsymbol * psymbol
val get_psymbol: lsymbol -> psymbol
......@@ -310,7 +352,7 @@ end = struct
| PSlogic
type psymbol = {
ps_impure : lsymbol;
(* ps_impure : lsymbol; *)
ps_effect : lsymbol;
ps_pure : lsymbol;
ps_kind : psymbol_kind;
......@@ -318,15 +360,14 @@ end = struct
let psymbols = Hls.create 17
let create_psymbol ~impure ~effect ~pure ~kind =
let create_psymbol ?impure ~effect ~pure ~kind =
let ps = {
ps_impure = impure;
ps_effect = effect;
ps_pure = pure;
ps_kind = kind;
}
in
Hls.add psymbols impure ps;
begin match impure with Some ls -> Hls.add psymbols ls ps | None -> () end;
Hls.add psymbols effect ps;
Hls.add psymbols pure ps;
ps
......@@ -339,7 +380,7 @@ end = struct
let impure = create v in
let effect = create ~effect:true v in
let pure = create ~pure: true v in
create_psymbol ~impure ~effect ~pure ~kind:(PSfun v)
impure, create_psymbol ~impure ~effect ~pure ~kind:(PSfun v)
let create_psymbol_var pv =
let name = pv.pv_name in
......@@ -347,22 +388,22 @@ end = struct
let impure = create_lsymbol (id_clone name) [] (Some tv) in
let effect = create_lsymbol (id_clone name) [] (Some pv.pv_effect.vs_ty) in
let pure = create_lsymbol (id_clone name) [] (Some pv.pv_pure.vs_ty) in
create_psymbol ~impure ~effect ~pure ~kind:(PSvar pv)
impure, create_psymbol ~impure ~effect ~pure ~kind:(PSvar pv)
let get_psymbol ls =
try
Hls.find psymbols ls
with Not_found ->
(* Format.eprintf "ls = %a@." Pretty.print_ls ls; *)
let ps = { ps_impure = ls; ps_effect = ls;
(* Format.eprintf "get_psymbol: ls = %a@." Pretty.print_ls ls; *)
let ps = { ps_effect = ls;
ps_pure = ls; ps_kind = PSlogic }
in
Hls.add psymbols ls ps;
ps
let ps_name ps = ps.ps_impure.ls_name
let ps_name ps = ps.ps_pure.ls_name
let ps_equal ps1 ps2 = ls_equal ps1.ps_impure ps2.ps_impure
let ps_equal ps1 ps2 = ls_equal ps1.ps_pure ps2.ps_pure
let subst_var ?(effect=false) ?(pure=false) ts s vs =
if effect && pure then invalid_arg "subst_var";
......@@ -557,43 +598,6 @@ end = struct
end
and R : sig
type t = private {
r_tv : tvsymbol;
r_ty : Ty.ty;
}
val compare : t -> t -> int
val create : tvsymbol -> Ty.ty -> t
val occurs_ty : t -> ty -> bool
val print : Format.formatter -> t -> unit
end = struct
type t = {
r_tv : tvsymbol;
r_ty : Ty.ty;
}
let compare r1 r2 =
Pervasives.compare (id_hash r1.r_tv.tv_name) (id_hash r2.r_tv.tv_name)
let create tv ty = {
r_tv = tv;
r_ty = ty;
}
(* FIXME: optimize *)
let occurs_ty r ty = Stv.mem r.r_tv (Ty.ty_freevars Stv.empty ty)
let print fmt r =
Format.fprintf fmt "%a(%a)" Pretty.print_tv r.r_tv Pretty.print_ty r.r_ty
end
and E : sig
......@@ -721,10 +725,6 @@ and Spv : sig include Set.S with type elt = T.pvsymbol end =
and Mpv : sig include Map.S with type key = T.pvsymbol end =
Map.Make(struct type t = T.pvsymbol let compare = T.compare_pvsymbol end)
and Sreg : sig include Set.S with type elt = R.t end = Set.Make(R)
and Mreg : sig include Map.S with type key = R.t end = Map.Make(R)
(* ghost code
abstract type ghost_ 'a model 'a
......
src/programs/pgm_types.mli
View file @ 9737c1b1
......@@ -61,6 +61,27 @@ val ty_exn : ty
(* val ts_label : tysymbol *)
(* regions *)
module R : sig
type t = private {
r_tv : tvsymbol;
r_ty : Ty.ty; (* effect type *)
}
val create : tvsymbol -> Ty.ty -> t
val print : Format.formatter -> t -> unit
end
module Mreg : Stdlib.Map.S with type key = R.t
module Sreg : Mreg.Set
(* exception sets *)
module Sexn : Set.S with type elt = lsymbol
(* program types *)
module rec T : sig
......@@ -108,17 +129,17 @@ module rec T : sig
| PSlogic
type psymbol = {
ps_impure : lsymbol;
(* ps_impure : lsymbol; *)
ps_effect : lsymbol;
ps_pure : lsymbol;
ps_kind : psymbol_kind;
}
val create_psymbol:
impure:lsymbol -> effect:lsymbol -> pure:lsymbol -> kind:psymbol_kind ->
?impure:lsymbol -> effect:lsymbol -> pure:lsymbol -> kind:psymbol_kind ->
psymbol
val create_psymbol_fun: preid -> type_v -> psymbol
val create_psymbol_var: pvsymbol -> psymbol
val create_psymbol_fun: preid -> type_v -> lsymbol * psymbol
val create_psymbol_var: pvsymbol -> lsymbol * psymbol
val get_psymbol: lsymbol -> psymbol
......@@ -162,23 +183,6 @@ end
and Spv : sig include Set.S with type elt = T.pvsymbol end
and Mpv : sig include Map.S with type key = T.pvsymbol end
(* regions *)
and R : sig
type t = private {
r_tv : tvsymbol;
r_ty : Ty.ty; (* effect type *)
}
val create : tvsymbol -> Ty.ty -> t
val print : Format.formatter -> t -> unit
end
and Sreg : sig include Set.S with type elt = R.t end
and Mreg : sig include Map.S with type key = R.t end
and Sexn : sig include Set.S with type elt = T.esymbol end
(* effects *)
and E : sig
......
src/programs/pgm_typing.ml
View file @ 9737c1b1
......@@ -397,7 +397,7 @@ and dexpr_desc ~ghost env loc = function
let dty = specialize_type_v ~loc htv tv in
DEglobal (ps, tv, htv), dty
| PSlogic ->
let tyl, ty = Denv.specialize_lsymbol ~loc ps.ps_impure in
let tyl, ty = Denv.specialize_lsymbol ~loc ls in
let ty = match ty with
| Some ty -> ty
| None -> dty_bool env.uc
......@@ -626,7 +626,7 @@ let region_type ts i =
let mutable_fields = Hts.create 17 (* ts -> field:int -> region:int *)
let declare_mutable_field ts i j =
Pgm_wp.declare_mutable_field ts j i;
Pgm_wp.declare_mutable_field ts i j;
let h =
try
Hts.find mutable_fields ts
......@@ -966,7 +966,7 @@ let rec print_iexpr fmt e = match e.iexpr_desc with
| IEglobal ({ ps_kind = PSvar v }, _) ->
fprintf fmt "<global var %a>" print_vs v.pv_effect
| IEglobal ({ ps_kind = PSfun v } as ps, _) ->
fprintf fmt "<global %a : %a>" print_ls ps.ps_impure T.print_type_v v
fprintf fmt "<global %a : %a>" print_ls ps.ps_effect T.print_type_v v
| IEapply (e, v) ->
fprintf fmt "@[((%a) %a)@]" print_iexpr e print_vs v.i_impure
| IEapply_var (e, v) ->
......@@ -1724,8 +1724,8 @@ let add_impure_decl uc ls =
let add_global_fun loc x tyv uc =
let x = parameter x in
try
let ps = create_psymbol_fun (id_user x loc) tyv in
let d = Decl.create_logic_decl [ps.ps_impure, None] in
let ls, ps = create_psymbol_fun (id_user x loc) tyv in
let d = Decl.create_logic_decl [ls, None] in
ps, Pgm_module.add_impure_decl d uc
with Pgm_module.ClashSymbol _ ->
errorm ~loc "clash with previous symbol %s" x
......@@ -1786,10 +1786,10 @@ let make_immutable_type td =
let add_logic_ps ?(nofail=false) uc x =
try
let get th = ns_find_ls (get_namespace th) [x] in
let impure = get (impure_uc uc) in
let effect = get (effect_uc uc) in
let pure = get (pure_uc uc) in
ignore (create_psymbol ~impure ~effect ~pure ~kind:PSlogic)
let effect = get (effect_uc uc) in
let impure = try Some (get (impure_uc uc)) with Not_found -> None in
ignore (create_psymbol ?impure ~effect ~pure ~kind:PSlogic)
with Not_found ->
(* can fail if x is a constructor of a model type (record or algebraic) *)
assert nofail
......@@ -2092,10 +2092,10 @@ let rec decl ~wp env penv ltm lmod uc = function
| Tpure _ ->
let id = id_user id.id loc in
let pv = create_pvsymbol_v id tyv in
let ps = create_psymbol_var pv in
let ls, ps = create_psymbol_var pv in
let uc = add_pure_decl uc ~loc ps.ps_pure in
let uc = add_effect_decl uc ps.ps_effect in
let uc = add_impure_decl uc ps.ps_impure in
let uc = add_impure_decl uc ls in
declare_global ps.ps_pure pv;
ps, uc
in
......
src/programs/pgm_wp.ml
View file @ 9737c1b1
......@@ -36,7 +36,7 @@ let debug = Debug.register_flag "program_wp"
(* mutable fields *)
let mutable_fields = Hts.create 17 (* ts -> region:int -> field:int *)
let mutable_fields = Hts.create 17 (* ts -> field:int -> region:int *)
let declare_mutable_field ts i j =
let h =
......@@ -47,6 +47,9 @@ let declare_mutable_field ts i j =
in
Hashtbl.add h i j
let get_mutable_field ts i =
Hashtbl.find (Hts.find mutable_fields ts) i
(* phase 4: weakest preconditions *******************************************)
(* smart constructors for building WPs
......@@ -198,6 +201,55 @@ let wp_close kn rm ef f =
let quantify_v v f = wp_forall kn v.pv_pure f in
Spv.fold quantify_v vars f
let get_ty_subst ty = match ty.ty_node with
| Tyapp (ts, tyl) ->
let add s tv ty = Mtv.add tv ty s in
List.fold_left2 add Mtv.empty ts.ts_args tyl
| Tyvar _ ->
assert false
(* x is pure, ty is effect *)
let rec update env mreg x ty =
if Mtv.is_empty mreg then
t_var x
else match ty.ty_node with
| Tyapp (ts, tyl) ->
let cl = find_constructors (get_known (effect_uc env)) ts in
if cl = [] then failwith "WP: cannot update a value of this type";
(* TODO: print the type *)
let s = get_ty_subst ty in
let branch cs =
let cs_pure = (get_psymbol cs).ps_pure in
let mk_var ty =
let ty = ty_inst s ty in
let ty_pure = purify ty in
create_vsymbol (id_fresh "y") ty_pure, ty
in
let vars = List.map mk_var cs.ls_args in
let pat_vars = List.map (fun (y, _) -> pat_var y) vars in
let pat = pat_app cs_pure pat_vars x.vs_ty in
let mk_arg i (y, ty) =
let y =
try
let j = get_mutable_field ts i in
begin match (List.nth tyl j).ty_node with
| Tyvar tv -> Mtv.find tv mreg
| Tyapp _ -> assert false
end
with Not_found ->
y
in
let keep tv _ = Stv.mem tv (ty_freevars Stv.empty ty) in
let mreg = Mtv.filter keep mreg in
update env mreg y ty
in
let t = fs_app cs_pure (list_mapi mk_arg vars) x.vs_ty in
t_close_branch pat t
in
t_case (t_var x) (List.map branch cl)
| Tyvar _ ->
assert false
(* quantify over all references in ef
ef : effect
rm : region -> pvsymbol set
......@@ -230,7 +282,9 @@ let quantify env rm ef f =
in
Mreg.fold add mreg Spv.empty
in
let mreg = Mreg.fold (fun r x -> Mtv.add r.R.r_tv x) mreg Mtv.empty in
(* s: v -> v' and vv': pv -> v', update_v *)
(****
let mreg, s, vv' =
let add pv (mreg, s, vv') = match pv.pv_effect.vs_ty.ty_node with
| Ty.Tyapp (ts, _) ->
......@@ -256,13 +310,26 @@ let quantify env rm ef f =
in
Spv.fold add vars (mreg, Mvs.empty, Mpv.empty)
in
let f = unref env s f in
let quantify_v' _pv (v', updatev) f =
t_let_close v' updatev f
****)
let vv' =
let add pv s =
let v = pv.pv_pure in
let v' = create_vsymbol (id_clone v.vs_name) v.vs_ty in
Mvs.add v v' s
in
Spv.fold add vars Mvs.empty
in
let f = unref env vv' f in
let f =
let add_update x f =
let v' = Mvs.find x.pv_pure vv' in
let updatev = update env mreg x.pv_pure x.pv_effect.vs_ty in
t_let_close_simp v' updatev f
in
Spv.fold add_update vars f
in
let f = Mpv.fold quantify_v' vv' f in
let quantify_r _ r' f = wp_forall env r' f in
Mreg.fold quantify_r mreg f
Mtv.fold quantify_r mreg f
(* let quantify ?(all=false) env rm ef f = *)
(* let r = quantify ~all env rm ef f in *)
......@@ -636,7 +703,7 @@ and f_btop env f = match f.t_node with
| _ -> TermTF.t_map (fun t -> t) (f_btop env) f
let add_wp_decl ps f uc =
let name = ps.ps_impure.ls_name in
let name = ps.ps_pure.ls_name in
let s = "WP_" ^ name.id_string in
let label = ["expl:correctness of " ^ name.id_string] in
let id = id_fresh ~label ?loc:name.id_loc s in
......@@ -651,7 +718,7 @@ let add_wp_decl ps f uc =
let decl uc = function
| Pgm_ttree.Dlet (ps, e) ->
Debug.dprintf debug "@[--effect %s-----@\n %a@]@\n----------------@."
ps.ps_impure.ls_name.id_string print_type_v e.expr_type_v;
ps.ps_pure.ls_name.id_string print_type_v e.expr_type_v;
let f = wp uc e in
Debug.dprintf debug "wp = %a@\n----------------@." Pretty.print_term f;
add_wp_decl ps f uc
......@@ -659,7 +726,7 @@ let decl uc = function
let add_one uc (ps, def) =
let f = wp_recfun uc !global_regions def in
Debug.dprintf debug "wp %s = %a@\n----------------@."
ps.ps_impure.ls_name.id_string Pretty.print_term f;
ps.ps_pure.ls_name.id_string Pretty.print_term f;
add_wp_decl ps f uc
in
List.fold_left add_one uc dl
......
tests/test-pgm-jcf.mlw
View file @ 9737c1b1
......@@ -4,7 +4,7 @@ module M
use import module array.Array
let foo (a: array int) =
{ true }
{ 1 <= a.length }
a[0] <- 1
{ a[0] = 1 }
......
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