Changeset 820 for src/ASM/Assembly.ma


Ignore:
Timestamp:
May 20, 2011, 6:09:00 PM (9 years ago)
Author:
mulligan
Message:

changes to get the semantics of pseudoassembly working

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Assembly.ma

    r757 r820  
    55include "ASM/Status.ma".
    66
    7 definition assembly1 ≝
    8  λi: instruction.
    9  match i with
    10   [ ACALL addr ⇒
    11      match addr return λx. bool_to_Prop (is_in ? [[addr11]] x) → ? with
    12       [ ADDR11 w ⇒ λ_.
    13          let 〈v1,v2〉 ≝ split ? 3 8 w in
    14           [ (v1 @@ [[true; false; false; false; true]]) ; v2 ]
    15       | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
    16   | ADD addr1 addr2 ⇒
     7definition assembly_preinstruction ≝
     8  λA: Type[0].
     9  λaddr_of: A → Byte. (* relative *)
     10  λpre: preinstruction A.
     11  match pre with
     12  [ ADD addr1 addr2 ⇒
    1713     match addr2 return λx. bool_to_Prop (is_in ? [[registr;direct;indirect;data]] x) → ? with
    1814      [ REGISTER r ⇒ λ_.[ ([[false;false;true;false;true]]) @@ r ]
     
    2824      | DATA b1 ⇒ λ_. [ ([[false;false;true;true;false;true;false;false]]) ; b1 ]
    2925      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
    30   | AJMP addr ⇒
    31      match addr return λx. bool_to_Prop (is_in ? [[addr11]] x) → ? with
    32       [ ADDR11 w ⇒ λ_.
    33          let 〈v1,v2〉 ≝ split ?  3 8 w in
    34           [ (v1 @@ [[false; false; false; false; true]]) ; v2 ]
    35       | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
    3626  | ANL addrs ⇒
    3727     match addrs with
     
    9080         [ ([[false; false; false; true; false; true; true; i1]]) ]
    9181      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
    92   | DIV addr1 addr2 ⇒
    93      [ ([[true;false;false;false;false;true;false;false]]) ]
    94   | Jump j ⇒
    95      match j with
    96       [ DJNZ addr1 addr2 ⇒
    97          let b2 ≝
    98           match addr2 return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with
    99            [ RELATIVE b2 ⇒ λ_. b2
    100            | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) in
     82      | DJNZ addr1 addr2 ⇒
     83         let b2 ≝ addr_of addr2 in
    10184         match addr1 return λx. bool_to_Prop (is_in ? [[registr;direct]] x) → ? with
    10285          [ REGISTER r ⇒ λ_.
     
    10689          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)
    10790      | JC addr ⇒
    108          match addr return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with
    109           [ RELATIVE b1 ⇒ λ_.
    110              [ ([[false; true; false; false; false; false; false; false]]); b1 ]
    111           | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
     91        let b1 ≝ addr_of addr in
     92          [ ([[false; true; false; false; false; false; false; false]]); b1 ]
    11293      | JNC addr ⇒
    113          match addr return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with
    114           [ RELATIVE b1 ⇒ λ_.
    115              [ ([[false; true; false; true; false; false; false; false]]); b1 ]
    116           | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
     94         let b1 ≝ addr_of addr in
     95           [ ([[false; true; false; true; false; false; false; false]]); b1 ]
    11796      | JZ addr ⇒
    118          match addr return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with
    119           [ RELATIVE b1 ⇒ λ_.
    120              [ ([[false; true; true; false; false; false; false; false]]); b1 ]
    121           | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
     97         let b1 ≝ addr_of addr in
     98           [ ([[false; true; true; false; false; false; false; false]]); b1 ]
    12299      | JNZ addr ⇒
    123          match addr return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with
    124           [ RELATIVE b1 ⇒ λ_.
    125              [ ([[false; true; true; true; false; false; false; false]]); b1 ]
    126           | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
     100         let b1 ≝ addr_of addr in
     101           [ ([[false; true; true; true; false; false; false; false]]); b1 ]
    127102      | JB addr1 addr2 ⇒
    128          let b2 ≝
    129           match addr2 return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with
    130            [ RELATIVE b2 ⇒ λ_. b2
    131            | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) in
     103         let b2 ≝ addr_of addr2 in
    132104         match addr1 return λx. bool_to_Prop (is_in ? [[bit_addr]] x) → ? with
    133105          [ BIT_ADDR b1 ⇒ λ_.
     
    135107          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)
    136108      | JNB addr1 addr2 ⇒
    137          let b2 ≝
    138           match addr2 return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with
    139            [ RELATIVE b2 ⇒ λ_. b2
    140            | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) in
     109         let b2 ≝ addr_of addr2 in
    141110         match addr1 return λx. bool_to_Prop (is_in ? [[bit_addr]] x) → ? with
    142111          [ BIT_ADDR b1 ⇒ λ_.
     
    144113          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)
    145114      | JBC addr1 addr2 ⇒
    146          let b2 ≝
    147           match addr2 return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with
    148            [ RELATIVE b2 ⇒ λ_. b2
    149            | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) in
     115         let b2 ≝ addr_of addr2 in
    150116         match addr1 return λx. bool_to_Prop (is_in ? [[bit_addr]] x) → ? with
    151117          [ BIT_ADDR b1 ⇒ λ_.
     
    153119          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)
    154120      | CJNE addrs addr3 ⇒
    155          let b3 ≝
    156           match addr3 return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with
    157            [ RELATIVE b3 ⇒ λ_. b3
    158            | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr3) in
     121         let b3 ≝ addr_of addr3 in
    159122         match addrs with
    160123          [ inl addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
     
    171134               | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) in
    172135             match addr1 return λx. bool_to_Prop (is_in ? [[registr;indirect]] x) → list Byte with
    173               [ REGISTER r⇒ λ_.
     136              [ REGISTER r ⇒ λ_.
    174137                 [ ([[true; false; true; true; true]]) @@ r; b2; b3 ]
    175138              | INDIRECT i1 ⇒ λ_.
    176139                 [ ([[true; false; true; true; false; true; true; i1]]); b2; b3 ]
    177               | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1) ]]
     140              | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)
     141         ]
     142  | DIV addr1 addr2 ⇒
     143     [ ([[true;false;false;false;false;true;false;false]]) ]
    178144  | INC addr ⇒
    179145     match addr return λx. bool_to_Prop (is_in ? [[acc_a;registr;direct;indirect;dptr]] x) → ? with
     
    188154      | DPTR ⇒ λ_.
    189155        [ ([[true;false;true;false;false;false;true;true]]) ]
    190       | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
    191   | JMP addr ⇒
    192      [ ([[false;true;true;true;false;false;true;true]]) ]
    193   | LCALL addr ⇒
    194      match addr return λx. bool_to_Prop (is_in ? [[addr16]] x) → ? with
    195       [ ADDR16 w ⇒ λ_.
    196          let 〈b1,b2〉 ≝ split ? 8 8 w in
    197           [ ([[false;false;false;true;false;false;true;false]]); b1; b2 ]         
    198       | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
    199   | LJMP addr ⇒
    200      match addr return λx. bool_to_Prop (is_in ? [[addr16]] x) → ? with
    201       [ ADDR16 w ⇒ λ_.
    202          let 〈b1,b2〉 ≝ split ? 8 8 w in
    203           [ ([[false;false;false;false;false;false;true;false]]); b1; b2 ]         
    204156      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
    205157  | MOV addrs ⇒
     
    263215             [ ([[true;false;false;true;false;false;true;false]]); b1 ]
    264216          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)]
    265   | MOVC addr1 addr2 ⇒
    266      match addr2 return λx. bool_to_Prop (is_in ? [[acc_dptr;acc_pc]] x) → ? with
    267       [ ACC_DPTR ⇒ λ_.
    268          [ ([[true;false;false;true;false;false;true;true]]) ]
    269       | ACC_PC ⇒ λ_.
    270          [ ([[true;false;false;false;false;false;true;true]]) ]
    271       | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
    272217  | MOVX addrs ⇒
    273218     match addrs with
     
    348293         [ ([[true;true;false;true;false;false;true;false]]); b1 ]
    349294      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
    350   | SJMP addr ⇒
    351      match addr return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with
    352       [ RELATIVE b1 ⇒ λ_.
    353          [ ([[true;false;false;false;false;false;false;false]]); b1 ]
    354       | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
    355295  | SUBB addr1 addr2 ⇒
    356296     match addr2 return λx. bool_to_Prop (is_in ? [[registr;direct;indirect;data]] x) → ? with
     
    403343          | DATA b2 ⇒ λ_.
    404344             [ ([[false;true;true;false;false;false;true;true]]); b1; b2 ]
    405           | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]].
    406          
    407 definition assembly_jump: (jump Identifier) → (Identifier → [[relative]]) → instruction ≝
    408   λj: jump Identifier.
    409   λaddr_of: Identifier → [[relative]].
    410     match j with
    411       [ JC jmp ⇒ Jump ? (JC ? (addr_of jmp))
    412       | JNC jmp ⇒ Jump ? (JNC ? (addr_of jmp))
    413       | JZ jmp ⇒ Jump ? (JZ ? (addr_of jmp))
    414       | JNZ jmp ⇒ Jump ? (JNZ ? (addr_of jmp))
    415       | JB jmp jmp' ⇒ Jump ? (JB ? jmp (addr_of jmp'))
    416       | JNB jmp jmp' ⇒ Jump ? (JNB ? jmp (addr_of jmp'))
    417       | JBC jmp jmp' ⇒ Jump ? (JBC ? jmp (addr_of jmp'))
    418       | CJNE jmp jmp' ⇒ Jump ? (CJNE ? jmp (addr_of jmp'))
    419       | DJNZ jmp jmp' ⇒ Jump ? (DJNZ ? jmp (addr_of jmp'))
    420       ].
     345          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]
     346       ].
    421347
    422 definition address_of: BitVectorTrie Word 16 → Identifier → addressing_mode ≝
     348definition assembly1 ≝
     349 λi: instruction.
     350 match i with
     351  [ ACALL addr ⇒
     352     match addr return λx. bool_to_Prop (is_in ? [[addr11]] x) → ? with
     353      [ ADDR11 w ⇒ λ_.
     354         let 〈v1,v2〉 ≝ split ? 3 8 w in
     355          [ (v1 @@ [[true; false; false; false; true]]) ; v2 ]
     356      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
     357  | AJMP addr ⇒
     358     match addr return λx. bool_to_Prop (is_in ? [[addr11]] x) → ? with
     359      [ ADDR11 w ⇒ λ_.
     360         let 〈v1,v2〉 ≝ split ?  3 8 w in
     361          [ (v1 @@ [[false; false; false; false; true]]) ; v2 ]
     362      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
     363  | JMP adptr ⇒
     364     [ ([[false;true;true;true;false;false;true;true]]) ]
     365  | LCALL addr ⇒
     366     match addr return λx. bool_to_Prop (is_in ? [[addr16]] x) → ? with
     367      [ ADDR16 w ⇒ λ_.
     368         let 〈b1,b2〉 ≝ split ? 8 8 w in
     369          [ ([[false;false;false;true;false;false;true;false]]); b1; b2 ]         
     370      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
     371  | LJMP addr ⇒
     372     match addr return λx. bool_to_Prop (is_in ? [[addr16]] x) → ? with
     373      [ ADDR16 w ⇒ λ_.
     374         let 〈b1,b2〉 ≝ split ? 8 8 w in
     375          [ ([[false;false;false;false;false;false;true;false]]); b1; b2 ]         
     376      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
     377  | MOVC addr1 addr2 ⇒
     378     match addr2 return λx. bool_to_Prop (is_in ? [[acc_dptr;acc_pc]] x) → ? with
     379      [ ACC_DPTR ⇒ λ_.
     380         [ ([[true;false;false;true;false;false;true;true]]) ]
     381      | ACC_PC ⇒ λ_.
     382         [ ([[true;false;false;false;false;false;true;true]]) ]
     383      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
     384  | SJMP addr ⇒
     385     match addr return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with
     386      [ RELATIVE b1 ⇒ λ_.
     387         [ ([[true;false;false;false;false;false;false;false]]); b1 ]
     388      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
     389  | RealInstruction instr ⇒
     390    assembly_preinstruction [[ relative ]]
     391      (λx.
     392        match x return λs. bool_to_Prop (is_in ? [[ relative ]] s) → ? with
     393        [ RELATIVE r ⇒ λ_. r
     394        | _ ⇒ λabsd. ⊥
     395        ] (subaddressing_modein … x)) instr
     396  ].
     397  cases absd
     398qed.
     399
     400definition address_of: BitVectorTrie Word 16 → Identifier → Byte ≝
    423401    λmap.
    424402    λid: Identifier.
     
    426404      let 〈high, low〉 ≝ split ? 8 8 address in
    427405      if eq_bv ? high (zero ?) then
    428         RELATIVE low
     406        low
    429407      else
    430408        ?.
     
    432410qed.
    433411
    434 definition assembly: assembly_program → option (list Byte × (BitVectorTrie Identifier 16)) ≝
     412definition assembly: pseudo_assembly_program → option (list Byte × (BitVectorTrie Identifier 16)) ≝
    435413  λp.
    436414    let 〈preamble, instr_list〉 ≝ p in
     
    458436            match i with
    459437              [ Instruction instr ⇒
    460                 let code_memory ≝ load_code_memory (assembly1 instr) in
     438                let code_memory ≝ load_code_memory (assembly_preinstruction Identifier (λx. zero 8) instr) in
    461439                let 〈instr_pc', ignore〉 ≝ fetch code_memory (zero 16) in
    462440                let 〈instr', program_counter'〉 ≝ instr_pc' in
     
    472450                  〈program_counter + 3, costs〉
    473451              | Mov dptr trgt ⇒ pc_costs
    474               | WithLabel jmp ⇒
    475                 let fake_addr ≝ RELATIVE (zero 8) in
    476                 let fake_jump ≝ assembly_jump jmp (λx: Identifier. fake_addr) in
    477                 let code_memory ≝ load_code_memory (assembly1 fake_jump) in
    478                 let 〈instr_pc', ignore〉 ≝ fetch code_memory (zero 16) in
    479                 let 〈instr', program_counter'〉 ≝ instr_pc' in
    480                 let program_counter_n' ≝ nat_of_bitvector 16 program_counter' in
    481                   〈program_counter + program_counter_n', costs〉
    482452              ]〉
    483453          ) 〈(Stub ? ?), 〈0,(Stub ? ?)〉〉 instr_list in
     
    496466                    let pc_offset ≝ lookup ? ? call labels (zero ?) in
    497467                    let address ≝ ADDR16 pc_offset in
    498                       assembly1 (LCALL ? address)
     468                      assembly1 (LCALL address)
    499469                  | Mov d trgt ⇒
    500470                    let pc_offset ≝ lookup ? ? trgt datalabels (zero ?) in
    501471                    let address ≝ DATA16 pc_offset in
    502472                      assembly1 (MOV ? (inl ? ? (inl ? ? (inr ? ? 〈DPTR, address〉))))
    503                   | Instruction instr ⇒ assembly1 instr
     473                  | Instruction instr ⇒ assembly_preinstruction ? (address_of labels) instr
    504474                  | Jmp jmp ⇒
    505475                    let pc_offset ≝ lookup ? ? jmp labels (zero ?) in
    506476                    let address ≝ ADDR16 pc_offset in
    507                       assembly1 (LJMP ? address)
    508                   | WithLabel jmp ⇒ assembly1 (assembly_jump jmp (address_of labels))
     477                      assembly1 (LJMP address)
     478(*                  | WithLabel jmp ⇒ assembly1 (assembly_jump jmp (address_of labels))
     479*)
    509480                  ]
    510481            ) instr_list
     
    514485    normalize; %;
    515486  | whd in ⊢ (? (? ? ? %));
    516       cases (split bool 8 8 (lookup Word 16 c0 labels (zero 16)))
     487      cases (split bool 8 8 (lookup Word 16 trgt labels (zero 16)))
    517488      # high
    518489      # low
     
    526497qed.
    527498
    528 definition assembly_unlabelled_program: list instruction → option (list Byte × (BitVectorTrie Identifier 16)) ≝
     499definition assembly_unlabelled_program: assembly_program → option (list Byte × (BitVectorTrie Identifier 16)) ≝
    529500 λp. Some ? (〈foldr ? ? (λi,l. assembly1 i @ l) [ ] p, Stub …〉).
    530501
Note: See TracChangeset for help on using the changeset viewer.