Change types of MEMr_tag, MEMval_tag and co. so that tag is separate from data and invent rmemt and wmvt effects for them. Extend the interpreter context to include lists of tagged memory read and write functions. The memory model must round down the address to the nearest capability aligned address when reading/writing tags. Remove TAGw which is no longer needed as a result.

1 files changed, 8 insertions, 65 deletions

diff --git a/src/lem_interp/sail_impl_base.lem b/src/lem_interp/sail_impl_base.lem
index 02d53896..856b90a1 100644
--- a/src/lem_interp/sail_impl_base.lem
+++ b/src/lem_interp/sail_impl_base.lem
@@ -41,7 +41,7 @@
 (*========================================================================*)
 
 open import Pervasives_extra
-            
+
 (* maybe isn't a member of type Ord - this should be in the Lem standard library*)
 instance forall 'a. Ord 'a => (Ord (maybe 'a))
   let compare = maybeCompare compare
@@ -422,7 +422,6 @@ end
 type read_kind =
   (* common reads *)
   | Read_plain
-  | Read_tag | Read_tag_reserve (*For reading the tag of tagged memory*)
   (* Power reads *)
   | Read_reserve
   (* AArch64 reads *)
@@ -431,8 +430,6 @@ type read_kind =
 instance (Show read_kind)
   let show = function
     | Read_plain -> "Read_plain"
-    | Read_tag -> "Read_tag"
-    | Read_tag_reserve -> "Read_tag_reserve"
     | Read_reserve -> "Read_reserve"
     | Read_acquire -> "Read_acquire"
     | Read_exclusive -> "Read_exclusive"
@@ -444,7 +441,6 @@ end
 type write_kind =
   (* common writes *)
   | Write_plain
-  | Write_tag | Write_tag_conditional (*For writing the tag of tagged memory*)
   (* Power writes *)
   | Write_conditional
   (* AArch64 writes *)
@@ -453,8 +449,6 @@ type write_kind =
 instance (Show write_kind)
   let show = function
     | Write_plain -> "Write_plain"
-    | Write_tag -> "Write_tag"
-    | Write_tag_conditional -> "Write_tag_conditional"
     | Write_conditional -> "Write_conditional"
     | Write_release -> "Write_release"
     | Write_exclusive -> "Write_exclusive"
@@ -536,8 +530,6 @@ let ~{ocaml} read_kindCompare rk1 rk2 =
   | (Read_plain, Read_exclusive)         -> LT
   | (Read_plain, Read_exclusive_acquire) -> LT
   | (Read_plain, Read_stream)            -> LT
-  | (Read_plain, Read_tag)               -> LT
-  | (Read_plain, Read_tag_reserve)       -> LT
 
   | (Read_reserve, Read_plain)             -> GT
   | (Read_reserve, Read_reserve)           -> EQ
@@ -545,8 +537,6 @@ let ~{ocaml} read_kindCompare rk1 rk2 =
   | (Read_reserve, Read_exclusive)         -> LT
   | (Read_reserve, Read_exclusive_acquire) -> LT
   | (Read_reserve, Read_stream)            -> LT
-  | (Read_reserve, Read_tag)               -> LT
-  | (Read_reserve, Read_tag_reserve)       -> LT
 
   | (Read_acquire, Read_plain)             -> GT
   | (Read_acquire, Read_reserve)           -> GT
@@ -554,8 +544,6 @@ let ~{ocaml} read_kindCompare rk1 rk2 =
   | (Read_acquire, Read_exclusive)         -> LT
   | (Read_acquire, Read_exclusive_acquire) -> LT
   | (Read_acquire, Read_stream)            -> LT
-  | (Read_acquire, Read_tag)               -> LT
-  | (Read_acquire, Read_tag_reserve)       -> LT
 
   | (Read_exclusive, Read_plain)             -> GT
   | (Read_exclusive, Read_reserve)           -> GT
@@ -563,8 +551,6 @@ let ~{ocaml} read_kindCompare rk1 rk2 =
   | (Read_exclusive, Read_exclusive)         -> EQ
   | (Read_exclusive, Read_exclusive_acquire) -> LT
   | (Read_exclusive, Read_stream)            -> LT
-  | (Read_exclusive, Read_tag)               -> LT
-  | (Read_exclusive, Read_tag_reserve)       -> LT
 
   | (Read_exclusive_acquire, Read_plain)             -> GT
   | (Read_exclusive_acquire, Read_reserve)           -> GT
@@ -572,8 +558,6 @@ let ~{ocaml} read_kindCompare rk1 rk2 =
   | (Read_exclusive_acquire, Read_exclusive)         -> GT
   | (Read_exclusive_acquire, Read_exclusive_acquire) -> EQ
   | (Read_exclusive_acquire, Read_stream)            -> GT
-  | (Read_exclusive_acquire, Read_tag)               -> LT
-  | (Read_exclusive_acquire, Read_tag_reserve)       -> LT
 
   | (Read_stream, Read_plain)             -> GT
   | (Read_stream, Read_reserve)           -> GT
@@ -581,27 +565,7 @@ let ~{ocaml} read_kindCompare rk1 rk2 =
   | (Read_stream, Read_exclusive)         -> GT
   | (Read_stream, Read_exclusive_acquire) -> GT
   | (Read_stream, Read_stream)            -> EQ
-  | (Read_stream, Read_tag)               -> LT
-  | (Read_stream, Read_tag_reserve)       -> LT
-                                               
-  | (Read_tag, Read_plain)             -> GT
-  | (Read_tag, Read_reserve)           -> GT
-  | (Read_tag, Read_acquire)           -> GT
-  | (Read_tag, Read_exclusive)         -> GT
-  | (Read_tag, Read_exclusive_acquire) -> GT
-  | (Read_tag, Read_stream)            -> GT
-  | (Read_tag, Read_tag)               -> EQ
-  | (Read_tag, Read_tag_reserve)       -> LT
-                                               
-  | (Read_tag_reserve, Read_plain)             -> GT
-  | (Read_tag_reserve, Read_reserve)           -> GT
-  | (Read_tag_reserve, Read_acquire)           -> GT
-  | (Read_tag_reserve, Read_exclusive)         -> GT
-  | (Read_tag_reserve, Read_exclusive_acquire) -> GT
-  | (Read_tag_reserve, Read_stream)            -> GT
-  | (Read_tag_reserve, Read_tag)               -> GT
-  | (Read_tag_reserve, Read_tag_reserve)       -> EQ
-  end
+end
 let inline {ocaml} read_kindCompare = defaultCompare
 
 let ~{ocaml} read_kindLess b1 b2      = read_kindCompare b1 b2 =  LT
@@ -629,57 +593,31 @@ let ~{ocaml} write_kindCompare wk1 wk2 =
   | (Write_plain, Write_release)           -> LT
   | (Write_plain, Write_exclusive)         -> LT
   | (Write_plain, Write_exclusive_release) -> LT
-  | (Write_plain, Write_tag)               -> LT
-  | (Write_plain, Write_tag_conditional)   -> LT
 
   | (Write_conditional, Write_plain)             -> GT
   | (Write_conditional, Write_conditional)       -> EQ
   | (Write_conditional, Write_release)           -> LT
   | (Write_conditional, Write_exclusive)         -> LT
   | (Write_conditional, Write_exclusive_release) -> LT
-  | (Write_conditional, Write_tag)               -> LT
-  | (Write_conditional, Write_tag_conditional)   -> LT
 
   | (Write_release, Write_plain)             -> GT
   | (Write_release, Write_conditional)       -> GT
   | (Write_release, Write_release)           -> EQ
   | (Write_release, Write_exclusive)         -> LT
   | (Write_release, Write_exclusive_release) -> LT
-  | (Write_release, Write_tag)               -> LT
-  | (Write_release, Write_tag_conditional)   -> LT
 
   | (Write_exclusive, Write_plain)             -> GT
   | (Write_exclusive, Write_conditional)       -> GT
   | (Write_exclusive, Write_release)           -> GT
   | (Write_exclusive, Write_exclusive)         -> EQ
   | (Write_exclusive, Write_exclusive_release) -> LT
-  | (Write_exclusive, Write_tag)               -> LT
-  | (Write_exclusive, Write_tag_conditional)   -> LT
 
   | (Write_exclusive_release, Write_plain)             -> GT
   | (Write_exclusive_release, Write_conditional)       -> GT
   | (Write_exclusive_release, Write_release)           -> GT
   | (Write_exclusive_release, Write_exclusive)         -> GT
   | (Write_exclusive_release, Write_exclusive_release) -> EQ
-  | (Write_exclusive_release, Write_tag)               -> LT
-  | (Write_exclusive_release, Write_tag_conditional)   -> LT
-
-  | (Write_tag, Write_plain)             -> GT
-  | (Write_tag, Write_conditional)       -> GT
-  | (Write_tag, Write_release)           -> GT
-  | (Write_tag, Write_exclusive)         -> GT
-  | (Write_tag, Write_exclusive_release) -> GT
-  | (Write_tag, Write_tag)               -> EQ
-  | (Write_tag, Write_tag_conditional)   -> LT
-
-  | (Write_tag_conditional, Write_plain)             -> GT
-  | (Write_tag_conditional, Write_conditional)       -> GT
-  | (Write_tag_conditional, Write_release)           -> GT
-  | (Write_tag_conditional, Write_exclusive)         -> GT
-  | (Write_tag_conditional, Write_exclusive_release) -> GT
-  | (Write_tag_conditional, Write_tag)               -> GT
-  | (Write_tag_conditional, Write_tag_conditional)   -> EQ
-  end
+end
 let inline {ocaml} write_kindCompare = defaultCompare
 
 let ~{ocaml} write_kindLess b1 b2      = write_kindCompare b1 b2 =  LT
@@ -778,9 +716,11 @@ end
 
 type event = 
 | E_read_mem of read_kind * address_lifted * nat * maybe (list reg_name)
+| E_read_memt of read_kind * address_lifted * nat * maybe (list reg_name)
 | E_write_mem of write_kind * address_lifted * nat * maybe (list reg_name) * memory_value * maybe (list reg_name)
 | E_write_ea of write_kind * address_lifted * nat * maybe (list reg_name)
 | E_write_memv of maybe address_lifted * memory_value * maybe (list reg_name)
+| E_write_memvt of maybe address_lifted * (bit_lifted * memory_value) * maybe (list reg_name)
 | E_barrier of barrier_kind
 | E_footprint 
 | E_read_reg of reg_name
@@ -793,11 +733,14 @@ let eventCompare e1 e2 =
   match (e1,e2) with
   | (E_read_mem rk1 v1 i1 tr1, E_read_mem rk2 v2 i2 tr2) ->
      compare (rk1, (v1,i1,tr1)) (rk2,(v2, i2, tr2)) 
+  | (E_read_memt rk1 v1 i1 tr1, E_read_memt rk2 v2 i2 tr2) ->
+     compare (rk1, (v1,i1,tr1)) (rk2,(v2, i2, tr2)) 
   | (E_write_mem wk1 v1 i1 tr1 v1' tr1', E_write_mem wk2 v2 i2 tr2 v2' tr2') -> 
     compare ((wk1,v1,i1),(tr1,v1',tr1'))  ((wk2,v2,i2),(tr2,v2',tr2')) 
   | (E_write_ea wk1 a1 i1 tr1, E_write_ea wk2 a2 i2 tr2) ->
     compare (wk1, (a1, i1, tr1)) (wk2, (a2, i2, tr2))
   | (E_write_memv _ mv1 tr1, E_write_memv _ mv2 tr2) -> compare (mv1,tr1) (mv2,tr2)
+  | (E_write_memvt _ mv1 tr1, E_write_memvt _ mv2 tr2) -> compare (mv1,tr1) (mv2,tr2)
   | (E_barrier bk1, E_barrier bk2) -> compare bk1 bk2
   | (E_read_reg r1, E_read_reg r2) -> compare r1 r2
   | (E_write_reg r1 v1, E_write_reg r2 v2) -> compare (r1,v1) (r2,v2)