Changeset 1560 for src/ASM


Ignore:
Timestamp:
Nov 24, 2011, 7:22:13 PM (10 years ago)
Author:
sacerdot
Message:

Complete re-implementation that:

1) assumes no code before the first cost label of main

Note: the preamble of the program is no longer paid by anyone;
but before it was paid every time main was recursively called

2) assumes a cost label as the target of every call/jmp

File:
1 edited

Legend:

Unmodified
Added
Removed

  • src/ASM/ASMCosts.ma

    r1557 r1560  
    33include "ASM/Fetch.ma".
    44include "ASM/Interpret.ma".
     5include "common/StructuredTraces.ma".
    56
    6 inductive 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.
     7definition current_instruction0 ≝
     8  λmem,pc. \fst (\fst (fetch … mem pc)).
    129
     10definition current_instruction ≝
     11 λs:Status. current_instruction0 (code_memory … s) (program_counter … s).
     12
     13definition ASM_classify0: instruction → status_class ≝
     14 λi.
     15  match i with
     16   [ RealInstruction pre ⇒
     17     match pre with
     18      [ RET ⇒ cl_return
     19      | JZ _ ⇒ cl_jump
     20      | JNZ _ ⇒ cl_jump
     21      | JC _ ⇒ cl_jump
     22      | JNC _ ⇒ cl_jump
     23      | JB _ _ ⇒ cl_jump
     24      | JNB _ _ ⇒ cl_jump
     25      | JBC _ _ ⇒ cl_jump
     26      | CJNE _ _ ⇒ cl_jump
     27      | DJNZ _ _ ⇒ cl_jump
     28      | _ ⇒ cl_other
     29      ]
     30   | ACALL _ ⇒ cl_call
     31   | LCALL _ ⇒ cl_call
     32   | JMP _ ⇒ cl_call
     33   | AJMP _ ⇒ cl_jump
     34   | LJMP _ ⇒ cl_jump
     35   | SJMP _ ⇒ cl_jump
     36   | _ ⇒ cl_other
     37   ].
     38
     39definition ASM_classify: Status → status_class ≝
     40 λs.ASM_classify0 (current_instruction s).
     41
     42definition current_instruction_is_labelled ≝
     43  λcost_labels: BitVectorTrie costlabel 16.
     44  λs: Status.
     45  let pc ≝ program_counter … s in
     46    match lookup_opt … pc cost_labels with
     47    [ None ⇒ False
     48    | _    ⇒ True
     49    ].
     50
     51definition label_of_current_instruction:
     52 BitVectorTrie costlabel 16 → Status → list costlabel
     53 ≝
     54  λcost_labels,s.
     55  let pc ≝ program_counter … s in
     56    match lookup_opt … pc cost_labels with
     57    [ None ⇒ []
     58    | Some l ⇒ [l]
     59    ].
     60
     61definition next_instruction_properly_relates_program_counters ≝
     62  λbefore: Status.
     63  λafter : Status.
     64  let size ≝ current_instruction_cost before in
     65  let pc_before ≝ program_counter … before in
     66  let pc_after ≝ program_counter … after in
     67  let sum ≝ \snd (half_add … pc_before (bitvector_of_nat … size)) in
     68    sum = pc_after.
     69
     70definition ASM_abstract_status: BitVectorTrie costlabel 16 → abstract_status ≝
     71 λcost_labels.
     72  mk_abstract_status
     73   Status
     74   (λs,s'. eject … (execute_1 s) = s')
     75   (λs,class. ASM_classify s = class)
     76   (current_instruction_is_labelled cost_labels)
     77   next_instruction_properly_relates_program_counters.
     78
     79(* To be moved in ASM/arithmetic.ma *)
    1380definition addr16_of_addr11: Word → Word11 → Word ≝
    1481  λpc: Word.
    … …  
    2592qed.
    2693
    27 definition 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 
    37 definition instruction_info:
    38     BitVectorTrie Byte 16 → Word → Σprod: (instruction_nature × Word × (list Word) × nat). |\snd (\fst prod)| = instruction_nature_next_pc_length (\fst (\fst (\fst prod))) ≝
    39   λmem.
    40   λpc.
    41   let 〈inst, next_pc, inst_cost〉 ≝ fetch mem pc in
    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
    44     [ RealInstruction ri ⇒
    45       match ri with
    46       [ RET ⇒ dp … 〈ret, [ ]〉 ?
    47       | RETI ⇒ dp … 〈ret, [ ]〉 ?
    48       | JC addr ⇒
    49         match addr return λx. bool_to_Prop (is_in ? [[ relative ]] x) → ? with
    50         [ RELATIVE addr ⇒ λ_.
    51           let 〈carry, addr〉 ≝ half_add … 16 next_pc (sign_extend 8 8 addr) in
    52             dp … 〈branch addr, [ next_pc; addr ]〉 ?
    53         | _ ⇒ λp. match p in False with [ ]
    54         ] (subaddressing_modein … addr)
    55       | JNC addr ⇒
    56         match addr return λx. bool_to_Prop (is_in ? [[ relative ]] x) → ? with
    57         [ RELATIVE addr ⇒ λ_.
    58           let 〈carry, addr〉 ≝ half_add … 16 next_pc (sign_extend 8 8 addr) in
    59             dp … 〈branch addr, [ next_pc; addr ]〉 ?
    60         | _ ⇒ λp. match p in False with [ ]
    61         ] (subaddressing_modein … addr)
    62       | JZ addr ⇒
    63         match addr return λx. bool_to_Prop (is_in ? [[ relative ]] x) → ? with
    64         [ RELATIVE addr ⇒ λ_.
    65           let 〈carry, addr〉 ≝ half_add … 16 next_pc (sign_extend 8 8 addr) in
    66             dp … 〈branch addr, [ next_pc; addr ]〉 ?
    67         | _ ⇒ λp. match p in False with [ ]
    68         ] (subaddressing_modein … addr)
    69       | JNZ addr ⇒
    70         match addr return λx. bool_to_Prop (is_in ? [[ relative ]] x) → ? with
    71         [ RELATIVE addr ⇒ λ_.
    72           let 〈carry, addr〉 ≝ half_add … 16 next_pc (sign_extend 8 8 addr) in
    73             dp … 〈branch addr, [ next_pc; addr ]〉 ?
    74         | _ ⇒ λp. match p in False with [ ]
    75         ] (subaddressing_modein … addr)
    76       | JB addr1 addr2 ⇒
    77         match addr2 return λx. bool_to_Prop (is_in ? [[ relative ]] x) → ? with
    78         [ RELATIVE addr ⇒ λ_.
    79           let 〈carry, addr〉 ≝ half_add … 16 next_pc (sign_extend 8 8 addr) in
    80             dp … 〈branch addr, [ next_pc; addr ]〉 ?
    81         | _ ⇒ λp. match p in False with [ ]
    82         ] (subaddressing_modein … addr2)
    83       | JNB addr1 addr2 ⇒
    84         match addr2 return λx. bool_to_Prop (is_in ? [[ relative ]] x) → ? with
    85         [ RELATIVE addr ⇒ λ_.
    86           let 〈carry, addr〉 ≝ half_add … 16 next_pc (sign_extend 8 8 addr) in
    87             dp … 〈branch addr, [ next_pc; addr ]〉 ?
    88         | _ ⇒ λp. match p in False with [ ]
    89         ] (subaddressing_modein … addr2)
    90       | JBC addr1 addr2 ⇒
    91         match addr2 return λx. bool_to_Prop (is_in ? [[ relative ]] x) → ? with
    92         [ RELATIVE addr ⇒ λ_.
    93           let 〈carry, addr〉 ≝ half_add … 16 next_pc (sign_extend 8 8 addr) in
    94             dp … 〈branch addr, [ next_pc; addr ]〉 ?
    95         | _ ⇒ λp. match p in False with [ ]
    96         ] (subaddressing_modein … addr2)
    97       | DJNZ addr1 addr2 ⇒
    98         match addr2 return λx. bool_to_Prop (is_in ? [[ relative ]] x) → ? with
    99         [ RELATIVE addr ⇒ λ_.
    100           let 〈carry, addr〉 ≝ half_add … 16 next_pc (sign_extend 8 8 addr) in
    101             dp … 〈branch addr, [ next_pc; addr ]〉 ?
    102         | _ ⇒ λp. match p in False with [ ]
    103         ] (subaddressing_modein … addr2)
    104       | CJNE addr1 addr2 ⇒
    105         match addr2 return λx. bool_to_Prop (is_in ? [[ relative ]] x) → ? with
    106         [ RELATIVE addr ⇒ λ_.
    107           let 〈carry, addr〉 ≝ half_add … 16 next_pc (sign_extend 8 8 addr) in
    108             dp … 〈branch addr, [ next_pc; addr ]〉 ?
    109         | _ ⇒ λp. match p in False with [ ]
    110         ] (subaddressing_modein … addr2)
    111       | _ ⇒ dp … 〈other, [ next_pc ]〉 ?
    112       ]
    113     | ACALL addr ⇒
    114       match addr return λx. bool_to_Prop (is_in ? [[ addr11 ]] x) → ? with
    115       [ ADDR11 addr ⇒ λ_.
    116         let addr ≝ addr16_of_addr11 pc addr in
    117           dp … 〈direct_fun_call addr, [ next_pc ]〉 ?
    118       | _ ⇒ λp. match p in False with [ ]
    119       ] (subaddressing_modein … addr)
    120     | LCALL addr ⇒
    121       match addr return λx. bool_to_Prop (is_in ? [[ addr16 ]] x) → ? with
    122       [ ADDR16 addr ⇒ λ_. dp … 〈direct_fun_call addr, [ next_pc ]〉 ?
    123       | _ ⇒ λp. match p in False with [ ]
    124       ] (subaddressing_modein … addr)
    125     | AJMP addr ⇒
    126       match addr return λx. bool_to_Prop (is_in ? [[ addr11 ]] x) → ? with
    127       [ ADDR11 addr ⇒ λ_.
    128         let addr ≝ addr16_of_addr11 pc addr in
    129           dp … 〈goto addr, [ addr ]〉 ?
    130       | _ ⇒ λp. match p in False with [ ]
    131       ] (subaddressing_modein … addr)
    132     | LJMP addr ⇒
    133       match addr return λx. bool_to_Prop (is_in ? [[ addr16 ]] x) → ? with
    134       [ ADDR16 addr ⇒ λ_. dp … 〈goto addr, [ addr ]〉 ?
    135       | _ ⇒ λp. match p in False with [ ]
    136       ] (subaddressing_modein … addr)
    137     | SJMP addr ⇒
    138       match addr return λx. bool_to_Prop (is_in ? [[ relative ]] x) → ? with
    139       [ RELATIVE addr ⇒ λ_.
    140         let 〈carry, addr〉 ≝ half_add 16 next_pc (sign_extend 8 8 addr) in
    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 ]〉 ?
    146     ]
    147   in
    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   ]
    157 qed.
    158 
    159 let rec block_cost'
     94let rec block_cost
    16095  (mem: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie costlabel 16)
    161     (program_counter: Word) (program_size: nat) (cost_so_far: nat)
    162       on program_size ≝
     96    (pc: Word) (program_size: nat) on program_size : nat ≝
    16397  match program_size with
    16498  [ O ⇒ 0
    165   | S program_size ⇒       
    166     let sigma ≝ instruction_info mem program_counter in
    167       match sigma with
    168       [ dp variety_costs their_proof ⇒
    169         let variety ≝ \fst (\fst (\fst variety_costs)) in
    170         let next_pc ≝ \snd (\fst (\fst variety_costs)) in
    171         let next_pcs ≝ \snd (\fst variety_costs) in
    172         let inst_cost ≝ \snd variety_costs in
    173           match variety return λx. |next_pcs| = instruction_nature_next_pc_length x → nat with
    174           [ other ⇒ λproof.
    175             match next_pcs return λx. |x| = 1 → nat with
    176             [ nil ⇒ λabsurd. ⊥
    177             | cons hd tl ⇒ λproof.
    178               match lookup_opt … hd cost_labels with
    179               [ None ⇒ block_cost' mem cost_labels hd program_size (cost_so_far + inst_cost)
    180               | Some _ ⇒ inst_cost + cost_so_far
    181               ]
    182             ] proof
    183           | _ ⇒ λ_. inst_cost + cost_so_far
    184           ] their_proof
    185       ]
    186   ].
    187   normalize in absurd;
    188   destruct(absurd)
    189 qed.
    190 
    191 definition block_cost ≝
    192   λmem: BitVectorTrie Byte 16.
    193   λcost_labels: BitVectorTrie costlabel 16.
    194   λprogram_counter: Word.
    195   λprogram_size: nat.
    196     block_cost' mem cost_labels program_counter program_size 0.
     99  | S program_size ⇒
     100    let 〈instr,newpc,ticks〉 ≝ fetch … mem pc in
     101    match lookup_opt … newpc cost_labels with
     102     [ None ⇒
     103        match ASM_classify0 instr with
     104         [ cl_jump ⇒ ticks
     105         | cl_call ⇒ ticks + block_cost mem cost_labels newpc program_size
     106         | cl_return ⇒ ticks
     107         | cl_other ⇒ ticks + block_cost mem cost_labels newpc program_size
     108         ]
     109     | Some _ ⇒ ticks ]].
    197110
    198111let rec traverse_code_internal
    … …  
    200113    (cost_labels: BitVectorTrie costlabel 16) (pc: Word) (program_size: nat)
    201114      on program: identifier_map CostTag nat ≝
    202   match instruction_info mem pc with
    203   [ dp info proof ⇒
    204     let newpc ≝ \snd (\fst (\fst info)) in
    205     match program with
    206     [ nil ⇒ empty_map …
    207     | cons hd tl ⇒
    208       match lookup_opt … pc cost_labels with
    209       [ None ⇒ traverse_code_internal tl mem cost_labels newpc program_size
    210       | Some lbl ⇒
    211         let cost ≝ block_cost mem cost_labels pc program_size in
    212         let cost_mapping ≝ traverse_code_internal tl mem cost_labels newpc program_size in
    213           add … cost_mapping lbl cost
    214       ]
    215     ]
    216   ].
     115 let 〈instr,newpc,ticks〉 ≝ fetch … mem pc in
     116 match program with
     117 [ nil ⇒ empty_map …
     118 | cons hd tl ⇒
     119   match lookup_opt … pc cost_labels with
     120   [ None ⇒ traverse_code_internal tl mem cost_labels newpc program_size
     121   | Some lbl ⇒
     122     let cost ≝ block_cost mem cost_labels pc program_size in
     123     let cost_mapping ≝ traverse_code_internal tl mem cost_labels newpc program_size in
     124       add … cost_mapping lbl cost ]].
    217125
    218126definition traverse_code ≝
    … …  
    223131    traverse_code_internal program mem cost_labels (zero …) program_size.
    224132
    225 let rec first_cost_label_internal
    226   (mem: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie costlabel 16)
    227     (program_size: nat) (oldpc: Word)
    228       on program_size: (costlabel × nat) ≝
    229   match program_size with
    230   [ O ⇒ ⊥ (* XXX: ummm ... ? *)
    231   | S program_size ⇒
    232     match lookup_opt … oldpc cost_labels with
    233     [ None ⇒
    234       match instruction_info mem oldpc with
    235       [ dp info proof ⇒
    236         let nature ≝ \fst (\fst (\fst info)) in
    237         let pc ≝ \snd (\fst (\fst info)) in
    238         let inst_cost ≝ \snd info in
    239         match nature with
    240         [ direct_fun_call addr ⇒
    241           let 〈lbl, cost〉 ≝ first_cost_label_internal mem cost_labels program_size addr in
    242             〈lbl, inst_cost + cost〉
    243         | other ⇒
    244           let 〈lbl, cost〉 ≝ first_cost_label_internal mem cost_labels program_size pc in
    245             〈lbl, inst_cost + cost〉
    246         | _ ⇒ ⊥ (* XXX: was assert false in o'caml *)
    247         ]
    248       ]
    249     | Some cost ⇒ 〈cost, 0〉
    250     ]
    251   ].
    252   cases daemon
    253 qed.
    254 
    255 definition first_cost_label ≝
    256   λmem: BitVectorTrie Byte 16.
    257   λcost_labels: BitVectorTrie costlabel 16.
    258   λprogram_size: nat.
    259     first_cost_label_internal mem cost_labels program_size (zero …).
    260 
    261 definition initialize_costs ≝
    262   λmem: BitVectorTrie Byte 16.
    263   λcost_labels: BitVectorTrie costlabel 16.
    264   λcost_mapping: identifier_map CostTag nat.
    265   λprogram_size: nat.
    266   let 〈lbl, cost〉 ≝ first_cost_label mem cost_labels program_size in
    267   let old_cost ≝
    268     match lookup ?? cost_mapping lbl with
    269     [ None ⇒ 0
    270     | Some cost ⇒ cost
    271     ]
    272   in
    273   let new_cost ≝ old_cost + cost in
    274     add … cost_mapping lbl new_cost.
    275 
    276133definition compute_costs ≝
    277134  λprogram: list Byte.
    … …  
    280137  let program_size ≝ |program| in
    281138  let memory ≝ load_code_memory program in
    282   let costs_mapping ≝ traverse_code program memory cost_labels program_size in
    283     match has_main with
    284     [ true ⇒ initialize_costs memory cost_labels costs_mapping program_size
    285     | false ⇒ costs_mapping
    286     ].
     139   traverse_code program memory cost_labels program_size.
Note: See TracChangeset for help on using the changeset viewer.