diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/gen_lib/state.lem | 96 |
1 files changed, 62 insertions, 34 deletions
diff --git a/src/gen_lib/state.lem b/src/gen_lib/state.lem index 98596b6d..02fe8094 100644 --- a/src/gen_lib/state.lem +++ b/src/gen_lib/state.lem @@ -3,32 +3,33 @@ open import Sail_impl_base open import Sail_values (* 'a is result type *) -type State 's 'a = 's -> (either 'a string * 's) type memstate = map integer memory_byte type regstate = map string (vector bitU) type sequential_state = <| regstate : regstate; memstate : memstate; - write_ea : maybe (integer * integer) |> + write_ea : maybe (write_kind * integer * integer); + last_exclusive_operation_was_load : bool|> -type M 'a = State sequential_state 'a - -val return : forall 's 'a. 'a -> State 's 'a -let return a s = (Left a,s) +type M 'a = sequential_state -> list ((either 'a string) * sequential_state) -val bind : forall 's 'a 'b. State 's 'a -> ('a -> State 's 'b) -> State 's 'b -let bind m f s = match m s with - | (Left a,s') -> f a s' - | (Right error,s') -> (Right error,s') - end +val return : forall 'a. 'a -> M 'a +let return a s = [(Left a,s)] + +val bind : forall 'a 'b. M 'a -> ('a -> M 'b) -> M 'b +let bind m f (s : sequential_state) = + List.concatMap (function + | (Left a, s') -> f a s' + | (Right e, s') -> [(Right e, s')] + end) (m s) let inline (>>=) = bind -val (>>): forall 's 'b. State 's unit -> State 's 'b -> State 's 'b +val (>>): forall 'b. M unit -> M 'b -> M 'b let inline (>>) m n = m >>= fun _ -> n -val exit : forall 's 'e 'a. 'e -> State 's 'a -let exit _ s = (Right "exit",s) +val exit : forall 'e 'a. 'e -> M 'a +let exit _ s = [(Right "exit",s)] val range : integer -> integer -> list integer @@ -45,45 +46,72 @@ let set_reg state reg bitv = val read_mem : end_flag -> bool -> read_kind -> vector bitU -> integer -> M (vector bitU) -let read_mem endian dir _ addr sz state = +let read_mem endian dir read_kind addr sz state = let addr = integer_of_address (address_of_bitv 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 endian dir memory_value in - (Left value,state) - + let is_exclusive = match read_kind with + | Sail_impl_base.Read_plain -> false + | Sail_impl_base.Read_tag -> failwith "Read_tag not implemented" + | Sail_impl_base.Read_tag_reserve -> failwith "Read_tag_reserve not implemented" + | Sail_impl_base.Read_reserve -> true + | Sail_impl_base.Read_acquire -> false + | Sail_impl_base.Read_exclusive -> true + | Sail_impl_base.Read_exclusive_acquire -> true + | Sail_impl_base.Read_stream -> false + end in + + if is_exclusive + then [(Left value, <| state with last_exclusive_operation_was_load = true |>)] + else [(Left value, state)] + -val write_mem_address_value : write_kind -> address -> integer -> end_flag -> vector bitU -> M bool -let write_mem_address_value _ addr sz endian v state = - let addr = integer_of_address addr in - let addrs = range addr (addr+sz-1) in - let v = external_mem_value endian v in - let addresses_with_value = List.zip addrs v in - let mem = List.foldl (fun mem (addr,v) -> Map.insert addr v mem) - state.memstate addresses_with_value in - (Left true,<| state with memstate = mem |>) val write_mem_ea : write_kind -> vector bitU -> integer -> M unit -let write_mem_ea _ addr sz state = +let write_mem_ea write_kind addr sz state = let addr = integer_of_address (address_of_bitv addr) in - (Left (), <| state with write_ea = Just (addr,sz) |>) + [(Left (), <| state with write_ea = Just (write_kind,addr,sz) |>)] val write_mem_val : end_flag -> vector bitU -> M bool let write_mem_val endian v state = - let (addr,sz) = match state.write_ea with + 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 endian v in let addresses_with_value = List.zip addrs v in - let mem = List.foldl (fun mem (addr,v) -> Map.insert addr v mem) - state.memstate addresses_with_value in - (Left true,<| state with memstate = mem |>) + let memstate = List.foldl (fun mem (addr,v) -> Map.insert addr v mem) + state.memstate addresses_with_value in + + let is_exclusive = match write_kind with + | Sail_impl_base.Write_plain -> false + | Sail_impl_base.Write_tag -> failwith "Write_tag not implemented" + | Sail_impl_base.Write_tag_conditional -> failwith "Write_tag_conditional not implemented" + | Sail_impl_base.Write_conditional -> true + | Sail_impl_base.Write_release -> false + | Sail_impl_base.Write_exclusive -> true + | Sail_impl_base.Write_exclusive_release -> true + end in + + if is_exclusive + then + let success = + (Left true, <| state with memstate = memstate; + last_exclusive_operation_was_load = false |>) in + let failure = + (Left false, <| state with last_exclusive_operation_was_load = false |>) in + if state.last_exclusive_operation_was_load + then [failure;success] + else [failure] + else [(Left true, <| state with memstate = memstate |>)] + + val read_reg : register -> M (vector bitU) let read_reg reg state = let v = Map_extra.find (name_of_reg reg) state.regstate in - (Left v,state) + [(Left v,state)] let read_reg_range reg i j = read_reg reg >>= fun rv -> return (slice rv i j) @@ -99,7 +127,7 @@ let read_reg_bitfield reg regfield = val write_reg : register -> vector bitU -> M unit let write_reg reg v state = - (Left (),<| state with regstate = Map.insert (name_of_reg reg) v state.regstate |>) + [(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 |