-
Notifications
You must be signed in to change notification settings - Fork 1
Expand file tree
/
Copy pathhandle_exception_sync.v
More file actions
219 lines (215 loc) · 10.8 KB
/
Copy pathhandle_exception_sync.v
File metadata and controls
219 lines (215 loc) · 10.8 KB
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
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
Require Import CodeDeps.
Require Import Ident.
Local Open Scope Z_scope.
Definition _ec := 1%positive.
Definition _esr := 2%positive.
Definition _exception := 3%positive.
Definition _g := 4%positive.
Definition _i := 5%positive.
Definition _info := 6%positive.
Definition _pc := 7%positive.
Definition _pc__1 := 8%positive.
Definition _rec := 9%positive.
Definition _rec__1 := 10%positive.
Definition _reg := 11%positive.
Definition _ret := 12%positive.
Definition _t'1 := 13%positive.
Definition _t'2 := 14%positive.
Definition _t'3 := 15%positive.
Definition _t'4 := 16%positive.
Definition _t'5 := 17%positive.
Definition _t'6 := 18%positive.
Definition handle_exception_sync_body :=
(Ssequence
(Ssequence
(Scall (Some _t'1)
(Evar _sysreg_read (Tfunction (Tcons tuint Tnil) tulong cc_default))
((Econst_int (Int.repr 82) tuint) :: nil))
(Sset _esr (Etempvar _t'1 tulong)))
(Ssequence
(Sset _ec
(Ebinop Oand (Etempvar _esr tulong)
(Econst_long (Int64.repr 4227858432) tulong) tulong))
(Sifthenelse (Ebinop Oeq (Etempvar _ec tulong)
(Econst_long (Int64.repr 67108864) tulong) tint)
(Ssequence
(Scall None
(Evar _set_rec_run_esr (Tfunction (Tcons tulong Tnil) tvoid
cc_default))
((Ebinop Oand (Etempvar _esr tulong)
(Ebinop Oor (Econst_long (Int64.repr 4227858432) tulong)
(Econst_long (Int64.repr 1) tulong) tulong) tulong) :: nil))
(Sreturn (Some (Econst_int (Int.repr 0) tuint))))
(Sifthenelse (Ebinop Oeq (Etempvar _ec tulong)
(Econst_long (Int64.repr 1476395008) tulong) tint)
(Ssequence
(Sset _i (Econst_int (Int.repr 0) tuint))
(Ssequence
(Sset _info
(Ebinop Oand (Etempvar _esr tulong)
(Ebinop Oor (Econst_long (Int64.repr 4227858432) tulong)
(Econst_long (Int64.repr 65535) tulong) tulong) tulong))
(Ssequence
(Scall None
(Evar _set_rec_last_run_info_esr (Tfunction
(Tcons
(tptr Tvoid)
(Tcons tulong Tnil))
tvoid cc_default))
((Etempvar _rec (tptr Tvoid)) ::
(Etempvar _info tulong) :: nil))
(Ssequence
(Scall None
(Evar _set_rec_run_esr (Tfunction (Tcons tulong Tnil) tvoid
cc_default))
((Etempvar _info tulong) :: nil))
(Ssequence
(Swhile
(Ebinop Olt (Etempvar _i tuint)
(Econst_long (Int64.repr 7) tulong) tint)
(Ssequence
(Ssequence
(Scall (Some _t'2)
(Evar _get_rec_regs (Tfunction
(Tcons
(tptr Tvoid)
(Tcons tuint Tnil)) tulong
cc_default))
((Etempvar _rec (tptr Tvoid)) ::
(Etempvar _i tuint) :: nil))
(Scall None
(Evar _set_rec_run_gprs (Tfunction
(Tcons tuint
(Tcons tulong Tnil))
tvoid cc_default))
((Etempvar _i tuint) :: (Etempvar _t'2 tulong) ::
nil)))
(Sset _i
(Ebinop Oadd (Etempvar _i tuint)
(Econst_int (Int.repr 1) tint) tuint))))
(Sreturn (Some (Econst_int (Int.repr 0) tuint))))))))
(Sifthenelse (Ebinop Oeq (Etempvar _ec tulong)
(Econst_long (Int64.repr 1543503872) tulong) tint)
(Ssequence
(Ssequence
(Scall (Some _t'3)
(Evar _sysreg_read (Tfunction (Tcons tuint Tnil) tulong
cc_default))
((Econst_int (Int.repr 81) tuint) :: nil))
(Sset _pc (Etempvar _t'3 tulong)))
(Ssequence
(Scall None
(Evar _sysreg_write (Tfunction
(Tcons tuint (Tcons tulong Tnil)) tvoid
cc_default))
((Econst_int (Int.repr 81) tuint) ::
(Ebinop Oadd (Etempvar _pc tulong)
(Econst_long (Int64.repr 4) tulong) tulong) :: nil))
(Ssequence
(Scall (Some _t'4)
(Evar _handle_realm_rsi (Tfunction
(Tcons
(tptr Tvoid)
Tnil) tuint cc_default))
((Etempvar _rec (tptr Tvoid)) :: nil))
(Sreturn (Some (Etempvar _t'4 tuint))))))
(Sifthenelse (Ebinop Oeq (Etempvar _ec tulong)
(Econst_long (Int64.repr 1610612736) tulong) tint)
(Ssequence
(Scall None
(Evar _handle_sysreg_access_trap (Tfunction
(Tcons
(tptr Tvoid)
(Tcons tulong Tnil))
tvoid cc_default))
((Etempvar _rec (tptr Tvoid)) ::
(Etempvar _esr tulong) :: nil))
(Ssequence
(Ssequence
(Scall (Some _t'5)
(Evar _sysreg_read (Tfunction (Tcons tuint Tnil) tulong
cc_default))
((Econst_int (Int.repr 81) tuint) :: nil))
(Sset _pc (Etempvar _t'5 tulong)))
(Ssequence
(Scall None
(Evar _sysreg_write (Tfunction
(Tcons tuint (Tcons tulong Tnil))
tvoid cc_default))
((Econst_int (Int.repr 81) tuint) ::
(Ebinop Oadd (Etempvar _pc tulong)
(Econst_long (Int64.repr 4) tulong) tulong) :: nil))
(Sreturn (Some (Econst_int (Int.repr 1) tuint))))))
(Sifthenelse (Ebinop Oeq (Etempvar _ec tulong)
(Econst_long (Int64.repr 2147483648) tulong) tint)
(Ssequence
(Scall (Some _t'6)
(Evar _handle_instruction_abort (Tfunction
(Tcons
(tptr Tvoid)
(Tcons tulong Tnil))
tuint cc_default))
((Etempvar _rec (tptr Tvoid)) ::
(Etempvar _esr tulong) :: nil))
(Sifthenelse (Ebinop Oeq (Etempvar _t'6 tuint)
(Econst_int (Int.repr 1) tuint) tint)
(Sreturn (Some (Econst_int (Int.repr 0) tuint)))
(Ssequence
(Scall None
(Evar _set_rec_run_esr (Tfunction (Tcons tulong Tnil)
tvoid cc_default))
((Econst_long (Int64.repr 0) tulong) :: nil))
(Ssequence
(Scall None
(Evar _set_rec_run_far (Tfunction (Tcons tulong Tnil)
tvoid cc_default))
((Econst_long (Int64.repr 0) tulong) :: nil))
(Ssequence
(Scall None
(Evar _set_rec_run_hpfar (Tfunction
(Tcons tulong Tnil)
tvoid cc_default))
((Econst_long (Int64.repr 0) tulong) :: nil))
(Sreturn (Some (Econst_int (Int.repr 0) tuint))))))))
(Sifthenelse (Ebinop Oeq (Etempvar _ec tulong)
(Econst_long (Int64.repr 2415919104) tulong)
tint)
(Ssequence
(Scall None
(Evar _handle_data_abort (Tfunction
(Tcons
(tptr Tvoid)
(Tcons tulong Tnil)) tvoid
cc_default))
((Etempvar _rec (tptr Tvoid)) ::
(Etempvar _esr tulong) :: nil))
(Sreturn (Some (Econst_int (Int.repr 0) tuint))))
(Ssequence
(Scall None
(Evar _set_rec_run_esr (Tfunction (Tcons tulong Tnil)
tvoid cc_default))
((Econst_long (Int64.repr 0) tulong) :: nil))
(Ssequence
(Scall None
(Evar _set_rec_run_far (Tfunction (Tcons tulong Tnil)
tvoid cc_default))
((Econst_long (Int64.repr 0) tulong) :: nil))
(Ssequence
(Scall None
(Evar _set_rec_run_hpfar (Tfunction
(Tcons tulong Tnil) tvoid
cc_default))
((Econst_long (Int64.repr 0) tulong) :: nil))
(Sreturn (Some (Econst_int (Int.repr 0) tuint))))))))))))))
.
Definition f_handle_exception_sync := {|
fn_return := tuint;
fn_callconv := cc_default;
fn_params := ((_rec, (tptr Tvoid)) :: nil);
fn_vars := nil;
fn_temps := ((_esr, tulong) :: (_ec, tulong) :: (_i, tuint) ::
(_info, tulong) :: (_pc, tulong) :: (_pc, tulong) ::
(_t'6, tuint) :: (_t'5, tulong) :: (_t'4, tuint) ::
(_t'3, tulong) :: (_t'2, tulong) :: (_t'1, tulong) :: nil);
fn_body := handle_exception_sync_body
|}.