Changeset 2841


Ignore:
Timestamp:
Mar 11, 2013, 12:40:46 PM (4 years ago)
Author:
sacerdot
Message:

The compiler now computes also the stack cost for every intermediate
back-end language. The extracted compiler now executes all back-end
passes up to the assembly lanuguage (excluded ATM).

Location:
src
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/compiler.ma

    r2835 r2841  
    3131 | lin_pass: pass.
    3232
     33definition with_stack_model : Type[0] → Type[0] ≝
     34 λA:Type[0].A × (ident → option ℕ).
     35
    3336definition syntax_of_pass : pass → Type[0] ≝
    3437 λpass.
     
    4043  | cminor_pass ⇒ Cminor_program
    4144  | rtlabs_pass ⇒ RTLabs_program
    42   | rtl_separate_pass ⇒ rtl_program
    43   | rtl_uniq_pass ⇒ rtl_program
    44   | ertl_pass ⇒ ertl_program
    45   | ertlptr_pass ⇒ ertlptr_program
    46   | ltl_pass ⇒ ltl_program
    47   | lin_pass ⇒ lin_program ].
     45  | rtl_separate_pass ⇒ with_stack_model rtl_program
     46  | rtl_uniq_pass ⇒ with_stack_model rtl_program
     47  | ertl_pass ⇒ with_stack_model ertl_program
     48  | ertlptr_pass ⇒ with_stack_model ertlptr_program
     49  | ltl_pass ⇒ with_stack_model ltl_program
     50  | lin_pass ⇒ with_stack_model lin_program ].
    4851
    4952definition observe_pass ≝ ∀pass. syntax_of_pass pass → unit.
     
    7376
    7477(* The compiler back-end *)
    75 include "ERTLptr/Uses.ma".  (* Included by the untrusted code *)
     78include "ERTLptr/uses.ma".  (* Included by the untrusted code *)
    7679axiom compute_fixpoint : fixpoint_computer.
    7780axiom colour_graph : coloured_graph_computer.
     81
     82include "common/AssocList.ma".
     83
     84(* Inefficient, replace with Trie lookup *)
     85definition lookup_stack_cost ≝
     86 λP,p,id.
     87  assoc_list_lookup ?? id (eq_identifier …) (stack_cost P p).
    7888
    7989definition back_end :
     
    8292λobserve,p.
    8393  let p ≝ rtlabs_to_rtl p in
    84   let i ≝ observe rtl_separate_pass p in
    85   let i ≝ observe rtl_uniq_pass p in
     94  let st ≝ lookup_stack_cost … p in
     95  let i ≝ observe rtl_separate_pass 〈p,st〉 in
     96  let i ≝ observe rtl_uniq_pass 〈p,st〉 in
    8697  let p ≝ rtl_to_ertl p in
    87   let i ≝ observe ertl_pass p in
     98  let st ≝ lookup_stack_cost … p in 
     99  let i ≝ observe ertl_pass 〈p,st〉 in
    88100  let p ≝ ertl_to_ertlptr p in
    89   let i ≝ observe ertlptr_pass p in
    90   let 〈p,stack_cost,max_stack〉 ≝ ertlptr_to_ltl compute_fixpoint colour_graph p in (* TODO: abstract over colouring *)
    91   let i ≝ observe ltl_pass p in
     101  let st ≝ lookup_stack_cost … p in 
     102  let i ≝ observe ertlptr_pass 〈p,st〉 in
     103  let 〈p,stack_cost,max_stack〉 ≝ ertlptr_to_ltl compute_fixpoint colour_graph p in
     104  (* The two stack models are the same *)
     105  let st ≝ lookup_stack_cost … p in
     106  let i ≝ observe ltl_pass 〈p,st〉 in
     107  let st ≝ lookup_stack_cost … p in
    92108  let p ≝ ltl_to_lin p in
    93   let i ≝ observe lin_pass p in
     109  let st ≝ lookup_stack_cost … p in
     110  let i ≝ observe lin_pass 〈p,st〉 in
    94111   ! p ← opt_to_res ? (msg AssemblyTooLarge) (lin_to_asm p) ;
    95112   return 〈p,stack_cost,max_stack〉.
  • src/semantics.ma

    r2828 r2841  
    3838     mk_preclassified_system_pass lin_pass (joint_preclassified_system LIN_semantics) ?
    3939  ].
    40 try %
    41 whd in ⊢ (??%%);
    42 cases daemon (* XXX False! Leads to core dump! *)
     40%
    4341qed.
    4442
Note: See TracChangeset for help on using the changeset viewer.