From 043ea8ec3faecadf34ef9010bdd539f595f9c6da Mon Sep 17 00:00:00 2001 From: Shaked Flur Date: Thu, 8 Feb 2018 12:06:00 +0000 Subject: replaced NIA_LR/CTR/register with NIA_indirect; removed IK_cond_branch, and added IK_branch --- src/gen_lib/deep_shallow_convert.lem | 4 +-- src/gen_lib/sail_values.lem | 8 ++---- src/lem_interp/interp_inter_imp.lem | 48 +++++++++++++----------------------- src/lem_interp/sail_impl_base.lem | 41 +++++++++--------------------- 4 files changed, 33 insertions(+), 68 deletions(-) (limited to 'src') diff --git a/src/gen_lib/deep_shallow_convert.lem b/src/gen_lib/deep_shallow_convert.lem index 76880dbd..7fea0409 100644 --- a/src/gen_lib/deep_shallow_convert.lem +++ b/src/gen_lib/deep_shallow_convert.lem @@ -532,7 +532,7 @@ let instruction_kindToInterpValue = function | IK_mem_read v -> V_ctor (Id_aux (Id "IK_mem_read") Unknown) (T_id "instruction_kind") C_Union (toInterpValue v) | IK_mem_write v -> V_ctor (Id_aux (Id "IK_mem_write") Unknown) (T_id "instruction_kind") C_Union (toInterpValue v) | IK_mem_rmw v -> V_ctor (Id_aux (Id "IK_mem_rmw") Unknown) (T_id "instruction_kind") C_Union (toInterpValue v) - | IK_cond_branch -> V_ctor (Id_aux (Id "IK_cond_branch") Unknown) (T_id "instruction_kind") C_Union (toInterpValue ()) + | IK_branch -> V_ctor (Id_aux (Id "IK_branch") Unknown) (T_id "instruction_kind") C_Union (toInterpValue ()) | IK_trans v -> V_ctor (Id_aux (Id "IK_trans") Unknown) (T_id "instruction_kind") C_Union (toInterpValue v) | IK_simple -> V_ctor (Id_aux (Id "IK_simple") Unknown) (T_id "instruction_kind") C_Union (toInterpValue ()) end @@ -541,7 +541,7 @@ let rec instruction_kindFromInterpValue v = match v with | V_ctor (Id_aux (Id "IK_mem_read") _) _ _ v -> IK_mem_read (fromInterpValue v) | V_ctor (Id_aux (Id "IK_mem_write") _) _ _ v -> IK_mem_write (fromInterpValue v) | V_ctor (Id_aux (Id "IK_mem_rmw") _) _ _ v -> IK_mem_rmw (fromInterpValue v) - | V_ctor (Id_aux (Id "IK_cond_branch") _) _ _ v -> IK_cond_branch + | V_ctor (Id_aux (Id "IK_branch") _) _ _ v -> IK_branch | V_ctor (Id_aux (Id "IK_trans") _) _ _ v -> IK_trans (fromInterpValue v) | V_ctor (Id_aux (Id "IK_simple") _) _ _ v -> IK_simple | V_tuple [v] -> instruction_kindFromInterpValue v diff --git a/src/gen_lib/sail_values.lem b/src/gen_lib/sail_values.lem index 121f6cc8..ffccaa7e 100644 --- a/src/gen_lib/sail_values.lem +++ b/src/gen_lib/sail_values.lem @@ -912,9 +912,7 @@ type regfp = type niafp = | NIAFP_successor | NIAFP_concrete_address of vector bitU - | NIAFP_LR - | NIAFP_CTR - | NIAFP_register of regfp + | NIAFP_indirect_address (* only for MIPS *) type diafp = @@ -946,9 +944,7 @@ end let niafp_to_nia reginfo = function | NIAFP_successor -> NIA_successor | NIAFP_concrete_address v -> NIA_concrete_address (address_of_bitv v) - | NIAFP_LR -> NIA_LR - | NIAFP_CTR -> NIA_CTR - | NIAFP_register r -> NIA_register (regfp_to_reg reginfo r) + | NIAFP_indirect_address -> NIA_indirect_address end let diafp_to_dia reginfo = function diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem index 2b754e25..9603b9fe 100644 --- a/src/lem_interp/interp_inter_imp.lem +++ b/src/lem_interp/interp_inter_imp.lem @@ -571,13 +571,11 @@ let instruction_analysis top_level end_flag thunk_name regn_to_reg_details regis | Interp_ast.V_ctor (Id_aux (Id "DIAFP_reg") _) _ _ reg -> DIA_register (reg_to_reg_name reg) | _ -> failwith "Register footprint analysis did not return dia of expected type" end in let nia_to_nia = function - | Interp_ast.V_ctor (Id_aux (Id "NIAFP_successor") _) _ _ _-> NIA_successor + | Interp_ast.V_ctor (Id_aux (Id "NIAFP_successor") _) _ _ _ -> NIA_successor | Interp_ast.V_ctor (Id_aux (Id "NIAFP_concrete_address") _) _ _ address -> NIA_concrete_address (get_addr address) - | Interp_ast.V_ctor (Id_aux (Id "NIAFP_LR") _) _ _ _ -> NIA_LR - | Interp_ast.V_ctor (Id_aux (Id "NIAFP_CTR") _) _ _ _ -> NIA_CTR - | Interp_ast.V_ctor (Id_aux (Id "NIAFP_register") _) _ _ reg -> - NIA_register (reg_to_reg_name reg) + | Interp_ast.V_ctor (Id_aux (Id "NIAFP_indirect_address") _) _ _ _ -> + NIA_indirect_address | _ -> failwith "Register footprint analysis did not return nia of expected type" end in let readk_to_readk = function | "Read_plain" -> Read_plain @@ -634,8 +632,8 @@ let instruction_analysis top_level end_flag thunk_name regn_to_reg_details regis (Interp_ast.V_tuple [(Interp_ast.V_ctor (Id_aux (Id readk) _) _ _ _) ; (Interp_ast.V_ctor (Id_aux (Id writek) _) _ _ _)]) -> IK_mem_rmw(readk_to_readk readk, writek_to_writek writek) - | Interp_ast.V_ctor (Id_aux (Id "IK_cond_branch") _) _ _ _ -> - IK_cond_branch + | Interp_ast.V_ctor (Id_aux (Id "IK_branch") _) _ _ _ -> + IK_branch | Interp_ast.V_ctor (Id_aux (Id "IK_simple") _) _ _ _ -> IK_simple | _ -> failwith "Analysis returned unexpected instruction kind" @@ -1157,7 +1155,7 @@ let rr_interp_exhaustive mode i_state events = *) -let instruction_kind_of_event : event -> maybe instruction_kind = function +let instruction_kind_of_event nia_reg : event -> maybe instruction_kind = function (* this is a hack to avoid adding special events for AArch64 transactional-memory *) | E_read_reg (Reg "TMStartEffect" 63 64 D_decreasing) -> Just (IK_trans Transaction_start) | E_write_reg (Reg "TMAbortEffect" 63 64 D_decreasing) _ -> Just (IK_trans Transaction_abort) @@ -1173,7 +1171,9 @@ let instruction_kind_of_event : event -> maybe instruction_kind = function | E_barrier bk -> Just (IK_barrier bk) | E_footprint -> Nothing | E_read_reg _ -> Nothing - | E_write_reg _ _ -> Nothing + | E_write_reg reg _ -> + if register_base_name reg = register_base_name nia_reg then Just IK_branch + else Nothing | E_error s -> failwith ("instruction_kind_of_event error: "^s) | E_escape -> Nothing (*failwith ("instruction_kind_of_event escape")*) end @@ -1252,8 +1252,8 @@ let interp_instruction_analysis (interp_exhaustive : ((list (reg_name * register_value)) -> list event)) instruction nia_reg - (nias_function : (list (maybe address) -> list reg_name -> list nia)) - ism environment = + (nias_function : (list (maybe address) -> list nia)) + ism environment = let es = interp_exhaustive environment in @@ -1263,19 +1263,15 @@ let interp_instruction_analysis let regs_feeding_address = List.concatMap regs_feeding_memory_access_address_of_event es in let nia_address = List.mapMaybe (nia_address_of_event nia_reg) es in - - let nias = nias_function nia_address regs_in in + let nias = nias_function nia_address in let dia = DIA_none in (* FIX THIS! *) - let inst_kind = - match List.mapMaybe instruction_kind_of_event es with - | [] -> if List.length nias > 1 then IK_cond_branch else IK_simple + match List.mapMaybe (instruction_kind_of_event nia_reg) es with + | [] -> IK_simple + | inst_kind :: [] -> inst_kind | inst_kind :: inst_kinds -> - let () = ensure (List.length nias > 1 --> inst_kind = IK_cond_branch) - "multiple NIAs must be IK_cond_branch" in - if forall (inst_kind' MEM inst_kinds). inst_kind' = inst_kind then inst_kind @@ -1286,19 +1282,9 @@ let interp_instruction_analysis | IK_mem_write _ -> true | IK_mem_rmw _ -> false | IK_barrier _ -> false - | IK_cond_branch -> false + | IK_branch -> false | IK_trans _ -> false | IK_simple -> false - end) && - (exists (inst_kind' MEM (inst_kind :: inst_kinds)). - match inst_kind' with - | IK_mem_read _ -> true - | _ -> false - end) && - (exists (inst_kind' MEM (inst_kind :: inst_kinds)). - match inst_kind' with - | IK_mem_write _ -> true - | _ -> false end) then match @@ -1355,7 +1341,7 @@ let interp_compare_analyses interp_exhaustive (instruction : Interp_ast.value) nia_reg - (nias_function : (list (maybe address) -> list reg_name -> list nia)) + (nias_function : (list (maybe address) -> list nia)) ism environment analysis_function diff --git a/src/lem_interp/sail_impl_base.lem b/src/lem_interp/sail_impl_base.lem index de3ba319..c7e01815 100644 --- a/src/lem_interp/sail_impl_base.lem +++ b/src/lem_interp/sail_impl_base.lem @@ -559,10 +559,9 @@ type instruction_kind = | IK_mem_read of read_kind | IK_mem_write of write_kind | IK_mem_rmw of (read_kind * write_kind) - | IK_cond_branch - (* unconditional branches are not distinguished in the instruction_kind; - they just have particular nias (and will be IK_simple *) - (* | IK_uncond_branch *) + | IK_branch (* this includes conditional-branch (multiple nias, none of which is NIA_indirect_address), + indirect/computed-branch (single nia of kind NIA_indirect_address) + and branch/jump (single nia of kind NIA_concrete_address) *) | IK_trans of trans_kind | IK_simple @@ -573,7 +572,7 @@ instance (Show instruction_kind) | IK_mem_read read_kind -> "IK_mem_read " ^ (show read_kind) | IK_mem_write write_kind -> "IK_mem_write " ^ (show write_kind) | IK_mem_rmw (r, w) -> "IK_mem_rmw " ^ (show r) ^ " " ^ (show w) - | IK_cond_branch -> "IK_cond_branch" + | IK_branch -> "IK_branch" | IK_trans trans_kind -> "IK_trans " ^ (show trans_kind) | IK_simple -> "IK_simple" end @@ -1232,32 +1231,18 @@ end type nia = | NIA_successor | NIA_concrete_address of address - | NIA_LR (* "LR0:61 || 0b00" in Power pseudocode *) - | NIA_CTR (* "CTR0:61 || 0b00" in Power pseudocode *) - | NIA_register of reg_name (* the address will be in a register, - corresponds to AArch64 BLR, BR, RET - instructions *) + | NIA_indirect_address let niaCompare n1 n2 = match (n1,n2) with | (NIA_successor, NIA_successor) -> EQ | (NIA_successor, _) -> LT - | (NIA_concrete_address _, NIA_successor) -> GT + | (_, NIA_successor) -> GT | (NIA_concrete_address a1, NIA_concrete_address a2) -> compare a1 a2 | (NIA_concrete_address _, _) -> LT - | (NIA_LR, NIA_successor) -> GT - | (NIA_LR, NIA_concrete_address _) -> GT - | (NIA_LR, NIA_LR) -> EQ - | (NIA_LR, _) -> LT - | (NIA_CTR, NIA_successor) -> GT - | (NIA_CTR, NIA_concrete_address _) -> GT - | (NIA_CTR, NIA_LR) -> GT - | (NIA_CTR, NIA_CTR) -> EQ - | (NIA_CTR, NIA_register _) -> LT - | (NIA_register _, NIA_successor) -> GT - | (NIA_register _, NIA_concrete_address _) -> GT - | (NIA_register _, NIA_LR) -> GT - | (NIA_register _, NIA_CTR) -> GT - | (NIA_register r1, NIA_register r2) -> compare r1 r2 + | (_, NIA_concrete_address _) -> GT + | (NIA_indirect_address, NIA_indirect_address) -> EQ + (* | (NIA_indirect_address, _) -> LT + | (_, NIA_indirect_address) -> GT *) end instance (Ord nia) @@ -1269,11 +1254,9 @@ instance (Ord nia) end let stringFromNia = function - | NIA_successor -> "NIA_successor" + | NIA_successor -> "NIA_successor" | NIA_concrete_address a -> "NIA_concrete_address " ^ show a - | NIA_LR -> "NIA_LR" - | NIA_CTR -> "NIA_CTR" - | NIA_register r -> "NIA_register " ^ show r + | NIA_indirect_address -> "NIA_indirect_address" end instance (Show nia) -- cgit v1.2.3