-
Notifications
You must be signed in to change notification settings - Fork 2
/
Copy pathtable_destroy_aux.v
162 lines (158 loc) · 9.53 KB
/
table_destroy_aux.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
Require Import SpecDeps.
Require Import RData.
Require Import EventReplay.
Require Import MoverTypes.
Require Import Constants.
Require Import CommonLib.
Require Import AbsAccessor.Spec.
Require Import TableAux2.Spec.
Require Import TableAux.Spec.
Local Open Scope Z_scope.
Section SpecLow.
Definition table_destroy_aux_spec0 (g_llt: Pointer) (g_tbl: Pointer) (ll_table: Pointer) (level: Z64) (index: Z64) (map_addr: Z64) (adt: RData) : option (RData * Z64) :=
match g_llt, g_tbl, ll_table, level, index, map_addr with
| (_g_llt_base, _g_llt_ofst), (_g_tbl_base, _g_tbl_ofst), (_ll_table_base, _ll_table_ofst), VZ64 _level, VZ64 _index, VZ64 _map_addr =>
let _ret := 0 in
when'' _table_base, _table_ofst, adt == granule_map_spec (_g_tbl_base, _g_tbl_ofst) 7 adt;
rely is_int _table_ofst;
when' _gcnt, adt == get_g_rtt_refcount_spec (_g_tbl_base, _g_tbl_ofst) adt;
rely is_int64 _gcnt;
if (_gcnt =? 1) then
let _t'6 := 1 in
if (_gcnt =? 1) then
when' _new_pgte, adt == table_delete_spec (_table_base, _table_ofst) (_g_llt_base, _g_llt_ofst) adt;
rely is_int64 _new_pgte;
rely is_int64 _index;
when adt == pgte_write_spec (_ll_table_base, _ll_table_ofst) (VZ64 _index) (VZ64 0) adt;
rely is_int64 (Z.land _new_pgte 504403158265495552);
rely is_int64 ((Z.land _new_pgte 504403158265495552) / 72057594037927936);
if (((Z.land _new_pgte 504403158265495552) / 72057594037927936) =? 2) then
rely is_int64 _map_addr;
when adt == invalidate_pages_in_block_spec (VZ64 _map_addr) adt;
when adt == pgte_write_spec (_ll_table_base, _ll_table_ofst) (VZ64 _index) (VZ64 _new_pgte) adt;
when adt == granule_put_spec (_g_tbl_base, _g_tbl_ofst) adt;
when'' _t'5_base, _t'5_ofst == null_ptr_spec adt;
rely is_int _t'5_ofst;
when adt == set_g_rtt_rd_spec (_g_tbl_base, _g_tbl_ofst) (_t'5_base, _t'5_ofst) adt;
when adt == granule_memzero_mapped_spec (_table_base, _table_ofst) adt;
when adt == granule_set_state_spec (_g_tbl_base, _g_tbl_ofst) 1 adt;
when adt == buffer_unmap_spec (_table_base, _table_ofst) adt;
Some (adt, (VZ64 _ret))
else
rely is_int64 _map_addr;
when adt == invalidate_block_spec (VZ64 _map_addr) adt;
when adt == pgte_write_spec (_ll_table_base, _ll_table_ofst) (VZ64 _index) (VZ64 _new_pgte) adt;
when adt == granule_put_spec (_g_tbl_base, _g_tbl_ofst) adt;
when'' _t'5_base, _t'5_ofst == null_ptr_spec adt;
rely is_int _t'5_ofst;
when adt == set_g_rtt_rd_spec (_g_tbl_base, _g_tbl_ofst) (_t'5_base, _t'5_ofst) adt;
when adt == granule_memzero_mapped_spec (_table_base, _table_ofst) adt;
when adt == granule_set_state_spec (_g_tbl_base, _g_tbl_ofst) 1 adt;
when adt == buffer_unmap_spec (_table_base, _table_ofst) adt;
Some (adt, (VZ64 _ret))
else
rely is_int64 _level;
when' _new_pgte, adt == table_fold_spec (_table_base, _table_ofst) (VZ64 _level) (_g_tbl_base, _g_tbl_ofst) adt;
rely is_int64 _new_pgte;
rely is_int64 _index;
when adt == pgte_write_spec (_ll_table_base, _ll_table_ofst) (VZ64 _index) (VZ64 0) adt;
rely is_int64 (Z.land _new_pgte 504403158265495552);
rely is_int64 ((Z.land _new_pgte 504403158265495552) / 72057594037927936);
if (((Z.land _new_pgte 504403158265495552) / 72057594037927936) =? 2) then
rely is_int64 _map_addr;
when adt == invalidate_pages_in_block_spec (VZ64 _map_addr) adt;
when adt == pgte_write_spec (_ll_table_base, _ll_table_ofst) (VZ64 _index) (VZ64 _new_pgte) adt;
when adt == granule_put_spec (_g_tbl_base, _g_tbl_ofst) adt;
when'' _t'5_base, _t'5_ofst == null_ptr_spec adt;
rely is_int _t'5_ofst;
when adt == set_g_rtt_rd_spec (_g_tbl_base, _g_tbl_ofst) (_t'5_base, _t'5_ofst) adt;
when adt == granule_memzero_mapped_spec (_table_base, _table_ofst) adt;
when adt == granule_set_state_spec (_g_tbl_base, _g_tbl_ofst) 1 adt;
when adt == buffer_unmap_spec (_table_base, _table_ofst) adt;
Some (adt, (VZ64 _ret))
else
rely is_int64 _map_addr;
when adt == invalidate_block_spec (VZ64 _map_addr) adt;
when adt == pgte_write_spec (_ll_table_base, _ll_table_ofst) (VZ64 _index) (VZ64 _new_pgte) adt;
when adt == granule_put_spec (_g_tbl_base, _g_tbl_ofst) adt;
when'' _t'5_base, _t'5_ofst == null_ptr_spec adt;
rely is_int _t'5_ofst;
when adt == set_g_rtt_rd_spec (_g_tbl_base, _g_tbl_ofst) (_t'5_base, _t'5_ofst) adt;
when adt == granule_memzero_mapped_spec (_table_base, _table_ofst) adt;
when adt == granule_set_state_spec (_g_tbl_base, _g_tbl_ofst) 1 adt;
when adt == buffer_unmap_spec (_table_base, _table_ofst) adt;
Some (adt, (VZ64 _ret))
else
rely is_int64 (512 + 1);
let _t'6 := (_gcnt =? (512 + 1)) in
if _t'6 then
if (_gcnt =? 1) then
when' _new_pgte, adt == table_delete_spec (_table_base, _table_ofst) (_g_llt_base, _g_llt_ofst) adt;
rely is_int64 _new_pgte;
rely is_int64 _index;
when adt == pgte_write_spec (_ll_table_base, _ll_table_ofst) (VZ64 _index) (VZ64 0) adt;
rely is_int64 (Z.land _new_pgte 504403158265495552);
rely is_int64 ((Z.land _new_pgte 504403158265495552) / 72057594037927936);
if (((Z.land _new_pgte 504403158265495552) / 72057594037927936) =? 2) then
rely is_int64 _map_addr;
when adt == invalidate_pages_in_block_spec (VZ64 _map_addr) adt;
when adt == pgte_write_spec (_ll_table_base, _ll_table_ofst) (VZ64 _index) (VZ64 _new_pgte) adt;
when adt == granule_put_spec (_g_tbl_base, _g_tbl_ofst) adt;
when'' _t'5_base, _t'5_ofst == null_ptr_spec adt;
rely is_int _t'5_ofst;
when adt == set_g_rtt_rd_spec (_g_tbl_base, _g_tbl_ofst) (_t'5_base, _t'5_ofst) adt;
when adt == granule_memzero_mapped_spec (_table_base, _table_ofst) adt;
when adt == granule_set_state_spec (_g_tbl_base, _g_tbl_ofst) 1 adt;
when adt == buffer_unmap_spec (_table_base, _table_ofst) adt;
Some (adt, (VZ64 _ret))
else
rely is_int64 _map_addr;
when adt == invalidate_block_spec (VZ64 _map_addr) adt;
when adt == pgte_write_spec (_ll_table_base, _ll_table_ofst) (VZ64 _index) (VZ64 _new_pgte) adt;
when adt == granule_put_spec (_g_tbl_base, _g_tbl_ofst) adt;
when'' _t'5_base, _t'5_ofst == null_ptr_spec adt;
rely is_int _t'5_ofst;
when adt == set_g_rtt_rd_spec (_g_tbl_base, _g_tbl_ofst) (_t'5_base, _t'5_ofst) adt;
when adt == granule_memzero_mapped_spec (_table_base, _table_ofst) adt;
when adt == granule_set_state_spec (_g_tbl_base, _g_tbl_ofst) 1 adt;
when adt == buffer_unmap_spec (_table_base, _table_ofst) adt;
Some (adt, (VZ64 _ret))
else
rely is_int64 _level;
when' _new_pgte, adt == table_fold_spec (_table_base, _table_ofst) (VZ64 _level) (_g_tbl_base, _g_tbl_ofst) adt;
rely is_int64 _new_pgte;
rely is_int64 _index;
when adt == pgte_write_spec (_ll_table_base, _ll_table_ofst) (VZ64 _index) (VZ64 0) adt;
rely is_int64 (Z.land _new_pgte 504403158265495552);
rely is_int64 ((Z.land _new_pgte 504403158265495552) / 72057594037927936);
if (((Z.land _new_pgte 504403158265495552) / 72057594037927936) =? 2) then
rely is_int64 _map_addr;
when adt == invalidate_pages_in_block_spec (VZ64 _map_addr) adt;
when adt == pgte_write_spec (_ll_table_base, _ll_table_ofst) (VZ64 _index) (VZ64 _new_pgte) adt;
when adt == granule_put_spec (_g_tbl_base, _g_tbl_ofst) adt;
when'' _t'5_base, _t'5_ofst == null_ptr_spec adt;
rely is_int _t'5_ofst;
when adt == set_g_rtt_rd_spec (_g_tbl_base, _g_tbl_ofst) (_t'5_base, _t'5_ofst) adt;
when adt == granule_memzero_mapped_spec (_table_base, _table_ofst) adt;
when adt == granule_set_state_spec (_g_tbl_base, _g_tbl_ofst) 1 adt;
when adt == buffer_unmap_spec (_table_base, _table_ofst) adt;
Some (adt, (VZ64 _ret))
else
rely is_int64 _map_addr;
when adt == invalidate_block_spec (VZ64 _map_addr) adt;
when adt == pgte_write_spec (_ll_table_base, _ll_table_ofst) (VZ64 _index) (VZ64 _new_pgte) adt;
when adt == granule_put_spec (_g_tbl_base, _g_tbl_ofst) adt;
when'' _t'5_base, _t'5_ofst == null_ptr_spec adt;
rely is_int _t'5_ofst;
when adt == set_g_rtt_rd_spec (_g_tbl_base, _g_tbl_ofst) (_t'5_base, _t'5_ofst) adt;
when adt == granule_memzero_mapped_spec (_table_base, _table_ofst) adt;
when adt == granule_set_state_spec (_g_tbl_base, _g_tbl_ofst) 1 adt;
when adt == buffer_unmap_spec (_table_base, _table_ofst) adt;
Some (adt, (VZ64 _ret))
else
let _ret := 1 in
when adt == buffer_unmap_spec (_table_base, _table_ofst) adt;
Some (adt, (VZ64 _ret))
end
.
End SpecLow.