source: src/RTLabs/RTLAbstoRTL.ma @ 789

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

More work on rtlabs -> rtl pass.

File size: 5.0 KB
Line 
1include "RTLabs/syntax.ma".
2include "RTL/RTL.ma".
3include "common/AssocList.ma".
4include "common/Graphs.ma".
5
6definition add_graph ≝
7  λlbl: label.
8  λstmt.
9  λdef.
10  let f_labgen' ≝ f_labgen def in
11  let f_reggen' ≝ f_reggen def in
12  let f_sig' ≝ f_sig def in
13  let f_result' ≝ f_result def in
14  let f_params' ≝ f_params def in
15  let f_locals' ≝ f_locals def in
16  let f_ptrs' ≝ f_ptrs def in
17  let f_stacksize' ≝ f_stacksize def in
18  let f_graph' ≝ add ? ? (f_graph def) lbl stmt in
19  let f_entry' ≝ f_entry def in
20  let f_exit' ≝ f_exit def in
21    mk_internal_function
22      f_labgen' f_reggen' f_sig' f_result'
23      f_params' f_locals' f_ptrs' f_stacksize'
24      f_graph' f_entry' f_exit'.
25     
26definition fresh_label ≝
27  λdef.
28    match fresh LabelTag (f_labgen def) with
29    [ OK lbl_univ ⇒ Some ? (\fst … lbl_univ)
30    | Error ⇒ None ?
31    ].
32
33axiom fresh_reg: internal_function → internal_function × register.
34
35let rec fresh_regs (def: internal_function) (n: nat) on n ≝
36  match n with
37  [ O   ⇒ 〈def, [ ]〉
38  | S n ⇒
39    let 〈def, res〉 ≝ fresh_regs def n in
40    let 〈def, r〉 ≝ fresh_reg def in
41      〈def, r :: res〉
42  ].
43
44definition addr_regs ≝
45  λregs.
46  match regs with
47  [ cons hd tl ⇒
48    match tl with
49    [ cons hd' tl' ⇒ Some (register × register) 〈hd, hd'〉
50    | nil          ⇒ None (register × register)
51    ]
52  | nil ⇒ None (register × register)
53  ].
54
55inductive register_type: Type[0] ≝
56  | register_int: register → register_type
57  | register_ptr: register → register → register_type.
58
59definition local_env ≝ assoc_list register register_type.
60
61definition initialize_local_env_internal ≝
62  λeq.
63  λruniverse.
64  λptrs.
65  λlenv.
66  λr.
67    let fresh ≝ snd ? ? (fresh_reg runiverse) in
68    let rt ≝
69      match member ? eq r ptrs with
70      [ true  ⇒ register_ptr r fresh
71      | false ⇒ register_int r
72      ]
73    in
74    assoc_list_add ? ? 〈r, rt〉 lenv.
75
76definition initialize_local_env ≝
77  λruniverse.
78  λptrs.
79  λregisters.
80    foldl ? ? (initialize_local_env_internal (eq_identifier RegisterTag) runiverse ptrs) [ ] registers.
81
82definition filter_and_to_list_local_env_internal ≝
83  λlenv.
84  λl.
85  λr.
86  match assoc_list_lookup ? ? r (eq_identifier RegisterTag) lenv with
87  [ Some entry ⇒
88    match entry with
89    [ register_ptr r1 r2 ⇒ (l @ [ r1; r2 ])
90    | register_int r ⇒ (l @ [ r ])
91    ]
92  | None       ⇒ [ ] (* dpm: should this be none? *)
93  ].
94
95definition filter_and_to_list_local_env ≝
96  λlenv.
97  λregisters.
98    foldl ? ? (filter_and_to_list_local_env_internal lenv) [ ] registers.
99
100definition list_of_register_type ≝
101  λrt.
102  match rt with
103  [ register_ptr r1 r2 ⇒ [ r1; r2 ]
104  | register_int r ⇒ [ r ]
105  ].
106
107definition find_and_list ≝
108  λr.
109  λlenv.
110  match assoc_list_lookup ? ? r (eq_identifier RegisterTag) lenv with
111  [ None      ⇒ [ ] (* dpm: should this be none? *)
112  | Some lkup ⇒ list_of_register_type lkup
113  ].
114
115definition find_and_list_args ≝
116  λargs.
117  λlenv.
118    map ? ? (λr. find_and_list r lenv) args.
119
120definition find_and_addr ≝
121  λr.
122  λlenv.
123  match find_and_list r lenv with
124  [ cons hd tl ⇒
125    match tl with
126    [ cons hd' tl' ⇒ Some ? 〈hd, hd'〉
127    | nil          ⇒ None ?
128    ]
129  | nil ⇒ None ? (* dpm: was assert false *)
130  ].
131
132definition rtl_args ≝
133  λregs_list.
134  λlenv.
135    flatten ? (find_and_list_args regs_list lenv).
136
137definition change_label ≝
138  λlbl.
139  λstmt.
140  match stmt with
141  [ rtl_st_skip _ ⇒ rtl_st_skip lbl
142  | rtl_st_cost cost_lbl _ ⇒ rtl_st_cost cost_lbl lbl
143  | rtl_st_addr r1 r2 id _ ⇒ rtl_st_addr r1 r2 id lbl
144  | rtl_st_stack_addr r1 r2 _ ⇒ rtl_st_stack_addr r1 r2 lbl
145  | rtl_st_int r i _ ⇒ rtl_st_int r i lbl
146  | rtl_st_move r1 r2 _ ⇒ rtl_st_move r1 r2 lbl
147  | rtl_st_opaccs opaccs d s1 s2 _ ⇒ rtl_st_opaccs opaccs d s1 s2 lbl
148  | rtl_st_op1 op1 d s _ ⇒ rtl_st_op1 op1 d s lbl
149  | rtl_st_op2 op2 d s1 s2 _ ⇒ rtl_st_op2 op2 d s1 s2 lbl
150  | rtl_st_clear_carry _ ⇒ rtl_st_clear_carry lbl
151  | rtl_st_load d a1 a2 _ ⇒ rtl_st_load d a1 a2 lbl
152  | rtl_st_store a1 a2 s _ ⇒ rtl_st_store a1 a2 s lbl
153  | rtl_st_call_id f a r _ ⇒ rtl_st_call_id f a r lbl
154  | rtl_st_call_ptr f1 f2 a r _ ⇒ rtl_st_call_ptr f1 f2 a r lbl
155  | rtl_st_tailcall_id f a ⇒ rtl_st_tailcall_id f a
156  | rtl_st_tailcall_ptr f1 f2 a ⇒ rtl_st_tailcall_ptr f1 f2 a
157  | rtl_st_cond_acc r l1 l2 ⇒ rtl_st_cond_acc r l1 l2
158  | rtl_st_return r ⇒ rtl_st_return r
159  | _ ⇒ ?
160  ].
161
162let rec adds_graph (stmt_list: ?) (start_lbl: label) (dest_lbl: label) def ≝
163  match stmt_list with
164  [ nil ⇒ def
165  | cons hd tl ⇒
166    match tl with
167    [ nil ⇒ add_graph start_lbl (change_lbl dest_lbl stmt) def
168    | cons hd' tl' ⇒ ?
169    ]
170  ].
171
172let rec adds_graph stmt_list start_lbl dest_lbl def = match stmt_list with
173  | [] -> def
174  | [stmt] ->
175    add_graph start_lbl (change_label dest_lbl stmt) def
176  | stmt :: stmt_list ->
177    let tmp_lbl = fresh_label def in
178    let stmt = change_label tmp_lbl stmt in
179    let def = add_graph start_lbl stmt def in
180    adds_graph stmt_list tmp_lbl dest_lbl def
Note: See TracBrowser for help on using the repository browser.