1(* ========================================================================= *) 2(* FILE : arm_emitScript.sml *) 3(* DATE : 2005 - 2009 *) 4(* ========================================================================= *) 5 6(* interactive use: 7 app load ["wordsLib", "wordsSyntax", "systemTheory", "basis_emitTheory"]; 8*) 9 10open HolKernel boolLib bossLib Parse; 11open Q updateTheory armTheory systemTheory; 12open EmitML basis_emitTheory; 13 14val _ = new_theory "arm_emit"; 15 16val _ = numLib.prefer_num(); 17val _ = wordsLib.prefer_word(); 18 19(*---------------------------------------------------------------------------*) 20 21val num2register = prove( 22 `!n. num2register n = 23 if n = 0 then r0 else 24 if n = 1 then r1 else 25 if n = 2 then r2 else 26 if n = 3 then r3 else 27 if n = 4 then r4 else 28 if n = 5 then r5 else 29 if n = 6 then r6 else 30 if n = 7 then r7 else 31 if n = 8 then r8 else 32 if n = 9 then r9 else 33 if n = 10 then r10 else 34 if n = 11 then r11 else 35 if n = 12 then r12 else 36 if n = 13 then r13 else 37 if n = 14 then r14 else 38 if n = 15 then r15 else 39 if n = 16 then r8_fiq else 40 if n = 17 then r9_fiq else 41 if n = 18 then r10_fiq else 42 if n = 19 then r11_fiq else 43 if n = 20 then r12_fiq else 44 if n = 21 then r13_fiq else 45 if n = 22 then r14_fiq else 46 if n = 23 then r13_irq else 47 if n = 24 then r14_irq else 48 if n = 25 then r13_svc else 49 if n = 26 then r14_svc else 50 if n = 27 then r13_abt else 51 if n = 28 then r14_abt else 52 if n = 29 then r13_und else 53 if n = 30 then r14_und else 54 FAIL num2register ^(mk_var("30 < n",bool)) n`, 55 SRW_TAC [] [num2register_thm, combinTheory.FAIL_THM]); 56 57val num2condition = prove( 58 `!n. num2condition n = 59 if n = 0 then EQ else 60 if n = 1 then CS else 61 if n = 2 then MI else 62 if n = 3 then VS else 63 if n = 4 then HI else 64 if n = 5 then GE else 65 if n = 6 then GT else 66 if n = 7 then AL else 67 if n = 8 then NE else 68 if n = 9 then CC else 69 if n = 10 then PL else 70 if n = 11 then VC else 71 if n = 12 then LS else 72 if n = 13 then LT else 73 if n = 14 then LE else 74 if n = 15 then NV else 75 FAIL num2condition ^(mk_var("15 < n",bool)) n`, 76 SRW_TAC [] [num2condition_thm, combinTheory.FAIL_THM]); 77 78val register_decl = `register = 79 r0 | r1 | r2 | r3 | r4 | r5 | r6 | r7 | 80 r8 | r9 | r10 | r11 | r12 | r13 | r14 | r15 | 81 r8_fiq | r9_fiq | r10_fiq | r11_fiq | r12_fiq | r13_fiq | r14_fiq | 82 r13_irq | r14_irq | 83 r13_svc | r14_svc | 84 r13_abt | r14_abt | 85 r13_und | r14_und`; 86 87val psr_decl = 88 `psr = CPSR | SPSR_fiq | SPSR_irq | SPSR_svc | SPSR_abt | SPSR_und`; 89 90val exceptions_decl = `exceptions = reset | undefined | software | pabort | 91 dabort | address |interrupt | fast`; 92 93val mode_decl = `mode = usr | fiq | irq | svc | abt | und | sys | safe`; 94 95val condition_decl = `condition = EQ | CS | MI | VS | HI | GE | GT | AL | 96 NE | CC | PL | VC | LS | LT | LE | NV`; 97 98val iclass_decl = `iclass = swp | mrs | msr | data_proc | mla_mul | 99 ldr_str | ldrh_strh | ldm_stm | br | swi_ex | 100 cdp_und | mcr | mrc | ldc_stc | unexec`; 101 102val n2w_w2n_rule = GEN_ALL o SIMP_RULE bool_ss [wordsTheory.n2w_w2n]; 103 104val spec_word_rule16 = n2w_w2n_rule o Q.SPEC `w2n (w:word16)`; 105val spec_word_rule32 = n2w_w2n_rule o Q.SPEC `w2n (w:word32)`; 106 107val spec_word_rule12 = 108 n2w_w2n_rule o INST [`opnd2` |-> `w2n (w:word12)`] o SPEC_ALL; 109 110val mem_rule = REWRITE_RULE [GSYM mem_read_def, GSYM mem_write_def]; 111 112fun mk_word n = 113 let val s = Int.toString n 114 val w = "type word" ^ s ^ " = wordsML.word" ^ s 115 in 116 MLSIG w 117 end; 118 119val _ = eSML "update" 120 (OPEN ["num", "sum", "fcp", "words"] 121 :: MLSIG "type 'a word = 'a wordsML.word" 122 :: MLSIG "type num = numML.num" 123 :: MLSIG "type word2 = wordsML.word2" 124 :: MLSIG "type word8 = wordsML.word8" 125 :: MLSIG "type word16 = wordsML.word16" 126 :: MLSIG "type word30 = wordsML.word30" 127 :: MLSIG "type word32 = wordsML.word32" 128 :: MLSTRUCT "type mem = word30->word32" 129 :: MLSIG "type mem" 130 :: MLSTRUCT "val mem_updates = ref ([]: word30 list)" 131 :: MLSIG "val mem_updates : word30 list ref" 132 :: DATATYPE (`formats = SignedByte | UnsignedByte 133 | SignedHalfWord | UnsignedHalfWord 134 | UnsignedWord`) 135 :: DATATYPE (`data = Byte word8 | Half word16 | Word word32`) 136 :: map DEFN [LUPDATE_def, mem_read_def, mem_write_def, mem_write_block_def] 137 @ map (DEFN o mem_rule) 138 [empty_memory_def, mem_items_def, addr30_def, GET_HALF_def, 139 SIMP_RULE std_ss [literal_case_DEF] GET_BYTE_def, 140 FORMAT_def, SET_BYTE_def, SET_HALF_def, 141 MEM_WRITE_BYTE_def, MEM_WRITE_HALF_def, 142 MEM_WRITE_WORD_def, MEM_WRITE_def]); 143 144val _ = eSML "arm" 145 (OPEN ["num", "sum", "option", "set", "fcp", "list", "rich_list", 146 "bit", "words", "update"] 147 :: MLSIG "type 'a itself = 'a fcpML.itself" 148 :: MLSIG "type 'a word = 'a wordsML.word" 149 :: MLSIG "type ('a,'b) cart = ('a,'b) fcpML.cart" 150 :: MLSIG "type ('a,'b) sum = ('a,'b) sumML.sum" 151 :: MLSIG "type 'a bit0 = 'a fcpML.bit0" 152 :: MLSIG "type 'a bit1 = 'a fcpML.bit1" 153 :: MLSIG "type num = numML.num" 154 :: map (fn decl => DATATYPE decl) 155 [register_decl, psr_decl, mode_decl, condition_decl] 156 @ map (fn decl => EQDATATYPE ([], decl)) [exceptions_decl,iclass_decl] 157 @ DATATYPE (`state_inp = <| state : 'a; inp : num -> 'b |>`) 158 :: DATATYPE (`state_out = <| state : 'a; out : 'b |>`) 159 :: map mk_word [2,3,4,5,8,12,16,24,30,32] 160 @ MLSTRUCT "type registers = register->word32" 161 :: MLSTRUCT "type psrs = psr->word32" 162 :: MLSTRUCT "type mem = updateML.mem" 163 :: MLSTRUCT "type data = updateML.data" 164 :: MLSIG "type registers = register->word32" 165 :: MLSIG "type psrs = psr->word32" 166 :: MLSIG "type mem = updateML.mem" 167 :: MLSIG "type data = updateML.data" 168 :: DATATYPE (`regs = <| reg : registers; psr : psrs |>`) 169 :: DATATYPE (`memop = MemRead word32 | MemWrite word32 data | 170 CPWrite word32`) 171 :: DATATYPE (`arm_state = <| regs : regs; ireg : word32; 172 exception : exceptions |>`) 173 :: DATATYPE (`arm_output = <| transfers : memop list; 174 cpi : bool; user : bool |>`) 175 :: DATATYPE (`cp_output = <| data : word32 option list; absent : bool |>`) 176 :: DATATYPE (`bus = <| data : word32 list; memory : mem; abort : num option; 177 cp_state : 'a |>`) 178 :: DATATYPE (`arm_sys_state = <| registers : registers; psrs : psrs; 179 memory : mem; undefined : bool; cp_state : 'a |>`) 180 :: DATATYPE (`interrupt = Reset regs | Undef | Prefetch | 181 Dabort num | Fiq | Irq`) 182 :: DATATYPE (`arm_input = <| ireg : word32; data : word32 list; 183 interrupt : interrupt option; no_cp : bool |>`) 184 :: DATATYPE (`coproc = 185 <| absent : bool -> word32 -> bool; 186 f_cdp : 'a -> bool -> word32 -> 'a; 187 f_mrc : 'a -> bool -> word32 -> word32; 188 f_mcr : 'a -> bool -> word32 -> word32 -> 'a; 189 f_stc : 'a -> bool -> word32 -> word32 option list; 190 f_ldc : 'a -> bool -> word32 -> word32 list -> 'a; 191 n_ldc : 'a -> bool -> word32 -> num |>`) 192 :: MLSTRUCT "val mem_updates = ref ([]: word30 list)" 193 :: MLSIG "val mem_updates : word30 list ref" 194 :: map DEFN (map spec_word_rule32 195 [DECODE_PSR_THM, DECODE_BRANCH_THM, DECODE_DATAP_THM, 196 DECODE_MRS_THM, DECODE_MSR_THM, DECODE_LDR_STR_THM, 197 DECODE_MLA_MUL_THM, DECODE_LDM_STM_THM, DECODE_SWP_THM, 198 DECODE_LDC_STC_THM, DECODE_LDRH_STRH_THM, DECODE_CDP_THM, 199 DECODE_MRC_MCR_THM] 200 @ [DECODE_CPN_def, DECODE_CP_def, USER_def, mode_reg2num_def, 201 DECODE_ARM_def, mode_num_def, exceptions2num_thm, register2num_thm, 202 num2register, num2condition, SET_IFMODE_def, 203 REG_READ_def, REG_WRITE_def, INC_PC_def, FETCH_PC_def, 204 SET_NZCV_def, SET_NZC_def, SET_NZ_def, 205 SIMP_RULE std_ss [literal_case_DEF] DECODE_MODE_def, 206 NZCV_def, CARRY_def, mode2psr_def, SPSR_READ_def, CPSR_READ_def, 207 CPSR_WRITE_def, SPSR_WRITE_def, exception2mode_def, 208 SPECL [`r`,`e`] EXCEPTION_def, BRANCH_def, LSL_def, LSR_def, 209 ASR_def, ROR_def, IMMEDIATE_def, SHIFT_IMMEDIATE2_def, 210 SHIFT_REGISTER2_def, spec_word_rule12 SHIFT_IMMEDIATE_THM, 211 spec_word_rule12 SHIFT_REGISTER_THM, ADDR_MODE1_def, 212 SPEC `f` ALU_arith_def, ALU_logic_def, 213 ADD_def, SUB_def, AND_def, EOR_def, ORR_def, 214 ALU_def, ARITHMETIC_def, TEST_OR_COMP_def, DATA_PROCESSING_def, 215 MRS_def, MSR_def, ALU_multiply_def, MLA_MUL_def, 216 UP_DOWN_def, ADDR_MODE2_def, IMP_DISJ_THM, LDR_STR_def, 217 ADDR_MODE3_def, LDRH_STRH_def,spec_word_rule16 REGISTER_LIST_THM, 218 ADDRESS_LIST_def, WB_ADDRESS_def, FIRST_ADDRESS_def, 219 ADDR_MODE4_def, LDM_LIST_def, STM_LIST_def, LDM_STM_def, 220 SWP_def, MRC_def, MCR_OUT_def, ADDR_MODE5_def, LDC_STC_def, 221 CONDITION_PASSED2_def, CONDITION_PASSED_def, 222 RUN_ARM_def, IS_Reset_def, PROJ_Dabort_def, PROJ_Reset_def , 223 interrupt2exception_def, PROJ_IF_FLAGS_def, NEXT_ARM_def, 224 OUT_ARM_def, mem_rule TRANSFER_def, TRANSFERS_def, 225 OUT_CP_def, RUN_CP_def, mem_rule NEXT_ARM_MMU, 226 mem_rule NEXT_ARM_MEM, empty_registers_def])); 227 228(* -------------------------------------------------------------------------- *) 229 230val _ = export_theory(); 231