From e9b40edcc325bfe5a0e3566c61ee12a236c5ddf8 Mon Sep 17 00:00:00 2001 From: Robert Norton Date: Thu, 11 May 2017 14:54:32 +0100 Subject: Change types of MEMr_tag, MEMval_tag and co. so that tag is separate from data and invent rmemt and wmvt effects for them. Extend the interpreter context to include lists of tagged memory read and write functions. The memory model must round down the address to the nearest capability aligned address when reading/writing tags. Remove TAGw which is no longer needed as a result. --- src/lem_interp/interp.lem | 11 ++++ src/lem_interp/interp_ast.lem | 2 + src/lem_interp/interp_inter_imp.lem | 84 +++++++++++++++++++++++------ src/lem_interp/interp_interface.lem | 10 +++- src/lem_interp/interp_utilities.lem | 5 ++ src/lem_interp/pretty_interp.ml | 2 + src/lem_interp/printing_functions.ml | 8 +++ src/lem_interp/run_interp_model.ml | 94 ++++++++++++++++++++++----------- src/lem_interp/run_with_elf.ml | 4 +- src/lem_interp/run_with_elf_cheri.ml | 8 +-- src/lem_interp/run_with_elf_cheri128.ml | 8 +-- src/lem_interp/sail_impl_base.lem | 73 +++---------------------- 12 files changed, 187 insertions(+), 122 deletions(-) (limited to 'src/lem_interp') 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) -- cgit v1.2.3