1(* ------------------------------------------------------------------------ *) 2(* ARM Machine Code Semantics (A and R profiles) *) 3(* ============================================= *) 4(* Top-level: fetch and run instructions *) 5(* ------------------------------------------------------------------------ *) 6 7(* interactive use: 8 app load ["arm_decoderTheory", "arm_opsemTheory", 9 "pred_setLib", "wordsLib", "parmonadsyntax"]; 10*) 11 12open HolKernel boolLib bossLib Parse pred_setLib; 13 14open arm_coretypesTheory arm_astTheory arm_seq_monadTheory 15 arm_decoderTheory arm_opsemTheory; 16 17val _ = new_theory "arm"; 18 19(* ------------------------------------------------------------------------ *) 20 21val _ = numLib.prefer_num(); 22val _ = wordsLib.prefer_word(); 23 24val _ = temp_overload_on (parmonadsyntax.monad_bind, ``seqT``); 25val _ = temp_overload_on (parmonadsyntax.monad_par, ``parT``); 26val _ = temp_overload_on ("return", ``constT``); 27 28val _ = temp_overload_on ("PAD0", ``list$PAD_LEFT #"0"``); 29 30(* ------------------------------------------------------------------------ *) 31 32(* Get the actual instruction set. An alternative version could raise an error 33 if iset is Thumb, Jazelle or ThumbEE when these aren't avaialble. *) 34 35val actual_instr_set_def = Define` 36 actual_instr_set ii : InstrSet M = 37 read_arch ii >>= 38 (\arch. 39 if arch = ARMv4 then 40 constT InstrSet_ARM 41 else 42 current_instr_set ii >>= 43 (\iset. 44 if iset = InstrSet_Jazelle then 45 have_jazelle ii >>= 46 (\HaveJazelle. 47 constT (if HaveJazelle then iset else InstrSet_ARM)) 48 else if iset = InstrSet_ThumbEE then 49 have_thumbEE ii >>= 50 (\HaveThumbEE. 51 constT (if HaveThumbEE then iset else InstrSet_Thumb)) 52 else 53 constT iset))`; 54 55val fetch_arm_def = Define` 56 fetch_arm ii read_word : (string # Encoding # word4 # ARMinstruction) M = 57 (read_pc ii ||| arch_version ii) >>= 58 (\(pc,v). 59 read_word pc >>= 60 (\ireg. 61 constT (PAD0 8 (word_to_hex_string ireg), 62 Encoding_ARM, arm_decode (v < 5) ireg)))`; 63 64val fetch_thumb_def = Define` 65 fetch_thumb ii ee read_halfword 66 : (string # Encoding # word4 # ARMinstruction) M = 67 (read_pc ii ||| read_cpsr ii ||| read_arch ii) >>= 68 (\(pc,cpsr,arch). 69 read_halfword pc >>= (\ireg1. 70 if ((15 -- 13) ireg1 = 0b111w) /\ (12 -- 11) ireg1 <> 0b00w then 71 read_halfword (pc + 2w) >>= (\ireg2. 72 constT (PAD0 4 (word_to_hex_string ireg1) ++ " " ++ 73 PAD0 4 (word_to_hex_string ireg2), 74 Encoding_Thumb2, thumb2_decode arch cpsr.IT (ireg1,ireg2))) 75 else 76 constT 77 (PAD0 4 (word_to_hex_string ireg1), 78 if ee then 79 thumbee_decode arch cpsr.IT ireg1 80 else 81 (Encoding_Thumb, thumb_decode arch cpsr.IT ireg1))))`; 82 83val fetch_instruction_def = Define` 84 fetch_instruction ii 85 read_word read_halfword : (string # Encoding # word4 # ARMinstruction) M = 86 actual_instr_set ii >>= 87 (\iset. 88 case iset 89 of InstrSet_ARM => fetch_arm ii read_word 90 | InstrSet_Thumb => fetch_thumb ii F read_halfword 91 | InstrSet_ThumbEE => fetch_thumb ii T read_halfword 92 | InstrSet_Jazelle => 93 errorT ("fetch_instruction: Jazelle not supported"))`; 94 95val arm_next_def = Define` 96 arm_next ii irpt : unit M = 97 if irpt = NoInterrupt then 98 waiting_for_interrupt ii >>= 99 (\wfi. 100 condT (~wfi) 101 (fetch_instruction ii 102 (\a. read_memA ii (a, 4) >>= (\d. return (word32 d))) 103 (\a. read_memA ii (a, 2) >>= (\d. return (word16 d))) >>= 104 (\(opc,instr). arm_instr ii instr))) 105 else 106 (if irpt = HW_Reset then 107 take_reset ii 108 else if irpt = HW_Fiq then 109 take_fiq_exception ii 110 else (* irpt = HW_Irq *) 111 take_irq_exception ii) >>= 112 (\u:unit. clear_wait_for_interrupt ii)`; 113 114val arm_run_def = Define` 115 arm_run t ii inp = 116 (forT 0 t 117 (\t. 118 let irpt = inp t in 119 if (irpt = NoInterrupt) \/ (irpt = HW_Reset) then 120 arm_next ii irpt 121 else 122 read_cpsr ii >>= 123 (\cpsr. 124 arm_next ii NoInterrupt >>= 125 (\u:unit. 126 condT ((irpt = HW_Fiq) /\ ~cpsr.F \/ 127 (irpt = HW_Irq) /\ ~cpsr.I) 128 (arm_next ii irpt))))) >>= 129 (\unit_list:unit list. constT ())`; 130 131(* ------------------------------------------------------------------------ *) 132 133val _ = export_theory (); 134