source: src/ASM/WellLabeled.ma @ 1487

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

committing some code for well labelling

File size: 1.9 KB
Line 
1include "ASM/ASM.ma".
2include "ASM/Fetch.ma".
3include "ASM/Arithmetic.ma".
4
5definition 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.