Add patches to (monomorphised) AArch64

- Initialise fault typ field of result record to avoid an unitialised read that
  can lead to an early return with a fault.  This looks like a bug in the ASL
  specification (the ASL tests probably assume that this field is initialised
  with Fault_None).

- In ZeroExtend_slice_append (one of the helper functions for monomorphisation
  rewrites), use extzv instead of ZeroExtend.  It allows not only extension,
  but also truncation, and in AArch64_TranslationTableWalk the
  ZeroExtend_slice_append function is used to construct a 52 bit physical address
  using parts of the 64 bit input address.

- Use the Lem library function for reversing endianness

4 files changed, 17 insertions, 6 deletions

diff --git a/aarch64/mono/BigEndianReverse.sail b/aarch64/mono/BigEndianReverse.sail
index 23b222f4..05ba4a72 100644
--- a/aarch64/mono/BigEndianReverse.sail
+++ b/aarch64/mono/BigEndianReverse.sail
@@ -1,4 +1,4 @@
-val BigEndianReverse : forall ('width : Int), 'width >= 0 & 'width >= 0.
+val BigEndianReverse = {lem: "BigEndianReverse"} : forall ('width : Int), 'width >= 0 & 'width >= 0.
   bits('width) -> bits('width) effect {escape}
 
 function BigEndianReverse value_name = {
diff --git a/aarch64/mono/_slice.sail b/aarch64/mono/_slice.sail
index 2bac9f8c..50e99028 100644
--- a/aarch64/mono/_slice.sail
+++ b/aarch64/mono/_slice.sail
@@ -21,8 +21,8 @@ val ZeroExtend_slice_append : forall 'n 'm 'o, 'n >= 0 & 'm >= 0 & 'o >= 0.
 function ZeroExtend_slice_append (xs, i, 'l, ys) = {
   assert(constraint('l >= 0));
   let xs = xs & slice_mask(i,l) in
-  let xs : bits('o) = ZeroExtend(xs >> i) << 'm in
-  let ys : bits('o) = ZeroExtend(ys) in
+  let xs : bits('o) = extzv(xs >> i) << 'm in
+  let ys : bits('o) = extzv(ys) in
   xs | ys
 }
 
diff --git a/aarch64/mono/aarch64_extras.lem b/aarch64/mono/aarch64_extras.lem
index f9027593..fb1e4861 100644
--- a/aarch64/mono/aarch64_extras.lem
+++ b/aarch64/mono/aarch64_extras.lem
@@ -58,6 +58,9 @@ let hex_slice v len lo =
    let bs = ext_list false (len + lo) bs in
    return (of_bools (subrange_list false bs hi lo))
 
+val BigEndianReverse : forall 'rv 'n 'e. Size 'n => mword 'n -> monad 'rv (mword 'n) 'e
+let BigEndianReverse w = return (reverse_endianness w)
+
 let internal_pick vs = return (head vs)
 
 (* Use constants for undefined values for now *)
diff --git a/aarch64/mono/demo/aarch64_no_vector/spec.sail b/aarch64/mono/demo/aarch64_no_vector/spec.sail
index 7f3fb09e..ab68c973 100644
--- a/aarch64/mono/demo/aarch64_no_vector/spec.sail
+++ b/aarch64/mono/demo/aarch64_no_vector/spec.sail
@@ -1943,7 +1943,7 @@ function EncodeLDFSC (typ, 'level) = {
   return(result)
 }
 
-val BigEndianReverse : forall ('width : Int), 'width >= 0 & 'width >= 0.
+val BigEndianReverse = {lem: "BigEndianReverse"} : forall ('width : Int), 'width >= 0 & 'width >= 0.
   bits('width) -> bits('width) effect {escape}
 
 function BigEndianReverse value_name = {
@@ -5275,8 +5275,8 @@ val ZeroExtend_slice_append : forall 'n 'm 'o, 'n >= 0 & 'm >= 0 & 'o >= 0.
 function ZeroExtend_slice_append (xs, i, 'l, ys) = {
   assert(constraint('l >= 0));
   let xs = xs & slice_mask(i,l) in
-  let xs : bits('o) = ZeroExtend(xs >> i) << 'm in
-  let ys : bits('o) = ZeroExtend(ys) in
+  let xs : bits('o) = extzv(xs >> i) << 'm in
+  let ys : bits('o) = extzv(ys) in
   xs | ys
 }
 
@@ -5288,6 +5288,14 @@ function AArch64_TranslationTableWalk (ipaddress, vaddress, acctype, iswrite, se
   descaddr : AddressDescriptor = undefined;
   baseregister : bits(64) = undefined;
   inputaddr : bits(64) = undefined;
+  /* Initialise typ field of FaultRecord; otherwise, there might be an
+   * read of the uninitialised value that can lead to an early return with a
+   * fault (when checking the return value of the second stage translation in
+   * the loop below, if second stage translation is disabled).  This looks like
+   * a bug in the ASL specification. */
+  __tmp_17 : FaultRecord = descaddr.fault;
+  __tmp_17.typ = Fault_None;
+  descaddr.fault = __tmp_17;
   __tmp_18 : MemoryAttributes = descaddr.memattrs;
   __tmp_18.typ = MemType_Normal;
   descaddr.memattrs = __tmp_18;