diff options
Diffstat (limited to 'language')
| -rw-r--r-- | language/sil.ott | 451 |
1 files changed, 451 insertions, 0 deletions
diff --git a/language/sil.ott b/language/sil.ott new file mode 100644 index 00000000..40adfc4d --- /dev/null +++ b/language/sil.ott @@ -0,0 +1,451 @@ +%%% 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 |