Changeset 1615 for src/ASM/Assembly.ma


Ignore:
Timestamp:
Dec 14, 2011, 5:28:11 PM (8 years ago)
Author:
sacerdot
Message:

Policy now depends on Assembly and not the other way around.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Assembly.ma

    r1614 r1615  
    66include alias "arithmetics/nat.ma".
    77include "utilities/extralib.ma".
    8 include "ASM/Policy.ma".
    98
    109(**************************************** START OF POLICY ABSTRACTION ********************)
    1110
     11(* definition of & operations on jump length *)
     12inductive jump_length: Type[0] ≝
     13  | short_jump: jump_length
     14  | medium_jump: jump_length
     15  | long_jump: jump_length.
     16
    1217definition policy_type ≝ Word → jump_length.
    1318
    14 definition jump_expansion':
    15  ∀program:preamble × (Σl:list labelled_instruction.|l| < 2^16).
    16  policy_type ≝
    17  λprogram.λpc.
    18   let policy ≝
    19     transform_policy (|\snd program|) (pi1 … (je_fixpoint (\snd program))) (Stub ??) in
    20   lookup ? ? pc policy long_jump.
    21 /2 by Stub, mk_Sig/
    22 qed.
     19definition assembly_preinstruction ≝
     20  λA: Type[0].
     21  λaddr_of: A → Byte. (* relative *)
     22  λpre: preinstruction A.
     23  match pre with
     24  [ ADD addr1 addr2 ⇒
     25     match addr2 return λx. bool_to_Prop (is_in ? [[registr;direct;indirect;data]] x) → ? with
     26      [ REGISTER r ⇒ λ_.[ ([[false;false;true;false;true]]) @@ r ]
     27      | DIRECT b1 ⇒ λ_.[ ([[false;false;true;false;false;true;false;true]]); b1 ]
     28      | INDIRECT i1 ⇒ λ_. [ ([[false;false;true;false;false;true;true;i1]]) ]
     29      | DATA b1 ⇒ λ_. [ ([[false;false;true;false;false;true;false;false]]) ; b1 ]
     30      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
     31  | ADDC addr1 addr2 ⇒
     32     match addr2 return λx. bool_to_Prop (is_in ? [[registr;direct;indirect;data]] x) → ? with
     33      [ REGISTER r ⇒ λ_.[ ([[false;false;true;true;true]]) @@ r ]
     34      | DIRECT b1 ⇒ λ_.[ ([[false;false;true;true;false;true;false;true]]); b1 ]
     35      | INDIRECT i1 ⇒ λ_. [ ([[false;false;true;true;false;true;true;i1]]) ]
     36      | DATA b1 ⇒ λ_. [ ([[false;false;true;true;false;true;false;false]]) ; b1 ]
     37      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
     38  | ANL addrs ⇒
     39     match addrs with
     40      [ inl addrs ⇒ match addrs with
     41         [ inl addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
     42           match addr2 return λx. bool_to_Prop (is_in ? [[registr;direct;indirect;data]] x) → ? with
     43            [ REGISTER r ⇒ λ_.[ ([[false;true;false;true;true]]) @@ r ]
     44            | DIRECT b1 ⇒ λ_.[ ([[false;true;false;true;false;true;false;true]]); b1 ]
     45            | INDIRECT i1 ⇒ λ_. [ ([[false;true;false;true;false;true;true;i1]]) ]
     46            | DATA b1 ⇒ λ_. [ ([[false;true;false;true;false;true;false;false]]) ; b1 ]
     47            | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
     48         | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
     49            let b1 ≝
     50             match addr1 return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with
     51              [ DIRECT b1 ⇒ λ_.b1
     52              | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1) in
     53            match addr2 return λx. bool_to_Prop (is_in ? [[acc_a;data]] x) → ? with
     54             [ ACC_A ⇒ λ_.[ ([[false;true;false;true;false;false;true;false]]) ; b1 ]
     55             | DATA b2 ⇒ λ_. [ ([[false;true;false;true;false;false;true;true]]) ; b1 ; b2 ]
     56             | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
     57         ]
     58      | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
     59         match addr2 return λx. bool_to_Prop (is_in ? [[bit_addr;n_bit_addr]] x) → ? with
     60          [ BIT_ADDR b1 ⇒ λ_.[ ([[true;false;false;false;false;false;true;false]]) ; b1 ]
     61          | N_BIT_ADDR b1 ⇒ λ_. [ ([[true;false;true;true;false;false;false;false]]) ; b1 ]
     62          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]
     63  | CLR addr ⇒
     64     match addr return λx. bool_to_Prop (is_in ? [[acc_a;carry;bit_addr]] x) → ? with
     65      [ ACC_A ⇒ λ_.
     66         [ ([[true; true; true; false; false; true; false; false]]) ]
     67      | CARRY ⇒ λ_.
     68         [ ([[true; true; false; false; false; false; true; true]]) ]
     69      | BIT_ADDR b1 ⇒ λ_.
     70         [ ([[true; true; false; false; false; false; true; false]]) ; b1 ]
     71      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
     72  | CPL addr ⇒
     73     match addr return λx. bool_to_Prop (is_in ? [[acc_a;carry;bit_addr]] x) → ? with
     74      [ ACC_A ⇒ λ_.
     75         [ ([[true; true; true; true; false; true; false; false]]) ]
     76      | CARRY ⇒ λ_.
     77         [ ([[true; false; true; true; false; false; true; true]]) ]
     78      | BIT_ADDR b1 ⇒ λ_.
     79         [ ([[true; false; true; true; false; false; true; false]]) ; b1 ]
     80      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
     81  | DA addr ⇒
     82     [ ([[true; true; false; true; false; true; false; false]]) ]
     83  | DEC addr ⇒
     84     match addr return λx. bool_to_Prop (is_in ? [[acc_a;registr;direct;indirect]] x) → ? with
     85      [ ACC_A ⇒ λ_.
     86         [ ([[false; false; false; true; false; true; false; false]]) ]
     87      | REGISTER r ⇒ λ_.
     88         [ ([[false; false; false; true; true]]) @@ r ]
     89      | DIRECT b1 ⇒ λ_.
     90         [ ([[false; false; false; true; false; true; false; true]]); b1 ]
     91      | INDIRECT i1 ⇒ λ_.
     92         [ ([[false; false; false; true; false; true; true; i1]]) ]
     93      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
     94      | DJNZ addr1 addr2 ⇒
     95         let b2 ≝ addr_of addr2 in
     96         match addr1 return λx. bool_to_Prop (is_in ? [[registr;direct]] x) → ? with
     97          [ REGISTER r ⇒ λ_.
     98             [ ([[true; true; false; true; true]]) @@ r ; b2 ]
     99          | DIRECT b1 ⇒ λ_.
     100             [ ([[true; true; false; true; false; true; false; true]]); b1; b2 ]
     101          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)
     102      | JC addr ⇒
     103        let b1 ≝ addr_of addr in
     104          [ ([[false; true; false; false; false; false; false; false]]); b1 ]
     105      | JNC addr ⇒
     106         let b1 ≝ addr_of addr in
     107           [ ([[false; true; false; true; false; false; false; false]]); b1 ]
     108      | JZ addr ⇒
     109         let b1 ≝ addr_of addr in
     110           [ ([[false; true; true; false; false; false; false; false]]); b1 ]
     111      | JNZ addr ⇒
     112         let b1 ≝ addr_of addr in
     113           [ ([[false; true; true; true; false; false; false; false]]); b1 ]
     114      | JB addr1 addr2 ⇒
     115         let b2 ≝ addr_of addr2 in
     116         match addr1 return λx. bool_to_Prop (is_in ? [[bit_addr]] x) → ? with
     117          [ BIT_ADDR b1 ⇒ λ_.
     118             [ ([[false; false; true; false; false; false; false; false]]); b1; b2 ]
     119          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)
     120      | JNB addr1 addr2 ⇒
     121         let b2 ≝ addr_of addr2 in
     122         match addr1 return λx. bool_to_Prop (is_in ? [[bit_addr]] x) → ? with
     123          [ BIT_ADDR b1 ⇒ λ_.
     124             [ ([[false; false; true; true; false; false; false; false]]); b1; b2 ]
     125          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)
     126      | JBC addr1 addr2 ⇒
     127         let b2 ≝ addr_of addr2 in
     128         match addr1 return λx. bool_to_Prop (is_in ? [[bit_addr]] x) → ? with
     129          [ BIT_ADDR b1 ⇒ λ_.
     130             [ ([[false; false; false; true; false; false; false; false]]); b1; b2 ]
     131          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)
     132      | CJNE addrs addr3 ⇒
     133         let b3 ≝ addr_of addr3 in
     134         match addrs with
     135          [ inl addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
     136             match addr2 return λx. bool_to_Prop (is_in ? [[direct;data]] x) → ? with
     137              [ DIRECT b1 ⇒ λ_.
     138                 [ ([[true; false; true; true; false; true; false; true]]); b1; b3 ]
     139              | DATA b1 ⇒ λ_.
     140                 [ ([[true; false; true; true; false; true; false; false]]); b1; b3 ]
     141              | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
     142          | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
     143             let b2 ≝
     144              match addr2 return λx. bool_to_Prop (is_in ? [[data]] x) → ? with
     145               [ DATA b2 ⇒ λ_. b2
     146               | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) in
     147             match addr1 return λx. bool_to_Prop (is_in ? [[registr;indirect]] x) → list Byte with
     148              [ REGISTER r ⇒ λ_.
     149                 [ ([[true; false; true; true; true]]) @@ r; b2; b3 ]
     150              | INDIRECT i1 ⇒ λ_.
     151                 [ ([[true; false; true; true; false; true; true; i1]]); b2; b3 ]
     152              | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)
     153         ]
     154  | DIV addr1 addr2 ⇒
     155     [ ([[true;false;false;false;false;true;false;false]]) ]
     156  | INC addr ⇒
     157     match addr return λx. bool_to_Prop (is_in ? [[acc_a;registr;direct;indirect;dptr]] x) → ? with
     158      [ ACC_A ⇒ λ_.
     159         [ ([[false;false;false;false;false;true;false;false]]) ]         
     160      | REGISTER r ⇒ λ_.
     161         [ ([[false;false;false;false;true]]) @@ r ]
     162      | DIRECT b1 ⇒ λ_.
     163         [ ([[false; false; false; false; false; true; false; true]]); b1 ]
     164      | INDIRECT i1 ⇒ λ_.
     165        [ ([[false; false; false; false; false; true; true; i1]]) ]
     166      | DPTR ⇒ λ_.
     167        [ ([[true;false;true;false;false;false;true;true]]) ]
     168      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
     169  | MOV addrs ⇒
     170     match addrs with
     171      [ inl addrs ⇒
     172         match addrs with
     173          [ inl addrs ⇒
     174             match addrs with
     175              [ inl addrs ⇒
     176                 match addrs with
     177                  [ inl addrs ⇒
     178                     match addrs with
     179                      [ inl addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
     180                         match addr2 return λx. bool_to_Prop (is_in ? [[registr;direct;indirect;data]] x) → ? with
     181                          [ REGISTER r ⇒ λ_.[ ([[true;true;true;false;true]]) @@ r ]
     182                          | DIRECT b1 ⇒ λ_.[ ([[true;true;true;false;false;true;false;true]]); b1 ]
     183                          | INDIRECT i1 ⇒ λ_. [ ([[true;true;true;false;false;true;true;i1]]) ]
     184                          | DATA b1 ⇒ λ_. [ ([[false;true;true;true;false;true;false;false]]) ; b1 ]
     185                          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
     186                      | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
     187                         match addr1 return λx. bool_to_Prop (is_in ? [[registr;indirect]] x) → ? with
     188                          [ REGISTER r ⇒ λ_.
     189                             match addr2 return λx. bool_to_Prop (is_in ? [[acc_a;direct;data]] x) → ? with
     190                              [ ACC_A ⇒ λ_.[ ([[true;true;true;true;true]]) @@ r ]
     191                              | DIRECT b1 ⇒ λ_.[ ([[true;false;true;false;true]]) @@ r; b1 ]
     192                              | DATA b1 ⇒ λ_. [ ([[false;true;true;true;true]]) @@ r; b1 ]
     193                              | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
     194                          | INDIRECT i1 ⇒ λ_.
     195                             match addr2 return λx. bool_to_Prop (is_in ? [[acc_a;direct;data]] x) → ? with
     196                              [ ACC_A ⇒ λ_.[ ([[true;true;true;true;false;true;true;i1]]) ]
     197                              | DIRECT b1 ⇒ λ_.[ ([[true;false;true;false;false;true;true;i1]]); b1 ]
     198                              | DATA b1 ⇒ λ_. [ ([[false;true;true;true;false;true;true;i1]]) ; b1 ]
     199                              | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
     200                          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)]
     201                  | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
     202                     let b1 ≝
     203                      match addr1 return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with
     204                       [ DIRECT b1 ⇒ λ_. b1
     205                       | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1) in
     206                     match addr2 return λx. bool_to_Prop (is_in ? [[acc_a;registr;direct;indirect;data]] x) → ? with
     207                      [ ACC_A ⇒ λ_.[ ([[true;true;true;true;false;true;false;true]]); b1]
     208                      | REGISTER r ⇒ λ_.[ ([[true;false;false;false;true]]) @@ r; b1 ]
     209                      | DIRECT b2 ⇒ λ_.[ ([[true;false;false;false;false;true;false;true]]); b1; b2 ]
     210                      | INDIRECT i1 ⇒ λ_. [ ([[true;false;false;false;false;true;true;i1]]); b1 ]
     211                      | DATA b2 ⇒ λ_. [ ([[false;true;true;true;false;true;false;true]]); b1; b2 ]
     212                      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]
     213              | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
     214                 match addr2 return λx. bool_to_Prop (is_in ? [[data16]] x) → ? with
     215                  [ DATA16 w ⇒ λ_.
     216                     let b1_b2 ≝ split ? 8 8 w in
     217                     let b1 ≝ \fst b1_b2 in
     218                     let b2 ≝ \snd b1_b2 in
     219                      [ ([[true;false;false;true;false;false;false;false]]); b1; b2]
     220                  | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]
     221          | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
     222             match addr2 return λx. bool_to_Prop (is_in ? [[bit_addr]] x) → ? with
     223              [ BIT_ADDR b1 ⇒ λ_.
     224                 [ ([[true;false;true;false;false;false;true;false]]); b1 ]
     225              | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]
     226      | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
     227         match addr1 return λx. bool_to_Prop (is_in ? [[bit_addr]] x) → ? with
     228          [ BIT_ADDR b1 ⇒ λ_.
     229             [ ([[true;false;false;true;false;false;true;false]]); b1 ]
     230          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)]
     231  | MOVX addrs ⇒
     232     match addrs with
     233      [ inl addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
     234         match addr2 return λx. bool_to_Prop (is_in ? [[ext_indirect;ext_indirect_dptr]] x) → ? with
     235          [ EXT_INDIRECT i1 ⇒ λ_.
     236             [ ([[true;true;true;false;false;false;true;i1]]) ]
     237          | EXT_INDIRECT_DPTR ⇒ λ_.
     238             [ ([[true;true;true;false;false;false;false;false]]) ]
     239          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
     240      | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
     241         match addr1 return λx. bool_to_Prop (is_in ? [[ext_indirect;ext_indirect_dptr]] x) → ? with
     242          [ EXT_INDIRECT i1 ⇒ λ_.
     243             [ ([[true;true;true;true;false;false;true;i1]]) ]
     244          | EXT_INDIRECT_DPTR ⇒ λ_.
     245             [ ([[true;true;true;true;false;false;false;false]]) ]
     246          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)]
     247  | MUL addr1 addr2 ⇒
     248     [ ([[true;false;true;false;false;true;false;false]]) ]
     249  | NOP ⇒
     250     [ ([[false;false;false;false;false;false;false;false]]) ]
     251  | ORL addrs ⇒
     252     match addrs with
     253      [ inl addrs ⇒
     254         match addrs with
     255          [ inl addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
     256             match addr2 return λx. bool_to_Prop (is_in ? [[registr;data;direct;indirect]] x) → ? with
     257             [ REGISTER r ⇒ λ_.[ ([[false;true;false;false;true]]) @@ r ]
     258             | DIRECT b1 ⇒ λ_.[ ([[false;true;false;false;false;true;false;true]]); b1 ]
     259             | INDIRECT i1 ⇒ λ_. [ ([[false;true;false;false;false;true;true;i1]]) ]
     260             | DATA b1 ⇒ λ_. [ ([[false;true;false;false;false;true;false;false]]) ; b1 ]
     261             | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
     262          | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
     263            let b1 ≝
     264              match addr1 return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with
     265               [ DIRECT b1 ⇒ λ_. b1
     266               | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1) in
     267             match addr2 return λx. bool_to_Prop (is_in ? [[acc_a;data]] x) → ? with
     268              [ ACC_A ⇒ λ_.
     269                 [ ([[false;true;false;false;false;false;true;false]]); b1 ]
     270              | DATA b2 ⇒ λ_.
     271                 [ ([[false;true;false;false;false;false;true;true]]); b1; b2 ]
     272              | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]
     273      | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in     
     274         match addr2 return λx. bool_to_Prop (is_in ? [[bit_addr;n_bit_addr]] x) → ? with
     275          [ BIT_ADDR b1 ⇒ λ_.
     276             [ ([[false;true;true;true;false;false;true;false]]); b1 ]
     277          | N_BIT_ADDR b1 ⇒ λ_.
     278             [ ([[true;false;true;false;false;false;false;false]]); b1 ]
     279          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]
     280  | POP addr ⇒
     281     match addr return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with
     282      [ DIRECT b1 ⇒ λ_.
     283         [ ([[true;true;false;true;false;false;false;false]]) ; b1 ]
     284      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
     285  | PUSH addr ⇒
     286     match addr return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with
     287      [ DIRECT b1 ⇒ λ_.
     288         [ ([[true;true;false;false;false;false;false;false]]) ; b1 ]
     289      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
     290  | RET ⇒
     291     [ ([[false;false;true;false;false;false;true;false]]) ]
     292  | RETI ⇒
     293     [ ([[false;false;true;true;false;false;true;false]]) ]
     294  | RL addr ⇒
     295     [ ([[false;false;true;false;false;false;true;true]]) ]
     296  | RLC addr ⇒
     297     [ ([[false;false;true;true;false;false;true;true]]) ]
     298  | RR addr ⇒
     299     [ ([[false;false;false;false;false;false;true;true]]) ]
     300  | RRC addr ⇒
     301     [ ([[false;false;false;true;false;false;true;true]]) ]
     302  | SETB addr ⇒     
     303     match addr return λx. bool_to_Prop (is_in ? [[carry;bit_addr]] x) → ? with
     304      [ CARRY ⇒ λ_.
     305         [ ([[true;true;false;true;false;false;true;true]]) ]
     306      | BIT_ADDR b1 ⇒ λ_.
     307         [ ([[true;true;false;true;false;false;true;false]]); b1 ]
     308      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
     309  | SUBB addr1 addr2 ⇒
     310     match addr2 return λx. bool_to_Prop (is_in ? [[registr;direct;indirect;data]] x) → ? with
     311      [ REGISTER r ⇒ λ_.
     312         [ ([[true;false;false;true;true]]) @@ r ]
     313      | DIRECT b1 ⇒ λ_.
     314         [ ([[true;false;false;true;false;true;false;true]]); b1]
     315      | INDIRECT i1 ⇒ λ_.
     316         [ ([[true;false;false;true;false;true;true;i1]]) ]
     317      | DATA b1 ⇒ λ_.
     318         [ ([[true;false;false;true;false;true;false;false]]); b1]
     319      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
     320  | SWAP addr ⇒
     321     [ ([[true;true;false;false;false;true;false;false]]) ]
     322  | XCH addr1 addr2 ⇒
     323     match addr2 return λx. bool_to_Prop (is_in ? [[registr;direct;indirect]] x) → ? with
     324      [ REGISTER r ⇒ λ_.
     325         [ ([[true;true;false;false;true]]) @@ r ]
     326      | DIRECT b1 ⇒ λ_.
     327         [ ([[true;true;false;false;false;true;false;true]]); b1]
     328      | INDIRECT i1 ⇒ λ_.
     329         [ ([[true;true;false;false;false;true;true;i1]]) ]
     330      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
     331  | XCHD addr1 addr2 ⇒
     332     match addr2 return λx. bool_to_Prop (is_in ? [[indirect]] x) → ? with
     333      [ INDIRECT i1 ⇒ λ_.
     334         [ ([[true;true;false;true;false;true;true;i1]]) ]
     335      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
     336  | XRL addrs ⇒
     337     match addrs with
     338      [ inl addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
     339         match addr2 return λx. bool_to_Prop (is_in ? [[data;registr;direct;indirect]] x) → ? with
     340          [ REGISTER r ⇒ λ_.
     341             [ ([[false;true;true;false;true]]) @@ r ]
     342          | DIRECT b1 ⇒ λ_.
     343             [ ([[false;true;true;false;false;true;false;true]]); b1]
     344          | INDIRECT i1 ⇒ λ_.
     345             [ ([[false;true;true;false;false;true;true;i1]]) ]
     346          | DATA b1 ⇒ λ_.
     347             [ ([[false;true;true;false;false;true;false;false]]); b1]
     348          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
     349      | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
     350         let b1 ≝
     351          match addr1 return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with
     352           [ DIRECT b1 ⇒ λ_. b1
     353           | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1) in
     354         match addr2 return λx. bool_to_Prop (is_in ? [[acc_a;data]] x) → ? with
     355          [ ACC_A ⇒ λ_.
     356             [ ([[false;true;true;false;false;false;true;false]]); b1 ]         
     357          | DATA b2 ⇒ λ_.
     358             [ ([[false;true;true;false;false;false;true;true]]); b1; b2 ]
     359          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]
     360       ].
     361
     362definition assembly1 ≝
     363 λi: instruction.
     364 match i with
     365  [ ACALL addr ⇒
     366     match addr return λx. bool_to_Prop (is_in ? [[addr11]] x) → ? with
     367      [ ADDR11 w ⇒ λ_.
     368         let v1_v2 ≝ split ? 3 8 w in
     369         let v1 ≝ \fst v1_v2 in
     370         let v2 ≝ \snd v1_v2 in
     371          [ (v1 @@ [[true; false; false; false; true]]) ; v2 ]
     372      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
     373  | AJMP addr ⇒
     374     match addr return λx. bool_to_Prop (is_in ? [[addr11]] x) → ? with
     375      [ ADDR11 w ⇒ λ_.
     376         let v1_v2 ≝ split ? 3 8 w in
     377         let v1 ≝ \fst v1_v2 in
     378         let v2 ≝ \snd v1_v2 in
     379          [ (v1 @@ [[false; false; false; false; true]]) ; v2 ]
     380      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
     381  | JMP adptr ⇒
     382     [ ([[false;true;true;true;false;false;true;true]]) ]
     383  | LCALL addr ⇒
     384     match addr return λx. bool_to_Prop (is_in ? [[addr16]] x) → ? with
     385      [ ADDR16 w ⇒ λ_.
     386         let b1_b2 ≝ split ? 8 8 w in
     387         let b1 ≝ \fst b1_b2 in
     388         let b2 ≝ \snd b1_b2 in
     389          [ ([[false;false;false;true;false;false;true;false]]); b1; b2 ]         
     390      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
     391  | LJMP addr ⇒
     392     match addr return λx. bool_to_Prop (is_in ? [[addr16]] x) → ? with
     393      [ ADDR16 w ⇒ λ_.
     394         let b1_b2 ≝ split ? 8 8 w in
     395         let b1 ≝ \fst b1_b2 in
     396         let b2 ≝ \snd b1_b2 in
     397          [ ([[false;false;false;false;false;false;true;false]]); b1; b2 ]         
     398      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
     399  | MOVC addr1 addr2 ⇒
     400     match addr2 return λx. bool_to_Prop (is_in ? [[acc_dptr;acc_pc]] x) → ? with
     401      [ ACC_DPTR ⇒ λ_.
     402         [ ([[true;false;false;true;false;false;true;true]]) ]
     403      | ACC_PC ⇒ λ_.
     404         [ ([[true;false;false;false;false;false;true;true]]) ]
     405      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
     406  | SJMP addr ⇒
     407     match addr return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with
     408      [ RELATIVE b1 ⇒ λ_.
     409         [ ([[true;false;false;false;false;false;false;false]]); b1 ]
     410      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
     411  | RealInstruction instr ⇒
     412    assembly_preinstruction [[ relative ]]
     413      (λx.
     414        match x return λs. bool_to_Prop (is_in ? [[ relative ]] s) → ? with
     415        [ RELATIVE r ⇒ λ_. r
     416        | _ ⇒ λabsd. ⊥
     417        ] (subaddressing_modein … x)) instr
     418  ].
     419  cases absd
     420qed.
     421
     422definition expand_relative_jump_internal:
     423 (Identifier → Word) → jump_length → Identifier → Word → ([[relative]] → preinstruction [[relative]]) →
     424 option (list instruction)
     425 ≝
     426  λlookup_labels,jmp_len.λjmp:Identifier.λpc,i.
     427  match jmp_len with
     428  [ short_jump ⇒
     429     let lookup_address ≝ lookup_labels jmp in
     430     let 〈result, flags〉 ≝ sub_16_with_carry pc lookup_address false in
     431     let 〈upper, lower〉 ≝ split ? 8 8 result in
     432     if eq_bv ? upper (zero 8) then
     433      let address ≝ RELATIVE lower in
     434       Some ? [ RealInstruction (i address) ]
     435     else
     436       None ?
     437  | medium_jump ⇒ None …
     438  | long_jump ⇒
     439    Some ?
     440    [ RealInstruction (i (RELATIVE (bitvector_of_nat ? 2)));
     441      SJMP (RELATIVE (bitvector_of_nat ? 3)); (* LJMP size? *)
     442      LJMP (ADDR16 (lookup_labels jmp))
     443    ]
     444  ].
     445  @ I
     446qed.
     447
     448definition expand_relative_jump: (Identifier → Word) → jump_length → Word → preinstruction Identifier → option (list instruction) ≝
     449  λlookup_labels.
     450  λjmp_len: jump_length.
     451  λpc.
     452  λi: preinstruction Identifier.
     453  let rel_jmp ≝ RELATIVE (bitvector_of_nat ? 2) in
     454  match i with
     455  [ JC jmp ⇒ expand_relative_jump_internal lookup_labels jmp_len jmp pc (JC ?)
     456  | JNC jmp ⇒ expand_relative_jump_internal lookup_labels jmp_len jmp pc (JNC ?)
     457  | JB baddr jmp ⇒ expand_relative_jump_internal lookup_labels jmp_len jmp pc (JB ? baddr)
     458  | JZ jmp ⇒ expand_relative_jump_internal lookup_labels jmp_len jmp pc (JZ ?)
     459  | JNZ jmp ⇒ expand_relative_jump_internal lookup_labels jmp_len jmp pc (JNZ ?)
     460  | JBC baddr jmp ⇒ expand_relative_jump_internal lookup_labels jmp_len jmp pc (JBC ? baddr)
     461  | JNB baddr jmp ⇒ expand_relative_jump_internal lookup_labels jmp_len jmp pc (JNB ? baddr)
     462  | CJNE addr jmp ⇒ expand_relative_jump_internal lookup_labels jmp_len jmp pc (CJNE ? addr)
     463  | DJNZ addr jmp ⇒ expand_relative_jump_internal lookup_labels jmp_len jmp pc (DJNZ ? addr)
     464  | ADD arg1 arg2 ⇒ Some ? [ ADD ? arg1 arg2 ]
     465  | ADDC arg1 arg2 ⇒ Some ? [ ADDC ? arg1 arg2 ]
     466  | SUBB arg1 arg2 ⇒ Some ? [ SUBB ? arg1 arg2 ]
     467  | INC arg ⇒ Some ? [ INC ? arg ]
     468  | DEC arg ⇒ Some ? [ DEC ? arg ]
     469  | MUL arg1 arg2 ⇒ Some ? [ MUL ? arg1 arg2 ]
     470  | DIV arg1 arg2 ⇒ Some ? [ DIV ? arg1 arg2 ]
     471  | DA arg ⇒ Some ? [ DA ? arg ]
     472  | ANL arg ⇒ Some ? [ ANL ? arg ]
     473  | ORL arg ⇒ Some ? [ ORL ? arg ]
     474  | XRL arg ⇒ Some ? [ XRL ? arg ]
     475  | CLR arg ⇒ Some ? [ CLR ? arg ]
     476  | CPL arg ⇒ Some ? [ CPL ? arg ]
     477  | RL arg ⇒ Some ? [ RL ? arg ]
     478  | RR arg ⇒ Some ? [ RR ? arg ]
     479  | RLC arg ⇒ Some ? [ RLC ? arg ]
     480  | RRC arg ⇒ Some ? [ RRC ? arg ]
     481  | SWAP arg ⇒ Some ? [ SWAP ? arg ]
     482  | MOV arg ⇒ Some ? [ MOV ? arg ]
     483  | MOVX arg ⇒ Some ? [ MOVX ? arg ]
     484  | SETB arg ⇒ Some ? [ SETB ? arg ]
     485  | PUSH arg ⇒ Some ? [ PUSH ? arg ]
     486  | POP arg ⇒ Some ? [ POP ? arg ]
     487  | XCH arg1 arg2 ⇒ Some ? [ XCH ? arg1 arg2 ]
     488  | XCHD arg1 arg2 ⇒ Some ? [ XCHD ? arg1 arg2 ]
     489  | RET ⇒ Some ? [ RET ? ]
     490  | RETI ⇒ Some ? [ RETI ? ]
     491  | NOP ⇒ Some ? [ RealInstruction (NOP ?) ]
     492  ].
     493
     494
     495definition expand_pseudo_instruction_safe: ? → ? → Word → jump_length → pseudo_instruction → option (list instruction) ≝
     496  λlookup_labels.
     497  λlookup_datalabels.
     498  λpc.
     499  λjmp_len.
     500  λi.
     501  match i with
     502  [ Cost cost ⇒ Some ? [ ]
     503  | Comment comment ⇒ Some ? [ ]
     504  | Call call ⇒
     505    match jmp_len with
     506    [ short_jump ⇒ None ?
     507    | medium_jump ⇒
     508      let 〈ignore, address〉 ≝ split ? 5 11 (lookup_labels call) in
     509      let 〈fst_5, rest〉 ≝ split ? 5 11 pc in
     510      if eq_bv ? ignore fst_5 then
     511        let address ≝ ADDR11 address in
     512          Some ? ([ ACALL address ])
     513      else
     514        None ?
     515    | long_jump ⇒
     516      let address ≝ ADDR16 (lookup_labels call) in
     517        Some ? [ LCALL address ]
     518    ]
     519  | Mov d trgt ⇒
     520    let address ≝ DATA16 (lookup_datalabels trgt) in
     521      Some ? [ RealInstruction (MOV ? (inl ? ? (inl ? ? (inr ? ? 〈DPTR, address〉))))]
     522  | Instruction instr ⇒ expand_relative_jump lookup_labels jmp_len pc instr
     523  | Jmp jmp ⇒
     524    match jmp_len with
     525    [ short_jump ⇒
     526      let lookup_address ≝ lookup_labels jmp in
     527      let 〈result, flags〉 ≝ sub_16_with_carry pc lookup_address false in
     528      let 〈upper, lower〉 ≝ split ? 8 8 result in
     529      if eq_bv ? upper (zero 8) then
     530        let address ≝ RELATIVE lower in
     531          Some ? [ SJMP address ]
     532      else
     533        None ?
     534    | medium_jump ⇒
     535      let address ≝ lookup_labels jmp in
     536      let 〈fst_5_addr, rest_addr〉 ≝ split ? 5 11 address in
     537      let 〈fst_5_pc, rest_pc〉 ≝ split ? 5 11 pc in
     538      if eq_bv ? fst_5_addr fst_5_pc then
     539        let address ≝ ADDR11 rest_addr in
     540          Some ? ([ AJMP address ])
     541      else
     542        None ?
     543    | long_jump ⇒
     544      let address ≝ ADDR16 (lookup_labels jmp) in
     545        Some ? [ LJMP address ]
     546    ]
     547  ].
     548  @ I
     549qed.
     550
    23551
    24552definition assembly_1_pseudoinstruction_safe ≝
Note: See TracChangeset for help on using the changeset viewer.