source: src/ASM/WellLabeled.ma @ 1646

Last change on this file since 1646 was 1494, checked in by mulligan, 8 years ago

changes to get everything compiling again

File size: 6.9 KB
Line 
1include "ASM/ASM.ma".
2include "ASM/Fetch.ma".
3include "ASM/Arithmetic.ma".
4
5let rec member_p
6  (a: Type[0]) (eq: a → a → bool) (element: a) (the_list: list a)
7    on the_list: Prop ≝
8  match the_list with
9  [ nil ⇒ False
10  | cons hd tl ⇒
11    match eq hd element with
12    [ true ⇒ True
13    | false ⇒ member_p … eq element tl
14    ]
15  ].
16
17definition well_labelled_p ≝
18  ∀pc: Word.
19  ∀acc_a: Byte.
20  ∀function_locations: list Word.
21  ∀program: BitVectorTrie Byte 16.
22  ∀cost_labels.
23    let 〈instruction, newpc, cost〉 ≝ fetch program pc in
24      match instruction with
25      [ LCALL lcall ⇒
26        match lcall return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → ? with
27        [ ADDR16 addr16 ⇒ λ_. member_p … (eq_bv …) addr16 function_locations
28        | _ ⇒ λabsurd. ⊥
29        ] (subaddressing_modein … lcall)
30      | ACALL acall ⇒
31        match acall return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → ? with
32        [ ADDR11 addr11 ⇒ λ_.
33          let 〈pc_bu, pc_bl〉 ≝ split … 8 8 pc in
34          let 〈thr, eig〉 ≝ split … 3 8 addr11 in
35          let 〈fiv, thr'〉 ≝ split … 5 3 pc_bu in
36          let new_pc ≝ (fiv @@ thr) @@ pc_bl in
37            match lookup_opt … new_pc cost_labels with
38            [ None ⇒ False
39            | _    ⇒ True
40            ]
41        | _ ⇒ λabsurd. ⊥
42        ] (subaddressing_modein … acall)
43      | AJMP ajmp ⇒
44        match ajmp return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → ? with
45        [ ADDR11 addr11 ⇒ λ_.
46          let 〈pc_bu, pc_bl〉 ≝ split … 8 8 pc in
47          let 〈nu, nl〉 ≝ split … 4 4 pc_bu in
48          let bit ≝ get_index' … O ? nl in
49          let 〈relevant1, relevant2〉 ≝ split … 3 8 addr11 in
50          let new_addr ≝ (nu @@ (bit ::: relevant1)) @@ relevant2 in
51          let 〈carry, new_pc〉 ≝ half_add … pc new_addr in
52            match lookup_opt … new_pc cost_labels with
53            [ None ⇒ False
54            | _    ⇒ True
55            ]
56        | _ ⇒ λabsurd. ⊥
57        ] (subaddressing_modein … ajmp)
58      | LJMP ljmp ⇒
59        match ljmp return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → ? with
60        [ ADDR16 addr16 ⇒ λ_.
61          match lookup_opt … addr16 cost_labels with
62          [ None ⇒ False
63          | _    ⇒ True
64          ]
65        | _ ⇒ λabsurd. ⊥
66        ] (subaddressing_modein … ljmp)
67      | SJMP sjmp ⇒
68        match sjmp return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
69        [ RELATIVE rel ⇒ λ_.
70          let 〈carry, new_pc〉 ≝ half_add … pc (sign_extend 8 8 rel) in
71            match lookup_opt … new_pc cost_labels with
72            [ None ⇒ False
73            | _    ⇒ True
74            ]
75        | _ ⇒ λabsurd. ⊥
76        ] (subaddressing_modein … sjmp)
77      | JMP jmp ⇒ True (* XXX: check is dynamic, as we can only jump to functions *)
78      | MOVC _ _ ⇒ True
79      | RealInstruction instruction ⇒
80        match instruction with
81        [ JZ jz ⇒
82          match jz return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
83          [ RELATIVE rel ⇒ λ_.
84            let 〈carry, new_pc〉 ≝ half_add … pc (sign_extend 8 8 rel) in
85              match lookup_opt … new_pc cost_labels with
86              [ None ⇒ False
87              | _    ⇒ True
88              ]
89          | _ ⇒ λabsurd. ⊥
90          ] (subaddressing_modein … jz)
91        | JNZ jnz ⇒
92          match jnz return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
93          [ RELATIVE rel ⇒ λ_.
94            let 〈carry, new_pc〉 ≝ half_add … pc (sign_extend 8 8 rel) in
95              match lookup_opt … new_pc cost_labels with
96              [ None ⇒ False
97              | _    ⇒ True
98              ]
99          | _ ⇒ λabsurd. ⊥
100          ] (subaddressing_modein … jnz)
101        | JC jc ⇒
102          match jc return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
103          [ RELATIVE rel ⇒ λ_.
104            let 〈carry, new_pc〉 ≝ half_add … pc (sign_extend 8 8 rel) in
105              match lookup_opt … new_pc cost_labels with
106              [ None ⇒ False
107              | _    ⇒ True
108              ]
109          | _ ⇒ λabsurd. ⊥
110          ] (subaddressing_modein … jc)
111        | JNC jnc ⇒
112          match jnc return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
113          [ RELATIVE rel ⇒ λ_.
114            let 〈carry, new_pc〉 ≝ half_add … pc (sign_extend 8 8 rel) in
115              match lookup_opt … new_pc cost_labels with
116              [ None ⇒ False
117              | _    ⇒ True
118              ]
119          | _ ⇒ λabsurd. ⊥
120          ] (subaddressing_modein … jnc)
121        | JB baddr jb ⇒
122          match jb return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
123          [ RELATIVE rel ⇒ λ_.
124            let 〈carry, new_pc〉 ≝ half_add … pc (sign_extend 8 8 rel) in
125              match lookup_opt … new_pc cost_labels with
126              [ None ⇒ False
127              | _    ⇒ True
128              ]
129          | _ ⇒ λabsurd. ⊥
130          ] (subaddressing_modein … jb)
131        | JNB baddr jnb ⇒
132          match jnb return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
133          [ RELATIVE rel ⇒ λ_.
134            let 〈carry, new_pc〉 ≝ half_add … pc (sign_extend 8 8 rel) in
135              match lookup_opt … new_pc cost_labels with
136              [ None ⇒ False
137              | _    ⇒ True
138              ]
139          | _ ⇒ λabsurd. ⊥
140          ] (subaddressing_modein … jnb)
141        | JBC baddr jbc ⇒
142          match jbc return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
143          [ RELATIVE rel ⇒ λ_.
144            let 〈carry, new_pc〉 ≝ half_add … pc (sign_extend 8 8 rel) in
145              match lookup_opt … new_pc cost_labels with
146              [ None ⇒ False
147              | _    ⇒ True
148              ]
149          | _ ⇒ λabsurd. ⊥
150          ] (subaddressing_modein … jbc)
151        | CJNE args cjne ⇒
152          match cjne return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
153          [ RELATIVE rel ⇒ λ_.
154            let 〈carry, new_pc〉 ≝ half_add … pc (sign_extend 8 8 rel) in
155              match lookup_opt … new_pc cost_labels with
156              [ None ⇒ False
157              | _    ⇒ True
158              ]
159          | _ ⇒ λabsurd. ⊥
160          ] (subaddressing_modein … cjne)
161        | DJNZ args djnz ⇒
162          match djnz return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
163          [ RELATIVE rel ⇒ λ_.
164            let 〈carry, new_pc〉 ≝ half_add … pc (sign_extend 8 8 rel) in
165              match lookup_opt … new_pc cost_labels with
166              [ None ⇒ False
167              | _    ⇒ True
168              ]
169          | _ ⇒ λabsurd. ⊥
170          ] (subaddressing_modein … djnz)
171        | _ ⇒ True
172        ]
173      ].
174  [*: normalize in absurd; // ]
175qed.
Note: See TracBrowser for help on using the repository browser.