Ignore:
Timestamp:
Nov 4, 2011, 5:01:39 PM (8 years ago)
Author:
mulligan
Message:

finished well labeled check, up to injectivity of the label map

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/WellLabeled.ma

    r1487 r1493  
    33include "ASM/Arithmetic.ma".
    44
     5let rec member_p
     6  (a: Type[0]) (eq: a → a → bool) (element: a) (the_list: list a)
     7    on the_list: Prop ≝
     8  match the_list with
     9  [ nil ⇒ False
     10  | cons hd tl ⇒
     11    match eq hd element with
     12    [ true ⇒ True
     13    | false ⇒ member_p … eq element tl
     14    ]
     15  ].
     16
    517definition well_labelled_p ≝
    618  ∀pc: Word.
     19  ∀dptr: Word.
     20  ∀acc_a: Byte.
     21  ∀function_locations: list Word.
    722  ∀program: BitVectorTrie Byte 16.
    823  ∀cost_labels.
    924    let 〈instruction, newpc, cost〉 ≝ fetch program pc in
    1025      match instruction with
    11       [ LCALL lcall ⇒ ?
    12       | ACALL acall ⇒ ?
     26      [ LCALL lcall ⇒
     27        match lcall return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → ? with
     28        [ ADDR16 addr16 ⇒ λ_. member_p … (eq_bv …) addr16 function_locations
     29        | _ ⇒ λabsurd. ⊥
     30        ] (subaddressing_modein … lcall)
     31      | ACALL acall ⇒
     32        match acall return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → ? with
     33        [ ADDR11 addr11 ⇒ λ_.
     34          let 〈pc_bu, pc_bl〉 ≝ split … 8 8 pc in
     35          let 〈thr, eig〉 ≝ split … 3 8 addr11 in
     36          let 〈fiv, thr'〉 ≝ split … 5 3 pc_bu in
     37          let new_pc ≝ (fiv @@ thr) @@ pc_bl in
     38            match lookup_opt … new_pc cost_labels with
     39            [ None ⇒ False
     40            | _    ⇒ True
     41            ]
     42        | _ ⇒ λabsurd. ⊥
     43        ] (subaddressing_modein … acall)
    1344      | AJMP ajmp ⇒
    1445        match ajmp return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → ? with
     
    2455            | _    ⇒ True
    2556            ]
    26         | _ ⇒ λ_. ⊥
     57        | _ ⇒ λabsurd. ⊥
    2758        ] (subaddressing_modein … ajmp)
    2859      | LJMP ljmp ⇒
     
    3364          | _    ⇒ True
    3465          ]
    35         | _ ⇒ λ_. ⊥
     66        | _ ⇒ λabsurd. ⊥
    3667        ] (subaddressing_modein … ljmp)
    3768      | SJMP sjmp ⇒
     
    4374            | _    ⇒ True
    4475            ]
    45         | _ ⇒ λ_. ⊥
     76        | _ ⇒ λabsurd. ⊥
    4677        ] (subaddressing_modein … sjmp)
    47       | JMP jmp ⇒ ?
     78      | JMP jmp ⇒
     79        let big_acc_a ≝ (zero 8) @@ acc_a in
     80        let 〈carry, jmp_addr〉 ≝ half_add … big_acc_a dptr in
     81        let 〈carry, new_pc〉 ≝ half_add … pc jmp_addr in
     82          match lookup_opt … new_pc cost_labels with
     83          [ None ⇒ False
     84          | _    ⇒ True
     85          ]
    4886      | MOVC _ _ ⇒ True
    4987      | RealInstruction instruction ⇒
    5088        match instruction with
    51         [ JZ jz ⇒ ?
    52         | _ ⇒ ?
     89        [ JZ jz ⇒
     90          match jz return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
     91          [ RELATIVE rel ⇒ λ_.
     92            let 〈carry, new_pc〉 ≝ half_add … pc (sign_extend 8 8 rel) in
     93              match lookup_opt … new_pc cost_labels with
     94              [ None ⇒ False
     95              | _    ⇒ True
     96              ]
     97          | _ ⇒ λabsurd. ⊥
     98          ] (subaddressing_modein … jz)
     99        | JNZ jnz ⇒
     100          match jnz return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
     101          [ RELATIVE rel ⇒ λ_.
     102            let 〈carry, new_pc〉 ≝ half_add … pc (sign_extend 8 8 rel) in
     103              match lookup_opt … new_pc cost_labels with
     104              [ None ⇒ False
     105              | _    ⇒ True
     106              ]
     107          | _ ⇒ λabsurd. ⊥
     108          ] (subaddressing_modein … jnz)
     109        | JC jc ⇒
     110          match jc return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
     111          [ RELATIVE rel ⇒ λ_.
     112            let 〈carry, new_pc〉 ≝ half_add … pc (sign_extend 8 8 rel) in
     113              match lookup_opt … new_pc cost_labels with
     114              [ None ⇒ False
     115              | _    ⇒ True
     116              ]
     117          | _ ⇒ λabsurd. ⊥
     118          ] (subaddressing_modein … jc)
     119        | JNC jnc ⇒
     120          match jnc return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
     121          [ RELATIVE rel ⇒ λ_.
     122            let 〈carry, new_pc〉 ≝ half_add … pc (sign_extend 8 8 rel) in
     123              match lookup_opt … new_pc cost_labels with
     124              [ None ⇒ False
     125              | _    ⇒ True
     126              ]
     127          | _ ⇒ λabsurd. ⊥
     128          ] (subaddressing_modein … jnc)
     129        | JB baddr jb ⇒
     130          match jb return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
     131          [ RELATIVE rel ⇒ λ_.
     132            let 〈carry, new_pc〉 ≝ half_add … pc (sign_extend 8 8 rel) in
     133              match lookup_opt … new_pc cost_labels with
     134              [ None ⇒ False
     135              | _    ⇒ True
     136              ]
     137          | _ ⇒ λabsurd. ⊥
     138          ] (subaddressing_modein … jb)
     139        | JNB baddr jnb ⇒
     140          match jnb return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
     141          [ RELATIVE rel ⇒ λ_.
     142            let 〈carry, new_pc〉 ≝ half_add … pc (sign_extend 8 8 rel) in
     143              match lookup_opt … new_pc cost_labels with
     144              [ None ⇒ False
     145              | _    ⇒ True
     146              ]
     147          | _ ⇒ λabsurd. ⊥
     148          ] (subaddressing_modein … jnb)
     149        | JBC baddr jbc ⇒
     150          match jbc return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
     151          [ RELATIVE rel ⇒ λ_.
     152            let 〈carry, new_pc〉 ≝ half_add … pc (sign_extend 8 8 rel) in
     153              match lookup_opt … new_pc cost_labels with
     154              [ None ⇒ False
     155              | _    ⇒ True
     156              ]
     157          | _ ⇒ λabsurd. ⊥
     158          ] (subaddressing_modein … jbc)
     159        | CJNE args cjne ⇒
     160          match cjne return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
     161          [ RELATIVE rel ⇒ λ_.
     162            let 〈carry, new_pc〉 ≝ half_add … pc (sign_extend 8 8 rel) in
     163              match lookup_opt … new_pc cost_labels with
     164              [ None ⇒ False
     165              | _    ⇒ True
     166              ]
     167          | _ ⇒ λabsurd. ⊥
     168          ] (subaddressing_modein … cjne)
     169        | DJNZ args djnz ⇒
     170          match djnz return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
     171          [ RELATIVE rel ⇒ λ_.
     172            let 〈carry, new_pc〉 ≝ half_add … pc (sign_extend 8 8 rel) in
     173              match lookup_opt … new_pc cost_labels with
     174              [ None ⇒ False
     175              | _    ⇒ True
     176              ]
     177          | _ ⇒ λabsurd. ⊥
     178          ] (subaddressing_modein … djnz)
     179        | _ ⇒ True
    53180        ]
    54181      ].
     182  [*: normalize in absurd; // ]
     183qed.
Note: See TracChangeset for help on using the changeset viewer.