1(* 2Updates since version 4: 3------------------------ 4 5 - integrate MMU into monad 6 - understand access lists already with one violating entry, even if the other entries are not understood 7 - leaving only one mmu_arm_next 8 9maybe todo: 10 11 - integrate evaluation for priv mode 12 13 14Updates since version 3: 15----------------------- 16 17 - cleaning up 18 - fixing a logical error in data_abort 19 20Updates since version 2: 21------------------------ 22 23 - old access list is truncated 24 - todos fixed 25 26 27Updates since version 1: 28------------------------ 29 30 - checking only recent updates in the access list 31 - correct values in mmu_supported 32 - check MMU_support for needed section descriptors only 33 - consistent error handling 34 35 - obtain coprocessor registers only once 36 - add mode to permitted_byte 37 - correct/check case analysis of permitted_byte 38 - more detailed version of mmu_arm_next (ValueState and Error X) 39 - distinction between read and write 40 41 42*) 43 44 45(* Loading: I assume that armLib is already loaded 46 47loadPath := "/NOBACKUP/workspaces/nargeskh/hol4.k.7/examples/ARM/v7/" :: !loadPath; 48loadPath := "/NOBACKUP/workspaces/nargeskh/hol4.k.7/examples/ARM/v7/eval" :: !loadPath; 49 50load "armLib"; 51open armLib; 52*) 53 54open HolKernel boolLib bossLib Parse; 55open arm_coretypesTheory arm_seq_monadTheory arm_opsemTheory armTheory; 56open parmonadsyntax; 57 58val _ = new_theory("MMU"); 59 60val _ = overload_on("UNKNOWN", ``ARB:bool``); 61val _ = overload_on("UNKNOWN", ``ARB:word32``); 62 63 64val read_mem32_def = Define ` read_mem32 add mem = 65 word32 ([mem (add);mem (add+1w);mem (add+2w);mem (add+3w)])`; 66 67 68val enabled_MMU_def = Define `enabled_MMU (c1:word32) = 69 let bit0 = BIT 0 (w2n(c1)) in 70 bit0`; 71 72 73(* checking MMU support only for one section descriptor *) 74(* further changes in version 2: expr3 = 0 and expr7 may be 01 as well *) 75val sd_supports_MMU_def = Define `sd_supports_MMU content_of_sd si = 76 let expr1 = (content_of_sd && 0x00000003w) in 77 let expr2 = (content_of_sd && 0x0000000Cw) >>> 2 in 78 let expr3 = (content_of_sd && 0x00000010w) >>> 4 in 79 let expr4 = (content_of_sd && 0x00000200w) >>> 9 in 80 let expr7 = (content_of_sd && 0x00000C00w) >>> 10 in 81 let expr5 = (content_of_sd && 0x000FF000w) >>> 12 in 82 let expr6 = (content_of_sd && 0xFFF00000w) >>> 20 in 83 (expr1 = 0b10w:bool[32]) /\ 84 (expr2 = 0b00w:word32) /\ 85 (expr3 = 0b0w:word32) /\ 86 (expr4 = 0b0w:word32) /\ 87 ((expr7 = 0b11w:word32) \/ (expr7 = 0b01w:word32)) /\ 88 (expr5 = 0b0w:word32) /\ 89 (expr6 = si)`; 90 91 92 93(* permitted_byte *) 94(* returns (understood, permitted, message) *) 95val permitted_byte_def = Define `permitted_byte adr is_write (c1:word32) c2 (c3:bool[32]) priv mem = 96 if (~(enabled_MMU c1)) then 97 (T, T, "MMU is disabled") 98 else 99 let si = (adr >>> 20) in 100 let first_sd = c2 && (0xFFFFC000w:bool[32]) in 101 let adr_sd = first_sd + 4w * si in 102 let content_of_sd = read_mem32 adr_sd mem in 103 let domain:bool[32] = 104 (content_of_sd && 0x000001E0w:bool[32]) >>> 5 in 105 (* make sure that it starts with one *) 106 let bit1_c3 = BIT (2*w2n(domain)) (w2n(c3)) in 107 let bit2_c3 = BIT (2*w2n(domain)+1) (w2n(c3)) in 108 let AP = (content_of_sd && 0x00000C00w) >>> 10 in 109 if (sd_supports_MMU content_of_sd si) 110 then 111 (case (bit2_c3, bit1_c3) of 112 (T,T) => (T, T, "uncontrolled manager domain") 113 | (F,F) => (T, F, "no access domain") 114 | (T,F) => (F, UNKNOWN , "unpredictable domain status") 115 | (F,T) => (case AP of 116 0b00w => (T, F, "no access according to PTE") 117 |0b01w => (if priv 118 then (T, T , "permitted by PTE") 119 else (T, F, "no access according to PTE") 120 ) 121 |0b10w => (if priv 122 then (T, T , "permitted by PTE") 123 else (T, ~is_write, "read-only access according to PTE") 124 ) 125 |0b11w => (T, T , "permitted by PTE") 126 | _ => (F, UNKNOWN, "AP wrongly determined") 127 ) 128 ) 129 else 130 (F, UNKNOWN, "no support") 131 `; 132 133 134(* permitted_byte_pure *) 135(* returns boolean "permitted" *) 136(* similar to permitted_byte when assuming *) 137(* that we always understand the MMU setup *) 138 139val permitted_byte_pure_def = Define `permitted_byte_pure adr is_write (c1:word32) c2 (c3:bool[32]) priv mem = 140 if (~(enabled_MMU c1)) then 141 T 142 else 143 let si = (adr >>> 20) in 144 let first_sd = c2 && (0xFFFFC000w:bool[32]) in 145 let adr_sd = first_sd + 4w * si in 146 let content_of_sd = read_mem32 adr_sd mem in 147 let domain:bool[32] = 148 (content_of_sd && 0x000001E0w:bool[32]) >>> 5 in 149 (* make sure that it starts with one *) 150 let bit1_c3 = BIT (2*w2n(domain)) (w2n(c3)) in 151 let bit2_c3 = BIT (2*w2n(domain)+1) (w2n(c3)) in 152 let AP = (content_of_sd && 0x00000C00w) >>> 10 in 153 case (bit2_c3, bit1_c3) of 154 (T,T) => T 155 | (F,F) => F 156 | (F,T) => (case AP of 157 0b00w => F 158 |0b01w => (if priv 159 then T 160 else F 161 ) 162 |0b10w => (if priv 163 then T 164 else (~is_write) 165 ) 166 |0b11w => T 167 ) 168 `; 169 170 171(* relate permitted_byte with permitted_byte_pure *) 172 173val permitted_byte_simp = store_thm ( 174 "permitted_byte_simp", 175 ``!u p m adr is_write c1 c2 c3 priv mem. 176 ((u,p,m) = permitted_byte adr is_write c1 c2 c3 priv mem) /\ u 177 ==> (permitted_byte_pure adr is_write c1 c2 c3 priv mem = p)``, 178 REPEAT STRIP_TAC THEN FULL_SIMP_TAC (srw_ss()) [permitted_byte_def, permitted_byte_pure_def] 179 THEN Cases_on `~enabled_MMU c1` THEN FULL_SIMP_TAC (srw_ss()) [] 180 THEN RW_TAC (srw_ss()) [] 181 THEN FULL_SIMP_TAC (srw_ss()) [LET_DEF] 182 THEN Cases_on `sd_supports_MMU content_of_sd si` THEN Cases_on `bit2_c3` THEN Cases_on `bit1_c3` THEN Cases_on `AP=0w` THEN Cases_on `AP=1w` THEN Cases_on `priv` THEN Cases_on `AP=2w` THEN Cases_on `AP=3w` THEN FULL_SIMP_TAC (srw_ss()) [] 183); 184 185 186(* check_accesses *) 187(* returns (understood, abort, address) *); 188 189 190val check_accesses_def = Define `check_accesses accesses c1 c2 c3 priv memory = 191 case accesses of 192 x::tl => 193 ( let (adr, is_write) = 194 ( case x of 195 MEM_READ address => (address, F) 196 | MEM_WRITE address _ => (address, T) 197 ) in 198 199 let (und, per, msg) = (permitted_byte adr is_write c1 c2 c3 priv memory) in 200 ( 201 if (und /\ (~per)) then 202 (T, T, adr) 203 else 204 ( 205 let (u, d, a) = check_accesses tl c1 c2 c3 priv memory in 206 if (u /\ d) then 207 (T, T, a) 208 else 209 ( 210 if (und /\ u) then 211 (T,F,UNKNOWN) 212 else 213 (F,UNKNOWN, UNKNOWN) 214 ) 215 ) 216 ) 217 ) 218 | _ => (T, F, UNKNOWN)`; 219 220 221 222 223(* check_accesses_pure *) 224(* returns boolean "abort" *) 225(* similar to check_accesses when assuming that we *) 226(* always understand the MMU setup *) 227val check_accesses_pure_def = Define `check_accesses_pure accesses c1 c2 c3 priv memory = 228 case accesses of 229 x::tl => 230 ( let (adr, is_write) = 231 ( case x of 232 MEM_READ address => (address, F) 233 | MEM_WRITE address _ => (address, T) 234 ) in 235 (~permitted_byte_pure adr is_write c1 c2 c3 priv memory) \/ (check_accesses_pure tl c1 c2 c3 priv memory) 236 ) 237 | _ => F`; 238 239 240 241 242 243(* relate check_accesses with check_accesses_pure *) 244 245 246val check_accesses_TAC = (fn IS_WRITE => 247 FULL_SIMP_TAC (srw_ss()) [LET_DEF] 248 THEN Cases_on [QUOTE ("permitted_byte c "^IS_WRITE^" c1 c2 c3 priv mem")] 249 THEN Cases_on `r` 250 THEN Cases_on `q` 251 THEN FULL_SIMP_TAC (srw_ss()) [permitted_byte_simp] 252 THEN MP_TAC ( SPECL [``T``, 253 ``q':bool``, 254 ``r':string``, 255 ``c:word32``, 256 Term [QUOTE IS_WRITE], 257 ``c1:word32``, 258 ``c2:word32``, 259 ``c3:word32``, 260 ``priv:bool``, 261 ``mem:bool[32] -> bool[8]``] permitted_byte_simp) 262 THEN RW_TAC (srw_ss()) [] 263 THEN Cases_on `check_accesses acc c1 c2 c3 priv mem` 264 THEN Cases_on `r` 265 THEN FULL_SIMP_TAC (srw_ss())[permitted_byte_simp] 266 THEN Cases_on `q` 267 THEN Cases_on `q'` 268 THEN (TRY (Cases_on `q''`)) 269 THEN FULL_SIMP_TAC (srw_ss()) [] 270 THEN (NO_TAC ORELSE METIS_TAC [])); 271 272 273val check_accesses_simp = store_thm ( 274 "check_accesses_simp", 275 ``!u a add acc c1 c2 c3 priv mem. 276 ((u,a,add) = check_accesses acc c1 c2 c3 priv mem) /\ u 277 ==> (check_accesses_pure acc c1 c2 c3 priv mem = a)``, 278 Induct_on `acc` 279 THENL [RW_TAC (srw_ss()) [check_accesses_def, check_accesses_pure_def], 280 ONCE_REWRITE_TAC [check_accesses_def, check_accesses_pure_def] 281 THEN FULL_SIMP_TAC (srw_ss()) [LET_DEF] 282 THEN NTAC 8 STRIP_TAC 283 THEN CASE_TAC 284 THENL [check_accesses_TAC ("F"), check_accesses_TAC ("T")] 285 ]); 286 287 288 289 290(* conclude the understandability of check_accesses from the understandability of permitted_byte *) 291 292val check_accesses_understand = store_thm ( 293 "check_accesses_understand", 294 ``!acc c1 c2 c3 priv mem. 295 (!add is_write. FST (permitted_byte add is_write c1 c2 c3 priv mem)) 296 ==> (FST (check_accesses acc c1 c2 c3 priv mem))``, 297 Induct_on `acc` 298 THENL [RW_TAC (srw_ss()) [check_accesses_def], 299 ONCE_REWRITE_TAC [check_accesses_def] 300 THEN FULL_SIMP_TAC (srw_ss()) [LET_DEF] 301 THEN STRIP_TAC 302 THEN CASE_TAC 303 THEN PairRules.PBETA_TAC 304 THEN RW_TAC (srw_ss()) [] 305 ]); 306 307 308 309(* access_violation_full *) 310 311 312val access_violation_full_def = Define `access_violation_full s = check_accesses s.accesses 313 s.coprocessors.state.cp15.C1 314 s.coprocessors.state.cp15.C2 315 s.coprocessors.state.cp15.C3 316 F 317 s.memory`; 318 319(* empty access list, no violation *) 320 321val empty_accesses_full_lem = store_thm( 322 "empty_accesses_full_lem", 323 ``(s.accesses = []) ==> ((access_violation_full s) = (T,F, ARB))``, 324 NTAC 2 (PURE_ONCE_REWRITE_TAC [access_violation_full_def, check_accesses_def]) 325 THEN RW_TAC (srw_ss()) []); 326 327 328 329(* access_violation_pure *) 330 331 332val access_violation_pure_def = Define `access_violation_pure s = check_accesses_pure s.accesses 333 s.coprocessors.state.cp15.C1 334 s.coprocessors.state.cp15.C2 335 s.coprocessors.state.cp15.C3 336 F 337 338 s.memory`; 339 340(* relate access_violation_pure and access_violation_full *) 341 342val access_violation_simp_pure= store_thm( 343 "access_violation_simp_pure", 344 ``!u a add s. 345 ((u,a,add) = access_violation_full s) /\ u 346 ==> (access_violation_pure s = a)``, 347 FULL_SIMP_TAC (srw_ss()) [access_violation_full_def, access_violation_pure_def] 348 THEN METIS_TAC [check_accesses_simp]); 349 350 351(* partially specified access_violation *) 352 353(*new_constant("access_violation", ``:arm_state -> bool``);*) 354 355val access_violation_def = new_axiom("access_violation_axiom", ``!state u x add. 356 ((u,x,add) = access_violation_full state) /\ u 357 ==> (access_violation state = x) ``); 358 359 360(* if full version is understood, access_violation is equal to pure version *) 361 362val access_violation_simp = store_thm ( 363 "access_violation_simp", 364 ``!s x add. 365 ((T,x,add) = access_violation_full s) 366 ==> (access_violation s = access_violation_pure s)``, 367 METIS_TAC [access_violation_simp_pure, access_violation_def]); 368 369val access_violation_simp_FST = store_thm ( 370 "access_violation_simp_FST", 371 ``!s. (FST (access_violation_full s)) 372 ==> (access_violation s = access_violation_pure s)``, 373 REPEAT STRIP_TAC 374 THEN Cases_on `access_violation_full s` 375 THEN Cases_on `r` 376 THEN FULL_SIMP_TAC (srw_ss()) [access_violation_simp]); 377 378(* empty access list, no violation *) 379 380val empty_accesses_lem = store_thm( 381 "empty_accesses_lem", 382 ``(s.accesses = []) ==> (~access_violation s)``, 383 STRIP_TAC 384 THEN IMP_RES_TAC empty_accesses_full_lem 385 THEN ASSUME_TAC (SPECL [``s:arm_state``, ``T``, ``F``, ``ARB:word32``] access_violation_def) 386 THEN FULL_SIMP_TAC (srw_ss()) []); 387 388(* take data abort exception *) 389 390val _ = temp_overload_on ("unit4", ``\( u1:unit,u2:unit,u3:unit,u4:unit). constT ()``); 391 392(* mmu_arm_next *) 393 394val _ = numLib.prefer_num(); 395val _ = wordsLib.prefer_word(); 396 397(*val _ = temp_overload_on (parmonadsyntax.monad_bind, ``seqT``);*) 398val _ = temp_overload_on (parmonadsyntax.monad_par, ``parT``); 399val _ = temp_overload_on ("return", ``constT``); 400 401val _ = temp_overload_on ("PAD0", ``list$PAD_LEFT #"0"``); 402 403 404val mmu_arm_next_def = Define `mmu_arm_next irpt state = 405 if irpt = NoInterrupt then 406 ( 407 case (waiting_for_interrupt <|proc:=0|> (state with accesses := [])) of 408 Error e => Error e 409 | ValueState wfi wfi_state => 410 ( 411 if (wfi) then ValueState () wfi_state 412 else 413 ( 414 case (fetch_instruction <|proc:=0|> (\a. read_memA <|proc:=0|> (a, 4) >>= (\d. return (word32 d))) 415 (\a. read_memA <|proc:=0|> (a, 2) >>= (\d. return (word16 d))) 416 (wfi_state with accesses := [])) of 417 Error e => Error e 418 | ValueState (opc,instr) fetched_state => 419 ( 420 if access_violation fetched_state then 421 take_prefetch_abort_exception <| proc := 0 |> (fetched_state with accesses := []) 422 else 423 case arm_instr <|proc:=0|> instr (fetched_state with accesses := []) of 424 Error e => Error e 425 | ValueState x end_state => 426 ( 427 if access_violation end_state then 428 take_data_abort_exception <| proc := 0 |> (end_state with accesses := []) 429 else 430 ValueState () end_state 431 ) 432 ) 433 ) 434 ) 435 436 ) 437 else 438 (((if irpt = HW_Reset then 439 take_reset <|proc:=0|> 440 else if irpt = HW_Fiq then 441 take_fiq_exception <|proc:=0|> 442 else (* irpt = HW_Irq *) 443 take_irq_exception <|proc:=0|>) >>= 444 (\u:unit. clear_wait_for_interrupt <|proc:=0|>)) (state with accesses := []))`; 445 446 447val _ = export_theory(); 448 449 450