source: src/ASM/Erase.ma @ 2211

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

utilities and ASM ported to the new standard library

File size: 3.5 KB
RevLine 
[1460]1include "ASM/ASM.ma".
[1515]2
[1461]3let rec pre_erase
4  (the_program: list labelled_instruction) (labels: list Identifier)
[1515]5    on the_program: ((identifier_map ASMTag Identifier) × (list labelled_instruction)) ≝
[1461]6  match the_program with
7  [ nil        ⇒
8    match labels with
[1515]9    [ nil ⇒ 〈empty_map ??, [ ]〉 (* XXX: labels should be empty *)
[1461]10    | _   ⇒ ⊥
11    ]
[1460]12  | cons hd tl ⇒
[1461]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〉
[1460]20        ]
[1461]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
[1515]26          let maps ≝ foldr ?? (λl. λmap. add … map l label) maps (label::labels) in
[1461]27            〈maps, the_program〉
28        ]
[1460]29      ]
30  ].
[1461]31  @daemon
32qed.
[1460]33
[1515]34definition relabel_instruction: preinstruction Identifier → identifier_map ASMTag Identifier → preinstruction Identifier ≝
[1461]35  λpre.
36  λmap.
37  match pre with
[1460]38  [ JC ident ⇒
[1515]39    let located ≝ lookup_def … map ident ident in
[1461]40      JC … located
[1460]41  | JNC ident ⇒
[1515]42    let located ≝ lookup_def … map ident ident in
[1461]43      JNC … located
[1460]44  | JB bit ident ⇒
[1515]45    let located ≝ lookup_def … map ident ident in
[1461]46      JB … bit located
[1460]47  | JNB bit ident ⇒
[1515]48    let located ≝ lookup_def … map ident ident in
[1461]49      JNB … bit located
[1460]50  | JBC bit ident ⇒
[1515]51    let located ≝ lookup_def … map ident ident in
[1461]52      JBC … bit located
[1460]53  | JZ ident ⇒
[1515]54    let located ≝ lookup_def … map ident ident in
[1461]55      JZ … located
[1460]56  | JNZ ident ⇒
[1515]57    let located ≝ lookup_def … map ident ident in
[1461]58      JNZ … located
[1460]59  | CJNE src ident ⇒
[1515]60    let located ≝ lookup_def … map ident ident in
[1461]61      CJNE … src located
[1460]62  | DJNZ src ident ⇒
[1515]63    let located ≝ lookup_def … map ident ident in
[1461]64      DJNZ … src located
[1460]65  (* XXX: no identifiers in rest of instructions *)
[1461]66  | _ ⇒ pre
[1460]67  ].
[1461]68
[1515]69definition relabel_pseudo_instruction: pseudo_instruction → identifier_map ASMTag Identifier → pseudo_instruction ≝
[1461]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
[1460]76  | Jmp ident ⇒
[1515]77    let located ≝ lookup_def … map ident ident in
[1461]78      Jmp located
[1460]79  | Call ident ⇒
[1515]80    let located ≝ lookup_def … map ident ident in
[1461]81      Call located
[1460]82  | Mov dptr ident ⇒
[1515]83    let located ≝ lookup_def … map ident ident in
[1461]84      Mov dptr located
[1460]85  ].
[1600]86
[1461]87let rec relabel
[1515]88  (the_program: list labelled_instruction) (map: identifier_map ASMTag Identifier)
[1461]89    on the_program: list labelled_instruction ≝
[1460]90  match the_program with
[1461]91  [ nil        ⇒ [ ]
92  | cons hd tl ⇒
93    let 〈label, instruction〉 ≝ hd in
94    let relabelled ≝ relabel_pseudo_instruction instruction map in
[1463]95    let label ≝
96      match label with
97      [ None ⇒ None …
[1600]98      | Some label ⇒ Some … (lookup_def ?? map ident ident)
[1463]99      ]
100    in
[1461]101      〈label, relabelled〉 :: relabel tl map
[1460]102  ].
103
104definition erase: pseudo_assembly_program → pseudo_assembly_program ≝
105  λprogram.
[1461]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.