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

programs: WP computed differently (code moved to pgm_fastwp.ml for later use)

parent e54cc00c
......@@ -26,6 +26,20 @@ 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
module Reference = struct
type t = reference
......
......@@ -24,6 +24,10 @@ 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
module Sref : Set.S with type elt = reference
module Mref : Map.S with type key = reference
......
(**************************************************************************)
(* *)
(* Copyright (C) 2010- *)
(* Francois Bobot *)
(* Jean-Christophe Filliatre *)
(* Johannes Kanig *)
(* 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. *)
(* *)
(**************************************************************************)
(* CURRENTLY DEAD CODE; FOR LATER USE... *)
open Format
open Why
open Ident
open Ty
open Term
open Decl
open Theory
open Pgm_ttree
open Pgm_itree
open Pgm_typing
module E = Pgm_effect
module State : sig
type t
val create : env -> E.t -> t
val push_label : env -> ?label:label -> t -> label * t
val havoc : env -> ?pre:label -> E.t -> t -> t
val term : env -> t -> term -> term
val fmla : env -> ?old:label -> t -> fmla -> fmla
val quantify : env -> t -> E.t -> fmla -> fmla
end = struct
type t = {
current : vsymbol E.Mref.t;
old : vsymbol E.Mref.t Mvs.t;
}
let unref_ty env ty = match ty.ty_node with
| Tyapp (ts, [ty]) when ts_equal ts (ts_ref env) -> ty
| _ -> assert false
let var_of_reference env = function
| E.Rlocal vs ->
create_vsymbol (id_fresh vs.vs_name.id_string) (unref_ty env vs.vs_ty)
| E.Rglobal { ls_name = id; ls_value = Some ty } ->
create_vsymbol (id_fresh id.id_string) (unref_ty env ty)
| E.Rglobal { ls_value = None } ->
assert false
let havoc1 env r m =
let v = var_of_reference env r in
E.Mref.add r v m
let create env ef =
let s = E.Sref.union ef.E.reads ef.E.writes in
{ current = E.Sref.fold (havoc1 env) s E.Mref.empty; old = Mvs.empty; }
let havoc env ?pre ef s =
let l = match pre with
| None -> fresh_label env
| Some l -> l
in
{ current = E.Sref.fold (havoc1 env) ef.E.writes s.current;
old = Mvs.add l s.current s.old; }
let push_label env ?label s =
let l = match label with None -> fresh_label env | Some l -> l in
l, havoc env ~pre:l E.empty s
let ref_at cur s r =
let m = match cur with
| None -> s.current
| Some l -> assert (Mvs.mem l s.old); Mvs.find l s.old
in
assert (E.Mref.mem r m);
E.Mref.find r m
(* old = label for old state, if any
cur = label for current state, if any *)
let rec term_at env old cur s t = match t.t_node with
| Tapp (ls, [t]) when ls_equal ls (ls_bang env) ->
let r = reference_of_term t in
t_var (ref_at cur s r)
(* TODO: old, at *)
| _ ->
t_map (term_at env old cur s) (fmla_at env old cur s) t
and fmla_at env old cur s f =
f_map (term_at env old cur s) (fmla_at env old cur s) f
let term env s t = term_at env None None s t
let fmla env ?old s f = fmla_at env old None s f
let quantify _env s ef f =
let quant r f = wp_forall [ref_at None s r] [] f in
let s = E.Sref.union ef.E.reads ef.E.writes in
E.Sref.fold quant s f
let print _fmt _s = assert false (*TODO*)
end
......@@ -47,6 +47,7 @@ type label = Pgm_ttree.label
type expr = {
expr_desc : expr_desc;
expr_type : Ty.ty;
expr_type_v: type_v;
expr_effect: Pgm_effect.t;
expr_loc : loc;
......
......@@ -384,7 +384,7 @@ and dexpr_desc env loc = function
DEtry (e1, List.map handler hl), e1.dexpr_type
| Pgm_ptree.Eassert (k, le) ->
DEassert (k, lexpr le), (dty_unit env.uc)
DEassert (k, lexpr le), dty_unit env.uc
| Pgm_ptree.Elabel ({id=l}, e1) ->
let s = "label " ^ l in
if Typing.mem_var s env.denv then
......
......@@ -19,6 +19,7 @@
open Format
open Why
open Util
open Ident
open Ty
open Term
......@@ -43,6 +44,8 @@ let add_global x v env = { env with globals = Mls.add x v env.globals }
let ts_ref env = ns_find_ts (get_namespace env.uc) ["ref"]
let ts_label env = ns_find_ts (get_namespace env.uc) ["label"]
let ls_old env = ns_find_ls (get_namespace env.uc) ["old"]
let ls_at env = ns_find_ls (get_namespace env.uc) ["at"]
let ls_bang env = ns_find_ls (get_namespace env.uc) ["prefix !"]
(* phase 3: translation to intermediate trees and effect inference **********)
......@@ -59,8 +62,12 @@ let rec term_effect env ef t = match t.t_node with
| _ ->
t_fold (term_effect env) (fmla_effect env) ef t
and fmla_effect _env _ef _f =
assert false (*TODO*)
and fmla_effect env ef f =
f_fold (term_effect env) (fmla_effect env) ef f
let post_effect env ef ((_,q),ql) =
let exn_effect ef (_,(_,q)) = fmla_effect env ef q in
List.fold_left exn_effect (fmla_effect env ef q) ql
let add_binder env (x, v) = add_local x v env
let add_binders = List.fold_left add_binder
......@@ -69,7 +76,8 @@ let rec expr env e =
let ty = e.Pgm_ttree.expr_type in
let loc = e.Pgm_ttree.expr_loc in
let d, v, ef = expr_desc env loc ty e.Pgm_ttree.expr_desc in
{ expr_desc = d; expr_type_v = v; expr_effect = ef; expr_loc = loc }
{ expr_desc = d; expr_type = ty;
expr_type_v = v; expr_effect = ef; expr_loc = loc }
and expr_desc env _loc ty = function
| Pgm_ttree.Elogic t ->
......@@ -95,14 +103,27 @@ and expr_desc env _loc ty = function
let e2 = expr env e2 in
let ef = E.union e1.expr_effect e2.expr_effect in
Elet (v, e1, e2), e2.expr_type_v, ef
| Pgm_ttree.Esequence (e1, e2) ->
let e1 = expr env e1 in
let e2 = expr env e2 in
let ef = E.union e1.expr_effect e2.expr_effect in
Esequence (e1, e2), e2.expr_type_v, ef
| Pgm_ttree.Eassert (k, f) ->
let ef = fmla_effect env E.empty f in
Eassert (k, f), Tpure ty, ef
| _ ->
assert false (*TODO*)
and triple env (p, e, q) =
let e = expr env e in
let ef = post_effect env (fmla_effect env e.expr_effect p) q in
let e = { e with expr_effect = ef } in
let c =
{ c_result_type = e.expr_type_v;
c_effect = e.expr_effect;
c_effect = ef;
c_pre = p;
c_post = q }
in
......@@ -118,89 +139,9 @@ let wp_and = f_and
let wp_implies = f_implies
let wp_forall = f_forall
module State : sig
type t
val create : env -> E.t -> t
val push_label : env -> ?label:label -> t -> label * t
val havoc : env -> ?pre:label -> E.t -> t -> t
val term : env -> t -> term -> term
val fmla : env -> ?old:label -> t -> fmla -> fmla
val quantify : env -> t -> E.t -> fmla -> fmla
end = struct
type t = {
current : vsymbol E.Mref.t;
old : vsymbol E.Mref.t Mvs.t;
}
let unref_ty env ty = match ty.ty_node with
| Tyapp (ts, [ty]) when ts_equal ts (ts_ref env) -> ty
| _ -> assert false
let var_of_reference env = function
| E.Rlocal vs ->
create_vsymbol (id_fresh vs.vs_name.id_string) (unref_ty env vs.vs_ty)
| E.Rglobal { ls_name = id; ls_value = Some ty } ->
create_vsymbol (id_fresh id.id_string) (unref_ty env ty)
| E.Rglobal { ls_value = None } ->
assert false
let havoc1 env r m =
let v = var_of_reference env r in
E.Mref.add r v m
let create env ef =
let s = E.Sref.union ef.E.reads ef.E.writes in
{ current = E.Sref.fold (havoc1 env) s E.Mref.empty; old = Mvs.empty; }
let fresh_label env =
let ty = ty_app (ts_label env) [] in
create_vsymbol (id_fresh "label") ty
let havoc env ?pre ef s =
let l = match pre with
| None -> fresh_label env
| Some l -> l
in
{ current = E.Sref.fold (havoc1 env) ef.E.writes s.current;
old = Mvs.add l s.current s.old; }
let push_label env ?label s =
let l = match label with None -> fresh_label env | Some l -> l in
l, havoc env ~pre:l E.empty s
let ref_at cur s r =
let m = match cur with
| None -> s.current
| Some l -> assert (Mvs.mem l s.old); Mvs.find l s.old
in
assert (E.Mref.mem r m);
E.Mref.find r m
(* old = label for old state, if any
cur = label for current state, if any *)
let rec term_at env old cur s t = match t.t_node with
| Tapp (ls, [t]) when ls_equal ls (ls_bang env) ->
let r = reference_of_term t in
t_var (ref_at cur s r)
(* TODO: old, at *)
| _ ->
t_map (term_at env old cur s) (fmla_at env old cur s) t
and fmla_at env old cur s f =
f_map (term_at env old cur s) (fmla_at env old cur s) f
let term env s t = term_at env None None s t
let fmla env ?old s f = fmla_at env old None s f
let quantify _env s ef f =
let quant r f = wp_forall [ref_at None s r] [] f in
let s = E.Sref.union ef.E.reads ef.E.writes in
E.Sref.fold quant s f
let print _fmt _s = assert false (*TODO*)
end
let fresh_label env =
let ty = ty_app (ts_label env) [] in
create_vsymbol (id_fresh "label") ty
let wp_binder (x, tv) f = match tv with
| Tpure _ -> wp_forall [x] [] f
......@@ -208,38 +149,127 @@ let wp_binder (x, tv) f = match tv with
let wp_binders = List.fold_right wp_binder
let get_normal_post env s = function
| _, None -> f_true
| old, Some ((_,q),_) -> State.fmla env ~old s q
let post_map f ((v, q), ql) =
(v, f q), List.map (fun (e,(v,q)) -> e, (v, f q)) ql
(* replace old(t) with at(t,lab) everywhere in formula f *)
let rec old_label env lab f =
f_map (old_label_term env lab) (old_label env lab) f
let rec wp_expr env s e q = match e.expr_desc with
and old_label_term env lab t = match t.t_node with
| Tapp (ls, [t]) when ls_equal ls (ls_old env) ->
let t = old_label_term env lab t in (* NECESSARY? *)
t_app (ls_at env) [t; t_var lab] t.t_ty
| _ ->
t_map (old_label_term env lab) (old_label env lab) t
(* replace at(t,lab) with t everywhere in formula f *)
let rec erase_label env lab f =
f_map (old_label_term env lab) (old_label env lab) f
and erase_label_term env lab t = match t.t_node with
| Tapp (ls, [t; {t_node = Tvar l}])
when ls_equal ls (ls_at env) && vs_equal l lab ->
erase_label_term env lab t
| _ ->
t_map (erase_label_term env lab) (erase_label env lab) t
let unref_ty env ty = match ty.ty_node with
| Tyapp (ts, [ty]) when ts_equal ts (ts_ref env) -> ty
| _ -> assert false
(* replace !r by v everywhere in formula f *)
let rec unref env r v f =
f_map (unref_term env r v) (unref env r v) f
and unref_term env r v t = match t.t_node with
| Tapp (ls, [t]) when ls_equal ls (ls_bang env) ->
let rt = reference_of_term t in
if E.ref_equal rt r then t_var v else t
| Tapp (ls, _) when ls_equal ls (ls_old env) ->
assert false
| Tapp (ls, _) when ls_equal ls (ls_at env) -> (* do not recurse in at(...) *)
t
| _ ->
t_map (unref_term env r v) (unref env r v) t
(* quantify over all references in ef *)
let quantify env ef f =
let quantify1 r f =
let ty = unref_ty env (E.type_of_reference r) in
let v = create_vsymbol (id_clone (E.name_of_reference r)) ty in
wp_forall [v] [] (unref env r v f)
in
let s = E.Sref.union ef.E.reads ef.E.writes in
E.Sref.fold quantify1 s f
(*s [filter_post k q] removes exc. postconditions from [q] which do not
appear in effect [ef] *)
let filter_post ef (q, ql) =
let keep (ls, _) = Sls.mem ls ef.E.raises in
q, List.filter keep ql
let rec ls_assoc ls = function
| [] -> raise Not_found
| (ls', x) :: _ when ls_equal ls ls' -> x
| _ :: r -> ls_assoc ls r
let v_result ty = create_vsymbol (id_fresh "result") ty
let exn_v_result ls = match ls.ls_args with
| [] -> None
| [ty] -> Some (v_result ty)
| _ -> assert false
let default_exn_post ls = ls, (exn_v_result ls, f_true)
let default_post ty ef =
(v_result ty, f_true),
List.map default_exn_post (Sls.elements ef.E.raises)
(*s [saturate_post ef f q] makes a postcondition for a program of effect [ef]
out of a normal postcondition [f] and the exc. postconditions from [q] *)
let saturate_post ty ef f (_, ql) =
let set_post x = try x, ls_assoc x ql with Not_found -> default_exn_post x in
let xs = Sls.elements ef.E.raises in
((v_result ty, f), List.map set_post xs)
let rec wp_expr env e q =
let lab = fresh_label env in
let q = post_map (old_label env lab) q in
let f = wp_desc env e q in
erase_label env lab f
and wp_desc env e q = match e.expr_desc with
| Elogic t ->
let t = State.term env s t in
begin match q with
| old, Some ((v,q),_) ->
let q = State.fmla env ~old s q in
f_let v t q
| _, None ->
f_true
end
let (v, q), _ = q in
f_let v t q
| Efun (bl, t) ->
let q = get_normal_post env s q in
let (_, q), _ = q in
let f = wp_triple env t in
wp_and q (wp_binders bl f)
| Esequence (e1, e2) ->
let w2 = wp_expr env e2 (filter_post e2.expr_effect q) in
let q1 = saturate_post e1.expr_type e1.expr_effect w2 q in
wp_expr env e1 q1
| Eassert (Pgm_ptree.Aassert, f) ->
let (_, q), _ = q in
wp_and f q
| _ ->
f_true (* TODO *)
and wp_triple env (p,e,q) =
let s = State.create env e.expr_effect in
let old, s = State.push_label env s in
let f = wp_expr env s e (old, Some q) in
let f = wp_implies (State.fmla env s p) f in
State.quantify env s e.expr_effect f
and wp_triple env (p, e, q) =
let f = wp_expr env e q in
let f = wp_implies p f in
quantify env e.expr_effect f
let wp env e =
let s = State.create env e.expr_effect in
let old, s = State.push_label env s in
wp_expr env s e (old, None)
wp_expr env e (default_post e.expr_type e.expr_effect)
let wp_recfun _env _l _def = f_true (* TODO *)
......
......@@ -14,6 +14,7 @@ parameter r : int ref
let ff () =
{ !r = 1 }
assert { !r = 1 };
!r + 2
{ result = 3 }
......
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