Merge branch 'sail2' into rmem_interpreter

7 files changed, 134 insertions, 24 deletions

diff --git a/lib/coq/Sail2_string.v b/lib/coq/Sail2_string.v
index 543b0fad..a0a23933 100644
--- a/lib/coq/Sail2_string.v
+++ b/lib/coq/Sail2_string.v
@@ -1,4 +1,5 @@
 Require Import Sail2_values.
+Require Import Coq.Strings.Ascii.
 
 Definition string_sub (s : string) (start : Z) (len : Z) : string :=
   String.substring (Z.to_nat start) (Z.to_nat len) s.
diff --git a/lib/coq/Sail2_values.v b/lib/coq/Sail2_values.v
index e6c5e786..f11e057a 100644
--- a/lib/coq/Sail2_values.v
+++ b/lib/coq/Sail2_values.v
@@ -10,6 +10,7 @@ Require Export Sumbool.
 Require Export DecidableClass.
 Require Import Eqdep_dec.
 Require Export Zeuclid.
+Require Import Psatz.
 Import ListNotations.
 
 Open Scope Z.
@@ -1037,27 +1038,31 @@ Ltac unbool_comparisons :=
   | H:context [generic_eq _ _ = false] |- _ => apply generic_eq_false in H
   | H:context [generic_neq _ _ = true] |- _ => apply generic_neq_true in H
   | H:context [generic_neq _ _ = false] |- _ => apply generic_neq_false in H
+  | H:context [_ <> true] |- _ => rewrite Bool.not_true_iff_false in H
+  | H:context [_ <> false] |- _ => rewrite Bool.not_false_iff_true in H
   end.
 Ltac unbool_comparisons_goal :=
   repeat match goal with
-  | |- context [Z.geb _ _] => rewrite Z.geb_leb
-  | |- context [Z.gtb _ _] => rewrite Z.gtb_ltb
-  | |- context [Z.leb _ _ = true] => rewrite Z.leb_le
-  | |- context [Z.ltb _ _ = true] => rewrite Z.ltb_lt
-  | |- context [Z.eqb _ _ = true] => rewrite Z.eqb_eq
-  | |- context [Z.leb _ _ = false] => rewrite Z.leb_gt
-  | |- context [Z.ltb _ _ = false] => rewrite Z.ltb_ge
-  | |- context [Z.eqb _ _ = false] => rewrite Z.eqb_neq
-  | |- context [orb _ _ = true] => rewrite Bool.orb_true_iff
-  | |- context [orb _ _ = false] => rewrite Bool.orb_false_iff
-  | |- context [andb _ _ = true] => rewrite Bool.andb_true_iff
-  | |- context [andb _ _ = false] => rewrite Bool.andb_false_iff
-  | |- context [negb _ = true] => rewrite Bool.negb_true_iff
-  | |- context [negb _ = false] => rewrite Bool.negb_false_iff
+  | |- context [Z.geb _ _] => setoid_rewrite Z.geb_leb
+  | |- context [Z.gtb _ _] => setoid_rewrite Z.gtb_ltb
+  | |- context [Z.leb _ _ = true] => setoid_rewrite Z.leb_le
+  | |- context [Z.ltb _ _ = true] => setoid_rewrite Z.ltb_lt
+  | |- context [Z.eqb _ _ = true] => setoid_rewrite Z.eqb_eq
+  | |- context [Z.leb _ _ = false] => setoid_rewrite Z.leb_gt
+  | |- context [Z.ltb _ _ = false] => setoid_rewrite Z.ltb_ge
+  | |- context [Z.eqb _ _ = false] => setoid_rewrite Z.eqb_neq
+  | |- context [orb _ _ = true] => setoid_rewrite Bool.orb_true_iff
+  | |- context [orb _ _ = false] => setoid_rewrite Bool.orb_false_iff
+  | |- context [andb _ _ = true] => setoid_rewrite Bool.andb_true_iff
+  | |- context [andb _ _ = false] => setoid_rewrite Bool.andb_false_iff
+  | |- context [negb _ = true] => setoid_rewrite Bool.negb_true_iff
+  | |- context [negb _ = false] => setoid_rewrite Bool.negb_false_iff
   | |- context [generic_eq _ _ = true] => apply generic_eq_true
   | |- context [generic_eq _ _ = false] => apply generic_eq_false
   | |- context [generic_neq _ _ = true] => apply generic_neq_true
   | |- context [generic_neq _ _ = false] => apply generic_neq_false
+  | |- context [_ <> true] => rewrite Bool.not_true_iff_false
+  | |- context [_ <> false] => rewrite Bool.not_false_iff_true
   end.
 
 (* Split up dependent pairs to get at proofs of properties *)
@@ -1190,6 +1195,13 @@ Ltac fill_in_evar_eq :=
    let y := eval cbn in y in*)
    idtac "Warning: unknown equality constraint"; constructor; exact (eq_refl _ : x = y) end.
 
+Ltac bruteforce_bool_exists :=
+match goal with
+| |- exists _ : bool,_ => solve [ exists true; bruteforce_bool_exists
+                                | exists false; bruteforce_bool_exists ]
+| _ => tauto
+end.
+
 Ltac solve_arithfact :=
 (* Attempt a simple proof first to avoid lengthy preparation steps (especially
    as the large proof terms can upset subsequent proofs). *)
@@ -1208,13 +1220,17 @@ prepare_for_solver;
  | constructor; eauto 3 with zarith sail
    (* The datatypes hints give us some list handling, esp In *)
  | constructor; drop_exists; eauto 3 with datatypes zarith sail
+ | match goal with |- context [Z.mul] => constructor; nia end
    (* Booleans - and_boolMP *)
- | match goal with |- ArithFact (forall l r:bool, _ -> _ -> exists _, _) => 
-     constructor; intros l r H1 H2;
-     solve [exists l; destruct l; intuition | exists r; destruct l; intuition]
+ | match goal with |- ArithFact (forall l r:bool, _ -> _ -> exists _ : bool, _) => 
+     constructor; intros [|] [|] H1 H2;
+     repeat match goal with H:?X = ?X -> _ |- _ => specialize (H eq_refl) end;
+     repeat match goal with H:@ex _ _ |- _ => destruct H end;
+     bruteforce_bool_exists
    end
- | match goal with |- context [@eq _ _ _] =>
-     constructor; intuition
+ | match goal with |- context [@eq bool _ _] =>
+     (* Don't use auto for the fallback to keep runtime down *)
+     firstorder fail
    end
  | constructor; idtac "Unable to solve constraint"; dump_context; fail
  ].
diff --git a/lib/mono_rewrites.sail b/lib/mono_rewrites.sail
index 90d74149..9e4010a0 100644
--- a/lib/mono_rewrites.sail
+++ b/lib/mono_rewrites.sail
@@ -119,9 +119,9 @@ function place_slice(m,xs,i,l,shift) = {
 }
 
 val set_slice_zeros : forall 'n, 'n >= 0.
-  (atom('n), int, bits('n), int) -> bits('n) effect pure
+  (atom('n), bits('n), int, int) -> bits('n) effect pure
 
-function set_slice_zeros(n, i, xs, l) = {
+function set_slice_zeros(n, xs, i, l) = {
   let ys : bits('n) = slice_mask(n, i, l) in
   xs & ~(ys)
 }
diff --git a/lib/regfp.sail b/lib/regfp.sail
index b2ecaa10..c191d654 100644
--- a/lib/regfp.sail
+++ b/lib/regfp.sail
@@ -93,6 +93,16 @@ enum trans_kind = {
   Transaction_abort
 }
 
+/* cache maintenance instructions */
+enum cache_op_kind = {
+  /* AArch64 DC */
+  Cache_op_D_IVAC, Cache_op_D_ISW,  Cache_op_D_CSW,  Cache_op_D_CISW,
+  Cache_op_D_ZVA,  Cache_op_D_CVAC, Cache_op_D_CVAU, Cache_op_D_CIVAC,
+  /* AArch64 IC */
+  Cache_op_I_IALLUIS, Cache_op_I_IALLU, Cache_op_I_IVAU
+}
+
+
 union instruction_kind = {
   IK_barrier : barrier_kind,
   IK_mem_read : read_kind,
@@ -100,7 +110,8 @@ union instruction_kind = {
   IK_mem_rmw : (read_kind, write_kind),
   IK_branch : unit,
   IK_trans : trans_kind,
-  IK_simple : unit
+  IK_simple : unit,
+  IK_cache_op : cache_op_kind
 }
 
 val __read_mem
diff --git a/lib/sail.c b/lib/sail.c
index 5c83690d..6c71d7ae 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;
@@ -890,6 +930,20 @@ void set_slice_int(sail_int *rop,
   }
 }
 
+void update_lbits(lbits *rop, const lbits op, const sail_int n_mpz, const uint64_t bit)
+{
+  uint64_t n = mpz_get_ui(n_mpz);
+
+  mpz_set(*rop->bits, *op.bits);
+  rop->len = op.len;
+
+  if (bit == UINT64_C(0)) {
+    mpz_clrbit(*rop->bits, n);
+  } else {
+    mpz_setbit(*rop->bits, n);
+  }
+}
+
 void vector_update_subrange_lbits(lbits *rop,
 				 const lbits op,
 				 const sail_int n_mpz,
@@ -911,6 +965,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 42f87294..e06629f0 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);
@@ -286,12 +290,19 @@ void set_slice_int(sail_int *rop,
 		   const sail_int start_mpz,
 		   const lbits slice);
 
+void update_lbits(lbits *rop, const lbits op, const sail_int n_mpz, const uint64_t bit);
+
 void vector_update_subrange_lbits(lbits *rop,
 				      const lbits op,
 				      const sail_int n_mpz,
 				      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/lib/string.sail b/lib/string.sail
index 9c4ad2f6..3fe74eb5 100644
--- a/lib/string.sail
+++ b/lib/string.sail
@@ -3,7 +3,7 @@ $define _STRING
 
 $include <arith.sail>
 
-val eq_string = {lem: "eq", _: "eq_string"} : (string, string) -> bool
+val eq_string = {lem: "eq", coq: "generic_eq", _: "eq_string"} : (string, string) -> bool
 
 infixl 9 ^-^