Changeset 2783 for src/joint/Joint.ma


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/joint/Joint.ma

    r2774 r2783  
    9191 ; paramsT : Type[0]
    9292 }.
     93 
     94record get_pseudo_reg_functs (p : unserialized_params) : Type[0] ≝
     95{ acc_a_regs : acc_a_reg p → list register
     96; acc_b_regs : acc_b_reg p → list register
     97; acc_a_args : acc_a_arg p → list register
     98; acc_b_args : acc_b_arg p → list register
     99; dpl_regs : dpl_reg p → list register
     100; dph_regs : dph_reg p → list register
     101; dpl_args : dpl_arg p → list register
     102; dph_args : dph_arg p → list register
     103; snd_args : snd_arg p → list register
     104; pair_move_regs : pair_move p → list register
     105; f_call_args : call_args p → list register
     106; f_call_dest : call_dest p → list register
     107; ext_seq_regs : ext_seq p → list register
     108; params_regs : paramsT p → list register
     109}.
     110
     111record uns_params : Type[1] ≝
     112{ u_pars :> unserialized_params
     113; functs : get_pseudo_reg_functs u_pars
     114}.
    93115
    94116inductive joint_seq (p:unserialized_params) (globals: list ident): Type[0] ≝
     
    108130  | STORE: dpl_arg p → dph_arg p → acc_a_arg p → joint_seq p globals
    109131  | extension_seq : ext_seq p → joint_seq p globals.
     132 
     133definition get_used_registers_from_seq : ∀p : unserialized_params.∀globals.
     134get_pseudo_reg_functs p → joint_seq p globals → list register ≝
     135λp,globals,functs,seq.
     136match seq with
     137[ COMMENT _ ⇒ [ ]
     138| MOVE pm ⇒ pair_move_regs … functs pm
     139| POP r ⇒ acc_a_regs … functs r
     140| PUSH r ⇒ acc_a_args … functs r
     141| ADDRESS i prf r1 r2 ⇒ (dpl_regs … functs r1) @ (dph_regs … functs r2)
     142| OPACCS o r1 r2 r3 r4 ⇒ (acc_a_regs … functs r1) @ (acc_b_regs … functs r2)
     143       @ (acc_a_args … functs r3) @ (acc_b_args … functs r4)
     144| OP1 o r1 r2 ⇒ (acc_a_regs … functs r1) @ (acc_a_regs … functs r2)
     145| OP2 o r1 r2 r3 ⇒ (acc_a_regs … functs r1) @ (acc_a_args … functs r2) @
     146         (snd_args … functs r3)
     147| CLEAR_CARRY ⇒ [ ]
     148| SET_CARRY ⇒ [ ]
     149| LOAD r1 r2 r3 ⇒ (acc_a_regs … functs r1) @ (dpl_args … functs r2) @
     150                  (dph_args … functs r3)
     151| STORE r1 r2 r3 ⇒ (dpl_args … functs r1) @ (dph_args … functs r2) @
     152                    (acc_a_args … functs r3)
     153| extension_seq ext ⇒ ext_seq_regs … functs ext
     154].
    110155
    111156definition NOOP ≝ λp,globals.COMMENT p globals EmptyString.
     
    139184  | COND: acc_a_reg p → label → joint_step p globals
    140185  | step_seq : joint_seq p globals → joint_step p globals.
     186 
     187definition get_used_registers_from_step : ∀p : unserialized_params.∀globals.
     188get_pseudo_reg_functs p → joint_step p globals → list register ≝
     189λp,globals,functs,step.
     190match step with
     191[ COST_LABEL c ⇒ [ ]
     192| CALL id args dest ⇒ (f_call_args … functs args) @ (f_call_dest … functs dest)
     193| COND r lbl ⇒  acc_a_regs … functs r
     194| step_seq s ⇒ get_used_registers_from_seq … functs s
     195].
    141196
    142197coercion seq_to_step : ∀p,globals.∀s : joint_seq p globals.joint_step p globals ≝
     
    160215
    161216record stmt_params : Type[1] ≝
    162   { uns_pars :> unserialized_params
     217  { uns_pars :> uns_params
    163218  ; succ : Type[0]
    164219  ; succ_label : succ → option label
     
    257312     | None ⇒ [ ]
    258313     ]) @ stmt_explicit_labels … stmt.
     314     
     315definition stmt_registers : ∀p : stmt_params.∀globals.
     316joint_statement p globals → list register ≝
     317λp,globals,stmt.
     318match stmt with
     319[ sequential c _ ⇒ get_used_registers_from_step … (functs … p) c
     320| final c ⇒
     321   match c with [ TAILCALL _ _ r ⇒ f_call_args … (functs … p) r | _ ⇒ [ ] ]
     322| FCOND _ r _ _ ⇒ acc_a_regs … (functs … p) r
     323].
    259324
    260325definition stmt_forall_labels ≝
    261326  λp, globals.λ P : label → Prop.λs : joint_statement p globals.
    262327  All … P (stmt_labels … s).
     328 
    263329
    264330lemma stmt_forall_labels_explicit : ∀p,globals,P.∀s : joint_statement p globals.
     
    290356
    291357record lin_params : Type[1] ≝
    292   { l_u_pars : unserialized_params }.
     358  { l_u_pars : uns_params }.
    293359 
    294360lemma index_of_label_length : ∀tag,A,lbl,l.occurs_exactly_once ?? lbl l → lt (index_of_label tag A lbl l) (|l|).
     
    361427
    362428record graph_params : Type[1] ≝
    363   { g_u_pars : unserialized_params }.
     429  { g_u_pars : uns_params }.
    364430
    365431(* One common instantiation of params via Graphs of joint_statements
     
    415481  joint_if_exit : Σpt.bool_to_Prop (code_has_point … joint_if_code pt) *)
    416482}.
     483
     484definition regs_in_universe : ∀p,globals.
     485codeT p globals → universe RegisterTag → Prop ≝
     486λp,globals,c,u.∀pt,stmt.stmt_at p globals c pt = return stmt →
     487All ? (λreg.fresh_for_univ … reg u) (stmt_registers … stmt).
    417488
    418489definition code_in_universe : ∀p,globals.
     
    459530; code_is_in_universe :
    460531  code_in_universe … (joint_if_code … def) (joint_if_luniverse … def)
     532; regs_are_in_univers :
     533  regs_in_universe … (joint_if_code … def) (joint_if_runiverse … def)
    461534}.
    462535 
Note: See TracChangeset for help on using the changeset viewer.