1(* ------------------------------------------------------------------------ *) 2(* ARM Machine Code Semantics *) 3(* ========================== *) 4(* Use EmitML to generate an SML version of the ARM model *) 5(* ------------------------------------------------------------------------ *) 6 7(* interactive use: 8 app load ["arm_evalTheory", "wordsLib", "pred_setSyntax", "emitLib", 9 "EmitTeX", "extended_emitTheory"]; 10*) 11 12open HolKernel boolLib bossLib Parse wordsLib; 13 14open arm_coretypesTheory arm_astTheory arm_seq_monadTheory 15 arm_decoderTheory arm_opsemTheory armTheory arm_evalTheory; 16 17open EmitML extended_emitTheory; 18 19val _ = new_theory "arm_emit"; 20 21(* ------------------------------------------------------------------------ *) 22 23val bytes = Q.prove( 24 `!w n. 25 bytes (w,n) = 26 if n = 1 then 27 [w2w w] 28 else if n = 2 then 29 [(7 >< 0) w; (15 >< 8) w] 30 else if n = 4 then 31 [(7 >< 0) w; (15 >< 8) w; (23 >< 16) w; (31 >< 24) w] 32 else 33 FAIL bytes ^(mk_var("n not 1, 2 or 4",bool)) (w,n)`, 34 SRW_TAC [] [bytes_def, combinTheory.FAIL_THM]); 35 36val SUM = Q.prove( 37 `!n f. SUM n f = if n = 0 then 0 else SUM (n - 1) f + f (n - 1)`, 38 Cases THEN SRW_TAC [] [sum_numTheory.SUM_def]); 39 40val LESS_THM = 41 CONV_RULE numLib.SUC_TO_NUMERAL_DEFN_CONV prim_recTheory.LESS_THM; 42 43val parallel_add_sub_op1 = Q.prove( 44 `!w. parallel_add_sub_op1 w = 45 case w 46 of 0b01w => Parallel_normal 47 | 0b10w => Parallel_saturating 48 | 0b11w => Parallel_halving 49 | _ => FAIL parallel_add_sub_op1 ^(mk_var("can't decode",bool)) w`, 50 Cases THEN FULL_SIMP_TAC (srw_ss()) 51 [parallel_add_sub_op1_def, LESS_THM, combinTheory.FAIL_THM]); 52 53val parallel_add_sub_op2 = Q.prove( 54 `!w. parallel_add_sub_op2 w = 55 case w 56 of 0b000w => Parallel_add_16 57 | 0b001w => Parallel_add_sub_exchange 58 | 0b010w => Parallel_sub_add_exchange 59 | 0b011w => Parallel_sub_16 60 | 0b100w => Parallel_add_8 61 | 0b111w => Parallel_sub_8 62 | _ => FAIL parallel_add_sub_op2 ^(mk_var("can't decode",bool)) w`, 63 Cases THEN FULL_SIMP_TAC (srw_ss()) 64 [parallel_add_sub_op2_def, LESS_THM, combinTheory.FAIL_THM]); 65 66val parallel_add_sub_thumb_op2 = Q.prove( 67 `!w. parallel_add_sub_thumb_op2 w = 68 case w 69 of 0b001w => Parallel_add_16 70 | 0b010w => Parallel_add_sub_exchange 71 | 0b110w => Parallel_sub_add_exchange 72 | 0b101w => Parallel_sub_16 73 | 0b000w => Parallel_add_8 74 | 0b100w => Parallel_sub_8 75 | _ => FAIL parallel_add_sub_thumb_op2 76 ^(mk_var("can't decode",bool)) w`, 77 Cases THEN FULL_SIMP_TAC (srw_ss()) 78 [parallel_add_sub_thumb_op2_def, LESS_THM, combinTheory.FAIL_THM]); 79 80(* Expand out data_processing_instr wrt ``n2w opc`` *) 81local 82 val dp_thm = ONCE_REWRITE_RULE [LET_THM] 83 (fetch "arm_opsem" "data_processing_instr") 84 fun mk_dp_opc (i,tm) = 85 let val opc = wordsSyntax.mk_wordii(i, 4) in 86 boolSyntax.mk_cond 87 (boolSyntax.mk_eq (``opc:word4``,opc), 88 ``arm_opsem$data_processing_instr ii enc 89 (Data_Processing ^opc setflags n d mode1)``,tm) 90 end 91 val tm = List.foldr mk_dp_opc ``ARB:unit M`` (List.tabulate(16,I)) 92 val thm = Q.prove( 93 `data_processing_instr ii enc 94 (Data_Processing opc setflags n d mode1) = ^tm`, 95 SRW_TAC [] [] THEN Cases_on `opc` 96 THEN FULL_SIMP_TAC (srw_ss()) [LESS_THM] 97 THEN FULL_SIMP_TAC std_ss []) 98 val pos = Lib.index (Lib.equal "data_processing_instr") 99 arm_opsemTheory.instruction_list 100 val data_processing_instr = 101 CONV_RULE (RHS_CONV 102 (SIMP_CONV (srw_ss()) [dp_thm, data_processing_alu_def] 103 THENC DEPTH_CONV (pairLib.LET_SIMP_CONV false))) thm 104 val l = map (fetch "arm_opsem") arm_opsemTheory.instruction_list 105in 106 val instruction_list = 107 let val (l,r) = Lib.split_after pos l in 108 l @ [data_processing_instr] @ (tl r) 109 end 110end; 111 112val i2bits_itself_def = Define` 113 i2bits_itself (i,N,(:'a)) = (i2bits (i,N)) : 'a word`; 114 115val signed_sat_itself_def = Define` 116 signed_sat_itself (i,N,(:'a)) = (signed_sat (i,N)) : 'a word`; 117 118val unsigned_sat_itself_def = Define` 119 unsigned_sat_itself (i,N,(:'a)) = (unsigned_sat (i,N)) : 'a word`; 120 121val signed_sat_q_itself_def = Define` 122 signed_sat_q_itself (i,N,(:'a)) = (signed_sat_q (i,N)) : 'a word # bool`; 123 124val unsigned_sat_q_itself_def = Define` 125 unsigned_sat_q_itself (i,N,(:'a)) = (unsigned_sat_q (i,N)) : 'a word # bool`; 126 127val _ = type_pp.pp_num_types := false; 128val _ = type_pp.pp_array_types := false; 129val _ = temp_disable_tyabbrev_printing "proc"; 130val _ = temp_disable_tyabbrev_printing "FullAddress"; 131val _ = temp_disable_tyabbrev_printing "cpid"; 132val _ = temp_type_abbrev("ARMextensions_set", ``:ARMextensions set``); 133val _ = temp_type_abbrev("word4", ``:bool[4]``); 134val _ = temp_type_abbrev("word32", ``:bool[32]``); 135val _ = temp_clear_overloads_on "UInt" 136val _ = temp_clear_overloads_on "SInt" 137val _ = temp_overload_on("w2i", ``integer_word$w2i``); 138 139fun f x = [QUOTE (trace ("Unicode",0) EmitTeX.datatype_thm_to_string x)] 140 141val n2w_rule = Q.SPEC `n2w m` 142 143val extension_rule = SIMP_RULE (srw_ss()) [thumb2_support_def]; 144 145val int_rule = SIMP_RULE std_ss (COND_RATOR :: map GSYM 146 [basis_emitTheory.i2w_itself_def, 147 i2bits_itself_def, signed_sat_itself_def, unsigned_sat_itself_def, 148 signed_sat_q_itself_def, unsigned_sat_q_itself_def]); 149 150val cons_rule = ONCE_REWRITE_RULE [GSYM (ETA_CONV ``\l. CONS f l``)]; 151 152fun mk_word n = 153let val s = Int.toString n in 154 MLSIG ("type word" ^ s ^ " = wordsML.word" ^ s) 155end; 156 157val _ = emitML (!Globals.emitMLDir) ("arm", 158 [OPEN ["num", "set", "string", "fcp", "bit", "words"], 159 MLSIG "type num = numML.num", 160 MLSIG "type int = intML.int", 161 MLSIG "type 'a ptree = 'a patriciaML.ptree", 162 MLSIG "type 'a set = 'a setML.set", 163 MLSIG "type 'a itself = 'a fcpML.itself", 164 MLSIG "type 'a bit0 = 'a fcpML.bit0", 165 MLSIG "type 'a bit1 = 'a fcpML.bit1", 166 MLSIG "type 'a word = 'a wordsML.word", 167 MLSIG "type ('a,'b) cart = ('a,'b) fcpML.cart", 168 MLSIG "type ('a,'b) sum = ('a,'b) sumML.sum", 169 MLSTRUCT "type int = intML.int", 170 MLSTRUCT "type 'a ptree = 'a patriciaML.ptree"] @ 171 map mk_word [2,3,4,5,6,8,12,16,24,32,64] @ 172 [DATATYPE (f datatype_ARMextensions), 173 MLSIG "type ARMextensions_set = ARMextensions set", 174 MLSTRUCT "type ARMextensions_set = ARMextensions set"] @ 175 map (DATATYPE o f) 176 [datatype_iiid, datatype_RName, datatype_PSRName, datatype_ARMpsr, 177 datatype_CP14reg, datatype_CP15sctlr, datatype_CP15scr, 178 datatype_CP15nsacr, datatype_CP15reg, 179 datatype_coproc_state, datatype_memory_access, datatype_ARMarch, 180 datatype_ARMinfo, datatype_SRType, datatype_InstrSet, datatype_Encoding, 181 datatype_MemType, datatype_MemoryAttributes, datatype_AddressDescriptor, 182 datatype_MBReqDomain, datatype_MBReqTypes, datatype_addressing_mode1, 183 datatype_addressing_mode2, datatype_addressing_mode3, datatype_hint, 184 datatype_parallel_add_sub_op1, datatype_parallel_add_sub_op2, 185 datatype_branch_instruction, datatype_data_processing_instruction, 186 datatype_status_access_instruction, datatype_load_store_instruction, 187 datatype_miscellaneous_instruction, datatype_coprocessor_instruction, 188 datatype_ARMinstruction] @ 189 [MLSIG "type CPinstruction = word4 * (word4 * coprocessor_instruction)", 190 MLSTRUCT "type CPinstruction = word4 * (word4 * coprocessor_instruction)", 191 MLSIG "type exclusive_triple = word32 * (iiid * num)", 192 MLSTRUCT "type exclusive_triple = word32 * (iiid * num)", 193 MLSIG "type exclusive_state = (num -> word32 set) * (word32 * num) set", 194 MLSTRUCT "type exclusive_state = (num -> word32 set) * (word32 * num) set", 195 MLSIG "type 'a ExclusiveM = exclusive_state -> ('a * exclusive_state)", 196 MLSTRUCT "type 'a ExclusiveM = exclusive_state -> ('a * exclusive_state)", 197 MLSIG "type 'a CoprocessorM = coproc_state -> ('a * coproc_state)", 198 MLSTRUCT "type 'a CoprocessorM = coproc_state -> ('a * coproc_state)"] @ 199 map (DATATYPE o f) 200 [datatype_ExclusiveMonitors, datatype_Coprocessors, 201 datatype_arm_state, datatype_error_option] @ 202 [MLSIG "type 'a M = arm_state -> ('a, arm_state) error_option", 203 MLSTRUCT "type 'a M = arm_state -> ('a, arm_state) error_option"] @ 204 map (DEFN o SIMP_RULE (srw_ss()) 205 [Q.ISPEC `FST` COND_RAND, combinTheory.o_THM, 206 i2bits_def, signed_sat_def, unsigned_sat_def, 207 signed_sat_q_def, unsigned_sat_q_def]) 208 [INST_TYPE [alpha |-> ``:8``] integer_wordTheory.i2w_def, i2bits_itself_def, 209 signed_sat_itself_def, unsigned_sat_itself_def, 210 signed_sat_q_itself_def, unsigned_sat_q_itself_def] @ 211 [DEFN data_processing_thumb2_unpredictable_def] @ 212 map (DEFN o int_rule) 213 ([IMP_DISJ_THM, 214 (* arm_coretypes *) 215 n2w_rule align_def, aligned_def, 216 n2w_rule count_leading_zeroes_def, 217 n2w_rule lowest_set_bit_compute, SUM, wordsTheory.bit_count_upto_def, 218 n2w_rule wordsTheory.bit_count_def, zero_extend32_def, 219 sign_extend32_def, word16_def, word32_def, word64_def, 220 bytes, n2w_rule LSL_C_def, LSR_C_def, n2w_rule ASR_C_def, 221 n2w_rule ROR_C_def, RRX_C_def, LSL_def, LSR_def, ASR_def, ROR_def, 222 RRX_def, ITAdvance_def, decode_psr_def, encode_psr_def, version_number_def, 223 224 (* arm_ast *) 225 is_mode1_immediate_def, is_mode2_immediate_def, is_mode3_immediate_def, 226 227 (* arm_seq_monad *) 228 constE_def, seqE_def, constC_def, seqC_def, constT_def, 229 errorT_def, seqT_def, parT_def, lockT_def, condT_def, 230 forT_def, readT_def, writeT_def, read_info_def, 231 read_arch_def, read_extensions_def, read__reg_def, 232 write__reg_def, read__psr_def, write__psr_def, 233 read_scr_def, write_scr_def, read_nsacr_def, 234 read_teehbr_def, read_sctlr_def, read_cpsr_def, write_cpsr_def, 235 read_isetstate_def, write_isetstate_def, 236 have_security_ext, have_jazelle, have_thumbEE, bad_mode_def, read_spsr_def, 237 write_spsr_def, current_mode_is_priviledged_def, 238 current_mode_is_user_or_system_def, is_secure_def, 239 read_vbar_def, read_mvbar_def, current_instr_set_def, 240 select_instr_set_def, RBankSelect_def, RfiqBankSelect_def, 241 LookUpRName_def, read_reg_mode_def, write_reg_mode_def, 242 read_pc_def, pc_store_value_def, read_reg_def, 243 write_reg_def, branch_to_def, increment_pc_def, 244 big_endian_def, translate_address_def, read_monitor_def, 245 write_monitor_def, cons_rule read_mem1_def, cons_rule write_mem1_def, 246 read_mem_def, write_mem_def, read_memA_with_priv_def, 247 write_memA_with_priv_def, read_memU_with_priv_def, 248 write_memU_with_priv_def, read_memA_def, 249 write_memA_def, read_memA_unpriv_def, write_memA_unpriv_def, 250 read_memU_def, write_memU_def, read_memU_unpriv_def, 251 write_memU_unpriv_def, data_memory_barrier_def, 252 data_synchronization_barrier_def, 253 instruction_synchronization_barrier_def, 254 hint_preload_data_for_write_def, hint_preload_data_def, 255 hint_preload_instr_def, hint_yield_def, hint_debug_def, 256 clear_event_register_def, event_registered_def, 257 send_event_def, wait_for_event_def, wait_for_interrupt_def, 258 clear_wait_for_interrupt_def, waiting_for_interrupt_def, 259 set_exclusive_monitors_def, exclusive_monitors_pass_def, 260 clear_exclusive_local_def, read_coprocessors_def, 261 write_coprocessors_def, coproc_accepted_def, 262 coproc_internal_operation_def, coproc_send_loaded_words_def, 263 coproc_get_words_to_store_def, coproc_send_one_word_def, 264 coproc_get_one_word_def, coproc_send_two_words_def, 265 coproc_get_two_words_def, 266 267 (* arm_opsem *) 268 unaligned_support_def, arch_version_def, read_reg_literal_def, 269 read_flags_def, write_flags_def, read_cflag_def, set_q_def, read_ge_def, 270 write_ge_def, write_e_def, extension_rule IT_advance_def, 271 cpsr_write_by_instr_def, spsr_write_by_instr_def, 272 branch_write_pc_def, bx_write_pc_def, load_write_pc_def, 273 alu_write_pc_def, decode_imm_shift_def, decode_reg_shift_def, 274 shift_c_def, shift_def, arm_expand_imm_c_def, thumb_expand_imm_c_def, 275 arm_expand_imm_def, 276 address_mode1_def, address_mode2_def, address_mode3_def, 277 address_mode5_def, 278 signed_parallel_add_sub_16_def, signed_normal_add_sub_16_def, 279 signed_saturating_add_sub_16_def, signed_halving_add_sub_16_def, 280 signed_parallel_add_sub_8_def, signed_normal_add_sub_8_def, 281 signed_saturating_add_sub_8_def, signed_halving_add_sub_8_def, 282 unsigned_parallel_add_sub_16_def, unsigned_normal_add_sub_16_def, 283 unsigned_saturating_add_sub_16_def, unsigned_halving_add_sub_16_def, 284 unsigned_parallel_add_sub_8_def, unsigned_normal_add_sub_8_def, 285 unsigned_saturating_add_sub_8_def, unsigned_halving_add_sub_8_def, 286 parallel_add_sub_def, barrier_option_def, exc_vector_base_def, 287 take_undef_instr_exception_def, take_svc_exception_def, 288 take_smc_exception_def, take_prefetch_abort_exception_def, 289 integer_zero_divide_trapping_enabled_def, null_check_if_thumbEE_def] @ 290 instruction_list @ 291 [condition_passed_def, branch_instruction_def, 292 data_processing_instruction_def, status_access_instruction_def, 293 load_store_instruction_def, miscellaneous_instruction_def, 294 coprocessor_instruction_def, arm_instr_def, 295 296 (* arm_decode and arm_eval *) 297 hint_decode_def, parallel_add_sub_op1, parallel_add_sub_op2, 298 parallel_add_sub_thumb_op2, parallel_add_sub_decode_def, 299 parallel_add_sub_thumb_decode_def, InITBlock_def, LastInITBlock_def, 300 arm_decode_def, extension_rule thumb_decode_def, thumbee_decode_def, 301 thumb2_decode_aux1_def, thumb2_decode_aux2_def, thumb2_decode_aux3_def, 302 thumb2_decode_aux4_def, thumb2_decode_aux5_def, thumb2_decode_aux6_def, 303 thumb2_decode_aux7_def, thumb2_decode_aux8_def, thumb2_decode_aux9_def, 304 extension_rule thumb2_decode_def, proc_def, ptree_read_word_def, 305 ptree_read_halfword_def, fetch_arm_def, fetch_thumb_def, attempt_def, 306 actual_instr_set_def, fetch_instruction_def])); 307 308(* ------------------------------------------------------------------------ *) 309 310val _ = export_theory (); 311