-
Notifications
You must be signed in to change notification settings - Fork 1
/
data_create.v
187 lines (159 loc) · 10.4 KB
/
data_create.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
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
Require Import CodeProofDeps.
Require Import Ident.
Require Import Constants.
Require Import RData.
Require Import EventReplay.
Require Import MoverTypes.
Require Import CommonLib.
Require Import TableWalk.Spec.
Require Import AbsAccessor.Spec.
Require Import TableWalk.Layer.
Require Import TableDataOpsIntro.Code.data_create.
Require Import TableDataOpsIntro.LowSpecs.data_create.
Local Open Scope Z_scope.
Section CodeProof.
Context `{real_params: RealParams}.
Context {memb} `{Hmemx: Mem.MemoryModelX memb}.
Context `{Hmwd: UseMemWithData memb}.
Let mem := mwd (cdata RData).
Context `{Hstencil: Stencil}.
Context `{make_program_ops: !MakeProgramOps Clight.function type Clight.fundef type}.
Context `{Hmake_program: !MakeProgram Clight.function type Clight.fundef type}.
Let L : compatlayer (cdata RData) :=
_table_walk_lock_unlock ↦ gensem table_walk_lock_unlock_spec
⊕ _get_wi_g_llt ↦ gensem get_wi_g_llt_spec
⊕ _get_wi_index ↦ gensem get_wi_index_spec
⊕ _is_null ↦ gensem is_null_spec
⊕ _granule_map ↦ gensem granule_map_spec
⊕ _pgte_read ↦ gensem pgte_read_spec
⊕ _ns_granule_map ↦ gensem ns_granule_map_spec
⊕ _ns_buffer_read_data ↦ gensem ns_buffer_read_data_spec
⊕ _ns_buffer_unmap ↦ gensem ns_buffer_unmap_spec
⊕ _buffer_unmap ↦ gensem buffer_unmap_spec
⊕ _granule_memzero_mapped ↦ gensem granule_memzero_mapped_spec
⊕ _granule_memzero ↦ gensem granule_memzero_spec
⊕ _pgte_write ↦ gensem pgte_write_spec
⊕ _set_mapping ↦ gensem set_mapping_spec
⊕ _granule_get ↦ gensem granule_get_spec
⊕ _granule_unlock ↦ gensem granule_unlock_spec
.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section BodyProof.
Context `{Hwb: WritableBlockOps}.
Variable (sc: stencil).
Variables (ge: genv) (STENCIL_MATCHES: stencil_matches sc ge).
Variable b_table_walk_lock_unlock: block.
Hypothesis h_table_walk_lock_unlock_s : Genv.find_symbol ge _table_walk_lock_unlock = Some b_table_walk_lock_unlock.
Hypothesis h_table_walk_lock_unlock_p : Genv.find_funct_ptr ge b_table_walk_lock_unlock
= Some (External (EF_external _table_walk_lock_unlock
(signature_of_type (Tcons Tptr (Tcons tulong (Tcons tulong Tnil))) tvoid cc_default))
(Tcons Tptr (Tcons tulong (Tcons tulong Tnil))) tvoid cc_default).
Local Opaque table_walk_lock_unlock_spec.
Variable b_get_wi_g_llt: block.
Hypothesis h_get_wi_g_llt_s : Genv.find_symbol ge _get_wi_g_llt = Some b_get_wi_g_llt.
Hypothesis h_get_wi_g_llt_p : Genv.find_funct_ptr ge b_get_wi_g_llt
= Some (External (EF_external _get_wi_g_llt
(signature_of_type Tnil Tptr cc_default))
Tnil Tptr cc_default).
Local Opaque get_wi_g_llt_spec.
Variable b_get_wi_index: block.
Hypothesis h_get_wi_index_s : Genv.find_symbol ge _get_wi_index = Some b_get_wi_index.
Hypothesis h_get_wi_index_p : Genv.find_funct_ptr ge b_get_wi_index
= Some (External (EF_external _get_wi_index
(signature_of_type Tnil tulong cc_default))
Tnil tulong cc_default).
Local Opaque get_wi_index_spec.
Variable b_is_null: block.
Hypothesis h_is_null_s : Genv.find_symbol ge _is_null = Some b_is_null.
Hypothesis h_is_null_p : Genv.find_funct_ptr ge b_is_null
= Some (External (EF_external _is_null
(signature_of_type (Tcons Tptr Tnil) tuint cc_default))
(Tcons Tptr Tnil) tuint cc_default).
Local Opaque is_null_spec.
Variable b_granule_map: block.
Hypothesis h_granule_map_s : Genv.find_symbol ge _granule_map = Some b_granule_map.
Hypothesis h_granule_map_p : Genv.find_funct_ptr ge b_granule_map
= Some (External (EF_external _granule_map
(signature_of_type (Tcons Tptr (Tcons tuint Tnil)) Tptr cc_default))
(Tcons Tptr (Tcons tuint Tnil)) Tptr cc_default).
Local Opaque granule_map_spec.
Variable b_pgte_read: block.
Hypothesis h_pgte_read_s : Genv.find_symbol ge _pgte_read = Some b_pgte_read.
Hypothesis h_pgte_read_p : Genv.find_funct_ptr ge b_pgte_read
= Some (External (EF_external _pgte_read
(signature_of_type (Tcons Tptr (Tcons tulong Tnil)) tulong cc_default))
(Tcons Tptr (Tcons tulong Tnil)) tulong cc_default).
Local Opaque pgte_read_spec.
Variable b_ns_granule_map: block.
Hypothesis h_ns_granule_map_s : Genv.find_symbol ge _ns_granule_map = Some b_ns_granule_map.
Hypothesis h_ns_granule_map_p : Genv.find_funct_ptr ge b_ns_granule_map
= Some (External (EF_external _ns_granule_map
(signature_of_type (Tcons tuint (Tcons Tptr Tnil)) tvoid cc_default))
(Tcons tuint (Tcons Tptr Tnil)) tvoid cc_default).
Local Opaque ns_granule_map_spec.
Variable b_ns_buffer_read_data: block.
Hypothesis h_ns_buffer_read_data_s : Genv.find_symbol ge _ns_buffer_read_data = Some b_ns_buffer_read_data.
Hypothesis h_ns_buffer_read_data_p : Genv.find_funct_ptr ge b_ns_buffer_read_data
= Some (External (EF_external _ns_buffer_read_data
(signature_of_type (Tcons tuint (Tcons Tptr Tnil)) tuint cc_default))
(Tcons tuint (Tcons Tptr Tnil)) tuint cc_default).
Local Opaque ns_buffer_read_data_spec.
Variable b_ns_buffer_unmap: block.
Hypothesis h_ns_buffer_unmap_s : Genv.find_symbol ge _ns_buffer_unmap = Some b_ns_buffer_unmap.
Hypothesis h_ns_buffer_unmap_p : Genv.find_funct_ptr ge b_ns_buffer_unmap
= Some (External (EF_external _ns_buffer_unmap
(signature_of_type (Tcons tuint Tnil) tvoid cc_default))
(Tcons tuint Tnil) tvoid cc_default).
Local Opaque ns_buffer_unmap_spec.
Variable b_buffer_unmap: block.
Hypothesis h_buffer_unmap_s : Genv.find_symbol ge _buffer_unmap = Some b_buffer_unmap.
Hypothesis h_buffer_unmap_p : Genv.find_funct_ptr ge b_buffer_unmap
= Some (External (EF_external _buffer_unmap
(signature_of_type (Tcons Tptr Tnil) tvoid cc_default))
(Tcons Tptr Tnil) tvoid cc_default).
Local Opaque buffer_unmap_spec.
Variable b_granule_memzero_mapped: block.
Hypothesis h_granule_memzero_mapped_s : Genv.find_symbol ge _granule_memzero_mapped = Some b_granule_memzero_mapped.
Hypothesis h_granule_memzero_mapped_p : Genv.find_funct_ptr ge b_granule_memzero_mapped
= Some (External (EF_external _granule_memzero_mapped
(signature_of_type (Tcons Tptr Tnil) tvoid cc_default))
(Tcons Tptr Tnil) tvoid cc_default).
Local Opaque granule_memzero_mapped_spec.
Variable b_granule_memzero: block.
Hypothesis h_granule_memzero_s : Genv.find_symbol ge _granule_memzero = Some b_granule_memzero.
Hypothesis h_granule_memzero_p : Genv.find_funct_ptr ge b_granule_memzero
= Some (External (EF_external _granule_memzero
(signature_of_type (Tcons Tptr (Tcons tuint Tnil)) tvoid cc_default))
(Tcons Tptr (Tcons tuint Tnil)) tvoid cc_default).
Local Opaque granule_memzero_spec.
Variable b_pgte_write: block.
Hypothesis h_pgte_write_s : Genv.find_symbol ge _pgte_write = Some b_pgte_write.
Hypothesis h_pgte_write_p : Genv.find_funct_ptr ge b_pgte_write
= Some (External (EF_external _pgte_write
(signature_of_type (Tcons Tptr (Tcons tulong (Tcons tulong Tnil))) tvoid cc_default))
(Tcons Tptr (Tcons tulong (Tcons tulong Tnil))) tvoid cc_default).
Local Opaque pgte_write_spec.
Variable b_set_mapping: block.
Hypothesis h_set_mapping_s : Genv.find_symbol ge _set_mapping = Some b_set_mapping.
Hypothesis h_set_mapping_p : Genv.find_funct_ptr ge b_set_mapping
= Some (External (EF_external _set_mapping
(signature_of_type (Tcons tulong (Tcons tulong Tnil)) tvoid cc_default))
(Tcons tulong (Tcons tulong Tnil)) tvoid cc_default).
Local Opaque set_mapping_spec.
Variable b_granule_get: block.
Hypothesis h_granule_get_s : Genv.find_symbol ge _granule_get = Some b_granule_get.
Hypothesis h_granule_get_p : Genv.find_funct_ptr ge b_granule_get
= Some (External (EF_external _granule_get
(signature_of_type (Tcons Tptr Tnil) tvoid cc_default))
(Tcons Tptr Tnil) tvoid cc_default).
Local Opaque granule_get_spec.
Variable b_granule_unlock: block.
Hypothesis h_granule_unlock_s : Genv.find_symbol ge _granule_unlock = Some b_granule_unlock.
Hypothesis h_granule_unlock_p : Genv.find_funct_ptr ge b_granule_unlock
= Some (External (EF_external _granule_unlock
(signature_of_type (Tcons Tptr Tnil) tvoid cc_default))
(Tcons Tptr Tnil) tvoid cc_default).
Local Opaque granule_unlock_spec.
End BodyProof.
End CodeProof.