From 2300d45d6645faae3c00a183e80547c1a6cb9165 Mon Sep 17 00:00:00 2001
From: Thomas Bauereiss
Date: Tue, 29 Aug 2017 17:42:56 +0100
Subject: Make Lem export of CHERI(-256) typecheck

Note: The effect annotations of the execute function differ between CHERI and
MIPS, so I split out a new file mips_ast_decl.sail for MIPS with just the
initial declarations of ast, decode, and execute (with the right effects for
MIPS).
---
 src/gen_lib/sail_operators.lem        | 2 ++
 src/gen_lib/sail_operators_mwords.lem | 2 ++
 src/gen_lib/sail_values.lem           | 2 ++
 3 files changed, 6 insertions(+)

(limited to 'src/gen_lib')

diff --git a/src/gen_lib/sail_operators.lem b/src/gen_lib/sail_operators.lem
index 3919d540..fbe096c9 100644
--- a/src/gen_lib/sail_operators.lem
+++ b/src/gen_lib/sail_operators.lem
@@ -34,6 +34,8 @@ let adjust_start_index (start, v) = set_vector_start (start, v)
 
 let cast_vec_bool v = bitU_to_bool (extract_only_element v)
 let cast_bit_vec (start, len, b) = Vector (repeat [b] len) start false
+let cast_boolvec_bitvec (Vector bs start inc) =
+  Vector (List.map bool_to_bitU bs) start inc
 
 let pp_bitu_vector (Vector elems start inc) =
   let elems_pp = List.foldl (fun acc elem -> acc ^ showBitU elem) "" elems in
diff --git a/src/gen_lib/sail_operators_mwords.lem b/src/gen_lib/sail_operators_mwords.lem
index 10a56ad5..9bc81b3e 100644
--- a/src/gen_lib/sail_operators_mwords.lem
+++ b/src/gen_lib/sail_operators_mwords.lem
@@ -96,6 +96,8 @@ let adjust_start_index (start, v) = set_bitvector_start (start, v)
 
 let cast_vec_bool v = bitU_to_bool (extract_only_bit v)
 let cast_bit_vec (start, len, b) = vec_to_bvec (Vector [b] start false)
+let cast_boolvec_bitvec (Vector bs start inc) =
+  vec_to_bvec (Vector (List.map bool_to_bitU bs) start inc)
 
 let pp_bitu_vector (Vector elems start inc) =
   let elems_pp = List.foldl (fun acc elem -> acc ^ showBitU elem) "" elems in
diff --git a/src/gen_lib/sail_values.lem b/src/gen_lib/sail_values.lem
index eeec7440..e2cbb98a 100644
--- a/src/gen_lib/sail_values.lem
+++ b/src/gen_lib/sail_values.lem
@@ -11,6 +11,8 @@ type nn = natural
 val pow : integer -> integer -> integer
 let pow m n = m ** (natFromInteger n)
 
+let pow2 n = pow 2 n
+
 let bool_or (l, r) = (l || r)
 let bool_and (l, r) = (l && r)
 let bool_xor (l, r) = xor l r
-- 
cgit v1.2.3