diff options
| -rw-r--r-- | mips/mips_extras_embed_sequential.lem | 31 | ||||
| -rw-r--r-- | src/gen_lib/state.lem | 36 |
2 files changed, 52 insertions, 15 deletions
diff --git a/mips/mips_extras_embed_sequential.lem b/mips/mips_extras_embed_sequential.lem index ad1231b6..73dc42ed 100644 --- a/mips/mips_extras_embed_sequential.lem +++ b/mips/mips_extras_embed_sequential.lem @@ -6,14 +6,21 @@ open import State val MEMr : (vector bitU * integer) -> M (vector bitU) val MEMr_reserve : (vector bitU * integer) -> M (vector bitU) -val MEMr_tag : (vector bitU * integer) -> M (vector bitU) -val MEMr_tag_reserve : (vector bitU * integer) -> M (vector bitU) +val MEMr_tag : (vector bitU * integer) -> M (bitU * vector bitU) +val MEMr_tag_reserve : (vector bitU * integer) -> M (bitU * vector bitU) let MEMr (addr,size) = read_mem false Read_plain addr size let MEMr_reserve (addr,size) = read_mem false Read_reserve addr size -let MEMr_tag (addr,size) = read_mem false Read_plain addr size -let MEMr_tag_reserve (addr,size) = read_mem false Read_reserve addr size +let MEMr_tag (addr,size) = + read_mem false Read_plain addr size >>= fun v -> + read_tag false Read_plain addr >>= fun t -> + return (t, v) + +let MEMr_tag_reserve (addr,size) = + read_mem false Read_plain addr size >>= fun v -> + read_tag false Read_plain addr >>= fun t -> + return (t, v) val MEMea : (vector bitU * integer) -> M unit @@ -30,17 +37,13 @@ let MEMea_tag_conditional (addr,size) = write_mem_ea Write_conditional addr size val MEMval : (vector bitU * integer * vector bitU) -> M unit val MEMval_conditional : (vector bitU * integer * vector bitU) -> M bitU -val MEMval_tag : (vector bitU * integer * vector bitU) -> M unit -val MEMval_tag_conditional : (vector bitU * integer * vector bitU) -> M bitU - -let MEMval (_,_,v) = write_mem_val v >>= fun _ -> return () -let MEMval_conditional (_,_,v) = write_mem_val v >>= fun b -> return (if b then B1 else B0) -let MEMval_tag (_,_,v) = write_mem_val v >>= fun _ -> return () -let MEMval_tag_conditional (_,_,v) = write_mem_val v >>= fun b -> return (if b then B1 else B0) +val MEMval_tag : (vector bitU * integer * bitU * vector bitU) -> M unit +val MEMval_tag_conditional : (vector bitU * integer * bitU * vector bitU) -> M bitU -(* TODO *) -val TAGw : (vector bitU * vector bitU) -> M unit -let TAGw (addr, tag) = failwith "TAGw not implemented" +let MEMval (_,_,v) = write_mem_val v >>= fun _ -> return () +let MEMval_conditional (_,_,v) = write_mem_val v >>= fun b -> return (if b then B1 else B0) +let MEMval_tag (_,_,t,v) = write_mem_val v >>= fun _ -> write_tag t >>= fun _ -> return () +let MEMval_tag_conditional (_,_,t,v) = write_mem_val v >>= fun b -> write_tag t >>= fun _ -> return (if b then B1 else B0) val MEM_sync : unit -> M unit diff --git a/src/gen_lib/state.lem b/src/gen_lib/state.lem index 61809cf1..430ee562 100644 --- a/src/gen_lib/state.lem +++ b/src/gen_lib/state.lem @@ -5,10 +5,12 @@ open import Sail_values (* 'a is result type *) type memstate = map integer memory_byte +type tagstate = map integer bitU type regstate = map string (vector bitU) type sequential_state = <| regstate : regstate; memstate : memstate; + tagstate : tagstate; write_ea : maybe (write_kind * integer * integer); last_exclusive_operation_was_load : bool|> @@ -63,7 +65,31 @@ let read_mem dir read_kind addr sz state = if is_exclusive then [(Left value, <| state with last_exclusive_operation_was_load = true |>)] else [(Left value, state)] - + +(* caps are aligned at 32 bytes *) +let cap_alignment = (32 : integer) + +val read_tag : bool -> read_kind -> vector bitU -> M bitU +let read_tag dir read_kind addr state = + let addr = (integer_of_address (address_of_bitv addr)) / cap_alignment in + let tag = match (Map.lookup addr state.tagstate) with + | Just t -> t + | Nothing -> B0 + end in + let is_exclusive = match read_kind with + | Sail_impl_base.Read_plain -> false + | 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 + + (* TODO Should reading a tag set the exclusive flag? *) + if is_exclusive + then [(Left tag, <| state with last_exclusive_operation_was_load = true |>)] + else [(Left tag, state)] + val excl_result : unit -> M bool let excl_result () state = let success = @@ -87,6 +113,14 @@ let write_mem_val v state = state.memstate addresses_with_value in [(Left true, <| state with memstate = memstate |>)] +val write_tag : bitU -> M bool +let write_tag t 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 taddr = addr / cap_alignment in + let tagstate = Map.insert taddr t state.tagstate in + [(Left true, <| state with tagstate = tagstate |>)] val read_reg : register -> M (vector bitU) let read_reg reg state = |