Ignore:
Timestamp:
Mar 19, 2013, 7:48:19 PM (7 years ago)
Author:
sacerdot
Message:
  1. a few bugs fixed
  2. as_return implemented for ASM & OC
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASMCostsSplit.ma

    r2899 r2907  
    66
    77let rec traverse_code_internal
    8   (code_memory: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie costlabel 16)
     8  (prog: labelled_object_code)
    99    (program_counter: Word) (program_size: nat)
    1010      (program_size_invariant: program_size = 0 ∨ nat_of_bitvector … program_counter + program_size = 2^16)
    1111        on program_size:
    1212          Σcost_map: identifier_map CostTag nat.
    13             (∀pc,k. nat_of_bitvector … program_counter ≤ nat_of_bitvector 16 pc → nat_of_bitvector … pc < program_size + nat_of_bitvector … program_counter → lookup_opt … pc cost_labels = Some … k → present … cost_map k) ∧
    14             (∀k. ∀k_pres:present … cost_map k. ∃pc. lookup_opt … pc cost_labels = Some … k ∧
    15                pi1 … (block_cost code_memory pc cost_labels) = lookup_present … k_pres) ≝
     13            (∀pc,k. nat_of_bitvector … program_counter ≤ nat_of_bitvector 16 pc → nat_of_bitvector … pc < program_size + nat_of_bitvector … program_counter → lookup_opt … pc (costlabels prog) = Some … k → present … cost_map k) ∧
     14            (∀k. ∀k_pres:present … cost_map k. ∃pc. lookup_opt … pc (costlabels prog) = Some … k ∧
     15               pi1 … (block_cost prog pc) = lookup_present … k_pres) ≝
    1616  match program_size return λx. x = program_size → Σcost_map: ?. ? with
    1717  [ O ⇒ λprogram_size_refl. empty_map CostTag nat
    1818  | S program_size' ⇒ λprogram_size_refl.
    1919    let new_program_counter' ≝ add 16 (bitvector_of_nat 16 1) program_counter in
    20     let cost_mapping ≝ traverse_code_internal code_memory cost_labels new_program_counter' program_size' ? in
    21     match lookup_opt … program_counter cost_labels return λx. x = lookup_opt … program_counter cost_labels → Σcost_map: ?. ? with
     20    let cost_mapping ≝ traverse_code_internal prog new_program_counter' program_size' ? in
     21    match lookup_opt … program_counter (costlabels prog)
     22    return λx. x = lookup_opt … program_counter (costlabels prog) → Σcost_map: ?. ? with
    2223    [ None ⇒ λlookup_refl. pi1 … cost_mapping
    2324    | Some lbl ⇒ λlookup_refl.
    24       let cost ≝ block_cost code_memory program_counter cost_labels in
     25      let cost ≝ block_cost prog program_counter in
    2526        cic:/matita/cerco/common/Identifiers/add.fix(0,2,3) ?? cost_mapping lbl cost
    26     ] (refl … (lookup_opt … program_counter cost_labels))
     27    ] (refl … (lookup_opt … program_counter (costlabels prog)))
    2728  ] (refl … program_size).
    2829  [3:
     
    279280 *)
    280281definition traverse_code:
    281   ∀code_memory: BitVectorTrie Byte 16.
    282   ∀cost_labels: BitVectorTrie costlabel 16.
    283   ∀cost_labels_injective:
    284     ∀pc, pc',l.
    285       lookup_opt … pc cost_labels = Some … l → lookup_opt … pc' cost_labels = Some … l →
    286         pc = pc'.
     282  ∀prog: labelled_object_code.
     283   let cost_labels ≝ costlabels prog in
    287284    Σcost_map: identifier_map CostTag nat.
    288285      (∀pc,k. nat_of_bitvector … pc < 2^16 → lookup_opt … pc cost_labels = Some … k → present … cost_map k) ∧
    289286      (∀k. ∀k_pres:present … cost_map k. ∀pc. lookup_opt … pc cost_labels = Some … k →
    290           pi1 … (block_cost code_memory pc cost_labels) = lookup_present … k_pres) ≝
    291   λcode_memory: BitVectorTrie Byte 16.
    292   λcost_labels: BitVectorTrie costlabel 16.
    293   λcost_labels_injective.
    294     pi1 ? ? (traverse_code_internal code_memory cost_labels (zero …) (2^16) ?).
     287          pi1 … (block_cost prog pc) = lookup_present … k_pres) ≝
     288  λprog.
     289    pi1 ? ? (traverse_code_internal prog (zero …) (2^16) ?).
    295290  [1:
    296291    @or_intror %
    297292  |2:
    298     cases (traverse_code_internal ?????)
     293    cases (traverse_code_internal ???)
    299294    #cost_mapping * #inductive_hypothesis1 #inductive_hypothesis2 %
    300295    [1:
     
    311306      cases (inductive_hypothesis2 ? k_pres)
    312307      #program_counter' * #lookup_opt_assm' #block_cost_assm
    313       >(cost_labels_injective … lookup_opt_assm lookup_opt_assm')
     308      >(oc_injective_costlabels … lookup_opt_assm lookup_opt_assm')
    314309      assumption
    315310    ]
     
    317312qed.
    318313   
    319 definition compute_costs ≝
    320   λprogram: object_code.
    321   λcost_labels: BitVectorTrie costlabel 16.
    322   λcost_labels_injective:
    323     ∀pc, pc',l.
    324       lookup_opt … pc cost_labels = Some … l → lookup_opt … pc' cost_labels = Some … l →
    325         pc = pc'.
    326     (* let program_size ≝ |program| in *)
    327     let code_memory ≝ load_code_memory program in
    328       traverse_code code_memory cost_labels cost_labels_injective.
     314definition compute_costs ≝ traverse_code.
    329315
    330316definition ASM_cost_map :
    331317  ∀p: labelled_object_code.
    332318  let code_memory ≝ load_code_memory (oc p) in
    333   let a_s ≝ OC_abstract_status code_memory (costlabels p) in
     319  let a_s ≝ OC_abstract_status p in
    334320  as_cost_map a_s ≝
    335321  λp.
    336   let cost_map ≝ compute_costs (oc p) (costlabels p) (oc_injective_costlabels … p) in
     322  let cost_map ≝ compute_costs p in
    337323  λl_sig.
    338324  lookup_present … cost_map (as_cost_get_label ? l_sig) ?.
Note: See TracChangeset for help on using the changeset viewer.