1(* ========================================================================= *) 2(* FILE : arm_evalLib.sml *) 3(* DESCRIPTION : Code for evaluating the I/O free ARM specification *) 4(* *) 5(* AUTHOR : (c) Anthony Fox, University of Cambridge *) 6(* DATE : 2006 - 2007 *) 7(* ========================================================================= *) 8 9structure arm_evalLib :> arm_evalLib = 10struct 11 12(* interactive use: 13 app load ["wordsLib", "computeLib", "pred_setSimps", "arm_evalTheory", 14 "systemTheory", "assemblerML", "instructionTheory", 15 "instructionSyntax"]; 16*) 17 18open HolKernel boolLib bossLib; 19open Q Parse computeLib combinTheory pairTheory wordsTheory wordsSyntax 20 optionTheory rich_listTheory armTheory arm_evalTheory 21 updateTheory systemTheory instructionTheory instructionSyntax assemblerML; 22 23val ERR = mk_HOL_ERR "arm_evalLib" 24 25(* ------------------------------------------------------------------------- *) 26(* Some conversions *) 27 28val SUC_RULE = numLib.SUC_RULE; 29 30fun NUM_ONLY_RULE n x = 31 let val y = SPEC_ALL x 32 in CONJ 33 ((GEN_ALL o INST [n |-> `0`]) y) 34 ((GEN_ALL o INST [n |-> `NUMERAL n`]) y) 35 end; 36 37fun WORD_ONLY_RULE n x = 38 let val y = SPEC_ALL x 39 in CONJ 40 ((GEN_ALL o CONV_RULE (RHS_CONV EVAL_CONV) o INST [n |-> `0w`]) y) 41 ((GEN_ALL o INST [n |-> `n2w (NUMERAL n)`]) y) 42 end; 43 44val arm_compset = wordsLib.words_compset(); 45 46val _ = Lib.C add_thms arm_compset 47 [FST,SND,listTheory.EL_compute,HD,TL,MAP,FILTER,LENGTH,ZIP,FOLDL, 48 APPEND,APPEND_NIL,ELL_compute,LAST_CONS,listTheory.FRONT_CONS, 49 SUC_RULE listTheory.GENLIST,SNOC,listTheory.TAKE_def,K_THM, 50 listTheory.NULL_DEF, 51 register_EQ_register,num2register_thm,register2num_thm, 52 mode_EQ_mode,mode2num_thm,mode_case_def,pairTheory.pair_case_thm, 53 formats_case_def, psr_EQ_psr,psr2num_thm, 54 iclass_EQ_iclass,iclass2num_thm, 55 exceptions_EQ_exceptions,exceptions2num_thm,exceptions_case_def, 56 num2exceptions_thm,exception2mode_def, 57 num2condition_thm,condition2num_thm,condition_case_def, 58 interrupt_case_def, literal_case_THM, iclass_case_def, data_case_def, 59 APPLY_UPDATE_THM, 60 61 SET_NZC_def,NZCV_def,USER_def,mode_num_def, 62 DECODE_IFMODE_SET_NZCV,DECODE_NZCV_SET_NZCV, 63 DECODE_IFMODE_SET_IFMODE,DECODE_NZCV_SET_IFMODE, 64 SET_NZCV_IDEM,SET_IFMODE_IDEM,SET_IFMODE_NZCV_SWP, 65 DECODE_PSR_def,DECODE_MODE_def,DECODE_PSR_THM, 66 CPSR_READ_def,CPSR_WRITE_def,SPSR_READ_def,SPSR_WRITE_def, 67 CPSR_WRITE_n2w,SPSR_WRITE_n2w,mode_reg2num_def,mode2psr_def, 68 REG_READ_def,REG_WRITE_def,INC_PC_def,FETCH_PC_def,REG_READ6_def, 69 word_modify_PSR,word_modify_PSR2, 70 ALU_arith_def,ALU_logic_def,SUB_def,ADD_def, 71 AND_def,EOR_def,ORR_def,ALU_def, 72 LSL_def,LSR_def,ASR_def,ROR_def, 73 WORD_ONLY_RULE `ireg` CONDITION_PASSED_def,CONDITION_PASSED2_def, 74 DECODE_ARM_THM, 75 76 ZIP,FOLDL, 77 regs_accessors, regs_updates_eq_literal, 78 regs_accfupds, regs_fupdfupds, regs_literal_11, 79 regs_fupdfupds_comp, regs_fupdcanon, 80 regs_fupdcanon_comp, 81 arm_state_accessors, arm_state_updates_eq_literal, 82 arm_state_accfupds, arm_state_fupdfupds, arm_state_literal_11, 83 arm_state_fupdfupds_comp, arm_state_fupdcanon, 84 arm_state_fupdcanon_comp, 85 state_inp_accessors, state_inp_updates_eq_literal, 86 state_inp_accfupds, state_inp_fupdfupds, state_inp_literal_11, 87 state_inp_fupdfupds_comp, state_inp_fupdcanon, 88 state_inp_fupdcanon_comp, 89 state_out_accessors, state_out_updates_eq_literal, 90 state_out_accfupds, state_out_fupdfupds, state_out_literal_11, 91 state_out_fupdfupds_comp, state_out_fupdcanon, 92 state_out_fupdcanon_comp, 93 transfer_options_accessors, transfer_options_updates_eq_literal, 94 transfer_options_accfupds, transfer_options_fupdfupds, 95 transfer_options_literal_11, transfer_options_fupdfupds_comp, 96 transfer_options_fupdcanon, transfer_options_fupdcanon_comp, 97 arm_output_accessors, arm_output_updates_eq_literal, 98 arm_output_accfupds, arm_output_fupdfupds, arm_output_literal_11, 99 arm_output_fupdfupds_comp, arm_output_fupdcanon, 100 arm_output_fupdcanon_comp, 101 bus_accessors, bus_updates_eq_literal, 102 bus_accfupds, bus_fupdfupds, bus_literal_11, 103 bus_fupdfupds_comp, bus_fupdcanon, 104 bus_fupdcanon_comp, 105 regs_case_def,shift_case_def, 106 107 DECODE_BRANCH_THM,DECODE_DATAP_THM,DECODE_MRS_THM, 108 DECODE_MSR_THM,DECODE_LDR_STR_THM,DECODE_SWP_THM, 109 DECODE_LDM_STM_THM,DECODE_MLA_MUL_THM,DECODE_LDC_STC_THM, 110 DECODE_CDP_THM,DECODE_MRC_MCR_THM, 111 DECODE_PSRD_def, 112 IS_DP_IMMEDIATE_def, IS_DT_SHIFT_IMMEDIATE_def, IS_MSR_IMMEDIATE_def, 113 IS_DTH_IMMEDIATE_def, 114 115 cond_pass_enc_br, cond_pass_enc_coproc, cond_pass_enc_swp, 116 cond_pass_enc_data_proc, cond_pass_enc_data_proc2, cond_pass_enc_data_proc3, 117 cond_pass_enc_ldm_stm, cond_pass_enc_ldr_str, cond_pass_enc_ldrh_strh, 118 cond_pass_enc_mla_mul, cond_pass_enc_mrs, cond_pass_enc_msr, 119 cond_pass_enc_swi, 120 121 decode_enc_br, decode_enc_coproc, decode_enc_swp, 122 decode_enc_data_proc, decode_enc_data_proc2, decode_enc_data_proc3, 123 decode_enc_ldm_stm, decode_enc_ldr_str, decode_enc_ldrh_strh, 124 decode_enc_mla_mul, decode_enc_mrs, decode_enc_msr, decode_enc_swi, 125 126 decode_br_enc, decode_ldc_stc_enc, decode_mrc_mcr_rd_enc, 127 decode_data_proc_enc, decode_data_proc_enc2, decode_data_proc_enc3, 128 decode_ldm_stm_enc, decode_ldr_str_enc, decode_ldrh_strh_enc, 129 decode_mla_mul_enc, decode_mrs_enc, decode_msr_enc, decode_swp_enc, 130 131 immediate_enc, immediate_enc2, immediate_enc3, register_enc3, 132 shift_immediate_enc, shift_immediate_enc2, shift_immediate_shift_register, 133 shift_register_enc, shift_register_enc2, 134 135 CARRY_def,GET_BYTE_def,GET_HALF_def,FORMAT_def, 136 SHIFT_IMMEDIATE2_def,SHIFT_REGISTER2_def, 137 NUM_ONLY_RULE `opnd2` SHIFT_IMMEDIATE_THM, 138 NUM_ONLY_RULE `opnd2` SHIFT_REGISTER_THM, 139 WORD_ONLY_RULE `opnd2` IMMEDIATE_def, 140 ALU_multiply_def,ARITHMETIC_def,TEST_OR_COMP_def,UP_DOWN_def, 141 ADDR_MODE1_def,ADDR_MODE2_def,ADDR_MODE3_def,ADDR_MODE4_def,ADDR_MODE5_def, 142 REGISTER_LIST_THM,ADDRESS_LIST_def,FIRST_ADDRESS_def,WB_ADDRESS_def, 143 LDM_LIST_def,STM_LIST_def, 144 145 EXCEPTION_def,BRANCH_def,DATA_PROCESSING_def,MRS_def,LDR_STR_def, 146 MLA_MUL_def,SWP_def,MRC_def,MCR_OUT_def,MSR_def,LDM_STM_def,LDC_STC_def, 147 LDRH_STRH_def, 148 149 empty_memory_def,empty_registers_def,empty_psrs_def, 150 SIMP_RULE (std_ss++pred_setSimps.PRED_SET_ss) [] interrupt2exception_def, 151 IS_Reset_def,PROJ_Dabort_def,PROJ_Reset_def, 152 THE_DEF,IS_SOME_DEF,IS_NONE_EQ_NONE,NOT_IS_SOME_EQ_NONE, 153 option_case_ID,option_case_SOME_ID, 154 option_case_def,SOME_11,NOT_SOME_NONE,PROJ_IF_FLAGS_def, 155 sumTheory.OUTL, sumTheory.OUTR, RUN_ARM_def,NEXT_ARM_def, 156 SIMP_RULE (bool_ss++pred_setSimps.PRED_SET_ss) [] OUT_ARM_def, 157 158 arm_sys_state_accessors, arm_sys_state_updates_eq_literal, 159 arm_sys_state_accfupds, arm_sys_state_fupdfupds, arm_sys_state_literal_11, 160 arm_sys_state_fupdfupds_comp, arm_sys_state_fupdcanon, 161 arm_sys_state_fupdcanon_comp, 162 coproc_accessors, coproc_updates_eq_literal, 163 coproc_accfupds, coproc_fupdfupds, 164 coproc_literal_11, coproc_fupdfupds_comp, 165 coproc_fupdcanon, coproc_fupdcanon_comp, 166 cp_output_accessors, cp_output_updates_eq_literal, 167 cp_output_accfupds, cp_output_fupdfupds, cp_output_literal_11, 168 cp_output_fupdfupds_comp, cp_output_fupdcanon, 169 cp_output_fupdcanon_comp, 170 bus_accessors, bus_updates_eq_literal, 171 bus_accfupds, bus_fupdfupds, bus_literal_11, 172 bus_fupdfupds_comp, bus_fupdcanon, 173 bus_fupdcanon_comp, 174 175 memop_case_def, fcpTheory.index_comp, decode_cp_enc_coproc, 176 decode_27_enc_coproc, decode_cdp_enc, decode_mrc_mcr_enc, 177 178 APPLY_LUPDATE_THM, fcpTheory.FCP_APPLY_UPDATE_THM, 179 addr30_def, SET_BYTE_def, SET_HALF_def, TRANSFERS_def, TRANSFER_def, 180 181 MEM_WRITE_BYTE_def, MEM_WRITE_HALF_def, MEM_WRITE_WORD_def, 182 MEM_WRITE_def, OUT_CP_def, RUN_CP_def, NO_CP_def, NEXT_ARM_MMU]; 183 184val ARM_CONV = CBV_CONV arm_compset; 185val ARM_RULE = CONV_RULE ARM_CONV; 186 187fun add_rws f rws = 188let val cmp_set = f() 189 val _ = add_thms rws cmp_set 190in cmp_set end; 191 192val EVAL_UPDATE_CONV = 193let val compset = add_rws reduceLib.num_compset 194 [register_EQ_register,register2num_thm,APPLY_UPDATE_THM] 195in 196 computeLib.CBV_CONV compset 197end; 198 199val SORT_UPDATE_CONV = 200let open arm_evalTheory fcpTheory updateTheory 201 val rule = SIMP_RULE std_ss [register2num_lt_neq, psr2num_lt_neq, 202 prim_recTheory.LESS_NOT_EQ] 203 fun rule1 t = (rule o ISPEC t) UPDATE_SORT_RULE1 204 fun rule2 t = (rule o ISPEC t) UPDATE_SORT_RULE2 205 val Ua_RULE4 = rule1 `\x y. register2num x < register2num y` 206 val Ub_RULE4 = rule2 `\x y. register2num x < register2num y` 207 val Ua_RULE_PSR = rule1 `\x y. psr2num x < psr2num y` 208 val Ub_RULE_PSR = rule2 `\x y. psr2num x < psr2num y` 209 val FUa_RULE = (rule o SPEC `\x y. x < y`) FCP_UPDATE_SORT_RULE1 210 val FUb_RULE = (rule o SPEC `\x y. x < y`) FCP_UPDATE_SORT_RULE2 211 val compset = add_rws wordsLib.words_compset 212 [o_THM,register_EQ_register,register2num_thm,psr_EQ_psr,psr2num_thm, 213 SYM Ua_def,UPDATE_EQ_RULE,Ua_RULE4,Ub_RULE4,Ua_RULE_PSR,Ub_RULE_PSR, 214 SYM FUa_def,FCP_UPDATE_EQ_RULE,FUa_RULE,FUb_RULE, 215 LENGTH,SUC_RULE JOIN,listTheory.DROP_def,APPEND, 216 PURE_REWRITE_RULE [SYM Ua_def] UPDATE_LUPDATE, 217 LIST_UPDATE_SORT_RULE1,LIST_UPDATE_SORT_RULE2,GSYM LUa_def] 218in 219 computeLib.CBV_CONV compset 220 THENC PURE_REWRITE_CONV [Ua_def,Ub_def,FUa_def,FUb_def,LUa_def,LUb_def] 221 THENC SIMP_CONV (srw_ss()) [UPDATE_APPLY_IMP_ID,APPLY_UPDATE_THM, 222 FCP_UPDATE_IMP_ID,FCP_APPLY_UPDATE_THM,FCP_BETA] 223end; 224 225val FOLD_UPDATE_CONV = 226let val compset = add_rws wordsLib.words_compset 227 [SET_IFMODE_def,SET_NZCV_def,FOLDL,APPLY_UPDATE_THM, 228 psr_EQ_psr,psr2num_thm,mode_num_def,mode_case_def, 229 register_EQ_register,register2num_thm, 230 empty_registers_def,empty_memory_def,empty_psrs_def] 231in 232 computeLib.CBV_CONV compset THENC SORT_UPDATE_CONV 233end; 234 235val ARM_ASSEMBLE_CONV = let open instructionTheory 236 val compset = add_rws wordsLib.words_compset 237 [transfer_options_accessors,transfer_options_updates_eq_literal, 238 transfer_options_accfupds,transfer_options_fupdfupds, 239 transfer_options_literal_11,transfer_options_fupdfupds_comp, 240 transfer_options_fupdcanon,transfer_options_fupdcanon_comp, 241 condition2num_thm,arm_instruction_case_def,addr_mode1_case_def, 242 addr_mode2_case_def,addr_mode3_case_def, 243 msr_mode_case_def,condition_encode, 244 shift_encode_def,addr_mode1_encode_def, 245 addr_mode2_encode_def,addr_mode3_encode_def, 246 msr_mode_encode_def,msr_psr_encode_def, 247 options_encode_def,options_encode2_def, 248 data_proc_encode_def,instruction_encode_def,K_THM, 249 SET_NZCV_def,SET_IFMODE_def,mode_num_def,mode_case_def] 250in 251 computeLib.CBV_CONV compset 252end; 253 254val rhsc = rhs o concl; 255val lhsc = lhs o concl; 256val fdest_comb = fst o dest_comb; 257val sdest_comb = snd o dest_comb; 258 259fun printn s = print (s ^ "\n"); 260 261fun findi p l = 262 let fun findin _ [] _ = NONE 263 | findin p (h::t) n = 264 if p h then SOME n else findin p t (n + 1) 265 in 266 findin p l 0 267 end; 268 269fun mapi f l = 270 let fun m f [] i = [] 271 | m f (h::t) i = (f(i, h))::m f t (i + 1) 272 in 273 m f l 0 274 end; 275 276local 277 fun take_dropn(l,n) a = 278 if n = 0 then (rev a,l) 279 else 280 case l of 281 [] => raise Subscript 282 | (h::t) => take_dropn(t,n - 1) (h::a) 283in 284 fun take_drop(l,n) = take_dropn(l,n) [] 285end; 286 287(* ------------------------------------------------------------------------- *) 288(* Syntax *) 289 290fun mk_word30 n = mk_n2w(numSyntax.mk_numeral n,``:30``); 291fun mk_word32 n = mk_n2w(numSyntax.mk_numeral n,``:32``); 292 293fun eval_word t = (numSyntax.dest_numeral o rhsc o FOLD_UPDATE_CONV o mk_w2n) t; 294 295val subst_tm = prim_mk_const{Name = "UPDATE", Thy = "combin"}; 296val lupdate_tm = prim_mk_const{Name = "|:", Thy = "update"}; 297 298fun mk_subst (a,b,m) = 299 list_mk_comb(inst[alpha |-> type_of a,beta |-> type_of b] subst_tm,[a,b,m]) 300 handle HOL_ERR _ => raise ERR "mk_subst" ""; 301 302fun mk_lupdate (a,b,m) = 303 list_mk_comb(inst[alpha |-> dim_of a,beta |-> listSyntax.eltype b] 304 lupdate_tm,[a,b,m]) 305 handle HOL_ERR _ => raise ERR "mk_lupdate" ""; 306 307val dest_subst = dest_triop subst_tm (ERR "dest_word_slice" ""); 308val dest_lupdate = dest_triop lupdate_tm (ERR "dest_word_slice" ""); 309 310local 311 fun do_dest_subst_reg t a = 312 let val (i,d,m) = dest_subst t in 313 do_dest_subst_reg m 314 (if isSome (List.find (fn a => term_eq (fst a) i) a) then a 315 else ((i,d)::a)) 316 end handle HOL_ERR _ => (``ARB:register``,t)::a; 317 318 fun do_dest_subst_mem t a = 319 let val (i,d,m) = dest_lupdate t in 320 do_dest_subst_mem m ((i,fst (listSyntax.dest_list d))::a) 321 end handle HOL_ERR _ => 322 let val (i,d,m) = dest_subst t in 323 do_dest_subst_mem m ((i,[d])::a) 324 end handle HOL_ERR _ => (``ARB:register``,[t])::(rev a); 325in 326 fun dest_subst_reg t = do_dest_subst_reg t [] 327 fun dest_subst_mem t = do_dest_subst_mem t [] 328end; 329 330fun get_reg l rest r = 331 case List.find (fn a => term_eq (fst a) r) l of 332 SOME (x,y) => y 333 | _ => (rhsc o EVAL_UPDATE_CONV o mk_comb) (rest,r); 334 335fun get_pc t = 336 let val regs = dest_subst_reg t 337 val l = tl regs 338 val rest = snd (hd regs) 339 in 340 get_reg l rest ``r15`` 341 end; 342 343datatype mode = USR | FIQ | IRQ | SVC | ABT | UND; 344 345local 346 val split_enum = (snd o strip_comb o sdest_comb o concl); 347 val und_regs = split_enum armTheory.datatype_register; 348 val (usr_regs,und_regs) = take_drop(und_regs,16) 349 val (fiq_regs,und_regs) = take_drop(und_regs,7) 350 val (irq_regs,und_regs) = take_drop(und_regs,2) 351 val (svc_regs,und_regs) = take_drop(und_regs,2) 352 val (abt_regs,und_regs) = take_drop(und_regs,2) 353 354 fun mode2int m = 355 case m of 356 USR => 0 357 | FIQ => 1 358 | IRQ => 2 359 | SVC => 3 360 | ABT => 4 361 | UND => 5; 362 363 fun mode_compare(a,b) = Int.compare(mode2int a, mode2int b); 364 365 fun rm_duplicates (h1::h2::l) = 366 if h1 = h2 then rm_duplicates (h2::l) 367 else h1::(rm_duplicates (h2::l)) 368 | rm_duplicates l = l; 369 370 fun print_reg l rest r = 371 (print_term r; print "="; print_term (get_reg l rest r); print "; "); 372 373 fun print_usr_reg l rest n = 374 if n <= 15 then 375 print_reg l rest (List.nth(usr_regs,n)) 376 else (); 377 378 fun print_fiq_reg l rest n = 379 if 8 <= n andalso n <= 14 then 380 (print_reg l rest (List.nth(fiq_regs,n - 8))) 381 else (); 382 383 fun print_irq_reg l rest n = 384 if 12 < n andalso n < 15 then 385 (print_reg l rest (List.nth(irq_regs,n - 13))) 386 else (); 387 388 fun print_svc_reg l rest n = 389 if 12 < n andalso n < 15 then 390 (print_reg l rest (List.nth(svc_regs,n - 13))) 391 else (); 392 393 fun print_abt_reg l rest n = 394 if 12 < n andalso n < 15 then 395 (print_reg l rest (List.nth(abt_regs,n - 13))) 396 else (); 397 398 fun print_und_reg l rest n = 399 if 12 < n andalso n < 15 then 400 (print_reg l rest (List.nth(und_regs,n - 13))) 401 else (); 402 403 fun mode2printer m = 404 case m of 405 USR => print_usr_reg 406 | FIQ => print_fiq_reg 407 | IRQ => print_irq_reg 408 | SVC => print_svc_reg 409 | ABT => print_abt_reg 410 | UND => print_und_reg; 411 412 val all_modes = [USR,FIQ,IRQ,SVC,ABT,UND]; 413 414 fun pprint_regs p t = 415 let val regs = dest_subst_reg t 416 val l = tl regs 417 val rest = snd (hd regs) 418 in 419 for_se 0 15 (fn i => 420 let val newline = 421 foldl (fn (m,e) => if p (i,m) then 422 ((mode2printer m) l rest i; true) 423 else e) false all_modes 424 in 425 if newline then print "\n" else () 426 end) 427 end 428in 429 val print_all_regs = pprint_regs (K true); 430 val print_usr_regs = pprint_regs (fn (i,m) => m = USR); 431 val print_std_regs = pprint_regs (fn (i,m) => (m = USR) orelse (m = UND)); 432 fun print_regs l = pprint_regs (fn x => mem x l); 433end; 434 435local 436 fun compute_bound (t, tl) = 437 let open Arbnum 438 val n4 = fromInt 4 439 val l = eval_word t 440 in 441 (l, l + fromInt (Int.-(length tl, 1))) 442 end; 443 444 fun get_blocki bounds n = 445 findi (fn (x,y) => Arbnum.<=(x, n) andalso Arbnum.<=(n, y)) bounds; 446 447 fun get_mem_val blocks rest bounds n = 448 case get_blocki bounds n of 449 SOME i => List.nth(List.nth(blocks, i), 450 Arbnum.toInt (Arbnum.-(n, fst (List.nth(bounds, i))))) 451 | NONE => (rhsc o EVAL_UPDATE_CONV o mk_comb) (rest,mk_word30 n) 452in 453 fun read_mem_range m start n = 454 let val dm = dest_subst_mem m 455 val rest = hd (snd (hd (dm))) 456 val bounds = map compute_bound (tl dm) 457 val blocks = map snd (tl dm) 458 val sa = Arbnum.div(start,Arbnum.fromInt 4) 459 val f = get_mem_val blocks rest bounds 460 val n4 = Arbnum.fromInt 4 461 in 462 List.tabulate(n, fn i => let val x = Arbnum.+(sa, Arbnum.fromInt i) in 463 (Arbnum.*(x, n4), f x) end) 464 end 465end; 466 467fun read_mem_block m n = 468 let open Arbnum 469 val dm = List.nth(dest_subst_mem m, n) 470 val sa = eval_word (fst dm) 471 val bl = snd dm 472 val n4 = fromInt 4 473 val addrs = List.tabulate(length bl, fn i => (sa + fromInt i) * n4) 474 in 475 zip addrs bl 476 end; 477 478fun mem_val_to_string(n, t) = 479 "0x" ^ Arbnum.toHexString n ^ ": " ^ 480 (let val (l, r) = dest_comb t in 481 if term_eq l ``enc`` then 482 dest_instruction (SOME n) r 483 else 484 term_to_string t 485 end handle HOL_ERR _ => term_to_string t); 486 487fun print_mem_range m (start, n) = 488 app printn (map mem_val_to_string (read_mem_range m start n)); 489 490fun print_mem_block m n = 491 app printn (map mem_val_to_string (read_mem_block m n)) 492 handle HOL_ERR _ => (); 493 494type arm_state = {mem : term, psrs : term, reg : term, undef : term}; 495 496fun dest_arm_eval t = 497 case snd (TypeBase.dest_record t) of 498 [("registers", reg), ("psrs", psrs), 499 ("memory", mem), ("undefined", undef),("cp_state", cp_reg)] => 500 {mem = mem, reg = reg, psrs = psrs, undef = undef} 501 | _ => raise ERR "dest_arm_eval" ""; 502 503(* ------------------------------------------------------------------------- *) 504 505fun hol_assemble m a l = let 506 val code = map (rhsc o ARM_ASSEMBLE_CONV o 507 (curry mk_comb ``instruction_encode``) o Term) l 508 val block = listSyntax.mk_list(code,``:word32``) 509in 510 rhsc (SORT_UPDATE_CONV (mk_lupdate(mk_word30 a,block,m))) 511end; 512 513fun hol_assemble1 m a t = hol_assemble m a [t]; 514 515local 516 fun add1 a = Data.add32 a Arbnum.one; 517 fun div4 a = Arbnum.div(a,Arbnum.fromInt 4); 518 fun mul4 a = Arbnum.*(a,Arbnum.fromInt 4); 519 val start = Arbnum.zero; 520 521 fun label_table() = 522 ref (Redblackmap.mkDict String.compare); 523 (* 524 Polyhash.mkPolyTable 525 (100,HOL_ERR {message = "Cannot find ARM label\n", 526 origin_function = "", origin_structure = "arm_evalLib"}); 527 *) 528 529 fun mk_links [] ht n = () 530 | mk_links (h::r) ht n = 531 case h of 532 Data.Code c => mk_links r ht (add1 n) 533 | Data.BranchS b => mk_links r ht (add1 n) 534 | Data.BranchN b => mk_links r ht (add1 n) 535 | Data.Label s => 536 (ht := Redblackmap.insert 537 (!ht, s, "0x" ^ Arbnum.toHexString (mul4 n)); 538 (*(Polyhash.insert ht (s, "0x" ^ Arbnum.toHexString (mul4 n));*) 539 mk_links r ht n) 540 | Data.Mark m => mk_links r ht (div4 m); 541 542 fun mk_link_table code = let val ht = label_table() in 543 mk_links code ht start; ht 544 end; 545 546 fun br_to_term (cond,link,label) ht n = 547 let val s = assembler_to_string NONE (Data.BranchS(cond,link,"")) NONE 548 val address = 549 Redblackmap.find (!ht, label) 550 handle Redblackmap.NotFound => 551 raise (HOL_ERR {message = "Cannot find ARM label\n", 552 origin_function = "", origin_structure = 553 "arm_evalLib"}) 554 (*Polyhash.find ht label*) 555 in 556 mk_instruction ("0x" ^ Arbnum.toHexString (mul4 n) ^ ": " ^ s ^ address) 557 end; 558 559 fun mk_enc t = if type_of t = ``:word32`` then t else mk_comb(``enc``, t); 560 561 fun is_label (Data.Label s) = true | is_label _ = false; 562 563 fun lcons h [] = [[h]] 564 | lcons h (x::l) = (h::x)::l; 565 566 fun do_link m l [] ht n = zip m l 567 | do_link m l (h::r) ht n = 568 case h of 569 Data.Code c => 570 do_link m (lcons (mk_enc (arm_to_term (validate_instruction c))) l) 571 r ht (add1 n) 572 | Data.BranchS b => 573 do_link m (lcons (mk_enc (br_to_term b ht n)) l) r ht (add1 n) 574 | Data.BranchN b => 575 let val t = mk_enc (arm_to_term (branch_to_arm b (mul4 n))) in 576 do_link m (lcons t l) r ht (add1 n) 577 end 578 | Data.Label s => do_link m l r ht n 579 | Data.Mark mk => let val k = div4 mk in 580 if k = n then 581 do_link m l r ht n 582 else if null (hd l) then 583 do_link (k::(tl m)) l r ht k 584 else 585 do_link (k::m) ([]::l) r ht k 586 end; 587 588 fun do_links code = 589 let val l = do_link [start] [[]] code (mk_link_table code) start in 590 rev (map (fn (a,b) => (a,rev b)) l) 591 end; 592 593 fun assemble_assambler m a = let 594 val l = do_links a 595 val b = map (fn (m,c) => (mk_word30 m,listSyntax.mk_list(c,``:word32``))) l 596 val t = foldr (fn ((a,c),t) => mk_lupdate(a,c,t)) m b 597 in 598 rhsc (SORT_UPDATE_CONV t) 599 end 600in 601 fun assemble m file = assemble_assambler m (parse_arm file); 602 fun list_assemble m l = 603 let val nll = String.concat (map (fn s => s ^ "\n") l) 604 val c = substring(nll,0,size nll - 1) 605 in 606 assemble_assambler m (string_to_code c) 607 end; 608 fun assemble1 m t = list_assemble m [t]; 609end; 610 611val empty_memory = rhsc empty_memory_def 612val empty_registers = rhsc empty_registers_def 613val empty_psrs = rhsc empty_psrs_def 614 615(* ------------------------------------------------------------------------- *) 616(* Funtions for memory loading and saving *) 617 618local 619 fun bytes2num (b0,b1,b2,b3) = 620 let open Arbnum 621 val byte2num = fromInt o Char.ord o Byte.byteToChar 622 in 623 (byte2num b0) * (fromInt 16777216) + (byte2num b1) * (fromInt 65536) + 624 (byte2num b2) * (fromInt 256) + byte2num b3 625 end 626 627 fun read_word (v,i) = 628 let val l = Word8Vector.length v 629 fun f i = if i < l then Word8Vector.sub(v,i) else 0wx0 630 in 631 mk_word32 (bytes2num (f i, f (i + 1), f (i + 2), f (i + 3))) 632 (* could change order to do little-endian *) 633 end 634in 635 fun load_mem fname skip top_addr m = 636 let open BinIO 637 val istr = openIn fname 638 val data = inputAll istr 639 val _ = closeIn istr 640 val lines = (Word8Vector.length data - skip) div 4 641 val l = List.tabulate(lines, fn i => read_word (data,4 * i + skip)) 642 val lterm = listSyntax.mk_list(l,``:word32``) 643 in 644 rhsc (SORT_UPDATE_CONV (mk_lupdate(mk_word30 top_addr,lterm,m))) 645 end 646end; 647 648fun mem_read m a = (eval_word o rhsc o ARM_CONV) (mk_comb(m,mk_word30 a)); 649 650fun save_mem fname start finish le m = let open BinIO Arbnum 651 fun bits h l n = (n mod pow(two,plus1 h)) div (pow(two,l)) 652 val ostr = openOut fname 653 val num2byte = Word8.fromInt o Arbnum.toInt; 654 fun num2bytes w = 655 map (fn (i,j) => num2byte (bits (fromInt i) (fromInt j) w)) 656 ((if le then rev else I) [(31,24),(23,16),(15,8),(7,0)]) 657 fun save_word i = map (fn b => output1(ostr,b)) (num2bytes (mem_read m i)) 658 fun recurse i = 659 if Arbnum.<=(i,finish) then recurse (save_word i; Arbnum.plus1 i) 660 else closeOut ostr 661in 662 recurse start 663end; 664 665(* ------------------------------------------------------------------------- *) 666(* Set the general purpose, program status and coprocessor registers *) 667 668val foldl_tm = ``FOLDL (\m (r:'a,v:word32). (r =+ v) m) x y``; 669 670fun assign_type_reg_list (t:term frag list) = 671 let val s = case hd t of QUOTE s => s | ANTIQUOTE x => "" in 672 Term [QUOTE (s ^ ": (register # word32) list")] 673 end; 674 675fun assign_type_psr_list (t:term frag list) = 676 let val s = case hd t of QUOTE s => s | ANTIQUOTE x => "" in 677 Term [QUOTE (s ^ ": (psr # word32) list")] 678 end; 679 680fun set_registers reg rvs = 681 (rhsc o FOLD_UPDATE_CONV o 682 subst [``x:registers`` |-> reg, 683 ``y:(register # word32) list`` |-> assign_type_reg_list rvs] o 684 inst [alpha |-> ``:register``]) foldl_tm; 685 686fun set_status_registers psr rvs = (rhsc o 687 (FOLD_UPDATE_CONV 688 THENC PURE_ONCE_REWRITE_CONV [SPEC `n2w n` arm_evalTheory.PSR_CONS] 689 THENC ARM_CONV) o 690 subst [``x:psrs`` |-> psr, 691 ``y:(psr # word32) list`` |-> assign_type_psr_list rvs] o 692 inst [alpha |-> ``:psr``]) foldl_tm; 693 694(* ------------------------------------------------------------------------- *) 695(* Running the model *) 696 697fun init f m r s c = 698 let 699 val ftyp = type_of f 700 val ttyp = type_of c 701 in 702 (PURE_ONCE_REWRITE_CONV [CONJUNCT1 STATE_ARM_MMU_def] o 703 subst [``f:^(ty_antiq ftyp)`` |-> f, ``mem:mem`` |-> m, 704 ``registers:registers`` |-> r, ``psrs:psrs`` |-> s, 705 ``cp_state:^(ty_antiq ttyp)`` |-> c]) 706 ``STATE_ARM_MMU (f:^(ty_antiq ftyp)) 0 707 <| registers := registers; psrs := psrs; 708 memory := mem; undefined := F; 709 cp_state := cp_state:^(ty_antiq ttyp) |>`` 710 end; 711 712(* 713 reg - rator 714 psr - rand rator 715 mem - rand rand rator 716 und - rand rand rand rator 717 cps - rand rand rand rand 718*) 719 720val NEXT_ARM_CONV = 721 ARM_CONV THENC 722 ONCE_DEPTH_CONV (RATOR_CONV SORT_UPDATE_CONV) THENC 723 ONCE_DEPTH_CONV (RAND_CONV (RATOR_CONV SORT_UPDATE_CONV)) THENC 724 ONCE_DEPTH_CONV (RAND_CONV (RAND_CONV (RATOR_CONV SORT_UPDATE_CONV))) THENC 725 ONCE_DEPTH_CONV 726 (RAND_CONV (RAND_CONV (RAND_CONV (RAND_CONV SORT_UPDATE_CONV)))) THENC 727 RATOR_CONV ARM_ASSEMBLE_CONV THENC 728 RAND_CONV (RAND_CONV (RAND_CONV (RAND_CONV ARM_ASSEMBLE_CONV))); 729 730fun next(f, t) = 731 let val t0 = rhsc t 732 val ttyp = type_of t0 733 val ftyp = type_of f 734 val t1 = (NEXT_ARM_CONV o 735 subst [``f:^(ty_antiq ftyp)`` |-> f, 736 ``s:^(ty_antiq ttyp)`` |-> t0]) 737 ``NEXT_ARM_MMU (f:^(ty_antiq ftyp)) (s:^(ty_antiq ttyp))`` 738 in 739 numLib.REDUCE_RULE (MATCH_MP STATE_ARM_MMU_NEXT (CONJ t t1)) 740 end; 741 742fun done t = term_eq T (#undef (dest_arm_eval (rhsc t))); 743 744fun lstate _ _ _ [] = [] 745 | lstate (tmr,prtr) n f (l as (t::ts)) = 746 if n = 0 then l 747 else 748 let val _ = prtr (dest_arm_eval (rhsc t)) 749 val nl = (tmr next (f, t)) :: l 750 in 751 if done t then nl else lstate (tmr,prtr) (n - 1) f nl 752 end; 753 754fun state (tmr,prtr) n f s = 755 if n = 0 then s 756 else 757 let val _ = prtr (dest_arm_eval (rhsc s)) 758 val ns = tmr next (f, s) 759 in 760 if done s then ns else state (tmr,prtr) (n - 1) f ns 761 end; 762 763fun pc_ptr (x : arm_state) = 764 let val pc = eval_word (get_pc (#reg x)) in 765 if term_eq T (#undef x) then 766 print ("0x" ^ Arbnum.toHexString pc ^ ": undefined exception\n") 767 else 768 print_mem_range (#mem x) (pc, 1) 769 end; 770 771fun A f x = f x 772 773fun evaluate_cp (n, f, m, r, s, p) = state (A,pc_ptr) n f (init f m r s p) 774fun eval_cp (n, f, m, r, s, p) = lstate (time,pc_ptr) n f [init f m r s p] 775 776fun evaluate (n, m, r, s) = 777 evaluate_cp (n, ``NO_CP:unit coproc``, m, r, s, ``()``); 778 779fun eval (n, m, r, s) = 780 eval_cp (n, ``NO_CP:unit coproc``, m, r, s, ``()``); 781 782(* ------------------------------------------------------------------------- *) 783 784fun myprint Gs backend sys ppfns (pg,lg,rg) d t = let 785 open Portable term_pp_types smpp 786 infix >> 787 val {add_string=strn,add_break=brk,ublock,add_newline,...} = 788 ppfns : ppstream_funs 789 val (l,typ) = listSyntax.dest_list t 790 val _ = typ = ``:word32`` andalso not (null l) orelse raise UserPP_Failed 791 fun delim act = 792 case pg of 793 Prec(_, "CONS") => act 794 | _ => ublock CONSISTENT 0 795 (strn "[" >> brk (1,1) >> 796 ublock CONSISTENT 0 (act >> brk(1,0) >> strn "]")) 797in 798 delim ( 799 smpp.pr_list 800 (sys {gravs = (Prec(0, "CONS"), Top, Top), 801 depth = d - 1, binderp = false}) 802 (strn ";" >> add_newline) 803 l) 804end handle HOL_ERR _ => raise term_pp_types.UserPP_Failed; 805 806val _ = temp_add_user_printer 807 ("arm_evalLib.myprint", ``x:word32 list``, myprint); 808 809(* ------------------------------------------------------------------------- *) 810 811end 812