Changeset 1486 for src/ASM


Ignore:
Timestamp:
Nov 3, 2011, 2:36:37 PM (8 years ago)
Author:
mulligan
Message:

finished asm costs

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASMCosts.ma

    r1474 r1486  
     1include "ASM/ASM.ma".
     2include "ASM/Arithmetic.ma".
     3include "ASM/Fetch.ma".
     4include "ASM/Interpret.ma".
     5
     6inductive instruction_nature: Type[0] ≝
     7  | goto: Word → instruction_nature
     8  | branch: Word → instruction_nature
     9  | direct_fun_call: Word → instruction_nature
     10  | ret: instruction_nature
     11  | other: instruction_nature.
     12
     13definition addr16_of_addr11: Word → Word11 → Word ≝
     14  λpc: Word.
     15  λa: Word11.
     16  let 〈pc_upper, ignore〉 ≝ split … 8 8 pc in
     17  let 〈n1, n2〉 ≝ split … 4 4 pc_upper in
     18  let 〈b123, b〉 ≝ split … 3 8 a in
     19  let b1 ≝ get_index_v … b123 0 ? in
     20  let b2 ≝ get_index_v … b123 1 ? in
     21  let b3 ≝ get_index_v … b123 2 ? in
     22  let p5 ≝ get_index_v … n2 0 ? in
     23    (n1 @@ [[ p5; b1; b2; b3 ]]) @@ b.
     24  //
     25qed.
     26
     27definition instruction_info:
     28    BitVectorTrie Byte 16 → Word → ? ≝
     29  λmem.
     30  λpc.
     31  let 〈inst, next_pc, inst_cost〉 ≝ fetch mem pc in
     32  let 〈nature, next_pcs〉 ≝
     33    match inst with
     34    [ RealInstruction ri ⇒
     35      match ri with
     36      [ RET ⇒ 〈ret, [ ]〉
     37      | RETI ⇒ 〈ret, [ ]〉
     38      | JC addr ⇒
     39        match addr return λx. bool_to_Prop (is_in ? [[ relative ]] x) → ? with
     40        [ RELATIVE addr ⇒ λ_.
     41          let 〈carry, addr〉 ≝ half_add … 16 next_pc (sign_extend 8 8 addr) in
     42            〈branch addr, [ next_pc; addr ]〉
     43        | _ ⇒ λp. match p in False with [ ]
     44        ] (subaddressing_modein … addr)
     45      | JNC addr ⇒
     46        match addr return λx. bool_to_Prop (is_in ? [[ relative ]] x) → ? with
     47        [ RELATIVE addr ⇒ λ_.
     48          let 〈carry, addr〉 ≝ half_add … 16 next_pc (sign_extend 8 8 addr) in
     49            〈branch addr, [ next_pc; addr ]〉
     50        | _ ⇒ λp. match p in False with [ ]
     51        ] (subaddressing_modein … addr)
     52      | JZ addr ⇒
     53        match addr return λx. bool_to_Prop (is_in ? [[ relative ]] x) → ? with
     54        [ RELATIVE addr ⇒ λ_.
     55          let 〈carry, addr〉 ≝ half_add … 16 next_pc (sign_extend 8 8 addr) in
     56            〈branch addr, [ next_pc; addr ]〉
     57        | _ ⇒ λp. match p in False with [ ]
     58        ] (subaddressing_modein … addr)
     59      | JNZ addr ⇒
     60        match addr return λx. bool_to_Prop (is_in ? [[ relative ]] x) → ? with
     61        [ RELATIVE addr ⇒ λ_.
     62          let 〈carry, addr〉 ≝ half_add … 16 next_pc (sign_extend 8 8 addr) in
     63            〈branch addr, [ next_pc; addr ]〉
     64        | _ ⇒ λp. match p in False with [ ]
     65        ] (subaddressing_modein … addr)
     66      | JB addr1 addr2 ⇒
     67        match addr2 return λx. bool_to_Prop (is_in ? [[ relative ]] x) → ? with
     68        [ RELATIVE addr ⇒ λ_.
     69          let 〈carry, addr〉 ≝ half_add … 16 next_pc (sign_extend 8 8 addr) in
     70            〈branch addr, [ next_pc; addr ]〉
     71        | _ ⇒ λp. match p in False with [ ]
     72        ] (subaddressing_modein … addr2)
     73      | JNB addr1 addr2 ⇒
     74        match addr2 return λx. bool_to_Prop (is_in ? [[ relative ]] x) → ? with
     75        [ RELATIVE addr ⇒ λ_.
     76          let 〈carry, addr〉 ≝ half_add … 16 next_pc (sign_extend 8 8 addr) in
     77            〈branch addr, [ next_pc; addr ]〉
     78        | _ ⇒ λp. match p in False with [ ]
     79        ] (subaddressing_modein … addr2)
     80      | JBC addr1 addr2 ⇒
     81        match addr2 return λx. bool_to_Prop (is_in ? [[ relative ]] x) → ? with
     82        [ RELATIVE addr ⇒ λ_.
     83          let 〈carry, addr〉 ≝ half_add … 16 next_pc (sign_extend 8 8 addr) in
     84            〈branch addr, [ next_pc; addr ]〉
     85        | _ ⇒ λp. match p in False with [ ]
     86        ] (subaddressing_modein … addr2)
     87      | DJNZ addr1 addr2 ⇒
     88        match addr2 return λx. bool_to_Prop (is_in ? [[ relative ]] x) → ? with
     89        [ RELATIVE addr ⇒ λ_.
     90          let 〈carry, addr〉 ≝ half_add … 16 next_pc (sign_extend 8 8 addr) in
     91            〈branch addr, [ next_pc; addr ]〉
     92        | _ ⇒ λp. match p in False with [ ]
     93        ] (subaddressing_modein … addr2)
     94      | CJNE addr1 addr2 ⇒
     95        match addr2 return λx. bool_to_Prop (is_in ? [[ relative ]] x) → ? with
     96        [ RELATIVE addr ⇒ λ_.
     97          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 ]〉
     102      ]
     103    | ACALL addr ⇒
     104      match addr return λx. bool_to_Prop (is_in ? [[ addr11 ]] x) → ? with
     105      [ ADDR11 addr ⇒ λ_.
     106        let addr ≝ addr16_of_addr11 pc addr in
     107          〈direct_fun_call addr, [ next_pc ]〉
     108      | _ ⇒ λp. match p in False with [ ]
     109      ] (subaddressing_modein … addr)
     110    | LCALL addr ⇒
     111      match addr return λx. bool_to_Prop (is_in ? [[ addr16 ]] x) → ? with
     112      [ ADDR16 addr ⇒ λ_. 〈direct_fun_call addr, [ next_pc ]〉
     113      | _ ⇒ λp. match p in False with [ ]
     114      ] (subaddressing_modein … addr)
     115    | AJMP addr ⇒
     116      match addr return λx. bool_to_Prop (is_in ? [[ addr11 ]] x) → ? with
     117      [ ADDR11 addr ⇒ λ_.
     118        let addr ≝ addr16_of_addr11 pc addr in
     119          〈goto addr, [ addr ]〉
     120      | _ ⇒ λp. match p in False with [ ]
     121      ] (subaddressing_modein … addr)
     122    | LJMP addr ⇒
     123      match addr return λx. bool_to_Prop (is_in ? [[ addr16 ]] x) → ? with
     124      [ ADDR16 addr ⇒ λ_. 〈goto addr, [ addr ]〉
     125      | _ ⇒ λp. match p in False with [ ]
     126      ] (subaddressing_modein … addr)
     127    | SJMP addr ⇒
     128      match addr return λx. bool_to_Prop (is_in ? [[ relative ]] x) → ? with
     129      [ RELATIVE addr ⇒ λ_.
     130        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 ]〉
     136    ]
     137  in
     138    〈nature, next_pc, next_pcs, inst_cost〉.
     139
     140let rec compare
     141  (a: Type[0]) (the_list: list (a × nat))
     142    on the_list: nat ≝
     143  match the_list with
     144  [ nil ⇒ ⊥ (* XXX: was assert false *)
     145  | cons hd tl ⇒
     146    match tl with
     147    [ nil ⇒
     148      let 〈pc, cost〉 ≝ hd in
     149        cost
     150    | cons hd' tl' ⇒
     151      let 〈pc1, cost1〉 ≝ hd in
     152      let 〈pc2, cost2〉 ≝ hd' in
     153        match eq_nat cost1 cost2 with
     154        [ true ⇒ max cost1 (compare … tl)
     155        | false ⇒ compare … tl'
     156        ]
     157    ]
     158  ].
     159  cases daemon
     160qed.
     161
     162let rec block_cost
     163  (mem: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie Byte 16)
     164    (the_list: list Word) (program_size: nat)
     165      on program_size: nat ≝
     166  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)
     182      ]
     183    ]
     184  ].
     185
     186let rec traverse_code_internal
     187  (program: list Byte) (mem: BitVectorTrie Byte 16)
     188    (cost_labels: BitVectorTrie Byte 16) (pc: Word) (program_size: nat)
     189      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
     200    ]
     201  ].
     202
     203definition traverse_code ≝
     204  λprogram: list Byte.
     205  λmem: BitVectorTrie Byte 16.
     206  λcost_labels.
     207  λprogram_size: nat.
     208    traverse_code_internal program mem cost_labels (zero …) program_size.
     209
     210let rec first_cost_label_internal
     211  (mem: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie Byte 16)
     212    (program_size: nat) (oldpc: Word)
     213      on program_size: (Byte × nat) ≝
     214  match program_size with
     215  [ O ⇒ ⊥ (* XXX: ummm ... ? *)
     216  | S program_size ⇒
     217    match lookup_opt … oldpc cost_labels with
     218    [ None ⇒
     219      let 〈nature, pc, ignore, inst_cost〉 ≝ instruction_info mem oldpc in
     220        match nature with
     221        [ direct_fun_call addr ⇒
     222          let 〈lbl, cost〉 ≝ first_cost_label_internal mem cost_labels program_size addr in
     223            〈lbl, inst_cost + cost〉
     224        | other ⇒
     225          let 〈lbl, cost〉 ≝ first_cost_label_internal mem cost_labels program_size pc in
     226            〈lbl, inst_cost + cost〉
     227        | _ ⇒ ⊥ (* XXX: was assert false in o'caml *)
     228        ]
     229    | Some cost ⇒ 〈cost, 0〉
     230    ]
     231  ].
     232  cases daemon
     233qed.
     234
     235definition first_cost_label ≝
     236  λmem: BitVectorTrie Byte 16.
     237  λcost_labels: BitVectorTrie Byte 16.
     238  λprogram_size: nat.
     239    first_cost_label_internal mem cost_labels program_size (zero …).
     240
     241definition initialize_costs ≝
     242  λmem: BitVectorTrie Byte 16.
     243  λcost_labels: BitVectorTrie Byte 16.
     244  λcost_mapping: BitVectorTrie nat 8.
     245  λprogram_size: nat.
     246  let 〈lbl, cost〉 ≝ first_cost_label mem cost_labels program_size in
     247  let old_cost ≝
     248    match lookup_opt … lbl cost_mapping with
     249    [ None ⇒ 0
     250    | Some cost ⇒ cost
     251    ]
     252  in
     253  let new_cost ≝ old_cost + cost in
     254    insert … lbl new_cost cost_mapping.
     255
     256definition compute_costs ≝
     257  λprogram: list Byte.
     258  λcost_labels: BitVectorTrie Byte 16.
     259  λhas_main: bool.
     260  let program_size ≝ |program| in
     261  let memory ≝ load_code_memory program in
     262  let costs_mapping ≝ traverse_code program memory cost_labels program_size in
     263    match has_main with
     264    [ true ⇒
     265      initialize_costs memory cost_labels costs_mapping program_size
     266    | false ⇒ costs_mapping
     267    ].
Note: See TracChangeset for help on using the changeset viewer.