From b5b74f9fca5a760cb388b1f9ed7873f73b983c45 Mon Sep 17 00:00:00 2001
From: Robert Norton
Date: Wed, 13 Apr 2016 15:28:05 +0100
Subject: add tagr and tagw in mips_extras (will need to change these to make
 tag writes atomic)

---
 mips/mips_extras.lem | 10 +++++++++-
 1 file changed, 9 insertions(+), 1 deletion(-)

(limited to 'mips')

diff --git a/mips/mips_extras.lem b/mips/mips_extras.lem
index d1eacc1c..4cf58ff5 100644
--- a/mips/mips_extras.lem
+++ b/mips/mips_extras.lem
@@ -43,7 +43,9 @@ let read_memory_functions : memory_reads =
                                  (v,(natFromInteger len),
                                   Just (loc_regs++
                                         (List.map (fun r -> extern_reg r Nothing) (Set_extra.toList size_regs))))
-                                 end end end)));                
+                                 end end end)));
+    ("TAGr", (MR Read_tag (fun mode v -> let (v, regs) = extern_mem_value mode v in 
+                                         (v, 1, regs))));
 ]
 let memory_writes : memory_writes = [
   ("MEMw", (MW Write_plain 
@@ -85,6 +87,12 @@ let memory_writes : memory_writes = [
                               let v = Interp.V_lit (L_aux (if success then L_one else L_zero) Unknown) in
                               IState (Interp.add_answer_to_stack interp_state v) c))
      ));
+  ("TAGw", (MW Write_tag (fun mode v -> let (v, regs) = extern_mem_value mode v in
+                                        (v, 1, regs))
+              (Just (fun (IState interp_state c) success ->
+                              let v = Interp.V_lit (L_aux (if success then L_one else L_zero) Unknown) in
+                              IState (Interp.add_answer_to_stack interp_state v) c))
+   ));
   ]
 
 let barrier_functions = [
-- 
cgit v1.2.3