Changeset 2783 for src/joint


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

Location:
src/joint
Files:
1 added
4 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 
  • src/joint/Traces.ma

    r2757 r2783  
    8282  (* use exit_pc as ra and call_dest_for_main as dest *)
    8383  let st0' ≝ mk_state_pc … (set_sp … spp st0) exit_pc exit_pc in
    84   ! st0_no_pc ← save_frame ?? sem_globals ID (call_dest_for_main … pars) (prog_main … p) st0' ;
     84  ! st0_no_pc ← save_frame ?? sem_globals ID (call_dest_for_main … pars) st0' ;
    8585  let st0'' ≝ set_no_pc … st0_no_pc st0' in
    8686  ! bl ← block_of_call … ge (inl … main) st0'';
  • src/joint/joint_semantics.ma

    r2688 r2783  
    5454
    5555record state (semp: sem_state_params): Type[0] ≝
    56  { st_frms: framesT semp
     56 { st_frms: option(framesT semp)
    5757 ; istack : internal_stack
    5858 ; carry: bebit
     
    103103
    104104definition set_frms: ∀p:sem_state_params. framesT p → state p → state p ≝
    105  λp,frms,st. mk_state … frms (istack … st) (carry … st) (regs … st) (m … st).
     105 λp,frms,st. mk_state … (Some ? (frms)) (istack … st) (carry … st) (regs … st) (m … st).
    106106
    107107(*
     
    184184  (* Paolo: save_frame separated from call_setup to factorize tailcall code *)
    185185  (* ; allocate_locals_ : localsT uns_pars → regsT st_pars → regsT st_pars *)
    186   ; save_frame: call_kind → call_dest uns_pars → ident → state_pc st_pars → res (state st_pars)
     186  ; save_frame: call_kind → call_dest uns_pars → state_pc st_pars → res (state st_pars)
    187187   (*CSC: setup_call returns a res only because we can call a function with the wrong number and
    188188     type of arguments. To be fixed using a dependent type *)
     
    528528match fd with
    529529[ Internal ifd ⇒
    530   let ident ≝ ? in
    531   ! st' ← save_frame … (kind_of_call … f) dest ident st ;
     530  ! st' ← save_frame … (kind_of_call … f) dest st ;
    532531  ! st'' ← eval_internal_call p globals ge i ifd args st' ;
    533532  let pc ≝ pc_of_point p bl (joint_if_entry … ifd) in
     
    536535  ! st' ← eval_external_call … efd args dest st ;
    537536  return mk_state_pc … st' (succ_pc p (pc … st) nxt) (last_pop … st)
    538 ]. cases daemon qed. (*TODO*)
     537].
    539538
    540539definition eval_statement_no_pc :
  • src/joint/semanticsUtils.ma

    r2708 r2783  
    5050}.
    5151
    52 definition reg_store ≝ λreg,v,locals. update RegisterTag beval locals reg v.
     52definition reg_store ≝ λreg,v,locals. OK ? (add RegisterTag beval locals reg v).
    5353
    5454definition reg_retrieve : register_env beval → register → res beval ≝
     
    6969
    7070record sem_graph_params : Type[1] ≝
    71 { sgp_pars : unserialized_params
     71{ sgp_pars : uns_params
    7272; sgp_sup : ∀F.sem_unserialized_params sgp_pars F
    7373}.
     74
    7475
    7576definition sem_graph_params_to_graph_params :
     
    107108
    108109record sem_lin_params : Type[1] ≝
    109 { slp_pars : unserialized_params
     110{ slp_pars : uns_params
    110111; slp_sup : ∀F.sem_unserialized_params slp_pars F
    111112}.
Note: See TracChangeset for help on using the changeset viewer.