]> matita.cs.unibo.it Git - pkg-cerco/acc-trusted.git/blob - extracted/switchRemoval.ml
Imported Upstream version 0.1
[pkg-cerco/acc-trusted.git] / extracted / switchRemoval.ml
1 open Preamble
2
3 open Deqsets
4
5 open Sets
6
7 open Bool
8
9 open Relations
10
11 open Nat
12
13 open Hints_declaration
14
15 open Core_notation
16
17 open Pts
18
19 open Logic
20
21 open Types
22
23 open List
24
25 open Listb
26
27 open Proper
28
29 open PositiveMap
30
31 open ErrorMessages
32
33 open PreIdentifiers
34
35 open Errors
36
37 open Extralib
38
39 open Setoids
40
41 open Monad
42
43 open Option
44
45 open Div_and_mod
46
47 open Jmeq
48
49 open Russell
50
51 open Util
52
53 open Lists
54
55 open Positive
56
57 open Identifiers
58
59 open CostLabel
60
61 open Coqlib
62
63 open Exp
64
65 open Arithmetic
66
67 open Vector
68
69 open FoldStuff
70
71 open BitVector
72
73 open Extranat
74
75 open Integers
76
77 open AST
78
79 open Csyntax
80
81 open Fresh
82
83 open CexecInd
84
85 open SmallstepExec
86
87 open Cexec
88
89 open IO
90
91 open IOMonad
92
93 open Star
94
95 open ClassifyOp
96
97 open Events
98
99 open Smallstep
100
101 open Extra_bool
102
103 open Values
104
105 open FrontEndVal
106
107 open Hide
108
109 open ByteValues
110
111 open Division
112
113 open Z
114
115 open BitVectorZ
116
117 open Pointers
118
119 open GenMem
120
121 open FrontEndMem
122
123 open Globalenvs
124
125 open Csem
126
127 open TypeComparison
128
129 open Frontend_misc
130
131 open MemProperties
132
133 open MemoryInjections
134
135 (** val convert_break_to_goto :
136     Csyntax.statement -> Csyntax.label -> Csyntax.statement **)
137 let rec convert_break_to_goto st lab =
138   match st with
139   | Csyntax.Sskip -> st
140   | Csyntax.Sassign (x, x0) -> st
141   | Csyntax.Scall (x, x0, x1) -> st
142   | Csyntax.Ssequence (s1, s2) ->
143     Csyntax.Ssequence ((convert_break_to_goto s1 lab),
144       (convert_break_to_goto s2 lab))
145   | Csyntax.Sifthenelse (e, iftrue, iffalse) ->
146     Csyntax.Sifthenelse (e, (convert_break_to_goto iftrue lab),
147       (convert_break_to_goto iffalse lab))
148   | Csyntax.Swhile (x, x0) -> st
149   | Csyntax.Sdowhile (x, x0) -> st
150   | Csyntax.Sfor (init, e, update, body) ->
151     Csyntax.Sfor ((convert_break_to_goto init lab), e, update, body)
152   | Csyntax.Sbreak -> Csyntax.Sgoto lab
153   | Csyntax.Scontinue -> st
154   | Csyntax.Sreturn x -> st
155   | Csyntax.Sswitch (x, x0) -> st
156   | Csyntax.Slabel (l, body) ->
157     Csyntax.Slabel (l, (convert_break_to_goto body lab))
158   | Csyntax.Sgoto x -> st
159   | Csyntax.Scost (cost, body) ->
160     Csyntax.Scost (cost, (convert_break_to_goto body lab))
161
162 (** val produce_cond :
163     Csyntax.expr -> Csyntax.labeled_statements -> Identifiers.universe ->
164     Csyntax.label -> ((Csyntax.statement, Csyntax.label) Types.prod,
165     Identifiers.universe) Types.prod **)
166 let rec produce_cond e switch_cases u exit =
167   match switch_cases with
168   | Csyntax.LSdefault st ->
169     let { Types.fst = lab; Types.snd = u1 } =
170       Identifiers.fresh PreIdentifiers.SymbolTag u
171     in
172     let st' = convert_break_to_goto st exit in
173     { Types.fst = { Types.fst = (Csyntax.Slabel (lab, st')); Types.snd =
174     lab }; Types.snd = u1 }
175   | Csyntax.LScase (sz, tag, st, other_cases) ->
176     let { Types.fst = eta2108; Types.snd = u1 } =
177       produce_cond e other_cases u exit
178     in
179     let { Types.fst = sub_statements; Types.snd = sub_label } = eta2108 in
180     let st' = convert_break_to_goto st exit in
181     let { Types.fst = lab; Types.snd = u2 } =
182       Identifiers.fresh PreIdentifiers.SymbolTag u1
183     in
184     let test = Csyntax.Expr ((Csyntax.Ebinop (Csyntax.Oeq, e, (Csyntax.Expr
185       ((Csyntax.Econst_int (sz, tag)), (Csyntax.typeof e))))), (Csyntax.Tint
186       (AST.I32, AST.Signed)))
187     in
188     let case_statement = Csyntax.Sifthenelse (test, (Csyntax.Slabel (lab,
189       (Csyntax.Ssequence (st', (Csyntax.Sgoto sub_label))))), Csyntax.Sskip)
190     in
191     { Types.fst = { Types.fst = (Csyntax.Ssequence (case_statement,
192     sub_statements)); Types.snd = lab }; Types.snd = u2 }
193
194 (** val simplify_switch :
195     Csyntax.expr -> Csyntax.labeled_statements -> Identifiers.universe ->
196     (Csyntax.statement, Identifiers.universe) Types.prod **)
197 let simplify_switch e switch_cases uv =
198   let { Types.fst = exit_label; Types.snd = uv1 } =
199     Identifiers.fresh PreIdentifiers.SymbolTag uv
200   in
201   let { Types.fst = eta2109; Types.snd = uv2 } =
202     produce_cond e switch_cases uv1 exit_label
203   in
204   let { Types.fst = result; Types.snd = useless_label } = eta2109 in
205   { Types.fst = (Csyntax.Ssequence (result, (Csyntax.Slabel (exit_label,
206   Csyntax.Sskip)))); Types.snd = uv2 }
207
208 (** val switch_removal :
209     Csyntax.statement -> Identifiers.universe -> ((Csyntax.statement,
210     (AST.ident, Csyntax.type0) Types.prod List.list) Types.prod,
211     Identifiers.universe) Types.prod **)
212 let rec switch_removal st u =
213   match st with
214   | Csyntax.Sskip ->
215     { Types.fst = { Types.fst = st; Types.snd = List.Nil }; Types.snd = u }
216   | Csyntax.Sassign (x, x0) ->
217     { Types.fst = { Types.fst = st; Types.snd = List.Nil }; Types.snd = u }
218   | Csyntax.Scall (x, x0, x1) ->
219     { Types.fst = { Types.fst = st; Types.snd = List.Nil }; Types.snd = u }
220   | Csyntax.Ssequence (s1, s2) ->
221     let { Types.fst = eta2123; Types.snd = u' } = switch_removal s1 u in
222     let { Types.fst = s1'; Types.snd = acc1 } = eta2123 in
223     let { Types.fst = eta2122; Types.snd = u'' } = switch_removal s2 u' in
224     let { Types.fst = s2'; Types.snd = acc2 } = eta2122 in
225     { Types.fst = { Types.fst = (Csyntax.Ssequence (s1', s2')); Types.snd =
226     (List.append acc1 acc2) }; Types.snd = u'' }
227   | Csyntax.Sifthenelse (e, s1, s2) ->
228     let { Types.fst = eta2125; Types.snd = u' } = switch_removal s1 u in
229     let { Types.fst = s1'; Types.snd = acc1 } = eta2125 in
230     let { Types.fst = eta2124; Types.snd = u'' } = switch_removal s2 u' in
231     let { Types.fst = s2'; Types.snd = acc2 } = eta2124 in
232     { Types.fst = { Types.fst = (Csyntax.Sifthenelse (e, s1', s2'));
233     Types.snd = (List.append acc1 acc2) }; Types.snd = u'' }
234   | Csyntax.Swhile (e, body) ->
235     let { Types.fst = eta2126; Types.snd = u' } = switch_removal body u in
236     let { Types.fst = body'; Types.snd = acc } = eta2126 in
237     { Types.fst = { Types.fst = (Csyntax.Swhile (e, body')); Types.snd =
238     acc }; Types.snd = u' }
239   | Csyntax.Sdowhile (e, body) ->
240     let { Types.fst = eta2127; Types.snd = u' } = switch_removal body u in
241     let { Types.fst = body'; Types.snd = acc } = eta2127 in
242     { Types.fst = { Types.fst = (Csyntax.Sdowhile (e, body')); Types.snd =
243     acc }; Types.snd = u' }
244   | Csyntax.Sfor (s1, e, s2, s3) ->
245     let { Types.fst = eta2130; Types.snd = u' } = switch_removal s1 u in
246     let { Types.fst = s1'; Types.snd = acc1 } = eta2130 in
247     let { Types.fst = eta2129; Types.snd = u'' } = switch_removal s2 u' in
248     let { Types.fst = s2'; Types.snd = acc2 } = eta2129 in
249     let { Types.fst = eta2128; Types.snd = u''' } = switch_removal s3 u'' in
250     let { Types.fst = s3'; Types.snd = acc3 } = eta2128 in
251     { Types.fst = { Types.fst = (Csyntax.Sfor (s1', e, s2', s3'));
252     Types.snd = (List.append acc1 (List.append acc2 acc3)) }; Types.snd =
253     u''' }
254   | Csyntax.Sbreak ->
255     { Types.fst = { Types.fst = st; Types.snd = List.Nil }; Types.snd = u }
256   | Csyntax.Scontinue ->
257     { Types.fst = { Types.fst = st; Types.snd = List.Nil }; Types.snd = u }
258   | Csyntax.Sreturn x ->
259     { Types.fst = { Types.fst = st; Types.snd = List.Nil }; Types.snd = u }
260   | Csyntax.Sswitch (e, branches) ->
261     let { Types.fst = eta2131; Types.snd = u' } =
262       switch_removal_branches branches u
263     in
264     let { Types.fst = sf_branches; Types.snd = acc } = eta2131 in
265     let { Types.fst = switch_tmp; Types.snd = u'' } =
266       Identifiers.fresh PreIdentifiers.SymbolTag u'
267     in
268     let ident = Csyntax.Expr ((Csyntax.Evar switch_tmp), (Csyntax.typeof e))
269     in
270     let assign = Csyntax.Sassign (ident, e) in
271     let { Types.fst = result; Types.snd = u''' } =
272       simplify_switch ident sf_branches u''
273     in
274     { Types.fst = { Types.fst = (Csyntax.Ssequence (assign, result));
275     Types.snd = (List.Cons ({ Types.fst = switch_tmp; Types.snd =
276     (Csyntax.typeof e) }, acc)) }; Types.snd = u''' }
277   | Csyntax.Slabel (label, body) ->
278     let { Types.fst = eta2132; Types.snd = u' } = switch_removal body u in
279     let { Types.fst = body'; Types.snd = acc } = eta2132 in
280     { Types.fst = { Types.fst = (Csyntax.Slabel (label, body')); Types.snd =
281     acc }; Types.snd = u' }
282   | Csyntax.Sgoto x ->
283     { Types.fst = { Types.fst = st; Types.snd = List.Nil }; Types.snd = u }
284   | Csyntax.Scost (cost, body) ->
285     let { Types.fst = eta2133; Types.snd = u' } = switch_removal body u in
286     let { Types.fst = body'; Types.snd = acc } = eta2133 in
287     { Types.fst = { Types.fst = (Csyntax.Scost (cost, body')); Types.snd =
288     acc }; Types.snd = u' }
289 (** val switch_removal_branches :
290     Csyntax.labeled_statements -> Identifiers.universe ->
291     ((Csyntax.labeled_statements, (AST.ident, Csyntax.type0) Types.prod
292     List.list) Types.prod, Identifiers.universe) Types.prod **)
293 and switch_removal_branches l u =
294   match l with
295   | Csyntax.LSdefault st ->
296     let { Types.fst = eta2134; Types.snd = u' } = switch_removal st u in
297     let { Types.fst = st'; Types.snd = acc1 } = eta2134 in
298     { Types.fst = { Types.fst = (Csyntax.LSdefault st'); Types.snd = acc1 };
299     Types.snd = u' }
300   | Csyntax.LScase (sz, int, st, tl) ->
301     let { Types.fst = eta2136; Types.snd = u' } =
302       switch_removal_branches tl u
303     in
304     let { Types.fst = tl_result; Types.snd = acc1 } = eta2136 in
305     let { Types.fst = eta2135; Types.snd = u'' } = switch_removal st u' in
306     let { Types.fst = st'; Types.snd = acc2 } = eta2135 in
307     { Types.fst = { Types.fst = (Csyntax.LScase (sz, int, st', tl_result));
308     Types.snd = (List.append acc1 acc2) }; Types.snd = u'' }
309
310 (** val ret_st :
311     (('a1, (AST.ident, Csyntax.type0) Types.prod List.list) Types.prod,
312     Identifiers.universe) Types.prod -> 'a1 **)
313 let ret_st x =
314   let { Types.fst = eta2137; Types.snd = u } = x in eta2137.Types.fst
315
316 (** val ret_vars :
317     (('a1, (AST.ident, Csyntax.type0) Types.prod List.list) Types.prod,
318     Identifiers.universe) Types.prod -> (AST.ident, Csyntax.type0) Types.prod
319     List.list **)
320 let ret_vars x =
321   let { Types.fst = eta2138; Types.snd = u } = x in eta2138.Types.snd
322
323 (** val ret_u :
324     (('a1, (AST.ident, Csyntax.type0) Types.prod List.list) Types.prod,
325     Identifiers.universe) Types.prod -> Identifiers.universe **)
326 let ret_u x =
327   let { Types.fst = eta2139; Types.snd = u } = x in
328   let { Types.fst = s; Types.snd = vars } = eta2139 in u
329
330 (** val least_identifier : PreIdentifiers.identifier **)
331 let least_identifier =
332   Positive.One
333
334 (** val max_of_expr : Csyntax.expr -> AST.ident **)
335 let rec max_of_expr = function
336 | Csyntax.Expr (ed, x) ->
337   (match ed with
338    | Csyntax.Econst_int (x0, x1) -> least_identifier
339    | Csyntax.Evar id -> id
340    | Csyntax.Ederef e1 -> max_of_expr e1
341    | Csyntax.Eaddrof e1 -> max_of_expr e1
342    | Csyntax.Eunop (x0, e1) -> max_of_expr e1
343    | Csyntax.Ebinop (x0, e1, e2) ->
344      Fresh.max_id (max_of_expr e1) (max_of_expr e2)
345    | Csyntax.Ecast (x0, e1) -> max_of_expr e1
346    | Csyntax.Econdition (e1, e2, e3) ->
347      Fresh.max_id (max_of_expr e1)
348        (Fresh.max_id (max_of_expr e2) (max_of_expr e3))
349    | Csyntax.Eandbool (e1, e2) ->
350      Fresh.max_id (max_of_expr e1) (max_of_expr e2)
351    | Csyntax.Eorbool (e1, e2) ->
352      Fresh.max_id (max_of_expr e1) (max_of_expr e2)
353    | Csyntax.Esizeof x0 -> least_identifier
354    | Csyntax.Efield (r, f) -> Fresh.max_id f (max_of_expr r)
355    | Csyntax.Ecost (x0, e1) -> max_of_expr e1)
356
357 (** val max_of_statement : Csyntax.statement -> AST.ident **)
358 let rec max_of_statement = function
359 | Csyntax.Sskip -> least_identifier
360 | Csyntax.Sassign (e1, e2) -> Fresh.max_id (max_of_expr e1) (max_of_expr e2)
361 | Csyntax.Scall (r, f, args) ->
362   let retmax =
363     match r with
364     | Types.None -> least_identifier
365     | Types.Some e -> max_of_expr e
366   in
367   Fresh.max_id (max_of_expr f)
368     (Fresh.max_id retmax
369       (List.foldr (fun elt acc -> Fresh.max_id (max_of_expr elt) acc)
370         least_identifier args))
371 | Csyntax.Ssequence (s1, s2) ->
372   Fresh.max_id (max_of_statement s1) (max_of_statement s2)
373 | Csyntax.Sifthenelse (e, s1, s2) ->
374   Fresh.max_id (max_of_expr e)
375     (Fresh.max_id (max_of_statement s1) (max_of_statement s2))
376 | Csyntax.Swhile (e, body) ->
377   Fresh.max_id (max_of_expr e) (max_of_statement body)
378 | Csyntax.Sdowhile (e, body) ->
379   Fresh.max_id (max_of_expr e) (max_of_statement body)
380 | Csyntax.Sfor (init, test, incr, body) ->
381   Fresh.max_id (Fresh.max_id (max_of_statement init) (max_of_expr test))
382     (Fresh.max_id (max_of_statement incr) (max_of_statement body))
383 | Csyntax.Sbreak -> least_identifier
384 | Csyntax.Scontinue -> least_identifier
385 | Csyntax.Sreturn opt ->
386   (match opt with
387    | Types.None -> least_identifier
388    | Types.Some e -> max_of_expr e)
389 | Csyntax.Sswitch (e, ls) -> Fresh.max_id (max_of_expr e) (max_of_ls ls)
390 | Csyntax.Slabel (lab, body) -> Fresh.max_id lab (max_of_statement body)
391 | Csyntax.Sgoto lab -> lab
392 | Csyntax.Scost (x, body) -> max_of_statement body
393 (** val max_of_ls : Csyntax.labeled_statements -> AST.ident **)
394 and max_of_ls = function
395 | Csyntax.LSdefault s -> max_of_statement s
396 | Csyntax.LScase (x, x0, s, ls') ->
397   Fresh.max_id (max_of_ls ls') (max_of_statement s)
398
399 (** val max_id_of_function : Csyntax.function0 -> AST.ident **)
400 let max_id_of_function f =
401   Fresh.max_id (max_of_statement f.Csyntax.fn_body) (Fresh.max_id_of_fn f)
402
403 (** val function_switch_removal :
404     Csyntax.function0 -> (Csyntax.function0, (AST.ident, Csyntax.type0)
405     Types.prod List.list) Types.prod **)
406 let function_switch_removal f =
407   let u = Fresh.universe_of_max (max_id_of_function f) in
408   let { Types.fst = eta2140; Types.snd = u' } =
409     switch_removal f.Csyntax.fn_body u
410   in
411   let { Types.fst = st; Types.snd = vars } = eta2140 in
412   let result = { Csyntax.fn_return = f.Csyntax.fn_return; Csyntax.fn_params =
413     f.Csyntax.fn_params; Csyntax.fn_vars =
414     (List.append vars f.Csyntax.fn_vars); Csyntax.fn_body = st }
415   in
416   { Types.fst = result; Types.snd = vars }
417
418 (** val fundef_switch_removal :
419     Csyntax.clight_fundef -> Csyntax.clight_fundef **)
420 let rec fundef_switch_removal f = match f with
421 | Csyntax.CL_Internal f0 ->
422   Csyntax.CL_Internal (function_switch_removal f0).Types.fst
423 | Csyntax.CL_External (x, x0, x1) -> f
424
425 (** val program_switch_removal :
426     Csyntax.clight_program -> Csyntax.clight_program **)
427 let rec program_switch_removal p =
428   AST.transform_program p (fun x -> fundef_switch_removal)
429
430 (** val nonempty_block_rect_Type4 :
431     GenMem.mem -> Pointers.block -> (__ -> __ -> 'a1) -> 'a1 **)
432 let rec nonempty_block_rect_Type4 m b h_mk_nonempty_block =
433   h_mk_nonempty_block __ __
434
435 (** val nonempty_block_rect_Type5 :
436     GenMem.mem -> Pointers.block -> (__ -> __ -> 'a1) -> 'a1 **)
437 let rec nonempty_block_rect_Type5 m b h_mk_nonempty_block =
438   h_mk_nonempty_block __ __
439
440 (** val nonempty_block_rect_Type3 :
441     GenMem.mem -> Pointers.block -> (__ -> __ -> 'a1) -> 'a1 **)
442 let rec nonempty_block_rect_Type3 m b h_mk_nonempty_block =
443   h_mk_nonempty_block __ __
444
445 (** val nonempty_block_rect_Type2 :
446     GenMem.mem -> Pointers.block -> (__ -> __ -> 'a1) -> 'a1 **)
447 let rec nonempty_block_rect_Type2 m b h_mk_nonempty_block =
448   h_mk_nonempty_block __ __
449
450 (** val nonempty_block_rect_Type1 :
451     GenMem.mem -> Pointers.block -> (__ -> __ -> 'a1) -> 'a1 **)
452 let rec nonempty_block_rect_Type1 m b h_mk_nonempty_block =
453   h_mk_nonempty_block __ __
454
455 (** val nonempty_block_rect_Type0 :
456     GenMem.mem -> Pointers.block -> (__ -> __ -> 'a1) -> 'a1 **)
457 let rec nonempty_block_rect_Type0 m b h_mk_nonempty_block =
458   h_mk_nonempty_block __ __
459
460 (** val nonempty_block_inv_rect_Type4 :
461     GenMem.mem -> Pointers.block -> (__ -> __ -> __ -> 'a1) -> 'a1 **)
462 let nonempty_block_inv_rect_Type4 x1 x2 h1 =
463   let hcut = nonempty_block_rect_Type4 x1 x2 h1 in hcut __
464
465 (** val nonempty_block_inv_rect_Type3 :
466     GenMem.mem -> Pointers.block -> (__ -> __ -> __ -> 'a1) -> 'a1 **)
467 let nonempty_block_inv_rect_Type3 x1 x2 h1 =
468   let hcut = nonempty_block_rect_Type3 x1 x2 h1 in hcut __
469
470 (** val nonempty_block_inv_rect_Type2 :
471     GenMem.mem -> Pointers.block -> (__ -> __ -> __ -> 'a1) -> 'a1 **)
472 let nonempty_block_inv_rect_Type2 x1 x2 h1 =
473   let hcut = nonempty_block_rect_Type2 x1 x2 h1 in hcut __
474
475 (** val nonempty_block_inv_rect_Type1 :
476     GenMem.mem -> Pointers.block -> (__ -> __ -> __ -> 'a1) -> 'a1 **)
477 let nonempty_block_inv_rect_Type1 x1 x2 h1 =
478   let hcut = nonempty_block_rect_Type1 x1 x2 h1 in hcut __
479
480 (** val nonempty_block_inv_rect_Type0 :
481     GenMem.mem -> Pointers.block -> (__ -> __ -> __ -> 'a1) -> 'a1 **)
482 let nonempty_block_inv_rect_Type0 x1 x2 h1 =
483   let hcut = nonempty_block_rect_Type0 x1 x2 h1 in hcut __
484
485 (** val nonempty_block_discr : GenMem.mem -> Pointers.block -> __ **)
486 let nonempty_block_discr a1 a2 =
487   Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __)) __
488
489 (** val nonempty_block_jmdiscr : GenMem.mem -> Pointers.block -> __ **)
490 let nonempty_block_jmdiscr a1 a2 =
491   Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __)) __
492
493 (** val sr_memext_rect_Type4 :
494     GenMem.mem -> GenMem.mem -> Pointers.block List.list -> (__ -> __ -> __
495     -> 'a1) -> 'a1 **)
496 let rec sr_memext_rect_Type4 m1 m2 writeable h_mk_sr_memext =
497   h_mk_sr_memext __ __ __
498
499 (** val sr_memext_rect_Type5 :
500     GenMem.mem -> GenMem.mem -> Pointers.block List.list -> (__ -> __ -> __
501     -> 'a1) -> 'a1 **)
502 let rec sr_memext_rect_Type5 m1 m2 writeable h_mk_sr_memext =
503   h_mk_sr_memext __ __ __
504
505 (** val sr_memext_rect_Type3 :
506     GenMem.mem -> GenMem.mem -> Pointers.block List.list -> (__ -> __ -> __
507     -> 'a1) -> 'a1 **)
508 let rec sr_memext_rect_Type3 m1 m2 writeable h_mk_sr_memext =
509   h_mk_sr_memext __ __ __
510
511 (** val sr_memext_rect_Type2 :
512     GenMem.mem -> GenMem.mem -> Pointers.block List.list -> (__ -> __ -> __
513     -> 'a1) -> 'a1 **)
514 let rec sr_memext_rect_Type2 m1 m2 writeable h_mk_sr_memext =
515   h_mk_sr_memext __ __ __
516
517 (** val sr_memext_rect_Type1 :
518     GenMem.mem -> GenMem.mem -> Pointers.block List.list -> (__ -> __ -> __
519     -> 'a1) -> 'a1 **)
520 let rec sr_memext_rect_Type1 m1 m2 writeable h_mk_sr_memext =
521   h_mk_sr_memext __ __ __
522
523 (** val sr_memext_rect_Type0 :
524     GenMem.mem -> GenMem.mem -> Pointers.block List.list -> (__ -> __ -> __
525     -> 'a1) -> 'a1 **)
526 let rec sr_memext_rect_Type0 m1 m2 writeable h_mk_sr_memext =
527   h_mk_sr_memext __ __ __
528
529 (** val sr_memext_inv_rect_Type4 :
530     GenMem.mem -> GenMem.mem -> Pointers.block List.list -> (__ -> __ -> __
531     -> __ -> 'a1) -> 'a1 **)
532 let sr_memext_inv_rect_Type4 x1 x2 x3 h1 =
533   let hcut = sr_memext_rect_Type4 x1 x2 x3 h1 in hcut __
534
535 (** val sr_memext_inv_rect_Type3 :
536     GenMem.mem -> GenMem.mem -> Pointers.block List.list -> (__ -> __ -> __
537     -> __ -> 'a1) -> 'a1 **)
538 let sr_memext_inv_rect_Type3 x1 x2 x3 h1 =
539   let hcut = sr_memext_rect_Type3 x1 x2 x3 h1 in hcut __
540
541 (** val sr_memext_inv_rect_Type2 :
542     GenMem.mem -> GenMem.mem -> Pointers.block List.list -> (__ -> __ -> __
543     -> __ -> 'a1) -> 'a1 **)
544 let sr_memext_inv_rect_Type2 x1 x2 x3 h1 =
545   let hcut = sr_memext_rect_Type2 x1 x2 x3 h1 in hcut __
546
547 (** val sr_memext_inv_rect_Type1 :
548     GenMem.mem -> GenMem.mem -> Pointers.block List.list -> (__ -> __ -> __
549     -> __ -> 'a1) -> 'a1 **)
550 let sr_memext_inv_rect_Type1 x1 x2 x3 h1 =
551   let hcut = sr_memext_rect_Type1 x1 x2 x3 h1 in hcut __
552
553 (** val sr_memext_inv_rect_Type0 :
554     GenMem.mem -> GenMem.mem -> Pointers.block List.list -> (__ -> __ -> __
555     -> __ -> 'a1) -> 'a1 **)
556 let sr_memext_inv_rect_Type0 x1 x2 x3 h1 =
557   let hcut = sr_memext_rect_Type0 x1 x2 x3 h1 in hcut __
558
559 (** val sr_memext_discr :
560     GenMem.mem -> GenMem.mem -> Pointers.block List.list -> __ **)
561 let sr_memext_discr a1 a2 a3 =
562   Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __)) __
563
564 (** val sr_memext_jmdiscr :
565     GenMem.mem -> GenMem.mem -> Pointers.block List.list -> __ **)
566 let sr_memext_jmdiscr a1 a2 a3 =
567   Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __)) __
568
569 (** val env_codomain :
570     Csem.env -> (AST.ident, Csyntax.type0) Types.prod List.list ->
571     Pointers.block Frontend_misc.lset **)
572 let env_codomain e l =
573   Identifiers.foldi PreIdentifiers.SymbolTag (fun id block acc ->
574     match Frontend_misc.mem_assoc_env id l with
575     | Bool.True -> List.Cons (block, acc)
576     | Bool.False -> acc) e List.Nil
577