diff options
| author | Shaked Flur | 2017-05-24 17:03:58 +0100 |
|---|---|---|
| committer | Shaked Flur | 2017-05-24 17:03:58 +0100 |
| commit | 817d87218d2470c9b8a89368209c97a709901717 (patch) | |
| tree | ccdce4b8b3e2542af5151d38d0df22b06913a79e | |
| parent | b400be4ea3917ace2237149e11dd5e1ab4e35078 (diff) | |
fixed missing _tag bits
| -rw-r--r-- | mips/mips_extras_embed.lem | 10 | ||||
| -rw-r--r-- | mips/mips_extras_embed_sequential.lem | 10 | ||||
| -rw-r--r-- | src/gen_lib/state.lem | 2 |
3 files changed, 12 insertions, 10 deletions
diff --git a/mips/mips_extras_embed.lem b/mips/mips_extras_embed.lem index 31be4db0..8abc9747 100644 --- a/mips/mips_extras_embed.lem +++ b/mips/mips_extras_embed.lem @@ -11,8 +11,9 @@ val MEMr_tag_reserve : (vector bitU * integer) -> M (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_tag addr size -let MEMr_tag_reserve (addr,size) = read_mem false Read_tag_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 val MEMea : (vector bitU * integer) -> M unit @@ -22,8 +23,9 @@ val MEMea_tag_conditional : (vector bitU * integer) -> M unit let MEMea (addr,size) = write_mem_ea Write_plain addr size let MEMea_conditional (addr,size) = write_mem_ea Write_conditional addr size -let MEMea_tag (addr,size) = write_mem_ea Write_tag addr size -let MEMea_tag_conditional (addr,size) = write_mem_ea Write_tag_conditional addr size + +let MEMea_tag (addr,size) = write_mem_ea Write_plain addr size +let MEMea_tag_conditional (addr,size) = write_mem_ea Write_conditional addr size val MEMval : (vector bitU * integer * vector bitU) -> M unit diff --git a/mips/mips_extras_embed_sequential.lem b/mips/mips_extras_embed_sequential.lem index bee8e972..ad1231b6 100644 --- a/mips/mips_extras_embed_sequential.lem +++ b/mips/mips_extras_embed_sequential.lem @@ -11,8 +11,9 @@ val MEMr_tag_reserve : (vector bitU * integer) -> M (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_tag addr size -let MEMr_tag_reserve (addr,size) = read_mem false Read_tag_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 val MEMea : (vector bitU * integer) -> M unit @@ -22,8 +23,9 @@ val MEMea_tag_conditional : (vector bitU * integer) -> M unit let MEMea (addr,size) = write_mem_ea Write_plain addr size let MEMea_conditional (addr,size) = write_mem_ea Write_conditional addr size -let MEMea_tag (addr,size) = write_mem_ea Write_tag addr size -let MEMea_tag_conditional (addr,size) = write_mem_ea Write_tag_conditional addr size + +let MEMea_tag (addr,size) = write_mem_ea Write_plain addr size +let MEMea_tag_conditional (addr,size) = write_mem_ea Write_conditional addr size val MEMval : (vector bitU * integer * vector bitU) -> M unit diff --git a/src/gen_lib/state.lem b/src/gen_lib/state.lem index ddd30eda..61809cf1 100644 --- a/src/gen_lib/state.lem +++ b/src/gen_lib/state.lem @@ -53,8 +53,6 @@ let read_mem dir read_kind addr sz state = let value = Sail_values.internal_mem_value dir memory_value in 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 |