From 70b8a25d893e8bec8ec05fe313c8e883fb3e8fbc Mon Sep 17 00:00:00 2001 From: Christopher Pulte Date: Fri, 9 Sep 2016 13:30:10 +0100 Subject: update instruction_analysis to support nias and instruction kind --- src/lem_interp/interp_inter_imp.lem | 72 +++++++++++++++++++++++++++++++------ src/lem_interp/interp_interface.lem | 13 ++++++- 2 files changed, 74 insertions(+), 11 deletions(-) (limited to 'src/lem_interp') diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem index 49d8cbfe..f36732fe 100644 --- a/src/lem_interp/interp_inter_imp.lem +++ b/src/lem_interp/interp_inter_imp.lem @@ -470,9 +470,13 @@ let instruction_analysis top_level end_flag thunk_name regn_to_reg_details regis (Interp_ast.Unknown, Nothing)) top_env Interp.eenv (Interp.emem "instruction analysis top level") Interp.Top) Nothing) in match (analysis_or_error) with - | Ivh_value regs -> - (match regs with - | Interp.V_tuple [Interp.V_list regs1; Interp.V_list regs2; Interp.V_list regs3] -> + | Ivh_value analysis -> + (match analysis with + | Interp.V_tuple [Interp.V_list regs1; + Interp.V_list regs2; + Interp.V_list regs3; + Interp.V_list nias; + 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) _)) -> let (start,length,direction,_) = regn_to_reg_details n Nothing in @@ -494,14 +498,62 @@ let instruction_analysis top_level end_flag thunk_name regn_to_reg_details regis Interp.V_lit (L_aux (L_string f) _);]) -> let (start,length,direction,span) = regn_to_reg_details n (Just f) in Reg_field n start direction f span - | _ -> Assert_extra.failwith "Analysis did not return an element of the specified type" end + | _ -> Assert_extra.failwith "Register footprint analysis did not return an element of the specified type" end in - let (regs1,regs2,regs3) = - (List.map reg_to_reg_name regs1, List.map reg_to_reg_name regs2, List.map reg_to_reg_name regs3) in - (Just (regs1,regs2,regs3), events) - | _ -> Assert_extra.failwith "Analysis did not return a three-tuple of lists" end) - | Ivh_value_after_exn _ -> - (Nothing, events) + let get_nia v = address_of_memory_value end_flag (fst (extern_mem_value mode v)) in + let ik_to_ik = function + | Interp.V_ctor (Id_aux (Id "IK_barrier") _) _ _ + (Interp.V_ctor (Id_aux (Id b) _) _ _ _) -> + IK_barrier (match b with + | "Barrier_Sync" -> Sync + | "Barrier_Lwsync" -> LwSync + | "Barrier_Eieio" -> Eieio + | "Barrier_Isync" -> Isync + | "Barrier_DMB" -> DMB + | "Barrier_DMB_ST" -> DMB_ST + | "Barrier_DMB_LD" -> DMB_LD + | "Barrier_DSB" -> DSB + | "Barrier_DSB_ST" -> DSB_ST + | "Barrier_DSB_LD" -> DSB_LD + | "Barrier_ISB" -> ISB + | "Barrier_Sync" -> Sync + end) + | Interp.V_ctor (Id_aux (Id "IK_mem_read") _) _ _ + (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 + | "Read_exclusive_acquire" -> Read_exclusive_acquire + | "Read_stream" -> Read_stream + end) + | Interp.V_ctor (Id_aux (Id "IK_mem_write") _) _ _ + (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 + | "Write_exclusive_release" -> Write_exclusive_release + end) + | Interp.V_ctor (Id_aux (Id "IK_cond_branch") _) _ _ _ -> + IK_cond_branch + | Interp.V_ctor (Id_aux (Id "IK_simple") _) _ _ _ -> + IK_simple + | _ -> failwith "Analysis returned unexpected instruction kind" + end in + let (regs1,regs2,regs3,nias,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, + ik_to_ik ik) in + ((regs1,regs2,regs3,nias,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 | Internal_error msg -> Assert_extra.failwith msg | _ -> Assert_extra.failwith "Not an internal error either" end diff --git a/src/lem_interp/interp_interface.lem b/src/lem_interp/interp_interface.lem index 2da9e060..5473e1a0 100644 --- a/src/lem_interp/interp_interface.lem +++ b/src/lem_interp/interp_interface.lem @@ -416,6 +416,17 @@ type barrier_kind = (* AArch64 barriers *) | DMB | DMB_ST | DMB_LD | DSB | DSB_ST | DSB_LD | ISB +type instruction_kind = + | IK_barrier of barrier_kind + | IK_mem_read of read_kind + | IK_mem_write of write_kind +(* SS reinstating cond_branches +at present branches are not distinguished in the instruction_kind; +they just have particular nias (and will be IK_simple *) + | IK_cond_branch +(* | IK_uncond_branch *) + | IK_simple + (*Map between external functions as preceived from a Sail spec and the actual implementation of the function *) type external_functions = list (string * (Interp.value -> Interp.value)) @@ -1156,7 +1167,7 @@ val translate_address : 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) + -> 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 = -- cgit v1.2.3