diff options
Diffstat (limited to 'src/lem_interp/interp_inter_imp.lem')
| -rw-r--r-- | src/lem_interp/interp_inter_imp.lem | 63 |
1 files changed, 62 insertions, 1 deletions
diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem index 3413494e..74e43a8f 100644 --- a/src/lem_interp/interp_inter_imp.lem +++ b/src/lem_interp/interp_inter_imp.lem @@ -579,13 +579,74 @@ let instruction_analysis top_level end_flag thunk_name regn_to_reg_details regis | 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 + | "Read_reserve" -> Read_reserve + | "Read_acquire" -> Read_acquire + | "Read_exclusive" -> Read_exclusive + | "Read_exclusive_acquire" -> Read_exclusive_acquire + | "Read_stream" -> Read_stream + | "Read_RISCV_acquire" -> Read_RISCV_acquire + | "Read_RISCV_strong_acquire" -> Read_RISCV_strong_acquire + | "Read_RISCV_reserved" -> Read_RISCV_reserved + | "Read_RISCV_reserved_acquire" -> Read_RISCV_reserved_acquire + | "Read_RISCV_reserved_strong_acquire" -> Read_RISCV_reserved_strong_acquire + | "Read_X86_locked" -> Read_X86_locked + | r -> failwith ("unknown read kind: " ^ r) end in + let writek_to_writek = function + | "Write_plain" -> Write_plain + | "Write_conditional" -> Write_conditional + | "Write_release" -> Write_release + | "Write_exclusive" -> Write_exclusive + | "Write_exclusive_release" -> Write_exclusive_release + | "Write_RISCV_release" -> Write_RISCV_release + | "Write_RISCV_strong_release" -> Write_RISCV_strong_release + | "Write_RISCV_conditional" -> Write_RISCV_conditional + | "Write_RISCV_conditional_release" -> Write_RISCV_conditional_release + | "Write_RISCV_conditional_strong_release" -> Write_RISCV_conditional_strong_release + | "Write_X86_locked" -> Write_X86_locked + | w -> failwith ("unknown write kind: " ^ w) end in + let ik_to_ik = function + | Interp_ast.V_ctor (Id_aux (Id "IK_barrier") _) _ _ + (Interp_ast.V_ctor (Id_aux (Id b) _) _ _ _) -> + IK_barrier (match b with + | "Barrier_Sync" -> Barrier_Sync + | "Barrier_LwSync" -> Barrier_LwSync + | "Barrier_Eieio" -> Barrier_Eieio + | "Barrier_Isync" -> Barrier_Isync + | "Barrier_DMB" -> Barrier_DMB + | "Barrier_DMB_ST" -> Barrier_DMB_ST + | "Barrier_DMB_LD" -> Barrier_DMB_LD + | "Barrier_DSB" -> Barrier_DSB + | "Barrier_DSB_ST" -> Barrier_DSB_ST + | "Barrier_DSB_LD" -> Barrier_DSB_LD + | "Barrier_ISB" -> Barrier_ISB + | "Barrier_MIPS_SYNC" -> Barrier_MIPS_SYNC + | "Barrier_x86_MFENCE" -> Barrier_x86_MFENCE + end) + | Interp_ast.V_ctor (Id_aux (Id "IK_mem_read") _) _ _ + (Interp_ast.V_ctor (Id_aux (Id r) _) _ _ _) -> + IK_mem_read(readk_to_readk r) + | Interp_ast.V_ctor (Id_aux (Id "IK_mem_write") _) _ _ + (Interp_ast.V_ctor (Id_aux (Id w) _) _ _ _) -> + IK_mem_write(writek_to_writek w) + | Interp_ast.V_ctor (Id_aux (Id "IK_mem_rmw") _) _ _ + (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_branch") _) _ _ _ -> + IK_branch + | Interp_ast.V_ctor (Id_aux (Id "IK_simple") _) _ _ _ -> + IK_simple + | _ -> failwith "Analysis returned unexpected instruction kind" + end in 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 nia_to_nia nias, dia_to_dia dia, - fromInterpValue ik) in + ik_to_ik ik) in ((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" |