source: src/ASM/Erase.ma @ 1600

Last change on this file since 1600 was 1600, checked in by sacerdot, 8 years ago

utilities and ASM ported to the new standard library

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