Fixes for full v8.5

4 files changed, 12 insertions, 5 deletions

diff --git a/lib/arith.sail b/lib/arith.sail
index a3a80fc5..b233048e 100644
--- a/lib/arith.sail
+++ b/lib/arith.sail
@@ -70,7 +70,11 @@ val _shl_int = "shl_int" : (int, int) -> int
 
 overload shl_int = {_shl8, _shl32, _shl_int}
 
-val shr_int = "shr_int" : (int, int) -> int
+val _shr32 = {c: "shr_mach_int", _: "shr_int"} : forall 'n, 0 <= 'n <= 31. (int('n), int(1)) -> {'m, 0 <= 'm <= 15. int('m)}
+
+val _shr_int = "shr_int" : (int, int) -> int
+
+overload shr_int = {_shr32, _shr_int}
 
 // ***** div and mod *****
 
diff --git a/lib/sail.c b/lib/sail.c
index 0fcb5d55..22cc5462 100644
--- a/lib/sail.c
+++ b/lib/sail.c
@@ -292,24 +292,26 @@ bool gteq(const mpz_t op1, const mpz_t op2)
   return mpz_cmp(op1, op2) >= 0;
 }
 
-inline
 void shl_int(sail_int *rop, const sail_int op1, const sail_int op2)
 {
   mpz_mul_2exp(*rop, op1, mpz_get_ui(op2));
 }
 
-inline
 mach_int shl_mach_int(const mach_int op1, const mach_int op2)
 {
   return op1 << op2;
 }
 
-inline
 void shr_int(sail_int *rop, const sail_int op1, const sail_int op2)
 {
   mpz_fdiv_q_2exp(*rop, op1, mpz_get_ui(op2));
 }
 
+mach_int shr_mach_int(const mach_int op1, const mach_int op2)
+{
+  return op1 >> op2;
+}
+
 inline
 void undefined_int(sail_int *rop, const int n)
 {
diff --git a/lib/sail.h b/lib/sail.h
index 53b9c6be..4225a3d4 100644
--- a/lib/sail.h
+++ b/lib/sail.h
@@ -116,6 +116,7 @@ bool gteq(const sail_int, const sail_int);
  * Left and right shift for integers
  */
 mach_int shl_mach_int(const mach_int, const mach_int);
+mach_int shr_mach_int(const mach_int, const mach_int);
 SAIL_INT_FUNCTION(shl_int, sail_int, const sail_int, const sail_int);
 SAIL_INT_FUNCTION(shr_int, sail_int, const sail_int, const sail_int);
 
diff --git a/src/sail.ml b/src/sail.ml
index 41aee119..58b224f2 100644
--- a/src/sail.ml
+++ b/src/sail.ml
@@ -400,7 +400,7 @@ let main() =
        then
          let ast_c = rewrite_ast_c ast in
          let ast_c, type_envs = Specialize.specialize ast_c type_envs in
-         let ast_c = Spec_analysis.top_sort_defs ast_c in
+         (* let ast_c = Spec_analysis.top_sort_defs ast_c in *)
          Util.opt_warnings := true;
          C_backend.compile_ast (C_backend.initial_ctx type_envs) (!opt_includes_c) ast_c
        else ());