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

Last change on this file since 374 was 374, checked in by sacerdot, 9 years ago

1) notation for cast fixed
2) ambiguity reduced: Empty => VEmpty, Cons => VCons
3) DoTest? modified to pretty-print the execution trace.

This should make debugging easier.

File size: 28.5 KB
Line 
1include "Status.ma".
2include "Fetch.ma".
3
4ndefinition sign_extension: Byte → Word ≝
5  λb.
6    zero eight @@ b.
7   
8nlemma inclusive_disjunction_true:
9  ∀b, c: Bool.
10    inclusive_disjunction b c = true → b = true ∨ c = true.
11  #b c;
12  nelim b
13    [ nnormalize; #H; napply or_introl; @;
14  ##| nnormalize; /2/;
15  ##]
16nqed.
17
18nlemma conjunction_true:
19  ∀b, c: Bool.
20    conjunction b c = true → b = true ∧ c = true.
21  #b c;
22  nelim b; nnormalize
23    [ /2/ | #K; ndestruct ]
24nqed.
25
26nlemma eq_true_false: false=true → False.
27 #K; ndestruct.
28nqed.
29
30nlemma eq_a_to_eq: ∀a,b. eq_a a b = true → a=b.
31 #a; #b; ncases a; ncases b; nnormalize; //; #K; ncases (eq_true_false K).
32nqed.
33
34nlemma inclusive_disjunction_b_true: ∀b. inclusive_disjunction b true = true.
35 #b; ncases b; @.
36nqed.
37
38nlemma is_a_to_mem_to_is_in:
39 ∀he,a,m,q. is_a he … a = true → mem … eq_a (S m) q he = true → is_in … q a = true.
40 #he a m q; nelim q
41  [ nnormalize; #_; #K; nassumption
42  | #m' t q' II H1 H2; nnormalize;
43    nchange in H2:(??%?) with (inclusive_disjunction ??);
44    ncases (inclusive_disjunction_true … H2)
45     [ #K; nrewrite < (eq_a_to_eq … K); nrewrite > H1; @
46     | #K; nrewrite > II; ntry nassumption; // ]
47nqed.
48
49nlemma execute_1_technical:
50  ∀n,m: Nat.
51  ∀v: Vector addressing_mode_tag (S n).
52  ∀q: Vector addressing_mode_tag (S m).
53  ∀a: addressing_mode.
54    bool_to_Prop (is_in ? v a) →
55    bool_to_Prop (subvector_with ? ? ? eq_a v q) →
56    bool_to_Prop (is_in ? q a).
57 #n m v q a; nelim v
58  [ nnormalize; #K; ncases K
59  | #n' he tl II;
60    nwhd in ⊢ (% → ? → ?);
61    nlapply (refl … (is_in … (he:::tl) a));
62    ncases (is_in … (he:::tl) a) in ⊢ (???% → %)
63     [ #K; #_; nnormalize in K; nwhd in ⊢ (% → ?);
64       nlapply (refl … (subvector_with … eq_a (he:::tl) q));
65       ncases (subvector_with … eq_a (he:::tl) q) in ⊢ (???% → %)
66       [ #K1; #_;
67        nchange in K1 with ((conjunction ? (subvector_with …)) = true);
68        ncases (conjunction_true … K1); #K3; #K4;
69        ncases (inclusive_disjunction_true … K); #K2
70         [ nrewrite > (is_a_to_mem_to_is_in … K2 K3); @
71         | napply II [ nrewrite > K2; @ | nrewrite > K4; @]##]
72     ##| #K1 K2; nnormalize in K2; ncases K2 ]
73   ##| #K1 K2; nnormalize in K2; ncases K2 ]
74nqed.
75   
76ndefinition execute_1: Status → Status ≝
77  λs.
78    let 〈 instr_pc, ticks 〉 ≝ fetch (code_memory s) (program_counter s) in
79    let 〈 instr, pc 〉 ≝ 〈 first … instr_pc, second … instr_pc 〉 in
80    let s ≝ set_clock s (clock s + ticks) in
81    let s ≝ set_program_counter s pc in
82    let s ≝
83      match instr with
84        [ ADD addr1 addr2 ⇒
85            let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 s false addr1)
86                                                   (get_arg_8 s false addr2) false in
87            let cy_flag ≝ get_index' ? Z  ? flags in
88            let ac_flag ≝ get_index' ? one ? flags in
89            let ov_flag ≝ get_index' ? two ? flags in
90            let s ≝ set_arg_8 s ACC_A result in
91              set_flags s cy_flag (Just Bit ac_flag) ov_flag
92        | ADDC addr1 addr2 ⇒
93            let old_cy_flag ≝ get_cy_flag s in
94            let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 s false addr1)
95                                                   (get_arg_8 s false addr2) old_cy_flag in
96            let cy_flag ≝ get_index' ? Z ? flags in
97            let ac_flag ≝ get_index' ? one ? flags in
98            let ov_flag ≝ get_index' ? two ? flags in
99            let s ≝ set_arg_8 s ACC_A result in
100              set_flags s cy_flag (Just Bit ac_flag) ov_flag
101        | SUBB addr1 addr2 ⇒
102            let old_cy_flag ≝ get_cy_flag s in
103            let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 s false addr1)
104                                                   (get_arg_8 s false addr2) old_cy_flag in
105            let cy_flag ≝ get_index' ? Z ? flags in
106            let ac_flag ≝ get_index' ? one ? flags in
107            let ov_flag ≝ get_index' ? two ? flags in
108            let s ≝ set_arg_8 s ACC_A result in
109              set_flags s cy_flag (Just Bit ac_flag) ov_flag
110        | ANL addr ⇒
111          match addr with
112            [ Left l ⇒
113              match l with
114                [ Left l' ⇒
115                  let 〈addr1, addr2〉 ≝ l' in
116                  let and_val ≝ conjunction_bv ? (get_arg_8 s true addr1) (get_arg_8 s true addr2) in
117                    set_arg_8 s addr1 and_val
118                | Right r ⇒
119                  let 〈addr1, addr2〉 ≝ r in
120                  let and_val ≝ conjunction_bv ? (get_arg_8 s true addr1) (get_arg_8 s true addr2) in
121                    set_arg_8 s addr1 and_val
122                ]
123            | Right r ⇒
124              let 〈addr1, addr2〉 ≝ r in
125              let and_val ≝ conjunction (get_cy_flag s) (get_arg_1 s addr2 true) in
126                set_flags s and_val (Nothing ?) (get_ov_flag s)
127            ]
128        | ORL addr ⇒
129          match addr with
130            [ Left l ⇒
131              match l with
132                [ Left l' ⇒
133                  let 〈addr1, addr2〉 ≝ l' in
134                  let or_val ≝ inclusive_disjunction_bv ? (get_arg_8 s true addr1) (get_arg_8 s true addr2) in
135                    set_arg_8 s addr1 or_val
136                | Right r ⇒
137                  let 〈addr1, addr2〉 ≝ r in
138                  let or_val ≝ inclusive_disjunction_bv ? (get_arg_8 s true addr1) (get_arg_8 s true addr2) in
139                    set_arg_8 s addr1 or_val
140                ]
141            | Right r ⇒
142              let 〈addr1, addr2〉 ≝ r in
143              let or_val ≝ inclusive_disjunction (get_cy_flag s) (get_arg_1 s addr2 true) in
144                set_flags s or_val (Nothing ?) (get_ov_flag s)
145            ]
146        | XRL addr ⇒
147          match addr with
148            [ Left l' ⇒
149              let 〈addr1, addr2〉 ≝ l' in
150              let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 s true addr1) (get_arg_8 s true addr2) in
151                set_arg_8 s addr1 xor_val
152            | Right r ⇒
153              let 〈addr1, addr2〉 ≝ r in
154              let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 s true addr1) (get_arg_8 s true addr2) in
155                set_arg_8 s addr1 xor_val
156            ]
157        | INC addr ⇒
158            match addr return λx. bool_to_Prop (is_in … [[ acc_a;
159                                                           register;
160                                                           direct;
161                                                           indirect;
162                                                           dptr ]] x) → ? with
163              [ ACC_A ⇒ λacc_a: True.
164                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 s true ACC_A) (bitvector_of_nat eight one) in
165                  set_arg_8 s ACC_A result
166              | REGISTER r ⇒ λregister: True.
167                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 s true (REGISTER r)) (bitvector_of_nat eight one) in
168                  set_arg_8 s (REGISTER r) result
169              | DIRECT d ⇒ λdirect: True.
170                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 s true (DIRECT d)) (bitvector_of_nat eight one) in
171                  set_arg_8 s (DIRECT d) result
172              | INDIRECT i ⇒ λindirect: True.
173                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 s true (INDIRECT i)) (bitvector_of_nat eight one) in
174                  set_arg_8 s (INDIRECT i) result
175              | DPTR ⇒ λdptr: True.
176                let 〈 carry, bl 〉 ≝ half_add ? (get_8051_sfr s SFR_DPL) (bitvector_of_nat eight one) in
177                let 〈 carry, bu 〉 ≝ full_add ? (get_8051_sfr s SFR_DPH) (zero eight) carry in
178                let s ≝ set_8051_sfr s SFR_DPL bl in
179                  set_8051_sfr s SFR_DPH bu
180              | _ ⇒ λother: False. ⊥
181              ] (subaddressing_modein … addr)
182       | DEC addr ⇒
183           let 〈 result, flags 〉 ≝ sub_8_with_carry (get_arg_8 s true addr) (bitvector_of_nat eight one) false in
184             set_arg_8 s addr result
185        | MUL addr1 addr2 ⇒
186           let acc_a_nat ≝ nat_of_bitvector eight (get_8051_sfr s SFR_ACC_A) in
187           let acc_b_nat ≝ nat_of_bitvector eight (get_8051_sfr s SFR_ACC_B) in
188           let product ≝ acc_a_nat * acc_b_nat in
189           let ov_flag ≝ product ≥ two_hundred_and_fifty_six in
190           let low ≝ bitvector_of_nat eight (product mod two_hundred_and_fifty_six) in
191           let high ≝ bitvector_of_nat eight (product ÷ two_hundred_and_fifty_six) in
192           let s ≝ set_8051_sfr s SFR_ACC_A low in
193             set_8051_sfr s SFR_ACC_B high
194        | DIV addr1 addr2 ⇒
195           let acc_a_nat ≝ nat_of_bitvector eight (get_8051_sfr s SFR_ACC_A) in
196           let acc_b_nat ≝ nat_of_bitvector eight (get_8051_sfr s SFR_ACC_B) in
197             match acc_b_nat with
198               [ Z ⇒ set_flags s false (Nothing Bit) true
199               | S o ⇒
200                 let q ≝ bitvector_of_nat eight (acc_a_nat ÷ (S o)) in
201                 let r ≝ bitvector_of_nat eight (acc_a_nat mod two_hundred_and_fifty_six) in
202                 let s ≝ set_8051_sfr s SFR_ACC_A q in
203                 let s ≝ set_8051_sfr s SFR_ACC_B r in
204                   set_flags s false (Nothing Bit) false
205               ]
206        | DA addr ⇒
207            let 〈 acc_nu, acc_nl 〉 ≝ split ? four four (get_8051_sfr s SFR_ACC_A) in
208              if inclusive_disjunction (greater_than_b (nat_of_bitvector ? acc_nl) nine) (get_ac_flag s) then
209                let 〈result, flags〉 ≝ add_8_with_carry (get_8051_sfr s SFR_ACC_A) (bitvector_of_nat eight six) false in
210                let cy_flag ≝ get_index' ? Z ? flags in
211                let 〈acc_nu', acc_nl'〉 ≝ split ? four four result in
212                  if (greater_than_b (nat_of_bitvector ? acc_nu') nine) ∨ cy_flag then
213                    let 〈 carry, nu 〉 ≝ half_add ? acc_nu' (bitvector_of_nat four six) in
214                    let new_acc ≝ nu @@ acc_nl' in
215                    let s ≝ set_8051_sfr s SFR_ACC_A new_acc in
216                      set_flags s cy_flag (Just ? (get_ac_flag s)) (get_ov_flag s)
217                  else
218                    s
219              else
220                s
221        | CLR addr ⇒
222          match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → ? with
223            [ ACC_A ⇒ λacc_a: True. set_arg_8 s ACC_A (zero eight)
224            | CARRY ⇒ λcarry: True. set_arg_1 s CARRY false
225            | BIT_ADDR b ⇒ λbit_addr: True. set_arg_1 s (BIT_ADDR b) false
226            | _ ⇒ λother: False. ⊥
227            ] (subaddressing_modein … addr)
228        | CPL addr ⇒
229          match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → ? with
230            [ ACC_A ⇒ λacc_a: True.
231                let old_acc ≝ get_8051_sfr s SFR_ACC_A in
232                let new_acc ≝ negation_bv ? old_acc in
233                  set_8051_sfr s SFR_ACC_A new_acc
234            | CARRY ⇒ λcarry: True.
235                let old_cy_flag ≝ get_arg_1 s CARRY true in
236                let new_cy_flag ≝ negation old_cy_flag in
237                  set_arg_1 s CARRY new_cy_flag
238            | BIT_ADDR b ⇒ λbit_addr: True.
239                let old_bit ≝ get_arg_1 s (BIT_ADDR b) true in
240                let new_bit ≝ negation old_bit in
241                  set_arg_1 s (BIT_ADDR b) new_bit
242            | _ ⇒ λother: False. ?
243            ] (subaddressing_modein … addr)
244        | SETB b ⇒ set_arg_1 s b false
245        | RL _ ⇒ (* DPM: always ACC_A *)
246            let old_acc ≝ get_8051_sfr s SFR_ACC_A in
247            let new_acc ≝ rotate_left … one old_acc in
248              set_8051_sfr s SFR_ACC_A new_acc
249        | RR _ ⇒ (* DPM: always ACC_A *)
250            let old_acc ≝ get_8051_sfr s SFR_ACC_A in
251            let new_acc ≝ rotate_right … one old_acc in
252              set_8051_sfr s SFR_ACC_A new_acc
253        | RLC _ ⇒ (* DPM: always ACC_A *)
254            let old_cy_flag ≝ get_cy_flag s in
255            let old_acc ≝ get_8051_sfr s SFR_ACC_A in
256            let new_cy_flag ≝ get_index' ? Z ? old_acc in
257            let new_acc ≝ shift_left … one old_acc old_cy_flag in
258            let s ≝ set_arg_1 s CARRY new_cy_flag in
259              set_8051_sfr s SFR_ACC_A new_acc
260        | RRC _ ⇒ (* DPM: always ACC_A *)
261            let old_cy_flag ≝ get_cy_flag s in
262            let old_acc ≝ get_8051_sfr s SFR_ACC_A in
263            let new_cy_flag ≝ get_index' ? seven ? old_acc in
264            let new_acc ≝ shift_right … one old_acc old_cy_flag in
265            let s ≝ set_arg_1 s CARRY new_cy_flag in
266              set_8051_sfr s SFR_ACC_A new_acc
267        | SWAP _ ⇒ (* DPM: always ACC_A *)
268            let old_acc ≝ get_8051_sfr s SFR_ACC_A in
269            let 〈nu,nl〉 ≝ split ? four four old_acc in
270            let new_acc ≝ nl @@ nu in
271              set_8051_sfr s SFR_ACC_A new_acc
272        | PUSH addr ⇒
273            match addr return λx. bool_to_Prop (is_in … [[ direct ]] x) → ? with
274              [ DIRECT d ⇒ λdirect: True.
275                let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr s SFR_SP) (bitvector_of_nat eight one) in
276                let s ≝ set_8051_sfr s SFR_SP new_sp in
277                  write_at_stack_pointer s d
278              | _ ⇒ λother: False. ⊥
279              ] (subaddressing_modein … addr)
280        | POP addr ⇒
281            let contents ≝ read_at_stack_pointer s in
282            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr s SFR_SP) (bitvector_of_nat eight one) false in
283            let s ≝ set_8051_sfr s SFR_SP new_sp in
284              set_arg_8 s addr contents
285        | XCH addr1 addr2 ⇒
286            let old_addr ≝ get_arg_8 s false addr2 in
287            let old_acc ≝ get_8051_sfr s SFR_ACC_A in
288            let s ≝ set_8051_sfr s SFR_ACC_A old_addr in
289              set_arg_8 s addr2 old_acc
290        | XCHD addr1 addr2 ⇒
291            let 〈acc_nu, acc_nl〉 ≝ split … four four (get_8051_sfr s SFR_ACC_A) in
292            let 〈arg_nu, arg_nl〉 ≝ split … four four (get_arg_8 s false addr2) in
293            let new_acc ≝ acc_nu @@ arg_nl in
294            let new_arg ≝ arg_nu @@ acc_nl in
295            let s ≝ set_8051_sfr s SFR_ACC_A new_acc in
296              set_arg_8 s addr2 new_arg
297        | RET ⇒
298            let high_bits ≝ read_at_stack_pointer s in
299            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr s SFR_SP) (bitvector_of_nat eight one) false in
300            let s ≝ set_8051_sfr s SFR_SP new_sp in
301            let low_bits ≝ read_at_stack_pointer s in
302            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr s SFR_SP) (bitvector_of_nat eight one) false in
303            let s ≝ set_8051_sfr s SFR_SP new_sp in
304            let new_pc ≝ high_bits @@ low_bits in
305              set_program_counter s new_pc
306        | RETI ⇒
307            let high_bits ≝ read_at_stack_pointer s in
308            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr s SFR_SP) (bitvector_of_nat eight one) false in
309            let s ≝ set_8051_sfr s SFR_SP new_sp in
310            let low_bits ≝ read_at_stack_pointer s in
311            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr s SFR_SP) (bitvector_of_nat eight one) false in
312            let s ≝ set_8051_sfr s SFR_SP new_sp in
313            let new_pc ≝ high_bits @@ low_bits in
314              set_program_counter s new_pc
315        | Jump j ⇒
316          match j with
317            [ JC addr ⇒
318              match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
319                [ RELATIVE r ⇒ λrel: True.
320                  if get_cy_flag s then
321                    let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in
322                      set_program_counter s new_pc
323                  else
324                    s
325                | _ ⇒ λother: False. ⊥
326                ] (subaddressing_modein … addr)
327            | JNC addr ⇒
328              match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
329                [ RELATIVE r ⇒ λrel: True.
330                  if negation (get_cy_flag s) then
331                    let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in
332                      set_program_counter s new_pc
333                  else
334                    s
335                | _ ⇒ λother: False. ⊥
336                ] (subaddressing_modein … addr)
337            | JB addr1 addr2 ⇒
338              match addr2 return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
339                [ RELATIVE r ⇒ λrel: True.
340                  if get_arg_1 s addr1 false then
341                    let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in
342                      set_program_counter s new_pc
343                  else
344                    s
345                | _ ⇒ λother: False. ⊥
346                ] (subaddressing_modein … addr2)
347            | JNB addr1 addr2 ⇒
348              match addr2 return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
349                [ RELATIVE r ⇒ λrel: True.
350                  if negation (get_arg_1 s addr1 false) then
351                    let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in
352                      set_program_counter s new_pc
353                  else
354                    s
355                | _ ⇒ λother: False. ⊥
356                ] (subaddressing_modein … addr2)
357            | JBC addr1 addr2 ⇒
358              match addr2 return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
359                [ RELATIVE r ⇒ λrel: True.
360                  let s ≝ set_arg_1 s addr1 false in
361                    if get_arg_1 s addr1 false then
362                      let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in
363                        set_program_counter s new_pc
364                    else
365                      s
366                | _ ⇒ λother: False. ⊥
367                ] (subaddressing_modein … addr2)
368            | JZ addr ⇒
369              match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
370                [ RELATIVE r ⇒ λrel: True.
371                    if eq_bv ? (get_8051_sfr s SFR_ACC_A) (zero eight) then
372                      let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in
373                        set_program_counter s new_pc
374                    else
375                      s
376                | _ ⇒ λother: False. ⊥
377                ] (subaddressing_modein … addr)
378            | JNZ addr ⇒
379              match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
380                [ RELATIVE r ⇒ λrel: True.
381                    if negation (eq_bv ? (get_8051_sfr s SFR_ACC_A) (zero eight)) then
382                      let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in
383                        set_program_counter s new_pc
384                    else
385                      s
386                | _ ⇒ λother: False. ⊥
387                ] (subaddressing_modein … addr)
388            | CJNE addr1 addr2 ⇒
389              match addr2 return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
390                [ RELATIVE r ⇒ λrelative: True.
391                  match addr1 with
392                    [ Left l ⇒
393                        let 〈addr1, addr2〉 ≝ l in
394                        let new_cy ≝ less_than_b (nat_of_bitvector ? (get_arg_8 s false addr1))
395                                                 (nat_of_bitvector ? (get_arg_8 s false addr2)) in
396                          if negation (eq_bv ? (get_arg_8 s false addr1) (get_arg_8 s false addr2)) then
397                            let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in
398                            let s ≝ set_program_counter s new_pc in
399                              set_flags s new_cy (Nothing ?) (get_ov_flag s)
400                          else
401                            (set_flags s new_cy (Nothing ?) (get_ov_flag s))
402                    | Right r' ⇒
403                        let 〈addr1, addr2〉 ≝ r' in
404                        let new_cy ≝ less_than_b (nat_of_bitvector ? (get_arg_8 s false addr1))
405                                                 (nat_of_bitvector ? (get_arg_8 s false addr2)) in
406                          if negation (eq_bv ? (get_arg_8 s false addr1) (get_arg_8 s false addr2)) then
407                            let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in
408                            let s ≝ set_program_counter s new_pc in
409                              set_flags s new_cy (Nothing ?) (get_ov_flag s)
410                          else
411                            (set_flags s new_cy (Nothing ?) (get_ov_flag s))
412                    ]
413                | _ ⇒ λother: False. ⊥
414                ] (subaddressing_modein … addr2)
415            | DJNZ addr1 addr2 ⇒
416              match addr2 return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
417                [ RELATIVE r ⇒ λrel: True.
418                    let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 s true addr1) (bitvector_of_nat eight one) false in
419                    let s ≝ set_arg_8 s addr1 result in
420                      if negation (eq_bv ? result (zero eight)) then
421                        let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in
422                          set_program_counter s new_pc
423                      else
424                        s
425                | _ ⇒ λother: False. ⊥
426                ] (subaddressing_modein … addr2)
427            ]
428        | JMP _ ⇒ (* DPM: always indirect_dptr *)
429          let dptr ≝ (get_8051_sfr s SFR_DPH) @@ (get_8051_sfr s SFR_DPL) in
430          let big_acc ≝ (zero eight) @@ (get_8051_sfr s SFR_ACC_A) in
431          let 〈carry, jmp_addr〉 ≝ half_add ? big_acc dptr in
432          let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) jmp_addr in
433            set_program_counter s new_pc
434        | LJMP addr ⇒
435          match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → ? with
436            [ ADDR16 a ⇒ λaddr16: True.
437                set_program_counter s a
438            | _ ⇒ λother: False. ⊥
439            ] (subaddressing_modein … addr)
440        | SJMP addr ⇒
441          match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
442            [ RELATIVE r ⇒ λrelative: True.
443                let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in
444                  set_program_counter s new_pc
445            | _ ⇒ λother: False. ⊥
446            ] (subaddressing_modein … addr)
447        | AJMP addr ⇒
448          match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → ? with
449            [ ADDR11 a ⇒ λaddr11: True.
450              let 〈pc_bu, pc_bl〉 ≝ split ? eight eight (program_counter s) in
451              let 〈nu, nl〉 ≝ split ? four four pc_bu in
452              let bit ≝ get_index' ? Z ? nl in
453              let 〈relevant1, relevant2〉 ≝ split ? three eight a in
454              let new_addr ≝ (nu @@ (bit ::: relevant1)) @@ relevant2 in
455              let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) new_addr in
456                set_program_counter s new_pc
457            | _ ⇒ λother: False. ⊥
458            ] (subaddressing_modein … addr)
459        | MOVC addr1 addr2 ⇒
460          match addr2 return λx. bool_to_Prop (is_in … [[ acc_dptr; acc_pc ]] x) → ? with
461            [ ACC_DPTR ⇒ λacc_dptr: True.
462              let big_acc ≝ (zero eight) @@ (get_8051_sfr s SFR_ACC_A) in
463              let dptr ≝ (get_8051_sfr s SFR_DPH) @@ (get_8051_sfr s SFR_DPL) in
464              let 〈carry, new_addr〉 ≝ half_add ? dptr big_acc in
465              let result ≝ lookup ? ? new_addr (code_memory s) (zero ?) in
466                set_8051_sfr s SFR_ACC_A result
467            | ACC_PC ⇒ λacc_pc: True.
468              let big_acc ≝ (zero eight) @@ (get_8051_sfr s SFR_ACC_A) in
469              let 〈carry,inc_pc〉 ≝ half_add ? (program_counter s) (bitvector_of_nat sixteen one) in
470              (* DPM: Under specified: does the carry from PC incrementation affect the *)
471              (*      addition of the PC with the DPTR? At the moment, no.              *)
472              let s ≝ set_program_counter s inc_pc in
473              let 〈carry, new_addr〉 ≝ half_add ? inc_pc big_acc in
474              let result ≝ lookup ? ? new_addr (code_memory s) (zero ?) in
475                set_8051_sfr s SFR_ACC_A result
476            | _ ⇒ λother: False. ⊥
477            ] (subaddressing_modein … addr2)
478        | MOVX addr ⇒
479          (* DPM: only copies --- doesn't affect I/O *)
480          match addr with
481            [ Left l ⇒
482              let 〈addr1, addr2〉 ≝ l in
483                set_arg_8 s addr1 (get_arg_8 s false addr2)
484            | Right r ⇒
485              let 〈addr1, addr2〉 ≝ r in
486                set_arg_8 s addr1 (get_arg_8 s false addr2)
487            ]
488        | MOV addr ⇒
489          match addr with
490            [ Left l ⇒
491              match l with
492                [ Left l' ⇒
493                  match l' with
494                    [ Left l'' ⇒
495                      match l'' with
496                        [ Left l''' ⇒
497                          match l''' with
498                            [ Left l'''' ⇒
499                              let 〈addr1, addr2〉 ≝ l'''' in
500                                set_arg_8 s addr1 (get_arg_8 s false addr2)
501                            | Right r'''' ⇒
502                              let 〈addr1, addr2〉 ≝ r'''' in
503                                set_arg_8 s addr1 (get_arg_8 s false addr2)
504                            ]
505                        | Right r''' ⇒
506                          let 〈addr1, addr2〉 ≝ r''' in
507                            set_arg_8 s addr1 (get_arg_8 s false addr2)
508                        ]
509                    | Right r'' ⇒
510                      let 〈addr1, addr2〉 ≝ r'' in
511                        set_arg_16 s (get_arg_16 s addr2) addr1
512                    ]
513                | Right r ⇒
514                  let 〈addr1, addr2〉 ≝ r in
515                    set_arg_1 s addr1 (get_arg_1 s addr2 false)
516                ]
517            | Right r ⇒
518              let 〈addr1, addr2〉 ≝ r in
519                set_arg_1 s addr1 (get_arg_1 s addr2 false)
520            ]
521        | LCALL addr ⇒
522          match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → ? with
523            [ ADDR16 a ⇒ λaddr16: True.
524              let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr s SFR_SP) (bitvector_of_nat eight one) in
525              let s ≝ set_8051_sfr s SFR_SP new_sp in
526              let 〈pc_bu, pc_bl〉 ≝ split ? eight eight (program_counter s) in
527              let s ≝ write_at_stack_pointer s pc_bl in
528              let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr s SFR_SP) (bitvector_of_nat eight one) in
529              let s ≝ set_8051_sfr s SFR_SP new_sp in
530              let s ≝ write_at_stack_pointer s pc_bu in
531                set_program_counter s a
532            | _ ⇒ λother: False. ⊥
533            ] (subaddressing_modein … addr)
534        | ACALL addr ⇒
535          match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → ? with
536            [ ADDR11 a ⇒ λaddr11: True.
537              let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr s SFR_SP) (bitvector_of_nat eight one) in
538              let s ≝ set_8051_sfr s SFR_SP new_sp in
539              let 〈pc_bu, pc_bl〉 ≝ split ? eight eight (program_counter s) in
540              let s ≝ write_at_stack_pointer s pc_bl in
541              let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr s SFR_SP) (bitvector_of_nat eight one) in
542              let s ≝ set_8051_sfr s SFR_SP new_sp in
543              let s ≝ write_at_stack_pointer s pc_bu in
544              let 〈thr, eig〉 ≝ split ? three eight a in
545              let 〈fiv, thr'〉 ≝ split ? five three pc_bu in
546              let new_addr ≝ (fiv @@ thr) @@ pc_bl in
547                set_program_counter s new_addr
548            | _ ⇒ λother: False. ⊥
549            ] (subaddressing_modein … addr)
550        | NOP ⇒ s
551        ]
552    in
553      s.
554    ntry nassumption;
555    ntry (
556      nnormalize
557      nrepeat (napply (less_than_or_equal_monotone))
558      napply (less_than_or_equal_zero)
559    );
560    ntry (
561      napply (execute_1_technical … (subaddressing_modein …))
562      napply I
563    );
564    ntry (
565      nnormalize
566      napply I
567    );     
568nqed.
569
570nlet rec execute (n: Nat) (s: Status) on n: Status ≝
571  match n with
572    [ Z ⇒ s
573    | S o ⇒ execute o (execute_1 s)
574    ].
Note: See TracBrowser for help on using the repository browser.