source: src/ASM/Erase.ma @ 1495

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

added erasure for lin

File size: 3.5 KB
Line 
1include "ASM/ASM.ma".
2include "ASM/BitVectorTrie.ma".
3     
4let rec pre_erase
5  (the_program: list labelled_instruction) (labels: list Identifier)
6    on the_program: ((BitVectorTrie Identifier 16) × (list labelled_instruction)) ≝
7  match the_program with
8  [ nil        ⇒
9    match labels with
10    [ nil ⇒ 〈Stub Identifier 16, [ ]〉 (* XXX: labels should be empty *)
11    | _   ⇒ ⊥
12    ]
13  | cons hd tl ⇒
14    let 〈label, instruction〉 ≝ hd in
15      match label with
16      [ None ⇒
17        let 〈maps, the_program〉 ≝ pre_erase tl labels in
18        match instruction with
19        [ Cost cost ⇒ 〈maps, the_program〉
20        | _ ⇒ 〈maps, 〈None …, instruction〉 :: the_program〉
21        ]
22      | Some label ⇒
23        match instruction with
24        [ Cost cost ⇒ pre_erase tl (label :: labels)
25        | _ ⇒
26          let 〈maps, the_program〉 ≝ pre_erase tl [ ] in
27          let maps ≝ foldr … (λl. λmap. insert … l label map) maps (label::labels) in
28            〈maps, the_program〉
29        ]
30      ]
31  ].
32  @daemon
33qed.
34
35definition relabel_instruction: preinstruction Identifier → BitVectorTrie Identifier 16 → preinstruction Identifier ≝
36  λpre.
37  λmap.
38  match pre with
39  [ JC ident ⇒
40    let located ≝ lookup … ident map ident in
41      JC … located
42  | JNC ident ⇒
43    let located ≝ lookup … ident map ident in
44      JNC … located
45  | JB bit ident ⇒
46    let located ≝ lookup … ident map ident in
47      JB … bit located
48  | JNB bit ident ⇒
49    let located ≝ lookup … ident map ident in
50      JNB … bit located
51  | JBC bit ident ⇒
52    let located ≝ lookup … ident map ident in
53      JBC … bit located
54  | JZ ident ⇒
55    let located ≝ lookup … ident map ident in
56      JZ … located
57  | JNZ ident ⇒
58    let located ≝ lookup … ident map ident in
59      JNZ … located
60  | CJNE src ident ⇒
61    let located ≝ lookup … ident map ident in
62      CJNE … src located
63  | DJNZ src ident ⇒
64    let located ≝ lookup … ident map ident in
65      DJNZ … src located
66  (* XXX: no identifiers in rest of instructions *)
67  | _ ⇒ pre
68  ].
69
70definition relabel_pseudo_instruction: pseudo_instruction → BitVectorTrie Identifier 16 → pseudo_instruction ≝
71  λpseudo.
72  λmap.
73  match pseudo with
74  [ Instruction instr ⇒ Instruction (relabel_instruction instr map)
75  | Cost cost ⇒ Cost cost
76  | Comment comment ⇒ Comment comment
77  | Jmp ident ⇒
78    let located ≝ lookup … ident map ident in
79      Jmp located
80  | Call ident ⇒
81    let located ≝ lookup … ident map ident in
82      Call located
83  | Mov dptr ident ⇒
84    let located ≝ lookup … ident map ident in
85      Mov dptr located
86  ].
87     
88let rec relabel
89  (the_program: list labelled_instruction) (map: BitVectorTrie Identifier 16)
90    on the_program: list labelled_instruction ≝
91  match the_program with
92  [ nil        ⇒ [ ]
93  | cons hd tl ⇒
94    let 〈label, instruction〉 ≝ hd in
95    let relabelled ≝ relabel_pseudo_instruction instruction map in
96    let label ≝
97      match label with
98      [ None ⇒ None …
99      | Some label ⇒ Some … (lookup … ident map ident)
100      ]
101    in
102      〈label, relabelled〉 :: relabel tl map
103  ].
104
105definition erase: pseudo_assembly_program → pseudo_assembly_program ≝
106  λprogram.
107  let 〈preamble, instructions〉 ≝ program in
108  let 〈maps, instructions〉 ≝ pre_erase instructions [ ] in
109  let relabelled ≝ relabel instructions maps in
110    〈preamble, relabelled〉.
Note: See TracBrowser for help on using the repository browser.