diff options
Diffstat (limited to 'src/gen_lib')
| -rw-r--r-- | src/gen_lib/prompt.lem | 6 | ||||
| -rw-r--r-- | src/gen_lib/state.lem | 30 |
2 files changed, 12 insertions, 24 deletions
diff --git a/src/gen_lib/prompt.lem b/src/gen_lib/prompt.lem index dd97541f..426b0811 100644 --- a/src/gen_lib/prompt.lem +++ b/src/gen_lib/prompt.lem @@ -11,6 +11,7 @@ let rec bind m f = match m with | Read_mem descr k -> Read_mem descr (fun v -> let (o,opt) = k v in (bind o f,opt)) | Read_reg descr k -> Read_reg descr (fun v -> let (o,opt) = k v in (bind o f,opt)) | Write_memv descr k -> Write_memv descr (fun v -> let (o,opt) = k v in (bind o f,opt)) + | Excl_res k -> Excl_res (fun v -> let (o,opt) = k v in (bind o f,opt)) | Write_ea descr o_s -> Write_ea descr (let (o,opt) = o_s in (bind o f,opt)) | Barrier descr o_s -> Barrier descr (let (o,opt) = o_s in (bind o f,opt)) | Footprint o_s -> Footprint (let (o,opt) = o_s in (bind o f,opt)) @@ -40,6 +41,11 @@ let read_mem dir rk addr sz = (Done bitv,Nothing) in Read_mem (rk,addr,sz) k +val excl_result : unit -> M bool +let excl_result () = + let k successful = (return successful,Nothing) in + Excl_res k + val write_mem_ea : write_kind -> vector bitU -> integer -> M unit let write_mem_ea wk addr sz = let addr = address_lifted_of_bitv addr in diff --git a/src/gen_lib/state.lem b/src/gen_lib/state.lem index 0dfd10d7..ddd30eda 100644 --- a/src/gen_lib/state.lem +++ b/src/gen_lib/state.lem @@ -66,7 +66,11 @@ let read_mem dir read_kind addr sz state = then [(Left value, <| state with last_exclusive_operation_was_load = true |>)] else [(Left value, state)] - +val excl_result : unit -> M bool +let excl_result () state = + let success = + (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 let write_mem_ea write_kind addr sz state = @@ -83,29 +87,7 @@ let write_mem_val v state = 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 - - 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 |>)] - + [(Left true, <| state with memstate = memstate |>)] val read_reg : register -> M (vector bitU) |