programs: on the way to the first WP

parent a8c2baa7
......@@ -48,25 +48,26 @@ module Reference = struct
end
module R = Set.Make(Reference)
module Sref = Set.Make(Reference)
module Mref = Map.Make(Reference)
module E = Term.Sls
type t = {
reads : R.t;
writes : R.t;
reads : Sref.t;
writes : Sref.t;
raises : E.t;
}
let empty = { reads = R.empty; writes = R.empty; raises = E.empty }
let empty = { reads = Sref.empty; writes = Sref.empty; raises = E.empty }
let add_read r t = { t with reads = R.add r t.reads }
let add_write r t = { t with writes = R.add r t.writes }
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 union t1 t2 =
{ reads = R.union t1.reads t2.reads;
writes = R.union t1.writes t2.writes;
{ reads = Sref.union t1.reads t2.reads;
writes = Sref.union t1.writes t2.writes;
raises = E.union t1.raises t2.raises; }
open Format
......@@ -77,13 +78,13 @@ 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 (R.elements s)
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 (R.is_empty e.reads) then
if not (Sref.is_empty e.reads) then
fprintf fmt "@ reads %a" print_rset e.reads;
if not (R.is_empty e.writes) then
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
......
......@@ -24,11 +24,12 @@ type reference =
| Rlocal of Term.vsymbol
| Rglobal of Term.lsymbol
module R : Set.S with type elt = reference
module Sref : Set.S with type elt = reference
module Mref : Map.S with type key = reference
type t = private {
reads : R.t;
writes : R.t;
reads : Sref.t;
writes : Sref.t;
raises : Sls.t;
}
......
......@@ -43,6 +43,8 @@ type binder = Pgm_ttree.binder
type loop_annotation = Pgm_ttree.loop_annotation
type label = Pgm_ttree.label
type expr = {
expr_desc : expr_desc;
expr_type_v: type_v;
......@@ -70,7 +72,7 @@ and expr_desc =
| Eassert of assertion_kind * Term.fmla
| Eghost of expr
| Elabel of string * expr
| Elabel of label * expr
| Eany of type_c
and recfun = Term.vsymbol * binder list * variant option * triple
......
......@@ -131,6 +131,8 @@ type loop_annotation = {
loop_variant : variant option;
}
type label = Term.vsymbol
type expr = {
expr_desc : expr_desc;
expr_type : Ty.ty;
......@@ -158,7 +160,7 @@ and expr_desc =
| Etry of expr * (Term.lsymbol * Term.vsymbol option * expr) list
| Eassert of assertion_kind * Term.fmla
| Elabel of string * expr
| Elabel of label * expr
| Eany of type_c
and recfun = Term.vsymbol * binder list * variant option * triple
......
......@@ -96,6 +96,7 @@ let ts_unit uc = ns_find_ts (get_namespace uc) ["unit"]
let ts_ref uc = ns_find_ts (get_namespace uc) ["ref"]
let ts_arrow uc = ns_find_ts (get_namespace uc) ["arrow"]
let ts_exn uc = ns_find_ts (get_namespace uc) ["exn"]
let ts_label uc = ns_find_ts (get_namespace uc) ["label"]
let ls_Unit uc = ns_find_ls (get_namespace uc) ["Unit"]
......@@ -103,7 +104,7 @@ let ls_Unit uc = ns_find_ls (get_namespace uc) ["Unit"]
let dty_bool uc = Tyapp (ns_find_ts (get_namespace uc) ["bool"], [])
let dty_unit uc = Tyapp (ts_unit uc, [])
let dty_label uc = Tyapp (ns_find_ts (get_namespace uc) ["label"], [])
let dty_label uc = Tyapp (ts_label uc, [])
type denv = {
uc : theory_uc;
......@@ -385,10 +386,13 @@ and dexpr_desc env loc = function
| Pgm_ptree.Eassert (k, le) ->
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
errorm ~loc "clash with previous label %s" l;
let ty = dty_label env.uc in
let env = { env with denv = Typing.add_var l ty env.denv } in
let env = { env with denv = Typing.add_var s ty env.denv } in
let e1 = dexpr env e1 in
DElabel (l, e1), e1.dexpr_type
DElabel (s, e1), e1.dexpr_type
| Pgm_ptree.Ecast (e1, ty) ->
let e1 = dexpr env e1 in
let ty = pure_type env ty in
......@@ -524,9 +528,10 @@ let make_logic_app loc ty ls el =
Elogic (t_app ls (List.rev args) ty)
| ({ expr_desc = Elogic t }, _) :: r ->
make (t :: args) r
| ({ expr_desc = Elocal v }, _) :: r ->
(* TODO: assert v is not a reference *)
make (t_var v :: args) r
| ({ expr_desc = Elocal vs }, _) :: r ->
make (t_var vs :: args) r
| ({ expr_desc = Eglobal ls; expr_type = ty }, _) :: r ->
make (t_app ls [] ty :: args) r
| (e, _) :: r ->
let v = create_vsymbol (id_fresh "x") e.expr_type in
let d = mk_expr loc ty (make (t_var v :: args) r) in
......@@ -542,7 +547,6 @@ let is_reference_type uc ty = match ty.ty_node with
f [e1; e2; ...; en]
-> let x1 = e1 in ... let xn = en in (...((f x1) x2)... xn)
*)
(* TODO?: check for references -> Eapply_ref instead of Eapply *)
let make_app uc loc ty f el =
let rec make k = function
| [] ->
......@@ -661,10 +665,10 @@ and expr_desc uc env denv loc ty = function
let f = Typing.type_fmla denv env f in
Eassert (k, f)
| DElabel (s, e1) ->
let ty = Denv.ty_of_dty (Typing.find_var s e1.dexpr_denv) in
let ty = Ty.ty_app (ts_label uc) [] in
let v = create_vsymbol (id_fresh s) ty in
let env = Mstr.add s v env in
Elabel (s, expr uc env e1)
Elabel (v, expr uc env e1)
| DEany c ->
let c = type_c uc env c in
Eany c
......@@ -736,11 +740,11 @@ let rec print_type_v fmt = function
| Tpure ty ->
print_ty fmt ty
| Tarrow (bl, c) ->
fprintf fmt "@[%a ->@ %a@]"
fprintf fmt "@[<hov 2>%a ->@ %a@]"
(print_list arrow print_binder) bl print_type_c c
and print_type_c fmt c =
fprintf fmt "@[{%a} %a%a %a@]" print_fmla c.c_pre
fprintf fmt "@[{%a}@ %a%a@ %a@]" print_fmla c.c_pre
print_type_v c.c_result_type Pgm_effect.print c.c_effect
print_post c.c_post
......@@ -870,6 +874,8 @@ End:
(*
TODO:
- use a pure structure for globals
- mutually recursive functions: allow order relation to be specified only once
- exhaustivity of pattern-matching (in WP?)
......
......@@ -31,3 +31,4 @@ val report : Format.formatter -> error -> unit
val file : Env.env -> theory_uc -> Pgm_ptree.file -> theory_uc * Pgm_ttree.file
val print_type_v : Format.formatter -> Pgm_ttree.type_v -> unit
......@@ -29,41 +29,75 @@ open Pgm_typing
module E = Pgm_effect
(* translation to intermediate trees and effect inference *)
type env = {
uc : theory_uc;
globals : type_v Mls.t;
locals : type_v Mvs.t;
}
let logic_effect _t =
Pgm_effect.empty (* TODO *)
let empty_env uc = { uc = uc; globals = Mls.empty; locals = Mvs.empty }
let add_local x v env = { env with locals = Mvs.add x v env.locals }
let add_global x v env = { env with globals = Mls.add x v env.globals }
let rec expr e =
let ts_label env = ns_find_ts (get_namespace env.uc) ["label"]
let ls_bang env = ns_find_ls (get_namespace env.uc) ["prefix !"]
(* phase 3: translation to intermediate trees and effect inference **********)
let reference_of_term t = match t.t_node with
| Tvar vs -> E.Rlocal vs
| Tapp (ls, []) -> E.Rglobal ls
| _ -> assert false
let rec term_effect env ef t = match t.t_node with
| Tapp (ls, [t]) when ls_equal ls (ls_bang env) ->
let r = reference_of_term t in
E.add_read r ef
| _ ->
t_fold (term_effect env) (fmla_effect env) ef t
and fmla_effect _env _ef _f =
assert false (*TODO*)
let add_binder env (x, v) = add_local x v env
let add_binders = List.fold_left add_binder
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 loc ty e.Pgm_ttree.expr_desc 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 }
and expr_desc _loc ty = function
and expr_desc env _loc ty = function
| Pgm_ttree.Elogic t ->
Elogic t, Tpure ty, logic_effect t
| Pgm_ttree.Elocal _ ->
assert false (*TODO*)
| Pgm_ttree.Eglobal _ ->
assert false (*TODO*)
let ef = term_effect env E.empty t in
Elogic t, Tpure ty, ef
| Pgm_ttree.Elocal vs ->
assert (Mvs.mem vs env.locals);
Elocal vs, Mvs.find vs env.locals, E.empty
| Pgm_ttree.Eglobal ls ->
assert (Mls.mem ls env.globals);
Eglobal ls, Mls.find ls env.globals, E.empty
| Pgm_ttree.Eapply _ ->
assert false (*TODO*)
| Pgm_ttree.Eapply_ref _ ->
assert false (*TODO*)
| Pgm_ttree.Efun (bl, t) ->
let t, c = triple t in
Efun (bl, t), Tarrow (bl, c), Pgm_effect.empty
let env = add_binders env bl in
let t, c = triple env t in
Efun (bl, t), Tarrow (bl, c), E.empty
| Pgm_ttree.Elet (v, e1, e2) ->
let e1 = expr e1 in
let e2 = expr e2 in
let ef = Pgm_effect.union e1.expr_effect e2.expr_effect in
let e1 = expr env e1 in
let env = { env with locals = Mvs.add v e1.expr_type_v env.locals } in
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
| _ ->
assert false (*TODO*)
and triple (p, e, q) =
let e = expr e in
and triple env (p, e, q) =
let e = expr env e in
let c =
{ c_result_type = e.expr_type_v;
c_effect = e.expr_effect;
......@@ -72,38 +106,125 @@ and triple (p, e, q) =
in
(p, e, q), c
and recfun _ =
and recfun _env _def =
assert false (*TODO*)
(* weakest preconditions *)
(* phase 4: weakest preconditions *******************************************)
module State : sig
type t
val create : E.t -> t
val push_label : env -> label -> t -> 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 havoc1 r m =
let v = match r with
| E.Rlocal vs ->
create_vsymbol (id_fresh vs.vs_name.id_string) vs.vs_ty
| E.Rglobal { ls_name = id; ls_value = Some ty } ->
create_vsymbol (id_fresh id.id_string) ty
| E.Rglobal { ls_value = None } ->
assert false
in
E.Mref.add r v m
let create ef =
let s = E.Sref.union ef.E.reads ef.E.writes in
{ current = E.Sref.fold havoc1 s E.Mref.empty;
old = Mvs.empty; }
let fresh_label env =
let ty = 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 ef.E.writes s.current;
old = Mvs.add l s.current s.old; }
let push_label env l s = 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 = assert false (*TODO*)
let print _fmt _s = assert false (*TODO*)
end
let rec wprec env s e = match e.expr_desc with
| Elogic t ->
assert false (*TODO*)
| _ ->
f_true (* TODO *)
let wp _l _e = f_true (* TODO *)
let wp env _ls e = wprec env (State.create e.expr_effect) e
let wp_recfun _l _def = f_true (* TODO *)
let wp_recfun _env _l _def = f_true (* TODO *)
let add_wp_decl uc l f =
let add_wp_decl l f env =
let pr = create_prsymbol (id_fresh ("WP_" ^ l.ls_name.id_string)) in
let d = create_prop_decl Pgoal pr f in
add_decl uc d
{ env with uc = add_decl env.uc d }
let decl uc = function
| Pgm_ttree.Dlet (l, e) ->
let e = expr e in
let decl env = function
| Pgm_ttree.Dlet (ls, e) ->
let e = expr env e in
(* DEBUG *)
printf "@[--effect %a-----@\n %a@]@\n---------@."
Pretty.print_ls l print_type_v e.expr_type_v;
let f = wp l e in
add_wp_decl uc l f
Pretty.print_ls ls print_type_v e.expr_type_v;
let f = wp env ls e in
let env = add_wp_decl ls f env in
let env = add_global ls e.expr_type_v env in
env
| Pgm_ttree.Dletrec dl ->
let add_one uc (l, def) =
let def = recfun def in
let f = wp_recfun l def in
add_wp_decl uc l f
let add_one env (ls, def) =
let def = recfun env def in
let f = wp_recfun env ls def in
let env = add_wp_decl ls f env in
let v = assert false (*TODO*) in
let env = add_global ls v env in
env
in
List.fold_left add_one uc dl
| Pgm_ttree.Dparam _ ->
uc
List.fold_left add_one env dl
| Pgm_ttree.Dparam (ls, v) ->
let env = add_global ls v env in
env
let file uc dl =
let uc = List.fold_left decl uc dl in
Theory.close_theory uc
let env = List.fold_left decl (empty_env uc) dl in
Theory.close_theory env.uc
......@@ -10,11 +10,12 @@ parameter sub : x:int -> y:int -> {x>=y} int {result=x-y}
parameter imp_sub :
x:int ref -> y:int ref -> {!x >= !y} unit writes x {!x = old(!x) - !y}
parameter r : int ref
let ff () =
{ }
let x = 1 in
f x 2
{ true }
{ !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