1(* ========================================================================= *)
2(* FILE          : instructionScript.sml                                     *)
3(* DESCRIPTION   : Datatype for ARM instructions, and an encoder -> word32   *)
4(*                                                                           *)
5(* AUTHORS       : (c) Anthony Fox, University of Cambridge                  *)
6(* DATE          : 2006 - 2007                                               *)
7(* ========================================================================= *)
8
9(* interactive use:
10  app load ["wordsTheory", "armTheory"];
11*)
12
13open HolKernel boolLib Parse bossLib;
14open Q wordsTheory armTheory;
15
16val _ = new_theory "instruction";
17
18(* ------------------------------------------------------------------------- *)
19
20val _ = Hol_datatype`
21  shift =
22    LSL of word4
23  | LSR of word4
24  | ASR of word4
25  | ROR of word4`;
26
27val _ = Hol_datatype
28  `addr_mode1 =
29     Dp_immediate of word4=>word8
30   | Dp_shift_immediate of shift=>word5
31   | Dp_shift_register of shift=>word4`;
32
33val _ = Hol_datatype
34  `addr_mode2 =
35     Dt_immediate of word12
36   | Dt_shift_immediate of shift=>word5`;
37
38val _ = Hol_datatype
39  `addr_mode3 =
40     Dth_immediate of word8
41   | Dth_register of word4`;
42
43val _ = Hol_datatype
44  `msr_mode =
45     Msr_immediate of word4=>word8
46   | Msr_register of word4`;
47
48val _ = Hol_datatype
49  `msr_psr = CPSR_c | CPSR_f | CPSR_a | SPSR_c | SPSR_f | SPSR_a`;
50
51val _ = Hol_datatype
52  `transfer_options = <| Pre : bool; Up : bool; Wb : bool |>`;
53
54val _ = Hol_datatype
55 `arm_instruction =
56    B of condition=>word24
57  | BL of condition=>word24
58  | SWI of condition
59  | AND of condition=>bool=>word4=>word4=>addr_mode1
60  | EOR of condition=>bool=>word4=>word4=>addr_mode1
61  | SUB of condition=>bool=>word4=>word4=>addr_mode1
62  | RSB of condition=>bool=>word4=>word4=>addr_mode1
63  | ADD of condition=>bool=>word4=>word4=>addr_mode1
64  | ADC of condition=>bool=>word4=>word4=>addr_mode1
65  | SBC of condition=>bool=>word4=>word4=>addr_mode1
66  | RSC of condition=>bool=>word4=>word4=>addr_mode1
67  | TST of condition=>word4=>addr_mode1
68  | TEQ of condition=>word4=>addr_mode1
69  | CMP of condition=>word4=>addr_mode1
70  | CMN of condition=>word4=>addr_mode1
71  | ORR of condition=>bool=>word4=>word4=>addr_mode1
72  | MOV of condition=>bool=>word4=>addr_mode1
73  | BIC of condition=>bool=>word4=>word4=>addr_mode1
74  | MVN of condition=>bool=>word4=>addr_mode1
75  | MUL of condition=>bool=>word4=>word4=>word4
76  | MLA of condition=>bool=>word4=>word4=>word4=>word4
77  | UMULL of condition=>bool=>word4=>word4=>word4=>word4
78  | UMLAL of condition=>bool=>word4=>word4=>word4=>word4
79  | SMULL of condition=>bool=>word4=>word4=>word4=>word4
80  | SMLAL of condition=>bool=>word4=>word4=>word4=>word4
81  | LDRH of condition=>bool=>bool=>transfer_options=>word4=>word4=>addr_mode3
82  | STRH of condition=>transfer_options=>word4=>word4=>addr_mode3
83  | LDR of condition=>bool=>transfer_options=>word4=>word4=>addr_mode2
84  | STR of condition=>bool=>transfer_options=>word4=>word4=>addr_mode2
85  | LDM of condition=>bool=>transfer_options=>word4=>word16
86  | STM of condition=>bool=>transfer_options=>word4=>word16
87  | SWP of condition=>bool=>word4=>word4=>word4
88  | MRS of condition=>bool=>word4
89  | MSR of condition=>msr_psr=>msr_mode
90  | CDP of condition=>word4=>word4=>word4=>word4=>word4=>word3
91  | LDC of condition=>bool=>transfer_options=>word4=>word4=>word4=>word8
92  | STC of condition=>bool=>transfer_options=>word4=>word4=>word4=>word8
93  | MRC of condition=>word4=>word3=>word4=>word4=>word4=>word3
94  | MCR of condition=>word4=>word3=>word4=>word4=>word4=>word3
95  | UND of condition`;
96
97(* ------------------------------------------------------------------------- *)
98
99val condition_encode_def = Define`
100  condition_encode cond =
101    (w2w (n2w (condition2num cond):word4 #<< 1) << 28):word32`;
102
103val shift_encode_def = Define`
104  (shift_encode (LSL Rm) = (w2w Rm):word32) /\
105  (shift_encode (LSR Rm) = 0x20w || w2w Rm) /\
106  (shift_encode (ASR Rm) = 0x40w || w2w Rm) /\
107  (shift_encode (ROR Rm) = 0x60w || w2w Rm)`;
108
109val addr_mode1_encode_def = Define`
110  addr_mode1_encode op2 =
111   case op2 of
112     Dp_immediate rot imm => (0x2000000w || w2w rot << 8 || w2w imm):word32
113   | Dp_shift_immediate shift amount => w2w amount << 7 || shift_encode shift
114   | Dp_shift_register shift Rs => 0x10w || w2w Rs << 8 || shift_encode shift`;
115
116val addr_mode2_encode_def = Define`
117  addr_mode2_encode op2 =
118   case op2 of
119     Dt_immediate imm => (w2w imm):word32
120   | Dt_shift_immediate shift amount =>
121        0x2000000w || w2w amount << 7 || shift_encode shift`;
122
123val addr_mode3_encode_def = Define`
124  addr_mode3_encode op2 =
125   case op2 of
126     Dth_immediate imm => 0x400000w || ((7 >< 4) imm) << 8 || ((3 >< 0) imm)
127   | Dth_register Rm => (w2w Rm):word32`;
128
129val msr_mode_encode_def = Define`
130  msr_mode_encode op =
131   case op of
132     Msr_immediate rot imm => (0x2000000w || w2w rot << 8 || w2w imm):word32
133   | Msr_register Rm => w2w Rm`;
134
135val msr_psr_encode_def = Define`
136  (msr_psr_encode CPSR_c = 0x10000w:word32) /\
137  (msr_psr_encode CPSR_f = 0x80000w) /\
138  (msr_psr_encode CPSR_a = 0x90000w) /\
139  (msr_psr_encode SPSR_c = 0x410000w) /\
140  (msr_psr_encode SPSR_f = 0x480000w) /\
141  (msr_psr_encode SPSR_a = 0x490000w)`;
142
143val options_encode_def = Define`
144  options_encode x opt =
145    word_modify (\i b. (i = 24) /\ opt.Pre \/ (i = 23) /\ opt.Up \/
146                       (i = 22) /\ x \/ (i = 21) /\ opt.Wb) (0w:word32)`;
147
148val options_encode2_def = Define`
149  options_encode2 h opt =
150    word_modify (\i b. (i = 24) /\ opt.Pre \/ (i = 23) /\ opt.Up \/
151                       (i = 21) /\ opt.Wb \/ (i = 5) /\ h) (0w:word32)`;
152
153val data_proc_encode_def = Define`
154  data_proc_encode cond (op:word4) s (Rn:word4) (Rd:word4) Op2 =
155    condition_encode cond || w2w op << 21 || (if s then 0x100000w else 0w) ||
156       w2w Rn << 16 || w2w Rd << 12 || addr_mode1_encode Op2`;
157
158val instruction_encode_def = with_flag (priming, SOME "") Define`
159  instruction_encode i =
160    case i of
161      B  cond offset24 => condition_encode cond || 0xA000000w || w2w offset24
162    | BL cond offset24 => condition_encode cond || 0xB000000w || w2w offset24
163    | SWI cond => condition_encode cond || 0xF000000w
164    | AND cond s Rd Rn Op2 => data_proc_encode cond 0w s Rn Rd Op2
165    | EOR cond s Rd Rn Op2 => data_proc_encode cond 1w s Rn Rd Op2
166    | SUB cond s Rd Rn Op2 => data_proc_encode cond 2w s Rn Rd Op2
167    | RSB cond s Rd Rn Op2 => data_proc_encode cond 3w s Rn Rd Op2
168    | ADD cond s Rd Rn Op2 => data_proc_encode cond 4w s Rn Rd Op2
169    | ADC cond s Rd Rn Op2 => data_proc_encode cond 5w s Rn Rd Op2
170    | SBC cond s Rd Rn Op2 => data_proc_encode cond 6w s Rn Rd Op2
171    | RSC cond s Rd Rn Op2 => data_proc_encode cond 7w s Rn Rd Op2
172    | TST cond Rn Op2      => data_proc_encode cond 8w T Rn 0w Op2
173    | TEQ cond Rn Op2      => data_proc_encode cond 9w T Rn 0w Op2
174    | CMP cond Rn Op2      => data_proc_encode cond 10w T Rn 0w Op2
175    | CMN cond Rn Op2      => data_proc_encode cond 11w T Rn 0w Op2
176    | ORR cond s Rd Rn Op2 => data_proc_encode cond 12w s Rn Rd Op2
177    | MOV cond s Rd Op2    => data_proc_encode cond 13w s 0w Rd Op2
178    | BIC cond s Rd Rn Op2 => data_proc_encode cond 14w s Rn Rd Op2
179    | MVN cond s Rd Op2    => data_proc_encode cond 15w s 0w Rd Op2
180    | MUL cond s Rd Rm Rs =>
181         condition_encode cond || (if s then 0x100090w else 0x90w) ||
182         w2w Rd << 16 || w2w Rs << 8 || w2w Rm
183    | MLA cond s Rd Rm Rs Rn =>
184         condition_encode cond || (if s then 0x300090w else 0x200090w) ||
185         w2w Rd << 16 || w2w Rn << 12 || w2w Rs << 8 || w2w Rm
186    | UMULL cond s RdLo RdHi Rm Rs =>
187         condition_encode cond || (if s then 0x900090w else 0x800090w) ||
188         w2w RdHi << 16 || w2w RdLo << 12 || w2w Rs << 8 || w2w Rm
189    | UMLAL cond s RdLo RdHi Rm Rs =>
190         condition_encode cond || (if s then 0xB00090w else 0xA00090w) ||
191         w2w RdHi << 16 || w2w RdLo << 12 || w2w Rs << 8 || w2w Rm
192    | SMULL cond s RdLo RdHi Rm Rs =>
193         condition_encode cond || (if s then 0xD00090w else 0xC00090w) ||
194         w2w RdHi << 16 || w2w RdLo << 12 || w2w Rs << 8 || w2w Rm
195    | SMLAL cond s RdLo RdHi Rm Rs =>
196         condition_encode cond || (if s then 0xF00090w else 0xE00090w) ||
197         w2w RdHi << 16 || w2w RdLo << 12 || w2w Rs << 8 || w2w Rm
198    | LDRH cond s h options Rd Rn mode3 =>
199         condition_encode cond || (if s then 0x1000D0w else 0x100090w) ||
200         options_encode2 (h \/ (~h /\ ~s)) options ||
201         w2w Rn << 16 || w2w Rd << 12 || addr_mode3_encode mode3
202    | STRH cond options Rd Rn mode3 =>
203         condition_encode cond || 0x90w || options_encode2 T options ||
204         w2w Rn << 16 || w2w Rd << 12 || addr_mode3_encode mode3
205    | LDR cond b options Rd Rn offset =>
206         condition_encode cond || 0x4100000w || options_encode b options ||
207         w2w Rn << 16 || w2w Rd << 12 || addr_mode2_encode offset
208    | STR cond b options Rd Rn offset =>
209         condition_encode cond || 0x4000000w || options_encode b options ||
210         w2w Rn << 16 || w2w Rd << 12 || addr_mode2_encode offset
211    | LDM cond s options Rn list =>
212         condition_encode cond || 0x8100000w || options_encode s options ||
213         w2w Rn << 16 || w2w list
214    | STM cond s options Rn list =>
215         condition_encode cond || 0x8000000w || options_encode s options ||
216         w2w Rn << 16 || w2w list
217    | SWP cond b Rd Rm Rn =>
218         condition_encode cond || (if b then 0x1400090w else 0x1000090w) ||
219         w2w Rn << 16 || w2w Rd << 12 || w2w Rm
220    | MRS cond R Rd =>
221         condition_encode cond || (if R then 0x14F0000w else 0x10F0000w) ||
222         w2w Rd << 12
223    | MSR cond psrd Op =>
224         condition_encode cond || 0x120F000w || msr_psr_encode psrd ||
225         (msr_mode_encode Op)
226    | CDP cond CPn Cop1 CRd CRn CRm Cop2 =>
227         condition_encode cond || 0xE000000w || w2w Cop1 << 20 ||
228         w2w CRn << 16 || w2w CRd << 12 || w2w CPn << 8 ||
229         w2w Cop2 << 5 || w2w CRm
230    | LDC cond n options CPn CRd Rn offset8 =>
231         condition_encode cond || 0xC100000w || options_encode n options ||
232         w2w Rn << 16 || w2w CRd << 12 || w2w CPn << 8 || w2w offset8
233    | STC cond n options CPn CRd Rn offset8 =>
234         condition_encode cond || 0xC000000w || options_encode n options ||
235         w2w Rn << 16 || w2w CRd << 12 || w2w CPn << 8 || w2w offset8
236    | MRC cond CPn Cop1b Rd CRn CRm Cop2 =>
237         condition_encode cond || 0xE100010w || w2w Cop1b << 21 ||
238         w2w CRn << 16 || w2w Rd << 12 || w2w CPn << 8 ||
239         w2w Cop2 << 5 || w2w CRm
240    | MCR cond CPn Cop1b Rd CRn CRm Cop2 =>
241         condition_encode cond || 0xE000010w || w2w Cop1b << 21 ||
242         w2w CRn << 16 || w2w Rd << 12 || w2w CPn << 8 ||
243         w2w Cop2 << 5 || w2w CRm
244    | UND cond => condition_encode cond || 0x6000010w`;
245
246val _ = overload_on("enc", ``instruction_encode``);
247
248(* ------------------------------------------------------------------------- *)
249
250val _ = export_theory();
251