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 = eta2130; Types.snd = u1 } =
 177       produce_cond e other_cases u exit
 178     in
 179     let { Types.fst = sub_statements; Types.snd = sub_label } = eta2130 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 = eta2131; Types.snd = uv2 } =
 202     produce_cond e switch_cases uv1 exit_label
 203   in
 204   let { Types.fst = result; Types.snd = useless_label } = eta2131 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 = eta2145; Types.snd = u' } = switch_removal s1 u in
 222     let { Types.fst = s1'; Types.snd = acc1 } = eta2145 in
 223     let { Types.fst = eta2144; Types.snd = u'' } = switch_removal s2 u' in
 224     let { Types.fst = s2'; Types.snd = acc2 } = eta2144 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 = eta2147; Types.snd = u' } = switch_removal s1 u in
 229     let { Types.fst = s1'; Types.snd = acc1 } = eta2147 in
 230     let { Types.fst = eta2146; Types.snd = u'' } = switch_removal s2 u' in
 231     let { Types.fst = s2'; Types.snd = acc2 } = eta2146 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 = eta2148; Types.snd = u' } = switch_removal body u in
 236     let { Types.fst = body'; Types.snd = acc } = eta2148 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 = eta2149; Types.snd = u' } = switch_removal body u in
 241     let { Types.fst = body'; Types.snd = acc } = eta2149 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 = eta2152; Types.snd = u' } = switch_removal s1 u in
 246     let { Types.fst = s1'; Types.snd = acc1 } = eta2152 in
 247     let { Types.fst = eta2151; Types.snd = u'' } = switch_removal s2 u' in
 248     let { Types.fst = s2'; Types.snd = acc2 } = eta2151 in
 249     let { Types.fst = eta2150; Types.snd = u''' } = switch_removal s3 u'' in
 250     let { Types.fst = s3'; Types.snd = acc3 } = eta2150 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 = eta2153; Types.snd = u' } =
 262       switch_removal_branches branches u
 263     in
 264     let { Types.fst = sf_branches; Types.snd = acc } = eta2153 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 = eta2154; Types.snd = u' } = switch_removal body u in
 279     let { Types.fst = body'; Types.snd = acc } = eta2154 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 = eta2155; Types.snd = u' } = switch_removal body u in
 286     let { Types.fst = body'; Types.snd = acc } = eta2155 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 = eta2156; Types.snd = u' } = switch_removal st u in
 297     let { Types.fst = st'; Types.snd = acc1 } = eta2156 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 = eta2158; Types.snd = u' } =
 302       switch_removal_branches tl u
 303     in
 304     let { Types.fst = tl_result; Types.snd = acc1 } = eta2158 in
 305     let { Types.fst = eta2157; Types.snd = u'' } = switch_removal st u' in
 306     let { Types.fst = st'; Types.snd = acc2 } = eta2157 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 = eta2159; Types.snd = u } = x in eta2159.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 = eta2160; Types.snd = u } = x in eta2160.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 = eta2161; Types.snd = u } = x in
 328   let { Types.fst = s; Types.snd = vars } = eta2161 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 = eta2162; Types.snd = u' } =
 409     switch_removal f.Csyntax.fn_body u
 410   in
 411   let { Types.fst = st; Types.snd = vars } = eta2162 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