Skip to content

GitLab

why3
why3
Commit 7f2d940d authored by Andrei Paskevich's avatar Andrei Paskevich
Browse files
Options

Ity: move reads and ghostness into effects 

Expr: separate first-order "expr" and higher-order "cexp"
Dexpr: add an "absurd" branch for non-exhaustive matches in programs
parent 2aa275ac
Expand all Hide whitespace changes
Inline Side-by-side
Showing with 1199 additions and 1171 deletions
src/mlw/dexpr.ml
View file @ 7f2d940d
This diff is collapsed.
src/mlw/dexpr.mli
View file @ 7f2d940d
......@@ -97,7 +97,8 @@ and dexpr_node =
| DElet of dlet_defn * dexpr
| DErec of drec_defn * dexpr
| DEnot of dexpr
| DElazy of lazy_op * dexpr * dexpr
| DEand of dexpr * dexpr
| DEor of dexpr * dexpr
| DEif of dexpr * dexpr * dexpr
| DEcase of dexpr * (dpattern * dexpr) list
| DEassign of (dexpr * rsymbol * dexpr) list
......@@ -157,4 +158,4 @@ val drec_defn : denv -> pre_fun_defn list -> denv * drec_defn
val expr : ?keep_loc:bool -> dexpr -> expr
val let_defn : ?keep_loc:bool -> dlet_defn -> let_defn
val rec_defn : ?keep_loc:bool -> drec_defn -> rec_defn
val rec_defn : ?keep_loc:bool -> drec_defn -> let_defn
src/mlw/expr.ml
View file @ 7f2d940d
This diff is collapsed.
src/mlw/expr.mli
View file @ 7f2d940d
......@@ -19,7 +19,6 @@ open Ity
type rsymbol = private {
rs_name : ident;
rs_cty : cty;
rs_ghost : bool;
rs_logic : rs_logic;
rs_field : pvsymbol option;
}
......@@ -64,6 +63,8 @@ val create_field : preid -> itysymbol -> pvsymbol -> rsymbol
val restore_rs : lsymbol -> rsymbol
(** raises [Not_found] if the argument is not a [rs_logic] *)
val rs_ghost : rsymbol -> bool
(** {2 Program patterns} *)
type prog_pattern = private {
......@@ -86,8 +87,6 @@ val create_prog_pattern :
(** {2 Program expressions} *)
type lazy_op = Eand | Eor
type assertion_kind = Assert | Assume | Check
type for_direction = To | DownTo
......@@ -100,130 +99,119 @@ type variant = term * lsymbol option (** tau * (tau -> tau -> prop) *)
type assign = pvsymbol * rsymbol * pvsymbol (* region * field * value *)
type vty =
| VtyI of ity
| VtyC of cty
type val_decl =
| ValV of pvsymbol
| ValS of rsymbol
type expr = private {
e_node : expr_node;
e_vty : vty;
e_ghost : bool;
e_ity : ity;
e_effect : effect;
e_vars : Spv.t;
e_syms : Srs.t;
e_label : Slab.t;
e_loc : Loc.position option;
}
and expr_node = private
| Evar of pvsymbol
| Esym of rsymbol
| Econst of Number.constant
| Eapp of expr * pvsymbol list * cty
| Efun of expr
| Eexec of cexp
| Eassign of assign list
| 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 assign list
| Ewhile of expr * invariant list * variant list * expr
| Efor of pvsymbol * for_bounds * invariant list * expr
| Etry of expr * (xsymbol * pvsymbol * expr) list
| Eraise of xsymbol * expr
| Eghost of expr
| Eassert of assertion_kind * term
| Epure of term
| Eabsurd
| Etrue
| Efalse
| Eany
and let_defn = private {
let_sym : val_decl;
let_expr : expr;
and cexp = private {
c_node : cexp_node;
c_cty : cty;
}
and cexp_node = private
| Capp of rsymbol * pvsymbol list
| Cfun of expr
| Cany
and let_defn = private
| LDvar of pvsymbol * expr
| LDsym of rsymbol * cexp
| LDrec of rec_defn list
and rec_defn = private {
rec_defn : fun_defn list;
rec_decr : lsymbol option;
rec_sym : rsymbol; (* exported symbol *)
rec_rsym : rsymbol; (* internal symbol *)
rec_fun : cexp; (* Cfun *)
rec_varl : variant list;
}
and fun_defn = {
fun_sym : rsymbol; (* exported symbol *)
fun_rsym : rsymbol; (* internal symbol *)
fun_expr : expr; (* Efun *)
fun_varl : variant list;
}
(** {2 Expressions} *)
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 e_ghost : expr -> bool
val c_ghost : cexp -> bool
val ity_of_expr : expr -> ity
val cty_of_expr : expr -> cty
val e_ghostify : bool -> expr -> expr
val c_ghostify : bool -> cexp -> cexp
val check_expr : expr -> unit
(** [check_expr e] verifies that [e] does not perform bad
ghost writes nor contains stale (i.e., reset) regions.
This function must be called for any expression which
is used outside of an [Efun]-closure. *)
(** {2 Definitions} *)
val e_fold : ('a -> expr -> 'a) -> 'a -> expr -> 'a
val let_var :
preid -> ?ghost:bool -> expr -> let_defn * pvsymbol
val e_find_minimal : (expr -> bool) -> expr -> expr
(** [e_find_minimal pr e] looks for a minimal sub-expression
of [e] satisfying [pr], raises [Not_found] if none found. *)
val let_sym :
preid -> ?ghost:bool -> ?kind:rs_kind -> cexp -> let_defn * rsymbol
val proxy_label : label
val let_rec :
(rsymbol * cexp * variant list * rs_kind) list -> let_defn * rec_defn list
(** {2 Smart constructors} *)
(** {2 Callable expressions} *)
val e_var : pvsymbol -> expr
val e_sym : rsymbol -> expr
val c_app : rsymbol -> pvsymbol list -> ity list -> ity -> cexp
val e_const : Number.constant -> expr
val e_nat_const : int -> expr
val c_fun :
pvsymbol list -> pre list -> post list -> post list Mexn.t -> expr -> cexp
val create_let_defn_pv :
preid -> ?ghost:bool -> expr -> let_defn * pvsymbol
val c_any : cty -> cexp
type ext_cexp = let_defn list * cexp
val create_let_defn_rs :
preid -> ?ghost:bool -> ?kind:rs_kind -> expr -> let_defn * rsymbol
val ext_c_sym : rsymbol -> ext_cexp
val create_let_defn :
preid -> ?ghost:bool -> ?kind:rs_kind -> expr -> let_defn
val ext_c_app : ext_cexp -> expr list -> ity list -> ity -> ext_cexp
val create_rec_defn :
(rsymbol * expr (* Efun *) * variant list * rs_kind) list -> rec_defn
(** {2 Expression constructors} *)
val e_fun :
pvsymbol list -> pre list -> post list -> post list Mexn.t -> expr -> expr
val e_var : pvsymbol -> expr
val e_const : Number.constant -> expr
val e_nat_const : int -> expr
val e_exec : cexp -> expr
val e_app : rsymbol -> expr list -> ity list -> ity -> expr
val e_let : let_defn -> expr -> expr
val e_rec : rec_defn -> expr -> expr
val e_app : expr -> expr list -> ity list -> ity -> expr
exception FieldExpected of rsymbol
val e_assign : (expr * rsymbol * expr) list -> expr
val e_ghost : expr -> expr
val e_ghostify : expr -> expr
val e_if : expr -> expr -> expr -> expr
val e_lazy : lazy_op -> expr -> expr -> expr
val e_and : expr -> expr -> expr
val e_or : expr -> expr -> expr
val e_not : expr -> expr
val e_true : expr
val e_true : expr
val e_false : expr
val is_e_true : expr -> bool
val is_e_false : expr -> bool
val e_raise : xsymbol -> expr -> ity -> expr
val e_try : expr -> (xsymbol * pvsymbol * expr) list -> expr
......@@ -232,8 +220,8 @@ val e_case : expr -> (prog_pattern * expr) list -> expr
val e_while : expr -> invariant list -> variant list -> expr -> expr
val e_for :
pvsymbol -> expr -> for_direction -> expr -> invariant list -> expr -> expr
val e_for : pvsymbol ->
expr -> for_direction -> expr -> invariant list -> expr -> expr
val e_pure : term -> expr
......@@ -241,15 +229,21 @@ val e_assert : assertion_kind -> term -> expr
val e_absurd : ity -> expr
val e_any : cty -> expr
(** {2 Expression manipulation tools} *)
(** {2 Built-in symbols} *)
val e_fold : ('a -> expr -> 'a) -> 'a -> expr -> 'a
(** [e_fold] does not descend into Cfun *)
val e_locate_effect : (effect -> bool) -> expr -> Loc.position option
(** [e_locate_effect pr e] looks for a minimal sub-expression of
[e] whose effect satisfies [pr] and returns its location *)
val rs_bool_true : rsymbol
val rs_bool_false : rsymbol
val proxy_label : label
(** {2 Built-in symbols} *)
val e_bool_true : expr
val e_bool_false : expr
val rs_true : rsymbol
val rs_false : rsymbol
val rs_tuple : int -> rsymbol
val e_tuple : expr list -> expr
......@@ -257,6 +251,7 @@ val e_tuple : expr list -> expr
val rs_void : rsymbol
val e_void : expr
val is_e_void : expr -> bool
val is_rs_tuple : rsymbol -> bool
val rs_func_app : rsymbol
......@@ -268,8 +263,7 @@ val e_func_app_l : expr -> expr list -> expr
val forget_rs : rsymbol -> unit (* flush id_unique for a program symbol *)
val print_rs : Format.formatter -> rsymbol -> unit (* program symbol *)
val print_expr : Format.formatter -> expr -> unit (* expression *)
val print_val_decl : Format.formatter -> val_decl -> unit
val print_let_defn : Format.formatter -> let_defn -> unit
val print_rec_defn : Format.formatter -> rec_defn -> unit
src/mlw/ity.ml
View file @ 7f2d940d
This diff is collapsed.
src/mlw/ity.mli
View file @ 7f2d940d
......@@ -13,7 +13,7 @@ open Ident
open Ty
open Term
(** {2 Individual types (first-order types w/o effects)} *)
(** {2 Individual types (first-order types without effects)} *)
type itysymbol = private {
its_ts : tysymbol; (** pure "snapshot" type symbol *)
......@@ -256,40 +256,55 @@ val create_xsymbol : preid -> ity -> xsymbol
(** {2 Effects} *)
exception IllegalAlias of region
exception AssignPrivate of region
exception StaleVariable of pvsymbol * region
exception BadGhostWrite of pvsymbol * region
exception DuplicateField of region * pvsymbol
exception WriteImmutable of region * pvsymbol
exception GhostDivergence
type effect = private {
eff_writes : Spv.t Mreg.t;
eff_resets : Sreg.t Mreg.t;
eff_raises : Sexn.t;
eff_diverg : bool;
eff_reads : Spv.t; (* known variables *)
eff_writes : Spv.t Mreg.t; (* modifications to specific fields *)
eff_covers : Sreg.t Mreg.t; (* confinement of regions to covers *)
eff_taints : Sreg.t; (* ghost modifications *)
eff_raises : Sexn.t; (* raised exceptions *)
eff_oneway : bool; (* non-termination *)
eff_ghost : bool; (* ghost status *)
}
val eff_empty : effect
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_equal : effect -> effect -> bool
val eff_pure : effect -> bool
exception AssignPrivate of region
exception DuplicateField of region * pvsymbol
exception WriteImmutable of region * pvsymbol
val eff_read : Spv.t -> effect
val eff_write : Spv.t -> Spv.t Mreg.t -> effect (* drops writes outside reads *)
val eff_assign : (pvsymbol * pvsymbol * pvsymbol) list -> effect (* r,field,v *)
val eff_write : effect -> region -> Spv.t -> effect
val eff_raise : effect -> xsymbol -> effect
val eff_catch : effect -> xsymbol -> effect
val eff_reset : effect -> region -> effect
val eff_read_pre : Spv.t -> effect -> effect (* no stale-variable check *)
val eff_read_post : effect -> Spv.t -> effect (* checks for stale variables *)
val eff_bind : Spv.t -> effect -> effect (* removes variables from reads *)
val eff_diverge : effect -> effect
val eff_read_single : pvsymbol -> effect
val eff_read_single_pre : pvsymbol -> effect -> effect
val eff_read_single_post : effect -> pvsymbol -> effect
val eff_bind_single : pvsymbol -> effect -> effect
val eff_assign : effect -> (region * pvsymbol * ity) list -> effect
val eff_reset : effect -> region -> effect (* confine to an empty cover *)
val eff_strong : effect -> effect (* confine all subregions under writes *)
val refresh_of_effect : effect -> effect
val eff_raise : effect -> xsymbol -> effect
val eff_catch : effect -> xsymbol -> effect
exception IllegalAlias of region
val eff_diverge : effect -> effect (* forbidden if ghost *)
val eff_ghostify : bool -> effect -> effect (* forbidden if diverges *)
val eff_full_inst : ity_subst -> effect -> effect
val eff_contagious : effect -> bool (* ghost and raising exceptions *)
val eff_stale_region : effect -> ity -> bool
val eff_union_seq : effect -> effect -> effect (* checks for stale variables *)
val eff_union_par : effect -> effect -> effect (* no stale-variable check *)
(** {2 Computation types (higher-order types with effects)} *)
......@@ -304,57 +319,52 @@ type cty = private {
cty_pre : pre list;
cty_post : post list;
cty_xpost : post list Mexn.t;
cty_reads : Spv.t;
cty_effect : effect;
cty_result : ity;
cty_freeze : ity_subst;
}
val create_cty : pvsymbol list ->
pre list -> post list -> post list Mexn.t -> Spv.t -> effect -> ity -> cty
(** [create_cty args pre post xpost reads effect result] creates a cty.
pre list -> post list -> post list Mexn.t -> effect -> ity -> cty
(** [create_cty args pre post xpost effect result] creates a cty.
The [cty_xpost] field does not have to cover all raised exceptions.
The [cty_reads] field contains all unbound variables from the spec.
The [cty_freeze] field freezes every pvsymbol in [cty_reads].
The [cty_effect] field is filtered wrt [cty_reads] and [args].
[cty_effect.eff_reads] is completed wrt the specification and [args].
[cty_freeze] freezes every unbound pvsymbol in [cty_effect.eff_reads].
All effects on regions outside [cty_effect.eff_reads] are removed.
Fresh regions in [result] are reset. Every type variable in [pre],
[post], and [xpost] must come from [cty_reads], [args] or [result]. *)
val cty_apply :
?ghost:bool -> cty -> pvsymbol list -> ity list -> ity -> bool * cty
(** [cty_apply ?(ghost=false) cty pvl rest res] instantiates [cty]
up to the types in [pvl], [rest] and [res], then applies it to
the arguments in [pvl], and returns the ghost status and the
computation type of the result, [rest -> res], with every type
variable and region in [pvl] freezed. Typecasts into a mapping
type are allowed for total effectless computations. *)
val cty_apply : cty -> pvsymbol list -> ity list -> ity -> cty
(** [cty_apply cty pvl rest res] instantiates [cty] up to the types in
[pvl], [rest] and [res], then applies it to the arguments in [pvl],
and returns the computation type of the result, [rest -> res],
with every type variable and region in [pvl] being frozen. *)
val cty_ghost : cty -> bool
(** [cty_ghost cty] returns [cty.cty_effect.eff_ghost] *)
val cty_r_visible : cty -> Sreg.t
(** [cty_r_visible cty] returns the set of regions which are visible
from the non-ghost read dependencies and arguments of [cty]. *)
val cty_ghostify : bool -> cty -> cty
(** [cty_ghostify ghost cty] ghostifies the effect of [cty]. *)
val cty_ghost_writes : bool -> cty -> Spv.t Mreg.t
(** [cty_ghost_writes ghost cty] returns the subset of the write effect
of [cty] which corresponds to ghost writes into visible fields of
the ghost read dependencies and arguments of [cty]. *)
val cty_reads : cty -> Spv.t
(** [cty_reads cty] returns the set of external dependencies of [cty]. *)
val cty_add_reads : cty -> Spv.t -> cty
(** [cty_add_reads cty pvs] adds variables in [pvs] to [cty.cty_reads].
This function performs capture: if some variables in [pvs] occur in
[cty.cty_args], they are removed from [pvs], and the corresponding
type variables and regions are not frozen. *)
(** [cty_add_reads cty pvs] adds [pvs] to [cty.cty_effect.eff_reads].
This function performs capture: if some variables in [pvs] occur
in [cty.cty_args], they are not frozen. *)
val cty_add_pre : cty -> pre list -> cty
(** [cty_add_pre cty fl] appends pre-conditions in [fl] to [cty.cty_pre].
val cty_add_pre : pre list -> cty -> cty
(** [cty_add_pre fl cty] appends pre-conditions in [fl] to [cty.cty_pre].
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. *)
in [fl] are added to [cty.cty_effect.eff_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. *)
are added to [cty.cty_effect.eff_reads] and frozen. *)
(** {2 Pretty-printing} *)
......@@ -371,5 +381,6 @@ val print_pv : Format.formatter -> pvsymbol -> unit (* program variable *)
val print_pvty : Format.formatter -> pvsymbol -> unit (* pvsymbol : type *)
val print_cty : Format.formatter -> cty -> unit (* computation type *)
val print_spec : pvsymbol list -> pre list -> post list -> post list Mexn.t ->
Spv.t -> effect -> Format.formatter -> ity option -> unit (* piecemeal cty *)
val print_spec :
pvsymbol list -> pre list -> post list -> post list Mexn.t ->
effect -> Format.formatter -> ity option -> unit (* piecemeal cty *)
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