63 open Hints_declaration
137 open MemoryInjections
225 open BitVectorTrieSet
231 | Clight_switch_removed_pass
233 | Clight_simplified_pass
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
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
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
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
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
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
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
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
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
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
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
397 (** val pass_discr : pass -> pass -> __ **)
399 Logic.eq_rect_Type2 x
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
415 (** val pass_jmdiscr : pass -> pass -> __ **)
416 let pass_jmdiscr x y =
417 Logic.eq_rect_Type2 x
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
433 type 'x with_stack_model = ('x, AST.ident -> Nat.nat Types.option) Types.prod
435 type syntax_of_pass = __
437 type observe_pass = pass -> syntax_of_pass -> Types.unit0
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
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))
462 Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
463 { Types.fst = init_cost; Types.snd = p' }; Types.snd = p3 }))))
467 (** val compute_fixpoint : Fixpoints.fixpoint_computer **)
468 let compute_fixpoint = Compute_fixpoints.compute_fixpoint
470 (** val colour_graph : Interference.coloured_graph_computer **)
471 let colour_graph = Compute_colouring.colour_graph
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)
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
491 Obj.magic observe Rtl_separate_pass { Types.fst = p0; Types.snd = st }
493 let i0 = Obj.magic observe Rtl_uniq_pass { Types.fst = p0; Types.snd = st }
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
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
509 (Monad.m_bind0 (Monad.max_def Errors.res0)
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 }))
530 observe_pass -> ASM.pseudo_assembly_program -> ASM.labelled_object_code
532 let assembler observe p =
534 (Monad.m_bind0 (Monad.max_def Errors.res0)
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
541 Obj.magic observe Assembly_pass { Types.fst = { Types.fst = p;
542 Types.snd = sigma }; Types.snd = pol }
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))))
548 open StructuredTraces
558 (** val lift_out_of_sigma :
559 'a2 -> ('a1 -> (__, __) Types.sum) -> ('a1 Types.sig0 -> 'a2) -> 'a1 ->
561 let lift_out_of_sigma dflt dec m a_sig =
563 | Types.Inl _ -> m a_sig
564 | Types.Inr _ -> dflt
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
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
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 }
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
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
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
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
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
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
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
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
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
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
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
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
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
672 (** val c_stack_cost : compiler_output -> Joint.stack_cost_model **)
673 let rec c_stack_cost xxx =
676 (** val c_max_stack : compiler_output -> Nat.nat **)
677 let rec c_max_stack xxx =
680 (** val c_init_costlabel : compiler_output -> CostLabel.costlabel **)
681 let rec c_init_costlabel xxx =
684 (** val c_labelled_clight : compiler_output -> Csyntax.clight_program **)
685 let rec c_labelled_clight xxx =
686 xxx.c_labelled_clight
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
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 __
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 __
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 __
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 __
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 __
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 =
735 Obj.magic (fun _ dH -> dH __ __ __ __ __ __)) y
738 observe_pass -> Csyntax.clight_program -> compiler_output Errors.res **)
739 let compile observe p =
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
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' }))))