Changeset 1995 for src/compiler.ma

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:

• src/compiler.ma (modified) (1 diff)

src/compiler.ma

@@ -13 +13 @@
   let p ≝ program_switch_removal p in
   ! p ← clight_to_cminor p;
-  cminor_to_rtlabs p.
+        cminor_to_rtlabs p.
+
+include "RTLabs/RTLabsToRTL.ma".
+include "RTL/RTLToERTL.ma".
+include "ERTL/ERTLToLTL.ma".
+include "LTL/LTLToLIN.ma".
+include "LIN/LINToASM.ma".
+
+axiom the_fixpoint : fixpoint.
+axiom build : ∀valuation. coloured_graph valuation.
+
+definition back_end : RTLabs_program → pseudo_assembly_program ≝
+λp.
+  let p ≝ rtlabs_to_rtl p in
+  let p ≝ rtl_to_ertl p in
+  let p ≝ ertl_to_ltl p in  (* TODO: abstract over colouring *)
+  let p ≝ ltl_to_lin p in
+          lin_to_asm p.
+
+include "ASM/Assembly.ma".
+
+definition object_code ≝ list Byte.
+definition costlabel_map ≝ BitVectorTrie costlabel 16.
+
+include "ASM/Policy.ma".
+
+axiom Jump_expansion_failed : String.
+
+definition assembler : pseudo_assembly_program → res (object_code × costlabel_map) ≝
+λp.
+  let 〈preamble, list_instr〉 ≝ p in
+  (* TODO: fail if p is too large. *)
+  let p' ≝ 〈preamble, list_instr〉 in
+  ! sigma_pol ← opt_to_res ? (msg Jump_expansion_failed) (jump_expansion' p');
+  let sigma ≝ λppc. \fst (sigma_pol ppc) in
+  let pol ≝ λppc. \snd (sigma_pol ppc) in
+  OK ? (assembly p sigma pol).
+cases daemon
+qed.
+
+definition compile : clight_program → res (object_code × costlabel_map) ≝
+λp.
+    ! p ← front_end p;
+  let p ≝ back_end p in
+          assembler p.
+
+
+