diff options
Diffstat (limited to 'language/bytecode.ott')
| -rw-r--r-- | language/bytecode.ott | 133 |
1 files changed, 133 insertions, 0 deletions
diff --git a/language/bytecode.ott b/language/bytecode.ott new file mode 100644 index 00000000..7342a1e9 --- /dev/null +++ b/language/bytecode.ott @@ -0,0 +1,133 @@ +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 }} + +embed +{{ lem + +open import Ast + +}} + +grammar + + +% Fragments are small pure snippets of (abstract) C code, mostly +% expressions, used by the aval and cval types. +fragment :: 'F_' ::= + | id :: :: id + | string :: :: lit + | have_exception :: :: have_exception + | current_exception :: :: current_exception + | fragment op fragment' :: :: op + | op fragment :: :: unary + | fragment . string :: :: field + +ctyp :: 'CT_' ::= + {{ com C type }} + | mpz_t :: :: mpz +% Arbitrary precision GMP integer, mpz_t in C. }} + | bv_t ( bool ) :: :: bv +% Variable length bitvector - flag represents direction, inc or dec }} + | uint64_t ( nat , bool ) :: :: uint64 +% Fixed length bitvector that fits within a 64-bit word. - int +% represents length, and flag is the same as CT_bv. }} + | int64_t :: :: int64 +% 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. + +cval :: 'CV_' ::= + {{ ocaml fragment * ctyp }} + {{ lem fragment * ctyp }} + +clexp :: 'CL_' ::= + | id :: :: id + | id . string :: :: field + | * id :: :: addr + | current_exception :: :: 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 + | alloc ctyp id :: :: alloc + | ctyp id = cval :: :: init + | if ( cval ) { instr0 ; ... ; instrn } + else { instr0 ; ... ; instrm } : ctyp :: :: if + | clexp = id ( cval0 , ... , cvaln ) : ctyp :: :: funcall + | clexp = cval :: :: copy + | clexp = ( ctyp ) id : ctyp' :: :: convert + | 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 + | match_failure :: :: match_failure + +cdef :: 'CDEF_' ::= + | register id : ctyp :: :: reg_dec + | ctype_def :: :: type + | function id mid ( id0 , ... , idn ) { + instr0 ; ... ; instrm + } :: :: fundef
\ No newline at end of file |