1(* m0 - generated by L3 - Thu Jun 22 15:54:54 2017 *)
2
3structure m0 :> m0 =
4struct
5
6structure Map = MutableMap
7
8(* -------------------------------------------------------------------------
9   Type declarations
10   ------------------------------------------------------------------------- *)
11
12type PRIMASK = { PM: bool, primask'rst: BitsN.nbit }
13
14type PSR =
15  { C: bool, ExceptionNumber: BitsN.nbit, N: bool, T: bool, V: bool,
16    Z: bool, psr'rst: BitsN.nbit }
17
18type CONTROL = { SPSEL: bool, control'rst: bool, nPRIV: bool }
19
20type AIRCR =
21  { ENDIANNESS: bool, SYSRESETREQ: bool, VECTCLRACTIVE: bool,
22    VECTKEY: BitsN.nbit, aircr'rst: BitsN.nbit }
23
24type CCR = { STKALIGN: bool, UNALIGN_TRP: bool, ccr'rst: BitsN.nbit }
25
26type SHPR2 = { PRI_11: BitsN.nbit, shpr2'rst: BitsN.nbit }
27
28type SHPR3 =
29  { PRI_14: BitsN.nbit, PRI_15: BitsN.nbit, shpr3'rst: BitsN.nbit }
30
31type IPR =
32  { PRI_N0: BitsN.nbit, PRI_N1: BitsN.nbit, PRI_N2: BitsN.nbit,
33    PRI_N3: BitsN.nbit, ipr'rst: BitsN.nbit }
34
35datatype Mode = Mode_Thread | Mode_Handler
36
37datatype ARM_Exception
38  = ExternalInterrupt of BitsN.nbit
39  | HardFault
40  | NMI
41  | PendSV
42  | Reset
43  | SVCall
44  | SysTick
45
46datatype RName
47  = RName_0 | RName_1 | RName_2 | RName_3 | RName_4 | RName_5 | RName_6
48  | RName_7 | RName_8 | RName_9 | RName_10 | RName_11 | RName_12
49  | RName_SP_main | RName_SP_process | RName_LR | RName_PC
50
51datatype SRType
52  = SRType_LSL | SRType_LSR | SRType_ASR | SRType_ROR | SRType_RRX
53
54datatype offset
55  = immediate_form of BitsN.nbit | register_form of BitsN.nbit
56
57datatype Hint
58  = Breakpoint of BitsN.nbit
59  | DataMemoryBarrier of BitsN.nbit
60  | DataSynchronizationBarrier of BitsN.nbit
61  | InstructionSynchronizationBarrier of BitsN.nbit
62  | SendEvent of unit
63  | WaitForEvent of unit
64  | WaitForInterrupt of unit
65  | Yield of unit
66
67datatype System
68  = ChangeProcessorState of bool
69  | MoveToRegisterFromSpecial of BitsN.nbit * BitsN.nbit
70  | MoveToSpecialRegister of BitsN.nbit * BitsN.nbit
71  | SupervisorCall of BitsN.nbit
72
73datatype Store
74  = Push of BitsN.nbit
75  | StoreByte of BitsN.nbit * (BitsN.nbit * offset)
76  | StoreHalf of BitsN.nbit * (BitsN.nbit * offset)
77  | StoreMultiple of BitsN.nbit * BitsN.nbit
78  | StoreWord of BitsN.nbit * (BitsN.nbit * offset)
79
80datatype Load
81  = LoadByte of bool * (BitsN.nbit * (BitsN.nbit * offset))
82  | LoadHalf of bool * (BitsN.nbit * (BitsN.nbit * offset))
83  | LoadLiteral of BitsN.nbit * BitsN.nbit
84  | LoadMultiple of bool * (BitsN.nbit * BitsN.nbit)
85  | LoadWord of BitsN.nbit * (BitsN.nbit * offset)
86
87datatype Media
88  = ByteReverse of BitsN.nbit * BitsN.nbit
89  | ByteReversePackedHalfword of BitsN.nbit * BitsN.nbit
90  | ByteReverseSignedHalfword of BitsN.nbit * BitsN.nbit
91  | ExtendByte of bool * (BitsN.nbit * BitsN.nbit)
92  | ExtendHalfword of bool * (BitsN.nbit * BitsN.nbit)
93
94datatype Multiply = Multiply32 of BitsN.nbit * (BitsN.nbit * BitsN.nbit)
95
96datatype Data
97  = ArithLogicImmediate of
98      BitsN.nbit * (bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))
99  | CompareImmediate of BitsN.nbit * BitsN.nbit
100  | Move of BitsN.nbit * BitsN.nbit
101  | Register of
102      BitsN.nbit * (bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))
103  | ShiftImmediate of
104      bool * (bool * (BitsN.nbit * (BitsN.nbit * (SRType * Nat.nat))))
105  | ShiftRegister of BitsN.nbit * (BitsN.nbit * (SRType * BitsN.nbit))
106  | TestCompareRegister of BitsN.nbit * (BitsN.nbit * BitsN.nbit)
107
108datatype Branch
109  = BranchExchange of BitsN.nbit
110  | BranchLinkExchangeRegister of BitsN.nbit
111  | BranchLinkImmediate of BitsN.nbit
112  | BranchTarget of BitsN.nbit
113
114datatype instruction
115  = Branch of Branch
116  | Data of Data
117  | Hint of Hint
118  | Load of Load
119  | Media of Media
120  | Multiply of Multiply
121  | NoOperation of unit
122  | Store of Store
123  | System of System
124  | Undefined of BitsN.nbit
125
126datatype MachineCode
127  = Thumb of BitsN.nbit | Thumb2 of BitsN.nbit * BitsN.nbit
128
129datatype enc = Enc_Thumb | Enc_Narrow | Enc_Wide
130
131datatype maybeMachineCode
132  = BadCode of string
133  | Thumb16 of BitsN.nbit
134  | Thumb32 of BitsN.nbit * BitsN.nbit
135
136datatype maybe_instruction
137  = FAIL of string
138  | HALFWORD of BitsN.nbit
139  | OK of (BitsN.nbit * string) * instruction
140  | PENDING of string * ((BitsN.nbit * string) * instruction)
141
142datatype nat_or_reg = NAT of Nat.nat | REGISTER of BitsN.nbit
143
144(* -------------------------------------------------------------------------
145   Casting maps (for enumerated types)
146   ------------------------------------------------------------------------- *)
147
148structure Cast =
149struct
150fun natToMode x =
151  case Nat.toInt x of
152     0 => Mode_Thread | 1 => Mode_Handler | _ => raise Fail "natToMode"
153
154fun natToRName x =
155  case Nat.toInt x of
156     0 => RName_0
157   | 1 => RName_1
158   | 2 => RName_2
159   | 3 => RName_3
160   | 4 => RName_4
161   | 5 => RName_5
162   | 6 => RName_6
163   | 7 => RName_7
164   | 8 => RName_8
165   | 9 => RName_9
166   | 10 => RName_10
167   | 11 => RName_11
168   | 12 => RName_12
169   | 13 => RName_SP_main
170   | 14 => RName_SP_process
171   | 15 => RName_LR
172   | 16 => RName_PC
173   | _ => raise Fail "natToRName"
174
175fun natToSRType x =
176  case Nat.toInt x of
177     0 => SRType_LSL
178   | 1 => SRType_LSR
179   | 2 => SRType_ASR
180   | 3 => SRType_ROR
181   | 4 => SRType_RRX
182   | _ => raise Fail "natToSRType"
183
184fun natToenc x =
185  case Nat.toInt x of
186     0 => Enc_Thumb
187   | 1 => Enc_Narrow
188   | 2 => Enc_Wide
189   | _ => raise Fail "natToenc"
190
191fun ModeToNat x =
192  case x of
193     Mode_Thread => 0 | Mode_Handler => 1
194
195fun RNameToNat x =
196  case x of
197     RName_0 => 0
198   | RName_1 => 1
199   | RName_2 => 2
200   | RName_3 => 3
201   | RName_4 => 4
202   | RName_5 => 5
203   | RName_6 => 6
204   | RName_7 => 7
205   | RName_8 => 8
206   | RName_9 => 9
207   | RName_10 => 10
208   | RName_11 => 11
209   | RName_12 => 12
210   | RName_SP_main => 13
211   | RName_SP_process => 14
212   | RName_LR => 15
213   | RName_PC => 16
214
215fun SRTypeToNat x =
216  case x of
217     SRType_LSL => 0
218   | SRType_LSR => 1
219   | SRType_ASR => 2
220   | SRType_ROR => 3
221   | SRType_RRX => 4
222
223fun encToNat x =
224  case x of
225     Enc_Thumb => 0 | Enc_Narrow => 1 | Enc_Wide => 2
226
227fun ModeToString x =
228  case x of
229     Mode_Thread => "Mode_Thread" | Mode_Handler => "Mode_Handler"
230
231fun RNameToString x =
232  case x of
233     RName_0 => "RName_0"
234   | RName_1 => "RName_1"
235   | RName_2 => "RName_2"
236   | RName_3 => "RName_3"
237   | RName_4 => "RName_4"
238   | RName_5 => "RName_5"
239   | RName_6 => "RName_6"
240   | RName_7 => "RName_7"
241   | RName_8 => "RName_8"
242   | RName_9 => "RName_9"
243   | RName_10 => "RName_10"
244   | RName_11 => "RName_11"
245   | RName_12 => "RName_12"
246   | RName_SP_main => "RName_SP_main"
247   | RName_SP_process => "RName_SP_process"
248   | RName_LR => "RName_LR"
249   | RName_PC => "RName_PC"
250
251fun SRTypeToString x =
252  case x of
253     SRType_LSL => "SRType_LSL"
254   | SRType_LSR => "SRType_LSR"
255   | SRType_ASR => "SRType_ASR"
256   | SRType_ROR => "SRType_ROR"
257   | SRType_RRX => "SRType_RRX"
258
259fun encToString x =
260  case x of
261     Enc_Thumb => "Enc_Thumb"
262   | Enc_Narrow => "Enc_Narrow"
263   | Enc_Wide => "Enc_Wide"
264
265fun stringToMode x =
266  case x of
267     "Mode_Thread" => Mode_Thread
268   | "Mode_Handler" => Mode_Handler
269   | _ => raise Fail "stringToMode"
270
271fun stringToRName x =
272  case x of
273     "RName_0" => RName_0
274   | "RName_1" => RName_1
275   | "RName_2" => RName_2
276   | "RName_3" => RName_3
277   | "RName_4" => RName_4
278   | "RName_5" => RName_5
279   | "RName_6" => RName_6
280   | "RName_7" => RName_7
281   | "RName_8" => RName_8
282   | "RName_9" => RName_9
283   | "RName_10" => RName_10
284   | "RName_11" => RName_11
285   | "RName_12" => RName_12
286   | "RName_SP_main" => RName_SP_main
287   | "RName_SP_process" => RName_SP_process
288   | "RName_LR" => RName_LR
289   | "RName_PC" => RName_PC
290   | _ => raise Fail "stringToRName"
291
292fun stringToSRType x =
293  case x of
294     "SRType_LSL" => SRType_LSL
295   | "SRType_LSR" => SRType_LSR
296   | "SRType_ASR" => SRType_ASR
297   | "SRType_ROR" => SRType_ROR
298   | "SRType_RRX" => SRType_RRX
299   | _ => raise Fail "stringToSRType"
300
301fun stringToenc x =
302  case x of
303     "Enc_Thumb" => Enc_Thumb
304   | "Enc_Narrow" => Enc_Narrow
305   | "Enc_Wide" => Enc_Wide
306   | _ => raise Fail "stringToenc"
307end
308
309(* -------------------------------------------------------------------------
310   Record update functions
311   ------------------------------------------------------------------------- *)
312
313fun PRIMASK_PM_rupd ({PM, primask'rst}: PRIMASK, x') =
314  {PM = x', primask'rst = primask'rst}: PRIMASK
315
316fun PRIMASK_primask'rst_rupd ({PM, primask'rst}: PRIMASK, x') =
317  {PM = PM, primask'rst = x'}: PRIMASK
318
319fun PSR_C_rupd ({C, ExceptionNumber, N, T, V, Z, psr'rst}: PSR, x') =
320  {C = x', ExceptionNumber = ExceptionNumber, N = N, T = T, V = V, Z = Z,
321   psr'rst = psr'rst}: PSR
322
323fun PSR_ExceptionNumber_rupd ({C, ExceptionNumber, N, T, V, Z, psr'rst}
324  : PSR, x') =
325  {C = C, ExceptionNumber = x', N = N, T = T, V = V, Z = Z,
326   psr'rst = psr'rst}: PSR
327
328fun PSR_N_rupd ({C, ExceptionNumber, N, T, V, Z, psr'rst}: PSR, x') =
329  {C = C, ExceptionNumber = ExceptionNumber, N = x', T = T, V = V, Z = Z,
330   psr'rst = psr'rst}: PSR
331
332fun PSR_T_rupd ({C, ExceptionNumber, N, T, V, Z, psr'rst}: PSR, x') =
333  {C = C, ExceptionNumber = ExceptionNumber, N = N, T = x', V = V, Z = Z,
334   psr'rst = psr'rst}: PSR
335
336fun PSR_V_rupd ({C, ExceptionNumber, N, T, V, Z, psr'rst}: PSR, x') =
337  {C = C, ExceptionNumber = ExceptionNumber, N = N, T = T, V = x', Z = Z,
338   psr'rst = psr'rst}: PSR
339
340fun PSR_Z_rupd ({C, ExceptionNumber, N, T, V, Z, psr'rst}: PSR, x') =
341  {C = C, ExceptionNumber = ExceptionNumber, N = N, T = T, V = V, Z = x',
342   psr'rst = psr'rst}: PSR
343
344fun PSR_psr'rst_rupd ({C, ExceptionNumber, N, T, V, Z, psr'rst}
345  : PSR, x') =
346  {C = C, ExceptionNumber = ExceptionNumber, N = N, T = T, V = V, Z = Z,
347   psr'rst = x'}: PSR
348
349fun CONTROL_SPSEL_rupd ({SPSEL, control'rst, nPRIV}: CONTROL, x') =
350  {SPSEL = x', control'rst = control'rst, nPRIV = nPRIV}: CONTROL
351
352fun CONTROL_control'rst_rupd ({SPSEL, control'rst, nPRIV}: CONTROL, x') =
353  {SPSEL = SPSEL, control'rst = x', nPRIV = nPRIV}: CONTROL
354
355fun CONTROL_nPRIV_rupd ({SPSEL, control'rst, nPRIV}: CONTROL, x') =
356  {SPSEL = SPSEL, control'rst = control'rst, nPRIV = x'}: CONTROL
357
358fun AIRCR_ENDIANNESS_rupd ({ENDIANNESS, SYSRESETREQ, VECTCLRACTIVE,
359   VECTKEY, aircr'rst}: AIRCR, x') =
360  {ENDIANNESS = x', SYSRESETREQ = SYSRESETREQ,
361   VECTCLRACTIVE = VECTCLRACTIVE, VECTKEY = VECTKEY, aircr'rst = aircr'rst}
362  : AIRCR
363
364fun AIRCR_SYSRESETREQ_rupd ({ENDIANNESS, SYSRESETREQ, VECTCLRACTIVE,
365   VECTKEY, aircr'rst}: AIRCR, x') =
366  {ENDIANNESS = ENDIANNESS, SYSRESETREQ = x',
367   VECTCLRACTIVE = VECTCLRACTIVE, VECTKEY = VECTKEY, aircr'rst = aircr'rst}
368  : AIRCR
369
370fun AIRCR_VECTCLRACTIVE_rupd ({ENDIANNESS, SYSRESETREQ, VECTCLRACTIVE,
371   VECTKEY, aircr'rst}: AIRCR, x') =
372  {ENDIANNESS = ENDIANNESS, SYSRESETREQ = SYSRESETREQ, VECTCLRACTIVE = x',
373   VECTKEY = VECTKEY, aircr'rst = aircr'rst}: AIRCR
374
375fun AIRCR_VECTKEY_rupd ({ENDIANNESS, SYSRESETREQ, VECTCLRACTIVE, VECTKEY,
376   aircr'rst}: AIRCR, x') =
377  {ENDIANNESS = ENDIANNESS, SYSRESETREQ = SYSRESETREQ,
378   VECTCLRACTIVE = VECTCLRACTIVE, VECTKEY = x', aircr'rst = aircr'rst}
379  : AIRCR
380
381fun AIRCR_aircr'rst_rupd ({ENDIANNESS, SYSRESETREQ, VECTCLRACTIVE,
382   VECTKEY, aircr'rst}: AIRCR, x') =
383  {ENDIANNESS = ENDIANNESS, SYSRESETREQ = SYSRESETREQ,
384   VECTCLRACTIVE = VECTCLRACTIVE, VECTKEY = VECTKEY, aircr'rst = x'}
385  : AIRCR
386
387fun CCR_STKALIGN_rupd ({STKALIGN, UNALIGN_TRP, ccr'rst}: CCR, x') =
388  {STKALIGN = x', UNALIGN_TRP = UNALIGN_TRP, ccr'rst = ccr'rst}: CCR
389
390fun CCR_UNALIGN_TRP_rupd ({STKALIGN, UNALIGN_TRP, ccr'rst}: CCR, x') =
391  {STKALIGN = STKALIGN, UNALIGN_TRP = x', ccr'rst = ccr'rst}: CCR
392
393fun CCR_ccr'rst_rupd ({STKALIGN, UNALIGN_TRP, ccr'rst}: CCR, x') =
394  {STKALIGN = STKALIGN, UNALIGN_TRP = UNALIGN_TRP, ccr'rst = x'}: CCR
395
396fun SHPR2_PRI_11_rupd ({PRI_11, shpr2'rst}: SHPR2, x') =
397  {PRI_11 = x', shpr2'rst = shpr2'rst}: SHPR2
398
399fun SHPR2_shpr2'rst_rupd ({PRI_11, shpr2'rst}: SHPR2, x') =
400  {PRI_11 = PRI_11, shpr2'rst = x'}: SHPR2
401
402fun SHPR3_PRI_14_rupd ({PRI_14, PRI_15, shpr3'rst}: SHPR3, x') =
403  {PRI_14 = x', PRI_15 = PRI_15, shpr3'rst = shpr3'rst}: SHPR3
404
405fun SHPR3_PRI_15_rupd ({PRI_14, PRI_15, shpr3'rst}: SHPR3, x') =
406  {PRI_14 = PRI_14, PRI_15 = x', shpr3'rst = shpr3'rst}: SHPR3
407
408fun SHPR3_shpr3'rst_rupd ({PRI_14, PRI_15, shpr3'rst}: SHPR3, x') =
409  {PRI_14 = PRI_14, PRI_15 = PRI_15, shpr3'rst = x'}: SHPR3
410
411fun IPR_PRI_N0_rupd ({PRI_N0, PRI_N1, PRI_N2, PRI_N3, ipr'rst}: IPR, x') =
412  {PRI_N0 = x', PRI_N1 = PRI_N1, PRI_N2 = PRI_N2, PRI_N3 = PRI_N3,
413   ipr'rst = ipr'rst}: IPR
414
415fun IPR_PRI_N1_rupd ({PRI_N0, PRI_N1, PRI_N2, PRI_N3, ipr'rst}: IPR, x') =
416  {PRI_N0 = PRI_N0, PRI_N1 = x', PRI_N2 = PRI_N2, PRI_N3 = PRI_N3,
417   ipr'rst = ipr'rst}: IPR
418
419fun IPR_PRI_N2_rupd ({PRI_N0, PRI_N1, PRI_N2, PRI_N3, ipr'rst}: IPR, x') =
420  {PRI_N0 = PRI_N0, PRI_N1 = PRI_N1, PRI_N2 = x', PRI_N3 = PRI_N3,
421   ipr'rst = ipr'rst}: IPR
422
423fun IPR_PRI_N3_rupd ({PRI_N0, PRI_N1, PRI_N2, PRI_N3, ipr'rst}: IPR, x') =
424  {PRI_N0 = PRI_N0, PRI_N1 = PRI_N1, PRI_N2 = PRI_N2, PRI_N3 = x',
425   ipr'rst = ipr'rst}: IPR
426
427fun IPR_ipr'rst_rupd ({PRI_N0, PRI_N1, PRI_N2, PRI_N3, ipr'rst}
428  : IPR, x') =
429  {PRI_N0 = PRI_N0, PRI_N1 = PRI_N1, PRI_N2 = PRI_N2, PRI_N3 = PRI_N3,
430   ipr'rst = x'}: IPR
431
432(* -------------------------------------------------------------------------
433   Exceptions
434   ------------------------------------------------------------------------- *)
435
436exception ASSERT of string
437
438exception UNPREDICTABLE of string
439
440(* -------------------------------------------------------------------------
441   Global variables (state)
442   ------------------------------------------------------------------------- *)
443
444val AIRCR = ref
445  ({ENDIANNESS = false, SYSRESETREQ = false, VECTCLRACTIVE = false,
446    VECTKEY = BitsN.B(0x0,16), aircr'rst = BitsN.B(0x0,13)}): AIRCR ref
447
448val CCR = ref
449  ({STKALIGN = false, UNALIGN_TRP = false, ccr'rst = BitsN.B(0x0,30)})
450  : CCR ref
451
452val CONTROL = ref ({SPSEL = false, control'rst = false, nPRIV = false})
453  : CONTROL ref
454
455val CurrentMode = ref (Mode_Handler): Mode ref
456
457val ExceptionActive = ref (Map.mkMap(SOME 64,false)): (bool Map.map) ref
458
459val MEM = ref (Map.mkMap(SOME 4294967296,BitsN.B(0x0,8)))
460  : (BitsN.nbit Map.map) ref
461
462val NVIC_IPR = ref
463  (Map.mkMap
464     (SOME 8,
465      {PRI_N0 = BitsN.B(0x0,2), PRI_N1 = BitsN.B(0x0,2),
466       PRI_N2 = BitsN.B(0x0,2), PRI_N3 = BitsN.B(0x0,2),
467       ipr'rst = BitsN.B(0x0,24)})): (IPR Map.map) ref
468
469val PRIMASK = ref ({PM = false, primask'rst = BitsN.B(0x0,31)})
470  : PRIMASK ref
471
472val PSR = ref
473  ({C = false, ExceptionNumber = BitsN.B(0x0,6), N = false, T = false,
474    V = false, Z = false, psr'rst = BitsN.B(0x0,21)}): PSR ref
475
476val REG = ref (Map.mkMap(SOME 17,BitsN.B(0x0,32)))
477  : (BitsN.nbit Map.map) ref
478
479val SHPR2 = ref ({PRI_11 = BitsN.B(0x0,2), shpr2'rst = BitsN.B(0x0,30)})
480  : SHPR2 ref
481
482val SHPR3 = ref
483  ({PRI_14 = BitsN.B(0x0,2), PRI_15 = BitsN.B(0x0,2),
484    shpr3'rst = BitsN.B(0x0,28)}): SHPR3 ref
485
486val VTOR = ref (BitsN.B(0x0,32)): BitsN.nbit ref
487
488val count = ref (0): Nat.nat ref
489
490val pcinc = ref (BitsN.B(0x0,32)): BitsN.nbit ref
491
492val pending = ref (NONE): (ARM_Exception option) ref
493
494(* -------------------------------------------------------------------------
495   Main specification
496   ------------------------------------------------------------------------- *)
497
498local
499  fun tuple'16 [t0,t1,t2,t3,t4,t5,t6,t7,t8,t9,t10,t11,t12,t13,t14,t15] =
500    (t0,
501     (t1,
502      (t2,
503       (t3,(t4,(t5,(t6,(t7,(t8,(t9,(t10,(t11,(t12,(t13,(t14,t15)))))))))))))))
504    | tuple'16 (_: bool list) = raise Fail "tuple'16"
505in
506  val boolify'16 = tuple'16 o BitsN.toList
507end
508
509local
510  fun tuple'4 [t0,t1,t2,t3] = (t0,(t1,(t2,t3)))
511    | tuple'4 (_: bool list) = raise Fail "tuple'4"
512in
513  val boolify'4 = tuple'4 o BitsN.toList
514end
515
516fun rec'PRIMASK x =
517  {PM = BitsN.bit(x,0), primask'rst = BitsN.bits(31,1) x};
518
519fun reg'PRIMASK x =
520  case x of
521     {PM = PM, primask'rst = primask'rst} =>
522       BitsN.@@(primask'rst,BitsN.fromBit PM);
523
524fun write'rec'PRIMASK (_,x) = reg'PRIMASK x;
525
526fun write'reg'PRIMASK (_,x) = rec'PRIMASK x;
527
528fun rec'PSR x =
529  {C = BitsN.bit(x,29), ExceptionNumber = BitsN.bits(5,0) x,
530   N = BitsN.bit(x,31), T = BitsN.bit(x,24), V = BitsN.bit(x,28),
531   Z = BitsN.bit(x,30),
532   psr'rst = BitsN.@@(BitsN.bits(23,6) x,BitsN.bits(27,25) x)};
533
534fun reg'PSR x =
535  case x of
536     {C = C, ExceptionNumber = ExceptionNumber, N = N, T = T, V = V,
537      Z = Z, psr'rst = psr'rst} =>
538       BitsN.concat
539         [BitsN.fromBit N,BitsN.fromBit Z,BitsN.fromBit C,BitsN.fromBit V,
540          BitsN.bits(2,0) psr'rst,BitsN.fromBit T,
541          BitsN.bits(20,3) psr'rst,ExceptionNumber];
542
543fun write'rec'PSR (_,x) = reg'PSR x;
544
545fun write'reg'PSR (_,x) = rec'PSR x;
546
547fun rec'CONTROL x =
548  {SPSEL = BitsN.bit(x,1), control'rst = BitsN.bit(x,2),
549   nPRIV = BitsN.bit(x,0)};
550
551fun reg'CONTROL x =
552  case x of
553     {SPSEL = SPSEL, control'rst = control'rst, nPRIV = nPRIV} =>
554       BitsN.concat
555         [BitsN.fromBit control'rst,BitsN.fromBit SPSEL,
556          BitsN.fromBit nPRIV];
557
558fun write'rec'CONTROL (_,x) = reg'CONTROL x;
559
560fun write'reg'CONTROL (_,x) = rec'CONTROL x;
561
562fun rec'AIRCR x =
563  {ENDIANNESS = BitsN.bit(x,15), SYSRESETREQ = BitsN.bit(x,2),
564   VECTCLRACTIVE = BitsN.bit(x,1), VECTKEY = BitsN.bits(31,16) x,
565   aircr'rst = BitsN.@@(BitsN.bits(0,0) x,BitsN.bits(14,3) x)};
566
567fun reg'AIRCR x =
568  case x of
569     {ENDIANNESS = ENDIANNESS, SYSRESETREQ = SYSRESETREQ,
570      VECTCLRACTIVE = VECTCLRACTIVE, VECTKEY = VECTKEY,
571      aircr'rst = aircr'rst} =>
572       BitsN.concat
573         [VECTKEY,BitsN.fromBit ENDIANNESS,BitsN.bits(11,0) aircr'rst,
574          BitsN.fromBit SYSRESETREQ,BitsN.fromBit VECTCLRACTIVE,
575          BitsN.bits(12,12) aircr'rst];
576
577fun write'rec'AIRCR (_,x) = reg'AIRCR x;
578
579fun write'reg'AIRCR (_,x) = rec'AIRCR x;
580
581fun rec'CCR x =
582  {STKALIGN = BitsN.bit(x,9), UNALIGN_TRP = BitsN.bit(x,3),
583   ccr'rst =
584     BitsN.concat[BitsN.bits(2,0) x,BitsN.bits(8,4) x,BitsN.bits(31,10) x]};
585
586fun reg'CCR x =
587  case x of
588     {STKALIGN = STKALIGN, UNALIGN_TRP = UNALIGN_TRP, ccr'rst = ccr'rst} =>
589       BitsN.concat
590         [BitsN.bits(21,0) ccr'rst,BitsN.fromBit STKALIGN,
591          BitsN.bits(26,22) ccr'rst,BitsN.fromBit UNALIGN_TRP,
592          BitsN.bits(29,27) ccr'rst];
593
594fun write'rec'CCR (_,x) = reg'CCR x;
595
596fun write'reg'CCR (_,x) = rec'CCR x;
597
598fun rec'SHPR2 x =
599  {PRI_11 = BitsN.bits(31,30) x, shpr2'rst = BitsN.bits(29,0) x};
600
601fun reg'SHPR2 x =
602  case x of
603     {PRI_11 = PRI_11, shpr2'rst = shpr2'rst} =>
604       BitsN.@@(PRI_11,shpr2'rst);
605
606fun write'rec'SHPR2 (_,x) = reg'SHPR2 x;
607
608fun write'reg'SHPR2 (_,x) = rec'SHPR2 x;
609
610fun rec'SHPR3 x =
611  {PRI_14 = BitsN.bits(23,22) x, PRI_15 = BitsN.bits(31,30) x,
612   shpr3'rst = BitsN.@@(BitsN.bits(21,0) x,BitsN.bits(29,24) x)};
613
614fun reg'SHPR3 x =
615  case x of
616     {PRI_14 = PRI_14, PRI_15 = PRI_15, shpr3'rst = shpr3'rst} =>
617       BitsN.concat
618         [PRI_15,BitsN.bits(5,0) shpr3'rst,PRI_14,
619          BitsN.bits(27,6) shpr3'rst];
620
621fun write'rec'SHPR3 (_,x) = reg'SHPR3 x;
622
623fun write'reg'SHPR3 (_,x) = rec'SHPR3 x;
624
625fun rec'IPR x =
626  {PRI_N0 = BitsN.bits(7,6) x, PRI_N1 = BitsN.bits(15,14) x,
627   PRI_N2 = BitsN.bits(23,22) x, PRI_N3 = BitsN.bits(31,30) x,
628   ipr'rst =
629     BitsN.concat
630       [BitsN.bits(5,0) x,BitsN.bits(13,8) x,BitsN.bits(21,16) x,
631        BitsN.bits(29,24) x]};
632
633fun reg'IPR x =
634  case x of
635     {PRI_N0 = PRI_N0, PRI_N1 = PRI_N1, PRI_N2 = PRI_N2, PRI_N3 = PRI_N3,
636      ipr'rst = ipr'rst} =>
637       BitsN.concat
638         [PRI_N3,BitsN.bits(5,0) ipr'rst,PRI_N2,BitsN.bits(11,6) ipr'rst,
639          PRI_N1,BitsN.bits(17,12) ipr'rst,PRI_N0,
640          BitsN.bits(23,18) ipr'rst];
641
642fun write'rec'IPR (_,x) = reg'IPR x;
643
644fun write'reg'IPR (_,x) = rec'IPR x;
645
646fun ProcessorID () = 0;
647
648fun ConditionPassed cond =
649  let
650    val result =
651      case BitsN.bits(3,1) cond of
652         BitsN.B(0x0,_) => #Z((!PSR) : PSR)
653       | BitsN.B(0x1,_) => #C((!PSR) : PSR)
654       | BitsN.B(0x2,_) => #N((!PSR) : PSR)
655       | BitsN.B(0x3,_) => #V((!PSR) : PSR)
656       | BitsN.B(0x4,_) =>
657         (#C((!PSR) : PSR)) andalso (not(#Z((!PSR) : PSR)))
658       | BitsN.B(0x5,_) => (#N((!PSR) : PSR)) = (#V((!PSR) : PSR))
659       | BitsN.B(0x6,_) =>
660         ((#N((!PSR) : PSR)) = (#V((!PSR) : PSR))) andalso
661         (not(#Z((!PSR) : PSR)))
662       | BitsN.B(0x7,_) => true
663       | _ => raise General.Bind
664  in
665    if (BitsN.bit(cond,0)) andalso (not(cond = (BitsN.B(0xF,4))))
666      then not result
667    else result
668  end;
669
670fun Raise e = pending := (Option.SOME e);
671
672fun CurrentModeIsPrivileged () =
673  ((!CurrentMode) = Mode_Handler) orelse
674  (not(#nPRIV((!CONTROL) : CONTROL)));
675
676fun LookUpSP () =
677  if #SPSEL((!CONTROL) : CONTROL) then RName_SP_process else RName_SP_main;
678
679fun R n =
680  if n = (BitsN.B(0xF,4))
681    then BitsN.+
682           (Map.lookup((!REG),Cast.RNameToNat RName_PC),BitsN.B(0x4,32))
683  else if n = (BitsN.B(0xE,4))
684    then Map.lookup((!REG),Cast.RNameToNat RName_LR)
685  else if n = (BitsN.B(0xD,4))
686    then Map.lookup((!REG),Cast.RNameToNat(LookUpSP ()))
687  else Map.lookup
688         ((!REG),Cast.RNameToNat((Cast.natToRName o BitsN.toNat) n));
689
690fun write'R (value,n) =
691  if n = (BitsN.B(0xF,4))
692    then raise ASSERT "n >= 0 and n <= 14"
693  else if n = (BitsN.B(0xE,4))
694    then REG := (Map.update((!REG),Cast.RNameToNat RName_LR,value))
695  else if n = (BitsN.B(0xD,4))
696    then let
697           val x = LookUpSP ()
698         in
699           REG :=
700           (Map.update
701              ((!REG),Cast.RNameToNat x,
702               BitsN.@@(BitsN.bits(31,2) value,BitsN.B(0x0,2))))
703         end
704  else let
705         val x = (Cast.natToRName o BitsN.toNat) n
706       in
707         REG := (Map.update((!REG),Cast.RNameToNat x,value))
708       end;
709
710fun SP_main () = Map.lookup((!REG),Cast.RNameToNat RName_SP_main);
711
712fun write'SP_main value =
713  REG := (Map.update((!REG),Cast.RNameToNat RName_SP_main,value));
714
715fun SP_process () = Map.lookup((!REG),Cast.RNameToNat RName_SP_process);
716
717fun write'SP_process value =
718  REG := (Map.update((!REG),Cast.RNameToNat RName_SP_process,value));
719
720fun SP () = R(BitsN.B(0xD,4));
721
722fun write'SP value = write'R(value,BitsN.B(0xD,4));
723
724fun LR () = R(BitsN.B(0xE,4));
725
726fun write'LR value = write'R(value,BitsN.B(0xE,4));
727
728fun PC () = R(BitsN.B(0xF,4));
729
730fun write'PC value =
731  REG := (Map.update((!REG),Cast.RNameToNat RName_PC,value));
732
733fun mem1 address =
734  BitsN.toBitstring(Map.lookup((!MEM),BitsN.toNat address));
735
736fun mem (address,size) =
737  case size of
738     1 => Bitstring.bits(7,0) (mem1(BitsN.+(address,BitsN.B(0x0,32))))
739   | 2 =>
740     Bitstring.bits(15,0)
741       ((mem1(BitsN.+(address,BitsN.B(0x1,32))))
742          @
743          (mem1(BitsN.+(address,BitsN.B(0x0,32)))))
744   | 4 =>
745     Bitstring.bits(31,0)
746       (List.concat
747          [mem1(BitsN.+(address,BitsN.B(0x3,32))),
748           mem1(BitsN.+(address,BitsN.B(0x2,32))),
749           mem1(BitsN.+(address,BitsN.B(0x1,32))),
750           mem1(BitsN.+(address,BitsN.B(0x0,32)))])
751   | _ => raise ASSERT "mem: size in {1, 2, 4}";
752
753fun write'mem (value,(address,size)) =
754  case size of
755     1 =>
756       let
757         val x = BitsN.+(address,BitsN.B(0x0,32))
758       in
759         MEM :=
760         (Map.update
761            ((!MEM),BitsN.toNat x,
762             BitsN.fromBitstring(Bitstring.bits(7,0) value,8)))
763       end
764   | 2 =>
765     ( let
766         val x = BitsN.+(address,BitsN.B(0x0,32))
767       in
768         MEM :=
769         (Map.update
770            ((!MEM),BitsN.toNat x,
771             BitsN.fromBitstring(Bitstring.bits(7,0) value,8)))
772       end
773     ; let
774         val x = BitsN.+(address,BitsN.B(0x1,32))
775       in
776         MEM :=
777         (Map.update
778            ((!MEM),BitsN.toNat x,
779             BitsN.fromBitstring(Bitstring.bits(15,8) value,8)))
780       end
781     )
782   | 4 =>
783     ( let
784         val x = BitsN.+(address,BitsN.B(0x0,32))
785       in
786         MEM :=
787         (Map.update
788            ((!MEM),BitsN.toNat x,
789             BitsN.fromBitstring(Bitstring.bits(7,0) value,8)))
790       end
791     ; let
792         val x = BitsN.+(address,BitsN.B(0x1,32))
793       in
794         MEM :=
795         (Map.update
796            ((!MEM),BitsN.toNat x,
797             BitsN.fromBitstring(Bitstring.bits(15,8) value,8)))
798       end
799     ; let
800         val x = BitsN.+(address,BitsN.B(0x2,32))
801       in
802         MEM :=
803         (Map.update
804            ((!MEM),BitsN.toNat x,
805             BitsN.fromBitstring(Bitstring.bits(23,16) value,8)))
806       end
807     ; let
808         val x = BitsN.+(address,BitsN.B(0x3,32))
809       in
810         MEM :=
811         (Map.update
812            ((!MEM),BitsN.toNat x,
813             BitsN.fromBitstring(Bitstring.bits(31,24) value,8)))
814       end
815     )
816   | _ => raise ASSERT "mem: size in {1, 2, 4}";
817
818fun BigEndianReverse (value,n) =
819  case n of
820     1 => Bitstring.bits(7,0) value
821   | 2 => (Bitstring.bits(7,0) value) @ (Bitstring.bits(15,8) value)
822   | 4 =>
823     List.concat
824       [Bitstring.bits(7,0) value,Bitstring.bits(15,8) value,
825        Bitstring.bits(23,16) value,Bitstring.bits(31,24) value]
826   | _ => raise ASSERT "BigEndianReverse: n in {1, 2, 4}";
827
828fun Align N (w,n) = BitsN.fromNat(Nat.*(n,Nat.div(BitsN.toNat w,n)),N);
829
830fun Aligned N (w,n) = w = (Align N (w,n));
831
832fun MemA N (address,size) =
833  if not(Aligned 32 (address,size))
834    then ( Raise HardFault; BitsN.fromNat(0,N) )
835  else let
836         val value = mem(address,size)
837       in
838         BitsN.fromBitstring
839           (if #ENDIANNESS((!AIRCR) : AIRCR)
840              then BigEndianReverse(value,size)
841            else value,N)
842       end;
843
844fun write'MemA N (value,(address,size)) =
845  if not(Aligned 32 (address,size))
846    then Raise HardFault
847  else let
848         val x = (address,size)
849       in
850         write'mem
851           (if #ENDIANNESS((!AIRCR) : AIRCR)
852              then BigEndianReverse(BitsN.toBitstring value,size)
853            else BitsN.toBitstring value,x)
854       end;
855
856fun MemU N (address,size) = MemA N (address,size);
857
858fun write'MemU N (value,(address,size)) =
859  let val x = (address,size) in write'MemA N (value,x) end;
860
861fun ExcNumber e =
862  case e of
863     Reset => BitsN.B(0x1,6)
864   | NMI => BitsN.B(0x2,6)
865   | HardFault => BitsN.B(0x3,6)
866   | SVCall => BitsN.B(0xB,6)
867   | PendSV => BitsN.B(0xE,6)
868   | SysTick => BitsN.B(0xF,6)
869   | ExternalInterrupt n => BitsN.+(BitsN.B(0x10,6),n);
870
871fun TakeReset () =
872  let
873    val vectortable = (!VTOR)
874  in
875    ( L3.for
876        (0,12,
877         fn i =>
878           let
879             val x = BitsN.fromNat(i,4)
880           in
881             write'R(BitsN.B(0x0,32),x)
882           end)
883    ; write'SP_main(MemA 32 (vectortable,4))
884    ; write'SP_process(BitsN.@@(BitsN.B(0x0,30),BitsN.B(0x0,2)))
885    ; write'LR(BitsN.B(0x0,32))
886    ; write'PC(MemA 32 (BitsN.+(vectortable,BitsN.B(0x4,32)),4))
887    ; CurrentMode := Mode_Thread
888    ; PSR :=
889      {C = false, ExceptionNumber = BitsN.B(0x0,6), N = false, T = false,
890       V = false, Z = false, psr'rst = BitsN.B(0x0,21)}
891    ; PSR := (PSR_ExceptionNumber_rupd((!PSR),BitsN.B(0x0,6)))
892    ; PRIMASK := (PRIMASK_PM_rupd((!PRIMASK),false))
893    ; CONTROL := (CONTROL_SPSEL_rupd((!CONTROL),false))
894    ; CONTROL := (CONTROL_nPRIV_rupd((!CONTROL),false))
895    ; L3.for
896        (0,63,
897         fn i =>
898           let
899             val x = BitsN.fromNat(i,6)
900           in
901             ExceptionActive :=
902             (Map.update((!ExceptionActive),BitsN.toNat x,false))
903           end)
904    )
905  end;
906
907fun ExceptionPriority n =
908  if n = 2
909    then IntInf.~ 2
910  else if n = 1
911    then IntInf.~ 1
912  else if n = 11
913    then BitsN.toInt(#PRI_11((!SHPR2) : SHPR2))
914  else if n = 14
915    then BitsN.toInt(#PRI_14((!SHPR3) : SHPR3))
916  else if n = 15
917    then BitsN.toInt(#PRI_15((!SHPR3) : SHPR3))
918  else if Nat.>=(n,16)
919    then let
920           val r =
921             Map.lookup
922               ((!NVIC_IPR),
923                BitsN.toNat(BitsN.fromNat(Nat.div(Nat.-(n,16),4),3)))
924         in
925           case BitsN.fromNat(Nat.mod(n,4),2) of
926              BitsN.B(0x0,_) => BitsN.toInt(#PRI_N0(r : IPR))
927            | BitsN.B(0x1,_) => BitsN.toInt(#PRI_N1(r : IPR))
928            | BitsN.B(0x2,_) => BitsN.toInt(#PRI_N2(r : IPR))
929            | BitsN.B(0x3,_) => BitsN.toInt(#PRI_N3(r : IPR))
930            | _ => raise General.Bind
931         end
932  else 4;
933
934fun ExecutionPriority () =
935  let
936    val highestpri = ref 4
937  in
938    let
939      val boostedpri = ref 4
940    in
941      ( L3.for
942          (2,48,
943           fn i =>
944             if Map.lookup
945                  ((!ExceptionActive),BitsN.toNat(BitsN.fromNat(i,6)))
946               then let
947                      val p = ExceptionPriority i
948                    in
949                      if IntInf.<(p,(!highestpri))
950                        then highestpri := p
951                      else ()
952                    end
953             else ())
954      ; if #PM((!PRIMASK) : PRIMASK) then boostedpri := 0 else ()
955      ; IntInf.min((!boostedpri),(!highestpri))
956      )
957    end
958  end;
959
960fun ReturnAddress () = PC ();
961
962fun PushStack () =
963  let
964    val frameptralign = ref (BitsN.B(0x0,1))
965  in
966    let
967      val frameptr = ref (BitsN.B(0x0,32))
968    in
969      ( if (#SPSEL((!CONTROL) : CONTROL)) andalso
970           ((!CurrentMode) = Mode_Thread)
971          then ( frameptralign := (BitsN.bits(2,2) (SP_process ()))
972               ; write'SP_process
973                   (BitsN.&&
974                      (BitsN.-(SP_process (),BitsN.B(0x20,32)),
975                       BitsN.~(BitsN.zeroExtend 32 (BitsN.B(0x4,3)))))
976               ; frameptr := (SP_process ())
977               )
978        else ( frameptralign := (BitsN.bits(2,2) (SP_main ()))
979             ; write'SP_process
980                 (BitsN.&&
981                    (BitsN.-(SP_main (),BitsN.B(0x20,32)),
982                     BitsN.~(BitsN.zeroExtend 32 (BitsN.B(0x4,3)))))
983             ; frameptr := (SP_main ())
984             )
985      ; let
986          val x = ((!frameptr),4)
987        in
988          write'MemA 32 (R(BitsN.B(0x0,4)),x)
989        end
990      ; let
991          val x = (BitsN.+((!frameptr),BitsN.B(0x4,32)),4)
992        in
993          write'MemA 32 (R(BitsN.B(0x1,4)),x)
994        end
995      ; let
996          val x = (BitsN.+((!frameptr),BitsN.B(0x8,32)),4)
997        in
998          write'MemA 32 (R(BitsN.B(0x2,4)),x)
999        end
1000      ; let
1001          val x = (BitsN.+((!frameptr),BitsN.B(0xC,32)),4)
1002        in
1003          write'MemA 32 (R(BitsN.B(0x3,4)),x)
1004        end
1005      ; let
1006          val x = (BitsN.+((!frameptr),BitsN.B(0x10,32)),4)
1007        in
1008          write'MemA 32 (R(BitsN.B(0xC,4)),x)
1009        end
1010      ; let
1011          val x = (BitsN.+((!frameptr),BitsN.B(0x14,32)),4)
1012        in
1013          write'MemA 32 (LR (),x)
1014        end
1015      ; let
1016          val x = (BitsN.+((!frameptr),BitsN.B(0x14,32)),4)
1017        in
1018          write'MemA 32 (ReturnAddress (),x)
1019        end
1020      ; let
1021          val x = (BitsN.+((!frameptr),BitsN.B(0x1C,32)),4)
1022        in
1023          write'MemA 32
1024            (BitsN.concat
1025               [BitsN.bits(31,10) (reg'PSR (!PSR)),(!frameptralign),
1026                BitsN.bits(8,0) (reg'PSR (!PSR))],x)
1027        end
1028      ; if (!CurrentMode) = Mode_Handler
1029          then write'LR(BitsN.B(0xFFFFFFF1,32))
1030        else if not(#SPSEL((!CONTROL) : CONTROL))
1031          then write'LR(BitsN.B(0xFFFFFFF9,32))
1032        else write'LR(BitsN.B(0xFFFFFFFD,32))
1033      )
1034    end
1035  end;
1036
1037fun ExceptionTaken ExceptionNumber =
1038  let
1039    val vectortable = (!VTOR)
1040  in
1041    ( L3.for
1042        (0,3,
1043         fn i =>
1044           let
1045             val x = BitsN.fromNat(i,4)
1046           in
1047             write'R(BitsN.B(0x0,32),x)
1048           end)
1049    ; write'R(BitsN.B(0x0,32),BitsN.B(0xC,4))
1050    ; write'PC
1051        (MemA 32
1052           (BitsN.+
1053              (vectortable,
1054               BitsN.*
1055                 (BitsN.B(0x4,32),
1056                  BitsN.fromNat(BitsN.toNat ExceptionNumber,32))),4))
1057    ; PSR :=
1058      {C = false, ExceptionNumber = BitsN.B(0x0,6), N = false, T = false,
1059       V = false, Z = false, psr'rst = BitsN.B(0x0,21)}
1060    ; CurrentMode := Mode_Handler
1061    ; PSR := (PSR_ExceptionNumber_rupd((!PSR),ExceptionNumber))
1062    ; CONTROL := (CONTROL_SPSEL_rupd((!CONTROL),false))
1063    ; ExceptionActive :=
1064      (Map.update((!ExceptionActive),BitsN.toNat ExceptionNumber,true))
1065    )
1066  end;
1067
1068fun ExceptionEntry () =
1069  case (!pending) of
1070     Option.SOME e => ( PushStack (); ExceptionTaken(ExcNumber e) )
1071   | NONE => ();
1072
1073fun PopStack (frameptr,EXC_RETURN) =
1074  ( write'R(MemA 32 (frameptr,4),BitsN.B(0x0,4))
1075  ; write'R(MemA 32 (BitsN.+(frameptr,BitsN.B(0x4,32)),4),BitsN.B(0x1,4))
1076  ; write'R(MemA 32 (BitsN.+(frameptr,BitsN.B(0x8,32)),4),BitsN.B(0x2,4))
1077  ; write'R(MemA 32 (BitsN.+(frameptr,BitsN.B(0xC,32)),4),BitsN.B(0x3,4))
1078  ; write'R(MemA 32 (BitsN.+(frameptr,BitsN.B(0x10,32)),4),BitsN.B(0xC,4))
1079  ; write'LR(MemA 32 (BitsN.+(frameptr,BitsN.B(0x14,32)),4))
1080  ; write'PC(MemA 32 (BitsN.+(frameptr,BitsN.B(0x18,32)),4))
1081  ; let
1082      val psr = MemA 32 (BitsN.+(frameptr,BitsN.B(0x1C,32)),4)
1083      val spmask =
1084        BitsN.zeroExtend 32 (BitsN.@@(BitsN.bits(9,9) psr,BitsN.B(0x0,2)))
1085    in
1086      ( case boolify'4(BitsN.bits(3,0) EXC_RETURN) of
1087           (_,(false,(false,true))) =>
1088             write'SP_main
1089               (BitsN.||(BitsN.+(SP_main (),BitsN.B(0x20,32)),spmask))
1090         | (true,(true,(false,true))) =>
1091           write'SP_process
1092             (BitsN.||(BitsN.+(SP_process (),BitsN.B(0x20,32)),spmask))
1093         | _ => ()
1094      ; let
1095          val w = reg'PSR (!PSR)
1096        in
1097          PSR :=
1098          (write'reg'PSR
1099             ((!PSR),BitsN.bitFieldInsert(31,27) (w,BitsN.bits(31,27) psr)))
1100        end
1101      ; let
1102          val w = reg'PSR (!PSR)
1103        in
1104          PSR :=
1105          (write'reg'PSR
1106             ((!PSR),
1107              BitsN.bitFieldInsert(24,24)
1108                (w,BitsN.fromBit(BitsN.bit(psr,24)))))
1109        end
1110      ; let
1111          val w = reg'PSR (!PSR)
1112        in
1113          PSR :=
1114          (write'reg'PSR
1115             ((!PSR),BitsN.bitFieldInsert(5,0) (w,BitsN.bits(5,0) psr)))
1116        end
1117      )
1118    end
1119  );
1120
1121fun DeActivate ReturningExceptionNumber =
1122  ExceptionActive :=
1123  (Map.update
1124     ((!ExceptionActive),BitsN.toNat ReturningExceptionNumber,false));
1125
1126fun IsOnes N w = w = (BitsN.neg(BitsN.BV(0x1,N)));
1127
1128fun ExceptionActiveBitCount () =
1129  let
1130    val count = ref 0
1131  in
1132    ( L3.for
1133        (0,63,
1134         fn i =>
1135           if Map.lookup
1136                ((!ExceptionActive),BitsN.toNat(BitsN.fromNat(i,6)))
1137             then count := (Nat.+((!count),1))
1138           else ())
1139    ; (!count)
1140    )
1141  end;
1142
1143fun ExceptionReturn EXC_RETURN =
1144  ( if not((!CurrentMode) = Mode_Handler)
1145      then raise ASSERT "CurrentMode == Mode_Handler"
1146    else ()
1147  ; if not(IsOnes 24 (BitsN.bits(27,4) EXC_RETURN))
1148      then raise UNPREDICTABLE "ExceptionReturn"
1149    else ()
1150  ; let
1151      val ReturningExceptionNumber = #ExceptionNumber((!PSR) : PSR)
1152      val NestedActivation = ExceptionActiveBitCount ()
1153    in
1154      if not(Map.lookup
1155               ((!ExceptionActive),BitsN.toNat ReturningExceptionNumber))
1156        then raise UNPREDICTABLE "ExceptionReturn"
1157      else let
1158             val frameptr = ref (BitsN.B(0x0,32))
1159           in
1160             ( case BitsN.bits(3,0) EXC_RETURN of
1161                  BitsN.B(0x1,_) =>
1162                    if NestedActivation = 1
1163                      then raise UNPREDICTABLE "ExceptionReturn"
1164                    else ( frameptr := (SP_main ())
1165                         ; CurrentMode := Mode_Handler
1166                         ; CONTROL :=
1167                           (CONTROL_SPSEL_rupd((!CONTROL),false))
1168                         )
1169                | BitsN.B(0x9,_) =>
1170                  if not(NestedActivation = 1)
1171                    then raise UNPREDICTABLE "ExceptionReturn"
1172                  else ( frameptr := (SP_main ())
1173                       ; CurrentMode := Mode_Thread
1174                       ; CONTROL := (CONTROL_SPSEL_rupd((!CONTROL),false))
1175                       )
1176                | BitsN.B(0xD,_) =>
1177                  if not(NestedActivation = 1)
1178                    then raise UNPREDICTABLE "ExceptionReturn"
1179                  else ( frameptr := (SP_process ())
1180                       ; CurrentMode := Mode_Thread
1181                       ; CONTROL := (CONTROL_SPSEL_rupd((!CONTROL),true))
1182                       )
1183                | _ => raise UNPREDICTABLE "ExceptionReturn"
1184             ; DeActivate ReturningExceptionNumber
1185             ; PopStack((!frameptr),EXC_RETURN)
1186             ; if (!CurrentMode) = Mode_Handler
1187                 then if (#ExceptionNumber((!PSR) : PSR)) =
1188                         (BitsN.B(0x0,6))
1189                        then raise UNPREDICTABLE "ExceptionReturn"
1190                      else ()
1191               else if not((#ExceptionNumber((!PSR) : PSR)) =
1192                      (BitsN.B(0x0,6)))
1193                 then raise UNPREDICTABLE "ExceptionReturn"
1194               else ()
1195             )
1196           end
1197    end
1198  );
1199
1200fun CallSupervisor () = Raise SVCall;
1201
1202fun BranchTo address = write'PC address;
1203
1204fun BranchWritePC address =
1205  BranchTo(BitsN.@@(BitsN.bits(31,1) address,BitsN.B(0x0,1)));
1206
1207fun BXWritePC address =
1208  if ((!CurrentMode) = Mode_Handler) andalso
1209     ((BitsN.bits(31,28) address) = (BitsN.B(0xF,4)))
1210    then ExceptionReturn(BitsN.bits(27,0) address)
1211  else ( if not(BitsN.bit(address,0)) then Raise HardFault else ()
1212       ; BranchTo(BitsN.@@(BitsN.bits(31,1) address,BitsN.B(0x0,1)))
1213       );
1214
1215fun BLXWritePC address =
1216  ( if not(BitsN.bit(address,0)) then Raise HardFault else ()
1217  ; BranchTo(BitsN.@@(BitsN.bits(31,1) address,BitsN.B(0x0,1)))
1218  );
1219
1220fun LoadWritePC address = BXWritePC address;
1221
1222fun ALUWritePC address = BranchWritePC address;
1223
1224fun IncPC () =
1225  BranchTo(BitsN.+(Map.lookup((!REG),Cast.RNameToNat RName_PC),(!pcinc)));
1226
1227fun HighestSetBit N w =
1228  if w = (BitsN.BV(0x0,N)) then IntInf.~ 1 else BitsN.toInt(BitsN.log2 w);
1229
1230fun CountLeadingZeroBits N w =
1231  Nat.fromInt
1232    (IntInf.-
1233       (IntInf.-(Nat.toInt(BitsN.size(BitsN.BV(0x0,N))),1),
1234        HighestSetBit N w));
1235
1236fun LowestSetBit N w = CountLeadingZeroBits N (BitsN.reverse w);
1237
1238fun BitCount N w =
1239  let
1240    val result = ref 0
1241  in
1242    ( L3.for
1243        (0,Nat.-(BitsN.size(BitsN.BV(0x0,N)),1),
1244         fn i =>
1245           if BitsN.bit(w,i) then result := (Nat.+((!result),1)) else ())
1246    ; (!result)
1247    )
1248  end;
1249
1250fun SignExtendFrom N (w,p) =
1251  let
1252    val s = Nat.-(BitsN.size(BitsN.BV(0x0,N)),p)
1253  in
1254    BitsN.>>(BitsN.<<(w,s),s)
1255  end;
1256
1257fun Extend (M,N) (unsigned,w) =
1258  if unsigned then BitsN.zeroExtend N w else BitsN.signExtend N w;
1259
1260fun UInt N w = Nat.toInt(BitsN.toNat w);
1261
1262fun LSL_C N (x,shift) =
1263  ( if shift = 0 then raise ASSERT "LSL_C" else ()
1264  ; let
1265      val extended_x =
1266        (BitsN.toBitstring x) @ (Bitstring.replicate([false],shift))
1267    in
1268      (BitsN.<<(x,shift),
1269       Bitstring.bit(extended_x,BitsN.size(BitsN.BV(0x0,N))))
1270    end
1271  );
1272
1273fun LSL N (x,shift) = if shift = 0 then x else L3.fst(LSL_C N (x,shift));
1274
1275fun LSR_C N (x,shift) =
1276  ( if shift = 0 then raise ASSERT "LSR_C" else ()
1277  ; (BitsN.>>+(x,shift),
1278     (Nat.<=(shift,BitsN.size(BitsN.BV(0x0,N)))) andalso
1279     (BitsN.bit(x,Nat.-(shift,1))))
1280  );
1281
1282fun LSR N (x,shift) = if shift = 0 then x else L3.fst(LSR_C N (x,shift));
1283
1284fun ASR_C N (x,shift) =
1285  ( if shift = 0 then raise ASSERT "ASR_C" else ()
1286  ; (BitsN.>>(x,shift),
1287     BitsN.bit(x,Nat.-(Nat.min(BitsN.size(BitsN.BV(0x0,N)),shift),1)))
1288  );
1289
1290fun ASR N (x,shift) = if shift = 0 then x else L3.fst(ASR_C N (x,shift));
1291
1292fun ROR_C N (x,shift) =
1293  ( if shift = 0 then raise ASSERT "ROR_C" else ()
1294  ; let val result = BitsN.#>>(x,shift) in (result,BitsN.msb result) end
1295  );
1296
1297fun ROR N (x,shift) = if shift = 0 then x else L3.fst(ROR_C N (x,shift));
1298
1299fun RRX_C N (x,carry_in) =
1300  let
1301    val result =
1302      BitsN.fromBitstring
1303        ((Bitstring.fromBool carry_in)
1304           @
1305           (Bitstring.bits(Nat.-(BitsN.size(BitsN.BV(0x0,N)),1),1)
1306              (BitsN.toBitstring x)),N)
1307  in
1308    (result,BitsN.bit(x,0))
1309  end;
1310
1311fun RRX N (x,carry_in) = L3.fst(RRX_C N (x,carry_in));
1312
1313fun DecodeImmShift (typ,imm5) =
1314  case typ of
1315     BitsN.B(0x0,_) => (SRType_LSL,BitsN.toNat imm5)
1316   | BitsN.B(0x1,_) =>
1317     (SRType_LSR,if imm5 = (BitsN.B(0x0,5)) then 32 else BitsN.toNat imm5)
1318   | BitsN.B(0x2,_) =>
1319     (SRType_ASR,if imm5 = (BitsN.B(0x0,5)) then 32 else BitsN.toNat imm5)
1320   | BitsN.B(0x3,_) =>
1321     if imm5 = (BitsN.B(0x0,5))
1322       then (SRType_RRX,1)
1323     else (SRType_ROR,BitsN.toNat imm5)
1324   | _ => raise General.Bind;
1325
1326fun DecodeRegShift typ =
1327  case typ of
1328     BitsN.B(0x0,_) => SRType_LSL
1329   | BitsN.B(0x1,_) => SRType_LSR
1330   | BitsN.B(0x2,_) => SRType_ASR
1331   | BitsN.B(0x3,_) => SRType_ROR
1332   | _ => raise General.Bind;
1333
1334fun Shift_C N (value,(typ,(amount,carry_in))) =
1335  if amount = 0
1336    then (value,carry_in)
1337  else case typ of
1338          SRType_LSL => LSL_C N (value,amount)
1339        | SRType_LSR => LSR_C N (value,amount)
1340        | SRType_ASR => ASR_C N (value,amount)
1341        | SRType_ROR => ROR_C N (value,amount)
1342        | SRType_RRX => RRX_C N (value,carry_in);
1343
1344fun Shift N (value,(typ,(amount,carry_in))) =
1345  L3.fst(Shift_C N (value,(typ,(amount,carry_in))));
1346
1347fun AddWithCarry N (x,(y,carry_in)) =
1348  let
1349    val unsigned_sum =
1350      Nat.+(Nat.+(BitsN.toNat x,BitsN.toNat y),Nat.fromBool carry_in)
1351    val signed_sum =
1352      IntInf.+
1353        (IntInf.+(BitsN.toInt x,BitsN.toInt y),IntExtra.fromBool carry_in)
1354    val result = BitsN.fromNat(unsigned_sum,N)
1355    val carry_out = not((BitsN.toNat result) = unsigned_sum)
1356    val overflow = not((BitsN.toInt result) = signed_sum)
1357  in
1358    (result,(carry_out,overflow))
1359  end;
1360
1361fun DataProcessingALU (opc,(a,(b,c))) =
1362  case opc of
1363     BitsN.B(0x0,_) => (BitsN.&&(a,b),(c,false))
1364   | BitsN.B(0x8,_) => (BitsN.&&(a,b),(c,false))
1365   | BitsN.B(0x1,_) => (BitsN.??(a,b),(c,false))
1366   | BitsN.B(0x9,_) => (BitsN.??(a,b),(c,false))
1367   | BitsN.B(0x2,_) => AddWithCarry 32 (a,(BitsN.~ b,true))
1368   | BitsN.B(0xA,_) => AddWithCarry 32 (a,(BitsN.~ b,true))
1369   | BitsN.B(0x3,_) => AddWithCarry 32 (BitsN.~ a,(b,true))
1370   | BitsN.B(0x4,_) => AddWithCarry 32 (a,(b,false))
1371   | BitsN.B(0xB,_) => AddWithCarry 32 (a,(b,false))
1372   | BitsN.B(0x5,_) => AddWithCarry 32 (a,(b,c))
1373   | BitsN.B(0x6,_) => AddWithCarry 32 (a,(BitsN.~ b,c))
1374   | BitsN.B(0x7,_) => AddWithCarry 32 (BitsN.~ a,(b,c))
1375   | BitsN.B(0xC,_) => (BitsN.||(a,b),(c,false))
1376   | BitsN.B(0xD,_) => (b,(c,false))
1377   | BitsN.B(0xE,_) => (BitsN.&&(a,BitsN.~ b),(c,false))
1378   | BitsN.B(0xF,_) => (BitsN.~ b,(c,false))
1379   | _ => raise General.Bind;
1380
1381fun ArithmeticOpcode opc =
1382  ((BitsN.bit(opc,2)) orelse (BitsN.bit(opc,1))) andalso
1383  (not((BitsN.bit(opc,3)) andalso (BitsN.bit(opc,2))));
1384
1385fun dfn'BranchTarget imm32 =
1386  ( BranchWritePC(BitsN.+(PC (),imm32)); count := (Nat.+((!count),3)) );
1387
1388fun dfn'BranchExchange m =
1389  ( BXWritePC(R m); count := (Nat.+((!count),3)) );
1390
1391fun dfn'BranchLinkImmediate imm32 =
1392  let
1393    val next_instr_addr = PC ()
1394  in
1395    ( write'LR(BitsN.@@(BitsN.bits(31,1) next_instr_addr,BitsN.B(0x1,1)))
1396    ; BranchWritePC(BitsN.+(PC (),imm32))
1397    ; count := (Nat.+((!count),4))
1398    )
1399  end;
1400
1401fun dfn'BranchLinkExchangeRegister m =
1402  let
1403    val target = R m
1404    val next_instr_addr = BitsN.-(PC (),BitsN.B(0x2,32))
1405  in
1406    ( write'LR(BitsN.@@(BitsN.bits(31,1) next_instr_addr,BitsN.B(0x1,1)))
1407    ; BLXWritePC target
1408    ; count := (Nat.+((!count),3))
1409    )
1410  end;
1411
1412fun DataProcessing (opc,(setflags,(d,(n,(imm32,C))))) =
1413  let
1414    val rn =
1415      if (opc = (BitsN.B(0xD,4))) orelse (opc = (BitsN.B(0xF,4)))
1416        then BitsN.B(0x0,32)
1417      else if (Set.mem(opc,[BitsN.B(0x4,4),BitsN.B(0x2,4)])) andalso
1418         ((n = (BitsN.B(0xF,4))) andalso (not setflags))
1419        then Align 32 (PC (),4)
1420      else R n
1421    val (result,(carry,overflow)) = DataProcessingALU(opc,(rn,(imm32,C)))
1422  in
1423    ( if not((BitsN.bits(3,2) opc) = (BitsN.B(0x2,2)))
1424        then write'R(result,d)
1425      else ()
1426    ; if setflags
1427        then ( PSR := (PSR_N_rupd((!PSR),BitsN.bit(result,31)))
1428             ; PSR := (PSR_Z_rupd((!PSR),result = (BitsN.B(0x0,32))))
1429             ; PSR := (PSR_C_rupd((!PSR),carry))
1430             ; if ArithmeticOpcode opc
1431                 then PSR := (PSR_V_rupd((!PSR),overflow))
1432               else ()
1433             )
1434      else ()
1435    ; IncPC ()
1436    ; count := (Nat.+((!count),1))
1437    )
1438  end;
1439
1440fun DataProcessingPC (opc,(n,(imm32,C))) =
1441  let
1442    val rn =
1443      if opc = (BitsN.B(0xD,4))
1444        then BitsN.B(0x0,32)
1445      else if n = (BitsN.B(0xF,4)) then PC () else R n
1446    val (result,_) = DataProcessingALU(opc,(rn,(imm32,C)))
1447  in
1448    ( ALUWritePC result; count := (Nat.+((!count),3)) )
1449  end;
1450
1451fun dfn'Move (d,imm32) =
1452  DataProcessing
1453    (BitsN.B(0xD,4),(true,(d,(BitsN.B(0xF,4),(imm32,#C((!PSR) : PSR))))));
1454
1455fun dfn'CompareImmediate (n,imm32) =
1456  DataProcessing
1457    (BitsN.B(0xA,4),(true,(BitsN.B(0x0,4),(n,(imm32,#C((!PSR) : PSR))))));
1458
1459fun dfn'ArithLogicImmediate (opc,(setflags,(d,(n,imm32)))) =
1460  DataProcessing(opc,(setflags,(d,(n,(imm32,#C((!PSR) : PSR))))));
1461
1462fun doRegister (opc,(setflags,(d,(n,(m,(shift_t,shift_n)))))) =
1463  let
1464    val (shifted,carry) =
1465      Shift_C 32 (R m,(shift_t,(shift_n,#C((!PSR) : PSR))))
1466    val carry = if ArithmeticOpcode opc then #C((!PSR) : PSR) else carry
1467  in
1468    if d = (BitsN.B(0xF,4))
1469      then DataProcessingPC(opc,(n,(shifted,carry)))
1470    else DataProcessing(opc,(setflags,(d,(n,(shifted,carry)))))
1471  end;
1472
1473fun dfn'Register (opc,(setflags,(d,(n,m)))) =
1474  doRegister(opc,(setflags,(d,(n,(m,(SRType_LSL,0))))));
1475
1476fun dfn'TestCompareRegister (opc,(n,m)) =
1477  doRegister
1478    (BitsN.@@(BitsN.B(0x2,2),opc),
1479     (true,(BitsN.B(0x0,4),(n,(m,(SRType_LSL,0))))));
1480
1481fun dfn'ShiftImmediate (negate,(setflags,(d,(m,(shift_t,shift_n))))) =
1482  if negate
1483    then doRegister
1484           (BitsN.B(0xF,4),
1485            (setflags,(d,(BitsN.B(0xF,4),(m,(shift_t,shift_n))))))
1486  else doRegister
1487         (BitsN.B(0xD,4),
1488          (setflags,(d,(BitsN.B(0x0,4),(m,(shift_t,shift_n))))));
1489
1490fun dfn'ShiftRegister (d,(n,(shift_t,m))) =
1491  let
1492    val shift_n = BitsN.toNat(BitsN.bits(7,0) (R m))
1493    val (shifted,carry) =
1494      Shift_C 32 (R n,(shift_t,(shift_n,#C((!PSR) : PSR))))
1495  in
1496    DataProcessing
1497      (BitsN.B(0xD,4),(true,(d,(BitsN.B(0x0,4),(shifted,carry)))))
1498  end;
1499
1500fun dfn'Multiply32 (d,(n,m)) =
1501  let
1502    val result = BitsN.*(R n,R m)
1503  in
1504    ( write'R(result,d)
1505    ; PSR := (PSR_N_rupd((!PSR),BitsN.bit(result,31)))
1506    ; PSR := (PSR_Z_rupd((!PSR),result = (BitsN.B(0x0,32))))
1507    ; IncPC ()
1508    ; count := (Nat.+((!count),1))
1509    )
1510  end;
1511
1512fun dfn'ExtendByte (unsigned,(d,m)) =
1513  ( write'R(Extend (8,32) (unsigned,BitsN.bits(7,0) (R m)),d)
1514  ; IncPC ()
1515  ; count := (Nat.+((!count),1))
1516  );
1517
1518fun dfn'ExtendHalfword (unsigned,(d,m)) =
1519  ( write'R(Extend (16,32) (unsigned,BitsN.bits(15,0) (R m)),d)
1520  ; IncPC ()
1521  ; count := (Nat.+((!count),1))
1522  );
1523
1524fun dfn'ByteReverse (d,m) =
1525  let
1526    val Rm = R m
1527  in
1528    ( write'R
1529        (BitsN.concat
1530           [BitsN.bits(7,0) Rm,BitsN.bits(15,8) Rm,BitsN.bits(23,16) Rm,
1531            BitsN.bits(31,24) Rm],d)
1532    ; IncPC ()
1533    ; count := (Nat.+((!count),1))
1534    )
1535  end;
1536
1537fun dfn'ByteReversePackedHalfword (d,m) =
1538  let
1539    val Rm = R m
1540  in
1541    ( write'R
1542        (BitsN.concat
1543           [BitsN.bits(23,16) Rm,BitsN.bits(31,24) Rm,BitsN.bits(7,0) Rm,
1544            BitsN.bits(15,8) Rm],d)
1545    ; IncPC ()
1546    ; count := (Nat.+((!count),1))
1547    )
1548  end;
1549
1550fun dfn'ByteReverseSignedHalfword (d,m) =
1551  let
1552    val Rm = R m
1553  in
1554    ( write'R
1555        (BitsN.@@
1556           (BitsN.signExtend 24 (BitsN.bits(7,0) Rm),BitsN.bits(15,8) Rm),
1557         d)
1558    ; IncPC ()
1559    ; count := (Nat.+((!count),1))
1560    )
1561  end;
1562
1563fun dfn'LoadWord (t,(n,m)) =
1564  let
1565    val offset =
1566      case m of
1567         register_form m =>
1568           Shift 32 (R m,(SRType_LSL,(0,#C((!PSR) : PSR))))
1569       | immediate_form imm32 => imm32
1570    val address = BitsN.+(R n,offset)
1571    val data = MemU 32 (address,4)
1572  in
1573    ( write'R(data,t); IncPC (); count := (Nat.+((!count),2)) )
1574  end;
1575
1576fun dfn'LoadLiteral (t,imm32) =
1577  let
1578    val base = Align 32 (PC (),4)
1579    val address = BitsN.+(base,imm32)
1580  in
1581    ( write'R(MemU 32 (address,4),t)
1582    ; IncPC ()
1583    ; count := (Nat.+((!count),2))
1584    )
1585  end;
1586
1587fun dfn'LoadByte (unsigned,(t,(n,m))) =
1588  let
1589    val offset =
1590      case m of
1591         register_form m =>
1592           Shift 32 (R m,(SRType_LSL,(0,#C((!PSR) : PSR))))
1593       | immediate_form imm32 => imm32
1594    val address = BitsN.+(R n,offset)
1595    val data = MemU 8 (address,1)
1596  in
1597    ( write'R(Extend (8,32) (unsigned,data),t)
1598    ; IncPC ()
1599    ; count := (Nat.+((!count),2))
1600    )
1601  end;
1602
1603fun dfn'LoadHalf (unsigned,(t,(n,m))) =
1604  let
1605    val offset =
1606      case m of
1607         register_form m =>
1608           Shift 32 (R m,(SRType_LSL,(0,#C((!PSR) : PSR))))
1609       | immediate_form imm32 => imm32
1610    val address = BitsN.+(R n,offset)
1611    val data = MemU 16 (address,2)
1612  in
1613    ( write'R(Extend (16,32) (unsigned,data),t)
1614    ; IncPC ()
1615    ; count := (Nat.+((!count),2))
1616    )
1617  end;
1618
1619fun dfn'LoadMultiple (wback,(n,registers)) =
1620  let
1621    val Rn = R n
1622    val bitcount = BitCount 9 registers
1623  in
1624    let
1625      val address = ref Rn
1626    in
1627      ( L3.for
1628          (0,7,
1629           fn i =>
1630             if BitsN.bit(registers,i)
1631               then ( let
1632                        val x = BitsN.fromNat(i,4)
1633                      in
1634                        write'R(MemA 32 ((!address),4),x)
1635                      end
1636                    ; address := (BitsN.+((!address),BitsN.B(0x4,32)))
1637                    )
1638             else ())
1639      ; if BitsN.bit(registers,8)
1640          then ( LoadWritePC(MemA 32 ((!address),4))
1641               ; count := (Nat.+(Nat.+((!count),bitcount),4))
1642               )
1643        else ( IncPC (); count := (Nat.+(Nat.+((!count),bitcount),1)) )
1644      ; if wback andalso (not(BitsN.bit(registers,BitsN.toNat n)))
1645          then write'R
1646                 (BitsN.+
1647                    (Rn,
1648                     BitsN.*(BitsN.B(0x4,32),BitsN.fromNat(bitcount,32))),
1649                  n)
1650        else ()
1651      )
1652    end
1653  end;
1654
1655fun dfn'StoreWord (t,(n,m)) =
1656  let
1657    val offset =
1658      case m of
1659         register_form m =>
1660           Shift 32 (R m,(SRType_LSL,(0,#C((!PSR) : PSR))))
1661       | immediate_form imm32 => imm32
1662    val address = BitsN.+(R n,offset)
1663  in
1664    ( let val x = (address,4) in write'MemU 32 (R t,x) end
1665    ; IncPC ()
1666    ; count := (Nat.+((!count),2))
1667    )
1668  end;
1669
1670fun dfn'StoreByte (t,(n,m)) =
1671  let
1672    val offset =
1673      case m of
1674         register_form m =>
1675           Shift 32 (R m,(SRType_LSL,(0,#C((!PSR) : PSR))))
1676       | immediate_form imm32 => imm32
1677    val address = BitsN.+(R n,offset)
1678  in
1679    ( let
1680        val x = (address,1)
1681      in
1682        write'MemU 8 (BitsN.bits(7,0) (R t),x)
1683      end
1684    ; IncPC ()
1685    ; count := (Nat.+((!count),2))
1686    )
1687  end;
1688
1689fun dfn'StoreHalf (t,(n,m)) =
1690  let
1691    val offset =
1692      case m of
1693         register_form m =>
1694           Shift 32 (R m,(SRType_LSL,(0,#C((!PSR) : PSR))))
1695       | immediate_form imm32 => imm32
1696    val address = BitsN.+(R n,offset)
1697  in
1698    ( let
1699        val x = (address,2)
1700      in
1701        write'MemU 16 (BitsN.bits(15,0) (R t),x)
1702      end
1703    ; IncPC ()
1704    ; count := (Nat.+((!count),2))
1705    )
1706  end;
1707
1708fun dfn'StoreMultiple (n,registers) =
1709  let
1710    val Rn = R n
1711    val bitcount = BitCount 8 registers
1712    val lowest = LowestSetBit 8 registers
1713  in
1714    let
1715      val address = ref Rn
1716    in
1717      ( L3.for
1718          (0,7,
1719           fn i =>
1720             if BitsN.bit(registers,i)
1721               then ( if ((BitsN.fromNat(i,4)) = n) andalso
1722                         (not(i = lowest))
1723                        then let
1724                               val x = ((!address),4)
1725                             in
1726                               write'MemA 32 (BitsN.B(0x0,32),x)
1727                             end
1728                      else let
1729                             val x = ((!address),4)
1730                           in
1731                             write'MemA 32 (R(BitsN.fromNat(i,4)),x)
1732                           end
1733                    ; address := (BitsN.+((!address),BitsN.B(0x4,32)))
1734                    )
1735             else ())
1736      ; write'R
1737          (BitsN.+(Rn,BitsN.*(BitsN.B(0x4,32),BitsN.fromNat(bitcount,32))),
1738           n)
1739      ; IncPC ()
1740      ; count := (Nat.+(Nat.+((!count),bitcount),1))
1741      )
1742    end
1743  end;
1744
1745fun dfn'Push registers =
1746  let
1747    val sp = SP ()
1748    val bitcount = BitCount 9 registers
1749    val length = BitsN.*(BitsN.B(0x4,32),BitsN.fromNat(bitcount,32))
1750  in
1751    let
1752      val address = ref (BitsN.-(sp,length))
1753    in
1754      ( L3.for
1755          (0,8,
1756           fn i =>
1757             if BitsN.bit(registers,i)
1758               then ( let
1759                        val x = ((!address),4)
1760                      in
1761                        write'MemA 32
1762                          (if i = 8 then LR () else R(BitsN.fromNat(i,4)),
1763                           x)
1764                      end
1765                    ; address := (BitsN.+((!address),BitsN.B(0x4,32)))
1766                    )
1767             else ())
1768      ; write'SP(BitsN.-(sp,length))
1769      ; IncPC ()
1770      ; count := (Nat.+(Nat.+((!count),bitcount),1))
1771      )
1772    end
1773  end;
1774
1775fun dfn'SupervisorCall imm32 =
1776  ( CallSupervisor (); count := (Nat.+((!count),0)) );
1777
1778fun dfn'ChangeProcessorState im =
1779  ( if CurrentModeIsPrivileged ()
1780      then PRIMASK := (PRIMASK_PM_rupd((!PRIMASK),im))
1781    else ()
1782  ; IncPC ()
1783  ; count := (Nat.+((!count),1))
1784  );
1785
1786fun dfn'MoveToRegisterFromSpecial (SYSm,d) =
1787  ( write'R(BitsN.B(0x0,32),d)
1788  ; case BitsN.bits(7,3) SYSm of
1789       BitsN.B(0x0,_) =>
1790         ( if BitsN.bit(SYSm,0)
1791             then let
1792                    val w = R d
1793                  in
1794                    write'R
1795                      (BitsN.bitFieldInsert(8,0)
1796                         (w,BitsN.bits(8,0) (reg'PSR (!PSR))),d)
1797                  end
1798           else ()
1799         ; if BitsN.bit(SYSm,1)
1800             then let
1801                    val w = R d
1802                  in
1803                    write'R
1804                      (BitsN.bitFieldInsert(24,24) (w,BitsN.fromBit false),
1805                       d)
1806                  end
1807           else ()
1808         ; if not(BitsN.bit(SYSm,2))
1809             then let
1810                    val w = R d
1811                  in
1812                    write'R
1813                      (BitsN.bitFieldInsert(31,27)
1814                         (w,BitsN.bits(31,27) (reg'PSR (!PSR))),d)
1815                  end
1816           else ()
1817         )
1818     | BitsN.B(0x1,_) =>
1819       (case BitsN.bits(2,0) SYSm of
1820           BitsN.B(0x0,_) => write'R(SP_main (),d)
1821         | BitsN.B(0x1,_) => write'R(SP_process (),d)
1822         | _ => ())
1823     | BitsN.B(0x2,_) =>
1824       (case BitsN.bits(2,0) SYSm of
1825           BitsN.B(0x0,_) =>
1826             let
1827               val w = R d
1828             in
1829               write'R
1830                 (BitsN.bitFieldInsert(0,0)
1831                    (w,BitsN.fromBit(#PM((!PRIMASK) : PRIMASK))),d)
1832             end
1833         | BitsN.B(0x4,_) =>
1834           let
1835             val w = R d
1836           in
1837             write'R
1838               (BitsN.bitFieldInsert(1,0)
1839                  (w,BitsN.bits(1,0) (reg'CONTROL (!CONTROL))),d)
1840           end
1841         | _ => ())
1842     | _ => ()
1843  ; IncPC ()
1844  ; count := (Nat.+((!count),4))
1845  );
1846
1847fun dfn'MoveToSpecialRegister (SYSm,n) =
1848  let
1849    val Rn = R n
1850  in
1851    ( case BitsN.bits(7,3) SYSm of
1852         BitsN.B(0x0,_) =>
1853           if not(BitsN.bit(SYSm,2))
1854             then let
1855                    val w = reg'PSR (!PSR)
1856                  in
1857                    PSR :=
1858                    (write'reg'PSR
1859                       ((!PSR),
1860                        BitsN.bitFieldInsert(31,27)
1861                          (w,BitsN.bits(31,27) Rn)))
1862                  end
1863           else ()
1864       | BitsN.B(0x1,_) =>
1865         if CurrentModeIsPrivileged ()
1866           then case BitsN.bits(2,0) SYSm of
1867                   BitsN.B(0x0,_) =>
1868                     write'SP_main
1869                       (BitsN.@@(BitsN.bits(31,2) Rn,BitsN.B(0x0,2)))
1870                 | BitsN.B(0x1,_) =>
1871                   write'SP_process
1872                     (BitsN.@@(BitsN.bits(31,2) Rn,BitsN.B(0x0,2)))
1873                 | _ => ()
1874         else ()
1875       | BitsN.B(0x2,_) =>
1876         if CurrentModeIsPrivileged ()
1877           then case BitsN.bits(2,0) SYSm of
1878                   BitsN.B(0x0,_) =>
1879                     PRIMASK :=
1880                     (PRIMASK_PM_rupd((!PRIMASK),BitsN.bit(Rn,0)))
1881                 | BitsN.B(0x4,_) =>
1882                   if (!CurrentMode) = Mode_Thread
1883                     then ( CONTROL :=
1884                            (CONTROL_SPSEL_rupd
1885                               ((!CONTROL),BitsN.bit(Rn,1)))
1886                          ; CONTROL :=
1887                            (CONTROL_nPRIV_rupd
1888                               ((!CONTROL),BitsN.bit(Rn,0)))
1889                          )
1890                   else ()
1891                 | _ => ()
1892         else ()
1893       | _ => ()
1894    ; IncPC ()
1895    ; count := (Nat.+((!count),4))
1896    )
1897  end;
1898
1899fun dfn'Undefined imm32 = Raise HardFault;
1900
1901fun dfn'NoOperation () = ( IncPC (); count := (Nat.+((!count),1)) );
1902
1903fun dfn'Breakpoint imm32 = ( IncPC (); count := (Nat.+((!count),0)) );
1904
1905fun dfn'DataMemoryBarrier option =
1906  ( IncPC (); count := (Nat.+((!count),4)) );
1907
1908fun dfn'DataSynchronizationBarrier option =
1909  ( IncPC (); count := (Nat.+((!count),4)) );
1910
1911fun dfn'InstructionSynchronizationBarrier option =
1912  ( IncPC (); count := (Nat.+((!count),4)) );
1913
1914fun dfn'SendEvent () = ( IncPC (); count := (Nat.+((!count),1)) );
1915
1916fun dfn'WaitForEvent () = ( IncPC (); count := (Nat.+((!count),2)) );
1917
1918fun dfn'WaitForInterrupt () = ( IncPC (); count := (Nat.+((!count),2)) );
1919
1920fun dfn'Yield () = ( IncPC (); count := (Nat.+((!count),1)) );
1921
1922fun Run v0 =
1923  case v0 of
1924     NoOperation () => dfn'NoOperation ()
1925   | Undefined v49 => dfn'Undefined v49
1926   | Branch v1 =>
1927     (case v1 of
1928         BranchExchange v2 => dfn'BranchExchange v2
1929       | BranchLinkExchangeRegister v3 =>
1930         dfn'BranchLinkExchangeRegister v3
1931       | BranchLinkImmediate v4 => dfn'BranchLinkImmediate v4
1932       | BranchTarget v5 => dfn'BranchTarget v5)
1933   | Data v6 =>
1934     (case v6 of
1935         ArithLogicImmediate v7 => dfn'ArithLogicImmediate v7
1936       | CompareImmediate v8 => dfn'CompareImmediate v8
1937       | Move v9 => dfn'Move v9
1938       | Register v10 => dfn'Register v10
1939       | ShiftImmediate v11 => dfn'ShiftImmediate v11
1940       | ShiftRegister v12 => dfn'ShiftRegister v12
1941       | TestCompareRegister v13 => dfn'TestCompareRegister v13)
1942   | Hint v14 =>
1943     (case v14 of
1944         Breakpoint v15 => dfn'Breakpoint v15
1945       | DataMemoryBarrier v16 => dfn'DataMemoryBarrier v16
1946       | DataSynchronizationBarrier v17 =>
1947         dfn'DataSynchronizationBarrier v17
1948       | InstructionSynchronizationBarrier v18 =>
1949         dfn'InstructionSynchronizationBarrier v18
1950       | SendEvent () => dfn'SendEvent ()
1951       | WaitForEvent () => dfn'WaitForEvent ()
1952       | WaitForInterrupt () => dfn'WaitForInterrupt ()
1953       | Yield () => dfn'Yield ())
1954   | Load v23 =>
1955     (case v23 of
1956         LoadByte v24 => dfn'LoadByte v24
1957       | LoadHalf v25 => dfn'LoadHalf v25
1958       | LoadLiteral v26 => dfn'LoadLiteral v26
1959       | LoadMultiple v27 => dfn'LoadMultiple v27
1960       | LoadWord v28 => dfn'LoadWord v28)
1961   | Media v29 =>
1962     (case v29 of
1963         ByteReverse v30 => dfn'ByteReverse v30
1964       | ByteReversePackedHalfword v31 =>
1965         dfn'ByteReversePackedHalfword v31
1966       | ByteReverseSignedHalfword v32 =>
1967         dfn'ByteReverseSignedHalfword v32
1968       | ExtendByte v33 => dfn'ExtendByte v33
1969       | ExtendHalfword v34 => dfn'ExtendHalfword v34)
1970   | Multiply v35 => (case v35 of Multiply32 v36 => dfn'Multiply32 v36)
1971   | Store v37 =>
1972     (case v37 of
1973         Push v38 => dfn'Push v38
1974       | StoreByte v39 => dfn'StoreByte v39
1975       | StoreHalf v40 => dfn'StoreHalf v40
1976       | StoreMultiple v41 => dfn'StoreMultiple v41
1977       | StoreWord v42 => dfn'StoreWord v42)
1978   | System v43 =>
1979     (case v43 of
1980         ChangeProcessorState v44 => dfn'ChangeProcessorState v44
1981       | MoveToRegisterFromSpecial v45 =>
1982         dfn'MoveToRegisterFromSpecial v45
1983       | MoveToSpecialRegister v46 => dfn'MoveToSpecialRegister v46
1984       | SupervisorCall v47 => dfn'SupervisorCall v47);
1985
1986fun Fetch () =
1987  let
1988    val fpc = Map.lookup((!REG),Cast.RNameToNat RName_PC)
1989    val ireg = MemA 16 (fpc,2)
1990  in
1991    if ((BitsN.bits(15,13) ireg) = (BitsN.B(0x7,3))) andalso
1992       (not((BitsN.bits(12,11) ireg) = (BitsN.B(0x0,2))))
1993      then Thumb2(ireg,MemA 16 (BitsN.+(fpc,BitsN.B(0x2,32)),2))
1994    else Thumb ireg
1995  end;
1996
1997fun DECODE_UNPREDICTABLE (mc,s) =
1998  raise UNPREDICTABLE
1999    (String.concat
2000       ["Decode ",
2001        case mc of
2002           Thumb opc =>
2003             (Bitstring.toBinString(BitsN.toBitstring opc)) ^ "; Thumb; "
2004         | Thumb2(opc1,opc2) =>
2005           String.concat
2006             [Bitstring.toBinString(BitsN.toBitstring opc1),", ",
2007              Bitstring.toBinString(BitsN.toBitstring opc2),"; Thumb2; "],
2008        s]);
2009
2010fun DecodeThumb h =
2011  let
2012    val mc = Thumb h
2013  in
2014    case boolify'16 h of
2015       (false,
2016        (false,
2017         (false,
2018          (true,
2019           (true,
2020            (false,
2021             (S'0,
2022              (Rm'2,(Rm'1,(Rm'0,(Rn'2,(Rn'1,(Rn'0,(Rd'2,(Rd'1,Rd'0))))))))))))))) =>
2023         let
2024           val d =
2025             BitsN.fromNat
2026               (BitsN.toNat(BitsN.fromBitstring([Rd'2,Rd'1,Rd'0],3)),4)
2027           val n =
2028             BitsN.fromNat
2029               (BitsN.toNat(BitsN.fromBitstring([Rn'2,Rn'1,Rn'0],3)),4)
2030           val m =
2031             BitsN.fromNat
2032               (BitsN.toNat(BitsN.fromBitstring([Rm'2,Rm'1,Rm'0],3)),4)
2033           val setflags = true
2034           val opc =
2035             if (BitsN.fromBitstring([S'0],1)) = (BitsN.B(0x1,1))
2036               then BitsN.B(0x2,4)
2037             else BitsN.B(0x4,4)
2038         in
2039           Data(Register(opc,(setflags,(d,(n,m)))))
2040         end
2041     | (false,
2042      (false,
2043       (false,
2044        (true,
2045         (true,
2046          (true,
2047           (S'0,
2048            (imm3'2,
2049             (imm3'1,(imm3'0,(Rn'2,(Rn'1,(Rn'0,(Rd'2,(Rd'1,Rd'0))))))))))))))) =>
2050       let
2051         val d =
2052           BitsN.fromNat
2053             (BitsN.toNat(BitsN.fromBitstring([Rd'2,Rd'1,Rd'0],3)),4)
2054         val n =
2055           BitsN.fromNat
2056             (BitsN.toNat(BitsN.fromBitstring([Rn'2,Rn'1,Rn'0],3)),4)
2057         val setflags = true
2058         val imm32 =
2059           BitsN.zeroExtend 32
2060             (BitsN.fromBitstring([imm3'2,imm3'1,imm3'0],3))
2061         val opc =
2062           if (BitsN.fromBitstring([S'0],1)) = (BitsN.B(0x1,1))
2063             then BitsN.B(0x2,4)
2064           else BitsN.B(0x4,4)
2065       in
2066         Data(ArithLogicImmediate(opc,(setflags,(d,(n,imm32)))))
2067       end
2068     | (false,
2069      (false,
2070       (false,
2071        (opc'1,
2072         (opc'0,
2073          (imm5'4,
2074           (imm5'3,
2075            (imm5'2,
2076             (imm5'1,(imm5'0,(Rm'2,(Rm'1,(Rm'0,(Rd'2,(Rd'1,Rd'0))))))))))))))) =>
2077       let
2078         val d =
2079           BitsN.fromNat
2080             (BitsN.toNat(BitsN.fromBitstring([Rd'2,Rd'1,Rd'0],3)),4)
2081         val m =
2082           BitsN.fromNat
2083             (BitsN.toNat(BitsN.fromBitstring([Rm'2,Rm'1,Rm'0],3)),4)
2084         val setflags = true
2085         val (shift_t,shift_n) =
2086           DecodeImmShift
2087             (BitsN.fromBitstring([opc'1,opc'0],2),
2088              BitsN.fromBitstring([imm5'4,imm5'3,imm5'2,imm5'1,imm5'0],5))
2089       in
2090         Data(ShiftImmediate(false,(setflags,(d,(m,(shift_t,shift_n))))))
2091       end
2092     | (false,
2093      (false,
2094       (true,
2095        (false,
2096         (false,
2097          (Rd'2,
2098           (Rd'1,
2099            (Rd'0,
2100             (imm8'7,
2101              (imm8'6,(imm8'5,(imm8'4,(imm8'3,(imm8'2,(imm8'1,imm8'0))))))))))))))) =>
2102       let
2103         val d =
2104           BitsN.fromNat
2105             (BitsN.toNat(BitsN.fromBitstring([Rd'2,Rd'1,Rd'0],3)),4)
2106         val imm32 =
2107           BitsN.zeroExtend 32
2108             (BitsN.fromBitstring
2109                ([imm8'7,imm8'6,imm8'5,imm8'4,imm8'3,imm8'2,imm8'1,imm8'0],
2110                 8))
2111       in
2112         Data(Move(d,imm32))
2113       end
2114     | (false,
2115      (false,
2116       (true,
2117        (false,
2118         (true,
2119          (Rn'2,
2120           (Rn'1,
2121            (Rn'0,
2122             (imm8'7,
2123              (imm8'6,(imm8'5,(imm8'4,(imm8'3,(imm8'2,(imm8'1,imm8'0))))))))))))))) =>
2124       let
2125         val n =
2126           BitsN.fromNat
2127             (BitsN.toNat(BitsN.fromBitstring([Rn'2,Rn'1,Rn'0],3)),4)
2128         val imm32 =
2129           BitsN.zeroExtend 32
2130             (BitsN.fromBitstring
2131                ([imm8'7,imm8'6,imm8'5,imm8'4,imm8'3,imm8'2,imm8'1,imm8'0],
2132                 8))
2133       in
2134         Data(CompareImmediate(n,imm32))
2135       end
2136     | (false,
2137      (false,
2138       (true,
2139        (true,
2140         (S'0,
2141          (Rdn'2,
2142           (Rdn'1,
2143            (Rdn'0,
2144             (imm8'7,
2145              (imm8'6,(imm8'5,(imm8'4,(imm8'3,(imm8'2,(imm8'1,imm8'0))))))))))))))) =>
2146       let
2147         val d =
2148           BitsN.fromNat
2149             (BitsN.toNat(BitsN.fromBitstring([Rdn'2,Rdn'1,Rdn'0],3)),4)
2150         val n = d
2151         val setflags = true
2152         val imm32 =
2153           BitsN.zeroExtend 32
2154             (BitsN.fromBitstring
2155                ([imm8'7,imm8'6,imm8'5,imm8'4,imm8'3,imm8'2,imm8'1,imm8'0],
2156                 8))
2157         val opc =
2158           if (BitsN.fromBitstring([S'0],1)) = (BitsN.B(0x1,1))
2159             then BitsN.B(0x2,4)
2160           else BitsN.B(0x4,4)
2161       in
2162         Data(ArithLogicImmediate(opc,(setflags,(d,(n,imm32)))))
2163       end
2164     | (false,
2165      (true,
2166       (false,
2167        (false,
2168         (false,
2169          (false,
2170           (opc'3,
2171            (opc'2,(opc'1,(opc'0,(Rx'2,(Rx'1,(Rx'0,(Ry'2,(Ry'1,Ry'0))))))))))))))) =>
2172       let
2173         val Ry = BitsN.fromBitstring([Ry'2,Ry'1,Ry'0],3)
2174         val Rx = BitsN.fromBitstring([Rx'2,Rx'1,Rx'0],3)
2175         val opc = BitsN.fromBitstring([opc'3,opc'2,opc'1,opc'0],4)
2176       in
2177         case opc of
2178            BitsN.B(0x0,_) =>
2179              let
2180                val d = BitsN.fromNat(BitsN.toNat Ry,4)
2181                val n = d
2182                val m = BitsN.fromNat(BitsN.toNat Rx,4)
2183                val setflags = true
2184              in
2185                Data(Register(opc,(setflags,(d,(n,m)))))
2186              end
2187          | BitsN.B(0x1,_) =>
2188            let
2189              val d = BitsN.fromNat(BitsN.toNat Ry,4)
2190              val n = d
2191              val m = BitsN.fromNat(BitsN.toNat Rx,4)
2192              val setflags = true
2193            in
2194              Data(Register(opc,(setflags,(d,(n,m)))))
2195            end
2196          | BitsN.B(0x5,_) =>
2197            let
2198              val d = BitsN.fromNat(BitsN.toNat Ry,4)
2199              val n = d
2200              val m = BitsN.fromNat(BitsN.toNat Rx,4)
2201              val setflags = true
2202            in
2203              Data(Register(opc,(setflags,(d,(n,m)))))
2204            end
2205          | BitsN.B(0x6,_) =>
2206            let
2207              val d = BitsN.fromNat(BitsN.toNat Ry,4)
2208              val n = d
2209              val m = BitsN.fromNat(BitsN.toNat Rx,4)
2210              val setflags = true
2211            in
2212              Data(Register(opc,(setflags,(d,(n,m)))))
2213            end
2214          | BitsN.B(0xC,_) =>
2215            let
2216              val d = BitsN.fromNat(BitsN.toNat Ry,4)
2217              val n = d
2218              val m = BitsN.fromNat(BitsN.toNat Rx,4)
2219              val setflags = true
2220            in
2221              Data(Register(opc,(setflags,(d,(n,m)))))
2222            end
2223          | BitsN.B(0xE,_) =>
2224            let
2225              val d = BitsN.fromNat(BitsN.toNat Ry,4)
2226              val n = d
2227              val m = BitsN.fromNat(BitsN.toNat Rx,4)
2228              val setflags = true
2229            in
2230              Data(Register(opc,(setflags,(d,(n,m)))))
2231            end
2232          | BitsN.B(0x2,_) =>
2233            let
2234              val d = BitsN.fromNat(BitsN.toNat Ry,4)
2235              val n = d
2236              val m = BitsN.fromNat(BitsN.toNat Rx,4)
2237              val shift_t =
2238                DecodeRegShift
2239                  (BitsN.fromNat
2240                     (BitsN.toNat(BitsN.-(opc,BitsN.B(0x2,4))),2))
2241            in
2242              Data(ShiftRegister(d,(n,(shift_t,m))))
2243            end
2244          | BitsN.B(0x3,_) =>
2245            let
2246              val d = BitsN.fromNat(BitsN.toNat Ry,4)
2247              val n = d
2248              val m = BitsN.fromNat(BitsN.toNat Rx,4)
2249              val shift_t =
2250                DecodeRegShift
2251                  (BitsN.fromNat
2252                     (BitsN.toNat(BitsN.-(opc,BitsN.B(0x2,4))),2))
2253            in
2254              Data(ShiftRegister(d,(n,(shift_t,m))))
2255            end
2256          | BitsN.B(0x4,_) =>
2257            let
2258              val d = BitsN.fromNat(BitsN.toNat Ry,4)
2259              val n = d
2260              val m = BitsN.fromNat(BitsN.toNat Rx,4)
2261              val shift_t =
2262                DecodeRegShift
2263                  (BitsN.fromNat
2264                     (BitsN.toNat(BitsN.-(opc,BitsN.B(0x2,4))),2))
2265            in
2266              Data(ShiftRegister(d,(n,(shift_t,m))))
2267            end
2268          | BitsN.B(0x7,_) =>
2269            let
2270              val d = BitsN.fromNat(BitsN.toNat Ry,4)
2271              val n = d
2272              val m = BitsN.fromNat(BitsN.toNat Rx,4)
2273            in
2274              Data(ShiftRegister(d,(n,(SRType_ROR,m))))
2275            end
2276          | BitsN.B(0x8,_) =>
2277            let
2278              val n = BitsN.fromNat(BitsN.toNat Ry,4)
2279              val m = BitsN.fromNat(BitsN.toNat Rx,4)
2280            in
2281              Data(TestCompareRegister(BitsN.bits(1,0) opc,(n,m)))
2282            end
2283          | BitsN.B(0xA,_) =>
2284            let
2285              val n = BitsN.fromNat(BitsN.toNat Ry,4)
2286              val m = BitsN.fromNat(BitsN.toNat Rx,4)
2287            in
2288              Data(TestCompareRegister(BitsN.bits(1,0) opc,(n,m)))
2289            end
2290          | BitsN.B(0xB,_) =>
2291            let
2292              val n = BitsN.fromNat(BitsN.toNat Ry,4)
2293              val m = BitsN.fromNat(BitsN.toNat Rx,4)
2294            in
2295              Data(TestCompareRegister(BitsN.bits(1,0) opc,(n,m)))
2296            end
2297          | BitsN.B(0x9,_) =>
2298            let
2299              val d = BitsN.fromNat(BitsN.toNat Ry,4)
2300              val n = BitsN.fromNat(BitsN.toNat Rx,4)
2301              val setflags = true
2302            in
2303              Data
2304                (ArithLogicImmediate
2305                   (BitsN.B(0x3,4),(setflags,(d,(n,BitsN.B(0x0,32))))))
2306            end
2307          | BitsN.B(0xD,_) =>
2308            let
2309              val d = BitsN.fromNat(BitsN.toNat Ry,4)
2310              val n = BitsN.fromNat(BitsN.toNat Rx,4)
2311              val m = d
2312            in
2313              Multiply(Multiply32(d,(n,m)))
2314            end
2315          | BitsN.B(0xF,_) =>
2316            let
2317              val d = BitsN.fromNat(BitsN.toNat Ry,4)
2318              val m = BitsN.fromNat(BitsN.toNat Rx,4)
2319              val setflags = true
2320              val (shift_t,shift_n) = (SRType_LSL,0)
2321            in
2322              Data
2323                (ShiftImmediate(true,(setflags,(d,(m,(shift_t,shift_n))))))
2324            end
2325          | _ => raise General.Bind
2326       end
2327     | (false,
2328      (true,
2329       (false,
2330        (false,
2331         (false,
2332          (true,
2333           (false,
2334            (false,
2335             (DN'0,(Rm'3,(Rm'2,(Rm'1,(Rm'0,(Rdn'2,(Rdn'1,Rdn'0))))))))))))))) =>
2336       let
2337         val Rm = BitsN.fromBitstring([Rm'3,Rm'2,Rm'1,Rm'0],4)
2338         val d =
2339           BitsN.@@
2340             (BitsN.fromBitstring([DN'0],1),
2341              BitsN.fromBitstring([Rdn'2,Rdn'1,Rdn'0],3))
2342         val n = d
2343       in
2344         ( if (n = (BitsN.B(0xF,4))) andalso (Rm = (BitsN.B(0xF,4)))
2345             then DECODE_UNPREDICTABLE(mc,"ADD")
2346           else ()
2347         ; let
2348             val setflags = false
2349           in
2350             Data(Register(BitsN.B(0x4,4),(setflags,(d,(n,Rm)))))
2351           end
2352         )
2353       end
2354     | (false,
2355      (true,
2356       (false,
2357        (false,
2358         (false,
2359          (true,
2360           (false,
2361            (true,(N'0,(Rm'3,(Rm'2,(Rm'1,(Rm'0,(Rn'2,(Rn'1,Rn'0))))))))))))))) =>
2362       let
2363         val Rm = BitsN.fromBitstring([Rm'3,Rm'2,Rm'1,Rm'0],4)
2364         val n =
2365           BitsN.@@
2366             (BitsN.fromBitstring([N'0],1),
2367              BitsN.fromBitstring([Rn'2,Rn'1,Rn'0],3))
2368       in
2369         ( if ((BitsN.<+(n,BitsN.B(0x8,4))) andalso
2370               (BitsN.<+(Rm,BitsN.B(0x8,4)))) orelse
2371              ((n = (BitsN.B(0xF,4))) orelse (Rm = (BitsN.B(0xF,4))))
2372             then DECODE_UNPREDICTABLE(mc,"CMP")
2373           else ()
2374         ; Data(TestCompareRegister(BitsN.B(0x2,2),(n,Rm)))
2375         )
2376       end
2377     | (false,
2378      (true,
2379       (false,
2380        (false,
2381         (false,
2382          (true,
2383           (true,
2384            (false,(D'0,(Rm'3,(Rm'2,(Rm'1,(Rm'0,(Rd'2,(Rd'1,Rd'0))))))))))))))) =>
2385       let
2386         val d =
2387           BitsN.@@
2388             (BitsN.fromBitstring([D'0],1),
2389              BitsN.fromBitstring([Rd'2,Rd'1,Rd'0],3))
2390         val setflags = false
2391         val (shift_t,shift_n) = (SRType_LSL,0)
2392       in
2393         Data
2394           (ShiftImmediate
2395              (false,
2396               (setflags,
2397                (d,
2398                 (BitsN.fromBitstring([Rm'3,Rm'2,Rm'1,Rm'0],4),
2399                  (shift_t,shift_n))))))
2400       end
2401     | (false,
2402      (true,
2403       (false,
2404        (false,
2405         (false,(true,(true,(true,(false,(Rm'3,(Rm'2,(Rm'1,(Rm'0,_))))))))))))) =>
2406       Branch
2407         (BranchExchange(BitsN.fromBitstring([Rm'3,Rm'2,Rm'1,Rm'0],4)))
2408     | (false,
2409      (true,
2410       (false,
2411        (false,
2412         (false,(true,(true,(true,(true,(Rm'3,(Rm'2,(Rm'1,(Rm'0,_))))))))))))) =>
2413       Branch
2414         (BranchLinkExchangeRegister
2415            (BitsN.fromBitstring([Rm'3,Rm'2,Rm'1,Rm'0],4)))
2416     | (false,
2417      (true,
2418       (false,
2419        (false,
2420         (true,
2421          (Rt'2,
2422           (Rt'1,
2423            (Rt'0,
2424             (imm8'7,
2425              (imm8'6,(imm8'5,(imm8'4,(imm8'3,(imm8'2,(imm8'1,imm8'0))))))))))))))) =>
2426       let
2427         val imm32 =
2428           BitsN.zeroExtend 32
2429             (BitsN.@@
2430                (BitsN.fromBitstring
2431                   ([imm8'7,imm8'6,imm8'5,imm8'4,imm8'3,imm8'2,imm8'1,
2432                     imm8'0],8),BitsN.B(0x0,2)))
2433       in
2434         Load
2435           (LoadLiteral
2436              (BitsN.fromNat
2437                 (BitsN.toNat(BitsN.fromBitstring([Rt'2,Rt'1,Rt'0],3)),4),
2438               imm32))
2439       end
2440     | (false,
2441      (true,
2442       (false,
2443        (true,
2444         (opc'2,
2445          (opc'1,
2446           (opc'0,
2447            (Rm'2,(Rm'1,(Rm'0,(Rn'2,(Rn'1,(Rn'0,(Rt'2,(Rt'1,Rt'0))))))))))))))) =>
2448       let
2449         val Rt = BitsN.fromBitstring([Rt'2,Rt'1,Rt'0],3)
2450         val Rn = BitsN.fromBitstring([Rn'2,Rn'1,Rn'0],3)
2451         val m =
2452           register_form
2453             (BitsN.fromNat
2454                (BitsN.toNat(BitsN.fromBitstring([Rm'2,Rm'1,Rm'0],3)),4))
2455       in
2456         case BitsN.fromBitstring([opc'2,opc'1,opc'0],3) of
2457            BitsN.B(0x0,_) =>
2458              Store
2459                (StoreWord
2460                   (BitsN.fromNat(BitsN.toNat Rt,4),
2461                    (BitsN.fromNat(BitsN.toNat Rn,4),m)))
2462          | BitsN.B(0x1,_) =>
2463            Store
2464              (StoreHalf
2465                 (BitsN.fromNat(BitsN.toNat Rt,4),
2466                  (BitsN.fromNat(BitsN.toNat Rn,4),m)))
2467          | BitsN.B(0x2,_) =>
2468            Store
2469              (StoreByte
2470                 (BitsN.fromNat(BitsN.toNat Rt,4),
2471                  (BitsN.fromNat(BitsN.toNat Rn,4),m)))
2472          | BitsN.B(0x3,_) =>
2473            Load
2474              (LoadByte
2475                 (false,
2476                  (BitsN.fromNat(BitsN.toNat Rt,4),
2477                   (BitsN.fromNat(BitsN.toNat Rn,4),m))))
2478          | BitsN.B(0x4,_) =>
2479            Load
2480              (LoadWord
2481                 (BitsN.fromNat(BitsN.toNat Rt,4),
2482                  (BitsN.fromNat(BitsN.toNat Rn,4),m)))
2483          | BitsN.B(0x5,_) =>
2484            Load
2485              (LoadHalf
2486                 (true,
2487                  (BitsN.fromNat(BitsN.toNat Rt,4),
2488                   (BitsN.fromNat(BitsN.toNat Rn,4),m))))
2489          | BitsN.B(0x6,_) =>
2490            Load
2491              (LoadByte
2492                 (true,
2493                  (BitsN.fromNat(BitsN.toNat Rt,4),
2494                   (BitsN.fromNat(BitsN.toNat Rn,4),m))))
2495          | BitsN.B(0x7,_) =>
2496            Load
2497              (LoadHalf
2498                 (false,
2499                  (BitsN.fromNat(BitsN.toNat Rt,4),
2500                   (BitsN.fromNat(BitsN.toNat Rn,4),m))))
2501          | _ => raise General.Bind
2502       end
2503     | (false,
2504      (true,
2505       (true,
2506        (false,
2507         (L'0,
2508          (imm5'4,
2509           (imm5'3,
2510            (imm5'2,
2511             (imm5'1,(imm5'0,(Rn'2,(Rn'1,(Rn'0,(Rt'2,(Rt'1,Rt'0))))))))))))))) =>
2512       let
2513         val Rt = BitsN.fromBitstring([Rt'2,Rt'1,Rt'0],3)
2514         val Rn = BitsN.fromBitstring([Rn'2,Rn'1,Rn'0],3)
2515         val imm32 =
2516           BitsN.zeroExtend 32
2517             (BitsN.@@
2518                (BitsN.fromBitstring
2519                   ([imm5'4,imm5'3,imm5'2,imm5'1,imm5'0],5),BitsN.B(0x0,2)))
2520         val m = immediate_form imm32
2521       in
2522         if (BitsN.fromBitstring([L'0],1)) = (BitsN.B(0x1,1))
2523           then Load
2524                  (LoadWord
2525                     (BitsN.fromNat(BitsN.toNat Rt,4),
2526                      (BitsN.fromNat(BitsN.toNat Rn,4),m)))
2527         else Store
2528                (StoreWord
2529                   (BitsN.fromNat(BitsN.toNat Rt,4),
2530                    (BitsN.fromNat(BitsN.toNat Rn,4),m)))
2531       end
2532     | (false,
2533      (true,
2534       (true,
2535        (true,
2536         (L'0,
2537          (imm5'4,
2538           (imm5'3,
2539            (imm5'2,
2540             (imm5'1,(imm5'0,(Rn'2,(Rn'1,(Rn'0,(Rt'2,(Rt'1,Rt'0))))))))))))))) =>
2541       let
2542         val Rt = BitsN.fromBitstring([Rt'2,Rt'1,Rt'0],3)
2543         val Rn = BitsN.fromBitstring([Rn'2,Rn'1,Rn'0],3)
2544         val imm32 =
2545           BitsN.zeroExtend 32
2546             (BitsN.fromBitstring([imm5'4,imm5'3,imm5'2,imm5'1,imm5'0],5))
2547         val m = immediate_form imm32
2548       in
2549         if (BitsN.fromBitstring([L'0],1)) = (BitsN.B(0x1,1))
2550           then Load
2551                  (LoadByte
2552                     (true,
2553                      (BitsN.fromNat(BitsN.toNat Rt,4),
2554                       (BitsN.fromNat(BitsN.toNat Rn,4),m))))
2555         else Store
2556                (StoreByte
2557                   (BitsN.fromNat(BitsN.toNat Rt,4),
2558                    (BitsN.fromNat(BitsN.toNat Rn,4),m)))
2559       end
2560     | (true,
2561      (false,
2562       (false,
2563        (false,
2564         (L'0,
2565          (imm5'4,
2566           (imm5'3,
2567            (imm5'2,
2568             (imm5'1,(imm5'0,(Rn'2,(Rn'1,(Rn'0,(Rt'2,(Rt'1,Rt'0))))))))))))))) =>
2569       let
2570         val Rt = BitsN.fromBitstring([Rt'2,Rt'1,Rt'0],3)
2571         val Rn = BitsN.fromBitstring([Rn'2,Rn'1,Rn'0],3)
2572         val imm32 =
2573           BitsN.zeroExtend 32
2574             (BitsN.@@
2575                (BitsN.fromBitstring
2576                   ([imm5'4,imm5'3,imm5'2,imm5'1,imm5'0],5),BitsN.B(0x0,1)))
2577         val m = immediate_form imm32
2578       in
2579         if (BitsN.fromBitstring([L'0],1)) = (BitsN.B(0x1,1))
2580           then Load
2581                  (LoadHalf
2582                     (true,
2583                      (BitsN.fromNat(BitsN.toNat Rt,4),
2584                       (BitsN.fromNat(BitsN.toNat Rn,4),m))))
2585         else Store
2586                (StoreHalf
2587                   (BitsN.fromNat(BitsN.toNat Rt,4),
2588                    (BitsN.fromNat(BitsN.toNat Rn,4),m)))
2589       end
2590     | (true,
2591      (false,
2592       (false,
2593        (true,
2594         (L'0,
2595          (Rt'2,
2596           (Rt'1,
2597            (Rt'0,
2598             (imm8'7,
2599              (imm8'6,(imm8'5,(imm8'4,(imm8'3,(imm8'2,(imm8'1,imm8'0))))))))))))))) =>
2600       let
2601         val Rt = BitsN.fromBitstring([Rt'2,Rt'1,Rt'0],3)
2602         val imm32 =
2603           BitsN.zeroExtend 32
2604             (BitsN.@@
2605                (BitsN.fromBitstring
2606                   ([imm8'7,imm8'6,imm8'5,imm8'4,imm8'3,imm8'2,imm8'1,
2607                     imm8'0],8),BitsN.B(0x0,2)))
2608         val m = immediate_form imm32
2609       in
2610         if (BitsN.fromBitstring([L'0],1)) = (BitsN.B(0x1,1))
2611           then Load
2612                  (LoadWord
2613                     (BitsN.fromNat(BitsN.toNat Rt,4),(BitsN.B(0xD,4),m)))
2614         else Store
2615                (StoreWord
2616                   (BitsN.fromNat(BitsN.toNat Rt,4),(BitsN.B(0xD,4),m)))
2617       end
2618     | (true,
2619      (false,
2620       (true,
2621        (false,
2622         (S'0,
2623          (Rd'2,
2624           (Rd'1,
2625            (Rd'0,
2626             (imm8'7,
2627              (imm8'6,(imm8'5,(imm8'4,(imm8'3,(imm8'2,(imm8'1,imm8'0))))))))))))))) =>
2628       let
2629         val imm32 =
2630           BitsN.zeroExtend 32
2631             (BitsN.@@
2632                (BitsN.fromBitstring
2633                   ([imm8'7,imm8'6,imm8'5,imm8'4,imm8'3,imm8'2,imm8'1,
2634                     imm8'0],8),BitsN.B(0x0,2)))
2635         val Rn =
2636           if (BitsN.fromBitstring([S'0],1)) = (BitsN.B(0x1,1))
2637             then BitsN.B(0xD,4)
2638           else BitsN.B(0xF,4)
2639       in
2640         Data
2641           (ArithLogicImmediate
2642              (BitsN.B(0x4,4),
2643               (false,
2644                (BitsN.fromNat
2645                   (BitsN.toNat(BitsN.fromBitstring([Rd'2,Rd'1,Rd'0],3)),4),
2646                 (Rn,imm32)))))
2647       end
2648     | (true,
2649      (false,
2650       (true,
2651        (true,
2652         (false,
2653          (false,
2654           (false,
2655            (false,
2656             (S'0,
2657              (imm7'6,(imm7'5,(imm7'4,(imm7'3,(imm7'2,(imm7'1,imm7'0))))))))))))))) =>
2658       let
2659         val imm32 =
2660           BitsN.zeroExtend 32
2661             (BitsN.@@
2662                (BitsN.fromBitstring
2663                   ([imm7'6,imm7'5,imm7'4,imm7'3,imm7'2,imm7'1,imm7'0],7),
2664                 BitsN.B(0x0,2)))
2665         val opc =
2666           if (BitsN.fromBitstring([S'0],1)) = (BitsN.B(0x1,1))
2667             then BitsN.B(0x2,4)
2668           else BitsN.B(0x4,4)
2669       in
2670         Data
2671           (ArithLogicImmediate
2672              (opc,(false,(BitsN.B(0xD,4),(BitsN.B(0xD,4),imm32)))))
2673       end
2674     | (true,
2675      (false,
2676       (true,
2677        (true,
2678         (false,
2679          (false,
2680           (true,
2681            (false,(U'0,(false,(Rm'2,(Rm'1,(Rm'0,(Rd'2,(Rd'1,Rd'0))))))))))))))) =>
2682       let
2683         val unsigned = (BitsN.fromBitstring([U'0],1)) = (BitsN.B(0x1,1))
2684       in
2685         Media
2686           (ExtendHalfword
2687              (unsigned,
2688               (BitsN.fromNat
2689                  (BitsN.toNat(BitsN.fromBitstring([Rd'2,Rd'1,Rd'0],3)),4),
2690                BitsN.fromNat
2691                  (BitsN.toNat(BitsN.fromBitstring([Rm'2,Rm'1,Rm'0],3)),4))))
2692       end
2693     | (true,
2694      (false,
2695       (true,
2696        (true,
2697         (false,
2698          (false,
2699           (true,
2700            (false,(U'0,(true,(Rm'2,(Rm'1,(Rm'0,(Rd'2,(Rd'1,Rd'0))))))))))))))) =>
2701       let
2702         val unsigned = (BitsN.fromBitstring([U'0],1)) = (BitsN.B(0x1,1))
2703       in
2704         Media
2705           (ExtendByte
2706              (unsigned,
2707               (BitsN.fromNat
2708                  (BitsN.toNat(BitsN.fromBitstring([Rd'2,Rd'1,Rd'0],3)),4),
2709                BitsN.fromNat
2710                  (BitsN.toNat(BitsN.fromBitstring([Rm'2,Rm'1,Rm'0],3)),4))))
2711       end
2712     | (true,
2713      (false,
2714       (true,
2715        (true,
2716         (false,
2717          (true,
2718           (false,
2719            (registers'8,
2720             (registers'7,
2721              (registers'6,
2722               (registers'5,
2723                (registers'4,
2724                 (registers'3,(registers'2,(registers'1,registers'0))))))))))))))) =>
2725       let
2726         val registers =
2727           BitsN.fromBitstring
2728             ([registers'8,registers'7,registers'6,registers'5,
2729               registers'4,registers'3,registers'2,registers'1,registers'0],
2730              9)
2731       in
2732         ( if Nat.<(BitCount 9 registers,1)
2733             then DECODE_UNPREDICTABLE(mc,"Push")
2734           else ()
2735         ; Store(Push registers)
2736         )
2737       end
2738     | (true,
2739      (false,
2740       (true,
2741        (true,(false,(true,(true,(false,(false,(true,(true,(im'0,_)))))))))))) =>
2742       System
2743         (ChangeProcessorState
2744            ((not o L3.equal (BitsN.zero (1)))
2745               (BitsN.fromBitstring([im'0],1))))
2746     | (true,
2747      (false,
2748       (true,
2749        (true,
2750         (true,
2751          (false,
2752           (true,
2753            (false,(opc'1,(opc'0,(Rm'2,(Rm'1,(Rm'0,(Rd'2,(Rd'1,Rd'0))))))))))))))) =>
2754       let
2755         val Rd = BitsN.fromBitstring([Rd'2,Rd'1,Rd'0],3)
2756         val Rm = BitsN.fromBitstring([Rm'2,Rm'1,Rm'0],3)
2757       in
2758         case BitsN.fromBitstring([opc'1,opc'0],2) of
2759            BitsN.B(0x0,_) =>
2760              Media
2761                (ByteReverse
2762                   (BitsN.fromNat(BitsN.toNat Rd,4),
2763                    BitsN.fromNat(BitsN.toNat Rm,4)))
2764          | BitsN.B(0x1,_) =>
2765            Media
2766              (ByteReversePackedHalfword
2767                 (BitsN.fromNat(BitsN.toNat Rd,4),
2768                  BitsN.fromNat(BitsN.toNat Rm,4)))
2769          | BitsN.B(0x3,_) =>
2770            Media
2771              (ByteReverseSignedHalfword
2772                 (BitsN.fromNat(BitsN.toNat Rd,4),
2773                  BitsN.fromNat(BitsN.toNat Rm,4)))
2774          | _ => Undefined(BitsN.B(0x0,32))
2775       end
2776     | (true,
2777      (false,
2778       (true,
2779        (true,
2780         (true,
2781          (true,
2782           (false,
2783            (registers'8,
2784             (registers'7,
2785              (registers'6,
2786               (registers'5,
2787                (registers'4,
2788                 (registers'3,(registers'2,(registers'1,registers'0))))))))))))))) =>
2789       let
2790         val registers =
2791           BitsN.fromBitstring
2792             ([registers'8,registers'7,registers'6,registers'5,
2793               registers'4,registers'3,registers'2,registers'1,registers'0],
2794              9)
2795       in
2796         ( if Nat.<(BitCount 9 registers,1)
2797             then DECODE_UNPREDICTABLE(mc,"POP")
2798           else ()
2799         ; let
2800             val wback = true
2801           in
2802             Load(LoadMultiple(wback,(BitsN.B(0xD,4),registers)))
2803           end
2804         )
2805       end
2806     | (true,
2807      (false,
2808       (true,
2809        (true,
2810         (true,
2811          (true,
2812           (true,
2813            (false,
2814             (imm8'7,
2815              (imm8'6,(imm8'5,(imm8'4,(imm8'3,(imm8'2,(imm8'1,imm8'0))))))))))))))) =>
2816       let
2817         val imm32 =
2818           BitsN.zeroExtend 32
2819             (BitsN.fromBitstring
2820                ([imm8'7,imm8'6,imm8'5,imm8'4,imm8'3,imm8'2,imm8'1,imm8'0],
2821                 8))
2822       in
2823         Hint(Breakpoint imm32)
2824       end
2825     | (true,
2826      (false,
2827       (true,
2828        (true,
2829         (true,
2830          (true,
2831           (true,
2832            (true,
2833             (op'3,(op'2,(op'1,(op'0,(false,(false,(false,false))))))))))))))) =>
2834       (case BitsN.fromBitstring([op'3,op'2,op'1,op'0],4) of
2835           BitsN.B(0x1,_) => Hint(Yield ())
2836         | BitsN.B(0x2,_) => Hint(WaitForEvent ())
2837         | BitsN.B(0x3,_) => Hint(WaitForInterrupt ())
2838         | BitsN.B(0x4,_) => Hint(SendEvent ())
2839         | _ => NoOperation ())
2840     | (true,
2841      (true,
2842       (false,
2843        (false,
2844         (false,
2845          (Rn'2,
2846           (Rn'1,
2847            (Rn'0,
2848             (registers'7,
2849              (registers'6,
2850               (registers'5,
2851                (registers'4,
2852                 (registers'3,(registers'2,(registers'1,registers'0))))))))))))))) =>
2853       let
2854         val registers =
2855           BitsN.fromBitstring
2856             ([registers'7,registers'6,registers'5,registers'4,
2857               registers'3,registers'2,registers'1,registers'0],8)
2858       in
2859         ( if Nat.<(BitCount 8 registers,1)
2860             then DECODE_UNPREDICTABLE(mc,"StoreMultiple")
2861           else ()
2862         ; Store
2863             (StoreMultiple
2864                (BitsN.fromNat
2865                   (BitsN.toNat(BitsN.fromBitstring([Rn'2,Rn'1,Rn'0],3)),4),
2866                 registers))
2867         )
2868       end
2869     | (true,
2870      (true,
2871       (false,
2872        (false,
2873         (true,
2874          (Rn'2,
2875           (Rn'1,
2876            (Rn'0,
2877             (register_list'7,
2878              (register_list'6,
2879               (register_list'5,
2880                (register_list'4,
2881                 (register_list'3,
2882                  (register_list'2,(register_list'1,register_list'0))))))))))))))) =>
2883       let
2884         val Rn = BitsN.fromBitstring([Rn'2,Rn'1,Rn'0],3)
2885         val registers =
2886           BitsN.fromNat
2887             (BitsN.toNat
2888                (BitsN.fromBitstring
2889                   ([register_list'7,register_list'6,register_list'5,
2890                     register_list'4,register_list'3,register_list'2,
2891                     register_list'1,register_list'0],8)),9)
2892       in
2893         ( if Nat.<(BitCount 9 registers,1)
2894             then DECODE_UNPREDICTABLE(mc,"LoadMultiple")
2895           else ()
2896         ; let
2897             val wback = not(BitsN.bit(registers,BitsN.toNat Rn))
2898           in
2899             Load
2900               (LoadMultiple
2901                  (wback,(BitsN.fromNat(BitsN.toNat Rn,4),registers)))
2902           end
2903         )
2904       end
2905     | (true,
2906      (true,
2907       (false,
2908        (true,
2909         (true,
2910          (true,
2911           (true,
2912            (false,
2913             (imm8'7,
2914              (imm8'6,(imm8'5,(imm8'4,(imm8'3,(imm8'2,(imm8'1,imm8'0))))))))))))))) =>
2915       let
2916         val imm32 =
2917           BitsN.zeroExtend 32
2918             (BitsN.fromBitstring
2919                ([imm8'7,imm8'6,imm8'5,imm8'4,imm8'3,imm8'2,imm8'1,imm8'0],
2920                 8))
2921       in
2922         Undefined imm32
2923       end
2924     | (true,
2925      (true,
2926       (false,
2927        (true,
2928         (true,
2929          (true,
2930           (true,
2931            (true,
2932             (imm8'7,
2933              (imm8'6,(imm8'5,(imm8'4,(imm8'3,(imm8'2,(imm8'1,imm8'0))))))))))))))) =>
2934       System
2935         (SupervisorCall
2936            (BitsN.zeroExtend 32
2937               (BitsN.fromBitstring
2938                  ([imm8'7,imm8'6,imm8'5,imm8'4,imm8'3,imm8'2,imm8'1,
2939                    imm8'0],8))))
2940     | (true,
2941      (true,
2942       (false,
2943        (true,
2944         (cond'3,
2945          (cond'2,
2946           (cond'1,
2947            (cond'0,
2948             (imm8'7,
2949              (imm8'6,(imm8'5,(imm8'4,(imm8'3,(imm8'2,(imm8'1,imm8'0))))))))))))))) =>
2950       (if ConditionPassed
2951             (BitsN.fromBitstring([cond'3,cond'2,cond'1,cond'0],4))
2952          then let
2953                 val imm32 =
2954                   BitsN.signExtend 32
2955                     (BitsN.@@
2956                        (BitsN.fromBitstring
2957                           ([imm8'7,imm8'6,imm8'5,imm8'4,imm8'3,imm8'2,
2958                             imm8'1,imm8'0],8),BitsN.B(0x0,1)))
2959               in
2960                 Branch(BranchTarget imm32)
2961               end
2962        else NoOperation ())
2963     | (true,
2964      (true,
2965       (true,
2966        (false,
2967         (false,
2968          (imm11'10,
2969           (imm11'9,
2970            (imm11'8,
2971             (imm11'7,
2972              (imm11'6,
2973               (imm11'5,(imm11'4,(imm11'3,(imm11'2,(imm11'1,imm11'0))))))))))))))) =>
2974       let
2975         val imm32 =
2976           BitsN.signExtend 32
2977             (BitsN.@@
2978                (BitsN.fromBitstring
2979                   ([imm11'10,imm11'9,imm11'8,imm11'7,imm11'6,imm11'5,
2980                     imm11'4,imm11'3,imm11'2,imm11'1,imm11'0],11),
2981                 BitsN.B(0x0,1)))
2982       in
2983         Branch(BranchTarget imm32)
2984       end
2985     | _ => Undefined(BitsN.B(0x0,32))
2986  end;
2987
2988fun DecodeThumb2 h =
2989  let
2990    val mc = Thumb2 h
2991  in
2992    case (boolify'16(L3.fst h),boolify'16(L3.snd h)) of
2993       ((true,
2994         (true,
2995          (true,
2996           (true,
2997            (false,
2998             (false,
2999              (true,
3000               (true,(true,(false,(false,(_,(Rn'3,(Rn'2,(Rn'1,Rn'0))))))))))))))),
3001        (true,
3002         (false,
3003          (_,
3004           (false,
3005            (_,
3006             (_,
3007              (_,
3008               (_,
3009                (SYSm'7,
3010                 (SYSm'6,
3011                  (SYSm'5,(SYSm'4,(SYSm'3,(SYSm'2,(SYSm'1,SYSm'0)))))))))))))))) =>
3012         let
3013           val Rn = BitsN.fromBitstring([Rn'3,Rn'2,Rn'1,Rn'0],4)
3014           val SYSm =
3015             BitsN.fromBitstring
3016               ([SYSm'7,SYSm'6,SYSm'5,SYSm'4,SYSm'3,SYSm'2,SYSm'1,SYSm'0],
3017                8)
3018         in
3019           ( if (Set.mem(Rn,[BitsN.B(0xD,4),BitsN.B(0xF,4)])) orelse
3020                (not(Set.mem
3021                       (SYSm,
3022                        [BitsN.B(0x0,8),BitsN.B(0x1,8),BitsN.B(0x2,8),
3023                         BitsN.B(0x3,8),BitsN.B(0x5,8),BitsN.B(0x6,8),
3024                         BitsN.B(0x7,8),BitsN.B(0x8,8),BitsN.B(0x9,8),
3025                         BitsN.B(0x10,8),BitsN.B(0x11,8),BitsN.B(0x12,8),
3026                         BitsN.B(0x13,8),BitsN.B(0x14,8)])))
3027               then DECODE_UNPREDICTABLE(mc,"MoveToSpecialRegister")
3028             else ()
3029           ; System(MoveToSpecialRegister(SYSm,Rn))
3030           )
3031         end
3032     | ((true,
3033       (true,
3034        (true,
3035         (true,
3036          (false,(false,(true,(true,(true,(false,(true,(true,_)))))))))))),
3037      (true,
3038       (false,
3039        (_,
3040         (false,
3041          (_,
3042           (_,
3043            (_,
3044             (_,
3045              (op'3,
3046               (op'2,
3047                (op'1,(op'0,(option'3,(option'2,(option'1,option'0)))))))))))))))) =>
3048       let
3049         val option =
3050           BitsN.fromBitstring([option'3,option'2,option'1,option'0],4)
3051       in
3052         case BitsN.fromBitstring([op'3,op'2,op'1,op'0],4) of
3053            BitsN.B(0x4,_) => Hint(DataSynchronizationBarrier option)
3054          | BitsN.B(0x5,_) => Hint(DataMemoryBarrier option)
3055          | BitsN.B(0x6,_) =>
3056            Hint(InstructionSynchronizationBarrier option)
3057          | _ => Undefined(BitsN.B(0x0,32))
3058       end
3059     | ((true,
3060       (true,
3061        (true,(true,(false,(false,(true,(true,(true,(true,(true,_))))))))))),
3062      (true,
3063       (false,
3064        (_,
3065         (false,
3066          (Rd'3,
3067           (Rd'2,
3068            (Rd'1,
3069             (Rd'0,
3070              (SYSm'7,
3071               (SYSm'6,(SYSm'5,(SYSm'4,(SYSm'3,(SYSm'2,(SYSm'1,SYSm'0)))))))))))))))) =>
3072       let
3073         val SYSm =
3074           BitsN.fromBitstring
3075             ([SYSm'7,SYSm'6,SYSm'5,SYSm'4,SYSm'3,SYSm'2,SYSm'1,SYSm'0],8)
3076         val Rd = BitsN.fromBitstring([Rd'3,Rd'2,Rd'1,Rd'0],4)
3077       in
3078         ( if (Set.mem(Rd,[BitsN.B(0xD,4),BitsN.B(0xF,4)])) orelse
3079              (not(Set.mem
3080                     (SYSm,
3081                      [BitsN.B(0x0,8),BitsN.B(0x1,8),BitsN.B(0x2,8),
3082                       BitsN.B(0x3,8),BitsN.B(0x5,8),BitsN.B(0x6,8),
3083                       BitsN.B(0x7,8),BitsN.B(0x8,8),BitsN.B(0x9,8),
3084                       BitsN.B(0x10,8),BitsN.B(0x11,8),BitsN.B(0x12,8),
3085                       BitsN.B(0x13,8),BitsN.B(0x14,8)])))
3086             then DECODE_UNPREDICTABLE(mc,"MoveToRegisterFromSpecial")
3087           else ()
3088         ; System(MoveToRegisterFromSpecial(SYSm,Rd))
3089         )
3090       end
3091     | ((true,
3092       (true,
3093        (true,
3094         (true,
3095          (false,
3096           (true,
3097            (true,
3098             (true,
3099              (true,(true,(true,(true,(imm4'3,(imm4'2,(imm4'1,imm4'0))))))))))))))),
3100      (true,
3101       (false,
3102        (true,
3103         (false,
3104          (imm12'11,
3105           (imm12'10,
3106            (imm12'9,
3107             (imm12'8,
3108              (imm12'7,
3109               (imm12'6,
3110                (imm12'5,(imm12'4,(imm12'3,(imm12'2,(imm12'1,imm12'0)))))))))))))))) =>
3111       let
3112         val imm32 =
3113           BitsN.zeroExtend 32
3114             (BitsN.@@
3115                (BitsN.fromBitstring([imm4'3,imm4'2,imm4'1,imm4'0],4),
3116                 BitsN.fromBitstring
3117                   ([imm12'11,imm12'10,imm12'9,imm12'8,imm12'7,imm12'6,
3118                     imm12'5,imm12'4,imm12'3,imm12'2,imm12'1,imm12'0],12)))
3119       in
3120         Undefined imm32
3121       end
3122     | ((true,
3123       (true,
3124        (true,
3125         (true,
3126          (false,
3127           (S'0,
3128            (imm10'9,
3129             (imm10'8,
3130              (imm10'7,
3131               (imm10'6,
3132                (imm10'5,(imm10'4,(imm10'3,(imm10'2,(imm10'1,imm10'0))))))))))))))),
3133      (true,
3134       (true,
3135        (J1'0,
3136         (true,
3137          (J2'0,
3138           (imm11'10,
3139            (imm11'9,
3140             (imm11'8,
3141              (imm11'7,
3142               (imm11'6,
3143                (imm11'5,(imm11'4,(imm11'3,(imm11'2,(imm11'1,imm11'0)))))))))))))))) =>
3144       let
3145         val S = BitsN.fromBitstring([S'0],1)
3146         val I1 = BitsN.~(BitsN.??(BitsN.fromBitstring([J1'0],1),S))
3147         val I2 = BitsN.~(BitsN.??(BitsN.fromBitstring([J2'0],1),S))
3148         val imm32 =
3149           BitsN.signExtend 32
3150             (BitsN.concat
3151                [S,I1,I2,
3152                 BitsN.fromBitstring
3153                   ([imm10'9,imm10'8,imm10'7,imm10'6,imm10'5,imm10'4,
3154                     imm10'3,imm10'2,imm10'1,imm10'0],10),
3155                 BitsN.fromBitstring
3156                   ([imm11'10,imm11'9,imm11'8,imm11'7,imm11'6,imm11'5,
3157                     imm11'4,imm11'3,imm11'2,imm11'1,imm11'0],11),
3158                 BitsN.B(0x0,1)])
3159       in
3160         Branch(BranchLinkImmediate imm32)
3161       end
3162     | _ => Undefined(BitsN.B(0x0,32))
3163  end;
3164
3165fun Decode mc =
3166  case mc of
3167     Thumb h => ( pcinc := (BitsN.B(0x2,32)); DecodeThumb h )
3168   | Thumb2 hs => ( pcinc := (BitsN.B(0x4,32)); DecodeThumb2 hs );
3169
3170fun Next () = Run(Decode(Fetch ()));
3171
3172fun EncodeImmShift (shift_t,shift_n) =
3173  case shift_t of
3174     SRType_LSL => (BitsN.B(0x0,2),BitsN.fromNat(shift_n,5))
3175   | SRType_LSR =>
3176     (BitsN.B(0x1,2),
3177      if shift_n = 32 then BitsN.B(0x0,5) else BitsN.fromNat(shift_n,5))
3178   | SRType_ASR =>
3179     (BitsN.B(0x2,2),
3180      if shift_n = 32 then BitsN.B(0x0,5) else BitsN.fromNat(shift_n,5))
3181   | SRType_ROR => (BitsN.B(0x3,2),BitsN.fromNat(shift_n,5))
3182   | SRType_RRX => (BitsN.B(0x3,2),BitsN.B(0x0,5));
3183
3184fun e_branch (c,(ast,e)) =
3185  case ast of
3186     BranchTarget imm32 =>
3187       (if Set.mem(c,[BitsN.B(0xE,4),BitsN.B(0xF,4)])
3188          then if (BitsN.<=(BitsN.neg(BitsN.B(0x800,32)),imm32)) andalso
3189                  ((BitsN.<=(imm32,BitsN.B(0x7FE,32))) andalso
3190                   (not(e = Enc_Wide)))
3191                 then Thumb16
3192                        (BitsN.@@(BitsN.B(0x1C,5),BitsN.bits(11,1) imm32))
3193               else let
3194                      val S = BitsN.bits(24,24) imm32
3195                      val I1 = BitsN.bits(23,23) imm32
3196                      val I2 = BitsN.bits(22,22) imm32
3197                      val J1 = BitsN.fromBit(I1 = S)
3198                      val J2 = BitsN.fromBit(I2 = S)
3199                      val imm10 = BitsN.bits(21,12) imm32
3200                      val imm11 = BitsN.bits(11,1) imm32
3201                    in
3202                      Thumb32
3203                        (BitsN.concat[BitsN.B(0x1E,5),S,imm10],
3204                         BitsN.concat
3205                           [BitsN.B(0x2,2),J1,BitsN.B(0x1,1),J2,imm11])
3206                    end
3207        else if (BitsN.<=(BitsN.neg(BitsN.B(0x100,32)),imm32)) andalso
3208           ((BitsN.<=(imm32,BitsN.B(0xFE,32))) andalso (not(e = Enc_Wide)))
3209          then Thumb16
3210                 (BitsN.concat[BitsN.B(0xD,4),c,BitsN.bits(8,1) imm32])
3211        else BadCode "BranchTarget")
3212   | BranchExchange Rm =>
3213     Thumb16(BitsN.concat[BitsN.B(0x8E,9),Rm,BitsN.B(0x0,3)])
3214   | BranchLinkExchangeRegister Rm =>
3215     Thumb16(BitsN.concat[BitsN.B(0x8F,9),Rm,BitsN.B(0x0,3)])
3216   | BranchLinkImmediate imm32 =>
3217     let
3218       val S = BitsN.bits(24,24) imm32
3219       val I1 = BitsN.bits(23,23) imm32
3220       val I2 = BitsN.bits(22,22) imm32
3221       val J1 = BitsN.fromBit(I1 = S)
3222       val J2 = BitsN.fromBit(I2 = S)
3223       val imm10 = BitsN.bits(21,12) imm32
3224       val imm11 = BitsN.bits(11,1) imm32
3225     in
3226       Thumb32
3227         (BitsN.concat[BitsN.B(0x1E,5),S,imm10],
3228          BitsN.concat[BitsN.B(0x3,2),J1,BitsN.B(0x1,1),J2,imm11])
3229     end;
3230
3231fun e_data ast =
3232  case ast of
3233     Move(d,imm32) =>
3234       Thumb16
3235         (BitsN.concat
3236            [BitsN.B(0x4,5),BitsN.bits(2,0) d,BitsN.bits(7,0) imm32])
3237   | ArithLogicImmediate(opc,(setflags,(d,(n,imm32)))) =>
3238     (if (Set.mem(opc,[BitsN.B(0x4,4),BitsN.B(0x2,4)])) andalso
3239         ((BitsN.<=+(imm32,BitsN.B(0x7,32))) andalso
3240          (setflags andalso
3241           (not((BitsN.bit(d,3)) orelse (BitsN.bit(n,3))))))
3242        then let
3243               val Rd = BitsN.bits(2,0) d
3244               val Rn = BitsN.bits(2,0) n
3245               val imm3 = BitsN.bits(2,0) imm32
3246               val S = BitsN.bits(1,1) opc
3247             in
3248               Thumb16(BitsN.concat[BitsN.B(0x7,6),S,imm3,Rn,Rd])
3249             end
3250      else if (Set.mem(opc,[BitsN.B(0x4,4),BitsN.B(0x2,4)])) andalso
3251         ((d = n) andalso
3252          ((BitsN.<=+(imm32,BitsN.B(0xFF,32))) andalso
3253           (setflags andalso (not(BitsN.bit(d,3))))))
3254        then let
3255               val Rdn = BitsN.bits(2,0) d
3256               val imm8 = BitsN.bits(7,0) imm32
3257               val S = BitsN.bits(1,1) opc
3258             in
3259               Thumb16(BitsN.concat[BitsN.B(0x3,4),S,Rdn,imm8])
3260             end
3261      else if (opc = (BitsN.B(0x3,4))) andalso
3262         ((imm32 = (BitsN.B(0x0,32))) andalso
3263          (setflags andalso
3264           (not((BitsN.bit(d,3)) orelse (BitsN.bit(n,3))))))
3265        then let
3266               val Rd = BitsN.bits(2,0) d
3267               val Rn = BitsN.bits(2,0) n
3268             in
3269               Thumb16(BitsN.concat[BitsN.B(0x109,10),Rn,Rd])
3270             end
3271      else if (opc = (BitsN.B(0x4,4))) andalso
3272         ((not setflags) andalso
3273          ((Set.mem(n,[BitsN.B(0xD,4),BitsN.B(0xF,4)])) andalso
3274           ((not setflags) andalso
3275            (((BitsN.&&(imm32,BitsN.B(0xFFFFFC03,32))) = (BitsN.B(0x0,32))) andalso
3276             (not(BitsN.bit(d,3)))))))
3277        then let
3278               val Rd = BitsN.bits(2,0) d
3279               val imm8 = BitsN.bits(9,2) imm32
3280               val S = BitsN.fromBit(n = (BitsN.B(0xD,4)))
3281             in
3282               Thumb16(BitsN.concat[BitsN.B(0xA,4),S,Rd,imm8])
3283             end
3284      else if (Set.mem(opc,[BitsN.B(0x4,4),BitsN.B(0x2,4)])) andalso
3285         ((d = (BitsN.B(0xD,4))) andalso
3286          ((n = (BitsN.B(0xD,4))) andalso
3287           ((not setflags) andalso
3288            (((BitsN.&&(imm32,BitsN.B(0xFFFFFE03,32))) = (BitsN.B(0x0,32))) andalso
3289             (not setflags)))))
3290        then let
3291               val imm7 = BitsN.bits(8,2) imm32
3292               val S = BitsN.bits(1,1) opc
3293             in
3294               Thumb16(BitsN.concat[BitsN.B(0xB0,8),S,imm7])
3295             end
3296      else BadCode "ArithLogicImmediate")
3297   | Register(opc,(setflags,(d,(n,m)))) =>
3298     (if (Set.mem(opc,[BitsN.B(0x2,4),BitsN.B(0x4,4)])) andalso
3299         (setflags andalso
3300          (not((BitsN.bit(d,3)) orelse
3301               ((BitsN.bit(n,3)) orelse (BitsN.bit(m,3))))))
3302        then let
3303               val Rn = BitsN.bits(2,0) n
3304               val Rd = BitsN.bits(2,0) d
3305               val Rm = BitsN.bits(2,0) m
3306               val S = BitsN.fromBit(opc = (BitsN.B(0x2,4)))
3307             in
3308               Thumb16(BitsN.concat[BitsN.B(0x6,6),S,Rm,Rn,Rd])
3309             end
3310      else if (Set.mem
3311            (opc,
3312             [BitsN.B(0x0,4),BitsN.B(0x1,4),BitsN.B(0x5,4),BitsN.B(0x6,4),
3313              BitsN.B(0xC,4),BitsN.B(0xE,4)])) andalso
3314         (setflags andalso
3315          ((d = n) andalso (not((BitsN.bit(d,3)) orelse (BitsN.bit(m,3))))))
3316        then let
3317               val Rdn = BitsN.bits(2,0) d
3318               val Rm = BitsN.bits(2,0) m
3319             in
3320               Thumb16(BitsN.concat[BitsN.B(0x10,6),opc,Rm,Rdn])
3321             end
3322      else if (opc = (BitsN.B(0x4,4))) andalso
3323         ((d = n) andalso (not setflags))
3324        then let
3325               val DN = BitsN.bits(3,3) d
3326               val Rdn = BitsN.bits(2,0) d
3327               val Rm = m
3328             in
3329               Thumb16(BitsN.concat[BitsN.B(0x44,8),DN,Rm,Rdn])
3330             end
3331      else BadCode "Register")
3332   | TestCompareRegister(opc,(n,m)) =>
3333     (if not((opc = (BitsN.B(0x1,2))) orelse
3334             ((BitsN.bit(n,3)) orelse (BitsN.bit(m,3))))
3335        then let
3336               val Rn = BitsN.bits(2,0) n
3337               val Rm = BitsN.bits(2,0) m
3338             in
3339               Thumb16(BitsN.concat[BitsN.B(0x42,8),opc,Rm,Rn])
3340             end
3341      else if opc = (BitsN.B(0x2,2))
3342        then let
3343               val N = BitsN.bits(3,3) n
3344               val Rn = BitsN.bits(2,0) n
3345               val Rm = m
3346             in
3347               Thumb16(BitsN.concat[BitsN.B(0x45,8),N,Rm,Rn])
3348             end
3349      else BadCode "TestCompareRegister")
3350   | CompareImmediate(n,imm32) =>
3351     Thumb16
3352       (BitsN.concat
3353          [BitsN.B(0x5,5),BitsN.bits(2,0) n,BitsN.bits(7,0) imm32])
3354   | ShiftImmediate(negate,(setflags,(d,(m,(shift_t,shift_n))))) =>
3355     (if negate andalso
3356         ((shift_t = SRType_LSL) andalso
3357          ((shift_n = 0) andalso
3358           (setflags andalso
3359            (not((BitsN.bit(m,3)) orelse (BitsN.bit(d,3)))))))
3360        then let
3361               val Rm = BitsN.bits(2,0) m
3362               val Rd = BitsN.bits(2,0) d
3363             in
3364               Thumb16(BitsN.concat[BitsN.B(0x10F,10),Rm,Rd])
3365             end
3366      else if (Set.mem(shift_t,[SRType_LSL,SRType_LSR,SRType_ASR])) andalso
3367         (setflags andalso
3368          (not(negate orelse ((BitsN.bit(m,3)) orelse (BitsN.bit(d,3))))))
3369        then let
3370               val Rm = BitsN.bits(2,0) m
3371               val Rd = BitsN.bits(2,0) d
3372               val (typ,imm5) = EncodeImmShift(shift_t,shift_n)
3373             in
3374               Thumb16(BitsN.concat[BitsN.B(0x0,3),typ,imm5,Rm,Rd])
3375             end
3376      else if (shift_t = SRType_LSL) andalso
3377         ((shift_n = 0) andalso (not(negate orelse setflags)))
3378        then let
3379               val D = BitsN.bits(3,3) d
3380               val Rd = BitsN.bits(2,0) d
3381               val Rm = m
3382             in
3383               Thumb16(BitsN.concat[BitsN.B(0x46,8),D,Rm,Rd])
3384             end
3385      else BadCode "ShiftImmediate")
3386   | ShiftRegister(_,(_,(SRType_RRX,_))) => BadCode "ShiftRegister: rrx"
3387   | ShiftRegister(d,(n,(shift_t,m))) =>
3388     let
3389       val Rm = BitsN.bits(2,0) m
3390       val Rdn = BitsN.bits(2,0) d
3391       val opc =
3392         case shift_t of
3393            SRType_LSL => BitsN.B(0x2,3)
3394          | SRType_LSR => BitsN.B(0x3,3)
3395          | SRType_ASR => BitsN.B(0x4,3)
3396          | SRType_ROR => BitsN.B(0x7,3)
3397          | _ => BitsN.B(0x0,3)
3398     in
3399       Thumb16(BitsN.concat[BitsN.B(0x20,7),opc,Rm,Rdn])
3400     end;
3401
3402fun e_media ast =
3403  case ast of
3404     ExtendByte(unsigned,(d,m)) =>
3405       let
3406         val U = BitsN.fromBit unsigned
3407         val Rd = BitsN.bits(2,0) d
3408         val Rm = BitsN.bits(2,0) m
3409       in
3410         Thumb16(BitsN.concat[BitsN.B(0xB2,8),U,BitsN.B(0x1,1),Rm,Rd])
3411       end
3412   | ExtendHalfword(unsigned,(d,m)) =>
3413     let
3414       val U = BitsN.fromBit unsigned
3415       val Rd = BitsN.bits(2,0) d
3416       val Rm = BitsN.bits(2,0) m
3417     in
3418       Thumb16(BitsN.concat[BitsN.B(0xB2,8),U,BitsN.B(0x0,1),Rm,Rd])
3419     end
3420   | ByteReverse(d,m) =>
3421     Thumb16
3422       (BitsN.concat
3423          [BitsN.B(0x2E8,10),BitsN.bits(2,0) m,BitsN.bits(2,0) d])
3424   | ByteReversePackedHalfword(d,m) =>
3425     Thumb16
3426       (BitsN.concat
3427          [BitsN.B(0x2E9,10),BitsN.bits(2,0) m,BitsN.bits(2,0) d])
3428   | ByteReverseSignedHalfword(d,m) =>
3429     Thumb16
3430       (BitsN.concat
3431          [BitsN.B(0x2EB,10),BitsN.bits(2,0) m,BitsN.bits(2,0) d]);
3432
3433fun e_hint (ast,e) =
3434  case ast of
3435     Breakpoint imm32 =>
3436       Thumb16(BitsN.@@(BitsN.B(0xBE,8),BitsN.bits(7,0) imm32))
3437   | DataMemoryBarrier option =>
3438     Thumb32(BitsN.B(0xF3BF,16),BitsN.@@(BitsN.B(0x8F5,12),option))
3439   | DataSynchronizationBarrier option =>
3440     Thumb32(BitsN.B(0xF3BF,16),BitsN.@@(BitsN.B(0x8F4,12),option))
3441   | InstructionSynchronizationBarrier option =>
3442     Thumb32(BitsN.B(0xF3BF,16),BitsN.@@(BitsN.B(0x8F6,12),option))
3443   | SendEvent () =>
3444     if e = Enc_Wide
3445       then Thumb32(BitsN.B(0xF3AF,16),BitsN.B(0x8004,16))
3446     else Thumb16(BitsN.B(0xBF40,16))
3447   | WaitForEvent () =>
3448     if e = Enc_Wide
3449       then Thumb32(BitsN.B(0xF3AF,16),BitsN.B(0x8002,16))
3450     else Thumb16(BitsN.B(0xBF20,16))
3451   | WaitForInterrupt () =>
3452     if e = Enc_Wide
3453       then Thumb32(BitsN.B(0xF3AF,16),BitsN.B(0x8003,16))
3454     else Thumb16(BitsN.B(0xBF30,16))
3455   | Yield () =>
3456     if e = Enc_Wide
3457       then Thumb32(BitsN.B(0xF3AF,16),BitsN.B(0x8001,16))
3458     else Thumb16(BitsN.B(0xBF10,16));
3459
3460fun e_system ast =
3461  case ast of
3462     ChangeProcessorState enable =>
3463       Thumb16
3464         (BitsN.concat
3465            [BitsN.B(0x5B3,11),BitsN.fromBit(not enable),BitsN.B(0x2,4)])
3466   | MoveToRegisterFromSpecial(SYSm,Rd) =>
3467     Thumb32(BitsN.B(0xF3EF,16),BitsN.concat[BitsN.B(0x8,4),Rd,SYSm])
3468   | MoveToSpecialRegister(SYSm,Rn) =>
3469     Thumb32
3470       (BitsN.@@(BitsN.B(0xF38,12),Rn),BitsN.@@(BitsN.B(0x88,8),SYSm))
3471   | SupervisorCall imm32 =>
3472     Thumb16(BitsN.@@(BitsN.B(0xDF,8),BitsN.bits(7,0) imm32));
3473
3474fun e_multiply ast =
3475  case ast of
3476     Multiply32(d,(n,m)) =>
3477       (if d = m
3478          then let
3479                 val Rn = BitsN.bits(2,0) n
3480                 val Rdm = BitsN.bits(2,0) d
3481               in
3482                 Thumb16(BitsN.concat[BitsN.B(0x10D,10),Rn,Rdm])
3483               end
3484        else BadCode "Multiply32");
3485
3486fun e_load ast =
3487  case ast of
3488     LoadWord(t,(n,immediate_form imm32)) =>
3489       (if n = (BitsN.B(0xD,4))
3490          then Thumb16
3491                 (BitsN.concat
3492                    [BitsN.B(0x13,5),BitsN.bits(2,0) t,
3493                     BitsN.bits(9,2) imm32])
3494        else Thumb16
3495               (BitsN.concat
3496                  [BitsN.B(0xD,5),BitsN.bits(6,2) imm32,BitsN.bits(2,0) n,
3497                   BitsN.bits(2,0) t]))
3498   | LoadWord(t,(n,register_form m)) =>
3499     Thumb16
3500       (BitsN.concat
3501          [BitsN.B(0x2C,7),BitsN.bits(2,0) m,BitsN.bits(2,0) n,
3502           BitsN.bits(2,0) t])
3503   | LoadLiteral(t,imm32) =>
3504     Thumb16
3505       (BitsN.concat
3506          [BitsN.B(0x9,5),BitsN.bits(2,0) t,BitsN.bits(9,2) imm32])
3507   | LoadByte(unsigned,(t,(n,immediate_form imm32))) =>
3508     Thumb16
3509       (BitsN.concat
3510          [BitsN.B(0xF,5),BitsN.bits(4,0) imm32,BitsN.bits(2,0) n,
3511           BitsN.bits(2,0) t])
3512   | LoadByte(unsigned,(t,(n,register_form m))) =>
3513     let
3514       val Rm = BitsN.bits(2,0) m
3515       val Rn = BitsN.bits(2,0) n
3516       val Rt = BitsN.bits(2,0) t
3517       val U = BitsN.fromBit unsigned
3518       val S = BitsN.~ U
3519     in
3520       Thumb16(BitsN.concat[BitsN.B(0x5,4),U,BitsN.B(0x1,1),S,Rm,Rn,Rt])
3521     end
3522   | LoadHalf(unsigned,(t,(n,immediate_form imm32))) =>
3523     Thumb16
3524       (BitsN.concat
3525          [BitsN.B(0x11,5),BitsN.bits(5,1) imm32,BitsN.bits(2,0) n,
3526           BitsN.bits(2,0) t])
3527   | LoadHalf(unsigned,(t,(n,register_form m))) =>
3528     Thumb16
3529       (BitsN.concat
3530          [BitsN.B(0xB,5),BitsN.fromBit(not unsigned),BitsN.B(0x1,1),
3531           BitsN.bits(2,0) m,BitsN.bits(2,0) n,BitsN.bits(2,0) t])
3532   | LoadMultiple(wback,(n,registers)) =>
3533     (if n = (BitsN.B(0xD,4))
3534        then Thumb16(BitsN.@@(BitsN.B(0x5E,7),registers))
3535      else Thumb16
3536             (BitsN.concat
3537                [BitsN.B(0x19,5),BitsN.bits(2,0) n,
3538                 BitsN.bits(7,0) registers]));
3539
3540fun e_store ast =
3541  case ast of
3542     StoreWord(t,(n,immediate_form imm32)) =>
3543       (if n = (BitsN.B(0xD,4))
3544          then Thumb16
3545                 (BitsN.concat
3546                    [BitsN.B(0x12,5),BitsN.bits(2,0) t,
3547                     BitsN.bits(9,2) imm32])
3548        else Thumb16
3549               (BitsN.concat
3550                  [BitsN.B(0xC,5),BitsN.bits(6,2) imm32,BitsN.bits(2,0) n,
3551                   BitsN.bits(2,0) t]))
3552   | StoreWord(t,(n,register_form m)) =>
3553     Thumb16
3554       (BitsN.concat
3555          [BitsN.B(0x28,7),BitsN.bits(2,0) m,BitsN.bits(2,0) n,
3556           BitsN.bits(2,0) t])
3557   | StoreByte(t,(n,immediate_form imm32)) =>
3558     Thumb16
3559       (BitsN.concat
3560          [BitsN.B(0xE,5),BitsN.bits(4,0) imm32,BitsN.bits(2,0) n,
3561           BitsN.bits(2,0) t])
3562   | StoreByte(t,(n,register_form m)) =>
3563     Thumb16
3564       (BitsN.concat
3565          [BitsN.B(0x2A,7),BitsN.bits(2,0) m,BitsN.bits(2,0) n,
3566           BitsN.bits(2,0) t])
3567   | StoreHalf(t,(n,immediate_form imm32)) =>
3568     Thumb16
3569       (BitsN.concat
3570          [BitsN.B(0x10,5),BitsN.bits(5,1) imm32,BitsN.bits(2,0) n,
3571           BitsN.bits(2,0) t])
3572   | StoreHalf(t,(n,register_form m)) =>
3573     Thumb16
3574       (BitsN.concat
3575          [BitsN.B(0x29,7),BitsN.bits(2,0) m,BitsN.bits(2,0) n,
3576           BitsN.bits(2,0) t])
3577   | Push registers => Thumb16(BitsN.@@(BitsN.B(0x5A,7),registers))
3578   | StoreMultiple(n,registers) =>
3579     Thumb16(BitsN.concat[BitsN.B(0x18,5),BitsN.bits(2,0) n,registers]);
3580
3581fun instructionEncode (c,(ast,e)) =
3582  case ast of
3583     Branch b => e_branch(c,(b,e))
3584   | Data d => e_data d
3585   | Load l => e_load l
3586   | Store s => e_store s
3587   | Multiply m => e_multiply m
3588   | Media m => e_media m
3589   | System s => e_system s
3590   | Hint h => e_hint(h,e)
3591   | Undefined imm32 =>
3592     (if (not(e = Enc_Wide)) andalso
3593         ((BitsN.bits(31,8) imm32) = (BitsN.B(0x0,24)))
3594        then let
3595               val imm8 = BitsN.bits(7,0) imm32
3596             in
3597               Thumb16(BitsN.@@(BitsN.B(0xDE,8),imm8))
3598             end
3599      else if not(e = Enc_Narrow)
3600        then let
3601               val imm4 = BitsN.bits(15,12) imm32
3602               val imm12 = BitsN.bits(11,0) imm32
3603             in
3604               Thumb32
3605                 (BitsN.@@(BitsN.B(0xF7F,12),imm4),
3606                  BitsN.@@(BitsN.B(0xA,4),imm12))
3607             end
3608      else BadCode "Undefined")
3609   | NoOperation () =>
3610     if e = Enc_Wide
3611       then Thumb32(BitsN.B(0xF3AF,16),BitsN.B(0x8000,16))
3612     else Thumb16(BitsN.B(0xBF00,16));
3613
3614fun SetPassCondition c =
3615  case c of
3616     BitsN.B(0x0,_) => PSR := (PSR_Z_rupd((!PSR),true))
3617   | BitsN.B(0x1,_) => PSR := (PSR_Z_rupd((!PSR),false))
3618   | BitsN.B(0x2,_) => PSR := (PSR_C_rupd((!PSR),true))
3619   | BitsN.B(0x3,_) => PSR := (PSR_C_rupd((!PSR),false))
3620   | BitsN.B(0x4,_) => PSR := (PSR_N_rupd((!PSR),true))
3621   | BitsN.B(0x5,_) => PSR := (PSR_N_rupd((!PSR),false))
3622   | BitsN.B(0x6,_) => PSR := (PSR_V_rupd((!PSR),true))
3623   | BitsN.B(0x7,_) => PSR := (PSR_V_rupd((!PSR),false))
3624   | BitsN.B(0x8,_) =>
3625     ( PSR := (PSR_C_rupd((!PSR),true))
3626     ; PSR := (PSR_Z_rupd((!PSR),false))
3627     )
3628   | BitsN.B(0x9,_) => PSR := (PSR_C_rupd((!PSR),false))
3629   | BitsN.B(0xA,_) =>
3630     ( PSR := (PSR_N_rupd((!PSR),false))
3631     ; PSR := (PSR_V_rupd((!PSR),false))
3632     )
3633   | BitsN.B(0xB,_) =>
3634     ( PSR := (PSR_N_rupd((!PSR),false))
3635     ; PSR := (PSR_V_rupd((!PSR),true))
3636     )
3637   | BitsN.B(0xC,_) =>
3638     ( PSR := (PSR_N_rupd((!PSR),false))
3639     ; PSR := (PSR_V_rupd((!PSR),false))
3640     ; PSR := (PSR_Z_rupd((!PSR),false))
3641     )
3642   | BitsN.B(0xD,_) =>
3643     ( PSR := (PSR_N_rupd((!PSR),false))
3644     ; PSR := (PSR_V_rupd((!PSR),true))
3645     )
3646   | _ => ();
3647
3648fun Encode (c,(ast,enc)) =
3649  ( SetPassCondition c
3650  ; case instructionEncode(c,(ast,enc)) of
3651       Thumb16 a =>
3652         (if (not(enc = Enc_Wide)) andalso ((Decode(Thumb a)) = ast)
3653            then Thumb16 a
3654          else BadCode "Failed to encode")
3655     | Thumb32 a =>
3656       (if (not(enc = Enc_Narrow)) andalso ((Decode(Thumb2 a)) = ast)
3657          then Thumb32 a
3658        else BadCode "Failed to encode")
3659     | mmc => mmc
3660  );
3661
3662val al = (BitsN.B(0xE,4),"")
3663
3664fun stripSpaces s =
3665  L3.fst
3666    (L3.splitr
3667       (fn c => Char.isSpace c,L3.snd(L3.splitl(fn c => Char.isSpace c,s))));
3668
3669fun p_number s =
3670  case String.explode(stripSpaces s) of
3671     #"0" :: (#"b" :: t) => Nat.fromBinString(String.implode t)
3672   | #"0" :: (#"x" :: t) => Nat.fromHexString(String.implode t)
3673   | _ => Nat.fromString s;
3674
3675fun p_signed_number (b,s) =
3676  case p_number s of Option.SOME n => Option.SOME(b,n) | NONE => NONE;
3677
3678fun p_encode_immediate N s =
3679  case p_number s of
3680     Option.SOME n =>
3681       let
3682         val r = BitsN.fromNat(n,N)
3683       in
3684         Option.SOME(n = (BitsN.toNat r),r)
3685       end
3686   | NONE => NONE;
3687
3688fun p_encode_signed_immediate N x =
3689  case p_signed_number x of
3690     Option.SOME(sub,n) =>
3691       let
3692         val r = BitsN.fromNat(n,N)
3693       in
3694         Option.SOME(sub,(n = (BitsN.toNat r),r))
3695       end
3696   | NONE => NONE;
3697
3698fun p_encode_signed_offset N x =
3699  case p_signed_number x of
3700     Option.SOME(sub,n) =>
3701       let
3702         val i =
3703           IntInf.-(if sub then IntInf.~(Nat.toInt n) else Nat.toInt n,4)
3704         val r = BitsN.fromInt(i,N)
3705       in
3706         Option.SOME(i = (BitsN.toInt r),r)
3707       end
3708   | NONE => NONE;
3709
3710fun p_unbounded_immediate s =
3711  case String.explode(stripSpaces s) of
3712     #"#" :: t => p_number(String.implode t)
3713   | _ => NONE;
3714
3715fun p_immediate N s =
3716  case String.explode(stripSpaces s) of
3717     #"#" :: t => p_encode_immediate N (String.implode t)
3718   | _ => NONE;
3719
3720fun p_immediate_number N s =
3721  case String.explode(stripSpaces s) of
3722     #"#" :: t => p_encode_immediate N (String.implode t)
3723   | t => p_encode_immediate N (String.implode t);
3724
3725fun p_signed_immediate N s =
3726  case String.explode(stripSpaces s) of
3727     #"#" :: (#"-" :: t) =>
3728       p_encode_signed_immediate N (true,String.implode t)
3729   | #"#" :: (#"+" :: t) =>
3730     p_encode_signed_immediate N (false,String.implode t)
3731   | #"#" :: t => p_encode_signed_immediate N (false,String.implode t)
3732   | _ => NONE;
3733
3734fun p_signed_offset N s =
3735  case String.explode(stripSpaces s) of
3736     #"+" :: (#"#" :: t) =>
3737       (case p_encode_signed_immediate N (false,String.implode t) of
3738           Option.SOME(false,(true,n)) =>
3739             Option.SOME
3740               (BitsN.<=+(BitsN.BV(0x4,N),n),BitsN.-(n,BitsN.BV(0x4,N)))
3741         | Option.SOME(_,(_,n)) => Option.SOME(false,n)
3742         | NONE => NONE)
3743   | _ => NONE;
3744
3745fun p_offset N s =
3746  case String.explode(stripSpaces s) of
3747     #"-" :: (#"#" :: t) =>
3748       p_encode_signed_offset N (true,String.implode t)
3749   | #"+" :: (#"#" :: t) =>
3750     p_encode_signed_offset N (false,String.implode t)
3751   | _ => NONE;
3752
3753fun p_label s =
3754  case L3.uncurry String.tokens (fn c => Char.isSpace c,s) of
3755     [t] =>
3756       let
3757         val (l,r) =
3758           L3.splitl
3759             (fn c => (Char.isAlphaNum c) orelse (Set.mem(c,[#"_",#"."])),
3760              t)
3761       in
3762         if (r = "") andalso
3763            ((not(l = "")) andalso (not(Char.isDigit(L3.strHd l))))
3764           then Option.SOME l
3765         else NONE
3766       end
3767   | _ => NONE;
3768
3769fun p_cond s =
3770  case s of
3771     "eq" => Option.SOME(BitsN.B(0x0,4))
3772   | "ne" => Option.SOME(BitsN.B(0x1,4))
3773   | "cs" => Option.SOME(BitsN.B(0x2,4))
3774   | "hs" => Option.SOME(BitsN.B(0x2,4))
3775   | "cc" => Option.SOME(BitsN.B(0x3,4))
3776   | "lo" => Option.SOME(BitsN.B(0x3,4))
3777   | "mi" => Option.SOME(BitsN.B(0x4,4))
3778   | "pl" => Option.SOME(BitsN.B(0x5,4))
3779   | "vs" => Option.SOME(BitsN.B(0x6,4))
3780   | "vc" => Option.SOME(BitsN.B(0x7,4))
3781   | "hi" => Option.SOME(BitsN.B(0x8,4))
3782   | "ls" => Option.SOME(BitsN.B(0x9,4))
3783   | "ge" => Option.SOME(BitsN.B(0xA,4))
3784   | "lt" => Option.SOME(BitsN.B(0xB,4))
3785   | "gt" => Option.SOME(BitsN.B(0xC,4))
3786   | "le" => Option.SOME(BitsN.B(0xD,4))
3787   | "al" => Option.SOME(BitsN.B(0xE,4))
3788   | "" => Option.SOME(BitsN.B(0xE,4))
3789   | _ => NONE;
3790
3791fun p_suffix s =
3792  case L3.uncurry String.fields (fn c => c = #".",s) of
3793     [cond,s] =>
3794       (case (p_cond cond,Set.mem(s,["w","n"])) of
3795           (Option.SOME c,true) => Option.SOME(c,s)
3796         | _ => NONE)
3797   | [cond] =>
3798     (case p_cond cond of
3799         Option.SOME c => Option.SOME(c,"")
3800       | NONE => NONE)
3801   | _ => NONE;
3802
3803fun p_al_suffix s =
3804  case p_suffix s of
3805     Option.SOME(BitsN.B(0xE,_),c) => Option.SOME(BitsN.B(0xE,4),c)
3806   | _ => NONE;
3807
3808fun p_special_register s =
3809  case stripSpaces s of
3810     "apsr" => Option.SOME(BitsN.B(0x0,8))
3811   | "iapsr" => Option.SOME(BitsN.B(0x1,8))
3812   | "eapsr" => Option.SOME(BitsN.B(0x2,8))
3813   | "xpsr" => Option.SOME(BitsN.B(0x3,8))
3814   | "ipsr" => Option.SOME(BitsN.B(0x5,8))
3815   | "epsr" => Option.SOME(BitsN.B(0x6,8))
3816   | "iepsr" => Option.SOME(BitsN.B(0x7,8))
3817   | "msp" => Option.SOME(BitsN.B(0x8,8))
3818   | "psp" => Option.SOME(BitsN.B(0x9,8))
3819   | "primask" => Option.SOME(BitsN.B(0x10,8))
3820   | "control" => Option.SOME(BitsN.B(0x14,8))
3821   | n =>
3822     (case p_encode_immediate 8 n of
3823         Option.SOME(true,imm8) => Option.SOME imm8
3824       | _ => NONE);
3825
3826fun p_register s =
3827  case stripSpaces s of
3828     "r0" => Option.SOME(BitsN.B(0x0,4))
3829   | "r1" => Option.SOME(BitsN.B(0x1,4))
3830   | "r2" => Option.SOME(BitsN.B(0x2,4))
3831   | "r3" => Option.SOME(BitsN.B(0x3,4))
3832   | "r4" => Option.SOME(BitsN.B(0x4,4))
3833   | "r5" => Option.SOME(BitsN.B(0x5,4))
3834   | "r6" => Option.SOME(BitsN.B(0x6,4))
3835   | "r7" => Option.SOME(BitsN.B(0x7,4))
3836   | "r8" => Option.SOME(BitsN.B(0x8,4))
3837   | "r9" => Option.SOME(BitsN.B(0x9,4))
3838   | "r10" => Option.SOME(BitsN.B(0xA,4))
3839   | "r11" => Option.SOME(BitsN.B(0xB,4))
3840   | "r12" => Option.SOME(BitsN.B(0xC,4))
3841   | "r13" => Option.SOME(BitsN.B(0xD,4))
3842   | "r14" => Option.SOME(BitsN.B(0xE,4))
3843   | "r15" => Option.SOME(BitsN.B(0xF,4))
3844   | "sp" => Option.SOME(BitsN.B(0xD,4))
3845   | "lr" => Option.SOME(BitsN.B(0xE,4))
3846   | "pc" => Option.SOME(BitsN.B(0xF,4))
3847   | _ => NONE;
3848
3849fun p_register1 l = case l of [r1] => p_register r1 | _ => NONE;
3850
3851fun p_register2 l =
3852  case l of
3853     [r1,r2] =>
3854       (case (p_register r1,p_register r2) of
3855           (Option.SOME v1,Option.SOME v2) => Option.SOME(v1,v2)
3856         | _ => NONE)
3857   | _ => NONE;
3858
3859fun p_register3 l =
3860  case l of
3861     [r1,r2,r3] =>
3862       (case (p_register r1,(p_register r2,p_register r3)) of
3863           (Option.SOME v1,(Option.SOME v2,Option.SOME v3)) =>
3864             Option.SOME(v1,(v2,v3))
3865         | _ => NONE)
3866   | _ => NONE;
3867
3868fun p_shift_amount (typ,(h,s)) =
3869  if Char.isSpace h
3870    then case p_unbounded_immediate s of
3871            Option.SOME n =>
3872              (if (Nat.<(n,32)) orelse
3873                  ((n = 32) andalso (Set.mem(typ,[SRType_LSR,SRType_ASR])))
3874                 then ("",(typ,NAT n))
3875               else ("shift amount too large",(SRType_LSL,NAT 0)))
3876          | NONE =>
3877            (case p_register s of
3878                Option.SOME rs => ("",(typ,REGISTER rs))
3879              | NONE => ("syntax error",(SRType_LSL,NAT 0)))
3880  else ("syntax error",(SRType_LSL,NAT 0));
3881
3882fun p_shift_imm_or_reg s =
3883  case String.explode(stripSpaces s) of
3884     #"l" :: (#"s" :: (#"l" :: (h :: t))) =>
3885       p_shift_amount(SRType_LSL,(h,String.implode t))
3886   | #"l" :: (#"s" :: (#"r" :: (h :: t))) =>
3887     p_shift_amount(SRType_LSR,(h,String.implode t))
3888   | #"a" :: (#"s" :: (#"r" :: (h :: t))) =>
3889     p_shift_amount(SRType_ASR,(h,String.implode t))
3890   | #"r" :: (#"o" :: (#"r" :: (h :: t))) =>
3891     p_shift_amount(SRType_ROR,(h,String.implode t))
3892   | _ => ("syntax error",(SRType_LSL,NAT 0));
3893
3894fun p_arith_logic_full (c,(opc,(setflags,l))) =
3895  case (p_al_suffix c,l) of
3896     (Option.SOME c,[r1,r2,x]) =>
3897       (case p_register2[r1,r2] of
3898           Option.SOME(rd,rn) =>
3899             (case p_register x of
3900                 Option.SOME rm =>
3901                   OK(c,Data(Register(opc,(setflags,(rd,(rn,rm))))))
3902               | NONE =>
3903                 (case p_immediate 32 x of
3904                     Option.SOME(true,imm32) =>
3905                       OK(c,
3906                          Data
3907                            (ArithLogicImmediate
3908                               (opc,(setflags,(rd,(rn,imm32))))))
3909                   | Option.SOME _ => FAIL "immediate too large"
3910                   | NONE => FAIL "syntax error"))
3911         | NONE => FAIL "syntax error")
3912   | _ => FAIL "syntax error";
3913
3914fun p_arith_logic (c,(opc,(setflags,l))) =
3915  case l of
3916     h :: _ =>
3917       (case p_arith_logic_full(c,(opc,(setflags,l))) of
3918           FAIL "syntax error" =>
3919             p_arith_logic_full(c,(opc,(setflags,h :: l)))
3920         | r => r)
3921   | [] => FAIL "syntax error";
3922
3923fun p_test_compare (c,(opc,l)) =
3924  case (p_al_suffix c,l) of
3925     (Option.SOME c,[r1,x]) =>
3926       (case p_register r1 of
3927           Option.SOME rn =>
3928             (case p_register x of
3929                 Option.SOME rm =>
3930                   OK(c,Data(TestCompareRegister(opc,(rn,rm))))
3931               | NONE =>
3932                 (case (opc,p_immediate 32 x) of
3933                     (BitsN.B(0x2,_),Option.SOME(true,imm32)) =>
3934                       OK(c,Data(CompareImmediate(rn,imm32)))
3935                   | (BitsN.B(0x2,_),Option.SOME _) =>
3936                     FAIL "immediate too large"
3937                   | _ => FAIL "syntax error"))
3938         | NONE => FAIL "syntax error")
3939   | _ => FAIL "syntax error";
3940
3941fun p_mov_mvn (c,(negate,(setflags,l))) =
3942  case (p_al_suffix c,l) of
3943     (Option.SOME c,[r1,x]) =>
3944       (case p_register r1 of
3945           Option.SOME rd =>
3946             (case p_register x of
3947                 Option.SOME rm =>
3948                   OK(c,
3949                      Data
3950                        (ShiftImmediate
3951                           (negate,(setflags,(rd,(rm,(SRType_LSL,0)))))))
3952               | NONE =>
3953                 (case (negate,p_immediate 32 x) of
3954                     (false,Option.SOME(true,imm32)) =>
3955                       OK(c,Data(Move(rd,imm32)))
3956                   | (false,Option.SOME _) => FAIL "immediate too large"
3957                   | _ => FAIL "syntax error"))
3958         | NONE => FAIL "syntax error")
3959   | (Option.SOME c,[r1,r2,sh]) =>
3960     (case (negate,(setflags,(p_register2[r1,r2],p_shift_imm_or_reg sh))) of
3961         (false,(true,(Option.SOME(rd,rm),("",(typ,NAT n))))) =>
3962           OK(c,Data(ShiftImmediate(negate,(setflags,(rd,(rm,(typ,n)))))))
3963       | (false,(true,(Option.SOME(rd,rm),("",(typ,REGISTER rs))))) =>
3964         OK(c,Data(ShiftRegister(rd,(rm,(typ,rs)))))
3965       | (false,(true,(Option.SOME _,(err,_)))) => FAIL err
3966       | _ => FAIL "syntax error")
3967   | _ => FAIL "syntax error";
3968
3969fun p_shift_full (c,(typ,l)) =
3970  case (p_al_suffix c,l) of
3971     (Option.SOME c,[r1,r2,s]) =>
3972       (case p_register2[r1,r2] of
3973           Option.SOME(rd,rn) =>
3974             (case p_register s of
3975                 Option.SOME rm =>
3976                   OK(c,Data(ShiftRegister(rd,(rn,(typ,rm)))))
3977               | NONE =>
3978                 (case p_unbounded_immediate s of
3979                     Option.SOME n =>
3980                       (if (Nat.<(n,32)) orelse
3981                           ((n = 32) andalso
3982                            (Set.mem(typ,[SRType_LSR,SRType_ASR])))
3983                          then OK(c,
3984                                  Data
3985                                    (ShiftImmediate
3986                                       (false,(true,(rd,(rn,(typ,n)))))))
3987                        else FAIL "shift amount too large")
3988                   | NONE => FAIL "syntax error"))
3989         | NONE => FAIL "syntax error")
3990   | _ => FAIL "syntax error";
3991
3992fun p_shift (c,(typ,l)) =
3993  case l of
3994     h :: _ =>
3995       (case p_shift_full(c,(typ,l)) of
3996           FAIL "syntax error" => p_shift_full(c,(typ,h :: l))
3997         | r => r)
3998   | [] => FAIL "syntax error";
3999
4000fun p_adr (c,l) =
4001  case (p_al_suffix c,l) of
4002     (Option.SOME c,[r,n]) =>
4003       (case p_register r of
4004           Option.SOME d =>
4005             (case p_signed_offset 10 n of
4006                 Option.SOME(true,imm10) =>
4007                   OK(c,
4008                      Data
4009                        (ArithLogicImmediate
4010                           (BitsN.B(0x4,4),
4011                            (false,
4012                             (d,
4013                              (BitsN.B(0xF,4),
4014                               BitsN.fromNat(BitsN.toNat imm10,32)))))))
4015               | Option.SOME _ => FAIL "bad offset"
4016               | NONE =>
4017                 (case p_label n of
4018                     Option.SOME s =>
4019                       PENDING
4020                         (s,
4021                          (c,
4022                           Data
4023                             (ArithLogicImmediate
4024                                (BitsN.B(0x4,4),
4025                                 (false,
4026                                  (d,(BitsN.B(0xF,4),BitsN.B(0x0,32))))))))
4027                   | NONE => FAIL "syntax error"))
4028         | NONE => FAIL "syntax error")
4029   | _ => FAIL "syntax error";
4030
4031fun p_bx (c,l) =
4032  case (p_al_suffix c,p_register1 l) of
4033     (Option.SOME c,Option.SOME rm) => OK(c,Branch(BranchExchange rm))
4034   | _ => FAIL "syntax error";
4035
4036fun p_bl (c,l) =
4037  case (p_al_suffix c,l) of
4038     (Option.SOME c,[a]) =>
4039       (case p_offset 32 a of
4040           Option.SOME(true,offset) =>
4041             OK(c,Branch(BranchLinkImmediate offset))
4042         | Option.SOME(false,_) => FAIL "offset too large"
4043         | NONE =>
4044           (case p_label a of
4045               Option.SOME label =>
4046                 PENDING
4047                   (label,(c,Branch(BranchLinkImmediate(BitsN.B(0x0,32)))))
4048             | NONE => FAIL "syntax error"))
4049   | _ => FAIL "syntax error";
4050
4051fun p_b (c,l) =
4052  case (p_suffix c,l) of
4053     (Option.SOME c,[a]) =>
4054       (case p_offset 32 a of
4055           Option.SOME(true,offset) => OK(c,Branch(BranchTarget offset))
4056         | Option.SOME(false,_) => FAIL "offset too large"
4057         | NONE =>
4058           (case p_label a of
4059               Option.SOME label =>
4060                 PENDING(label,(c,Branch(BranchTarget(BitsN.B(0x0,32)))))
4061             | NONE => FAIL "syntax error"))
4062   | _ => FAIL "syntax error";
4063
4064fun p_blx (c,l) =
4065  case (p_al_suffix c,p_register1 l) of
4066     (Option.SOME c,Option.SOME rm) =>
4067       OK(c,Branch(BranchLinkExchangeRegister rm))
4068   | _ => FAIL "syntax error";
4069
4070fun p_mul (c,l) =
4071  case (p_al_suffix c,l) of
4072     (Option.SOME c,[_,_,_]) =>
4073       (case p_register3 l of
4074           Option.SOME(rd,(rn,rm)) =>
4075             OK(c,Multiply(Multiply32(rd,(rn,rm))))
4076         | NONE => FAIL "syntax error")
4077   | (Option.SOME c,[_,_]) =>
4078     (case p_register2 l of
4079         Option.SOME(rn,rm) => OK(c,Multiply(Multiply32(rn,(rm,rn))))
4080       | NONE => FAIL "syntax error")
4081   | _ => FAIL "syntax error";
4082
4083fun p_sxtb_etc (c,(half,(unsigned,l))) =
4084  case (p_al_suffix c,l) of
4085     (Option.SOME c,[r1,r2]) =>
4086       (case p_register2[r1,r2] of
4087           Option.SOME(rd,rm) =>
4088             let
4089               val a = (unsigned,(rd,rm))
4090             in
4091               OK(c,Media(if half then ExtendHalfword a else ExtendByte a))
4092             end
4093         | NONE => FAIL "syntax error")
4094   | _ => FAIL "syntax error";
4095
4096fun p_rev (c,l) =
4097  case (p_al_suffix c,p_register2 l) of
4098     (Option.SOME c,Option.SOME(rd,rm)) => OK(c,Media(ByteReverse(rd,rm)))
4099   | _ => FAIL "syntax error";
4100
4101fun p_rev16 (c,l) =
4102  case (p_al_suffix c,p_register2 l) of
4103     (Option.SOME c,Option.SOME(rd,rm)) =>
4104       OK(c,Media(ByteReversePackedHalfword(rd,rm)))
4105   | _ => FAIL "syntax error";
4106
4107fun p_revsh (c,l) =
4108  case (p_al_suffix c,p_register2 l) of
4109     (Option.SOME c,Option.SOME(rd,rm)) =>
4110       OK(c,Media(ByteReverseSignedHalfword(rd,rm)))
4111   | _ => FAIL "syntax error";
4112
4113fun closingRegList s =
4114  case L3.splitr(fn c => c = #"}",stripSpaces s) of
4115     (l,"}") => Option.SOME l
4116   | _ => NONE;
4117
4118fun p_reg_list (w,s) =
4119  case p_register s of
4120     Option.SOME r =>
4121       let
4122         val n = BitsN.toNat r
4123       in
4124         if BitsN.bit(w,n)
4125           then NONE
4126         else Option.SOME(BitsN.||(w,BitsN.<<(BitsN.B(0x1,16),n)))
4127       end
4128   | NONE =>
4129     (case L3.uncurry String.fields (fn c => c = #"-",s) of
4130         [r1,r2] =>
4131           (case p_register2[r1,r2] of
4132               Option.SOME(rlo,rhi) =>
4133                 let
4134                   val lo = BitsN.toNat rlo
4135                   val hi = BitsN.toNat rhi
4136                   val mask =
4137                     BitsN.-
4138                       (BitsN.<<(BitsN.B(0x1,16),Nat.+(hi,1)),
4139                        BitsN.<<(BitsN.B(0x1,16),lo))
4140                 in
4141                   if (Nat.<(lo,hi)) andalso
4142                      ((BitsN.&&(w,mask)) = (BitsN.B(0x0,16)))
4143                     then Option.SOME(BitsN.||(w,mask))
4144                   else NONE
4145                 end
4146             | NONE => NONE)
4147       | _ => NONE);
4148
4149fun p_registers_loop (w,l) =
4150  case l of
4151     [s] =>
4152       (case closingRegList s of
4153           Option.SOME h =>
4154             (case p_reg_list(w,h) of
4155                 Option.SOME r => Option.SOME r
4156               | NONE => NONE)
4157         | NONE => NONE)
4158   | h :: t =>
4159     (case p_reg_list(w,h) of
4160         Option.SOME r => p_registers_loop(r,t)
4161       | NONE => NONE)
4162   | [] => NONE;
4163
4164fun p_registers l =
4165  case l of
4166     h :: t =>
4167       (case String.explode(stripSpaces h) of
4168           #"{" :: r =>
4169             let
4170               val r = stripSpaces(String.implode r)
4171             in
4172               p_registers_loop
4173                 (BitsN.B(0x0,16),if r = "" then t else r :: t)
4174             end
4175         | _ => NONE)
4176   | _ => NONE;
4177
4178fun closingAddress l =
4179  case l of
4180     [s] =>
4181       (case L3.splitr(fn c => c = #"]",stripSpaces s) of
4182           (l,"]") => Option.SOME l
4183         | _ => NONE)
4184   | _ => NONE;
4185
4186fun p_address_mode l =
4187  case l of
4188     h1 :: t1 =>
4189       (case String.explode(stripSpaces h1) of
4190           #"[" :: r1 =>
4191             let
4192               val r1 = String.implode r1
4193             in
4194               case p_register r1 of
4195                  Option.SOME rn =>
4196                    (case closingAddress t1 of
4197                        Option.SOME offset =>
4198                          (case p_signed_immediate 32 offset of
4199                              Option.SOME(false,(true,imm32)) =>
4200                                ("",Option.SOME(rn,immediate_form imm32))
4201                            | Option.SOME(true,_) =>
4202                              ("negative offset",NONE)
4203                            | Option.SOME(_,(false,_)) =>
4204                              ("immediate too large",NONE)
4205                            | NONE =>
4206                              (case p_register offset of
4207                                  Option.SOME rm =>
4208                                    ("",Option.SOME(rn,register_form rm))
4209                                | NONE => ("syntax error",NONE)))
4210                      | NONE => ("syntax error",NONE))
4211                | NONE =>
4212                  (case closingAddress(r1 :: t1) of
4213                      Option.SOME r2 =>
4214                        (case p_register r2 of
4215                            Option.SOME rn =>
4216                              ("",
4217                               Option.SOME
4218                                 (rn,immediate_form(BitsN.B(0x0,32))))
4219                          | NONE => ("syntax error",NONE))
4220                    | _ => ("syntax error",NONE))
4221             end
4222         | _ =>
4223           (case (p_signed_offset 32 h1,t1) of
4224               (Option.SOME(true,imm32),[]) =>
4225                 ("",Option.SOME(BitsN.B(0xF,4),immediate_form imm32))
4226             | (Option.SOME(false,_),[]) => ("bad offset",NONE)
4227             | _ => ("syntax error",NONE)))
4228   | _ => ("syntax error",NONE);
4229
4230fun pick_ldr_str (opc,(rt,(rn,offset))) =
4231  let
4232    val r = (rt,(rn,offset))
4233  in
4234    case opc of
4235       0 =>
4236         (case (rn,offset) of
4237             (BitsN.B(0xF,_),immediate_form imm32) =>
4238               Load(LoadLiteral(rt,imm32))
4239           | _ => Load(LoadWord r))
4240     | 1 => Store(StoreByte r)
4241     | 2 => Store(StoreHalf r)
4242     | _ => Store(StoreWord r)
4243  end;
4244
4245fun p_ldr_str (c,(opc,l)) =
4246  case (p_al_suffix c,l) of
4247     (Option.SOME c,h :: t) =>
4248       (case p_register h of
4249           Option.SOME rt =>
4250             (case p_address_mode t of
4251                 ("",Option.SOME(rn,offset)) =>
4252                   OK(c,pick_ldr_str(opc,(rt,(rn,offset))))
4253               | (err,_) =>
4254                 (case t of
4255                     [l] =>
4256                       (case p_label l of
4257                           Option.SOME s =>
4258                             PENDING
4259                               (s,
4260                                (c,
4261                                 pick_ldr_str
4262                                   (opc,
4263                                    (rt,
4264                                     (BitsN.B(0xF,4),
4265                                      immediate_form(BitsN.B(0x0,32)))))))
4266                         | NONE => FAIL err)
4267                   | _ => FAIL err))
4268         | NONE => FAIL "syntax error")
4269   | _ => FAIL "syntax error";
4270
4271fun p_ldrb_ldrh (c,(unsigned,(byte,l))) =
4272  case (p_al_suffix c,l) of
4273     (Option.SOME c,h :: t) =>
4274       (case p_register h of
4275           Option.SOME rt =>
4276             (case p_address_mode t of
4277                 ("",Option.SOME(rn,offset)) =>
4278                   let
4279                     val r = (unsigned,(rt,(rn,offset)))
4280                   in
4281                     OK(c,Load(if byte then LoadByte r else LoadHalf r))
4282                   end
4283               | (err,_) =>
4284                 (case t of
4285                     [l] =>
4286                       (case p_label l of
4287                           Option.SOME s =>
4288                             let
4289                               val r =
4290                                 (unsigned,
4291                                  (rt,
4292                                   (BitsN.B(0xF,4),
4293                                    immediate_form(BitsN.B(0x0,32)))))
4294                               val a =
4295                                 if byte then LoadByte r else LoadHalf r
4296                             in
4297                               PENDING(s,(c,Load a))
4298                             end
4299                         | NONE => FAIL err)
4300                   | _ => FAIL err))
4301         | NONE => FAIL "syntax error")
4302   | _ => FAIL "syntax error";
4303
4304fun p_pop_push (c,(pop,l)) =
4305  case (p_al_suffix c,p_registers l) of
4306     (Option.SOME c,Option.SOME w) =>
4307       (if pop
4308          then if (BitsN.&&(w,BitsN.B(0x7F00,16))) = (BitsN.B(0x0,16))
4309                 then OK(c,
4310                         Load
4311                           (LoadMultiple
4312                              (true,
4313                               (BitsN.B(0xD,4),
4314                                BitsN.@@
4315                                  (BitsN.bits(15,15) w,BitsN.bits(7,0) w)))))
4316               else FAIL "bad register list"
4317        else if (BitsN.&&(w,BitsN.B(0xBF00,16))) = (BitsN.B(0x0,16))
4318          then OK(c,
4319                  Store
4320                    (Push(BitsN.@@(BitsN.bits(14,14) w,BitsN.bits(7,0) w))))
4321        else FAIL "bad register list")
4322   | (NONE,_) => FAIL "syntax error"
4323   | _ => FAIL "bad register list";
4324
4325fun p_ldm_stm (c,(load,l)) =
4326  case (p_al_suffix c,l) of
4327     (Option.SOME c,h :: t) =>
4328       let
4329         val (r,wb) = L3.splitr(fn c => c = #"!",stripSpaces h)
4330       in
4331         case (p_register r,(p_registers t,Set.mem(wb,["","!"]))) of
4332            (Option.SOME rn,(Option.SOME w,true)) =>
4333              (if (BitsN.bits(15,8) w) = (BitsN.B(0x0,8))
4334                 then let
4335                        val wback = wb = "!"
4336                      in
4337                        if load
4338                          then OK(c,
4339                                  Load
4340                                    (LoadMultiple
4341                                       (wback,(rn,BitsN.bits(8,0) w))))
4342                        else if wback
4343                          then if (rn = (BitsN.B(0xD,4))) andalso
4344                                  ((BitsN.&&(w,BitsN.B(0xBF00,16))) =
4345                                   (BitsN.B(0x0,16)))
4346                                 then OK(c,
4347                                         Store
4348                                           (Push
4349                                              (BitsN.@@
4350                                                 (BitsN.bits(14,14) w,
4351                                                  BitsN.bits(7,0) w))))
4352                               else OK(c,
4353                                       Store
4354                                         (StoreMultiple
4355                                            (rn,BitsN.bits(7,0) w)))
4356                        else FAIL "syntax error"
4357                      end
4358               else FAIL "bad register list")
4359          | (Option.SOME _,(NONE,true)) => FAIL "bad register list"
4360          | _ => FAIL "syntax error"
4361       end
4362   | _ => FAIL "syntax error";
4363
4364fun p_cps (enable,l) =
4365  case l of
4366     [i] =>
4367       (if (stripSpaces i) = "i"
4368          then OK(al,System(ChangeProcessorState enable))
4369        else FAIL "syntax error")
4370   | _ => FAIL "syntax error";
4371
4372fun p_mrs (c,l) =
4373  case (p_al_suffix c,l) of
4374     (Option.SOME c,[r,s]) =>
4375       (case (p_register r,p_special_register s) of
4376           (Option.SOME rd,Option.SOME SYSm) =>
4377             OK(c,System(MoveToRegisterFromSpecial(SYSm,rd)))
4378         | _ => FAIL "syntax error")
4379   | _ => FAIL "syntax error";
4380
4381fun p_msr (c,l) =
4382  case (p_al_suffix c,l) of
4383     (Option.SOME c,[s,r]) =>
4384       (case (p_special_register s,p_register r) of
4385           (Option.SOME SYSm,Option.SOME rn) =>
4386             OK(c,System(MoveToSpecialRegister(SYSm,rn)))
4387         | _ => FAIL "syntax error")
4388   | _ => FAIL "syntax error";
4389
4390fun p_barrier_option l =
4391  case l of
4392     [] => Option.SOME(BitsN.B(0xF,4))
4393   | [s] =>
4394     (case stripSpaces s of
4395         "sy" => Option.SOME(BitsN.B(0xF,4))
4396       | "st" => Option.SOME(BitsN.B(0xE,4))
4397       | "ish" => Option.SOME(BitsN.B(0xB,4))
4398       | "ishst" => Option.SOME(BitsN.B(0xA,4))
4399       | "nsh" => Option.SOME(BitsN.B(0x7,4))
4400       | "nshst" => Option.SOME(BitsN.B(0x6,4))
4401       | "osh" => Option.SOME(BitsN.B(0x3,4))
4402       | "oshst" => Option.SOME(BitsN.B(0x2,4))
4403       | n =>
4404         (case Nat.fromString n of
4405             Option.SOME v => Option.SOME(BitsN.fromNat(v,4))
4406           | NONE => NONE))
4407   | _ => NONE;
4408
4409fun p_dmb_dsb (c,(sync,l)) =
4410  case (p_suffix c,p_barrier_option l) of
4411     (Option.SOME c,Option.SOME option) =>
4412       OK(c,
4413          Hint
4414            (if sync
4415               then DataSynchronizationBarrier option
4416             else DataMemoryBarrier option))
4417   | _ => FAIL "syntax error";
4418
4419fun p_isb (c,l) =
4420  case (p_suffix c,p_barrier_option l) of
4421     (Option.SOME c,Option.SOME(BitsN.B(0xF,_))) =>
4422       OK(c,Hint(InstructionSynchronizationBarrier(BitsN.B(0xF,4))))
4423   | _ => FAIL "syntax error";
4424
4425fun p_call (c,(opc,l)) =
4426  case (p_al_suffix c,l) of
4427     (Option.SOME c,[imm]) =>
4428       (case p_immediate_number 32 imm of
4429           Option.SOME(true,imm32) =>
4430             let
4431               val ast =
4432                 case opc of
4433                    0 => Undefined imm32
4434                  | 1 => System(SupervisorCall imm32)
4435                  | _ => Hint(Breakpoint imm32)
4436             in
4437               OK(c,ast)
4438             end
4439         | Option.SOME(false,_) => FAIL "immediate too large"
4440         | _ => FAIL "syntax error")
4441   | _ => FAIL "syntax error";
4442
4443fun p_noarg (c,i) =
4444  case p_al_suffix c of
4445     Option.SOME c => OK(c,i)
4446   | NONE => FAIL "syntax error";
4447
4448fun p_tokens s =
4449  let
4450    val (l,r) =
4451      L3.splitl
4452        (fn c => not(Char.isSpace c),
4453         L3.lowercase(L3.snd(L3.splitl(fn c => Char.isSpace c,s))))
4454    val r = L3.uncurry String.fields (fn c => c = #",",r)
4455    val r =
4456      if ((L3.length r) = 1) andalso ((stripSpaces(List.hd r)) = "")
4457        then []
4458      else r
4459  in
4460    l :: r
4461  end;
4462
4463fun instructionFromString s =
4464  case p_tokens s of
4465     v'0 :: v'1 =>
4466       (case (String.explode v'0,v'1) of
4467           (#"a" :: (#"d" :: (#"r" :: c)),l) => p_adr(String.implode c,l)
4468         | (#"a" :: (#"n" :: (#"d" :: (#"s" :: c))),l) =>
4469           p_arith_logic(String.implode c,(BitsN.B(0x0,4),(true,l)))
4470         | (#"e" :: (#"o" :: (#"r" :: (#"s" :: c))),l) =>
4471           p_arith_logic(String.implode c,(BitsN.B(0x1,4),(true,l)))
4472         | (#"s" :: (#"u" :: (#"b" :: (#"s" :: c))),l) =>
4473           p_arith_logic(String.implode c,(BitsN.B(0x2,4),(true,l)))
4474         | (#"s" :: (#"u" :: (#"b" :: c)),l) =>
4475           p_arith_logic(String.implode c,(BitsN.B(0x2,4),(false,l)))
4476         | (#"r" :: (#"s" :: (#"b" :: (#"s" :: c))),l) =>
4477           p_arith_logic(String.implode c,(BitsN.B(0x3,4),(true,l)))
4478         | (#"a" :: (#"d" :: (#"d" :: (#"s" :: c))),l) =>
4479           p_arith_logic(String.implode c,(BitsN.B(0x4,4),(true,l)))
4480         | (#"a" :: (#"d" :: (#"d" :: c)),l) =>
4481           p_arith_logic(String.implode c,(BitsN.B(0x4,4),(false,l)))
4482         | (#"a" :: (#"d" :: (#"c" :: (#"s" :: c))),l) =>
4483           p_arith_logic(String.implode c,(BitsN.B(0x5,4),(true,l)))
4484         | (#"s" :: (#"b" :: (#"c" :: (#"s" :: c))),l) =>
4485           p_arith_logic(String.implode c,(BitsN.B(0x6,4),(true,l)))
4486         | (#"o" :: (#"r" :: (#"r" :: (#"s" :: c))),l) =>
4487           p_arith_logic(String.implode c,(BitsN.B(0xC,4),(true,l)))
4488         | (#"b" :: (#"i" :: (#"c" :: (#"s" :: c))),l) =>
4489           p_arith_logic(String.implode c,(BitsN.B(0xE,4),(true,l)))
4490         | (#"t" :: (#"s" :: (#"t" :: c)),l) =>
4491           p_test_compare(String.implode c,(BitsN.B(0x0,2),l))
4492         | (#"c" :: (#"m" :: (#"p" :: c)),l) =>
4493           p_test_compare(String.implode c,(BitsN.B(0x2,2),l))
4494         | (#"c" :: (#"m" :: (#"n" :: c)),l) =>
4495           p_test_compare(String.implode c,(BitsN.B(0x3,2),l))
4496         | (#"m" :: (#"o" :: (#"v" :: (#"s" :: c))),l) =>
4497           p_mov_mvn(String.implode c,(false,(true,l)))
4498         | (#"m" :: (#"o" :: (#"v" :: c)),l) =>
4499           p_mov_mvn(String.implode c,(false,(false,l)))
4500         | (#"m" :: (#"v" :: (#"n" :: (#"s" :: c))),l) =>
4501           p_mov_mvn(String.implode c,(true,(true,l)))
4502         | (#"l" :: (#"s" :: (#"l" :: (#"s" :: c))),l) =>
4503           p_shift(String.implode c,(SRType_LSL,l))
4504         | (#"l" :: (#"s" :: (#"r" :: (#"s" :: c))),l) =>
4505           p_shift(String.implode c,(SRType_LSR,l))
4506         | (#"a" :: (#"s" :: (#"r" :: (#"s" :: c))),l) =>
4507           p_shift(String.implode c,(SRType_ASR,l))
4508         | (#"r" :: (#"o" :: (#"r" :: (#"s" :: c))),l) =>
4509           p_shift(String.implode c,(SRType_ROR,l))
4510         | (#"m" :: (#"u" :: (#"l" :: (#"s" :: c))),l) =>
4511           p_mul(String.implode c,l)
4512         | (#"s" :: (#"x" :: (#"t" :: (#"b" :: c))),l) =>
4513           p_sxtb_etc(String.implode c,(false,(false,l)))
4514         | (#"u" :: (#"x" :: (#"t" :: (#"b" :: c))),l) =>
4515           p_sxtb_etc(String.implode c,(false,(true,l)))
4516         | (#"s" :: (#"x" :: (#"t" :: (#"h" :: c))),l) =>
4517           p_sxtb_etc(String.implode c,(true,(false,l)))
4518         | (#"u" :: (#"x" :: (#"t" :: (#"h" :: c))),l) =>
4519           p_sxtb_etc(String.implode c,(true,(true,l)))
4520         | (#"r" :: (#"e" :: (#"v" :: (#"1" :: (#"6" :: c)))),l) =>
4521           p_rev16(String.implode c,l)
4522         | (#"r" :: (#"e" :: (#"v" :: (#"s" :: (#"h" :: c)))),l) =>
4523           p_revsh(String.implode c,l)
4524         | (#"r" :: (#"e" :: (#"v" :: c)),l) => p_rev(String.implode c,l)
4525         | (#"l" :: (#"d" :: (#"r" :: (#"b" :: c))),l) =>
4526           p_ldrb_ldrh(String.implode c,(true,(true,l)))
4527         | (#"l" :: (#"d" :: (#"r" :: (#"s" :: (#"b" :: c)))),l) =>
4528           p_ldrb_ldrh(String.implode c,(false,(true,l)))
4529         | (#"l" :: (#"d" :: (#"r" :: (#"h" :: c))),l) =>
4530           p_ldrb_ldrh(String.implode c,(true,(false,l)))
4531         | (#"l" :: (#"d" :: (#"r" :: (#"s" :: (#"h" :: c)))),l) =>
4532           p_ldrb_ldrh(String.implode c,(false,(false,l)))
4533         | (#"l" :: (#"d" :: (#"r" :: c)),l) =>
4534           p_ldr_str(String.implode c,(0,l))
4535         | (#"s" :: (#"t" :: (#"r" :: (#"b" :: c))),l) =>
4536           p_ldr_str(String.implode c,(1,l))
4537         | (#"s" :: (#"t" :: (#"r" :: (#"h" :: c))),l) =>
4538           p_ldr_str(String.implode c,(2,l))
4539         | (#"s" :: (#"t" :: (#"r" :: c)),l) =>
4540           p_ldr_str(String.implode c,(3,l))
4541         | (#"p" :: (#"o" :: (#"p" :: c)),l) =>
4542           p_pop_push(String.implode c,(true,l))
4543         | (#"p" :: (#"u" :: (#"s" :: (#"h" :: c))),l) =>
4544           p_pop_push(String.implode c,(false,l))
4545         | (#"l" :: (#"d" :: (#"m" :: (#"i" :: (#"a" :: c)))),l) =>
4546           p_ldm_stm(String.implode c,(true,l))
4547         | (#"l" :: (#"d" :: (#"m" :: (#"f" :: (#"d" :: c)))),l) =>
4548           p_ldm_stm(String.implode c,(true,l))
4549         | (#"l" :: (#"d" :: (#"m" :: c)),l) =>
4550           p_ldm_stm(String.implode c,(true,l))
4551         | (#"s" :: (#"t" :: (#"m" :: (#"i" :: (#"a" :: c)))),l) =>
4552           p_ldm_stm(String.implode c,(false,l))
4553         | (#"s" :: (#"t" :: (#"m" :: (#"e" :: (#"a" :: c)))),l) =>
4554           p_ldm_stm(String.implode c,(false,l))
4555         | (#"s" :: (#"t" :: (#"m" :: c)),l) =>
4556           p_ldm_stm(String.implode c,(false,l))
4557         | ([#"c",#"p",#"s",#"i",#"e"],l) => p_cps(true,l)
4558         | ([#"c",#"p",#"s",#"i",#"d"],l) => p_cps(false,l)
4559         | (#"m" :: (#"r" :: (#"s" :: c)),l) => p_mrs(String.implode c,l)
4560         | (#"m" :: (#"s" :: (#"r" :: c)),l) => p_msr(String.implode c,l)
4561         | (#"u" :: (#"d" :: (#"f" :: c)),l) =>
4562           p_call(String.implode c,(0,l))
4563         | (#"s" :: (#"v" :: (#"c" :: c)),l) =>
4564           p_call(String.implode c,(1,l))
4565         | (#"b" :: (#"k" :: (#"p" :: (#"t" :: c))),l) =>
4566           p_call(String.implode c,(2,l))
4567         | (#"d" :: (#"m" :: (#"b" :: c)),l) =>
4568           p_dmb_dsb(String.implode c,(false,l))
4569         | (#"d" :: (#"s" :: (#"b" :: c)),l) =>
4570           p_dmb_dsb(String.implode c,(true,l))
4571         | (#"i" :: (#"s" :: (#"b" :: c)),l) => p_isb(String.implode c,l)
4572         | (#"n" :: (#"o" :: (#"p" :: c)),[]) =>
4573           p_noarg(String.implode c,NoOperation ())
4574         | (#"s" :: (#"e" :: (#"v" :: c)),[]) =>
4575           p_noarg(String.implode c,Hint(SendEvent ()))
4576         | (#"w" :: (#"f" :: (#"e" :: c)),[]) =>
4577           p_noarg(String.implode c,Hint(WaitForEvent ()))
4578         | (#"w" :: (#"f" :: (#"i" :: c)),[]) =>
4579           p_noarg(String.implode c,Hint(WaitForInterrupt ()))
4580         | (#"y" :: (#"i" :: (#"e" :: (#"l" :: (#"d" :: c)))),[]) =>
4581           p_noarg(String.implode c,Hint(Yield ()))
4582         | ([#"b",#"l",c1,c2,#".",e],l) =>
4583           p_bl(String.implode[c1,c2,#".",e],l)
4584         | ([#"b",#"l",#".",e],l) => p_bl(String.implode[#".",e],l)
4585         | ([#"b",#"l"],l) => p_bl("",l)
4586         | (#"b" :: (#"x" :: c),l) => p_bx(String.implode c,l)
4587         | (#"b" :: (#"l" :: (#"x" :: c)),l) => p_blx(String.implode c,l)
4588         | (#"b" :: c,l) => p_b(String.implode c,l)
4589         | ([#"h",#"a",#"l",#"f"],[w]) =>
4590           (case p_encode_immediate 16 w of
4591               Option.SOME(true,w) => HALFWORD w
4592             | Option.SOME _ => FAIL "immediate too large"
4593             | NONE => FAIL "syntax error")
4594         | _ => FAIL "Unrecognised op-code")
4595   | _ => FAIL "Unrecognised op-code";
4596
4597fun halfString w = L3.padLeftString(#"0",(4,BitsN.toHexString w));
4598
4599fun EncodeThumb s =
4600  case instructionFromString s of
4601     OK((c,e),ast) =>
4602       let
4603         val enc =
4604           case e of "n" => Enc_Narrow | "w" => Enc_Wide | _ => Enc_Thumb
4605       in
4606         case instructionEncode(c,(ast,enc)) of
4607            Thumb16 w => ("",Option.SOME(halfString w))
4608          | Thumb32(w1,w2) =>
4609            ("",
4610             Option.SOME(String.concat[halfString w1," ",halfString w2]))
4611          | BadCode err => ("Encode error: " ^ err,NONE)
4612       end
4613   | HALFWORD w => ("",Option.SOME(halfString w))
4614   | PENDING _ => ("Contains label",NONE)
4615   | FAIL err => ("Parse error: " ^ err,NONE);
4616
4617fun s_cond c =
4618  case c of
4619     BitsN.B(0x0,_) => "eq"
4620   | BitsN.B(0x1,_) => "ne"
4621   | BitsN.B(0x2,_) => "cs"
4622   | BitsN.B(0x3,_) => "cc"
4623   | BitsN.B(0x4,_) => "mi"
4624   | BitsN.B(0x5,_) => "pl"
4625   | BitsN.B(0x6,_) => "vs"
4626   | BitsN.B(0x7,_) => "vc"
4627   | BitsN.B(0x8,_) => "hi"
4628   | BitsN.B(0x9,_) => "ls"
4629   | BitsN.B(0xA,_) => "ge"
4630   | BitsN.B(0xB,_) => "lt"
4631   | BitsN.B(0xC,_) => "gt"
4632   | BitsN.B(0xD,_) => "le"
4633   | _ => "";
4634
4635fun s_reg r =
4636  case r of
4637     BitsN.B(0xD,_) => "sp"
4638   | BitsN.B(0xE,_) => "lr"
4639   | BitsN.B(0xF,_) => "pc"
4640   | _ => "r" ^ (Nat.toString(BitsN.toNat r));
4641
4642fun s_reg2 (r1,r2) = String.concat[s_reg r1,", ",s_reg r2];
4643
4644fun s_reg3 (r1,(r2,r3)) = String.concat[s_reg2(r1,r2),", ",s_reg r3];
4645
4646fun s_reg4 (r1,(r2,(r3,r4))) =
4647  String.concat[s_reg3(r1,(r2,r3)),", ",s_reg r4];
4648
4649fun s_hex N v =
4650  if BitsN.<+(v,BitsN.BV(0x64,N))
4651    then Nat.toString(BitsN.toNat v)
4652  else "0x" ^ (BitsN.toHexString v);
4653
4654fun s_offset imm32 =
4655  let
4656    val imm32 = BitsN.+(imm32,BitsN.B(0x4,32))
4657  in
4658    if BitsN.<(imm32,BitsN.B(0x0,32))
4659      then "-#" ^ (s_hex 32 (BitsN.neg imm32))
4660    else "+#" ^ (s_hex 32 imm32)
4661  end;
4662
4663fun s_maybe_offset imm32 =
4664  if imm32 = (BitsN.B(0x0,32)) then "" else ", #" ^ (s_hex 32 imm32);
4665
4666fun s_special_reg SYSm =
4667  case SYSm of
4668     BitsN.B(0x0,_) => "apsr"
4669   | BitsN.B(0x1,_) => "iapsr"
4670   | BitsN.B(0x2,_) => "eapsr"
4671   | BitsN.B(0x3,_) => "xpsr"
4672   | BitsN.B(0x5,_) => "ipsr"
4673   | BitsN.B(0x6,_) => "epsr"
4674   | BitsN.B(0x7,_) => "iepsr"
4675   | BitsN.B(0x8,_) => "msp"
4676   | BitsN.B(0x9,_) => "psp"
4677   | BitsN.B(0x10,_) => "primask"
4678   | BitsN.B(0x14,_) => "control"
4679   | _ => Nat.toString(BitsN.toNat SYSm);
4680
4681fun s_barrier_option option =
4682  case option of
4683     BitsN.B(0x2,_) => "oshst"
4684   | BitsN.B(0x3,_) => "osh"
4685   | BitsN.B(0x6,_) => "nshst"
4686   | BitsN.B(0x7,_) => "nsh"
4687   | BitsN.B(0xA,_) => "ishst"
4688   | BitsN.B(0xB,_) => "ish"
4689   | BitsN.B(0xE,_) => "st"
4690   | BitsN.B(0xF,_) => "sy"
4691   | _ => Nat.toString(BitsN.toNat option);
4692
4693fun s_imm_form (t,(n,imm32)) =
4694  String.concat[s_reg t,", [",s_reg n,s_maybe_offset imm32,"]"];
4695
4696fun s_reg_form (t,(n,m)) = String.concat[s_reg t,", [",s_reg2(n,m),"]"];
4697
4698fun contiguous (a,(i,l)) =
4699  case l of
4700     [] => a
4701   | y :: x =>
4702     contiguous
4703       (if y
4704          then case a of
4705                  [] => [(i,i)]
4706                | (b,t) :: r =>
4707                  (if (Nat.+(i,1)) = b then (i,t) :: r else (i,i) :: a)
4708        else a,(Nat.-(i,1),x));
4709
4710fun s_registers_from_contiguous (a,l) =
4711  case l of
4712     [] => a
4713   | (b,t) :: r =>
4714     let
4715       val d = Nat.-(t,b)
4716     in
4717       s_registers_from_contiguous
4718         (if d = 0
4719            then String.concat[a,", ",s_reg(BitsN.fromNat(b,4))]
4720          else if d = 1
4721            then String.concat
4722                   [a,", ",s_reg2(BitsN.fromNat(b,4),BitsN.fromNat(t,4))]
4723          else String.concat
4724                 [a,", ",s_reg(BitsN.fromNat(b,4)),"-",
4725                  s_reg(BitsN.fromNat(t,4))],r)
4726     end;
4727
4728fun s_registers N l =
4729  case String.explode
4730    (s_registers_from_contiguous
4731       ("",
4732        contiguous
4733          ([],(Nat.-(BitsN.size(BitsN.BV(0x0,N)),1),BitsN.toBitstring l)))) of
4734     [] => "{}"
4735   | #"," :: (#" " :: s) => String.concat["{",String.implode s,"}"]
4736   | _ => "???";
4737
4738fun s_test_compare opc =
4739  case opc of
4740     BitsN.B(0x0,_) => "tst"
4741   | BitsN.B(0x1,_) => "teq"
4742   | BitsN.B(0x2,_) => "cmp"
4743   | BitsN.B(0x3,_) => "cmn"
4744   | _ => raise General.Bind;
4745
4746fun s_arith_logic opc =
4747  case opc of
4748     BitsN.B(0x0,_) => "and"
4749   | BitsN.B(0x1,_) => "eor"
4750   | BitsN.B(0x2,_) => "sub"
4751   | BitsN.B(0x3,_) => "rsb"
4752   | BitsN.B(0x4,_) => "add"
4753   | BitsN.B(0x5,_) => "adc"
4754   | BitsN.B(0x6,_) => "sbc"
4755   | BitsN.B(0x7,_) => "rsc"
4756   | BitsN.B(0x8,_) => "tst"
4757   | BitsN.B(0x9,_) => "teq"
4758   | BitsN.B(0xA,_) => "cmp"
4759   | BitsN.B(0xB,_) => "cmn"
4760   | BitsN.B(0xC,_) => "orr"
4761   | BitsN.B(0xD,_) => "mov"
4762   | BitsN.B(0xE,_) => "bic"
4763   | BitsN.B(0xF,_) => "mvn"
4764   | _ => raise General.Bind;
4765
4766fun s_shift shift_t =
4767  case shift_t of
4768     SRType_LSL => "lsl"
4769   | SRType_LSR => "lsr"
4770   | SRType_ASR => "asr"
4771   | SRType_ROR => "ror"
4772   | SRType_RRX => "rrx";
4773
4774fun s_shift_n (shift_t,shift_n) =
4775  case (shift_t,shift_n) of
4776     (SRType_LSL,0) => ""
4777   | (SRType_RRX,1) => ", rrx"
4778   | _ => String.concat[", ",s_shift shift_t," #",Nat.toString shift_n];
4779
4780fun s_shift_r (add,(r,(shift_t,shift_n))) =
4781  String.concat
4782    [", ",if add then "" else "-",s_reg r,s_shift_n(shift_t,shift_n)];
4783
4784fun s_branch (c,ast) =
4785  case ast of
4786     BranchTarget imm32 => ("b" ^ (s_cond c),s_offset imm32)
4787   | BranchExchange m => ("bx",s_reg m)
4788   | BranchLinkImmediate imm32 => ("bl",s_offset imm32)
4789   | BranchLinkExchangeRegister m => ("blx",s_reg m);
4790
4791fun s_data ast =
4792  case ast of
4793     Move(d,imm12) => ("movs",String.concat[s_reg d,", #",s_hex 32 imm12])
4794   | ArithLogicImmediate(opc,(setflags,(d,(n,imm12)))) =>
4795     ((s_arith_logic opc) ^ (if setflags then "s" else ""),
4796      String.concat[s_reg2(d,n),", #",s_hex 32 imm12])
4797   | Register(opc,(setflags,(d,(n,m)))) =>
4798     ((s_arith_logic opc) ^ (if setflags then "s" else ""),s_reg3(d,(n,m)))
4799   | TestCompareRegister(opc,(n,m)) => (s_test_compare opc,s_reg2(n,m))
4800   | CompareImmediate(n,imm32) =>
4801     ("cmp",String.concat[s_reg n,", #",s_hex 32 imm32])
4802   | ShiftImmediate(true,(setflags,(d,(m,(shift_t,shift_n))))) =>
4803     ("mvn" ^ (if setflags then "s" else ""),
4804      (s_reg2(d,m)) ^ (s_shift_n(shift_t,shift_n)))
4805   | ShiftImmediate(false,(setflags,(d,(m,(SRType_LSL,0))))) =>
4806     ("mov" ^ (if setflags then "s" else ""),s_reg2(d,m))
4807   | ShiftImmediate(false,(setflags,(d,(m,(shift_t,shift_n))))) =>
4808     ((s_shift shift_t) ^ (if setflags then "s" else ""),
4809      (s_reg2(d,m))
4810        ^
4811        (if (shift_t = SRType_RRX) andalso (shift_n = 1)
4812           then ""
4813         else ", #" ^ (Nat.toString shift_n)))
4814   | ShiftRegister(d,(n,(shift_t,m))) =>
4815     ((s_shift shift_t) ^ "s",s_reg3(d,(n,m)));
4816
4817fun s_load ast =
4818  case ast of
4819     LoadWord(t,(n,immediate_form imm32)) =>
4820       ("ldr",s_imm_form(t,(n,imm32)))
4821   | LoadWord(t,(n,register_form m)) => ("ldr",s_reg_form(t,(n,m)))
4822   | LoadLiteral(t,imm32) =>
4823     ("ldr",String.concat[s_reg t,", [pc",s_maybe_offset imm32,"]"])
4824   | LoadByte(unsigned,(t,(n,immediate_form imm32))) =>
4825     ("ldr" ^ (if unsigned then "b" else "sb"),s_imm_form(t,(n,imm32)))
4826   | LoadByte(unsigned,(t,(n,register_form m))) =>
4827     ("ldr" ^ (if unsigned then "b" else "sb"),s_reg_form(t,(n,m)))
4828   | LoadHalf(unsigned,(t,(n,immediate_form imm32))) =>
4829     ("ldr" ^ (if unsigned then "h" else "sh"),s_imm_form(t,(n,imm32)))
4830   | LoadHalf(unsigned,(t,(n,register_form m))) =>
4831     ("ldr" ^ (if unsigned then "h" else "sh"),s_reg_form(t,(n,m)))
4832   | LoadMultiple(true,(BitsN.B(0xD,4),registers)) =>
4833     ("pop",
4834      s_registers 16
4835        (BitsN.concat
4836           [BitsN.bits(8,8) registers,BitsN.B(0x0,7),
4837            BitsN.bits(7,0) registers]))
4838   | LoadMultiple(wback,(n,registers)) =>
4839     ("ldm",
4840      String.concat
4841        [s_reg n,if wback then "!" else "",", ",
4842         s_registers 16
4843           (BitsN.concat
4844              [BitsN.bits(8,8) registers,BitsN.B(0x0,7),
4845               BitsN.bits(7,0) registers])]);
4846
4847fun s_store ast =
4848  case ast of
4849     StoreWord(t,(n,immediate_form imm32)) =>
4850       ("str",s_imm_form(t,(n,imm32)))
4851   | StoreWord(t,(n,register_form m)) => ("str",s_reg_form(t,(n,m)))
4852   | StoreByte(t,(n,immediate_form imm32)) =>
4853     ("strb",s_imm_form(t,(n,imm32)))
4854   | StoreByte(t,(n,register_form m)) => ("strb",s_reg_form(t,(n,m)))
4855   | StoreHalf(t,(n,immediate_form imm32)) =>
4856     ("strh",s_imm_form(t,(n,imm32)))
4857   | StoreHalf(t,(n,register_form m)) => ("strh",s_reg_form(t,(n,m)))
4858   | Push registers =>
4859     ("push",
4860      s_registers 15
4861        (BitsN.concat
4862           [BitsN.bits(8,8) registers,BitsN.B(0x0,6),
4863            BitsN.bits(7,0) registers]))
4864   | StoreMultiple(n,registers) =>
4865     ("stm",String.concat[s_reg n,"!, ",s_registers 8 registers]);
4866
4867fun s_hint ast =
4868  case ast of
4869     Breakpoint imm32 => ("bkpt","#" ^ (s_hex 32 imm32))
4870   | DataMemoryBarrier option => ("dmb",s_barrier_option option)
4871   | DataSynchronizationBarrier option => ("dsb",s_barrier_option option)
4872   | InstructionSynchronizationBarrier option =>
4873     ("isb",s_barrier_option option)
4874   | SendEvent () => ("sev","")
4875   | WaitForEvent () => ("wfe","")
4876   | WaitForInterrupt () => ("wfi","")
4877   | Yield () => ("yield","");
4878
4879fun s_media ast =
4880  case ast of
4881     ExtendByte(unsigned,(d,m)) =>
4882       ((if unsigned then "u" else "s") ^ "xtb",s_reg2(d,m))
4883   | ExtendHalfword(unsigned,(d,m)) =>
4884     ((if unsigned then "u" else "s") ^ "xth",s_reg2(d,m))
4885   | ByteReverse(d,m) => ("rev",s_reg2(d,m))
4886   | ByteReversePackedHalfword(d,m) => ("rev16",s_reg2(d,m))
4887   | ByteReverseSignedHalfword(d,m) => ("revsh",s_reg2(d,m));
4888
4889fun s_system ast =
4890  case ast of
4891     ChangeProcessorState enable =>
4892       ("cps" ^ (if enable then "ie" else "id"),"i")
4893   | MoveToRegisterFromSpecial(SYSm,d) =>
4894     ("mrs",String.concat[s_reg d,", ",s_special_reg SYSm])
4895   | MoveToSpecialRegister(SYSm,n) =>
4896     ("msr",String.concat[s_special_reg SYSm,", ",s_reg n])
4897   | SupervisorCall imm32 => ("svc","#" ^ (s_hex 32 imm32));
4898
4899fun instructionToString (c,ast) =
4900  case ast of
4901     Branch b => s_branch(c,b)
4902   | Data d => s_data d
4903   | Load l => s_load l
4904   | Store s => s_store s
4905   | Media m => s_media m
4906   | System s => s_system s
4907   | Hint h => s_hint h
4908   | Multiply(Multiply32(d,(n,m))) => ("muls",s_reg3(d,(n,m)))
4909   | Undefined imm32 => ("udf","#" ^ (s_hex 32 imm32))
4910   | NoOperation () => ("nop","");
4911
4912end