Changeset 1411 for src/joint


Ignore:
Timestamp:
Oct 19, 2011, 1:39:54 PM (8 years ago)
Author:
sacerdot
Message:
  1. sem_params2 splitted into sem_params1 + sem_params2 to take out the semantics of the extended statements
  2. pointer call semantics given in RTL/semantics
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/semantics.ma

    r1408 r1411  
    5858definition genv ≝ λglobals.λp:params globals. (genv_t Genv) (joint_function globals p).
    5959
    60 record more_sem_params2 (globals: list ident) (p: params globals) : Type[1] ≝
    61  { more_sparams1 :> more_sem_params p
    62 
    63  ; fetch_statement: genv … p → state (mk_sem_params … more_sparams1) → res (joint_statement (mk_sem_params … more_sparams1) globals)
    64 
    65  ; fetch_ra: state (mk_sem_params … more_sparams1) → res ((state (mk_sem_params … more_sparams1)) × address)
    66  ; result_regs: genv globals p → state (mk_sem_params … more_sparams1) → res (list (generic_reg p))
    67 
    68  ; init_locals : localsT p → regsT … more_sparams1 → regsT … more_sparams1
     60record more_sem_params1 (globals: list ident) (p: params globals) : Type[1] ≝
     61 { more_sparams :> more_sem_params p
     62
     63 ; fetch_statement: genv … p → state (mk_sem_params … more_sparams) → res (joint_statement (mk_sem_params … more_sparams) globals)
     64
     65 ; fetch_ra: state (mk_sem_params … more_sparams) → res ((state (mk_sem_params … more_sparams)) × address)
     66 ; result_regs: genv globals p → state (mk_sem_params … more_sparams) → res (list (generic_reg p))
     67
     68 ; init_locals : localsT p → regsT … more_sparams → regsT … more_sparams
    6969   (*CSC: save_frame returns a res only because we can call a function with the wrong number and
    7070     type of arguments. To be fixed using a dependent type *)
    71  ; save_frame: address → nat → paramsT … p → call_args p → call_dest p → state (mk_sem_params … more_sparams1) → res (state (mk_sem_params … more_sparams1))
    72  ; pop_frame: genv globals p → state (mk_sem_params … more_sparams1) → res ((state (mk_sem_params … more_sparams1)))
    73 
    74  ; fetch_external_args: external_function → state (mk_sem_params … more_sparams1) → res (list val)
    75  ; set_result: list val → state (mk_sem_params … more_sparams1) → res (state (mk_sem_params … more_sparams1))
    76 
    77  ; exec_extended: genv globals p → extend_statements (mk_sem_params … more_sparams1) → succ p → state (mk_sem_params … more_sparams1) → IO io_out io_in (trace × (state (mk_sem_params … more_sparams1)))
     71 ; save_frame: address → nat → paramsT … p → call_args p → call_dest p → state (mk_sem_params … more_sparams) → res (state (mk_sem_params … more_sparams))
     72 ; pop_frame: genv globals p → state (mk_sem_params … more_sparams) → res ((state (mk_sem_params … more_sparams)))
     73
     74 ; fetch_external_args: external_function → state (mk_sem_params … more_sparams) → res (list val)
     75 ; set_result: list val → state (mk_sem_params … more_sparams) → res (state (mk_sem_params … more_sparams))
     76 }.
     77
     78record sem_params1 (globals: list ident): Type[1] ≝
     79 { p1:> params globals
     80 ; more_sparams1:> more_sem_params1 globals p1
     81 }.
     82
     83record more_sem_params2 (globals: list ident) (p: params globals) : Type[1] ≝
     84 { more_sparams_1 :> more_sem_params1 … p
     85 ; exec_extended: genv globals p → extend_statements (mk_sem_params … more_sparams_1) → succ p → state (mk_sem_params … more_sparams_1) → IO io_out io_in (trace × (state (mk_sem_params … more_sparams_1)))
    7886 }.
    7987
     
    8391 }.
    8492
    85 definition sem_params_of_sem_params2 ≝ λglobals. λsp2: sem_params2 globals. mk_sem_params sp2 sp2.
    86 coercion sem_params_of_sem_params2 : ∀globals. ∀_x:sem_params2 globals. sem_params
    87  ≝ sem_params_of_sem_params2 on _x: sem_params2 ? to sem_params.
     93definition sem_params_of_sem_params1 ≝ λglobals. λsp1: sem_params1 globals. mk_sem_params sp1 sp1.
     94coercion sem_params_of_sem_params1 : ∀globals. ∀_x:sem_params1 globals. sem_params
     95 ≝ sem_params_of_sem_params1 on _x: sem_params1 ? to sem_params.
     96
     97definition sem_params1_of_sem_params2 ≝ λglobals. λsp2: sem_params2 globals. mk_sem_params1 … sp2 sp2.
     98coercion sem_params1_of_sem_params2 : ∀globals. ∀_x:sem_params2 globals. sem_params1 globals
     99 ≝ sem_params1_of_sem_params2 on _x: sem_params2 ? to sem_params1 ?.
    88100
    89101definition address_of_label: sem_params → label → address ≝
     
    196208
    197209definition eval_call_block:
    198  ∀globals.∀p:sem_params2 globals. genv globals p → state p →
     210 ∀globals.∀p:sem_params1 globals. genv globals p → state p →
    199211  block → call_args p → call_dest p → address → IO io_out io_in (trace×(state p)) ≝
    200212 λglobals,p,ge,st,b,args,dest,ra.
     
    220232
    221233definition eval_call_id:
    222  ∀globals.∀p:sem_params2 globals. genv globals p → state p →
     234 ∀globals.∀p:sem_params1 globals. genv globals p → state p →
    223235  ident → call_args p → call_dest p → address → IO io_out io_in (trace×(state p)) ≝
    224236 λglobals,p,ge,st,id,args,dest,ra.
     
    330342      | CALL_ID id args dest ⇒
    331343        ! ra ← succ_pc … (more_sem_pars p) l (pc … st) ;         
    332           eval_call_id … ge st id args dest ra ]
     344          eval_call_id … p ge st id args dest ra ]
    333345    | RETURN ⇒
    334346      ! 〈st,ra〉 ← fetch_ra … st;
     
    389401  let st0 ≝ mk_state … (empty_framesT …) dummy_pc sp BVfalse (empty_regsT …) m in
    390402  let trace_state ≝
    391    eval_call_id … ge st0 main (call_args_for_main … (sparams2 …))
    392     (call_dest_for_main … (sparams2 …)) (exit sem_globals) in
     403   eval_call_id … (mk_sem_params1 … (sparams …)) ge st0 main (call_args_for_main … (sparams …))
     404    (call_dest_for_main … (sparams …)) (exit sem_globals) in
    393405  match trace_state with
    394406  [ Value tr_st ⇒ OK … (\snd tr_st) (* E0 trace thrown away *)
Note: See TracChangeset for help on using the changeset viewer.