Commit 94d62349 authored by Andrei Paskevich's avatar Andrei Paskevich
Browse files

Expr: add post-conditions to pure psymbols

parent 7ed67a1e
......@@ -65,28 +65,36 @@ type ps_kind =
| PKlemma (* top-level or local let-lemma *)
let create_psymbol id ?(ghost=false) ?(kind=PKnone) c =
let add_arg a t = ity_func (ity_purify a.pv_ity) t in
let mk_arg a = ty_of_ity a.pv_ity in
let check_effects { cty_effect = e } =
(* TODO/FIXME: prove that we can indeed ignore resets.
Normally, resets neither consult nor change the
external state, and do not affect the specification. *)
if not (Mreg.is_empty e.eff_writes &&
Sexn.is_empty e.eff_raises &&
not e.eff_diverg) then
if not (eff_is_pure e) then
Loc.errorm "this function has side effects, \
it cannot be declared as pure" in
let check_reads { cty_freeze = isb } =
if not (Mreg.is_empty isb.isb_reg) then
Loc.errorm "this function depends on the global state, \
it cannot be declared as pure" in
let res_type c = ty_of_ity c.cty_result in
let arg_type c = List.map (fun a -> a.pv_vs.vs_ty) c.cty_args in
let arg_list c = List.map (fun a -> t_var a.pv_vs) c.cty_args in
let add_post c t = match t.t_ty with
| Some ty ->
let res = create_vsymbol (id_fresh "result") ty in
cty_add_post c [create_post res (t_equ (t_var res) t)]
| None ->
let res = create_vsymbol (id_fresh "result") Ty.ty_bool in
let q = t_iff (t_equ (t_var res) t_bool_true) t in
cty_add_post c [create_post res q] in
match kind with
| PKnone ->
mk_ps (id_register id) c ghost PLnone
| PKlocal ->
check_effects c; check_reads c;
let ity = ity_purify c.cty_result in
let ity = List.fold_right add_arg c.cty_args ity in
let ity = List.fold_right (fun a ty ->
ity_func (ity_purify a.pv_ity) ty) c.cty_args ity in
(* When declaring local let-functions, we need to create a
mapping vsymbol to use in assertions. As vsymbols are not
generalisable, we have to freeze the type variables (but
......@@ -100,24 +108,25 @@ let create_psymbol id ?(ghost=false) ?(kind=PKnone) c =
be used in the program, as it has lost all preconditions,
which is why we declare it as ghost. In other words,
this pvsymbol behaves exactly as Epure of its pv_vs. *)
let pv = create_pvsymbol ~ghost:true id ity in
let c = cty_add_reads c (Spv.singleton pv) in
mk_ps pv.pv_vs.vs_name c ghost (PLvs pv.pv_vs)
let v = create_pvsymbol ~ghost:true id ity in
let t = t_func_app_l (t_var v.pv_vs) (arg_list c) in
mk_ps v.pv_vs.vs_name (add_post c t) ghost (PLvs v.pv_vs)
| PKfunc constr ->
check_effects c; check_reads c;
let ls = create_fsymbol id ~constr
(List.map mk_arg c.cty_args) (ty_of_ity c.cty_result) in
(* we don't really need to check the well-formedness of
constructor's signature here, the type declaration
will take care of it *)
mk_ps ls.ls_name c ghost (PLls ls)
let ls = create_fsymbol id ~constr (arg_type c) (res_type c) in
let t = t_app ls (arg_list c) ls.ls_value in
mk_ps ls.ls_name (add_post c t) ghost (PLls ls)
| PKpred ->
check_effects c; check_reads c;
if not (ity_equal c.cty_result ity_bool) then
Loc.errorm "this function does not return a boolean value, \
it cannot be declared as a pure predicate";
let ls = create_psymbol id (List.map mk_arg c.cty_args) in
mk_ps ls.ls_name c ghost (PLls ls)
let ls = create_psymbol id (arg_type c) in
let f = t_app ls (arg_list c) None in
mk_ps ls.ls_name (add_post c f) ghost (PLls ls)
| PKlemma ->
check_effects c;
mk_ps (id_register id) c ghost PLlemma
......@@ -178,6 +187,8 @@ let create_prog_pattern pp ?(ghost=false) ity =
(** {2 Program expressions} *)
type lazy_op = Eand | Eor
type assertion_kind = Assert | Assume | Check
type for_direction = To | DownTo
......@@ -208,10 +219,13 @@ type expr = {
and expr_node =
| Evar of pvsymbol
| Esym of psymbol
| Econst of Number.constant
| Eapp of expr * pvsymbol list * cty
| Efun of expr
| Elet of let_defn * expr
| Erec of rec_defn * expr
| Enot of expr
| Elazy of lazy_op * expr * expr
| Eif of expr * expr * expr
| Ecase of expr * (prog_pattern * expr) list
| Eassign of expr * pvsymbol (*field*) * pvsymbol
......@@ -238,3 +252,72 @@ and fun_defn = {
fun_expr : expr; (* Efun *)
fun_varl : variant list;
}
(* base tools *)
let e_label ?loc l e = { e with e_label = l; e_loc = loc }
let e_label_add l e = { e with e_label = Slab.add l e.e_label }
let e_label_copy { e_label = lab; e_loc = loc } e =
let lab = Slab.union lab e.e_label in
let loc = if e.e_loc = None then loc else e.e_loc in
{ e with e_label = lab; e_loc = loc }
exception ItyExpected of expr
exception CtyExpected of expr
let ity_of_expr e = match e.e_vty with
| VtyI ity -> ity
| VtyC _ -> Loc.error ?loc:e.e_loc (ItyExpected e)
let cty_of_expr e = match e.e_vty with
| VtyI _ -> Loc.error ?loc:e.e_loc (CtyExpected e)
| VtyC cty -> cty
(* smart constructors *)
let mk_expr node vty ghost eff = {
e_node = node;
e_vty = vty;
e_ghost = ghost;
e_effect = eff;
e_label = Slab.empty;
e_loc = None;
}
let e_var pv = mk_expr (Evar pv) (VtyI pv.pv_ity) pv.pv_ghost eff_empty
let e_sym ps = mk_expr (Esym ps) (VtyC ps.ps_cty) ps.ps_ghost eff_empty
let e_const c =
let ity = match c with
| Number.ConstInt _ -> ity_int
| Number.ConstReal _ -> ity_real in
mk_expr (Econst c) (VtyI ity) false eff_empty
let e_nat_const n =
e_const (Number.ConstInt (Number.int_const_dec (string_of_int n)))
let create_let_defn id e =
let ghost = e.e_ghost in
let lv = match e.e_vty with
| VtyI ity -> ValV (create_pvsymbol id ~ghost ity)
| VtyC cty -> ValS (create_psymbol id ~ghost ~kind:PKnone cty) in
{ let_sym = lv; let_expr = e }
let create_let_defn_pv id e =
(* let_defn * pvsymbol *)
assert false
let create_let_defn_ps id ?(kind=PKnone) e = assert false
(*
let create_let_defn_ps id ?(kind=PKnone) e = match e.e_vty, kind with
| VtyI
| _, PKfunc n when n > 0 -> invalid_arg "Expr.create_let_defn_ps"
|
| _ ->
let ps = create_psymbol id ~ghost:e.
(* let_defn * psymbol *)
assert false
*)
......@@ -78,6 +78,8 @@ val create_prog_pattern :
(** {2 Program expressions} *)
type lazy_op = Eand | Eor
type assertion_kind = Assert | Assume | Check
type for_direction = To | DownTo
......@@ -108,10 +110,13 @@ type expr = private {
and expr_node = private
| Evar of pvsymbol
| Esym of psymbol
| Econst of Number.constant
| Eapp of expr * pvsymbol list * cty
| Efun of expr
| Elet of let_defn * expr
| Erec of rec_defn * expr
| Enot of expr
| Elazy of lazy_op * expr * expr
| Eif of expr * expr * expr
| Ecase of expr * (prog_pattern * expr) list
| Eassign of expr * pvsymbol (*field*) * pvsymbol
......@@ -138,3 +143,25 @@ and fun_defn = {
fun_expr : expr; (* Efun *)
fun_varl : variant list;
}
val e_label : ?loc:Loc.position -> Slab.t -> expr -> expr
val e_label_add : label -> expr -> expr
val e_label_copy : expr -> expr -> expr
exception ItyExpected of expr
exception CtyExpected of expr
val ity_of_expr : expr -> ity
val cty_of_expr : expr -> cty
(** {2 Smart constructors} *)
val e_var : pvsymbol -> expr
val e_sym : psymbol -> expr
val e_const : Number.constant -> expr
val e_nat_const : int -> expr
val create_let_defn : preid -> expr -> let_defn
val create_let_defn_pv : preid -> expr -> let_defn * pvsymbol
val create_let_defn_ps : preid -> ?kind:ps_kind -> expr -> let_defn * psymbol
......@@ -635,6 +635,11 @@ let eff_is_empty e =
Sexn.is_empty e.eff_raises &&
not e.eff_diverg
let eff_is_pure e =
Mreg.is_empty e.eff_writes &&
Sexn.is_empty e.eff_raises &&
not e.eff_diverg
let eff_equal e1 e2 =
Mreg.equal Spv.equal e1.eff_writes e2.eff_writes &&
Mreg.equal Sreg.equal e1.eff_resets e2.eff_resets &&
......@@ -822,16 +827,20 @@ let check_tvs reads result pre post xpost =
(UnboundTypeVar (Stv.choose (Stv.diff ttv tvs))) in
spec_t_fold check_tvs () pre post xpost
let check_pre pre = List.iter (fun p -> if p.t_ty <> None
then Loc.error ?loc:p.t_loc (Term.FmlaExpected p)) pre
let check_post exn ity post =
let ty = ty_of_ity ity in
List.iter (fun q -> match q.t_node with
| Teps _ -> Ty.ty_equal_check ty (t_type q)
| _ -> raise exn) post
let create_cty args pre post xpost reads effect result =
let exn = Invalid_argument "Ity.create_cty" in
(* pre, post, and xpost are well-typed *)
let check_post ity f = match f.t_node with
| Teps _ -> Ty.ty_equal_check (ty_of_ity ity) (t_type f)
| _ -> raise exn in
List.iter (fun f -> if f.t_ty <> None then
Loc.error ?loc:f.t_loc (Term.FmlaExpected f)) pre;
List.iter (check_post result) post;
Mexn.iter (fun xs q -> List.iter (check_post xs.xs_ity) q) xpost;
check_pre pre; check_post exn result post;
Mexn.iter (fun xs xq -> check_post exn xs.xs_ity xq) xpost;
(* the arguments must be pairwise distinct *)
let sarg = List.fold_right (Spv.add_new exn) args Spv.empty in
(* complete reads and freeze the external context *)
......@@ -908,9 +917,19 @@ let cty_add_reads c pvs =
cty_freeze = Spv.fold freeze_pv pvs c.cty_freeze }
let cty_add_pre c pre =
List.iter (fun f -> if f.t_ty <> None then
Loc.error ?loc:f.t_loc (Term.FmlaExpected f)) pre;
check_pre pre;
let pvs = List.fold_left t_freepvs Spv.empty pre in
let c = cty_add_reads c pvs in
check_tvs c.cty_reads c.cty_result pre [] Mexn.empty;
{ c with cty_pre = pre @ c.cty_pre }
let cty_add_post c post =
check_post (Invalid_argument "Ity.cty_add_post") c.cty_result post;
let pvs = List.fold_left t_freepvs Spv.empty post in
let c = cty_add_reads c pvs in
check_tvs c.cty_reads c.cty_result [] post Mexn.empty;
{ c with cty_post = post @ c.cty_post }
let cty_pop_post c = match c.cty_post with
| [] -> invalid_arg "Ity.cty_pop_post"
| _::post -> { c with cty_post = post }
......@@ -266,6 +266,7 @@ val eff_equal : effect -> effect -> bool
val eff_union : effect -> effect -> effect
val eff_is_empty : effect -> bool
val eff_is_pure : effect -> bool
val eff_write : effect -> region -> pvsymbol option -> effect
val eff_raise : effect -> xsymbol -> effect
......@@ -333,3 +334,12 @@ val cty_add_pre : cty -> pre list -> cty
This function performs capture: the formulas in [fl] may refer to
the variables in [cty.cty_args]. Only the new external dependencies
in [fl] are added to [cty.cty_reads] and frozen. *)
val cty_add_post : cty -> post list -> cty
(** [cty_add_post cty fl] appends post-conditions in [fl] to [cty.cty_post].
This function performs capture: the formulas in [fl] may refer to the
variables in [cty.cty_args]. Only the new external dependencies in [fl]
are added to [cty.cty_reads] and frozen. *)
val cty_pop_post : cty -> cty
(** [cty_pop_post cty] removes the first post-condition from [cty.cty_post]. *)
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