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(*open arm_parserLib arm_encoderLib arm_disassemblerLib;*) 5 6 7val _ = new_theory("priv_constraints_cpsr_pc"); 8val _ = diminish_srw_ss ["one"] 9val _ = augment_srw_ss [rewrites [oneTheory.FORALL_ONE]] 10 11val _ = goalStack.chatting := !Globals.interactive 12 13(**** the problem: vector table is based on mode not exception type ******) 14 15 16(****************************************************************) 17(* CONSTRAINTS ON CPSR FLAGS IN PRIVILEGED MODE *) 18(* Narges *) 19(****************************************************************) 20val priv_cpsr_flags_constraints_def = 21 Define `priv_cpsr_flags_constraints f sctlr = 22 ! s s' a . (f s = ValueState a s') ==> 23 (~access_violation s') ==> 24 (((s'.psrs (0, CPSR)).I = T) 25 /\ 26 ((s'.psrs (0, CPSR)).J = F) 27 /\ 28 ((s'.psrs (0, CPSR)).IT = 0w) /\ 29 ((s'.psrs (0,CPSR)).E = sctlr.EE) 30 )`; 31 32val priv_cpsr_flags_constraints_abs_def = 33 Define `priv_cpsr_flags_constraints_abs f sctlr = 34 ! s s' a c. (f c s = ValueState a s') ==> 35 (~access_violation s') ==> 36 (((s'.psrs (0, CPSR)).I = T) 37 /\ 38 ((s'.psrs (0, CPSR)).J = F) 39 /\ 40 ((s'.psrs (0, CPSR)).IT = 0w) 41 /\ 42 ((s'.psrs (0,CPSR)).E = sctlr.EE) 43 )`; 44 45 46fun define_cfc_goal a expr = 47 let val sctlr = List.nth(expr,0) 48 in 49 set_goal([], `` 50 (priv_cpsr_flags_constraints ^a ^sctlr) ``) 51 end; 52 53fun define_cfc_goal_abs a expr = 54 let val sctlr = List.nth(expr,0) 55 in 56 set_goal([], `` 57 (priv_cpsr_flags_constraints_abs ^a ^sctlr) ``) 58 end; 59 60val seqT_priv_cpsr_flags_constraints_thm = 61 store_thm("seqT_priv_cpsr_flags_constraints_thm", 62 `` !f g sctlr. priv_cpsr_flags_constraints_abs f sctlr ==> 63 priv_cpsr_flags_constraints (g >>= f) sctlr``, 64 (RW_TAC (srw_ss()) [priv_cpsr_flags_constraints_def, 65 priv_cpsr_flags_constraints_abs_def]) 66 THEN Cases_on `g s` 67 THEN IMP_RES_TAC switching_lemma_helperTheory.seqT_access_violation_thm 68 THEN FULL_SIMP_TAC (srw_ss()) [arm_seq_monadTheory.seqT_def] 69 THEN Cases_on `access_violation b` 70 THEN PAT_X_ASSUM ``! s s' a c.X ==> Z`` 71 (fn thm => ASSUME_TAC 72 (SPECL [``b:arm_state``,``s':arm_state``, 73 ``a:'b``,``a':'a``] thm)) 74 THEN FULL_SIMP_TAC (srw_ss()) [] 75 THEN RES_TAC 76 THEN FULL_SIMP_TAC (srw_ss()) [] 77 ); 78 79val parT_priv_cpsr_flags_constraints_thm = 80 store_thm("parT_priv_cpsr_flags_constraints_thm", 81 `` !f g ee. priv_cpsr_flags_constraints f ee ==> 82 priv_cpsr_flags_constraints (g ||| f) ee``, 83 (RW_TAC (srw_ss()) 84 [ 85 priv_cpsr_flags_constraints_def]) 86 THEN Cases_on `g s` 87 THEN IMP_RES_TAC switching_lemma_helperTheory.parT_access_violation_thm 88 THEN FULL_SIMP_TAC (srw_ss()) [parT_def,seqT_def] 89 THEN Cases_on `f b` 90 THEN Cases_on `access_violation b` 91 THEN Cases_on `access_violation b'` 92 THEN FULL_SIMP_TAC (srw_ss()) [] 93 THEN PAT_X_ASSUM ``! s s' a.(f s = ValueState a s') ==> Z`` 94 (fn thm => ASSUME_TAC 95 (SPECL [``b:arm_state``,``b':arm_state``,``a'':'a``] thm)) 96 THEN FIRST_PROVE [RES_TAC 97 THEN FULL_SIMP_TAC (srw_ss()) [] 98 THEN RW_TAC (srw_ss()) [] , 99 (UNDISCH_ALL_TAC 100 THEN EVAL_TAC 101 THEN RW_TAC (srw_ss()) [])]); 102 103val write_cpsr_cfc_thm = 104 store_thm("write_cpsr_cfc_thm", 105 ``! sctlr. 106 (priv_cpsr_flags_constraints 107 ( write_cpsr <|proc:=0|> 108 (cpsr with 109 <|IT := 0w; J := F; E := sctlr.EE; I := T; 110 T := sctlr.TE|>)) sctlr) 111/\ 112 (priv_cpsr_flags_constraints 113 ( write_cpsr <|proc:=0|> 114 (cpsr with 115 <|I := T; 116 A := 117 ((��have_security_exta ��� ��scr.NS ��� scr.AW) ��� 118 cpsr.A); IT := 0w; J := F; T := sctlr.TE; 119 E := sctlr.EE|>)) sctlr) 120/\ 121 (priv_cpsr_flags_constraints 122 (write_cpsr <|proc:=0|> 123 (cpsr with 124 <|I := T; 125 F := 126 ((��have_security_exta ��� ��scr.NS ��� scr.AW) ��� 127 cpsr.F); 128 A := 129 ((��have_security_exta ��� ��scr.NS ��� scr.AW) ��� 130 cpsr.A); IT := 0w; J := F; T := sctlr.TE; 131 E := sctlr.EE|>)) sctlr) 132 ``, 133 EVAL_TAC 134 THEN RW_TAC (srw_ss()) [priv_cpsr_flags_constraints_def] 135 THEN EVAL_TAC 136 THEN RW_TAC (srw_ss()) []); 137 138 139val cfc_first_abs_lemma = 140 store_thm ("cfc_first_abs_lemma", 141 ``!f g x. (f=g) ==> ((priv_cpsr_flags_constraints f x) = 142 (priv_cpsr_flags_constraints g x))``, 143 RW_TAC (srw_ss()) []); 144 145 146val cfc_second_abs_lemma = 147 store_thm ("cfc_second_abs_lemma", 148 ``! f x. (! y. priv_cpsr_flags_constraints (f y) x ) = 149 priv_cpsr_flags_constraints_abs f x``, 150 RW_TAC (srw_ss()) [priv_cpsr_flags_constraints_def, 151 priv_cpsr_flags_constraints_abs_def] 152 THEN METIS_TAC []); 153 154val branch_to_ut_cfc_thm = 155 store_thm ("branch_to_ut_cfc_thm", 156 ``! s s' a x ee. 157 (((s.psrs (0, CPSR)).I = T) 158 /\ 159 ((s.psrs (0, CPSR)).J = F) 160 /\ 161 ((s.psrs (0, CPSR)).IT = 0w) /\ 162 ((s.psrs (0,CPSR)).E = ee) 163 ) ==> 164 (branch_to <|proc:=0|> x s = ValueState a s') ==> 165 (((s'.psrs (0, CPSR)).I = T) 166 /\ 167 ((s'.psrs (0, CPSR)).J = F) 168 /\ 169 ((s'.psrs (0, CPSR)).IT = 0w) /\ 170 ((s'.psrs (0,CPSR)).E = ee) 171 )``, 172 EVAL_TAC THEN 173 RW_TAC (srw_ss()) [] THEN 174 RW_TAC (srw_ss()) []); 175 176val constT_cfc_ut_thm = 177 store_thm ("constT_cfc_ut_thm", 178 ``! s s' a ii x. 179 (((s.psrs (ii.proc, CPSR)).I = T) 180 /\ 181 ((s.psrs (ii.proc, CPSR)).J = F) 182 /\ 183 ((s.psrs (ii.proc, CPSR)).IT = 0w)) ==> 184 (branch_to ii x s = ValueState a s') ==> 185 (((s'.psrs (ii.proc, CPSR)).I = T) 186 /\ 187 ((s'.psrs (ii.proc, CPSR)).J = F) 188 /\ 189 ((s'.psrs (ii.proc, CPSR)).IT = 0w))``, 190 EVAL_TAC THEN 191 RW_TAC (srw_ss()) [] THEN 192 RW_TAC (srw_ss()) []); 193 194val branch_cfc_thm = 195 store_thm("branch_cfc_thm", 196 `` !f sctlr x . priv_cpsr_flags_constraints f sctlr ==> 197 (priv_cpsr_flags_constraints (f ||| branch_to <|proc:=0|> x) sctlr)``, 198 (RW_TAC (srw_ss()) [parT_def, 199 seqT_def,priv_cpsr_flags_constraints_def]) 200 THEN 201 Cases_on `f s` THEN 202 Cases_on `branch_to <|proc:=0|> x b` THEN 203 Cases_on `access_violation b` THEN 204 Cases_on `access_violation b'` THEN 205 FULL_SIMP_TAC (srw_ss()) [] THEN 206 PAT_X_ASSUM ``! s s' a.(f s = ValueState a s') ==> Z`` (fn thm => ASSUME_TAC 207 (SPECL [``s:arm_state``,``b:arm_state``,``a':'a``] thm)) 208 THEN ASSUME_TAC 209 (SPECL [``b:arm_state``,``b':arm_state``, 210 ``a'':unit``,``x:bool[32]``, ``sctlr.EE:bool``] 211 branch_to_ut_cfc_thm) 212 THEN FIRST_PROVE [ 213 RES_TAC 214 THEN FULL_SIMP_TAC (srw_ss()) [] 215 THEN RW_TAC (srw_ss()) [] , 216 (UNDISCH_ALL_TAC 217 THEN EVAL_TAC 218 THEN RW_TAC (srw_ss()) [])] 219 ); 220 221val constT_cfc_thm = 222 store_thm("constT_cfc_thm", 223 `` !f ee . priv_cpsr_flags_constraints f ee ==> 224 (priv_cpsr_flags_constraints (f >>= (��(u1:unit,u2:unit,u3:unit,u4:unit). constT ()))) ee ``, 225 (RW_TAC (srw_ss()) [seqT_def,priv_cpsr_flags_constraints_def, 226 priv_cpsr_flags_constraints_abs_def,constT_def]) 227 THEN Cases_on `f s` 228 THEN Cases_on `access_violation b` 229 THEN Cases_on `access_violation b'` 230 THEN FULL_SIMP_TAC (srw_ss()) [] 231 THEN PAT_X_ASSUM ``! s s' a.(f s = ValueState a s') ==> Z`` 232 (fn thm => ASSUME_TAC 233 (SPECL [``s:arm_state``,``b:arm_state``, 234 ``a:(unit#unit#unit#unit)``] thm)) 235 THEN (UNDISCH_ALL_TAC 236 THEN EVAL_TAC 237 THEN RW_TAC (srw_ss()) [])); 238 239val joint_point_cfc_thm = 240 store_thm("joint_point_cfc_thm", 241 ``!H sctlr. (priv_cpsr_flags_constraints H sctlr) ==> 242 (priv_cpsr_flags_constraints_abs ((\(pc,ExcVectorBase,cpsr,scr,sctlr). H ):(word32 # word32 # ARMpsr # CP15scr # CP15sctlr -> unit M)) sctlr)``, 243 UNDISCH_ALL_TAC THEN 244 EVAL_TAC THEN 245 RW_TAC (srw_ss()) [priv_cpsr_flags_constraints_def,priv_cpsr_flags_constraints_abs_def]THEN 246 (PAT_X_ASSUM ``! s s' a. X`` (fn thm => (ASSUME_TAC (SPECL [``s:'a``,``s':arm_state``,``a:'b``] thm)))) THEN 247 FULL_SIMP_TAC (srw_ss()) [priv_cpsr_flags_constraints_def,priv_cpsr_flags_constraints_abs_def] THEN 248 RW_TAC (srw_ss()) [priv_cpsr_flags_constraints_def,priv_cpsr_flags_constraints_abs_def]); 249 250val base_thms = [priv_cpsr_flags_constraints_def, 251 seqT_priv_cpsr_flags_constraints_thm, 252 parT_priv_cpsr_flags_constraints_thm, 253 cfc_first_abs_lemma, 254 cfc_second_abs_lemma, 255 constT_cfc_thm 256 ]; 257 258 259fun prove_base_cfc base_cfc bv = 260 261 let val (thm1,_) = 262 ARM_prover_extLib.prove_const base_cfc 263 [define_cfc_goal,define_cfc_goal_abs] 264 [``sctlr:CP15sctlr``] 265 ``0w:bool[5]`` 266 "_cfc_thm" base_thms 267 ; 268 in 269 MP (SPECL [base_cfc, ``(sctlr:CP15sctlr)``, ``(ExcVectorBase + ^bv:bool[32])``] 270 (INST_TYPE[alpha |-> ``:(unit)``] branch_cfc_thm )) thm1 271 end 272 273 274 275val undef_read_write_cpsr_cfc_thm = 276 save_thm ("undef_read_write_cpsr_cfc_thm" , 277 let 278 val base_cfc = ``(read_cpsr <|proc:=0|> >>= 279 (��cpsr. 280 write_cpsr <|proc:=0|> 281 (cpsr with 282 <|I := T; IT := 0w; J := F; T := sctlr.TE; 283 E := sctlr.EE|>)) 284 )`` 285 286 in 287 prove_base_cfc base_cfc ``4w:bool[32]`` 288 end 289 ); 290 291val svc_read_write_cpsr_cfc_thm = 292 save_thm ("svc_read_write_cpsr_cfc_thm" , 293 let 294 val base_cfc = ``(read_cpsr <|proc:=0|> >>= 295 (��cpsr. 296 write_cpsr <|proc:=0|> 297 (cpsr with 298 <|I := T; IT := 0w; J := F; T := sctlr.TE; 299 E := sctlr.EE|>)) 300 )`` 301 302 in 303 prove_base_cfc base_cfc ``8w:bool[32]`` 304 end 305 ); 306 307val data_abt_read_write_cpsr_cfc_thm = 308 save_thm ("data_abt_read_write_cpsr_cfc_thm" , 309 let 310 val base_cfc = 311 ``(read_cpsr <|proc:=0|> >>= 312 (��cpsr. 313 write_cpsr <|proc:=0|> 314 (cpsr with 315 <|I := T; 316 A := 317 ((��have_security_exta ��� ��scr.NS ��� scr.AW) ��� 318 cpsr.A); IT := 0w; J := F; T := sctlr.TE; 319 E := sctlr.EE|>)))`` 320 in 321 prove_base_cfc base_cfc ``16w:bool[32]`` 322 end 323 ); 324 325val prefetch_abt_read_write_cpsr_cfc_thm = 326 save_thm ("prefetch_abt_read_write_cpsr_cfc_thm" , 327 let 328 val base_cfc = 329 ``(read_cpsr <|proc:=0|> >>= 330 (��cpsr. 331 write_cpsr <|proc:=0|> 332 (cpsr with 333 <|I := T; 334 A := 335 ((��have_security_exta ��� ��scr.NS ��� scr.AW) ��� 336 cpsr.A); IT := 0w; J := F; T := sctlr.TE; 337 E := sctlr.EE|>)))`` 338 in 339 prove_base_cfc base_cfc ``12w:bool[32]`` 340 end 341 ); 342 343 344val irq_read_write_cpsr_cfc_thm = 345 save_thm ("irq_read_write_cpsr_cfc_thm" , 346 let 347 val base_cfc = 348 ``(read_cpsr <|proc:=0|> >>= 349 (��cpsr. 350 write_cpsr <|proc:=0|> 351 (cpsr with 352 <|I := T; 353 A := 354 ((��have_security_exta ��� ��scr.NS ��� scr.AW) ��� 355 cpsr.A); IT := 0w; J := F; T := sctlr.TE; 356 E := sctlr.EE|>)))`` 357 in 358 prove_base_cfc base_cfc ``24w:bool[32]`` 359 end 360 ); 361 362val fiq_read_write_cpsr_cfc_thm = 363 save_thm ("fiq_read_write_cpsr_cfc_thm" , 364 let 365 val base_cfc = 366 ``(read_cpsr <|proc:=0|> >>= 367 (��cpsr. 368 write_cpsr <|proc:=0|> 369 (cpsr with 370 <|I := T; 371 F := 372 ((��have_security_exta ��� ��scr.NS ��� scr.AW) ��� 373 cpsr.F); 374 A := 375 ((��have_security_exta ��� ��scr.NS ��� scr.AW) ��� 376 cpsr.A); IT := 0w; J := F; T := sctlr.TE; 377 E := sctlr.EE|>)))`` 378 in 379 prove_base_cfc base_cfc ``4w:bool[32]`` 380 end 381 ); 382 383val const_comp_seqT_priv_cpsr_flags_constraints_thm = 384 store_thm( 385 "const_comp_seqT_priv_cpsr_flags_constraints_thm", 386 ``! f g s s' a x. 387 (const_comp f) ==> 388 ��access_violation s' ==> 389 priv_cpsr_flags_constraints_abs g x ==> 390 ((f>>=g) s = ValueState a s') ==> 391 ((((s'.psrs (0,CPSR)).I ��� T) ��� ((s'.psrs (0,CPSR)).J ��� F) ��� 392 ((s'.psrs (0,CPSR)).IT = 0w) ��� ((s'.psrs (0,CPSR)).E ��� x.EE)))``, 393 RW_TAC (srw_ss()) [const_comp_def,priv_cpsr_flags_constraints_def, 394 priv_cpsr_flags_constraints_abs_def] 395 THEN FULL_SIMP_TAC (srw_ss()) [] 396 THEN Cases_on ` f s` 397 THEN IMP_RES_TAC seqT_access_violation_thm 398 THEN FULL_SIMP_TAC (srw_ss()) [seqT_def] 399 THEN PAT_X_ASSUM ``���s s' a c. X`` (fn thm => ASSUME_TAC ( 400 SPECL [``b:arm_state``,``s':arm_state``, 401 ``a:'b``,``a':'a``] thm )) 402 THEN RES_TAC 403 THEN FULL_SIMP_TAC (srw_ss()) [] 404 ); 405 406 407fun prove_take_exception_cfc_thm 408 read_write_cpsr_cfc_thm 409 body 410 sl_elm 411 sl_elm2 412 spec_list 413 spec_list2 414 te_def 415 const_comp_rp_thm 416 fixed_sctrl_thm 417 fixed_sctrl_thm2 ltype 418 = 419 let 420 val thms1 = [priv_cpsr_flags_constraints_def, 421 seqT_priv_cpsr_flags_constraints_thm, 422 parT_priv_cpsr_flags_constraints_thm, 423 cfc_first_abs_lemma, 424 cfc_second_abs_lemma, 425 read_write_cpsr_cfc_thm, 426 constT_cfc_thm 427 ]; 428 429 val (l,r,rbody)= ARM_prover_extLib.decompose_term body; 430 val (rbody_thm,_) = ARM_prover_extLib.prove_const rbody 431 [define_cfc_goal,define_cfc_goal_abs] 432 [``sctlr:CP15sctlr``] 433 ``(12w:bool[5])`` "_cfc_thm" thms1; 434 435 val (_,sr) = dest_eq ( concl (SIMP_RULE (srw_ss()) [] 436 (SPECL [``s:arm_state``,r] 437 (INST_TYPE [alpha |-> ``:unit``] 438 fixed_sctrl_thm)))); 439 val (_,simpr,_) = ARM_prover_extLib.decompose_term sr; 440 val (rabs,rbody) = pairLib.dest_pabs r; 441 val unbeta_thm= (PairRules.UNPBETA_CONV rabs rbody); 442 val unbeta_a = mk_comb (r, rabs) 443 val snd = get_type_inst (type_of(rbody) , false) 444 val rbody_type = get_type_inst (snd, true); 445 446 val thm4 = prove( 447 ``(priv_cpsr_flags_constraints 448 ^rbody (sctlr:CP15sctlr))= 449 (priv_cpsr_flags_constraints ^unbeta_a 450 (sctlr:CP15sctlr))``, 451 (ASSUME_TAC (SPECL [rbody, 452 ``^unbeta_a``, 453 ``sctlr:CP15sctlr``] 454 (INST_TYPE 455 [beta |-> rbody_type, 456 alpha |-> ``:arm_state``] 457 (cfc_first_abs_lemma)))) 458 THEN ASSUME_TAC unbeta_thm 459 THEN RES_TAC); 460 val thm5 = SIMP_RULE (bool_ss) [thm4] rbody_thm; 461 in 462 RW_TAC (srw_ss()) [te_def] 463 THEN ASSUME_TAC (SPECL [``s:arm_state``,r] 464 (INST_TYPE [alpha |-> ``:unit``] 465 fixed_sctrl_thm)) 466 THEN FULL_SIMP_TAC (srw_ss()) [] 467 THEN POP_ASSUM (fn thm => THROW_AWAY_TAC (concl thm)) 468 THEN ASSUME_TAC const_comp_rp_thm 469 THEN RW_TAC (srw_ss()) [priv_cpsr_flags_constraints_def, 470 priv_cpsr_flags_constraints_abs_def] 471 THEN NTAC 4 472 ( FULL_SIMP_TAC (srw_ss()) [const_comp_def] 473 THEN Cases_on [QUOTE ("("^(term_to_string l) ^ ") s")] 474 THENL 475 [ 476 IMP_RES_TAC seqT_access_violation_thm 477 THEN RES_TAC 478 THEN RW_TAC (srw_ss()) [] 479 THEN IMP_RES_TAC hlp_seqT_thm 480 THEN PAT_X_ASSUM ``X a' b= ValueState a s'`` 481 (fn thm => ASSUME_TAC (PairRules.PBETA_RULE thm)) 482 THEN ASSUME_TAC 483 ( SPECL spec_list 484 (GEN_ALL (SIMP_RULE (bool_ss) 485 [priv_cpsr_flags_constraints_def] thm5))) 486 THEN PAT_X_ASSUM ``X ==> Y`` 487 (fn thm => ASSUME_TAC (PairRules.PBETA_RULE thm)) 488 THEN ASSUME_TAC (SPECL spec_list2 fixed_sctrl_thm2) 489 THEN RES_TAC 490 THEN FULL_SIMP_TAC (srw_ss()) [], 491 492 IMP_RES_TAC (SPEC simpr 493 (INST_TYPE [beta |-> ``:unit``, 494 alpha |-> ltype] 495 hlp_errorT_thm)) 496 THEN PAT_X_ASSUM ``! (s''':arm_state) . X `` 497 (fn thm => ASSUME_TAC (SPEC ``s:arm_state`` thm)) 498 THEN RW_TAC (srw_ss()) [] 499 THEN FULL_SIMP_TAC (srw_ss()) [] ]) 500 end 501 502 503 504val take_undef_instr_exception_cfc_thm = 505 store_thm ("take_undef_instr_exception_cfc_thm", 506 ``!s a s'. 507 (��access_violation s')==> 508 (take_undef_instr_exception <|proc:=0|> s = ValueState a s') ==> 509 (((s'.psrs (0,CPSR)).I ��� T) 510 ���((s'.psrs (0,CPSR)).J ��� F) ��� 511 ((s'.psrs (0,CPSR)).IT = 0w) ��� 512 ((s'.psrs (0,CPSR)).E ��� s.coprocessors.state.cp15.SCTLR.EE))``, 513 let 514 val athm = SIMP_CONV (bool_ss) [take_undef_instr_exception_def] 515 ``take_undef_instr_exception <|proc:=0|> ``; 516 val (_, body) = (dest_eq (concl athm)) 517 val sl_elm2 = ``(a':(word32 # word32 # ARMpsr # CP15scr # CP15sctlr))``; 518 val sl_elm = ``(a:(word32 # word32 # ARMpsr # CP15scr # CP15sctlr))``; 519 val const_comp_rp_thm = 520 const_comp_take_undef_svc_exception_rp_thm; 521 val fixed_sctrl_thm2 = fixed_sctrl_undef_svc_thm2; 522 val fixed_sctrl_thm = fixed_sctrl_undef_svc_thm; 523 val spec_list = (mk_spec_list sl_elm2) @ 524 [``b:arm_state``, 525 ``s':arm_state``, 526 ``a:unit``]; 527 val spec_list2 = [``b:arm_state``]@ ( (mk_spec_list2 sl_elm2)); 528 val ltype = ``:(word32 # word32 # ARMpsr # CP15scr # CP15sctlr)`` ; 529 (* val read_write_cpsr_cfc_thm = undef_read_write_cpsr_cfc_thm; *) 530 in 531 prove_take_exception_cfc_thm 532 undef_read_write_cpsr_cfc_thm 533 body sl_elm sl_elm2 534 spec_list spec_list2 535 take_undef_instr_exception_def 536 const_comp_rp_thm fixed_sctrl_thm 537 fixed_sctrl_thm2 ltype 538 end 539); 540 541val take_data_abort_exception_cfc_thm = 542 store_thm ("take_data_abort_exception_cfc_thm", 543 ``!s a s'. 544 (��access_violation s')==> 545 (take_data_abort_exception <|proc:=0|> s = ValueState a s') ==> 546 (((s'.psrs (0,CPSR)).I ��� T) 547 ���((s'.psrs (0,CPSR)).J ��� F) ��� 548 ((s'.psrs (0,CPSR)).IT = 0w) ��� 549 ((s'.psrs (0,CPSR)).E ��� s.coprocessors.state.cp15.SCTLR.EE))``, 550 let 551 val athm = SIMP_CONV (bool_ss) [take_data_abort_exception_def] 552 ``take_data_abort_exception <|proc:=0|> ``; 553 val (_, body) = (dest_eq (concl athm)); 554 val sl_elm2 = ``(a':(word32 # word32 # bool # ARMpsr # CP15scr # CP15sctlr))``; 555 val sl_elm = ``(a:(word32 # word32 # bool # ARMpsr # CP15scr # CP15sctlr))``; 556 val read_write_cpsr_cfc_thm = data_abt_read_write_cpsr_cfc_thm; 557 val const_comp_rp_thm = const_comp_take_abort_irq_exception_rp_thm 558 val fixed_sctrl_thm2 = fixed_sctrl_abt_irq_thm2; 559 val fixed_sctrl_thm1 = fixed_sctrl_abt_irq_thm; 560 val spec_list = (mk_spec_list3 sl_elm2) @ 561 [``b:arm_state``, 562 ``s':arm_state``, 563 ``a:unit``]; 564 val spec_list2 = [``b:arm_state``]@ ( (mk_spec_list4 sl_elm2)); 565 val ltype = ``:(word32 # word32 # bool # ARMpsr # CP15scr # CP15sctlr)`` ; 566 in 567 prove_take_exception_cfc_thm 568 data_abt_read_write_cpsr_cfc_thm 569 body 570 sl_elm 571 sl_elm2 572 spec_list 573 spec_list2 574 take_data_abort_exception_def 575 const_comp_rp_thm 576 fixed_sctrl_thm1 577 fixed_sctrl_thm2 ltype 578 end 579); 580 581 582val take_prefetch_abort_exception_cfc_thm = 583 store_thm ("take_prefetch_abort_exception_cfc_thm", 584 ``!s a s'. 585 (��access_violation s')==> 586 (take_prefetch_abort_exception <|proc:=0|> s = ValueState a s') ==> 587 (((s'.psrs (0,CPSR)).I ��� T) 588 ���((s'.psrs (0,CPSR)).J ��� F) ��� 589 ((s'.psrs (0,CPSR)).IT = 0w) ��� 590 ((s'.psrs (0,CPSR)).E ��� s.coprocessors.state.cp15.SCTLR.EE))``, 591 let 592 val athm = SIMP_CONV (bool_ss) [take_prefetch_abort_exception_def] 593 ``take_prefetch_abort_exception <|proc:=0|> ``; 594 val (_, body) = (dest_eq (concl athm)); 595 val sl_elm2 = ``(a':(word32 # word32 # bool # ARMpsr # CP15scr # CP15sctlr))``; 596 val sl_elm = ``(a:(word32 # word32 # bool # ARMpsr # CP15scr # CP15sctlr))``; 597 val read_write_cpsr_cfc_thm = prefetch_abt_read_write_cpsr_cfc_thm; 598 val const_comp_rp_thm = const_comp_take_abort_irq_exception_rp_thm 599 val fixed_sctrl_thm2 = fixed_sctrl_abt_irq_thm2; 600 val fixed_sctrl_thm1 = fixed_sctrl_abt_irq_thm; 601 val spec_list = (mk_spec_list3 sl_elm2) @ 602 [``b:arm_state``, 603 ``s':arm_state``, 604 ``a:unit``]; 605 val spec_list2 = [``b:arm_state``]@ ( (mk_spec_list4 sl_elm2)); 606 val ltype = ``:(word32 # word32 # bool # ARMpsr # CP15scr # CP15sctlr)`` ; 607 in 608 prove_take_exception_cfc_thm 609 prefetch_abt_read_write_cpsr_cfc_thm 610 body 611 sl_elm 612 sl_elm2 613 spec_list 614 spec_list2 615 take_prefetch_abort_exception_def 616 const_comp_rp_thm 617 fixed_sctrl_thm1 618 fixed_sctrl_thm2 ltype 619 end 620); 621 622 623 624val take_irq_exception_cfc_thm = 625 store_thm ("take_irq_exception_cfc_thm", 626 ``!s a s'. 627 (��access_violation s')==> 628 (take_irq_exception <|proc:=0|> s = ValueState a s') ==> 629 (((s'.psrs (0,CPSR)).I ��� T) 630 ���((s'.psrs (0,CPSR)).J ��� F) ��� 631 ((s'.psrs (0,CPSR)).IT = 0w) ��� 632 ((s'.psrs (0,CPSR)).E ��� s.coprocessors.state.cp15.SCTLR.EE))``, 633 let 634 val athm = SIMP_CONV (bool_ss) [take_irq_exception_def] 635 ``take_irq_exception <|proc:=0|> ``; 636 val (_, body) = (dest_eq (concl athm)); 637 val sl_elm2 = ``(a':(word32 # word32 # bool # ARMpsr # CP15scr # CP15sctlr))``; 638 val sl_elm = ``(a:(word32 # word32 # bool # ARMpsr # CP15scr # CP15sctlr))``; 639 val read_write_cpsr_cfc_thm = irq_read_write_cpsr_cfc_thm; 640 val const_comp_rp_thm = const_comp_take_abort_irq_exception_rp_thm 641 val fixed_sctrl_thm2 = fixed_sctrl_abt_irq_thm2; 642 val fixed_sctrl_thm1 = fixed_sctrl_abt_irq_thm; 643 val spec_list = (mk_spec_list3 sl_elm2) @ 644 [``b:arm_state``, 645 ``s':arm_state``, 646 ``a:unit``]; 647 val spec_list2 = [``b:arm_state``]@ ( (mk_spec_list4 sl_elm2)); 648 val ltype = ``:(word32 # word32 # bool # ARMpsr # CP15scr # CP15sctlr)`` ; 649 in 650 prove_take_exception_cfc_thm 651 irq_read_write_cpsr_cfc_thm 652 body 653 sl_elm 654 sl_elm2 655 spec_list 656 spec_list2 657 take_irq_exception_def 658 const_comp_rp_thm 659 fixed_sctrl_thm1 660 fixed_sctrl_thm2 ltype 661 end 662); 663 664 665(* TO DO SVC *) 666 667val take_svc_exception_cfc_thm = 668 store_thm ("take_svc_exception_cfc_thm", 669 let 670 val athm = SIMP_CONV (bool_ss) [take_svc_exception_def] 671 ``take_svc_exception <|proc:=0|> ``; 672 val (_, body) = (dest_eq (concl athm)) 673 val (_,_,a) = ARM_prover_extLib.decompose_term body; 674 in 675 ``!s a s'. 676 (��access_violation s')==> 677 (^a s = ValueState a s') ==> 678 (((s'.psrs (0,CPSR)).I ��� T) 679 ���((s'.psrs (0,CPSR)).J ��� F) ��� 680 ((s'.psrs (0,CPSR)).IT = 0w) ��� 681 ((s'.psrs (0,CPSR)).E ��� s.coprocessors.state.cp15.SCTLR.EE))`` 682 end, 683 let 684 val athm = SIMP_CONV (bool_ss) [take_svc_exception_def] 685 ``take_svc_exception <|proc:=0|> `` 686 val (_, a) = (dest_eq (concl athm)) 687 val (_,_,body) = ARM_prover_extLib.decompose_term a 688 689 val sl_elm2 = ``(a':(word32 # word32 # ARMpsr # CP15scr # CP15sctlr))`` 690 val sl_elm = ``(a:(word32 # word32 # ARMpsr # CP15scr # CP15sctlr))`` 691 val const_comp_rp_thm = 692 const_comp_take_undef_svc_exception_rp_thm 693 val fixed_sctrl_thm2 = fixed_sctrl_undef_svc_thm2 694 val fixed_sctrl_thm = fixed_sctrl_undef_svc_thm 695 val spec_list = (mk_spec_list sl_elm2) @ 696 [``b:arm_state``, 697 ``s':arm_state``, 698 ``a:unit``]; 699 val spec_list2 = [``b:arm_state``]@ ( (mk_spec_list2 sl_elm2)) 700 val ltype = ``:(word32 # word32 # ARMpsr # CP15scr # CP15sctlr)`` 701 in 702 prove_take_exception_cfc_thm 703 svc_read_write_cpsr_cfc_thm 704 body sl_elm sl_elm2 705 spec_list spec_list2 706 take_svc_exception_def 707 const_comp_rp_thm fixed_sctrl_thm 708 fixed_sctrl_thm2 ltype 709 end 710 ); 711 712 713 714 715 716 717 718 719 720 721 722 723 724 725 726(**************************************************************) 727(* SET PROGRAM TO AN ADDRESS IN VECTOR TABLE *) 728(**************************************************************) 729val set_pc_to_def = 730 Define `set_pc_to f (m:bool[5]) vt = 731 !s1 s2 c . 732 (f s1 = ValueState c s2) ==> 733 (��access_violation s2) ==> 734 ((s2.registers (0, RName_PC) = HD(vector_table_address vt m)) \/ 735 (s2.registers (0, RName_PC) = HD (TL(vector_table_address vt m)))) `; 736 737val set_pc_to_abs_def = 738 Define `set_pc_to_abs f (m:bool[5]) vt = 739 !s1 s2 c a . 740 (f a s1 = ValueState c s2) ==> 741 (��access_violation s2) ==> 742 ((s2.registers (0, RName_PC) = HD(vector_table_address vt m)) \/ 743 (s2.registers (0, RName_PC) = HD (TL(vector_table_address vt m)))) `; 744 745val branch_to_spc_thm = 746 store_thm("branch_to_spc_thm", 747 ``! m adr . (adr = HD(vector_table_address ExcVectorBase m)) 748 \/ (adr = HD(TL(vector_table_address ExcVectorBase m))) ==> 749 set_pc_to (branch_to <|proc := 0|> adr) m ExcVectorBase``, 750 EVAL_TAC THEN 751 FULL_SIMP_TAC (srw_ss()) [] THEN 752 RW_TAC (srw_ss()) [] THEN 753 EVAL_TAC THEN 754 FULL_SIMP_TAC (srw_ss()) []); 755 756val seqT_set_pc_to_thm = 757 store_thm("seqT_set_pc_to_thm", 758 `` !g f m vt. set_pc_to_abs g m vt ==> 759 set_pc_to (f >>= g) m vt``, 760 (RW_TAC (srw_ss()) [seqT_def,set_pc_to_abs_def, 761 set_pc_to_def]) 762 THEN Cases_on `f s1` 763 THEN FULL_SIMP_TAC (srw_ss()) [] 764 THEN Cases_on `access_violation b` 765 THEN (RW_TAC (srw_ss()) []) 766 THEN FULL_SIMP_TAC (srw_ss()) [] 767 THEN RW_TAC (srw_ss()) [] 768 THEN FULL_SIMP_TAC (srw_ss()) [] 769 THEN FULL_SIMP_TAC (srw_ss()) [] 770 THEN PAT_X_ASSUM ``! s1 s2 c.t`` 771 (fn thm => ASSUME_TAC 772 (SPECL [``b:arm_state``,``s2:arm_state``,``c:('b)``] thm)) 773 THEN RES_TAC 774 THEN FULL_SIMP_TAC (srw_ss()) []); 775 776val parT_set_pc_to_thm = 777 store_thm("parT_set_pc_to_thm", 778 `` !g f m vt. set_pc_to g m vt ==> 779 set_pc_to (f ||| g) m vt ``, 780 (RW_TAC (srw_ss()) [parT_def,seqT_def,set_pc_to_def]) 781 THEN Cases_on `f s1` 782 THEN Cases_on `g b` 783 THEN Cases_on `access_violation b` 784 THEN Cases_on `access_violation b'` 785 THEN FULL_SIMP_TAC (srw_ss()) [] 786 THEN RES_TAC 787 THEN UNDISCH_ALL_TAC 788 THEN EVAL_TAC 789 THEN (RW_TAC (srw_ss()) [])); 790 791val pc_first_abs_lemma = 792 store_thm ("pc_first_abs_lemma", 793 ``!f g m vt . (f=g) ==> ((set_pc_to f m vt) = 794 (set_pc_to g m vt))``, 795 RW_TAC (srw_ss()) []); 796 797val pc_second_abs_lemma = 798 store_thm ("pc_second_abs_lemma", 799 ``! f m vt. (! y. set_pc_to (f y) m vt) = 800 set_pc_to_abs f m vt``, 801 RW_TAC (srw_ss()) [set_pc_to_def,set_pc_to_abs_def] 802 THEN METIS_TAC []); 803 804val vector_table_adr_thm = 805 store_thm( 806 "vector_table_adr_thm", 807 ``!vt. 808 (HD (vector_table_address vt (19w:bool[5])) = (vt + 8w:bool[32] )) 809 /\ 810 (HD (vector_table_address vt (23w:bool[5])) = (vt + 16w:bool[32] )) 811 /\ 812 (HD (TL(vector_table_address vt (23w:bool[5]))) = (vt + 12w:bool[32] )) 813 /\ 814 (HD (vector_table_address vt (27w:bool[5])) = (vt + 4w:bool[32]))``, 815 EVAL_TAC 816 THEN RW_TAC (srw_ss()) []); 817 818 819val constT_spc_thm = 820 store_thm("constT_spc_thm", 821 `` !f m vt. set_pc_to f m vt ==> 822 (set_pc_to (f >>= (��(u1:unit,u2:unit,u3:unit,u4:unit). constT ())) m vt)``, 823 (RW_TAC (srw_ss()) 824 [seqT_def,set_pc_to_def,constT_def]) 825 THEN 826 Cases_on `f s1` THEN 827 Cases_on `access_violation b` THEN 828 PAT_X_ASSUM ``! s1 s2 c. Z`` (fn thm => ASSUME_TAC (SPECL [``s1:arm_state``,``b:arm_state``,``a:(unit#unit#unit#unit)``] thm)) 829 THEN FULL_SIMP_TAC (srw_ss()) [] 830 THENL [RW_TAC (srw_ss()) [] THEN 831 RES_TAC, 832 UNDISCH_ALL_TAC 833 THEN EVAL_TAC 834 THEN RW_TAC (srw_ss()) []]); 835 836fun define_set_pc_goal a [expr,vt] = 837 set_goal([], `` 838 (set_pc_to ^a ^expr ^vt) ``); 839 840fun define_set_pc_goal_abs a [expr,vt] = 841 set_goal([], `` (set_pc_to_abs ^a ^expr ^vt) ``); 842 843fun get_action_body a thm = 844 let val (_,body) = (dest_eq o concl) (REWRITE_CONV [thm] 845 ``^a <|proc:=0|> ``) 846 in 847 body 848 end; 849 850 851val (_,take_undef_exception_body) = (dest_eq o concl) (REWRITE_CONV [take_undef_instr_exception_def] 852 ``take_undef_instr_exception <|proc:=0|> ``); 853 854fun get_joint_write_body_spc_thm body mode vb = 855 let 856 val set_pc_thms = [set_pc_to_def, 857 seqT_set_pc_to_thm, 858 parT_set_pc_to_thm, 859 pc_first_abs_lemma, 860 pc_second_abs_lemma, 861 REWRITE_RULE [vector_table_address_def] branch_to_spc_thm, 862 constT_spc_thm 863 ]; 864 val postfix = "_spc_thm" 865 val (l,r,rb) = (ARM_prover_extLib.decompose_term body); 866 val (l1,r1,rb1) = ARM_prover_extLib.decompose_term rb; 867 val (wp1,r2,rb1) = ARM_prover_extLib.decompose_term rb1; 868 869 val (wp1_thm,_) = ARM_prover_extLib.prove_const wp1 870 [define_set_pc_goal,define_set_pc_goal_abs] 871 [mode,``(ExcVectorBase:bool[32])``] 872 vb 873 "_spc_thm" 874 set_pc_thms; 875 876 val writing_part_spc_thm = (MP (SPECL [wp1 , 877 mode, 878 ``(ExcVectorBase:bool[32])``] 879 constT_spc_thm) wp1_thm); 880 val writing_part_abs_spc_thm = 881 store_thm ("writing_part_spc_thm" , 882 ``set_pc_to_abs ^r1 ^mode ExcVectorBase``, 883 MP_TAC writing_part_spc_thm 884 THEN RW_TAC (srw_ss()) [set_pc_to_def,set_pc_to_abs_def] 885 THEN PAT_X_ASSUM ``! s1 s2. X`` (fn thm => 886 ASSUME_TAC (SPECL [``s1:arm_state``,``s2:arm_state``] thm)) 887 THEN PAT_X_ASSUM ``X a s1 = ValueState () s2`` 888 (fn thm => ASSUME_TAC (PairRules.PBETA_RULE thm)) 889 THEN RES_TAC 890 THEN RW_TAC (srw_ss()) [] 891 ); 892 893 val thm = MP (SPECL [r1,l1, 894 mode, 895 ``(ExcVectorBase:bool[32])``] 896 (INST_TYPE [alpha |-> ``:unit#unit``, 897 beta |-> ``:unit`` 898 ] 899 seqT_set_pc_to_thm)) writing_part_abs_spc_thm; 900 in 901 thm 902 end; 903 904val joint_write_body_data_abort_spc_thm = 905 save_thm ("joint_write_body_data_abort_spc_thm", 906 let val body = 907 get_action_body ``take_data_abort_exception`` 908 take_data_abort_exception_def 909 in 910 get_joint_write_body_spc_thm body ``23w:bool[5]`` ``16w:bool[5]`` 911 end 912 ); 913 914 915val joint_write_body_irq_spc_thm = 916 save_thm ("joint_write_body_irq_spc_thm", 917 let val body = 918 get_action_body ``take_irq_exception`` 919 take_irq_exception_def 920 in 921 get_joint_write_body_spc_thm body ``18w:bool[5]`` ``24w:bool[5]`` 922 end 923 ); 924 925val joint_write_body_svc_spc_thm = 926 save_thm ("joint_write_body_svc_spc_thm", 927 let val a = 928 get_action_body ``take_svc_exception`` 929 take_svc_exception_def 930 val (l,r,body)= ARM_prover_extLib.decompose_term a 931 in 932 get_joint_write_body_spc_thm body ``19w:bool[5]`` ``8w:bool[5]`` 933 end 934 ); 935 936val joint_write_body_undef_instr_spc_thm = 937 save_thm ("joint_write_body_undef_instr_spc_thm", 938 let val body = 939 get_action_body ``take_undef_instr_exception`` 940 take_undef_instr_exception_def 941 in 942 get_joint_write_body_spc_thm body ``27w:bool[5]`` ``4w:bool[5]`` 943 end 944 ); 945 946val joint_write_body_prefetch_abort_spc_thm = 947 save_thm ("joint_write_body_prefetch_abort_spc_thm", 948 let 949 val body = 950 get_action_body ``take_prefetch_abort_exception`` 951 take_prefetch_abort_exception_def 952 in 953 get_joint_write_body_spc_thm body ``23w:bool[5]`` ``12w:bool[5]`` 954 end 955 ); 956 957fun prove_take_exception_spc 958 body def_thm sl_elm 959 const_rp_thm fixed_vb_rp_thm2 960 fixed_vb_rp_thm1 joint_write_body_spc_thm 961 l_type spec_list1 spec_list2 = 962 let 963 val (l,r,rb) = ARM_prover_extLib.decompose_term body; 964 in 965 FULL_SIMP_TAC (srw_ss()) 966 [def_thm] 967 THEN (REPEAT DISCH_TAC) 968 THEN ASSUME_SPECL_INST_TAC 969 [``s:arm_state``,r] 970 [alpha |-> ``:unit``] 971 fixed_vb_rp_thm2 972 THEN FULL_SIMP_TAC (srw_ss()) [] 973 THEN WEAKEN_TAC (is_imp) 974 THEN ASSUME_TAC const_rp_thm 975 THEN RW_TAC (srw_ss()) [] 976 THEN FULL_SIMP_TAC (srw_ss()) [const_comp_def] 977 THEN Cases_on [QUOTE ("("^(term_to_string l) ^ ") s")] 978 979 THENL 980 [ 981 RES_TAC 982 THEN 983 RW_TAC (srw_ss()) [] 984 THEN IMP_RES_TAC hlp_seqT_thm 985 THEN PAT_X_ASSUM ``X a' b= ValueState a s'`` 986 (fn thm => ASSUME_TAC (PairRules.PBETA_RULE thm)) 987 THEN IMP_RES_TAC (SPECL (spec_list2@[``b:arm_state``]) 988 fixed_vb_rp_thm1) 989 THEN PAT_X_ASSUM ``!a.X`` (fn thm => ASSUME_TAC (SPEC sl_elm thm)) 990 THEN ASSUME_SPECL_GEN_REWRITE_TAC 991 (spec_list1@ [``b:arm_state``, 992 ``s':arm_state``, 993 ``():unit``], 994 joint_write_body_spc_thm, [set_pc_to_def]) 995 THEN FULL_SIMP_TAC (srw_ss()) [] 996 THEN RES_TAC 997 THEN RW_TAC (srw_ss()) [] 998 , 999 IMP_RES_TAC (SPEC r (INST_TYPE [beta |-> ``:unit``, 1000 alpha |-> l_type ] 1001 hlp_errorT_thm)) 1002 THEN PAT_X_ASSUM ``! (s''':arm_state). X `` 1003 (fn thm => ASSUME_TAC (SPEC ``s':arm_state``thm)) 1004 THEN RW_TAC (srw_ss()) [] 1005 THEN FULL_SIMP_TAC (srw_ss()) [] ] 1006 end; 1007 1008 1009val take_data_abort_exception_spc_thm = 1010 store_thm ("take_data_abort_exception_spc_thm", 1011 ``!s a s'. 1012 (��access_violation s')==> 1013 (��access_violation s)==> 1014 (take_data_abort_exception <|proc:=0|> s = 1015 ValueState a s') ==> 1016 ((s'.registers (0,RName_PC) = 1017 (HD (vector_table_address 1018 (get_base_vector_table s) 23w))) 1019 \/ 1020 (s'.registers (0,RName_PC) = 1021 (HD (TL (vector_table_address 1022 (get_base_vector_table s) 23w))))) 1023 ``, 1024 let 1025 val body = 1026 get_action_body ``take_data_abort_exception`` 1027 take_data_abort_exception_def; 1028 val sl_elm = ``(a:(word32 # word32 # bool # ARMpsr # CP15scr # CP15sctlr))``; 1029 val def_thm = take_data_abort_exception_def; 1030 val const_rp_thm = const_comp_take_abort_irq_exception_rp_thm; 1031 val fixed_vb_rp_thm2 = fixed_VectorBase_abort_irq_exception_thm2; 1032 val fixed_vb_rp_thm1 = fixed_VectorBase_abort_irq_exception_thm1; 1033 val joint_write_body_spc_thm = joint_write_body_data_abort_spc_thm; 1034 1035 val l_type = ``:(word32 # word32 # bool # ARMpsr # CP15scr # CP15sctlr)``; 1036 val spec_list1 = mk_spec_list3(sl_elm); 1037 val spec_list2 = mk_spec_list4(sl_elm); 1038 in 1039 prove_take_exception_spc 1040 body def_thm sl_elm 1041 const_rp_thm fixed_vb_rp_thm2 1042 fixed_vb_rp_thm1 joint_write_body_spc_thm 1043 l_type spec_list1 spec_list2 1044 end 1045); 1046 1047val take_prefetch_abort_exception_spc_thm = 1048 store_thm ("take_prefetch_abort_exception_spc_thm", 1049 ``!s a s'. 1050 (��access_violation s')==> 1051 (��access_violation s)==> 1052 (take_prefetch_abort_exception <|proc:=0|> s = 1053 ValueState a s') ==> 1054 ((s'.registers (0,RName_PC) = 1055 HD (vector_table_address (get_base_vector_table s) 23w)) ��� 1056 (s'.registers (0,RName_PC) = 1057 HD (TL (vector_table_address (get_base_vector_table s) 23w)))) 1058 ``, 1059 let 1060 val body = 1061 get_action_body ``take_prefetch_abort_exception`` 1062 take_prefetch_abort_exception_def; 1063 val sl_elm = ``(a:(word32 # word32 # bool # ARMpsr # CP15scr # CP15sctlr))``; 1064 val def_thm = take_prefetch_abort_exception_def; 1065 val const_rp_thm = const_comp_take_abort_irq_exception_rp_thm; 1066 val fixed_vb_rp_thm2 = fixed_VectorBase_abort_irq_exception_thm2; 1067 val fixed_vb_rp_thm1 = fixed_VectorBase_abort_irq_exception_thm1; 1068 val joint_write_body_spc_thm = joint_write_body_prefetch_abort_spc_thm; 1069 1070 val l_type = ``:(word32 # word32 # bool # ARMpsr # CP15scr # CP15sctlr)``; 1071 val spec_list1 = mk_spec_list3(sl_elm); 1072 val spec_list2 = mk_spec_list4(sl_elm); 1073 in 1074 prove_take_exception_spc 1075 body def_thm sl_elm 1076 const_rp_thm fixed_vb_rp_thm2 1077 fixed_vb_rp_thm1 joint_write_body_spc_thm 1078 l_type spec_list1 spec_list2 1079 end 1080); 1081 1082 1083val take_undef_instr_exception_spc_thm = 1084 store_thm ("take_undef_instr_exception_spc_thm", 1085 ``!s a s'. 1086 (��access_violation s')==> 1087 (��access_violation s)==> 1088 (take_undef_instr_exception <|proc:=0|> s = 1089 ValueState a s') ==> 1090 ((s'.registers (0,RName_PC) = 1091 (HD (vector_table_address 1092 (get_base_vector_table s) 27w))) 1093 \/ 1094 (s'.registers (0,RName_PC) = 1095 (HD (TL (vector_table_address 1096 (get_base_vector_table s) 27w))))) 1097 ``, 1098 let 1099 val body = 1100 get_action_body ``take_undef_instr_exception`` 1101 take_undef_instr_exception_def; 1102 val sl_elm = ``(a:(word32 # word32 # ARMpsr # CP15scr # CP15sctlr))``; 1103 val const_rp_thm = const_comp_take_undef_svc_exception_rp_thm; 1104 val fixed_vb_rp_thm2 = fixed_VectorBase_undef_instr_exception_thm2; 1105 val fixed_vb_rp_thm1 = fixed_VectorBase_undef_instr_exception_thm1; 1106 val l_type = ``:(word32 # word32 # ARMpsr # CP15scr # CP15sctlr)``; 1107 val spec_list1 = mk_spec_list(sl_elm); 1108 val spec_list2 = mk_spec_list2(sl_elm); 1109 in 1110 prove_take_exception_spc 1111 body take_undef_instr_exception_def sl_elm 1112 const_rp_thm fixed_vb_rp_thm2 1113 fixed_vb_rp_thm1 joint_write_body_undef_instr_spc_thm 1114 l_type spec_list1 spec_list2 1115 end 1116 ); 1117 1118 1119val take_irq_exception_spc_thm = 1120 store_thm ("take_irq_exception_spc_thm", 1121 ``!s a s'. 1122 (��access_violation s')==> 1123 (��access_violation s)==> 1124 (take_irq_exception <|proc:=0|> s = 1125 ValueState a s') ==> 1126 ((s'.registers (0,RName_PC) = 1127 (HD (vector_table_address 1128 (get_base_vector_table s) 18w))) 1129 \/ 1130 (s'.registers (0,RName_PC) = 1131 (HD (TL (vector_table_address 1132 (get_base_vector_table s) 18w)))))``, 1133 let 1134 val body = 1135 get_action_body ``take_irq_exception`` 1136 take_irq_exception_def; 1137 val sl_elm = ``(a:(word32 # word32 # bool # ARMpsr # CP15scr # CP15sctlr))``; 1138 val const_rp_thm = const_comp_take_abort_irq_exception_rp_thm; 1139 val fixed_vb_rp_thm2 = fixed_VectorBase_abort_irq_exception_thm2; 1140 val fixed_vb_rp_thm1 = fixed_VectorBase_abort_irq_exception_thm1; 1141 val joint_write_body_spc_thm = joint_write_body_irq_spc_thm; 1142 1143 val l_type = ``:(word32 # word32 # bool # ARMpsr # CP15scr # CP15sctlr)``; 1144 val spec_list1 = mk_spec_list3(sl_elm); 1145 val spec_list2 = mk_spec_list4(sl_elm); 1146 1147 in 1148 prove_take_exception_spc 1149 body take_irq_exception_def sl_elm 1150 const_rp_thm fixed_vb_rp_thm2 1151 fixed_vb_rp_thm1 joint_write_body_irq_spc_thm 1152 l_type spec_list1 spec_list2 1153 end 1154 ); 1155 1156 1157val take_svc_exception_spc_thm = 1158 store_thm ("take_svc_exception_spc_thm", 1159 let 1160 val athm = SIMP_CONV (bool_ss) [take_svc_exception_def] 1161 ``take_svc_exception <|proc:=0|> `` 1162 val (_, a) = (dest_eq (concl athm)) 1163 val (_,_,rb)= decompose_term a; 1164 in 1165 ``!s a s'. 1166 (��access_violation s')==> 1167 (��access_violation s)==> 1168 (^rb s = ValueState a s') ==> 1169 ((s'.registers (0,RName_PC) = 1170 (HD (vector_table_address 1171 (get_base_vector_table s) 19w))) 1172 \/ 1173 (s'.registers (0,RName_PC) = 1174 (HD (TL (vector_table_address 1175 (get_base_vector_table s) 19w))))) 1176 `` 1177 end, 1178 let 1179 val athm = SIMP_CONV (bool_ss) [take_svc_exception_def] 1180 ``take_svc_exception <|proc:=0|> `` 1181 val (_, a) = (dest_eq (concl athm)) 1182 val (_,_,body)= decompose_term a; 1183 1184 val sl_elm = ``(a:(word32 # word32 # ARMpsr # CP15scr # CP15sctlr))``; 1185 val const_rp_thm = const_comp_take_undef_svc_exception_rp_thm; 1186 val fixed_vb_rp_thm2 = fixed_VectorBase_undef_instr_exception_thm2; 1187 val fixed_vb_rp_thm1 = fixed_VectorBase_undef_instr_exception_thm1; 1188 val l_type = ``:(word32 # word32 # ARMpsr # CP15scr # CP15sctlr)``; 1189 val spec_list1 = mk_spec_list(sl_elm); 1190 val spec_list2 = mk_spec_list2(sl_elm); 1191 in 1192 prove_take_exception_spc 1193 body take_undef_instr_exception_def sl_elm 1194 const_rp_thm fixed_vb_rp_thm2 1195 fixed_vb_rp_thm1 joint_write_body_svc_spc_thm 1196 l_type spec_list1 spec_list2 1197 end 1198 ); 1199 1200 1201val _ = export_theory(); 1202