source: src/ASM/Interpret.ma @ 1515

Last change on this file since 1515 was 1515, checked in by campbell, 10 years ago

Add type of maps on positive binary numbers, and use them for identifers.

Also:

  • fix interpretation for - on positives
  • move eq_nat_dec to a more appropriate place
  • split out costs from other identifiers in ASM
  • use identifier abstractions in back-end
File size: 30.8 KB
RevLine 
[698]1include "ASM/Status.ma".
2include "ASM/Fetch.ma".
[475]3
4definition sign_extension: Byte → Word ≝
5  λc.
6    let b ≝ get_index_v ? 8 c 1 ? in
7      [[ b; b; b; b; b; b; b; b ]] @@ c.
8  normalize;
9  repeat (@ (le_S_S ?));
10  @ (le_O_n);
11qed.
12   
13lemma eq_a_to_eq: ∀a,b. eq_a a b = true → a=b.
14 # a
15 # b
16 cases a
17 cases b
18 normalize
19 //
20 # K
21 cases (eq_true_false K)
22qed.
23
24lemma is_a_to_mem_to_is_in:
25 ∀he,a,m,q. is_a he … a = true → mem … eq_a (S m) q he = true → is_in … q a = true.
26 # he
27 # a
28 # m
29 # q
30 elim q
31 [ normalize
32   # _
33   # K
34   assumption
35 | # m'
36   # t
37   # q'
38   # II
39   # H1
40   # H2
41   normalize
42   change in H2: (??%?) with (orb ??)
43   cases (inclusive_disjunction_true … H2)
44   [ # K
45     < (eq_a_to_eq … K)
46     > H1
47     %
48   | # K
49     > II
50     try assumption
51     cases (is_a t a)
52     normalize
53     %
54   ]
55 ]
56qed.
57
58lemma execute_1_technical:
59  ∀n, m: nat.
60  ∀v: Vector addressing_mode_tag (S n).
61  ∀q: Vector addressing_mode_tag (S m).
62  ∀a: addressing_mode.
63    bool_to_Prop (is_in ? v a) →
64    bool_to_Prop (subvector_with ? ? ? eq_a v q) →
65    bool_to_Prop (is_in ? q a).
66 # n
67 # m
68 # v
69 # q
70 # a
71 elim v
72 [ normalize
73   # K
74   cases K
75 | # n'
76   # he
77   # tl
78   # II
79   whd in ⊢ (% → ? → ?)
80   lapply (refl … (is_in … (he:::tl) a))
81   cases (is_in … (he:::tl) a) in ⊢ (???% → %)
82   [ # K
83     # _
84     normalize in K;
85     whd in ⊢ (% → ?)
86     lapply (refl … (subvector_with … eq_a (he:::tl) q))
87     cases (subvector_with … eq_a (he:::tl) q) in ⊢ (???% → %)
88     [ # K1
89       # _
90       change in K1 with ((andb ? (subvector_with …)) = true)
91       cases (conjunction_true … K1)
92       # K3
93       # K4
94       cases (inclusive_disjunction_true … K)
95       # K2
96       [ > (is_a_to_mem_to_is_in … K2 K3)
97         %
98       | @ II
99         [ > K2
100           %
101         | > K4
102           %
103         ]
104       ]
105     | # K1
106       # K2
107       (normalize in K2)
108       cases K2;
109     ]
110   | # K1
111     # K2
112     normalize in K2;
113     cases K2
114   ]
115 ]
116qed.
[712]117
118include alias "arithmetics/nat.ma".
[757]119include alias "ASM/BitVectorTrie.ma".
[712]120
[936]121definition execute_1_preinstruction:
122 ∀ticks: nat × nat.
123 ∀A, M: Type[0]. (A → PreStatus M → Word) → preinstruction A → PreStatus M → PreStatus M ≝
124  λticks.
[821]125  λA, M: Type[0].
[822]126  λaddr_of: A → (PreStatus M) → Word.
[820]127  λinstr: preinstruction A.
[821]128  λs: PreStatus M.
[936]129  let add_ticks1 ≝ λs: PreStatus M.set_clock … s (\fst ticks + clock … s) in
130  let add_ticks2 ≝ λs: PreStatus M.set_clock … s (\snd ticks + clock … s) in
[820]131  match instr with
[475]132        [ ADD addr1 addr2 ⇒
[936]133            let s ≝ add_ticks1 s in
[821]134            let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 ? s false addr1)
135                                                   (get_arg_8 ? s false addr2) false in
[475]136            let cy_flag ≝ get_index' ? O  ? flags in
137            let ac_flag ≝ get_index' ? 1 ? flags in
138            let ov_flag ≝ get_index' ? 2 ? flags in
[821]139            let s ≝ set_arg_8 ? s ACC_A result in
140              set_flags ? s cy_flag (Some Bit ac_flag) ov_flag
[475]141        | ADDC addr1 addr2 ⇒
[936]142            let s ≝ add_ticks1 s in
[821]143            let old_cy_flag ≝ get_cy_flag ? s in
144            let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 ? s false addr1)
145                                                   (get_arg_8 ? s false addr2) old_cy_flag in
[475]146            let cy_flag ≝ get_index' ? O ? flags in
147            let ac_flag ≝ get_index' ? 1 ? flags in
148            let ov_flag ≝ get_index' ? 2 ? flags in
[821]149            let s ≝ set_arg_8 ? s ACC_A result in
150              set_flags ? s cy_flag (Some Bit ac_flag) ov_flag
[475]151        | SUBB addr1 addr2 ⇒
[936]152            let s ≝ add_ticks1 s in
[821]153            let old_cy_flag ≝ get_cy_flag ? s in
154            let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 ? s false addr1)
155                                                   (get_arg_8 ? s false addr2) old_cy_flag in
[475]156            let cy_flag ≝ get_index' ? O ? flags in
157            let ac_flag ≝ get_index' ? 1 ? flags in
158            let ov_flag ≝ get_index' ? 2 ? flags in
[821]159            let s ≝ set_arg_8 ? s ACC_A result in
160              set_flags ? s cy_flag (Some Bit ac_flag) ov_flag
[475]161        | ANL addr ⇒
[936]162          let s ≝ add_ticks1 s in
[475]163          match addr with
164            [ inl l ⇒
165              match l with
166                [ inl l' ⇒
167                  let 〈addr1, addr2〉 ≝ l' in
[821]168                  let and_val ≝ conjunction_bv ? (get_arg_8 ? s true addr1) (get_arg_8 ? s true addr2) in
169                    set_arg_8 ? s addr1 and_val
[475]170                | inr r ⇒
171                  let 〈addr1, addr2〉 ≝ r in
[821]172                  let and_val ≝ conjunction_bv ? (get_arg_8 ? s true addr1) (get_arg_8 ? s true addr2) in
173                    set_arg_8 ? s addr1 and_val
[475]174                ]
175            | inr r ⇒
176              let 〈addr1, addr2〉 ≝ r in
[822]177              let and_val ≝ andb (get_cy_flag ? s) (get_arg_1 ? s addr2 true) in
[821]178                set_flags ? s and_val (None ?) (get_ov_flag ? s)
[475]179            ]
180        | ORL addr ⇒
[936]181          let s ≝ add_ticks1 s in
[475]182          match addr with
183            [ inl l ⇒
184              match l with
185                [ inl l' ⇒
186                  let 〈addr1, addr2〉 ≝ l' in
[821]187                  let or_val ≝ inclusive_disjunction_bv ? (get_arg_8 ? s true addr1) (get_arg_8 ? s true addr2) in
188                    set_arg_8 ? s addr1 or_val
[475]189                | inr r ⇒
190                  let 〈addr1, addr2〉 ≝ r in
[821]191                  let or_val ≝ inclusive_disjunction_bv ? (get_arg_8 ? s true addr1) (get_arg_8 ? s true addr2) in
192                    set_arg_8 ? s addr1 or_val
[475]193                ]
194            | inr r ⇒
195              let 〈addr1, addr2〉 ≝ r in
[821]196              let or_val ≝ (get_cy_flag ? s) ∨ (get_arg_1 ? s addr2 true) in
197                set_flags ? s or_val (None ?) (get_ov_flag ? s)
[475]198            ]
199        | XRL addr ⇒
[936]200          let s ≝ add_ticks1 s in
[475]201          match addr with
202            [ inl l' ⇒
203              let 〈addr1, addr2〉 ≝ l' in
[821]204              let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 ? s true addr1) (get_arg_8 ? s true addr2) in
205                set_arg_8 ? s addr1 xor_val
[475]206            | inr r ⇒
207              let 〈addr1, addr2〉 ≝ r in
[821]208              let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 ? s true addr1) (get_arg_8 ? s true addr2) in
209                set_arg_8 ? s addr1 xor_val
[475]210            ]
211        | INC addr ⇒
[936]212            let s ≝ add_ticks1 s in
[475]213            match addr return λx. bool_to_Prop (is_in … [[ acc_a;
[757]214                                                           registr;
[475]215                                                           direct;
216                                                           indirect;
217                                                           dptr ]] x) → ? with
218              [ ACC_A ⇒ λacc_a: True.
[821]219                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 ? s true ACC_A) (bitvector_of_nat 8 1) in
220                  set_arg_8 ? s ACC_A result
[475]221              | REGISTER r ⇒ λregister: True.
[821]222                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 ? s true (REGISTER r)) (bitvector_of_nat 8 1) in
223                  set_arg_8 ? s (REGISTER r) result
[475]224              | DIRECT d ⇒ λdirect: True.
[821]225                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 ? s true (DIRECT d)) (bitvector_of_nat 8 1) in
226                  set_arg_8 ? s (DIRECT d) result
[475]227              | INDIRECT i ⇒ λindirect: True.
[821]228                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 ? s true (INDIRECT i)) (bitvector_of_nat 8 1) in
229                  set_arg_8 ? s (INDIRECT i) result
[475]230              | DPTR ⇒ λdptr: True.
[821]231                let 〈 carry, bl 〉 ≝ half_add ? (get_8051_sfr ? s SFR_DPL) (bitvector_of_nat 8 1) in
232                let 〈 carry, bu 〉 ≝ full_add ? (get_8051_sfr ? s SFR_DPH) (zero 8) carry in
233                let s ≝ set_8051_sfr ? s SFR_DPL bl in
234                  set_8051_sfr ? s SFR_DPH bu
[475]235              | _ ⇒ λother: False. ⊥
236              ] (subaddressing_modein … addr)
237        | DEC addr ⇒
[936]238           let s ≝ add_ticks1 s in
[821]239           let 〈 result, flags 〉 ≝ sub_8_with_carry (get_arg_8 ? s true addr) (bitvector_of_nat 8 1) false in
240             set_arg_8 ? s addr result
[475]241        | MUL addr1 addr2 ⇒
[936]242           let s ≝ add_ticks1 s in
[821]243           let acc_a_nat ≝ nat_of_bitvector 8 (get_8051_sfr ? s SFR_ACC_A) in
244           let acc_b_nat ≝ nat_of_bitvector 8 (get_8051_sfr ? s SFR_ACC_B) in
[475]245           let product ≝ acc_a_nat * acc_b_nat in
246           let ov_flag ≝ product ≥ 256 in
247           let low ≝ bitvector_of_nat 8 (product mod 256) in
248           let high ≝ bitvector_of_nat 8 (product ÷ 256) in
[821]249           let s ≝ set_8051_sfr ? s SFR_ACC_A low in
250             set_8051_sfr ? s SFR_ACC_B high
[475]251        | DIV addr1 addr2 ⇒
[936]252           let s ≝ add_ticks1 s in
[821]253           let acc_a_nat ≝ nat_of_bitvector 8 (get_8051_sfr ? s SFR_ACC_A) in
254           let acc_b_nat ≝ nat_of_bitvector 8 (get_8051_sfr ? s SFR_ACC_B) in
[475]255             match acc_b_nat with
[821]256               [ O ⇒ set_flags ? s false (None Bit) true
[475]257               | S o ⇒
258                 let q ≝ bitvector_of_nat 8 (acc_a_nat ÷ (S o)) in
259                 let r ≝ bitvector_of_nat 8 (acc_a_nat mod 256) in
[821]260                 let s ≝ set_8051_sfr ? s SFR_ACC_A q in
261                 let s ≝ set_8051_sfr ? s SFR_ACC_B r in
262                   set_flags ? s false (None Bit) false
[475]263               ]
264        | DA addr ⇒
[936]265            let s ≝ add_ticks1 s in
[821]266            let 〈 acc_nu, acc_nl 〉 ≝ split ? 4 4 (get_8051_sfr ? s SFR_ACC_A) in
267              if (gtb (nat_of_bitvector ? acc_nl) 9) ∨ (get_ac_flag ? s) then
268                let 〈result, flags〉 ≝ add_8_with_carry (get_8051_sfr ? s SFR_ACC_A) (bitvector_of_nat 8 6) false in
[475]269                let cy_flag ≝ get_index' ? O ? flags in
270                let 〈acc_nu', acc_nl'〉 ≝ split ? 4 4 result in
271                  if (gtb (nat_of_bitvector ? acc_nu') 9) ∨ cy_flag then
272                    let 〈 carry, nu 〉 ≝ half_add ? acc_nu' (bitvector_of_nat 4 6) in
273                    let new_acc ≝ nu @@ acc_nl' in
[821]274                    let s ≝ set_8051_sfr ? s SFR_ACC_A new_acc in
275                      set_flags ? s cy_flag (Some ? (get_ac_flag ? s)) (get_ov_flag ? s)
[475]276                  else
277                    s
278              else
279                s
280        | CLR addr ⇒
[936]281          let s ≝ add_ticks1 s in
[475]282          match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → ? with
[821]283            [ ACC_A ⇒ λacc_a: True. set_arg_8 ? s ACC_A (zero 8)
284            | CARRY ⇒ λcarry: True. set_arg_1 ? s CARRY false
285            | BIT_ADDR b ⇒ λbit_addr: True. set_arg_1 ? s (BIT_ADDR b) false
[475]286            | _ ⇒ λother: False. ⊥
287            ] (subaddressing_modein … addr)
288        | CPL addr ⇒
[936]289          let s ≝ add_ticks1 s in
[475]290          match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → ? with
291            [ ACC_A ⇒ λacc_a: True.
[821]292                let old_acc ≝ get_8051_sfr ? s SFR_ACC_A in
[475]293                let new_acc ≝ negation_bv ? old_acc in
[821]294                  set_8051_sfr ? s SFR_ACC_A new_acc
[475]295            | CARRY ⇒ λcarry: True.
[821]296                let old_cy_flag ≝ get_arg_1 ? s CARRY true in
[475]297                let new_cy_flag ≝ ¬old_cy_flag in
[821]298                  set_arg_1 ? s CARRY new_cy_flag
[475]299            | BIT_ADDR b ⇒ λbit_addr: True.
[821]300                let old_bit ≝ get_arg_1 ? s (BIT_ADDR b) true in
[475]301                let new_bit ≝ ¬old_bit in
[821]302                  set_arg_1 ? s (BIT_ADDR b) new_bit
[475]303            | _ ⇒ λother: False. ?
304            ] (subaddressing_modein … addr)
[936]305        | SETB b ⇒
306            let s ≝ add_ticks1 s in
307            set_arg_1 ? s b false
[475]308        | RL _ ⇒ (* DPM: always ACC_A *)
[936]309            let s ≝ add_ticks1 s in
[821]310            let old_acc ≝ get_8051_sfr ? s SFR_ACC_A in
[475]311            let new_acc ≝ rotate_left … 1 old_acc in
[821]312              set_8051_sfr ? s SFR_ACC_A new_acc
[475]313        | RR _ ⇒ (* DPM: always ACC_A *)
[936]314            let s ≝ add_ticks1 s in
[821]315            let old_acc ≝ get_8051_sfr ? s SFR_ACC_A in
[475]316            let new_acc ≝ rotate_right … 1 old_acc in
[821]317              set_8051_sfr ? s SFR_ACC_A new_acc
[475]318        | RLC _ ⇒ (* DPM: always ACC_A *)
[936]319            let s ≝ add_ticks1 s in
[821]320            let old_cy_flag ≝ get_cy_flag ? s in
321            let old_acc ≝ get_8051_sfr ? s SFR_ACC_A in
[475]322            let new_cy_flag ≝ get_index' ? O ? old_acc in
323            let new_acc ≝ shift_left … 1 old_acc old_cy_flag in
[821]324            let s ≝ set_arg_1 ? s CARRY new_cy_flag in
325              set_8051_sfr ? s SFR_ACC_A new_acc
[475]326        | RRC _ ⇒ (* DPM: always ACC_A *)
[936]327            let s ≝ add_ticks1 s in
[821]328            let old_cy_flag ≝ get_cy_flag ? s in
329            let old_acc ≝ get_8051_sfr ? s SFR_ACC_A in
[475]330            let new_cy_flag ≝ get_index' ? 7 ? old_acc in
331            let new_acc ≝ shift_right … 1 old_acc old_cy_flag in
[821]332            let s ≝ set_arg_1 ? s CARRY new_cy_flag in
333              set_8051_sfr ? s SFR_ACC_A new_acc
[475]334        | SWAP _ ⇒ (* DPM: always ACC_A *)
[936]335            let s ≝ add_ticks1 s in
[821]336            let old_acc ≝ get_8051_sfr ? s SFR_ACC_A in
[475]337            let 〈nu,nl〉 ≝ split ? 4 4 old_acc in
338            let new_acc ≝ nl @@ nu in
[821]339              set_8051_sfr ? s SFR_ACC_A new_acc
[475]340        | PUSH addr ⇒
[936]341            let s ≝ add_ticks1 s in
[475]342            match addr return λx. bool_to_Prop (is_in … [[ direct ]] x) → ? with
343              [ DIRECT d ⇒ λdirect: True.
[821]344                let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
345                let s ≝ set_8051_sfr ? s SFR_SP new_sp in
346                  write_at_stack_pointer ? s d
[475]347              | _ ⇒ λother: False. ⊥
348              ] (subaddressing_modein … addr)
349        | POP addr ⇒
[936]350            let s ≝ add_ticks1 s in
[821]351            let contents ≝ read_at_stack_pointer ? s in
352            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) false in
353            let s ≝ set_8051_sfr ? s SFR_SP new_sp in
354              set_arg_8 ? s addr contents
[475]355        | XCH addr1 addr2 ⇒
[936]356            let s ≝ add_ticks1 s in
[821]357            let old_addr ≝ get_arg_8 ? s false addr2 in
358            let old_acc ≝ get_8051_sfr ? s SFR_ACC_A in
359            let s ≝ set_8051_sfr ? s SFR_ACC_A old_addr in
360              set_arg_8 ? s addr2 old_acc
[475]361        | XCHD addr1 addr2 ⇒
[936]362            let s ≝ add_ticks1 s in
[821]363            let 〈acc_nu, acc_nl〉 ≝ split … 4 4 (get_8051_sfr ? s SFR_ACC_A) in
364            let 〈arg_nu, arg_nl〉 ≝ split … 4 4 (get_arg_8 ? s false addr2) in
[475]365            let new_acc ≝ acc_nu @@ arg_nl in
366            let new_arg ≝ arg_nu @@ acc_nl in
[821]367            let s ≝ set_8051_sfr ? s SFR_ACC_A new_acc in
368              set_arg_8 ? s addr2 new_arg
[475]369        | RET ⇒
[936]370            let s ≝ add_ticks1 s in
[821]371            let high_bits ≝ read_at_stack_pointer ? s in
372            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) false in
373            let s ≝ set_8051_sfr ? s SFR_SP new_sp in
374            let low_bits ≝ read_at_stack_pointer ? s in
375            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) false in
376            let s ≝ set_8051_sfr ? s SFR_SP new_sp in
[475]377            let new_pc ≝ high_bits @@ low_bits in
[821]378              set_program_counter ? s new_pc
[475]379        | RETI ⇒
[936]380            let s ≝ add_ticks1 s in
[821]381            let high_bits ≝ read_at_stack_pointer ? s in
382            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) false in
383            let s ≝ set_8051_sfr ? s SFR_SP new_sp in
384            let low_bits ≝ read_at_stack_pointer ? s in
385            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) false in
386            let s ≝ set_8051_sfr ? s SFR_SP new_sp in
[475]387            let new_pc ≝ high_bits @@ low_bits in
[821]388              set_program_counter ? s new_pc
[475]389        | MOVX addr ⇒
[936]390          let s ≝ add_ticks1 s in
[475]391          (* DPM: only copies --- doesn't affect I/O *)
392          match addr with
393            [ inl l ⇒
394              let 〈addr1, addr2〉 ≝ l in
[821]395                set_arg_8 ? s addr1 (get_arg_8 ? s false addr2)
[475]396            | inr r ⇒
397              let 〈addr1, addr2〉 ≝ r in
[821]398                set_arg_8 ? s addr1 (get_arg_8 ? s false addr2)
[475]399            ]
400        | MOV addr ⇒
[936]401          let s ≝ add_ticks1 s in
[475]402          match addr with
403            [ inl l ⇒
404              match l with
405                [ inl l' ⇒
406                  match l' with
407                    [ inl l'' ⇒
408                      match l'' with
409                        [ inl l''' ⇒
410                          match l''' with
411                            [ inl l'''' ⇒
412                              let 〈addr1, addr2〉 ≝ l'''' in
[821]413                                set_arg_8 ? s addr1 (get_arg_8 ? s false addr2)
[475]414                            | inr r'''' ⇒
415                              let 〈addr1, addr2〉 ≝ r'''' in
[821]416                                set_arg_8 ? s addr1 (get_arg_8 ? s false addr2)
[475]417                            ]
418                        | inr r''' ⇒
419                          let 〈addr1, addr2〉 ≝ r''' in
[821]420                            set_arg_8 ? s addr1 (get_arg_8 ? s false addr2)
[475]421                        ]
422                    | inr r'' ⇒
423                      let 〈addr1, addr2〉 ≝ r'' in
[821]424                        set_arg_16 ? s (get_arg_16 ? s addr2) addr1
[475]425                    ]
426                | inr r ⇒
427                  let 〈addr1, addr2〉 ≝ r in
[821]428                    set_arg_1 ? s addr1 (get_arg_1 ? s addr2 false)
[475]429                ]
430            | inr r ⇒
431              let 〈addr1, addr2〉 ≝ r in
[821]432                set_arg_1 ? s addr1 (get_arg_1 ? s addr2 false)
[475]433            ]
[820]434          | JC addr ⇒
[821]435                  if get_cy_flag ? s then
[936]436                   let s ≝ add_ticks1 s in
437                    set_program_counter ? s (addr_of addr s)
[712]438                  else
[936]439                   let s ≝ add_ticks2 s in
[712]440                    s
441            | JNC addr ⇒
[821]442                  if ¬(get_cy_flag ? s) then
[936]443                   let s ≝ add_ticks1 s in
444                    set_program_counter ? s (addr_of addr s)
[712]445                  else
[936]446                   let s ≝ add_ticks2 s in
[712]447                    s
448            | JB addr1 addr2 ⇒
[821]449                  if get_arg_1 ? s addr1 false then
[936]450                   let s ≝ add_ticks1 s in
451                    set_program_counter ? s (addr_of addr2 s)
[712]452                  else
[936]453                   let s ≝ add_ticks2 s in
[712]454                    s
455            | JNB addr1 addr2 ⇒
[821]456                  if ¬(get_arg_1 ? s addr1 false) then
[936]457                   let s ≝ add_ticks1 s in
458                    set_program_counter ? s (addr_of addr2 s)
[712]459                  else
[936]460                   let s ≝ add_ticks2 s in
[712]461                    s
462            | JBC addr1 addr2 ⇒
[821]463                  let s ≝ set_arg_1 ? s addr1 false in
464                    if get_arg_1 ? s addr1 false then
[936]465                     let s ≝ add_ticks1 s in
466                      set_program_counter ? s (addr_of addr2 s)
[712]467                    else
[936]468                     let s ≝ add_ticks2 s in
[712]469                      s
470            | JZ addr ⇒
[821]471                    if eq_bv ? (get_8051_sfr ? s SFR_ACC_A) (zero 8) then
[936]472                     let s ≝ add_ticks1 s in
473                      set_program_counter ? s (addr_of addr s)
[712]474                    else
[936]475                     let s ≝ add_ticks2 s in
[712]476                      s
477            | JNZ addr ⇒
[821]478                    if ¬(eq_bv ? (get_8051_sfr ? s SFR_ACC_A) (zero 8)) then
[936]479                     let s ≝ add_ticks1 s in
480                      set_program_counter ? s (addr_of addr s)
[712]481                    else
[936]482                     let s ≝ add_ticks2 s in
[712]483                      s
484            | CJNE addr1 addr2 ⇒
485                  match addr1 with
486                    [ inl l ⇒
[822]487                        let 〈addr1, addr2'〉 ≝ l in
[821]488                        let new_cy ≝ ltb (nat_of_bitvector ? (get_arg_8 ? s false addr1))
[822]489                                                 (nat_of_bitvector ? (get_arg_8 ? s false addr2')) in
490                          if ¬(eq_bv ? (get_arg_8 ? s false addr1) (get_arg_8 ? s false addr2')) then
[936]491                            let s ≝ add_ticks1 s in
[822]492                            let s ≝ set_program_counter ? s (addr_of addr2 s) in
[821]493                              set_flags ? s new_cy (None ?) (get_ov_flag ? s)
[712]494                          else
[936]495                            let s ≝ add_ticks2 s in
[821]496                            (set_flags ? s new_cy (None ?) (get_ov_flag ? s))
[712]497                    | inr r' ⇒
[822]498                        let 〈addr1, addr2'〉 ≝ r' in
[821]499                        let new_cy ≝ ltb (nat_of_bitvector ? (get_arg_8 ? s false addr1))
[822]500                                                 (nat_of_bitvector ? (get_arg_8 ? s false addr2')) in
501                          if ¬(eq_bv ? (get_arg_8 ? s false addr1) (get_arg_8 ? s false addr2')) then
[936]502                            let s ≝ add_ticks1 s in
[822]503                            let s ≝ set_program_counter ? s (addr_of addr2 s) in
[821]504                              set_flags ? s new_cy (None ?) (get_ov_flag ? s)
[712]505                          else
[936]506                            let s ≝ add_ticks2 s in
[821]507                            (set_flags ? s new_cy (None ?) (get_ov_flag ? s))
[712]508                    ]
509            | DJNZ addr1 addr2 ⇒
[821]510              let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 ? s true addr1) (bitvector_of_nat 8 1) false in
511              let s ≝ set_arg_8 ? s addr1 result in
[820]512                if ¬(eq_bv ? result (zero 8)) then
[936]513                 let s ≝ add_ticks1 s in
514                  set_program_counter ? s (addr_of addr2 s)
[820]515                else
[936]516                 let s ≝ add_ticks2 s in
[820]517                  s
[936]518        | NOP ⇒
519           let s ≝ add_ticks2 s in
520            s
[820]521        ].
522    try assumption
[856]523    try @I
[820]524    try (
525      @ (execute_1_technical … (subaddressing_modein …))
526      @ I
527    )
528qed.
529
[928]530definition execute_1_0: Status → instruction × Word × nat → Status ≝
531  λs,instr_pc_ticks.
532    let 〈instr_pc, ticks〉 ≝ instr_pc_ticks in
[820]533    let 〈instr, pc〉 ≝ 〈fst … instr_pc, snd … instr_pc〉 in
[821]534    let s ≝ set_program_counter ? s pc in
[820]535    let s ≝
536      match instr with
[936]537      [ RealInstruction instr ⇒ execute_1_preinstruction 〈ticks,ticks〉 [[ relative ]] ?
[822]538        (λx. λs.
[820]539        match x return λs. bool_to_Prop (is_in ? [[ relative ]] s) → ? with
[822]540        [ RELATIVE r ⇒ λ_. \snd (half_add ? (program_counter ? s) (sign_extension r))
[820]541        | _ ⇒ λabsd. ⊥
542        ] (subaddressing_modein … x)) instr s
543      | ACALL addr ⇒
[936]544          let s ≝ set_clock ? s (ticks + clock ? s) in
[820]545          match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → ? with
546            [ ADDR11 a ⇒ λaddr11: True.
[1511]547              let new_sp ≝ \snd (half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1)) in
[821]548              let s ≝ set_8051_sfr ? s SFR_SP new_sp in
[1511]549              let pc_bu ≝ \fst (split ? 8 8 (program_counter ? s)) in
550              let pc_bl ≝ \snd (split ? 8 8 (program_counter ? s)) in
[821]551              let s ≝ write_at_stack_pointer ? s pc_bl in
[1511]552              let new_sp ≝ \snd (half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1)) in
[821]553              let s ≝ set_8051_sfr ? s SFR_SP new_sp in
554              let s ≝ write_at_stack_pointer ? s pc_bu in
[1511]555              let thr ≝ \fst (split ? 3 8 a) in
556              let eig ≝ \snd (split ? 3 8 a) in
557              let fiv ≝ \fst (split ? 5 3 pc_bu) in
558              let thr' ≝ \snd (split ? 5 3 pc_bu) in
[820]559              let new_addr ≝ (fiv @@ thr) @@ pc_bl in
[821]560                set_program_counter ? s new_addr
[820]561            | _ ⇒ λother: False. ⊥
562            ] (subaddressing_modein … addr)
563        | LCALL addr ⇒
[936]564          let s ≝ set_clock ? s (ticks + clock ? s) in
[820]565          match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → ? with
566            [ ADDR16 a ⇒ λaddr16: True.
[1511]567              let new_sp ≝ \snd (half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1)) in
[821]568              let s ≝ set_8051_sfr ? s SFR_SP new_sp in
[1511]569              let pc_bu ≝ \fst (split ? 8 8 (program_counter ? s)) in
570              let pc_bl ≝ \snd (split ? 8 8 (program_counter ? s)) in
[821]571              let s ≝ write_at_stack_pointer ? s pc_bl in
[1511]572              let new_sp ≝ \snd (half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1)) in
[821]573              let s ≝ set_8051_sfr ? s SFR_SP new_sp in
574              let s ≝ write_at_stack_pointer ? s pc_bu in
575                set_program_counter ? s a
[820]576            | _ ⇒ λother: False. ⊥
577            ] (subaddressing_modein … addr)
[757]578        | MOVC addr1 addr2 ⇒
[936]579          let s ≝ set_clock ? s (ticks + clock ? s) in
[757]580          match addr2 return λx. bool_to_Prop (is_in … [[ acc_dptr; acc_pc ]] x) → ? with
581            [ ACC_DPTR ⇒ λacc_dptr: True.
[821]582              let big_acc ≝ (zero 8) @@ (get_8051_sfr ? s SFR_ACC_A) in
583              let dptr ≝ (get_8051_sfr ? s SFR_DPH) @@ (get_8051_sfr ? s SFR_DPL) in
[1514]584              let new_addr ≝ \snd (half_add ? dptr big_acc) in
[821]585              let result ≝ lookup ? ? new_addr (code_memory ? s) (zero ?) in
586                set_8051_sfr ? s SFR_ACC_A result
[757]587            | ACC_PC ⇒ λacc_pc: True.
[821]588              let big_acc ≝ (zero 8) @@ (get_8051_sfr ? s SFR_ACC_A) in
[1514]589              let inc_pc ≝ \snd (half_add ? (program_counter ? s) (bitvector_of_nat 16 1)) in
[757]590              (* DPM: Under specified: does the carry from PC incrementation affect the *)
591              (*      addition of the PC with the DPTR? At the moment, no.              *)
[821]592              let s ≝ set_program_counter ? s inc_pc in
[1514]593              let new_addr ≝ \snd (half_add ? inc_pc big_acc) in
[821]594              let result ≝ lookup ? ? new_addr (code_memory ? s) (zero ?) in
595                set_8051_sfr ? s SFR_ACC_A result
[757]596            | _ ⇒ λother: False. ⊥
597            ] (subaddressing_modein … addr2)
[820]598        | JMP _ ⇒ (* DPM: always indirect_dptr *)
[936]599          let s ≝ set_clock ? s (ticks + clock ? s) in
[821]600          let dptr ≝ (get_8051_sfr ? s SFR_DPH) @@ (get_8051_sfr ? s SFR_DPL) in
601          let big_acc ≝ (zero 8) @@ (get_8051_sfr ? s SFR_ACC_A) in
[1511]602          let jmp_addr ≝ \snd (half_add ? big_acc dptr) in
603          let new_pc ≝ \snd (half_add ? (program_counter ? s) jmp_addr) in
[821]604            set_program_counter ? s new_pc
[820]605        | LJMP addr ⇒
[936]606          let s ≝ set_clock ? s (ticks + clock ? s) in
[820]607          match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → ? with
608            [ ADDR16 a ⇒ λaddr16: True.
[821]609                set_program_counter ? s a
[820]610            | _ ⇒ λother: False. ⊥
611            ] (subaddressing_modein … addr)
612        | SJMP addr ⇒
[936]613          let s ≝ set_clock ? s (ticks + clock ? s) in
[820]614          match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
615            [ RELATIVE r ⇒ λrelative: True.
[1511]616                let new_pc ≝ \snd (half_add ? (program_counter ? s) (sign_extension r)) in
[821]617                  set_program_counter ? s new_pc
[820]618            | _ ⇒ λother: False. ⊥
619            ] (subaddressing_modein … addr)
620        | AJMP addr ⇒
[936]621          let s ≝ set_clock ? s (ticks + clock ? s) in
[820]622          match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → ? with
623            [ ADDR11 a ⇒ λaddr11: True.
[1511]624              let pc_bu ≝ \fst (split ? 8 8 (program_counter ? s)) in
625              let pc_bl ≝ \snd (split ? 8 8 (program_counter ? s)) in
626              let nu ≝ \fst (split ? 4 4 pc_bu) in
627              let nl ≝ \snd (split ? 4 4 pc_bu) in
[820]628              let bit ≝ get_index' ? O ? nl in
[1511]629              let relevant1 ≝ \fst (split ? 3 8 a) in
630              let relevant2 ≝ \snd (split ? 3 8 a) in
[820]631              let new_addr ≝ (nu @@ (bit ::: relevant1)) @@ relevant2 in
[1511]632              let new_pc ≝ \snd (half_add ? (program_counter ? s) new_addr) in
[821]633                set_program_counter ? s new_pc
[820]634            | _ ⇒ λother: False. ⊥
635            ] (subaddressing_modein … addr)
636      ]
[475]637    in
638      s.
639    try assumption
640    try (
641      normalize
642      repeat (@ (le_S_S))
643      @ (le_O_n)
644    )
645    try (
646      @ (execute_1_technical … (subaddressing_modein …))
647      @ I
648    )
649    try (
650      normalize
651      @ I
652    )     
653qed.
654
[928]655definition execute_1: Status → Status ≝
656  λs: Status.
657    let instr_pc_ticks ≝ fetch (code_memory ? s) (program_counter ? s) in
658     execute_1_0 s instr_pc_ticks.
659
[1037]660definition execute_1_pseudo_instruction0: (nat × nat) → PseudoStatus → ? → ? → PseudoStatus ≝
661  λticks,s,instr,pc.
[821]662  let s ≝ set_program_counter ? s pc in
[820]663  let s ≝
664    match instr with
[936]665    [ Instruction instr ⇒ execute_1_preinstruction ticks … (λx, y. address_of_word_labels y x) instr s
666    | Comment cmt ⇒
667       let s ≝ set_clock ? s (\fst ticks + clock ? s) in
668        s
[820]669    | Cost cst ⇒ s
[936]670    | Jmp jmp ⇒
671       let s ≝ set_clock ? s (\fst ticks + clock ? s) in
672        set_program_counter ? s (address_of_word_labels s jmp)
[820]673    | Call call ⇒
[936]674      let s ≝ set_clock ? s (\fst ticks + clock ? s) in
[822]675      let a ≝ address_of_word_labels s call in
[821]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
[910]684    | Mov dptr ident ⇒
[936]685      let s ≝ set_clock ? s (\fst ticks + clock ? s) in
[910]686      let preamble ≝ \fst (code_memory ? s) in
[1494]687      let data_labels ≝ construct_datalabels (map … (fst …) preamble) in
[1515]688        set_arg_16 ? s (get_arg_16 ? s (DATA16 (lookup_def ? ? data_labels ident (zero ?)))) dptr
[820]689    ]
690  in
691    s.
692  normalize
693  @ I
694qed.
695
[1037]696definition execute_1_pseudo_instruction: (Word → nat × nat) → PseudoStatus → PseudoStatus ≝
697  λticks_of,s.
698  let 〈instr, pc〉 ≝ fetch_pseudo_instruction (\snd (code_memory ? s)) (program_counter ? s) in
699  let ticks ≝ ticks_of (program_counter ? s) in
700   execute_1_pseudo_instruction0 ticks s instr pc.
701
[475]702let rec execute (n: nat) (s: Status) on n: Status ≝
703  match n with
704    [ O ⇒ s
705    | S o ⇒ execute o (execute_1 s)
706    ].
[820]707
[936]708let rec execute_pseudo_instruction (n: nat) (ticks_of: Word → nat × nat) (s: PseudoStatus) on n: PseudoStatus ≝
[820]709  match n with
710    [ O ⇒ s
[822]711    | S o ⇒ execute_pseudo_instruction o ticks_of (execute_1_pseudo_instruction ticks_of s)
[820]712    ].
Note: See TracBrowser for help on using the repository browser.