From 8718a39778d4c673ceea1c7f9bb219b29788ebae Mon Sep 17 00:00:00 2001
From: Alasdair
Date: Tue, 5 Mar 2019 03:09:16 +0000
Subject: Additional optimizations for C compilation

---
 lib/sail.c | 59 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++-
 lib/sail.h |  9 +++++++++
 2 files changed, 67 insertions(+), 1 deletion(-)

(limited to 'lib')

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);
-- 
cgit v1.2.3


From 361458ae5dbe8414b5a7ba1bc51ece8ebcfd5bc5 Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Tue, 5 Mar 2019 10:38:55 +0000
Subject: Coq 8.9 compatibility fix

---
 lib/coq/Sail2_string.v | 1 +
 1 file changed, 1 insertion(+)

(limited to 'lib')

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.
-- 
cgit v1.2.3


From 701b188b6f17d9f54480654e5959c606a8947c88 Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Tue, 5 Mar 2019 12:17:49 +0000
Subject: Coq: use setoid rewriting to apply under an existential binder

---
 lib/coq/Sail2_values.v | 28 ++++++++++++++--------------
 1 file changed, 14 insertions(+), 14 deletions(-)

(limited to 'lib')

diff --git a/lib/coq/Sail2_values.v b/lib/coq/Sail2_values.v
index e6c5e786..ba94a237 100644
--- a/lib/coq/Sail2_values.v
+++ b/lib/coq/Sail2_values.v
@@ -1040,20 +1040,20 @@ Ltac unbool_comparisons :=
   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
-- 
cgit v1.2.3


From 98f447e1ca70999350dac4b7a0d3fbce5c64071b Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Tue, 5 Mar 2019 15:13:15 +0000
Subject: Coq: firstorder is better at the boolean goals

---
 lib/coq/Sail2_values.v | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'lib')

diff --git a/lib/coq/Sail2_values.v b/lib/coq/Sail2_values.v
index ba94a237..fa40e01a 100644
--- a/lib/coq/Sail2_values.v
+++ b/lib/coq/Sail2_values.v
@@ -1213,8 +1213,9 @@ prepare_for_solver;
      constructor; intros l r H1 H2;
      solve [exists l; destruct l; intuition | exists r; destruct l; intuition]
    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
  ].
-- 
cgit v1.2.3


From e2ba378d45b0072d22ae0e63c0437fd22b25c361 Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Thu, 7 Mar 2019 11:59:18 +0000
Subject: Coq: apply a little brute force in some boolean goals

---
 lib/coq/Sail2_values.v | 12 +++++++++---
 1 file changed, 9 insertions(+), 3 deletions(-)

(limited to 'lib')

diff --git a/lib/coq/Sail2_values.v b/lib/coq/Sail2_values.v
index fa40e01a..10571412 100644
--- a/lib/coq/Sail2_values.v
+++ b/lib/coq/Sail2_values.v
@@ -1190,6 +1190,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). *)
@@ -1209,9 +1216,8 @@ prepare_for_solver;
    (* The datatypes hints give us some list handling, esp In *)
  | constructor; drop_exists; eauto 3 with datatypes zarith sail
    (* 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; bruteforce_bool_exists
    end
  | match goal with |- context [@eq bool _ _] =>
      (* Don't use auto for the fallback to keep runtime down *)
-- 
cgit v1.2.3


From e9d0335845cf2caffd4b4626bdedb02732fd8141 Mon Sep 17 00:00:00 2001
From: Thomas Bauereiss
Date: Thu, 7 Mar 2019 13:28:04 +0000
Subject: Fix bug in a mono rewrite helper function

---
 lib/mono_rewrites.sail | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'lib')

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)
 }
-- 
cgit v1.2.3


From 87ffe603e44e9be6f4109f6a9dd475df6dcfc489 Mon Sep 17 00:00:00 2001
From: Shaked Flur
Date: Fri, 8 Mar 2019 16:02:02 +0000
Subject: Adds the DC and IC instructions to AArch64_small; Also, removes
 etc/regfp.sail and etc/regfp2.sail in favour of lib/regfp.sail

---
 lib/regfp.sail | 13 ++++++++++++-
 1 file changed, 12 insertions(+), 1 deletion(-)

(limited to 'lib')

diff --git a/lib/regfp.sail b/lib/regfp.sail
index cc017585..6044e1cc 100644
--- a/lib/regfp.sail
+++ b/lib/regfp.sail
@@ -90,6 +90,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,
@@ -97,5 +107,6 @@ 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
 }
-- 
cgit v1.2.3


From 70bd4e69c0e520d46c65129a731714eb04ca6847 Mon Sep 17 00:00:00 2001
From: Prashanth Mundkur
Date: Fri, 8 Mar 2019 10:50:31 -0800
Subject: Fix the Coq mapping for eq_string in Sail lib.

---
 lib/string.sail | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'lib')

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 ^-^
 
-- 
cgit v1.2.3


From c3d10cdb1787077425e174fa638f1d43de7c797f Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Tue, 12 Mar 2019 11:09:33 +0000
Subject: Coq: fix some boolean issues seen in arm Fixes bad precedence issues,
 removes an out-of-date special case that's not necessary, and solves more
 goals.

---
 lib/coq/Sail2_values.v | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

(limited to 'lib')

diff --git a/lib/coq/Sail2_values.v b/lib/coq/Sail2_values.v
index 10571412..7db9d5aa 100644
--- a/lib/coq/Sail2_values.v
+++ b/lib/coq/Sail2_values.v
@@ -1037,6 +1037,8 @@ 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
@@ -1058,6 +1060,8 @@ Ltac unbool_comparisons_goal :=
   | |- 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 *)
@@ -1217,7 +1221,10 @@ prepare_for_solver;
  | constructor; drop_exists; eauto 3 with datatypes zarith sail
    (* Booleans - and_boolMP *)
  | match goal with |- ArithFact (forall l r:bool, _ -> _ -> exists _ : bool, _) => 
-     constructor; intros [|] [|] H1 H2; bruteforce_bool_exists
+     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 bool _ _] =>
      (* Don't use auto for the fallback to keep runtime down *)
-- 
cgit v1.2.3


From 8c56dcf65016c3669b24e2c5828b5588436e078d Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Tue, 12 Mar 2019 17:25:15 +0000
Subject: Coq: try non-linear nia solver too

---
 lib/coq/Sail2_values.v | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'lib')

diff --git a/lib/coq/Sail2_values.v b/lib/coq/Sail2_values.v
index 7db9d5aa..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.
@@ -1219,6 +1220,7 @@ 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 _ : bool, _) => 
      constructor; intros [|] [|] H1 H2;
-- 
cgit v1.2.3


From ee54fe8fc8a4afc8fb9f6cc0bd8e2930162f49ad Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Wed, 13 Mar 2019 14:25:00 +0000
Subject: C: Add missing update_lbits builtin

---
 lib/sail.c | 14 ++++++++++++++
 lib/sail.h |  2 ++
 2 files changed, 16 insertions(+)

(limited to 'lib')

diff --git a/lib/sail.c b/lib/sail.c
index c66c057c..6c71d7ae 100644
--- a/lib/sail.c
+++ b/lib/sail.c
@@ -930,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,
diff --git a/lib/sail.h b/lib/sail.h
index d5597a64..5a7722de 100644
--- a/lib/sail.h
+++ b/lib/sail.h
@@ -290,6 +290,8 @@ 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,
-- 
cgit v1.2.3