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