%%% Sail Intermediate Language %%% % An attempt to precisely document the subset of sail that the % rewriter is capable of re-writing sail into. It is intended to be a % strict subset of the Sail AST, and be typecheckable with the full % typechecker. % % Notably, it lacks: % - Special (bit)vector syntax. % - Complex l-values. % - Existential types. % - Polymorphism, of any kind. indexvar n , m , i , j ::= {{ phantom }} {{ com Index variables for meta-lists }} metavar num,numZero,numOne ::= {{ phantom }} {{ lex numeric }} {{ ocaml int }} {{ hol num }} {{ lem integer }} {{ com Numeric literals }} metavar nat ::= {{ phantom }} {{ ocaml int }} {{ lex numeric }} {{ lem nat }} metavar string ::= {{ phantom }} {{ ocaml string }} {{ lem string }} {{ hol string }} {{ com String literals }} metavar real ::= {{ phantom }} {{ ocaml string }} {{ lem string }} {{ hol string }} {{ com Real number literal }} embed {{ ocaml type text = string type l = Parse_ast.l type 'a annot = l * 'a type loop = While | Until }} embed {{ lem open import Pervasives open import Pervasives_extra 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 loop = While | Until }} metavar x , y , z ::= {{ ocaml text }} {{ lem string }} {{ hol string }} {{ com identifier }} {{ ocamlvar "[[x]]" }} {{ lemvar "[[x]]" }} grammar l :: '' ::= {{ phantom }} {{ ocaml Parse_ast.l }} {{ lem l }} {{ hol unit }} {{ com source location }} | :: :: Unknown {{ ocaml Unknown }} {{ lem Unknown }} {{ hol () }} id :: '' ::= {{ com Identifier }} {{ aux _ l }} | x :: :: id | ( deinfix x ) :: D :: deIid {{ com remove infix status }} base_effect :: 'BE_' ::= {{ com effect }} {{ aux _ l }} | rreg :: :: rreg {{ com read register }} | wreg :: :: wreg {{ com write register }} | rmem :: :: rmem {{ com read memory }} | rmemt :: :: rmemt {{ com read memory and tag }} | wmem :: :: wmem {{ com write memory }} | wmea :: :: eamem {{ com signal effective address for writing memory }} | exmem :: :: exmem {{ com determine if a store-exclusive (ARM) is going to succeed }} | wmv :: :: wmv {{ com write memory, sending only value }} | wmvt :: :: wmvt {{ com write memory, sending only value and tag }} | barr :: :: barr {{ com memory barrier }} | depend :: :: depend {{ com dynamic footprint }} | undef :: :: undef {{ com undefined-instruction exception }} | unspec :: :: unspec {{ com unspecified values }} | nondet :: :: nondet {{ com nondeterminism, from $[[nondet]]$ }} | escape :: :: escape {{ com potential call of $[[exit]]$ }} | lset :: :: lset {{ com local mutation; not user-writable }} | lret :: :: lret {{ com local return; not user-writable }} effect :: 'Effect_' ::= {{ com effect set, of kind $[[Effect]]$ }} {{ aux _ l }} | { base_effect1 , .. , base_effectn } :: :: set {{ com effect set }} | pure :: M :: pure {{ com sugar for empty effect set }} {{ lem (Effect_set []) }} {{icho [[{}]] }} | effect1 u+ .. u+ effectn :: M :: union {{ com union of sets of effects }} {{ icho [] }} {{ lem (List.foldr effect_union (Effect_aux (Effect_set []) Unknown) [[effect1..effectn]]) }} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Types % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% typ :: 'Typ_' ::= {{ com type expressions, of kind $[[Type]]$ }} {{ aux _ l }} | id :: :: id {{ com defined type }} | typ1 -> typ2 effectkw effect :: :: fn {{ com Function (first-order only in user code) }} | ( typ1 , .... , typn ) :: :: tup {{ com Tuple }} | id < typ_arg1 , .. , typ_argn > :: :: app {{ com type constructor application }} typ_arg :: 'Typ_arg_' ::= {{ com type constructor arguments of all kinds }} {{ aux _ l }} | typ :: :: typ typquant :: 'TypQ_' ::= {{ com type quantifiers and constraints}} {{ aux _ l }} | :: :: no_forall {{ com empty }} typschm :: 'TypSchm_' ::= {{ com type scheme }} {{ aux _ l }} | typquant typ :: :: ts %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Type definitions % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% type_def {{ ocaml 'a type_def }} {{ lem type_def 'a }} :: 'TD_' ::= {{ ocaml TD_aux of type_def_aux * 'a annot }} {{ lem TD_aux of type_def_aux * annot 'a }} | type_def_aux :: :: aux type_def_aux :: 'TD_' ::= {{ com type definition body }} | typedef id = typschm :: :: abbrev {{ com type abbreviation }} {{ texlong }} | typedef id = const struct typquant { typ1 id1 ; ... ; typn idn } :: :: record {{ com struct type definition }} {{ texlong }} | typedef id = const union typquant { type_union1 ; ... ; type_unionn } :: :: variant {{ com tagged union type definition}} {{ texlong }} | typedef id = enumerate { id1 ; ... ; idn } :: :: enum {{ com enumeration type definition}} {{ texlong }} % This one is a bit unusual - I think all nexps here must be constant, so replace with num. | typedef id = register bits [ num : num' ] { index_range1 : id1 ; ... ; index_rangen : idn } :: :: register {{ com register mutable bitfield type definition }} {{ texlong }} type_union :: 'Tu_' ::= {{ com type union constructors }} {{ aux _ l }} | id :: :: id | typ id :: :: ty_id index_range :: 'BF_' ::= {{ com index specification, for bitfields in register types}} {{ aux _ l }} | num :: :: 'single' {{ com single index }} | num1 '..' num2 :: :: range {{ com index range }} | index_range1 , index_range2 :: :: concat {{ com concatenation of index ranges }} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Literals % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% lit :: 'L_' ::= {{ com literal constant }} {{ aux _ l }} | ( ) :: :: unit {{ com $() : [[unit]]$ }} | bitzero :: :: zero {{ com $[[bitzero]] : [[bit]]$ }} | bitone :: :: one {{ com $[[bitone]] : [[bit]]$ }} | true :: :: true {{ com $[[true]] : [[bool]]$ }} | false :: :: false {{ com $[[false]] : [[bool]]$ }} | num :: :: num {{ com natural number constant }} % Need to represent as a function call, e.g. sil#hex_string "0xFFFF". % | hex :: :: hex {{ com bit vector constant, C-style }} % | bin :: :: bin {{ com bit vector constant, C-style }} | string :: :: string {{ com string constant }} | undefined :: :: undef {{ com undefined-value constant }} | real :: :: real {{ com real number }} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Patterns % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% pat :: 'P_' ::= {{ com pattern }} {{ aux _ annot }} {{ auxparam 'a }} | _ :: :: wild {{ com wildcard }} | ( pat as id ) :: :: as {{ com named pattern }} | ( typ ) pat :: :: typ {{ com typed pattern }} | id :: :: id {{ com identifier }} | id ( pat1 , .. , patn ) :: :: app {{ com union constructor pattern }} | { fpat1 ; ... ; fpatn } :: :: record {{ com struct pattern }} | ( pat1 , .... , patn ) :: :: tup {{ com tuple pattern }} | [|| pat1 , .. , patn ||] :: :: list {{ com list pattern }} | ( pat ) :: S :: paren {{ ichlo [[pat]] }} | pat1 '::' pat2 :: :: cons {{ com Cons patterns }} fpat :: 'FP_' ::= {{ com field pattern }} {{ aux _ annot }} {{ auxparam 'a }} | id = pat :: :: Fpat %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Expressions % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% loop :: loop ::= {{ phantom }} | while :: :: while | until :: :: until exp :: 'E_' ::= {{ com expression }} {{ aux _ annot }} {{ auxparam 'a }} | { exp1 ; ... ; expn } :: :: block {{ com sequential block }} | nondet { exp1 ; ... ; expn } :: :: nondet {{ com nondeterministic block }} | id :: :: id {{ com identifier }} | lit :: :: lit {{ com literal constant }} % Purely an annotation as all casting is resolved by type checker, can % be evaluated by simply dropping the type. | ( typ ) exp :: :: cast {{ com cast }} | id ( exp1 , .. , expn ) :: :: app {{ com function application }} | ( exp1 , .... , expn ) :: :: tuple {{ com tuple }} | if exp1 then exp2 else exp3 :: :: if {{ com conditional }} | loop exp1 exp2 :: :: loop {{ com while or until loop }} | foreach ( id from exp1 to exp2 by exp3 in order ) exp4 :: :: for {{ com for loop }} | [|| exp1 , .. , expn ||] :: :: list {{ com list }} | exp1 '::' exp2 :: :: cons {{ com cons }} | { fexps } :: :: record {{ com struct }} | { exp with fexps } :: :: record_update {{ com functional update of struct }} | exp . id :: :: field {{ com field projection from struct }} | switch exp { case pexp1 ... case pexpn } :: :: case {{ com pattern matching }} | letbind in exp :: :: let {{ com let expression }} | lexp := exp :: :: assign {{ com imperative assignment }} | return exp :: :: return {{ com return $[[exp]]$ from current function }} | exit exp :: :: exit {{ com halt all current execution }} | value :: I :: value {{ com For internal use in interpreter to wrap pre-evaluated values when returning an action }} lexp :: 'LEXP_' ::= {{ com lvalue expression }} {{ aux _ annot }} {{ auxparam 'a }} | id :: :: id {{ com identifier }} | ( typ ) id :: :: cast {{ com cast }} | ( lexp0 , .. , lexpn ) :: :: tup {{ com multiple (non-memory) assignment }} % SIL: Not sure how much to rewrite L-expressions. % | lexp [ exp ] :: :: vector {{ com vector element }} % | lexp [ exp1 '..' exp2 ] :: :: vector_range {{ com subvector }} % | lexp . id :: :: field {{ com struct field }} fexp :: 'FE_' ::= {{ com field expression }} {{ aux _ annot }} {{ auxparam 'a }} | id = exp :: :: Fexp fexps :: 'FES_' ::= {{ com field expression list }} {{ aux _ annot }} {{ auxparam 'a }} | fexp1 ; ... ; fexpn :: :: Fexps pexp :: 'Pat_' ::= {{ com pattern match }} {{ aux _ annot }} {{ auxparam 'a }} | pat -> exp :: :: exp | pat when exp1 -> exp :: :: when %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Function definitions % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% tannot_opt :: 'Typ_annot_opt_' ::= {{ com optional type annotation for functions}} {{ aux _ l }} | :: :: none | typquant typ :: :: some rec_opt :: 'Rec_' ::= {{ com optional recursive annotation for functions }} {{ aux _ l }} | :: :: nonrec {{ com non-recursive }} | rec :: :: rec {{ com recursive }} effect_opt :: 'Effect_opt_' ::= {{ com optional effect annotation for functions }} {{ aux _ l }} | :: :: pure {{ com sugar for empty effect set }} | effectkw effect :: :: effect funcl :: 'FCL_' ::= {{ com function clause }} {{ aux _ annot }} {{ auxparam 'a }} | id pat = exp :: :: Funcl fundef :: 'FD_' ::= {{ com function definition}} {{ aux _ annot }} {{ auxparam 'a }} | function rec_opt tannot_opt effect_opt funcl1 and ... and funcln :: :: function {{ texlong }} letbind :: 'LB_' ::= {{ com let binding }} {{ aux _ annot }} {{ auxparam 'a }} | let pat = exp :: :: val {{ com let, implicit type ($[[pat]]$ must be total)}} val_spec {{ ocaml 'a val_spec }} {{ lem val_spec 'a }} :: 'VS_' ::= {{ ocaml VS_aux of val_spec_aux * 'a annot }} {{ lem VS_aux of val_spec_aux * annot 'a }} | val_spec_aux :: :: aux val_spec_aux :: 'VS_' ::= {{ com value type specification }} {{ ocaml VS_val_spec of typschm * id * (string -> string option) * bool }} {{ lem VS_val_spec of typschm * id * maybe string * bool }} | val typschm id :: S :: val_spec {{ com specify the type of an upcoming definition }} {{ ocaml (VS_val_spec [[typschm]] [[id]] None false) }} {{ lem }} default_spec :: 'DT_' ::= {{ com default kinding or typing assumption }} {{ aux _ l }} | default Order order :: :: order reg_id :: 'RI_' ::= {{ aux _ annot }} {{ auxparam 'a }} | id :: :: id alias_spec :: 'AL_' ::= {{ com register alias expression forms }} {{ aux _ annot }} {{ auxparam 'a }} | reg_id . id :: :: subreg | reg_id [ exp ] :: :: bit | reg_id [ exp '..' exp' ] :: :: slice | reg_id : reg_id' :: :: concat dec_spec :: 'DEC_' ::= {{ com register declarations }} {{ aux _ annot }} {{ auxparam 'a }} | register typ id :: :: reg | register alias id = alias_spec :: :: alias | register alias typ id = alias_spec :: :: typ_alias %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Top-level definitions % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% prec :: '' ::= | infix :: :: Infix | infixl :: :: InfixL | infixr :: :: InfixR def :: 'DEF_' ::= {{ com top-level definition }} {{ auxparam 'a }} | type_def :: :: type {{ com type definition }} | fundef :: :: fundef {{ com function definition }} | letbind :: :: val {{ com value definition }} | val_spec :: :: spec {{ com top-level type constraint }} | fix prec num id :: :: fixity {{ com fixity declaration }} | overload id [ id1 ; ... ; idn ] :: :: overload {{ com operator overload specification }} | default_spec :: :: default {{ com default kind and type assumptions }} | dec_spec :: :: reg_dec {{ com register declaration }} defs :: '' ::= {{ com definition sequence }} {{ auxparam 'a }} | def1 .. defn :: :: Defs