Last change
on this file since 1487 was
1487,
checked in by mulligan, 9 years ago
|
committing some code for well labelling
|
File size:
1.9 KB
|
Line | |
---|
1 | include "ASM/ASM.ma". |
---|
2 | include "ASM/Fetch.ma". |
---|
3 | include "ASM/Arithmetic.ma". |
---|
4 | |
---|
5 | definition well_labelled_p ≝ |
---|
6 | ∀pc: Word. |
---|
7 | ∀program: BitVectorTrie Byte 16. |
---|
8 | ∀cost_labels. |
---|
9 | let 〈instruction, newpc, cost〉 ≝ fetch program pc in |
---|
10 | match instruction with |
---|
11 | [ LCALL lcall ⇒ ? |
---|
12 | | ACALL acall ⇒ ? |
---|
13 | | AJMP ajmp ⇒ |
---|
14 | match ajmp return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → ? with |
---|
15 | [ ADDR11 addr11 ⇒ λ_. |
---|
16 | let 〈pc_bu, pc_bl〉 ≝ split … 8 8 pc in |
---|
17 | let 〈nu, nl〉 ≝ split … 4 4 pc_bu in |
---|
18 | let bit ≝ get_index' … O ? nl in |
---|
19 | let 〈relevant1, relevant2〉 ≝ split … 3 8 addr11 in |
---|
20 | let new_addr ≝ (nu @@ (bit ::: relevant1)) @@ relevant2 in |
---|
21 | let 〈carry, new_pc〉 ≝ half_add … pc new_addr in |
---|
22 | match lookup_opt … new_pc cost_labels with |
---|
23 | [ None ⇒ False |
---|
24 | | _ ⇒ True |
---|
25 | ] |
---|
26 | | _ ⇒ λ_. ⊥ |
---|
27 | ] (subaddressing_modein … ajmp) |
---|
28 | | LJMP ljmp ⇒ |
---|
29 | match ljmp return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → ? with |
---|
30 | [ ADDR16 addr16 ⇒ λ_. |
---|
31 | match lookup_opt … addr16 cost_labels with |
---|
32 | [ None ⇒ False |
---|
33 | | _ ⇒ True |
---|
34 | ] |
---|
35 | | _ ⇒ λ_. ⊥ |
---|
36 | ] (subaddressing_modein … ljmp) |
---|
37 | | SJMP sjmp ⇒ |
---|
38 | match sjmp return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with |
---|
39 | [ RELATIVE rel ⇒ λ_. |
---|
40 | let 〈carry, new_pc〉 ≝ half_add … pc (sign_extend 8 8 rel) in |
---|
41 | match lookup_opt … new_pc cost_labels with |
---|
42 | [ None ⇒ False |
---|
43 | | _ ⇒ True |
---|
44 | ] |
---|
45 | | _ ⇒ λ_. ⊥ |
---|
46 | ] (subaddressing_modein … sjmp) |
---|
47 | | JMP jmp ⇒ ? |
---|
48 | | MOVC _ _ ⇒ True |
---|
49 | | RealInstruction instruction ⇒ |
---|
50 | match instruction with |
---|
51 | [ JZ jz ⇒ ? |
---|
52 | | _ ⇒ ? |
---|
53 | ] |
---|
54 | ]. |
---|
Note: See
TracBrowser
for help on using the repository browser.