Changeset 2001 for src/compiler.ma


Ignore:
Timestamp:
May 25, 2012, 1:47:32 PM (8 years ago)
Author:
campbell
Message:

Get the compiler to output more.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/compiler.ma

    r1995 r2001  
    77include "Cminor/toRTLabs.ma".
    88
    9 definition front_end : clight_program → res RTLabs_program
     9definition front_end : clight_program → res (clight_program × RTLabs_program)
    1010λp.
    11   let p ≝ clight_label p in
    12   let p ≝ simplify_program p in
     11  let p' ≝ clight_label p in
     12  let p ≝ simplify_program p' in
    1313  let p ≝ program_switch_removal p in
    1414  ! p ← clight_to_cminor p;
    15         cminor_to_rtlabs p.
     15  ! p ← cminor_to_rtlabs p;
     16  return 〈p',p〉.
    1617
    1718include "RTLabs/RTLabsToRTL.ma".
     
    3435include "ASM/Assembly.ma".
    3536
    36 definition object_code ≝ list Byte.
    37 definition costlabel_map ≝ BitVectorTrie costlabel 16.
    38 
    3937include "ASM/Policy.ma".
    4038
    4139axiom Jump_expansion_failed : String.
     40
     41include "ASM/ASMCostsSplit.ma".
    4242
    4343definition assembler : pseudo_assembly_program → res (object_code × costlabel_map) ≝
     
    5353qed.
    5454
    55 definition compile : clight_program → res (object_code × costlabel_map) ≝
     55include "RTLabs/semantics.ma".
     56
     57axiom RTLabs_abstract_status : genv → abstract_status.
     58
     59include "joint/semantics.ma".
     60axiom joint_abstract_status :
     61  ∀globals.∀p:params globals.genv globals p → abstract_status.
     62
     63include "common/StructuredTraces.ma".
     64
     65definition in_clight_program : costlabel → Prop ≝ λ_.True.
     66
     67definition lift_cost_map_back_to_front :
     68  ∀code_memory, lbls.
     69   (∀l. (∃pc.as_label_of_pc (ASM_abstract_status code_memory lbls) pc = Some … l) +
     70       ¬(∃pc.as_label_of_pc (ASM_abstract_status code_memory lbls) pc = Some … l)) →
     71  as_cost_map (ASM_abstract_status code_memory lbls) →
     72  (Σl : costlabel.in_clight_program l) → ℕ ≝ λcode_memory,lbls,dec,k,l_sig.
     73   match dec l_sig with
     74   [ inl prf ⇒ k «l_sig, prf»
     75   | inr _ ⇒ 0 (* labels not present in out code get 0 *)
     76   ].
     77
     78definition compile : clight_program →
     79  res (object_code × costlabel_map × clight_program × ((Σl.in_clight_program l) → ℕ)) ≝
    5680λp.
    57     ! p ← front_end p;
     81  ! 〈p',p〉 ← front_end p;
    5882  let p ≝ back_end p in
    59           assembler p.
     83    ! p ← assembler p;
     84  let k ≝ ASM_cost_map p ? in
     85  let k' ≝ lift_cost_map_back_to_front
     86    (load_code_memory (\fst p))
     87    (\snd p)
     88    ? k
     89    in
     90  return 〈p, p', k'〉.
     91  cases daemon
     92  qed.
    6093
    61 
    62 
Note: See TracChangeset for help on using the changeset viewer.