1(* ------------------------------------------------------------------------ *)
2(*     ARM Machine Code Semantics                                           *)
3(*     ==========================                                           *)
4(*     Use EmitML to generate an SML version of the ARM model               *)
5(* ------------------------------------------------------------------------ *)
6
7(* interactive use:
8  app load ["arm_evalTheory", "wordsLib", "pred_setSyntax", "emitLib",
9            "EmitTeX", "extended_emitTheory"];
10*)
11
12open HolKernel boolLib bossLib Parse wordsLib;
13
14open arm_coretypesTheory arm_astTheory arm_seq_monadTheory
15     arm_decoderTheory arm_opsemTheory armTheory arm_evalTheory;
16
17open EmitML extended_emitTheory;
18
19val _ = new_theory "arm_emit";
20
21(* ------------------------------------------------------------------------ *)
22
23val bytes = Q.prove(
24  `!w n.
25     bytes (w,n) =
26       if n = 1 then
27         [w2w w]
28       else if n = 2 then
29         [(7 >< 0) w; (15 >< 8) w]
30       else if n = 4 then
31         [(7 >< 0) w; (15 >< 8) w; (23 >< 16) w; (31 >< 24) w]
32       else
33         FAIL bytes ^(mk_var("n not 1, 2 or 4",bool)) (w,n)`,
34  SRW_TAC [] [bytes_def, combinTheory.FAIL_THM]);
35
36val SUM = Q.prove(
37  `!n f. SUM n f = if n = 0 then 0 else SUM (n - 1) f + f (n - 1)`,
38  Cases THEN SRW_TAC [] [sum_numTheory.SUM_def]);
39
40val LESS_THM =
41  CONV_RULE numLib.SUC_TO_NUMERAL_DEFN_CONV prim_recTheory.LESS_THM;
42
43val parallel_add_sub_op1 = Q.prove(
44  `!w. parallel_add_sub_op1 w =
45         case w
46         of 0b01w => Parallel_normal
47          | 0b10w => Parallel_saturating
48          | 0b11w => Parallel_halving
49          | _ => FAIL parallel_add_sub_op1 ^(mk_var("can't decode",bool)) w`,
50  Cases THEN FULL_SIMP_TAC (srw_ss())
51    [parallel_add_sub_op1_def, LESS_THM, combinTheory.FAIL_THM]);
52
53val parallel_add_sub_op2 = Q.prove(
54  `!w. parallel_add_sub_op2 w =
55         case w
56         of 0b000w => Parallel_add_16
57          | 0b001w => Parallel_add_sub_exchange
58          | 0b010w => Parallel_sub_add_exchange
59          | 0b011w => Parallel_sub_16
60          | 0b100w => Parallel_add_8
61          | 0b111w => Parallel_sub_8
62          | _ => FAIL parallel_add_sub_op2 ^(mk_var("can't decode",bool)) w`,
63  Cases THEN FULL_SIMP_TAC (srw_ss())
64    [parallel_add_sub_op2_def, LESS_THM, combinTheory.FAIL_THM]);
65
66val parallel_add_sub_thumb_op2 = Q.prove(
67  `!w. parallel_add_sub_thumb_op2 w =
68         case w
69         of 0b001w => Parallel_add_16
70          | 0b010w => Parallel_add_sub_exchange
71          | 0b110w => Parallel_sub_add_exchange
72          | 0b101w => Parallel_sub_16
73          | 0b000w => Parallel_add_8
74          | 0b100w => Parallel_sub_8
75          | _ => FAIL parallel_add_sub_thumb_op2
76                   ^(mk_var("can't decode",bool)) w`,
77  Cases THEN FULL_SIMP_TAC (srw_ss())
78    [parallel_add_sub_thumb_op2_def, LESS_THM, combinTheory.FAIL_THM]);
79
80(* Expand out data_processing_instr wrt ``n2w opc`` *)
81local
82  val dp_thm = ONCE_REWRITE_RULE [LET_THM]
83                 (fetch "arm_opsem" "data_processing_instr")
84  fun mk_dp_opc (i,tm) =
85        let val opc = wordsSyntax.mk_wordii(i, 4) in
86          boolSyntax.mk_cond
87            (boolSyntax.mk_eq (``opc:word4``,opc),
88            ``arm_opsem$data_processing_instr ii enc
89                (Data_Processing ^opc setflags n d mode1)``,tm)
90        end
91  val tm = List.foldr mk_dp_opc ``ARB:unit M`` (List.tabulate(16,I))
92  val thm = Q.prove(
93              `data_processing_instr ii enc
94                 (Data_Processing opc setflags n d mode1) = ^tm`,
95              SRW_TAC [] [] THEN Cases_on `opc`
96                THEN FULL_SIMP_TAC (srw_ss()) [LESS_THM]
97                THEN FULL_SIMP_TAC std_ss [])
98  val pos = Lib.index (Lib.equal "data_processing_instr")
99              arm_opsemTheory.instruction_list
100  val data_processing_instr =
101        CONV_RULE (RHS_CONV
102           (SIMP_CONV (srw_ss()) [dp_thm, data_processing_alu_def]
103              THENC DEPTH_CONV (pairLib.LET_SIMP_CONV false))) thm
104  val l = map (fetch "arm_opsem") arm_opsemTheory.instruction_list
105in
106  val instruction_list =
107        let val (l,r) = Lib.split_after pos l in
108          l @ [data_processing_instr] @ (tl r)
109        end
110end;
111
112val i2bits_itself_def = Define`
113  i2bits_itself (i,N,(:'a)) = (i2bits (i,N)) : 'a word`;
114
115val signed_sat_itself_def = Define`
116  signed_sat_itself (i,N,(:'a)) = (signed_sat (i,N)) : 'a word`;
117
118val unsigned_sat_itself_def = Define`
119  unsigned_sat_itself (i,N,(:'a)) = (unsigned_sat (i,N)) : 'a word`;
120
121val signed_sat_q_itself_def = Define`
122  signed_sat_q_itself (i,N,(:'a)) = (signed_sat_q (i,N)) : 'a word # bool`;
123
124val unsigned_sat_q_itself_def = Define`
125  unsigned_sat_q_itself (i,N,(:'a)) = (unsigned_sat_q (i,N)) : 'a word # bool`;
126
127val _ = type_pp.pp_num_types := false;
128val _ = type_pp.pp_array_types := false;
129val _ = temp_disable_tyabbrev_printing "proc";
130val _ = temp_disable_tyabbrev_printing "FullAddress";
131val _ = temp_disable_tyabbrev_printing "cpid";
132val _ = temp_type_abbrev("ARMextensions_set", ``:ARMextensions set``);
133val _ = temp_type_abbrev("word4", ``:bool[4]``);
134val _ = temp_type_abbrev("word32", ``:bool[32]``);
135val _ = temp_clear_overloads_on "UInt"
136val _ = temp_clear_overloads_on "SInt"
137val _ = temp_overload_on("w2i", ``integer_word$w2i``);
138
139fun f x = [QUOTE (trace ("Unicode",0) EmitTeX.datatype_thm_to_string x)]
140
141val n2w_rule = Q.SPEC `n2w m`
142
143val extension_rule = SIMP_RULE (srw_ss()) [thumb2_support_def];
144
145val int_rule = SIMP_RULE std_ss (COND_RATOR :: map GSYM
146  [basis_emitTheory.i2w_itself_def,
147   i2bits_itself_def, signed_sat_itself_def, unsigned_sat_itself_def,
148   signed_sat_q_itself_def, unsigned_sat_q_itself_def]);
149
150val cons_rule = ONCE_REWRITE_RULE [GSYM (ETA_CONV ``\l. CONS f l``)];
151
152fun mk_word n =
153let val s = Int.toString n in
154  MLSIG ("type word" ^ s ^ " = wordsML.word" ^ s)
155end;
156
157val _ = emitML (!Globals.emitMLDir) ("arm",
158  [OPEN  ["num", "set", "string", "fcp", "bit", "words"],
159   MLSIG "type num = numML.num",
160   MLSIG "type int = intML.int",
161   MLSIG "type 'a ptree = 'a patriciaML.ptree",
162   MLSIG "type 'a set = 'a setML.set",
163   MLSIG "type 'a itself = 'a fcpML.itself",
164   MLSIG "type 'a bit0 = 'a fcpML.bit0",
165   MLSIG "type 'a bit1 = 'a fcpML.bit1",
166   MLSIG "type 'a word = 'a wordsML.word",
167   MLSIG "type ('a,'b) cart = ('a,'b) fcpML.cart",
168   MLSIG "type ('a,'b) sum = ('a,'b) sumML.sum",
169   MLSTRUCT "type int = intML.int",
170   MLSTRUCT "type 'a ptree = 'a patriciaML.ptree"] @
171  map mk_word [2,3,4,5,6,8,12,16,24,32,64] @
172  [DATATYPE (f datatype_ARMextensions),
173   MLSIG    "type ARMextensions_set = ARMextensions set",
174   MLSTRUCT "type ARMextensions_set = ARMextensions set"] @
175  map (DATATYPE o f)
176    [datatype_iiid, datatype_RName, datatype_PSRName, datatype_ARMpsr,
177     datatype_CP14reg, datatype_CP15sctlr, datatype_CP15scr,
178     datatype_CP15nsacr, datatype_CP15reg,
179     datatype_coproc_state, datatype_memory_access, datatype_ARMarch,
180     datatype_ARMinfo, datatype_SRType, datatype_InstrSet, datatype_Encoding,
181     datatype_MemType, datatype_MemoryAttributes, datatype_AddressDescriptor,
182     datatype_MBReqDomain, datatype_MBReqTypes, datatype_addressing_mode1,
183     datatype_addressing_mode2, datatype_addressing_mode3, datatype_hint,
184     datatype_parallel_add_sub_op1, datatype_parallel_add_sub_op2,
185     datatype_branch_instruction, datatype_data_processing_instruction,
186     datatype_status_access_instruction, datatype_load_store_instruction,
187     datatype_miscellaneous_instruction, datatype_coprocessor_instruction,
188     datatype_ARMinstruction] @
189  [MLSIG    "type CPinstruction = word4 * (word4 * coprocessor_instruction)",
190   MLSTRUCT "type CPinstruction = word4 * (word4 * coprocessor_instruction)",
191   MLSIG    "type exclusive_triple = word32 * (iiid * num)",
192   MLSTRUCT "type exclusive_triple = word32 * (iiid * num)",
193   MLSIG    "type exclusive_state = (num -> word32 set) * (word32 * num) set",
194   MLSTRUCT "type exclusive_state = (num -> word32 set) * (word32 * num) set",
195   MLSIG    "type 'a ExclusiveM = exclusive_state -> ('a * exclusive_state)",
196   MLSTRUCT "type 'a ExclusiveM = exclusive_state -> ('a * exclusive_state)",
197   MLSIG    "type 'a CoprocessorM = coproc_state -> ('a * coproc_state)",
198   MLSTRUCT "type 'a CoprocessorM = coproc_state -> ('a * coproc_state)"] @
199  map (DATATYPE o f)
200    [datatype_ExclusiveMonitors, datatype_Coprocessors,
201     datatype_arm_state, datatype_error_option] @
202  [MLSIG    "type 'a M = arm_state -> ('a, arm_state) error_option",
203   MLSTRUCT "type 'a M = arm_state -> ('a, arm_state) error_option"] @
204  map (DEFN o SIMP_RULE (srw_ss())
205         [Q.ISPEC `FST` COND_RAND, combinTheory.o_THM,
206          i2bits_def, signed_sat_def, unsigned_sat_def,
207          signed_sat_q_def, unsigned_sat_q_def])
208    [INST_TYPE [alpha |-> ``:8``] integer_wordTheory.i2w_def, i2bits_itself_def,
209     signed_sat_itself_def, unsigned_sat_itself_def,
210     signed_sat_q_itself_def, unsigned_sat_q_itself_def] @
211  [DEFN data_processing_thumb2_unpredictable_def] @
212  map (DEFN o int_rule)
213   ([IMP_DISJ_THM,
214     (* arm_coretypes *)
215     n2w_rule align_def, aligned_def,
216     n2w_rule count_leading_zeroes_def,
217     n2w_rule lowest_set_bit_compute, SUM, wordsTheory.bit_count_upto_def,
218     n2w_rule wordsTheory.bit_count_def, zero_extend32_def,
219     sign_extend32_def, word16_def, word32_def, word64_def,
220     bytes, n2w_rule LSL_C_def, LSR_C_def, n2w_rule ASR_C_def,
221     n2w_rule ROR_C_def, RRX_C_def, LSL_def, LSR_def, ASR_def, ROR_def,
222     RRX_def, ITAdvance_def, decode_psr_def, encode_psr_def, version_number_def,
223
224     (* arm_ast *)
225     is_mode1_immediate_def, is_mode2_immediate_def, is_mode3_immediate_def,
226
227     (* arm_seq_monad *)
228     constE_def, seqE_def, constC_def, seqC_def, constT_def,
229     errorT_def, seqT_def, parT_def, lockT_def, condT_def,
230     forT_def, readT_def, writeT_def, read_info_def,
231     read_arch_def, read_extensions_def, read__reg_def,
232     write__reg_def, read__psr_def, write__psr_def,
233     read_scr_def, write_scr_def, read_nsacr_def,
234     read_teehbr_def, read_sctlr_def, read_cpsr_def, write_cpsr_def,
235     read_isetstate_def, write_isetstate_def,
236     have_security_ext, have_jazelle, have_thumbEE, bad_mode_def, read_spsr_def,
237     write_spsr_def, current_mode_is_priviledged_def,
238     current_mode_is_user_or_system_def, is_secure_def,
239     read_vbar_def, read_mvbar_def, current_instr_set_def,
240     select_instr_set_def, RBankSelect_def, RfiqBankSelect_def,
241     LookUpRName_def, read_reg_mode_def, write_reg_mode_def,
242     read_pc_def, pc_store_value_def, read_reg_def,
243     write_reg_def, branch_to_def, increment_pc_def,
244     big_endian_def, translate_address_def, read_monitor_def,
245     write_monitor_def, cons_rule read_mem1_def, cons_rule write_mem1_def,
246     read_mem_def, write_mem_def, read_memA_with_priv_def,
247     write_memA_with_priv_def, read_memU_with_priv_def,
248     write_memU_with_priv_def, read_memA_def,
249     write_memA_def, read_memA_unpriv_def, write_memA_unpriv_def,
250     read_memU_def, write_memU_def, read_memU_unpriv_def,
251     write_memU_unpriv_def, data_memory_barrier_def,
252     data_synchronization_barrier_def,
253     instruction_synchronization_barrier_def,
254     hint_preload_data_for_write_def, hint_preload_data_def,
255     hint_preload_instr_def, hint_yield_def, hint_debug_def,
256     clear_event_register_def, event_registered_def,
257     send_event_def, wait_for_event_def, wait_for_interrupt_def,
258     clear_wait_for_interrupt_def, waiting_for_interrupt_def,
259     set_exclusive_monitors_def, exclusive_monitors_pass_def,
260     clear_exclusive_local_def, read_coprocessors_def,
261     write_coprocessors_def, coproc_accepted_def,
262     coproc_internal_operation_def, coproc_send_loaded_words_def,
263     coproc_get_words_to_store_def, coproc_send_one_word_def,
264     coproc_get_one_word_def, coproc_send_two_words_def,
265     coproc_get_two_words_def,
266
267     (* arm_opsem *)
268     unaligned_support_def, arch_version_def, read_reg_literal_def,
269     read_flags_def, write_flags_def, read_cflag_def, set_q_def, read_ge_def,
270     write_ge_def, write_e_def, extension_rule IT_advance_def,
271     cpsr_write_by_instr_def, spsr_write_by_instr_def,
272     branch_write_pc_def, bx_write_pc_def, load_write_pc_def,
273     alu_write_pc_def, decode_imm_shift_def, decode_reg_shift_def,
274     shift_c_def, shift_def, arm_expand_imm_c_def, thumb_expand_imm_c_def,
275     arm_expand_imm_def,
276     address_mode1_def, address_mode2_def, address_mode3_def,
277     address_mode5_def,
278     signed_parallel_add_sub_16_def, signed_normal_add_sub_16_def,
279     signed_saturating_add_sub_16_def, signed_halving_add_sub_16_def,
280     signed_parallel_add_sub_8_def, signed_normal_add_sub_8_def,
281     signed_saturating_add_sub_8_def, signed_halving_add_sub_8_def,
282     unsigned_parallel_add_sub_16_def, unsigned_normal_add_sub_16_def,
283     unsigned_saturating_add_sub_16_def, unsigned_halving_add_sub_16_def,
284     unsigned_parallel_add_sub_8_def, unsigned_normal_add_sub_8_def,
285     unsigned_saturating_add_sub_8_def, unsigned_halving_add_sub_8_def,
286     parallel_add_sub_def, barrier_option_def, exc_vector_base_def,
287     take_undef_instr_exception_def, take_svc_exception_def,
288     take_smc_exception_def, take_prefetch_abort_exception_def,
289     integer_zero_divide_trapping_enabled_def, null_check_if_thumbEE_def] @
290    instruction_list @
291    [condition_passed_def, branch_instruction_def,
292     data_processing_instruction_def, status_access_instruction_def,
293     load_store_instruction_def, miscellaneous_instruction_def,
294     coprocessor_instruction_def, arm_instr_def,
295
296     (* arm_decode and arm_eval *)
297     hint_decode_def, parallel_add_sub_op1, parallel_add_sub_op2,
298     parallel_add_sub_thumb_op2, parallel_add_sub_decode_def,
299     parallel_add_sub_thumb_decode_def, InITBlock_def, LastInITBlock_def,
300     arm_decode_def, extension_rule thumb_decode_def, thumbee_decode_def,
301     thumb2_decode_aux1_def, thumb2_decode_aux2_def, thumb2_decode_aux3_def,
302     thumb2_decode_aux4_def, thumb2_decode_aux5_def, thumb2_decode_aux6_def,
303     thumb2_decode_aux7_def, thumb2_decode_aux8_def, thumb2_decode_aux9_def,
304     extension_rule thumb2_decode_def, proc_def, ptree_read_word_def,
305     ptree_read_halfword_def, fetch_arm_def, fetch_thumb_def, attempt_def,
306     actual_instr_set_def, fetch_instruction_def]));
307
308(* ------------------------------------------------------------------------ *)
309
310val _ = export_theory ();
311