1 | |
---|

2 | include "Clight/label.ma". |
---|

3 | (* include "Clight/SimplifyCasts.ma". *) definition simplify_program : clight_program → clight_program ≝ λp.p. |
---|

4 | include "Clight/switchRemoval.ma". |
---|

5 | include "Clight/toCminor.ma". |
---|

6 | include "Cminor/initialisation.ma". |
---|

7 | include "Cminor/toRTLabs.ma". |
---|

8 | |
---|

9 | definition 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 | |
---|

17 | include "RTLabs/RTLabsToRTL.ma". |
---|

18 | include "RTL/RTLToERTL.ma". |
---|

19 | include "ERTL/ERTLToLTL.ma". |
---|

20 | include "LTL/LTLToLIN.ma". |
---|

21 | include "LIN/LINToASM.ma". |
---|

22 | |
---|

23 | axiom the_fixpoint : fixpoint. |
---|

24 | axiom build : ∀valuation. coloured_graph valuation. |
---|

25 | |
---|

26 | definition 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 | |
---|

34 | include "ASM/Assembly.ma". |
---|

35 | |
---|

36 | definition object_code ≝ list Byte. |
---|

37 | definition costlabel_map ≝ BitVectorTrie costlabel 16. |
---|

38 | |
---|

39 | include "ASM/Policy.ma". |
---|

40 | |
---|

41 | axiom Jump_expansion_failed : String. |
---|

42 | |
---|

43 | definition 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). |
---|

52 | cases daemon |
---|

53 | qed. |
---|

54 | |
---|

55 | definition 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 | |
---|