From 084fb032de3495671d557e31dbc55dc8400f9d81 Mon Sep 17 00:00:00 2001
From: Alasdair
Date: Thu, 21 Feb 2019 23:15:15 +0000
Subject: Allow monomorphisation with C generation

Run C tests with -O -Oconstant_fold -auto_mono
---
 lib/sail.c          | 14 +++++++++++++-
 lib/sail.h          |  3 +++
 src/c_backend.ml    |  2 ++
 src/rewrites.ml     | 11 +++++++++++
 test/c/run_tests.py |  1 +
 5 files changed, 30 insertions(+), 1 deletion(-)

diff --git a/lib/sail.c b/lib/sail.c
index 22cc5462..5c83690d 100644
--- a/lib/sail.c
+++ b/lib/sail.c
@@ -1460,7 +1460,8 @@ void get_time_ns(sail_int *rop, const unit u)
 
 // ARM specific optimisations
 
-void arm_align(lbits *rop, const lbits x_bv, const sail_int y_mpz) {
+void arm_align(lbits *rop, const lbits x_bv, const sail_int y_mpz)
+{
   uint64_t x = mpz_get_ui(*x_bv.bits);
   uint64_t y = mpz_get_ui(y_mpz);
   uint64_t z = y * (x / y);
@@ -1468,3 +1469,14 @@ void arm_align(lbits *rop, const lbits x_bv, const sail_int y_mpz) {
   mpz_set_ui(*rop->bits, safe_rshift(UINT64_MAX, 64l - (n - 1)) & z);
   rop->len = n;
 }
+
+// Monomorphisation
+void make_the_value(sail_int *rop, const sail_int op)
+{
+  mpz_set(*rop, op);
+}
+
+void size_itself_int(sail_int *rop, const sail_int op)
+{
+  mpz_set(*rop, op);
+}
diff --git a/lib/sail.h b/lib/sail.h
index 4225a3d4..8f113339 100644
--- a/lib/sail.h
+++ b/lib/sail.h
@@ -153,6 +153,9 @@ SAIL_INT_FUNCTION(pow_int, sail_int, const sail_int, const sail_int);
 
 SAIL_INT_FUNCTION(pow2, sail_int, const sail_int);
 
+void make_the_value(sail_int *, const sail_int);
+void size_itself_int(sail_int *, const sail_int);
+
 /* ***** Sail bitvectors ***** */
 
 typedef uint64_t fbits;
diff --git a/src/c_backend.ml b/src/c_backend.ml
index fd728111..3b289572 100644
--- a/src/c_backend.ml
+++ b/src/c_backend.ml
@@ -143,6 +143,8 @@ let rec ctyp_of_typ ctx typ =
 
   | Typ_app (id, _) when string_of_id id = "atom_bool" -> CT_bool
 
+  | Typ_app (id, args) when string_of_id id = "itself" ->
+     ctyp_of_typ ctx (Typ_aux (Typ_app (mk_id "atom", args), l))
   | Typ_app (id, _) when string_of_id id = "range" || string_of_id id = "atom" || string_of_id id = "implicit" ->
      begin match destruct_range Env.empty typ with
      | None -> assert false (* Checked if range type in guard *)
diff --git a/src/rewrites.ml b/src/rewrites.ml
index c78c9aee..f14d423c 100644
--- a/src/rewrites.ml
+++ b/src/rewrites.ml
@@ -5172,10 +5172,21 @@ let rewrite_defs_ocaml = [
 
 let rewrite_defs_c = [
   ("no_effect_check", (fun _ defs -> opt_no_effects := true; defs));
+
+  (* Remove bidirectional mappings *)
   ("realise_mappings", rewrite_defs_realise_mappings);
   ("toplevel_string_append", rewrite_defs_toplevel_string_append);
   ("pat_string_append", rewrite_defs_pat_string_append);
   ("mapping_builtins", rewrite_defs_mapping_patterns);
+
+  (* Monomorphisation *)
+  ("mono_rewrites", if_mono mono_rewrites);
+  ("recheck_defs", if_mono recheck_defs);
+  ("rewrite_toplevel_nexps", if_mono rewrite_toplevel_nexps);
+  ("monomorphise", if_mono monomorphise);
+  ("rewrite_atoms_to_singletons", if_mono (fun _ -> Monomorphise.rewrite_atoms_to_singletons));
+  ("recheck_defs", if_mono recheck_defs);
+
   ("rewrite_undefined", rewrite_undefined_if_gen false);
   ("rewrite_defs_vector_string_pats_to_bit_list", rewrite_defs_vector_string_pats_to_bit_list);
   ("remove_not_pats", rewrite_defs_not_pats);
diff --git a/test/c/run_tests.py b/test/c/run_tests.py
index 4927e281..4a02dd78 100755
--- a/test/c/run_tests.py
+++ b/test/c/run_tests.py
@@ -93,6 +93,7 @@ xml = '<testsuites>\n'
 xml += test_c('unoptimized C', '', '', True)
 xml += test_c('optimized C', '-O2', '-O', True)
 xml += test_c('constant folding', '', '-Oconstant_fold', True)
+xml += test_c('monomorphised C', '-O2', '-O -Oconstant_fold -auto_mono', True)
 xml += test_c('full optimizations', '-O2 -mbmi2 -DINTRINSICS', '-O -Oconstant_fold', True)
 xml += test_c('address sanitised', '-O2 -fsanitize=undefined', '-O', False)
 
-- 
cgit v1.2.3