-
Notifications
You must be signed in to change notification settings - Fork 81
/
backend_arm8_cvScript.sml
151 lines (127 loc) · 5.16 KB
/
backend_arm8_cvScript.sml
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
(*
Translate cv version of arm8 specialised backend functions.
*)
open preamble cv_transLib cv_stdTheory;
open backend_arm8Theory arm8Theory arm8_targetTheory;
val _ = new_theory "backend_arm8_cv";
(*---------------------------------------------------------------------------*
Translation of instruction encoder
*---------------------------------------------------------------------------*)
Theorem IN_INSERT[cv_inline,local] = IN_INSERT;
Theorem NOT_IN_EMPTY[cv_inline,local] = NOT_IN_EMPTY;
Theorem word_len[cv_inline,local] = word_len_def;
Theorem v2w_sing[cv_inline,local] = miscTheory.v2w_sing;
val _ = cv_trans e_LoadStoreImmediate_def;
val _ = cv_trans ExtendType2num_thm;
val _ = cv_trans e_LoadStoreRegister_def;
val res = cv_trans_pre $ SRULE [word_len_def] e_load_store_def;
Theorem e_load_store_pre[cv_pre]:
∀i. e_load_store_pre i
Proof
simp[res] >> simp[IS_SOME_EXISTS, PULL_EXISTS]
QED
val _ = cv_trans e_branch_def;
val _ = cv_trans e_crc_def;
val _ = cv_trans e_debug_def;
val _ = cv_trans e_system_def;
Theorem e_sf_word32_F[cv_inline,local] =
e_sf_def |> INST_TYPE [``:'N`` |-> ``:32``] |>
SRULE [word_len_def, v2w_sing]
Theorem e_sf_word64_T[cv_inline,local] =
e_sf_def |> INST_TYPE [``:'N`` |-> ``:64``] |>
SRULE [word_len_def, v2w_sing]
val _ = cv_trans ShiftType2num_thm;
val highest_set_bit_pre =
cv_trans_pre (HighestSetBit_def |> INST_TYPE [``:'N`` |-> ``:7``]);
Theorem HighestSetBit_pre[cv_pre,local]:
∀w. HighestSetBit_pre w
Proof
simp[highest_set_bit_pre]
QED
Theorem cv_inline_v2w_Ones[cv_inline,local] = v2w_Ones;
val _ = cv_trans (bitstringTheory.replicate_def |> SRULE [GSYM REPLICATE_GENLIST]);
val _ = cv_trans (Ones_def |> SRULE [PAD_LEFT, GSYM REPLICATE_GENLIST]);
val _ = cv_trans cv_primTheory.v2n_custom_def;
val _ = cv_trans (INST_TYPE [``:'N`` |-> ``:32``] Replicate_def);
val _ = cv_trans (INST_TYPE [``:'N`` |-> ``:64``] Replicate_def);
val _ = cv_auto_trans (INST_TYPE [``:'M`` |-> ``:32``] DecodeBitMasks_def);
val _ = cv_auto_trans (INST_TYPE [``:'M`` |-> ``:64``] DecodeBitMasks_def);
Definition CountTrailing_T_def:
CountTrailing_T w =
if w = 0w then 0n
else if word_bit 0 w then 0
else 1 + CountTrailing_T (w >>> 1)
End
Definition CountTrailing_F_def:
CountTrailing_F w =
if ¬word_bit 0 w then 0n
else 1 + CountTrailing_F (w >>> 1)
Termination
WF_REL_TAC `measure w2n` >> rw[] >>
Cases_on `w` >> gvs[w2n_lsr] >>
simp[DIV_LT_X] >> Cases_on `n` >> gvs[]
End
val count_trailing_tac =
(WF_REL_TAC `measure cv_sum_depth` >> cv_termination_tac >>
gvs[GSYM cv_primTheory.cv_rep_exp] >>
Cases_on `cv_w` >> gvs[] >>
rw[DIV_LT_X] >> Cases_on `m` >> gvs[])
val _ = cv_trans_rec (INST_TYPE [alpha |-> ``:32``] CountTrailing_T_def)
count_trailing_tac;
val _ = cv_trans_rec (INST_TYPE [alpha |-> ``:64``] CountTrailing_T_def)
count_trailing_tac;
val _ = cv_trans_rec (INST_TYPE [alpha |-> ``:32``] CountTrailing_F_def)
count_trailing_tac;
val _ = cv_trans_rec (INST_TYPE [alpha |-> ``:64``] CountTrailing_F_def)
count_trailing_tac;
Theorem cv_inline_CountTrailing_T[cv_inline,local]:
∀w. CountTrailing (T,w) = CountTrailing_T w
Proof
recInduct CountTrailing_T_ind >> rw[] >>
once_rewrite_tac[CountTrailing_def, CountTrailing_T_def] >>
rw[] >> gvs[]
QED
Theorem cv_inline_CountTrailing_F[cv_inline,local]:
∀w. CountTrailing (F,w) = if w = -1w then 0 else CountTrailing_F w
Proof
rw[] >- simp[Once CountTrailing_def] >>
pop_assum mp_tac >> qid_spec_tac `w` >>
recInduct CountTrailing_F_ind >> rw[] >>
once_rewrite_tac[CountTrailing_def, CountTrailing_F_def] >>
rw[] >> gvs[] >> first_x_assum irule >>
Cases_on `w` >> gvs[GSYM n2w_DIV] >> simp[word_eq_n2w] >>
gvs[bitTheory.MOD_2EXP_MAX_def, bitTheory.MOD_2EXP_def, dimword_def] >>
simp[DIV_MOD_MOD_DIV] >>
qsuff_tac `n DIV 2 < 2 ** dimindex (:'a) - 1` >> gvs[] >> simp[DIV_LT_X] >>
pop_assum mp_tac >> rpt $ pop_assum kall_tac >>
`dimindex (:'a) ≠ 0` by gvs[] >>
rename1 `x ≠ 0` >> Induct_on `x` >> rw[] >> gvs[EXP] >>
Cases_on `x` >> gvs[]
QED
val _ = cv_trans EncodeLogicalOp_def;
val _ = cv_trans (INST_TYPE [``:'N`` |-> ``:32``] EncodeBitMaskAux_def);
val _ = cv_trans (INST_TYPE [``:'N`` |-> ``:32``] EncodeBitMask_def);
val _ = cv_trans (INST_TYPE [``:'N`` |-> ``:64``] EncodeBitMaskAux_def);
val _ = cv_trans (INST_TYPE [``:'N`` |-> ``:64``] EncodeBitMask_def);
val _ = cv_trans RevOp2num_thm;
val _ = cv_trans e_data_def;
val _ = cv_trans SystemHintOp2num_thm;
val _ = cv_trans MemBarrierOp2num_thm;
val _ = cv_trans arm8Theory.Encode_def;
val _ = cv_trans arm8_encode_def;
val _ = cv_trans NoOperation_def;
val _ = cv_trans arm8_enc_mov_imm_def;
val _ = cv_trans arm8_encode_fail_def;
val _ = cv_trans arm8_load_store_ast_def;
val _ = cv_trans cmp_cond_def;
val _ = cv_trans asmSemTheory.is_test_def;
val bop_enc_pre = cv_trans_pre bop_enc_def;
val arm8_ast_pre = cv_trans_pre (SRULE [SF LET_ss] arm8_ast_def);
Theorem arm8_ast_pre[cv_pre]:
∀v. arm8_ast_pre v
Proof
simp[arm8_ast_pre, bop_enc_pre]
QED
val _ = cv_auto_trans (arm8_targetTheory.arm8_enc_def |>
SRULE [combinTheory.o_DEF, LIST_BIND_def, FUN_EQ_THM]);
val _ = export_theory();