Previous  Up  Next

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 -> 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 -> Ty.ty 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 : BigInt.t -> Value.value
val string_value : string -> Value.value
val num_value : Ity.ity -> BigInt.t -> Value.value
val float_value : Ity.ity -> Value.big_float -> Value.value
val real_value : Big_real.real -> Value.value
val constr_value : Ity.ity ->
       Expr.rsymbol option ->
       Expr.rsymbol list ->
       Value.value list -> Value.value
val purefun_value : result_ity:Ity.ity ->
       arg_ity:Ity.ity ->
       Value.value Mv.t ->
       Value.value -> Value.value
val unit_value : Value.value
val range_value : Ity.ity -> BigInt.t -> Value.value

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

val term_value : Ity.ity -> 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 Term.Mvs.t -> Value.value Term.Mvs.t
val snapshot_oldies : Ity.pvsymbol Ity.Mpv.t ->
       Value.value Term.Mvs.t -> Value.value 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 : Term.term list -> premises -> unit

add_premises ts p adds the terms ts to the premises.

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

Fold the terms in the premises.

The execution environment

type env = {
   why_env : Env.env;
   pmodule : Pmodule.pmodule;
   funenv : (Expr.cexp * Expr.rec_defn list option) Expr.Mrs.t; (*

local functions

*)
   tvenv : Ty.ty Ty.Mtv.t; (*

current instances of type variables

*)
   vsenv : Value.value Term.Mvs.t; (*

local variables

*)
   lsenv : Value.value Stdlib.Lazy.t Term.Mls.t; (*

global logical functions and constants

*)
   rsenv : Value.value Stdlib.Lazy.t 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 : Env.env -> Pmodule.pmodule -> env
val get_vs : env -> Term.Mvs.key -> Value.value
val get_pvs : env -> Ity.pvsymbol -> Value.value
val bind_vs : Term.Mvs.key ->
       Value.value -> env -> env
val bind_ls : Term.Mls.key ->
       Value.value Stdlib.Lazy.t ->
       env -> env
val bind_rs : Expr.Mrs.key ->
       Value.value Stdlib.Lazy.t ->
       env -> env
val bind_pvs : ?register:(Ident.ident -> Value.value -> unit) ->
       Ity.pvsymbol ->
       Value.value -> env -> env
val multibind_pvs : ?register:(Ident.ident -> Value.value -> unit) ->
       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

Term of value

val term_of_value : ?ty_mt:Ty.ty Ty.Mtv.t ->
       env ->
       (Term.vsymbol * Term.term) list ->
       Value.value -> (Term.vsymbol * Term.term) list * 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 -> Term.term -> 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 -> Ity.ity -> Value.value

Return the default value of the given type.

Oracles

type check_value = Ity.ity -> Value.value -> unit 
type oracle = {
   for_variable : env ->
?check:check_value ->
loc:Loc.position option ->
Ident.ident -> Ity.ity -> Value.value option;
   for_result : env ->
?check:check_value ->
loc:Loc.position ->
call_id:Expr.expr_id option -> 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.

val oracle_dummy : oracle

Always returns in None.

Log functions

val register_used_value : env ->
       Loc.position option -> Ident.ident -> Value.value -> unit
val register_res_value : env ->
       Loc.position -> Expr.rsymbol option -> Value.value -> unit
val register_const_init : env -> Loc.position option -> Ident.ident -> unit
val register_call : env ->
       Loc.position option ->
       Expr.rsymbol option ->
       Value.value Term.Mvs.t -> Log.exec_mode -> unit
val register_pure_call : env ->
       Loc.position option -> Term.lsymbol -> Log.exec_mode -> unit
val register_any_call : env ->
       Loc.position option ->
       Expr.rsymbol option -> Value.value Term.Mvs.t -> unit
val register_iter_loop : env -> Loc.position option -> Log.exec_mode -> unit
val register_exec_main : env -> Expr.rsymbol -> unit
val register_failure : env ->
       Loc.position option -> string -> Value.value Ident.Mid.t -> unit
val register_stucked : env ->
       Loc.position option -> string -> Value.value Ident.Mid.t -> unit
val register_ended : env -> 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 : Ident.attribute; (*

Some attribute Vc.expl_*

*)
   desc : string option;
   loc : Loc.position option;
   attrs : 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:Loc.position ->
       ?attrs:Ident.Sattr.t ->
       ?desc:string -> 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) Pp.pp
val report_cntr_head : (cntr_ctx * string * Term.term) Pp.pp
val report_cntr_body : (cntr_ctx * Term.term) Pp.pp
val report_cntr : (cntr_ctx * string * Term.term) Pp.pp

Exceptions for failures in RAC

exception Fail of cntr_ctx * Term.term

Caused by invalid assertions

exception Stuck of cntr_ctx * Loc.position option * string

Caused by invalid assumptions

exception Cannot_decide of cntr_ctx * 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: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:Loc.position -> cntr_ctx -> 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:(Term.vsymbol * Term.term) list ->
       cntr_ctx -> Term.term -> unit

A function of type check_term comprises a RAC engine.

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:(Term.vsymbol * Term.term) list ->
       cntr_ctx -> Term.term -> unit
val check_assume_term : rac -> cntr_ctx -> Term.term -> unit
val check_terms : rac -> cntr_ctx -> Term.term list -> unit
val check_assume_terms : rac -> cntr_ctx -> Term.term list -> unit
val check_post : rac ->
       cntr_ctx -> Value.value -> Ity.post -> unit

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

val check_posts : rac ->
       cntr_ctx -> Value.value -> Ity.post list -> unit
val check_assume_posts : rac ->
       cntr_ctx -> Value.value -> Ity.post list -> unit
val check_type_invs : rac ->
       ?loc:Loc.position ->
       giant_steps:bool ->
       env -> Ity.ity -> Value.value -> unit
val check_assume_type_invs : rac ->
       ?loc:Loc.position ->
       giant_steps:bool ->
       env -> Ity.ity -> Value.value -> unit
val oldify_varl : env ->
       (Term.term * Term.lsymbol option) list ->
       (Term.term * Term.lsymbol option) list * Value.value Term.Mvs.t

Prepare a variant for later call with Pinterp_core.check_variant.

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

Auxiliaries

val t_undefined : Ty.ty -> Term.term
val ty_app_arg : Ty.tysymbol -> int -> Ty.ty -> 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 : Ity.ity -> Ity.itysymbol * Ity.ity list * Ity.ity list

Gets the components of an ity

val is_range_ty : Ty.ty -> bool

Checks if the argument is a range type

val debug_array_as_update_chains_not_epsilon : 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 -> Ity.ity -> Value.value
val debug_trace_exec : Debug.flag

Print debug information during the interpretation of an expression.