C: Refactor C backend

Main change is splitting apart the Sail->IR compilation stage and the
C code generation and optimization phase. Rather than variously
calling the intermediate language either bytecode (when it's not
really) or simply IR, we give it a name: Jib (a type of Sail). Most of
the types are still prefixed by c/C, and I don't think it's worth
changing this.

The various parts of the C backend are now in the src/jib/ subdirectory

src/jib/anf.ml         - Sail->ANF translation
src/jib/jib_util.ml    - various Jib AST processing and helper functions (formerly bytecode_util)
src/jib/jib_compile.ml - Sail->Jib translation (using Sail->ANF)
src/jib/c_backend.ml   - Jib->C code generator and optimizations

Further, bytecode.ott is now jib.ott and generates jib.ml (which still
lives in src/ for now)

The optimizations in c_backend.ml should eventually be moved in a
separate jib_optimization file.

The Sail->Jib compilation can be parameterised by two functions - one
is a custom ANF->ANF optimization pass that can be specified on a per
Jib backend basis, and the other is the rule for translating Sail
types in Jib types. This can be more or less precise depending on how
precise we want to be about bit-widths etc, i.e. we only care about <64
and >64 for C, but for SMT generation we would want to be as precise
as possible.

Additional improvements:

The Jib IR is now agnostic about whether arguments are allocated on
the heap vs the stack and this is handled by the C code generator.

jib.ott now has some more comments explaining various parts of the Jib
AST.

A Set module and comparison function for ctyps is defined, and some
functions now return ctyp sets rather than lists to avoid repeated
work.

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