diff options
Diffstat (limited to 'language/bytecode.ott')
| -rw-r--r-- | language/bytecode.ott | 172 |
1 files changed, 0 insertions, 172 deletions
diff --git a/language/bytecode.ott b/language/bytecode.ott deleted file mode 100644 index cc329e02..00000000 --- a/language/bytecode.ott +++ /dev/null @@ -1,172 +0,0 @@ -indexvar n , m , i , j ::= - {{ phantom }} - {{ com Index variables for meta-lists }} - -metavar nat ::= - {{ phantom }} - {{ ocaml int }} - {{ lem nat }} - -metavar id ::= - {{ phantom }} - {{ ocaml id }} - {{ lem id }} - -metavar mid ::= - {{ phantom }} - {{ ocaml id option }} - {{ lem maybe id }} - -metavar string ::= - {{ phantom }} - {{ ocaml string }} - {{ lem string }} - -metavar op ::= - {{ phantom }} - {{ ocaml string }} - {{ lem string }} - -metavar bool ::= - {{ phantom }} - {{ ocaml bool }} - {{ lem bool }} - -metavar value ::= - {{ phantom }} - {{ lem vl }} - {{ ocaml vl }} - -embed -{{ lem - -open import Ast -open import Value2 - -}} - -grammar - -% Fragments are small pure snippets of (abstract) C code, mostly -% expressions, used by the aval and cval types. -fragment :: 'F_' ::= - | id :: :: id - | '&' id :: :: ref - | value :: :: lit - | have_exception :: :: have_exception - | current_exception :: :: current_exception - | fragment op fragment' :: :: op - | op fragment :: :: unary - | string ( fragment0 , ... , fragmentn ) :: :: call - | fragment . string :: :: field - | string :: :: raw - | poly fragment :: :: poly - -% init / clear -> create / kill - -ctyp :: 'CT_' ::= - {{ com C type }} - | mpz_t :: :: lint -% Arbitrary precision GMP integer, mpz_t in C. - | bv_t ( bool ) :: :: lbits -% Variable length bitvector - flag represents direction, true - dec or false - inc - | sbv_t ( bool ) :: :: sbits -% Small variable length bitvector - less than 64 bits - | 'uint64_t' ( nat , bool ) :: :: fbits -% Fixed length bitvector that fits within a 64-bit word. - int -% represents length, and flag is the same as CT_bv. - | 'int64_t' nat :: :: fint -% Used for (signed) integers that fit within 64-bits. - | unit_t :: :: unit -% unit is a value in sail, so we represent it as a one element type -% here too for clarity but we actually compile it to an int which is -% always 0. - | bool_t :: :: bool - | real_t :: :: real - | bit_t :: :: bit -% The real type in sail. Abstract here, but implemented using either -% GMP rationals or high-precision floating point. - | ( ctyp0 , ... , ctypn ) :: :: tup - | string_t :: :: string - | enum id ( id0 , ... , idn ) :: :: enum - | struct id ( id0 * ctyp0 , ... , idn * ctypn ) :: :: struct - | variant id ( id0 * ctyp0 , ... , idn * ctypn ) :: :: variant -% Abstractly represent how all the Sail user defined types get mapped -% into C. We don't fully worry about precise implementation details at -% this point, as C doesn't have variants or tuples natively, but these -% need to be encoded. - | vector ( bool , ctyp ) :: :: vector - | list ( ctyp ) :: :: list -% A vector type for non-bit vectors, and a list type. - | ref ( ctyp ) :: :: ref - | poly :: :: poly - -cval :: 'CV_' ::= - {{ ocaml fragment * ctyp }} - {{ lem fragment * ctyp }} - -clexp :: 'CL_' ::= - | id : ctyp :: :: id - | clexp . string :: :: field - | * clexp :: :: addr - | clexp . nat :: :: tuple - | current_exception : ctyp :: :: current_exception - | have_exception :: :: have_exception - -ctype_def :: 'CTD_' ::= - {{ com C type definition }} - | enum id = id0 '|' ... '|' idn :: :: enum - | struct id = { id0 : ctyp0 , ... , idn : ctypn } :: :: struct - | variant id = { id0 : ctyp0 , ... , idn : ctypn } :: :: variant - -iannot :: 'IA_' ::= - {{ lem nat * nat * nat }} - {{ ocaml int * int * int }} - -instr :: 'I_' ::= - {{ aux _ iannot }} - | ctyp id :: :: decl - | ctyp id = cval :: :: init - | if ( cval ) { instr0 ; ... ; instrn } - else { instr0 ; ... ; instrm } : ctyp :: :: if - | jump ( cval ) string :: :: jump - | clexp = bool id ( cval0 , ... , cvaln ) :: :: funcall - | clexp = cval :: :: copy - | alias clexp = cval :: :: alias - | clear ctyp id :: :: clear - | return cval :: :: return - | { instr0 ; ... ; instrn } :: :: block - | try { instr0 ; ... ; instrn } :: :: try_block - | throw cval :: :: throw - | '//' string :: :: comment - | C string :: :: raw % only used for GCC attributes - | string : :: :: label - | goto string :: :: goto - | undefined ctyp :: :: undefined - | match_failure :: :: match_failure - -% For optimising away allocations. - | reset ctyp id :: :: reset - | ctyp id = cval :: :: reinit - -cdef :: 'CDEF_' ::= - | register id : ctyp = { - instr0 ; ... ; instrn - } :: :: reg_dec - | ctype_def :: :: type - | let nat ( id0 : ctyp0 , ... , idn : ctypn ) = { - instr0 ; ... ; instrm - } :: :: let -% The first list of instructions creates up the global letbinding, the -% second kills it. - | val id ( ctyp0 , ... , ctypn ) -> ctyp - :: :: spec - | function id mid ( id0 , ... , idn ) { - instr0 ; ... ; instrm - } :: :: fundef - | startup id { - instr0 ; ... ; instrn - } :: :: startup - | finish id { - instr0 ; ... ; instrn - } :: :: finish |