1(* ------------------------------------------------------------------------ *)
2(*  Support running ARM model with a Patricia tree program memory           *)
3(* ------------------------------------------------------------------------ *)
4
5(* interactive use:
6  app load ["arm_decoderTheory", "armTheory", "wordsLib",
7            "patriciaTheory", "parmonadsyntax"];
8*)
9
10open HolKernel boolLib bossLib Parse;
11
12open patriciaTheory arm_coretypesTheory arm_astTheory arm_seq_monadTheory
13     arm_decoderTheory arm_opsemTheory armTheory;
14
15val _ = new_theory "arm_eval";
16
17(* ------------------------------------------------------------------------ *)
18
19val _ = numLib.prefer_num();
20val _ = wordsLib.prefer_word();
21
22infix \\ << >>
23
24val op \\ = op THEN;
25val op << = op THENL;
26val op >> = op THEN1;
27
28val _ = temp_overload_on (parmonadsyntax.monad_bind, ``seqT``);
29val _ = temp_overload_on (parmonadsyntax.monad_par,  ``parT``);
30val _ = temp_overload_on ("return", ``constT``);
31
32(* ------------------------------------------------------------------------ *)
33
34val ptree_read_word_def = Define`
35  ptree_read_word (prog:word8 ptree) (a:word32) : word32 M =
36  let pc = w2n a in
37   (case prog ' pc
38    of SOME b1 =>
39       (case prog ' (pc + 1)
40        of SOME b2 =>
41           (case prog ' (pc + 2)
42            of SOME b3 =>
43               (case prog ' (pc + 3)
44                of SOME b4 => constT (word32 [b1; b2; b3; b4])
45                 | NONE => errorT "couldn't fetch an instruction")
46             | NONE => errorT "couldn't fetch an instruction")
47         | NONE => errorT "couldn't fetch an instruction")
48     | NONE => errorT "couldn't fetch an instruction")`;
49
50val ptree_read_halfword_def = Define`
51  ptree_read_halfword (prog:word8 ptree) (a:word32) : word16 M =
52  let pc = w2n a in
53    case prog ' pc
54    of SOME b1 =>
55       (case prog ' (pc + 1)
56        of SOME b2 => constT (word16 [b1; b2])
57         | NONE => errorT "couldn't fetch an instruction")
58     | NONE => errorT "couldn't fetch an instruction"`;
59
60val ptree_arm_next_def = zDefine
61  `ptree_arm_next ii (x:string # Encoding # word4 # ARMinstruction)
62     (pc:word32) (cycle:num) : unit M =
63   arm_instr ii (SND x)`;
64
65val attempt_def = Define`
66  attempt c f g =
67  \s:arm_state.
68      case f s
69      of Error e => ValueState (c, e) s
70       | ValueState v s' => g v s'`;
71
72val ptree_arm_loop_def = Define`
73  ptree_arm_loop ii cycle prog t : (num # string) M =
74    if t = 0 then
75      constT (cycle, "finished")
76    else
77      attempt cycle
78        (fetch_instruction ii (ptree_read_word prog) (ptree_read_halfword prog))
79        (\x.
80          read_pc ii >>=
81          (\pc:word32.
82              ptree_arm_next ii x pc cycle >>=
83              (\u:unit.
84                 ptree_arm_loop ii (cycle + 1) prog (t - 1))))`;
85
86val ptree_arm_run_def = Define`
87  ptree_arm_run prog state t =
88    case ptree_arm_loop <| proc := 0 |> 0 prog t state
89    of Error e => (e, NONE)
90     | ValueState (c,v) s =>
91          ("at cycle " ++ num_to_dec_string c ++ ": " ++ v, SOME s)`;
92
93(* ------------------------------------------------------------------------ *)
94
95val proc_def = zDefine `proc (n:num) f = \(i,x). if i = n then f x else ARB`;
96
97val mk_arm_state_def = Define`
98  mk_arm_state arch regs psrs md mem =
99    <| registers := proc 0 regs;
100       psrs := proc 0 psrs;
101       event_register := (K T);
102       interrupt_wait := (K F);
103       memory := (\a. case patricia$PEEK mem (w2n a)
104                        of SOME d => d
105                         | NONE => md);
106       accesses := [];
107       information := <| arch := arch;
108                         unaligned_support := T;
109                         extensions := {} |>;
110       coprocessors updated_by
111         (Coprocessors_state_fupd
112            (cp15_fupd (CP15reg_SCTLR_fupd
113              (\sctlr. sctlr with <| V := F; A := T; U := F;
114                                     IE := T; TE := F; NMFI := T;
115                                     EE := T; VE := F |>)) o
116             cp14_fupd (CP14reg_TEEHBR_fupd (K 0xF0000000w))));
117       monitors := <| ClearExclusiveByAddress := (K (constE ())) |> |>`;
118
119(* ------------------------------------------------------------------------ *)
120
121val registers_def = Define`
122   registers r0 r1 r2 r3 r4 r5 r6 r7 r8 r9 r10 r11 r12 r13
123             r14 r15 r16 r17 r18 r19 r20 r21 r22 r23 r24 r25
124             r26 r27 r28 r29 r30 r31 (r32:word32) =
125   \name.
126      RName_CASE
127         name r0 r1 r2 r3 r4 r5 r6 r7 r8 r9 r10 r11 r12 r13
128              r14 r15 r16 r17 r18 r19 r20 r21 r22 r23 r24 r25
129              r26 r27 r28 r29 r30 r31 r32`
130
131val psrs_def = Define`
132   psrs r0 r1 r2 r3 r4 r5 (r6:ARMpsr) =
133   \name. PSRName_CASE name r0 r1 r2 r3 r4 r5 r6`
134
135(* ------------------------------------------------------------------------ *)
136
137local
138  val tm1 = ``((n:num,r:RName) =+ d:word32)``
139
140  val tm2 =
141    ``proc n
142        (registers r0 r1 r2 r3 r4 r5 r6 r7 r8 r9 r10 r11 r12 r13
143                   r14 r15 r16 r17 r18 r19 r20 r21 r22 r23 r24 r25
144                   r26 r27 r28 r29 r30 r31 r32)``
145
146  fun reg n = mk_var ("r" ^ Int.toString n, ``:word32``)
147
148  fun reg_update (n,name) =
149        mk_eq (mk_comb (Term.subst [``r:RName`` |-> name] tm1, tm2),
150               Term.subst [reg n  |-> ``d:word32``] tm2)
151
152  val thm = list_mk_conj (map reg_update (Lib.zip (List.tabulate(33,I))
153           [``RName_0usr ``, ``RName_1usr ``, ``RName_2usr ``, ``RName_3usr``,
154            ``RName_4usr ``, ``RName_5usr ``, ``RName_6usr ``, ``RName_7usr``,
155            ``RName_8usr ``, ``RName_8fiq ``, ``RName_9usr ``, ``RName_9fiq``,
156            ``RName_10usr``, ``RName_10fiq``, ``RName_11usr``, ``RName_11fiq``,
157            ``RName_12usr``, ``RName_12fiq``,
158            ``RName_SPusr``, ``RName_SPfiq``, ``RName_SPirq``, ``RName_SPsvc``,
159            ``RName_SPabt``, ``RName_SPund``, ``RName_SPmon``,
160            ``RName_LRusr``, ``RName_LRfiq``, ``RName_LRirq``, ``RName_LRsvc``,
161            ``RName_LRabt``, ``RName_LRund``, ``RName_LRmon``, ``RName_PC``]))
162
163  val register_update = Tactical.prove(thm,
164    SRW_TAC [] [combinTheory.UPDATE_def, FUN_EQ_THM, registers_def, proc_def]
165      \\ Cases_on `x` \\ SRW_TAC [] [] \\ FULL_SIMP_TAC (srw_ss()) []
166      \\ Cases_on `r` \\ FULL_SIMP_TAC (srw_ss()) [])
167in
168  val register_update = save_thm("register_update", GEN_ALL register_update)
169end
170
171local
172  val tm1 = ``((n:num,p:PSRName) =+ d:ARMpsr)``
173  val tm2 = ``proc n (psrs r0 r1 r2 r3 r4 r5 r6)``;
174
175  fun psr n = mk_var ("r" ^ Int.toString n, ``:ARMpsr``)
176
177  fun psr_update (n,name) =
178        mk_eq (mk_comb (Term.subst [``p:PSRName`` |-> name] tm1, tm2),
179               Term.subst [psr n  |-> ``d:ARMpsr``] tm2)
180
181  val thm = list_mk_conj (map psr_update (Lib.zip (List.tabulate(7,I))
182           [``CPSR ``, ``SPSR_fiq ``, ``SPSR_irq ``, ``SPSR_svc``,
183            ``SPSR_mon``, ``SPSR_abt``, ``SPSR_und``]))
184
185  val psr_update = Tactical.prove(thm,
186    SRW_TAC [] [combinTheory.UPDATE_def, FUN_EQ_THM, psrs_def, proc_def]
187      \\ Cases_on `x` \\ SRW_TAC [] [] \\ FULL_SIMP_TAC (srw_ss()) []
188      \\ Cases_on `r` \\ FULL_SIMP_TAC (srw_ss()) [])
189in
190  val psr_update = save_thm("psr_update", GEN_ALL psr_update)
191end
192
193val proc = Q.store_thm("proc", `proc n f (n,x) = f x`, SRW_TAC [] [proc_def])
194
195val _ = computeLib.add_persistent_funs
196  ["combin.o_THM", "proc", "register_update", "psr_update"]
197
198(* ------------------------------------------------------------------------ *)
199
200val _ = export_theory ()
201