diff options
Diffstat (limited to 'src/lem_interp')
| -rw-r--r-- | src/lem_interp/interp_inter_imp.lem | 27 | ||||
| -rw-r--r-- | src/lem_interp/interp_interface.lem | 58 |
2 files changed, 76 insertions, 9 deletions
diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem index 9a06b0ba..483968ca 100644 --- a/src/lem_interp/interp_inter_imp.lem +++ b/src/lem_interp/interp_inter_imp.lem @@ -476,6 +476,7 @@ let instruction_analysis top_level end_flag thunk_name regn_to_reg_details regis Interp.V_list regs2; Interp.V_list regs3; Interp.V_list nias; + dia; ik] -> let reg_to_reg_name v = match v with | Interp.V_ctor (Id_aux (Id "RFull") _) _ _ (Interp.V_lit (L_aux (L_string n) _)) -> @@ -500,7 +501,24 @@ let instruction_analysis top_level end_flag thunk_name regn_to_reg_details regis Reg_field n start direction f (extern_slice direction start span) | _ -> Assert_extra.failwith "Register footprint analysis did not return an element of the specified type" end in - let get_nia v = address_of_memory_value end_flag (fst (extern_mem_value mode v)) in + let get_addr v = match address_of_memory_value end_flag (fst (extern_mem_value mode v)) with + | Just addr -> addr + | Nothing -> failwith "get_nia encountered invalid address" end in + let dia_to_dia = function + | Interp.V_ctor (Id_aux (Id "DIA_none") _) _ _ _ -> DIA_none + | Interp.V_ctor (Id_aux (Id "DIA_concrete") _) _ _ address -> + DIA_concrete_address (get_addr address) + | Interp.V_ctor (Id_aux (Id "DIA_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.V_ctor (Id_aux (Id "NIA_successor") _) _ _ _-> NIA_successor + | Interp.V_ctor (Id_aux (Id "NIA_concrete_address") _) _ _ address -> + NIA_concrete_address (get_addr address) + | Interp.V_ctor (Id_aux (Id "NIA_LR") _) _ _ _ -> NIA_LR + | Interp.V_ctor (Id_aux (Id "NIA_CTR") _) _ _ _ -> NIA_CTR + | Interp.V_ctor (Id_aux (Id "NIA_register") _) _ _ reg -> + NIA_register (reg_to_reg_name reg) + | _ -> failwith "Register footprint analysis did not return nia of expected type" end in let ik_to_ik = function | Interp.V_ctor (Id_aux (Id "IK_barrier") _) _ _ (Interp.V_ctor (Id_aux (Id b) _) _ _ _) -> @@ -544,13 +562,14 @@ let instruction_analysis top_level end_flag thunk_name regn_to_reg_details regis IK_simple | _ -> failwith "Analysis returned unexpected instruction kind" end in - let (regs1,regs2,regs3,nias,ik) = + let (regs1,regs2,regs3,nias,dia,ik) = (List.map reg_to_reg_name regs1, List.map reg_to_reg_name regs2, List.map reg_to_reg_name regs3, - List.map get_nia nias, + List.map nia_to_nia nias, + dia_to_dia dia, ik_to_ik ik) in - ((regs1,regs2,regs3,nias,ik), events) + ((regs1,regs2,regs3,nias,dia,ik), events) | _ -> Assert_extra.failwith "Analysis did not return a four-tuple of lists" end) | Ivh_value_after_exn _ -> Assert_extra.failwith "Instruction analysis failed" | Ivh_error err -> match err with diff --git a/src/lem_interp/interp_interface.lem b/src/lem_interp/interp_interface.lem index cc0bef06..2e649ec1 100644 --- a/src/lem_interp/interp_interface.lem +++ b/src/lem_interp/interp_interface.lem @@ -413,7 +413,6 @@ instance (Show read_kind) end end - type write_kind = (* common writes *) Write_plain @@ -1179,10 +1178,6 @@ val translate_address : context -> end_flag -> string -> maybe (list (reg_name * register_value)) -> address -> maybe address * maybe (list event) -val instruction_analysis : - context -> end_flag -> string -> (string -> (nat * nat * direction * (nat * nat))) - -> maybe (list (reg_name * register_value)) -> instruction -> (list reg_name * list reg_name * list reg_name * list address) - val byte_list_of_memory_value : end_flag -> memory_value -> maybe (list byte) let byte_list_of_memory_value endian mv = let mv = if endian = E_big_endian then mv else List.reverse mv in @@ -1405,3 +1400,56 @@ instance (Show byte_lifted) let show = stringFromByte_lifted end +(* possible next instruction address options *) +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 *) + +let niaCompare n1 n2 = match (n1,n2) with + | (NIA_successor,NIA_successor) -> EQ + | (NIA_concrete_address a1, NIA_concrete_address a2) -> compare a1 a2 + | (NIA_LR,NIA_LR) -> EQ + | (NIA_CTR,NIA_CTR) -> EQ + | (NIA_register r1,NIA_register r2) -> compare r1 r2 + + | (NIA_successor,_) -> LT + | (NIA_concrete_address _,_) -> LT + | (NIA_LR,_) -> LT + | (NIA_CTR,_) -> LT + | (_,_) -> GT + end + +instance (Ord nia) + let compare = niaCompare + let (<) n1 n2 = (niaCompare n1 n2) = LT + let (<=) n1 n2 = (niaCompare n1 n2) <> GT + let (>) n1 n2 = (niaCompare n1 n2) = GT + let (>=) n1 n2 = (niaCompare n1 n2) <> LT +end + +let stringFromNia = function + | 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 +end + +instance (Show nia) + let show = stringFromNia +end + +type dia = + | DIA_none + | DIA_concrete_address of address + | DIA_register of reg_name + + +val instruction_analysis : + context -> end_flag -> string -> (string -> (nat * nat * direction * (nat * nat))) + -> maybe (list (reg_name * register_value)) -> instruction -> (list reg_name * list reg_name * list reg_name * list nia * dia * instruction_kind) |