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   Obj.magic
 534     (Monad.m_bind0 (Monad.max_def Errors.res0)
 535       (Obj.magic
 536         (Errors.opt_to_res (Errors.msg ErrorMessages.Jump_expansion_failed)
 537           (Policy.jump_expansion' p))) (fun sigma_pol ->
 538       let sigma = fun ppc -> (Types.pi1 sigma_pol).Types.fst ppc in
 539       let pol = fun ppc -> (Types.pi1 sigma_pol).Types.snd ppc in
 540       let i =
 541         Obj.magic observe Assembly_pass { Types.fst = { Types.fst = p;
 542           Types.snd = sigma }; Types.snd = pol }
 543       in
 544       let p0 = Assembly.assembly p sigma pol in
 545       let i0 = Obj.magic observe Object_code_pass (Types.pi1 p0) in
 546       Obj.magic (Errors.OK (Types.pi1 p0))))
 547
 548 open StructuredTraces
 549
 550 open AbstractStatus
 551
 552 open StatusProofs
 553
 554 open Interpret
 555
 556 open ASMCosts
 557
 558 (** val lift_out_of_sigma :
 559     'a2 -> ('a1 -> (__, __) Types.sum) -> ('a1 Types.sig0 -> 'a2) -> 'a1 ->
 560     'a2 **)
 561 let lift_out_of_sigma dflt dec m a_sig =
 562   match dec a_sig with
 563   | Types.Inl _ -> m a_sig
 564   | Types.Inr _ -> dflt
 565
 566 (** val lift_cost_map_back_to_front :
 567     ASM.labelled_object_code -> StructuredTraces.as_cost_map ->
 568     Label.clight_cost_map **)
 569 let lift_cost_map_back_to_front oc asm_cost_map =
 570   lift_out_of_sigma Nat.O
 571     (Obj.magic
 572       (BitVectorTrie.strong_decidable_in_codomain
 573         (Identifiers.deq_identifier PreIdentifiers.CostTag) (Nat.S (Nat.S
 574         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 575         (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))))))))))
 576         (Obj.magic oc.ASM.costlabels))) asm_cost_map
 577
 578 open UtilBranch
 579
 580 open ASMCostsSplit
 581
 582 type compiler_output = { c_labelled_object_code : ASM.labelled_object_code;
 583                          c_stack_cost : Joint.stack_cost_model;
 584                          c_max_stack : Nat.nat;
 585                          c_init_costlabel : CostLabel.costlabel;
 586                          c_labelled_clight : Csyntax.clight_program;
 587                          c_clight_cost_map : Label.clight_cost_map }
 588
 589 (** val compiler_output_rect_Type4 :
 590     (ASM.labelled_object_code -> Joint.stack_cost_model -> Nat.nat ->
 591     CostLabel.costlabel -> Csyntax.clight_program -> Label.clight_cost_map ->
 592     'a1) -> compiler_output -> 'a1 **)
 593 let rec compiler_output_rect_Type4 h_mk_compiler_output x_185 =
 594   let { c_labelled_object_code = c_labelled_object_code0; c_stack_cost =
 595     c_stack_cost0; c_max_stack = c_max_stack0; c_init_costlabel =
 596     c_init_costlabel0; c_labelled_clight = c_labelled_clight0;
 597     c_clight_cost_map = c_clight_cost_map0 } = x_185
 598   in
 599   h_mk_compiler_output c_labelled_object_code0 c_stack_cost0 c_max_stack0
 600     c_init_costlabel0 c_labelled_clight0 c_clight_cost_map0
 601
 602 (** val compiler_output_rect_Type5 :
 603     (ASM.labelled_object_code -> Joint.stack_cost_model -> Nat.nat ->
 604     CostLabel.costlabel -> Csyntax.clight_program -> Label.clight_cost_map ->
 605     'a1) -> compiler_output -> 'a1 **)
 606 let rec compiler_output_rect_Type5 h_mk_compiler_output x_187 =
 607   let { c_labelled_object_code = c_labelled_object_code0; c_stack_cost =
 608     c_stack_cost0; c_max_stack = c_max_stack0; c_init_costlabel =
 609     c_init_costlabel0; c_labelled_clight = c_labelled_clight0;
 610     c_clight_cost_map = c_clight_cost_map0 } = x_187
 611   in
 612   h_mk_compiler_output c_labelled_object_code0 c_stack_cost0 c_max_stack0
 613     c_init_costlabel0 c_labelled_clight0 c_clight_cost_map0
 614
 615 (** val compiler_output_rect_Type3 :
 616     (ASM.labelled_object_code -> Joint.stack_cost_model -> Nat.nat ->
 617     CostLabel.costlabel -> Csyntax.clight_program -> Label.clight_cost_map ->
 618     'a1) -> compiler_output -> 'a1 **)
 619 let rec compiler_output_rect_Type3 h_mk_compiler_output x_189 =
 620   let { c_labelled_object_code = c_labelled_object_code0; c_stack_cost =
 621     c_stack_cost0; c_max_stack = c_max_stack0; c_init_costlabel =
 622     c_init_costlabel0; c_labelled_clight = c_labelled_clight0;
 623     c_clight_cost_map = c_clight_cost_map0 } = x_189
 624   in
 625   h_mk_compiler_output c_labelled_object_code0 c_stack_cost0 c_max_stack0
 626     c_init_costlabel0 c_labelled_clight0 c_clight_cost_map0
 627
 628 (** val compiler_output_rect_Type2 :
 629     (ASM.labelled_object_code -> Joint.stack_cost_model -> Nat.nat ->
 630     CostLabel.costlabel -> Csyntax.clight_program -> Label.clight_cost_map ->
 631     'a1) -> compiler_output -> 'a1 **)
 632 let rec compiler_output_rect_Type2 h_mk_compiler_output x_191 =
 633   let { c_labelled_object_code = c_labelled_object_code0; c_stack_cost =
 634     c_stack_cost0; c_max_stack = c_max_stack0; c_init_costlabel =
 635     c_init_costlabel0; c_labelled_clight = c_labelled_clight0;
 636     c_clight_cost_map = c_clight_cost_map0 } = x_191
 637   in
 638   h_mk_compiler_output c_labelled_object_code0 c_stack_cost0 c_max_stack0
 639     c_init_costlabel0 c_labelled_clight0 c_clight_cost_map0
 640
 641 (** val compiler_output_rect_Type1 :
 642     (ASM.labelled_object_code -> Joint.stack_cost_model -> Nat.nat ->
 643     CostLabel.costlabel -> Csyntax.clight_program -> Label.clight_cost_map ->
 644     'a1) -> compiler_output -> 'a1 **)
 645 let rec compiler_output_rect_Type1 h_mk_compiler_output x_193 =
 646   let { c_labelled_object_code = c_labelled_object_code0; c_stack_cost =
 647     c_stack_cost0; c_max_stack = c_max_stack0; c_init_costlabel =
 648     c_init_costlabel0; c_labelled_clight = c_labelled_clight0;
 649     c_clight_cost_map = c_clight_cost_map0 } = x_193
 650   in
 651   h_mk_compiler_output c_labelled_object_code0 c_stack_cost0 c_max_stack0
 652     c_init_costlabel0 c_labelled_clight0 c_clight_cost_map0
 653
 654 (** val compiler_output_rect_Type0 :
 655     (ASM.labelled_object_code -> Joint.stack_cost_model -> Nat.nat ->
 656     CostLabel.costlabel -> Csyntax.clight_program -> Label.clight_cost_map ->
 657     'a1) -> compiler_output -> 'a1 **)
 658 let rec compiler_output_rect_Type0 h_mk_compiler_output x_195 =
 659   let { c_labelled_object_code = c_labelled_object_code0; c_stack_cost =
 660     c_stack_cost0; c_max_stack = c_max_stack0; c_init_costlabel =
 661     c_init_costlabel0; c_labelled_clight = c_labelled_clight0;
 662     c_clight_cost_map = c_clight_cost_map0 } = x_195
 663   in
 664   h_mk_compiler_output c_labelled_object_code0 c_stack_cost0 c_max_stack0
 665     c_init_costlabel0 c_labelled_clight0 c_clight_cost_map0
 666
 667 (** val c_labelled_object_code :
 668     compiler_output -> ASM.labelled_object_code **)
 669 let rec c_labelled_object_code xxx =
 670   xxx.c_labelled_object_code
 671
 672 (** val c_stack_cost : compiler_output -> Joint.stack_cost_model **)
 673 let rec c_stack_cost xxx =
 674   xxx.c_stack_cost
 675
 676 (** val c_max_stack : compiler_output -> Nat.nat **)
 677 let rec c_max_stack xxx =
 678   xxx.c_max_stack
 679
 680 (** val c_init_costlabel : compiler_output -> CostLabel.costlabel **)
 681 let rec c_init_costlabel xxx =
 682   xxx.c_init_costlabel
 683
 684 (** val c_labelled_clight : compiler_output -> Csyntax.clight_program **)
 685 let rec c_labelled_clight xxx =
 686   xxx.c_labelled_clight
 687
 688 (** val c_clight_cost_map : compiler_output -> Label.clight_cost_map **)
 689 let rec c_clight_cost_map xxx =
 690   xxx.c_clight_cost_map
 691
 692 (** val compiler_output_inv_rect_Type4 :
 693     compiler_output -> (ASM.labelled_object_code -> Joint.stack_cost_model ->
 694     Nat.nat -> CostLabel.costlabel -> Csyntax.clight_program ->
 695     Label.clight_cost_map -> __ -> 'a1) -> 'a1 **)
 696 let compiler_output_inv_rect_Type4 hterm h1 =
 697   let hcut = compiler_output_rect_Type4 h1 hterm in hcut __
 698
 699 (** val compiler_output_inv_rect_Type3 :
 700     compiler_output -> (ASM.labelled_object_code -> Joint.stack_cost_model ->
 701     Nat.nat -> CostLabel.costlabel -> Csyntax.clight_program ->
 702     Label.clight_cost_map -> __ -> 'a1) -> 'a1 **)
 703 let compiler_output_inv_rect_Type3 hterm h1 =
 704   let hcut = compiler_output_rect_Type3 h1 hterm in hcut __
 705
 706 (** val compiler_output_inv_rect_Type2 :
 707     compiler_output -> (ASM.labelled_object_code -> Joint.stack_cost_model ->
 708     Nat.nat -> CostLabel.costlabel -> Csyntax.clight_program ->
 709     Label.clight_cost_map -> __ -> 'a1) -> 'a1 **)
 710 let compiler_output_inv_rect_Type2 hterm h1 =
 711   let hcut = compiler_output_rect_Type2 h1 hterm in hcut __
 712
 713 (** val compiler_output_inv_rect_Type1 :
 714     compiler_output -> (ASM.labelled_object_code -> Joint.stack_cost_model ->
 715     Nat.nat -> CostLabel.costlabel -> Csyntax.clight_program ->
 716     Label.clight_cost_map -> __ -> 'a1) -> 'a1 **)
 717 let compiler_output_inv_rect_Type1 hterm h1 =
 718   let hcut = compiler_output_rect_Type1 h1 hterm in hcut __
 719
 720 (** val compiler_output_inv_rect_Type0 :
 721     compiler_output -> (ASM.labelled_object_code -> Joint.stack_cost_model ->
 722     Nat.nat -> CostLabel.costlabel -> Csyntax.clight_program ->
 723     Label.clight_cost_map -> __ -> 'a1) -> 'a1 **)
 724 let compiler_output_inv_rect_Type0 hterm h1 =
 725   let hcut = compiler_output_rect_Type0 h1 hterm in hcut __
 726
 727 (** val compiler_output_jmdiscr :
 728     compiler_output -> compiler_output -> __ **)
 729 let compiler_output_jmdiscr x y =
 730   Logic.eq_rect_Type2 x
 731     (let { c_labelled_object_code = a0; c_stack_cost = a1; c_max_stack = a2;
 732        c_init_costlabel = a3; c_labelled_clight = a4; c_clight_cost_map =
 733        a5 } = x
 734      in
 735     Obj.magic (fun _ dH -> dH __ __ __ __ __ __)) y
 736
 737 (** val compile :
 738     observe_pass -> Csyntax.clight_program -> compiler_output Errors.res **)
 739 let compile observe p =
 740   Obj.magic
 741     (Monad.m_bind3 (Monad.max_def Errors.res0)
 742       (Obj.magic (front_end observe p)) (fun init_cost p' p0 ->
 743       Monad.m_bind3 (Monad.max_def Errors.res0)
 744         (Obj.magic (back_end observe init_cost p0))
 745         (fun p_init_costlabel stack_cost max_stack ->
 746         let { Types.fst = p1; Types.snd = init_costlabel } = p_init_costlabel
 747         in
 748         Monad.m_bind0 (Monad.max_def Errors.res0)
 749           (Obj.magic (assembler observe p1)) (fun p2 ->
 750           let k = ASMCostsSplit.aSM_cost_map p2 in
 751           let k' = lift_cost_map_back_to_front p2 k in
 752           Monad.m_return0 (Monad.max_def Errors.res0)
 753             { c_labelled_object_code = p2; c_stack_cost = stack_cost;
 754             c_max_stack = max_stack; c_init_costlabel = init_costlabel;
 755             c_labelled_clight = p'; c_clight_cost_map = k' }))))
 756