source: Deliverables/D4.1/Matita/Interpret.ma @ 337

Last change on this file since 337 was 337, checked in by mulligan, 9 years ago

Changes to execute_1 file. Changes to get everything type checking.

File size: 9.8 KB
Line 
1include "Status.ma".
2(* include "Fetch.ma". *)
3include "Cartesian.ma".
4include "Arithmetic.ma".
5include "List.ma".
6
7naxiom fetch: BitVectorTrie Byte sixteen → Word → (preinstruction [[relative]]) × Word × Nat.
8
9alias id "inclusive_disjunction" = "cic:/matita/ng/Bool/inclusive_disjunction.fix(0,0,1)".
10
11ndefinition execute_1: Status → Status ≝
12  λs.
13    let 〈 instr_pc, ticks 〉 ≝ fetch (code_memory s) (program_counter s) in
14    let 〈 instr, pc 〉 ≝ 〈 first … instr_pc, second … instr_pc 〉 in
15    let s ≝ set_clock s (clock s + ticks) in
16    let s ≝ set_program_counter s pc in
17    let s ≝
18      match instr with
19        [ ADD addr1 addr2 ⇒
20            let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 s false addr1)
21                                                   (get_arg_8 s false addr2) false in
22            let cy_flag ≝ get_index … flags Z ? in
23            let ac_flag ≝ get_index … flags one ? in
24            let ov_flag ≝ get_index … flags two ? in
25            let s ≝ set_arg_8 s ACC_A result in
26              set_flags s cy_flag (Just Bit ac_flag) ov_flag
27        | ADDC addr1 addr2 ⇒
28            let old_cy_flag ≝ get_cy_flag s in
29            let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 s false addr1)
30                                                   (get_arg_8 s false addr2) old_cy_flag in
31            let cy_flag ≝ get_index … flags Z ? in
32            let ac_flag ≝ get_index … flags one ? in
33            let ov_flag ≝ get_index … flags two ? in
34            let s ≝ set_arg_8 s ACC_A result in
35              set_flags s cy_flag (Just Bit ac_flag) ov_flag
36        | SUBB addr1 addr2 ⇒
37            let old_cy_flag ≝ get_cy_flag s in
38            let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 s false addr1)
39                                                   (get_arg_8 s false addr2) old_cy_flag in
40            let cy_flag ≝ get_index … flags Z ? in
41            let ac_flag ≝ get_index … flags one ? in
42            let ov_flag ≝ get_index … flags two ? in
43            let s ≝ set_arg_8 s ACC_A result in
44              set_flags s cy_flag (Just Bit ac_flag) ov_flag
45        | INC addr ⇒
46            match addr return λx. bool_to_Prop (is_in … [[ acc_a;
47                                                           register;
48                                                           direct;
49                                                           indirect;
50                                                           dptr ]] x) → ? with
51              [ ACC_A ⇒ λacc_a: True.
52                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 s true ACC_A) (bitvector_of_nat eight one) in
53                  set_arg_8 s ACC_A result
54              | REGISTER r ⇒ λregister: True.
55                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 s true (REGISTER r)) (bitvector_of_nat eight one) in
56                  set_arg_8 s (REGISTER r) result
57              | DIRECT d ⇒ λdirect: True.
58                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 s true (DIRECT d)) (bitvector_of_nat eight one) in
59                  set_arg_8 s (DIRECT d) result
60              | INDIRECT i ⇒ λindirect: True.
61                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 s true (INDIRECT i)) (bitvector_of_nat eight one) in
62                  set_arg_8 s (INDIRECT i) result
63              | DPTR ⇒ λdptr: True.
64                let 〈 carry, bl 〉 ≝ half_add ? (get_8051_sfr s SFR_DPL) (bitvector_of_nat eight one) in
65                let 〈 carry, bu 〉 ≝ full_add ? (get_8051_sfr s SFR_DPH) (zero eight) carry in
66                let s ≝ set_8051_sfr s SFR_DPL bl in
67                  set_8051_sfr s SFR_DPH bu
68              | _ ⇒ λother: False. ?
69              ] (subaddressing_modein … addr)
70       | DEC addr ⇒
71           let 〈 result, flags 〉 ≝ sub_8_with_carry (get_arg_8 s true addr) (bitvector_of_nat eight one) false in
72             set_arg_8 s addr result
73        | MUL addr1 addr2 ⇒
74           let acc_a_nat ≝ nat_of_bitvector eight (get_8051_sfr s SFR_ACC_A) in
75           let acc_b_nat ≝ nat_of_bitvector eight (get_8051_sfr s SFR_ACC_B) in
76           let product ≝ acc_a_nat * acc_b_nat in
77           let ov_flag ≝ product ≥ two_hundred_and_fifty_six in
78           let low ≝ bitvector_of_nat eight (product mod two_hundred_and_fifty_six) in
79           let high ≝ bitvector_of_nat eight (product ÷ two_hundred_and_fifty_six) in
80           let s ≝ set_8051_sfr s SFR_ACC_A low in
81             set_8051_sfr s SFR_ACC_B high
82        | DIV addr1 addr2 ⇒
83           let acc_a_nat ≝ nat_of_bitvector eight (get_8051_sfr s SFR_ACC_A) in
84           let acc_b_nat ≝ nat_of_bitvector eight (get_8051_sfr s SFR_ACC_B) in
85             match acc_b_nat with
86               [ Z ⇒ set_flags s false (Nothing Bit) true
87               | S o ⇒
88                 let q ≝ bitvector_of_nat eight (acc_a_nat ÷ (S o)) in
89                 let r ≝ bitvector_of_nat eight (acc_a_nat mod two_hundred_and_fifty_six) in
90                 let s ≝ set_8051_sfr s SFR_ACC_A q in
91                 let s ≝ set_8051_sfr s SFR_ACC_B r in
92                   set_flags s false (Nothing Bit) false
93               ]
94        | DA addr ⇒
95            let 〈 acc_nu, acc_nl 〉 ≝ split ? four four (get_8051_sfr s SFR_ACC_A) in
96              if inclusive_disjunction (greater_than_b (nat_of_bitvector ? acc_nl) nine) (get_ac_flag s) then
97                let 〈result, flags〉 ≝ add_8_with_carry (get_8051_sfr s SFR_ACC_A) (bitvector_of_nat eight six) false in
98                let cy_flag ≝ get_index ? flags Z ? in
99                let 〈acc_nu', acc_nl'〉 ≝ split ? four four result in
100                  if (greater_than_b (nat_of_bitvector ? acc_nu') nine) ∨ cy_flag then
101                    let 〈 carry, nu 〉 ≝ half_add ? acc_nu' (bitvector_of_nat four six) in
102                    let new_acc ≝ nu @@ acc_nl' in
103                    let s ≝ set_8051_sfr s SFR_ACC_A new_acc in
104                      set_flags s cy_flag (Just ? (get_ac_flag s)) (get_ov_flag s)
105                  else
106                    s
107              else
108                s
109        | CLR addr ⇒
110          match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → ? with
111            [ ACC_A ⇒ λacc_a: True. set_arg_8 s ACC_A (zero eight)
112            | CARRY ⇒ λcarry: True. set_arg_1 s CARRY false
113            | BIT_ADDR b ⇒ λbit_addr: True. set_arg_1 s (BIT_ADDR b) false
114            | _ ⇒ λother: False. ?
115            ] (subaddressing_modein … addr)
116        | CPL addr ⇒
117          match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → ? with
118            [ ACC_A ⇒ λacc_a: True.
119                let old_acc ≝ get_8051_sfr s SFR_ACC_A in
120                let new_acc ≝ negation_bv ? old_acc in
121                  set_8051_sfr s SFR_ACC_A new_acc
122            | CARRY ⇒ λcarry: True.
123                let old_cy_flag ≝ get_arg_1 s CARRY true in
124                let new_cy_flag ≝ negation old_cy_flag in
125                  set_arg_1 s CARRY new_cy_flag
126            | BIT_ADDR b ⇒ λbit_addr: True.
127                let old_bit ≝ get_arg_1 s (BIT_ADDR b) true in
128                let new_bit ≝ negation old_bit in
129                  set_arg_1 s (BIT_ADDR b) new_bit
130            | _ ⇒ λother: False. ?
131            ] (subaddressing_modein … addr)
132        | SETB b ⇒ set_arg_1 s b false
133        | RL _ ⇒ (* DPM: always ACC_A *)
134            let old_acc ≝ get_8051_sfr s SFR_ACC_A in
135            let new_acc ≝ rotate_left_bv ? one old_acc in
136              set_8051_sfr s SFR_ACC_A new_acc
137        | RR _ ⇒ (* DPM: always ACC_A *)
138            let old_acc ≝ get_8051_sfr s SFR_ACC_A in
139            let new_acc ≝ rotate_right_bv ? one old_acc in
140              set_8051_sfr s SFR_ACC_A new_acc
141        | RLC _ ⇒ (* DPM: always ACC_A *)
142            let old_cy_flag ≝ get_cy_flag s in
143            let old_acc ≝ get_8051_sfr s SFR_ACC_A in
144            let new_cy_flag ≝ get_index_bv ? old_acc Z ? in
145            let new_acc ≝ shift_left_bv eight one old_acc old_cy_flag in
146            let s ≝ set_arg_1 s CARRY new_cy_flag in
147              set_8051_sfr s SFR_ACC_A new_acc
148        | RRC _ ⇒ (* DPM: always ACC_A *)
149            let old_cy_flag ≝ get_cy_flag s in
150            let old_acc ≝ get_8051_sfr s SFR_ACC_A in
151            let new_cy_flag ≝ get_index_bv ? old_acc seven ? in
152            let new_acc ≝ shift_right_bv eight one old_acc old_cy_flag in
153            let s ≝ set_arg_1 s CARRY new_cy_flag in
154              set_8051_sfr s SFR_ACC_A new_acc
155        | SWAP _ ⇒ (* DPM: always ACC_A *)
156            let old_acc ≝ get_8051_sfr s SFR_ACC_A in
157            let 〈nu,nl〉 ≝ split ? four four old_acc in
158            let new_acc ≝ nl @@ nu in
159              set_8051_sfr s SFR_ACC_A new_acc
160        | PUSH addr ⇒
161            match addr return λx. bool_to_Prop (is_in … [[ direct ]] x) → ? with
162              [ DIRECT d ⇒ λdirect: True.
163                let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr s SFR_SP) (bitvector_of_nat eight one) in
164                let s ≝ set_8051_sfr s SFR_SP new_sp in
165                  write_at_stack_pointer s d
166              | _ ⇒ λother: False. ?
167              ] (subaddressing_modein … addr)
168        | POP addr ⇒
169            let contents ≝ read_at_stack_pointer s in
170            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr s SFR_SP) (bitvector_of_nat eight one) false in
171            let s ≝ set_8051_sfr s SFR_SP new_sp in
172              set_arg_8 s addr contents
173        | XCH addr1 addr2 ⇒
174            let old_addr ≝ get_arg_8 s false addr2 in
175            let old_acc ≝ get_8051_sfr s SFR_ACC_A in
176            let s ≝ set_8051_sfr s SFR_ACC_A old_addr in
177              set_arg_8 s addr2 old_acc
178        | NOP ⇒ s
179        | _ ⇒ s
180        ]
181    in
182      s.
Note: See TracBrowser for help on using the repository browser.