Changeset 2774 for src/compiler.ma

Timestamp:

Mar 5, 2013, 6:15:06 PM (8 years ago)

Author:

sacerdot

Message:

1. the compiler now outputs both the stack cost model and the max stack available
2. hypothesis on initial status not failing removed from correctness.ma by using the low level definition

File:

• src/compiler.ma (modified) (2 diffs)

src/compiler.ma

@@ -32 +32 @@
 axiom colour_graph : coloured_graph_computer.
 
-definition back_end : RTLabs_program → res pseudo_assembly_program ≝
+definition back_end :
+ RTLabs_program →
+  res (pseudo_assembly_program × stack_cost_model × nat) ≝
 λp.
   let p ≝ rtlabs_to_rtl p in
   let p ≝ rtl_to_ertl p in
   let p ≝ ertl_to_ertlptr p in
-  let p ≝ ertlptr_to_ltl compute_fixpoint colour_graph p in (* TODO: abstract over colouring *)
+  let 〈p,stack_cost,max_stack〉 ≝ ertlptr_to_ltl compute_fixpoint colour_graph p in (* TODO: abstract over colouring *)
   let p ≝ ltl_to_lin p in
-          opt_to_res ? (msg AssemblyTooLarge) (lin_to_asm p).
+  let p ≝ lin_to_asm p in
+   match p with
+   [ None ⇒ Error … (msg AssemblyTooLarge)
+   | Some p ⇒ OK … 〈p,stack_cost,max_stack〉 ].
 
 include "ASM/Policy.ma".
@@ -71 +76 @@
 include "ASM/ASMCostsSplit.ma". 
 
-definition compile : clight_program →
-  res (labelled_object_code × (𝚺labelled:clight_program. clight_cost_map labelled)) ≝ 
+record compiler_output : Type[0] ≝
+ { c_labelled_object_code: labelled_object_code
+ ; c_stack_cost: stack_cost_model
+ ; c_max_stack: nat
+ ; c_labelled_clight: clight_program
+ ; c_clight_cost_map: clight_cost_map c_labelled_clight
+ }.
+
+definition compile : clight_program → res compiler_output ≝ 
 λp.
   ! 〈init_cost,p',p〉 ← front_end p;
-  ! p ← back_end p;
+  ! 〈p,stack_cost,max_stack〉 ← back_end p;
   ! p ← assembler p;
   let k ≝ ASM_cost_map p in
   let k' ≝
    lift_cost_map_back_to_front p' (load_code_memory (oc p)) (costlabels p) k in
-  return 〈p, ❬p', k'❭〉.
+  return mk_compiler_output p stack_cost max_stack p' k'.