source: src/ERTL/uses.ma @ 1243

include "ERTL/ERTL.ma".

include "utilities/adt/table_adt.ma".

definition lookup: table register nat → register → nat ≝
  λuses.
  λr: register.
  match tbl_find … r uses with
  [ None      ⇒ 0
  | Some uses ⇒ uses
  ].

definition count: register → table register nat → ? ≝
  λr: register.
  λuses: table register nat.
    tbl_insert … r ((lookup uses r) + 1) uses.
  
definition examine_statement ≝
  λglobals: list ident.
  λstmt: ertl_statement globals.
  λuses: table register nat.
  match stmt with
  [ joint_st_sequential seq l ⇒
    match seq with
    [ joint_instr_comment c ⇒ uses
    | joint_instr_cost_label c ⇒ uses
    | joint_instr_move pair_regs ⇒
      let reg1 ≝ \fst pair_regs in
      let reg2 ≝ \snd pair_regs in
      match reg1 with
      [ pseudo p ⇒ count p uses
      | hardware h1 ⇒
        match reg2 with
        [ pseudo p ⇒ count p uses
        | hardware h2 ⇒ uses
        ]
      ]
    | joint_instr_clear_carry ⇒ uses
    | joint_instr_set_carry ⇒ uses
    | joint_instr_call_id _ _ ⇒ uses
    | joint_instr_pop r ⇒ count r uses
    | joint_instr_push r ⇒ count r uses
    | joint_instr_int r _ ⇒ count r uses
    | joint_instr_address lbl prf r1 r2 ⇒ count r1 (count r2 uses)
    | joint_instr_opaccs opaccs acc_a acc_b ⇒ count acc_a (count acc_b uses)
    | joint_instr_op1 op1 r1 ⇒ count r1 uses
    | joint_instr_op2 op2 r1 r2 ⇒ count r1 (count r2 uses)
    | joint_instr_load destr r1 r2 ⇒ count r1 (count r2 (count destr uses))
    | joint_instr_store srcr r1 r2 ⇒ count r1 (count r2 (count srcr uses))
    | joint_instr_cond srcr l2 ⇒ count srcr uses
    ]
  | joint_st_return ⇒ uses
  | joint_st_goto l ⇒ uses
  | joint_st_extension ext ⇒
    match ext with
    [ ertl_st_ext_new_frame l ⇒ uses
    | ertl_st_ext_del_frame l ⇒ uses
    | ertl_st_ext_frame_size r l ⇒ count r uses
    ]
  ].

axiom recover_graph: ∀globals. ertl_internal_function globals → table label (ertl_statement globals).

definition examine_internal ≝
  λglobals: list ident.
  λint_fun: ertl_internal_function globals.
  let graph ≝ recover_graph globals int_fun in
  let uses ≝ tbl_fold ?? (examine_statement globals) (joint_if_graph … int_fun) (tbl_empty …) in
      lookup uses.