source: src/ERTL/Liveness.ma @ 756

Last change on this file since 756 was 756, checked in by mulligan, 10 years ago

Made a start on RTL. Renaming in ERTL and below to move closer to Brian's naming convention and datatypes.

File size: 1.3 KB
Line 
1include "ERTL/ERTL.ma".
2
3definition statement_successors ≝
4  λstmt: ertl_statement.
5  match stmt with
6  [ ertl_st_return _ ⇒ [ ]
7  | ertl_st_skip l ⇒ [ l ]
8  | ertl_st_comment comment l ⇒ [ l ]
9  | ertl_st_cost cost l ⇒ [ l ]
10  | ertl_st_set_hdw r1 r2 l ⇒ [ l ]
11  | ertl_st_get_hdw r1 r2 l ⇒ [ l ]
12  | ertl_st_hdw_to_hdw r1 r2 l ⇒ [ l ]
13  | ertl_st_new_frame l ⇒ [ l ]
14  | ertl_st_del_frame l ⇒ [ l ]
15  | ertl_st_frame_size r l ⇒ [ l ]
16  | ertl_st_push r l ⇒ [ l ]
17  | ertl_st_pop r l ⇒ [ l ]
18  | ertl_st_addr_h r l1 l2 ⇒ [ l2 ]
19  | ertl_st_addr_l r l1 l2 ⇒ [ l2 ]
20  | ertl_st_int r v l ⇒ [ l ]
21  | ertl_st_move r1 r2 l ⇒ [ l ]
22  | ertl_st_opaccs opaccs r1 r2 r3 l ⇒ [ l ]
23  | ertl_st_op2 op2 r1 r2 r3 l ⇒ [ l ]
24  | ertl_st_op1 op1 r1 r2 l ⇒ [ l ]
25  | ertl_st_clear_carry l ⇒ [ l ]
26  | ertl_st_load r1 r2 r3 l ⇒ [ l ]
27  | ertl_st_store r1 r2 r3 l ⇒ [ l ]
28  | ertl_st_call_id id v l ⇒ [ l ]
29  | ertl_st_cond_acc _ l1 l2 ⇒ [ l1 ] @ [ l2 ]
30  ].
31 
32(* dpm: this needs sorting out!  just what exactly is a register? *)
33
34definition set_of_list ≝
35  λn: nat.
36  λl: list (BitVector n).
37    foldr ? ? (set_insert ?) (set_empty ?) l.
38   
39definition dptr ≝
40  set_insert ? (word_of_register RegisterDPL) (set_singleton ? (word_of_register RegisterDPH)).
Note: See TracBrowser for help on using the repository browser.