1 | open Preamble |
---|
2 | |
---|
3 | open SmallstepExec |
---|
4 | |
---|
5 | open Cexec |
---|
6 | |
---|
7 | open Sets |
---|
8 | |
---|
9 | open Listb |
---|
10 | |
---|
11 | open IO |
---|
12 | |
---|
13 | open IOMonad |
---|
14 | |
---|
15 | open Star |
---|
16 | |
---|
17 | open ClassifyOp |
---|
18 | |
---|
19 | open Events |
---|
20 | |
---|
21 | open Smallstep |
---|
22 | |
---|
23 | open Extra_bool |
---|
24 | |
---|
25 | open Values |
---|
26 | |
---|
27 | open FrontEndVal |
---|
28 | |
---|
29 | open Hide |
---|
30 | |
---|
31 | open ByteValues |
---|
32 | |
---|
33 | open Division |
---|
34 | |
---|
35 | open Z |
---|
36 | |
---|
37 | open BitVectorZ |
---|
38 | |
---|
39 | open Pointers |
---|
40 | |
---|
41 | open GenMem |
---|
42 | |
---|
43 | open FrontEndMem |
---|
44 | |
---|
45 | open Globalenvs |
---|
46 | |
---|
47 | open Csem |
---|
48 | |
---|
49 | open BitVectorTrie |
---|
50 | |
---|
51 | open CostLabel |
---|
52 | |
---|
53 | open Coqlib |
---|
54 | |
---|
55 | open Proper |
---|
56 | |
---|
57 | open PositiveMap |
---|
58 | |
---|
59 | open Deqsets |
---|
60 | |
---|
61 | open ErrorMessages |
---|
62 | |
---|
63 | open PreIdentifiers |
---|
64 | |
---|
65 | open Errors |
---|
66 | |
---|
67 | open Extralib |
---|
68 | |
---|
69 | open Setoids |
---|
70 | |
---|
71 | open Monad |
---|
72 | |
---|
73 | open Option |
---|
74 | |
---|
75 | open Lists |
---|
76 | |
---|
77 | open Positive |
---|
78 | |
---|
79 | open Identifiers |
---|
80 | |
---|
81 | open Exp |
---|
82 | |
---|
83 | open Arithmetic |
---|
84 | |
---|
85 | open Vector |
---|
86 | |
---|
87 | open Div_and_mod |
---|
88 | |
---|
89 | open Jmeq |
---|
90 | |
---|
91 | open Russell |
---|
92 | |
---|
93 | open List |
---|
94 | |
---|
95 | open Util |
---|
96 | |
---|
97 | open FoldStuff |
---|
98 | |
---|
99 | open BitVector |
---|
100 | |
---|
101 | open Extranat |
---|
102 | |
---|
103 | open Bool |
---|
104 | |
---|
105 | open Relations |
---|
106 | |
---|
107 | open Nat |
---|
108 | |
---|
109 | open Integers |
---|
110 | |
---|
111 | open Hints_declaration |
---|
112 | |
---|
113 | open Core_notation |
---|
114 | |
---|
115 | open Pts |
---|
116 | |
---|
117 | open Logic |
---|
118 | |
---|
119 | open Types |
---|
120 | |
---|
121 | open AST |
---|
122 | |
---|
123 | open Csyntax |
---|
124 | |
---|
125 | open TypeComparison |
---|
126 | |
---|
127 | open Frontend_misc |
---|
128 | |
---|
129 | open MemProperties |
---|
130 | |
---|
131 | (** val zoo : Pointers.offset -> Z.z **) |
---|
132 | let zoo x = |
---|
133 | BitVectorZ.z_of_unsigned_bitvector Pointers.offset_size (Pointers.offv x) |
---|
134 | |
---|
135 | (** val boo : Z.z -> Pointers.offset **) |
---|
136 | let boo x = |
---|
137 | BitVectorZ.bitvector_of_Z Pointers.offset_size x |
---|
138 | |
---|
139 | (** val block_decidable_eq : |
---|
140 | Pointers.block -> Pointers.block -> (__, __) Types.sum **) |
---|
141 | let block_decidable_eq clearme = |
---|
142 | let a = clearme in |
---|
143 | (fun clearme0 -> |
---|
144 | let b = clearme0 in |
---|
145 | (match Z.decidable_eq_Z_Type a b with |
---|
146 | | Types.Inl _ -> Types.Inl __ |
---|
147 | | Types.Inr _ -> Types.Inr __)) |
---|
148 | |
---|
149 | type embedding = |
---|
150 | Pointers.block -> (Pointers.block, Pointers.offset) Types.prod Types.option |
---|
151 | |
---|
152 | (** val offset_plus : |
---|
153 | Pointers.offset -> Pointers.offset -> Pointers.offset **) |
---|
154 | let offset_plus o1 o2 = |
---|
155 | Arithmetic.addition_n Pointers.offset_size (Pointers.offv o1) |
---|
156 | (Pointers.offv o2) |
---|
157 | |
---|
158 | (** val pointer_translation : |
---|
159 | Pointers.pointer -> embedding -> Pointers.pointer Types.option **) |
---|
160 | let pointer_translation p e1 = |
---|
161 | let { Pointers.pblock = pblock0; Pointers.poff = poff0 } = p in |
---|
162 | (match e1 pblock0 with |
---|
163 | | Types.None -> Types.None |
---|
164 | | Types.Some loc -> |
---|
165 | let { Types.fst = dest_block; Types.snd = dest_off } = loc in |
---|
166 | let ptr = { Pointers.pblock = dest_block; Pointers.poff = |
---|
167 | (offset_plus poff0 dest_off) } |
---|
168 | in |
---|
169 | Types.Some ptr) |
---|
170 | |
---|
171 | (** val memory_inj_rect_Type4 : |
---|
172 | embedding -> GenMem.mem1 -> GenMem.mem1 -> (__ -> __ -> __ -> __ -> __ -> |
---|
173 | __ -> __ -> 'a1) -> 'a1 **) |
---|
174 | let rec memory_inj_rect_Type4 e1 m1 m2 h_mk_memory_inj = |
---|
175 | h_mk_memory_inj __ __ __ __ __ __ __ |
---|
176 | |
---|
177 | (** val memory_inj_rect_Type5 : |
---|
178 | embedding -> GenMem.mem1 -> GenMem.mem1 -> (__ -> __ -> __ -> __ -> __ -> |
---|
179 | __ -> __ -> 'a1) -> 'a1 **) |
---|
180 | let rec memory_inj_rect_Type5 e1 m1 m2 h_mk_memory_inj = |
---|
181 | h_mk_memory_inj __ __ __ __ __ __ __ |
---|
182 | |
---|
183 | (** val memory_inj_rect_Type3 : |
---|
184 | embedding -> GenMem.mem1 -> GenMem.mem1 -> (__ -> __ -> __ -> __ -> __ -> |
---|
185 | __ -> __ -> 'a1) -> 'a1 **) |
---|
186 | let rec memory_inj_rect_Type3 e1 m1 m2 h_mk_memory_inj = |
---|
187 | h_mk_memory_inj __ __ __ __ __ __ __ |
---|
188 | |
---|
189 | (** val memory_inj_rect_Type2 : |
---|
190 | embedding -> GenMem.mem1 -> GenMem.mem1 -> (__ -> __ -> __ -> __ -> __ -> |
---|
191 | __ -> __ -> 'a1) -> 'a1 **) |
---|
192 | let rec memory_inj_rect_Type2 e1 m1 m2 h_mk_memory_inj = |
---|
193 | h_mk_memory_inj __ __ __ __ __ __ __ |
---|
194 | |
---|
195 | (** val memory_inj_rect_Type1 : |
---|
196 | embedding -> GenMem.mem1 -> GenMem.mem1 -> (__ -> __ -> __ -> __ -> __ -> |
---|
197 | __ -> __ -> 'a1) -> 'a1 **) |
---|
198 | let rec memory_inj_rect_Type1 e1 m1 m2 h_mk_memory_inj = |
---|
199 | h_mk_memory_inj __ __ __ __ __ __ __ |
---|
200 | |
---|
201 | (** val memory_inj_rect_Type0 : |
---|
202 | embedding -> GenMem.mem1 -> GenMem.mem1 -> (__ -> __ -> __ -> __ -> __ -> |
---|
203 | __ -> __ -> 'a1) -> 'a1 **) |
---|
204 | let rec memory_inj_rect_Type0 e1 m1 m2 h_mk_memory_inj = |
---|
205 | h_mk_memory_inj __ __ __ __ __ __ __ |
---|
206 | |
---|
207 | (** val memory_inj_inv_rect_Type4 : |
---|
208 | embedding -> GenMem.mem1 -> GenMem.mem1 -> (__ -> __ -> __ -> __ -> __ -> |
---|
209 | __ -> __ -> __ -> 'a1) -> 'a1 **) |
---|
210 | let memory_inj_inv_rect_Type4 x1 x2 x3 h1 = |
---|
211 | let hcut = memory_inj_rect_Type4 x1 x2 x3 h1 in hcut __ |
---|
212 | |
---|
213 | (** val memory_inj_inv_rect_Type3 : |
---|
214 | embedding -> GenMem.mem1 -> GenMem.mem1 -> (__ -> __ -> __ -> __ -> __ -> |
---|
215 | __ -> __ -> __ -> 'a1) -> 'a1 **) |
---|
216 | let memory_inj_inv_rect_Type3 x1 x2 x3 h1 = |
---|
217 | let hcut = memory_inj_rect_Type3 x1 x2 x3 h1 in hcut __ |
---|
218 | |
---|
219 | (** val memory_inj_inv_rect_Type2 : |
---|
220 | embedding -> GenMem.mem1 -> GenMem.mem1 -> (__ -> __ -> __ -> __ -> __ -> |
---|
221 | __ -> __ -> __ -> 'a1) -> 'a1 **) |
---|
222 | let memory_inj_inv_rect_Type2 x1 x2 x3 h1 = |
---|
223 | let hcut = memory_inj_rect_Type2 x1 x2 x3 h1 in hcut __ |
---|
224 | |
---|
225 | (** val memory_inj_inv_rect_Type1 : |
---|
226 | embedding -> GenMem.mem1 -> GenMem.mem1 -> (__ -> __ -> __ -> __ -> __ -> |
---|
227 | __ -> __ -> __ -> 'a1) -> 'a1 **) |
---|
228 | let memory_inj_inv_rect_Type1 x1 x2 x3 h1 = |
---|
229 | let hcut = memory_inj_rect_Type1 x1 x2 x3 h1 in hcut __ |
---|
230 | |
---|
231 | (** val memory_inj_inv_rect_Type0 : |
---|
232 | embedding -> GenMem.mem1 -> GenMem.mem1 -> (__ -> __ -> __ -> __ -> __ -> |
---|
233 | __ -> __ -> __ -> 'a1) -> 'a1 **) |
---|
234 | let memory_inj_inv_rect_Type0 x1 x2 x3 h1 = |
---|
235 | let hcut = memory_inj_rect_Type0 x1 x2 x3 h1 in hcut __ |
---|
236 | |
---|
237 | (** val memory_inj_jmdiscr : |
---|
238 | embedding -> GenMem.mem1 -> GenMem.mem1 -> __ **) |
---|
239 | let memory_inj_jmdiscr a1 a2 a3 = |
---|
240 | Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __)) __ |
---|
241 | |
---|
242 | (** val typesize' : Csyntax.type0 -> Nat.nat **) |
---|
243 | let typesize' ty = |
---|
244 | AST.typesize (Csyntax.typ_of_type ty) |
---|
245 | |
---|