From f9b81e15c97014425a9a958492ebf4fd92d8a8bc Mon Sep 17 00:00:00 2001
From: Thomas Bauereiss
Date: Wed, 14 Mar 2018 11:49:37 +0000
Subject: Fix Lem generation for CHERI-MIPS and Aarch64

- Update Lem bindings and extras files
- Rewrite Nexp_var's if they are bound to a constant, similar to Nexp_id's
  (used for cap_size in the CHERI spec)
- Add Lem and Isabelle Makefile targets for CHERI
---
 src/gen_lib/sail_operators_bitlists.lem | 3 +++
 src/gen_lib/sail_operators_mwords.lem   | 6 +++---
 2 files changed, 6 insertions(+), 3 deletions(-)

(limited to 'src/gen_lib')

diff --git a/src/gen_lib/sail_operators_bitlists.lem b/src/gen_lib/sail_operators_bitlists.lem
index 9b81e233..edba83ba 100644
--- a/src/gen_lib/sail_operators_bitlists.lem
+++ b/src/gen_lib/sail_operators_bitlists.lem
@@ -220,6 +220,9 @@ let duplicate_oracle b n =
   bool_of_bitU_oracle b >>= (fun b ->
   return (duplicate (bitU_of_bool b) n))
 
+val reverse_endianness : list bitU -> list bitU
+let reverse_endianness v = reverse_endianness_list v
+
 val eq_vec    : list bitU -> list bitU -> bool
 val neq_vec   : list bitU -> list bitU -> bool
 val ult_vec   : list bitU -> list bitU -> bool
diff --git a/src/gen_lib/sail_operators_mwords.lem b/src/gen_lib/sail_operators_mwords.lem
index ea7c11cf..e87f4b7c 100644
--- a/src/gen_lib/sail_operators_mwords.lem
+++ b/src/gen_lib/sail_operators_mwords.lem
@@ -5,9 +5,6 @@ open import Sail_operators
 open import Prompt_monad
 open import Prompt
 
-val mword_zero : forall 'a. Size 'a => mword 'a
-let mword_zero = wordFromInteger 0
-
 (* Specialisation of operators to machine words *)
 
 let uint v = unsignedIntegerFromWord v
@@ -233,6 +230,9 @@ let duplicate_fail   b n = bool_of_bitU_fail b >>= (fun b -> return (duplicate_b
 let duplicate_oracle b n = bool_of_bitU_oracle b >>= (fun b -> return (duplicate_bool b n))
 let duplicate        b n = maybe_failwith (duplicate_maybe b n)
 
+val reverse_endianness : forall 'a. Size 'a => mword 'a -> mword 'a
+let reverse_endianness v = wordFromBitlist (reverse_endianness_list (bitlistFromWord v))
+
 val eq_vec    : forall 'a. Size 'a => mword 'a -> mword 'a -> bool
 val neq_vec   : forall 'a. Size 'a => mword 'a -> mword 'a -> bool
 val ult_vec   : forall 'a. Size 'a => mword 'a -> mword 'a -> bool
-- 
cgit v1.2.3