Changeset 820


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

changes to get the semantics of pseudoassembly working

Location:
src/ASM
Files:
4 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASM.ma

    r757 r820  
    112112 ≝ mk_subaddressing_mode on a:addressing_mode to subaddressing_mode ? ?.
    113113
    114 inductive jump (A: Type[0]): Type[0] ≝
    115   JC: A → jump A
    116 | JNC: A → jump A
    117 | JB: [[bit_addr]] → A → jump A
    118 | JNB: [[bit_addr]] → A → jump A
    119 | JBC: [[bit_addr]] → A → jump A
    120 | JZ: A → jump A
    121 | JNZ: A → jump A
    122 | CJNE:
    123    [[acc_a]] × [[direct; data]] ⊎ [[registr; indirect]] × [[data]] → A → jump A
    124 | DJNZ: [[registr ; direct]] → A → jump A.
    125 
    126114inductive preinstruction (A: Type[0]) : Type[0] ≝
    127115  ADD: [[acc_a]] → [[ registr ; direct ; indirect ; data ]] → preinstruction A
     
    134122| DA: [[acc_a]] → preinstruction A
    135123
     124(* conditional jumps *)
     125| JC: A → preinstruction A
     126| JNC: A → preinstruction A
     127| JB: [[bit_addr]] → A → preinstruction A
     128| JNB: [[bit_addr]] → A → preinstruction A
     129| JBC: [[bit_addr]] → A → preinstruction A
     130| JZ: A → preinstruction A
     131| JNZ: A → preinstruction A
     132| CJNE:
     133   [[acc_a]] × [[direct; data]] ⊎ [[registr; indirect]] × [[data]] → A → preinstruction A
     134| DJNZ: [[registr ; direct]] → A → preinstruction A
    136135 (* logical operations *)
    137136| ANL:
     
    162161    [[carry]] × [[bit_addr]] ⊎
    163162    [[bit_addr]] × [[carry]] → preinstruction A
    164 | MOVC: [[acc_a]] → [[ acc_dptr ; acc_pc ]] → preinstruction A
    165163| MOVX:
    166164    [[acc_a]] × [[ ext_indirect ; ext_indirect_dptr ]] ⊎
     
    173171
    174172 (* program branching *)
    175 | Jump: jump A → preinstruction A
    176 | ACALL: [[addr11]] → preinstruction A
    177 | LCALL: [[addr16]] → preinstruction A
    178173| RET: preinstruction A
    179174| RETI: preinstruction A
    180 | AJMP: [[addr11]] → preinstruction A
    181 | LJMP: [[addr16]] → preinstruction A
    182 | SJMP: [[relative]] → preinstruction A
    183 | JMP: [[indirect_dptr]] → preinstruction A
    184175| NOP: preinstruction A.
    185176
    186 definition instruction ≝ preinstruction [[relative]].
     177inductive instruction: Type[0] ≝
     178  | ACALL: [[addr11]] → instruction
     179  | LCALL: [[addr16]] → instruction
     180  | AJMP: [[addr11]] → instruction
     181  | LJMP: [[addr16]] → instruction
     182  | SJMP: [[relative]] → instruction
     183  | JMP: [[indirect_dptr]] → instruction
     184  | MOVC: [[acc_a]] → [[ acc_dptr ; acc_pc ]] → instruction
     185  | RealInstruction: preinstruction [[ relative ]] → instruction.
     186 
     187coercion RealInstruction: ∀p: preinstruction [[ relative ]]. instruction ≝
     188  RealInstruction on _p: preinstruction ? to instruction.
    187189
    188190inductive pseudo_instruction: Type[0] ≝
    189   Instruction: instruction → pseudo_instruction
    190 | Comment: String → pseudo_instruction
    191 | Cost: Identifier → pseudo_instruction
    192 | Jmp: Identifier → pseudo_instruction
    193 | Call: Identifier → pseudo_instruction
    194 | Mov: [[dptr]] → Identifier → pseudo_instruction
    195 | WithLabel: jump Identifier → pseudo_instruction.
     191  | Instruction: preinstruction Identifier → pseudo_instruction
     192  | Comment: String → pseudo_instruction
     193  | Cost: Identifier → pseudo_instruction
     194  | Jmp: Identifier → pseudo_instruction
     195  | Call: Identifier → pseudo_instruction
     196  | Mov: [[dptr]] → Identifier → pseudo_instruction.
    196197
    197198definition labelled_instruction ≝ option Identifier × pseudo_instruction.
    198 
    199199definition preamble ≝ list (Identifier × nat).
    200 
    201 definition assembly_program ≝ preamble × (list labelled_instruction).
     200definition assembly_program ≝ list instruction.
     201definition pseudo_assembly_program ≝ preamble × (list labelled_instruction).
  • 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
  • src/ASM/Fetch.ma

    r712 r820  
    2020      let 〈b,v〉 ≝ head … v in if b then
    2121       let 〈b,v〉 ≝ head … v in if b then
    22         〈〈MOV … (inl … (inl … (inl … (inl … (inr … 〈REGISTER v,ACC_A〉))))), pc〉, 1〉
    23        else
    24         let 〈b,v〉≝  head … v in if b then
    25          let 〈b,v〉≝  head … v in if b then
    26           〈〈MOV … (inl … (inl … (inl … (inl … (inr … 〈INDIRECT (from_singl … v),ACC_A〉))))), pc〉, 1〉
    27          else
    28           let 〈b,v〉≝  head … v in if b then
    29            let 〈pc,b1〉≝ next pmem pc in 〈〈MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,ACC_A〉)))), pc〉, 1〉
     22        〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inr … 〈REGISTER v,ACC_A〉)))))), pc〉, 1〉
     23       else
     24        let 〈b,v〉≝  head … v in if b then
     25         let 〈b,v〉≝  head … v in if b then
     26          〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inr … 〈INDIRECT (from_singl … v),ACC_A〉)))))), pc〉, 1〉
     27         else
     28          let 〈b,v〉≝  head … v in if b then
     29           let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,ACC_A〉))))), pc〉, 1〉
    3030          else
    3131           〈〈CPL … ACC_A, pc〉, 1〉
    3232        else
    3333         let 〈b,v〉≝  head … v in if b then
    34           〈〈MOVX … (inr … 〈EXT_INDIRECT (from_singl … v),ACC_A〉), pc〉, 2〉
     34          〈〈RealInstruction (MOVX … (inr … 〈EXT_INDIRECT (from_singl … v),ACC_A〉)), pc〉, 2〉
    3535         else
    3636          let 〈b,v〉≝  head … v in if b then
    3737           let 〈pc,b1〉≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[false;false;false]]) @@ b1)), pc〉, 2〉
    3838          else
    39            〈〈MOVX … (inr … 〈EXT_INDIRECT_DPTR,ACC_A〉), pc〉, 2〉
    40       else
    41        let 〈b,v〉≝  head … v in if b then
    42         〈〈MOV … (inl … (inl … (inl … (inl … (inl … 〈ACC_A,REGISTER v〉))))), pc〉, 1〉
    43        else
    44         let 〈b,v〉≝  head … v in if b then
    45          let 〈b,v〉≝  head … v in if b then
    46           〈〈MOV … (inl … (inl … (inl … (inl … (inl … 〈ACC_A,INDIRECT (from_singl … v)〉))))), pc〉, 1〉
    47          else
    48           let 〈b,v〉≝  head … v in if b then
    49            let 〈pc,b1〉≝ next pmem pc in 〈〈MOV … (inl … (inl … (inl … (inl … (inl … 〈ACC_A,DIRECT b1〉))))), pc〉, 1〉
    50           else
    51            〈〈CLR … ACC_A, pc〉, 1〉
    52         else
    53          let 〈b,v〉≝  head … v in if b then
    54           〈〈MOVX … (inl … 〈ACC_A,EXT_INDIRECT (from_singl … v)〉), pc〉, 2〉
     39           〈〈RealInstruction (MOVX … (inr … 〈EXT_INDIRECT_DPTR,ACC_A〉)), pc〉, 2〉
     40      else
     41       let 〈b,v〉≝  head … v in if b then
     42        〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inl … 〈ACC_A,REGISTER v〉)))))), pc〉, 1〉
     43       else
     44        let 〈b,v〉≝  head … v in if b then
     45         let 〈b,v〉≝  head … v in if b then
     46          〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inl … 〈ACC_A,INDIRECT (from_singl … v)〉)))))), pc〉, 1〉
     47         else
     48          let 〈b,v〉≝  head … v in if b then
     49           let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inl … 〈ACC_A,DIRECT b1〉)))))), pc〉, 1〉
     50          else
     51           〈〈RealInstruction (CLR … ACC_A), pc〉, 1〉
     52        else
     53         let 〈b,v〉≝  head … v in if b then
     54          〈〈RealInstruction (MOVX … (inl … 〈ACC_A,EXT_INDIRECT (from_singl … v)〉)), pc〉, 2〉
    5555         else
    5656          let 〈b,v〉≝  head … v in if b then
    5757           let 〈pc,b1〉≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[false;false;false]]) @@ b1)), pc〉, 2〉
    5858          else
    59            〈〈MOVX … (inl … 〈ACC_A,EXT_INDIRECT_DPTR〉), pc〉, 2〉
     59           〈〈RealInstruction (MOVX … (inl … 〈ACC_A,EXT_INDIRECT_DPTR〉)), pc〉, 2〉
    6060     else
    6161      let 〈b,v〉≝  head … v in if b then
    6262       let 〈b,v〉≝  head … v in if b then
    63         let 〈pc,b1〉≝ next pmem pc in 〈〈Jump [[relative]] (DJNZ … (REGISTER v) (RELATIVE b1)), pc〉, 2〉
    64        else
    65         let 〈b,v〉≝  head … v in if b then
    66          let 〈b,v〉≝  head … v in if b then
    67           〈〈XCHD … ACC_A (INDIRECT (from_singl … v)), pc〉, 1〉
    68          else
    69           let 〈b,v〉≝  head … v in if b then
    70            let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈Jump [[relative]] (DJNZ … (DIRECT b1) (RELATIVE b2)), pc〉, 2〉
    71           else
    72            〈〈DA … ACC_A, pc〉, 1〉
    73         else
    74          let 〈b,v〉≝  head … v in if b then
    75           let 〈b,v〉≝  head … v in if b then
    76            〈〈SETB … CARRY, pc〉, 1〉
    77           else
    78            let 〈pc,b1〉≝ next pmem pc in 〈〈SETB … (BIT_ADDR b1), pc〉, 1〉
     63        let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (DJNZ … (REGISTER v) (RELATIVE b1)), pc〉, 2〉
     64       else
     65        let 〈b,v〉≝  head … v in if b then
     66         let 〈b,v〉≝  head … v in if b then
     67          〈〈RealInstruction (XCHD … ACC_A (INDIRECT (from_singl … v))), pc〉, 1〉
     68         else
     69          let 〈b,v〉≝  head … v in if b then
     70           let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈RealInstruction (DJNZ … (DIRECT b1) (RELATIVE b2)), pc〉, 2〉
     71          else
     72           〈〈RealInstruction (DA … ACC_A), pc〉, 1〉
     73        else
     74         let 〈b,v〉≝  head … v in if b then
     75          let 〈b,v〉≝  head … v in if b then
     76           〈〈RealInstruction (SETB … CARRY), pc〉, 1〉
     77          else
     78           let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (SETB … (BIT_ADDR b1)), pc〉, 1〉
    7979         else
    8080          let 〈b,v〉≝  head … v in if b then
    8181           let 〈pc,b1〉≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[false;false;true]]) @@ b1)), pc〉, 2〉
    8282          else
    83            let 〈pc,b1〉≝ next pmem pc in 〈〈POP … (DIRECT b1), pc〉, 2〉
    84       else
    85        let 〈b,v〉≝  head … v in if b then
    86         〈〈XCH … ACC_A (REGISTER v), pc〉, 1〉
    87        else
    88         let 〈b,v〉≝  head … v in if b then
    89          let 〈b,v〉≝  head … v in if b then
    90           〈〈XCH … ACC_A (INDIRECT (from_singl … v)), pc〉, 1〉
    91          else
    92           let 〈b,v〉≝  head … v in if b then
    93            let 〈pc,b1〉≝ next pmem pc in 〈〈XCH … ACC_A (DIRECT b1), pc〉, 1〉
    94           else
    95            〈〈SWAP … ACC_A, pc〉, 1〉
    96         else
    97          let 〈b,v〉≝  head … v in if b then
    98           let 〈b,v〉≝  head … v in if b then
    99            〈〈CLR … CARRY, pc〉, 1〉
    100           else
    101            let 〈pc,b1〉≝ next pmem pc in 〈〈CLR … (BIT_ADDR b1), pc〉, 1〉
     83           let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (POP … (DIRECT b1)), pc〉, 2〉
     84      else
     85       let 〈b,v〉≝  head … v in if b then
     86        〈〈RealInstruction (XCH … ACC_A (REGISTER v)), pc〉, 1〉
     87       else
     88        let 〈b,v〉≝  head … v in if b then
     89         let 〈b,v〉≝  head … v in if b then
     90          〈〈RealInstruction (XCH … ACC_A (INDIRECT (from_singl … v))), pc〉, 1〉
     91         else
     92          let 〈b,v〉≝  head … v in if b then
     93           let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (XCH … ACC_A (DIRECT b1)), pc〉, 1〉
     94          else
     95           〈〈RealInstruction (SWAP … ACC_A), pc〉, 1〉
     96        else
     97         let 〈b,v〉≝  head … v in if b then
     98          let 〈b,v〉≝  head … v in if b then
     99           〈〈RealInstruction (CLR … CARRY), pc〉, 1〉
     100          else
     101           let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (CLR … (BIT_ADDR b1)), pc〉, 1〉
    102102         else
    103103          let 〈b,v〉≝  head … v in if b then
    104104           let 〈pc,b1〉≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[false;false;true]]) @@ b1)), pc〉, 2〉
    105105          else
    106            let 〈pc,b1〉≝ next pmem pc in 〈〈PUSH … (DIRECT b1), pc〉, 2〉
     106           let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (PUSH … (DIRECT b1)), pc〉, 2〉
    107107    else
    108108     let 〈b,v〉≝  head … v in if b then
    109109      let 〈b,v〉≝  head … v in if b then
    110110       let 〈b,v〉≝  head … v in if b then
    111         let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈Jump [[relative]] (CJNE …  (inr … 〈REGISTER v,DATA b1〉) (RELATIVE b2)), pc〉, 2〉
    112        else
    113         let 〈b,v〉≝  head … v in if b then
    114          let 〈b,v〉≝  head … v in if b then
    115           let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈Jump [[relative]] (CJNE … (inr … 〈INDIRECT (from_singl … v),DATA b1〉) (RELATIVE b2)), pc〉, 2〉
    116          else
    117           let 〈b,v〉≝  head … v in if b then
    118            let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈Jump [[relative]] (CJNE …  (inl … 〈ACC_A,DIRECT b1〉) (RELATIVE b2)), pc〉, 2〉
    119           else
    120            let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈Jump [[relative]] (CJNE … (inl … 〈ACC_A,DATA b1〉) (RELATIVE b2)), pc〉, 2〉
    121         else
    122          let 〈b,v〉≝  head … v in if b then
    123           let 〈b,v〉≝  head … v in if b then
    124            〈〈CPL … CARRY, pc〉, 1〉
    125           else
    126            let 〈pc,b1〉≝ next pmem pc in 〈〈CPL … (BIT_ADDR b1), pc〉, 1〉
     111        let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈RealInstruction (CJNE …  (inr … 〈REGISTER v,DATA b1〉) (RELATIVE b2)), pc〉, 2〉
     112       else
     113        let 〈b,v〉≝  head … v in if b then
     114         let 〈b,v〉≝  head … v in if b then
     115          let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈RealInstruction (CJNE … (inr … 〈INDIRECT (from_singl … v),DATA b1〉) (RELATIVE b2)), pc〉, 2〉
     116         else
     117          let 〈b,v〉≝  head … v in if b then
     118           let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈RealInstruction (CJNE …  (inl … 〈ACC_A,DIRECT b1〉) (RELATIVE b2)), pc〉, 2〉
     119          else
     120           let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈RealInstruction (CJNE … (inl … 〈ACC_A,DATA b1〉) (RELATIVE b2)), pc〉, 2〉
     121        else
     122         let 〈b,v〉≝  head … v in if b then
     123          let 〈b,v〉≝  head … v in if b then
     124           〈〈RealInstruction (CPL … CARRY), pc〉, 1〉
     125          else
     126           let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (CPL … (BIT_ADDR b1)), pc〉, 1〉
    127127         else
    128128          let 〈b,v〉≝  head … v in if b then
    129129           let 〈pc,b1〉≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[false;true;false]]) @@ b1)), pc〉, 2〉
    130130          else
    131            let 〈pc,b1〉≝ next pmem pc in 〈〈ANL … (inr … 〈CARRY,N_BIT_ADDR b1〉), pc〉, 2〉
    132       else
    133        let 〈b,v〉≝  head … v in if b then
    134         let 〈pc,b1〉≝ next pmem pc in 〈〈MOV … (inl … (inl … (inl … (inl … (inr … 〈REGISTER v,DIRECT b1〉))))), pc〉, 2〉
    135        else
    136         let 〈b,v〉≝  head … v in if b then
    137          let 〈b,v〉≝  head … v in if b then
    138           let 〈pc,b1〉≝ next pmem pc in 〈〈MOV … (inl … (inl … (inl … (inl … (inr … 〈INDIRECT (from_singl … v),DIRECT b1〉))))), pc〉, 2〉
    139          else
    140           〈〈MUL … ACC_A ACC_B, pc〉, 4〉
    141         else
    142          let 〈b,v〉≝  head … v in if b then
    143           let 〈b,v〉≝  head … v in if b then
    144            〈〈INC … DPTR, pc〉, 2〉
    145           else
    146            let 〈pc,b1〉≝ next pmem pc in 〈〈MOV … (inl … (inr … 〈CARRY,BIT_ADDR b1〉)), pc〉, 1〉
     131           let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (ANL … (inr … 〈CARRY,N_BIT_ADDR b1〉)), pc〉, 2〉
     132      else
     133       let 〈b,v〉≝  head … v in if b then
     134        let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inr … 〈REGISTER v,DIRECT b1〉)))))), pc〉, 2〉
     135       else
     136        let 〈b,v〉≝  head … v in if b then
     137         let 〈b,v〉≝  head … v in if b then
     138          let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inr … 〈INDIRECT (from_singl … v),DIRECT b1〉)))))), pc〉, 2〉
     139         else
     140          〈〈RealInstruction (MUL … ACC_A ACC_B), pc〉, 4〉
     141        else
     142         let 〈b,v〉≝  head … v in if b then
     143          let 〈b,v〉≝  head … v in if b then
     144           〈〈RealInstruction (INC … DPTR), pc〉, 2〉
     145          else
     146           let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inr … 〈CARRY,BIT_ADDR b1〉))), pc〉, 1〉
    147147         else
    148148          let 〈b,v〉≝  head … v in if b then
    149149           let 〈pc,b1〉≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[false;true;false]]) @@ b1)), pc〉, 2〉
    150150          else
    151            let 〈pc,b1〉≝ next pmem pc in 〈〈ORL … (inr … 〈CARRY,N_BIT_ADDR b1〉), pc〉, 2〉
     151           let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (ORL … (inr … 〈CARRY,N_BIT_ADDR b1〉)), pc〉, 2〉
    152152     else
    153153      let 〈b,v〉≝  head … v in if b then
    154154       let 〈b,v〉≝  head … v in if b then
    155         〈〈SUBB … ACC_A (REGISTER v), pc〉, 1〉
    156        else
    157         let 〈b,v〉≝  head … v in if b then
    158          let 〈b,v〉≝  head … v in if b then
    159           〈〈SUBB … ACC_A (INDIRECT (from_singl … v)), pc〉, 1〉
    160          else
    161           let 〈b,v〉≝  head … v in if b then
    162            let 〈pc,b1〉≝ next pmem pc in 〈〈SUBB … ACC_A (DIRECT b1), pc〉, 1〉
    163           else
    164            let 〈pc,b1〉≝ next pmem pc in 〈〈SUBB … ACC_A (DATA b1), pc〉, 1〉
     155        〈〈RealInstruction (SUBB … ACC_A (REGISTER v)), pc〉, 1〉
     156       else
     157        let 〈b,v〉≝  head … v in if b then
     158         let 〈b,v〉≝  head … v in if b then
     159          〈〈RealInstruction (SUBB … ACC_A (INDIRECT (from_singl … v))), pc〉, 1〉
     160         else
     161          let 〈b,v〉≝  head … v in if b then
     162           let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (SUBB … ACC_A (DIRECT b1)), pc〉, 1〉
     163          else
     164           let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (SUBB … ACC_A (DATA b1)), pc〉, 1〉
    165165        else
    166166         let 〈b,v〉≝  head … v in if b then
     
    168168           〈〈MOVC … ACC_A (ACC_DPTR), pc〉, 2〉
    169169          else
    170            let 〈pc,b1〉≝ next pmem pc in 〈〈MOV … (inr … 〈BIT_ADDR b1,CARRY〉), pc〉, 2〉
     170           let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (MOV … (inr … 〈BIT_ADDR b1,CARRY〉)), pc〉, 2〉
    171171         else
    172172          let 〈b,v〉≝  head … v in if b then
    173173           let 〈pc,b1〉≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[false;true;true]]) @@ b1)), pc〉, 2〉
    174174          else
    175            let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈MOV … (inl … (inl … (inr … 〈DPTR,DATA16 (b1 @@ b2)〉))), pc〉, 2〉
    176       else
    177        let 〈b,v〉≝  head … v in if b then
    178         let 〈pc,b1〉≝ next pmem pc in 〈〈MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,REGISTER v〉)))), pc〉, 2〉
    179        else
    180         let 〈b,v〉≝  head … v in if b then
    181          let 〈b,v〉≝  head … v in if b then
    182           let 〈pc,b1〉≝ next pmem pc in 〈〈MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,INDIRECT (from_singl … v)〉)))), pc〉, 2〉
    183          else
    184           let 〈b,v〉≝  head … v in if b then
    185            let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,DIRECT b2〉)))), pc〉, 2〉
    186           else
    187            〈〈DIV … ACC_A ACC_B, pc〉, 4〉
     175           let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inr … 〈DPTR,DATA16 (b1 @@ b2)〉)))), pc〉, 2〉
     176      else
     177       let 〈b,v〉≝  head … v in if b then
     178        let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,REGISTER v〉))))), pc〉, 2〉
     179       else
     180        let 〈b,v〉≝  head … v in if b then
     181         let 〈b,v〉≝  head … v in if b then
     182          let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,INDIRECT (from_singl … v)〉))))), pc〉, 2〉
     183         else
     184          let 〈b,v〉≝  head … v in if b then
     185           let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,DIRECT b2〉))))), pc〉, 2〉
     186          else
     187           〈〈RealInstruction (DIV … ACC_A ACC_B), pc〉, 4〉
    188188        else
    189189         let 〈b,v〉≝  head … v in if b then
     
    191191           〈〈MOVC … ACC_A (ACC_PC), pc〉, 2〉
    192192          else
    193            let 〈pc,b1〉≝ next pmem pc in 〈〈ANL … (inr … 〈CARRY,BIT_ADDR b1〉), pc〉, 2〉
     193           let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (ANL … (inr … 〈CARRY,BIT_ADDR b1〉)), pc〉, 2〉
    194194         else
    195195          let 〈b,v〉≝  head … v in if b then
     
    202202      let 〈b,v〉≝  head … v in if b then
    203203       let 〈b,v〉≝  head … v in if b then
    204         let 〈pc,b1〉≝ next pmem pc in 〈〈MOV … (inl … (inl … (inl … (inl … (inr … 〈REGISTER v,DATA b1〉))))), pc〉, 1〉
    205        else
    206         let 〈b,v〉≝  head … v in if b then
    207          let 〈b,v〉≝  head … v in if b then
    208           let 〈pc,b1〉≝ next pmem pc in 〈〈MOV … (inl … (inl … (inl … (inl … (inr … 〈INDIRECT (from_singl … v),DATA b1〉))))), pc〉, 1〉
    209          else
    210           let 〈b,v〉≝  head … v in if b then
    211            let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,DATA b2〉)))), pc〉, 3〉
    212           else
    213            let 〈pc,b1〉≝ next pmem pc in 〈〈MOV … (inl … (inl … (inl … (inl … (inl … 〈ACC_A,DATA b1〉))))), pc〉, 1〉
     204        let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inr … 〈REGISTER v,DATA b1〉)))))), pc〉, 1〉
     205       else
     206        let 〈b,v〉≝  head … v in if b then
     207         let 〈b,v〉≝  head … v in if b then
     208          let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inr … 〈INDIRECT (from_singl … v),DATA b1〉)))))), pc〉, 1〉
     209         else
     210          let 〈b,v〉≝  head … v in if b then
     211           let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,DATA b2〉))))), pc〉, 3〉
     212          else
     213           let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inl … 〈ACC_A,DATA b1〉)))))), pc〉, 1〉
    214214        else
    215215         let 〈b,v〉≝  head … v in if b then
     
    217217           〈〈JMP … INDIRECT_DPTR, pc〉, 2〉
    218218          else
    219            let 〈pc,b1〉≝ next pmem pc in 〈〈ORL … (inr … 〈CARRY,BIT_ADDR b1〉), pc〉, 2〉
     219           let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (ORL … (inr … 〈CARRY,BIT_ADDR b1〉)), pc〉, 2〉
    220220         else
    221221          let 〈b,v〉≝  head … v in if b then
    222222           let 〈pc,b1〉≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[true;false;false]]) @@ b1)), pc〉, 2〉
    223223          else
    224            let 〈pc,b1〉≝ next pmem pc in 〈〈Jump [[relative]] (JNZ … (RELATIVE b1)), pc〉, 2〉
    225       else
    226        let 〈b,v〉≝  head … v in if b then
    227         〈〈XRL … (inl … 〈ACC_A,REGISTER v〉), pc〉, 1〉
    228        else
    229         let 〈b,v〉≝  head … v in if b then
    230          let 〈b,v〉≝  head … v in if b then
    231           〈〈XRL … (inl … 〈ACC_A,INDIRECT (from_singl … v)〉), pc〉, 1〉
    232          else
    233           let 〈b,v〉≝  head … v in if b then
    234            let 〈pc,b1〉≝ next pmem pc in 〈〈XRL … (inl … 〈ACC_A,DIRECT b1〉), pc〉, 1〉
    235           else
    236            let 〈pc,b1〉≝ next pmem pc in 〈〈XRL … (inl … 〈ACC_A,DATA b1〉), pc〉, 1〉
    237         else
    238          let 〈b,v〉≝  head … v in if b then
    239           let 〈b,v〉≝  head … v in if b then
    240            let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈XRL … (inr … 〈DIRECT b1,DATA b2〉), pc〉, 2〉
    241           else
    242            let 〈pc,b1〉≝ next pmem pc in 〈〈XRL … (inr … 〈DIRECT b1,ACC_A〉), pc〉, 1〉
     224           let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (JNZ … (RELATIVE b1)), pc〉, 2〉
     225      else
     226       let 〈b,v〉≝  head … v in if b then
     227        〈〈RealInstruction (XRL … (inl … 〈ACC_A,REGISTER v〉)), pc〉, 1〉
     228       else
     229        let 〈b,v〉≝  head … v in if b then
     230         let 〈b,v〉≝  head … v in if b then
     231          〈〈RealInstruction (XRL … (inl … 〈ACC_A,INDIRECT (from_singl … v)〉)), pc〉, 1〉
     232         else
     233          let 〈b,v〉≝  head … v in if b then
     234           let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (XRL … (inl … 〈ACC_A,DIRECT b1〉)), pc〉, 1〉
     235          else
     236           let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (XRL … (inl … 〈ACC_A,DATA b1〉)), pc〉, 1〉
     237        else
     238         let 〈b,v〉≝  head … v in if b then
     239          let 〈b,v〉≝  head … v in if b then
     240           let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈RealInstruction (XRL … (inr … 〈DIRECT b1,DATA b2〉)), pc〉, 2〉
     241          else
     242           let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (XRL … (inr … 〈DIRECT b1,ACC_A〉)), pc〉, 1〉
    243243         else
    244244          let 〈b,v〉≝  head … v in if b then
    245245           let 〈pc,b1〉≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[true;false;false]]) @@ b1)), pc〉, 2〉
    246246          else
    247            let 〈pc,b1〉≝ next pmem pc in 〈〈Jump [[relative]] (JZ … (RELATIVE b1)), pc〉, 2〉
     247           let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (JZ … (RELATIVE b1)), pc〉, 2〉
    248248     else
    249249      let 〈b,v〉≝  head … v in if b then
    250250       let 〈b,v〉≝  head … v in if b then
    251         〈〈ANL … (inl … (inl … 〈ACC_A,REGISTER v〉)), pc〉, 1〉
    252        else
    253         let 〈b,v〉≝  head … v in if b then
    254          let 〈b,v〉≝  head … v in if b then
    255           〈〈ANL … (inl … (inl … 〈ACC_A,INDIRECT (from_singl … v)〉)), pc〉, 1〉
    256          else
    257           let 〈b,v〉≝  head … v in if b then
    258            let 〈pc,b1〉≝ next pmem pc in 〈〈ANL … (inl … (inl … 〈ACC_A,DIRECT b1〉)), pc〉, 1〉
    259           else
    260            let 〈pc,b1〉≝ next pmem pc in 〈〈ANL … (inl … (inl … 〈ACC_A,DATA b1〉)), pc〉, 1〉
    261         else
    262          let 〈b,v〉≝  head … v in if b then
    263           let 〈b,v〉≝  head … v in if b then
    264            let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈ANL … (inl … (inr … 〈DIRECT b1,DATA b2〉)), pc〉, 2〉
    265           else
    266            let 〈pc,b1〉≝ next pmem pc in 〈〈ANL … (inl … (inr … 〈DIRECT b1,ACC_A〉)), pc〉, 1〉
     251        〈〈RealInstruction (ANL … (inl … (inl … 〈ACC_A,REGISTER v〉))), pc〉, 1〉
     252       else
     253        let 〈b,v〉≝  head … v in if b then
     254         let 〈b,v〉≝  head … v in if b then
     255          〈〈RealInstruction (ANL … (inl … (inl … 〈ACC_A,INDIRECT (from_singl … v)〉))), pc〉, 1〉
     256         else
     257          let 〈b,v〉≝  head … v in if b then
     258           let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (ANL … (inl … (inl … 〈ACC_A,DIRECT b1〉))), pc〉, 1〉
     259          else
     260           let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (ANL … (inl … (inl … 〈ACC_A,DATA b1〉))), pc〉, 1〉
     261        else
     262         let 〈b,v〉≝  head … v in if b then
     263          let 〈b,v〉≝  head … v in if b then
     264           let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈RealInstruction (ANL … (inl … (inr … 〈DIRECT b1,DATA b2〉))), pc〉, 2〉
     265          else
     266           let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (ANL … (inl … (inr … 〈DIRECT b1,ACC_A〉))), pc〉, 1〉
    267267         else
    268268          let 〈b,v〉≝  head … v in if b then
    269269           let 〈pc,b1〉≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[true;false;true]]) @@ b1)), pc〉, 2〉
    270270          else
    271            let 〈pc,b1〉≝ next pmem pc in 〈〈Jump [[relative]] (JNC … (RELATIVE b1)), pc〉, 2〉
    272       else
    273        let 〈b,v〉≝  head … v in if b then
    274         〈〈ORL … (inl … (inl … 〈ACC_A,REGISTER v〉)), pc〉, 1〉
    275        else
    276         let 〈b,v〉≝  head … v in if b then
    277          let 〈b,v〉≝  head … v in if b then
    278           〈〈ORL … (inl … (inl … 〈ACC_A,INDIRECT (from_singl … v)〉)), pc〉, 1〉
    279          else
    280           let 〈b,v〉≝  head … v in if b then
    281            let 〈pc,b1〉≝ next pmem pc in 〈〈ORL … (inl … (inl … 〈ACC_A,DIRECT b1〉)), pc〉, 1〉
    282           else
    283            let 〈pc,b1〉≝ next pmem pc in 〈〈ORL … (inl … (inl … 〈ACC_A,DATA b1〉)), pc〉, 1〉
    284         else
    285          let 〈b,v〉≝  head … v in if b then
    286           let 〈b,v〉≝  head … v in if b then
    287            let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈ORL … (inl … (inr … 〈DIRECT b1,DATA b2〉)), pc〉, 2〉
    288           else
    289            let 〈pc,b1〉≝ next pmem pc in 〈〈ORL … (inl … (inr … 〈DIRECT b1,ACC_A〉)), pc〉, 1〉
     271           let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (JNC … (RELATIVE b1)), pc〉, 2〉
     272      else
     273       let 〈b,v〉≝  head … v in if b then
     274        〈〈RealInstruction (ORL … (inl … (inl … 〈ACC_A,REGISTER v〉))), pc〉, 1〉
     275       else
     276        let 〈b,v〉≝  head … v in if b then
     277         let 〈b,v〉≝  head … v in if b then
     278          〈〈RealInstruction (ORL … (inl … (inl … 〈ACC_A,INDIRECT (from_singl … v)〉))), pc〉, 1〉
     279         else
     280          let 〈b,v〉≝  head … v in if b then
     281           let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (ORL … (inl … (inl … 〈ACC_A,DIRECT b1〉))), pc〉, 1〉
     282          else
     283           let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (ORL … (inl … (inl … 〈ACC_A,DATA b1〉))), pc〉, 1〉
     284        else
     285         let 〈b,v〉≝  head … v in if b then
     286          let 〈b,v〉≝  head … v in if b then
     287           let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈RealInstruction (ORL … (inl … (inr … 〈DIRECT b1,DATA b2〉))), pc〉, 2〉
     288          else
     289           let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (ORL … (inl … (inr … 〈DIRECT b1,ACC_A〉))), pc〉, 1〉
    290290         else
    291291          let 〈b,v〉≝  head … v in if b then
    292292           let 〈pc,b1〉≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[true;false;true]]) @@ b1)), pc〉, 2〉
    293293          else
    294            let 〈pc,b1〉≝ next pmem pc in 〈〈Jump [[relative]] (JC … (RELATIVE b1)), pc〉, 2〉
     294           let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (JC … (RELATIVE b1)), pc〉, 2〉
    295295    else
    296296     let 〈b,v〉≝  head … v in if b then
    297297      let 〈b,v〉≝  head … v in if b then
    298298       let 〈b,v〉≝  head … v in if b then
    299         〈〈ADDC … ACC_A (REGISTER v), pc〉, 1〉
    300        else
    301         let 〈b,v〉≝  head … v in if b then
    302          let 〈b,v〉≝  head … v in if b then
    303           〈〈ADDC … ACC_A (INDIRECT (from_singl … v)), pc〉, 1〉
    304          else
    305           let 〈b,v〉≝  head … v in if b then
    306            let 〈pc,b1〉≝ next pmem pc in 〈〈ADDC … ACC_A (DIRECT b1), pc〉, 1〉
    307           else
    308            let 〈pc,b1〉≝ next pmem pc in 〈〈ADDC … ACC_A (DATA b1), pc〉, 1〉
    309         else
    310          let 〈b,v〉≝  head … v in if b then
    311           let 〈b,v〉≝  head … v in if b then
    312            〈〈RLC … ACC_A, pc〉, 1〉
    313           else
    314            〈〈RETI …, pc〉, 2〉
     299        〈〈RealInstruction (ADDC … ACC_A (REGISTER v)), pc〉, 1〉
     300       else
     301        let 〈b,v〉≝  head … v in if b then
     302         let 〈b,v〉≝  head … v in if b then
     303          〈〈RealInstruction (ADDC … ACC_A (INDIRECT (from_singl … v))), pc〉, 1〉
     304         else
     305          let 〈b,v〉≝  head … v in if b then
     306           let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (ADDC … ACC_A (DIRECT b1)), pc〉, 1〉
     307          else
     308           let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (ADDC … ACC_A (DATA b1)), pc〉, 1〉
     309        else
     310         let 〈b,v〉≝  head … v in if b then
     311          let 〈b,v〉≝  head … v in if b then
     312           〈〈RealInstruction (RLC … ACC_A), pc〉, 1〉
     313          else
     314           〈〈RealInstruction (RETI …), pc〉, 2〉
    315315         else
    316316          let 〈b,v〉≝  head … v in if b then
    317317           let 〈pc,b1〉≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[true;true;false]]) @@ b1)), pc〉, 2〉
    318318          else
    319            let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈Jump [[relative]] (JNB … (BIT_ADDR b1) (RELATIVE b2)), pc〉, 2〉
    320       else
    321        let 〈b,v〉≝  head … v in if b then
    322         〈〈ADD … ACC_A (REGISTER v), pc〉, 1〉
    323        else
    324         let 〈b,v〉≝  head … v in if b then
    325          let 〈b,v〉≝  head … v in if b then
    326           〈〈ADD … ACC_A (INDIRECT (from_singl … v)), pc〉, 1〉
    327          else
    328           let 〈b,v〉≝  head … v in if b then
    329            let 〈pc,b1〉≝ next pmem pc in 〈〈ADD … ACC_A (DIRECT b1), pc〉, 1〉
    330           else
    331            let 〈pc,b1〉≝ next pmem pc in 〈〈ADD … ACC_A (DATA b1), pc〉, 1〉
    332         else
    333          let 〈b,v〉≝  head … v in if b then
    334           let 〈b,v〉≝  head … v in if b then
    335            〈〈RL … ACC_A, pc〉, 1〉
    336           else
    337            〈〈RET …, pc〉, 2〉
     319           let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈RealInstruction (JNB … (BIT_ADDR b1) (RELATIVE b2)), pc〉, 2〉
     320      else
     321       let 〈b,v〉≝  head … v in if b then
     322        〈〈RealInstruction (ADD … ACC_A (REGISTER v)), pc〉, 1〉
     323       else
     324        let 〈b,v〉≝  head … v in if b then
     325         let 〈b,v〉≝  head … v in if b then
     326          〈〈RealInstruction (ADD … ACC_A (INDIRECT (from_singl … v))), pc〉, 1〉
     327         else
     328          let 〈b,v〉≝  head … v in if b then
     329           let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (ADD … ACC_A (DIRECT b1)), pc〉, 1〉
     330          else
     331           let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (ADD … ACC_A (DATA b1)), pc〉, 1〉
     332        else
     333         let 〈b,v〉≝  head … v in if b then
     334          let 〈b,v〉≝  head … v in if b then
     335           〈〈RealInstruction (RL … ACC_A), pc〉, 1〉
     336          else
     337           〈〈RealInstruction (RET …), pc〉, 2〉
    338338         else
    339339          let 〈b,v〉≝  head … v in if b then
    340340           let 〈pc,b1〉≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[true;true;false]]) @@ b1)), pc〉, 2〉
    341341          else
    342            let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈Jump [[relative]] (JB … (BIT_ADDR b1) (RELATIVE b2)), pc〉, 2〉
     342           let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈RealInstruction (JB … (BIT_ADDR b1) (RELATIVE b2)), pc〉, 2〉
    343343     else
    344344      let 〈b,v〉≝  head … v in if b then
    345345       let 〈b,v〉≝  head … v in if b then
    346         〈〈DEC … (REGISTER v), pc〉, 1〉
    347        else
    348         let 〈b,v〉≝  head … v in if b then
    349          let 〈b,v〉≝  head … v in if b then
    350           〈〈DEC … (INDIRECT (from_singl … v)), pc〉, 1〉
    351          else
    352           let 〈b,v〉≝  head … v in if b then
    353            let 〈pc,b1〉≝ next pmem pc in 〈〈DEC … (DIRECT b1), pc〉, 1〉
    354           else
    355            〈〈DEC … ACC_A, pc〉, 1〉
    356         else
    357          let 〈b,v〉≝  head … v in if b then
    358           let 〈b,v〉≝  head … v in if b then
    359            〈〈RRC … ACC_A, pc〉, 1〉
     346        〈〈RealInstruction (DEC … (REGISTER v)), pc〉, 1〉
     347       else
     348        let 〈b,v〉≝  head … v in if b then
     349         let 〈b,v〉≝  head … v in if b then
     350          〈〈RealInstruction (DEC … (INDIRECT (from_singl … v))), pc〉, 1〉
     351         else
     352          let 〈b,v〉≝  head … v in if b then
     353           let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (DEC … (DIRECT b1)), pc〉, 1〉
     354          else
     355           〈〈RealInstruction (DEC … ACC_A), pc〉, 1〉
     356        else
     357         let 〈b,v〉≝  head … v in if b then
     358          let 〈b,v〉≝  head … v in if b then
     359           〈〈RealInstruction (RRC … ACC_A), pc〉, 1〉
    360360          else
    361361           let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈LCALL … (ADDR16 (b1 @@ b2)), pc〉, 2〉
     
    364364           let 〈pc,b1〉≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[true;true;true]]) @@ b1)), pc〉, 2〉
    365365          else
    366            let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈Jump [[relative]] (JBC … (BIT_ADDR b1) (RELATIVE b2)), pc〉, 2〉
    367       else
    368        let 〈b,v〉≝  head … v in if b then
    369         〈〈INC … (REGISTER v), pc〉, 1〉
    370        else
    371         let 〈b,v〉≝  head … v in if b then
    372          let 〈b,v〉≝  head … v in if b then
    373           〈〈INC … (INDIRECT (from_singl … v)), pc〉, 1〉
    374          else
    375           let 〈b,v〉≝  head … v in if b then
    376            let 〈pc,b1〉≝ next pmem pc in 〈〈INC … (DIRECT b1), pc〉, 1〉
    377           else
    378            〈〈INC … ACC_A, pc〉, 1〉
    379         else
    380          let 〈b,v〉≝  head … v in if b then
    381           let 〈b,v〉≝  head … v in if b then
    382            〈〈RR … ACC_A, pc〉, 1〉
     366           let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈RealInstruction (JBC … (BIT_ADDR b1) (RELATIVE b2)), pc〉, 2〉
     367      else
     368       let 〈b,v〉≝  head … v in if b then
     369        〈〈RealInstruction (INC … (REGISTER v)), pc〉, 1〉
     370       else
     371        let 〈b,v〉≝  head … v in if b then
     372         let 〈b,v〉≝  head … v in if b then
     373          〈〈RealInstruction (INC … (INDIRECT (from_singl … v))), pc〉, 1〉
     374         else
     375          let 〈b,v〉≝  head … v in if b then
     376           let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (INC … (DIRECT b1)), pc〉, 1〉
     377          else
     378           〈〈RealInstruction (INC … ACC_A), pc〉, 1〉
     379        else
     380         let 〈b,v〉≝  head … v in if b then
     381          let 〈b,v〉≝  head … v in if b then
     382           〈〈RealInstruction (RR … ACC_A), pc〉, 1〉
    383383          else
    384384           let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈LJMP … (ADDR16 (b1 @@ b2)), pc〉, 2〉
     
    387387           let 〈pc,b1〉≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[true;true;true]]) @@ b1)), pc〉, 2〉
    388388          else
    389            〈〈NOP …, pc〉, 1〉.
     389           〈〈RealInstruction (NOP …), pc〉, 1〉.
    390390  %.
    391391qed.
  • src/ASM/Interpret.ma

    r757 r820  
    158158include alias "ASM/BitVectorTrie.ma".
    159159
    160 definition execute_1: Status → Status ≝
     160definition execute_1_preinstruction: ∀A: Type[0]. (A → Byte) → preinstruction A → Status → Status ≝
     161  λA: Type[0].
     162  λaddr_of: A → Byte.
     163  λinstr: preinstruction A.
    161164  λs: Status.
    162     let 〈instr_pc, ticks〉 ≝ fetch (code_memory s) (program_counter s) in
    163     let 〈instr, pc〉 ≝ 〈fst … instr_pc, snd … instr_pc〉 in
    164     let s ≝ set_clock s (clock s + ticks) in
    165     let s ≝ set_program_counter s pc in
    166     let s ≝
    167       match instr with
     165  match instr with
    168166        [ ADD addr1 addr2 ⇒
    169167            let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 s false addr1)
     
    397395            let new_pc ≝ high_bits @@ low_bits in
    398396              set_program_counter s new_pc
    399         | JMP _ ⇒ (* DPM: always indirect_dptr *)
    400           let dptr ≝ (get_8051_sfr s SFR_DPH) @@ (get_8051_sfr s SFR_DPL) in
    401           let big_acc ≝ (zero 8) @@ (get_8051_sfr s SFR_ACC_A) in
    402           let 〈carry, jmp_addr〉 ≝ half_add ? big_acc dptr in
    403           let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) jmp_addr in
    404             set_program_counter s new_pc
    405         | LJMP addr ⇒
    406           match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → ? with
    407             [ ADDR16 a ⇒ λaddr16: True.
    408                 set_program_counter s a
    409             | _ ⇒ λother: False. ⊥
    410             ] (subaddressing_modein … addr)
    411         | SJMP addr ⇒
    412           match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
    413             [ RELATIVE r ⇒ λrelative: True.
    414                 let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in
    415                   set_program_counter s new_pc
    416             | _ ⇒ λother: False. ⊥
    417             ] (subaddressing_modein … addr)
    418         | AJMP addr ⇒
    419           match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → ? with
    420             [ ADDR11 a ⇒ λaddr11: True.
    421               let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter s) in
    422               let 〈nu, nl〉 ≝ split ? 4 4 pc_bu in
    423               let bit ≝ get_index' ? O ? nl in
    424               let 〈relevant1, relevant2〉 ≝ split ? 3 8 a in
    425               let new_addr ≝ (nu @@ (bit ::: relevant1)) @@ relevant2 in
    426               let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) new_addr in
    427                 set_program_counter s new_pc
    428             | _ ⇒ λother: False. ⊥
    429             ] (subaddressing_modein … addr)
    430397        | MOVX addr ⇒
    431398          (* DPM: only copies --- doesn't affect I/O *)
     
    471438                set_arg_1 s addr1 (get_arg_1 s addr2 false)
    472439            ]
    473         | LCALL addr ⇒
    474           match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → ? with
    475             [ ADDR16 a ⇒ λaddr16: True.
    476               let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr s SFR_SP) (bitvector_of_nat 8 1) in
    477               let s ≝ set_8051_sfr s SFR_SP new_sp in
    478               let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter s) in
    479               let s ≝ write_at_stack_pointer s pc_bl in
    480               let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr s SFR_SP) (bitvector_of_nat 8 1) in
    481               let s ≝ set_8051_sfr s SFR_SP new_sp in
    482               let s ≝ write_at_stack_pointer s pc_bu in
    483                 set_program_counter s a
    484             | _ ⇒ λother: False. ⊥
    485             ] (subaddressing_modein … addr)
    486         | ACALL addr ⇒
    487           match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → ? with
    488             [ ADDR11 a ⇒ λaddr11: True.
    489               let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr s SFR_SP) (bitvector_of_nat 8 1) in
    490               let s ≝ set_8051_sfr s SFR_SP new_sp in
    491               let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter s) in
    492               let s ≝ write_at_stack_pointer s pc_bl in
    493               let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr s SFR_SP) (bitvector_of_nat 8 1) in
    494               let s ≝ set_8051_sfr s SFR_SP new_sp in
    495               let s ≝ write_at_stack_pointer s pc_bu in
    496               let 〈thr, eig〉 ≝ split ? 3 8 a in
    497               let 〈fiv, thr'〉 ≝ split ? 5 3 pc_bu in
    498               let new_addr ≝ (fiv @@ thr) @@ pc_bl in
    499                 set_program_counter s new_addr
    500             | _ ⇒ λother: False. ⊥
    501             ] (subaddressing_modein … addr)
    502         | Jump j ⇒
    503           match j with
    504             [ JC addr ⇒
    505               match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
    506                 [ RELATIVE r ⇒ λrel: True.
     440          | JC addr ⇒
     441              let r ≝ addr_of addr in
    507442                  if get_cy_flag s then
    508443                    let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in
     
    510445                  else
    511446                    s
    512                 | _ ⇒ λother: False. ⊥
    513                 ] (subaddressing_modein … addr)
    514447            | JNC addr ⇒
    515               match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
    516                 [ RELATIVE r ⇒ λrel: True.
     448              let r ≝ addr_of addr in
    517449                  if ¬(get_cy_flag s) then
    518450                    let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in
     
    520452                  else
    521453                    s
    522                 | _ ⇒ λother: False. ⊥
    523                 ] (subaddressing_modein … addr)
    524454            | JB addr1 addr2 ⇒
    525               match addr2 return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
    526                 [ RELATIVE r ⇒ λrel: True.
     455              let r ≝ addr_of addr2 in
    527456                  if get_arg_1 s addr1 false then
    528457                    let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in
     
    530459                  else
    531460                    s
    532                 | _ ⇒ λother: False. ⊥
    533                 ] (subaddressing_modein … addr2)
    534461            | JNB addr1 addr2 ⇒
    535               match addr2 return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
    536                 [ RELATIVE r ⇒ λrel: True.
     462              let r ≝ addr_of addr2 in
    537463                  if ¬(get_arg_1 s addr1 false) then
    538464                    let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in
     
    540466                  else
    541467                    s
    542                 | _ ⇒ λother: False. ⊥
    543                 ] (subaddressing_modein … addr2)
    544468            | JBC addr1 addr2 ⇒
    545               match addr2 return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
    546                 [ RELATIVE r ⇒ λrel: True.
     469              let r ≝ addr_of addr2 in
    547470                  let s ≝ set_arg_1 s addr1 false in
    548471                    if get_arg_1 s addr1 false then
     
    551474                    else
    552475                      s
    553                 | _ ⇒ λother: False. ⊥
    554                 ] (subaddressing_modein … addr2)
    555476            | JZ addr ⇒
    556               match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
    557                 [ RELATIVE r ⇒ λrel: True.
     477              let r ≝ addr_of addr in
    558478                    if eq_bv ? (get_8051_sfr s SFR_ACC_A) (zero 8) then
    559479                      let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in
     
    561481                    else
    562482                      s
    563                 | _ ⇒ λother: False. ⊥
    564                 ] (subaddressing_modein … addr)
    565483            | JNZ addr ⇒
    566               match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
    567                 [ RELATIVE r ⇒ λrel: True.
     484              let r ≝ addr_of addr in
    568485                    if ¬(eq_bv ? (get_8051_sfr s SFR_ACC_A) (zero 8)) then
    569486                      let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in
     
    571488                    else
    572489                      s
    573                 | _ ⇒ λother: False. ⊥
    574                 ] (subaddressing_modein … addr)
    575490            | CJNE addr1 addr2 ⇒
    576               match addr2 return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
    577                 [ RELATIVE r ⇒ λrelative: True.
     491              let r ≝ addr_of addr2 in
    578492                  match addr1 with
    579493                    [ inl l ⇒
     
    598512                            (set_flags s new_cy (None ?) (get_ov_flag s))
    599513                    ]
    600                 | _ ⇒ λother: False. ⊥
    601                 ] (subaddressing_modein … addr2)
    602514            | DJNZ addr1 addr2 ⇒
    603               match addr2 return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
    604                 [ RELATIVE r ⇒ λrel: True.
    605                     let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 s true addr1) (bitvector_of_nat 8 1) false in
    606                     let s ≝ set_arg_8 s addr1 result in
    607                       if ¬(eq_bv ? result (zero 8)) then
    608                         let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in
    609                           set_program_counter s new_pc
    610                       else
    611                         s
    612                 | _ ⇒ λother: False. ⊥
    613                 ] (subaddressing_modein … addr2)
    614             ]
     515              let r ≝ addr_of addr2 in
     516              let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 s true addr1) (bitvector_of_nat 8 1) false in
     517              let s ≝ set_arg_8 s addr1 result in
     518                if ¬(eq_bv ? result (zero 8)) then
     519                  let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in
     520                    set_program_counter s new_pc
     521                else
     522                  s
     523        | NOP ⇒ s
     524        ].
     525    try assumption
     526    try (
     527      normalize
     528      repeat (@ (le_S_S))
     529      @ (le_O_n)
     530    )
     531    try (
     532      @ (execute_1_technical … (subaddressing_modein …))
     533      @ I
     534    )
     535    try (
     536      normalize
     537      @ I
     538    )
     539qed.
     540
     541definition execute_1: Status → Status ≝
     542  λs: Status.
     543    let 〈instr_pc, ticks〉 ≝ fetch (code_memory s) (program_counter s) in
     544    let 〈instr, pc〉 ≝ 〈fst … instr_pc, snd … instr_pc〉 in
     545    let s ≝ set_clock s (clock s + ticks) in
     546    let s ≝ set_program_counter s pc in
     547    let s ≝
     548      match instr with
     549      [ RealInstruction instr ⇒ execute_1_preinstruction [[ relative ]]
     550        (λx.
     551        match x return λs. bool_to_Prop (is_in ? [[ relative ]] s) → ? with
     552        [ RELATIVE r ⇒ λ_. r
     553        | _ ⇒ λabsd. ⊥
     554        ] (subaddressing_modein … x)) instr s
     555      | ACALL addr ⇒
     556          match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → ? with
     557            [ ADDR11 a ⇒ λaddr11: True.
     558              let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr s SFR_SP) (bitvector_of_nat 8 1) in
     559              let s ≝ set_8051_sfr s SFR_SP new_sp in
     560              let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter s) in
     561              let s ≝ write_at_stack_pointer s pc_bl in
     562              let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr s SFR_SP) (bitvector_of_nat 8 1) in
     563              let s ≝ set_8051_sfr s SFR_SP new_sp in
     564              let s ≝ write_at_stack_pointer s pc_bu in
     565              let 〈thr, eig〉 ≝ split ? 3 8 a in
     566              let 〈fiv, thr'〉 ≝ split ? 5 3 pc_bu in
     567              let new_addr ≝ (fiv @@ thr) @@ pc_bl in
     568                set_program_counter s new_addr
     569            | _ ⇒ λother: False. ⊥
     570            ] (subaddressing_modein … addr)
     571        | LCALL addr ⇒
     572          match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → ? with
     573            [ ADDR16 a ⇒ λaddr16: True.
     574              let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr s SFR_SP) (bitvector_of_nat 8 1) in
     575              let s ≝ set_8051_sfr s SFR_SP new_sp in
     576              let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter s) in
     577              let s ≝ write_at_stack_pointer s pc_bl in
     578              let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr s SFR_SP) (bitvector_of_nat 8 1) in
     579              let s ≝ set_8051_sfr s SFR_SP new_sp in
     580              let s ≝ write_at_stack_pointer s pc_bu in
     581                set_program_counter s a
     582            | _ ⇒ λother: False. ⊥
     583            ] (subaddressing_modein … addr)
    615584        | MOVC addr1 addr2 ⇒
    616585          match addr2 return λx. bool_to_Prop (is_in … [[ acc_dptr; acc_pc ]] x) → ? with
     
    632601            | _ ⇒ λother: False. ⊥
    633602            ] (subaddressing_modein … addr2)
    634         | NOP ⇒ s
    635         ]
     603        | JMP _ ⇒ (* DPM: always indirect_dptr *)
     604          let dptr ≝ (get_8051_sfr s SFR_DPH) @@ (get_8051_sfr s SFR_DPL) in
     605          let big_acc ≝ (zero 8) @@ (get_8051_sfr s SFR_ACC_A) in
     606          let 〈carry, jmp_addr〉 ≝ half_add ? big_acc dptr in
     607          let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) jmp_addr in
     608            set_program_counter s new_pc
     609        | LJMP addr ⇒
     610          match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → ? with
     611            [ ADDR16 a ⇒ λaddr16: True.
     612                set_program_counter s a
     613            | _ ⇒ λother: False. ⊥
     614            ] (subaddressing_modein … addr)
     615        | SJMP addr ⇒
     616          match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
     617            [ RELATIVE r ⇒ λrelative: True.
     618                let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in
     619                  set_program_counter s new_pc
     620            | _ ⇒ λother: False. ⊥
     621            ] (subaddressing_modein … addr)
     622        | AJMP addr ⇒
     623          match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → ? with
     624            [ ADDR11 a ⇒ λaddr11: True.
     625              let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter s) in
     626              let 〈nu, nl〉 ≝ split ? 4 4 pc_bu in
     627              let bit ≝ get_index' ? O ? nl in
     628              let 〈relevant1, relevant2〉 ≝ split ? 3 8 a in
     629              let new_addr ≝ (nu @@ (bit ::: relevant1)) @@ relevant2 in
     630              let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) new_addr in
     631                set_program_counter s new_pc
     632            | _ ⇒ λother: False. ⊥
     633            ] (subaddressing_modein … addr)
     634      ]
    636635    in
    637636      s.
     
    652651qed.
    653652
     653axiom fetch_pseudo_instruction:
     654  ∀p: list labelled_instruction.
     655  ∀pc: Word.
     656    (pseudo_instruction × Word) × nat.
     657
     658axiom address_of_labels: Identifier → Byte.
     659axiom address_of_word_labels: Identifier → Word.
     660
     661definition execute_1_pseudo_instruction: pseudo_assembly_program → Status → Status ≝
     662  λp.
     663  λs.
     664  let 〈instr_pc, ticks〉 ≝ fetch_pseudo_instruction (\snd p) (program_counter s) in
     665  let 〈instr, pc〉 ≝ 〈fst … instr_pc, snd … instr_pc〉 in
     666  let s ≝ set_clock s (clock s + ticks) in
     667  let s ≝ set_program_counter s pc in
     668  let s ≝
     669    match instr with
     670    [ Instruction instr ⇒ execute_1_preinstruction ? address_of_labels instr s
     671    | Comment cmt ⇒ s
     672    | Cost cst ⇒ s
     673    | Jmp jmp ⇒ set_program_counter s (address_of_word_labels jmp)
     674    | Call call ⇒
     675      let a ≝ address_of_word_labels call in
     676      let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr s SFR_SP) (bitvector_of_nat 8 1) in
     677      let s ≝ set_8051_sfr s SFR_SP new_sp in
     678      let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter s) in
     679      let s ≝ write_at_stack_pointer s pc_bl in
     680      let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr s SFR_SP) (bitvector_of_nat 8 1) in
     681      let s ≝ set_8051_sfr s SFR_SP new_sp in
     682      let s ≝ write_at_stack_pointer s pc_bu in
     683        set_program_counter s a
     684    | Mov dptr ident ⇒ set_arg_16 s (get_arg_16 s (DATA16 (address_of_word_labels ident))) dptr
     685    ]
     686  in
     687    s.
     688  normalize
     689  @ I
     690qed.
     691
    654692let rec execute (n: nat) (s: Status) on n: Status ≝
    655693  match n with
     
    657695    | S o ⇒ execute o (execute_1 s)
    658696    ].
     697
     698let rec execute_pseudo_instruction (n: nat) (p: pseudo_assembly_program) (s: Status) on n: Status ≝
     699  match n with
     700    [ O ⇒ s
     701    | S o ⇒ execute_pseudo_instruction o p (execute_1_pseudo_instruction p s)
     702    ].
Note: See TracChangeset for help on using the changeset viewer.