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, 114 insertions, 19 deletions

diff --git a/src/bytecode_util.ml b/src/bytecode_util.ml
index 6334210e..783f6793 100644
--- a/src/bytecode_util.ml
+++ b/src/bytecode_util.ml
@@ -131,6 +131,73 @@ let rec frag_rename from_id to_id = function
   | F_raw raw -> F_raw raw
   | F_poly f -> F_poly (frag_rename from_id to_id f)
 
+let cval_rename from_id to_id (frag, ctyp) = (frag_rename from_id to_id frag, ctyp)
+
+let rec clexp_rename from_id to_id = function
+  | CL_id (id, ctyp) when Id.compare id from_id = 0 -> CL_id (to_id, ctyp)
+  | CL_id (id, ctyp) -> CL_id (id, ctyp)
+  | CL_field (clexp, field) ->
+     CL_field (clexp_rename from_id to_id clexp, field)
+  | CL_addr clexp ->
+     CL_addr (clexp_rename from_id to_id clexp)
+  | CL_tuple (clexp, n) ->
+     CL_tuple (clexp_rename from_id to_id clexp, n)
+  | CL_current_exception ctyp -> CL_current_exception ctyp
+  | CL_have_exception -> CL_have_exception
+
+let rec instr_rename from_id to_id (I_aux (instr, aux)) =
+  let instr = match instr with
+    | I_decl (ctyp, id) when Id.compare id from_id = 0 -> I_decl (ctyp, to_id)
+    | I_decl (ctyp, id) -> I_decl (ctyp, id)
+
+    | I_init (ctyp, id, cval) when Id.compare id from_id = 0 ->
+       I_init (ctyp, to_id, cval_rename from_id to_id cval)
+    | I_init (ctyp, id, cval) ->
+       I_init (ctyp, id, cval_rename from_id to_id cval)
+
+    | I_if ((frag, ctyp1), then_instrs, else_instrs, ctyp2) ->
+       I_if ((frag_rename from_id to_id frag, ctyp1), then_instrs, else_instrs, ctyp2)
+
+    | I_jump (cval, label) -> I_jump (cval_rename from_id to_id cval, label)
+
+    | I_funcall (clexp, extern, id, args) ->
+       I_funcall (clexp_rename from_id to_id clexp, extern, id, List.map (cval_rename from_id to_id) args)
+
+    | I_copy (clexp, cval) -> I_copy (clexp_rename from_id to_id clexp, cval_rename from_id to_id cval)
+
+    | I_clear (ctyp, id) when Id.compare id from_id = 0 -> I_clear (ctyp, to_id)
+    | I_clear (ctyp, id) -> I_clear (ctyp, id)
+
+    | I_return cval -> I_return (cval_rename from_id to_id cval)
+
+    | I_block instrs -> I_block (List.map (instr_rename from_id to_id) instrs)
+
+    | I_try_block instrs -> I_try_block (List.map (instr_rename from_id to_id) instrs)
+
+    | I_throw cval -> I_throw (cval_rename from_id to_id cval)
+
+    | I_comment str -> I_comment str
+
+    | I_raw str -> I_raw str
+
+    | I_label label -> I_label label
+
+    | I_goto label -> I_goto label
+
+    | I_undefined ctyp -> I_undefined ctyp
+
+    | I_match_failure -> I_match_failure
+
+    | I_reset (ctyp, id) when Id.compare id from_id = 0 -> I_reset (ctyp, to_id)
+    | I_reset (ctyp, id) -> I_reset (ctyp, id)
+
+    | I_reinit (ctyp, id, cval) when Id.compare id from_id = 0 ->
+       I_reinit (ctyp, to_id, cval_rename from_id to_id cval)
+    | I_reinit (ctyp, id, cval) ->
+       I_reinit (ctyp, id, cval_rename from_id to_id cval)
+  in
+  I_aux (instr, aux)
+
 (**************************************************************************)
 (* 1. Instruction pretty printer                                          *)
 (**************************************************************************)
@@ -175,12 +242,14 @@ and string_of_fragment' ?zencode:(zencode=true) f =
 (* String representation of ctyps here is only for debugging and
    intermediate language pretty-printer. *)
 and string_of_ctyp = function
-  | CT_int -> "mpz_t"
-  | CT_bits true -> "bv_t(dec)"
-  | CT_bits false -> "bv_t(inc)"
-  | CT_bits64 (n, true) -> "uint64_t(" ^ string_of_int n ^ ", dec)"
-  | CT_bits64 (n, false) -> "uint64_t(" ^ string_of_int n ^ ", int)"
-  | CT_int64 -> "int64_t"
+  | CT_int -> "int"
+  | CT_lbits true -> "lbits(dec)"
+  | CT_lbits false -> "lbits(inc)"
+  | CT_fbits (n, true) -> "fbits(" ^ string_of_int n ^ ", dec)"
+  | CT_fbits (n, false) -> "fbits(" ^ string_of_int n ^ ", int)"
+  | CT_sbits true -> "sbits(dec)"
+  | CT_sbits false -> "sbits(inc)"
+  | CT_int64 -> "int64"
   | CT_bit -> "bit"
   | CT_unit -> "unit"
   | CT_bool -> "bool"
@@ -197,12 +266,14 @@ and string_of_ctyp = function
 (** This function is like string_of_ctyp, but recursively prints all
    constructors in variants and structs. Used for debug output. *)
 and full_string_of_ctyp = function
-  | CT_int -> "mpz_t"
-  | CT_bits true -> "bv_t(dec)"
-  | CT_bits false -> "bv_t(inc)"
-  | CT_bits64 (n, true) -> "uint64_t(" ^ string_of_int n ^ ", dec)"
-  | CT_bits64 (n, false) -> "uint64_t(" ^ string_of_int n ^ ", int)"
-  | CT_int64 -> "int64_t"
+  | CT_int -> "int"
+  | CT_lbits true -> "lbits(dec)"
+  | CT_lbits false -> "lbits(inc)"
+  | CT_fbits (n, true) -> "fbits(" ^ string_of_int n ^ ", dec)"
+  | CT_fbits (n, false) -> "fbits(" ^ string_of_int n ^ ", int)"
+  | CT_sbits true -> "sbits(dec)"
+  | CT_sbits false -> "sbits(inc)"
+  | CT_int64 -> "int64"
   | CT_bit -> "bit"
   | CT_unit -> "unit"
   | CT_bool -> "bool"
@@ -222,7 +293,8 @@ and full_string_of_ctyp = function
   | CT_poly -> "*"
 
 let rec map_ctyp f = function
-  | (CT_int | CT_int64 | CT_bits _ | CT_bits64 _ | CT_bit | CT_unit | CT_bool | CT_real | CT_string | CT_poly | CT_enum _) as ctyp -> f ctyp
+  | (CT_int | CT_int64 | CT_lbits _ | CT_fbits _ | CT_sbits _
+     | CT_bit | CT_unit | CT_bool | CT_real | CT_string | CT_poly | CT_enum _) as ctyp -> f ctyp
   | CT_tup ctyps -> f (CT_tup (List.map (map_ctyp f) ctyps))
   | CT_ref ctyp -> f (CT_ref (map_ctyp f ctyp))
   | CT_vector (direction, ctyp) -> f (CT_vector (direction, map_ctyp f ctyp))
@@ -233,8 +305,9 @@ let rec map_ctyp f = function
 let rec ctyp_equal ctyp1 ctyp2 =
   match ctyp1, ctyp2 with
   | CT_int, CT_int -> true
-  | CT_bits d1, CT_bits d2 -> d1 = d2
-  | CT_bits64 (m1, d1), CT_bits64 (m2, d2) -> m1 = m2 && d1 = d2
+  | CT_lbits d1, CT_lbits d2 -> d1 = d2
+  | CT_sbits d1, CT_sbits d2 -> d1 = d2
+  | CT_fbits (m1, d1), CT_fbits (m2, d2) -> m1 = m2 && d1 = d2
   | CT_bit, CT_bit -> true
   | CT_int64, CT_int64 -> true
   | CT_unit, CT_unit -> true
@@ -271,8 +344,9 @@ let rec ctyp_unify ctyp1 ctyp2 =
 
 let rec ctyp_suprema = function
   | CT_int -> CT_int
-  | CT_bits d -> CT_bits d
-  | CT_bits64 (_, d) -> CT_bits d
+  | CT_lbits d -> CT_lbits d
+  | CT_fbits (_, d) -> CT_lbits d
+  | CT_sbits d -> CT_lbits d
   | CT_int64 -> CT_int
   | CT_unit -> CT_unit
   | CT_bool -> CT_bool
@@ -298,7 +372,7 @@ let rec ctyp_ids = function
      IdSet.add id (List.fold_left (fun ids (_, ctyp) -> IdSet.union (ctyp_ids ctyp) ids) IdSet.empty ctors)
   | CT_tup ctyps -> List.fold_left (fun ids ctyp -> IdSet.union (ctyp_ids ctyp) ids) IdSet.empty ctyps
   | CT_vector (_, ctyp) | CT_list ctyp | CT_ref ctyp -> ctyp_ids ctyp
-  | CT_int | CT_int64 | CT_bits _ | CT_bits64 _ | CT_unit
+  | CT_int | CT_int64 | CT_lbits _ | CT_fbits _ | CT_sbits _ | CT_unit
     | CT_bool | CT_real | CT_bit | CT_string | CT_poly -> IdSet.empty
 
 let rec unpoly = function
@@ -310,7 +384,7 @@ let rec unpoly = function
   | f -> f
 
 let rec is_polymorphic = function
-  | CT_int | CT_int64 | CT_bits _ | CT_bits64 _ | CT_bit | CT_unit | CT_bool | CT_real | CT_string -> false
+  | CT_int | CT_int64 | CT_lbits _ | CT_fbits _ | CT_sbits _ | CT_bit | CT_unit | CT_bool | CT_real | CT_string -> false
   | CT_tup ctyps -> List.exists is_polymorphic ctyps
   | CT_enum _ -> false
   | CT_struct (_, ctors) | CT_variant (_, ctors) -> List.exists (fun (_, ctyp) -> is_polymorphic ctyp) ctors
@@ -685,3 +759,24 @@ let rec map_instrs f (I_aux (instr, aux)) =
     | I_comment _ | I_label _ | I_goto _ | I_raw _ | I_match_failure | I_undefined _ -> instr
   in
   I_aux (instr, aux)
+
+let rec instr_ids (I_aux (instr, _)) =
+  let reads, writes = instr_deps instr in
+  let get_id = function
+    | G_id id -> Some id
+    | _ -> None
+  in
+  NS.elements reads @ NS.elements writes
+  |> List.map get_id
+  |> Util.option_these
+  |> IdSet.of_list
+
+let rec filter_instrs f instrs =
+  let filter_instrs' = function
+    | I_aux (I_block instrs, aux) -> I_aux (I_block (filter_instrs f instrs), aux)
+    | I_aux (I_try_block instrs, aux) -> I_aux (I_try_block (filter_instrs f instrs), aux)
+    | I_aux (I_if (cval, instrs1, instrs2, ctyp), aux) ->
+       I_aux (I_if (cval, filter_instrs f instrs1, filter_instrs f instrs2, ctyp), aux)
+    | instr -> instr
+  in
+  List.filter f (List.map filter_instrs' instrs)