Formalize C backend intermediate representation in Ott

Describes precisely the intermediate representation used in the C
backend in an ott grammar, and also removes several C-isms where raw C
code was inserted into the IR, so in theory this IR could be
interpreted by a small VM/interpreter or compiled to LLVM bytecode
etc. Currently the I_raw constructor for inserting C code is just used
for inserting GCC attributes, so it can safely be ignored.

Also augment and refactor the instruction type with an aux constructor
so location information can be propagated down to this level.

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