source: src/ASM/Erase.ma @ 1461

Last change on this file since 1461 was 1461, checked in by mulligan, 9 years ago

rewrote erasure for assembly programs

File size: 3.3 KB
RevLine 
[1460]1include "ASM/ASM.ma".
[1461]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    ]
[1460]13  | cons hd tl ⇒
[1461]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〉
[1460]21        ]
[1461]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        ]
[1460]30      ]
31  ].
[1461]32  @daemon
33qed.
[1460]34
[1461]35definition relabel_instruction: preinstruction Identifier → BitVectorTrie Identifier 16 → preinstruction Identifier ≝
36  λpre.
37  λmap.
38  match pre with
[1460]39  [ JC ident ⇒
[1461]40    let located ≝ lookup … ident map ident in
41      JC … located
[1460]42  | JNC ident ⇒
[1461]43    let located ≝ lookup … ident map ident in
44      JNC … located
[1460]45  | JB bit ident ⇒
[1461]46    let located ≝ lookup … ident map ident in
47      JB … bit located
[1460]48  | JNB bit ident ⇒
[1461]49    let located ≝ lookup … ident map ident in
50      JNB … bit located
[1460]51  | JBC bit ident ⇒
[1461]52    let located ≝ lookup … ident map ident in
53      JBC … bit located
[1460]54  | JZ ident ⇒
[1461]55    let located ≝ lookup … ident map ident in
56      JZ … located
[1460]57  | JNZ ident ⇒
[1461]58    let located ≝ lookup … ident map ident in
59      JNZ … located
[1460]60  | CJNE src ident ⇒
[1461]61    let located ≝ lookup … ident map ident in
62      CJNE … src located
[1460]63  | DJNZ src ident ⇒
[1461]64    let located ≝ lookup … ident map ident in
65      DJNZ … src located
[1460]66  (* XXX: no identifiers in rest of instructions *)
[1461]67  | _ ⇒ pre
[1460]68  ].
[1461]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
[1460]77  | Jmp ident ⇒
[1461]78    let located ≝ lookup … ident map ident in
79      Jmp located
[1460]80  | Call ident ⇒
[1461]81    let located ≝ lookup … ident map ident in
82      Call located
[1460]83  | Mov dptr ident ⇒
[1461]84    let located ≝ lookup … ident map ident in
85      Mov dptr located
[1460]86  ].
87     
[1461]88let rec relabel
89  (the_program: list labelled_instruction) (map: BitVectorTrie Identifier 16)
90    on the_program: list labelled_instruction ≝
[1460]91  match the_program with
[1461]92  [ nil        ⇒ [ ]
93  | cons hd tl ⇒
94    let 〈label, instruction〉 ≝ hd in
95    let relabelled ≝ relabel_pseudo_instruction instruction map in
96      〈label, relabelled〉 :: relabel tl map
[1460]97  ].
98
99definition erase: pseudo_assembly_program → pseudo_assembly_program ≝
100  λprogram.
[1461]101  let 〈preamble, instructions〉 ≝ program in
102  let 〈maps, instructions〉 ≝ pre_erase instructions [ ] in
103  let relabelled ≝ relabel instructions maps in
104    〈preamble, relabelled〉.
Note: See TracBrowser for help on using the repository browser.