-
Notifications
You must be signed in to change notification settings - Fork 1
/
check_pending_ptimers.v
164 lines (160 loc) · 7.47 KB
/
check_pending_ptimers.v
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
Require Import CodeDeps.
Require Import Ident.
Local Open Scope Z_scope.
Definition _cntp_ctl := 1%positive.
Definition _cntv_ctl := 2%positive.
Definition _emulated_timer_state := 3%positive.
Definition _g := 4%positive.
Definition _g_rec := 5%positive.
Definition _granule := 6%positive.
Definition _i := 7%positive.
Definition _lock := 8%positive.
Definition _rec := 9%positive.
Definition _rec__1 := 10%positive.
Definition _rec_rvic_state := 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 _t'7 := 19%positive.
Definition check_pending_ptimers_body :=
(Ssequence
(Ssequence
(Scall (Some _t'1)
(Evar _get_rec_g_rec (Tfunction
(Tcons (tptr Tvoid) Tnil)
(tptr Tvoid) cc_default))
((Etempvar _rec (tptr Tvoid)) :: nil))
(Sset _g_rec (Etempvar _t'1 (tptr Tvoid))))
(Ssequence
(Ssequence
(Scall (Some _t'2)
(Evar _sysreg_read (Tfunction (Tcons tuint Tnil) tulong cc_default))
((Econst_int (Int.repr 32) tuint) :: nil))
(Sset _cntp_ctl (Etempvar _t'2 tulong)))
(Ssequence
(Ssequence
(Scall (Some _t'6)
(Evar _get_rec_ptimer (Tfunction
(Tcons (tptr Tvoid) Tnil)
(tptr Tvoid)
cc_default))
((Etempvar _rec (tptr Tvoid)) :: nil))
(Scall (Some _t'7)
(Evar _check_timer_became_asserted (Tfunction
(Tcons
(tptr Tvoid)
(Tcons tulong Tnil)) tuint
cc_default))
((Etempvar _t'6 (tptr Tvoid)) ::
(Etempvar _cntp_ctl tulong) :: nil)))
(Sifthenelse (Ebinop Oeq (Etempvar _t'7 tuint)
(Econst_int (Int.repr 1) tuint) tint)
(Ssequence
(Scall None
(Evar _granule_lock (Tfunction
(Tcons (tptr Tvoid)
Tnil) tvoid cc_default))
((Etempvar _g_rec (tptr Tvoid)) :: nil))
(Ssequence
(Sset _cntp_ctl
(Ebinop Oor (Etempvar _cntp_ctl tulong)
(Econst_long (Int64.repr 2) tulong) tulong))
(Ssequence
(Scall None
(Evar _sysreg_write (Tfunction
(Tcons tuint (Tcons tulong Tnil)) tvoid
cc_default))
((Econst_int (Int.repr 32) tuint) ::
(Etempvar _cntp_ctl tulong) :: nil))
(Ssequence
(Ssequence
(Scall (Some _t'3)
(Evar _get_rec_sysregs (Tfunction
(Tcons
(tptr Tvoid)
(Tcons tuint Tnil)) tulong
cc_default))
((Etempvar _rec (tptr Tvoid)) ::
(Econst_int (Int.repr 69) tuint) :: nil))
(Scall None
(Evar _set_rec_sysregs (Tfunction
(Tcons
(tptr Tvoid)
(Tcons tuint
(Tcons tulong Tnil))) tvoid
cc_default))
((Etempvar _rec (tptr Tvoid)) ::
(Econst_int (Int.repr 69) tuint) ::
(Ebinop Oand (Etempvar _t'3 tulong)
(Econst_long (Int64.repr (18446744073709549567)) tulong) tulong) ::
nil)))
(Ssequence
(Ssequence
(Scall (Some _t'4)
(Evar _get_rec_sysregs (Tfunction
(Tcons
(tptr Tvoid)
(Tcons tuint Tnil)) tulong
cc_default))
((Etempvar _rec (tptr Tvoid)) ::
(Econst_int (Int.repr 69) tuint) :: nil))
(Scall None
(Evar _sysreg_write (Tfunction
(Tcons tuint (Tcons tulong Tnil))
tvoid cc_default))
((Econst_int (Int.repr 69) tuint) ::
(Etempvar _t'4 tulong) :: nil)))
(Ssequence
(Scall None
(Evar _set_rec_ptimer_asserted (Tfunction
(Tcons
(tptr Tvoid)
(Tcons tuint Tnil))
tvoid cc_default))
((Etempvar _rec (tptr Tvoid)) ::
(Econst_int (Int.repr 1) tuint) :: nil))
(Ssequence
(Ssequence
(Scall (Some _t'5)
(Evar _get_rec_rvic (Tfunction
(Tcons
(tptr Tvoid)
Tnil)
(tptr Tvoid)
cc_default))
((Etempvar _rec (tptr Tvoid)) ::
nil))
(Scall None
(Evar _rvic_set_pending (Tfunction
(Tcons
(tptr Tvoid)
(Tcons tulong Tnil))
tvoid cc_default))
((Etempvar _t'5 (tptr Tvoid)) ::
(Econst_long (Int64.repr 30) tulong) :: nil)))
(Scall None
(Evar _granule_unlock (Tfunction
(Tcons
(tptr Tvoid)
Tnil) tvoid cc_default))
((Etempvar _g_rec (tptr Tvoid)) ::
nil)))))))))
Sskip))))
.
Definition f_check_pending_ptimers := {|
fn_return := tvoid;
fn_callconv := cc_default;
fn_params := ((_rec, (tptr Tvoid)) :: nil);
fn_vars := nil;
fn_temps := ((_cntv_ctl, tulong) :: (_cntp_ctl, tulong) ::
(_g_rec, (tptr Tvoid)) :: (_t'7, tuint) ::
(_t'6, (tptr Tvoid)) ::
(_t'5, (tptr Tvoid)) ::
(_t'4, tulong) :: (_t'3, tulong) :: (_t'2, tulong) ::
(_t'1, (tptr Tvoid)) :: nil);
fn_body := check_pending_ptimers_body
|}.