Module Pinterp_core

module Pinterp_core: sig .. end

WhyML program interpreter: basic definitions

          Pinterp_core
             /    \
            /      \
       Pinterp     Rac
            \      /
             \    /
            Check_ce

Basic definitions for Pinterp

Values

module Value: sig .. end

(Mutable) values used in Pinterp

module Mv: Extmap.S  with type key = Value.value

A map with values as keys

val print_value : Stdlib.Format.formatter -> Value.value -> unit

val compare_values : Value.value -> Value.value -> int

Accessors

val v_ty : Value.value -> Why3.Ty.ty

val v_desc : Value.value -> Value.value_desc

val field : Value.value -> Value.field

val field_get : Value.field -> Value.value

val field_set : Value.field -> Value.value -> unit

val v_inst : Value.value ->
       Why3.Ty.ty Why3.Ty.Mtv.t -> Value.value

Constructors

Non defensive API for building values: there are no checks that ity is compatible with the value being built.

val bool_value : bool -> Value.value

val int_value : Why3.BigInt.t -> Value.value

val string_value : string -> Value.value

val num_value : Why3.Ity.ity -> Why3.BigInt.t -> Value.value

val float_value : Why3.Ity.ity -> Value.big_float -> Value.value

val real_value : Why3.Big_real.real -> Value.value

val constr_value : Why3.Ity.ity ->
       Why3.Expr.rsymbol option ->
       Why3.Expr.rsymbol list ->
       Value.value list -> Value.value

val purefun_value : result_ity:Why3.Ity.ity ->
       arg_ity:Why3.Ity.ity ->
       Value.value Mv.t ->
       Value.value -> Value.value

val unit_value : Value.value

val range_value : Why3.Ity.ity -> Why3.BigInt.t -> Value.value

Returns a range value, or raises Incomplete if the value is outside the range.

val term_value : Why3.Ity.ity -> Why3.Term.term -> Value.value

Snapshots

Values are mutable, the following functions make deep-copies.

val snapshot : Value.value -> Value.value

val snapshot_vsenv : Value.value Why3.Term.Mvs.t ->
       Value.value Why3.Term.Mvs.t

val snapshot_oldies : Why3.Ity.pvsymbol Why3.Ity.Mpv.t ->
       Value.value Why3.Term.Mvs.t ->
       Value.value Why3.Term.Mvs.t

Used for checking function variants

Interpreter log

module Log: sig .. end

Premises

type premises

The premises during RAC, i.e. the assertions in the execution context that have been checked. The premises are a stack of scopes, where a scope contains a set of checks.

val with_push_premises : premises -> (unit -> 'a) -> 'a

with_push_premises p f calls f in a new scope of premises in p. The scope is removed again after with_push_premises ends.

val add_premises : Why3.Term.term list -> premises -> unit

add_premises ts p adds the terms ts to the premises.

val fold_premises : ('a -> Why3.Term.term -> 'a) -> premises -> 'a -> 'a

Fold the terms in the premises.

The execution environment

type env = {

`why_env : Why3.Env.env;`
`pmodule : Why3.Pmodule.pmodule0;`
`funenv : (Why3.Expr.cexp * Why3.Expr.rec_defn list option) Why3.Expr.Mrs.t;`	`(*`	local functions	`*)`
`tvenv : Why3.Ty.ty Why3.Ty.Mtv.t;`	`(*`	current instances of type variables	`*)`
`vsenv : Value.value Why3.Term.Mvs.t;`	`(*`	local variables	`*)`
`lsenv : Value.value Stdlib.Lazy.t Why3.Term.Mls.t;`	`(*`	global logical functions and constants	`*)`
`rsenv : Value.value Stdlib.Lazy.t Why3.Expr.Mrs.t;`	`(*`	global variables	`*)`
`premises : premises;`
`log_uc : Log.log_uc;`

}

The parts of the execution environment in Pinterp which are relevant for Rac.

val mk_empty_env : Why3.Env.env -> Why3.Pmodule.pmodule0 -> env

val get_vs : env -> Why3.Term.Mvs.key -> Value.value

val get_pvs : env -> Why3.Ity.pvsymbol -> Value.value

val bind_vs : Why3.Term.Mvs.key ->
       Value.value -> env -> env

val bind_ls : Why3.Term.Mls.key ->
       Value.value Stdlib.Lazy.t ->
       env -> env

val bind_rs : Why3.Expr.Mrs.key ->
       Value.value Stdlib.Lazy.t ->
       env -> env

val bind_pvs : ?register:(Why3.Ident.ident -> Value.value -> unit) ->
       Why3.Ity.pvsymbol ->
       Value.value -> env -> env

val multibind_pvs : ?register:(Why3.Ident.ident -> Value.value -> unit) ->
       Why3.Ity.pvsymbol list ->
       Value.value list -> env -> env

Exception for incomplete execution (and RAC)

exception Cannot_evaluate of string

Raised when the execution in Pinterp is incomplete (not implemented or not possible)

val cannot_evaluate : ('a, Stdlib.Format.formatter, unit, 'b) Stdlib.format4 -> 'a

Raises Cannot_evaluate with the formatted string as reason

Term of value

val term_of_value : ?ty_mt:Why3.Ty.ty Why3.Ty.Mtv.t ->
       env ->
       (Why3.Term.vsymbol * Why3.Term.term) list ->
       Value.value ->
       (Why3.Term.vsymbol * Why3.Term.term) list * Why3.Term.term

Convert a value into a term. The first component of the result are additional bindings from closures.

Compute term

type compute_term = env -> Why3.Term.term -> Why3.Term.term

Reduce a term (for RAC or for computing ghost expressions). An implementation based on Why3 transformations is available at Rac.Why.mk_compute_term and Rac.Why.mk_compute_term_lit.

val compute_term_dummy : compute_term

An implementation that is just the identity, i.e. it does not reduce the term.

Default values

val default_value_of_type : env -> Why3.Ity.ity -> Value.value

Return the default value of the given type.

Oracles

type check_value = Why3.Ity.ity -> Value.value -> unit

type oracle = {

	`for_variable : env -> ?check:check_value -> loc:Why3.Loc.position option -> Why3.Ident.ident -> Why3.Ity.ity -> Value.value option;`
	`for_result : env -> ?check:check_value -> loc:Why3.Loc.position -> call_id:Why3.Expr.expr_id option -> Why3.Ity.ity -> Value.value option;`

}

An oracle provides values during execution in Pinterp for program parameters and during giant steps. The check is called on the value and every component.

Raises
- CannotCompute if the value or any component is invalid (e.g., a range value outside its bounds). See Check_ce.oracle_of_model for an implementation.
- Stuck if the value or any component is invalid (e.g., a range value outside its bounds).

val oracle_dummy : oracle

Always returns in None.

Log functions

val register_used_value : env ->
       Why3.Loc.position option ->
       Why3.Ident.ident -> Value.value -> unit

val register_res_value : env ->
       Why3.Loc.position ->
       Why3.Expr.rsymbol option -> Value.value -> unit

val register_const_init : env -> Why3.Loc.position option -> Why3.Ident.ident -> unit

val register_call : env ->
       Why3.Loc.position option ->
       Why3.Expr.rsymbol option ->
       Value.value Why3.Term.Mvs.t ->
       Log.exec_mode -> unit

val register_pure_call : env ->
       Why3.Loc.position option ->
       Why3.Term.lsymbol -> Log.exec_mode -> unit

val register_any_call : env ->
       Why3.Loc.position option ->
       Why3.Expr.rsymbol option -> Value.value Why3.Term.Mvs.t -> unit

val register_iter_loop : env ->
       Why3.Loc.position option -> Log.exec_mode -> unit

val register_exec_main : env -> Why3.Expr.rsymbol -> unit

val register_failure : env ->
       Why3.Loc.position option ->
       string -> Value.value Why3.Ident.Mid.t -> unit

val register_stucked : env ->
       Why3.Loc.position option ->
       string -> Value.value Why3.Ident.Mid.t -> unit

val register_ended : env -> Why3.Loc.position option -> unit

Basic definitions for RAC

Interfaces for runtime-assertion checking (RAC), implemented in module Rac.

The contradiction context

type cntr_ctx = {

`attr : Why3.Ident.attribute;`	`(*`	Some attribute `Vc.expl_*`	`*)`
`desc : string option;`
`loc : Why3.Loc.position option;`
`attrs : Why3.Ident.Sattr.t;`
`cntr_env : env;`
`giant_steps : bool option;`

}

A contradiction context carries all necessary information about a contradiction (with snapshot'ed values).

val mk_cntr_ctx : env ->
       giant_steps:bool option ->
       ?loc:Why3.Loc.position ->
       ?attrs:Why3.Ident.Sattr.t ->
       ?desc:string -> Why3.Ident.attribute -> cntr_ctx

Construct a new Pinterp_core.cntr_ctx with a snapshot of the environment env.

val describe_cntr_ctx : cntr_ctx -> string

val report_cntr_title : (cntr_ctx * string) Why3.Pp.pp

val report_cntr_head : (cntr_ctx * string * Why3.Term.term) Why3.Pp.pp

val report_cntr_body : (cntr_ctx * Why3.Term.term) Why3.Pp.pp

val report_cntr : (cntr_ctx * string * Why3.Term.term) Why3.Pp.pp

Exceptions for failures in RAC

exception Fail of cntr_ctx * Why3.Term.term

Caused by invalid assertions

exception Stuck of cntr_ctx * Why3.Loc.position option * string

Caused by invalid assumptions

exception Cannot_decide of cntr_ctx * Why3.Term.term list * string

The check cannot be decided (for example, because the execution is incomplete

exception FatalRACError of Log.log_uc * string

The RAC couldn't continue execution because of a fatal error

val fatal_rac_error : Log.log_uc ->
       ('a, Stdlib.Format.formatter, unit, 'b) Stdlib.format4 -> 'a

Raise a Pinterp_core.FatalRACError with a formatted string.

val stuck : ?loc:Why3.Loc.position ->
       cntr_ctx ->
       ('a, Stdlib.Format.formatter, unit, 'b) Stdlib.format4 -> 'a

Raise an exception Pinterp_core.Stuck with a formatted string.

val stuck_for_fail : ?loc:Why3.Loc.position -> cntr_ctx -> Why3.Term.term -> 'a

Raise an exception Pinterp_core.Stuck and register in the log for a Fail (cntr_ctx, t).

A RAC engine

type check_term = ?vsenv:(Why3.Term.vsymbol * Why3.Term.term) list ->
       cntr_ctx -> Why3.Term.term -> unit

A function of type check_term comprises a RAC engine.

Raises
- Fail when the term is invalid
- Incomplete when the validity of the term cannot be decided.

val check_term_dummy : check_term

Always raise Incomplete

type rac = {

	`check_term : check_term;`
	`ignore_incomplete : bool;`

}

RAC is defined by a single function Pinterp_core.check_term. When the flag ignore_incomplete is true, the functions under "RAC checks" ignore incomplete checks and output only a warning.

val mk_rac : ?ignore_incomplete:bool -> check_term -> rac

Plain constructor for Pinterp_core.rac, ignore_incomplete is false by default.

val rac_dummy : rac

Dummy RAC that always raises Failure.

RAC checks

The following functions use Pinterp_core.rac.check_term to check assertions and assumptions. If Pinterp_core.rac.ignore_incomplete is true, incomplete checks do not raise an exception Incomplete but trigger only a warning.

val check_term : rac ->
       ?vsenv:(Why3.Term.vsymbol * Why3.Term.term) list ->
       cntr_ctx -> Why3.Term.term -> unit

Raises Fail when the term is invalid

val check_assume_term : rac -> cntr_ctx -> Why3.Term.term -> unit

Raises Stuck when the term is invalid.

val check_terms : rac -> cntr_ctx -> Why3.Term.term list -> unit

Raises Fail when one of the terms is invalid

val check_assume_terms : rac -> cntr_ctx -> Why3.Term.term list -> unit

Raises Stuck when one of the terms is invalid.

val check_post : rac ->
       cntr_ctx -> Value.value -> Why3.Ity.post -> unit

Check a post-condition t by binding the result variable to the term vt representing the result value.

Raises Fail when the postcondition is invalid for the given value

val check_posts : rac ->
       cntr_ctx ->
       Value.value -> Why3.Ity.post list -> unit

Raises Fail when one of the postconditions is invalid for the given value

val check_assume_posts : rac ->
       cntr_ctx ->
       Value.value -> Why3.Ity.post list -> unit

Raises Stuck when one of the postconditions is invalid for the given return value.

val check_type_invs : rac ->
       ?loc:Why3.Loc.position ->
       giant_steps:bool ->
       env -> Why3.Ity.ity -> Value.value -> unit

Raises Fail when one of the type invariant of the type is invalid for the given value

val check_assume_type_invs : rac ->
       ?loc:Why3.Loc.position ->
       giant_steps:bool ->
       env -> Why3.Ity.ity -> Value.value -> unit

Raises Stuck when the type invariant for the given type is invalid for the given value.

val oldify_varl : env ->
       (Why3.Term.term * Why3.Term.lsymbol option) list ->
       (Why3.Term.term * Why3.Term.lsymbol option) list *
       Value.value Why3.Term.Mvs.t

Prepare a variant for later call with Pinterp_core.check_variant.

val check_variant : rac ->
       Why3.Ident.Sattr.elt ->
       Why3.Loc.position option ->
       giant_steps:bool ->
       env ->
       (Why3.Term.term * Why3.Term.lsymbol option) list *
       Value.value Why3.Term.Mvs.t ->
       (Why3.Term.term * Why3.Term.lsymbol option) list -> unit

Raises Fail when the variant is invalid.

Auxiliaries

val t_undefined : string -> Why3.Ty.ty -> Why3.Term.term

val ty_app_arg : Why3.Ty.tysymbol -> int -> Why3.Ty.ty -> Why3.Ty.ty

ty_app_arg ts n ty returns the n-th argument of the type application of ts in ty. Fails if ty is not an type application of ts

val ity_components : Why3.Ity.ity -> Why3.Ity.itysymbol * Why3.Ity.ity list * Why3.Ity.ity list

Gets the components of an ity

val is_range_ty : Why3.Ty.ty -> bool

Checks if the argument is a range type

val debug_array_as_update_chains_not_epsilon : Why3.Debug.flag

The debug parameter "rac-array-as-update-chains", a parameter for the conversion of arrays to terms in RAC. Normally, an array a of length n is converted to:

(epsilon v. v.length = n /\ v[0] = a[0] /\ ... /\ a[n-1] = a[n-1]).

As an update chain, it is instead converted into a formula:

(make n undefined)[0 <- a[0]]... [n-1 <- a[n-1]].

val undefined_value : env -> Why3.Ity.ity -> Value.value

val debug_trace_exec : Why3.Debug.flag

Print debug information during the interpretation of an expression.