source: src/ERTL/liveness.ma @ 1090

include "ASM/Util.ma".
include "ERTL/ERTL.ma".

definition list_set_union ≝
  λA: Type[0].
  λeq_a: A → A → bool.
  λl: list A.
  λr: list A.
    nub_by A eq_a (l @ r).

definition list_set_add ≝
  λA: Type[0].
  λeq_a: A → A → bool.
  λa: A.
  λs: list A.
    nub_by A eq_a (a :: s).

definition list_set_diff ≝
  λA: Type[0].
  λeq_a: A → A → bool.
  λl: list A.
  λr: list A.
    filter A (λx. member A eq_a x r) l.

definition list_set_equal ≝
  λA: Type[0].
  λeq_a: A → A → bool.
  λl: list A.
  λr: list A.
    foldr ? ? andb true (map ? ? (λx. member A eq_a x r) l).

definition statement_successors ≝
  λs: ertl_statement.
  match s with
  [ ertl_st_return _ ⇒ [ ]
  | ertl_st_skip l ⇒ [ l ]
  | ertl_st_comment c l ⇒ [ l ]
  | ertl_st_cost c l ⇒ [ l ]
  | ertl_st_set_hdw _ _ l ⇒ [ l ]
  | ertl_st_get_hdw _ _ l ⇒ [ l ]
  | ertl_st_hdw_to_hdw _ _ l ⇒ [ l ]
  | ertl_st_new_frame l ⇒ [ l ]
  | ertl_st_del_frame l ⇒ [ l ]
  | ertl_st_frame_size _ l ⇒ [ l ]
  | ertl_st_push _ l ⇒ [ l ]
  | ertl_st_pop _ l ⇒ [ l ]
  | ertl_st_addr_h _ _ l ⇒ [ l ]
  | ertl_st_addr_l _ _ l ⇒ [ l ]
  | ertl_st_int _ _ l ⇒ [ l ]
  | ertl_st_move _ _ l ⇒ [ l ]
  | ertl_st_opaccs_a _ _ _ _ l ⇒ [ l ]
  | ertl_st_opaccs_b _ _ _ _ l ⇒ [ l ]
  | ertl_st_op1 _ _ _ l ⇒ [ l ]
  | ertl_st_op2 _ _ _ _ l ⇒ [ l ]
  | ertl_st_clear_carry l ⇒ [ l ]
  | ertl_st_set_carry l ⇒ [ l ]
  | ertl_st_load _ _ _ l ⇒ [ l ]
  | ertl_st_store _ _ _ l ⇒ [ l ]
  | ertl_st_call_id _ _ l ⇒ [ l ]
  | ertl_st_cond _ l1 l2 ⇒
      list_set_add ? (eq_identifier ?) l1 [ l2 ]
  ].

definition register_lattice ≝ (list register) × (list Register).
definition lattice_property ≝ register_lattice.
definition lattice_bottom: register_lattice ≝ 〈[ ], [ ]〉.
definition lattice_psingleton: register → register_lattice ≝
  λr.
    〈[ r ], [ ]〉.
definition lattice_hsingleton: Register → register_lattice ≝
  λr.
    〈[ ], [ r ]〉.

definition lattice_join: register_lattice → register_lattice → register_lattice ≝
  λleft.
  λright.
  let 〈lp, lh〉 ≝ left in
  let 〈rp, rh〉 ≝ right in
    〈list_set_union ? (eq_identifier ?) lp rp, list_set_union ? eq_Register lh rh〉.

definition lattice_diff: register_lattice → register_lattice → register_lattice ≝
  λleft.
  λright.
  let 〈lp, lh〉 ≝ left in
  let 〈rp, rh〉 ≝ right in
    〈list_set_diff ? (eq_identifier ?) lp rp, list_set_diff ? eq_Register lh rh〉.

definition lattice_equal: register_lattice → register_lattice → bool ≝
  λleft.
  λright.
  let 〈lp, lh〉 ≝ left in
  let 〈rp, rh〉 ≝ right in
    andb (list_set_equal ? (eq_identifier ?) lp rp) (list_set_equal ? eq_Register lh rh).

definition lattice_is_maximal: register_lattice → bool ≝ λl. false.

definition defined: ertl_statement → register_lattice ≝
  λs.
  match s with
  [ ertl_st_skip _ ⇒ lattice_bottom
  | ertl_st_comment _ _ ⇒ lattice_bottom
  | ertl_st_cost _ _ ⇒ lattice_bottom
  | ertl_st_push _ _⇒ lattice_bottom
  | ertl_st_store _ _ _ _ ⇒ lattice_bottom
  | ertl_st_cond _ _ _ ⇒ lattice_bottom
  | ertl_st_return _ ⇒ lattice_bottom
  | ertl_st_clear_carry _ ⇒ 〈[ ], [ RegisterCarry ]〉
  | ertl_st_set_carry _ ⇒ 〈[ ], [ RegisterCarry ]〉
  | _ ⇒ ?
  ].

let defined (stmt : statement) : L.t =
  match stmt with
  | St_clear_carry _
  | St_set_carry _ ->
    Register.Set.empty, I8051.RegisterSet.singleton I8051.carry
  | St_op2 (I8051.Add, r, _, _, _)
  | St_op2 (I8051.Addc, r, _, _, _)
  | St_op2 (I8051.Sub, r, _, _, _) ->
    L.join (L.hsingleton I8051.carry) (L.psingleton r)
  | St_op1 (I8051.Inc, r, _, _)
  | St_get_hdw (r, _, _)
  | St_framesize (r, _)
  | St_pop (r, _)
  | St_int (r, _, _)
  | St_addrH (r, _, _)
  | St_addrL (r, _, _)
  | St_move (r, _, _)
  | St_opaccsA (_, r, _, _, _)
  | St_opaccsB (_, r, _, _, _)
  | St_op1 (_, r, _, _)
  | St_op2 (_, r, _, _, _)
  | St_load (r, _, _, _) ->
    L.psingleton r
  | St_set_hdw (r, _, _)
  | St_hdw_to_hdw (r, _, _) ->
    L.hsingleton r
  | St_call_id _ ->
      (* Potentially destroys all caller-save hardware registers. *)
    Register.Set.empty, I8051.caller_saved
  | St_newframe _
  | St_delframe _ ->
    L.join (L.hsingleton I8051.spl) (L.hsingleton I8051.sph)