Changeset 1615


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.

Location:
src/ASM
Files:
2 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 ≝

  • src/ASM/Policy.ma

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