1(* ------------------------------------------------------------------------ *)
2(*     ARM Machine Code Semantics (A and R profiles)                        *)
3(*     =============================================                        *)
4(*     Top-level: fetch and run instructions                                *)
5(* ------------------------------------------------------------------------ *)
6
7(* interactive use:
8  app load ["arm_decoderTheory", "arm_opsemTheory",
9            "pred_setLib", "wordsLib", "parmonadsyntax"];
10*)
11
12open HolKernel boolLib bossLib Parse pred_setLib;
13
14open arm_coretypesTheory arm_astTheory arm_seq_monadTheory
15     arm_decoderTheory arm_opsemTheory;
16
17val _ = new_theory "arm";
18
19(* ------------------------------------------------------------------------ *)
20
21val _ = numLib.prefer_num();
22val _ = wordsLib.prefer_word();
23
24val _ = temp_overload_on (parmonadsyntax.monad_bind, ``seqT``);
25val _ = temp_overload_on (parmonadsyntax.monad_par,  ``parT``);
26val _ = temp_overload_on ("return", ``constT``);
27
28val _ = temp_overload_on ("PAD0", ``list$PAD_LEFT #"0"``);
29
30(* ------------------------------------------------------------------------ *)
31
32(* Get the actual instruction set.  An alternative version could raise an error
33   if iset is Thumb, Jazelle or ThumbEE when these aren't avaialble. *)
34
35val actual_instr_set_def = Define`
36  actual_instr_set ii : InstrSet M =
37    read_arch ii >>=
38    (\arch.
39      if arch = ARMv4 then
40        constT InstrSet_ARM
41      else
42        current_instr_set ii >>=
43        (\iset.
44          if iset = InstrSet_Jazelle then
45            have_jazelle ii >>=
46            (\HaveJazelle.
47              constT (if HaveJazelle then iset else InstrSet_ARM))
48          else if iset = InstrSet_ThumbEE then
49            have_thumbEE ii >>=
50            (\HaveThumbEE.
51              constT (if HaveThumbEE then iset else InstrSet_Thumb))
52          else
53            constT iset))`;
54
55val fetch_arm_def = Define`
56  fetch_arm ii read_word : (string # Encoding # word4 # ARMinstruction) M =
57    (read_pc ii ||| arch_version ii) >>=
58    (\(pc,v).
59       read_word pc >>=
60       (\ireg.
61          constT (PAD0 8 (word_to_hex_string ireg),
62                  Encoding_ARM, arm_decode (v < 5) ireg)))`;
63
64val fetch_thumb_def = Define`
65  fetch_thumb ii ee read_halfword
66    : (string # Encoding # word4 # ARMinstruction) M =
67    (read_pc ii ||| read_cpsr ii ||| read_arch ii) >>=
68    (\(pc,cpsr,arch).
69      read_halfword pc >>= (\ireg1.
70        if ((15 -- 13) ireg1 = 0b111w) /\ (12 -- 11) ireg1 <> 0b00w then
71          read_halfword (pc + 2w) >>= (\ireg2.
72            constT (PAD0 4 (word_to_hex_string ireg1) ++ " " ++
73                    PAD0 4 (word_to_hex_string ireg2),
74                    Encoding_Thumb2, thumb2_decode arch cpsr.IT (ireg1,ireg2)))
75        else
76          constT
77            (PAD0 4 (word_to_hex_string ireg1),
78             if ee then
79               thumbee_decode arch cpsr.IT ireg1
80             else
81               (Encoding_Thumb, thumb_decode arch cpsr.IT ireg1))))`;
82
83val fetch_instruction_def = Define`
84  fetch_instruction ii
85    read_word read_halfword : (string # Encoding # word4 # ARMinstruction) M =
86    actual_instr_set ii >>=
87    (\iset.
88       case iset
89       of InstrSet_ARM     => fetch_arm ii read_word
90        | InstrSet_Thumb   => fetch_thumb ii F read_halfword
91        | InstrSet_ThumbEE => fetch_thumb ii T read_halfword
92        | InstrSet_Jazelle =>
93            errorT ("fetch_instruction: Jazelle not supported"))`;
94
95val arm_next_def = Define`
96  arm_next ii irpt : unit M =
97    if irpt = NoInterrupt then
98      waiting_for_interrupt ii >>=
99      (\wfi.
100         condT (~wfi)
101           (fetch_instruction ii
102               (\a. read_memA ii (a, 4) >>= (\d. return (word32 d)))
103               (\a. read_memA ii (a, 2) >>= (\d. return (word16 d))) >>=
104            (\(opc,instr). arm_instr ii instr)))
105    else
106      (if irpt = HW_Reset then
107          take_reset ii
108        else if irpt = HW_Fiq then
109          take_fiq_exception ii
110        else (* irpt = HW_Irq *)
111          take_irq_exception ii) >>=
112      (\u:unit. clear_wait_for_interrupt ii)`;
113
114val arm_run_def = Define`
115  arm_run t ii inp =
116    (forT 0 t
117      (\t.
118         let irpt = inp t in
119           if (irpt = NoInterrupt) \/ (irpt = HW_Reset) then
120             arm_next ii irpt
121           else
122             read_cpsr ii >>=
123             (\cpsr.
124                arm_next ii NoInterrupt >>=
125                (\u:unit.
126                  condT ((irpt = HW_Fiq) /\ ~cpsr.F \/
127                         (irpt = HW_Irq) /\ ~cpsr.I)
128                        (arm_next ii irpt))))) >>=
129    (\unit_list:unit list. constT ())`;
130
131(* ------------------------------------------------------------------------ *)
132
133val _ = export_theory ();
134