diff options
Diffstat (limited to 'mips')
| -rw-r--r-- | mips/mips_extras.lem | 25 | ||||
| -rw-r--r-- | mips/mips_extras_ml.ml | 22 | ||||
| -rw-r--r-- | mips/run_embed.ml | 2 |
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 |