(*========================================================================*) (* Sail *) (* *) (* Copyright (c) 2013-2017 *) (* Kathyrn Gray *) (* Shaked Flur *) (* Stephen Kell *) (* Gabriel Kerneis *) (* Robert Norton-Wright *) (* Christopher Pulte *) (* Peter Sewell *) (* *) (* All rights reserved. *) (* *) (* This software was developed by the University of Cambridge Computer *) (* Laboratory as part of the Rigorous Engineering of Mainstream Systems *) (* (REMS) project, funded by EPSRC grant EP/K008528/1. *) (* *) (* Redistribution and use in source and binary forms, with or without *) (* modification, are permitted provided that the following conditions *) (* are met: *) (* 1. Redistributions of source code must retain the above copyright *) (* notice, this list of conditions and the following disclaimer. *) (* 2. Redistributions in binary form must reproduce the above copyright *) (* notice, this list of conditions and the following disclaimer in *) (* the documentation and/or other materials provided with the *) (* distribution. *) (* *) (* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' *) (* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED *) (* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A *) (* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR *) (* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, *) (* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT *) (* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF *) (* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND *) (* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, *) (* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT *) (* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF *) (* SUCH DAMAGE. *) (*========================================================================*) (* generated by Ott 0.25 from: l2_typ.ott l2.ott *) open import Pervasives open import Map open import Maybe open import Set_extra type l = | Unknown | Int of string * maybe l (*internal types, functions*) | Range of string * nat * nat * nat * nat | Generated of l (*location for a generated node, where l is the location of the closest original source*) type annot 'a = l * 'a val duplicates : forall 'a. list 'a -> list 'a val set_from_list : forall 'a. list 'a -> set 'a val subst : forall 'a. list 'a -> list 'a -> bool type x = string (* identifier *) type ix = string (* infix identifier *) type base_kind_aux = (* base kind *) | BK_type (* kind of types *) | BK_nat (* kind of natural number size expressions *) | BK_order (* kind of vector order specifications *) | BK_effect (* kind of effect sets *) type base_kind = | BK_aux of base_kind_aux * l type kid_aux = (* variables with kind, ticked to differntiate from program variables *) | Var of x type id_aux = (* Identifier *) | Id of x | DeIid of x (* remove infix status *) type kind_aux = (* kinds *) | K_kind of list base_kind type kid = | Kid_aux of kid_aux * l type id = | Id_aux of id_aux * l type kind = | K_aux of kind_aux * l type nexp_aux = (* expression of kind Nat, for vector sizes and origins *) | Nexp_id of id (* identifier, bound by def Nat x = nexp *) | Nexp_var of kid (* variable *) | Nexp_constant of integer (* constant *) | Nexp_times of nexp * nexp (* product *) | Nexp_sum of nexp * nexp (* sum *) | Nexp_minus of nexp * nexp (* subtraction *) | Nexp_exp of nexp (* exponential *) | Nexp_neg of nexp (* For internal use *) and nexp = | Nexp_aux of nexp_aux * l type base_effect_aux = (* effect *) | BE_rreg (* read register *) | BE_wreg (* write register *) | BE_rmem (* read memory *) | BE_wmem (* write memory *) | BE_eamem (* signal effective address for writing memory *) | BE_wmv (* write memory, sending only value *) | BE_barr (* memory barrier *) | BE_depend (* dynamic footprint *) | BE_undef (* undefined-instruction exception *) | BE_unspec (* unspecified values *) | BE_nondet (* nondeterminism from intra-instruction parallelism *) | BE_escape (* Tracking of expressions and functions that might call exit *) | BE_lset (* Local mutation happend; not user-writable *) | BE_lret (* Local return happened; not user-writable *) type base_effect = | BE_aux of base_effect_aux * l type order_aux = (* vector order specifications, of kind Order *) | Ord_var of kid (* variable *) | Ord_inc (* increasing (little-endian) *) | Ord_dec (* decreasing (big-endian) *) type effect_aux = (* effect set, of kind Effects *) | Effect_var of kid | Effect_set of list base_effect (* effect set *) type order = | Ord_aux of order_aux * l type effect = | Effect_aux of effect_aux * l let effect_union e1 e2 = match (e1,e2) with | ((Effect_aux (Effect_set els) _),(Effect_aux (Effect_set els2) l)) -> Effect_aux (Effect_set (els++els2)) l end type kinded_id_aux = (* optionally kind-annotated identifier *) | KOpt_none of kid (* identifier *) | KOpt_kind of kind * kid (* kind-annotated variable *) type n_constraint_aux = (* constraint over kind $Nat$ *) | NC_fixed of nexp * nexp | NC_bounded_ge of nexp * nexp | NC_bounded_le of nexp * nexp | NC_nat_set_bounded of kid * list integer type kinded_id = | KOpt_aux of kinded_id_aux * l type n_constraint = | NC_aux of n_constraint_aux * l type quant_item_aux = (* Either a kinded identifier or a nexp constraint for a typquant *) | QI_id of kinded_id (* An optionally kinded identifier *) | QI_const of n_constraint (* A constraint for this type *) type quant_item = | QI_aux of quant_item_aux * l type typquant_aux = (* type quantifiers and constraints *) | TypQ_tq of list quant_item | TypQ_no_forall (* sugar, omitting quantifier and constraints *) type lit_aux = (* Literal constant *) | L_unit (* $() : unit$ *) | L_zero (* $bitzero : bit$ *) | L_one (* $bitone : bit$ *) | L_true (* $true : bool$ *) | L_false (* $false : bool$ *) | L_num of integer (* natural number constant *) | L_hex of string (* bit vector constant, C-style *) | L_bin of string (* bit vector constant, C-style *) | L_undef (* constant representing undefined values *) | L_string of string (* string constant *) type typquant = | TypQ_aux of typquant_aux * l type typ_aux = (* Type expressions, of kind $Type$ *) | Typ_wild (* Unspecified type *) | Typ_id of id (* Defined type *) | Typ_var of kid (* Type variable *) | Typ_fn of typ * typ * effect (* Function type (first-order only in user code) *) | Typ_tup of list typ (* Tuple type *) | Typ_app of id * list typ_arg (* type constructor application *) and typ = | Typ_aux of typ_aux * l and typ_arg_aux = (* Type constructor arguments of all kinds *) | Typ_arg_nexp of nexp | Typ_arg_typ of typ | Typ_arg_order of order | Typ_arg_effect of effect and typ_arg = | Typ_arg_aux of typ_arg_aux * l type lit = | L_aux of lit_aux * l type typschm_aux = (* type scheme *) | TypSchm_ts of typquant * typ type pat_aux 'a = (* Pattern *) | P_lit of lit (* literal constant pattern *) | P_wild (* wildcard *) | P_as of (pat 'a) * id (* named pattern *) | P_typ of typ * (pat 'a) (* typed pattern *) | P_id of id (* identifier *) | P_app of id * list (pat 'a) (* union constructor pattern *) | P_record of list (fpat 'a) * bool (* struct pattern *) | P_vector of list (pat 'a) (* vector pattern *) | P_vector_indexed of list (integer * (pat 'a)) (* vector pattern (with explicit indices) *) | P_vector_concat of list (pat 'a) (* concatenated vector pattern *) | P_tup of list (pat 'a) (* tuple pattern *) | P_list of list (pat 'a) (* list pattern *) and pat 'a = | P_aux of (pat_aux 'a) * annot 'a and fpat_aux 'a = (* Field pattern *) | FP_Fpat of id * (pat 'a) and fpat 'a = | FP_aux of (fpat_aux 'a) * annot 'a type typschm = | TypSchm_aux of typschm_aux * l type reg_id_aux 'a = | RI_id of id type exp_aux 'a = (* Expression *) | E_block of list (exp 'a) (* block *) | E_nondet of list (exp 'a) (* nondeterminisitic block, expressions evaluate in an unspecified order, or concurrently *) | E_id of id (* identifier *) | E_lit of lit (* literal constant *) | E_cast of typ * (exp 'a) (* cast *) | E_app of id * list (exp 'a) (* function application *) | E_app_infix of (exp 'a) * id * (exp 'a) (* infix function application *) | E_tuple of list (exp 'a) (* tuple *) | E_if of (exp 'a) * (exp 'a) * (exp 'a) (* conditional *) | E_for of id * (exp 'a) * (exp 'a) * (exp 'a) * order * (exp 'a) (* loop *) | E_vector of list (exp 'a) (* vector (indexed from 0) *) | E_vector_indexed of list (integer * (exp 'a)) * (opt_default 'a) (* vector (indexed consecutively) *) | E_vector_access of (exp 'a) * (exp 'a) (* vector access *) | E_vector_subrange of (exp 'a) * (exp 'a) * (exp 'a) (* subvector extraction *) | E_vector_update of (exp 'a) * (exp 'a) * (exp 'a) (* vector functional update *) | E_vector_update_subrange of (exp 'a) * (exp 'a) * (exp 'a) * (exp 'a) (* vector subrange update (with vector) *) | E_vector_append of (exp 'a) * (exp 'a) (* vector concatenation *) | E_list of list (exp 'a) (* list *) | E_cons of (exp 'a) * (exp 'a) (* cons *) | E_record of (fexps 'a) (* struct *) | E_record_update of (exp 'a) * (fexps 'a) (* functional update of struct *) | E_field of (exp 'a) * id (* field projection from struct *) | E_case of (exp 'a) * list (pexp 'a) (* pattern matching *) | E_let of (letbind 'a) * (exp 'a) (* let expression *) | E_assign of (lexp 'a) * (exp 'a) (* imperative assignment *) | E_sizeof of nexp (* Expression to return the value of the nexp variable or expression at run time *) | E_exit of (exp 'a) (* expression to halt all current execution, potentially calling a system, trap, or interrupt handler with exp *) | E_return of (exp 'a) (* expression to end current function execution and return the value of exp from the function; this can be used to break out of for loops *) | E_assert of (exp 'a) * (exp 'a) (* expression to halt with error, when the first expression is false, reporting the optional string as an error *) | E_internal_cast of annot 'a * (exp 'a) (* This is an internal cast, generated during type checking that will resolve into a syntactic cast after *) | E_internal_exp of annot 'a (* This is an internal use for passing nexp information to library functions, postponed for constraint solving *) | E_sizeof_internal of annot 'a (* For sizeof during type checking, to replace nexp with internal n *) | E_internal_exp_user of annot 'a * annot 'a (* This is like the above but the user has specified an implicit parameter for the current function *) | E_comment of string (* For generated unstructured comments *) | E_comment_struc of (exp 'a) (* For generated structured comments *) | E_internal_let of (lexp 'a) * (exp 'a) * (exp 'a) (* This is an internal node for compilation that demonstrates the scope of a local mutable variable *) | E_internal_plet of (pat 'a) * (exp 'a) * (exp 'a) (* This is an internal node, used to distinguised some introduced lets during processing from original ones *) | E_internal_return of (exp 'a) (* For internal use to embed into monad definition *) and exp 'a = | E_aux of (exp_aux 'a) * annot 'a and lexp_aux 'a = (* lvalue expression *) | LEXP_id of id (* identifier *) | LEXP_memory of id * list (exp 'a) (* memory write via function call *) | LEXP_cast of typ * id | LEXP_tup of list (lexp 'a) (* set multiple at a time, a check will ensure it's not memory *) | LEXP_vector of (lexp 'a) * (exp 'a) (* vector element *) | LEXP_vector_range of (lexp 'a) * (exp 'a) * (exp 'a) (* subvector *) | LEXP_field of (lexp 'a) * id (* struct field *) and lexp 'a = | LEXP_aux of (lexp_aux 'a) * annot 'a and fexp_aux 'a = (* Field-expression *) | FE_Fexp of id * (exp 'a) and fexp 'a = | FE_aux of (fexp_aux 'a) * annot 'a and fexps_aux 'a = (* Field-expression list *) | FES_Fexps of list (fexp 'a) * bool and fexps 'a = | FES_aux of (fexps_aux 'a) * annot 'a and opt_default_aux 'a = (* Optional default value for indexed vectors, to define a defualt value for any unspecified positions in a sparse map *) | Def_val_empty | Def_val_dec of (exp 'a) and opt_default 'a = | Def_val_aux of (opt_default_aux 'a) * annot 'a and pexp_aux 'a = (* Pattern match *) | Pat_exp of (pat 'a) * (exp 'a) and pexp 'a = | Pat_aux of (pexp_aux 'a) * annot 'a and letbind_aux 'a = (* Let binding *) | LB_val_explicit of typschm * (pat 'a) * (exp 'a) (* value binding, explicit type ((pat 'a) must be total) *) | LB_val_implicit of (pat 'a) * (exp 'a) (* value binding, implicit type ((pat 'a) must be total) *) and letbind 'a = | LB_aux of (letbind_aux 'a) * annot 'a type reg_id 'a = | RI_aux of (reg_id_aux 'a) * annot 'a type type_union_aux = (* Type union constructors *) | Tu_id of id | Tu_ty_id of typ * id type name_scm_opt_aux = (* Optional variable-naming-scheme specification for variables of defined type *) | Name_sect_none | Name_sect_some of string type effect_opt_aux = (* Optional effect annotation for functions *) | Effect_opt_pure (* sugar for empty effect set *) | Effect_opt_effect of effect type funcl_aux 'a = (* Function clause *) | FCL_Funcl of id * (pat 'a) * (exp 'a) type rec_opt_aux = (* Optional recursive annotation for functions *) | Rec_nonrec (* non-recursive *) | Rec_rec (* recursive *) type tannot_opt_aux = (* Optional type annotation for functions *) | Typ_annot_opt_some of typquant * typ type alias_spec_aux 'a = (* Register alias expression forms. Other than where noted, each id must refer to an unaliased register of type vector *) | AL_subreg of (reg_id 'a) * id | AL_bit of (reg_id 'a) * (exp 'a) | AL_slice of (reg_id 'a) * (exp 'a) * (exp 'a) | AL_concat of (reg_id 'a) * (reg_id 'a) type type_union = | Tu_aux of type_union_aux * l type index_range_aux = (* index specification, for bitfields in register types *) | BF_single of integer (* single index *) | BF_range of integer * integer (* index range *) | BF_concat of index_range * index_range (* concatenation of index ranges *) and index_range = | BF_aux of index_range_aux * l type name_scm_opt = | Name_sect_aux of name_scm_opt_aux * l type effect_opt = | Effect_opt_aux of effect_opt_aux * l type funcl 'a = | FCL_aux of (funcl_aux 'a) * annot 'a type rec_opt = | Rec_aux of rec_opt_aux * l type tannot_opt = | Typ_annot_opt_aux of tannot_opt_aux * l type alias_spec 'a = | AL_aux of (alias_spec_aux 'a) * annot 'a type default_spec_aux 'a = (* Default kinding or typing assumption *) | DT_kind of base_kind * kid | DT_order of order | DT_typ of typschm * id type type_def_aux 'a = (* Type definition body *) | TD_abbrev of id * name_scm_opt * typschm (* type abbreviation *) | TD_record of id * name_scm_opt * typquant * list (typ * id) * bool (* struct type definition *) | TD_variant of id * name_scm_opt * typquant * list type_union * bool (* union type definition *) | TD_enum of id * name_scm_opt * list id * bool (* enumeration type definition *) | TD_register of id * nexp * nexp * list (index_range * id) (* register mutable bitfield type definition *) type val_spec_aux 'a = (* Value type specification *) | VS_val_spec of typschm * id | VS_extern_no_rename of typschm * id | VS_extern_spec of typschm * id * string (* Specify the type and id of a function from Lem, where the string must provide an explicit path to the required function but will not be checked *) type kind_def_aux 'a = (* Definition body for elements of kind; many are shorthands for type\_defs *) | KD_nabbrev of kind * id * name_scm_opt * nexp (* nexp abbreviation *) | KD_abbrev of kind * id * name_scm_opt * typschm (* type abbreviation *) | KD_record of kind * id * name_scm_opt * typquant * list (typ * id) * bool (* struct type definition *) | KD_variant of kind * id * name_scm_opt * typquant * list type_union * bool (* union type definition *) | KD_enum of kind * id * name_scm_opt * list id * bool (* enumeration type definition *) | KD_register of kind * id * nexp * nexp * list (index_range * id) (* register mutable bitfield type definition *) type scattered_def_aux 'a = (* Function and type union definitions that can be spread across a file. Each one must end in $id$ *) | SD_scattered_function of rec_opt * tannot_opt * effect_opt * id (* scattered function definition header *) | SD_scattered_funcl of (funcl 'a) (* scattered function definition clause *) | SD_scattered_variant of id * name_scm_opt * typquant (* scattered union definition header *) | SD_scattered_unioncl of id * type_union (* scattered union definition member *) | SD_scattered_end of id (* scattered definition end *) type fundef_aux 'a = (* Function definition *) | FD_function of rec_opt * tannot_opt * effect_opt * list (funcl 'a) type dec_spec_aux 'a = (* Register declarations *) | DEC_reg of typ * id | DEC_alias of id * (alias_spec 'a) | DEC_typ_alias of typ * id * (alias_spec 'a) type default_spec 'a = | DT_aux of (default_spec_aux 'a) * l type type_def 'a = | TD_aux of (type_def_aux 'a) * annot 'a type val_spec 'a = | VS_aux of (val_spec_aux 'a) * annot 'a type kind_def 'a = | KD_aux of (kind_def_aux 'a) * annot 'a type scattered_def 'a = | SD_aux of (scattered_def_aux 'a) * annot 'a type fundef 'a = | FD_aux of (fundef_aux 'a) * annot 'a type dec_spec 'a = | DEC_aux of (dec_spec_aux 'a) * annot 'a type dec_comm 'a = (* Top-level generated comments *) | DC_comm of string (* generated unstructured comment *) | DC_comm_struct of (def 'a) (* generated structured comment *) and def 'a = (* Top-level definition *) | DEF_kind of (kind_def 'a) (* definition of named kind identifiers *) | DEF_type of (type_def 'a) (* type definition *) | DEF_fundef of (fundef 'a) (* function definition *) | DEF_val of (letbind 'a) (* value definition *) | DEF_spec of (val_spec 'a) (* top-level type constraint *) | DEF_default of (default_spec 'a) (* default kind and type assumptions *) | DEF_scattered of (scattered_def 'a) (* scattered function and type definition *) | DEF_reg_dec of (dec_spec 'a) (* register declaration *) | DEF_comm of (dec_comm 'a) (* generated comments *) type defs 'a = (* Definition sequence *) | Defs of list (def 'a) let rec remove_one i l = match l with | [] -> [] | i2::l2 -> if i2 = i then l2 else i2::(remove_one i l2) end let rec remove_from l l2 = match l2 with | [] -> l | i::l2' -> remove_from (remove_one i l) l2' end let disjoint s1 s2 = Set.null (s1 inter s2) let rec disjoint_all sets = match sets with | [] -> true | s1::[] -> true | s1::s2::sets -> (disjoint s1 s2) && (disjoint_all (s2::sets)) end type ne = (* internal numeric expressions *) | Ne_id of x | Ne_var of x | Ne_const of integer | Ne_inf | Ne_mult of ne * ne | Ne_add of list ne | Ne_minus of ne * ne | Ne_exp of ne | Ne_unary of ne type k = (* Internal kinds *) | Ki_typ | Ki_nat | Ki_ord | Ki_efct | Ki_ctor of list k * k | Ki_infer (* Representing an unknown kind, inferred by context *) type nec = (* Numeric expression constraints *) | Nec_lteq of ne * ne | Nec_eq of ne * ne | Nec_gteq of ne * ne | Nec_in of x * list integer | Nec_cond of list nec * list nec | Nec_branch of list nec type tid = (* A type identifier or type variable *) | Tid_id of id | Tid_var of kid type kinf = (* Whether a kind is default or from a local binding *) | Kinf_k of k | Kinf_def of k type t = (* Internal types *) | T_id of x | T_var of x | T_fn of t * t * effect | T_tup of list t | T_app of x * t_args | T_abbrev of t * t and t_arg = (* Argument to type constructors *) | T_arg_typ of t | T_arg_nexp of ne | T_arg_effect of effect | T_arg_order of order and t_args = (* Arguments to type constructors *) | T_args of list t_arg type tag = (* Data indicating where the identifier arises and thus information necessary in compilation *) | Tag_empty | Tag_intro (* Denotes an assignment and lexp that introduces a binding *) | Tag_set (* Denotes an expression that mutates a local variable *) | Tag_tuple_assign (* Denotes an assignment with a tuple lexp *) | Tag_global (* Globally let-bound or enumeration based value/variable *) | Tag_ctor (* Data constructor from a type union *) | Tag_extern of maybe string (* External function, specied only with a val statement *) | Tag_default (* Type has come from default declaration, identifier may not be bound locally *) | Tag_spec | Tag_enum of integer | Tag_alias | Tag_unknown of maybe string (* Tag to distinguish an unknown path from a non-analysis non deterministic path *) type tinf = (* Type variables, type, and constraints, bound to an identifier *) | Tinf_typ of t | Tinf_quant_typ of (map tid kinf) * list nec * tag * t type conformsto = (* how much conformance does overloading need *) | Conformsto_full | Conformsto_parm type widenvec = | Widenvec_widen | Widenvec_dont | Widenvec_dontcare type widennum = | Widennum_widen | Widennum_dont | Widennum_dontcare type tinflist = (* In place so that a list of tinfs can be referred to without the dot form *) | Tinfs_empty | Tinfs_ls of list tinf type widening = (* Should we widen vector start locations, should we widen atoms and ranges *) | Widening_w of widennum * widenvec type definition_env = | DenvEmp | Denv of (map tid kinf) * (map (list (id*t)) tinf) * (map t (list (nat*id))) let blength (bit) = Ne_const 8 let hlength (bit) = Ne_const 8 type env = | EnvEmp | Env of (map id tinf) * definition_env type inf = | Iemp | Inf of (list nec) * effect val denv_union : definition_env -> definition_env -> definition_env let denv_union de1 de2 = match (de1,de2) with | (DenvEmp,de2) -> de2 | (de1,DenvEmp) -> de1 | ((Denv ke1 re1 ee1),(Denv ke2 re2 ee2)) -> Denv (ke1 union ke2) (re1 union re2) (ee1 union ee2) end val env_union : env -> env -> env let env_union e1 e2 = match (e1,e2) with | (EnvEmp,e2) -> e2 | (e1,EnvEmp) -> e1 | ((Env te1 de1),(Env te2 de2)) -> Env (te1 union te2) (denv_union de1 de2) end let inf_union i1 i2 = match (i1,i2) with | (Iemp,i2) -> i2 | (i1,Iemp) -> i1 | (Inf n1 e1,Inf n2 e2) -> (Inf (n1++n2) (effect_union e1 e2)) end let fresh_kid denv = Var "x" (*TODO When strings can be manipulated, this should actually build a fresh string*) type E = env type I = inf