1structure arm_stepLib :> arm_stepLib = 2struct 3 4(* interactive use: 5 app load ["arm_stepTheory", "armSyntax", "intLib", "wordsLib", 6 "SatisfySimps"]; 7*) 8 9open HolKernel boolLib bossLib; 10open wordsTheory combinTheory updateLib; 11open arm_coretypesTheory arm_seq_monadTheory arm_opsemTheory armTheory; 12open arm_stepTheory; 13 14structure Parse = struct 15 open Parse 16 val (Type,Term) = parse_from_grammars arm_stepTheory.arm_step_grammars 17end 18 19open Parse 20 21(* ------------------------------------------------------------------------- *) 22 23val _ = numLib.prefer_num(); 24val _ = wordsLib.prefer_word(); 25 26infix \\ 27 28val op \\ = op Tactical.THEN; 29 30val ERR = Feedback.mk_HOL_ERR "arm_stepLib"; 31 32val arm_step_trace = ref 0; 33val arm_step_check = ref false; 34 35val _ = Feedback.register_trace ("arm step", arm_step_trace, 3); 36val _ = Feedback.register_btrace ("arm step check", arm_step_check); 37 38(* ------------------------------------------------------------------------- *) 39(* Facilitate evaluation *) 40(* ------------------------------------------------------------------------- *) 41 42val mk_constants = 43 List.concat o List.map (fn (thy, l) => 44 List.map (fn name => Term.prim_mk_const {Thy = thy, Name = name}) l); 45 46(* Things to avoid evaluating *) 47 48val restr_terms = mk_constants 49 [("words", ["word_div", "word_quot", "add_with_carry", 50 "bit_field_insert", "word_sign_extend"]), 51 ("integer_word", ["w2i", "i2w"]), 52 ("arm_coretypes", ["signed_sat_q", "unsigned_sat_q", 53 "signed_sat", "unsigned_sat", 54 "encode_psr", "decode_psr", "count_leading_zeroes"])]; 55 56val _ = computeLib.del_consts (mk_constants 57 [("arm_opsem", 58 ["branch_write_pc", "bx_write_pc", "load_write_pc", "alu_write_pc", 59 "branch_target_instr", 60 "branch_exchange_instr", 61 "branch_link_exchange_imm_instr", 62 "branch_link_exchange_reg_instr", 63 "null_check_if_thumbEE", 64 "compare_branch_instr", 65 "table_branch_byte_instr", 66 "check_array_instr", 67 "handler_branch_link_instr", 68 "handler_branch_link_parameter_instr", 69 "handler_branch_parameter_instr", 70 "add_sub_instr", 71 "data_processing_instr", 72 "load_instr", 73 "load_multiple_instr", 74 "return_from_exception_instr", 75 "saturating_add_subtract_instr", 76 "signed_16_multiply_32_accumulate_instr", 77 "signed_16x32_multiply_32_accumulate_instr", 78 "signed_multiply_dual_instr", 79 "saturate_instr", "saturate_16_instr", 80 "branch_instruction", "data_processing_instruction", 81 "load_store_instruction", 82 "arm_instr"]), 83 ("arm", ["arm_next"])]); 84 85val _ = computeLib.add_funs 86 (List.map (REWRITE_RULE [condT_set_q]) 87 [saturating_add_subtract_instr, signed_16_multiply_32_accumulate_instr, 88 signed_16x32_multiply_32_accumulate_instr, signed_multiply_dual_instr, 89 saturate_instr, saturate_16_instr] @ 90 [branch_write_pc, bx_write_pc, load_write_pc_def, alu_write_pc_def, 91 null_check_if_thumbEE_def, branch_target_instr, branch_exchange_instr, 92 branch_link_exchange_imm_instr, branch_link_exchange_reg_instr, 93 arm_stepTheory.compare_branch_instr, table_branch_byte_instr, 94 check_array_instr, handler_branch_link_instr, 95 handler_branch_link_parameter_instr, handler_branch_parameter_instr, 96 add_sub_instr, data_processing_instr, load_instr, load_multiple_instr, 97 return_from_exception_instr, branch_instruction_def, 98 data_processing_instruction_def, load_store_instruction_def, arm_instr_def, 99 armTheory.arm_next_def]); 100 101val WORD_EQ_ADD_LCANCEL_0 = 102 simpLib.SIMP_PROVE (srw_ss()++wordsLib.WORD_ARITH_EQ_ss) [] 103 ``(v = v + w) <=> (w = 0w:'a word)``; 104 105val word_add_sub2 = wordsLib.WORD_DECIDE ``(a + b) + -a = b : 'a word`` 106val word_add_sub3 = wordsLib.WORD_DECIDE ``a + b + -b = a : 'a word`` 107val word_add_sub4 = wordsLib.WORD_DECIDE ``a + -b + b = a : 'a word`` 108val word_add_sub5 = wordsLib.WORD_DECIDE ``a + -(a + -b) = b : 'a word`` 109 110local 111 val rule = GSYM o ONCE_REWRITE_RULE [aligned_def] 112in 113 val aligned_con_thms2 = rule aligned_con_thms 114 val aligned_con_plus4_thm2 = rule aligned_con_plus4_thm 115 val aligned_con_shift_thms2 = rule aligned_con_shift_thms 116 val aligned_con_rrx_thms2 = rule aligned_con_rrx_thms 117 val aligned_and_aligned_bx_thms2 = rule aligned_and_aligned_bx_thms 118 val aligned_and_aligned_bx_thms2 = rule aligned_and_aligned_bx_thms 119 val aligned_and_aligned_bx_rrx2 = rule aligned_and_aligned_bx_rrx 120 val aligned_rm_thms2 = rule aligned_rm_thms 121 val aligned_shift_rm_thms2 = rule aligned_shift_rm_thms 122 val aligned_rrx_rm_thms2 = rule aligned_rrx_rm_thms 123 val aligned_aligned2 = aligned_aligned 124 |> CONJUNCTS 125 |> Lib.C (curry List.take) 2 126 |> LIST_CONJ 127 |> rule 128end; 129 130val inst_type2 = Thm.INST_TYPE [Type.alpha |-> ``:2``]; 131val inst_type32 = Thm.INST_TYPE [Type.alpha |-> ``:32``]; 132 133fun bitwise_clauses f thm = 134 List.drop (thm |> f |> Drule.SPEC_ALL |> Drule.CONJUNCTS,2) 135 |> Drule.LIST_CONJ; 136 137val _ = computeLib.add_funs 138 [align_1, align_2_align_4, align_bits, (* align_neq, *) align_aligned, 139 aligned_align_thms, aligned_align_thms2, align2_add_times2, 140 aligned_rm_thms, aligned_rm_thms2, aligned_align_rm_thms, 141 aligned_shift_rm_thms, aligned_shift_rm_thms2, aligned_align_shift_rm_thms, 142 aligned_rrx_rm_thms, aligned_rrx_rm_thms2, aligned_align_rrx_rm_thms, 143 aligned_align, aligned_sum, align_bits_sum, aligned_0_thms, 144 aligned_pair_thms, aligned_shift_pair_thms, aligned_rrx_pair_thms, 145 aligned_aligned, aligned_aligned2, 146 aligned_over_bitwise, aligned_aligned_add_with_carry, 147 aligned_pc_pc, aligned_aligned_rsb, add_with_carry, add_with_carry0, 148 aligned_aligned_shift_thms, aligned_aligned_shift_pc_thms, 149 aligned_aligned_rrx, aligned_aligned_rrx_pc, 150 aligned_con_thms, aligned_con_thms2, 151 aligned_con_plus4_thm, aligned_con_plus4_thm2, 152 aligned_con_shift_thms, aligned_con_shift_thms2, 153 aligned_con_rrx_thms, aligned_con_rrx_thms2, 154 align_bx_bit, aligned_bx_branch, align_ldr_lsl, 155 aligned_bx_1comp, aligned_bx_2comp, 156 aligned_bx_and, aligned_bx_eor, aligned_bx_orr, 157 aligned_bx_add_with_carry, aligned_bx_add_sub, 158 aligned_bx_add_with_carry_pair, aligned_bx_add_pair, 159 aligned_bx_pair_shift_thms, 160 aligned_bx_1comp_pc, aligned_bx_and_pc, aligned_bx_eor_pc, 161 aligned_bx_orr_pc, aligned_bx_bic_pc, aligned_bx_add_with_carry_pc, 162 aligned_bx_add_with_carry_pair_pc, aligned_bx_add_sub_pc, 163 aligned_bx_add_with_carry_literal_pc, 164 aligned_bx_rrx_pair, aligned_bx_add_with_carry_rrx_pair, 165 aligned_bx_add_sub_rrx_pc, aligned_and_aligned_bx_rrx, 166 aligned_and_aligned_bx_rrx2, aligned_bx_and_aligned_add_with_carry_rrx, 167 aligned_bx_and_aligned_rrx, aligned_and_aligned_bx_rrx, 168 aligned_bx_and_pc |> CONJUNCT2 |> ONCE_REWRITE_RULE [WORD_AND_COMM], 169 aligned_bx_eor_pc |> CONJUNCT2 |> ONCE_REWRITE_RULE [WORD_XOR_COMM], 170 aligned_bx_orr_pc |> CONJUNCT2 |> ONCE_REWRITE_RULE [WORD_OR_COMM], 171 aligned_and_aligned_bx_thms, aligned_and_aligned_bx_thms2, 172 aligned_bx_and_aligned_thms, IT_concat, good_mode, good_it, divisor_neq_zero, 173 neq_pc_plus4, neq_pc_plus4_t2, neq_pc_plus4_plus, aligned_over_memread, 174 aligned_bx_aligned_bx, aligned_concat, aligned_bx_concat, 175 it_mode_concat, it_con_thm, 176 word_add_sub2, word_add_sub3, word_add_sub4, word_add_sub5, 177 WORD_ADD_RINV, WORD_NEG_NEG, WORD_ADD_0, UPDATE_ID_o, 178 wordsLib.WORD_ARITH_CONV ``~(n2w n + -a) : word32``, 179 wordsLib.WORD_ARITH_CONV ``~-a : word32``, 180 wordsLib.WORD_ARITH_CONV ``a + ~a + 1w : word32``, 181 extract_of_double_word, encode_psr_bit, encode_psr_bits, 182 Q.ISPEC `IS_SOME:'a option -> bool` COND_RAND, 183 Q.ISPEC `FST:'a # 'b -> 'a` COND_RAND, 184 Q.ISPEC `SND:'a # 'b -> 'b` COND_RAND, 185 Q.ISPEC `ARMpsr_N` COND_RAND, 186 Q.ISPEC `ARMpsr_Z` COND_RAND, 187 Q.ISPEC `ARMpsr_C` COND_RAND, 188 Q.ISPEC `ARMpsr_V` COND_RAND, 189 Q.ISPEC `ARMpsr_Q` COND_RAND, 190 Q.ISPEC `ARMpsr_IT` COND_RAND, 191 Q.ISPEC `ARMpsr_J` COND_RAND, 192 Q.ISPEC `ARMpsr_GE` COND_RAND, 193 Q.ISPEC `ARMpsr_E` COND_RAND, 194 Q.ISPEC `ARMpsr_A` COND_RAND, 195 Q.ISPEC `ARMpsr_I` COND_RAND, 196 Q.ISPEC `ARMpsr_F` COND_RAND, 197 Q.ISPEC `ARMpsr_T` COND_RAND, 198 Q.ISPEC `ARMpsr_IT_fupd f` COND_RAND, 199 error_option_case_COND_RAND, COND_RATOR, 200 FST_ADD_WITH_CARRY, 201 DECIDE ``if b then b else T``, 202 DECIDE ``~((n <=> if z then v else ~n) /\ ~z)``, 203 DECIDE ``n <=/=> ~n``, 204 DECIDE ``~((z /\ c) /\ ~z)``, 205 WORD_ADD_ASSOC |> Q.SPECL [`v`,`n2w n`,`n2w m`] |> GSYM |> inst_type32, 206 pairTheory.FST_PAIR_MAP, pairTheory.SND_PAIR_MAP, 207 bitwise_clauses inst_type32 WORD_AND_CLAUSES, 208 bitwise_clauses inst_type32 WORD_XOR_CLAUSES, 209 bitwise_clauses inst_type32 WORD_OR_CLAUSES, 210 inst_type32 WORD_AND_COMP, 211 inst_type32 WORD_EQ_ADD_LCANCEL, 212 inst_type32 WORD_EQ_ADD_RCANCEL, 213 inst_type32 WORD_EQ_ADD_LCANCEL_0, 214 inst_type32 WORD_ADD_INV_0_EQ, 215 inst_type32 WORD_ADD_LINV]; 216 217(* ------------------------------------------------------------------------- *) 218 219val lowercase = String.map Char.toLower 220val rhsc = boolSyntax.rhs o Thm.concl; 221val eval = rhsc o bossLib.EVAL; 222fun apply_conv conv = rhsc o (Conv.QCONV conv); 223val restr_eval = apply_conv (computeLib.RESTR_EVAL_CONV restr_terms); 224val dest_strip = armSyntax.dest_strip; 225 226fun dest_arm_state_updates tm = 227 (case dest_strip tm 228 of (s, [a,b]) => (s, a) :: dest_arm_state_updates b 229 | _ => []) handle HOL_ERR _ => []; 230 231fun mk_test (c,l,v) = boolSyntax.mk_eq (Term.list_mk_comb (c,l),v) 232fun mk_arm_const s = Term.prim_mk_const {Name = s, Thy = "arm_step"} 233 234local 235 val I_flags_fupd = Term.inst [Type.alpha |-> ``:ARMpsr``] combinSyntax.I_tm 236 val read_status_tm = mk_arm_const "ARM_READ_STATUS" 237 fun mk_read_status (t,s) = 238 Term.list_mk_comb (read_status_tm,[t,s]) 239 handle HOL_ERR _ => raise ERR "mk_read_status" "" 240in 241 fun set_flags state cond pass = 242 let fun test_flag t = mk_read_status (t,state) 243 val flag_n = test_flag ``arm_step$psrN`` 244 val flag_z = test_flag ``arm_step$psrZ`` 245 val flag_c = test_flag ``arm_step$psrC`` 246 val flag_v = test_flag ``arm_step$psrV`` 247 val not_flag_n = mk_neg flag_n 248 val not_flag_z = mk_neg flag_z 249 val not_flag_c = mk_neg flag_c 250 val not_flag_v = mk_neg flag_v 251 in 252 case (Arbnum.toInt (wordsLib.dest_word_literal cond),pass) 253 of (0,true) => (``arm_coretypes$ARMpsr_Z_fupd (K T)``,flag_z) 254 | (0,false) => (``arm_coretypes$ARMpsr_Z_fupd (K F)``,not_flag_z) 255 | (1,true) => (``arm_coretypes$ARMpsr_Z_fupd (K F)``,not_flag_z) 256 | (1,false) => (``arm_coretypes$ARMpsr_Z_fupd (K T)``,flag_z) 257 | (2,true) => (``arm_coretypes$ARMpsr_C_fupd (K T)``,flag_c) 258 | (2,false) => (``arm_coretypes$ARMpsr_C_fupd (K F)``,not_flag_c) 259 | (3,true) => (``arm_coretypes$ARMpsr_C_fupd (K F)``,not_flag_c) 260 | (3,false) => (``arm_coretypes$ARMpsr_C_fupd (K T)``,flag_c) 261 | (4,true) => (``arm_coretypes$ARMpsr_N_fupd (K T)``,flag_n) 262 | (4,false) => (``arm_coretypes$ARMpsr_N_fupd (K F)``,not_flag_n) 263 | (5,true) => (``arm_coretypes$ARMpsr_N_fupd (K F)``,not_flag_n) 264 | (5,false) => (``arm_coretypes$ARMpsr_N_fupd (K T)``,flag_n) 265 | (6,true) => (``arm_coretypes$ARMpsr_V_fupd (K T)``,flag_v) 266 | (6,false) => (``arm_coretypes$ARMpsr_V_fupd (K F)``,not_flag_v) 267 | (7,true) => (``arm_coretypes$ARMpsr_V_fupd (K F)``,not_flag_v) 268 | (7,false) => (``arm_coretypes$ARMpsr_V_fupd (K T)``,flag_v) 269 | (8,true) => (``arm_coretypes$ARMpsr_C_fupd (K T) o 270 arm_coretypes$ARMpsr_Z_fupd (K F)``, 271 mk_conj (flag_c,not_flag_z)) 272 | (8,false) => (``arm_coretypes$ARMpsr_C_fupd (K(^flag_z /\ ^flag_c))``, 273 mk_neg (mk_conj (flag_c,not_flag_z))) 274 | (9,true) => (``arm_coretypes$ARMpsr_C_fupd (K(^flag_z /\ ^flag_c))``, 275 mk_neg (mk_conj (flag_c,not_flag_z))) 276 | (9,false) => (``arm_coretypes$ARMpsr_C_fupd (K T) o 277 arm_coretypes$ARMpsr_Z_fupd (K F)``, 278 mk_conj (flag_c,not_flag_z)) 279 | (10,true) => (``arm_coretypes$ARMpsr_V_fupd (K ^flag_n)``, 280 mk_eq (flag_n,flag_v)) 281 | (10,false) => (``arm_coretypes$ARMpsr_V_fupd (K (~^flag_n))``, 282 mk_neg (mk_eq (flag_n,flag_v))) 283 | (11,true) => (``arm_coretypes$ARMpsr_V_fupd (K (~^flag_n))``, 284 mk_neg (mk_eq (flag_n,flag_v))) 285 | (11,false) => (``arm_coretypes$ARMpsr_V_fupd (K ^flag_n)``, 286 mk_eq (flag_n,flag_v)) 287 | (12,true) => (``arm_coretypes$ARMpsr_V_fupd (K ^flag_n) o 288 arm_coretypes$ARMpsr_Z_fupd (K F)``, 289 mk_conj (mk_eq (flag_n,flag_v),not_flag_z)) 290 | (12,false) => (``arm_coretypes$ARMpsr_V_fupd 291 (K (if ^flag_z then ^flag_v else ~^flag_n))``, 292 mk_neg (mk_conj (mk_eq (flag_n,flag_v),not_flag_z))) 293 | (13,true) => (``arm_coretypes$ARMpsr_V_fupd 294 (K (if ^flag_z then ^flag_v else ~^flag_n))``, 295 mk_neg (mk_conj (mk_eq (flag_n,flag_v),not_flag_z))) 296 | (13,false) => (``arm_coretypes$ARMpsr_V_fupd (K ^flag_n) o 297 arm_coretypes$ARMpsr_Z_fupd (K F)``, 298 mk_conj (mk_eq (flag_n,flag_v),not_flag_z)) 299 | (14,true) => (I_flags_fupd,T) 300 | (15,true) => (I_flags_fupd,T) 301 | _ => raise ERR "set_flags" "Invalid pass status." 302 end 303end; 304 305datatype endian = BigEndian | LittleEndian; 306 307datatype mode = Usr | Fiq | Irq | Svc | Mon | Abt | Und | Sys; 308 309datatype arch = ARMv4 | ARMv4T 310 | ARMv5T | ARMv5TE 311 | ARMv6 | ARMv6K | ARMv6T2 312 | ARMv7_A | ARMv7_R; 313 314type options = 315 { arch : arch, mode : mode, endian : endian, 316 pass : bool, thumb : bool, thumbee : bool, itblock : int }; 317 318fun endian_to_term BigEndian = boolSyntax.T 319 | endian_to_term LittleEndian = boolSyntax.F; 320 321fun mode_to_term m = Parse.Term 322 (case m 323 of Usr => `0b10000w:word5` 324 | Fiq => `0b10001w:word5` 325 | Irq => `0b10010w:word5` 326 | Svc => `0b10011w:word5` 327 | Mon => `0b10110w:word5` 328 | Abt => `0b10111w:word5` 329 | Und => `0b10111w:word5` 330 | Sys => `0b11111w:word5`); 331 332fun arch_to_term s = Parse.Term 333 (case s 334 of ARMv4 => `ARMv4` 335 | ARMv4T => `ARMv4T` 336 | ARMv5T => `ARMv5T` 337 | ARMv5TE => `ARMv5TE` 338 | ARMv6 => `ARMv6` 339 | ARMv6K => `ARMv6K` 340 | ARMv6T2 => `ARMv6T2` 341 | ARMv7_A => `ARMv7_A` 342 | ARMv7_R => `ARMv7_R`); 343 344fun arch_version s = 345 case s 346 of ARMv4 => 4 347 | ARMv4T => 4 348 | ARMv5T => 5 349 | ARMv5TE => 5 350 | ARMv6 => 6 351 | ARMv6K => 6 352 | ARMv6T2 => 6 353 | ARMv7_A => 7 354 | ARMv7_R => 7; 355 356fun thumb2_support a = Lib.mem a [ARMv6T2, ARMv7_A, ARMv7_R] 357 358local 359 val arch_tm = mk_arm_const "ARM_ARCH" 360 val extensions_tm = mk_arm_const "ARM_EXTENSIONS" 361 val unaligned_support_tm = mk_arm_const "ARM_UNALIGNED_SUPPORT" 362 val read_event_register_tm = mk_arm_const "ARM_READ_EVENT_REGISTER" 363 val read_interrupt_wait_tm = mk_arm_const "ARM_READ_INTERRUPT_WAIT" 364 val read_sctlr_tm = mk_arm_const "ARM_READ_SCTLR" 365 val read_status_tm = mk_arm_const "ARM_READ_STATUS" 366 val read_it_tm = mk_arm_const "ARM_READ_IT" 367 val ALIGN_CONV = SIMP_CONV (srw_ss()) [aligned_n2w, align_n2w] 368 val ALIGN_ss = simpLib.std_conv_ss 369 {conv = ALIGN_CONV, name = "ALIGN_CONV", 370 pats = [``arm_coretypes$aligned (n2w a:'a word,n)``]} 371 fun cond_mk_test c f l = 372 [case c 373 of SOME b => mk_test (f,l,b) 374 | NONE => boolSyntax.T] 375in 376 fun mk_precondition 377 the_state arch itstate ext thumbee thumb endian flags regs memory = 378 apply_conv 379 (SIMP_CONV (pure_ss++ALIGN_ss++boolSimps.CONJ_ss) 380 [GSYM CONJ_ASSOC, aligned_thm, 381 NOT_CLAUSES, AND_CLAUSES, REFL_CLAUSE, COND_CLAUSES, 382 ARM_READ_CPSR_def, ARM_MODE_def, ARM_READ_STATUS_def, 383 ARM_READ_IT_def]) 384 (list_mk_conj 385 ([mk_test (arch_tm,[the_state],arch), 386 mk_test (extensions_tm,[the_state], ext), 387 mk_test (unaligned_support_tm,[the_state],T), 388 mk_test (read_event_register_tm,[the_state],T), 389 mk_test (read_interrupt_wait_tm,[the_state],F), 390 mk_test (read_sctlr_tm,[``arm_step$sctlrV``,the_state],F), 391 mk_test (read_sctlr_tm,[``arm_step$sctlrA``,the_state],T), 392 mk_test (read_sctlr_tm,[``arm_step$sctlrU``,the_state],F)] @ 393 cond_mk_test itstate read_it_tm [the_state] @ 394 cond_mk_test endian read_status_tm [``arm_step$psrE``,the_state] @ 395 [mk_test (read_status_tm,[``arm_step$psrJ``,the_state],thumbee), 396 mk_test (read_status_tm,[``arm_step$psrT``,the_state],thumb), 397 flags, regs, memory])) 398end; 399 400fun list_dest_o t = 401let 402 fun F t a = let val (f,g) = combinSyntax.dest_o t in 403 F g (f :: a) 404 end handle HOL_ERR _ => (t :: a) 405in 406 List.rev (F t []) 407end; 408 409fun butlastn (l,n) = List.take (l, List.length l - n); 410 411fun list_mk_o l = List.foldr combinSyntax.mk_o (List.last l) (butlastn (l,1)); 412 413val dropn_o = total (fn (t,n) => list_mk_o (butlastn (list_dest_o t, n))); 414 415fun find_arm_state_updates upd tm = 416 case List.find (fn (s,_) => s = upd) (dest_arm_state_updates tm) 417 of SOME (_,t) => t 418 | _ => raise ERR "pick_arm_state_updates" "no matching updates"; 419 420fun arm_state_standard_updates tm = 421let 422 val upd = dest_arm_state_updates tm 423 val (reg,upd) = Lib.pluck (fn (s,_) => s = "arm_state_registers_fupd") upd 424 val (psr,upd) = Lib.pluck (fn (s,_) => s = "arm_state_psrs_fupd") upd 425 val (mem,upd) = Lib.trypluck' (fn (s,u) => 426 if s = "arm_state_memory_fupd" then SOME u else NONE) upd 427 val (evt,upd) = Lib.pluck 428 (fn (s,_) => s = "arm_state_event_register_fupd") upd 429 val (wfi,upd) = Lib.pluck 430 (fn (s,_) => s = "arm_state_interrupt_wait_fupd") upd 431 val (acc,upd) = Lib.trypluck' (fn (s,u) => 432 if s = "arm_state_accesses_fupd" then SOME u else NONE) upd 433 val (mon,upd) = Lib.trypluck' (fn (s,u) => 434 if s = "arm_state_monitors_fupd" then 435 SOME u 436 else 437 NONE) upd 438in 439 (snd reg, snd psr, mem, snd evt, snd wfi, acc, mon, upd) 440end; 441 442local 443 val mode_tm = mk_arm_const "ARM_MODE" 444 val registers_tm = 445 Term.prim_mk_const {Name = "arm_state_registers", Thy = "arm_seq_monad"} 446 447 val ALIGN_EQ_ss = simpLib.merge_ss 448 [simpLib.rewrites [WORD_NEG_NEG, align_relative_thm, 449 GSYM aligned_def, GSYM aligned_248], 450 simpLib.std_conv_ss 451 {conv = Conv.CHANGED_CONV wordsLib.WORD_EVAL_CONV, 452 name = "WORD_EVAL_CONV", pats = [``a = b : word32``]}] 453 454 val arm_reg_updates = 455 List.map combinSyntax.dest_update o list_dest_o o 456 find_arm_state_updates "arm_state_registers_fupd" 457 458 fun mk_reg_mode_updates (the_state,state') = 459 let val updates = arm_reg_updates state' handle HOL_ERR _ => [] 460 fun mk_reg_test (r,v) = 461 let val c = total (find_term is_cond) v 462 val t = mk_test (registers_tm, [the_state,r], v) 463 in 464 case c 465 of SOME tm => 466 let val (b,_,_) = dest_cond tm 467 val c2 = total (find_term is_cond) b 468 in 469 case c2 470 of SOME tm2 => 471 let val (b2,_,_) = dest_cond tm2 in 472 list_mk_conj [b2,b,t] 473 end 474 | NONE => mk_conj (b,t) 475 end 476 | NONE => t 477 end 478 val tms = List.map mk_reg_test updates 479 in 480 List.map (apply_conv 481 (SIMP_CONV (std_ss++boolSimps.CONJ_ss++ALIGN_EQ_ss) [])) tms 482 end 483 484 val arm_psrs_updates = 485 List.map combinSyntax.dest_update o list_dest_o o 486 find_arm_state_updates "arm_state_psrs_fupd" 487 488 fun mk_psrs_updates (the_state,state') = 489 let val updates = arm_psrs_updates state' in 490 case List.find 491 (fn tm => not (term_eq ``(0n,arm_coretypes$CPSR)`` (fst tm))) 492 updates 493 of SOME (t,v) => 494 (case total (find_term is_cond) v 495 of SOME tm => let val (b,_,_) = dest_cond tm in [b] end 496 | NONE => []) 497 | NONE => [] 498 end 499in 500 fun mk_reg_pre (the_state,M,state') = 501 let val tmode = mk_test (mode_tm, [the_state], M) 502 val regs = mk_reg_mode_updates (the_state,state') 503 val psrs = mk_psrs_updates (the_state,state') 504 val mregs = list_mk_conj (tmode :: regs @ psrs) 505 in 506 (List.length regs, apply_conv (SIMP_CONV (std_ss++boolSimps.CONJ_ss) 507 [GSYM word_sub_def]) mregs) 508 end 509end; 510 511val aligned_bx_tm = Term.prim_mk_const {Name = "aligned_bx", Thy = "arm_step"} 512 513fun mk_aligned_bx (w,n:term) = 514 Term.mk_comb 515 (Term.inst [Type.alpha |-> wordsSyntax.dest_word_type (Term.type_of w)] 516 aligned_bx_tm, w) 517 handle HOL_ERR _ => raise ERR "mk_aligned_bx" ""; 518 519fun concat_bytes l = 520let val _ = List.length l = 4 orelse raise ERR "concat_bytes" "" in 521 List.foldl wordsSyntax.mk_word_concat (hd l) (tl l) 522end; 523 524fun bits32 (n,h,l) = 525 let val s = StringCvt.padLeft #"0" 32 (Arbnum.toBinString n) 526 val ss = Substring.slice (Substring.full s, 31 - h, SOME (h + 1 - l)) 527 in 528 Arbnum.fromBinString (Substring.string ss) 529 end; 530 531local 532 val read_mem_tm = ``arm_seq_monad$arm_state_memory`` 533 val read_reg_tm = ``arm_seq_monad$arm_state_registers`` 534 val pc_tm = ``(0n,arm_coretypes$RName_PC)`` 535 fun mk_word32 x = wordsSyntax.mk_wordii (x,32) 536 537 fun make_bytes t = 538 if optionSyntax.is_some t then 539 let val a = optionSyntax.dest_some t in 540 List.tabulate (4, fn x => wordsSyntax.mk_word_add (a,mk_word32 x)) 541 end 542 else if optionSyntax.is_none t then 543 [] 544 else raise ERR "make_bytes" "" 545 546 val I_mem = ``I : (FullAddress -> word8) -> (FullAddress -> word8)`` 547 548 (* a =+ if f d then d else 0w *) 549 fun mk_conform_mem (f,a,d) = 550 combinSyntax.mk_update (a, mk_cond (f d, d, ``0w:word8``)) 551 552 (* a =+ if GOOD_MODE ((4 >< 0) d) then d else d || 31w *) 553 fun mk_good_mode_mem (a,d) = 554 let val good = ``GOOD_MODE ((4 >< 0) ^d)`` in 555 combinSyntax.mk_update 556 (a, mk_cond (good, d, 557 wordsSyntax.mk_word_or (d,``31w:word8``))) 558 end 559 560 fun mk_aligned_the_mem (f:term -> term,s,l) = 561 let val bytes = List.map (fn a => restr_eval 562 (list_mk_comb (read_mem_tm, [s,a]))) l 563 val aliged_word = concat_bytes bytes 564 in 565 (1, mk_conform_mem (f,hd l,hd bytes), f aliged_word) 566 end 567 568 fun mk_good_it_mode_the_mem (s,l) = 569 let val bytes = List.map (fn a => restr_eval 570 (list_mk_comb (read_mem_tm, [s,a]))) l 571 val aliged_word = concat_bytes bytes 572 in 573 (3, list_mk_o 574 [mk_good_mode_mem (hd l,hd bytes), 575 mk_conform_mem 576 (fn d => ``(7 >< 2) ^d = 0w:word6``, 577 List.nth(l,1), List.nth(bytes,1)), 578 mk_conform_mem 579 (fn d => ``(2 >< 1) ^d = 0w:word2``, 580 List.nth(l,3), List.nth(bytes,3))], 581 ``GOOD_MODE ((4 >< 0) ^aliged_word) /\ 582 ((((15 >< 10) ^aliged_word):word6) @@ 583 (((26 >< 25) ^aliged_word):word2) = 0w:word8)``) 584 end 585 586 fun fold_mem f init l = 587 List.foldl (fn (a,(n,tm1,tm2)) => 588 let val (u,t) = f a in 589 if n = 0 then 590 (1,u,t) 591 else 592 (n + 1, combinSyntax.mk_o (u,tm1), mk_conj (t,tm2)) 593 end) init l 594 595 fun mk_memory_good (endian,arch,bx,s,aligns) = 596 if optionSyntax.is_none bx then 597 (0,I_mem,T) 598 else 599 let val bytes = make_bytes aligns 600 val bytes = if endian = BigEndian then rev bytes else bytes 601 val align_fn = if arch_version arch >= 5 then 602 Lib.C (Lib.curry mk_aligned_bx) ``4n`` 603 else 604 Lib.C (Lib.curry armSyntax.mk_aligned) ``4n`` 605 in 606 if term_eq (optionSyntax.dest_some bx) T then 607 mk_aligned_the_mem (align_fn,s,bytes) 608 else 609 mk_good_it_mode_the_mem (s,bytes) 610 end 611 612 fun mk_memory_opc data_mem (s,endian,enc,opc) = 613 let open wordsSyntax 614 val (n,bytes) = 615 case fst (Term.dest_const enc) 616 of "Encoding_Thumb" => 617 let val l = eval (armSyntax.mk_bytes (opc,``2n``)) 618 val bytes = fst (listSyntax.dest_list l) 619 in 620 (1,if endian = BigEndian then rev bytes else bytes) 621 end 622 | "Encoding_Thumb2" => 623 let val l = eval (armSyntax.mk_bytes (opc,``4n``)) in 624 (3,case fst (listSyntax.dest_list l) 625 of [a,b,c,d] => if endian = BigEndian then 626 [d,c,b,a] 627 else 628 [c,d,a,b] 629 | _ => raise ERR "mk_memory_opc" "") 630 end 631 | "Encoding_ARM" => 632 let val l = eval (armSyntax.mk_bytes (opc,``4n``)) 633 val bytes = fst (listSyntax.dest_list l) 634 in 635 (3,if endian = BigEndian then rev bytes else bytes) 636 end 637 | s => 638 if s = "Encoding_Thumb" orelse 639 s = "Encoding_ThumbEE" 640 then 641 let val l = eval (armSyntax.mk_bytes (opc,``2n``)) 642 val bytes = fst (listSyntax.dest_list l) 643 in 644 (1,if endian = BigEndian then rev bytes else bytes) 645 end 646 else 647 raise ERR "mk_memory_opc" "Invalid encoding." 648 val registers = mk_comb (read_reg_tm,s) 649 val pc = restr_eval (mk_comb (registers,pc_tm)) 650 val addrs = pc :: List.tabulate (n, 651 fn x => mk_word_add (pc,mk_word32 (x+1))) 652 in 653 fold_mem (fn (a,b) => 654 (restr_eval (combinSyntax.mk_update (a,b)), 655 restr_eval (mk_test (read_mem_tm, [s,a], b)))) 656 data_mem (Lib.zip addrs bytes) 657 end 658in 659 fun mk_arm_memory state' endian arch enc opc bx aligns = 660 let val data_mem = mk_memory_good (endian,arch,bx,state',aligns) 661 val (nmem,tm1,tm2) = mk_memory_opc data_mem (state',endian,enc,opc) 662 in 663 (nmem, tm1, 664 apply_conv 665 (SIMP_CONV (std_ss++boolSimps.CONJ_ss) 666 [GSYM word_sub_def, WORD_ADD_0]) tm2) 667 end 668end; 669 670fun get_valuestate s tm = 671 armSyntax.dest_valuestate tm handle HOL_ERR _ => 672 (let val e = armSyntax.dest_error tm handle HOL_ERR _ => 673 (if (!arm_step_trace div 2) mod 2 = 1 then Parse.print_term tm else (); 674 raise ERR "eval_inst" ("Failed to fully evaluate " ^ s)) 675 in 676 raise ERR "eval_inst" ("Error: " ^ stringSyntax.fromHOLstring e) 677 end); 678 679fun mk_inp instr = 680 case lowercase instr 681 of "rst" => armSyntax.HW_Reset_tm 682 | "reset" => armSyntax.HW_Reset_tm 683 | "fiq" => armSyntax.HW_Fiq_tm 684 | "fast" => armSyntax.HW_Fiq_tm 685 | "irq" => armSyntax.HW_Irq_tm 686 | "interrupt" => armSyntax.HW_Irq_tm 687 | _ => armSyntax.NoInterrupt_tm 688 689local 690 val read_status_tm = mk_arm_const "ARM_READ_STATUS" 691 692 fun init s cpsr arch thumbee = let 693 val ext = if thumbee then 694 ``{Extension_ThumbEE}`` 695 else 696 ``{}:ARMextensions set`` 697 in 698 (ext, 699 ``^s with 700 <| psrs updated_by ((0,CPSR) =+ ^cpsr); 701 event_register updated_by (0 =+ T); 702 interrupt_wait updated_by (0 =+ F); 703 information := 704 <| arch := ^arch; unaligned_support := T; extensions := ^ext |>; 705 coprocessors updated_by 706 (Coprocessors_state_fupd (cp15_fupd (CP15reg_SCTLR_fupd 707 (\sctlr. sctlr with <| V := F; A := T; U := F |>)))) |>``) 708 end 709 710 fun mk_bool b = if b then T else F 711 712 fun mk_cpsr the_state flags_fupd itstate T ThumbEE E M = let 713 val cpsr = case itstate 714 of SOME IT => 715 ``^the_state.psrs (0,CPSR) with 716 <| IT := ^IT; J := ^ThumbEE; T := ^T; E := ^E; M := ^M |>`` 717 | _ => ``^the_state.psrs (0,CPSR) with 718 <| J := F; T := ^T; E := ^E; M := ^M |>`` 719 in 720 eval (mk_comb (flags_fupd, cpsr)) 721 end 722 723 fun mk_irpt_cpsr the_state T ThumbEE M = 724 ``^the_state.psrs (0,CPSR) with <| J := ^ThumbEE; T := ^T; M := ^M |>`` 725 726 fun decode_opcode IT arch thumb thumbee opc = 727 if thumb then 728 let val n = wordsSyntax.mk_wordi (bits32 (opc,15,0),16) 729 in 730 if bits32 (opc,31,29) = Arbnum.fromBinString "111" andalso 731 bits32 (opc,28,27) <> Arbnum.zero 732 then 733 (armSyntax.Encoding_Thumb2_tm, 734 eval (armSyntax.mk_thumb2_decode (arch_to_term arch,IT, 735 wordsSyntax.mk_wordi (bits32 (opc,31,16),16),n))) 736 else if bits32 (opc,31,16) = Arbnum.zero then 737 if thumbee then 738 pairSyntax.dest_pair (eval 739 (armSyntax.mk_thumbee_decode (arch_to_term arch,IT,n))) 740 else 741 (armSyntax.Encoding_Thumb_tm, 742 eval (armSyntax.mk_thumb_decode (arch_to_term arch,IT,n))) 743 else 744 raise ERR "decode_opcode" "not a valid thumb op-code" 745 end 746 else 747 let val n = wordsSyntax.mk_wordi (opc,32) 748 val v4 = arch = ARMv4 orelse arch = ARMv4T 749 in 750 (armSyntax.Encoding_ARM_tm, 751 eval (armSyntax.mk_arm_decode (mk_bool v4,n))) 752 end 753 754 val remove_white_space = 755 String.translate 756 (fn c => if Char.isSpace c then "" else Char.toString c) 757in 758 fun make_arm_state_and_pre the_state (opt:options) instr = 759 let 760 val arch = #arch opt 761 val thumb = #thumb opt 762 val thumbee = #thumbee opt 763 val endian = #endian opt 764 val _ = not (arch = ARMv4 andalso thumb) orelse 765 raise ERR "make_arm_state_and_pre" "ARMv4 does not support Thumb." 766 val Thumb = mk_bool thumb 767 val ThumbEE = if thumbee then 768 if arch = ARMv7_A orelse arch = ARMv7_R then 769 boolSyntax.T 770 else 771 raise ERR "make_arm_state_and_pre" 772 "ThumbEE not supported by architecture." 773 else 774 boolSyntax.F 775 val ii = ``<| proc := 0 |> : arm_coretypes$iiid`` 776 val T2 = thumb2_support arch 777 val IT = wordsSyntax.mk_wordii (if T2 then #itblock opt else 0,8) 778 val itstate = if T2 then SOME IT else NONE 779 val M = mode_to_term (#mode opt) 780 val E = endian_to_term endian 781 val A = arch_to_term arch 782 val inp = mk_inp instr 783 in 784 if mk_inp instr <> armSyntax.NoInterrupt_tm then 785 let 786 val CPSR = mk_irpt_cpsr the_state Thumb ThumbEE M 787 val (ext,state') = init the_state CPSR A thumbee 788 val reg_pre = snd (mk_reg_pre (the_state,M,state')) 789 in 790 (0,0,state', 791 mk_precondition the_state A NONE ext ThumbEE Thumb NONE 792 boolSyntax.T reg_pre boolSyntax.T) 793 end 794 else 795 let 796 val opc = Arbnum.fromHexString (remove_white_space instr) 797 handle Option => raise ERR "make_arm_state_and_pre" 798 "not a valid hex opcode" 799 val (enc,dec) = decode_opcode IT arch thumb thumbee opc 800 val (cond,instruction) = pairSyntax.dest_pair dec 801 val (flags_fupd,flags_pre) = set_flags the_state cond (#pass opt) 802 val CPSR = mk_cpsr the_state flags_fupd itstate Thumb ThumbEE E M 803 val (ext,state') = init the_state CPSR A thumbee 804 val opc = wordsSyntax.mk_wordi (opc,32) 805 val opc' = if not thumb orelse arch_version arch >= 5 806 then opc else ``0w:word32`` 807 val npass = if #pass opt then F else T 808 val tm = list_mk_comb (``arm_step$ARM_ALIGN_BX``, 809 [ii,npass,opc',enc,instruction,state']) 810 val (bx,state') = get_valuestate "ARM_ALIGN_BX" (restr_eval tm) 811 val tm = list_mk_comb (``arm_step$ARM_MEMORY_FOOTPRINT``, 812 [ii,npass,instruction,state']) 813 val (aligns,state') = 814 get_valuestate "ARM_MEMORY_FOOTPRINT" (restr_eval tm) 815 val (nmem,memory_fupd,memory_pre) = 816 mk_arm_memory state' endian arch enc opc bx aligns 817 val state' = list_mk_comb (``arm_seq_monad$arm_state_memory_fupd``, 818 [memory_fupd,state']) 819 val state' = restr_eval state' 820 val state' = apply_conv (PURE_REWRITE_CONV [UPDATE_ID_o2]) state' 821 val (nreg,reg_pre) = mk_reg_pre (the_state,M,state') 822 in 823 (nreg,nmem,state', 824 mk_precondition the_state A itstate ext ThumbEE Thumb 825 (SOME E) flags_pre reg_pre memory_pre) 826 end 827 end 828end; 829 830local 831 val lem1 = DECIDE ``(a <=/=> b) ==> (a <=> ~b)`` 832 val lem2 = DECIDE ``(a <=/=> b) ==> (b <=> ~a)`` 833 val lem3 = ``(-1w * a:'a word) << 1 = -1w * (a << 1)`` 834 |> wordsLib.WORD_ARITH_CONV |> Drule.EQT_ELIM |> Drule.GEN_ALL 835in 836 fun prove_character P G = Q.prove( 837 `!s. ^P s ==> (^G s = s)`, 838 STRIP_TAC 839 \\ PURE_REWRITE_TAC [ARM_ARCH_def, ARM_EXTENSIONS_def, 840 ARM_UNALIGNED_SUPPORT_def, ARM_READ_EVENT_REGISTER_def, 841 ARM_READ_INTERRUPT_WAIT_def, ARM_READ_SCTLR_def, ARM_READ_SCR_def, 842 ARM_READ_TEEHBR_def] 843 \\ Cases_on `s` 844 \\ SIMP_TAC (srw_ss()) 845 [WORD_NOT, WORD_LEFT_ADD_DISTRIB, IT_concat0, 846 aligned_concat, aligned_bx_concat, it_mode_concat] 847 \\ STRIP_TAC 848 \\ ASM_SIMP_TAC (srw_ss()) [arm_state_component_equality, 849 ARMinfo_component_equality, Coprocessors_component_equality, 850 coproc_state_component_equality, CP15reg_component_equality, 851 CP15sctlr_component_equality, ARMpsr_component_equality, 852 optionTheory.option_CLAUSES, APPLY_UPDATE_ID, aligned_thm, 853 aligned_n2w, align_n2w] 854 \\ ASM_SIMP_TAC (srw_ss()) 855 [align_relative_add_with_carry, lem3, APPLY_UPDATE_THM, 856 WORD_NOT, WORD_LEFT_ADD_DISTRIB, UPDATE_APPLY_IMP_ID] 857 \\ MATCH_MP_TAC UPDATE_APPLY_IMP_ID 858 \\ SRW_TAC [] [ARMpsr_component_equality, lem1, lem2] 859 ) 860end; 861 862fun prove_comp_thm the_state P H G X = Q.prove( 863 `^P ^the_state ==> (^H (^G ^the_state) = ^X)`, 864 BETA_TAC \\ STRIP_TAC 865 \\ PURE_REWRITE_TAC [arm_state_accfupds] 866 \\ computeLib.RESTR_EVAL_TAC restr_terms 867 \\ ASM_SIMP_TAC (srw_ss()++boolSimps.CONJ_ss) 868 [UPD11_SAME_KEY_AND_BASE, UPDATE_EQ, UPDATE_ID_o2, APPLY_UPDATE_THM, 869 WORD_EQ_ADD_LCANCEL_0, align_aligned, align_aligned3]); 870 871local 872 val lem1 = trace ("metis",0) (METIS_PROVE [WORD_EQ_ADD_RCANCEL]) 873 ``(((state:arm_seq_monad$arm_state).memory p = x) ==> 874 ((if p = a then x else state.memory a) = state.memory a)) /\ 875 ((state.memory (p + n) = x) ==> 876 ((if p = a then x else state.memory (a + n)) = state.memory (a + n)))`` 877 878 val lem2 = (CONJ signed_sat_def unsigned_sat_def) 879 |> SIMP_RULE std_ss [FUN_EQ_THM] |> GSYM 880 881 val lem4 = intLib.COOPER_PROVE ``&a + &b >= &c:int = a + b >= c:num`` 882 val lem5 = intLib.COOPER_PROVE ``a - b >= 0i = a >= b`` 883 val lem6 = intLib.COOPER_PROVE ``&a >= &b:int = a >= b:num`` 884 885 val lem7 = ``(~a + n2w b : word32) = (n2w b - 1w) - a`` 886 |> wordsLib.WORD_ARITH_CONV 887 |> Drule.EQT_ELIM |> bossLib.EVAL_RULE 888 |> REWRITE_RULE [GSYM word_sub_def] |> Drule.GEN_ALL 889 val lem8 = intLib.ARITH_PROVE ``(a + b * 65536i) / 65536 = a / 65536 + b`` 890 val lem9 = ``arm_step$word4 (a,b,c,d)`` |> EVAL |> SYM |> GEN_ALL 891 val lem10 = DECIDE ``~((a <=> b) /\ ~c) ==> ((if c then b else ~a) = b)`` 892 val lem11 = simpLib.SIMP_PROVE std_ss [COND_RAND] 893 ``(if b then align (x:word32,m) else align (x,n)) = 894 align (x,if b then m else n)`` 895 val lem12 = Q.prove(`word_modify (\i. COND (i = 0) T) (w:word32) = 896 (((31 >< 1) w):31 word) @@ (1w:bool[unit])`, 897 SRW_TAC [wordsLib.WORD_BIT_EQ_ss] []) 898 899 val align_rws = [lem1, lem7, aligned_thm, aligned_n2w, align_n2w, 900 aligned_bitwise_thm, aligned_pc_thm, optionTheory.option_CLAUSES, 901 WORD_SUB_LZERO, GSYM word_sub_def, UPDATE_ID_o2, it_mode_imp_thm, 902 aligned_bx_concat |> Drule.SPEC_ALL |> Thm.EQ_IMP_RULE |> fst |> GEN_ALL, 903 aligned_concat |> Drule.SPEC_ALL |> Thm.EQ_IMP_RULE |> fst |> GEN_ALL] 904 905 val record_rws = 906 [GSYM ARM_READ_MEM_def, GSYM ARM_WRITE_MEM_def, GSYM ARM_WRITE_MEM_o, 907 GSYM ARM_WRITE_MEM_READ_def, GSYM ARM_WRITE_MEM_WRITE_def, 908 ARM_READ_REG_FROM_MODE, ARM_WRITE_REG_FROM_MODE, 909 GSYM ARM_READ_REG_MODE, GSYM ARM_WRITE_REG_MODE, 910 GSYM ARM_WRITE_REG_o, GSYM ARM_MODE_def, 911 GSYM ARM_READ_IT_def, GSYM ARM_READ_GE_def, 912 GSYM ARM_READ_CPSR_def, GSYM ARM_WRITE_CPSR_def, 913 ARM_READ_SCTLR_def |> SIMP_RULE (srw_ss()) [] |> GSYM, 914 ARM_READ_SCR_def |> SIMP_RULE (srw_ss()) [] |> GSYM, 915 ARM_READ_TEEHBR_def |> SIMP_RULE (srw_ss()) [] |> GSYM, 916 GSYM ARM_READ_STATUS_def, GSYM ARM_READ_SCTLR_def, GSYM ARM_READ_SCR_def, 917 GSYM ARM_READ_TEEHBR_def, 918 GSYM ARM_READ_STATUS_SPSR_def, GSYM ARM_READ_MODE_SPSR_def, 919 GSYM ARM_READ_IT_SPSR_def, GSYM ARM_READ_GE_SPSR_def, 920 GSYM ARM_WAIT_FOR_EVENT_def, GSYM ARM_SEND_EVENT_def, 921 GSYM ARM_WAIT_FOR_INTERRUPT_def, 922 GSYM ARM_READ_SPSR_MODE, ARM_READ_SPSR_FROM_MODE, 923 GSYM ARM_WRITE_SPSR_MODE, ARM_WRITE_SPSR_FROM_MODE, 924 GSYM ARM_WRITE_PSR_o, ARM_WRITE_CPSR_o, ARM_WRITE_SPSR_o, 925 CPSR_COMPONENTS_OF_UPDATES, MARK_AND_CLEAR_EXCLUSIVE, MONITORS_OF_UPDATES, 926 FST_SHIFT_C, EXTRACT_ROR, SInt_0, 927 integerTheory.INT_ADD_RID, integerTheory.INT_ADD_LID, 928 integer_wordTheory.word_add_i2w_w2n, 929 integer_wordTheory.word_sub_i2w_w2n, 930 integer_wordTheory.word_add_i2w, 931 integer_wordTheory.word_sub_i2w, 932 GSYM integer_wordTheory.WORD_GEi, GSYM WORD_HS, WORD_EQ_SUB_ZERO, 933 lem2, lem4, lem5, lem6, lem8, lem9, lem10] 934 935 val updates_rws = 936 [ARM_WRITE_CPSR, ARM_WRITE_SPSR, 937 PSR_OF_UPDATES, REG_OF_UPDATES, MEM_OF_UPDATES, 938 CPSR_COMPONENTS_OF_UPDATES, SPSR_COMPONENTS_OF_UPDATES, 939 ARM_READ_STATUS_UPDATES, ARM_WRITE_SPSR_FROM_MODE, 940 ARM_READ_UNCHANGED, ARM_WRITE_STATUS_Q, 941 ARM_READ_CPSR_COMPONENT_UNCHANGED, 942 COND_RATOR, 943 Q.ISPEC `ARM_WRITE_CPSR` COND_RAND, 944 Q.ISPEC `ARM_WRITE_IT n` COND_RAND, 945 arm_bit_distinct, lem11, lem12] 946 947 fun OFFSET_CONV tm = 948 let 949 val (l,r) = wordsSyntax.dest_word_add tm 950 val (ll,lr) = wordsSyntax.dest_word_add l 951 in 952 if wordsSyntax.is_word_literal lr andalso 953 wordsSyntax.is_word_literal r 954 then 955 (REWR_CONV (GSYM wordsTheory.WORD_ADD_ASSOC) THENC 956 RAND_CONV wordsLib.WORD_EVAL_CONV) tm 957 else 958 raise ERR "OFFSET_CONV" "" 959 end 960in 961 val OFFSET_ss = simpLib.merge_ss [simpLib.rewrites [wordsTheory.WORD_ADD_0], 962 simpLib.std_conv_ss 963 {conv = OFFSET_CONV, name = "OFFSET_CONV", 964 pats = [``a + n2w b + n2w c : word32``]}] 965 966 val WORD_EQ_ss = simpLib.std_conv_ss 967 {conv = wordsLib.word_EQ_CONV, name = "word_EQ_CONV", 968 pats = [``n2w w = n2w y :'a word``]} 969 970 val BFC_ss = simpLib.std_conv_ss 971 {conv = wordsLib.WORD_EVAL_CONV, name = "WORD_EVAL_CONV", 972 pats = [``words$word_modify f 0xFFFFFFFFw : word32``]} 973 974 val ARM_ALIGN_ss = simpLib.merge_ss 975 [simpLib.rewrites align_rws, wordsLib.SIZES_ss, 976 numSimps.REDUCE_ss, SatisfySimps.SATISFY_ss] 977 978 val ARM_RECORD_ss = simpLib.merge_ss 979 [simpLib.rewrites record_rws, WORD_EQ_ss, 980 boolSimps.CONJ_ss, numSimps.REDUCE_ss] 981 982 val ARM_UPDATES_ss = simpLib.merge_ss 983 [simpLib.rewrites updates_rws, 984 OFFSET_ss, WORD_EQ_ss, BFC_ss] 985end; 986 987val SORT_PSR_UPDATES_CONV = 988 updateLib.OVERRIDE_UPDATES_CONV ``:(num # PSRName) -> ARMpsr`` 989 (PURE_REWRITE_CONV 990 [GSYM arm_coretypesTheory.PSRName2num_11, 991 arm_coretypesTheory.PSRName2num_thm, 992 pairTheory.PAIR_EQ, pairTheory.FST, pairTheory.SND] 993 THENC numLib.REDUCE_CONV); 994 995val SORT_REG_UPDATES_CONV = 996 updateLib.OVERRIDE_UPDATES_CONV ``:(num # RName) -> word32`` 997 (PURE_REWRITE_CONV 998 [GSYM arm_coretypesTheory.RName2num_11, 999 arm_coretypesTheory.RName2num_thm, 1000 pairTheory.PAIR_EQ, pairTheory.FST, pairTheory.SND] 1001 THENC numLib.REDUCE_CONV); 1002 1003val SORT_REG_UPDATES_RULE = 1004 Conv.CONV_RULE (Conv.RAND_CONV (Conv.RHS_CONV 1005 (Conv.ONCE_DEPTH_CONV SORT_PSR_UPDATES_CONV THENC 1006 Conv.ONCE_DEPTH_CONV SORT_REG_UPDATES_CONV))); 1007 1008local 1009 val endian_options = List.map (List.map lowercase) 1010 [["le", "little-endian", "LittleEndian"], 1011 ["be", "big-endian", "BigEndian"]] 1012 1013 val arch_options = List.map (List.map lowercase) 1014 [["v4", "ARMv4"], 1015 ["v4T", "ARMv4T"], 1016 ["v5", "v5T", "ARMv5", "ARMv5T"], 1017 ["v5TE", "ARMv5TE"], 1018 ["v6", "ARMv6"], 1019 ["v6K", "ARMv6K"], 1020 ["v6T2", "ARMv6T2"], 1021 ["v7", "v7_A", "v7-A", "ARMv7", "ARMv7_A", "ARMv7-A"], 1022 ["v7_R", "v7-R", "ARMv7_R", "ARMv7-R"]] 1023 1024 val mode_options = List.map (List.map lowercase) 1025 [["Usr", "User"], 1026 ["Fiq"], 1027 ["Irq"], 1028 ["Svc", "Supervisor"], 1029 ["Mon", "Monitor"], 1030 ["Abt", "Abort"], 1031 ["Und", "Undefined"], 1032 ["Sys", "System"]] 1033 1034 val pass_options = 1035 [["pass", "passed"], 1036 ["fail", "not-passed", "skip"]] 1037 1038 val thumb_options = 1039 [["thumb","thumb2","16-bit","16"], 1040 ["arm","32-bit","32"]] 1041 1042 val thumbee_options = 1043 [["thumbee","thumbx"]] 1044 1045 fun find_pos P l = 1046 let fun tail [] n = n 1047 | tail (h::t) n = if P h then n else tail t (n + 1) 1048 in 1049 tail l 0 1050 end 1051 1052 fun isDelim c = Char.isPunct c andalso (c <> #"-") andalso (c <> #":") orelse 1053 Char.isSpace c 1054 1055 val fromDec = Option.valOf o Int.fromString 1056 1057 val empty_string_set = Redblackset.empty Int.compare 1058 1059 fun process_option P g s d l f = 1060 let val (l,r) = List.partition P l 1061 val positions = Lib.mk_set (List.map g l) 1062 val result = 1063 if null positions then d else 1064 if List.length positions = 1 then 1065 f (hd positions) 1066 else 1067 raise ERR "process_option" 1068 ("More than one " ^ s ^ " option.") 1069 in 1070 (result,r) 1071 end 1072 1073 fun process_opt opt = process_option (Lib.C Lib.mem (List.concat opt)) 1074 (fn option => find_pos (Lib.mem option) opt) 1075 1076 val default_options = 1077 {arch = ARMv7_A, mode = Usr, endian = LittleEndian, 1078 pass = true, thumb = false, thumbee = false, itblock = 0} 1079in 1080 fun process_options s = 1081 let val l = Substring.tokens isDelim (Substring.full s) 1082 val l = List.map (lowercase o Substring.string) l 1083 val (endian,l) = process_opt endian_options "Endian" 1084 (#endian default_options) l 1085 (fn i => if i = 0 then LittleEndian else BigEndian) 1086 val (arch,l) = process_opt arch_options "Arch" 1087 (#arch default_options) l 1088 (fn i => 1089 case i 1090 of 0 => ARMv4 | 1 => ARMv4T 1091 | 2 => ARMv5T | 3 => ARMv5TE 1092 | 4 => ARMv6 | 5 => ARMv6K | 6 => ARMv6T2 1093 | 7 => ARMv7_A | 8 => ARMv7_R 1094 | _ => raise ERR "process_options" 1095 "Invalid Arch option.") 1096 val (mode,l) = process_opt mode_options "Mode" 1097 (#mode default_options) l 1098 (fn i => 1099 case i 1100 of 0 => Usr | 1 => Fiq | 2 => Irq | 3 => Svc 1101 | 4 => Mon | 5 => Abt | 6 => Und | 7 => Sys 1102 | _ => raise ERR "process_options" 1103 "Invalid Mode option.") 1104 val (pass,l) = process_opt pass_options "Pass" 1105 (#pass default_options) l (fn i => i = 0) 1106 val (thumbee,l) = process_opt thumbee_options "ThumbEE" 1107 (#thumbee default_options) l (fn i => i = 0) 1108 val (thumb,l) = process_opt thumb_options "Thumb" 1109 thumbee l (fn i => i = 0) 1110 val (itblock,l) = process_option (String.isPrefix "it:") 1111 (fn s => fromDec (String.extract (s,3,NONE))) 1112 "IT block" (#itblock default_options) l I 1113 in 1114 if null l then 1115 {arch = arch, mode = mode, endian = endian, pass = pass, 1116 thumb = thumb, thumbee = thumb andalso thumbee, itblock = itblock} 1117 else 1118 raise ERR "process_options" 1119 ("Unrecognized option: " ^ String.concat (commafy l)) 1120 end 1121end; 1122 1123local 1124 val fupd_set = 1125 (DB.definitions "arm_coretypes" @ 1126 DB.definitions "arm_seq_monad") 1127 |> List.map fst 1128 |> List.filter (String.isSuffix "_fupd") 1129 |> Redblackset.fromList String.compare 1130 fun is_fupd tm = 1131 case Lib.total Term.dest_const tm 1132 of SOME (s,_) => Redblackset.member (fupd_set,s) 1133 | NONE => false 1134in 1135 fun check_step thm = 1136 if !arm_step_check andalso 1137 Lib.can (HolKernel.find_term is_fupd) (concl thm) 1138 then 1139 (Parse.print_thm thm; 1140 print "\n"; 1141 raise ERR "check_step" "Found record update!") 1142 else 1143 thm 1144end 1145 1146local 1147 fun get_valuestate2 s tm = let 1148 val f = snd o get_valuestate s 1149 in 1150 case Lib.total boolSyntax.dest_cond tm 1151 of SOME (c,tm1,tm2) => [f tm1, f tm2] 1152 | NONE => [f tm] 1153 end 1154 val the_state = mk_var ("state",``:arm_seq_monad$arm_state``) 1155 fun mk_arm_next inp t = ``arm$arm_next <| proc := 0 |> ^inp ^t`` 1156 fun some_update fupd v s = 1157 case v of SOME u => list_mk_comb (fupd, [u,s]) 1158 | NONE => s 1159 fun maybe_dropn_o tm = 1160 if combinSyntax.is_update tm orelse combinSyntax.is_o tm then 1161 dropn_o (tm, 1) 1162 else 1163 SOME tm 1164 fun print_progress s = if !arm_step_trace mod 2 = 1 then 1165 TextIO.print s 1166 else 1167 () 1168 fun prove_comp_thms nreg nmem P G X = 1169 let 1170 val (reg,psr,mem,evt,wfi,acc,mon,_) = arm_state_standard_updates X 1171 val reg' = dropn_o (reg, nreg) 1172 val mem' = case mem of SOME m => dropn_o (m, nmem) 1173 | NONE => mem 1174 val psr' = dropn_o (psr, 1) 1175 val evt' = maybe_dropn_o evt 1176 val wfi' = maybe_dropn_o wfi 1177 val h = some_update 1178 ``arm_seq_monad$arm_state_registers_fupd`` reg' the_state 1179 val h = some_update ``arm_seq_monad$arm_state_memory_fupd`` mem' h 1180 val h = some_update ``arm_seq_monad$arm_state_psrs_fupd`` psr' h 1181 val h = some_update ``arm_seq_monad$arm_state_event_register_fupd`` evt' h 1182 val h = some_update ``arm_seq_monad$arm_state_interrupt_wait_fupd`` wfi' h 1183 val h = some_update ``arm_seq_monad$arm_state_accesses_fupd`` acc h 1184 val h = some_update ``arm_seq_monad$arm_state_monitors_fupd`` mon h 1185 val H = Term.mk_abs (the_state,h) 1186 in 1187 prove_comp_thm the_state P H G X handle HOL_ERR _ => 1188 raise ERR "eval_inst" "Failed to prove composition theorem" 1189 end 1190in 1191 fun arm_step options instr = 1192 let 1193 val opt = process_options options 1194 val (nreg, nmem, s, pre) = make_arm_state_and_pre the_state opt instr 1195 val P = mk_abs (the_state,pre) 1196 val G = mk_abs (the_state,s) 1197 val character_thm = prove_character P G handle HOL_ERR _ => 1198 raise ERR "eval_inst" 1199 "Failed to prove characteristic theorem" 1200 val init_state = mk_comb (mk_abs (the_state,s),the_state) 1201 val tm = mk_arm_next (mk_inp instr) init_state 1202 val _ = print_progress "Starting evaluation ...\n" 1203 val eval_thm = computeLib.RESTR_EVAL_CONV restr_terms tm 1204 val _ = print_progress "... finished evaluation.\n" 1205 val Xs = get_valuestate2 "next_arm" (rhsc eval_thm) 1206 val _ = print_progress "Starting composition proof(s) ...\n" 1207 val comp_thms = List.map (prove_comp_thms nreg nmem P G) Xs 1208 val _ = print_progress "... finished composition proof(s).\n" 1209 val next_thm = case comp_thms 1210 of [comp_thm] => 1211 Conv.BETA_RULE (Drule.MATCH_MP arm_next_thm 1212 (Drule.LIST_CONJ [character_thm,comp_thm,eval_thm])) 1213 | [comp_thm1, comp_thm2] => 1214 Conv.BETA_RULE (Drule.MATCH_MP arm_next_thm2 1215 (Drule.LIST_CONJ 1216 [character_thm,comp_thm1,comp_thm2,eval_thm])) 1217 | _ => raise ERR "arm_step" 1218 "Unexpected number of composition theorems" 1219 val thm = next_thm |> SORT_REG_UPDATES_RULE 1220 |> Drule.UNDISCH 1221 |> SIMP_RULE (bool_ss++ARM_ALIGN_ss) [Thm.ASSUME pre] 1222 |> Thm.DISCH pre 1223 |> with_flag (Cond_rewr.stack_limit,50) 1224 (SIMP_RULE (bool_ss++ARM_RECORD_ss) []) 1225 |> Drule.UNDISCH 1226 val pre' = hd (fst (Thm.dest_thm thm)) 1227 in 1228 thm |> with_flag (Cond_rewr.stack_limit,50) 1229 (SIMP_RULE (bool_ss++ARM_UPDATES_ss) [Thm.ASSUME pre']) 1230 |> Thm.DISCH pre' 1231 |> Thm.GEN the_state 1232 |> check_step 1233 end 1234end; 1235 1236end 1237 1238(* 1239open arm_encoderLib; 1240fun test opt s = arm_step opt (arm_encode_from_string s); 1241test "" "svc #4"; 1242test "" "adds r1, r2"; 1243test "" "ldrex r1,[r2]"; 1244 1245val test = arm_step "fiq"; 1246val _ = test "0xE591F000"; (* ldr pc,[r1] *) 1247val _ = test "0xF8110A00"; (* rfeda r1 *) 1248 1249Unsupported: 1250 all coprocessor instructions. 1251 1252Unsupported: 1253 strex <rd>,<rt>,[<rn>{,#<imm>}] 1254 strexb <rd>,<rt>,[<rn>] 1255 strexh <rd>,<rt>,[<rn>] 1256 strexd <rd>,<rt>,<rt2>,[<rn>] 1257 1258Unsupported: 1259 tbh [<rn>,<rn>,lsl #1] 1260 1261Unsupported for version < 6 (may give unpredictable results): 1262 adc pc,pc,#<const> 1263 sbc pc,pc,#<const> 1264 rsc pc,pc,#<const> 1265 mvn pc,<rn>,<shift> 1266 adc pc,<rn>,<rn>{,<shift>} 1267 sbc pc,<rn>,<rn>{,<shift>} 1268 rsc pc,<rn>,<rn>{,<shift>} 1269 1270Unsupported: 1271 ldr pc,[<rm>,+/-<rm>{,{shift}]{!} 1272 ldr pc,[pc,+/-<rm>{,{shift}] 1273 1274when UInt rm in {1,2,3,5,6,7,9,10,11,13,14} for version = 4 1275 and UInt rm in {2,6,10,13} for version >= 5 1276*) 1277