1(* ========================================================================= *)
2(* FILE          : arm_emitScript.sml                                        *)
3(* DATE          : 2005 - 2009                                               *)
4(* ========================================================================= *)
5
6(* interactive use:
7  app load ["wordsLib", "wordsSyntax", "systemTheory", "basis_emitTheory"];
8*)
9
10open HolKernel boolLib bossLib Parse;
11open Q updateTheory armTheory systemTheory;
12open EmitML basis_emitTheory;
13
14val _ = new_theory "arm_emit";
15
16val _ = numLib.prefer_num();
17val _ = wordsLib.prefer_word();
18
19(*---------------------------------------------------------------------------*)
20
21val num2register = prove(
22  `!n. num2register n =
23         if n = 0 then r0 else
24         if n = 1 then r1 else
25         if n = 2 then r2 else
26         if n = 3 then r3 else
27         if n = 4 then r4 else
28         if n = 5 then r5 else
29         if n = 6 then r6 else
30         if n = 7 then r7 else
31         if n = 8 then r8 else
32         if n = 9 then r9 else
33         if n = 10 then r10 else
34         if n = 11 then r11 else
35         if n = 12 then r12 else
36         if n = 13 then r13 else
37         if n = 14 then r14 else
38         if n = 15 then r15 else
39         if n = 16 then r8_fiq else
40         if n = 17 then r9_fiq else
41         if n = 18 then r10_fiq else
42         if n = 19 then r11_fiq else
43         if n = 20 then r12_fiq else
44         if n = 21 then r13_fiq else
45         if n = 22 then r14_fiq else
46         if n = 23 then r13_irq else
47         if n = 24 then r14_irq else
48         if n = 25 then r13_svc else
49         if n = 26 then r14_svc else
50         if n = 27 then r13_abt else
51         if n = 28 then r14_abt else
52         if n = 29 then r13_und else
53         if n = 30 then r14_und else
54           FAIL num2register ^(mk_var("30 < n",bool)) n`,
55  SRW_TAC [] [num2register_thm, combinTheory.FAIL_THM]);
56
57val num2condition = prove(
58  `!n. num2condition n =
59         if n = 0 then EQ else
60         if n = 1 then CS else
61         if n = 2 then MI else
62         if n = 3 then VS else
63         if n = 4 then HI else
64         if n = 5 then GE else
65         if n = 6 then GT else
66         if n = 7 then AL else
67         if n = 8 then NE else
68         if n = 9 then CC else
69         if n = 10 then PL else
70         if n = 11 then VC else
71         if n = 12 then LS else
72         if n = 13 then LT else
73         if n = 14 then LE else
74         if n = 15 then NV else
75           FAIL num2condition ^(mk_var("15 < n",bool)) n`,
76  SRW_TAC [] [num2condition_thm, combinTheory.FAIL_THM]);
77
78val register_decl = `register =
79 r0     | r1     | r2      | r3      | r4      | r5      | r6      | r7  |
80 r8     | r9     | r10     | r11     | r12     | r13     | r14     | r15 |
81 r8_fiq | r9_fiq | r10_fiq | r11_fiq | r12_fiq | r13_fiq | r14_fiq |
82                                                 r13_irq | r14_irq |
83                                                 r13_svc | r14_svc |
84                                                 r13_abt | r14_abt |
85                                                 r13_und | r14_und`;
86
87val psr_decl =
88  `psr = CPSR | SPSR_fiq | SPSR_irq | SPSR_svc | SPSR_abt | SPSR_und`;
89
90val exceptions_decl = `exceptions = reset | undefined | software | pabort |
91                                    dabort | address |interrupt | fast`;
92
93val mode_decl = `mode = usr | fiq | irq | svc | abt | und | sys | safe`;
94
95val condition_decl = `condition = EQ | CS | MI | VS | HI | GE | GT | AL |
96                                  NE | CC | PL | VC | LS | LT | LE | NV`;
97
98val iclass_decl = `iclass = swp | mrs | msr | data_proc | mla_mul |
99                            ldr_str | ldrh_strh | ldm_stm | br | swi_ex |
100                            cdp_und | mcr | mrc | ldc_stc | unexec`;
101
102val n2w_w2n_rule = GEN_ALL o SIMP_RULE bool_ss [wordsTheory.n2w_w2n];
103
104val spec_word_rule16 = n2w_w2n_rule o Q.SPEC `w2n (w:word16)`;
105val spec_word_rule32 = n2w_w2n_rule o Q.SPEC `w2n (w:word32)`;
106
107val spec_word_rule12 =
108  n2w_w2n_rule o INST [`opnd2` |-> `w2n (w:word12)`] o SPEC_ALL;
109
110val mem_rule = REWRITE_RULE [GSYM mem_read_def, GSYM mem_write_def];
111
112fun mk_word n =
113  let val s = Int.toString n
114      val w = "type word" ^ s ^ " = wordsML.word" ^ s
115  in
116    MLSIG w
117  end;
118
119val _ = eSML "update"
120  (OPEN ["num", "sum", "fcp", "words"]
121    :: MLSIG "type 'a word = 'a wordsML.word"
122    :: MLSIG "type num = numML.num"
123    :: MLSIG "type word2 = wordsML.word2"
124    :: MLSIG "type word8 = wordsML.word8"
125    :: MLSIG "type word16 = wordsML.word16"
126    :: MLSIG "type word30 = wordsML.word30"
127    :: MLSIG "type word32 = wordsML.word32"
128    :: MLSTRUCT "type mem = word30->word32"
129    :: MLSIG "type mem"
130    :: MLSTRUCT "val mem_updates = ref ([]: word30 list)"
131    :: MLSIG "val mem_updates : word30 list ref"
132    :: DATATYPE (`formats = SignedByte | UnsignedByte
133                          | SignedHalfWord | UnsignedHalfWord
134                          | UnsignedWord`)
135    :: DATATYPE (`data = Byte word8 | Half word16 | Word word32`)
136    :: map DEFN [LUPDATE_def, mem_read_def, mem_write_def, mem_write_block_def]
137     @ map (DEFN o mem_rule)
138        [empty_memory_def, mem_items_def, addr30_def, GET_HALF_def,
139         SIMP_RULE std_ss [literal_case_DEF] GET_BYTE_def,
140         FORMAT_def, SET_BYTE_def, SET_HALF_def,
141         MEM_WRITE_BYTE_def, MEM_WRITE_HALF_def,
142         MEM_WRITE_WORD_def, MEM_WRITE_def]);
143
144val _ = eSML "arm"
145  (OPEN ["num", "sum", "option", "set", "fcp", "list", "rich_list",
146         "bit", "words", "update"]
147    :: MLSIG "type 'a itself = 'a fcpML.itself"
148    :: MLSIG "type 'a word = 'a wordsML.word"
149    :: MLSIG "type ('a,'b) cart = ('a,'b) fcpML.cart"
150    :: MLSIG "type ('a,'b) sum = ('a,'b) sumML.sum"
151    :: MLSIG "type 'a bit0 = 'a fcpML.bit0"
152    :: MLSIG "type 'a bit1 = 'a fcpML.bit1"
153    :: MLSIG "type num = numML.num"
154    :: map (fn decl => DATATYPE decl)
155           [register_decl, psr_decl, mode_decl, condition_decl]
156     @ map (fn decl => EQDATATYPE ([], decl)) [exceptions_decl,iclass_decl]
157     @ DATATYPE (`state_inp = <| state : 'a; inp : num -> 'b |>`)
158    :: DATATYPE (`state_out = <| state : 'a; out : 'b |>`)
159    :: map mk_word [2,3,4,5,8,12,16,24,30,32]
160     @ MLSTRUCT "type registers = register->word32"
161    :: MLSTRUCT "type psrs = psr->word32"
162    :: MLSTRUCT "type mem = updateML.mem"
163    :: MLSTRUCT "type data = updateML.data"
164    :: MLSIG "type registers = register->word32"
165    :: MLSIG "type psrs = psr->word32"
166    :: MLSIG "type mem = updateML.mem"
167    :: MLSIG "type data = updateML.data"
168    :: DATATYPE (`regs = <| reg : registers; psr : psrs |>`)
169    :: DATATYPE (`memop = MemRead word32 | MemWrite word32 data |
170                          CPWrite word32`)
171    :: DATATYPE (`arm_state = <| regs : regs; ireg : word32;
172                                 exception : exceptions |>`)
173    :: DATATYPE (`arm_output = <| transfers : memop list;
174                                  cpi : bool; user : bool |>`)
175    :: DATATYPE (`cp_output = <| data : word32 option list; absent : bool |>`)
176    :: DATATYPE (`bus = <| data : word32 list; memory : mem; abort : num option;
177                           cp_state : 'a |>`)
178    :: DATATYPE (`arm_sys_state = <| registers : registers; psrs : psrs;
179                        memory : mem; undefined : bool; cp_state : 'a |>`)
180    :: DATATYPE (`interrupt = Reset regs | Undef | Prefetch |
181                              Dabort num | Fiq | Irq`)
182    :: DATATYPE (`arm_input = <| ireg : word32; data : word32 list;
183                                 interrupt : interrupt option; no_cp : bool |>`)
184    :: DATATYPE (`coproc =
185           <| absent : bool -> word32 -> bool;
186              f_cdp  : 'a -> bool -> word32 -> 'a;
187              f_mrc  : 'a -> bool -> word32 -> word32;
188              f_mcr  : 'a -> bool -> word32 -> word32 -> 'a;
189              f_stc  : 'a -> bool -> word32 -> word32 option list;
190              f_ldc  : 'a -> bool -> word32 -> word32 list -> 'a;
191              n_ldc  : 'a -> bool -> word32 -> num |>`)
192    :: MLSTRUCT "val mem_updates = ref ([]: word30 list)"
193    :: MLSIG "val mem_updates : word30 list ref"
194    :: map DEFN (map spec_word_rule32
195         [DECODE_PSR_THM, DECODE_BRANCH_THM, DECODE_DATAP_THM,
196          DECODE_MRS_THM, DECODE_MSR_THM, DECODE_LDR_STR_THM,
197           DECODE_MLA_MUL_THM, DECODE_LDM_STM_THM, DECODE_SWP_THM,
198           DECODE_LDC_STC_THM, DECODE_LDRH_STRH_THM, DECODE_CDP_THM,
199           DECODE_MRC_MCR_THM]
200       @ [DECODE_CPN_def, DECODE_CP_def, USER_def, mode_reg2num_def,
201          DECODE_ARM_def, mode_num_def, exceptions2num_thm, register2num_thm,
202          num2register, num2condition, SET_IFMODE_def,
203          REG_READ_def, REG_WRITE_def, INC_PC_def, FETCH_PC_def,
204          SET_NZCV_def, SET_NZC_def, SET_NZ_def,
205          SIMP_RULE std_ss [literal_case_DEF] DECODE_MODE_def,
206          NZCV_def, CARRY_def, mode2psr_def, SPSR_READ_def, CPSR_READ_def,
207          CPSR_WRITE_def, SPSR_WRITE_def, exception2mode_def,
208          SPECL [`r`,`e`]  EXCEPTION_def, BRANCH_def, LSL_def, LSR_def,
209          ASR_def, ROR_def, IMMEDIATE_def, SHIFT_IMMEDIATE2_def,
210          SHIFT_REGISTER2_def, spec_word_rule12 SHIFT_IMMEDIATE_THM,
211          spec_word_rule12 SHIFT_REGISTER_THM, ADDR_MODE1_def,
212          SPEC `f` ALU_arith_def, ALU_logic_def,
213          ADD_def, SUB_def, AND_def, EOR_def, ORR_def,
214          ALU_def, ARITHMETIC_def, TEST_OR_COMP_def, DATA_PROCESSING_def,
215          MRS_def, MSR_def, ALU_multiply_def, MLA_MUL_def,
216          UP_DOWN_def, ADDR_MODE2_def, IMP_DISJ_THM, LDR_STR_def,
217          ADDR_MODE3_def, LDRH_STRH_def,spec_word_rule16 REGISTER_LIST_THM,
218          ADDRESS_LIST_def, WB_ADDRESS_def, FIRST_ADDRESS_def,
219          ADDR_MODE4_def, LDM_LIST_def, STM_LIST_def, LDM_STM_def,
220          SWP_def, MRC_def, MCR_OUT_def, ADDR_MODE5_def, LDC_STC_def,
221          CONDITION_PASSED2_def, CONDITION_PASSED_def,
222          RUN_ARM_def, IS_Reset_def, PROJ_Dabort_def, PROJ_Reset_def ,
223          interrupt2exception_def, PROJ_IF_FLAGS_def, NEXT_ARM_def,
224          OUT_ARM_def, mem_rule TRANSFER_def, TRANSFERS_def,
225          OUT_CP_def, RUN_CP_def, mem_rule NEXT_ARM_MMU,
226          mem_rule NEXT_ARM_MEM, empty_registers_def]));
227
228(* -------------------------------------------------------------------------- *)
229
230val _ = export_theory();
231