source: src/compiler.ma @ 1995

Last change on this file since 1995 was 1995, checked in by campbell, 8 years ago

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

File size: 1.7 KB
Line 
1
2include "Clight/label.ma".
3(* include "Clight/SimplifyCasts.ma". *)  definition simplify_program : clight_program → clight_program ≝ λp.p.
4include "Clight/switchRemoval.ma".
5include "Clight/toCminor.ma".
6include "Cminor/initialisation.ma".
7include "Cminor/toRTLabs.ma".
8
9definition front_end : clight_program → res RTLabs_program ≝
10λp.
11  let p ≝ clight_label p in
12  let p ≝ simplify_program p in
13  let p ≝ program_switch_removal p in
14  ! p ← clight_to_cminor 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 TracBrowser for help on using the repository browser.