1(* ------------------------------------------------------------------------ *) 2(* ARM Machine Code Semantics (A and R profiles) *) 3(* ============================================= *) 4(* Defines ARM state-space and a sequential state-transforming Monad *) 5(* ------------------------------------------------------------------------ *) 6 7(* interactive use: 8 app load ["arm_astTheory", "wordsLib"]; 9*) 10 11open HolKernel boolLib bossLib Parse; 12open wordsLib; 13 14open arm_astTheory; 15 16val _ = new_theory "arm_seq_monad"; 17 18(* ------------------------------------------------------------------------ *) 19 20(* ---------------------------- *) 21(* Monad for exclusive monitors *) 22(* ---------------------------- *) 23 24val _ = type_abbrev("exclusive_triple", ``: FullAddress # iiid # num``); 25 26val _ = type_abbrev("exclusive_state", 27 ``: (proc -> FullAddress set) # (FullAddress # proc) set``); 28 29val _ = type_abbrev("ExclusiveM", 30 ``: exclusive_state -> ('a # exclusive_state)``); 31 32val constE_def = Define` 33 (constE: 'a -> 'a ExclusiveM) x = \y. (x,y)`; 34 35val seqE_def = Define` 36 (seqE: 'a ExclusiveM -> ('a -> 'b ExclusiveM) -> 'b ExclusiveM) s f = 37 \y. let (v,x) = s y in f v x`; 38 39val _ = Hol_datatype `ExclusiveMonitors = 40 <| state : exclusive_state; 41 MarkExclusiveGlobal : exclusive_triple -> unit ExclusiveM; 42 MarkExclusiveLocal : exclusive_triple -> unit ExclusiveM; 43 IsExclusiveGlobal : exclusive_triple -> bool ExclusiveM; 44 IsExclusiveLocal : exclusive_triple -> bool ExclusiveM; 45 ClearExclusiveByAddress : exclusive_triple -> unit ExclusiveM; 46 ClearExclusiveLocal : proc -> unit ExclusiveM 47 |>`; 48 49(* ---------------------- *) 50(* Monad for Coprocessors *) 51(* ---------------------- *) 52 53val _ = Hol_datatype `coproc_state = 54 <| cp14 : CP14reg; 55 cp15 : CP15reg |>`; 56 57val _ = type_abbrev("CoprocessorM", ``:coproc_state -> ('a # coproc_state)``); 58 59val constC_def = Define` 60 (constC: 'a -> 'a CoprocessorM) x = \y. (x,y)`; 61 62val seqC_def = Define` 63 (seqC: 'a CoprocessorM -> ('a -> 'b CoprocessorM) -> 'b CoprocessorM) s f = 64 \y. let (v,x) = s y in f v x`; 65 66val _ = Hol_datatype `Coprocessors = 67 <| state : coproc_state; 68 accept : CPinstruction -> bool CoprocessorM; 69 internal_op : CPinstruction -> unit CoprocessorM; 70 load_count : CPinstruction -> num CoprocessorM; 71 load : CPinstruction -> word32 list -> unit CoprocessorM; 72 store : CPinstruction -> word32 list CoprocessorM; 73 send_one : CPinstruction -> word32 -> unit CoprocessorM; 74 get_one : CPinstruction -> word32 CoprocessorM; 75 send_two : CPinstruction -> word32 # word32 -> unit CoprocessorM; 76 get_two : CPinstruction -> (word32 # word32) CoprocessorM 77 |>`; 78 79(* ------------- *) 80(* Monad for ARM *) 81(* ------------- *) 82 83val _ = Hol_datatype `arm_state = 84 <| registers : proc # RName -> word32; (* general-purpose *) 85 psrs : proc # PSRName -> ARMpsr; (* program-status *) 86 event_register : proc -> bool; 87 interrupt_wait : proc -> bool; 88 memory : FullAddress -> word8; 89 accesses : memory_access list; 90 information : ARMinfo; 91 coprocessors : Coprocessors; 92 monitors : ExclusiveMonitors (* synchronization & semaphores *) 93 |>`; 94 95(* ------------------------------------------------------------------------ *) 96 97val _ = Hol_datatype `error_option = ValueState of 'a => 'b | Error of string`; 98 99val _ = type_abbrev("M",``:arm_state -> ('a, arm_state) error_option``); 100 101val constT_def = Define` 102 (constT: 'a -> 'a M) x = \y. ValueState x y`; 103 104val errorT_def = Define` 105 (errorT : string -> 'a M) e = K (Error e)`; 106 107new_constant("access_violation", ``:arm_state -> bool``); 108val seqT_def = Define` (* new seqT *) 109 (seqT: 'a M -> ('a -> 'b M) -> 'b M) s f = 110 \y. case s y of Error e => Error e 111 | ValueState z t => 112 ( 113 if (access_violation t) 114 then (ValueState ARB t) 115 else (f z t) 116 )`; 117 118val parT_def = Define` 119 (parT: 'a M -> 'b M -> ('a # 'b) M) s t = 120 seqT s (\x. seqT t (\y. constT (x,y)))`; 121 122val lockT_def = Define` 123 (lockT: 'a M -> 'a M) s = s`; 124 125val condT_def = Define` 126 (condT: bool -> unit M -> unit M) = 127 \b s. if b then s else constT ()`; 128 129val forT_def = tDefine "forT" 130 `forT (l : num) (h : num) (f : num -> 'a M) : ('a list) M = 131 if l <= h then 132 seqT (f l) 133 (\r. seqT (forT (l + 1) h f) (\l. constT (r::l))) 134 else 135 constT []` 136 (WF_REL_TAC `measure (\(l,h,f). h + 1 - l)`); 137 138val readT_def = Define `(readT f : 'a M) = \y. ValueState (f y) y`; 139val writeT_def = Define `(writeT f : unit M) = \y. ValueState () (f y)`; 140 141(* ARM specific operations *) 142 143val read_info_def = Define` 144 read_info (ii:iiid) = readT arm_state_information`; 145 146val read_arch_def = Define` 147 read_arch (ii:iiid) = readT (ARMinfo_arch o arm_state_information)`; 148 149val read_extensions_def = Define` 150 read_extensions (ii:iiid) = 151 readT (ARMinfo_extensions o arm_state_information)`; 152 153val read__reg_def = Define` 154 read__reg (ii:iiid) rname = readT (\s. s.registers (ii.proc,rname))`; 155 156val write__reg_def = Define` 157 write__reg (ii:iiid) rname value = 158 writeT (arm_state_registers_fupd ((ii.proc,rname) =+ value))`; 159 160val read__psr_def = Define` 161 read__psr (ii:iiid) i = readT (\s. s.psrs (ii.proc,i))`; 162 163val write__psr_def = Define` 164 (write__psr (ii:iiid) psrname value):unit M = 165 writeT (arm_state_psrs_fupd ((ii.proc,psrname) =+ value))`; 166 167val read_scr_def = Define` 168 read_scr (ii:iiid) = readT (\s. s.coprocessors.state.cp15.SCR)`; 169 170val write_scr_def = Define` 171 write_scr (ii:iiid) value = 172 writeT (arm_state_coprocessors_fupd (Coprocessors_state_fupd 173 (coproc_state_cp15_fupd (\cp15. cp15 with <| SCR := value |>))))`; 174 175val read_nsacr_def = Define` 176 read_nsacr (ii:iiid) = readT (\s. s.coprocessors.state.cp15.NSACR)`; 177 178val read_sctlr_def = Define` 179 read_sctlr (ii:iiid) = readT (\s. s.coprocessors.state.cp15.SCTLR)`; 180 181val read_teehbr_def = Define` 182 read_teehbr (ii:iiid) = readT (\s. s.coprocessors.state.cp14.TEEHBR)`; 183 184val read_cpsr_def = Define `read_cpsr ii = read__psr ii CPSR`; 185 186val write_cpsr_def = Define` 187 write_cpsr ii value = write__psr ii CPSR value`; 188 189val read_isetstate_def = Define` 190 read_isetstate (ii:iiid) = 191 seqT (read_cpsr ii) 192 (\cpsr. 193 constT ((FCP i. (i = 1) /\ cpsr.J \/ (i = 0) /\ cpsr.T):word2))`; 194 195val write_isetstate_def = Define` 196 write_isetstate ii (isetstate:word2) = 197 seqT (read_cpsr ii) 198 (\cpsr. 199 write_cpsr ii 200 (cpsr with <| J := isetstate ' 1; T := isetstate ' 0 |>))`; 201 202val have_extension_def = new_definition("have_extension_def", 203 ``have_extension P (ii:iiid) : bool M = 204 seqT (read_info ii) (\info. constT ((info.arch,info.extensions) IN P))``); 205 206val have_security_ext_def = new_definition("have_security_ext_def", 207 ``have_security_ext = have_extension security_support``); 208 209val have_thumbEE_def = new_definition("have_thumbEE_def", 210 ``have_thumbEE = have_extension thumbee_support``); 211 212val have_jazelle_def = new_definition("have_jazelle_def", 213 ``have_jazelle = have_extension jazelle_support``); 214 215val rule = 216 SIMP_RULE (std_ss++pred_setLib.PRED_SET_ss) [] o 217 ONCE_REWRITE_RULE 218 [pred_setTheory.SPECIFICATION 219 |> GSYM 220 |> INST_TYPE [alpha |-> ``:ARMarch # ARMextensions set``]] o 221 REWRITE_RULE [FUN_EQ_THM, have_extension_def, 222 arm_coretypesTheory.thumbee_support_def, 223 arm_coretypesTheory.security_support_def, 224 arm_coretypesTheory.jazelle_support_def] 225 226val have_security_ext = save_thm("have_security_ext", 227 rule have_security_ext_def); 228 229val have_thumbEE = save_thm("have_thumbEE", 230 rule have_thumbEE_def); 231 232val have_jazelle = save_thm("have_jazelle", 233 rule have_jazelle_def); 234 235val bad_mode_def = Define` 236 bad_mode (ii:iiid) (mode:word5) = 237 if mode = 0b10110w then 238 seqT (have_security_ext ii) 239 (\have_security_ext. constT (~have_security_ext)) 240 else 241 constT (mode NOTIN {0b10000w; 242 0b10001w; 243 0b10010w; 244 0b10011w; 245 0b10111w; 246 0b11011w; 247 0b11111w})`; 248 249val read_spsr_def = Define` 250 read_spsr (ii:iiid) = 251 seqT (read_cpsr ii) 252 (\cpsr. 253 seqT (bad_mode ii cpsr.M) 254 (\bad_mode. 255 if bad_mode then 256 errorT "read_spsr: unpredictable" 257 else 258 case cpsr.M 259 of 0b10001w => read__psr ii SPSR_fiq (* FIQ mode *) 260 | 0b10010w => read__psr ii SPSR_irq (* IRQ mode *) 261 | 0b10011w => read__psr ii SPSR_svc (* Supervisor mode *) 262 | 0b10110w => read__psr ii SPSR_mon (* Monitor mode *) 263 | 0b10111w => read__psr ii SPSR_abt (* Abort mode *) 264 | 0b11011w => read__psr ii SPSR_und (* Undefined mode *) 265 | _ => errorT "read_spsr: unpredictable"))`; 266 267val write_spsr_def = Define` 268 write_spsr (ii:iiid) value = 269 seqT (read_cpsr ii) 270 (\cpsr. 271 seqT (bad_mode ii cpsr.M) 272 (\bad_mode. 273 if bad_mode then 274 errorT "write_spsr: unpredictable" 275 else 276 case cpsr.M 277 of 0b10001w => write__psr ii SPSR_fiq value (* FIQ mode *) 278 | 0b10010w => write__psr ii SPSR_irq value (* IRQ mode *) 279 | 0b10011w => write__psr ii SPSR_svc value (* Supervisor mode *) 280 | 0b10110w => write__psr ii SPSR_mon value (* Monitor mode *) 281 | 0b10111w => write__psr ii SPSR_abt value (* Abort mode *) 282 | 0b11011w => write__psr ii SPSR_und value (* Undefined mode *) 283 | _ => errorT "write_spsr: unpredictable"))`; 284 285val current_mode_is_priviledged_def = Define` 286 current_mode_is_priviledged (ii:iiid) = 287 seqT (read_cpsr ii) 288 (\cpsr. 289 seqT (bad_mode ii cpsr.M) 290 (\bad_mode. 291 if bad_mode then 292 errorT "current_mode_is_priviledged: unpredictable" 293 else 294 constT (cpsr.M <> 0b10000w)))`; 295 296val current_mode_is_user_or_system_def = Define` 297 current_mode_is_user_or_system (ii:iiid) = 298 seqT (read_cpsr ii) 299 (\cpsr. 300 seqT (bad_mode ii cpsr.M) 301 (\bad_mode. 302 if bad_mode then 303 errorT "current_mode_is_user_or_system: unpredictable" 304 else 305 constT (cpsr.M IN {0b10000w; 0b11111w})))`; 306 307val is_secure_def = Define` 308 is_secure (ii:iiid) = 309 seqT 310 (parT (have_security_ext ii) 311 (parT (read_scr ii) (read_cpsr ii))) 312 (\(have_security_ext,scr,cpsr). 313 constT (~have_security_ext \/ ~scr.NS \/ (cpsr.M = 0b10110w)))`; 314 315val read_vbar_def = Define` 316 read_vbar ii = readT (\s. s.coprocessors.state.cp15.VBAR)`; 317 318val read_mvbar_def = Define` 319 read_mvbar (ii:iiid) = readT (\s. s.coprocessors.state.cp15.MVBAR)`; 320 321val current_instr_set_def = Define` 322 current_instr_set ii = 323 seqT (read_isetstate ii) 324 (\isetstate. 325 constT 326 (case isetstate 327 of 0b00w => InstrSet_ARM 328 | 0b01w => InstrSet_Thumb 329 | 0b10w => InstrSet_Jazelle 330 | 0b11w => InstrSet_ThumbEE))`; 331 332val select_instr_set_def = Define` 333 select_instr_set ii (iset:InstrSet) = 334 case iset 335 of InstrSet_ARM => 336 seqT (current_instr_set ii) 337 (\current_instr_set. 338 if current_instr_set = InstrSet_ThumbEE then 339 errorT "select_instr_set: unpredictable" 340 else 341 write_isetstate ii 0b00w) 342 | InstrSet_Thumb => 343 write_isetstate ii 0b01w 344 | InstrSet_Jazelle => 345 write_isetstate ii 0b10w 346 | InstrSet_ThumbEE => 347 write_isetstate ii 0b11w`; 348 349val RBankSelect_def = Define` 350 RBankSelect (ii:iiid) (mode, usr, fiq, irq, svc, abt, und, mon) : RName M = 351 seqT (bad_mode ii mode) 352 (\bad_mode. 353 if bad_mode then 354 errorT "RBankSelect: unpredictable" 355 else 356 constT 357 ((case mode 358 of 0b10000w => usr (* User mode *) 359 | 0b10001w => fiq (* FIQ mode *) 360 | 0b10010w => irq (* IRQ mode *) 361 | 0b10011w => svc (* Supervisor mode *) 362 | 0b10110w => mon (* Monitor mode *) 363 | 0b10111w => abt (* Abort mode *) 364 | 0b11011w => und (* Undefined mode *) 365 | 0b11111w => usr (* System mode uses User mode registers *))))`; 366 367val RfiqBankSelect_def = Define` 368 RfiqBankSelect ii (mode, usr, fiq) = 369 RBankSelect ii (mode, usr, fiq, usr, usr, usr, usr, usr)`; 370 371val LookUpRName_def = Define` 372 LookUpRName (ii:iiid) (n:word4, mode) = 373 case n 374 of 0w => constT RName_0usr 375 | 1w => constT RName_1usr 376 | 2w => constT RName_2usr 377 | 3w => constT RName_3usr 378 | 4w => constT RName_4usr 379 | 5w => constT RName_5usr 380 | 6w => constT RName_6usr 381 | 7w => constT RName_7usr 382 | 8w => RfiqBankSelect ii (mode, RName_8usr, RName_8fiq) 383 | 9w => RfiqBankSelect ii (mode, RName_9usr, RName_9fiq) 384 | 10w => RfiqBankSelect ii (mode, RName_10usr, RName_10fiq) 385 | 11w => RfiqBankSelect ii (mode, RName_11usr, RName_11fiq) 386 | 12w => RfiqBankSelect ii (mode, RName_12usr, RName_12fiq) 387 | 13w => RBankSelect ii 388 (mode, RName_SPusr, RName_SPfiq, RName_SPirq, 389 RName_SPsvc, RName_SPabt, RName_SPund, RName_SPmon) 390 | 14w => RBankSelect ii 391 (mode, RName_LRusr, RName_LRfiq, RName_LRirq, 392 RName_LRsvc, RName_LRabt, RName_LRund, RName_LRmon) 393 | _ => errorT "LookUpRName: n = 15w"`; 394 395val read_reg_mode_def = Define` 396 read_reg_mode ii (n, mode) = 397 seqT (parT (is_secure ii) (read_nsacr ii)) 398 (\(is_secure,nsacr). 399 if (n = 15w) \/ ~is_secure /\ 400 ((mode = 0b10110w) \/ (mode = 0b10001w) /\ nsacr.RFR) 401 then 402 errorT "read_reg_mode: unpredictable" 403 else 404 seqT 405 (LookUpRName ii (n, mode)) 406 (\rname. read__reg ii rname))`; 407 408val write_reg_mode_def = Define` 409 write_reg_mode ii (n, mode) value = 410 seqT (parT (is_secure ii) 411 (parT (read_nsacr ii) 412 (current_instr_set ii))) 413 (\(is_secure,nsacr,current_instr_set). 414 if (n = 15w) \/ 415 ~is_secure /\ 416 ((mode = 0b10110w) \/ 417 (mode = 0b10001w) /\ nsacr.RFR) \/ 418 (n = 13w) /\ ~aligned(value,4) /\ (current_instr_set <> InstrSet_ARM) 419 then 420 errorT "write_reg_mode: unpredictable" 421 else 422 seqT (LookUpRName ii (n, mode)) 423 (\rname. write__reg ii rname value))`; 424 425val read_pc_def = Define `read_pc ii = read__reg ii RName_PC`; 426 427val pc_store_value_def = Define` 428 pc_store_value ii = 429 seqT (read_pc ii) 430 (\pc. constT (pc + 8w))`; 431 432val read_reg_def = Define` 433 read_reg (ii:iiid) n = 434 if n = 15w then 435 seqT (parT (read_pc ii) (current_instr_set ii)) 436 (\(pc,current_instr_set). 437 constT 438 (if current_instr_set = InstrSet_ARM then 439 pc + 8w 440 else 441 pc + 4w)) 442 else 443 seqT (read_cpsr ii) 444 (\cpsr. read_reg_mode ii (n,cpsr.M))`; 445 446val write_reg_def = Define` 447 write_reg (ii:iiid) n value = 448 if n = 15w then 449 errorT "write_reg: assert" 450 else 451 seqT (read_cpsr ii) 452 (\cpsr. write_reg_mode ii (n,cpsr.M) value)`; 453 454val branch_to_def = Define` 455 branch_to ii (address:word32) = 456 write__reg ii RName_PC address`; 457 458val increment_pc_def = Define` 459 increment_pc ii enc = 460 seqT (read_pc ii) 461 (\pc. branch_to ii 462 (pc + if (enc = Encoding_Thumb) \/ (enc = Encoding_ThumbEE) then 463 2w 464 else 465 4w))`; 466 467val big_endian_def = Define` 468 big_endian (ii:iiid) = 469 seqT (read_cpsr ii) (\cpsr. constT (cpsr.E))`; 470 471(* A basic memory address translation *) 472 473val translate_address_def = Define` 474 translate_address 475 (address : word32, ispriv : bool, iswrite : bool) : AddressDescriptor M = 476 constT 477 (<| memattrs := <| 478 type := MemType_Normal; 479 innerattrs := 0w; (* Non-cacheable *) 480 outerattrs := 0w; (* Non-cacheable *) 481 shareable := T; 482 outershareable := T |>; 483 paddress := address |>)`; 484 485val read_monitor_def = Define` 486 read_monitor (ii:iiid) = readT arm_state_monitors`; 487 488val write_monitor_def = Define` 489 write_monitor (ii:iiid) d = writeT (\s. s with monitors := d)`; 490 491val read_mem1_def = Define` 492 read_mem1 (ii:iiid) (address:FullAddress) : word8 M = 493 seqT (writeT (arm_state_accesses_fupd (CONS (MEM_READ address)))) 494 (\u:unit. readT (\s. s.memory address))`; 495 496val write_mem1_def = Define` 497 write_mem1 (ii:iiid) (address:FullAddress) (byte:word8) = 498 seqT (writeT (arm_state_accesses_fupd (CONS (MEM_WRITE address byte)))) 499 (\u:unit. writeT (arm_state_memory_fupd (address =+ byte)))`; 500 501(* aligned, atomic, little-endian memory access - read *) 502 503val read_mem_def = Define` 504 read_mem (ii:iiid) 505 (memaddrdesc:AddressDescriptor, size:num) : (word8 list) M = 506 if size NOTIN {1; 2; 4; 8} then 507 errorT "read_mem: size is not 1, 2, 4 or 8" 508 else let address = memaddrdesc.paddress in 509 forT 0 (size - 1) 510 (\i. read_mem1 ii (address + n2w i))`; 511 512(* aligned, atomic, little-endian memory access - write *) 513 514val write_mem_def = Define` 515 write_mem (ii:iiid) 516 (memaddrdesc:AddressDescriptor, size:num) (value:word8 list) : unit M = 517 if size NOTIN {1; 2; 4; 8} then 518 errorT "write_mem: size is not 1, 2, 4 or 8" 519 else if LENGTH value <> size then 520 errorT "write_mem: value has wrong size" 521 else let address = memaddrdesc.paddress in 522 seqT 523 (forT 0 (size - 1) 524 (\i. write_mem1 ii (address + n2w i) (EL i value))) 525 (\l. constT ())`; 526 527val read_memA_with_priv_def = Define` 528 read_memA_with_priv (ii:iiid) (address:word32, size:num, privileged:bool) = 529 seqT 530 (if aligned(address,size) then 531 constT address 532 else 533 seqT (read_sctlr ii) 534 (\sctlr. 535 if sctlr.A \/ sctlr.U then 536 errorT "read_memA_with_priv: DAbort_Alignment" 537 else 538 constT (align(address,size)))) 539 (\VA. 540 seqT (translate_address(VA, privileged, F)) 541 (\memaddrdesc. 542 seqT (read_mem ii (memaddrdesc, size)) 543 (\value. 544 seqT 545 (big_endian ii) 546 (\E. constT (if E then REVERSE value else value)))))`; 547 548val write_memA_with_priv_def = Define` 549 write_memA_with_priv (ii:iiid) 550 (address:word32, size:num, privileged:bool) (value:word8 list) = 551 seqT 552 (if aligned(address,size) then 553 constT address 554 else 555 seqT (read_sctlr ii) 556 (\sctlr. 557 if sctlr.A \/ sctlr.U then 558 errorT "write_memA_with_priv: DAbort_Alignment" 559 else 560 constT (align(address,size)))) 561 (\VA. 562 seqT (translate_address(VA, privileged, T)) 563 (\memaddrdesc. 564 seqT 565 (if memaddrdesc.memattrs.shareable then 566 seqT 567 (read_monitor ii) 568 (\monitor. 569 write_monitor ii 570 (monitor with 571 state := SND (monitor.ClearExclusiveByAddress 572 (memaddrdesc.paddress,ii,size) monitor.state))) 573 else 574 constT ()) 575 (\u. 576 seqT 577 (seqT (big_endian ii) 578 (\E. constT (if E then REVERSE value else value))) 579 (\value. write_mem ii (memaddrdesc,size) value))))`; 580 581val read_memU_with_priv_def = Define` 582 read_memU_with_priv (ii:iiid) (address:word32, size:num, privileged:bool) = 583 seqT (read_sctlr ii) 584 (\sctlr. 585 seqT 586 (if ~sctlr.A /\ ~sctlr.U then 587 constT (align(address,size)) 588 else 589 constT (address)) 590 (\address. 591 if aligned(address,size) then 592 read_memA_with_priv ii (address,size,privileged) 593 else if sctlr.A then 594 errorT "read_memU_with_priv: DAbort_Alignment" 595 else 596 seqT 597 (forT 0 (size - 1) 598 (\i. read_memA_with_priv ii (address + n2w i,1,privileged))) 599 (\values. let value = FLAT values in 600 seqT 601 (big_endian ii) 602 (\E. constT (if E then REVERSE value else value)))))`; 603 604val write_memU_with_priv_def = Define` 605 write_memU_with_priv (ii:iiid) 606 (address:word32, size:num, privileged:bool) (value:word8 list) = 607 seqT (read_sctlr ii) 608 (\sctlr. 609 seqT 610 (if ~sctlr.A /\ ~sctlr.U then 611 constT (align(address,size)) 612 else 613 constT (address)) 614 (\address. 615 if aligned(address,size) then 616 write_memA_with_priv ii (address,size,privileged) value 617 else if sctlr.A then 618 errorT "write_memU_with_priv: DAbort_Alignment" 619 else 620 seqT 621 (seqT (big_endian ii) 622 (\E. constT (if E then REVERSE value else value))) 623 (\value. 624 seqT 625 (forT 0 (size - 1) 626 (\i. write_memA_with_priv ii 627 (address + n2w i,1,privileged) [EL i value])) 628 (\u. constT ()))))`; 629 630val read_memA_def = Define` 631 read_memA ii (address:word32, size:num) = 632 seqT (current_mode_is_priviledged ii) 633 (\priviledged. read_memA_with_priv ii (address,size,priviledged))`; 634 635val write_memA_def = Define` 636 write_memA ii (address:word32, size:num) (value:word8 list) = 637 seqT (current_mode_is_priviledged ii) 638 (\priviledged. write_memA_with_priv ii (address,size,priviledged) value)`; 639 640val read_memA_unpriv_def = Define` 641 read_memA_unpriv ii (address:word32, size:num) = 642 read_memA_with_priv ii (address,size,F)`; 643 644val write_memA_unpriv_def = Define` 645 write_memA_unpriv ii (address:word32, size:num) (value:word8 list) = 646 write_memA_with_priv ii (address,size,F) value`; 647 648val read_memU_def = Define` 649 read_memU ii (address:word32, size:num) = 650 seqT (current_mode_is_priviledged ii) 651 (\priviledged. read_memU_with_priv ii (address,size,priviledged))`; 652 653val write_memU_def = Define` 654 write_memU ii (address:word32, size:num) (value:word8 list) = 655 seqT (current_mode_is_priviledged ii) 656 (\priviledged. write_memU_with_priv ii (address,size,priviledged) value)`; 657 658val read_memU_unpriv_def = Define` 659 read_memU_unpriv ii (address:word32, size:num) = 660 read_memU_with_priv ii (address,size,F)`; 661 662val write_memU_unpriv_def = Define` 663 write_memU_unpriv ii (address:word32, size:num) (value:word8 list) = 664 write_memU_with_priv ii (address,size,F) value`; 665 666(* hints and event operations *) 667 668val data_memory_barrier_def = Define` 669 (data_memory_barrier : iiid -> MBReqDomain # MBReqTypes -> unit M) ii x = 670 constT ()`; 671 672val data_synchronization_barrier_def = Define` 673 (data_synchronization_barrier : 674 iiid -> MBReqDomain # MBReqTypes -> unit M) ii x = 675 constT ()`; 676 677val instruction_synchronization_barrier_def = Define` 678 (instruction_synchronization_barrier : iiid -> unit M) ii = 679 constT ()`; 680 681val hint_yield_def = Define` 682 (hint_yield : iiid -> unit M) ii = constT ()`; 683 684val hint_preload_data_for_write_def = Define` 685 (hint_preload_data_for_write : iiid -> FullAddress -> unit M) ii x = 686 constT ()`; 687 688val hint_preload_data_def = Define` 689 (hint_preload_data : iiid -> FullAddress -> unit M) ii x = 690 constT ()`; 691 692val hint_preload_instr_def = Define` 693 (hint_preload_instr : iiid -> FullAddress -> unit M) ii x = 694 constT ()`; 695 696val hint_debug_def = Define` 697 (hint_debug : iiid -> word4 -> unit M) ii option = constT ()`; 698 699val clear_event_register_def = Define` 700 (clear_event_register : iiid -> unit M) ii = 701 writeT (arm_state_event_register_fupd (ii.proc =+ F))`; 702 703val event_registered_def = Define` 704 (event_registered : iiid -> bool M) ii = 705 readT (\s. s.event_register ii.proc)`; 706 707val send_event_def = Define` 708 (send_event : iiid -> unit M) ii = 709 writeT (\s. s with event_register := K T)`; 710 711val wait_for_event_def = Define` 712 (wait_for_event : iiid -> unit M) ii = constT ()`; 713 714val waiting_for_interrupt_def = Define` 715 (waiting_for_interrupt : iiid -> bool M) ii = 716 readT (\s. s.interrupt_wait ii.proc)`; 717 718val clear_wait_for_interrupt_def = Define` 719 (clear_wait_for_interrupt : iiid -> unit M) ii = 720 writeT (arm_state_interrupt_wait_fupd (ii.proc =+ F))`; 721 722val wait_for_interrupt_def = Define` 723 (wait_for_interrupt : iiid -> unit M) ii = 724 writeT (arm_state_interrupt_wait_fupd (ii.proc =+ T))`; 725 726(* exclusive monitor operations. *) 727 728val set_exclusive_monitors_def = Define` 729 (set_exclusive_monitors ii (address:word32,size:num)) : unit M = 730 seqT 731 (parT (read_cpsr ii) (read_monitor ii)) 732 (\(cpsr,monitor). 733 seqT (translate_address(address, cpsr.M <> 0b10000w, F)) 734 (\memaddrdesc. let triple = (memaddrdesc.paddress,ii,size) in 735 write_monitor ii 736 (monitor with 737 state := 738 SND ((if memaddrdesc.memattrs.shareable then 739 seqE 740 (monitor.MarkExclusiveGlobal triple) 741 (\u. monitor.MarkExclusiveLocal triple) 742 else 743 monitor.MarkExclusiveLocal triple) 744 monitor.state))))`; 745 746val exclusive_monitors_pass_def = Define` 747 (exclusive_monitors_pass ii (address:word32,size:num)) : bool M = 748 seqT 749 (parT (read_cpsr ii) (read_monitor ii)) 750 (\(cpsr,monitor). 751 if ~aligned(address,size) then 752 errorT "exclusive_monitors_pass: alignment fault" 753 else 754 seqT (translate_address(address, cpsr.M <> 0b10000w, F)) 755 (\memaddrdesc. 756 let triple = (memaddrdesc.paddress,ii,size) in 757 let (passed,state') = 758 seqE (monitor.IsExclusiveLocal triple) 759 (\local_passed. 760 seqE 761 (if memaddrdesc.memattrs.shareable then 762 seqE (monitor.IsExclusiveGlobal triple) 763 (\global_passed. 764 constE (local_passed /\ global_passed)) 765 else 766 constE local_passed) 767 (\passed. 768 if passed then 769 seqE (monitor.ClearExclusiveLocal ii.proc) 770 (\u. constE passed) 771 else 772 constE passed)) monitor.state 773 in 774 seqT 775 (write_monitor ii (monitor with state := state')) 776 (\u. constT passed)))`; 777 778val clear_exclusive_local_def = Define` 779 (clear_exclusive_local (ii:iiid)) : unit M = 780 seqT (read_monitor ii) 781 (\monitor. 782 let state' = SND (monitor.ClearExclusiveLocal ii.proc monitor.state) 783 in 784 write_monitor ii (monitor with state := state'))`; 785 786(* coprocessor operations. *) 787 788val read_coprocessors_def = Define` 789 read_coprocessors (ii:iiid) = readT arm_state_coprocessors`; 790 791val write_coprocessors_def = Define` 792 write_coprocessors (ii:iiid) d = writeT (\s. s with coprocessors := d)`; 793 794val coproc_accepted_def = Define` 795 coproc_accepted (ii:iiid) (inst:CPinstruction) : bool M = 796 seqT (read_coprocessors ii) 797 (\coprocessors. 798 let accept = FST (coprocessors.accept inst coprocessors.state) in 799 constT accept)`; 800 801val coproc_internal_operation_def = Define` 802 coproc_internal_operation (ii:iiid) (inst:CPinstruction) : unit M = 803 seqT (read_coprocessors ii) 804 (\coprocessors. 805 let cp_state = SND (coprocessors.internal_op inst coprocessors.state) in 806 write_coprocessors ii (coprocessors with state := cp_state))`; 807 808val coproc_send_loaded_words_def = Define` 809 coproc_send_loaded_words (ii:iiid) 810 (readm:num->word32 M, inst:CPinstruction) : unit M = 811 seqT (read_coprocessors ii) 812 (\coprocessors. 813 let count = FST (coprocessors.load_count inst coprocessors.state) 814 in 815 seqT 816 (forT 0 (count - 1) readm) 817 (\data. 818 let cp_state = SND (coprocessors.load inst data coprocessors.state) 819 in 820 write_coprocessors ii 821 (coprocessors with state := cp_state)))`; 822 823val coproc_get_words_to_store_def = Define` 824 coproc_get_words_to_store (ii:iiid) 825 (inst:CPinstruction) : (word32 list) M = 826 seqT (read_coprocessors ii) 827 (\coprocessors. 828 let data = FST (coprocessors.store inst coprocessors.state) in 829 constT data)`; 830 831val coproc_send_one_word_def = Define` 832 coproc_send_one_word (ii:iiid) 833 (data:word32, inst:CPinstruction) : unit M = 834 seqT (read_coprocessors ii) 835 (\coprocessors. 836 let cp_state = SND (coprocessors.send_one inst data coprocessors.state) 837 in 838 write_coprocessors ii (coprocessors with state := cp_state))`; 839 840val coproc_get_one_word_def = Define` 841 coproc_get_one_word (ii:iiid) (inst:CPinstruction) : word32 M = 842 seqT (read_coprocessors ii) 843 (\coprocessors. 844 let data = FST (coprocessors.get_one inst coprocessors.state) in 845 constT data)`; 846 847val coproc_send_two_words_def = Define` 848 coproc_send_two_words (ii:iiid) 849 (data:word32 # word32, inst:CPinstruction) : unit M = 850 seqT (read_coprocessors ii) 851 (\coprocessors. 852 let cp_state = SND (coprocessors.send_two inst data coprocessors.state) 853 in 854 write_coprocessors ii (coprocessors with state := cp_state))`; 855 856val coproc_get_two_words_def = Define` 857 coproc_get_two_words (ii:iiid) (inst:CPinstruction) : (word32#word32) M = 858 seqT (read_coprocessors ii) 859 (\coprocessors. 860 let data = FST (coprocessors.get_two inst coprocessors.state) in 861 constT data)`; 862 863val _ = computeLib.add_persistent_funs 864 ["have_security_ext", 865 "have_thumbEE", 866 "have_jazelle"]; 867 868val _ = export_theory (); 869