Changeset 2783 for src/RTL


Ignore:
Timestamp:
Mar 6, 2013, 12:09:52 PM (7 years ago)
Author:
piccolo
Message:

modified joint_closed_internal_function definition (added condition on pseudo-registers)
added new record for parameters
modified state definition with option for framesT

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTL/RTL.ma

    r2681 r2783  
    2222    (* paramsT ≝ *) (list register).
    2323
    24 definition RTL ≝ mk_graph_params RTL_uns.
     24definition RTL_functs ≝ mk_get_pseudo_reg_functs RTL_uns
     25(* acc_a_regs *) (λr.[r])
     26(* acc_b_regs *) (λr.[r])
     27(* acc_a_args *) (λa. match a with [Reg r ⇒ [r] |Imm _ ⇒ [ ]])
     28(* acc_b_args *) (λa. match a with [Reg r ⇒ [r] |Imm _ ⇒ [ ]])
     29(* dpl_regs *) (λr.[r])
     30(* dph_regs *) (λr.[r])
     31(* dpl_args *) (λa. match a with [Reg r ⇒ [r] |Imm _ ⇒ [ ]])
     32(* dph_args *) (λa. match a with [Reg r ⇒ [r] |Imm _ ⇒ [ ]])
     33(* snd_args *) (λa. match a with [Reg r ⇒ [r] |Imm _ ⇒ [ ]])
     34(* pair_move_regs *) (λx.[\fst x] @ (match \snd x with [Reg r ⇒ [r] |Imm _ ⇒ [ ]]))
     35(* f_call_args *) (λl.foldl ?? (λl1.λa.l1@(match a with [Reg r ⇒ [r] |Imm _ ⇒ [ ]])) [ ] l)
     36(* f_call_dest *) (λx.x)
     37(* ext_seq_regs *) (λext.match ext with [rtl_stack_address r1 r2 ⇒ [r1;r2]])
     38(* params_regs *) (λx.x).
     39
     40definition RTL ≝ mk_graph_params (mk_uns_params RTL_uns RTL_functs).
    2541definition rtl_program ≝ joint_program RTL.
    2642
Note: See TracChangeset for help on using the changeset viewer.