From 61e6bc97a7d5efb58f9b91738f1dd64404091137 Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Wed, 7 Nov 2018 18:40:57 +0000
Subject: Move inline forall in function definitions

* Previously we allowed the following bizarre syntax for a forall
  quantifier on a function:

  val foo(arg1: int('n), arg2: typ2) -> forall 'n, 'n >= 0. unit

  this commit changes this to the more sane:

  val foo forall 'n, 'n >= 2. (arg1: int('n), arg2: typ2) -> unit

  Having talked about it today, we could consider adding the syntax

  val foo where 'n >= 2. (arg1: int('n), arg2: typ2) -> unit

  which would avoid the forall (by implicitly quantifying variables in
  the constraint), and be slightly more friendly especially for
  documentation purposes. Only RISC-V used this syntax, so all uses of
  it there have been switched to the new style.

* Second, there is a new (somewhat experimental) syntax for
  existentials, that is hopefully more readable and closer to
  minisail:

  val foo(x: int, y: int) -> int('m) with 'm >= 2

  "type('n) with constraint" is equivalent to minisail: {'n: type | constraint}
  the type variables in typ are implicitly quantified, so this is equivalent to
  {'n, constraint. typ('n)}

  In order to make this syntax non-ambiguous we have to use == in
  constraints rather than =, but this is a good thing anyway because
  the previous situation where = was type level equality and == term
  level equality was confusing. Now all the type type-level and
  term-level operators can be consistent. However, to avoid breaking
  anything = is still allowed in non-with constraints, and produces a
  deprecated warning when parsed.
---
 lib/smt.sail | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'lib')

diff --git a/lib/smt.sail b/lib/smt.sail
index efcbe48c..c57f7bd1 100644
--- a/lib/smt.sail
+++ b/lib/smt.sail
@@ -9,7 +9,7 @@ val div = {
   lem: "integerDiv",
   c: "tdiv_int",
   coq: "div_with_eq"
-} : forall 'n 'm. (atom('n), atom('m)) -> {'o, 'o = div('n, 'm). atom('o)}
+} : forall 'n 'm. (atom('n), atom('m)) -> {'o, 'o == div('n, 'm). atom('o)}
 
 overload operator / = {div}
 
@@ -19,7 +19,7 @@ val mod = {
   lem: "integerMod",
   c: "tmod_int",
   coq: "mod_with_eq"
-} : forall 'n 'm. (atom('n), atom('m)) -> {'o, 'o = mod('n, 'm). atom('o)}
+} : forall 'n 'm. (atom('n), atom('m)) -> {'o, 'o == mod('n, 'm). atom('o)}
 
 overload operator % = {mod}
 
@@ -29,7 +29,7 @@ val abs_atom = {
   lem: "abs_int",
   c: "abs_int",
   coq: "abs_with_eq"
-} : forall 'n. atom('n) -> {'o, 'o = abs_atom('n). atom('o)}
+} : forall 'n. atom('n) -> {'o, 'o == abs_atom('n). atom('o)}
 
 $ifdef TEST
 
-- 
cgit v1.2.3


From e06619625300a3bbf275f1cae6b327b6447f6625 Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Wed, 7 Nov 2018 18:40:57 +0000
Subject: Move inline forall in function definitions

* Previously we allowed the following bizarre syntax for a forall
  quantifier on a function:

  val foo(arg1: int('n), arg2: typ2) -> forall 'n, 'n >= 0. unit

  this commit changes this to the more sane:

  val foo forall 'n, 'n >= 2. (arg1: int('n), arg2: typ2) -> unit

  Having talked about it today, we could consider adding the syntax

  val foo where 'n >= 2. (arg1: int('n), arg2: typ2) -> unit

  which would avoid the forall (by implicitly quantifying variables in
  the constraint), and be slightly more friendly especially for
  documentation purposes. Only RISC-V used this syntax, so all uses of
  it there have been switched to the new style.

* Second, there is a new (somewhat experimental) syntax for
  existentials, that is hopefully more readable and closer to
  minisail:

  val foo(x: int, y: int) -> int('m) with 'm >= 2

  "type('n) with constraint" is equivalent to minisail: {'n: type | constraint}
  the type variables in typ are implicitly quantified, so this is equivalent to
  {'n, constraint. typ('n)}

  In order to make this syntax non-ambiguous we have to use == in
  constraints rather than =, but this is a good thing anyway because
  the previous situation where = was type level equality and == term
  level equality was confusing. Now all the type type-level and
  term-level operators can be consistent. However, to avoid breaking
  anything = is still allowed in non-with constraints, and produces a
  deprecated warning when parsed.
---
 lib/smt.sail | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'lib')

diff --git a/lib/smt.sail b/lib/smt.sail
index efcbe48c..c57f7bd1 100644
--- a/lib/smt.sail
+++ b/lib/smt.sail
@@ -9,7 +9,7 @@ val div = {
   lem: "integerDiv",
   c: "tdiv_int",
   coq: "div_with_eq"
-} : forall 'n 'm. (atom('n), atom('m)) -> {'o, 'o = div('n, 'm). atom('o)}
+} : forall 'n 'm. (atom('n), atom('m)) -> {'o, 'o == div('n, 'm). atom('o)}
 
 overload operator / = {div}
 
@@ -19,7 +19,7 @@ val mod = {
   lem: "integerMod",
   c: "tmod_int",
   coq: "mod_with_eq"
-} : forall 'n 'm. (atom('n), atom('m)) -> {'o, 'o = mod('n, 'm). atom('o)}
+} : forall 'n 'm. (atom('n), atom('m)) -> {'o, 'o == mod('n, 'm). atom('o)}
 
 overload operator % = {mod}
 
@@ -29,7 +29,7 @@ val abs_atom = {
   lem: "abs_int",
   c: "abs_int",
   coq: "abs_with_eq"
-} : forall 'n. atom('n) -> {'o, 'o = abs_atom('n). atom('o)}
+} : forall 'n. atom('n) -> {'o, 'o == abs_atom('n). atom('o)}
 
 $ifdef TEST
 
-- 
cgit v1.2.3


From 953bfdd18c71bcd6c486aac74fe145104c3b2a4d Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Wed, 7 Nov 2018 18:56:28 +0000
Subject: Improvements to latex generation

The main changes so far are:

* Allow markdown formatting in doc comments. We parse the markdown
  using Omd, which is a OCaml library for parsing markdown. The nice
  thing about this library is it's pure OCaml and has no dependencies
  other the the stdlib. Incidentally it was also developed at OCaml
  labs. Using markdown keeps our doc-comments from becoming latex
  specfic, and having an actual parser is _much_ nicer than trying to
  hackily process latex in doc-comments using OCamls somewhat sub-par
  regex support.

* More sane conversion latex identifiers the main approach is to
  convert Sail identifiers to lowerCamelCase, replacing numbers with
  words, and then add a 'category' code based on the type of
  identifier, so for a function we'd have fnlowerCamelCase and for
  type synonym typelowerCamelCase etc. Because this transformation is
  non-injective we keep track of identifiers we've generated so we end
  up with identifierA, identifierB, identifierC when there are
  collisions.

* Because we parse markdown in doc comments doc comments can use Sail
  identifiers directly in hyperlinks, without having to care about how
  they are name-mangled down into TeX compatible things.

* Allow directives to be passed through the compiler to
  backends. There are various $latex directives that modify the latex
  output. Most usefully there's a

  $latex newcommand name markdown

  directive that uses the markdown parser to generate latex
  commands. An example of why this is useful is bellow. We can also use

  $latex noref id

  To suppress automatically inserting links to an identifier

* Refactor the latex generator to make the overall generation process
  cleaner

* Work around the fact that some operating systems consider
  case-sensitive file names to be a good thing

* Fix a bug where latex generation wouldn't occur unless the directory
  specified by -o didn't exist

This isn't quite all the requested features for good CHERI
documentation, but new features should be much easier to add now.
---
 lib/flow.sail       | 2 +-
 lib/vector_dec.sail | 2 --
 2 files changed, 1 insertion(+), 3 deletions(-)

(limited to 'lib')

diff --git a/lib/flow.sail b/lib/flow.sail
index 5ee9a74a..cdc6b2fd 100644
--- a/lib/flow.sail
+++ b/lib/flow.sail
@@ -11,7 +11,7 @@ therefore be included in just about every Sail specification.
 
 val eq_unit : (unit, unit) -> bool
 
-val "eq_bit" : (bit, bit) -> bool
+val eq_bit = { lem : "eq", _ : "eq_bit" } : (bit, bit) -> bool
 
 function eq_unit(_, _) = true
 
diff --git a/lib/vector_dec.sail b/lib/vector_dec.sail
index 8abcd218..37e10c2f 100644
--- a/lib/vector_dec.sail
+++ b/lib/vector_dec.sail
@@ -5,8 +5,6 @@ $include <flow.sail>
 
 type bits ('n : Int) = vector('n, dec, bit)
 
-val eq_bit = { lem : "eq", _ : "eq_bit" } : (bit, bit) -> bool
-
 val eq_bits = {
   ocaml: "eq_list",
   lem: "eq_vec",
-- 
cgit v1.2.3


From 60bcce4648ed029ca3c19c023f5ca525b43eced4 Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Tue, 13 Nov 2018 18:54:35 +0000
Subject: Make pretty printer stricter with brace placement

Also add a special case for shift-left when we are shifting 8 by a two
bit opcode, or 32 by a one bit opcode.
---
 lib/arith.sail | 20 +++++++++++++++++++-
 1 file changed, 19 insertions(+), 1 deletion(-)

(limited to 'lib')

diff --git a/lib/arith.sail b/lib/arith.sail
index 61a1ff76..e61ec473 100644
--- a/lib/arith.sail
+++ b/lib/arith.sail
@@ -50,7 +50,25 @@ val "prerr_int" : (string, int) -> unit
 
 // ***** Integer shifts *****
 
-val shl_int = "shl_int" : (int, int) -> int
+/*!
+A common idiom in asl is to take two bits of an opcode and convert in into a variable like
+```
+let elsize = shl_int(8, UInt(size))
+```
+THIS ensures that in this case the typechecker knows that the end result will be a value in the set `{8, 16, 32, 64}`
+*/
+val _shl8 = "shl_int" :
+  forall 'n, 0 <= 'n <= 3. (int(8), int('n)) -> int('m) with 'm in {8, 16, 32, 64}
+
+/*!
+Similarly, we can shift 32 by either 0 or 1 to get a value in `{32, 64}`
+*/
+val _shl32 = "shl_int" :
+  forall 'n, 'n in {0, 1}. (int(32), int('n)) -> int('m) with 'm in {32, 64}
+
+val _shl_int = "shl_int" : (int, int) -> int
+
+overload shl_int = {_shl8, _shl32, _shl_int}
 
 val shr_int = "shr_int" : (int, int) -> int
 
-- 
cgit v1.2.3


From 8c2739ace6ddc9b506d8e6782a4075574115cb34 Mon Sep 17 00:00:00 2001
From: Robert Norton
Date: Thu, 15 Nov 2018 17:13:47 +0000
Subject: document signed and unsigned

---
 lib/vector_dec.sail | 6 ++++++
 1 file changed, 6 insertions(+)

(limited to 'lib')

diff --git a/lib/vector_dec.sail b/lib/vector_dec.sail
index 37e10c2f..bfe1dae7 100644
--- a/lib/vector_dec.sail
+++ b/lib/vector_dec.sail
@@ -133,6 +133,9 @@ val slice = "slice" : forall 'n 'm 'o, 0 <= 'o < 'm & 'o + 'n <= 'm & 0 <= 'n.
 
 val replicate_bits = "replicate_bits" : forall 'n 'm. (bits('n), atom('m)) -> bits('n * 'm)
 
+/*!
+converts a bit vector of length $n$ to an integer in the range $0$ to $2^n - 1$.
+ */
 val unsigned = {
   ocaml: "uint",
   lem: "uint",
@@ -142,6 +145,9 @@ val unsigned = {
 } : forall 'n. bits('n) -> range(0, 2 ^ 'n - 1)
 
 /* We need a non-empty vector so that the range makes sense */
+/*!
+converts a bit vector of length $n$ to an integer in the range $-2^{n-1}$ to $2^{n-1} - 1$ using twos-complement.
+ */
 val signed = {
   c: "sail_signed",
   _: "sint"
-- 
cgit v1.2.3


From b3ea287bcf8be43714595b6921a0c47d25a67eee Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Fri, 16 Nov 2018 16:26:35 +0000
Subject: Various bugfixes and a simple profiling feature for rewrites

---
 lib/arith.sail |  4 ++--
 lib/rts.c      |  4 ++++
 lib/sail.c     | 11 +++++++++++
 lib/sail.h     |  3 +++
 4 files changed, 20 insertions(+), 2 deletions(-)

(limited to 'lib')

diff --git a/lib/arith.sail b/lib/arith.sail
index e61ec473..db011f14 100644
--- a/lib/arith.sail
+++ b/lib/arith.sail
@@ -57,13 +57,13 @@ let elsize = shl_int(8, UInt(size))
 ```
 THIS ensures that in this case the typechecker knows that the end result will be a value in the set `{8, 16, 32, 64}`
 */
-val _shl8 = "shl_int" :
+val _shl8 = {c: "shl_mach_int", _: "shl_int"} :
   forall 'n, 0 <= 'n <= 3. (int(8), int('n)) -> int('m) with 'm in {8, 16, 32, 64}
 
 /*!
 Similarly, we can shift 32 by either 0 or 1 to get a value in `{32, 64}`
 */
-val _shl32 = "shl_int" :
+val _shl32 = {c: "shl_mach_int", _: "shl_int"} :
   forall 'n, 'n in {0, 1}. (int(32), int('n)) -> int('m) with 'm in {32, 64}
 
 val _shl_int = "shl_int" : (int, int) -> int
diff --git a/lib/rts.c b/lib/rts.c
index 6bd97934..2f594ff8 100644
--- a/lib/rts.c
+++ b/lib/rts.c
@@ -94,6 +94,10 @@ void write_mem(uint64_t address, uint64_t byte)
   uint64_t mask = address & ~MASK;
   uint64_t offset = address & MASK;
 
+  //if ((byte >= 97 && byte <= 122) || (byte >= 64 && byte <= 90) || (byte >= 48 && byte <= 57) || byte == 10 || byte == 32) {
+  //  fprintf(stderr, "%c", (char) byte);
+  //}
+
   struct block *current = sail_memory;
 
   while (current != NULL) {
diff --git a/lib/sail.c b/lib/sail.c
index 94cd5c2c..fc11a40d 100644
--- a/lib/sail.c
+++ b/lib/sail.c
@@ -290,6 +290,12 @@ 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)
 {
@@ -446,6 +452,11 @@ void CREATE_OF(sail_bits, mach_bits)(sail_bits *rop, const uint64_t op, const ui
   mpz_init_set_ui(*rop->bits, op);
 }
 
+mach_bits CREATE_OF(mach_bits, sail_bits)(const sail_bits op)
+{
+  return mpz_get_ui(*op.bits);
+}
+
 void RECREATE_OF(sail_bits, mach_bits)(sail_bits *rop, const uint64_t op, const uint64_t len, const bool direction)
 {
   rop->len = len;
diff --git a/lib/sail.h b/lib/sail.h
index 4ccd8b93..b3386198 100644
--- a/lib/sail.h
+++ b/lib/sail.h
@@ -131,6 +131,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);
 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);
 
@@ -192,6 +193,8 @@ void RECREATE_OF(sail_bits, mach_bits)(sail_bits *,
 				       const mach_bits len,
 				       const bool direction);
 
+mach_bits CREATE_OF(mach_bits, sail_bits)(const sail_bits);
+
 mach_bits CONVERT_OF(mach_bits, sail_bits)(const sail_bits, const bool);
 void CONVERT_OF(sail_bits, mach_bits)(sail_bits *, const mach_bits, const uint64_t, const bool);
 
-- 
cgit v1.2.3


From 1bc81fa6dcafcfe24fce3685c2eb61f882e6b65c Mon Sep 17 00:00:00 2001
From: Robert Norton
Date: Mon, 19 Nov 2018 14:44:42 +0000
Subject: Add missing constraints on bitvector_access, with regression
 test.Fixes #24.

---
 lib/vector_dec.sail | 2 +-
 lib/vector_inc.sail | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'lib')

diff --git a/lib/vector_dec.sail b/lib/vector_dec.sail
index 8abcd218..7011a55c 100644
--- a/lib/vector_dec.sail
+++ b/lib/vector_dec.sail
@@ -63,7 +63,7 @@ val bitvector_access = {
   lem: "access_vec_dec",
   coq: "access_vec_dec",
   c: "vector_access"
-} : forall ('n : Int), 'n >= 0. (bits('n), int) -> bit
+} : forall ('n : Int) ('m : Int), 0 <= 'm < 'n . (bits('n), int('m)) -> bit
 
 val plain_vector_access = {
   ocaml: "access",
diff --git a/lib/vector_inc.sail b/lib/vector_inc.sail
index b295c92c..042a6324 100644
--- a/lib/vector_inc.sail
+++ b/lib/vector_inc.sail
@@ -61,7 +61,7 @@ val bitvector_access = {
   lem: "access_vec_inc",
   coq: "access_vec_inc",
   c: "vector_access"
-} : forall ('n : Int), 'n >= 0. (bits('n), int) -> bit
+} : forall ('n : Int) ('m : Int), 0 <= 'm < 'n . (bits('n), int('m)) -> bit
 
 val plain_vector_access = {
   ocaml: "access",
-- 
cgit v1.2.3


From 8c2fa417866f4c70fc5e4d17609a073e73c8ce71 Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Tue, 20 Nov 2018 11:30:49 +0000
Subject: Add full constraints for vector updates Also fix a test with an
 insufficient constraint

---
 lib/vector_dec.sail | 6 +++---
 lib/vector_inc.sail | 6 +++---
 2 files changed, 6 insertions(+), 6 deletions(-)

(limited to 'lib')

diff --git a/lib/vector_dec.sail b/lib/vector_dec.sail
index a4d1a0b1..6953264f 100644
--- a/lib/vector_dec.sail
+++ b/lib/vector_dec.sail
@@ -77,14 +77,14 @@ val bitvector_update = {
   lem: "update_vec_dec",
   coq: "update_vec_dec",
   c: "vector_update"
-} : forall 'n, 'n >= 0. (bits('n), int, bit) -> bits('n)
+} : forall 'n 'm, 0 <= 'm < 'n. (bits('n), atom('m), bit) -> bits('n)
 
 val plain_vector_update = {
   ocaml: "update",
   lem: "update_list_dec",
   coq: "vec_update_dec",
   c: "vector_update"
-} : forall 'n ('a : Type). (vector('n, dec, 'a), int, 'a) -> vector('n, dec, 'a)
+} : forall 'n 'm ('a : Type), 0 <= 'm < 'n. (vector('n, dec, 'a), atom('m), 'a) -> vector('n, dec, 'a)
 
 overload vector_update = {bitvector_update, plain_vector_update}
 
@@ -117,7 +117,7 @@ val vector_update_subrange = {
   lem: "update_subrange_vec_dec",
   c: "vector_update_subrange",
   coq: "update_subrange_vec_dec"
-} : forall 'n 'm 'o. (bits('n), atom('m), atom('o), bits('m - ('o - 1))) -> bits('n)
+} : forall 'n 'm 'o, 0 <= 'o <= 'm < 'n. (bits('n), atom('m), atom('o), bits('m - ('o - 1))) -> bits('n)
 
 // Some ARM specific builtins
 
diff --git a/lib/vector_inc.sail b/lib/vector_inc.sail
index 042a6324..581dded7 100644
--- a/lib/vector_inc.sail
+++ b/lib/vector_inc.sail
@@ -77,14 +77,14 @@ val bitvector_update = {
   lem: "update_vec_inc",
   coq: "update_vec_inc",
   c: "vector_update"
-} : forall 'n, 'n >= 0. (bits('n), int, bit) -> bits('n)
+} : forall 'n 'm, 0 <= 'm < 'n. (bits('n), atom('m), bit) -> bits('n)
 
 val plain_vector_update = {
   ocaml: "update",
   lem: "update_list_inc",
   coq: "update_list_inc",
   c: "vector_update"
-} : forall 'n ('a : Type). (vector('n, inc, 'a), int, 'a) -> vector('n, inc, 'a)
+} : forall 'n 'm ('a : Type), 0 <= 'm < 'n. (vector('n, inc, 'a), atom('m), 'a) -> vector('n, inc, 'a)
 
 overload vector_update = {bitvector_update, plain_vector_update}
 
@@ -113,7 +113,7 @@ val vector_update_subrange = {
   lem: "update_subrange_vec_inc",
   c: "vector_update_subrange",
   coq: "update_subrange_vec_inc"
-} : forall 'n 'm 'o. (bits('n), atom('m), atom('o), bits('m - ('o - 1))) -> bits('n)
+} : forall 'n 'm 'o, 0 <= 'm <= 'o < 'n. (bits('n), atom('m), atom('o), bits('m - ('o - 1))) -> bits('n)
 
 // Some ARM specific builtins
 
-- 
cgit v1.2.3


From c249747d681cb8e4c15af3d48f9191aa24777b27 Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Tue, 20 Nov 2018 15:12:48 +0000
Subject: Minor coq updates

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

(limited to 'lib')

diff --git a/lib/coq/Sail2_operators_mwords.v b/lib/coq/Sail2_operators_mwords.v
index 497b4a46..b5bcfe5f 100644
--- a/lib/coq/Sail2_operators_mwords.v
+++ b/lib/coq/Sail2_operators_mwords.v
@@ -471,3 +471,5 @@ Definition set_slice_int len n lo (v : mword len) : Z :=
     let bs : mword (hi + 1) := mword_of_int n in
     (int_of_mword true (update_subrange_vec_dec bs hi lo v))
   else n.
+
+Definition prerr_bits {a} (s : string) (bs : mword a) : unit := tt.
-- 
cgit v1.2.3


From 9b68baa58c1c6a3fc28df961624c522cca74cf8c Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Wed, 21 Nov 2018 13:58:26 +0000
Subject: Coq: add equality for records and polymorphic vectors

---
 lib/coq/Sail2_operators_mwords.v | 20 ++++++++++++++------
 lib/coq/Sail2_values.v           | 38 ++++++++++++++++++++++++++++++++++++++
 2 files changed, 52 insertions(+), 6 deletions(-)

(limited to 'lib')

diff --git a/lib/coq/Sail2_operators_mwords.v b/lib/coq/Sail2_operators_mwords.v
index b5bcfe5f..e37e9d26 100644
--- a/lib/coq/Sail2_operators_mwords.v
+++ b/lib/coq/Sail2_operators_mwords.v
@@ -9,12 +9,6 @@ Require Import ZArith.
 Require Import Omega.
 Require Import Eqdep_dec.
 
-Module Z_eq_dec.
-Definition U := Z.
-Definition eq_dec := Z.eq_dec.
-End Z_eq_dec.
-Module ZEqdep := DecidableEqDep (Z_eq_dec).
-
 Fixpoint cast_positive (T : positive -> Type) (p q : positive) : T p -> p = q -> T q.
 refine (
 match p, q with
@@ -444,6 +438,20 @@ Definition sgteq_vec := sgteq_bv.
 
 *)
 
+Definition eq_vec_dec {n} : forall (x y : mword n), {x = y} + {x <> y}.
+refine (match n with
+| Z0 => _
+| Zpos m => _
+| Zneg m => _
+end).
+* simpl. apply Word.weq.
+* simpl. apply Word.weq.
+* simpl. destruct x.
+Defined.
+
+Instance Decidable_eq_mword {n} : forall (x y : mword n), Decidable (x = y) :=
+  Decidable_eq_from_dec eq_vec_dec.
+
 Program Fixpoint reverse_endianness_word {n} (bits : word n) : word n :=
   match n with
   | S (S (S (S (S (S (S (S m))))))) =>
diff --git a/lib/coq/Sail2_values.v b/lib/coq/Sail2_values.v
index 83fe1dc7..48cfc222 100644
--- a/lib/coq/Sail2_values.v
+++ b/lib/coq/Sail2_values.v
@@ -8,10 +8,18 @@ Require Import bbv.Word.
 Require Export List.
 Require Export Sumbool.
 Require Export DecidableClass.
+Require Import Eqdep_dec.
 Import ListNotations.
 
 Open Scope Z.
 
+Module Z_eq_dec.
+Definition U := Z.
+Definition eq_dec := Z.eq_dec.
+End Z_eq_dec.
+Module ZEqdep := DecidableEqDep (Z_eq_dec).
+
+
 (* Constraint solving basics.  A HintDb which unfolding hints and lemmata
    can be added to, and a typeclass to wrap constraint arguments in to
    trigger automatic solving. *)
@@ -93,6 +101,22 @@ split.
   tauto.
 Qed.
 
+Definition generic_dec {T:Type} (x y:T) `{Decidable (x = y)} : {x = y} + {x <> y}.
+refine ((if Decidable_witness as b return (b = true <-> x = y -> _) then fun H' => _ else fun H' => _) Decidable_spec).
+* left. tauto.
+* right. intuition.
+Defined.
+
+(* Used by generated code that builds Decidable equality instances for records. *)
+Ltac cmp_record_field x y :=
+  let H := fresh "H" in
+  case (generic_dec x y);
+  intro H; [ |
+    refine (Build_Decidable _ false _);
+    split; [congruence | intros Z; destruct H; injection Z; auto]
+  ].
+
+
 
 (* Project away range constraints in comparisons *)
 Definition ltb_range_l {lo hi} (l : {x & ArithFact (lo <= x /\ x <= hi)}) r := Z.ltb (projT1 l) r.
@@ -1736,6 +1760,20 @@ Qed.
 
 Definition list_of_vec {A n} (v : vec A n) : list A := projT1 v.
 
+Definition vec_eq_dec {T n} (D : forall x y : T, {x = y} + {x <> y}) (x y : vec T n) :
+  {x = y} + {x <> y}.
+refine (if List.list_eq_dec D (projT1 x) (projT1 y) then left _ else right _).
+* apply eq_sigT_hprop; auto using ZEqdep.UIP.
+* contradict n0. rewrite n0. reflexivity.
+Defined.
+
+Instance Decidable_eq_vec {T : Type} {n} `(DT : forall x y : T, Decidable (x = y)) :
+  forall x y : vec T n, Decidable (x = y) := {
+  Decidable_witness := proj1_sig (bool_of_sumbool (vec_eq_dec (fun x y => generic_dec x y) x y))
+}.
+destruct (vec_eq_dec _ x y); simpl; split; congruence.
+Defined.
+
 Program Definition vec_of_list {A} n (l : list A) : option (vec A n) :=
   if sumbool_of_bool (n =? length_list l) then Some (existT _ l _) else None.
 Next Obligation.
-- 
cgit v1.2.3


From 7fbf5d8ffb99e63d46d53fc3444764986764df9f Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Wed, 21 Nov 2018 13:58:39 +0000
Subject: Coq: min_nat

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

(limited to 'lib')

diff --git a/lib/coq/Sail2_values.v b/lib/coq/Sail2_values.v
index 48cfc222..aebc3376 100644
--- a/lib/coq/Sail2_values.v
+++ b/lib/coq/Sail2_values.v
@@ -1794,3 +1794,7 @@ Definition sub_nat (x : {x : Z & ArithFact (x >= 0)}) (y : {y : Z & ArithFact (y
   {z : Z & ArithFact (z >= 0)} :=
   let z := projT1 x - projT1 y in
   if sumbool_of_bool (z >=? 0) then build_ex z else build_ex 0.
+
+Definition min_nat (x : {x : Z & ArithFact (x >= 0)}) (y : {y : Z & ArithFact (y >= 0)}) :
+  {z : Z & ArithFact (z >= 0)} :=
+  build_ex (Z.min (projT1 x) (projT1 y)).
-- 
cgit v1.2.3


From ea177d95766789b0500317f12fe0939d1508e19c Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Fri, 23 Nov 2018 17:55:54 +0000
Subject: C backend improvements

- Propagate types more accurately to improve optimization on ANF
  representation.

- Add a generic optimization pass to remove redundant variables that
  simply alias other variables.

- Modify Sail interactive mode, so it can compile a specification with
  the :compile command, view generated intermediate representation via
  the :ir <function> command, and step-through the IR with :exec <exp>
  (although this is very incomplete)

- Introduce a third bitvector representation, between fast
  fixed-precision bitvectors, and variable length large
  bitvectors. The bitvector types are now from most efficient to least

   * CT_fbits for fixed precision, 64-bit or less bitvectors
   * CT_sbits for 64-bit or less, variable length bitvectors
   * CT_lbits for arbitrary variable length bitvectors

- Support for generating C code using CT_sbits is currently
  incomplete, it just exists in the intermediate representation right
  now.

- Include ctyp in AV_C_fragment, so we don't have to recompute it
---
 lib/sail.c | 6 ++++++
 lib/sail.h | 3 +++
 2 files changed, 9 insertions(+)

(limited to 'lib')

diff --git a/lib/sail.c b/lib/sail.c
index fc11a40d..6ea41fcc 100644
--- a/lib/sail.c
+++ b/lib/sail.c
@@ -693,6 +693,12 @@ void sail_signed(sail_int *rop, const sail_bits op)
   }
 }
 
+inline
+mach_int fast_unsigned(const mach_bits op)
+{
+  return (mach_int) op;
+}
+
 void append(sail_bits *rop, const sail_bits op1, const sail_bits op2)
 {
   rop->len = op1.len + op2.len;
diff --git a/lib/sail.h b/lib/sail.h
index b3386198..6b67b7e0 100644
--- a/lib/sail.h
+++ b/lib/sail.h
@@ -196,6 +196,7 @@ void RECREATE_OF(sail_bits, mach_bits)(sail_bits *,
 mach_bits CREATE_OF(mach_bits, sail_bits)(const sail_bits);
 
 mach_bits CONVERT_OF(mach_bits, sail_bits)(const sail_bits, const bool);
+
 void CONVERT_OF(sail_bits, mach_bits)(sail_bits *, const mach_bits, const uint64_t, const bool);
 
 void UNDEFINED(sail_bits)(sail_bits *, const sail_int len, const mach_bits bit);
@@ -249,6 +250,8 @@ mach_bits bitvector_access(const sail_bits op, const sail_int n_mpz);
 void sail_unsigned(sail_int *rop, const sail_bits op);
 void sail_signed(sail_int *rop, const sail_bits op);
 
+mach_int fast_unsigned(const mach_bits);
+
 void append(sail_bits *rop, const sail_bits op1, const sail_bits op2);
 
 void replicate_bits(sail_bits *rop, const sail_bits op1, const sail_int op2);
-- 
cgit v1.2.3


From 2e271d91c58a2d4db4adbb4c47d34bcbe1a6992e Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Fri, 23 Nov 2018 22:05:24 +0000
Subject: Introduce intermediate bitvector representation in C

Bitvectors that aren't fixed size, but can still be shown to fit
within 64-bits, now have a specialised representation. Still need to
introduce more optimized functions, as right now we mostly have to
convert them into large bitvectors to pass them into most
functions. Nevertheless, this doubles the performance of the TLBLookup
function in ARMv8.
---
 lib/rts.c  |  20 ++---
 lib/rts.h  |  24 +++---
 lib/sail.c | 255 +++++++++++++++++++++++++++++++++++++++++++------------------
 lib/sail.h | 190 ++++++++++++++++++++++++---------------------
 4 files changed, 305 insertions(+), 184 deletions(-)

(limited to 'lib')

diff --git a/lib/rts.c b/lib/rts.c
index 2f594ff8..bc0d4732 100644
--- a/lib/rts.c
+++ b/lib/rts.c
@@ -32,7 +32,7 @@ unit sail_exit(unit u)
 
 static uint64_t g_verbosity = 0;
 
-mach_bits sail_get_verbosity(const unit u)
+fbits sail_get_verbosity(const unit u)
 {
   return g_verbosity;
 }
@@ -214,9 +214,9 @@ void kill_mem()
 
 bool write_ram(const mpz_t addr_size,     // Either 32 or 64
 	       const mpz_t data_size_mpz, // Number of bytes
-	       const sail_bits  hex_ram,       // Currently unused
-	       const sail_bits  addr_bv,
-	       const sail_bits  data)
+	       const lbits  hex_ram,       // Currently unused
+	       const lbits  addr_bv,
+	       const lbits  data)
 {
   uint64_t addr = mpz_get_ui(*addr_bv.bits);
   uint64_t data_size = mpz_get_ui(data_size_mpz);
@@ -238,11 +238,11 @@ bool write_ram(const mpz_t addr_size,     // Either 32 or 64
   return true;
 }
 
-void read_ram(sail_bits *data,
+void read_ram(lbits *data,
 	      const mpz_t addr_size,
 	      const mpz_t data_size_mpz,
-	      const sail_bits hex_ram,
-	      const sail_bits addr_bv)
+	      const lbits hex_ram,
+	      const lbits addr_bv)
 {
   uint64_t addr = mpz_get_ui(*addr_bv.bits);
   uint64_t data_size = mpz_get_ui(data_size_mpz);
@@ -261,7 +261,7 @@ void read_ram(sail_bits *data,
   mpz_clear(byte);
 }
 
-unit load_raw(mach_bits addr, const sail_string file)
+unit load_raw(fbits addr, const sail_string file)
 {
   FILE *fp = fopen(file, "r");
 
@@ -339,7 +339,7 @@ bool is_tracing(const unit u)
   return g_trace_enabled;
 }
 
-void trace_mach_bits(const mach_bits x) {
+void trace_fbits(const fbits x) {
   if (g_trace_enabled) fprintf(stderr, "0x%" PRIx64, x);
 }
 
@@ -355,7 +355,7 @@ void trace_sail_int(const sail_int op) {
   if (g_trace_enabled) mpz_out_str(stderr, 10, op);
 }
 
-void trace_sail_bits(const sail_bits op) {
+void trace_lbits(const lbits op) {
   if (g_trace_enabled) fprint_bits("", op, "", stderr);
 }
 
diff --git a/lib/rts.h b/lib/rts.h
index 98bbd078..f5e5e3b1 100644
--- a/lib/rts.h
+++ b/lib/rts.h
@@ -26,7 +26,7 @@ unit sail_exit(unit);
  * The intention is that you can use individual bits to turn on/off different
  * pieces of debugging output.
  */
-mach_bits sail_get_verbosity(const unit u);
+fbits sail_get_verbosity(const unit u);
 
 /*
  * Put processor to sleep until an external device calls wakeup_request().
@@ -55,20 +55,20 @@ uint64_t read_mem(uint64_t);
 
 bool write_ram(const mpz_t addr_size,     // Either 32 or 64
 	       const mpz_t data_size_mpz, // Number of bytes
-	       const sail_bits hex_ram,       // Currently unused
-	       const sail_bits addr_bv,
-	       const sail_bits data);
+	       const lbits hex_ram,       // Currently unused
+	       const lbits addr_bv,
+	       const lbits data);
 
-void read_ram(sail_bits *data,
+void read_ram(lbits *data,
 	      const mpz_t addr_size,
 	      const mpz_t data_size_mpz,
-	      const sail_bits hex_ram,
-	      const sail_bits addr_bv);
+	      const lbits hex_ram,
+	      const lbits addr_bv);
 
-unit write_tag_bool(const mach_bits, const bool);
-bool read_tag_bool(const mach_bits);
+unit write_tag_bool(const fbits, const bool);
+bool read_tag_bool(const fbits);
 
-unit load_raw(mach_bits addr, const sail_string file);
+unit load_raw(fbits addr, const sail_string file);
 
 void load_image(char *);
 
@@ -106,8 +106,8 @@ void trace_sail_int(const sail_int);
 void trace_bool(const bool);
 void trace_unit(const unit);
 void trace_sail_string(const sail_string);
-void trace_mach_bits(const mach_bits);
-void trace_sail_bits(const sail_bits);
+void trace_fbits(const fbits);
+void trace_lbits(const lbits);
 
 void trace_unknown(void);
 void trace_argsep(void);
diff --git a/lib/sail.c b/lib/sail.c
index 6ea41fcc..fbf230a6 100644
--- a/lib/sail.c
+++ b/lib/sail.c
@@ -7,6 +7,8 @@
 #include<string.h>
 #include<time.h>
 
+#include <x86intrin.h>
+
 #include"sail.h"
 
 /*
@@ -53,7 +55,7 @@ unit skip(const unit u)
 
 /* ***** Sail bit type ***** */
 
-bool eq_bit(const mach_bits a, const mach_bits b)
+bool eq_bit(const fbits a, const fbits b)
 {
   return a == b;
 }
@@ -415,74 +417,144 @@ void pow2(sail_int *rop, const sail_int exp)
 
 /* ***** Sail bitvectors ***** */
 
-bool EQUAL(mach_bits)(const mach_bits op1, const mach_bits op2)
+bool EQUAL(fbits)(const fbits op1, const fbits op2)
 {
   return op1 == op2;
 }
 
-void CREATE(sail_bits)(sail_bits *rop)
+void CREATE(lbits)(lbits *rop)
 {
   rop->bits = malloc(sizeof(mpz_t));
   rop->len = 0;
   mpz_init(*rop->bits);
 }
 
-void RECREATE(sail_bits)(sail_bits *rop)
+void RECREATE(lbits)(lbits *rop)
 {
   rop->len = 0;
   mpz_set_ui(*rop->bits, 0);
 }
 
-void COPY(sail_bits)(sail_bits *rop, const sail_bits op)
+void COPY(lbits)(lbits *rop, const lbits op)
 {
   rop->len = op.len;
   mpz_set(*rop->bits, *op.bits);
 }
 
-void KILL(sail_bits)(sail_bits *rop)
+void KILL(lbits)(lbits *rop)
 {
   mpz_clear(*rop->bits);
   free(rop->bits);
 }
 
-void CREATE_OF(sail_bits, mach_bits)(sail_bits *rop, const uint64_t op, const uint64_t len, const bool direction)
+void CREATE_OF(lbits, fbits)(lbits *rop, const uint64_t op, const uint64_t len, const bool direction)
 {
   rop->bits = malloc(sizeof(mpz_t));
   rop->len = len;
   mpz_init_set_ui(*rop->bits, op);
 }
 
-mach_bits CREATE_OF(mach_bits, sail_bits)(const sail_bits op)
+fbits CREATE_OF(fbits, lbits)(const lbits op, const bool direction)
 {
   return mpz_get_ui(*op.bits);
 }
 
-void RECREATE_OF(sail_bits, mach_bits)(sail_bits *rop, const uint64_t op, const uint64_t len, const bool direction)
+sbits CREATE_OF(sbits, lbits)(const lbits op, const bool direction)
+{
+  sbits rop;
+  rop.bits = mpz_get_ui(*op.bits);
+  rop.len = op.len;
+  return rop;
+}
+
+sbits CREATE_OF(sbits, fbits)(const fbits op, const uint64_t len, const bool direction)
+{
+  sbits rop;
+  rop.bits = op;
+  rop.len = len;
+  return rop;
+}
+
+void RECREATE_OF(lbits, fbits)(lbits *rop, const uint64_t op, const uint64_t len, const bool direction)
 {
   rop->len = len;
   mpz_set_ui(*rop->bits, op);
 }
 
-mach_bits CONVERT_OF(mach_bits, sail_bits)(const sail_bits op, const bool direction)
+void CREATE_OF(lbits, sbits)(lbits *rop, const sbits op, const bool direction)
+{
+  rop->bits = malloc(sizeof(mpz_t));
+  rop->len = op.len;
+  mpz_init_set_ui(*rop->bits, op.bits);
+}
+
+void RECREATE_OF(lbits, sbits)(lbits *rop, const sbits op, const bool direction)
+{
+  rop->len = op.len;
+  mpz_set_ui(*rop->bits, op.bits);
+}
+
+// Bitvector conversions
+
+inline
+fbits CONVERT_OF(fbits, lbits)(const lbits op, const bool direction)
 {
   return mpz_get_ui(*op.bits);
 }
 
-void CONVERT_OF(sail_bits, mach_bits)(sail_bits *rop, const mach_bits op, const uint64_t len, const bool direction)
+inline
+fbits CONVERT_OF(fbits, sbits)(const sbits op, const bool direction)
+{
+  return op.bits;
+}
+
+void CONVERT_OF(lbits, fbits)(lbits *rop, const fbits op, const uint64_t len, const bool direction)
 {
   rop->len = len;
   // use safe_rshift to correctly handle the case when we have a 0-length vector.
   mpz_set_ui(*rop->bits, op & safe_rshift(UINT64_MAX, 64 - len));
 }
 
-void UNDEFINED(sail_bits)(sail_bits *rop, const sail_int len, const mach_bits bit)
+void CONVERT_OF(lbits, sbits)(lbits *rop, const sbits op, const bool direction)
+{
+  rop->len = op.len;
+  mpz_set_ui(*rop->bits, op.bits & safe_rshift(UINT64_MAX, 64 - op.len));
+}
+
+inline
+sbits CONVERT_OF(sbits, fbits)(const fbits op, const uint64_t len, const bool direction)
+{
+  sbits rop;
+  rop.len = len;
+  rop.bits = op;
+  return rop;
+}
+
+inline
+sbits CONVERT_OF(sbits, lbits)(const lbits op, const bool direction)
+{
+  sbits rop;
+  rop.len = op.len;
+  rop.bits = mpz_get_ui(*op.bits);
+  return rop;
+}
+
+void UNDEFINED(lbits)(lbits *rop, const sail_int len, const fbits bit)
 {
   zeros(rop, len);
 }
 
-mach_bits UNDEFINED(mach_bits)(const unit u) { return 0; }
+fbits UNDEFINED(fbits)(const unit u) { return 0; }
 
-mach_bits safe_rshift(const mach_bits x, const mach_bits n)
+sbits undefined_sbits(void)
+{
+  sbits rop;
+  rop.bits = UINT64_C(0);
+  rop.len = UINT64_C(0);
+  return rop;
+}
+
+fbits safe_rshift(const fbits x, const fbits n)
 {
   if (n >= 64) {
     return 0ul;
@@ -491,7 +563,7 @@ mach_bits safe_rshift(const mach_bits x, const mach_bits n)
   }
 }
 
-void normalize_sail_bits(sail_bits *rop) {
+void normalize_lbits(lbits *rop) {
   /* TODO optimisation: keep a set of masks of various sizes handy */
   mpz_set_ui(sail_lib_tmp1, 1);
   mpz_mul_2exp(sail_lib_tmp1, sail_lib_tmp1, rop->len);
@@ -499,64 +571,64 @@ void normalize_sail_bits(sail_bits *rop) {
   mpz_and(*rop->bits, *rop->bits, sail_lib_tmp1);
 }
 
-void append_64(sail_bits *rop, const sail_bits op, const mach_bits chunk)
+void append_64(lbits *rop, const lbits op, const fbits chunk)
 {
   rop->len = rop->len + 64ul;
   mpz_mul_2exp(*rop->bits, *op.bits, 64ul);
   mpz_add_ui(*rop->bits, *rop->bits, chunk);
 }
 
-void add_bits(sail_bits *rop, const sail_bits op1, const sail_bits op2)
+void add_bits(lbits *rop, const lbits op1, const lbits op2)
 {
   rop->len = op1.len;
   mpz_add(*rop->bits, *op1.bits, *op2.bits);
-  normalize_sail_bits(rop);
+  normalize_lbits(rop);
 }
 
-void sub_bits(sail_bits *rop, const sail_bits op1, const sail_bits op2)
+void sub_bits(lbits *rop, const lbits op1, const lbits op2)
 {
   assert(op1.len == op2.len);
   rop->len = op1.len;
   mpz_sub(*rop->bits, *op1.bits, *op2.bits);
-  normalize_sail_bits(rop);
+  normalize_lbits(rop);
 }
 
-void add_bits_int(sail_bits *rop, const sail_bits op1, const mpz_t op2)
+void add_bits_int(lbits *rop, const lbits op1, const mpz_t op2)
 {
   rop->len = op1.len;
   mpz_add(*rop->bits, *op1.bits, op2);
-  normalize_sail_bits(rop);
+  normalize_lbits(rop);
 }
 
-void sub_bits_int(sail_bits *rop, const sail_bits op1, const mpz_t op2)
+void sub_bits_int(lbits *rop, const lbits op1, const mpz_t op2)
 {
   rop->len = op1.len;
   mpz_sub(*rop->bits, *op1.bits, op2);
-  normalize_sail_bits(rop);
+  normalize_lbits(rop);
 }
 
-void and_bits(sail_bits *rop, const sail_bits op1, const sail_bits op2)
+void and_bits(lbits *rop, const lbits op1, const lbits op2)
 {
   assert(op1.len == op2.len);
   rop->len = op1.len;
   mpz_and(*rop->bits, *op1.bits, *op2.bits);
 }
 
-void or_bits(sail_bits *rop, const sail_bits op1, const sail_bits op2)
+void or_bits(lbits *rop, const lbits op1, const lbits op2)
 {
   assert(op1.len == op2.len);
   rop->len = op1.len;
   mpz_ior(*rop->bits, *op1.bits, *op2.bits);
 }
 
-void xor_bits(sail_bits *rop, const sail_bits op1, const sail_bits op2)
+void xor_bits(lbits *rop, const lbits op1, const lbits op2)
 {
   assert(op1.len == op2.len);
   rop->len = op1.len;
   mpz_xor(*rop->bits, *op1.bits, *op2.bits);
 }
 
-void not_bits(sail_bits *rop, const sail_bits op)
+void not_bits(lbits *rop, const lbits op)
 {
   rop->len = op.len;
   mpz_set(*rop->bits, *op.bits);
@@ -565,7 +637,7 @@ void not_bits(sail_bits *rop, const sail_bits op)
   }
 }
 
-void mults_vec(sail_bits *rop, const sail_bits op1, const sail_bits op2)
+void mults_vec(lbits *rop, const lbits op1, const lbits op2)
 {
   mpz_t op1_int, op2_int;
   mpz_init(op1_int);
@@ -574,33 +646,33 @@ void mults_vec(sail_bits *rop, const sail_bits op1, const sail_bits op2)
   sail_signed(&op2_int, op2);
   rop->len = op1.len * 2;
   mpz_mul(*rop->bits, op1_int, op2_int);
-  normalize_sail_bits(rop);
+  normalize_lbits(rop);
   mpz_clear(op1_int);
   mpz_clear(op2_int);
 }
 
-void mult_vec(sail_bits *rop, const sail_bits op1, const sail_bits op2)
+void mult_vec(lbits *rop, const lbits op1, const lbits op2)
 {
   rop->len = op1.len * 2;
   mpz_mul(*rop->bits, *op1.bits, *op2.bits);
-  normalize_sail_bits(rop); /* necessary? */
+  normalize_lbits(rop); /* necessary? */
 }
 
 
-void zeros(sail_bits *rop, const sail_int op)
+void zeros(lbits *rop, const sail_int op)
 {
   rop->len = mpz_get_ui(op);
   mpz_set_ui(*rop->bits, 0);
 }
 
-void zero_extend(sail_bits *rop, const sail_bits op, const sail_int len)
+void zero_extend(lbits *rop, const lbits op, const sail_int len)
 {
   assert(op.len <= mpz_get_ui(len));
   rop->len = mpz_get_ui(len);
   mpz_set(*rop->bits, *op.bits);
 }
 
-void sign_extend(sail_bits *rop, const sail_bits op, const sail_int len)
+void sign_extend(lbits *rop, const lbits op, const sail_int len)
 {
   assert(op.len <= mpz_get_ui(len));
   rop->len = mpz_get_ui(len);
@@ -614,12 +686,12 @@ void sign_extend(sail_bits *rop, const sail_bits op, const sail_int len)
   }
 }
 
-void length_sail_bits(sail_int *rop, const sail_bits op)
+void length_lbits(sail_int *rop, const lbits op)
 {
   mpz_set_ui(*rop, op.len);
 }
 
-bool eq_bits(const sail_bits op1, const sail_bits op2)
+bool eq_bits(const lbits op1, const lbits op2)
 {
   assert(op1.len == op2.len);
   for (mp_bitcnt_t i = 0; i < op1.len; i++) {
@@ -628,12 +700,12 @@ bool eq_bits(const sail_bits op1, const sail_bits op2)
   return true;
 }
 
-bool EQUAL(sail_bits)(const sail_bits op1, const sail_bits op2)
+bool EQUAL(lbits)(const lbits op1, const lbits op2)
 {
   return eq_bits(op1, op2);
 }
 
-bool neq_bits(const sail_bits op1, const sail_bits op2)
+bool neq_bits(const lbits op1, const lbits op2)
 {
   assert(op1.len == op2.len);
   for (mp_bitcnt_t i = 0; i < op1.len; i++) {
@@ -642,8 +714,8 @@ bool neq_bits(const sail_bits op1, const sail_bits op2)
   return false;
 }
 
-void vector_subrange_sail_bits(sail_bits *rop,
-			       const sail_bits op,
+void vector_subrange_lbits(lbits *rop,
+			       const lbits op,
 			       const sail_int n_mpz,
 			       const sail_int m_mpz)
 {
@@ -652,30 +724,30 @@ void vector_subrange_sail_bits(sail_bits *rop,
 
   rop->len = n - (m - 1ul);
   mpz_fdiv_q_2exp(*rop->bits, *op.bits, m);
-  normalize_sail_bits(rop);
+  normalize_lbits(rop);
 }
 
-void sail_truncate(sail_bits *rop, const sail_bits op, const sail_int len)
+void sail_truncate(lbits *rop, const lbits op, const sail_int len)
 {
   assert(op.len >= mpz_get_ui(len));
   rop->len = mpz_get_ui(len);
   mpz_set(*rop->bits, *op.bits);
-  normalize_sail_bits(rop);
+  normalize_lbits(rop);
 }
 
-mach_bits bitvector_access(const sail_bits op, const sail_int n_mpz)
+fbits bitvector_access(const lbits op, const sail_int n_mpz)
 {
   uint64_t n = mpz_get_ui(n_mpz);
-  return (mach_bits) mpz_tstbit(*op.bits, n);
+  return (fbits) mpz_tstbit(*op.bits, n);
 }
 
-void sail_unsigned(sail_int *rop, const sail_bits op)
+void sail_unsigned(sail_int *rop, const lbits op)
 {
   /* Normal form of bv_t is always positive so just return the bits. */
   mpz_set(*rop, *op.bits);
 }
 
-void sail_signed(sail_int *rop, const sail_bits op)
+void sail_signed(sail_int *rop, const lbits op)
 {
   if (op.len == 0) {
     mpz_set_ui(*rop, 0);
@@ -694,19 +766,19 @@ void sail_signed(sail_int *rop, const sail_bits op)
 }
 
 inline
-mach_int fast_unsigned(const mach_bits op)
+mach_int fast_unsigned(const fbits op)
 {
   return (mach_int) op;
 }
 
-void append(sail_bits *rop, const sail_bits op1, const sail_bits op2)
+void append(lbits *rop, const lbits op1, const lbits op2)
 {
   rop->len = op1.len + op2.len;
   mpz_mul_2exp(*rop->bits, *op1.bits, op2.len);
   mpz_ior(*rop->bits, *rop->bits, *op2.bits);
 }
 
-void replicate_bits(sail_bits *rop, const sail_bits op1, const mpz_t op2)
+void replicate_bits(lbits *rop, const lbits op1, const mpz_t op2)
 {
   uint64_t op2_ui = mpz_get_ui(op2);
   rop->len = op1.len * op2_ui;
@@ -742,7 +814,7 @@ uint64_t fast_replicate_bits(const uint64_t shift, const uint64_t v, const int64
 //                    <-------^
 //                    (8 bit) 4
 //
-void get_slice_int(sail_bits *rop, const sail_int len_mpz, const sail_int n, const sail_int start_mpz)
+void get_slice_int(lbits *rop, const sail_int len_mpz, const sail_int n, const sail_int start_mpz)
 {
   uint64_t start = mpz_get_ui(start_mpz);
   uint64_t len = mpz_get_ui(len_mpz);
@@ -761,7 +833,7 @@ void set_slice_int(sail_int *rop,
 		   const sail_int len_mpz,
 		   const sail_int n,
 		   const sail_int start_mpz,
-		   const sail_bits slice)
+		   const lbits slice)
 {
   uint64_t start = mpz_get_ui(start_mpz);
 
@@ -776,11 +848,11 @@ void set_slice_int(sail_int *rop,
   }
 }
 
-void vector_update_subrange_sail_bits(sail_bits *rop,
-				 const sail_bits op,
+void vector_update_subrange_lbits(lbits *rop,
+				 const lbits op,
 				 const sail_int n_mpz,
 				 const sail_int m_mpz,
-				 const sail_bits slice)
+				 const lbits slice)
 {
   uint64_t n = mpz_get_ui(n_mpz);
   uint64_t m = mpz_get_ui(m_mpz);
@@ -797,7 +869,7 @@ void vector_update_subrange_sail_bits(sail_bits *rop,
   }
 }
 
-void slice(sail_bits *rop, const sail_bits op, const sail_int start_mpz, const sail_int len_mpz)
+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);
   uint64_t start = mpz_get_ui(start_mpz);
@@ -811,12 +883,25 @@ void slice(sail_bits *rop, const sail_bits op, const sail_int start_mpz, const s
   }
 }
 
-void set_slice(sail_bits *rop,
+inline
+sbits sslice(const fbits op, const mach_int start, const mach_int len)
+{
+  sbits rop;
+#ifdef INTRINSICS
+  rop.bits = _bzhi_u64(op >> start, len);
+#else
+  rop.bits = (op >> start) & safe_rshift(UINT64_MAX, 64 - len);
+#endif
+  rop.len = len;
+  return rop;
+}
+
+void set_slice(lbits *rop,
 	       const sail_int len_mpz,
 	       const sail_int slen_mpz,
-	       const sail_bits op,
+	       const lbits op,
 	       const sail_int start_mpz,
-	       const sail_bits slice)
+	       const lbits slice)
 {
   uint64_t start = mpz_get_ui(start_mpz);
 
@@ -832,21 +917,21 @@ void set_slice(sail_bits *rop,
   }
 }
 
-void shift_bits_left(sail_bits *rop, const sail_bits op1, const sail_bits op2)
+void shift_bits_left(lbits *rop, const lbits op1, const lbits op2)
 {
   rop->len = op1.len;
   mpz_mul_2exp(*rop->bits, *op1.bits, mpz_get_ui(*op2.bits));
-  normalize_sail_bits(rop);
+  normalize_lbits(rop);
 }
 
-void shift_bits_right(sail_bits *rop, const sail_bits op1, const sail_bits op2)
+void shift_bits_right(lbits *rop, const lbits op1, const lbits op2)
 {
   rop->len = op1.len;
   mpz_tdiv_q_2exp(*rop->bits, *op1.bits, mpz_get_ui(*op2.bits));
 }
 
 /* FIXME */
-void shift_bits_right_arith(sail_bits *rop, const sail_bits op1, const sail_bits op2)
+void shift_bits_right_arith(lbits *rop, const lbits op1, const lbits op2)
 {
   rop->len = op1.len;
   mp_bitcnt_t shift_amt = mpz_get_ui(*op2.bits);
@@ -860,20 +945,20 @@ 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)
+void shiftl(lbits *rop, const lbits op1, const sail_int op2)
 {
   rop->len = op1.len;
   mpz_mul_2exp(*rop->bits, *op1.bits, mpz_get_ui(op2));
-  normalize_sail_bits(rop);
+  normalize_lbits(rop);
 }
 
-void shiftr(sail_bits *rop, const sail_bits op1, const sail_int op2)
+void shiftr(lbits *rop, const lbits 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)
+void reverse_endianness(lbits *rop, const lbits op)
 {
   rop->len = op.len;
   if (rop->len == 64ul) {
@@ -907,6 +992,26 @@ void reverse_endianness(sail_bits *rop, const sail_bits op)
   }
 }
 
+inline
+bool eq_sbits(const sbits op1, const sbits op2)
+{
+  return op1.bits == op2.bits;
+}
+
+inline
+bool neq_sbits(const sbits op1, const sbits op2)
+{
+  return op1.bits != op2.bits;
+}
+
+sbits xor_sbits(const sbits op1, const sbits op2)
+{
+  sbits rop;
+  rop.bits = op1.bits ^ op2.bits;
+  rop.len = op1.len;
+  return rop;
+}
+
 /* ***** Sail Reals ***** */
 
 void CREATE(real)(real *rop)
@@ -1148,7 +1253,7 @@ void string_of_int(sail_string *str, const sail_int i)
 }
 
 /* asprinf is a GNU extension, but it should exist on BSD */
-void string_of_mach_bits(sail_string *str, const mach_bits op)
+void string_of_fbits(sail_string *str, const fbits op)
 {
   int bytes = asprintf(str, "0x%" PRIx64, op);
   if (bytes == -1) {
@@ -1156,7 +1261,7 @@ void string_of_mach_bits(sail_string *str, const mach_bits op)
   }
 }
 
-void string_of_sail_bits(sail_string *str, const sail_bits op)
+void string_of_lbits(sail_string *str, const lbits op)
 {
   if ((op.len % 4) == 0) {
     gmp_asprintf(str, "0x%*0Zx", op.len / 4, *op.bits);
@@ -1165,7 +1270,7 @@ void string_of_sail_bits(sail_string *str, const sail_bits op)
   }
 }
 
-void decimal_string_of_mach_bits(sail_string *str, const mach_bits op)
+void decimal_string_of_fbits(sail_string *str, const fbits op)
 {
   int bytes = asprintf(str, "%" PRId64, op);
   if (bytes == -1) {
@@ -1173,13 +1278,13 @@ void decimal_string_of_mach_bits(sail_string *str, const mach_bits op)
   }
 }
 
-void decimal_string_of_sail_bits(sail_string *str, const sail_bits op)
+void decimal_string_of_lbits(sail_string *str, const lbits op)
 {
   gmp_asprintf(str, "%Z", *op.bits);
 }
 
 void fprint_bits(const sail_string pre,
-		 const sail_bits op,
+		 const lbits op,
 		 const sail_string post,
 		 FILE *stream)
 {
@@ -1214,13 +1319,13 @@ void fprint_bits(const sail_string pre,
   fputs(post, stream);
 }
 
-unit print_bits(const sail_string str, const sail_bits op)
+unit print_bits(const sail_string str, const lbits op)
 {
   fprint_bits(str, op, "\n", stdout);
   return UNIT;
 }
 
-unit prerr_bits(const sail_string str, const sail_bits op)
+unit prerr_bits(const sail_string str, const lbits op)
 {
   fprint_bits(str, op, "\n", stderr);
   return UNIT;
diff --git a/lib/sail.h b/lib/sail.h
index 6b67b7e0..56df9740 100644
--- a/lib/sail.h
+++ b/lib/sail.h
@@ -4,10 +4,7 @@
 #include<stdlib.h>
 #include<stdio.h>
 #include<stdbool.h>
-
-#ifndef USE_INT128
 #include<gmp.h>
-#endif
 
 #include<time.h>
 
@@ -85,14 +82,6 @@ typedef int64_t mach_int;
 
 bool EQUAL(mach_int)(const mach_int, const mach_int);
 
-/*
- * Integers can be either stack-allocated as 128-bit integers if
- * __int128 is available, or use GMP arbitrary precision
- * integers. This affects the function signatures, so use a macro to
- * paper over the differences.
- */
-#ifndef USE_INT128
-
 typedef mpz_t sail_int;
 
 #define SAIL_INT_FUNCTION(fname, rtype, ...) void fname(rtype*, __VA_ARGS__)
@@ -110,13 +99,6 @@ void RECREATE_OF(sail_int, sail_string)(mpz_t *, const sail_string);
 mach_int CONVERT_OF(mach_int, sail_int)(const sail_int);
 void CONVERT_OF(sail_int, mach_int)(sail_int *, const mach_int);
 
-#else
-
-typedef __int128 sail_int;
-#define SAIL_INT_FUNCTION(fname, rtype, ...) rtype fname(__VA_ARGS__)
-
-#endif
-
 /*
  * Comparison operators for integers
  */
@@ -170,125 +152,159 @@ SAIL_INT_FUNCTION(pow2, sail_int, const sail_int);
 
 /* ***** Sail bitvectors ***** */
 
-typedef uint64_t mach_bits;
+typedef uint64_t fbits;
 
-bool eq_bit(const mach_bits a, const mach_bits b);
+bool eq_bit(const fbits a, const fbits b);
 
-bool EQUAL(mach_bits)(const mach_bits, const mach_bits);
+bool EQUAL(fbits)(const fbits, const fbits);
+
+typedef struct {
+  uint64_t len;
+  uint64_t bits;
+} sbits;
 
 typedef struct {
   mp_bitcnt_t len;
   mpz_t *bits;
-} sail_bits;
+} lbits;
 
-SAIL_BUILTIN_TYPE(sail_bits);
+// For backwards compatability
+typedef uint64_t mach_bits;
+typedef lbits sail_bits;
+
+SAIL_BUILTIN_TYPE(lbits);
+
+void CREATE_OF(lbits, fbits)(lbits *,
+			     const fbits op,
+			     const uint64_t len,
+			     const bool direction);
+
+void RECREATE_OF(lbits, fbits)(lbits *,
+			       const fbits op,
+			       const uint64_t len,
+			       const bool direction);
+
+void CREATE_OF(lbits, sbits)(lbits *,
+			     const sbits op,
+			     const bool direction);
 
-void CREATE_OF(sail_bits, mach_bits)(sail_bits *,
-				     const mach_bits op,
-				     const mach_bits len,
-				     const bool direction);
+void RECREATE_OF(lbits, sbits)(lbits *,
+			       const sbits op,
+			       const bool direction);
 
-void RECREATE_OF(sail_bits, mach_bits)(sail_bits *,
-				       const mach_bits op,
-				       const mach_bits len,
-				       const bool direction);
+sbits CREATE_OF(sbits, lbits)(const lbits op, const bool direction);
+fbits CREATE_OF(fbits, lbits)(const lbits op, const bool direction);
+sbits CREATE_OF(sbits, fbits)(const fbits op, const uint64_t len, const bool direction);
 
-mach_bits CREATE_OF(mach_bits, sail_bits)(const sail_bits);
+/* Bitvector conversions */
 
-mach_bits CONVERT_OF(mach_bits, sail_bits)(const sail_bits, const bool);
+fbits CONVERT_OF(fbits, lbits)(const lbits, const bool);
+fbits CONVERT_OF(fbits, sbits)(const sbits, const bool);
 
-void CONVERT_OF(sail_bits, mach_bits)(sail_bits *, const mach_bits, const uint64_t, const bool);
+void CONVERT_OF(lbits, fbits)(lbits *, const fbits, const uint64_t, const bool);
+void CONVERT_OF(lbits, sbits)(lbits *, const sbits, const bool);
 
-void UNDEFINED(sail_bits)(sail_bits *, const sail_int len, const mach_bits bit);
-mach_bits UNDEFINED(mach_bits)(const unit);
+sbits CONVERT_OF(sbits, fbits)(const fbits, const uint64_t, const bool);
+sbits CONVERT_OF(sbits, lbits)(const lbits, const bool);
+
+void UNDEFINED(lbits)(lbits *, const sail_int len, const fbits bit);
+fbits UNDEFINED(fbits)(const unit);
+
+sbits undefined_sbits(void);
 
 /*
  * Wrapper around >> operator to avoid UB when shift amount is greater
  * than or equal to 64.
  */
-mach_bits safe_rshift(const mach_bits, const mach_bits);
+fbits safe_rshift(const fbits, const fbits);
 
 /*
  * Used internally to construct large bitvector literals.
  */
-void append_64(sail_bits *rop, const sail_bits op, const mach_bits chunk);
+void append_64(lbits *rop, const lbits op, const fbits chunk);
 
-void add_bits(sail_bits *rop, const sail_bits op1, const sail_bits op2);
-void sub_bits(sail_bits *rop, const sail_bits op1, const sail_bits op2);
+void add_bits(lbits *rop, const lbits op1, const lbits op2);
+void sub_bits(lbits *rop, const lbits op1, const lbits op2);
 
-void add_bits_int(sail_bits *rop, const sail_bits op1, const mpz_t op2);
-void sub_bits_int(sail_bits *rop, const sail_bits op1, const mpz_t op2);
+void add_bits_int(lbits *rop, const lbits op1, const mpz_t op2);
+void sub_bits_int(lbits *rop, const lbits op1, const mpz_t op2);
 
-void and_bits(sail_bits *rop, const sail_bits op1, const sail_bits op2);
-void or_bits(sail_bits *rop, const sail_bits op1, const sail_bits op2);
-void xor_bits(sail_bits *rop, const sail_bits op1, const sail_bits op2);
-void not_bits(sail_bits *rop, const sail_bits op);
+void and_bits(lbits *rop, const lbits op1, const lbits op2);
+void or_bits(lbits *rop, const lbits op1, const lbits op2);
+void xor_bits(lbits *rop, const lbits op1, const lbits op2);
+void not_bits(lbits *rop, const lbits op);
 
-void mults_vec(sail_bits *rop, const sail_bits op1, const sail_bits op2);
-void mult_vec(sail_bits *rop, const sail_bits op1, const sail_bits op2);
+void mults_vec(lbits *rop, const lbits op1, const lbits op2);
+void mult_vec(lbits *rop, const lbits op1, const lbits op2);
 
-void zeros(sail_bits *rop, const sail_int op);
+void zeros(lbits *rop, const sail_int op);
 
-void zero_extend(sail_bits *rop, const sail_bits op, const sail_int len);
-void sign_extend(sail_bits *rop, const sail_bits op, const sail_int len);
+void zero_extend(lbits *rop, const lbits op, const sail_int len);
+void sign_extend(lbits *rop, const lbits op, const sail_int len);
 
-void length_sail_bits(sail_int *rop, const sail_bits op);
+void length_lbits(sail_int *rop, const lbits op);
 
-bool eq_bits(const sail_bits op1, const sail_bits op2);
-bool EQUAL(sail_bits)(const sail_bits op1, const sail_bits op2);
-bool neq_bits(const sail_bits op1, const sail_bits op2);
+bool eq_bits(const lbits op1, const lbits op2);
+bool EQUAL(lbits)(const lbits op1, const lbits op2);
+bool neq_bits(const lbits op1, const lbits op2);
 
-void vector_subrange_sail_bits(sail_bits *rop,
-			       const sail_bits op,
+void vector_subrange_lbits(lbits *rop,
+			       const lbits op,
 			       const sail_int n_mpz,
 			       const sail_int m_mpz);
 
-void sail_truncate(sail_bits *rop, const sail_bits op, const sail_int len);
+void sail_truncate(lbits *rop, const lbits op, const sail_int len);
 
-mach_bits bitvector_access(const sail_bits op, const sail_int n_mpz);
+fbits bitvector_access(const lbits op, const sail_int n_mpz);
 
-void sail_unsigned(sail_int *rop, const sail_bits op);
-void sail_signed(sail_int *rop, const sail_bits op);
+void sail_unsigned(sail_int *rop, const lbits op);
+void sail_signed(sail_int *rop, const lbits op);
 
-mach_int fast_unsigned(const mach_bits);
+mach_int fast_unsigned(const fbits);
 
-void append(sail_bits *rop, const sail_bits op1, const sail_bits op2);
+void append(lbits *rop, const lbits op1, const lbits op2);
 
-void replicate_bits(sail_bits *rop, const sail_bits op1, const sail_int op2);
-mach_bits fast_replicate_bits(const mach_bits shift, const mach_bits v, const mach_int times);
+void replicate_bits(lbits *rop, const lbits op1, const sail_int op2);
+fbits fast_replicate_bits(const fbits shift, const fbits v, const mach_int times);
 
-void get_slice_int(sail_bits *rop, const sail_int len_mpz, const sail_int n, const sail_int start_mpz);
+void get_slice_int(lbits *rop, const sail_int len_mpz, const sail_int n, const sail_int start_mpz);
 
 void set_slice_int(sail_int *rop,
 		   const sail_int len_mpz,
 		   const sail_int n,
 		   const sail_int start_mpz,
-		   const sail_bits slice);
+		   const lbits slice);
 
-void vector_update_subrange_sail_bits(sail_bits *rop,
-				      const sail_bits op,
+void vector_update_subrange_lbits(lbits *rop,
+				      const lbits op,
 				      const sail_int n_mpz,
 				      const sail_int m_mpz,
-				      const sail_bits slice);
+				      const lbits slice);
 
-void slice(sail_bits *rop, const sail_bits op, const sail_int start_mpz, const sail_int len_mpz);
+void slice(lbits *rop, const lbits op, const sail_int start_mpz, const sail_int len_mpz);
 
-void set_slice(sail_bits *rop,
+sbits sslice(const fbits op, const mach_int start, const mach_int len);
+
+void set_slice(lbits *rop,
 	       const sail_int len_mpz,
 	       const sail_int slen_mpz,
-	       const sail_bits op,
+	       const lbits op,
 	       const sail_int start_mpz,
-	       const sail_bits slice);
+	       const lbits slice);
+
 
+void shift_bits_left(lbits *rop, const lbits op1, const lbits op2);
+void shift_bits_right(lbits *rop, const lbits op1, const lbits op2);
+void shift_bits_right_arith(lbits *rop, const lbits op1, const lbits op2);
 
-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(lbits *rop, const lbits op1, const sail_int op2);
+void shiftr(lbits *rop, const lbits op1, const sail_int 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(lbits*, lbits);
 
-void reverse_endianness(sail_bits*, sail_bits);
+bool eq_sbits(const sbits op1, const sbits op2);
+bool neq_sbits(const sbits op1, const sbits op2);
+sbits xor_sbits(const sbits op1, const sbits op2);
 
 /* ***** Sail reals ***** */
 
@@ -338,21 +354,21 @@ void string_take(sail_string *dst, sail_string s, sail_int len);
 /* ***** Printing ***** */
 
 void string_of_int(sail_string *str, const sail_int i);
-void string_of_sail_bits(sail_string *str, const sail_bits op);
-void string_of_mach_bits(sail_string *str, const mach_bits op);
-void decimal_string_of_sail_bits(sail_string *str, const sail_bits op);
-void decimal_string_of_mach_bits(sail_string *str, const mach_bits op);
+void string_of_lbits(sail_string *str, const lbits op);
+void string_of_fbits(sail_string *str, const fbits op);
+void decimal_string_of_lbits(sail_string *str, const lbits op);
+void decimal_string_of_fbits(sail_string *str, const fbits op);
 
 /*
  * Utility function not callable from Sail!
  */
 void fprint_bits(const sail_string pre,
-		 const sail_bits op,
+		 const lbits op,
 		 const sail_string post,
 		 FILE *stream);
 
-unit print_bits(const sail_string str, const sail_bits op);
-unit prerr_bits(const sail_string str, const sail_bits op);
+unit print_bits(const sail_string str, const lbits op);
+unit prerr_bits(const sail_string str, const lbits op);
 
 unit print(const sail_string str);
 unit print_endline(const sail_string str);
-- 
cgit v1.2.3


From 134ceff00b6a4837b133cb49b6d775161420dc62 Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Tue, 27 Nov 2018 21:23:48 +0000
Subject: Fix memory leak in string_of_bits

Should hopefully fix memory leak in RISC-V.

Also adds an optimization pass that removes copying structs and allows
some structs to simply alias each other and avoid copying their
contents. This requires knowing certain things about the lifetimes of
the structs involved, as can't free the struct if another variable is
referencing it - therefore we conservatively only apply this
optimization for variables that are lifted outside function
definitions, and should therefore never get freed until the model
exits - however this may cause issues outside ARMv8, as there may be
cases where a struct can exist within a variant type (which are not
yet subject to this lifting optimisation), that would break these
assumptions - therefore this optimisation is only enabled with the
-Oexperimental flag.
---
 lib/sail.c | 17 ++++++++++++++---
 1 file changed, 14 insertions(+), 3 deletions(-)

(limited to 'lib')

diff --git a/lib/sail.c b/lib/sail.c
index fbf230a6..28f318fa 100644
--- a/lib/sail.c
+++ b/lib/sail.c
@@ -1249,12 +1249,14 @@ void random_real(real *rop, const unit u)
 
 void string_of_int(sail_string *str, const sail_int i)
 {
+  free(*str);
   gmp_asprintf(str, "%Zd", i);
 }
 
-/* asprinf is a GNU extension, but it should exist on BSD */
+/* asprintf is a GNU extension, but it should exist on BSD */
 void string_of_fbits(sail_string *str, const fbits op)
 {
+  free(*str);
   int bytes = asprintf(str, "0x%" PRIx64, op);
   if (bytes == -1) {
     fprintf(stderr, "Could not print bits 0x%" PRIx64 "\n", op);
@@ -1263,15 +1265,23 @@ void string_of_fbits(sail_string *str, const fbits op)
 
 void string_of_lbits(sail_string *str, const lbits op)
 {
+  free(*str);
   if ((op.len % 4) == 0) {
-    gmp_asprintf(str, "0x%*0Zx", op.len / 4, *op.bits);
+    gmp_asprintf(str, "0x%*0ZX", op.len / 4, *op.bits);
   } else {
-    gmp_asprintf(str, "0b%*0Zb", op.len, *op.bits);
+    *str = (char *) malloc((op.len + 3) * sizeof(char));
+    (*str)[0] = '0';
+    (*str)[1] = 'b';
+    for (int i = 1; i <= op.len; ++i) {
+      (*str)[i + 1] = mpz_tstbit(*op.bits, op.len - i) + 0x30;
+    }
+    (*str)[op.len + 2] = '\0';
   }
 }
 
 void decimal_string_of_fbits(sail_string *str, const fbits op)
 {
+  free(*str);
   int bytes = asprintf(str, "%" PRId64, op);
   if (bytes == -1) {
     fprintf(stderr, "Could not print bits %" PRId64 "\n", op);
@@ -1280,6 +1290,7 @@ void decimal_string_of_fbits(sail_string *str, const fbits op)
 
 void decimal_string_of_lbits(sail_string *str, const lbits op)
 {
+  free(*str);
   gmp_asprintf(str, "%Z", *op.bits);
 }
 
-- 
cgit v1.2.3


From 4fd0c147e6c53ec64b7e4a8cd0324f6e8e56714f Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Fri, 30 Nov 2018 16:30:47 +0000
Subject: Improvements for ASL parser

- Fix pretty printing nested constraints

- Add flow typing for if condition then { throw exn }; ... blocks

- Add optimisations for bitvector concatenation in C
---
 lib/sail.c | 35 +++++++++++++++++++++++++++++++++++
 lib/sail.h |  8 ++++++++
 2 files changed, 43 insertions(+)

(limited to 'lib')

diff --git a/lib/sail.c b/lib/sail.c
index 28f318fa..24ff1fd2 100644
--- a/lib/sail.c
+++ b/lib/sail.c
@@ -778,6 +778,30 @@ void append(lbits *rop, const lbits op1, const lbits op2)
   mpz_ior(*rop->bits, *rop->bits, *op2.bits);
 }
 
+sbits append_sf(const sbits op1, const fbits op2, const uint64_t len)
+{
+  sbits rop;
+  rop.bits = (op1.bits << len) | op2;
+  rop.len = op1.len + len;
+  return rop;
+}
+
+sbits append_fs(const fbits op1, const uint64_t len, const sbits op2)
+{
+  sbits rop;
+  rop.bits = (op1 << op2.len) | op2.bits;
+  rop.len = len + op2.len;
+  return rop;
+}
+
+sbits append_ss(const sbits op1, const sbits op2)
+{
+  sbits rop;
+  rop.bits = (op1.bits << op2.len) | op2.bits;
+  rop.len = op1.len + op2.len;
+  return rop;
+}
+
 void replicate_bits(lbits *rop, const lbits op1, const mpz_t op2)
 {
   uint64_t op2_ui = mpz_get_ui(op2);
@@ -1398,3 +1422,14 @@ void get_time_ns(sail_int *rop, const unit u)
   mpz_mul_ui(*rop, *rop, 1000000000);
   mpz_add_ui(*rop, *rop, t.tv_nsec);
 }
+
+// ARM specific optimisations
+
+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);
+  mp_bitcnt_t n = x_bv.len;
+  mpz_set_ui(*rop->bits, safe_rshift(UINT64_MAX, 64l - (n - 1)) & z);
+  rop->len = n;
+}
diff --git a/lib/sail.h b/lib/sail.h
index 56df9740..49a5cf72 100644
--- a/lib/sail.h
+++ b/lib/sail.h
@@ -264,6 +264,10 @@ mach_int fast_unsigned(const fbits);
 
 void append(lbits *rop, const lbits op1, const lbits op2);
 
+sbits append_sf(const sbits, const fbits, const uint64_t);
+sbits append_fs(const fbits, const uint64_t, const sbits);
+sbits append_ss(const sbits, const sbits);
+
 void replicate_bits(lbits *rop, const lbits op1, const sail_int op2);
 fbits fast_replicate_bits(const fbits shift, const fbits v, const mach_int times);
 
@@ -384,3 +388,7 @@ unit sail_putchar(const sail_int op);
 /* ***** Misc ***** */
 
 void get_time_ns(sail_int*, const unit);
+
+/* ***** ARM optimisations ***** */
+
+void arm_align(lbits *, const lbits, const sail_int);
-- 
cgit v1.2.3


From 0363a325ca6c498e086519c4ecaf1f51dbff7f64 Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Fri, 30 Nov 2018 18:54:42 +0000
Subject: Parser tweaks and fixes

- Completely remove the nexp = nexp syntax in favour of nexp ==
  nexp. All our existing specs have already switched over. As part of
  this fix every test that used the old syntax, and update the
  generated aarch64 specs

- Remove the `type when constraint` syntax. It just makes changing the
  parser in any way really awkward.

- Change the syntax for declaring new types with multiple type
  parameters from:

  type foo('a : Type) ('n : Int), constraint = ...

  to

  type foo('a: Type, 'n: Int), constraint = ...

  This makes type declarations mimic function declarations, and makes
  the syntax for declaring types match the syntax for using types, as
  foo is used as foo(type, nexp). None of our specifications use types
  with multiple type parameters so this change doesn't actually break
  anything, other than some tests. The brackets around the type
  parameters are now mandatory.

- Experiment with splitting Type/Order type parameters from Int type
  parameters in the parser.

  Currently in a type bar(x, y, z) all of x, y, and z could be either
  numeric expressions, orders, or types. This means that in the parser
  we are severely restricted in what we can parse in numeric
  expressions because everything has to be parseable as a type (atyp)
  - it also means we can't introduce boolean type
  variables/expressions or other minisail features (like removing
  ticks from type variables!) because we are heavily constrained by
  what we can parse unambigiously due to how these different type
  parameters can be mixed and interleaved.

  There is now experimental syntax: vector::<'o, 'a>('n) <-->
  vector('n, 'o, 'a) which splits the type argument list into two
  between Type/Order-polymorphic arguments and Int-polymorphic
  arguments. The exact choice of delimiters isn't set in stone - ::<
  and > match generics in Rust. The obvious choices of < and > / [ and
  ] are ambigious in various ways.

  Using this syntax right now triggers a warning.

- Fix undefined behaviour in C compilation when concatenating a
  0-length vector with a 64-length vector.
---
 lib/arith.sail  | 4 ++--
 lib/option.sail | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)

(limited to 'lib')

diff --git a/lib/arith.sail b/lib/arith.sail
index db011f14..a3a80fc5 100644
--- a/lib/arith.sail
+++ b/lib/arith.sail
@@ -58,13 +58,13 @@ let elsize = shl_int(8, UInt(size))
 THIS ensures that in this case the typechecker knows that the end result will be a value in the set `{8, 16, 32, 64}`
 */
 val _shl8 = {c: "shl_mach_int", _: "shl_int"} :
-  forall 'n, 0 <= 'n <= 3. (int(8), int('n)) -> int('m) with 'm in {8, 16, 32, 64}
+  forall 'n, 0 <= 'n <= 3. (int(8), int('n)) -> {'m, 'm in {8, 16, 32, 64}. int('m)}
 
 /*!
 Similarly, we can shift 32 by either 0 or 1 to get a value in `{32, 64}`
 */
 val _shl32 = {c: "shl_mach_int", _: "shl_int"} :
-  forall 'n, 'n in {0, 1}. (int(32), int('n)) -> int('m) with 'm in {32, 64}
+  forall 'n, 'n in {0, 1}. (int(32), int('n)) -> {'m, 'm in {32, 64}. int('m)}
 
 val _shl_int = "shl_int" : (int, int) -> int
 
diff --git a/lib/option.sail b/lib/option.sail
index 3869167b..514cf7ba 100644
--- a/lib/option.sail
+++ b/lib/option.sail
@@ -6,7 +6,7 @@ $define _OPTION
 // this won't work - also no other type should be created with
 // constructors named Some or None.
 
-union option ('a : Type) = {
+union option('a: Type) = {
   Some : 'a,
   None : unit
 }
-- 
cgit v1.2.3


From 5bc5f5dee8921f8d24260dae54177e00c291fcb1 Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Mon, 10 Dec 2018 20:39:16 +0000
Subject: Various changes:

* Improve type inference for numeric if statements (if_infer test)

* Correctly handle constraints for existentially quantified constructors (constraint_ctor test)

* Canonicalise all numeric types in function arguments, which
  triggers some weird edge cases between parametric polymorphism and
  subtyping of numeric arguments

* Because of this eq_int, eq_range, and eq_atom etc become identical

* Avoid duplicating destruct_exist in Env

* Handle some odd subtyping cases better
---
 lib/flow.sail | 37 ++++++-------------------------------
 1 file changed, 6 insertions(+), 31 deletions(-)

(limited to 'lib')

diff --git a/lib/flow.sail b/lib/flow.sail
index cdc6b2fd..b9653828 100644
--- a/lib/flow.sail
+++ b/lib/flow.sail
@@ -20,34 +20,9 @@ val not_bool = {coq: "negb", _: "not"} : bool -> bool
    or_bool that are not shown here. */
 val and_bool = {coq: "andb", _: "and_bool"} : (bool, bool) -> bool
 val or_bool = {coq: "orb", _: "or_bool"} : (bool, bool) -> bool
-
-val eq_atom = {ocaml: "eq_int", lem: "eq", c: "eq_int", coq: "Z.eqb"} : forall 'n 'm. (atom('n), atom('m)) -> bool
-
-val neq_atom = {lem: "neq", coq: "neq_atom"} : forall 'n 'm. (atom('n), atom('m)) -> bool
-
-function neq_atom (x, y) = not_bool(eq_atom(x, y))
-
-val lteq_atom = {coq: "Z.leb", _: "lteq"} : forall 'n 'm. (atom('n), atom('m)) -> bool
-val gteq_atom = {coq: "Z.geb", _: "gteq"} : forall 'n 'm. (atom('n), atom('m)) -> bool
-val lt_atom = {coq: "Z.ltb", _: "lt"}     : forall 'n 'm. (atom('n), atom('m)) -> bool
-val gt_atom = {coq: "Z.gtb", _: "gt"}     : forall 'n 'm. (atom('n), atom('m)) -> bool
-
-val lt_range_atom = {coq: "ltb_range_l", _: "lt"}     : forall 'n 'm 'o. (range('n, 'm), atom('o)) -> bool
-val lteq_range_atom = {coq: "leb_range_l", _: "lteq"} : forall 'n 'm 'o. (range('n, 'm), atom('o)) -> bool
-val gt_range_atom = {coq: "gtb_range_l", _: "gt"}     : forall 'n 'm 'o. (range('n, 'm), atom('o)) -> bool
-val gteq_range_atom = {coq: "geb_range_l", _: "gteq"} : forall 'n 'm 'o. (range('n, 'm), atom('o)) -> bool
-val lt_atom_range = {coq: "ltb_range_r", _: "lt"}     : forall 'n 'm 'o. (atom('n), range('m, 'o)) -> bool
-val lteq_atom_range = {coq: "leb_range_r", _: "lteq"} : forall 'n 'm 'o. (atom('n), range('m, 'o)) -> bool
-val gt_atom_range = {coq: "gtb_range_r", _: "gt"}     : forall 'n 'm 'o. (atom('n), range('m, 'o)) -> bool
-val gteq_atom_range = {coq: "geb_range_r", _: "gteq"} : forall 'n 'm 'o. (atom('n), range('m, 'o)) -> bool
-
-val eq_range = {ocaml: "eq_int", lem: "eq", c: "eq_int", coq: "eq_range"} : forall 'n 'm 'o 'p. (range('n, 'm), range('o, 'p)) -> bool
 val eq_int = {ocaml: "eq_int", lem: "eq", c: "eq_int", coq: "Z.eqb"} : (int, int) -> bool
 val eq_bool = {ocaml: "eq_bool", lem: "eq", c: "eq_bool", coq: "Bool.eqb"} : (bool, bool) -> bool
 
-val neq_range = {lem: "neq"} : forall 'n 'm 'o 'p. (range('n, 'm), range('o, 'p)) -> bool
-function neq_range (x, y) = not_bool(eq_range(x, y))
-
 val neq_int = {lem: "neq"} : (int, int) -> bool
 function neq_int (x, y) = not_bool(eq_int(x, y))
 
@@ -59,15 +34,15 @@ val gteq_int = {coq: "Z.geb", _:"gteq"} : (int, int) -> bool
 val lt_int = {coq: "Z.ltb", _:"lt"} : (int, int) -> bool
 val gt_int = {coq: "Z.gtb", _:"gt"} : (int, int) -> bool
 
-overload operator == = {eq_atom, eq_range, eq_int, eq_bit, eq_bool, eq_unit}
-overload operator != = {neq_atom, neq_range, neq_int, neq_bool}
+overload operator == = {eq_int, eq_bit, eq_bool, eq_unit}
+overload operator != = {neq_int, neq_bool}
 overload operator | = {or_bool}
 overload operator & = {and_bool}
 
-overload operator <= = {lteq_atom, lteq_range_atom, lteq_atom_range, lteq_int}
-overload operator < = {lt_atom, lt_range_atom, lt_atom_range, lt_int}
-overload operator >= = {gteq_atom, gteq_range_atom, gteq_atom_range, gteq_int}
-overload operator > = {gt_atom, gt_range_atom, gt_atom_range, gt_int}
+overload operator <= = {lteq_int}
+overload operator < = {lt_int}
+overload operator >= = {gteq_int}
+overload operator > = {gt_int}
 
 $ifdef TEST
 
-- 
cgit v1.2.3


From c0500a16891e57b2856e47a3c233cd0c1d247a70 Mon Sep 17 00:00:00 2001
From: Alasdair
Date: Tue, 11 Dec 2018 01:12:50 +0000
Subject: Fix most remaining tests on branch

---
 lib/flow.sail | 14 --------------
 1 file changed, 14 deletions(-)

(limited to 'lib')

diff --git a/lib/flow.sail b/lib/flow.sail
index b9653828..5c182af2 100644
--- a/lib/flow.sail
+++ b/lib/flow.sail
@@ -44,18 +44,4 @@ overload operator < = {lt_int}
 overload operator >= = {gteq_int}
 overload operator > = {gt_int}
 
-$ifdef TEST
-
-val __flow_test : forall 'n 'm. (atom('n), atom('m)) -> unit
-
-function __flow_test (x, y) = {
-  if lteq_atom(x, y) then {
-    _prove(constraint('n <= 'm))
-  } else {
-    _prove(constraint('n > 'm))
-  }
-}
-
-$endif
-
 $endif
-- 
cgit v1.2.3


From 4f20163965e7c336f28740628fa9d64528006861 Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Tue, 11 Dec 2018 11:54:36 +0000
Subject: Initial attempt at using termination measures in Coq This only
 applies to recursive functions and uses the termination measure merely as a
 limit to the recursive call depth, rather than proving the measure correct.

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

(limited to 'lib')

diff --git a/lib/coq/Sail2_prompt.v b/lib/coq/Sail2_prompt.v
index 1b12f360..8c0ca33c 100644
--- a/lib/coq/Sail2_prompt.v
+++ b/lib/coq/Sail2_prompt.v
@@ -1,7 +1,7 @@
 (*Require Import Sail_impl_base*)
 Require Import Sail2_values.
 Require Import Sail2_prompt_monad.
-
+Require Export ZArith.Zwf.
 Require Import List.
 Import ListNotations.
 (*
@@ -77,6 +77,13 @@ match b with
   | BU => undefined_bool tt
 end.
 
+(* For termination of recursive functions. *)
+Lemma _limit_is_limit {_limit : Z} : _limit >? 0 = true -> Zwf 0 (_limit - 1) _limit.
+intros.
+prepare_for_solver.
+red.
+omega.
+Qed.
 
 (*val whileM : forall 'rv 'vars 'e. 'vars -> ('vars -> monad 'rv bool 'e) ->
                 ('vars -> monad 'rv 'vars 'e) -> monad 'rv 'vars 'e
-- 
cgit v1.2.3


From ab4b9ca4f7cab45b6a2a13d0ef125dcf9c276a06 Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Tue, 11 Dec 2018 19:54:14 +0000
Subject: Fix all tests with type checking changes

---
 lib/sail.c | 23 +++++++++++++++++++++++
 lib/sail.h |  3 +++
 2 files changed, 26 insertions(+)

(limited to 'lib')

diff --git a/lib/sail.c b/lib/sail.c
index 24ff1fd2..f897fc11 100644
--- a/lib/sail.c
+++ b/lib/sail.c
@@ -232,6 +232,12 @@ void CREATE_OF(sail_int, sail_string)(sail_int *rop, sail_string str)
   mpz_init_set_str(*rop, str, 10);
 }
 
+inline
+void CONVERT_OF(sail_int, sail_string)(sail_int *rop, sail_string str)
+{
+  mpz_set_str(*rop, str, 10);
+}
+
 inline
 void RECREATE_OF(sail_int, sail_string)(mpz_t *rop, sail_string str)
 {
@@ -1246,6 +1252,23 @@ void CREATE_OF(real, sail_string)(real *rop, const sail_string op)
   mpq_add(*rop, *rop, sail_lib_tmp_real);
 }
 
+void CONVERT_OF(real, sail_string)(real *rop, const sail_string op)
+{
+  int decimal;
+  int total;
+
+  gmp_sscanf(op, "%Zd.%n%Zd%n", sail_lib_tmp1, &decimal, sail_lib_tmp2, &total);
+
+  int len = total - decimal;
+  mpz_ui_pow_ui(sail_lib_tmp3, 10, len);
+  mpz_set(mpq_numref(*rop), sail_lib_tmp2);
+  mpz_set(mpq_denref(*rop), sail_lib_tmp3);
+  mpq_canonicalize(*rop);
+  mpz_set(mpq_numref(sail_lib_tmp_real), sail_lib_tmp1);
+  mpz_set_ui(mpq_denref(sail_lib_tmp_real), 1);
+  mpq_add(*rop, *rop, sail_lib_tmp_real);
+}
+
 unit print_real(const sail_string str, const real op)
 {
   gmp_printf("%s%Qd\n", str, op);
diff --git a/lib/sail.h b/lib/sail.h
index 49a5cf72..1310dd72 100644
--- a/lib/sail.h
+++ b/lib/sail.h
@@ -96,6 +96,8 @@ mach_int CREATE_OF(mach_int, sail_int)(const sail_int);
 void CREATE_OF(sail_int, sail_string)(sail_int *, const sail_string);
 void RECREATE_OF(sail_int, sail_string)(mpz_t *, const sail_string);
 
+void CONVERT_OF(sail_int, sail_string)(sail_int *, const sail_string);
+
 mach_int CONVERT_OF(mach_int, sail_int)(const sail_int);
 void CONVERT_OF(sail_int, mach_int)(sail_int *, const mach_int);
 
@@ -317,6 +319,7 @@ typedef mpq_t real;
 SAIL_BUILTIN_TYPE(real);
 
 void CREATE_OF(real, sail_string)(real *rop, const sail_string op);
+void CONVERT_OF(real, sail_string)(real *rop, const sail_string op);
 
 void UNDEFINED(real)(real *rop, unit u);
 
-- 
cgit v1.2.3


From f8d88d4cf2439f4920fa948b054c4f0b2899e368 Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Wed, 12 Dec 2018 18:23:00 +0000
Subject: Move much of recursive function termination to a rewrite It now
 includes updating the effects so that morally pure recursive functions can be
 turned into this impure termination-by-assertion form.

---
 lib/coq/Sail2_prompt.v | 11 ++++++-----
 1 file changed, 6 insertions(+), 5 deletions(-)

(limited to 'lib')

diff --git a/lib/coq/Sail2_prompt.v b/lib/coq/Sail2_prompt.v
index 8c0ca33c..85ca95f6 100644
--- a/lib/coq/Sail2_prompt.v
+++ b/lib/coq/Sail2_prompt.v
@@ -77,13 +77,14 @@ match b with
   | BU => undefined_bool tt
 end.
 
-(* For termination of recursive functions. *)
-Lemma _limit_is_limit {_limit : Z} : _limit >? 0 = true -> Zwf 0 (_limit - 1) _limit.
-intros.
-prepare_for_solver.
+(* For termination of recursive functions.  We don't name assertions, so use
+   the type class mechanism to find it. *)
+Definition _limit_reduces {_limit} (_acc:Acc (Zwf 0) _limit) `{ArithFact (_limit >= 0)} : Acc (Zwf 0) (_limit - 1).
+refine (Acc_inv _acc _).
+destruct H.
 red.
 omega.
-Qed.
+Defined.
 
 (*val whileM : forall 'rv 'vars 'e. 'vars -> ('vars -> monad 'rv bool 'e) ->
                 ('vars -> monad 'rv 'vars 'e) -> monad 'rv 'vars 'e
-- 
cgit v1.2.3


From 7bbed580db0abeaa1acaa47610f01571ffe75ff4 Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Thu, 13 Dec 2018 19:06:50 +0000
Subject: Fix issue with sizeof-rewriting and monomorphisation

Sizeof-rewriting could introduce extra arguments to functions that
instantiate_simple_equations could fill in with overly complicated
types, causing unification to fail when building lem.
---
 lib/mono_rewrites.sail | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

(limited to 'lib')

diff --git a/lib/mono_rewrites.sail b/lib/mono_rewrites.sail
index 9e837e10..0825f9d0 100644
--- a/lib/mono_rewrites.sail
+++ b/lib/mono_rewrites.sail
@@ -63,7 +63,7 @@ function slice_slice_concat (xs, i, l, ys, i', l') = {
   extzv(xs) << l' | extzv(ys)
 }
 
-val slice_zeros_concat : forall 'n 'p 'q 'r, 'r = 'p + 'q & 'n >= 0 & 'p >= 0 & 'q >= 0 & 'r >= 0.
+val slice_zeros_concat : forall 'n 'p 'q 'r, 'r == 'p + 'q & 'n >= 0 & 'p >= 0 & 'q >= 0 & 'r >= 0.
   (bits('n), int, atom('p), atom('q)) -> bits('r) effect pure
 
 function slice_zeros_concat (xs, i, l, l') = {
@@ -82,13 +82,15 @@ function subrange_subrange_eq (xs, i, j, ys, i', j') = {
   xs == ys
 }
 
-val subrange_subrange_concat : forall 'n 'o 'p 'm 'q 'r 's, 's = 'o - ('p - 1) + 'q - ('r - 1) & 'n >= 0 & 'm >= 0.
+val subrange_subrange_concat : forall 'n 'o 'p 'm 'q 'r 's, 's == 'o - ('p - 1) + 'q - ('r - 1) & 'n >= 0 & 'm >= 0.
   (bits('n), atom('o), atom('p), bits('m), atom('q), atom('r)) -> bits('s) effect pure
 
 function subrange_subrange_concat (xs, i, j, ys, i', j') = {
   let xs = (xs & slice_mask(j,i-j+1)) >> j in
   let ys = (ys & slice_mask(j',i'-j'+1)) >> j' in
-  extzv(xs) << (i' - j' + 1) | extzv(ys)
+  // We need to avoid sizeof-rewriting
+  // extzv(xs) << (i' - j' + 1) | extzv(ys)
+  extz_vec(i - (j - 1) + i' - (j' - 1), xs) << (i' - j' + 1) | extz_vec(i - (j - 1) + i' - (j' - 1), ys)
 }
 
 val place_subrange : forall 'n 'm, 'n >= 0 & 'm >= 0.
-- 
cgit v1.2.3


From cbd4eedf0d278572e70b04d9e9ef8750c4cae0a4 Mon Sep 17 00:00:00 2001
From: Thomas Bauereiss
Date: Thu, 13 Dec 2018 20:37:36 +0000
Subject: Remove redundant zero extensions more aggressively in mono rewrites

subrange_subrange_concat does a zero extension internally, so another
zero extension of its result is redundant and can lead to a type error
in Lem (because Lem's type system cannot calculate the length of the
intermediate result of subrange_subrange_concat).
---
 lib/mono_rewrites.sail | 6 ++----
 1 file changed, 2 insertions(+), 4 deletions(-)

(limited to 'lib')

diff --git a/lib/mono_rewrites.sail b/lib/mono_rewrites.sail
index 0825f9d0..93ad3db5 100644
--- a/lib/mono_rewrites.sail
+++ b/lib/mono_rewrites.sail
@@ -82,15 +82,13 @@ function subrange_subrange_eq (xs, i, j, ys, i', j') = {
   xs == ys
 }
 
-val subrange_subrange_concat : forall 'n 'o 'p 'm 'q 'r 's, 's == 'o - ('p - 1) + 'q - ('r - 1) & 'n >= 0 & 'm >= 0.
+val subrange_subrange_concat : forall 'n 'o 'p 'm 'q 'r 's, 's >= 0 & 'n >= 0 & 'm >= 0.
   (bits('n), atom('o), atom('p), bits('m), atom('q), atom('r)) -> bits('s) effect pure
 
 function subrange_subrange_concat (xs, i, j, ys, i', j') = {
   let xs = (xs & slice_mask(j,i-j+1)) >> j in
   let ys = (ys & slice_mask(j',i'-j'+1)) >> j' in
-  // We need to avoid sizeof-rewriting
-  // extzv(xs) << (i' - j' + 1) | extzv(ys)
-  extz_vec(i - (j - 1) + i' - (j' - 1), xs) << (i' - j' + 1) | extz_vec(i - (j - 1) + i' - (j' - 1), ys)
+  extzv(xs) << (i' - j' + 1) | extzv(ys)
 }
 
 val place_subrange : forall 'n 'm, 'n >= 0 & 'm >= 0.
-- 
cgit v1.2.3


From 6f8d5bdacd5accbd4aa689071304d3255792030b Mon Sep 17 00:00:00 2001
From: Robert Norton
Date: Fri, 14 Dec 2018 11:06:31 +0000
Subject: Add truncateLSB builtin useful for implementing Cheri Concentrate.
 Also add bool_of_bit and bit_of_bool in sail_lib

---
 lib/sail.c          | 10 ++++++++++
 lib/sail.h          |  1 +
 lib/vector_dec.sail | 13 +++++++++++++
 3 files changed, 24 insertions(+)

(limited to 'lib')

diff --git a/lib/sail.c b/lib/sail.c
index f897fc11..0fcb5d55 100644
--- a/lib/sail.c
+++ b/lib/sail.c
@@ -741,6 +741,16 @@ void sail_truncate(lbits *rop, const lbits op, const sail_int len)
   normalize_lbits(rop);
 }
 
+void sail_truncateLSB(lbits *rop, const lbits op, const sail_int len)
+{
+  uint64_t rlen = mpz_get_ui(len);
+  assert(op.len >= rlen);
+  rop->len = rlen;
+  // similar to vector_subrange_lbits above -- right shift LSBs away
+  mpz_fdiv_q_2exp(*rop->bits, *op.bits, op.len - rlen);
+  normalize_lbits(rop);
+}
+
 fbits bitvector_access(const lbits op, const sail_int n_mpz)
 {
   uint64_t n = mpz_get_ui(n_mpz);
diff --git a/lib/sail.h b/lib/sail.h
index 1310dd72..53b9c6be 100644
--- a/lib/sail.h
+++ b/lib/sail.h
@@ -256,6 +256,7 @@ void vector_subrange_lbits(lbits *rop,
 			       const sail_int m_mpz);
 
 void sail_truncate(lbits *rop, const lbits op, const sail_int len);
+void sail_truncateLSB(lbits *rop, const lbits op, const sail_int len);
 
 fbits bitvector_access(const lbits op, const sail_int n_mpz);
 
diff --git a/lib/vector_dec.sail b/lib/vector_dec.sail
index 6953264f..4e4bad5a 100644
--- a/lib/vector_dec.sail
+++ b/lib/vector_dec.sail
@@ -35,6 +35,9 @@ val sail_sign_extend = "sign_extend" : forall 'n 'm, 'm >= 'n. (bits('n), atom('
 
 val sail_zero_extend = "zero_extend" : forall 'n 'm, 'm >= 'n. (bits('n), atom('m)) -> bits('m)
 
+/*!
+THIS`(v, n)` truncates `v`, keeping only the _least_ significant `n` bits.
+ */
 val truncate = {
   ocaml: "vector_truncate",
   lem: "vector_truncate",
@@ -42,6 +45,16 @@ val truncate = {
   c: "sail_truncate"
 } : forall 'm 'n, 'm >= 0 & 'm <= 'n. (vector('n, dec, bit), atom('m)) -> vector('m, dec, bit)
 
+/*!
+THIS`(v, n)` truncates `v`, keeping only the _most_ significant `n` bits.
+ */
+val truncateLSB = {
+  ocaml: "vector_truncateLSB",
+  lem: "vector_truncateLSB",
+  coq: "vector_truncateLSB",
+  c: "sail_truncateLSB"
+} : forall 'm 'n, 'm >= 0 & 'm <= 'n. (vector('n, dec, bit), atom('m)) -> vector('m, dec, bit)
+
 val sail_mask : forall 'len 'v, 'len >= 0 & 'v >= 0. (atom('len), vector('v, dec, bit)) -> vector('len, dec, bit)
 
 function sail_mask(len, v) = if len <= length(v) then truncate(v, len) else sail_zero_extend(v, len)
-- 
cgit v1.2.3


From e5d108332cf700f73ea7b7527d0ae6006b0944c5 Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Mon, 17 Dec 2018 12:23:30 +0000
Subject: Adapt Coq and termination measure support to typechecker changes Also
 output termination measures in Sail printer

---
 lib/coq/Sail2_string.v | 8 ++++----
 lib/coq/Sail2_values.v | 8 ++++----
 2 files changed, 8 insertions(+), 8 deletions(-)

(limited to 'lib')

diff --git a/lib/coq/Sail2_string.v b/lib/coq/Sail2_string.v
index a02556b2..0a00f8d7 100644
--- a/lib/coq/Sail2_string.v
+++ b/lib/coq/Sail2_string.v
@@ -7,12 +7,12 @@ Definition string_startswith s expected :=
   let prefix := String.substring 0 (String.length expected) s in
   generic_eq prefix expected.
 
-Definition string_drop s (n : {n : Z & ArithFact (n >= 0)}) :=
-  let n := Z.to_nat (projT1 n) in
+Definition string_drop s (n : Z) `{ArithFact (n >= 0)} :=
+  let n := Z.to_nat n in
   String.substring n (String.length s - n) s.
 
-Definition string_take s (n : {n : Z & ArithFact (n >= 0)}) :=
-  let n := Z.to_nat (projT1 n) in
+Definition string_take s (n : Z) `{ArithFact (n >= 0)} :=
+  let n := Z.to_nat n in
   String.substring 0 n s.
 
 Definition string_length s : {n : Z & ArithFact (n >= 0)} :=
diff --git a/lib/coq/Sail2_values.v b/lib/coq/Sail2_values.v
index aebc3376..37e75961 100644
--- a/lib/coq/Sail2_values.v
+++ b/lib/coq/Sail2_values.v
@@ -1790,11 +1790,11 @@ match a with
 | None => None
 end.
 
-Definition sub_nat (x : {x : Z & ArithFact (x >= 0)}) (y : {y : Z & ArithFact (y >= 0)}) :
+Definition sub_nat (x : Z) `{ArithFact (x >= 0)} (y : Z) `{ArithFact (y >= 0)} :
   {z : Z & ArithFact (z >= 0)} :=
-  let z := projT1 x - projT1 y in
+  let z := x - y in
   if sumbool_of_bool (z >=? 0) then build_ex z else build_ex 0.
 
-Definition min_nat (x : {x : Z & ArithFact (x >= 0)}) (y : {y : Z & ArithFact (y >= 0)}) :
+Definition min_nat (x : Z) `{ArithFact (x >= 0)} (y : Z) `{ArithFact (y >= 0)} :
   {z : Z & ArithFact (z >= 0)} :=
-  build_ex (Z.min (projT1 x) (projT1 y)).
+  build_ex (Z.min x y).
-- 
cgit v1.2.3


From 66b55de7e24ab546aff3eba17d21b86d47306a6d Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Tue, 18 Dec 2018 10:30:27 +0000
Subject: Coq: handle existentials in hypotheses during solving, add max_nat,
 better casts

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

(limited to 'lib')

diff --git a/lib/coq/Sail2_values.v b/lib/coq/Sail2_values.v
index 37e75961..b7e9bbc9 100644
--- a/lib/coq/Sail2_values.v
+++ b/lib/coq/Sail2_values.v
@@ -1125,6 +1125,10 @@ repeat
   end.
 *)
 
+(* The linear solver doesn't like existentials. *)
+Ltac destruct_exists :=
+  repeat match goal with H:@ex Z _ |- _ => destruct H end.
+
 Ltac prepare_for_solver :=
 (*dump_context;*)
  clear_irrelevant_defns;
@@ -1134,6 +1138,7 @@ Ltac prepare_for_solver :=
  extract_properties;
  repeat match goal with w:mword ?n |- _ => apply ArithFact_mword in w end;
  unwrap_ArithFacts;
+ destruct_exists;
  unbool_comparisons;
  unfold_In; (* after unbool_comparisons to deal with && and || *)
  reduce_list_lengths;
@@ -1798,3 +1803,7 @@ Definition sub_nat (x : Z) `{ArithFact (x >= 0)} (y : Z) `{ArithFact (y >= 0)} :
 Definition min_nat (x : Z) `{ArithFact (x >= 0)} (y : Z) `{ArithFact (y >= 0)} :
   {z : Z & ArithFact (z >= 0)} :=
   build_ex (Z.min x y).
+
+Definition max_nat (x : Z) `{ArithFact (x >= 0)} (y : Z) `{ArithFact (y >= 0)} :
+  {z : Z & ArithFact (z >= 0)} :=
+  build_ex (Z.max x y).
-- 
cgit v1.2.3


From 502e0010ae4dfe24dde9dba0174d62540f9fc993 Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Wed, 19 Dec 2018 11:17:15 +0000
Subject: Coq: add zeros library function (used by MIPS)

---
 lib/coq/Sail2_operators_mwords.v | 7 +++++++
 1 file changed, 7 insertions(+)

(limited to 'lib')

diff --git a/lib/coq/Sail2_operators_mwords.v b/lib/coq/Sail2_operators_mwords.v
index e37e9d26..809f9d89 100644
--- a/lib/coq/Sail2_operators_mwords.v
+++ b/lib/coq/Sail2_operators_mwords.v
@@ -172,6 +172,13 @@ Definition zero_extend {a} (v : mword a) (n : Z) `{ArithFact (n >= a)} : mword n
 
 Definition sign_extend {a} (v : mword a) (n : Z) `{ArithFact (n >= a)} : mword n := exts_vec n v.
 
+Definition zeros (n : Z) `{ArithFact (n >= 0)} : mword n.
+refine (cast_to_mword (Word.wzero (Z.to_nat n)) _).
+unwrap_ArithFacts.
+apply Z2Nat.id.
+auto with zarith.
+Defined.
+
 Lemma truncate_eq {m n} : m >= 0 -> m <= n -> (Z.to_nat n = Z.to_nat m + (Z.to_nat n - Z.to_nat m))%nat.
 intros.
 assert ((Z.to_nat m <= Z.to_nat n)%nat).
-- 
cgit v1.2.3


From 8dbe18b8976e30fa88814542ea913ddc4193cd8b Mon Sep 17 00:00:00 2001
From: Shaked Flur
Date: Sat, 22 Dec 2018 15:40:32 +0000
Subject: Added RISC-V fence.tso

---
 lib/regfp.sail | 1 +
 1 file changed, 1 insertion(+)

(limited to 'lib')

diff --git a/lib/regfp.sail b/lib/regfp.sail
index fcf10850..cc017585 100644
--- a/lib/regfp.sail
+++ b/lib/regfp.sail
@@ -79,6 +79,7 @@ enum barrier_kind = {
   Barrier_RISCV_rw_r,
   Barrier_RISCV_r_w,
   Barrier_RISCV_w_r,
+  Barrier_RISCV_tso,
   Barrier_RISCV_i,
   Barrier_x86_MFENCE
 }
-- 
cgit v1.2.3


From cb5773b3b4d69750f9693e9c9f4e20de5e06ed3b Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Thu, 20 Dec 2018 16:41:39 +0000
Subject: Coq: make solver try hints before stripping away existentials (which
 allows us to avoid a Coq bug where the proof isn't recorded correctly)

---
 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 b7e9bbc9..e3e039c2 100644
--- a/lib/coq/Sail2_values.v
+++ b/lib/coq/Sail2_values.v
@@ -1180,6 +1180,8 @@ prepare_for_solver;
  [ match goal with |- ArithFact (?x _) => is_evar x; idtac "Warning: unknown constraint"; constructor; exact (I : (fun _ => True) _) end
  | apply ArithFact_mword; assumption
  | constructor; omega with Z
+   (* Try sail hints before dropping the existential *)
+ | 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
  | constructor; idtac "Unable to solve constraint"; dump_context; fail
-- 
cgit v1.2.3