diff options
27 files changed, 257 insertions, 190 deletions
diff --git a/cheri/cheri_prelude_common.sail b/cheri/cheri_prelude_common.sail index 63af1021..b839b282 100644 --- a/cheri/cheri_prelude_common.sail +++ b/cheri/cheri_prelude_common.sail @@ -214,52 +214,38 @@ function bool register_inaccessible((regno) r) = else false -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 forall Nat 'n. ( bit[64] , [|'n|] ) -> (bool, bit[8 * 'n]) effect { rmemt } MEMr_tag +val extern forall Nat 'n. ( bit[64] , [|'n|] ) -> (bool, bit[8 * 'n]) effect { rmemt } MEMr_tag_reserve -val extern (bit[64] , bit[8]) -> unit effect { wmem } TAGw -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 +val extern forall Nat 'n. ( bit[64] , [|'n|] , bool, bit[8 * 'n]) -> unit effect { wmvt } MEMval_tag +val extern forall Nat 'n. ( bit[64] , [|'n|] , bool, bit[8 * 'n]) -> bool effect { wmvt } MEMval_tag_conditional function (bool, bit[cap_size_t * 8]) MEMr_tagged ((bit[64]) addr) = -{ (* assumes addr is cap. aligned *) - let tagmem = reverse_endianness(MEMr_tag (addr, cap_size)) in - let tag = tagmem[((8 * cap_size) + 7) .. (8 * cap_size)] in - let mem = tagmem[((8 * cap_size) - 1) .. 0] in - (tag[0], mem) -} + let (tag, data) = MEMr_tag (addr, cap_size) in + (tag, reverse_endianness(data)) + function (bool, bit[cap_size_t * 8]) MEMr_tagged_reserve ((bit[64]) addr) = -{ (* assumes addr is cap. aligned *) - let tagmem = reverse_endianness(MEMr_tag_reserve (addr, cap_size)) in - let tag = tagmem[((8 * cap_size) + 7) .. (8 * cap_size)] in - let mem = tagmem[((8 * cap_size) - 1) .. 0] in - (tag[0], mem) -} + let (tag, data) = MEMr_tag_reserve(addr, cap_size) in + (tag, reverse_endianness(data)) function unit MEMw_tagged((bit[64]) addr, (bool) tag, (bit[cap_size_t * 8]) data) = { (* assumes addr is cap. aligned *) - MEMea_tag(addr, cap_size); - MEMval_tag(addr, cap_size, reverse_endianness(0b0000000 : [tag] : data)); + MEMea(addr, cap_size); + MEMval_tag(addr, cap_size, tag, reverse_endianness(data)); } function bool MEMw_tagged_conditional((bit[64]) addr, (bool) tag, (bit[cap_size_t * 8]) data) = { (* assumes addr is cap. aligned *) - MEMea_tag_conditional(addr, cap_size); - MEMval_tag_conditional(addr, cap_size, reverse_endianness(0b0000000 : [tag] : data)); + MEMea_conditional(addr, cap_size); + MEMval_tag_conditional(addr, cap_size, tag, reverse_endianness(data)); } -function (bit[64]) align((bit[64]) addr, (nat) alignment) = - let remainder = unsigned(addr) mod alignment in - addr - remainder - function unit effect {wmem} MEMw_wrapper(addr, size, data) = let ledata = reverse_endianness(data) in if (addr == 0x000000007f000000) then @@ -269,23 +255,16 @@ function unit effect {wmem} MEMw_wrapper(addr, size, data) = } else { - (* 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(align(addr, cap_size), 0x00); - MEMea(addr,size); - MEMval(addr, size, ledata); + (* On cheri non-capability writes must clear the corresponding tag *) + MEMea(addr, size); + MEMval_tag(addr, size, false, ledata); } function bool effect {wmem} MEMw_conditional_wrapper(addr, size, data) = { (* On cheri non-capability writes must clear the corresponding tag*) MEMea_conditional(addr, size); - success := MEMval_conditional(addr,size,reverse_endianness(data)); - if (success) then - (* XXX as above TAGw is vestigal and must die *) - TAGw(align(addr, cap_size), 0x00); - success; + MEMval_tag_conditional(addr,size,false,reverse_endianness(data)); } function bit[64] addrWrapper((bit[64]) addr, (MemAccessType) accessType, (WordType) width) = 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 @@ -117,9 +117,11 @@ base_effect_aux = (* effect *) BE_rreg (* read register *) | BE_wreg (* write register *) | BE_rmem (* read memory *) + | BE_rmemt (* read memory tagged *) | BE_wmem (* write memory *) | BE_eamem (* signal effective address for writing memory *) | BE_wmv (* write memory, sending only value *) + | BE_wmvt (* write memory, sending only value and tag *) | BE_barr (* memory barrier *) | BE_depend (* dynamic footprint *) | BE_undef (* undefined-instruction exception *) diff --git a/src/initial_check.ml b/src/initial_check.ml index 82cc6b7c..8f204a65 100644 --- a/src/initial_check.ml +++ b/src/initial_check.ml @@ -277,8 +277,10 @@ and to_ast_effects (k_env : kind Envmap.t) (e : Parse_ast.atyp) : Ast.effect = | Parse_ast.BE_rreg -> BE_rreg | Parse_ast.BE_wreg -> BE_wreg | Parse_ast.BE_rmem -> BE_rmem + | Parse_ast.BE_rmemt -> BE_rmemt | Parse_ast.BE_wmem -> BE_wmem | Parse_ast.BE_wmv -> BE_wmv + | Parse_ast.BE_wmvt -> BE_wmvt | Parse_ast.BE_eamem -> BE_eamem | Parse_ast.BE_depend -> BE_depend | Parse_ast.BE_undef -> BE_undef diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem index 24f624e3..f72bd100 100644 --- a/src/lem_interp/interp.lem +++ b/src/lem_interp/interp.lem @@ -356,9 +356,11 @@ type action = | Read_reg of reg_form * maybe (nat * nat) | Write_reg of reg_form * maybe (nat * nat) * value | Read_mem of id * value * maybe (nat * nat) + | Read_mem_tagged of id * value * maybe (nat * nat) | Write_mem of id * value * maybe (nat * nat) * value | Write_ea of id * value | Write_memv of id * value * value + | Write_memv_tagged of id * value * value * value | Barrier of id * value | Footprint of id * value | Nondet of list (exp tannot) * tag @@ -2227,6 +2229,8 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) = let mk_thunk_frame act = (Action act (mk_thunk l annot t_level le lm), lm, le) in if has_rmem_effect effects then mk_hole_frame (Read_mem (id_of_string name_ext) v Nothing) + else if has_rmemt_effect effects + then mk_hole_frame (Read_mem_tagged (id_of_string name_ext) v Nothing) else if has_barr_effect effects then mk_thunk_frame (Barrier (id_of_string name_ext) v) else if has_depend_effect effects @@ -2251,6 +2255,11 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) = (List_extra.head reved,V_tuple (List.reverse (List_extra.tail reved))) | _ -> (v,unitv) end in mk_hole_frame (Write_memv (id_of_string name_ext) v wv) + else if has_wmvt_effect effects + then match v with + | V_tuple [addr; size; tag; data] -> + mk_hole_frame (Write_memv_tagged (id_of_string name_ext) (V_tuple([addr; size])) tag data) + | _ -> Assert_extra.failwith("wmvt: expected tuple of four elements") end else mk_hole_frame (Call_extern name_ext v) | _ -> (Error l (String.stringAppend "Tag not empty, spec, ctor, or extern on function call " name),lm,le) end) @@ -2384,6 +2393,7 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) = | (Action (Write_reg regf range value) stack) -> a | (Action (Write_mem id a_ range value) stack) -> a | (Action (Write_memv _ _ _) stack) -> a + | (Action (Write_memv_tagged _ _ _ _) stack) -> a | _ -> update_stack a (add_to_top_frame (fun e env -> let (ev,env') = (to_exp mode env v) in @@ -3047,6 +3057,7 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level match a with | Read_reg _ _ -> ((Action a s,lm,le), next_builder, Nothing) | Read_mem _ _ _ -> ((Action a s,lm,le), next_builder, Nothing) + | Read_mem_tagged _ _ _ -> ((Action a s,lm,le), next_builder, Nothing) | Call_extern _ _ -> ((Action a s,lm,le), next_builder, Nothing) | Write_reg ((Reg _ (Just(T_id id',_,_,_,_)) _) as regf) Nothing value -> match in_env subregs id' with diff --git a/src/lem_interp/interp_ast.lem b/src/lem_interp/interp_ast.lem index 64fb14b2..c65963d7 100644 --- a/src/lem_interp/interp_ast.lem +++ b/src/lem_interp/interp_ast.lem @@ -119,9 +119,11 @@ type base_effect_aux = (* effect *) | BE_rreg (* read register *) | BE_wreg (* write register *) | BE_rmem (* read memory *) + | BE_rmemt (* read memory and tag *) | BE_wmem (* write memory *) | BE_eamem (* signal effective address for writing memory *) | BE_wmv (* write memory, sending only value *) + | BE_wmvt (* write memory, sending only value and tag *) | BE_barr (* memory barrier *) | BE_depend (* dynamic footprint *) | BE_undef (* undefined-instruction exception *) diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem index 72bf0bcc..ec747457 100644 --- a/src/lem_interp/interp_inter_imp.lem +++ b/src/lem_interp/interp_inter_imp.lem @@ -96,10 +96,7 @@ let is_bool = function | Bitl_unknown -> false end -let bits_to_ibits l = List.map bit_to_ibit l -let bitls_to_ibits l = List.map bitl_to_ibit l -let bitls_from_ibits l = List.map - (fun b -> +let bitl_from_ibit b = let b = Interp.detaint b in match b with | Interp.V_lit (L_aux L_zero _) -> Bitl_zero @@ -109,7 +106,11 @@ let bitls_from_ibits l = List.map | Interp.V_lit (L_aux L_undef _) -> Bitl_undef | Interp.V_vector _ _ [Interp.V_lit (L_aux L_undef _)] -> Bitl_undef | Interp.V_unknown -> Bitl_unknown - | _ -> Assert_extra.failwith ("bitls_from_ibits given unexpected " ^ (Interp.string_of_value b)) end) l + | _ -> Assert_extra.failwith ("bit_from_ibit given unexpected " ^ (Interp.string_of_value b)) end + +let bits_to_ibits l = List.map bit_to_ibit l +let bitls_to_ibits l = List.map bitl_to_ibit l +let bitls_from_ibits l = List.map bitl_from_ibit l let bits_from_ibits l = List.map (fun b -> @@ -426,12 +427,16 @@ let rec interp_to_value_helper arg ivh_mode err_str instr direction registers ev exn_seen (fun _ -> Interp.resume mode stack Nothing) | (Interp.Action (Interp.Read_mem _ _ _) _,_,_) -> (Ivh_error (Interp_interface.Internal_error ("Read memory request in a " ^ errk_str)), events_out) + | (Interp.Action (Interp.Read_mem_tagged _ _ _) _,_,_) -> + (Ivh_error (Interp_interface.Internal_error ("Read memory tagged request in a " ^ errk_str)), events_out) | (Interp.Action (Interp.Write_mem _ _ _ _) _,_,_) -> (Ivh_error (Interp_interface.Internal_error ("Write memory request in a " ^ errk_str)), events_out) | (Interp.Action (Interp.Write_ea _ _) _,_,_) -> (Ivh_error (Interp_interface.Internal_error ("Write ea request in a " ^ errk_str)), events_out) | (Interp.Action (Interp.Write_memv _ _ _) _,_,_) -> (Ivh_error (Interp_interface.Internal_error ("Write memory value request in a " ^ errk_str)), events_out) + | (Interp.Action (Interp.Write_memv_tagged _ _ _ _) _,_,_) -> + (Ivh_error (Interp_interface.Internal_error ("Write memory value tagged request in a " ^ errk_str)), events_out) | _ -> (Ivh_error (Interp_interface.Internal_error ("Non expected action in a " ^ errk_str)), events_out) end @@ -455,7 +460,7 @@ let translate_address top_level end_flag thunk_name registers address = let (Address bytes i) = address in let mode = make_mode true false in let int_mode = mode.internal_mode in - let (Context top_env direction _ _ _ _ _ _) = top_level in + let (Context top_env direction _ _ _ _ _ _ _ _) = top_level in let intern_val = intern_mem_value mode direction (memory_value_of_address end_flag address) in let val_str = Interp.string_of_value intern_val in let (arg,_) = Interp.to_exp int_mode Interp.eenv intern_val in @@ -499,7 +504,7 @@ let intern_instruction direction (name,parms) = let instruction_analysis top_level end_flag thunk_name regn_to_reg_details registers instruction = let mode = make_mode true false in let int_mode = mode.internal_mode in - let (Context top_env direction _ _ _ _ _ _) = top_level in + let (Context top_env direction _ _ _ _ _ _ _ _) = top_level in let intern_val = intern_instruction direction instruction in let val_str = Interp.string_of_value intern_val in let (arg,_) = Interp.to_exp int_mode Interp.eenv intern_val in @@ -584,7 +589,6 @@ let instruction_analysis top_level end_flag thunk_name regn_to_reg_details regis (Interp.V_ctor (Id_aux (Id r) _) _ _ _) -> IK_mem_read (match r with | "Read_plain" -> Read_plain - | "Read_tag" -> Read_tag | "Read_reserve" -> Read_reserve | "Read_acquire" -> Read_acquire | "Read_exclusive" -> Read_exclusive @@ -595,7 +599,6 @@ let instruction_analysis top_level end_flag thunk_name regn_to_reg_details regis (Interp.V_ctor (Id_aux (Id w) _) _ _ _) -> IK_mem_write (match w with | "Write_plain" -> Write_plain - | "Write_tag" -> Write_tag | "Write_conditional" -> Write_conditional | "Write_release" -> Write_release | "Write_exclusive" -> Write_exclusive @@ -641,7 +644,7 @@ end let interp_value_to_instr_external top_level instr = - let (Context (Interp.Env _ instructions _ _ _ _ _ _) _ _ _ _ _ _ _) = top_level in + let (Context (Interp.Env _ instructions _ _ _ _ _ _) _ _ _ _ _ _ _ _ _) = top_level in match instr with | Interp.V_ctor (Id_aux (Id i) _) _ _ parm -> match (find_instruction i instructions) with @@ -666,7 +669,7 @@ let interp_value_to_instr_external top_level instr = let decode_to_instruction top_level registers value : instruction_or_decode_error = let mode = make_interpreter_mode true false in - let (Context ((Interp.Env _ instructions _ _ _ _ _ _) as top_env) direction _ _ _ _ _ _) = top_level in + let (Context ((Interp.Env _ instructions _ _ _ _ _ _) as top_env) direction _ _ _ _ _ _ _ _) = top_level in let intern_val = intern_opcode direction value in let val_str = Interp.string_of_value intern_val in let (arg,_) = Interp.to_exp mode Interp.eenv intern_val in @@ -703,7 +706,7 @@ end let decode_to_istate (top_level:context) registers (value:opcode) : i_state_or_error = - let (Context top_env _ _ _ _ _ _ _) = top_level in + let (Context top_env _ _ _ _ _ _ _ _ _) = top_level in match decode_to_instruction top_level registers value with | IDE_instr instr instrv -> let mode = make_interpreter_mode true false in @@ -718,7 +721,7 @@ let decode_to_istate (top_level:context) registers (value:opcode) : i_state_or_e let instr_external_to_interp_value top_level instr = - let (Context _ direction _ _ _ _ _ _) = top_level in + let (Context _ direction _ _ _ _ _ _ _ _) = top_level in let (name,parms) = instr in let get_value (_,typ,v) = @@ -745,7 +748,7 @@ let instr_external_to_interp_value top_level instr = val instruction_to_istate : context -> instruction -> instruction_state let instruction_to_istate (top_level:context) (((name, parms) as instr):instruction) : instruction_state = let mode = make_interpreter_mode true false in - let (Context top_env _ _ _ _ _ _ _) = top_level in + let (Context top_env _ _ _ _ _ _ _ _ _) = top_level in let ast_node = fst (Interp.to_exp mode Interp.eenv (instr_external_to_interp_value top_level instr)) in (IState (Interp.Thunk_frame @@ -755,7 +758,7 @@ let instruction_to_istate (top_level:context) (((name, parms) as instr):instruct top_level) let rec interp_to_outcome mode context thunk = - let (Context _ direction mem_reads mem_writes mem_write_eas mem_write_vals barriers spec_externs) = context in + let (Context _ direction mem_reads mem_reads_tagged mem_writes mem_write_eas mem_write_vals mem_write_vals_tagged barriers spec_externs) = context in let internal_direction = if direction = D_increasing then Interp.IInc else Interp.IDec in match thunk () with | (Interp.Value _,lm,le) -> (Done,lm) @@ -784,6 +787,19 @@ let rec interp_to_outcome mode context thunk = else Error ("Memory address on read is not 64 bits") | _ -> Error ("Memory function " ^ i ^ " not found") end , lm) + | Interp.Read_mem_tagged (Id_aux (Id i) _) value slice -> + (match List.lookup i mem_reads_tagged with + | (Just (MRT read_k f)) -> + let (location, length, tracking) = (f mode value) in + if (List.length location) = 8 + then let address_int = match (maybe_all (List.map byte_of_byte_lifted location)) with + | Just bs -> Just (integer_of_byte_list bs) + | _ -> Nothing end in + Read_mem_tagged read_k (Address_lifted location address_int) length tracking + (fun (tag, v) -> IState (Interp.add_answer_to_stack next_state (Interp.V_tuple ([(bitl_to_ibit tag);(intern_mem_value mode direction v)]))) context) + else Error ("Memory address on read is not 64 bits") + | _ -> Error ("Memory function " ^ i ^ " not found") + end , lm) | Interp.Write_mem (Id_aux (Id i) _) loc_val slice write_val -> (match List.lookup i mem_writes with | (Just (MW write_k f return)) -> @@ -832,6 +848,25 @@ let rec interp_to_outcome mode context thunk = | Nothing -> (IState (Interp.add_answer_to_stack next_state Interp.unitv) context) | Just return_bool -> return_bool (IState next_state context) b end) | _ -> Error ("Memory function " ^ i ^ " not found") end, lm) + | Interp.Write_memv_tagged (Id_aux (Id i) _) address_val tag_val write_val -> + (match List.lookup i mem_write_vals_tagged with + | (Just (MVT parmf return)) -> + let (value, v_tracking) = + match (Interp.detaint write_val) with + | Interp.V_tuple[_;v] -> extern_with_track mode extern_mem_value (Interp.retaint write_val v) + | _ -> extern_with_track mode extern_mem_value write_val end in + let location_opt = match parmf mode address_val with + | Nothing -> Nothing + | Just mv -> let address_int = match (maybe_all (List.map byte_of_byte_lifted mv)) with + | Just bs -> Just (integer_of_byte_list bs) + | _ -> Nothing end in Just (Address_lifted mv address_int) end + in + Write_memv_tagged location_opt ((bitl_from_ibit tag_val), value) v_tracking + (fun b -> + match return with + | Nothing -> (IState (Interp.add_answer_to_stack next_state Interp.unitv) context) + | Just return_bool -> return_bool (IState next_state context) b end) + | _ -> Error ("Memory function " ^ i ^ " not found") end, lm) | Interp.Barrier (Id_aux (Id i) _) lval -> (match List.lookup i barriers with | Just barrier -> @@ -899,7 +934,7 @@ end (*ie_loop returns a tuple of event list, and a tuple ofinternal interpreter memory, bool to indicate normal or exceptional termination*) let rec ie_loop mode register_values (IState interp_state context) = - let (Context _ direction externs reads writes write_eas write_vals barriers) = context in + let (Context _ direction externs reads reads_tagged writes write_eas write_vals write_vals_tagged barriers) = context in let unknown_reg size = <| rv_bits = (List.replicate size Bitl_unknown); rv_start = 0; @@ -927,6 +962,9 @@ let rec ie_loop mode register_values (IState interp_state context) = | (Read_mem read_k loc length tracking i_state_fun, _) -> let (events,analysis_data) = ie_loop mode register_values (i_state_fun (unknown_mem length)) in ((E_read_mem read_k loc length tracking)::events,analysis_data) + | (Read_mem_tagged read_k loc length tracking i_state_fun, _) -> + let (events,analysis_data) = ie_loop mode register_values (i_state_fun (Bitl_unknown, (unknown_mem length))) in + ((E_read_memt read_k loc length tracking)::events,analysis_data) | (Write_mem write_k loc length tracking value v_tracking i_state_fun, _) -> let (events,analysis_data) = ie_loop mode register_values (i_state_fun true) in let (events',analysis_data) = ie_loop mode register_values (i_state_fun false) in @@ -940,6 +978,11 @@ let rec ie_loop mode register_values (IState interp_state context) = let (events',analysis_data) = ie_loop mode register_values (i_state_fun false) in (*TODO: consider if lm and lm should be merged*) ((E_write_memv opt_address value tracking)::(events++events'),analysis_data) + | (Write_memv_tagged opt_address value tracking i_state_fun, _) -> + let (events,analysis_data) = ie_loop mode register_values (i_state_fun true) in + let (events',analysis_data) = ie_loop mode register_values (i_state_fun false) in + (*TODO: consider if lm and lm should be merged*) + ((E_write_memvt opt_address value tracking)::(events++events'),analysis_data) | (Barrier barrier_k i_state, _) -> let (events,analysis_data) = ie_loop mode register_values i_state in ((E_barrier barrier_k)::events,analysis_data) @@ -1076,9 +1119,11 @@ let instruction_kind_of_event : event -> maybe instruction_kind = function | E_barrier Barrier_TM_COMMIT -> Just (IK_trans Transaction_commit) | E_read_mem rk _ _ _ -> Just (IK_mem_read rk) + | E_read_memt rk _ _ _ -> Just (IK_mem_read rk) | E_write_mem wk _ _ _ _ _ -> Just (IK_mem_write wk) | E_write_ea wk _ _ _ -> Just (IK_mem_write wk) | E_write_memv _ _ _ -> Nothing + | E_write_memvt _ _ _ -> Nothing | E_barrier bk -> Just (IK_barrier bk) | E_footprint -> Nothing | E_read_reg _ -> Nothing @@ -1091,9 +1136,11 @@ let instruction_kind_of_event : event -> maybe instruction_kind = function let regs_in_of_event : event -> list reg_name = function | E_read_mem _ _ _ _ -> [] + | E_read_memt _ _ _ _ -> [] | E_write_mem _ _ _ _ _ _ -> [] | E_write_ea _ _ _ _ -> [] | E_write_memv _ _ _ -> [] + | E_write_memvt _ _ _ -> [] | E_barrier _ -> [] | E_footprint -> [] | E_read_reg r -> [r] @@ -1104,9 +1151,11 @@ let regs_in_of_event : event -> list reg_name = function let regs_out_of_event : event -> list reg_name = function | E_read_mem _ _ _ _ -> [] + | E_read_memt _ _ _ _ -> [] | E_write_mem _ _ _ _ _ _ -> [] | E_write_ea _ _ _ _ -> [] | E_write_memv _ _ _ -> [] + | E_write_memvt _ _ _ -> [] | E_barrier _ -> [] | E_footprint -> [] | E_read_reg _ -> [] @@ -1119,11 +1168,14 @@ let regs_out_of_event : event -> list reg_name = function let regs_feeding_memory_access_address_of_event : event -> list reg_name = function | E_read_mem _ _ _ (Just rs) -> rs | E_read_mem _ _ _ None -> [] + | E_read_memt _ _ _ (Just rs) -> rs + | E_read_memt _ _ _ None -> [] | E_write_mem _ _ _ (Just rs) _ _ -> rs | E_write_mem _ _ _ None _ _ -> [] | E_write_ea wk _ _ (Just rs) -> rs | E_write_ea wk _ _ None -> [] | E_write_memv _ _ _ -> [] + | E_write_memvt _ _ _ -> [] | E_barrier bk -> [] | E_footprint -> [] | E_read_reg _ -> [] diff --git a/src/lem_interp/interp_interface.lem b/src/lem_interp/interp_interface.lem index 3ef6abb8..fce5b14f 100644 --- a/src/lem_interp/interp_interface.lem +++ b/src/lem_interp/interp_interface.lem @@ -179,17 +179,21 @@ type memory_parameter_transformer = interp_mode -> Interp.value -> (memory_value type optional_memory_transformer = interp_mode -> Interp.value -> maybe memory_value type memory_read = MR of read_kind * memory_parameter_transformer type memory_reads = list (string * memory_read) +type memory_read_tagged = MRT of read_kind * memory_parameter_transformer +type memory_read_taggeds = list (string * memory_read_tagged) type memory_write_ea = MEA of write_kind * memory_parameter_transformer type memory_write_eas = list (string * memory_write_ea) type memory_write = MW of write_kind * memory_parameter_transformer * (maybe (instruction_state -> bool -> instruction_state)) and memory_writes = list (string * memory_write) and memory_write_val = MV of optional_memory_transformer * (maybe (instruction_state -> bool -> instruction_state)) and memory_write_vals = list (string * memory_write_val) +and memory_write_val_tagged = MVT of optional_memory_transformer * (maybe (instruction_state -> bool -> instruction_state)) +and memory_write_vals_tagged = list (string * memory_write_val_tagged) (* Definition information needed to run an instruction *) and context = Context of Interp.top_level * direction * - memory_reads * memory_writes * memory_write_eas * memory_write_vals * barriers * external_functions + memory_reads * memory_read_taggeds * memory_writes * memory_write_eas * memory_write_vals * memory_write_vals_tagged * barriers * external_functions (* An instruction in flight *) and instruction_state = IState of interpreter_state * context @@ -199,6 +203,7 @@ type outcome = (* Request to read N bytes at address *) (* The register list, used when mode.track_values, is those that the address depended on *) | Read_mem of read_kind * address_lifted * nat * maybe (list reg_name) * (memory_value -> instruction_state) +| Read_mem_tagged of read_kind * address_lifted * nat * maybe (list reg_name) * ((bit_lifted * memory_value) -> instruction_state) (* Request to write memory *) | Write_mem of write_kind * address_lifted * nat * maybe (list reg_name) @@ -209,6 +214,7 @@ type outcome = (* Request to write memory at last signaled address. Memory value should be 8* the size given in Write_ea *) | Write_memv of maybe address_lifted * memory_value * maybe (list reg_name) * (bool -> instruction_state) +| Write_memv_tagged of maybe address_lifted * (bit_lifted * memory_value) * maybe (list reg_name) * (bool -> instruction_state) (* Request a memory barrier *) | Barrier of barrier_kind * instruction_state @@ -248,7 +254,7 @@ type outcome = (* Functions to build up the initial state for interpretation *) -val build_context : specification -> memory_reads -> memory_writes -> memory_write_eas -> memory_write_vals -> barriers -> external_functions -> context +val build_context : specification -> memory_reads -> memory_read_taggeds-> memory_writes -> memory_write_eas -> memory_write_vals -> memory_write_vals_tagged -> barriers -> external_functions -> context val initial_instruction_state : context -> string -> list register_value -> instruction_state (* string is a function name, list of value are the parameters to that function *) diff --git a/src/lem_interp/interp_utilities.lem b/src/lem_interp/interp_utilities.lem index 86042d61..f54fad5a 100644 --- a/src/lem_interp/interp_utilities.lem +++ b/src/lem_interp/interp_utilities.lem @@ -105,6 +105,7 @@ end let ~{ocaml} list_to_string format sep list = "" val has_rmem_effect : list base_effect -> bool +val has_rmemt_effect : list base_effect -> bool val has_barr_effect : list base_effect -> bool val has_wmem_effect : list base_effect -> bool val has_depend_effect : list base_effect -> bool @@ -116,8 +117,10 @@ let rec has_effect which efcts = | (BE_rreg,BE_rreg) -> true | (BE_wreg,BE_wreg) -> true | (BE_rmem,BE_rmem) -> true + | (BE_rmemt,BE_rmemt) -> true | (BE_wmem,BE_wmem) -> true | (BE_wmv,BE_wmv) -> true + | (BE_wmvt,BE_wmvt) -> true | (BE_eamem,BE_eamem) -> true | (BE_barr,BE_barr) -> true | (BE_undef,BE_undef) -> true @@ -128,10 +131,12 @@ let rec has_effect which efcts = end end let has_rmem_effect = has_effect BE_rmem +let has_rmemt_effect = has_effect BE_rmemt let has_barr_effect = has_effect BE_barr let has_wmem_effect = has_effect BE_wmem let has_eamem_effect = has_effect BE_eamem let has_wmv_effect = has_effect BE_wmv +let has_wmvt_effect = has_effect BE_wmvt let has_depend_effect = has_effect BE_depend let get_typ (TypSchm_aux (TypSchm_ts tq t) _) = t diff --git a/src/lem_interp/pretty_interp.ml b/src/lem_interp/pretty_interp.ml index 7d182258..c9ec4e76 100644 --- a/src/lem_interp/pretty_interp.ml +++ b/src/lem_interp/pretty_interp.ml @@ -122,8 +122,10 @@ let doc_effect (BE_aux (e,_)) = | BE_rreg -> "rreg" | BE_wreg -> "wreg" | BE_rmem -> "rmem" + | BE_rmemt -> "rmemt" | BE_wmem -> "wmem" | BE_wmv -> "wmv" + | BE_wmvt -> "wmvt" | BE_eamem -> "eamem" | BE_barr -> "barr" | BE_depend -> "depend" diff --git a/src/lem_interp/printing_functions.ml b/src/lem_interp/printing_functions.ml index 4922a59a..9594f238 100644 --- a/src/lem_interp/printing_functions.ml +++ b/src/lem_interp/printing_functions.ml @@ -425,6 +425,10 @@ let rec format_events = function " Read_mem at " ^ (memory_value_to_string E_big_endian location) ^ " based on registers " ^ format_tracking tracking ^ " for " ^ (string_of_int length) ^ " bytes \n" ^ (format_events events) + | (E_read_memt(read_kind, (Address_lifted(location, _)), length, tracking))::events -> + " Read_memt at " ^ (memory_value_to_string E_big_endian location) ^ " based on registers " ^ + format_tracking tracking ^ " for " ^ (string_of_int length) ^ " bytes \n" ^ + (format_events events) | (E_write_mem(write_kind,(Address_lifted (location,_)), length, tracking, value, v_tracking))::events -> " Write_mem at " ^ (memory_value_to_string E_big_endian location) ^ ", based on registers " ^ format_tracking tracking ^ ", writing " ^ (memory_value_to_string E_big_endian value) ^ @@ -438,6 +442,10 @@ let rec format_events = function " Write_memv of " ^ (memory_value_to_string E_big_endian value) ^ ", based on registers " ^ format_tracking v_tracking ^ "\n" ^ (format_events events) + | (E_write_memvt(_, (tag, value), v_tracking))::events -> + " Write_memvt of " ^ (memory_value_to_string E_big_endian value) ^ ", based on registers " ^ + format_tracking v_tracking ^ "\n" ^ + (format_events events) | ((E_barrier b_kind)::events) -> " Memory_barrier occurred\n" ^ (format_events events) diff --git a/src/lem_interp/run_interp_model.ml b/src/lem_interp/run_interp_model.ml index 8be5354a..fc78f163 100644 --- a/src/lem_interp/run_interp_model.ml +++ b/src/lem_interp/run_interp_model.ml @@ -148,7 +148,10 @@ let combine_slices (start, stop) (inner_start,inner_stop) = let unit_lit = (L_aux(L_unit,Interp_ast.Unknown)) -let rec perform_action ((reg, mem, tagmem) as env) = function +let align_addr addr size = + sub addr (modulus addr size) + +let rec perform_action ((reg, mem, tagmem) as env, cap_size) = function (* registers *) | Read_reg1(Reg(id,_,_,_), _) -> (Some(Reg.find id reg), env) | Read_reg1(Reg_slice(id, _, _, range), _) @@ -170,48 +173,41 @@ let rec perform_action ((reg, mem, tagmem) as env) = function | Some a -> a | None -> assert false (*TODO remember how to report an error *)in let naddress = integer_of_address address in - (match kind with - | Read_tag | Read_tag_reserve -> - let tag = Mem.find naddress tagmem in - let rec reading (n : num) length = - if length = 0 - then [] - else (Mem.find n mem)::(reading (add n big_num_unit) (length - 1)) in - (Some (register_value_of_memory_value (tag::(reading naddress length)) !default_order), env) - | _ -> - let rec reading (n : num) length = - if length = 0 - then [] - else (Mem.find n mem)::(reading (add n big_num_unit) (length - 1)) in - (Some (register_value_of_memory_value (reading naddress length) !default_order), env)) + let rec reading (n : num) length = + if length = 0 + then [] + else (Mem.find n mem)::(reading (add n big_num_unit) (length - 1)) in + (Some (register_value_of_memory_value (reading naddress length) !default_order), env) + | Read_mem_tagged0(kind,location, length, _,_) -> + let address = match address_of_address_lifted location with + | Some a -> a + | None -> assert false (*TODO remember how to report an error *)in + let naddress = integer_of_address address in + let tag = Mem.find (align_addr naddress cap_size) tagmem in + let rec reading (n : num) length = + if length = 0 + then [] + else (Mem.find n mem)::(reading (add n big_num_unit) (length - 1)) in + (Some (register_value_of_memory_value (tag::(reading naddress length)) !default_order), env) | Write_mem0(kind,location, length, _, bytes,_,_) -> let address = match address_of_address_lifted location with | Some a -> a | None -> assert false (*TODO remember how to report an error *)in let naddress = integer_of_address address in - (match kind with - | Write_tag | Write_tag_conditional -> - (match bytes with - | [b] -> (None,(reg,mem,Mem.add naddress b tagmem)) - | _ -> assert false) - | _ -> - let rec writing location length bytes mem = - if length = 0 - then mem - else match bytes with + let rec writing location length bytes mem = + if length = 0 + then mem + else match bytes with | [] -> mem | b::bytes -> writing (add location big_num_unit) (length - 1) bytes (Mem.add location b mem) in - (None,(reg,writing naddress length bytes mem,tagmem))) + (None,(reg,writing naddress length bytes mem,tagmem)) | Write_memv1(Some location, bytes, _, _) -> let address = match address_of_address_lifted location with | Some a -> a | _ -> failwith "Write address not known" in let naddress = integer_of_address address in let length = List.length bytes in - let (length,tag_mem,bytes) = if length = 17 || length = 33 - then (length - 1, Mem.add naddress (List.hd bytes) tagmem, (List.tl bytes)) - else (length,tagmem,bytes) in let rec writing location length bytes mem = if length = 0 then mem @@ -219,7 +215,22 @@ let rec perform_action ((reg, mem, tagmem) as env) = function | [] -> mem | b::bytes -> writing (add location big_num_unit) (length - 1) bytes (Mem.add location b mem) in - (None, (reg,writing naddress length bytes mem, tag_mem)) + (None, (reg,writing naddress length bytes mem, tagmem)) + | Write_memv_tagged0(Some location, (tag, bytes), _, _) -> + let address = match address_of_address_lifted location with + | Some a -> a + | _ -> failwith "Write address not known" in + let naddress = integer_of_address address in + let length = List.length bytes in + let rec writing location length bytes mem = + if length = 0 + then mem + else match bytes with + | [] -> mem + | b::bytes -> + writing (add location big_num_unit) (length - 1) bytes (Mem.add location b mem) in + let tagmem = Mem.add (align_addr naddress cap_size) (Byte_lifted ([Bitl_zero;Bitl_zero;Bitl_zero;Bitl_zero;Bitl_zero;Bitl_zero;Bitl_zero;tag])) tagmem in + (None, (reg,writing naddress length bytes mem, tagmem)) | _ -> (None, env) ;; @@ -245,6 +256,7 @@ let run reg mem tagmem + cap_size eager_eval track_dependencies mode @@ -321,7 +333,7 @@ let run errorf "%s: %s: %s\n" (grey name) (red "assertion failed") "No message provided"; (false, mode, !track_dependencies, env) | action -> - let (return,env') = perform_action env action in + let (return,env') = perform_action (env, cap_size) action in let step ?(force=false) (state: instruction_state) = let stack = match state with IState(stack,_) -> stack in let (top_exp,(top_env,top_mem)) = top_frame_exp_state stack in @@ -356,6 +368,22 @@ let run let next = next_thunk (memory_value_of_register_value value) in (step next, env', next) | None -> assert false) + | Read_mem_tagged0(kind, (Address_lifted(location,_)), length, tracking, next_thunk) -> + (match return with + | Some(value) -> + show "read_mem_tagged" + (memory_value_to_string !default_endian location) right + (register_value_to_string value); + (match tracking with + | None -> () + | Some(deps) -> + show "read_mem address depended on" (dependencies_to_string deps) "" ""); + let next = + (match (memory_value_of_register_value value) with + | (Byte_lifted tag)::bytes -> next_thunk ((List.nth tag 7), bytes) + | _ -> assert false) in + (step next, env', next) + | None -> assert false) | Write_mem0(kind,(Address_lifted(location,_)), length, tracking, value, v_tracking, next_thunk) -> show "write_mem" (memory_value_to_string !default_endian location) left (memory_value_to_string !default_endian value); @@ -374,6 +402,10 @@ let run show "write_mem value" (memory_value_to_string !default_endian location) left (memory_value_to_string !default_endian value); let next = next_thunk true in (step next,env',next) + | Write_memv_tagged0(Some(Address_lifted(location,_)),(tag, value),_,next_thunk) -> + show "write_mem_tagged value" (memory_value_to_string !default_endian location) left (memory_value_to_string !default_endian value); + let next = next_thunk true in + (step next,env',next) | Write_ea1(_,(Address_lifted(location,_)), size,_,next) -> show "write_announce" (memory_value_to_string !default_endian location) left ((string_of_int size) ^ " bytes"); (step next, env, next) diff --git a/src/lem_interp/run_with_elf.ml b/src/lem_interp/run_with_elf.ml index 6ce5d5e8..6920b47e 100644 --- a/src/lem_interp/run_with_elf.ml +++ b/src/lem_interp/run_with_elf.ml @@ -1214,7 +1214,7 @@ let rec fde_loop count context model mode track_dependencies addr_trans = then resultf "\nSUCCESS program terminated after %d instructions\n" count else begin - match Run_interp_model.run istate !reg !prog_mem !tag_mem !eager_eval track_dependencies mode "execute" with + match Run_interp_model.run istate !reg !prog_mem !tag_mem (Nat_big_num.of_int 1) !eager_eval track_dependencies mode "execute" with | false, _,_, _ -> errorf "FAILURE\n"; exit 1 | true, mode, track_dependencies, (my_reg, my_mem, my_tags) -> reg := my_reg; @@ -1292,7 +1292,7 @@ let run () = startaddr, startaddr_internal), pp_symbol_map) = initial_system_state_of_elf_file !file in - let context = build_context isa_defs isa_m0 isa_m1 isa_m2 isa_m3 isa_m4 isa_externs in + let context = build_context isa_defs isa_m0 [] isa_m1 isa_m2 isa_m3 [] isa_m4 isa_externs in (*NOTE: this is likely MIPS specific, so should probably pull from initial_system_state info on to translate or not, endian mode, and translate function name *) diff --git a/src/lem_interp/run_with_elf_cheri.ml b/src/lem_interp/run_with_elf_cheri.ml index 546fe6c8..2237d6be 100644 --- a/src/lem_interp/run_with_elf_cheri.ml +++ b/src/lem_interp/run_with_elf_cheri.ml @@ -804,9 +804,11 @@ let initial_system_state_of_elf_file name = (Cheri.defs, (Mips_extras.read_memory_functions, + Mips_extras.read_memory_tagged_functions, Mips_extras.memory_writes, Mips_extras.memory_eas, Mips_extras.memory_vals, + Mips_extras.memory_vals_tagged, Mips_extras.barrier_functions), [], MIPS, @@ -1304,7 +1306,7 @@ let rec fde_loop count context model mode track_dependencies addr_trans = then resultf "\nSUCCESS program terminated after %d instructions\n" count else begin - match Run_interp_model.run istate !reg !prog_mem !tag_mem !eager_eval track_dependencies mode "execute" with + match Run_interp_model.run istate !reg !prog_mem !tag_mem (Nat_big_num.of_int 32) !eager_eval track_dependencies mode "execute" with | false, _,_, _ -> errorf "FAILURE\n"; exit 1 | true, mode, track_dependencies, (my_reg, my_mem, my_tags) -> reg := my_reg; @@ -1377,14 +1379,14 @@ let run () = if !break_point then eager_eval := true; let ((isa_defs, - (isa_m0, isa_m1, isa_m2, isa_m3,isa_m4), + (isa_m0, isa_m1, isa_m2, isa_m3,isa_m4,isa_m5,isa_m6), isa_externs, isa_model, model_reg_d, startaddr, startaddr_internal), pp_symbol_map) = initial_system_state_of_elf_file !file in - let context = build_context isa_defs isa_m0 isa_m1 isa_m2 isa_m3 isa_m4 isa_externs in + let context = build_context isa_defs isa_m0 isa_m1 isa_m2 isa_m3 isa_m4 isa_m5 isa_m6 isa_externs in (*NOTE: this is likely MIPS specific, so should probably pull from initial_system_state info on to translate or not, endian mode, and translate function name *) diff --git a/src/lem_interp/run_with_elf_cheri128.ml b/src/lem_interp/run_with_elf_cheri128.ml index 4c881b04..b34b1753 100644 --- a/src/lem_interp/run_with_elf_cheri128.ml +++ b/src/lem_interp/run_with_elf_cheri128.ml @@ -804,9 +804,11 @@ let initial_system_state_of_elf_file name = (Cheri128.defs, (Mips_extras.read_memory_functions, + Mips_extras.read_memory_tagged_functions, Mips_extras.memory_writes, Mips_extras.memory_eas, Mips_extras.memory_vals, + Mips_extras.memory_vals_tagged, Mips_extras.barrier_functions), [], MIPS, @@ -1304,7 +1306,7 @@ let rec fde_loop count context model mode track_dependencies addr_trans = then resultf "\nSUCCESS program terminated after %d instructions\n" count else begin - match Run_interp_model.run istate !reg !prog_mem !tag_mem !eager_eval track_dependencies mode "execute" with + match Run_interp_model.run istate !reg !prog_mem !tag_mem (Nat_big_num.of_int 16) !eager_eval track_dependencies mode "execute" with | false, _,_, _ -> errorf "FAILURE\n"; exit 1 | true, mode, track_dependencies, (my_reg, my_mem, my_tags) -> reg := my_reg; @@ -1377,14 +1379,14 @@ let run () = if !break_point then eager_eval := true; let ((isa_defs, - (isa_m0, isa_m1, isa_m2, isa_m3,isa_m4), + (isa_m0, isa_m1, isa_m2, isa_m3, isa_m4, isa_m5, isa_m6), isa_externs, isa_model, model_reg_d, startaddr, startaddr_internal), pp_symbol_map) = initial_system_state_of_elf_file !file in - let context = build_context isa_defs isa_m0 isa_m1 isa_m2 isa_m3 isa_m4 isa_externs in + let context = build_context isa_defs isa_m0 isa_m1 isa_m2 isa_m3 isa_m4 isa_m5 isa_m6 isa_externs in (*NOTE: this is likely MIPS specific, so should probably pull from initial_system_state info on to translate or not, endian mode, and translate function name *) 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) diff --git a/src/lexer.mll b/src/lexer.mll index 98c9098d..bc8a1434 100644 --- a/src/lexer.mll +++ b/src/lexer.mll @@ -117,8 +117,10 @@ let kw_table = ("rreg", (fun x -> Rreg)); ("wreg", (fun x -> Wreg)); ("rmem", (fun x -> Rmem)); + ("rmemt", (fun x -> Rmemt)); ("wmem", (fun x -> Wmem)); ("wmv", (fun x -> Wmv)); + ("wmvt", (fun x -> Wmvt)); ("eamem", (fun x -> Eamem)); ("undef", (fun x -> Undef)); ("unspec", (fun x -> Unspec)); diff --git a/src/parse_ast.ml b/src/parse_ast.ml index 2e72761e..5b51439d 100644 --- a/src/parse_ast.ml +++ b/src/parse_ast.ml @@ -77,8 +77,10 @@ base_effect_aux = (* effect *) BE_rreg (* read register *) | BE_wreg (* write register *) | BE_rmem (* read memory *) + | BE_rmemt (* read memory tagged *) | BE_wmem (* write memory *) | BE_wmv (* write memory value *) + | BE_wmvt (* write memory value + tag *) | BE_eamem (* address for write signaled *) | BE_barr (* memory barrier *) | BE_depend (* dynmically dependent footprint *) diff --git a/src/parser.mly b/src/parser.mly index d172f61b..fae8d33f 100644 --- a/src/parser.mly +++ b/src/parser.mly @@ -132,7 +132,7 @@ let make_vector_sugar order_set is_inc typ typ1 = %token Enumerate Else Exit Extern False Forall Foreach Function_ If_ In IN Inc Let_ Member Nat Order %token Pure Rec Register Return Scattered Sizeof Struct Switch Then True TwoStarStar Type TYPE Typedef %token Undefined Union With Val -%token Barr Depend Rreg Wreg Rmem Wmem Wmv Eamem Undef Unspec Nondet Escape +%token Barr Depend Rreg Wreg Rmem Rmemt Wmem Wmv Wmvt Eamem Undef Unspec Nondet Escape /* Avoid shift/reduce conflict - see right_atomic_exp rule */ @@ -309,10 +309,14 @@ effect: { efl BE_wreg } | Rmem { efl BE_rmem } + | Rmemt + { efl BE_rmemt } | Wmem { efl BE_wmem } | Wmv { efl BE_wmv } + | Wmvt + { efl BE_wmvt } | Eamem { efl BE_eamem } | Undef diff --git a/src/pretty_print_common.ml b/src/pretty_print_common.ml index e90d9cf1..8422ab11 100644 --- a/src/pretty_print_common.ml +++ b/src/pretty_print_common.ml @@ -88,8 +88,10 @@ let doc_effect (BE_aux (e,_)) = | BE_rreg -> "rreg" | BE_wreg -> "wreg" | BE_rmem -> "rmem" + | BE_rmemt -> "rmemt" | BE_wmem -> "wmem" | BE_wmv -> "wmv" + | BE_wmvt -> "wmvt" | BE_eamem -> "eamem" | BE_barr -> "barr" | BE_depend -> "depend" diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml index b55685f4..92735f87 100644 --- a/src/pretty_print_lem.ml +++ b/src/pretty_print_lem.ml @@ -125,7 +125,7 @@ let effectful (Effect_aux (eff,_)) = List.exists (fun (BE_aux (eff,_)) -> match eff with - | BE_rreg | BE_wreg | BE_rmem | BE_wmem | BE_eamem | BE_wmv + | BE_rreg | BE_wreg | BE_rmem | BE_rmemt | BE_wmem | BE_eamem | BE_wmv | BE_wmvt | BE_barr | BE_depend | BE_nondet | BE_escape -> true | _ -> false) effs diff --git a/src/pretty_print_lem_ast.ml b/src/pretty_print_lem_ast.ml index 03b8bdf5..54a6168e 100644 --- a/src/pretty_print_lem_ast.ml +++ b/src/pretty_print_lem_ast.ml @@ -181,8 +181,10 @@ and pp_format_base_effect_lem (BE_aux(e,l)) = | BE_rreg -> "BE_rreg" | BE_wreg -> "BE_wreg" | BE_rmem -> "BE_rmem" + | BE_rmemt -> "BE_rmemt" | BE_wmem -> "BE_wmem" | BE_wmv -> "BE_wmv" + | BE_wmvt -> "BE_wmvt" | BE_eamem -> "BE_eamem" | BE_barr -> "BE_barr" | BE_depend -> "BE_depend" diff --git a/src/pretty_print_t_ascii.ml b/src/pretty_print_t_ascii.ml index 79897f4b..1313fb37 100644 --- a/src/pretty_print_t_ascii.ml +++ b/src/pretty_print_t_ascii.ml @@ -96,8 +96,10 @@ and pp_format_base_effect_ascii (BE_aux(e,l)) = | BE_rreg -> "rreg" | BE_wreg -> "wreg" | BE_rmem -> "rmem" + | BE_rmemt -> "rmemt" | BE_wmem -> "wmem" | BE_wmv -> "wmv" + | BE_wmvt -> "wmvt" | BE_eamem -> "eamem" | BE_barr -> "barr" | BE_depend -> "depend" diff --git a/src/type_internal.ml b/src/type_internal.ml index 2eaef407..0459c906 100644 --- a/src/type_internal.ml +++ b/src/type_internal.ml @@ -382,8 +382,10 @@ and ef_to_string (Ast.BE_aux(b,l)) = | Ast.BE_rreg -> "rreg" | Ast.BE_wreg -> "wreg" | Ast.BE_rmem -> "rmem" + | Ast.BE_rmemt -> "rmemt" | Ast.BE_wmem -> "wmem" | Ast.BE_wmv -> "wmv" + | Ast.BE_wmvt -> "wmvt" | Ast.BE_eamem -> "eamem" | Ast.BE_barr -> "barr" | Ast.BE_undef -> "undef" @@ -3075,12 +3077,18 @@ let compare_effect (BE_aux(e1,_)) (BE_aux(e2,_)) = | (BE_rmem,BE_rmem) -> 0 | (BE_rmem,_) -> -1 | (_,BE_rmem) -> 1 + | (BE_rmemt,BE_rmemt) -> 0 + | (BE_rmemt,_) -> -1 + | (_,BE_rmemt) -> 1 | (BE_wmem,BE_wmem) -> 0 | (BE_wmem,_) -> -1 | (_,BE_wmem) -> 1 | (BE_wmv,BE_wmv) -> 0 | (BE_wmv, _ ) -> -1 | (_,BE_wmv) -> 1 + | (BE_wmvt,BE_wmvt) -> 0 + | (BE_wmvt, _ ) -> -1 + | (_,BE_wmvt) -> 1 | (BE_eamem,BE_eamem) -> 0 | (BE_eamem,_) -> -1 | (_,BE_eamem) -> 1 @@ -3139,9 +3147,11 @@ let has_effect searched_for eff = let has_rreg_effect = has_effect (BE_aux(BE_rreg, Parse_ast.Unknown)) let has_wreg_effect = has_effect (BE_aux(BE_wreg, Parse_ast.Unknown)) let has_rmem_effect = has_effect (BE_aux(BE_rmem, Parse_ast.Unknown)) +let has_rmemt_effect = has_effect (BE_aux(BE_rmemt, Parse_ast.Unknown)) let has_wmem_effect = has_effect (BE_aux(BE_wmem, Parse_ast.Unknown)) let has_eamem_effect = has_effect (BE_aux(BE_eamem, Parse_ast.Unknown)) let has_memv_effect = has_effect (BE_aux(BE_wmv, Parse_ast.Unknown)) +let has_memvt_effect = has_effect (BE_aux(BE_wmvt, Parse_ast.Unknown)) let has_lret_effect = has_effect (BE_aux(BE_lret, Parse_ast.Unknown)) (*Similarly to above.*) diff --git a/src/type_internal.mli b/src/type_internal.mli index 4912585a..11aff1ee 100644 --- a/src/type_internal.mli +++ b/src/type_internal.mli @@ -248,9 +248,11 @@ val e_to_string : effect -> string val has_rreg_effect : effect -> bool val has_wreg_effect : effect -> bool val has_rmem_effect : effect -> bool +val has_rmemt_effect : effect -> bool val has_wmem_effect : effect -> bool val has_eamem_effect : effect -> bool val has_memv_effect : effect -> bool +val has_memvt_effect : effect -> bool val has_lret_effect : effect -> bool val initial_kind_env : kind Envmap.t |