1open HolKernel boolLib bossLib Parse proofManagerLib; 2open arm_coretypesTheory arm_seq_monadTheory arm_opsemTheory arm_stepTheory; 3open MMUTheory MMU_SetupTheory inference_rulesTheory switching_lemma_helperTheory tacticsLib ARM_prover_extLib; 4 5val _ = new_theory("priv_constraints_spsr"); 6 7val _ = diminish_srw_ss ["one"] 8val _ = augment_srw_ss [rewrites [oneTheory.FORALL_ONE]] 9 10(****************************************************************) 11(* CONSTRAINTS ON SPSR FLAGS IN PRIVILEGED MODE *) 12(* Narges *) 13(****************************************************************) 14 15val let_ss = simpLib.mk_simpset [boolSimps.LET_ss] ; 16 17val prove_abs_spsr_flags_const_action = 18 fn (a, thms, abody_thm, expr,mode) => 19 let 20 val _ = set_goal([], `` 21 (priv_spsr_flags_constraints_abs ^a ^expr ^mode) ``) 22 val (a_abs,a_body) = pairLib.dest_pabs a; 23 val unbeta_thm= (PairRules.UNPBETA_CONV a_abs a_body) 24 val unbeta_a = mk_comb (a, a_abs) 25 val snd = get_type_inst (type_of(a_body) , false) 26 val a_body_type = get_type_inst (snd, true); 27 val proved_unbeta_lemma = store_thm ("proved_unbeta_lemma", 28 ``(priv_spsr_flags_constraints ^a_body ^expr ^mode)= 29 (priv_spsr_flags_constraints ^unbeta_a ^expr ^mode)``, 30 (ASSUME_TAC (SPECL [a_body,``^unbeta_a``, expr,mode] 31 (INST_TYPE [beta |-> a_body_type, 32 alpha |-> ``:arm_state``] 33 (List.nth(thms,0))))) 34 THEN ASSUME_TAC unbeta_thm 35 THEN RES_TAC); 36 37 val proved_preserve_unbeta_a = 38 store_thm ("proved_preserve_unbeta_a", 39 `` (priv_spsr_flags_constraints ^unbeta_a ^expr ^mode)``, 40 (ASSUME_TAC (proved_unbeta_lemma)) 41 THEN (ASSUME_TAC abody_thm) 42 THEN (FULL_SIMP_TAC (srw_ss()) [])); 43 44 val abs_type = type_of a_abs 45 val (abs_args, abs_body) = generate_uncurry_abs a 46 val tacs = (ASSUME_TAC proved_preserve_unbeta_a) 47 val gen_preserve_unbeta_thm = generalize_theorem proved_preserve_unbeta_a a; 48 val tacs = tacs THEN (ASSUME_TAC gen_preserve_unbeta_thm) 49 THEN (ASSUME_TAC ( 50 SPECL[a, expr,mode] 51 (INST_TYPE [alpha |-> abs_type, 52 beta |-> ``:arm_state``, 53 gamma |-> a_body_type] 54 (List.nth(thms,1))))) 55 THEN (RW_TAC (srw_ss()) []) 56 THEN (FULL_SIMP_TAC (srw_ss()) []) 57 THEN (UNDISCH_ALL_TAC THEN 58 (RW_TAC (srw_ss()) []) 59 THEN (FULL_SIMP_TAC (srw_ss()) [])) 60 val _ = e (tacs) 61 val proved_thm = top_thm() 62 val _ = proofManagerLib.drop(); 63 in 64 (proved_thm,tacs) 65 end 66 67 68 69val untouched_spsr_flags_abs_def = 70 Define `untouched_spsr_flags_abs f (mode:bool[5]) = 71 !s a c s'. (f a s = ValueState c s') ==> 72 let spsr = 73 case mode of 74 17w => SPSR_fiq 75 | 18w => SPSR_irq 76 | 19w => SPSR_svc 77 | 22w => SPSR_mon 78 | 23w => SPSR_abt 79 | 27w => SPSR_und 80 | _ => CPSR 81 in (*(spsr<>CPSR) ==>*) 82 ( 83 ((*! spsr. (spsr<>CPSR) ==>*) 84 (((s'.psrs(0,spsr)).I = (s.psrs(0,spsr)).I) /\ 85 ((s'.psrs(0,spsr)).F = (s.psrs(0,spsr)).F) /\ 86 ((s'.psrs (0,spsr)).M=(s.psrs (0,spsr)).M) /\ 87 ((s'.psrs (0,CPSR)).M=(s.psrs (0,CPSR)).M)) )) 88 `; 89 90val untouched_spsr_flags_def = 91 Define `untouched_spsr_flags f (mode:bool[5]) = 92 !s c s'. (f s = ValueState c s') ==> 93 let spsr = 94 case mode of 95 17w => SPSR_fiq 96 | 18w => SPSR_irq 97 | 19w => SPSR_svc 98 | 22w => SPSR_mon 99 | 23w => SPSR_abt 100 | 27w => SPSR_und 101 | _ => CPSR 102 in (*(spsr<>CPSR) ==>*) 103 ((*! spsr. (spsr<>CPSR) ==>*) 104 (((s'.psrs(0,spsr)).I = (s.psrs(0,spsr)).I) /\ 105 ((s'.psrs(0,spsr)).F = (s.psrs(0,spsr)).F) /\ 106 ((s'.psrs (0,spsr)).M=(s.psrs (0,spsr)).M)/\ 107 ((s'.psrs (0,CPSR)).M=(s.psrs (0,CPSR)).M)) ) 108 `; 109 110 111val priv_spsr_flags_constraints_def = 112 Define `priv_spsr_flags_constraints f cpsr mode = 113 ! s s' a . (f s = ValueState a s') ==> 114 (~access_violation s') ==> 115 ((s'.psrs(0,CPSR)).M = mode) ==> 116 ( let spsr = 117 case mode of 118 17w => SPSR_fiq 119 | 18w => SPSR_irq 120 | 19w => SPSR_svc 121 | 22w => SPSR_mon 122 | 23w => SPSR_abt 123 | 27w => SPSR_und 124 | _ => CPSR 125 in (*(spsr<>CPSR) ==>*) 126 ( ((s'.psrs(0,spsr)).I = cpsr.I) /\ 127 ((s'.psrs(0,spsr)).F = cpsr.F)/\ 128 ((s'.psrs (0,spsr)).M=cpsr.M)) 129 130 )`; 131 132 133val priv_spsr_flags_constraints_abs_def = 134 Define `priv_spsr_flags_constraints_abs f cpsr mode = 135 ! s s' a c. (f c s = ValueState a s') ==> 136 (~access_violation s') ==> 137 ((s'.psrs(0,CPSR)).M = mode) ==> 138 ( let spsr = 139 case mode of 140 17w => SPSR_fiq 141 | 18w => SPSR_irq 142 | 19w => SPSR_svc 143 | 22w => SPSR_mon 144 | 23w => SPSR_abt 145 | 27w => SPSR_und 146 | _ => CPSR 147 148 in 149 150 (* (spsr<>CPSR) ==>*) 151 (((s'.psrs(0,spsr)).I = cpsr.I) /\ 152 ((s'.psrs(0,spsr)).F = cpsr.F)/\ 153 ((s'.psrs (0,spsr)).M=cpsr.M))) 154 `; 155 156 157(********************* proof rules *******************************) 158 159val seqT_priv_spsr_flags_constraints_before_thm = 160 store_thm("seqT_priv_spsr_flags_constraints_before_thm", 161 `` ! g f cpsr spsr. priv_spsr_flags_constraints_abs f cpsr spsr ==> 162 priv_spsr_flags_constraints (g >>= f) cpsr spsr ``, 163 (RW_TAC (srw_ss()) [seqT_def, 164 priv_spsr_flags_constraints_def, 165 priv_spsr_flags_constraints_abs_def]) 166 THEN FULL_SIMP_TAC (let_ss) [] 167 THEN ASSUME_TAC 168 (SPECL [``g:'a M``, ``f: 'a -> 'b M``, 169 ``s:arm_state``,``a:'b``, 170 ``s':arm_state``(* ,``b:arm_state``, *) 171 (* ``a':'a`` *)] 172 seqT_access_violation_thm) 173 THEN FULL_SIMP_TAC (srw_ss()) [seqT_def] 174 THEN Cases_on `g s` 175 THEN FULL_SIMP_TAC (srw_ss()) [] 176 THEN Cases_on `access_violation b` 177 (* THEN Q.UNABBREV_TAC `spsr` *) 178 THEN PAT_X_ASSUM ``! s s' a c .X ==> Z`` 179 (fn thm => ASSUME_TAC 180 (SPECL [``b:arm_state``,``s':arm_state``, 181 ``a:'b``,``a':'a``] thm)) 182 THEN FULL_SIMP_TAC (srw_ss()) [] 183 THEN RES_TAC 184 THEN FULL_SIMP_TAC (srw_ss()) [seqT_def] 185 ); 186 187 188 189val parT_priv_spsr_flags_constraints_before_thm = 190 store_thm("parT_priv_spsr_flags_constraints_before_thm", 191 `` !f g cpsr spsr . priv_spsr_flags_constraints f cpsr spsr ==> 192 priv_spsr_flags_constraints (g ||| f) cpsr spsr ``, 193 RW_TAC (srw_ss()) 194 [parT_def,seqT_def, 195 priv_spsr_flags_constraints_def, 196 untouched_spsr_flags_def,constT_def] 197 THEN FULL_SIMP_TAC (let_ss) [] 198 THEN IMP_RES_TAC 199 (SIMP_RULE bool_ss 200 [seqT_def,parT_def,constT_def] 201 (SPECL [``g:'a M``, ``f: 'b M``, 202 ``s:arm_state``,``a:('a#'b)``, 203 ``s':arm_state`` ,``b:arm_state``, 204 ``a':'a`` ] 205 parT_access_violation_thm)) 206 THEN Cases_on `g s` 207 THEN Cases_on `f b` 208 (* THEN Q.UNABBREV_TAC `spsr` *) 209 THEN FULL_SIMP_TAC (srw_ss()) [] 210 THEN PAT_X_ASSUM ``! s s' a .(f s = ValueState a s') ==> Z`` (fn thm => ASSUME_TAC 211 (SPECL [``b:arm_state``,``b':arm_state``,``a'':'a``] thm)) 212 THEN Cases_on `access_violation b` 213 THEN Cases_on `access_violation b'` 214 THEN RES_TAC 215 THEN FULL_SIMP_TAC (srw_ss()) [] 216 THEN FIRST_PROVE [ FULL_SIMP_TAC (srw_ss()) [] 217 THEN RW_TAC (srw_ss()) [] , 218 (UNDISCH_ALL_TAC 219 THEN RW_TAC (srw_ss()) [] 220 THEN FULL_SIMP_TAC (srw_ss()) [])]); 221 222 223 224val seqT_priv_spsr_flags_constraints_after_thm = 225 store_thm("seqT_priv_spsr_flags_constraints_after_thm", 226 `` !f g cpsr mode. priv_spsr_flags_constraints g cpsr mode ==> 227 ( untouched_spsr_flags_abs f mode) ==> 228 priv_spsr_flags_constraints (g >>= f) cpsr mode``, 229 (RW_TAC (srw_ss()) [seqT_def, 230 priv_spsr_flags_constraints_def, 231 priv_spsr_flags_constraints_abs_def, 232untouched_spsr_flags_abs_def]) THEN 233 FULL_SIMP_TAC (let_ss) [] THEN 234 Cases_on `g s` THEN 235 FULL_SIMP_TAC (srw_ss()) [] THEN 236 Cases_on `access_violation b` 237 THEN Q.UNABBREV_TAC `spsr` 238 THEN PAT_X_ASSUM ``! s s' a .X ==> Z`` 239 (fn thm => ASSUME_TAC 240 (SPECL [``s:arm_state``,``b:arm_state``, 241 ``a':'a``] thm)) 242 243 THEN PAT_X_ASSUM ``! s1 a c s2. X`` 244 (fn thm => ASSUME_TAC 245 (SPECL [``b:arm_state``,``a':'a``, 246 ``a:'b``,``s':arm_state``] thm)) 247 248 THEN RES_TAC 249 THEN UNDISCH_ALL_TAC 250 THEN RW_TAC (srw_ss()) [] 251 THEN FULL_SIMP_TAC (srw_ss()) [] 252 THEN FULL_SIMP_TAC (srw_ss()) []); 253 254val parT_priv_spsr_flags_constraints_after_thm = 255 store_thm("parT_priv_spsr_flags_constraints_after_thm", 256`` !f g cpsr spsr. priv_spsr_flags_constraints g cpsr spsr ==> 257 (untouched_spsr_flags f spsr) ==> 258 priv_spsr_flags_constraints (g ||| f) cpsr spsr``, 259 (RW_TAC (srw_ss()) 260 [parT_def,seqT_def, 261 priv_spsr_flags_constraints_def, 262 untouched_spsr_flags_def,constT_def]) 263 THEN FULL_SIMP_TAC (let_ss) []THEN 264 Cases_on `g s` THEN 265 Cases_on `f b` THEN 266 Cases_on `access_violation b` THEN 267 Cases_on `access_violation b'` THEN 268 FULL_SIMP_TAC (srw_ss()) [] THEN 269 PAT_X_ASSUM ``! s a s' .(f s = ValueState a s') ==> Z`` 270 (fn thm => ASSUME_TAC 271 (SPECL [``b:arm_state``,``a'':'a``,``b':arm_state``] thm)) 272 THEN PAT_X_ASSUM ``! s1 c s2. X`` 273 (fn thm => ASSUME_TAC 274 (SPECL [``s:arm_state``,``b:arm_state``,``a':'b``] thm)) 275 THEN RES_TAC 276 THEN UNDISCH_ALL_TAC 277 THEN RW_TAC (srw_ss()) [] 278 THEN FULL_SIMP_TAC (srw_ss()) [] 279 ); 280 281 282val seqT_trans_untouched_thm = 283 store_thm("seqT_trans_untouched_thm", 284 `` !f g mode. 285 (untouched_spsr_flags f mode) ==> 286 (untouched_spsr_flags_abs g mode) ==> 287 (untouched_spsr_flags (f>>=g) mode)``, 288 (RW_TAC (srw_ss()) [seqT_def,untouched_spsr_flags_abs_def, 289 untouched_spsr_flags_def]) 290THEN Cases_on `f s` 291 THEN FULL_SIMP_TAC (let_ss) [] 292 THEN PAT_X_ASSUM ``! s1 c s2. (f _ = ValueState _ _) ==> _`` 293 (fn thm => ASSUME_TAC 294 (SPECL [``s:arm_state``,``a:'a``,``b:arm_state``] thm)) 295 THEN RES_TAC 296 THEN Cases_on `access_violation b` 297 THEN FULL_SIMP_TAC (srw_ss()) [] 298 THEN RW_TAC (srw_ss()) [] 299 THEN PAT_X_ASSUM ``! s a c s'. X`` 300 (fn thm => ASSUME_TAC 301 (SPECL [``b:arm_state``,``a:'a``, 302 ``c:'b``,``s':arm_state``] thm)) 303 THEN RES_TAC 304 THEN FULL_SIMP_TAC (srw_ss()) [] 305 THEN RW_TAC (srw_ss()) []); 306 307val parT_trans_untouched_thm = 308 store_thm("parT_trans_untouched_thm", 309 `` !f g spsr. 310 (untouched_spsr_flags f spsr) ==> 311 (untouched_spsr_flags g spsr) ==> 312 (untouched_spsr_flags (f ||| g) spsr)``, 313 (RW_TAC (srw_ss()) [seqT_def,parT_def,constT_def, 314 untouched_spsr_flags_def]) 315 THEN Cases_on `f s` 316 THEN Cases_on `access_violation b` 317 THEN Cases_on `g b` 318 THEN Cases_on `access_violation b'` 319 THEN FULL_SIMP_TAC (let_ss) [] 320 THEN PAT_X_ASSUM ``! s c s'. X`` 321 (fn thm => ASSUME_TAC 322 (SPECL [``b:arm_state``,``a':'b``, 323 ``b':arm_state``] thm)) 324 THEN PAT_X_ASSUM ``! s1 c s2. (f _ = ValueState _ _) ==> _`` 325 (fn thm => ASSUME_TAC 326 (SPECL [``s:arm_state``,``a:'a``,``b:arm_state``] thm)) 327 THEN RES_TAC 328 THEN FULL_SIMP_TAC (srw_ss()) [] 329 THEN RW_TAC (srw_ss()) [] 330 ); 331 332 333val spfc_first_abs_lemma = 334 store_thm ("spfc_first_abs_lemma", 335 ``!f g x y. (f=g) ==> ((priv_spsr_flags_constraints f x y) = 336 (priv_spsr_flags_constraints g x y))``, 337 RW_TAC (srw_ss()) []); 338 339 340val spfc_second_abs_lemma = 341 store_thm ("spfc_second_abs_lemma", 342 ``! f x z. (! y. priv_spsr_flags_constraints (f y) x z) = 343 priv_spsr_flags_constraints_abs f x z``, 344 RW_TAC (srw_ss()) [priv_spsr_flags_constraints_def,priv_spsr_flags_constraints_abs_def] 345 THEN METIS_TAC []); 346 347 348(********************* end of proof rules *******************************) 349(******************* basic lemmas **************************************) 350 351val read_cpsr_fixed_lem = 352 store_thm("read_cpsr_fixed_lem", 353 ``!s. read_cpsr <|proc := 0|> s = ValueState (s.psrs (0,CPSR)) s``, 354 EVAL_TAC 355 THEN RW_TAC (srw_ss()) []); 356 357(* if possible, try to optimize it *) 358val write_spsr_sfc_thm = 359 store_thm("write_spsr_sfc_thm", 360 ``! cpsr mode. priv_spsr_flags_constraints (write_spsr <|proc := 0|> cpsr) 361 cpsr mode ``, 362 363 RW_TAC (bool_ss) [write_spsr_def,seqT_def,priv_spsr_flags_constraints_def] 364 THEN Cases_on `read_cpsr <|proc := 0|> s` 365 THEN FIRST_PROVE [ 366 FULL_SIMP_TAC (srw_ss()) [] 367 THEN ASSUME_TAC (SPEC ``s:arm_state`` read_cpsr_fixed_lem) 368 THEN Cases_on `access_violation b` 369 THENL [ 370 FULL_SIMP_TAC (srw_ss()) [] 371 THEN RW_TAC (srw_ss()) [] 372 THEN FULL_SIMP_TAC (srw_ss()) [], 373 Cases_on ` bad_mode <|proc := 0|> a'.M b` 374 THENL 375 [ 376 FULL_SIMP_TAC (srw_ss()) [] 377 THEN Cases_on `access_violation b'` 378 THENL[ 379 FULL_SIMP_TAC (srw_ss()) [] 380 THEN RW_TAC (srw_ss()) [] 381 THEN FULL_SIMP_TAC (srw_ss()) [] 382 , 383 FULL_SIMP_TAC (srw_ss()) [] 384 THEN Cases_on `a''` 385 THENL [ 386 FULL_SIMP_TAC (srw_ss()) [] 387 (* THEN Q.UNABBREV_TAC `spsr` *) 388 THEN UNDISCH_ALL_TAC 389 THEN EVAL_TAC, 390 TRY (Q.UNABBREV_TAC `spsr`) 391 THEN UNDISCH_ALL_TAC 392 THEN EVAL_TAC 393 THEN RW_TAC (srw_ss()) [] THEN 394 FULL_SIMP_TAC (srw_ss()) [] 395 THEN UNDISCH_ALL_TAC 396 THEN EVAL_TAC 397 THEN RW_TAC (srw_ss()) [] THEN 398 FULL_SIMP_TAC (srw_ss()) []]], 399 FULL_SIMP_TAC (srw_ss()) []]], 400 FULL_SIMP_TAC (srw_ss()) []]); 401 402 403val write_lr_reg_sfc_ut_thm = 404 store_thm("write_lr_reg_sfc_ut_thm", 405 ``! value mode. 406 (untouched_spsr_flags (write_reg <|proc:=0|> 14w value) mode)``, 407 EVAL_TAC 408 THEN RW_TAC (srw_ss()) [] 409 THEN UNDISCH_ALL_TAC 410 THEN EVAL_TAC 411 THEN RW_TAC (srw_ss()) [] 412 THEN FULL_SIMP_TAC (srw_ss()) []); 413 414val read_cpsr_sfc_ut_thm = 415 store_thm("read_cpsr_sfc_ut_thm", 416 `` !mode. 417 (untouched_spsr_flags (read_cpsr <|proc:=0|> ) mode )``, 418 EVAL_TAC 419 THEN RW_TAC (srw_ss()) [] ); 420 421val branch_to_sfc_ut_thm = 422 store_thm("branch_to_sfc_ut_thm", 423 ``!adr mode. untouched_spsr_flags ( 424 branch_to <|proc:=0|> adr) mode``, 425 EVAL_TAC 426 THEN RW_TAC (srw_ss()) [] 427 THEN UNDISCH_ALL_TAC 428 THEN EVAL_TAC 429 THEN RW_TAC (srw_ss()) [] 430 THEN FULL_SIMP_TAC (srw_ss()) []); 431 432val constT_sfc_ut_thm = 433 store_thm("constT_sfc_ut_thm", 434 ``! mode. untouched_spsr_flags_abs (��(u1:unit,u2:unit,u3:unit,u4:unit). constT ()) mode``, 435 EVAL_TAC 436 THEN RW_TAC (srw_ss()) [] ); 437 438val write_cpsr_sfc_ut_thm = 439 store_thm("write_cpsr_sfc_ut_thm", 440 ``untouched_spsr_flags ( 441 read_cpsr <|proc:=0|> >>= 442 (��cpsr. 443 write_cpsr <|proc:=0|> 444 (cpsr with 445<|I := T; IT := 0w; J := F; T := sctlr.TE; 446E := sctlr.EE|>))) 27w``, 447 EVAL_TAC 448 THEN RW_TAC (srw_ss()) [] 449 THEN UNDISCH_ALL_TAC 450 THEN EVAL_TAC 451 THEN RW_TAC (srw_ss()) [] 452 THEN FULL_SIMP_TAC (srw_ss()) []); 453 454val take_undef_writing_part_spf_thm = 455 save_thm ("take_undef_writing_part_spf_thm", 456 let 457 val a = SIMP_CONV (bool_ss) [take_undef_instr_exception_def] 458 ``take_undef_instr_exception <|proc:=0|> ``; 459 val (_, a') = (dest_eq (concl a)) 460 val (l,r,rb1)= decompose_term a'; 461 val (l2,r2,rb2)= decompose_term rb1 462 val (l3,r3,rb3)= decompose_term rb2 463 val (l4,r4,rb4)= decompose_term l3 464 val (l5,r5,rb5)= decompose_term r4 465 val (l6,r6,rb6)= decompose_term r5; 466 (* proof of r5 *) 467 val thm1 = LIST_MP [ write_cpsr_sfc_ut_thm, 468 (SPECL [``(ExcVectorBase + 4w:bool[32])``, 469 ``27w:bool[5]``] branch_to_sfc_ut_thm)] 470 (SPECL [l6,r6,``27w:bool[5]``] 471 (INST_TYPE [alpha |-> ``:unit``, 472 beta |-> ``:unit``] 473 parT_trans_untouched_thm)); 474 (* proof of r4 *) 475 val thm2 = LIST_MP [ 476 (SPECL [``(if cpsr:ARMpsr.T then 477 (pc:word32) ��� 2w else pc ��� 4w)``, 478 ``27w:word5``] write_lr_reg_sfc_ut_thm), 479 thm1] 480 (SPECL [l5,r5,``27w:bool[5]``] 481 (INST_TYPE [alpha |-> ``:unit``, 482 beta |-> ``:(unit#unit)``] 483 parT_trans_untouched_thm)); 484 (* proof of l3 *) 485 val thm3 = LIST_MP [ 486 (SPECL [``cpsr:ARMpsr``,``27w:word5``] write_spsr_sfc_thm), 487 thm2] 488 (SPECL [r4,l4,``cpsr:ARMpsr``,``27w:word5``] 489 (INST_TYPE [beta |-> ``:unit``, 490 alpha |-> ``:(unit#unit#unit)``] 491 parT_priv_spsr_flags_constraints_after_thm)); 492 (* proof of rb2 *) 493 val thm4 = LIST_MP [ 494 thm3, 495 SPEC ``27w:word5`` constT_sfc_ut_thm] 496 (SPECL [r3,l3,``cpsr:ARMpsr``,``27w:word5``] 497 (INST_TYPE [beta |-> ``:unit``, 498 alpha |-> ``:(unit#unit#unit#unit)``] 499 seqT_priv_spsr_flags_constraints_after_thm)); 500 (* proof of rb1 *) 501 val (thm5 , _) = prove_abs_spsr_flags_const_action (r2, [spfc_first_abs_lemma, 502 spfc_second_abs_lemma], 503 thm4, ``cpsr:ARMpsr``, 504 ``27w:word5``); 505 val thm6 = MP (SPECL [l2,r2,``cpsr:ARMpsr``,``27w:word5``] 506 (INST_TYPE [beta |-> ``:unit``, 507 alpha |-> ``:(unit#unit)``] 508 seqT_priv_spsr_flags_constraints_before_thm)) thm5; 509 in 510 (GEN_ALL thm6) 511 end 512); 513 514(* to be replaced *) 515val r' = ``(��(pc,ExcVectorBase,cpsr:ARMpsr,scr,sctlr). 516 (condT ((s.psrs (0,CPSR)).M = 22w) 517 (write_scr <|proc := 0|> (scr with NS := F)) ||| 518 write_cpsr <|proc := 0|> (s.psrs (0,CPSR) with M := 27w)) >>= 519 (��(u1,u2). 520 (write_spsr <|proc := 0|> (s.psrs (0,CPSR)) ||| 521 write_reg <|proc := 0|> 14w 522 (if (s.psrs (0,CPSR)).T then 523 pc + 0xFFFFFFFEw 524 else 525 pc + 0xFFFFFFFCw) ||| 526 read_cpsr <|proc := 0|> >>= 527 (��cpsr. 528 write_cpsr <|proc := 0|> 529 (cpsr with 530 <|IT := 0w; J := F; E := sctlr.EE; I := T; 531 T := sctlr.TE|>)) ||| 532 branch_to <|proc := 0|> (ExcVectorBase + 4w)) >>= 533 (��(u1,u2,u3,u4). constT ())))``; 534 535(* 536val take_undef_instr_exception_spsr_flags_thm = 537 store_thm ("take_undef_instr_exception_spsr_flags_thm", 538 `` ! s a s' . (take_undef_instr_exception <|proc:=0|> s = ValueState a s') ==> 539 (~access_violation s') ==> 540 ((s'.psrs(0,CPSR)).M = 27w) ==> 541 ( ( ((s'.psrs(0,SPSR_und)).I = (s.psrs(0,CPSR)).I) 542 /\ 543 ((s'.psrs(0,SPSR_und)).F = (s.psrs(0,CPSR)).F) 544 /\ 545 ((s'.psrs (0,SPSR_und)).M=(s.psrs(0,CPSR)).M)))``, 546 let val athm = SIMP_CONV (bool_ss) [take_undef_instr_exception_def] 547 ``take_undef_instr_exception <|proc:=0|> `` 548 val (_, a) = (dest_eq (concl athm)) 549 val (l,r,_)= decompose_term a 550 val sl_elm2 = ``(a':(word32 # word32 # ARMpsr # CP15scr # CP15sctlr))`` 551 val spec_list = (mk_spec_list sl_elm2)@[``b:arm_state``, ``s':arm_state``,``a:unit``] 552 val spec_list2 = [``b:arm_state``] @ List.rev (mk_spec_list2 (sl_elm2)) 553 in 554 RW_TAC (bool_ss) [take_undef_instr_exception_def] 555 THEN ASSUME_TAC (SPECL [``s:arm_state``,r] 556 (INST_TYPE [alpha |-> ``:unit``] fixed_cpsr_thm)) 557 THEN FULL_SIMP_TAC (srw_ss()) [] 558 THEN FULL_SIMP_TAC (let_ss) [] 559 THEN PAT_X_ASSUM ``X=Y`` (fn thm => THROW_AWAY_TAC (concl thm)) 560 THEN ASSUME_TAC const_comp_take_undef_exception_rp_thm 561 THEN RW_TAC (srw_ss()) [priv_spsr_flags_constraints_def, 562 priv_spsr_flags_constraints_abs_def] 563 THEN FULL_SIMP_TAC (srw_ss()) [const_comp_def] 564 THEN NTAC 3 565 (Cases_on [QUOTE ("("^(term_to_string l) ^ ") s")] 566 THEN IMP_RES_TAC seqT_access_violation_thm 567 THENL 568 [ RES_TAC 569 THEN RW_TAC (srw_ss()) [] 570 THEN IMP_RES_TAC hlp_seqT_thm 571 THEN PAT_X_ASSUM ``X a' b= ValueState a s'`` 572 (fn thm => ASSUME_TAC (PairRules.PBETA_RULE thm)) 573 THEN 574 ASSUME_SPECL_TAC spec_list (GEN_ALL 575 (SIMP_RULE (bool_ss) 576 [priv_spsr_flags_constraints_def] 577 take_undef_writing_part_spf_thm)) 578 THEN PAT_X_ASSUM ``X ==> Y`` (fn thm => ASSUME_TAC (PairRules.PBETA_RULE thm)) 579 THEN 580 ASSUME_TAC (SPECL spec_list2 fixed_cpsr_thm2) 581 THEN RES_TAC 582 THEN RES_TAC 583 THEN FULL_SIMP_TAC (srw_ss()) [get_spsr_by_mode_def] 584 THEN FULL_SIMP_TAC (let_ss) [] 585 THEN RW_TAC (srw_ss()) [] 586 , 587 IMP_RES_TAC (SPEC r' ( 588 INST_TYPE [beta |-> ``:unit``, 589 alpha |-> ``:(word32 # word32 # ARMpsr # CP15scr # CP15sctlr)`` ] 590 hlp_errorT_thm)) 591 THEN 592 PAT_X_ASSUM ``! (s:arm_state) . X `` 593 (fn thm => ASSUME_TAC (SPEC ``s:arm_state`` thm)) 594 THEN RW_TAC (srw_ss()) [] 595 THEN FULL_SIMP_TAC (srw_ss()) [] 596 ]) 597 end); 598*) 599 600val _ = export_theory(); 601