Changeset 2505


Ignore:
Timestamp:
Nov 29, 2012, 3:37:22 PM (7 years ago)
Author:
mckinna
Message:

Cleaned up compiler.ma; some refactoring/additional code needed in Clight/label, and a tweak to translate_cst in RTLabsToRTL to restore its checked status.

Location:
src
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/label.ma

    r2399 r2505  
    5353λp,l. Exists … (λx.x=l) (labels_of_clight p).
    5454
     55definition in_clight_label ≝
     56  λp. Σl. in_clight_program p l.
     57
     58definition clight_cost_map ≝
     59  λp. (in_clight_label p) → ℕ.
     60
    5561definition clight_label_free : clight_program → bool ≝
    5662λp. match labels_of_clight p with [ nil ⇒ true | _ ⇒ false ].
  • src/RTLabs/RTLabsToRTL.ma

    r2493 r2505  
    161161  λr,lenv,prf. make_addr ? (find_local_env_arg r lenv prf).
    162162
    163 include alias "common/Identifiers.ma".
     163(*include alias "common/Identifiers.ma".*)
    164164let rec rtl_args (args : list register) (env : local_env) on args :
    165165  All ? (λr.bool_to_Prop (r∈env)) args → list psd_argument ≝
  • src/compiler.ma

    r2497 r2505  
    2626axiom build : ∀valuation. coloured_graph valuation.
    2727*)
     28
    2829definition back_end : RTLabs_program → pseudo_assembly_program ≝
    2930λp.
     
    3435          lin_to_asm p.
    3536
    36 include "ASM/Assembly.ma".
     37include "ASM/Fetch.ma". (* minimum needed for axiom to typecheck *)
    3738
    3839axiom assembler : pseudo_assembly_program → res (object_code × costlabel_map).
    39 (*
    40 include "ASM/Policy.ma".
     40
     41(* include "ASM/Policy.ma".
    4142
    4243axiom Jump_expansion_failed : String.
     
    5556*)
    5657
    57 include "ASM/ASMCostsSplit.ma".
     58
     59include "ASM/ASMCosts.ma".
    5860
    5961definition lift_cost_map_back_to_front :
    6062  ∀clight, code_memory, lbls.
    61    (∀l. (∃pc.as_label_of_pc (ASM_abstract_status code_memory lbls) pc = Some … l) +
    62        ¬(∃pc.as_label_of_pc (ASM_abstract_status code_memory lbls) pc = Some … l)) →
    63   as_cost_map (ASM_abstract_status code_memory lbls) →
    64   (Σl : costlabel.in_clight_program clight l) → ℕ ≝ λclight,code_memory,lbls,dec,k,l_sig.
    65    match dec l_sig with
     63    let abstat ≝ ASM_abstract_status code_memory lbls in
     64   (∀l. (as_cost_labelled abstat l) + ¬(as_cost_labelled abstat l)) →
     65  as_cost_map abstat → clight_cost_map clight ≝
     66  λclight,code_memory,lbls,dec,k,asm_cost_map.
     67  lift_sigma_map_id … 0 (* labels not present in out code get 0 *)
     68    dec k asm_cost_map
     69  (*
     70   match dec asm_cost_map with
    6671   [ inl prf ⇒ k «l_sig, prf»
    6772   | inr _ ⇒ 0 (* labels not present in out code get 0 *)
    68    ].
     73   ]*).
     74
     75include "ASM/ASMCostsSplit.ma".
    6976
    7077definition compile : clight_program →
    71   res (object_code × costlabel_map × (𝚺labelled:clight_program. ((Σl.in_clight_program labelled l) → ℕ))) ≝
     78  res (object_code × costlabel_map × (𝚺labelled:clight_program. clight_cost_map labelled)) (*(Σl.in_clight_program labelled l) → ℕ*) ≝
    7279λp.
    7380  ! 〈init_cost,p',p〉 ← front_end p;
     
    8491  cases daemon
    8592  qed.
    86 
Note: See TracChangeset for help on using the changeset viewer.