Changeset 1641


Ignore:
Timestamp:
Jan 11, 2012, 8:03:53 PM (8 years ago)
Author:
tranquil
Message:
  • semanticsUtils_paolo.ma contains code to generate both graph and linear semantics parameters (partially migrated from LIN/semantics.ma)
  • fetch_function is now common to both graph and linear
  • started porting RTL's semantics
Location:
src
Files:
2 added
2 edited

Legend:

Unmodified
Added
Removed
  • src/RTL/RTL_paolo.ma

    r1640 r1641  
    2525  | rtl_st_ext_tailcall_ptr: register → register → list rtl_argument → rtl_statement_extension.
    2626
    27 definition rtl_params ≝ mk_graph_params (mk_unserialized_params
     27definition rtl_uns_params ≝ mk_unserialized_params
    2828  (mk_inst_params
    2929    (* acc_a_reg ≝ *) register
     
    4545      (* resultT ≝ *) (list register)
    4646      (* paramsT ≝ *) (list register))
    47       (* localsT ≝ *) (list register))).
     47      (* localsT ≝ *) (list register)).
     48
     49definition rtl_params ≝ mk_graph_params rtl_uns_params.
     50definition lin_rtl_params ≝ mk_lin_params rtl_uns_params.
    4851
    4952interpretation "move" 'mov r a = (MOVE ? ? (mk_Prod ?? r a)).
     
    8992
    9093
    91 definition rtl_instruction ≝ joint_instruction rtl_params.
    92 (* Paolo: can't understand why coercions do not compose implicitly here *)
    93 definition rtl_statement ≝ joint_statement (rtl_params : params).
     94definition rtl_instruction ≝ joint_instruction rtl_uns_params.
     95
     96definition rtl_statement ≝ joint_statement rtl_params.
    9497
    9598definition rtl_internal_function ≝
  • src/joint/semantics_paolo.ma

    r1640 r1641  
    1414
    1515record sem_state_params : Type[1] ≝
    16  { regsT : Type[0]
    17  ; framesT: Type[0]
     16 { framesT: Type[0]
    1817 ; empty_framesT: framesT
     18 ; regsT : Type[0]
    1919 ; empty_regsT: address → regsT (* Stack pointer *)
    2020 }.
     
    5151 λp,frms,st. mk_state … frms (pc … st) (sp … st) (isp … st) (carry … st) (regs … st) (m … st).
    5252
    53 
    54 
     53axiom BadProgramCounter : String.
     54(* this can replace graph_fetch function and lin_fetch_function *)
     55definition fetch_function:
     56 ∀pars : params.
     57 ∀globals.
     58  genv globals pars →
     59  pointer →
     60  res (joint_internal_function … pars) ≝
     61 λpars,globals,ge,p.
     62  let b ≝ pblock p in
     63  do def ← opt_to_res ? [MSG BadProgramCounter] (find_funct_ptr … ge b) ;
     64  match def with
     65  [ Internal def' ⇒ OK … def'
     66  | External _ ⇒ Error … [MSG BadProgramCounter]].
     67 
    5568record more_sem_unserialized_params (uns_pars : unserialized_params) : Type[1] ≝
    5669  { st_pars :> sem_state_params
     
    98111  λX,f,up,p,x,v,st.! r ← f ? p x v (regs … st) ; return (set_regs … r st).
    99112
    100 (* all res are cast to IO to aid unification later *)
    101113definition acca_retrieve ≝ helper_def_retrieve ? acca_retrieve_.
    102114definition acca_store ≝ helper_def_store ? acca_store_.
     
    117129    return (set_regs ? r st).
    118130
    119 record more_sem_params (pp : params) : Type[1] ≝
     131(* parameters that need full params to have type of functions,
     132   but are still independent of serialization *)
     133record more_sem_genv_params (pp : params) : Type[1] ≝
    120134  { msu_pars :> more_sem_unserialized_params pp
    121   ; succ_pc: succ pp → address → res address
    122135  ; read_result: ∀globals.genv globals pp → state msu_pars → res (list beval)
    123136  ; exec_extended: ∀globals.genv globals pp → extend_statements pp →
    124137      state msu_pars → IO io_out io_in ((option label) × trace × (state msu_pars))
    125 
     138  ; pop_frame: ∀globals.genv globals pp → state msu_pars → res (state msu_pars)
     139  }.
     140
     141(* parameters that are defined by serialization *)
     142record more_sem_params (pp : params) : Type[1] ≝
     143  { msg_pars :> more_sem_genv_params pp
     144  ; succ_pc: succ pp → address → res address
    126145  ; pointer_of_label: ∀globals.genv globals pp → pointer → label → res (Σp:pointer. ptype p = Code)
    127 
    128   ; pop_frame: ∀globals.genv globals pp → state msu_pars → res (state msu_pars)
    129  
    130   ; fetch_statement: ∀globals.genv globals pp → state msu_pars → res (joint_statement pp globals)
     146  ; fetch_statement: ∀globals.genv globals pp → state msg_pars → res (joint_statement pp globals)
    131147  }.
    132148
     
    451467 ∀pars:sem_params.fullexec io_out io_in ≝
    452468 λpars.mk_fullexec ??? joint_exec (make_global pars) (make_initial_state pars).
    453  
    454  
Note: See TracChangeset for help on using the changeset viewer.