1 files changed, 11 insertions, 11 deletions
diff --git a/src/gen_lib/state.lem b/src/gen_lib/state.lem
index f9011323..df530bc7 100644
--- a/src/gen_lib/state.lem
+++ b/src/gen_lib/state.lem
@@ -127,12 +127,12 @@ let is_exclusive = function
 end
 
 
-val read_mem : forall 'regs 'a 'b 'e. Bitvector 'a, Bitvector 'b => bool -> read_kind -> 'a -> integer -> M 'regs 'b 'e
-let read_mem dir read_kind addr sz state =
+val read_mem : forall 'regs 'a 'b 'e. Bitvector 'a, Bitvector 'b => read_kind -> 'a -> integer -> M 'regs 'b 'e
+let read_mem read_kind addr sz state =
   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 = of_bits (Sail_values.internal_mem_value dir memory_value) in
+  let value = of_bits (Sail_values.internal_mem_value memory_value) in
   if is_exclusive read_kind
   then [(Value value, <| state with last_exclusive_operation_was_load = true |>)]
   else [(Value value, state)]
@@ -140,8 +140,8 @@ let read_mem dir read_kind addr sz state =
 (* caps are aligned at 32 bytes *)
 let cap_alignment = (32 : integer)
 
-val read_tag : forall 'regs 'a 'e. Bitvector 'a => bool -> read_kind -> 'a -> M 'regs bitU 'e
-let read_tag dir read_kind addr state =
+val read_tag : forall 'regs 'a 'e. Bitvector 'a => read_kind -> 'a -> M 'regs bitU 'e
+let read_tag read_kind addr state =
   let addr = (unsigned addr) / cap_alignment in
   let tag = match (Map.lookup addr state.tagstate) with
     | Just t -> t
@@ -216,30 +216,30 @@ let update_reg reg f v state =
 let write_reg_field reg regfield = update_reg reg regfield.set_field
 
 val update_reg_range : forall 'regs 'a 'b. Bitvector 'a, Bitvector 'b => register_ref 'regs 'a -> integer -> integer -> 'a -> 'b -> 'a
-let update_reg_range reg i j reg_val new_val = set_bits (reg.reg_is_inc) (reg.reg_start) reg_val i j (bits_of new_val)
+let update_reg_range reg i j reg_val new_val = set_bits (reg.reg_is_inc) reg_val i j (bits_of new_val)
 let write_reg_range reg i j = update_reg reg (update_reg_range reg i j)
 
-let update_reg_pos reg i reg_val x = update_pos reg_val i x
+let update_reg_pos reg i reg_val x = update_list reg.reg_is_inc reg_val i x
 let write_reg_pos reg i = update_reg reg (update_reg_pos reg i)
 
-let update_reg_bit reg i reg_val bit = set_bit (reg.reg_is_inc) (reg.reg_start) reg_val i (to_bitU bit)
+let update_reg_bit reg i reg_val bit = set_bit (reg.reg_is_inc) reg_val i (to_bitU bit)
 let write_reg_bit reg i = update_reg reg (update_reg_bit reg i)
 
 let update_reg_field_range regfield i j reg_val new_val =
   let current_field_value = regfield.get_field reg_val in
-  let new_field_value = set_bits (regfield.field_is_inc) (regfield.field_start) current_field_value i j (bits_of new_val) in
+  let new_field_value = set_bits (regfield.field_is_inc) current_field_value i j (bits_of new_val) in
   regfield.set_field reg_val new_field_value
 let write_reg_field_range reg regfield i j = update_reg reg (update_reg_field_range regfield i j)
 
 let update_reg_field_pos regfield i reg_val x =
   let current_field_value = regfield.get_field reg_val in
-  let new_field_value = update_pos current_field_value i x in
+  let new_field_value = update_list regfield.field_is_inc current_field_value i x in
   regfield.set_field reg_val new_field_value
 let write_reg_field_pos reg regfield i = update_reg reg (update_reg_field_pos regfield i)
 
 let update_reg_field_bit regfield i reg_val bit =
   let current_field_value = regfield.get_field reg_val in
-  let new_field_value = set_bit (regfield.field_is_inc) (regfield.field_start) current_field_value i (to_bitU bit) in
+  let new_field_value = set_bit (regfield.field_is_inc) current_field_value i (to_bitU bit) in
   regfield.set_field reg_val new_field_value
 let write_reg_field_bit reg regfield i = update_reg reg (update_reg_field_bit regfield i)