1 | open Preamble |
---|
2 | |
---|
3 | open BitVectorTrie |
---|
4 | |
---|
5 | open CostLabel |
---|
6 | |
---|
7 | open Coqlib |
---|
8 | |
---|
9 | open Proper |
---|
10 | |
---|
11 | open PositiveMap |
---|
12 | |
---|
13 | open Deqsets |
---|
14 | |
---|
15 | open ErrorMessages |
---|
16 | |
---|
17 | open PreIdentifiers |
---|
18 | |
---|
19 | open Errors |
---|
20 | |
---|
21 | open Extralib |
---|
22 | |
---|
23 | open Setoids |
---|
24 | |
---|
25 | open Monad |
---|
26 | |
---|
27 | open Option |
---|
28 | |
---|
29 | open Lists |
---|
30 | |
---|
31 | open Positive |
---|
32 | |
---|
33 | open Identifiers |
---|
34 | |
---|
35 | open Exp |
---|
36 | |
---|
37 | open Arithmetic |
---|
38 | |
---|
39 | open Vector |
---|
40 | |
---|
41 | open Div_and_mod |
---|
42 | |
---|
43 | open Jmeq |
---|
44 | |
---|
45 | open Russell |
---|
46 | |
---|
47 | open List |
---|
48 | |
---|
49 | open Util |
---|
50 | |
---|
51 | open FoldStuff |
---|
52 | |
---|
53 | open BitVector |
---|
54 | |
---|
55 | open Extranat |
---|
56 | |
---|
57 | open Bool |
---|
58 | |
---|
59 | open Relations |
---|
60 | |
---|
61 | open Nat |
---|
62 | |
---|
63 | open Integers |
---|
64 | |
---|
65 | open Hints_declaration |
---|
66 | |
---|
67 | open Core_notation |
---|
68 | |
---|
69 | open Pts |
---|
70 | |
---|
71 | open Logic |
---|
72 | |
---|
73 | open Types |
---|
74 | |
---|
75 | open AST |
---|
76 | |
---|
77 | open Csyntax |
---|
78 | |
---|
79 | open TypeComparison |
---|
80 | |
---|
81 | open ClassifyOp |
---|
82 | |
---|
83 | open Smallstep |
---|
84 | |
---|
85 | open Extra_bool |
---|
86 | |
---|
87 | open FrontEndVal |
---|
88 | |
---|
89 | open Hide |
---|
90 | |
---|
91 | open ByteValues |
---|
92 | |
---|
93 | open GenMem |
---|
94 | |
---|
95 | open FrontEndMem |
---|
96 | |
---|
97 | open Globalenvs |
---|
98 | |
---|
99 | open Csem |
---|
100 | |
---|
101 | open SmallstepExec |
---|
102 | |
---|
103 | open Division |
---|
104 | |
---|
105 | open Z |
---|
106 | |
---|
107 | open BitVectorZ |
---|
108 | |
---|
109 | open Pointers |
---|
110 | |
---|
111 | open Values |
---|
112 | |
---|
113 | open Events |
---|
114 | |
---|
115 | open IOMonad |
---|
116 | |
---|
117 | open IO |
---|
118 | |
---|
119 | open Cexec |
---|
120 | |
---|
121 | open Casts |
---|
122 | |
---|
123 | open CexecInd |
---|
124 | |
---|
125 | open CexecSound |
---|
126 | |
---|
127 | open Sets |
---|
128 | |
---|
129 | open Listb |
---|
130 | |
---|
131 | open Star |
---|
132 | |
---|
133 | open Frontend_misc |
---|
134 | |
---|
135 | (** val reduce_bits : |
---|
136 | Nat.nat -> Nat.nat -> Bool.bool -> BitVector.bitVector -> |
---|
137 | BitVector.bitVector Types.option **) |
---|
138 | let rec reduce_bits n m exp0 v = |
---|
139 | (match n with |
---|
140 | | Nat.O -> (fun v0 -> Types.Some v0) |
---|
141 | | Nat.S n' -> |
---|
142 | (fun v0 -> |
---|
143 | match BitVector.eq_b (Vector.head' (Nat.plus n' (Nat.S m)) v0) exp0 with |
---|
144 | | Bool.True -> |
---|
145 | reduce_bits n' m exp0 (Vector.tail0 (Nat.plus n' (Nat.S m)) v0) |
---|
146 | | Bool.False -> Types.None)) v |
---|
147 | |
---|
148 | (** val pred_bitsize_of_intsize : AST.intsize -> Nat.nat **) |
---|
149 | let pred_bitsize_of_intsize sz = |
---|
150 | Nat.pred (AST.bitsize_of_intsize sz) |
---|
151 | |
---|
152 | (** val signed : AST.signedness -> Bool.bool **) |
---|
153 | let signed = function |
---|
154 | | AST.Signed -> Bool.True |
---|
155 | | AST.Unsigned -> Bool.False |
---|
156 | |
---|
157 | (** val simplify_int : |
---|
158 | AST.intsize -> AST.intsize -> AST.signedness -> AST.signedness -> |
---|
159 | AST.bvint -> AST.bvint Types.option **) |
---|
160 | let rec simplify_int sz sz' sg sg' i = |
---|
161 | let bit0 = |
---|
162 | Bool.andb (signed sg) |
---|
163 | (Vector.head' |
---|
164 | (Nat.plus (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
165 | Nat.O))))))) |
---|
166 | (Nat.times (AST.pred_size_intsize sz) (Nat.S (Nat.S (Nat.S (Nat.S |
---|
167 | (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))) i) |
---|
168 | in |
---|
169 | (match Extranat.nat_compare (pred_bitsize_of_intsize sz) |
---|
170 | (pred_bitsize_of_intsize sz') with |
---|
171 | | Extranat.Nat_lt (x, x0) -> (fun i0 -> Types.None) |
---|
172 | | Extranat.Nat_eq x -> (fun i0 -> Types.Some i0) |
---|
173 | | Extranat.Nat_gt (x, y) -> |
---|
174 | (fun i0 -> |
---|
175 | match reduce_bits (Nat.S x) y bit0 i0 with |
---|
176 | | Types.None -> Types.None |
---|
177 | | Types.Some i' -> |
---|
178 | (match signed sg' with |
---|
179 | | Bool.True -> |
---|
180 | (match BitVector.eq_b bit0 (Vector.head' y i') with |
---|
181 | | Bool.True -> Types.Some i' |
---|
182 | | Bool.False -> Types.None) |
---|
183 | | Bool.False -> Types.Some i'))) i |
---|
184 | |
---|
185 | (** val size_lt_dec : AST.intsize -> AST.intsize -> (__, __) Types.sum **) |
---|
186 | let size_lt_dec = function |
---|
187 | | AST.I8 -> |
---|
188 | (fun clearme0 -> |
---|
189 | match clearme0 with |
---|
190 | | AST.I8 -> Types.Inr __ |
---|
191 | | AST.I16 -> Types.Inl __ |
---|
192 | | AST.I32 -> Types.Inl __) |
---|
193 | | AST.I16 -> |
---|
194 | (fun clearme0 -> |
---|
195 | match clearme0 with |
---|
196 | | AST.I8 -> Types.Inr __ |
---|
197 | | AST.I16 -> Types.Inr __ |
---|
198 | | AST.I32 -> Types.Inl __) |
---|
199 | | AST.I32 -> |
---|
200 | (fun clearme0 -> |
---|
201 | match clearme0 with |
---|
202 | | AST.I8 -> Types.Inr __ |
---|
203 | | AST.I16 -> Types.Inr __ |
---|
204 | | AST.I32 -> Types.Inr __) |
---|
205 | |
---|
206 | (** val size_not_lt_to_ge : |
---|
207 | AST.intsize -> AST.intsize -> (__, __) Types.sum **) |
---|
208 | let size_not_lt_to_ge clearme sz2 = |
---|
209 | (match clearme with |
---|
210 | | AST.I8 -> |
---|
211 | (fun clearme0 -> |
---|
212 | match clearme0 with |
---|
213 | | AST.I8 -> (fun _ -> Types.Inl __) |
---|
214 | | AST.I16 -> (fun _ -> Types.Inr __) |
---|
215 | | AST.I32 -> (fun _ -> Types.Inr __)) |
---|
216 | | AST.I16 -> |
---|
217 | (fun clearme0 -> |
---|
218 | match clearme0 with |
---|
219 | | AST.I8 -> (fun _ -> Types.Inr __) |
---|
220 | | AST.I16 -> (fun _ -> Types.Inl __) |
---|
221 | | AST.I32 -> (fun _ -> Types.Inr __)) |
---|
222 | | AST.I32 -> |
---|
223 | (fun clearme0 -> |
---|
224 | match clearme0 with |
---|
225 | | AST.I8 -> (fun _ -> Types.Inr __) |
---|
226 | | AST.I16 -> (fun _ -> Types.Inr __) |
---|
227 | | AST.I32 -> (fun _ -> Types.Inl __))) sz2 __ |
---|
228 | |
---|
229 | (** val sign_eq_dect : |
---|
230 | AST.signedness -> AST.signedness -> (__, __) Types.sum **) |
---|
231 | let sign_eq_dect = function |
---|
232 | | AST.Signed -> |
---|
233 | (fun clearme0 -> |
---|
234 | match clearme0 with |
---|
235 | | AST.Signed -> TypeComparison.sg_eq_dec AST.Signed AST.Signed |
---|
236 | | AST.Unsigned -> TypeComparison.sg_eq_dec AST.Signed AST.Unsigned) |
---|
237 | | AST.Unsigned -> |
---|
238 | (fun clearme0 -> |
---|
239 | match clearme0 with |
---|
240 | | AST.Signed -> TypeComparison.sg_eq_dec AST.Unsigned AST.Signed |
---|
241 | | AST.Unsigned -> TypeComparison.sg_eq_dec AST.Unsigned AST.Unsigned) |
---|
242 | |
---|
243 | (** val necessary_conditions : |
---|
244 | AST.intsize -> AST.signedness -> AST.intsize -> AST.signedness -> |
---|
245 | Bool.bool **) |
---|
246 | let necessary_conditions src_sz src_sg target_sz target_sg = |
---|
247 | match size_lt_dec target_sz src_sz with |
---|
248 | | Types.Inl _ -> Bool.True |
---|
249 | | Types.Inr _ -> |
---|
250 | (match TypeComparison.sz_eq_dec target_sz src_sz with |
---|
251 | | Types.Inl _ -> |
---|
252 | (match sign_eq_dect src_sg target_sg with |
---|
253 | | Types.Inl _ -> Bool.False |
---|
254 | | Types.Inr _ -> Bool.True) |
---|
255 | | Types.Inr _ -> Bool.False) |
---|
256 | |
---|
257 | (** val assert_int_value : |
---|
258 | Values.val0 Types.option -> AST.intsize -> BitVector.bitVector |
---|
259 | Types.option **) |
---|
260 | let rec assert_int_value v expected_size = |
---|
261 | match v with |
---|
262 | | Types.None -> Types.None |
---|
263 | | Types.Some v0 -> |
---|
264 | (match v0 with |
---|
265 | | Values.Vundef -> Types.None |
---|
266 | | Values.Vint (sz, i) -> |
---|
267 | (match TypeComparison.sz_eq_dec sz expected_size with |
---|
268 | | Types.Inl _ -> |
---|
269 | Types.Some |
---|
270 | (Extralib.eq_rect_Type0_r1 expected_size (fun i0 -> i0) sz i) |
---|
271 | | Types.Inr _ -> Types.None) |
---|
272 | | Values.Vnull -> Types.None |
---|
273 | | Values.Vptr x -> Types.None) |
---|
274 | |
---|
275 | (** val binop_simplifiable : Csyntax.binary_operation -> Bool.bool **) |
---|
276 | let binop_simplifiable = function |
---|
277 | | Csyntax.Oadd -> Bool.True |
---|
278 | | Csyntax.Osub -> Bool.True |
---|
279 | | Csyntax.Omul -> Bool.False |
---|
280 | | Csyntax.Odiv -> Bool.False |
---|
281 | | Csyntax.Omod -> Bool.False |
---|
282 | | Csyntax.Oand -> Bool.False |
---|
283 | | Csyntax.Oor -> Bool.False |
---|
284 | | Csyntax.Oxor -> Bool.False |
---|
285 | | Csyntax.Oshl -> Bool.False |
---|
286 | | Csyntax.Oshr -> Bool.False |
---|
287 | | Csyntax.Oeq -> Bool.False |
---|
288 | | Csyntax.One0 -> Bool.False |
---|
289 | | Csyntax.Olt -> Bool.False |
---|
290 | | Csyntax.Ogt -> Bool.False |
---|
291 | | Csyntax.Ole -> Bool.False |
---|
292 | | Csyntax.Oge -> Bool.False |
---|
293 | |
---|
294 | (** val simplify_expr : |
---|
295 | Csyntax.expr -> AST.intsize -> AST.signedness -> (Bool.bool, |
---|
296 | Csyntax.expr) Types.prod Types.sig0 **) |
---|
297 | let rec simplify_expr e1 target_sz target_sg = |
---|
298 | (let Csyntax.Expr (ed, ty) = e1 in |
---|
299 | (fun _ -> |
---|
300 | (match ed with |
---|
301 | | Csyntax.Econst_int (cst_sz, i) -> |
---|
302 | (fun _ -> |
---|
303 | (match ty with |
---|
304 | | Csyntax.Tvoid -> |
---|
305 | (fun _ -> { Types.fst = Bool.False; Types.snd = e1 }) |
---|
306 | | Csyntax.Tint (ty_sz, sg) -> |
---|
307 | (fun _ -> |
---|
308 | match TypeComparison.sz_eq_dec cst_sz ty_sz with |
---|
309 | | Types.Inl _ -> |
---|
310 | (match TypeComparison.type_eq_dec ty (Csyntax.Tint (target_sz, |
---|
311 | target_sg)) with |
---|
312 | | Types.Inl _ -> { Types.fst = Bool.True; Types.snd = e1 } |
---|
313 | | Types.Inr _ -> |
---|
314 | (match simplify_int cst_sz target_sz sg target_sg i with |
---|
315 | | Types.None -> |
---|
316 | (fun _ -> { Types.fst = Bool.False; Types.snd = e1 }) |
---|
317 | | Types.Some i' -> |
---|
318 | (fun _ -> { Types.fst = Bool.True; Types.snd = |
---|
319 | (Csyntax.Expr ((Csyntax.Econst_int (target_sz, i')), |
---|
320 | (Csyntax.Tint (target_sz, target_sg)))) })) __) |
---|
321 | | Types.Inr _ -> { Types.fst = Bool.False; Types.snd = e1 }) |
---|
322 | | Csyntax.Tpointer x -> |
---|
323 | (fun _ -> { Types.fst = Bool.False; Types.snd = e1 }) |
---|
324 | | Csyntax.Tarray (x, x0) -> |
---|
325 | (fun _ -> { Types.fst = Bool.False; Types.snd = e1 }) |
---|
326 | | Csyntax.Tfunction (x, x0) -> |
---|
327 | (fun _ -> { Types.fst = Bool.False; Types.snd = e1 }) |
---|
328 | | Csyntax.Tstruct (x, x0) -> |
---|
329 | (fun _ -> { Types.fst = Bool.False; Types.snd = e1 }) |
---|
330 | | Csyntax.Tunion (x, x0) -> |
---|
331 | (fun _ -> { Types.fst = Bool.False; Types.snd = e1 }) |
---|
332 | | Csyntax.Tcomp_ptr x -> |
---|
333 | (fun _ -> { Types.fst = Bool.False; Types.snd = e1 })) __) |
---|
334 | | Csyntax.Evar id -> |
---|
335 | (fun _ -> { Types.fst = |
---|
336 | (TypeComparison.type_eq ty (Csyntax.Tint (target_sz, target_sg))); |
---|
337 | Types.snd = (Csyntax.Expr (ed, ty)) }) |
---|
338 | | Csyntax.Ederef e2 -> |
---|
339 | (fun _ -> |
---|
340 | (let e3 = simplify_inside e2 in |
---|
341 | (fun _ -> { Types.fst = Bool.False; Types.snd = (Csyntax.Expr |
---|
342 | ((Csyntax.Ederef e3), ty)) })) __) |
---|
343 | | Csyntax.Eaddrof e2 -> |
---|
344 | (fun _ -> |
---|
345 | (let e3 = simplify_inside e2 in |
---|
346 | (fun _ -> { Types.fst = Bool.False; Types.snd = (Csyntax.Expr |
---|
347 | ((Csyntax.Eaddrof e3), ty)) })) __) |
---|
348 | | Csyntax.Eunop (op0, e2) -> |
---|
349 | (fun _ -> |
---|
350 | (let e3 = simplify_inside e2 in |
---|
351 | (fun _ -> { Types.fst = Bool.False; Types.snd = (Csyntax.Expr |
---|
352 | ((Csyntax.Eunop (op0, e3)), ty)) })) __) |
---|
353 | | Csyntax.Ebinop (op0, lhs, rhs) -> |
---|
354 | (fun _ -> |
---|
355 | (match binop_simplifiable op0 with |
---|
356 | | Bool.True -> |
---|
357 | (fun _ -> |
---|
358 | match TypeComparison.assert_type_eq ty (Csyntax.typeof lhs) with |
---|
359 | | Errors.OK _ -> |
---|
360 | (match TypeComparison.assert_type_eq (Csyntax.typeof lhs) |
---|
361 | (Csyntax.typeof rhs) with |
---|
362 | | Errors.OK _ -> |
---|
363 | (let eta2519 = simplify_expr lhs target_sz target_sg in |
---|
364 | (fun _ -> |
---|
365 | (let { Types.fst = desired_type_lhs; Types.snd = lhs1 } = |
---|
366 | eta2519 |
---|
367 | in |
---|
368 | (fun _ -> |
---|
369 | (let eta2518 = simplify_expr rhs target_sz target_sg in |
---|
370 | (fun _ -> |
---|
371 | (let { Types.fst = desired_type_rhs; Types.snd = |
---|
372 | rhs1 } = eta2518 |
---|
373 | in |
---|
374 | (fun _ -> |
---|
375 | (match Bool.andb desired_type_lhs desired_type_rhs with |
---|
376 | | Bool.True -> |
---|
377 | (fun _ -> { Types.fst = Bool.True; Types.snd = |
---|
378 | (Csyntax.Expr ((Csyntax.Ebinop (op0, lhs1, rhs1)), |
---|
379 | (Csyntax.Tint (target_sz, target_sg)))) }) |
---|
380 | | Bool.False -> |
---|
381 | (fun _ -> |
---|
382 | (let lhs10 = simplify_inside lhs in |
---|
383 | (fun _ -> |
---|
384 | (let rhs10 = simplify_inside rhs in |
---|
385 | (fun _ -> { Types.fst = Bool.False; Types.snd = |
---|
386 | (Csyntax.Expr ((Csyntax.Ebinop (op0, lhs10, |
---|
387 | rhs10)), ty)) })) __)) __)) __)) __)) __)) __)) |
---|
388 | __ |
---|
389 | | Errors.Error x -> |
---|
390 | (let lhs1 = simplify_inside lhs in |
---|
391 | (fun _ -> |
---|
392 | (let rhs1 = simplify_inside rhs in |
---|
393 | (fun _ -> { Types.fst = Bool.False; Types.snd = |
---|
394 | (Csyntax.Expr ((Csyntax.Ebinop (op0, lhs1, rhs1)), |
---|
395 | ty)) })) __)) __) |
---|
396 | | Errors.Error x -> |
---|
397 | (let lhs1 = simplify_inside lhs in |
---|
398 | (fun _ -> |
---|
399 | (let rhs1 = simplify_inside rhs in |
---|
400 | (fun _ -> { Types.fst = Bool.False; Types.snd = |
---|
401 | (Csyntax.Expr ((Csyntax.Ebinop (op0, lhs1, rhs1)), ty)) })) |
---|
402 | __)) __) |
---|
403 | | Bool.False -> |
---|
404 | (fun _ -> |
---|
405 | (let lhs1 = simplify_inside lhs in |
---|
406 | (fun _ -> |
---|
407 | (let rhs1 = simplify_inside rhs in |
---|
408 | (fun _ -> { Types.fst = Bool.False; Types.snd = (Csyntax.Expr |
---|
409 | ((Csyntax.Ebinop (op0, lhs1, rhs1)), ty)) })) __)) __)) __) |
---|
410 | | Csyntax.Ecast (cast_ty, castee) -> |
---|
411 | (fun _ -> |
---|
412 | (match cast_ty with |
---|
413 | | Csyntax.Tvoid -> |
---|
414 | (fun _ -> |
---|
415 | (let castee1 = simplify_inside castee in |
---|
416 | (fun _ -> { Types.fst = Bool.False; Types.snd = (Csyntax.Expr |
---|
417 | ((Csyntax.Ecast (cast_ty, castee1)), ty)) })) __) |
---|
418 | | Csyntax.Tint (cast_sz, cast_sg) -> |
---|
419 | (fun _ -> |
---|
420 | match TypeComparison.type_eq_dec ty cast_ty with |
---|
421 | | Types.Inl _ -> |
---|
422 | (match necessary_conditions cast_sz cast_sg target_sz target_sg with |
---|
423 | | Bool.True -> |
---|
424 | (fun _ -> |
---|
425 | (let eta2521 = simplify_expr castee target_sz target_sg in |
---|
426 | (fun _ -> |
---|
427 | (let { Types.fst = desired_type; Types.snd = castee1 } = |
---|
428 | eta2521 |
---|
429 | in |
---|
430 | (fun _ -> |
---|
431 | (match desired_type with |
---|
432 | | Bool.True -> |
---|
433 | (fun _ -> { Types.fst = Bool.True; Types.snd = |
---|
434 | castee1 }) |
---|
435 | | Bool.False -> |
---|
436 | (fun _ -> |
---|
437 | (let eta2520 = simplify_expr castee cast_sz cast_sg |
---|
438 | in |
---|
439 | (fun _ -> |
---|
440 | (let { Types.fst = desired_type2; Types.snd = |
---|
441 | castee2 } = eta2520 |
---|
442 | in |
---|
443 | (fun _ -> |
---|
444 | (match desired_type2 with |
---|
445 | | Bool.True -> |
---|
446 | (fun _ -> { Types.fst = Bool.False; |
---|
447 | Types.snd = castee2 }) |
---|
448 | | Bool.False -> |
---|
449 | (fun _ -> { Types.fst = Bool.False; |
---|
450 | Types.snd = (Csyntax.Expr ((Csyntax.Ecast |
---|
451 | (ty, castee2)), cast_ty)) })) __)) __)) __)) |
---|
452 | __)) __)) __) |
---|
453 | | Bool.False -> |
---|
454 | (fun _ -> |
---|
455 | (let eta2522 = simplify_expr castee cast_sz cast_sg in |
---|
456 | (fun _ -> |
---|
457 | (let { Types.fst = desired_type2; Types.snd = |
---|
458 | castee2 } = eta2522 |
---|
459 | in |
---|
460 | (fun _ -> |
---|
461 | (match desired_type2 with |
---|
462 | | Bool.True -> |
---|
463 | (fun _ -> { Types.fst = Bool.False; Types.snd = |
---|
464 | castee2 }) |
---|
465 | | Bool.False -> |
---|
466 | (fun _ -> { Types.fst = Bool.False; Types.snd = |
---|
467 | (Csyntax.Expr ((Csyntax.Ecast (ty, castee2)), |
---|
468 | cast_ty)) })) __)) __)) __)) __ |
---|
469 | | Types.Inr _ -> |
---|
470 | (let castee1 = simplify_inside castee in |
---|
471 | (fun _ -> { Types.fst = Bool.False; Types.snd = (Csyntax.Expr |
---|
472 | ((Csyntax.Ecast (cast_ty, castee1)), ty)) })) __) |
---|
473 | | Csyntax.Tpointer x -> |
---|
474 | (fun _ -> |
---|
475 | (let castee1 = simplify_inside castee in |
---|
476 | (fun _ -> { Types.fst = Bool.False; Types.snd = (Csyntax.Expr |
---|
477 | ((Csyntax.Ecast (cast_ty, castee1)), ty)) })) __) |
---|
478 | | Csyntax.Tarray (x, x0) -> |
---|
479 | (fun _ -> |
---|
480 | (let castee1 = simplify_inside castee in |
---|
481 | (fun _ -> { Types.fst = Bool.False; Types.snd = (Csyntax.Expr |
---|
482 | ((Csyntax.Ecast (cast_ty, castee1)), ty)) })) __) |
---|
483 | | Csyntax.Tfunction (x, x0) -> |
---|
484 | (fun _ -> |
---|
485 | (let castee1 = simplify_inside castee in |
---|
486 | (fun _ -> { Types.fst = Bool.False; Types.snd = (Csyntax.Expr |
---|
487 | ((Csyntax.Ecast (cast_ty, castee1)), ty)) })) __) |
---|
488 | | Csyntax.Tstruct (x, x0) -> |
---|
489 | (fun _ -> |
---|
490 | (let castee1 = simplify_inside castee in |
---|
491 | (fun _ -> { Types.fst = Bool.False; Types.snd = (Csyntax.Expr |
---|
492 | ((Csyntax.Ecast (cast_ty, castee1)), ty)) })) __) |
---|
493 | | Csyntax.Tunion (x, x0) -> |
---|
494 | (fun _ -> |
---|
495 | (let castee1 = simplify_inside castee in |
---|
496 | (fun _ -> { Types.fst = Bool.False; Types.snd = (Csyntax.Expr |
---|
497 | ((Csyntax.Ecast (cast_ty, castee1)), ty)) })) __) |
---|
498 | | Csyntax.Tcomp_ptr x -> |
---|
499 | (fun _ -> |
---|
500 | (let castee1 = simplify_inside castee in |
---|
501 | (fun _ -> { Types.fst = Bool.False; Types.snd = (Csyntax.Expr |
---|
502 | ((Csyntax.Ecast (cast_ty, castee1)), ty)) })) __)) __) |
---|
503 | | Csyntax.Econdition (cond, iftrue, iffalse) -> |
---|
504 | (fun _ -> |
---|
505 | (let cond1 = simplify_inside cond in |
---|
506 | (fun _ -> |
---|
507 | match TypeComparison.assert_type_eq ty (Csyntax.typeof iftrue) with |
---|
508 | | Errors.OK _ -> |
---|
509 | (match TypeComparison.assert_type_eq (Csyntax.typeof iftrue) |
---|
510 | (Csyntax.typeof iffalse) with |
---|
511 | | Errors.OK _ -> |
---|
512 | (let eta2524 = simplify_expr iftrue target_sz target_sg in |
---|
513 | (fun _ -> |
---|
514 | (let { Types.fst = desired_true; Types.snd = iftrue1 } = |
---|
515 | eta2524 |
---|
516 | in |
---|
517 | (fun _ -> |
---|
518 | (let eta2523 = simplify_expr iffalse target_sz target_sg in |
---|
519 | (fun _ -> |
---|
520 | (let { Types.fst = desired_false; Types.snd = iffalse1 } = |
---|
521 | eta2523 |
---|
522 | in |
---|
523 | (fun _ -> |
---|
524 | (match Bool.andb desired_true desired_false with |
---|
525 | | Bool.True -> |
---|
526 | (fun _ -> { Types.fst = Bool.True; Types.snd = |
---|
527 | (Csyntax.Expr ((Csyntax.Econdition (cond1, iftrue1, |
---|
528 | iffalse1)), (Csyntax.Tint (target_sz, target_sg)))) }) |
---|
529 | | Bool.False -> |
---|
530 | (fun _ -> |
---|
531 | (let iftrue10 = simplify_inside iftrue in |
---|
532 | (fun _ -> |
---|
533 | (let iffalse10 = simplify_inside iffalse in |
---|
534 | (fun _ -> { Types.fst = Bool.False; Types.snd = |
---|
535 | (Csyntax.Expr ((Csyntax.Econdition (cond1, |
---|
536 | iftrue10, iffalse10)), ty)) })) __)) __)) __)) __)) |
---|
537 | __)) __)) __ |
---|
538 | | Errors.Error x -> |
---|
539 | (let iftrue1 = simplify_inside iftrue in |
---|
540 | (fun _ -> |
---|
541 | (let iffalse1 = simplify_inside iffalse in |
---|
542 | (fun _ -> { Types.fst = Bool.False; Types.snd = |
---|
543 | (Csyntax.Expr ((Csyntax.Econdition (cond1, iftrue1, |
---|
544 | iffalse1)), ty)) })) __)) __) |
---|
545 | | Errors.Error x -> |
---|
546 | (let iftrue1 = simplify_inside iftrue in |
---|
547 | (fun _ -> |
---|
548 | (let iffalse1 = simplify_inside iffalse in |
---|
549 | (fun _ -> { Types.fst = Bool.False; Types.snd = (Csyntax.Expr |
---|
550 | ((Csyntax.Econdition (cond1, iftrue1, iffalse1)), ty)) })) __)) |
---|
551 | __)) __) |
---|
552 | | Csyntax.Eandbool (lhs, rhs) -> |
---|
553 | (fun _ -> |
---|
554 | (let lhs1 = simplify_inside lhs in |
---|
555 | (fun _ -> |
---|
556 | (let rhs1 = simplify_inside rhs in |
---|
557 | (fun _ -> { Types.fst = Bool.False; Types.snd = (Csyntax.Expr |
---|
558 | ((Csyntax.Eandbool (lhs1, rhs1)), ty)) })) __)) __) |
---|
559 | | Csyntax.Eorbool (lhs, rhs) -> |
---|
560 | (fun _ -> |
---|
561 | (let lhs1 = simplify_inside lhs in |
---|
562 | (fun _ -> |
---|
563 | (let rhs1 = simplify_inside rhs in |
---|
564 | (fun _ -> { Types.fst = Bool.False; Types.snd = (Csyntax.Expr |
---|
565 | ((Csyntax.Eorbool (lhs1, rhs1)), ty)) })) __)) __) |
---|
566 | | Csyntax.Esizeof t -> |
---|
567 | (fun _ -> { Types.fst = |
---|
568 | (TypeComparison.type_eq ty (Csyntax.Tint (target_sz, target_sg))); |
---|
569 | Types.snd = (Csyntax.Expr (ed, ty)) }) |
---|
570 | | Csyntax.Efield (rec_expr, f) -> |
---|
571 | (fun _ -> |
---|
572 | (let rec_expr1 = simplify_inside rec_expr in |
---|
573 | (fun _ -> { Types.fst = Bool.False; Types.snd = (Csyntax.Expr |
---|
574 | ((Csyntax.Efield (rec_expr1, f)), ty)) })) __) |
---|
575 | | Csyntax.Ecost (l, e2) -> |
---|
576 | (fun _ -> |
---|
577 | match TypeComparison.type_eq_dec ty (Csyntax.typeof e2) with |
---|
578 | | Types.Inl _ -> |
---|
579 | (let eta2525 = simplify_expr e2 target_sz target_sg in |
---|
580 | (fun _ -> |
---|
581 | (let { Types.fst = desired_type; Types.snd = e3 } = eta2525 in |
---|
582 | (fun _ -> { Types.fst = desired_type; Types.snd = (Csyntax.Expr |
---|
583 | ((Csyntax.Ecost (l, e3)), (Csyntax.typeof e3))) })) __)) __ |
---|
584 | | Types.Inr _ -> |
---|
585 | (let e3 = simplify_inside e2 in |
---|
586 | (fun _ -> { Types.fst = Bool.False; Types.snd = (Csyntax.Expr |
---|
587 | ((Csyntax.Ecost (l, e3)), ty)) })) __)) __)) __ |
---|
588 | (** val simplify_inside : Csyntax.expr -> Csyntax.expr Types.sig0 **) |
---|
589 | and simplify_inside e1 = |
---|
590 | (let Csyntax.Expr (ed, ty) = e1 in |
---|
591 | (fun _ -> |
---|
592 | (match ed with |
---|
593 | | Csyntax.Econst_int (x, x0) -> (fun _ -> e1) |
---|
594 | | Csyntax.Evar x -> (fun _ -> e1) |
---|
595 | | Csyntax.Ederef e2 -> |
---|
596 | (fun _ -> |
---|
597 | (let e3 = simplify_inside e2 in |
---|
598 | (fun _ -> Csyntax.Expr ((Csyntax.Ederef e3), ty))) __) |
---|
599 | | Csyntax.Eaddrof e2 -> |
---|
600 | (fun _ -> |
---|
601 | (let e3 = simplify_inside e2 in |
---|
602 | (fun _ -> Csyntax.Expr ((Csyntax.Eaddrof e3), ty))) __) |
---|
603 | | Csyntax.Eunop (op0, e2) -> |
---|
604 | (fun _ -> |
---|
605 | (let e3 = simplify_inside e2 in |
---|
606 | (fun _ -> Csyntax.Expr ((Csyntax.Eunop (op0, e3)), ty))) __) |
---|
607 | | Csyntax.Ebinop (op0, lhs, rhs) -> |
---|
608 | (fun _ -> |
---|
609 | (let lhs1 = simplify_inside lhs in |
---|
610 | (fun _ -> |
---|
611 | (let rhs1 = simplify_inside rhs in |
---|
612 | (fun _ -> Csyntax.Expr ((Csyntax.Ebinop (op0, lhs1, rhs1)), ty))) |
---|
613 | __)) __) |
---|
614 | | Csyntax.Ecast (cast_ty, castee) -> |
---|
615 | (fun _ -> |
---|
616 | match TypeComparison.type_eq_dec ty cast_ty with |
---|
617 | | Types.Inl _ -> |
---|
618 | (match cast_ty with |
---|
619 | | Csyntax.Tvoid -> (fun _ -> e1) |
---|
620 | | Csyntax.Tint (cast_sz, cast_sg) -> |
---|
621 | (fun _ -> |
---|
622 | (let eta2526 = simplify_expr castee cast_sz cast_sg in |
---|
623 | (fun _ -> |
---|
624 | (let { Types.fst = success; Types.snd = castee1 } = eta2526 |
---|
625 | in |
---|
626 | (fun _ -> |
---|
627 | (match success with |
---|
628 | | Bool.True -> (fun _ -> castee1) |
---|
629 | | Bool.False -> |
---|
630 | (fun _ -> Csyntax.Expr ((Csyntax.Ecast (cast_ty, |
---|
631 | castee1)), ty))) __)) __)) __) |
---|
632 | | Csyntax.Tpointer x -> (fun _ -> e1) |
---|
633 | | Csyntax.Tarray (x, x0) -> (fun _ -> e1) |
---|
634 | | Csyntax.Tfunction (x, x0) -> (fun _ -> e1) |
---|
635 | | Csyntax.Tstruct (x, x0) -> (fun _ -> e1) |
---|
636 | | Csyntax.Tunion (x, x0) -> (fun _ -> e1) |
---|
637 | | Csyntax.Tcomp_ptr x -> (fun _ -> e1)) __ |
---|
638 | | Types.Inr _ -> e1) |
---|
639 | | Csyntax.Econdition (cond, iftrue, iffalse) -> |
---|
640 | (fun _ -> |
---|
641 | (let cond1 = simplify_inside cond in |
---|
642 | (fun _ -> |
---|
643 | (let iftrue1 = simplify_inside iftrue in |
---|
644 | (fun _ -> |
---|
645 | (let iffalse1 = simplify_inside iffalse in |
---|
646 | (fun _ -> Csyntax.Expr ((Csyntax.Econdition (cond1, iftrue1, |
---|
647 | iffalse1)), ty))) __)) __)) __) |
---|
648 | | Csyntax.Eandbool (lhs, rhs) -> |
---|
649 | (fun _ -> |
---|
650 | (let lhs1 = simplify_inside lhs in |
---|
651 | (fun _ -> |
---|
652 | (let rhs1 = simplify_inside rhs in |
---|
653 | (fun _ -> Csyntax.Expr ((Csyntax.Eandbool (lhs1, rhs1)), ty))) __)) |
---|
654 | __) |
---|
655 | | Csyntax.Eorbool (lhs, rhs) -> |
---|
656 | (fun _ -> |
---|
657 | (let lhs1 = simplify_inside lhs in |
---|
658 | (fun _ -> |
---|
659 | (let rhs1 = simplify_inside rhs in |
---|
660 | (fun _ -> Csyntax.Expr ((Csyntax.Eorbool (lhs1, rhs1)), ty))) __)) |
---|
661 | __) |
---|
662 | | Csyntax.Esizeof x -> (fun _ -> e1) |
---|
663 | | Csyntax.Efield (rec_expr, f) -> |
---|
664 | (fun _ -> |
---|
665 | (let rec_expr1 = simplify_inside rec_expr in |
---|
666 | (fun _ -> Csyntax.Expr ((Csyntax.Efield (rec_expr1, f)), ty))) __) |
---|
667 | | Csyntax.Ecost (l, e2) -> |
---|
668 | (fun _ -> |
---|
669 | (let e3 = simplify_inside e2 in |
---|
670 | (fun _ -> Csyntax.Expr ((Csyntax.Ecost (l, e3)), ty))) __)) __)) __ |
---|
671 | |
---|
672 | (** val simplify_e : Csyntax.expr -> Csyntax.expr **) |
---|
673 | let simplify_e e1 = |
---|
674 | Types.pi1 (simplify_inside e1) |
---|
675 | |
---|
676 | (** val simplify_statement : Csyntax.statement -> Csyntax.statement **) |
---|
677 | let rec simplify_statement = function |
---|
678 | | Csyntax.Sskip -> Csyntax.Sskip |
---|
679 | | Csyntax.Sassign (e1, e2) -> |
---|
680 | Csyntax.Sassign ((simplify_e e1), (simplify_e e2)) |
---|
681 | | Csyntax.Scall (eo, e1, es) -> |
---|
682 | Csyntax.Scall ((Types.option_map simplify_e eo), (simplify_e e1), |
---|
683 | (List.map simplify_e es)) |
---|
684 | | Csyntax.Ssequence (s1, s2) -> |
---|
685 | Csyntax.Ssequence ((simplify_statement s1), (simplify_statement s2)) |
---|
686 | | Csyntax.Sifthenelse (e1, s1, s2) -> |
---|
687 | Csyntax.Sifthenelse ((simplify_e e1), (simplify_statement s1), |
---|
688 | (simplify_statement s2)) |
---|
689 | | Csyntax.Swhile (e1, s1) -> |
---|
690 | Csyntax.Swhile ((simplify_e e1), (simplify_statement s1)) |
---|
691 | | Csyntax.Sdowhile (e1, s1) -> |
---|
692 | Csyntax.Sdowhile ((simplify_e e1), (simplify_statement s1)) |
---|
693 | | Csyntax.Sfor (s1, e1, s2, s3) -> |
---|
694 | Csyntax.Sfor ((simplify_statement s1), (simplify_e e1), |
---|
695 | (simplify_statement s2), (simplify_statement s3)) |
---|
696 | | Csyntax.Sbreak -> Csyntax.Sbreak |
---|
697 | | Csyntax.Scontinue -> Csyntax.Scontinue |
---|
698 | | Csyntax.Sreturn eo -> Csyntax.Sreturn (Types.option_map simplify_e eo) |
---|
699 | | Csyntax.Sswitch (e1, ls) -> |
---|
700 | Csyntax.Sswitch ((simplify_e e1), (simplify_ls ls)) |
---|
701 | | Csyntax.Slabel (l, s1) -> Csyntax.Slabel (l, (simplify_statement s1)) |
---|
702 | | Csyntax.Sgoto l -> Csyntax.Sgoto l |
---|
703 | | Csyntax.Scost (l, s1) -> Csyntax.Scost (l, (simplify_statement s1)) |
---|
704 | (** val simplify_ls : |
---|
705 | Csyntax.labeled_statements -> Csyntax.labeled_statements **) |
---|
706 | and simplify_ls = function |
---|
707 | | Csyntax.LSdefault s -> Csyntax.LSdefault (simplify_statement s) |
---|
708 | | Csyntax.LScase (sz, i, s, ls') -> |
---|
709 | Csyntax.LScase (sz, i, (simplify_statement s), (simplify_ls ls')) |
---|
710 | |
---|
711 | (** val simplify_function : Csyntax.function0 -> Csyntax.function0 **) |
---|
712 | let simplify_function f = |
---|
713 | { Csyntax.fn_return = f.Csyntax.fn_return; Csyntax.fn_params = |
---|
714 | f.Csyntax.fn_params; Csyntax.fn_vars = f.Csyntax.fn_vars; |
---|
715 | Csyntax.fn_body = (simplify_statement f.Csyntax.fn_body) } |
---|
716 | |
---|
717 | (** val simplify_fundef : Csyntax.clight_fundef -> Csyntax.clight_fundef **) |
---|
718 | let simplify_fundef f = match f with |
---|
719 | | Csyntax.CL_Internal f0 -> Csyntax.CL_Internal (simplify_function f0) |
---|
720 | | Csyntax.CL_External (x, x0, x1) -> f |
---|
721 | |
---|
722 | (** val simplify_program : |
---|
723 | Csyntax.clight_program -> Csyntax.clight_program **) |
---|
724 | let simplify_program p = |
---|
725 | AST.transform_program p (fun x -> simplify_fundef) |
---|
726 | |
---|
727 | (** val related_globals_rect_Type6 : |
---|
728 | ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ -> |
---|
729 | __ -> __ -> 'a2) -> 'a2 **) |
---|
730 | let rec related_globals_rect_Type6 t ge0 ge' h_mk_related_globals = |
---|
731 | h_mk_related_globals __ __ __ |
---|
732 | |
---|
733 | (** val related_globals_rect_Type7 : |
---|
734 | ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ -> |
---|
735 | __ -> __ -> 'a2) -> 'a2 **) |
---|
736 | let rec related_globals_rect_Type7 t ge0 ge' h_mk_related_globals = |
---|
737 | h_mk_related_globals __ __ __ |
---|
738 | |
---|
739 | (** val related_globals_rect_Type8 : |
---|
740 | ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ -> |
---|
741 | __ -> __ -> 'a2) -> 'a2 **) |
---|
742 | let rec related_globals_rect_Type8 t ge0 ge' h_mk_related_globals = |
---|
743 | h_mk_related_globals __ __ __ |
---|
744 | |
---|
745 | (** val related_globals_rect_Type9 : |
---|
746 | ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ -> |
---|
747 | __ -> __ -> 'a2) -> 'a2 **) |
---|
748 | let rec related_globals_rect_Type9 t ge0 ge' h_mk_related_globals = |
---|
749 | h_mk_related_globals __ __ __ |
---|
750 | |
---|
751 | (** val related_globals_rect_Type10 : |
---|
752 | ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ -> |
---|
753 | __ -> __ -> 'a2) -> 'a2 **) |
---|
754 | let rec related_globals_rect_Type10 t ge0 ge' h_mk_related_globals = |
---|
755 | h_mk_related_globals __ __ __ |
---|
756 | |
---|
757 | (** val related_globals_rect_Type11 : |
---|
758 | ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ -> |
---|
759 | __ -> __ -> 'a2) -> 'a2 **) |
---|
760 | let rec related_globals_rect_Type11 t ge0 ge' h_mk_related_globals = |
---|
761 | h_mk_related_globals __ __ __ |
---|
762 | |
---|
763 | (** val related_globals_inv_rect_Type5 : |
---|
764 | ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ -> |
---|
765 | __ -> __ -> __ -> 'a2) -> 'a2 **) |
---|
766 | let related_globals_inv_rect_Type5 x2 x3 x4 h1 = |
---|
767 | let hcut = related_globals_rect_Type6 x2 x3 x4 h1 in hcut __ |
---|
768 | |
---|
769 | (** val related_globals_inv_rect_Type6 : |
---|
770 | ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ -> |
---|
771 | __ -> __ -> __ -> 'a2) -> 'a2 **) |
---|
772 | let related_globals_inv_rect_Type6 x2 x3 x4 h1 = |
---|
773 | let hcut = related_globals_rect_Type8 x2 x3 x4 h1 in hcut __ |
---|
774 | |
---|
775 | (** val related_globals_inv_rect_Type7 : |
---|
776 | ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ -> |
---|
777 | __ -> __ -> __ -> 'a2) -> 'a2 **) |
---|
778 | let related_globals_inv_rect_Type7 x2 x3 x4 h1 = |
---|
779 | let hcut = related_globals_rect_Type9 x2 x3 x4 h1 in hcut __ |
---|
780 | |
---|
781 | (** val related_globals_inv_rect_Type8 : |
---|
782 | ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ -> |
---|
783 | __ -> __ -> __ -> 'a2) -> 'a2 **) |
---|
784 | let related_globals_inv_rect_Type8 x2 x3 x4 h1 = |
---|
785 | let hcut = related_globals_rect_Type10 x2 x3 x4 h1 in hcut __ |
---|
786 | |
---|
787 | (** val related_globals_inv_rect_Type9 : |
---|
788 | ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ -> |
---|
789 | __ -> __ -> __ -> 'a2) -> 'a2 **) |
---|
790 | let related_globals_inv_rect_Type9 x2 x3 x4 h1 = |
---|
791 | let hcut = related_globals_rect_Type11 x2 x3 x4 h1 in hcut __ |
---|
792 | |
---|
793 | (** val related_globals_discr0 : |
---|
794 | ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> __ **) |
---|
795 | let related_globals_discr0 a2 a3 a4 = |
---|
796 | Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __)) __ |
---|
797 | |
---|
798 | (** val related_globals_jmdiscr0 : |
---|
799 | ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> __ **) |
---|
800 | let related_globals_jmdiscr0 a2 a3 a4 = |
---|
801 | Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __)) __ |
---|
802 | |
---|