Changeset 1411


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
Location:
src
Files:
4 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/semantics.ma

    r1408 r1411  
    117117definition ertl_more_sem_params2: ∀globals. more_sem_params2 … (ertl_params globals) ≝
    118118 λglobals.
    119   mk_more_sem_params2 … ertl_more_sem_params
    120    (graph_fetch_statement …) (load_ra …) (ertl_result_regs …)
    121    ertl_init_locals ertl_save_frame (ertl_pop_frame …)
    122    ertl_fetch_external_args ertl_set_result (ertl_exec_extended …).
     119  mk_more_sem_params2 …
     120   (mk_more_sem_params1 … ertl_more_sem_params
     121    (graph_fetch_statement …) (load_ra …) (ertl_result_regs …)
     122    ertl_init_locals ertl_save_frame (ertl_pop_frame …)
     123    ertl_fetch_external_args ertl_set_result)
     124   (ertl_exec_extended …).
    123125
    124126definition ertl_fullexec ≝
  • src/LIN/joint_LTL_LIN_semantics.ma

    r1408 r1411  
    5555 ∀globals. more_sem_params2 … (mk_params globals succT ltl_lin_params1 (codeT globals) (lookup globals)) ≝
    5656 λsuccT,succ,pointer_of_label,codeT,lookup,fetch,globals.
    57   mk_more_sem_params2 … (ltl_lin_more_sem_params … succ pointer_of_label)
    58    (fetch globals) (load_ra …) (ltl_lin_result_regs …)
    59    ltl_lin_init_locals (ltl_lin_save_frame …) (ltl_lin_pop_frame …)
    60    (ltl_lin_fetch_external_args …) (ltl_lin_set_result …) (ltl_lin_exec_extended …).
     57  mk_more_sem_params2 …
     58   (mk_more_sem_params1 … (ltl_lin_more_sem_params … succ pointer_of_label)
     59    (fetch globals) (load_ra …) (ltl_lin_result_regs …)
     60    ltl_lin_init_locals (ltl_lin_save_frame …) (ltl_lin_pop_frame …)
     61    (ltl_lin_fetch_external_args …) (ltl_lin_set_result …)) (ltl_lin_exec_extended …).
    6162
    6263definition ltl_lin_fullexec ≝
  • src/RTL/semantics.ma

    r1408 r1411  
    9292axiom rtl_set_result: list val → state rtl_sem_params → res (state rtl_sem_params).
    9393
     94definition rtl_more_sem_params1: ∀globals. more_sem_params1 … (rtl_params globals) ≝
     95 λglobals.
     96  mk_more_sem_params1 … rtl_more_sem_params
     97   (graph_fetch_statement …) rtl_fetch_ra (rtl_result_regs …)
     98   rtl_init_locals rtl_save_frame (rtl_pop_frame …)
     99   rtl_fetch_external_args rtl_set_result.
     100
     101definition block_of_register_pair: register → register → state rtl_sem_params → res block ≝
     102 λr1,r2,st.
     103 do v1 ← greg_retrieve rtl_sem_params st r1 ;
     104 do v2 ← greg_retrieve rtl_sem_params st r2 ;
     105 do ptr ← pointer_of_address 〈v1,v2〉 ;
     106 OK … (pblock ptr). 
     107
    94108definition rtl_exec_extended:
    95109 ∀globals. genv globals (rtl_params globals) →
     
    104118      ! st ← greg_store rtl_sem_params dreg2 dph st ;
    105119       ret ? 〈E0, goto … l st〉
    106    | rtl_st_ext_call_ptr _ _ _ _ ⇒ ?
     120   | rtl_st_ext_call_ptr r1 r2 args dest ⇒
     121      ! b ← block_of_register_pair r1 r2 st ;
     122      ! ra ← succ_pc … (rtl_more_sem_params1 globals) l (pc … st) ;
     123      eval_call_block … (mk_sem_params1 … (rtl_more_sem_params1 globals))
     124       ge st b args dest ra
    107125   | rtl_st_ext_tailcall_id id regs ⇒ ?
    108    | rtl_st_ext_tailcall_ptr _ _ _ ⇒ ?
     126   | rtl_st_ext_tailcall_ptr r1 r2 args ⇒
     127      ! b ← block_of_register_pair r1 r2 st ;
     128      ?
    109129   ].
    110 [1,2,3: cases not_implemented ] (*CSC: tailcalls and pointer calls not implemented ATM *)
     130[1,2: cases not_implemented ] (*CSC: tailcall semantics not implemented ATM *)
    111131qed.
    112132
    113133definition rtl_more_sem_params2: ∀globals. more_sem_params2 … (rtl_params globals) ≝
    114  λglobals.
    115   mk_more_sem_params2 … rtl_more_sem_params
    116    (graph_fetch_statement …) rtl_fetch_ra (rtl_result_regs …)
    117    rtl_init_locals rtl_save_frame (rtl_pop_frame …)
    118    rtl_fetch_external_args rtl_set_result (rtl_exec_extended …).
     134 λglobals. mk_more_sem_params2 … (rtl_more_sem_params1 globals) (rtl_exec_extended …).
    119135
    120136definition rtl_fullexec ≝
  • 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.