Changeset 1495 for src/ASM


Ignore:
Timestamp:
Nov 7, 2011, 3:45:18 PM (8 years ago)
Author:
mulligan
Message:

proper calculation of costs

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASMCosts.ma

    r1486 r1495  
    2525qed.
    2626
     27definition instruction_nature_next_pc_length ≝
     28  λvariety: instruction_nature.
     29  match variety with
     30  [ ret ⇒ 0
     31  | branch _ ⇒ 2
     32  | goto _ ⇒ 1
     33  | direct_fun_call _ ⇒ 1
     34  | other ⇒ 1
     35  ].
     36
    2737definition instruction_info:
    28     BitVectorTrie Byte 16 → Word → ?
     38    BitVectorTrie Byte 16 → Word → Σprod: (instruction_nature × Word × (list Word) × nat). |\snd (\fst prod)| = instruction_nature_next_pc_length (\fst (\fst (\fst prod)))
    2939  λmem.
    3040  λpc.
    3141  let 〈inst, next_pc, inst_cost〉 ≝ fetch mem pc in
    32   let 〈nature, next_pcs〉
    33     match inst with
     42  let nature_next_pcs_proof
     43    match inst return λx. Σpair: (instruction_nature × (list Word)). |(\snd pair)| = instruction_nature_next_pc_length (\fst pair) with
    3444    [ RealInstruction ri ⇒
    3545      match ri with
    36       [ RET ⇒ 〈ret, [ ]〉
    37       | RETI ⇒ 〈ret, [ ]〉
     46      [ RET ⇒ dp … 〈ret, [ ]〉 ?
     47      | RETI ⇒ dp … 〈ret, [ ]〉 ?
    3848      | JC addr ⇒
    3949        match addr return λx. bool_to_Prop (is_in ? [[ relative ]] x) → ? with
    4050        [ RELATIVE addr ⇒ λ_.
    4151          let 〈carry, addr〉 ≝ half_add … 16 next_pc (sign_extend 8 8 addr) in
    42             〈branch addr, [ next_pc; addr ]〉
     52            dp … 〈branch addr, [ next_pc; addr ]〉 ?
    4353        | _ ⇒ λp. match p in False with [ ]
    4454        ] (subaddressing_modein … addr)
     
    4757        [ RELATIVE addr ⇒ λ_.
    4858          let 〈carry, addr〉 ≝ half_add … 16 next_pc (sign_extend 8 8 addr) in
    49             〈branch addr, [ next_pc; addr ]〉
     59            dp … 〈branch addr, [ next_pc; addr ]〉 ?
    5060        | _ ⇒ λp. match p in False with [ ]
    5161        ] (subaddressing_modein … addr)
     
    5464        [ RELATIVE addr ⇒ λ_.
    5565          let 〈carry, addr〉 ≝ half_add … 16 next_pc (sign_extend 8 8 addr) in
    56             〈branch addr, [ next_pc; addr ]〉
     66            dp … 〈branch addr, [ next_pc; addr ]〉 ?
    5767        | _ ⇒ λp. match p in False with [ ]
    5868        ] (subaddressing_modein … addr)
     
    6171        [ RELATIVE addr ⇒ λ_.
    6272          let 〈carry, addr〉 ≝ half_add … 16 next_pc (sign_extend 8 8 addr) in
    63             〈branch addr, [ next_pc; addr ]〉
     73            dp … 〈branch addr, [ next_pc; addr ]〉 ?
    6474        | _ ⇒ λp. match p in False with [ ]
    6575        ] (subaddressing_modein … addr)
     
    6878        [ RELATIVE addr ⇒ λ_.
    6979          let 〈carry, addr〉 ≝ half_add … 16 next_pc (sign_extend 8 8 addr) in
    70             〈branch addr, [ next_pc; addr ]〉
     80            dp … 〈branch addr, [ next_pc; addr ]〉 ?
    7181        | _ ⇒ λp. match p in False with [ ]
    7282        ] (subaddressing_modein … addr2)
     
    7585        [ RELATIVE addr ⇒ λ_.
    7686          let 〈carry, addr〉 ≝ half_add … 16 next_pc (sign_extend 8 8 addr) in
    77             〈branch addr, [ next_pc; addr ]〉
     87            dp … 〈branch addr, [ next_pc; addr ]〉 ?
    7888        | _ ⇒ λp. match p in False with [ ]
    7989        ] (subaddressing_modein … addr2)
     
    8292        [ RELATIVE addr ⇒ λ_.
    8393          let 〈carry, addr〉 ≝ half_add … 16 next_pc (sign_extend 8 8 addr) in
    84             〈branch addr, [ next_pc; addr ]〉
     94            dp … 〈branch addr, [ next_pc; addr ]〉 ?
    8595        | _ ⇒ λp. match p in False with [ ]
    8696        ] (subaddressing_modein … addr2)
     
    8999        [ RELATIVE addr ⇒ λ_.
    90100          let 〈carry, addr〉 ≝ half_add … 16 next_pc (sign_extend 8 8 addr) in
    91             〈branch addr, [ next_pc; addr ]〉
     101            dp … 〈branch addr, [ next_pc; addr ]〉 ?
    92102        | _ ⇒ λp. match p in False with [ ]
    93103        ] (subaddressing_modein … addr2)
     
    96106        [ RELATIVE addr ⇒ λ_.
    97107          let 〈carry, addr〉 ≝ half_add … 16 next_pc (sign_extend 8 8 addr) in
    98             〈branch addr, [ next_pc; addr ]〉
    99         | _ ⇒ λp. match p in False with [ ]
    100         ] (subaddressing_modein … addr2)
    101       | _ ⇒ 〈other, [ next_pc ]〉
     108            dp … 〈branch addr, [ next_pc; addr ]〉 ?
     109        | _ ⇒ λp. match p in False with [ ]
     110        ] (subaddressing_modein … addr2)
     111      | _ ⇒ dp … 〈other, [ next_pc ]〉 ?
    102112      ]
    103113    | ACALL addr ⇒
     
    105115      [ ADDR11 addr ⇒ λ_.
    106116        let addr ≝ addr16_of_addr11 pc addr in
    107           〈direct_fun_call addr, [ next_pc ]〉
     117          dp … 〈direct_fun_call addr, [ next_pc ]〉 ?
    108118      | _ ⇒ λp. match p in False with [ ]
    109119      ] (subaddressing_modein … addr)
    110120    | LCALL addr ⇒
    111121      match addr return λx. bool_to_Prop (is_in ? [[ addr16 ]] x) → ? with
    112       [ ADDR16 addr ⇒ λ_. 〈direct_fun_call addr, [ next_pc ]〉
     122      [ ADDR16 addr ⇒ λ_. dp … 〈direct_fun_call addr, [ next_pc ]〉 ?
    113123      | _ ⇒ λp. match p in False with [ ]
    114124      ] (subaddressing_modein … addr)
     
    117127      [ ADDR11 addr ⇒ λ_.
    118128        let addr ≝ addr16_of_addr11 pc addr in
    119           〈goto addr, [ addr ]〉
     129          dp … 〈goto addr, [ addr ]〉 ?
    120130      | _ ⇒ λp. match p in False with [ ]
    121131      ] (subaddressing_modein … addr)
    122132    | LJMP addr ⇒
    123133      match addr return λx. bool_to_Prop (is_in ? [[ addr16 ]] x) → ? with
    124       [ ADDR16 addr ⇒ λ_. 〈goto addr, [ addr ]〉
     134      [ ADDR16 addr ⇒ λ_. dp … 〈goto addr, [ addr ]〉 ?
    125135      | _ ⇒ λp. match p in False with [ ]
    126136      ] (subaddressing_modein … addr)
     
    129139      [ RELATIVE addr ⇒ λ_.
    130140        let 〈carry, addr〉 ≝ half_add 16 next_pc (sign_extend 8 8 addr) in
    131           〈goto addr, [ addr ]〉
    132       | _ ⇒ λp. match p in False with [ ]
    133       ] (subaddressing_modein … addr)
    134     | JMP addr ⇒ 〈other, [ next_pc ]〉
    135     | MOVC acc_a addr ⇒ 〈other, [ next_pc ]〉
     141          dp … 〈goto addr, [ addr ]〉 ?
     142      | _ ⇒ λp. match p in False with [ ]
     143      ] (subaddressing_modein … addr)
     144    | JMP addr ⇒ dp … 〈other, [ next_pc ]〉 ?
     145    | MOVC acc_a addr ⇒ dp … 〈other, [ next_pc ]〉 ?
    136146    ]
    137147  in
    138     〈nature, next_pc, next_pcs, inst_cost〉.
     148    match nature_next_pcs_proof with
     149    [ dp nature_next_pcs their_proof ⇒
     150      let nature ≝ \fst nature_next_pcs in
     151      let next_pcs ≝ \snd nature_next_pcs in
     152        dp … 〈〈〈nature, next_pc〉, next_pcs〉, inst_cost〉 ?
     153    ].
     154  [1: >their_proof %
     155  |*: %
     156  ]
     157qed.
    139158
    140159let rec compare
     
    160179qed.
    161180
    162 let rec block_cost
     181let rec block_cost'
    163182  (mem: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie Byte 16)
    164     (the_list: list Word) (program_size: nat)
    165       on program_size: nat
     183    (program_counter: Word) (program_size: nat) (cost_so_far: nat)
     184      on program_size
    166185  match program_size with
    167   [ O ⇒ 0 (* XXX: empty program *)
    168   | S program_size ⇒
    169     match the_list with
    170     [ nil ⇒ 0 (* XXX: should be empty program *)
    171     | cons pc tl ⇒
    172       match tl with
    173       [ nil ⇒
    174         match lookup_opt … pc cost_labels with
    175         [ None ⇒
    176           let 〈ignore, ignore, next_pcs, cost〉 ≝ instruction_info mem pc in
    177           let tail ≝ block_cost mem cost_labels next_pcs program_size in
    178             cost + tail
    179         | Some _ ⇒ O
    180         ]
    181       | _   ⇒ compare ? (map … (λpc. 〈pc, block_cost mem cost_labels [pc] program_size〉) the_list)
     186  [ O ⇒ 0
     187  | S program_size ⇒       
     188    let sigma ≝ instruction_info mem program_counter in
     189      match sigma with
     190      [ dp variety_costs their_proof ⇒
     191        let variety ≝ \fst (\fst (\fst variety_costs)) in
     192        let next_pc ≝ \snd (\fst (\fst variety_costs)) in
     193        let next_pcs ≝ \snd (\fst variety_costs) in
     194        let inst_cost ≝ \snd variety_costs in
     195          match variety return λx. |next_pcs| = instruction_nature_next_pc_length x → nat with
     196          [ other ⇒ λproof.
     197            match next_pcs return λx. |x| = 1 → nat with
     198            [ nil ⇒ λabsurd. ⊥
     199            | cons hd tl ⇒ λproof.
     200              match lookup_opt … hd cost_labels with
     201              [ None ⇒ block_cost' mem cost_labels hd program_size (cost_so_far + inst_cost)
     202              | Some _ ⇒ inst_cost + cost_so_far
     203              ]
     204            ] proof
     205          | _ ⇒ λ_. inst_cost + cost_so_far
     206          ] their_proof
    182207      ]
    183     ]
    184   ].
     208  ].
     209  normalize in absurd
     210  destruct(absurd)
     211qed.
     212
     213definition block_cost ≝
     214  λmem: BitVectorTrie Byte 16.
     215  λcost_labels: BitVectorTrie Byte 16.
     216  λprogram_counter: Word.
     217  λprogram_size: nat.
     218    block_cost' mem cost_labels program_counter program_size 0.
    185219
    186220let rec traverse_code_internal
     
    188222    (cost_labels: BitVectorTrie Byte 16) (pc: Word) (program_size: nat)
    189223      on program: BitVectorTrie nat 8 ≝
    190   let 〈ignore, newpc, ignore, ignore〉 ≝ instruction_info mem pc in
    191   match program with
    192   [ nil ⇒ Stub …
    193   | cons hd tl ⇒
    194     match lookup_opt … pc cost_labels with
    195     [ None ⇒ traverse_code_internal tl mem cost_labels newpc program_size
    196     | Some lbl ⇒
    197       let cost ≝ block_cost mem cost_labels [ pc ] program_size in
    198       let cost_mapping ≝ traverse_code_internal tl mem cost_labels newpc program_size in
    199         insert … lbl cost cost_mapping
     224  match instruction_info mem pc with
     225  [ dp info proof ⇒
     226    let newpc ≝ \snd (\fst (\fst info)) in
     227    match program with
     228    [ nil ⇒ Stub …
     229    | cons hd tl ⇒
     230      match lookup_opt … pc cost_labels with
     231      [ None ⇒ traverse_code_internal tl mem cost_labels newpc program_size
     232      | Some lbl ⇒
     233        let cost ≝ block_cost mem cost_labels pc program_size in
     234        let cost_mapping ≝ traverse_code_internal tl mem cost_labels newpc program_size in
     235          insert … lbl cost cost_mapping
     236      ]
    200237    ]
    201238  ].
     
    217254    match lookup_opt … oldpc cost_labels with
    218255    [ None ⇒
    219       let 〈nature, pc, ignore, inst_cost〉 ≝ instruction_info mem oldpc in
     256      match instruction_info mem oldpc with
     257      [ dp info proof ⇒
     258        let nature ≝ \fst (\fst (\fst info)) in
     259        let pc ≝ \snd (\fst (\fst info)) in
     260        let inst_cost ≝ \snd info in
    220261        match nature with
    221262        [ direct_fun_call addr ⇒
     
    227268        | _ ⇒ ⊥ (* XXX: was assert false in o'caml *)
    228269        ]
     270      ]
    229271    | Some cost ⇒ 〈cost, 0〉
    230272    ]
Note: See TracChangeset for help on using the changeset viewer.