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