Switch mips/cheri over to using memory ea/val for writes. Tag is now first byte of value for capability writes. Still need TAGw for now but should kill eventually.

6 files changed, 103 insertions, 112 deletions

diff --git a/cheri/cheri_prelude.sail b/cheri/cheri_prelude.sail
index 4716d720..428b3d8c 100644
--- a/cheri/cheri_prelude.sail
+++ b/cheri/cheri_prelude.sail
@@ -362,39 +362,42 @@ function bool register_inaccessible((regno) r) =
     case _       -> bitone
   })
 
+val extern forall Nat 'n. ( bit[64] , [|'n|] ) -> (bit[8 * ('n + 1)]) effect { rmem } MEMr_tag
+val extern forall Nat 'n. ( bit[64] , [|'n|] ) -> (bit[8 * ('n + 1)]) effect { rmem } MEMr_tag_reserve
+
 val extern (bit[64] , bit[8]) -> unit effect { wmem } TAGw
-val extern (bit[64]) -> (bit[8]) effect { rmem } TAGr
+val extern forall Nat 'n. ( bit[64] , [|'n|]) -> unit effect { eamem } MEMea_tag
+val extern forall Nat 'n. ( bit[64] , [|'n|]) -> unit effect { eamem } MEMea_tag_conditional
+val extern forall Nat 'n. ( bit[64] , [|'n|] , bit[8 * ('n + 1)]) -> unit effect { wmv } MEMval_tag
+val extern forall Nat 'n. ( bit[64] , [|'n|] , bit[8 * ('n + 1)]) -> bool effect { wmv } MEMval_tag_conditional
+
 
 function (bool, bit[cap_size_t * 8]) MEMr_tagged ((bit[64]) addr) =
 {
   (* assumes addr is cap. aligned *)
-  let tag = (TAGr (addr)) in
-  let mem = (MEMr (addr, cap_size)) in
+  let ((bit[8]) tag : mem) = (MEMr_tag (addr, cap_size)) in
   (tag[0], mem)
 }
 
 function (bool, bit[cap_size_t * 8]) MEMr_tagged_reserve ((bit[64]) addr) =
 {
   (* assumes addr is cap. aligned *)
-  let tag = (TAGr (addr)) in
-  let mem = (MEMr_reserve (addr, cap_size)) in
+  let ((bit[8]) tag : mem) = (MEMr_tag_reserve (addr, cap_size)) in
   (tag[0], mem)
 }
 
 function unit MEMw_tagged((bit[64]) addr, (bool) tag, (bit[cap_size_t * 8]) data) =
 {
   (* assumes addr is cap. aligned *)
-  MEMw(addr, cap_size, data);
-  TAGw(addr, (0b0000000 : [tag]));
+  MEMea_tag(addr, cap_size);
+  MEMval_tag(addr, cap_size, 0b0000000 : [tag] :  data);
 }
 
 function bool MEMw_tagged_conditional((bit[64]) addr, (bool) tag, (bit[cap_size_t * 8]) data) =
 {
   (* assumes addr is cap. aligned *)
-  success := MEMw_conditional(addr, cap_size, data);
-  if (success) then
-    TAGw(addr, (0b0000000 : [tag]));
-  success;
+  MEMea_tag_conditional(addr, cap_size);
+  MEMval_tag_conditional(addr, cap_size, 0b0000000 : [tag] :  data);
 }
 
 function unit effect {wmem} MEMw_wrapper(addr, size, data) =
@@ -405,16 +408,21 @@ function unit effect {wmem} MEMw_wrapper(addr, size, data) =
   }
   else
   {
-    (* On cheri non-capability writes must clear the corresponding tag*)
+    (* On cheri non-capability writes must clear the corresponding tag
+       XXX this is vestigal and only works on sequential modle -- tag clearing
+       should probably be done in memory model. *)
     TAGw((addr[63..5] : 0b00000), 0x00);
-    MEMw(addr,size,data)
+    MEMea(addr,size);
+    MEMval(addr, size, data);
   }
 
 function bool effect {wmem} MEMw_conditional_wrapper(addr, size, data) =
   {
     (* On cheri non-capability writes must clear the corresponding tag*)
-    success := MEMw_conditional(addr,size,data);
+    MEMea_conditional(addr, size);
+    success := MEMval_conditional(addr,size,data);
     if (success) then
+      (* XXX as above TAGw is vestigal and must die *)
       TAGw((addr[63..5] : 0b00000), 0x00);
     success;
   }
diff --git a/mips/mips_extras.lem b/mips/mips_extras.lem
index 4cf58ff5..0875903f 100644
--- a/mips/mips_extras.lem
+++ b/mips/mips_extras.lem
@@ -1,101 +1,77 @@
 open import Pervasives
 open import Interp_ast
-open import Interp_interface 
-open import Interp_inter_imp 
+open import Interp_interface
+open import Interp_inter_imp
 import Set_extra
 
+let memory_parameter_transformer mode v =
+  let mode = <|mode with endian = E_big_endian|> in
+  match v with
+  | Interp.V_tuple [location;length] ->
+    match length with
+    | Interp.V_lit (L_aux (L_num len) _) ->
+      let (v,regs) = extern_mem_value mode location in
+      (v,(natFromInteger len),regs)
+    | Interp.V_track (Interp.V_lit (L_aux (L_num len) _)) size_regs ->
+      let (v,loc_regs) = extern_mem_value mode location in
+      match loc_regs with
+      | Nothing -> (v,(natFromInteger len),Just (List.map (fun r -> extern_reg r Nothing) (Set_extra.toList size_regs)))
+      | Just loc_regs -> (v,(natFromInteger len),Just (loc_regs++(List.map (fun r -> extern_reg r Nothing) (Set_extra.toList size_regs))))
+      end
+    | _ -> Assert_extra.failwith "expected 'V_lit (L_aux (L_num _) _)' or 'V_track (V_lit (L_aux (L_num len) _)) _'"
+    end
+  | _ -> Assert_extra.failwith ("memory_parameter_transformer: expected 'V_tuple [_;_]' given " ^ (Interp.string_of_value v))
+  end
+
+let memory_parameter_transformer_option_address mode v =
+  let mode = <|mode with endian = E_big_endian|> in
+  match v with
+  | Interp.V_tuple [location;_] ->
+     let (v,_) = extern_mem_value mode location in
+     Just v
+  | _ -> Assert_extra.failwith ("memory_parameter_transformer_option_address: expected 'V_tuple [_;_]' given " ^ (Interp.string_of_value v))
+  end
 
-(*MIPS specific external functions*)
-let mips_externs = [
-]
 
 let read_memory_functions : memory_reads =
-  [ ("MEMr", (MR Read_plain
-                (fun mode v -> match v with
-                   | Interp.V_tuple [location;length] ->
-                     match length with
-                     | Interp.V_lit (L_aux (L_num len) _) ->
-                       let (v,regs) = extern_mem_value mode location in
-                       (v,(natFromInteger len),regs) 
-                     | Interp.V_track (Interp.V_lit (L_aux (L_num len) _)) size_regs ->
-                       let (v,loc_regs) = extern_mem_value mode location in
-                       match loc_regs with
-                       | Nothing -> (v,(natFromInteger len),
-                                     Just (List.map (fun r -> extern_reg r Nothing) (Set_extra.toList size_regs)))
-                       | Just loc_regs -> 
-                         (v,(natFromInteger len),
-                          Just (loc_regs++(List.map (fun r -> extern_reg r Nothing) (Set_extra.toList size_regs))))
-              end end end)));
-    ("MEMr_reserve", (MR Read_reserve (*TODO Likely this isn't really best to be the same as Power*)
-                        (fun mode v -> match v with
-                           | Interp.V_tuple [location;length] ->
-                             match length with
-                             | Interp.V_lit (L_aux (L_num len) _) ->
-                               let (v,regs) = extern_mem_value mode location in
-                               (v,(natFromInteger len),regs) 
-                             | Interp.V_track (Interp.V_lit (L_aux (L_num len) _)) size_regs ->
-                               let (v,loc_regs) = extern_mem_value mode location in
-                               match loc_regs with
-                               | Nothing -> 
-                                 (v,(natFromInteger len),
-                                  Just (List.map (fun r -> extern_reg r Nothing) (Set_extra.toList size_regs)))
-                               | Just loc_regs -> 
-                                 (v,(natFromInteger len),
-                                  Just (loc_regs++
-                                        (List.map (fun r -> extern_reg r Nothing) (Set_extra.toList size_regs))))
-                                 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 
-              (fun mode v -> match v with
-                 | Interp.V_tuple [location;length] ->
-                   match length with
-                   | Interp.V_lit (L_aux (L_num len) _) ->
-                     let (v,regs) = extern_mem_value mode location in
-                     (v,(natFromInteger len),regs)
-                   | Interp.V_track (Interp.V_lit (L_aux (L_num len) _)) size_regs ->
-                     let (v,loc_regs) = extern_mem_value mode location in
-                     match loc_regs with
-                     | Nothing -> (v,(natFromInteger len),
-                                   Just (List.map (fun r -> extern_reg r Nothing) (Set_extra.toList size_regs)))
-                     | Just loc_regs -> 
-                       (v,(natFromInteger len),
-                        Just (loc_regs++(List.map (fun r -> extern_reg r Nothing) (Set_extra.toList size_regs))))
-                      end end end) Nothing));
-  (* As above, probably not best to be the same write kind as power *)
-  ("MEMw_conditional", (MW Write_conditional 
-                          (fun mode v -> match v with
-                             | Interp.V_tuple [location;length] ->
-                               match length with
-                               | Interp.V_lit (L_aux (L_num len) _) ->
-                                 let (v,regs) = extern_mem_value mode location in
-                                 (v,(natFromInteger len),regs)
-                               | Interp.V_track (Interp.V_lit (L_aux (L_num len) _)) size_regs ->
-                                 let (v,loc_regs) = extern_mem_value mode location in
-                                 match loc_regs with
-                                 | Nothing -> 
-                                   (v,(natFromInteger len),
-                                    Just (List.map (fun r -> extern_reg r Nothing) (Set_extra.toList size_regs)))
-                                 | Just loc_regs -> 
-                                   (v,(natFromInteger len),
-                                    Just (loc_regs++
-                                          (List.map (fun r -> extern_reg r Nothing) (Set_extra.toList size_regs))))
-                                end end end) 
-                            (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))
-     ));
-  ("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))
-   ));
+  [ ("MEMr",             (MR Read_plain              memory_parameter_transformer));
+    ("MEMr_reserve",     (MR Read_reserve            memory_parameter_transformer));
+    ("MEMr_tag",         (MR Read_tag                memory_parameter_transformer));
+    ("MEMr_tag_reserve", (MR Read_tag_reserve        memory_parameter_transformer));
+  ]
+
+let memory_writes : memory_writes =
+  [ ("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 memory_eas : memory_write_eas =
+  [ ("MEMea",                 (MEA Write_plain           memory_parameter_transformer));
+    ("MEMea_conditional",     (MEA Write_conditional     memory_parameter_transformer));
+    ("MEMea_tag",             (MEA Write_tag             memory_parameter_transformer));
+    ("MEMea_tag_conditional", (MEA Write_tag_conditional memory_parameter_transformer));
   ]
 
+let memory_vals : memory_write_vals =
+  [ ("MEMval",      (MV memory_parameter_transformer_option_address Nothing));
+    ("MEMval_conditional", (MV memory_parameter_transformer_option_address
+                           (Just 
+                           (fun (IState interp context) b -> 
+                             let bit = Interp.V_lit (L_aux (if b then L_one else L_zero) Interp_ast.Unknown) in
+                             (IState (Interp.add_answer_to_stack interp bit) context)))));
+    ("MEMval_tag",      (MV memory_parameter_transformer_option_address Nothing));
+    ("MEMval_tag_conditional", (MV memory_parameter_transformer_option_address
+                           (Just 
+                           (fun (IState interp context) b -> 
+                             let bit = Interp.V_lit (L_aux (if b then L_one else L_zero) Interp_ast.Unknown) in
+                             (IState (Interp.add_answer_to_stack interp bit) context)))));
+  ]
+
+
 let barrier_functions = [
   (*Need to know what barrier kind to install*)
   ("MEM_sync", Isync);
-]
+  ]
diff --git a/mips/mips_prelude.sail b/mips/mips_prelude.sail
index 957ce041..b282764d 100644
--- a/mips/mips_prelude.sail
+++ b/mips/mips_prelude.sail
@@ -357,12 +357,15 @@ function unit wGPR (idx, v) = {
          if idx == 0 then () else GPR[idx] := v
 }
 
-val extern forall Nat 'n. ( bit[64] , [|'n|] , bit[8*'n]) -> unit effect { wmem } MEMw
 val extern forall Nat 'n. ( bit[64] , [|'n|] ) -> (bit[8 * 'n]) effect { rmem } MEMr
 val extern forall Nat 'n. ( bit[64] , [|'n|] ) -> (bit[8 * 'n]) effect { rmem } MEMr_reserve
-val extern forall Nat 'n. ( bit[64] , [|'n|] , bit[8*'n]) -> bool effect { wmem } MEMw_conditional
 val extern unit -> unit effect { barr } MEM_sync
 
+val extern forall Nat 'n. ( bit[64] , [|'n|]) -> unit effect { eamem } MEMea
+val extern forall Nat 'n. ( bit[64] , [|'n|]) -> unit effect { eamem } MEMea_conditional
+val extern forall Nat 'n. ( bit[64] , [|'n|] , bit[8*'n]) -> unit effect { wmv } MEMval
+val extern forall Nat 'n. ( bit[64] , [|'n|] , bit[8*'n]) -> bool effect { wmv } MEMval_conditional
+
 typedef Exception = enumerate
 {
    Int; TLBMod; TLBL; TLBS; AdEL; AdES; Sys; Bp; ResI; CpU; Ov; Tr; C2E; C2Trap;
diff --git a/mips/mips_wrappers.sail b/mips/mips_wrappers.sail
index cda96b2c..a620f5f3 100644
--- a/mips/mips_wrappers.sail
+++ b/mips/mips_wrappers.sail
@@ -40,12 +40,16 @@ function unit effect {wmem} MEMw_wrapper(addr, size, data) =
       {
         UART_WDATA   := data[31..24];
         UART_WRITTEN := 1;
+      } else {
+        MEMea(addr, size);
+        MEMval(addr, size, data);
       }
-    else
-      MEMw(addr, size, data)
 
 function bool effect {wmem} MEMw_conditional_wrapper(addr, size, data) =
-  MEMw_conditional(addr, size, data)
+    {
+      MEMea_conditional(addr, size);
+      MEMval_conditional(addr, size, data)
+    }
 
 function bit[64] addrWrapper((bit[64]) addr, (MemAccessType) accessType, (WordType) width) =
     addr
diff --git a/src/lem_interp/run_with_elf.ml b/src/lem_interp/run_with_elf.ml
index 5b27bf1a..20601fec 100644
--- a/src/lem_interp/run_with_elf.ml
+++ b/src/lem_interp/run_with_elf.ml
@@ -689,8 +689,8 @@ let initial_system_state_of_elf_file name =
           (Mips.defs,
            (Mips_extras.read_memory_functions,
             Mips_extras.memory_writes,
-	    [],
-	    [],
+            Mips_extras.memory_eas,
+            Mips_extras.memory_vals,
             Mips_extras.barrier_functions),
            [],
            MIPS,
diff --git a/src/lem_interp/run_with_elf_cheri.ml b/src/lem_interp/run_with_elf_cheri.ml
index 5eb560e1..9991c8aa 100644
--- a/src/lem_interp/run_with_elf_cheri.ml
+++ b/src/lem_interp/run_with_elf_cheri.ml
@@ -765,8 +765,8 @@ let initial_system_state_of_elf_file name =
           (Cheri.defs,
            (Mips_extras.read_memory_functions,
             Mips_extras.memory_writes,
-	    [],
-	    [],
+            Mips_extras.memory_eas,
+            Mips_extras.memory_vals,
             Mips_extras.barrier_functions),
            [],
            MIPS,