Changeset 2001


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

Get the compiler to output more.

Location:
src
Files:
4 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASMCostsSplit.ma

    r1946 r2001  
    326326    let code_memory ≝ load_code_memory program in
    327327      traverse_code code_memory cost_labels cost_labels_injective.
     328
     329definition object_code ≝ list Byte.
     330definition costlabel_map ≝ BitVectorTrie costlabel 16.     
     331
     332definition ASM_cost_map :
     333  ∀p.let code_memory ≝ load_code_memory (\fst p) in
     334  ? → as_cost_map (ASM_abstract_status code_memory (\snd p)) ≝
     335  λp : object_code × costlabel_map.
     336  λcost_labels_injective.
     337  let cost_map ≝ compute_costs (\fst p) (\snd p) cost_labels_injective in
     338  λl_sig.
     339  lookup_present … cost_map l_sig ?.
     340  cases cost_map
     341  #m * #prf #_ cases l_sig cases daemon (*bla bla*)
     342  qed.
  • src/ASM/CostsProof.ma

    r1976 r2001  
    722722  @nat_of_bitvector_lt_bound
    723723qed.
    724 
    725 definition ASM_cost_map :
    726   ∀code_memory: BitVectorTrie Byte 16.
    727   ∀cost_labels: BitVectorTrie costlabel 16.
    728   ∀cost_map: identifier_map CostTag nat.
    729   (∀pc,k. lookup_opt … pc cost_labels = Some … k → present … cost_map k) →
    730   as_cost_map (ASM_abstract_status code_memory cost_labels) ≝
    731   λcode_memory,cost_labels,cost_map,codom_dom,l_sig.
    732   (lookup_present … cost_map (pi1 … l_sig) ?).
    733   cases l_sig #l * #pc @(codom_dom pc)
    734   qed.
    735724 
    736725include "utilities/permutations.ma".
  • 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 
  • src/correctness.ma

    r1996 r2001  
    99
    1010∀input_program.
    11 ! output ← compile input_program
     11! 〈labelled,output〉 ← compile input_program
    1212
    13 exec_inf … clight_fullexec input_program ≈ exec_inf … ASM_fullexec output
     13exec_inf … clight_fullexec input_program ≃l exec_inf … clight_fullexec labelled
     14
     15
     16
     17exec_inf … clight_fullexec labelled ≈ exec_inf … ASM_fullexec output
    1418
    1519
     
    2125→ clock σ_f = clock σ_0 + δ
    2226
     27
     28
     29What is ≃l?  Must show that "labelled" does everything that
     30"input_program" does, without getting lost in some
     31non-terminating loop part way.
     32
    2333*)
    2434
Note: See TracChangeset for help on using the changeset viewer.