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