C backend improvements

- Propagate types more accurately to improve optimization on ANF
  representation.

- Add a generic optimization pass to remove redundant variables that
  simply alias other variables.

- Modify Sail interactive mode, so it can compile a specification with
  the :compile command, view generated intermediate representation via
  the :ir <function> command, and step-through the IR with :exec <exp>
  (although this is very incomplete)

- Introduce a third bitvector representation, between fast
  fixed-precision bitvectors, and variable length large
  bitvectors. The bitvector types are now from most efficient to least

   * CT_fbits for fixed precision, 64-bit or less bitvectors
   * CT_sbits for 64-bit or less, variable length bitvectors
   * CT_lbits for arbitrary variable length bitvectors

- Support for generating C code using CT_sbits is currently
  incomplete, it just exists in the intermediate representation right
  now.

- Include ctyp in AV_C_fragment, so we don't have to recompute it

1 files changed, 16 insertions, 14 deletions

diff --git a/language/bytecode.ott b/language/bytecode.ott
index cbc60e52..d8d01fb5 100644
--- a/language/bytecode.ott
+++ b/language/bytecode.ott
@@ -66,26 +66,28 @@ fragment :: 'F_' ::=
 
 ctyp :: 'CT_' ::=
   {{ com C type }}
-  | mpz_t                   :: :: int
-% Arbitrary precision GMP integer, mpz_t in C. }}
-  | bv_t ( bool )           :: :: bits
-% Variable length bitvector - flag represents direction, true - dec or false - inc }}
-  | 'uint64_t' ( nat , bool ) :: :: bits64
+  | mpz_t                     :: :: int
+% 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'               :: :: int64
-% Used for (signed) integers that fit within 64-bits. }}
-  | unit_t                  :: :: unit
+% 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
+  | 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
+  | ( 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