source: src/compiler.ma @ 2645

Last change on this file since 2645 was 2645, checked in by sacerdot, 8 years ago
  1. some broken back-end files repaires, several still to go
  2. the string datatype has been refined into three different data types: string (for backend comments); identifierTag; ErrorMessage?
  3. all axioms of type String have been turned into constructors of one of the three datatypes. In this way we do not have axioms to be implemented in the extracted files
File size: 2.8 KB
Line 
1
2include "Clight/label.ma".
3include "Clight/SimplifyCasts.ma".
4include "Clight/switchRemoval.ma".
5include "Clight/toCminor.ma".
6include "Cminor/initialisation.ma".
7include "Cminor/toRTLabs.ma".
8
9definition front_end : clight_program → res (costlabel × clight_program × RTLabs_program) ≝
10λp.
11  let p ≝ program_switch_removal p in
12  let 〈p',init_cost〉 ≝ clight_label p in
13  let p ≝ simplify_program p' in
14  ! p ← clight_to_cminor p;
15  let p ≝ cminor_to_rtlabs init_cost p in
16  return 〈init_cost,p',p〉.
17
18(*
19include "RTLabs/RTLabsToRTL.ma".
20include "RTL/RTLToERTL.ma".
21include "ERTL/ERTLToLTL.ma".
22include "LTL/LTLToLIN.ma".
23include "LIN/LINToASM.ma".
24
25(* these are already defined in utilities/fixpoint.ma and ERTL/Interference.ma
26axiom the_fixpoint : fixpoint.
27axiom build : ∀valuation. coloured_graph valuation.
28*)
29
30definition back_end : RTLabs_program → pseudo_assembly_program ≝
31λp.
32  let p ≝ rtlabs_to_rtl p in
33  let p ≝ rtl_to_ertl p in
34  let p ≝ ertl_to_ltl p in  (* TODO: abstract over colouring *)
35  let p ≝ ltl_to_lin p in
36          lin_to_asm p.
37*)
38include "ASM/ASM.ma".
39axiom back_end : RTLabs_program → pseudo_assembly_program.
40
41(* JHM: minimum needed for assembler axiom to typecheck *)
42(* JHM: moved from ASMCostsSplit.ma                     *)
43(* JHM: should move elsewhere in ASM/                   *)
44definition object_code ≝ list Byte.
45definition costlabel_map ≝ BitVectorTrie costlabel 16.
46
47axiom assembler : pseudo_assembly_program → res (object_code × costlabel_map).
48
49(* include "ASM/Policy.ma".
50
51definition assembler : pseudo_assembly_program → res (object_code × costlabel_map) ≝
52λp.
53  let 〈preamble, list_instr〉 ≝ p in
54  (* TODO: fail if p is too large. *)
55  let p' ≝ 〈preamble, list_instr〉 in
56  ! sigma_pol ← opt_to_res ? (msg Jump_expansion_failed) (jump_expansion' p');
57  let sigma ≝ λppc. \fst (sigma_pol ppc) in
58  let pol ≝ λppc. \snd (sigma_pol ppc) in
59  OK ? (assembly p sigma pol).
60cases daemon
61qed.
62*)
63
64include "ASM/ASMCosts.ma".
65
66definition lift_cost_map_back_to_front :
67  ∀clight, code_memory, lbls.
68    let abstat ≝ ASM_abstract_status code_memory lbls in
69   (∀l. (as_cost_labelled abstat l) + ¬(as_cost_labelled abstat l)) →
70  as_cost_map abstat → clight_cost_map clight ≝
71  λclight,code_memory,lbls,dec,k,asm_cost_map.
72  lift_sigma_map_id … 0 (* labels not present in out code get 0 *)
73    dec k asm_cost_map.
74
75include "ASM/ASMCostsSplit.ma".
76
77definition compile : clight_program →
78  res (object_code × costlabel_map × (𝚺labelled:clight_program. clight_cost_map labelled)) ≝
79λp.
80  ! 〈init_cost,p',p〉 ← front_end p;
81  let p ≝ back_end p in
82    ! p ← assembler p;
83  let k ≝ ASM_cost_map p ? in
84  let k' ≝ lift_cost_map_back_to_front
85    p'
86    (load_code_memory (\fst p))
87    (\snd p)
88    ? k
89    in
90  return 〈p, ❬p', k'❭〉.
91  cases daemon
92  qed.
Note: See TracBrowser for help on using the repository browser.