-
Notifications
You must be signed in to change notification settings - Fork 2
/
Copy pathsmc_realm_destroy.v
155 lines (151 loc) · 6.89 KB
/
smc_realm_destroy.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
Require Import CodeDeps.
Require Import Ident.
Local Open Scope Z_scope.
Definition _addr := 1%positive.
Definition _g := 2%positive.
Definition _g_rd := 3%positive.
Definition _g_rec := 4%positive.
Definition _g_rec_list := 5%positive.
Definition _g_rtt := 6%positive.
Definition _granule := 7%positive.
Definition _i := 8%positive.
Definition _lock := 9%positive.
Definition _rd := 10%positive.
Definition _rd__1 := 11%positive.
Definition _rd_addr := 12%positive.
Definition _rec := 13%positive.
Definition _rec_list := 14%positive.
Definition _ret := 15%positive.
Definition _rt := 16%positive.
Definition _t'1 := 17%positive.
Definition _t'2 := 18%positive.
Definition _t'3 := 19%positive.
Definition _t'4 := 20%positive.
Definition _t'5 := 21%positive.
Definition _t'6 := 22%positive.
Definition smc_realm_destroy_body :=
(Ssequence
(Ssequence
(Scall (Some _t'1)
(Evar _find_lock_unused_granule (Tfunction
(Tcons tulong (Tcons tulong Tnil))
(tptr Tvoid)
cc_default))
((Etempvar _rd_addr tulong) :: (Econst_int (Int.repr 2) tuint) :: nil))
(Sset _g_rd (Etempvar _t'1 (tptr Tvoid))))
(Ssequence
(Ssequence
(Scall (Some _t'6)
(Evar _is_null (Tfunction (Tcons (tptr Tvoid) Tnil) tuint cc_default))
((Etempvar _g_rd (tptr Tvoid)) :: nil))
(Sifthenelse (Ebinop Oeq (Etempvar _t'6 tuint)
(Econst_int (Int.repr 0) tuint) tint)
(Ssequence
(Ssequence
(Scall (Some _t'2)
(Evar _granule_map (Tfunction
(Tcons (tptr Tvoid)
(Tcons tuint Tnil)) (tptr Tvoid)
cc_default))
((Etempvar _g_rd (tptr Tvoid)) ::
(Econst_int (Int.repr 2) tuint) :: nil))
(Sset _rd (Etempvar _t'2 (tptr Tvoid))))
(Ssequence
(Ssequence
(Scall (Some _t'3)
(Evar _get_rd_g_rtt (Tfunction
(Tcons (tptr Tvoid)
Tnil)
(tptr Tvoid)
cc_default))
((Etempvar _rd (tptr Tvoid)) :: nil))
(Sset _g_rtt (Etempvar _t'3 (tptr Tvoid))))
(Ssequence
(Ssequence
(Scall (Some _t'4)
(Evar _get_rd_g_rec_list (Tfunction
(Tcons
(tptr Tvoid)
Tnil)
(tptr Tvoid)
cc_default))
((Etempvar _rd (tptr Tvoid)) :: nil))
(Sset _g_rec_list
(Etempvar _t'4 (tptr Tvoid))))
(Ssequence
(Scall None
(Evar _buffer_unmap (Tfunction (Tcons (tptr Tvoid) Tnil)
tvoid cc_default))
((Etempvar _rd (tptr Tvoid)) :: nil))
(Ssequence
(Scall None
(Evar _granule_lock (Tfunction
(Tcons
(tptr Tvoid)
Tnil) tvoid cc_default))
((Etempvar _g_rtt (tptr Tvoid)) ::
nil))
(Ssequence
(Ssequence
(Scall (Some _t'5)
(Evar _get_g_rtt_refcount (Tfunction
(Tcons
(tptr Tvoid)
Tnil) tulong
cc_default))
((Etempvar _g_rtt (tptr Tvoid)) ::
nil))
(Sifthenelse (Ebinop One (Etempvar _t'5 tulong)
(Econst_long (Int64.repr 0) tulong)
tint)
(Ssequence
(Scall None
(Evar _granule_unlock (Tfunction
(Tcons
(tptr Tvoid)
Tnil) tvoid cc_default))
((Etempvar _g_rtt (tptr Tvoid)) ::
nil))
(Sset _ret (Econst_long (Int64.repr 1) tulong)))
(Ssequence
(Scall None
(Evar _realm_destroy_ops (Tfunction
(Tcons
(tptr Tvoid)
(Tcons
(tptr Tvoid)
(Tcons
(tptr Tvoid)
Tnil))) tvoid
cc_default))
((Etempvar _g_rtt (tptr Tvoid)) ::
(Etempvar _g_rec_list (tptr Tvoid)) ::
(Etempvar _g_rd (tptr Tvoid)) ::
nil))
(Sset _ret (Econst_long (Int64.repr 0) tulong)))))
(Scall None
(Evar _granule_unlock (Tfunction
(Tcons
(tptr Tvoid)
Tnil) tvoid cc_default))
((Etempvar _g_rd (tptr Tvoid)) ::
nil))))))))
(Sset _ret (Econst_long (Int64.repr 1) tulong))))
(Sreturn (Some (Etempvar _ret tulong)))))
.
Definition f_smc_realm_destroy := {|
fn_return := tulong;
fn_callconv := cc_default;
fn_params := ((_rd_addr, tulong) :: nil);
fn_vars := nil;
fn_temps := ((_g_rd, (tptr Tvoid)) ::
(_g_rtt, (tptr Tvoid)) ::
(_g_rec_list, (tptr Tvoid)) ::
(_rd, (tptr Tvoid)) :: (_ret, tulong) ::
(_t'6, tuint) :: (_t'5, tulong) ::
(_t'4, (tptr Tvoid)) ::
(_t'3, (tptr Tvoid)) ::
(_t'2, (tptr Tvoid)) ::
(_t'1, (tptr Tvoid)) :: nil);
fn_body := smc_realm_destroy_body
|}.