wrap state monad into list monoad for non-deterministic write exclusive operations

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