Add missing builtins needed for cheri128 C. Still doesn't build possibly due to code gen issue.

3 files changed, 18 insertions, 2 deletions

diff --git a/lib/sail.c b/lib/sail.c
index 4cb9cdc1..38c8c273 100644
--- a/lib/sail.c
+++ b/lib/sail.c
@@ -781,6 +781,19 @@ void shift_bits_right_arith(sail_bits *rop, const sail_bits op1, const sail_bits
   }
 }
 
+void shiftl(sail_bits *rop, const sail_bits op1, const sail_int op2)
+{
+  rop->len = op1.len;
+  mpz_mul_2exp(*rop->bits, *op1.bits, mpz_get_ui(op2));
+  normalize_sail_bits(rop);
+}
+
+void shiftr(sail_bits *rop, const sail_bits op1, const sail_int op2)
+{
+  rop->len = op1.len;
+  mpz_tdiv_q_2exp(*rop->bits, *op1.bits, mpz_get_ui(op2));
+}
+
 void reverse_endianness(sail_bits *rop, const sail_bits op)
 {
   rop->len = op.len;
diff --git a/lib/sail.h b/lib/sail.h
index bbdccd09..9ce3ec6b 100644
--- a/lib/sail.h
+++ b/lib/sail.h
@@ -273,6 +273,9 @@ void shift_bits_left(sail_bits *rop, const sail_bits op1, const sail_bits op2);
 void shift_bits_right(sail_bits *rop, const sail_bits op1, const sail_bits op2);
 void shift_bits_right_arith(sail_bits *rop, const sail_bits op1, const sail_bits op2);
 
+void shiftl(sail_bits *rop, const sail_bits op1, const sail_int op2);
+void shiftr(sail_bits *rop, const sail_bits op1, const sail_int op2);
+
 void reverse_endianness(sail_bits*, sail_bits);
 
 /* ***** Sail reals ***** */
diff --git a/mips/prelude.sail b/mips/prelude.sail
index 85060dda..4c77d522 100644
--- a/mips/prelude.sail
+++ b/mips/prelude.sail
@@ -116,9 +116,9 @@ val max_nat = {lem: "max", coq: "Z.max", _: "max_int"} : (nat, nat) -> nat
 
 val max_int = {lem: "max", coq: "Z.max", _: "max_int"} : (int, int) -> int
 
-val min_atom = {ocaml: "min_int", lem: "min", coq: "min_atom"} : forall 'a 'b . (atom('a), atom('b)) -> {'c, ('c = 'a | 'c = 'b) & 'c <= 'a & 'c <= 'b . atom('c)}
+val min_atom = {ocaml: "min_int", lem: "min", coq: "min_atom", c:"min_int"} : forall 'a 'b . (atom('a), atom('b)) -> {'c, ('c = 'a | 'c = 'b) & 'c <= 'a & 'c <= 'b . atom('c)}
 
-val max_atom = {ocaml: "max_int", lem: "max", coq: "max_atom"} : forall 'a 'b . (atom('a), atom('b)) -> {'c, ('c = 'a | 'c = 'b) & 'c >= 'a & 'c >= 'b . atom('c)}
+val max_atom = {ocaml: "max_int", lem: "max", coq: "max_atom", c:"max_int"} : forall 'a 'b . (atom('a), atom('b)) -> {'c, ('c = 'a | 'c = 'b) & 'c >= 'a & 'c >= 'b . atom('c)}
 
 overload min = {min_atom, min_nat, min_int}