Additional optimizations for C compilation

9 files changed, 189 insertions, 2 deletions

diff --git a/lib/sail.c b/lib/sail.c
index 5c83690d..c66c057c 100644
--- a/lib/sail.c
+++ b/lib/sail.c
@@ -680,6 +680,11 @@ void zero_extend(lbits *rop, const lbits op, const sail_int len)
   mpz_set(*rop->bits, *op.bits);
 }
 
+fbits fast_zero_extend(const sbits op, const uint64_t n)
+{
+  return op.bits;
+}
+
 void sign_extend(lbits *rop, const lbits op, const sail_int len)
 {
   assert(op.len <= mpz_get_ui(len));
@@ -694,6 +699,32 @@ void sign_extend(lbits *rop, const lbits op, const sail_int len)
   }
 }
 
+fbits fast_sign_extend(const fbits op, const uint64_t n, const uint64_t m)
+{
+  uint64_t rop = op;
+  if (op & (UINT64_C(1) << (n - 1))) {
+    for (uint64_t i = m - 1; i >= n; i--) {
+      rop = rop | (UINT64_C(1) << i);
+    }
+    return rop;
+  } else {
+    return rop;
+  }
+}
+
+fbits fast_sign_extend2(const sbits op, const uint64_t m)
+{
+  uint64_t rop = op.bits;
+  if (op.bits & (UINT64_C(1) << (op.len - 1))) {
+    for (uint64_t i = m - 1; i >= op.len; i--) {
+      rop = rop | (UINT64_C(1) << i);
+    }
+    return rop;
+  } else {
+    return rop;
+  }
+}
+
 void length_lbits(sail_int *rop, const lbits op)
 {
   mpz_set_ui(*rop, op.len);
@@ -783,12 +814,21 @@ void sail_signed(sail_int *rop, const lbits op)
   }
 }
 
-inline
 mach_int fast_unsigned(const fbits op)
 {
   return (mach_int) op;
 }
 
+mach_int fast_signed(const fbits op, const uint64_t n)
+{
+  if (op & (UINT64_C(1) << (n - 1))) {
+    uint64_t rop = op & ~(UINT64_C(1) << (n - 1));
+    return (mach_int) (rop - (UINT64_C(1) << (n - 1)));
+  } else {
+    return (mach_int) op;
+  }
+}
+
 void append(lbits *rop, const lbits op1, const lbits op2)
 {
   rop->len = op1.len + op2.len;
@@ -911,6 +951,23 @@ void vector_update_subrange_lbits(lbits *rop,
   }
 }
 
+fbits fast_update_subrange(const fbits op,
+			   const mach_int n,
+			   const mach_int m,
+			   const fbits slice)
+{
+  fbits rop = op;
+  for (mach_int i = 0; i < n - (m - UINT64_C(1)); i++) {
+    uint64_t bit = UINT64_C(1) << ((uint64_t) i);
+    if (slice & bit) {
+      rop |= (bit << m);
+    } else {
+      rop &= ~(bit << m);
+    }
+  }
+  return rop;
+}
+
 void slice(lbits *rop, const lbits op, const sail_int start_mpz, const sail_int len_mpz)
 {
   assert(mpz_get_ui(start_mpz) + mpz_get_ui(len_mpz) <= op.len);
diff --git a/lib/sail.h b/lib/sail.h
index 8f113339..d5597a64 100644
--- a/lib/sail.h
+++ b/lib/sail.h
@@ -246,7 +246,10 @@ void mult_vec(lbits *rop, const lbits op1, const lbits op2);
 void zeros(lbits *rop, const sail_int op);
 
 void zero_extend(lbits *rop, const lbits op, const sail_int len);
+fbits fast_zero_extend(const sbits op, const uint64_t n);
 void sign_extend(lbits *rop, const lbits op, const sail_int len);
+fbits fast_sign_extend(const fbits op, const uint64_t n, const uint64_t m);
+fbits fast_sign_extend2(const sbits op, const uint64_t m);
 
 void length_lbits(sail_int *rop, const lbits op);
 
@@ -267,6 +270,7 @@ fbits bitvector_access(const lbits op, const sail_int n_mpz);
 void sail_unsigned(sail_int *rop, const lbits op);
 void sail_signed(sail_int *rop, const lbits op);
 
+mach_int fast_signed(const fbits, const uint64_t);
 mach_int fast_unsigned(const fbits);
 
 void append(lbits *rop, const lbits op1, const lbits op2);
@@ -292,6 +296,11 @@ void vector_update_subrange_lbits(lbits *rop,
 				      const sail_int m_mpz,
 				      const lbits slice);
 
+fbits fast_update_subrange(const fbits op,
+			   const mach_int n,
+			   const mach_int m,
+			   const fbits slice);
+
 void slice(lbits *rop, const lbits op, const sail_int start_mpz, const sail_int len_mpz);
 
 sbits sslice(const fbits op, const mach_int start, const mach_int len);
diff --git a/src/c_backend.ml b/src/c_backend.ml
index ab388223..d14b5391 100644
--- a/src/c_backend.ml
+++ b/src/c_backend.ml
@@ -174,6 +174,7 @@ let rec ctyp_of_typ ctx typ =
      begin match destruct_range Env.empty typ with
      | None -> assert false (* Checked if range type in guard *)
      | Some (kids, constr, n, m) ->
+        let ctx = { ctx with local_env = add_existential Parse_ast.Unknown (List.map (mk_kopt K_int) kids) constr ctx.local_env } in
         match nexp_simp n, nexp_simp m with
         | Nexp_aux (Nexp_constant n, _), Nexp_aux (Nexp_constant m, _)
              when Big_int.less_equal (min_int 64) n && Big_int.less_equal m (max_int 64) ->
@@ -483,6 +484,38 @@ let analyze_primop' ctx id args typ =
      | _ -> no_change
      end
 
+  | "zero_extend", [AV_C_fragment (v1, _, CT_fbits _); _] ->
+     begin match destruct_vector ctx.tc_env typ with
+     | Some (Nexp_aux (Nexp_constant n, _), _, Typ_aux (Typ_id id, _))
+          when string_of_id id = "bit" && Big_int.less_equal n (Big_int.of_int 64) ->
+        AE_val (AV_C_fragment (v1, typ, CT_fbits (Big_int.to_int n, true)))
+     | _ -> no_change
+     end
+
+  | "zero_extend", [AV_C_fragment (v1, _, CT_sbits _); _] ->
+     begin match destruct_vector ctx.tc_env typ with
+     | Some (Nexp_aux (Nexp_constant n, _), _, Typ_aux (Typ_id id, _))
+          when string_of_id id = "bit" && Big_int.less_equal n (Big_int.of_int 64) ->
+        AE_val (AV_C_fragment (F_call ("fast_zero_extend", [v1; v_int (Big_int.to_int n)]), typ, CT_fbits (Big_int.to_int n, true)))
+     | _ -> no_change
+     end
+    
+  | "sign_extend", [AV_C_fragment (v1, _, CT_fbits (n, _)); _] ->
+     begin match destruct_vector ctx.tc_env typ with
+     | Some (Nexp_aux (Nexp_constant m, _), _, Typ_aux (Typ_id id, _))
+          when string_of_id id = "bit" && Big_int.less_equal m (Big_int.of_int 64) ->
+        AE_val (AV_C_fragment (F_call ("fast_sign_extend", [v1; v_int n; v_int (Big_int.to_int m)]) , typ, CT_fbits (Big_int.to_int m, true)))
+     | _ -> no_change
+     end
+
+  | "sign_extend", [AV_C_fragment (v1, _, CT_sbits _); _] ->
+     begin match destruct_vector ctx.tc_env typ with
+     | Some (Nexp_aux (Nexp_constant m, _), _, Typ_aux (Typ_id id, _))
+          when string_of_id id = "bit" && Big_int.less_equal m (Big_int.of_int 64) ->
+        AE_val (AV_C_fragment (F_call ("fast_sign_extend2", [v1; v_int (Big_int.to_int m)]) , typ, CT_fbits (Big_int.to_int m, true)))
+     | _ -> no_change
+     end
+    
   | "gteq", [AV_C_fragment (v1, _, _); AV_C_fragment (v2, _, _)] ->
      AE_val (AV_C_fragment (F_op (v1, ">=", v2), typ, CT_bool))
 
@@ -568,6 +601,14 @@ let analyze_primop' ctx id args typ =
      | _ -> no_change
      end
 
+  | "sail_signed", [AV_C_fragment (frag, vtyp, _)] ->
+     begin match destruct_vector ctx.tc_env vtyp with
+     | Some (Nexp_aux (Nexp_constant n, _), _, _)
+          when Big_int.less_equal n (Big_int.of_int 64) && is_stack_typ ctx typ ->
+        AE_val (AV_C_fragment (F_call ("fast_signed", [frag; v_int (Big_int.to_int n)]), typ, ctyp_of_typ ctx typ))
+     | _ -> no_change
+     end
+    
   | "add_int", [AV_C_fragment (op1, _, _); AV_C_fragment (op2, _, _)] ->
      begin match destruct_range Env.empty typ with
      | None -> no_change
@@ -592,6 +633,12 @@ let analyze_primop' ctx id args typ =
      | _ -> no_change
      end
 
+  | "vector_update_subrange", [AV_C_fragment (xs, _, CT_fbits (n, true));
+                               AV_C_fragment (hi, _, CT_fint 64);
+                               AV_C_fragment (lo, _, CT_fint 64);
+                               AV_C_fragment (ys, _, CT_fbits (m, true))] ->
+     AE_val (AV_C_fragment (F_call ("fast_update_subrange", [xs; hi; lo; ys]), typ, CT_fbits (n, true)))
+     
   | "undefined_bool", _ ->
      AE_val (AV_C_fragment (F_lit (V_bool false), typ, CT_bool))
 
diff --git a/src/sail.ml b/src/sail.ml
index 2a15f26e..eb81a0ee 100644
--- a/src/sail.ml
+++ b/src/sail.ml
@@ -67,6 +67,7 @@ let opt_print_cgen = ref false
 let opt_memo_z3 = ref false
 let opt_sanity = ref false
 let opt_includes_c = ref ([]:string list)
+let opt_specialize_c = ref false
 let opt_libs_lem = ref ([]:string list)
 let opt_libs_coq = ref ([]:string list)
 let opt_file_arguments = ref ([]:string list)
@@ -151,6 +152,9 @@ let options = Arg.align ([
   ( "-c_extra_args",
     Arg.String (fun args -> C_backend.opt_extra_arguments := Some args),
     "<arguments> supply extra argument to every generated C function call" );
+  ( "-c_specialize",
+    Arg.Set opt_specialize_c,
+    " specialize integer arguments in C output");
   ( "-elf",
     Arg.String (fun elf -> opt_process_elf := Some elf),
     " process an ELF file so that it can be executed by compiled C code");
@@ -422,7 +426,12 @@ let main() =
        then
          let ast_c = rewrite_ast_c type_envs ast in
          let ast_c, type_envs = Specialize.(specialize typ_ord_specialization ast_c type_envs) in
-         (* let ast_c, type_envs = Specialize.(specialize' 2 int_specialization_with_externs ast_c type_envs) in *)
+         let ast_c, type_envs =
+           if !opt_specialize_c then
+             Specialize.(specialize' 2 int_specialization ast_c type_envs)
+           else
+             ast_c, type_envs
+         in
          let output_chan = match !opt_file_out with Some f -> open_out (f ^ ".c") | None -> stdout in
          Util.opt_warnings := true;
          C_backend.compile_ast (C_backend.initial_ctx type_envs) output_chan (!opt_includes_c) ast_c;
diff --git a/src/specialize.ml b/src/specialize.ml
index 19c5df7a..a487fc2f 100644
--- a/src/specialize.ml
+++ b/src/specialize.ml
@@ -52,6 +52,8 @@ open Ast
 open Ast_util
 open Rewriter
 
+let opt_ddump_spec_ast = ref None
+   
 let is_typ_ord_arg = function
   | A_aux (A_typ _, _) -> true
   | A_aux (A_order _, _) -> true
@@ -565,6 +567,15 @@ let specialize_ids spec ids ast =
       (1, ast) (IdSet.elements ids)
   in
   let ast = reorder_typedefs ast in
+  begin match !opt_ddump_spec_ast with
+  | Some (f, i) ->
+     let filename = f ^ "_spec_" ^ string_of_int i ^ ".sail" in
+     let out_chan = open_out filename in
+     Pretty_print_sail.pp_defs out_chan ast;
+     close_out out_chan;
+     opt_ddump_spec_ast := Some (f, i + 1)
+  | None -> ()
+  end;
   let ast, _ = Type_error.check Type_check.initial_env ast in
   let ast =
     List.fold_left (fun ast id -> rewrite_polymorphic_calls spec id ast) ast (IdSet.elements ids)
diff --git a/test/c/extend_simple.expect b/test/c/extend_simple.expect
new file mode 100644
index 00000000..3a652eaf
--- /dev/null
+++ b/test/c/extend_simple.expect
@@ -0,0 +1,2 @@
+x = 0xFFFFFFFF
+y = 0x00000000FFFFFFFF
diff --git a/test/c/extend_simple.sail b/test/c/extend_simple.sail
new file mode 100644
index 00000000..23f14235
--- /dev/null
+++ b/test/c/extend_simple.sail
@@ -0,0 +1,10 @@
+default Order dec
+
+$include <prelude.sail>
+
+function main((): unit) -> unit = {
+  let x = sail_sign_extend(0xFF, 32);
+  let y = sail_zero_extend(x, 64);
+  print_bits("x = ", x);
+  print_bits("y = ", y)
+}
\ No newline at end of file
diff --git a/test/c/fast_signed.expect b/test/c/fast_signed.expect
new file mode 100644
index 00000000..9fcfea23
--- /dev/null
+++ b/test/c/fast_signed.expect
@@ -0,0 +1,12 @@
+x = -1
+y = -1
+z = -1
+w = -1
+x = -128
+y = -32768
+z = -9223372036854775808
+w = -170141183460469231731687303715884105728
+x = 127
+y = 32767
+z = 9223372036854775807
+w = 170141183460469231731687303715884105727
diff --git a/test/c/fast_signed.sail b/test/c/fast_signed.sail
new file mode 100644
index 00000000..b0f16f89
--- /dev/null
+++ b/test/c/fast_signed.sail
@@ -0,0 +1,30 @@
+default Order dec
+
+$include <prelude.sail>
+
+function main((): unit) -> unit = {
+  let x = signed(0xFF);
+  let y = signed(0xFFFF);
+  let z = signed(0xFFFFFFFF_FFFFFFFF);
+  let w = signed(0xFFFFFFFF_FFFFFFFF_FFFFFFFF_FFFFFFFF);
+  print_int("x = ", x);
+  print_int("y = ", y);
+  print_int("z = ", z);
+  print_int("w = ", w);
+  let x = signed(0x80);
+  let y = signed(0x8000);
+  let z = signed(0x80000000_00000000);
+  let w = signed(0x80000000_00000000_00000000_00000000);
+  print_int("x = ", x);
+  print_int("y = ", y);
+  print_int("z = ", z);
+  print_int("w = ", w);
+  let x = signed(0x7F);
+  let y = signed(0x7FFF);
+  let z = signed(0x7FFFFFFF_FFFFFFFF);
+  let w = signed(0x7FFFFFFF_FFFFFFFF_FFFFFFFF_FFFFFFFF);
+  print_int("x = ", x);
+  print_int("y = ", y);
+  print_int("z = ", z);
+  print_int("w = ", w);
+}
\ No newline at end of file