Changeset 1082 for src/ERTL/Liveness.ma


Ignore:
Timestamp:
Jul 20, 2011, 5:17:38 PM (9 years ago)
Author:
mulligan
Message:

work from today on ertl -> ltl pass

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/Liveness.ma

    r756 r1082  
    11include "ERTL/ERTL.ma".
    2 
    3 definition 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 
    34 definition set_of_list ≝
    35   λn: nat.
    36   λl: list (BitVector n).
    37     foldr ? ? (set_insert ?) (set_empty ?) l.
    38    
    39 definition dptr ≝
    40   set_insert ? (word_of_register RegisterDPL) (set_singleton ? (word_of_register RegisterDPH)).
Note: See TracChangeset for help on using the changeset viewer.