Attempt to document intermediate language used by Sail in ott.

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