Changeset 2828


Ignore:
Timestamp:
Mar 8, 2013, 11:17:44 PM (7 years ago)
Author:
sacerdot
Message:
  1. New semantics.ma file that puts together all semantics. It contains a function to observe the semantics of an intermediate program. Note: the type of backend semantics is currently wrong because of the stack cost! If you observe a back-end language now, it will core dump.
  2. Added observations into compiler.ma
Location:
src
Files:
1 added
1 edited

Legend:

Unmodified
Added
Removed
  • src/compiler.ma

    r2794 r2828  
     1(* Front-end related includes *)
    12include "Clight/label.ma".
    23include "Clight/SimplifyCasts.ma".
     
    78include "RTLabs/CostInj.ma".
    89
    9 definition front_end : clight_program → res (costlabel × clight_program × RTLabs_program) ≝
    10 λp.
     10(* Back-end related includes *)
     11include "RTLabs/RTLabsToRTL.ma".
     12include "RTL/RTLToERTL.ma".
     13include "ERTL/ERTLToERTLptr.ma".
     14include "ERTLptr/ERTLptrToLTL.ma".
     15include "LTL/LTLToLIN.ma".
     16include "LIN/LINToASM.ma".
     17
     18(* List of all passes whose outputs can be observed *)
     19inductive pass : Type[0] ≝
     20   clight_pass: pass
     21 | clight_switch_removed_pass: pass
     22 | clight_label_pass: pass
     23 | clight_simplified_pass: pass
     24 | cminor_pass: pass
     25 | rtlabs_pass: pass
     26 | rtl_separate_pass: pass
     27 | rtl_uniq_pass: pass
     28 | ertl_pass: pass
     29 | ertlptr_pass: pass
     30 | ltl_pass: pass
     31 | lin_pass: pass.
     32
     33definition syntax_of_pass : pass → Type[0] ≝
     34 λpass.
     35  match pass with
     36  [ clight_pass ⇒ clight_program
     37  | clight_switch_removed_pass ⇒ clight_program
     38  | clight_label_pass ⇒ clight_program
     39  | clight_simplified_pass ⇒ clight_program
     40  | cminor_pass ⇒ Cminor_program
     41  | 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 ].
     48
     49definition observe_pass ≝ ∀pass. syntax_of_pass pass → unit.
     50
     51(* The compiler front-end *)
     52definition front_end :
     53 observe_pass → clight_program → res (costlabel × clight_program × RTLabs_program) ≝
     54λobserve,p.
     55  let i ≝ observe clight_pass p in
    1156  let p ≝ program_switch_removal p in
     57  let i ≝ observe clight_switch_removed_pass p in
    1258  let 〈p',init_cost〉 ≝ clight_label p in
     59  let i ≝ observe clight_label_pass p' in
    1360  let p ≝ simplify_program p' in
     61  let i ≝ observe clight_simplified_pass p in
    1462  ! p ← clight_to_cminor p;
     63  let i ≝ observe cminor_pass p in
    1564  let p ≝ cminor_to_rtlabs init_cost p in
     65  let i ≝ observe rtlabs_pass p in
    1666  if check_cost_program p then
    1767    if check_program_cost_injectivity p then
     
    2272    (Error ? (msg BadCostLabelling)).
    2373
    24 include "RTLabs/RTLabsToRTL.ma".
    25 include "RTL/RTLToERTL.ma".
    26 include "ERTL/ERTLToERTLptr.ma".
    27 include "ERTLptr/ERTLptrToLTL.ma".
    28 include "LTL/LTLToLIN.ma".
    29 include "LIN/LINToASM.ma".
    30 
     74(* The compiler back-end *)
    3175axiom compute_fixpoint : fixpoint_computer.
    3276axiom colour_graph : coloured_graph_computer.
    3377
    3478definition back_end :
    35  RTLabs_program →
     79 observe_pass → RTLabs_program →
    3680  res (pseudo_assembly_program × stack_cost_model × nat) ≝
    37 λp.
     81λobserve,p.
    3882  let p ≝ rtlabs_to_rtl p in
     83  let i ≝ observe rtl_separate_pass p in
     84  let i ≝ observe rtl_uniq_pass p in
    3985  let p ≝ rtl_to_ertl p in
     86  let i ≝ observe ertl_pass p in
    4087  let p ≝ ertl_to_ertlptr p in
     88  let i ≝ observe ertlptr_pass p in
    4189  let 〈p,stack_cost,max_stack〉 ≝ ertlptr_to_ltl compute_fixpoint colour_graph p in (* TODO: abstract over colouring *)
     90  let i ≝ observe ltl_pass p in
    4291  let p ≝ ltl_to_lin p in
     92  let i ≝ observe lin_pass p in
    4393   ! p ← opt_to_res ? (msg AssemblyTooLarge) (lin_to_asm p) ;
    4494   return 〈p,stack_cost,max_stack〉.
    4595
     96(* The assembler *)
    4697include "ASM/Policy.ma".
    4798
     
    53104  OK ? (assembly p sigma pol).
    54105
     106(* Cost lifting *)
    55107include "ASM/ASMCosts.ma".
    56108
     
    63115    (strong_decidable_in_codomain …) k asm_cost_map.
    64116
    65 include "ASM/ASMCostsSplit.ma".
     117(* Cost model computation *)
     118include "ASM/ASMCostsSplit.ma".
    66119
    67120record compiler_output : Type[0] ≝
     
    73126 }.
    74127
    75 definition compile : clight_program → res compiler_output ≝
    76 λp.
    77   ! 〈init_cost,p',p〉 ← front_end p;
    78   ! 〈p,stack_cost,max_stack〉 ← back_end p;
     128definition compile : observe_pass → clight_program → res compiler_output ≝
     129λobserve,p.
     130  ! 〈init_cost,p',p〉 ← front_end observe p;
     131  ! 〈p,stack_cost,max_stack〉 ← back_end observe p;
    79132  ! p ← assembler p;
    80133  let k ≝ ASM_cost_map p in
Note: See TracChangeset for help on using the changeset viewer.