Changeset 2774 for src/compiler.ma


Ignore:
Timestamp:
Mar 5, 2013, 6:15:06 PM (7 years ago)
Author:
sacerdot
Message:
  1. the compiler now outputs both the stack cost model and the max stack available
  2. hypothesis on initial status not failing removed from correctness.ma by using the low level definition
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/compiler.ma

    r2767 r2774  
    3232axiom colour_graph : coloured_graph_computer.
    3333
    34 definition back_end : RTLabs_program → res pseudo_assembly_program ≝
     34definition back_end :
     35 RTLabs_program →
     36  res (pseudo_assembly_program × stack_cost_model × nat) ≝
    3537λp.
    3638  let p ≝ rtlabs_to_rtl p in
    3739  let p ≝ rtl_to_ertl p in
    3840  let p ≝ ertl_to_ertlptr p in
    39   let p ≝ ertlptr_to_ltl compute_fixpoint colour_graph p in (* TODO: abstract over colouring *)
     41  let 〈p,stack_cost,max_stack〉 ≝ ertlptr_to_ltl compute_fixpoint colour_graph p in (* TODO: abstract over colouring *)
    4042  let p ≝ ltl_to_lin p in
    41           opt_to_res ? (msg AssemblyTooLarge) (lin_to_asm p).
     43  let p ≝ lin_to_asm p in
     44   match p with
     45   [ None ⇒ Error … (msg AssemblyTooLarge)
     46   | Some p ⇒ OK … 〈p,stack_cost,max_stack〉 ].
    4247
    4348include "ASM/Policy.ma".
     
    7176include "ASM/ASMCostsSplit.ma".
    7277
    73 definition compile : clight_program →
    74   res (labelled_object_code × (𝚺labelled:clight_program. clight_cost_map labelled)) ≝
     78record compiler_output : Type[0] ≝
     79 { c_labelled_object_code: labelled_object_code
     80 ; c_stack_cost: stack_cost_model
     81 ; c_max_stack: nat
     82 ; c_labelled_clight: clight_program
     83 ; c_clight_cost_map: clight_cost_map c_labelled_clight
     84 }.
     85
     86definition compile : clight_program → res compiler_output ≝
    7587λp.
    7688  ! 〈init_cost,p',p〉 ← front_end p;
    77   ! p ← back_end p;
     89  ! 〈p,stack_cost,max_stack〉 ← back_end p;
    7890  ! p ← assembler p;
    7991  let k ≝ ASM_cost_map p in
    8092  let k' ≝
    8193   lift_cost_map_back_to_front p' (load_code_memory (oc p)) (costlabels p) k in
    82   return 〈p, ❬p', k'❭〉.
     94  return mk_compiler_output p stack_cost max_stack p' k'.
Note: See TracChangeset for help on using the changeset viewer.