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