path: root/language/sil.ott

%%% 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