summaryrefslogtreecommitdiff
path: root/src/gen_lib
diff options
context:
space:
mode:
Diffstat (limited to 'src/gen_lib')
-rw-r--r--src/gen_lib/prompt.lem4
-rw-r--r--src/gen_lib/sail_values.lem53
-rw-r--r--src/gen_lib/state.lem72
3 files changed, 76 insertions, 53 deletions
diff --git a/src/gen_lib/prompt.lem b/src/gen_lib/prompt.lem
index 426b0811..70850dc1 100644
--- a/src/gen_lib/prompt.lem
+++ b/src/gen_lib/prompt.lem
@@ -71,12 +71,12 @@ let read_reg_range reg i j =
read_reg_aux (external_reg_slice reg (natFromInteger i,natFromInteger j))
let read_reg_bit reg i =
read_reg_aux (external_reg_slice reg (natFromInteger i,natFromInteger i)) >>= fun v ->
- return (extract_only_bit v)
+ return (extract_only_element v)
let read_reg_field reg regfield =
read_reg_aux (external_reg_field_whole reg regfield)
let read_reg_bitfield reg regfield =
read_reg_aux (external_reg_field_whole reg regfield) >>= fun v ->
- return (extract_only_bit v)
+ return (extract_only_element v)
val write_reg_aux : reg_name -> vector bitU -> M unit
let write_reg_aux reg_name v =
diff --git a/src/gen_lib/sail_values.lem b/src/gen_lib/sail_values.lem
index ecfd3ce7..bccdd8f2 100644
--- a/src/gen_lib/sail_values.lem
+++ b/src/gen_lib/sail_values.lem
@@ -218,6 +218,14 @@ instance forall 'a. Show 'a => (Show (bitvector 'a))
let show = showBitvector
end
+let bvec_to_vec (Bitvector bs start is_inc) =
+ let bits = List.map bool_to_bitU (bitlistFromWord bs) in
+ Vector bits start is_inc
+
+let vec_to_bvec (Vector elems start is_inc) =
+ let word = wordFromBitlist (List.map bitU_to_bool elems) in
+ Bitvector word start is_inc
+
(*** Vector operations *)
val set_bitvector_start : forall 'a. integer -> bitvector 'a -> bitvector 'a
@@ -265,7 +273,7 @@ let bvupdate_aux (Bitvector bs start is_inc) i j bs' =
let bits = word_update bs lo hi bs' in
Bitvector bits start is_inc
-val bvupdate : forall 'a. bitvector 'a -> integer -> integer -> bitvector 'a -> bitvector 'a
+val bvupdate : forall 'a 'b. bitvector 'a -> integer -> integer -> bitvector 'b -> bitvector 'a
let bvupdate v i j (Bitvector bs' _ _) =
bvupdate_aux v i j bs'
@@ -273,25 +281,32 @@ let bvupdate v i j (Bitvector bs' _ _) =
val getBit' : forall 'a. mword 'a -> nat -> bool
let getBit' w n = getBit w (naturalFromNat n)
-val bvaccess : forall 'a. bitvector 'a -> integer -> bool
-let bvaccess (Bitvector bs start is_inc) n =
+val bvaccess : forall 'a. bitvector 'a -> integer -> bitU
+let bvaccess (Bitvector bs start is_inc) n = bool_to_bitU (
if is_inc then getBit' bs (natFromInteger (n - start))
- else getBit' bs (natFromInteger (start - n))
+ else getBit' bs (natFromInteger (start - n)))
-val bvupdate_pos : forall 'a. Size 'a => bitvector 'a -> integer -> bool -> bitvector 'a
+val bvupdate_pos : forall 'a. Size 'a => bitvector 'a -> integer -> bitU -> bitvector 'a
let bvupdate_pos v n b =
- bvupdate_aux v n n ((wordFromNatural (if b then 1 else 0)) : mword ty1)
+ bvupdate_aux v n n ((wordFromNatural (if bitU_to_bool b then 1 else 0)) : mword ty1)
(*** Bit vector operations *)
+let extract_only_element (Vector elems _ _) = match elems with
+ | [] -> failwith "extract_only_element called for empty vector"
+ | [e] -> e
+ | _ -> failwith "extract_only_element called for vector with more elements"
+end
+
+val extract_only_bit : bitvector ty1 -> bitU
let extract_only_bit (Bitvector elems _ _) =
- let l = word_length elems in
- if l = 1 then
- msb elems
- else if l = 0 then
+ (*let l = word_length elems in
+ if l = 1 then*)
+ bool_to_bitU (msb elems)
+ (*else if l = 0 then
failwith "extract_single_bit called for empty vector"
else
- failwith "extract_single_bit called for vector with more bits"
+ failwith "extract_single_bit called for vector with more bits"*)
let pp_bitu_vector (Vector elems start inc) =
let elems_pp = List.foldl (fun acc elem -> acc ^ showBitU elem) "" elems in
@@ -302,7 +317,7 @@ let most_significant (Bitvector v _ _) =
if word_length v = 0 then
failwith "most_significant applied to empty vector"
else
- msb v
+ bool_to_bitU (msb v)
let bitwise_not_bitlist = List.map bitwise_not_bit
@@ -402,13 +417,14 @@ let to_vec_big = to_vec
let to_vec_inc = to_vec true
let to_vec_dec = to_vec false
-(* TODO??
+
+(* TODO: Think about undefined bit(vector)s *)
let to_vec_undef is_inc (len : integer) =
- Vector (replicate (natFromInteger len) BU) (if is_inc then 0 else len-1) is_inc
+ Bitvector (failwith "undefined bitvector") (if is_inc then 0 else len-1) is_inc
let to_vec_inc_undef = to_vec_undef true
let to_vec_dec_undef = to_vec_undef false
-*)
+
let exts (len, vec) = to_vec (bvget_dir vec) (len,signed vec)
let extz (len, vec) = to_vec (bvget_dir vec) (len,unsigned vec)
@@ -737,9 +753,9 @@ let make_bitvector_undef length =
(* let bitwise_not_range_bit n = bitwise_not (to_vec defaultDir n) *)
-let mask (n,Vector bits start dir) =
- let current_size = List.length bits in
- Vector (drop (current_size - (natFromInteger n)) bits) (if dir then 0 else (n-1)) dir
+let mask (n,bv) =
+ let len = bvlength bv in
+ bvslice_raw bv (len - n) (len - 1)
val byte_chunks : forall 'a. nat -> list 'a -> list (list 'a)
@@ -1026,4 +1042,3 @@ let diafp_to_dia reginfo = function
| DIAFP_concrete v -> DIA_concrete_address (address_of_bitv v)
| DIAFP_reg r -> DIA_register (regfp_to_reg reginfo r)
end
-
diff --git a/src/gen_lib/state.lem b/src/gen_lib/state.lem
index 430ee562..709052fe 100644
--- a/src/gen_lib/state.lem
+++ b/src/gen_lib/state.lem
@@ -47,12 +47,12 @@ let set_reg state reg bitv =
<| state with regstate = Map.insert reg bitv state.regstate |>
-val read_mem : bool -> read_kind -> vector bitU -> integer -> M (vector bitU)
+val read_mem : forall 'a 'b. Size 'b => bool -> read_kind -> bitvector 'a -> integer -> M (bitvector 'b)
let read_mem dir read_kind addr sz state =
- let addr = integer_of_address (address_of_bitv addr) in
+ let addr = unsigned addr in
let addrs = range addr (addr+sz-1) in
let memory_value = List.map (fun addr -> Map_extra.find addr state.memstate) addrs in
- let value = Sail_values.internal_mem_value dir memory_value in
+ let value = vec_to_bvec (Sail_values.internal_mem_value dir memory_value) in
let is_exclusive = match read_kind with
| Sail_impl_base.Read_plain -> false
| Sail_impl_base.Read_reserve -> true
@@ -69,9 +69,9 @@ let read_mem dir read_kind addr sz state =
(* caps are aligned at 32 bytes *)
let cap_alignment = (32 : integer)
-val read_tag : bool -> read_kind -> vector bitU -> M bitU
+val read_tag : forall 'a. bool -> read_kind -> bitvector 'a -> M bitU
let read_tag dir read_kind addr state =
- let addr = (integer_of_address (address_of_bitv addr)) / cap_alignment in
+ let addr = (unsigned addr) / cap_alignment in
let tag = match (Map.lookup addr state.tagstate) with
| Just t -> t
| Nothing -> B0
@@ -96,18 +96,18 @@ let excl_result () state =
(Left true, <| state with last_exclusive_operation_was_load = false |>) in
(Left false, state) :: if state.last_exclusive_operation_was_load then [success] else []
-val write_mem_ea : write_kind -> vector bitU -> integer -> M unit
+val write_mem_ea : forall 'a. write_kind -> bitvector 'a -> integer -> M unit
let write_mem_ea write_kind addr sz state =
- let addr = integer_of_address (address_of_bitv addr) in
+ let addr = unsigned addr in
[(Left (), <| state with write_ea = Just (write_kind,addr,sz) |>)]
-val write_mem_val : vector bitU -> M bool
+val write_mem_val : forall 'b. bitvector 'b -> M bool
let write_mem_val v state =
let (write_kind,addr,sz) = match state.write_ea with
| Nothing -> failwith "write ea has not been announced yet"
| Just write_ea -> write_ea end in
let addrs = range addr (addr+sz-1) in
- let v = external_mem_value v in
+ let v = external_mem_value (bvec_to_vec v) in
let addresses_with_value = List.zip addrs v in
let memstate = List.foldl (fun mem (addr,v) -> Map.insert addr v mem)
state.memstate addresses_with_value in
@@ -122,16 +122,16 @@ let write_tag t state =
let tagstate = Map.insert taddr t state.tagstate in
[(Left true, <| state with tagstate = tagstate |>)]
-val read_reg : register -> M (vector bitU)
+val read_reg : forall 'a. Size 'a => register -> M (bitvector 'a)
let read_reg reg state =
- let v = Map_extra.find (name_of_reg reg) state.regstate in
+ let v = get_reg state (name_of_reg reg) in
+ [(Left (vec_to_bvec v),state)]
+let read_reg_range reg i j state =
+ let v = slice (get_reg state (name_of_reg reg)) i j in
+ [(Left (vec_to_bvec v),state)]
+let read_reg_bit reg i state =
+ let v = access (get_reg state (name_of_reg reg)) i in
[(Left v,state)]
-let read_reg_range reg i j =
- read_reg reg >>= fun rv ->
- return (slice rv i j)
-let read_reg_bit reg i =
- read_reg_range reg i i >>= fun v ->
- return (extract_only_bit v)
let read_reg_field reg regfield =
let (i,j) = register_field_indices reg regfield in
read_reg_range reg i j
@@ -139,25 +139,30 @@ let read_reg_bitfield reg regfield =
let (i,_) = register_field_indices reg regfield in
read_reg_bit reg i
-val write_reg : register -> vector bitU -> M unit
+val write_reg : forall 'a. Size 'a => register -> bitvector 'a -> M unit
let write_reg reg v state =
- [(Left (),<| state with regstate = Map.insert (name_of_reg reg) v state.regstate |>)]
-let write_reg_range reg i j v =
- read_reg reg >>= fun current_value ->
- let new_value = update current_value i j v in
- write_reg reg new_value
-let write_reg_bit reg i bit =
- write_reg_range reg i i (Vector [bit] i (is_inc_of_reg reg))
+ [(Left (), set_reg state (name_of_reg reg) (bvec_to_vec v))]
+let write_reg_range reg i j v state =
+ let current_value = get_reg state (name_of_reg reg) in
+ let new_value = update current_value i j (bvec_to_vec v) in
+ [(Left (), set_reg state (name_of_reg reg) new_value)]
+let write_reg_bit reg i bit state =
+ let current_value = get_reg state (name_of_reg reg) in
+ let new_value = update_pos current_value i bit in
+ [(Left (), set_reg state (name_of_reg reg) new_value)]
let write_reg_field reg regfield =
- let (i,j) = register_field_indices reg regfield in
+ let (i,j) = register_field_indices reg regfield in
write_reg_range reg i j
let write_reg_bitfield reg regfield =
let (i,_) = register_field_indices reg regfield in
write_reg_bit reg i
-let write_reg_field_range reg regfield i j v =
- read_reg_field reg regfield >>= fun current_field_value ->
- let new_field_value = update current_field_value i j v in
- write_reg_field reg regfield new_field_value
+let write_reg_field_range reg regfield i j v state =
+ let (i0,j0) = register_field_indices reg regfield in
+ let current_value = get_reg state (name_of_reg reg) in
+ let current_field_value = slice current_value i0 j0 in
+ let new_field_value = update current_field_value i j (bvec_to_vec v) in
+ let new_value = update current_value i j new_field_value in
+ [(Left (), set_reg state (name_of_reg reg) new_value)]
val barrier : barrier_kind -> M unit
@@ -186,7 +191,8 @@ let rec foreachM_dec (i,stop,by) vars body =
foreachM_dec (i - by,stop,by) vars body
else return vars
-let write_two_regs r1 r2 vec =
+let write_two_regs r1 r2 bvec state =
+ let vec = bvec_to_vec bvec in
let is_inc =
let is_inc_r1 = is_inc_of_reg r1 in
let is_inc_r2 = is_inc_of_reg r2 in
@@ -205,4 +211,6 @@ let write_two_regs r1 r2 vec =
if is_inc
then slice vec (size_r1 - start_vec) (size_vec - start_vec)
else slice vec (start_vec - size_r1) (start_vec - size_vec) in
- write_reg r1 r1_v >> write_reg r2 r2_v
+ let state1 = set_reg state (name_of_reg r1) r1_v in
+ let state2 = set_reg state1 (name_of_reg r2) r2_v in
+ [(Left (), state2)]
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 18:38:53 +0000