extracted/compiler.ml

   1 open Preamble
   2
   3 open CostLabel
   4
   5 open Coqlib
   6
   7 open Proper
   8
   9 open PositiveMap
  10
  11 open Deqsets
  12
  13 open ErrorMessages
  14
  15 open PreIdentifiers
  16
  17 open Errors
  18
  19 open Extralib
  20
  21 open Lists
  22
  23 open Positive
  24
  25 open Identifiers
  26
  27 open Exp
  28
  29 open Arithmetic
  30
  31 open Vector
  32
  33 open Div_and_mod
  34
  35 open Util
  36
  37 open FoldStuff
  38
  39 open BitVector
  40
  41 open Jmeq
  42
  43 open Russell
  44
  45 open List
  46
  47 open Setoids
  48
  49 open Monad
  50
  51 open Option
  52
  53 open Extranat
  54
  55 open Bool
  56
  57 open Relations
  58
  59 open Nat
  60
  61 open Integers
  62
  63 open Hints_declaration
  64
  65 open Core_notation
  66
  67 open Pts
  68
  69 open Logic
  70
  71 open Types
  72
  73 open AST
  74
  75 open Csyntax
  76
  77 open Label
  78
  79 open Sets
  80
  81 open Listb
  82
  83 open Star
  84
  85 open Frontend_misc
  86
  87 open CexecInd
  88
  89 open Casts
  90
  91 open ClassifyOp
  92
  93 open Smallstep
  94
  95 open Extra_bool
  96
  97 open FrontEndVal
  98
  99 open Hide
 100
 101 open ByteValues
 102
 103 open GenMem
 104
 105 open FrontEndMem
 106
 107 open Globalenvs
 108
 109 open Csem
 110
 111 open SmallstepExec
 112
 113 open Division
 114
 115 open Z
 116
 117 open BitVectorZ
 118
 119 open Pointers
 120
 121 open Values
 122
 123 open Events
 124
 125 open IOMonad
 126
 127 open IO
 128
 129 open Cexec
 130
 131 open TypeComparison
 132
 133 open SimplifyCasts
 134
 135 open MemProperties
 136
 137 open MemoryInjections
 138
 139 open Fresh
 140
 141 open SwitchRemoval
 142
 143 open FrontEndOps
 144
 145 open Cminor_syntax
 146
 147 open ToCminor
 148
 149 open BitVectorTrie
 150
 151 open Graphs
 152
 153 open Order
 154
 155 open Registers
 156
 157 open RTLabs_syntax
 158
 159 open ToRTLabs
 160
 161 open Deqsets_extra
 162
 163 open CostMisc
 164
 165 open Listb_extra
 166
 167 open CostSpec
 168
 169 open CostCheck
 170
 171 open CostInj
 172
 173 open State
 174
 175 open Bind_new
 176
 177 open BindLists
 178
 179 open Blocks
 180
 181 open TranslateUtils
 182
 183 open String
 184
 185 open LabelledObjects
 186
 187 open I8051
 188
 189 open BackEndOps
 190
 191 open Joint
 192
 193 open RTL
 194
 195 open RTLabsToRTL
 196
 197 open ERTL
 198
 199 open RegisterSet
 200
 201 open RTLToERTL
 202
 203 open Fixpoints
 204
 205 open Set_adt
 206
 207 open Liveness
 208
 209 open Interference
 210
 211 open Joint_LTL_LIN
 212
 213 open LTL
 214
 215 open ERTLToLTL
 216
 217 open LIN
 218
 219 open Linearise
 220
 221 open LTLToLIN
 222
 223 open ASM
 224
 225 open BitVectorTrieSet
 226
 227 open LINToASM
 228
 229 type pass =
 230 | Clight_pass
 231 | Clight_switch_removed_pass
 232 | Clight_label_pass
 233 | Clight_simplified_pass
 234 | Cminor_pass
 235 | Rtlabs_pass
 236 | Rtl_separate_pass
 237 | Rtl_uniq_pass
 238 | Ertl_pass
 239 | Ltl_pass
 240 | Lin_pass
 241 | Assembly_pass
 242 | Object_code_pass
 243
 244 (** val pass_rect_Type4 :
 245     'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
 246     -> 'a1 -> 'a1 -> pass -> 'a1 **)
 247 let rec pass_rect_Type4 h_clight_pass h_clight_switch_removed_pass h_clight_label_pass h_clight_simplified_pass h_cminor_pass h_rtlabs_pass h_rtl_separate_pass h_rtl_uniq_pass h_ertl_pass h_ltl_pass h_lin_pass h_assembly_pass h_object_code_pass = function
 248 | Clight_pass -> h_clight_pass
 249 | Clight_switch_removed_pass -> h_clight_switch_removed_pass
 250 | Clight_label_pass -> h_clight_label_pass
 251 | Clight_simplified_pass -> h_clight_simplified_pass
 252 | Cminor_pass -> h_cminor_pass
 253 | Rtlabs_pass -> h_rtlabs_pass
 254 | Rtl_separate_pass -> h_rtl_separate_pass
 255 | Rtl_uniq_pass -> h_rtl_uniq_pass
 256 | Ertl_pass -> h_ertl_pass
 257 | Ltl_pass -> h_ltl_pass
 258 | Lin_pass -> h_lin_pass
 259 | Assembly_pass -> h_assembly_pass
 260 | Object_code_pass -> h_object_code_pass
 261
 262 (** val pass_rect_Type5 :
 263     'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
 264     -> 'a1 -> 'a1 -> pass -> 'a1 **)
 265 let rec pass_rect_Type5 h_clight_pass h_clight_switch_removed_pass h_clight_label_pass h_clight_simplified_pass h_cminor_pass h_rtlabs_pass h_rtl_separate_pass h_rtl_uniq_pass h_ertl_pass h_ltl_pass h_lin_pass h_assembly_pass h_object_code_pass = function
 266 | Clight_pass -> h_clight_pass
 267 | Clight_switch_removed_pass -> h_clight_switch_removed_pass
 268 | Clight_label_pass -> h_clight_label_pass
 269 | Clight_simplified_pass -> h_clight_simplified_pass
 270 | Cminor_pass -> h_cminor_pass
 271 | Rtlabs_pass -> h_rtlabs_pass
 272 | Rtl_separate_pass -> h_rtl_separate_pass
 273 | Rtl_uniq_pass -> h_rtl_uniq_pass
 274 | Ertl_pass -> h_ertl_pass
 275 | Ltl_pass -> h_ltl_pass
 276 | Lin_pass -> h_lin_pass
 277 | Assembly_pass -> h_assembly_pass
 278 | Object_code_pass -> h_object_code_pass
 279
 280 (** val pass_rect_Type3 :
 281     'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
 282     -> 'a1 -> 'a1 -> pass -> 'a1 **)
 283 let rec pass_rect_Type3 h_clight_pass h_clight_switch_removed_pass h_clight_label_pass h_clight_simplified_pass h_cminor_pass h_rtlabs_pass h_rtl_separate_pass h_rtl_uniq_pass h_ertl_pass h_ltl_pass h_lin_pass h_assembly_pass h_object_code_pass = function
 284 | Clight_pass -> h_clight_pass
 285 | Clight_switch_removed_pass -> h_clight_switch_removed_pass
 286 | Clight_label_pass -> h_clight_label_pass
 287 | Clight_simplified_pass -> h_clight_simplified_pass
 288 | Cminor_pass -> h_cminor_pass
 289 | Rtlabs_pass -> h_rtlabs_pass
 290 | Rtl_separate_pass -> h_rtl_separate_pass
 291 | Rtl_uniq_pass -> h_rtl_uniq_pass
 292 | Ertl_pass -> h_ertl_pass
 293 | Ltl_pass -> h_ltl_pass
 294 | Lin_pass -> h_lin_pass
 295 | Assembly_pass -> h_assembly_pass
 296 | Object_code_pass -> h_object_code_pass
 297
 298 (** val pass_rect_Type2 :
 299     'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
 300     -> 'a1 -> 'a1 -> pass -> 'a1 **)
 301 let rec pass_rect_Type2 h_clight_pass h_clight_switch_removed_pass h_clight_label_pass h_clight_simplified_pass h_cminor_pass h_rtlabs_pass h_rtl_separate_pass h_rtl_uniq_pass h_ertl_pass h_ltl_pass h_lin_pass h_assembly_pass h_object_code_pass = function
 302 | Clight_pass -> h_clight_pass
 303 | Clight_switch_removed_pass -> h_clight_switch_removed_pass
 304 | Clight_label_pass -> h_clight_label_pass
 305 | Clight_simplified_pass -> h_clight_simplified_pass
 306 | Cminor_pass -> h_cminor_pass
 307 | Rtlabs_pass -> h_rtlabs_pass
 308 | Rtl_separate_pass -> h_rtl_separate_pass
 309 | Rtl_uniq_pass -> h_rtl_uniq_pass
 310 | Ertl_pass -> h_ertl_pass
 311 | Ltl_pass -> h_ltl_pass
 312 | Lin_pass -> h_lin_pass
 313 | Assembly_pass -> h_assembly_pass
 314 | Object_code_pass -> h_object_code_pass
 315
 316 (** val pass_rect_Type1 :
 317     'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
 318     -> 'a1 -> 'a1 -> pass -> 'a1 **)
 319 let rec pass_rect_Type1 h_clight_pass h_clight_switch_removed_pass h_clight_label_pass h_clight_simplified_pass h_cminor_pass h_rtlabs_pass h_rtl_separate_pass h_rtl_uniq_pass h_ertl_pass h_ltl_pass h_lin_pass h_assembly_pass h_object_code_pass = function
 320 | Clight_pass -> h_clight_pass
 321 | Clight_switch_removed_pass -> h_clight_switch_removed_pass
 322 | Clight_label_pass -> h_clight_label_pass
 323 | Clight_simplified_pass -> h_clight_simplified_pass
 324 | Cminor_pass -> h_cminor_pass
 325 | Rtlabs_pass -> h_rtlabs_pass
 326 | Rtl_separate_pass -> h_rtl_separate_pass
 327 | Rtl_uniq_pass -> h_rtl_uniq_pass
 328 | Ertl_pass -> h_ertl_pass
 329 | Ltl_pass -> h_ltl_pass
 330 | Lin_pass -> h_lin_pass
 331 | Assembly_pass -> h_assembly_pass
 332 | Object_code_pass -> h_object_code_pass
 333
 334 (** val pass_rect_Type0 :
 335     'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
 336     -> 'a1 -> 'a1 -> pass -> 'a1 **)
 337 let rec pass_rect_Type0 h_clight_pass h_clight_switch_removed_pass h_clight_label_pass h_clight_simplified_pass h_cminor_pass h_rtlabs_pass h_rtl_separate_pass h_rtl_uniq_pass h_ertl_pass h_ltl_pass h_lin_pass h_assembly_pass h_object_code_pass = function
 338 | Clight_pass -> h_clight_pass
 339 | Clight_switch_removed_pass -> h_clight_switch_removed_pass
 340 | Clight_label_pass -> h_clight_label_pass
 341 | Clight_simplified_pass -> h_clight_simplified_pass
 342 | Cminor_pass -> h_cminor_pass
 343 | Rtlabs_pass -> h_rtlabs_pass
 344 | Rtl_separate_pass -> h_rtl_separate_pass
 345 | Rtl_uniq_pass -> h_rtl_uniq_pass
 346 | Ertl_pass -> h_ertl_pass
 347 | Ltl_pass -> h_ltl_pass
 348 | Lin_pass -> h_lin_pass
 349 | Assembly_pass -> h_assembly_pass
 350 | Object_code_pass -> h_object_code_pass
 351
 352 (** val pass_inv_rect_Type4 :
 353     pass -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
 354     -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
 355     (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
 356 let pass_inv_rect_Type4 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 =
 357   let hcut = pass_rect_Type4 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 hterm
 358   in
 359   hcut __
 360
 361 (** val pass_inv_rect_Type3 :
 362     pass -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
 363     -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
 364     (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
 365 let pass_inv_rect_Type3 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 =
 366   let hcut = pass_rect_Type3 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 hterm
 367   in
 368   hcut __
 369
 370 (** val pass_inv_rect_Type2 :
 371     pass -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
 372     -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
 373     (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
 374 let pass_inv_rect_Type2 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 =
 375   let hcut = pass_rect_Type2 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 hterm
 376   in
 377   hcut __
 378
 379 (** val pass_inv_rect_Type1 :
 380     pass -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
 381     -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
 382     (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
 383 let pass_inv_rect_Type1 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 =
 384   let hcut = pass_rect_Type1 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 hterm
 385   in
 386   hcut __
 387
 388 (** val pass_inv_rect_Type0 :
 389     pass -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
 390     -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
 391     (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
 392 let pass_inv_rect_Type0 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 =
 393   let hcut = pass_rect_Type0 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 hterm
 394   in
 395   hcut __
 396
 397 (** val pass_discr : pass -> pass -> __ **)
 398 let pass_discr x y =
 399   Logic.eq_rect_Type2 x
 400     (match x with
 401      | Clight_pass -> Obj.magic (fun _ dH -> dH)
 402      | Clight_switch_removed_pass -> Obj.magic (fun _ dH -> dH)
 403      | Clight_label_pass -> Obj.magic (fun _ dH -> dH)
 404      | Clight_simplified_pass -> Obj.magic (fun _ dH -> dH)
 405      | Cminor_pass -> Obj.magic (fun _ dH -> dH)
 406      | Rtlabs_pass -> Obj.magic (fun _ dH -> dH)
 407      | Rtl_separate_pass -> Obj.magic (fun _ dH -> dH)
 408      | Rtl_uniq_pass -> Obj.magic (fun _ dH -> dH)
 409      | Ertl_pass -> Obj.magic (fun _ dH -> dH)
 410      | Ltl_pass -> Obj.magic (fun _ dH -> dH)
 411      | Lin_pass -> Obj.magic (fun _ dH -> dH)
 412      | Assembly_pass -> Obj.magic (fun _ dH -> dH)
 413      | Object_code_pass -> Obj.magic (fun _ dH -> dH)) y
 414
 415 (** val pass_jmdiscr : pass -> pass -> __ **)
 416 let pass_jmdiscr x y =
 417   Logic.eq_rect_Type2 x
 418     (match x with
 419      | Clight_pass -> Obj.magic (fun _ dH -> dH)
 420      | Clight_switch_removed_pass -> Obj.magic (fun _ dH -> dH)
 421      | Clight_label_pass -> Obj.magic (fun _ dH -> dH)
 422      | Clight_simplified_pass -> Obj.magic (fun _ dH -> dH)
 423      | Cminor_pass -> Obj.magic (fun _ dH -> dH)
 424      | Rtlabs_pass -> Obj.magic (fun _ dH -> dH)
 425      | Rtl_separate_pass -> Obj.magic (fun _ dH -> dH)
 426      | Rtl_uniq_pass -> Obj.magic (fun _ dH -> dH)
 427      | Ertl_pass -> Obj.magic (fun _ dH -> dH)
 428      | Ltl_pass -> Obj.magic (fun _ dH -> dH)
 429      | Lin_pass -> Obj.magic (fun _ dH -> dH)
 430      | Assembly_pass -> Obj.magic (fun _ dH -> dH)
 431      | Object_code_pass -> Obj.magic (fun _ dH -> dH)) y
 432
 433 type 'x with_stack_model = ('x, AST.ident -> Nat.nat Types.option) Types.prod
 434
 435 type syntax_of_pass = __
 436
 437 type observe_pass = pass -> syntax_of_pass -> Types.unit0
 438
 439 (** val front_end :
 440     observe_pass -> Csyntax.clight_program -> ((CostLabel.costlabel,
 441     Csyntax.clight_program) Types.prod, RTLabs_syntax.rTLabs_program)
 442     Types.prod Errors.res **)
 443 let front_end observe p =
 444   let i = Obj.magic observe Clight_pass p in
 445   let p0 = SwitchRemoval.program_switch_removal p in
 446   let i0 = Obj.magic observe Clight_switch_removed_pass p0 in
 447   let { Types.fst = p'; Types.snd = init_cost } = Label.clight_label p0 in
 448   let i1 = Obj.magic observe Clight_label_pass p' in
 449   let p1 = SimplifyCasts.simplify_program p' in
 450   let i2 = Obj.magic observe Clight_simplified_pass p1 in
 451   Obj.magic
 452     (Monad.m_bind0 (Monad.max_def Errors.res0)
 453       (Obj.magic (ToCminor.clight_to_cminor p1)) (fun p2 ->
 454       let i3 = observe Cminor_pass p2 in
 455       let p3 = ToRTLabs.cminor_to_rtlabs (Obj.magic p2) in
 456       let i4 = Obj.magic observe Rtlabs_pass p3 in
 457       Monad.m_bind0 (Monad.max_def Errors.res0)
 458         (Obj.magic (CostCheck.check_cost_program_prf p3)) (fun _ ->
 459         Monad.m_bind0 (Monad.max_def Errors.res0)
 460           (Obj.magic (CostInj.check_program_cost_injectivity_prf p3))
 461           (fun _ ->
 462           Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
 463             { Types.fst = init_cost; Types.snd = p' }; Types.snd = p3 }))))
 464
 465 open Uses
 466
 467 (** val compute_fixpoint : Fixpoints.fixpoint_computer **)
 468 let compute_fixpoint = Compute_fixpoints.compute_fixpoint
 469
 470 (** val colour_graph : Interference.coloured_graph_computer **)
 471 let colour_graph = Compute_colouring.colour_graph
 472
 473 open AssocList
 474
 475 (** val lookup_stack_cost :
 476     Joint.params -> Joint.joint_program -> PreIdentifiers.identifier ->
 477     Nat.nat Types.option **)
 478 let lookup_stack_cost p p0 id =
 479   AssocList.assoc_list_lookup id
 480     (Identifiers.eq_identifier PreIdentifiers.SymbolTag)
 481     (Joint.stack_cost p p0)
 482
 483 (** val back_end :
 484     observe_pass -> CostLabel.costlabel -> RTLabs_syntax.rTLabs_program ->
 485     (((ASM.pseudo_assembly_program, CostLabel.costlabel) Types.prod,
 486     Joint.stack_cost_model) Types.prod, Nat.nat) Types.prod Errors.res **)
 487 let back_end observe init_cost p =
 488   let p0 = RTLabsToRTL.rtlabs_to_rtl init_cost p in
 489   let st = lookup_stack_cost (Joint.graph_params_to_params RTL.rTL) p0 in
 490   let i =
 491     Obj.magic observe Rtl_separate_pass { Types.fst = p0; Types.snd = st }
 492   in
 493   let i0 = Obj.magic observe Rtl_uniq_pass { Types.fst = p0; Types.snd = st }
 494   in
 495   let p1 = RTLToERTL.rtl_to_ertl p0 in
 496   let st0 = lookup_stack_cost (Joint.graph_params_to_params ERTL.eRTL) p1 in
 497   let i1 = Obj.magic observe Ertl_pass { Types.fst = p1; Types.snd = st0 } in
 498   let { Types.fst = eta2; Types.snd = max_stack } =
 499     ERTLToLTL.ertl_to_ltl compute_fixpoint colour_graph p1
 500   in
 501   let { Types.fst = p2; Types.snd = stack_cost } = eta2 in
 502   let st1 = lookup_stack_cost (Joint.graph_params_to_params LTL.lTL) p2 in
 503   let i2 = Obj.magic observe Ltl_pass { Types.fst = p2; Types.snd = st1 } in
 504   let st2 = lookup_stack_cost (Joint.graph_params_to_params LTL.lTL) p2 in
 505   let p3 = LTLToLIN.ltl_to_lin p2 in
 506   let st3 = lookup_stack_cost (Joint.lin_params_to_params LIN.lIN) p3 in
 507   let i3 = Obj.magic observe Lin_pass { Types.fst = p3; Types.snd = st3 } in
 508   Obj.magic
 509     (Monad.m_bind0 (Monad.max_def Errors.res0)
 510       (Obj.magic
 511         (Errors.opt_to_res (Errors.msg ErrorMessages.AssemblyTooLarge)
 512           (LINToASM.lin_to_asm p3))) (fun p4 ->
 513       Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = { Types.fst =
 514         { Types.fst = p4; Types.snd = init_cost }; Types.snd = stack_cost };
 515         Types.snd = max_stack }))
 516
 517 open Assembly
 518
 519 open Status
 520
 521 open Fetch
 522
 523 open PolicyFront
 524
 525 open PolicyStep
 526
 527 open Policy
 528
 529 (** val assembler :
 530     observe_pass -> ASM.pseudo_assembly_program -> ASM.labelled_object_code
 531     Errors.res **)
 532 let assembler observe p =
 533 prerr_endline "Y1";
 534   Obj.magic
 535     (Monad.m_bind0 (Monad.max_def Errors.res0)
 536       (Obj.magic
 537         (Errors.opt_to_res (Errors.msg ErrorMessages.Jump_expansion_failed)
 538           (Policy.jump_expansion' p))) (fun sigma_pol ->
 539 prerr_endline "Y2";
 540       let sigma = fun ppc -> (Types.pi1 sigma_pol).Types.fst ppc in
 541       let pol = fun ppc -> (Types.pi1 sigma_pol).Types.snd ppc in
 542       let i =
 543         Obj.magic observe Assembly_pass { Types.fst = { Types.fst = p;
 544           Types.snd = sigma }; Types.snd = pol }
 545       in
 546 prerr_endline "Y3";
 547       let p0 = Assembly.assembly p sigma pol in
 548 prerr_endline "Y4";
 549       let i0 = Obj.magic observe Object_code_pass (Types.pi1 p0) in
 550 prerr_endline "Y5";
 551       Obj.magic (Errors.OK (Types.pi1 p0))))
 552
 553 open StructuredTraces
 554
 555 open AbstractStatus
 556
 557 open StatusProofs
 558
 559 open Interpret
 560
 561 open ASMCosts
 562
 563 (** val lift_out_of_sigma :
 564     'a2 -> ('a1 -> (__, __) Types.sum) -> ('a1 Types.sig0 -> 'a2) -> 'a1 ->
 565     'a2 **)
 566 let lift_out_of_sigma dflt dec m a_sig =
 567   match dec a_sig with
 568   | Types.Inl _ -> m a_sig
 569   | Types.Inr _ -> dflt
 570
 571 (** val lift_cost_map_back_to_front :
 572     ASM.labelled_object_code -> StructuredTraces.as_cost_map ->
 573     Label.clight_cost_map **)
 574 let lift_cost_map_back_to_front oc asm_cost_map =
 575   lift_out_of_sigma Nat.O
 576     (Obj.magic
 577       (BitVectorTrie.strong_decidable_in_codomain
 578         (Identifiers.deq_identifier PreIdentifiers.CostTag) (Nat.S (Nat.S
 579         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 580         (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))))))))))
 581         (Obj.magic oc.ASM.costlabels))) asm_cost_map
 582
 583 open UtilBranch
 584
 585 open ASMCostsSplit
 586
 587 type compiler_output = { c_labelled_object_code : ASM.labelled_object_code;
 588                          c_stack_cost : Joint.stack_cost_model;
 589                          c_max_stack : Nat.nat;
 590                          c_init_costlabel : CostLabel.costlabel;
 591                          c_labelled_clight : Csyntax.clight_program;
 592                          c_clight_cost_map : Label.clight_cost_map }
 593
 594 (** val compiler_output_rect_Type4 :
 595     (ASM.labelled_object_code -> Joint.stack_cost_model -> Nat.nat ->
 596     CostLabel.costlabel -> Csyntax.clight_program -> Label.clight_cost_map ->
 597     'a1) -> compiler_output -> 'a1 **)
 598 let rec compiler_output_rect_Type4 h_mk_compiler_output x_185 =
 599   let { c_labelled_object_code = c_labelled_object_code0; c_stack_cost =
 600     c_stack_cost0; c_max_stack = c_max_stack0; c_init_costlabel =
 601     c_init_costlabel0; c_labelled_clight = c_labelled_clight0;
 602     c_clight_cost_map = c_clight_cost_map0 } = x_185
 603   in
 604   h_mk_compiler_output c_labelled_object_code0 c_stack_cost0 c_max_stack0
 605     c_init_costlabel0 c_labelled_clight0 c_clight_cost_map0
 606
 607 (** val compiler_output_rect_Type5 :
 608     (ASM.labelled_object_code -> Joint.stack_cost_model -> Nat.nat ->
 609     CostLabel.costlabel -> Csyntax.clight_program -> Label.clight_cost_map ->
 610     'a1) -> compiler_output -> 'a1 **)
 611 let rec compiler_output_rect_Type5 h_mk_compiler_output x_187 =
 612   let { c_labelled_object_code = c_labelled_object_code0; c_stack_cost =
 613     c_stack_cost0; c_max_stack = c_max_stack0; c_init_costlabel =
 614     c_init_costlabel0; c_labelled_clight = c_labelled_clight0;
 615     c_clight_cost_map = c_clight_cost_map0 } = x_187
 616   in
 617   h_mk_compiler_output c_labelled_object_code0 c_stack_cost0 c_max_stack0
 618     c_init_costlabel0 c_labelled_clight0 c_clight_cost_map0
 619
 620 (** val compiler_output_rect_Type3 :
 621     (ASM.labelled_object_code -> Joint.stack_cost_model -> Nat.nat ->
 622     CostLabel.costlabel -> Csyntax.clight_program -> Label.clight_cost_map ->
 623     'a1) -> compiler_output -> 'a1 **)
 624 let rec compiler_output_rect_Type3 h_mk_compiler_output x_189 =
 625   let { c_labelled_object_code = c_labelled_object_code0; c_stack_cost =
 626     c_stack_cost0; c_max_stack = c_max_stack0; c_init_costlabel =
 627     c_init_costlabel0; c_labelled_clight = c_labelled_clight0;
 628     c_clight_cost_map = c_clight_cost_map0 } = x_189
 629   in
 630   h_mk_compiler_output c_labelled_object_code0 c_stack_cost0 c_max_stack0
 631     c_init_costlabel0 c_labelled_clight0 c_clight_cost_map0
 632
 633 (** val compiler_output_rect_Type2 :
 634     (ASM.labelled_object_code -> Joint.stack_cost_model -> Nat.nat ->
 635     CostLabel.costlabel -> Csyntax.clight_program -> Label.clight_cost_map ->
 636     'a1) -> compiler_output -> 'a1 **)
 637 let rec compiler_output_rect_Type2 h_mk_compiler_output x_191 =
 638   let { c_labelled_object_code = c_labelled_object_code0; c_stack_cost =
 639     c_stack_cost0; c_max_stack = c_max_stack0; c_init_costlabel =
 640     c_init_costlabel0; c_labelled_clight = c_labelled_clight0;
 641     c_clight_cost_map = c_clight_cost_map0 } = x_191
 642   in
 643   h_mk_compiler_output c_labelled_object_code0 c_stack_cost0 c_max_stack0
 644     c_init_costlabel0 c_labelled_clight0 c_clight_cost_map0
 645
 646 (** val compiler_output_rect_Type1 :
 647     (ASM.labelled_object_code -> Joint.stack_cost_model -> Nat.nat ->
 648     CostLabel.costlabel -> Csyntax.clight_program -> Label.clight_cost_map ->
 649     'a1) -> compiler_output -> 'a1 **)
 650 let rec compiler_output_rect_Type1 h_mk_compiler_output x_193 =
 651   let { c_labelled_object_code = c_labelled_object_code0; c_stack_cost =
 652     c_stack_cost0; c_max_stack = c_max_stack0; c_init_costlabel =
 653     c_init_costlabel0; c_labelled_clight = c_labelled_clight0;
 654     c_clight_cost_map = c_clight_cost_map0 } = x_193
 655   in
 656   h_mk_compiler_output c_labelled_object_code0 c_stack_cost0 c_max_stack0
 657     c_init_costlabel0 c_labelled_clight0 c_clight_cost_map0
 658
 659 (** val compiler_output_rect_Type0 :
 660     (ASM.labelled_object_code -> Joint.stack_cost_model -> Nat.nat ->
 661     CostLabel.costlabel -> Csyntax.clight_program -> Label.clight_cost_map ->
 662     'a1) -> compiler_output -> 'a1 **)
 663 let rec compiler_output_rect_Type0 h_mk_compiler_output x_195 =
 664   let { c_labelled_object_code = c_labelled_object_code0; c_stack_cost =
 665     c_stack_cost0; c_max_stack = c_max_stack0; c_init_costlabel =
 666     c_init_costlabel0; c_labelled_clight = c_labelled_clight0;
 667     c_clight_cost_map = c_clight_cost_map0 } = x_195
 668   in
 669   h_mk_compiler_output c_labelled_object_code0 c_stack_cost0 c_max_stack0
 670     c_init_costlabel0 c_labelled_clight0 c_clight_cost_map0
 671
 672 (** val c_labelled_object_code :
 673     compiler_output -> ASM.labelled_object_code **)
 674 let rec c_labelled_object_code xxx =
 675   xxx.c_labelled_object_code
 676
 677 (** val c_stack_cost : compiler_output -> Joint.stack_cost_model **)
 678 let rec c_stack_cost xxx =
 679   xxx.c_stack_cost
 680
 681 (** val c_max_stack : compiler_output -> Nat.nat **)
 682 let rec c_max_stack xxx =
 683   xxx.c_max_stack
 684
 685 (** val c_init_costlabel : compiler_output -> CostLabel.costlabel **)
 686 let rec c_init_costlabel xxx =
 687   xxx.c_init_costlabel
 688
 689 (** val c_labelled_clight : compiler_output -> Csyntax.clight_program **)
 690 let rec c_labelled_clight xxx =
 691   xxx.c_labelled_clight
 692
 693 (** val c_clight_cost_map : compiler_output -> Label.clight_cost_map **)
 694 let rec c_clight_cost_map xxx =
 695   xxx.c_clight_cost_map
 696
 697 (** val compiler_output_inv_rect_Type4 :
 698     compiler_output -> (ASM.labelled_object_code -> Joint.stack_cost_model ->
 699     Nat.nat -> CostLabel.costlabel -> Csyntax.clight_program ->
 700     Label.clight_cost_map -> __ -> 'a1) -> 'a1 **)
 701 let compiler_output_inv_rect_Type4 hterm h1 =
 702   let hcut = compiler_output_rect_Type4 h1 hterm in hcut __
 703
 704 (** val compiler_output_inv_rect_Type3 :
 705     compiler_output -> (ASM.labelled_object_code -> Joint.stack_cost_model ->
 706     Nat.nat -> CostLabel.costlabel -> Csyntax.clight_program ->
 707     Label.clight_cost_map -> __ -> 'a1) -> 'a1 **)
 708 let compiler_output_inv_rect_Type3 hterm h1 =
 709   let hcut = compiler_output_rect_Type3 h1 hterm in hcut __
 710
 711 (** val compiler_output_inv_rect_Type2 :
 712     compiler_output -> (ASM.labelled_object_code -> Joint.stack_cost_model ->
 713     Nat.nat -> CostLabel.costlabel -> Csyntax.clight_program ->
 714     Label.clight_cost_map -> __ -> 'a1) -> 'a1 **)
 715 let compiler_output_inv_rect_Type2 hterm h1 =
 716   let hcut = compiler_output_rect_Type2 h1 hterm in hcut __
 717
 718 (** val compiler_output_inv_rect_Type1 :
 719     compiler_output -> (ASM.labelled_object_code -> Joint.stack_cost_model ->
 720     Nat.nat -> CostLabel.costlabel -> Csyntax.clight_program ->
 721     Label.clight_cost_map -> __ -> 'a1) -> 'a1 **)
 722 let compiler_output_inv_rect_Type1 hterm h1 =
 723   let hcut = compiler_output_rect_Type1 h1 hterm in hcut __
 724
 725 (** val compiler_output_inv_rect_Type0 :
 726     compiler_output -> (ASM.labelled_object_code -> Joint.stack_cost_model ->
 727     Nat.nat -> CostLabel.costlabel -> Csyntax.clight_program ->
 728     Label.clight_cost_map -> __ -> 'a1) -> 'a1 **)
 729 let compiler_output_inv_rect_Type0 hterm h1 =
 730   let hcut = compiler_output_rect_Type0 h1 hterm in hcut __
 731
 732 (** val compiler_output_jmdiscr :
 733     compiler_output -> compiler_output -> __ **)
 734 let compiler_output_jmdiscr x y =
 735   Logic.eq_rect_Type2 x
 736     (let { c_labelled_object_code = a0; c_stack_cost = a1; c_max_stack = a2;
 737        c_init_costlabel = a3; c_labelled_clight = a4; c_clight_cost_map =
 738        a5 } = x
 739      in
 740     Obj.magic (fun _ dH -> dH __ __ __ __ __ __)) y
 741
 742 (** val compile :
 743     observe_pass -> Csyntax.clight_program -> compiler_output Errors.res **)
 744 let compile observe p =
 745   Obj.magic
 746     (Monad.m_bind3 (Monad.max_def Errors.res0)
 747       (Obj.magic (front_end observe p)) (fun init_cost p' p0 ->
 748       Monad.m_bind3 (Monad.max_def Errors.res0)
 749         (Obj.magic (back_end observe init_cost p0))
 750         (fun p_init_costlabel stack_cost max_stack ->
 751         let { Types.fst = p1; Types.snd = init_costlabel } = p_init_costlabel
 752         in
 753         Monad.m_bind0 (Monad.max_def Errors.res0)
 754           (Obj.magic (assembler observe p1)) (fun p2 ->
 755           let k = ASMCostsSplit.aSM_cost_map p2 in
 756           let k' = lift_cost_map_back_to_front p2 k in
 757           Monad.m_return0 (Monad.max_def Errors.res0)
 758             { c_labelled_object_code = p2; c_stack_cost = stack_cost;
 759             c_max_stack = max_stack; c_init_costlabel = init_costlabel;
 760             c_labelled_clight = p'; c_clight_cost_map = k' }))))
 761