Changeset 1995 for src/compiler.ma


Ignore:
Timestamp:
May 24, 2012, 7:18:35 PM (8 years ago)
Author:
campbell
Message:

Overall compiler definition; bits and pieces to
make everything happy(ish).

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/compiler.ma

    r1991 r1995  
    1313  let p ≝ program_switch_removal p in
    1414  ! p ← clight_to_cminor p;
    15   cminor_to_rtlabs p.
     15        cminor_to_rtlabs p.
     16
     17include "RTLabs/RTLabsToRTL.ma".
     18include "RTL/RTLToERTL.ma".
     19include "ERTL/ERTLToLTL.ma".
     20include "LTL/LTLToLIN.ma".
     21include "LIN/LINToASM.ma".
     22
     23axiom the_fixpoint : fixpoint.
     24axiom build : ∀valuation. coloured_graph valuation.
     25
     26definition back_end : RTLabs_program → pseudo_assembly_program ≝
     27λp.
     28  let p ≝ rtlabs_to_rtl p in
     29  let p ≝ rtl_to_ertl p in
     30  let p ≝ ertl_to_ltl p in  (* TODO: abstract over colouring *)
     31  let p ≝ ltl_to_lin p in
     32          lin_to_asm p.
     33
     34include "ASM/Assembly.ma".
     35
     36definition object_code ≝ list Byte.
     37definition costlabel_map ≝ BitVectorTrie costlabel 16.
     38
     39include "ASM/Policy.ma".
     40
     41axiom Jump_expansion_failed : String.
     42
     43definition assembler : pseudo_assembly_program → res (object_code × costlabel_map) ≝
     44λp.
     45  let 〈preamble, list_instr〉 ≝ p in
     46  (* TODO: fail if p is too large. *)
     47  let p' ≝ 〈preamble, list_instr〉 in
     48  ! sigma_pol ← opt_to_res ? (msg Jump_expansion_failed) (jump_expansion' p');
     49  let sigma ≝ λppc. \fst (sigma_pol ppc) in
     50  let pol ≝ λppc. \snd (sigma_pol ppc) in
     51  OK ? (assembly p sigma pol).
     52cases daemon
     53qed.
     54
     55definition compile : clight_program → res (object_code × costlabel_map) ≝
     56λp.
     57    ! p ← front_end p;
     58  let p ≝ back_end p in
     59          assembler p.
     60
     61
     62
Note: See TracChangeset for help on using the changeset viewer.