Changeset 293


Ignore:
Timestamp:
Nov 25, 2010, 3:09:42 PM (9 years ago)
Author:
sacerdot
Message:

...

Location:
Deliverables/D4.1/Matita
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D4.1/Matita/ASM.ma

    r283 r293  
    9999  JC: A → jump A
    100100| JNC: A → jump A
    101 | JB: Bit → A → jump A
    102 | JNB: Bit → A → jump A
    103 | JBC: Bit → A → jump A
     101| JB: [[bit_addr]] → A → jump A
     102| JNB: [[bit_addr]] → A → jump A
     103| JBC: [[bit_addr]] → A → jump A
    104104| JZ: A → jump A
    105105| JNZ: A → jump A
    106106| CJNE:
    107    [[acc_a]] × [[direct; data]] ⊎
    108    [[register; indirect]] × [[data]] → A → jump A
     107   [[acc_a]] × [[direct; data]] ⊎ [[register; indirect]] × [[data]] → A → jump A
    109108| DJNZ: [[register ; direct]] → A → jump A.
    110109
  • Deliverables/D4.1/Matita/Assembly.ma

    r284 r293  
    22
    33ndefinition assembly1 ≝
    4  λA.λi: preinstruction A.match i with
     4 λi: instruction.match i with
    55  [ ACALL addr ⇒
    66     match addr return λx. bool_to_Prop (is_in ? [[addr11]] x) → ? with
     
    5454          | N_BIT_ADDR b1 ⇒ λ_. [ ([[true;false;true;true;false;false;false;false]]) ; b1 ]
    5555          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]
    56   (*
    57   | `CJNE (`U1 (`A, `DIRECT b1), `REL b2) ->
    58     [mk_byte_from_bits ((true,false,true,true),(false,true,false,true)); b1; b2]
    59   | `CJNE (`U1 (`A, `DATA b1), `REL b2) ->
    60     [mk_byte_from_bits ((true,false,true,true),(false,true,false,false)); b1; b2]
    61   | `CJNE (`U2 (`REG(r1,r2,r3), `DATA b1), `REL b2) ->
    62     [mk_byte_from_bits ((true,false,true,true),(true,r1,r2,r3)); b1; b2]
    63   | `CJNE (`U2 (`INDIRECT i1, `DATA b1), `REL b2) ->
    64     [mk_byte_from_bits ((true,false,true,true),(false,true,true,i1)); b1; b2]
    65   *)
    6656  | CLR addr ⇒
    6757     match addr return λx. bool_to_Prop (is_in ? [[acc_a;carry;bit_addr]] x) → ? with
     
    9787  | DIV addr1 addr2 ⇒
    9888     [ ([[true;false;false;false;false;true;false;false]]) ]
    99 
     89  | Jump j ⇒
     90     match j with
     91      [ DJNZ addr1 addr2 ⇒
     92         let b2 ≝
     93          match addr2 return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with
     94           [ RELATIVE b2 ⇒ λ_. b2
     95           | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) in
     96         match addr1 return λx. bool_to_Prop (is_in ? [[register;direct]] x) → ? with
     97          [ REGISTER r1 r2 r3 ⇒ λ_.
     98             [ ([[true; true; false; true; true; r1; r2; r3]]) ; 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         match addr return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with
     104          [ RELATIVE b1 ⇒ λ_.
     105             [ ([[false; true; false; false; false; false; false; false]]); b1 ]
     106          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
     107      | JNC addr ⇒
     108         match addr return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with
     109          [ RELATIVE b1 ⇒ λ_.
     110             [ ([[false; true; false; true; false; false; false; false]]); b1 ]
     111          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
     112      | JZ addr ⇒
     113         match addr return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with
     114          [ RELATIVE b1 ⇒ λ_.
     115             [ ([[false; true; true; false; false; false; false; false]]); b1 ]
     116          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
     117      | JNZ addr ⇒
     118         match addr return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with
     119          [ RELATIVE b1 ⇒ λ_.
     120             [ ([[false; true; true; true; false; false; false; false]]); b1 ]
     121          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
     122      | JB addr1 addr2 ⇒
     123         let b2 ≝
     124          match addr2 return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with
     125           [ RELATIVE b2 ⇒ λ_. b2
     126           | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) in
     127         match addr1 return λx. bool_to_Prop (is_in ? [[bit_addr]] x) → ? with
     128          [ BIT_ADDR b1 ⇒ λ_.
     129             [ ([[false; false; true; false; false; false; false; false]]); b1; b2 ]
     130          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)
     131      | JNB addr1 addr2 ⇒
     132         let b2 ≝
     133          match addr2 return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with
     134           [ RELATIVE b2 ⇒ λ_. b2
     135           | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) in
     136         match addr1 return λx. bool_to_Prop (is_in ? [[bit_addr]] x) → ? with
     137          [ BIT_ADDR b1 ⇒ λ_.
     138             [ ([[false; false; true; true; false; false; false; false]]); b1; b2 ]
     139          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)
     140      | JBC addr1 addr2 ⇒
     141         let b2 ≝
     142          match addr2 return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with
     143           [ RELATIVE b2 ⇒ λ_. b2
     144           | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) in
     145         match addr1 return λx. bool_to_Prop (is_in ? [[bit_addr]] x) → ? with
     146          [ BIT_ADDR b1 ⇒ λ_.
     147             [ ([[false; false; false; true; false; false; false; false]]); b1; b2 ]
     148          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)
     149      | CJNE addrs addr3 ⇒
     150         let b3 ≝
     151          match addr3 return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with
     152           [ RELATIVE b3 ⇒ λ_. b3
     153           | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr3) in
     154         match addrs with
     155          [ Left addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
     156             match addr2 return λx. bool_to_Prop (is_in ? [[direct;data]] x) → ? with
     157              [ DIRECT b1 ⇒ λ_.
     158                 [ ([[true; false; true; true; false; true; false; true]]); b1; b3 ]
     159              [ DATA b1 ⇒ λ_.
     160                 [ ([[true; false; true; true; false; true; false; false]]); b1; b3 ]
     161              | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
     162          | Right addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
     163             let b2 ≝
     164              match addr2 return λx. bool_to_Prop (is_in ? [[data]] x) → ? with
     165               [ DATA b2 ⇒ λ_. b2
     166               | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) in
     167             match addr2 return λx. bool_to_Prop (is_in ? [[direct;data]] x) → ? with
     168              [ DIRECT b1 ⇒ λ_.
     169                 [ ([[true; false; true; true; false; true; false; true]]); b1; b3 ]
     170              [ DATA b1 ⇒ λ_.
     171                 [ ([[true; false; true; true; false; true; false; false]]); b1; b3 ]
     172              | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
     173
     174          ]
     175      | _ ⇒ [ ]
     176      ]
    100177  | _ ⇒ [ ]].
    101178
    102179(*
    103   | `DJNZ (`REG(r1,r2,r3), `REL b1) ->
    104     [mk_byte_from_bits ((true,true,false,true),(true,r1,r2,r3)); b1]
    105   | `DJNZ (`DIRECT b1, `REL b2) ->
    106     [mk_byte_from_bits ((true,true,false,true),(false,true,false,true)); b1; b2]
     180  | `CJNE (`U2 (`REG(r1,r2,r3), `DATA b1), `REL b2) ->
     181    [mk_byte_from_bits ((true,false,true,true),(true,r1,r2,r3)); b1; b2]
     182  | `CJNE (`U2 (`INDIRECT i1, `DATA b1), `REL b2) ->
     183    [mk_byte_from_bits ((true,false,true,true),(false,true,true,i1)); b1; b2]
     184
     185
    107186  | `INC `A ->
    108187    [mk_byte_from_bits ((false,false,false,false),(false,true,false,false))]
     
    115194  | `INC `DPTR ->
    116195    [mk_byte_from_bits ((true,false,true,false),(false,false,true,true))]
    117   | `JB (`BIT b1, `REL b2) ->
    118     [mk_byte_from_bits ((false,false,true,false),(false,false,false,false)); b1; b2]
    119   | `JBC (`BIT b1, `REL b2) ->
    120     [mk_byte_from_bits ((false,false,false,true),(false,false,false,false)); b1; b2]
    121   | `JC (`REL b1) ->
    122     [mk_byte_from_bits ((false,true,false,false),(false,false,false,false)); b1]
    123196  | `JMP `IND_DPTR ->
    124197    [mk_byte_from_bits ((false,true,true,true),(false,false,true,true))]
    125   | `JNB (`BIT b1, `REL b2) ->
    126     [mk_byte_from_bits ((false,false,true,true),(false,false,false,false)); b1; b2]
    127   | `JNC (`REL b1) ->
    128     [mk_byte_from_bits ((false,true,false,true),(false,false,false,false)); b1]
    129   | `JNZ (`REL b1) ->
    130     [mk_byte_from_bits ((false,true,true,true),(false,false,false,false)); b1]
    131   | `JZ (`REL b1) ->
    132     [mk_byte_from_bits ((false,true,true,false),(false,false,false,false)); b1]
    133198  | `LCALL (`ADDR16 w) ->
    134199      let (b1,b2) = from_word w in
Note: See TracChangeset for help on using the changeset viewer.