Merge branch 'master' of bitbucket.org:Peter_Sewell/sail

# Conflicts:
#	src/lem_interp/interp.lem
#	src/lem_interp/interp_inter_imp.lem
#	src/lem_interp/interp_interface.lem
#	src/parser.mly
#	src/pretty_print_lem.ml

3 files changed, 21 insertions, 28 deletions

diff --git a/mips/mips_extras.lem b/mips/mips_extras.lem
index bdaa08e6..99487f49 100644
--- a/mips/mips_extras.lem
+++ b/mips/mips_extras.lem
@@ -34,23 +34,19 @@ let memory_parameter_transformer_option_address _mode v =
 let read_memory_functions : memory_reads =
   [ ("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 read_memory_tagged_functions : memory_read_taggeds =
+  [ ("MEMr_tag",         (MRT Read_plain             memory_parameter_transformer));
+    ("MEMr_tag_reserve", (MRT Read_reserve           memory_parameter_transformer));
   ]
 
 let memory_writes : memory_writes =
-  [ ("TAGw", (MW Write_tag (fun mode v -> let (v, regs) = extern_with_track mode extern_vector_value 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 =
@@ -60,15 +56,18 @@ let memory_vals : memory_write_vals =
                            (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
+  ]
+
+let memory_vals_tagged : memory_write_vals_tagged =
+  [
+    ("MEMval_tag",      (MVT memory_parameter_transformer_option_address Nothing));
+    ("MEMval_tag_conditional", (MVT 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 = [
   ("MEM_sync", Barrier_MIPS_SYNC);
   ]
diff --git a/mips/mips_extras_ml.ml b/mips/mips_extras_ml.ml
index 61f34425..d4ea0681 100644
--- a/mips/mips_extras_ml.ml
+++ b/mips/mips_extras_ml.ml
@@ -11,6 +11,7 @@ module Mem = struct
     end)
 end
 
+let cap_size_shift = ref 5;; (* caps every 2**5 = 32 bytes *)
 let mem_pages = (ref Mem.empty : (Bytes.t Mem.t) ref);;
 let tag_mem = (ref Mem.empty : (bool Mem.t) ref);;
 
@@ -74,13 +75,11 @@ let _MEMval (addr, size, data) =
     tracef "MEM[%s] <- %s\n" (big_int_to_hex a) (string_of_value data);
   add_mem_bytes a buf 0 s
 
-let _MEMval_tag (addr, size, data) =
-  let tag = bit_vector_access_int data 0 in
-  let data = vector_subrange_int data (8*(int_of_big_int size) + 7) 8 in 
+let _MEMval_tag (addr, size, tag, data) =
   let addr_bi = (unsigned_big(addr)) in
   begin
     _MEMval (addr, size, data);
-    tag_mem := Mem.add addr_bi (to_bool tag) !tag_mem;
+    tag_mem := Mem.add (shift_right_big_int addr_bi !cap_size_shift) (to_bool tag) !tag_mem;
   end
 
   
@@ -88,8 +87,8 @@ let _MEMval_conditional (addr, size, data) =
     let _ = _MEMval (addr, size, data) in
     Vone
 
-let _MEMval_tag_conditional (addr, size, data) =
-    let _ = _MEMval_tag (addr, size, data) in
+let _MEMval_tag_conditional (addr, size, tag, data) =
+    let _ = _MEMval_tag (addr, size, tag, data) in
     Vone
 
 let _MEMr (addr, size) = begin
@@ -112,17 +111,10 @@ let _MEMr_tag (addr, size) =
   let data = _MEMr(addr, size) in
   let addr_bi = unsigned_big(addr) in 
   let tag = try
-      Mem.find addr_bi !tag_mem 
+      Mem.find (shift_right_big_int addr_bi !cap_size_shift) !tag_mem 
     with Not_found -> false in
-  begin
-    set_start_to_length (vector_concat data (to_vec_dec_int (8, if tag then 1 else 0)))
-  end
+  (bool_to_bit tag, data)
 
 let _MEMr_tag_reserve = _MEMr_tag
 
-let _TAGw (addr, tag) = 
-  begin
-    tag_mem := Mem.add (unsigned_big addr) (to_bool (bit_vector_access_int tag 0)) !tag_mem
-  end
-
 let _MEM_sync _ = ()
diff --git a/mips/run_embed.ml b/mips/run_embed.ml
index 70dee4b6..463caffd 100644
--- a/mips/run_embed.ml
+++ b/mips/run_embed.ml
@@ -197,6 +197,7 @@ module CHERI_model : ISA_model = struct
     set_register Cheri_embed._PCC initial_cap_vec;
     set_register Cheri_embed._nextPCC initial_cap_vec;
     set_register Cheri_embed._delayedPCC initial_cap_vec;
+    cap_size_shift := 5; (* configure memory model cap_size in mips_extras_ml *)
     for i = 0 to 31 do
       set_register (vector_access_int Cheri_embed._CapRegs i) initial_cap_vec
     done
@@ -254,6 +255,7 @@ module CHERI128_model : ISA_model = struct
     set_register Cheri128_embed._PCC initial_cap_vec;
     set_register Cheri128_embed._nextPCC initial_cap_vec;
     set_register Cheri128_embed._delayedPCC initial_cap_vec;
+    cap_size_shift := 4; (* configure memory model cap_size in mips_extras_ml *)
     for i = 0 to 31 do
       set_register (vector_access_int Cheri128_embed._CapRegs i) initial_cap_vec
     done