diff options
| author | Thomas Bauereiss | 2017-08-29 17:42:56 +0100 |
|---|---|---|
| committer | Thomas Bauereiss | 2017-08-29 17:47:52 +0100 |
| commit | 2300d45d6645faae3c00a183e80547c1a6cb9165 (patch) | |
| tree | 8e038185e5fa14ee216cd04217665de8f7d91c85 /src/gen_lib | |
| parent | 5ec766ceb381f15e6ab4cf568b0f6ab919ca6b68 (diff) | |
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).
Diffstat (limited to 'src/gen_lib')
| -rw-r--r-- | src/gen_lib/sail_operators.lem | 2 | ||||
| -rw-r--r-- | src/gen_lib/sail_operators_mwords.lem | 2 | ||||
| -rw-r--r-- | src/gen_lib/sail_values.lem | 2 |
3 files changed, 6 insertions, 0 deletions
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 |