Changeset 1641 for src/joint


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/joint
Files:
1 added
1 edited

Legend:

Unmodified
Added
Removed
  • 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.