Ignore:
Timestamp:
Jan 13, 2012, 12:23:30 PM (8 years ago)
Author:
tranquil
Message:
  • some changes in everything
  • separated extensions in sequential and final, to accomodate tailcalls
  • finished RTL's semantics
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/semantics_paolo.ma

    r1641 r1643  
    8686
    8787  ; init_locals : localsT uns_pars → regsT st_pars → regsT st_pars
    88    (*CSC: save_frame returns a res only because we can call a function with the wrong number and
     88  (* Paolo: save_frame separated from call_setup to factorize tailcall code *)
     89  ; save_frame: address → call_dest uns_pars → state st_pars → state st_pars
     90   (*CSC: setup_call returns a res only because we can call a function with the wrong number and
    8991     type of arguments. To be fixed using a dependent type *)
    90   ; save_frame: address → nat → paramsT … uns_pars → call_args uns_pars → call_dest uns_pars →
     92  ; setup_call : nat → paramsT … uns_pars → call_args uns_pars →
    9193      state st_pars → res (state st_pars)
    9294  ; fetch_external_args: external_function → state st_pars →
     
    129131    return (set_regs ? r st).
    130132
     133axiom BadPointer : String.
     134
     135(* this is preamble to all calls (including tail ones). The optional argument in
     136   input tells the function whether it has to save the frame for internal
     137   calls.
     138   the first element of the triple is the label at the start of the function
     139   in case of an internal call, or None in case of an external one.
     140   The actual update of the pc is left to later, as it depends on
     141   serialization and on whether the call is a tail one. *)
     142definition eval_call_block_preamble:
     143 ∀globals.∀p : params.∀p':more_sem_unserialized_params p.
     144  genv globals p → state p' → block → call_args p → option ((call_dest p) × address) →
     145    IO io_out io_in ((option label)×trace×(state p')) ≝
     146 λglobals,p,p',ge,st,b,args,dest_ra.
     147  ! fd ← (opt_to_res ? [MSG BadPointer] (find_funct_ptr ?? ge b) : IO ? io_in ?);
     148    match fd with
     149    [ Internal fn ⇒
     150      let st ≝ match dest_ra with
     151        [ Some p ⇒ let 〈dest, ra〉 ≝ p in save_frame … ra dest st
     152        | None ⇒ st
     153        ] in
     154      ! st ← setup_call … (joint_if_stacksize … fn) (joint_if_params … fn)
     155              args st ;
     156      let regs ≝ init_locals … (joint_if_locals … fn) (regs … st) in
     157      let l' ≝ joint_if_entry … fn in
     158      let st ≝ set_regs p' regs st in
     159      return 〈Some label l', E0, st〉
     160    | External fn ⇒
     161      ! params ← fetch_external_args … p' fn st : IO ???;
     162      ! evargs ← check_eventval_list params (sig_args (ef_sig fn)) : IO ???;
     163      ! evres ← do_io (ef_id fn) evargs (proj_sig_res (ef_sig fn));
     164      (* CSC: XXX bug here; I think I should split it into Byte-long
     165         components; instead I am making a singleton out of it. To be
     166         fixed once we fully implement external functions. *)
     167      let vs ≝ [mk_val ? evres] in
     168      ! st ← set_result … p' vs st : IO ???;
     169      return 〈None ?, Eextcall (ef_id fn) evargs (mk_eventval ? evres), st〉
     170      ].
     171
     172axiom FailedStore: String.
     173
     174definition push: ∀p. state p → beval → res (state p) ≝
     175 λp,st,v.
     176  let isp ≝ isp … st in
     177  do m ← opt_to_res … (msg FailedStore) (bestorev (m … st) isp v);
     178  let isp ≝ shift_pointer … isp [[false;false;false;false;false;false;false;true]] in
     179  OK … (set_m … m (set_sp … isp st)).
     180
     181definition pop: ∀p. state p → res (state p × beval) ≝
     182 λp,st.
     183  let isp ≝ isp ? st in
     184  let isp ≝ neg_shift_pointer ? isp [[false;false;false;false;false;false;false;true]] in
     185  let ist ≝ set_sp … isp st in
     186  do v ← opt_to_res ? (msg FailedStore) (beloadv (m ? st) isp);
     187  OK ? 〈st,v〉.
     188
     189definition save_ra : ∀p. state p → address → res (state p) ≝
     190 λp,st,l.
     191  let 〈addrl,addrh〉 ≝ l in
     192  do st ← push … st addrl;
     193  push … st addrh.
     194
     195definition load_ra : ∀p.state p → res (state p × address) ≝
     196 λp,st.
     197  do 〈st,addrh〉 ← pop … st;
     198  do 〈st,addrl〉 ← pop … st;
     199  OK ? 〈st, 〈addrl,addrh〉〉.
     200
     201
    131202(* parameters that need full params to have type of functions,
    132    but are still independent of serialization *)
     203   but are still independent of serialization
     204   Paolo: the first element returned by exec extended is None if flow is
     205   left to regular sequential one, otherwise a label.
     206   The address input is the address of the next statement, to be provided to
     207   accomodate extensions that make calls. *)
    133208record more_sem_genv_params (pp : params) : Type[1] ≝
    134209  { msu_pars :> more_sem_unserialized_params pp
    135210  ; read_result: ∀globals.genv globals pp → state msu_pars → res (list beval)
    136   ; exec_extended: ∀globals.genv globals pp → extend_statements pp →
    137       state msu_pars → IO io_out io_in ((option label) × trace × (state msu_pars))
     211  ; exec_extended: ∀globals.genv globals pp → ext_instruction pp →
     212      state msu_pars → address → IO io_out io_in ((option label)× trace × (state msu_pars))
     213  ; exec_fin_extended: ∀globals.genv globals pp → ext_fin_instruction pp →
     214      state msu_pars → IO io_out io_in (trace × (state msu_pars))
    138215  ; pop_frame: ∀globals.genv globals pp → state msu_pars → res (state msu_pars)
    139216  }.
     217 
    140218
    141219(* parameters that are defined by serialization *)
     
    165243  OK (state p) (set_pc … newpc st).
    166244
    167 axiom FailedStore: String.
    168 
    169 definition push: ∀p. state p → beval → res (state p) ≝
    170  λp,st,v.
    171   let isp ≝ isp … st in
    172   do m ← opt_to_res … (msg FailedStore) (bestorev (m … st) isp v);
    173   let isp ≝ shift_pointer … isp [[false;false;false;false;false;false;false;true]] in
    174   OK … (set_m … m (set_sp … isp st)).
    175 
    176 definition pop: ∀p. state p → res (state p × beval) ≝
    177  λp,st.
    178   let isp ≝ isp ? st in
    179   let isp ≝ neg_shift_pointer ? isp [[false;false;false;false;false;false;false;true]] in
    180   let ist ≝ set_sp … isp st in
    181   do v ← opt_to_res ? (msg FailedStore) (beloadv (m ? st) isp);
    182   OK ? 〈st,v〉.
    183 
    184 definition save_ra : ∀p. state p → address → res (state p) ≝
    185  λp,st,l.
    186   let 〈addrl,addrh〉 ≝ l in
    187   do st ← push … st addrl;
    188   push … st addrh.
    189 
    190 definition load_ra : ∀p.state p → res (state p × address) ≝
    191  λp,st.
    192   do 〈st,addrh〉 ← pop … st;
    193   do 〈st,addrl〉 ← pop … st;
    194   OK ? 〈st, 〈addrl,addrh〉〉.
    195 
    196 
    197245(*
    198246definition empty_state: ∀p. more_sem_params p → state p ≝
     
    208256axiom FailedLoad : String.
    209257axiom BadFunction : String.
    210 axiom BadPointer : String.
    211258
    212259definition eval_call_block:
     
    214261  block → call_args p → call_dest p → address → IO io_out io_in (trace×(state p)) ≝
    215262 λglobals,p,ge,st,b,args,dest,ra.
    216   ! fd ← (opt_to_res … [MSG BadPointer] (find_funct_ptr ?? ge b) : IO ? io_in ?);
    217     match fd with
    218     [ Internal fn ⇒
    219       ! st ← save_frame … ra (joint_if_stacksize … fn) (joint_if_params … fn) args dest st ;
    220       let regs ≝ init_locals … (joint_if_locals … fn) (regs … st) in
    221       let l' ≝ joint_if_entry … fn in
    222       let st ≝ set_regs p regs st in
    223       let pointer_in_fn ≝ mk_pointer Code (mk_block Code (block_id b)) ? (mk_offset 0) in
    224       ! newpc ← address_of_label … ge pointer_in_fn l' ;
    225       let st ≝ set_pc … newpc st in
    226       return 〈 E0, st〉
    227     | External fn ⇒
    228       ! params ← fetch_external_args … p fn st : IO ???;
    229       ! evargs ← check_eventval_list params (sig_args (ef_sig fn)) : IO ???;
    230       ! evres ← do_io (ef_id fn) evargs (proj_sig_res (ef_sig fn));
    231       (* CSC: XXX bug here; I think I should split it into Byte-long
    232          components; instead I am making a singleton out of it. To be
    233          fixed once we fully implement external functions. *)
    234       let vs ≝ [mk_val ? evres] in
    235       ! st ← set_result … p vs st : IO ???;
    236       let st ≝ set_pc … ra st in
    237       return 〈Eextcall (ef_id fn) evargs (mk_eventval ? evres), st〉
    238       ].
     263 ! 〈next, tr, st〉 ← eval_call_block_preamble … ge st b args (Some ? 〈dest,ra〉) ;
     264 ! new_pc ← match next with
     265  [ Some lbl ⇒
     266    let pointer_in_fn ≝ mk_pointer Code (mk_block Code (block_id b)) ? (mk_offset 0) in
     267    address_of_label globals p ge pointer_in_fn lbl
     268  | None ⇒ return ra
     269  ] ;
     270 let st ≝ set_pc … new_pc st in
     271 return 〈tr, st〉.
    239272% qed.
    240273
     
    273306
    274307(* defining because otherwise typechecker stalls *)
    275 definition eval_call_id_succ:
     308definition eval_sequential :
    276309 ∀globals.∀p:sem_params. genv globals p → state p →
    277   ident → call_args p → call_dest p → succ p → IO io_out io_in (trace×(state p)) ≝
    278  λglobals,p,ge,st,id,args,dest,l.
    279    ! ra ← succ_pc … p l (pc … st) : IO ??? ;
    280    eval_call_id … ge st id args dest ra.
     310  joint_instruction p globals → succ p → IO io_out io_in (trace×(state p)) ≝
     311 λglobals,p,ge,st,seq,l.
     312  match seq with
     313  [ extension c ⇒
     314    ! next_addr ← succ_pc … p l (pc … st) : IO ? ? ? ;
     315    ! 〈next_pc, tr, st〉 ← exec_extended … ge c st next_addr;
     316    ! st ← match next_pc with
     317      [ None ⇒ next … p l st
     318      | Some lbl ⇒ goto … ge lbl st
     319      ] ;
     320    return 〈tr, st〉
     321  | COST_LABEL cl ⇒
     322    ! st ← next … p l st ;
     323    return 〈Echarge cl, st〉
     324  | COMMENT c ⇒
     325    ! st ← next … p l st ;
     326    return 〈E0, st〉
     327  | LOAD dst addrl addrh ⇒
     328    ! vaddrh ← dph_arg_retrieve … st addrh ;
     329    ! vaddrl ← dpl_arg_retrieve … st addrl;
     330    ! vaddr ← pointer_of_address 〈vaddrl,vaddrh〉;
     331    ! v ← opt_to_res … (msg FailedLoad) (beloadv (m … st) vaddr);
     332    ! st ← acca_store p … dst v st ;
     333    ! st ← next … p l st ;
     334    return 〈E0, st〉
     335  | STORE addrl addrh src ⇒
     336    ! vaddrh ← dph_arg_retrieve … st addrh;
     337    ! vaddrl ← dpl_arg_retrieve … st addrl;
     338    ! vaddr ← pointer_of_address 〈vaddrl,vaddrh〉;
     339    ! v ← acca_arg_retrieve … st src;
     340    ! m' ← opt_to_res … (msg FailedStore) (bestorev (m … st) vaddr v);
     341    let st ≝ set_m … m' st in
     342    ! st ← next … p l st ;
     343    return 〈E0, st〉
     344  | COND src ltrue ⇒
     345    ! v ← acca_retrieve … st src;
     346    ! b ← bool_of_beval v;
     347    if b then
     348     ! st ← goto … p ge ltrue st ;
     349     return 〈E0, st〉
     350    else
     351     ! st ← next … p l st ;
     352     return 〈E0, st〉
     353  | ADDRESS ident prf ldest hdest ⇒
     354    eval_address … ge st ident prf ldest hdest l
     355  | OP1 op dacc_a sacc_a ⇒
     356    ! v ← acca_retrieve … st sacc_a;
     357    ! v ← Byte_of_val v;
     358    let v' ≝ BVByte (op1 eval op v) in
     359    ! st ← acca_store … dacc_a v' st;
     360    ! st ← next … l st ;
     361    return 〈E0, st〉
     362  | OP2 op dacc_a sacc_a src ⇒
     363    ! v1 ← acca_arg_retrieve … st sacc_a;
     364    ! v1 ← Byte_of_val v1;
     365    ! v2 ← snd_arg_retrieve … st src;
     366    ! v2 ← Byte_of_val v2;
     367    ! carry ← bool_of_beval (carry … st);
     368      let 〈v',carry〉 ≝ op2 eval carry op v1 v2 in
     369      let v' ≝ BVByte v' in
     370      let carry ≝ beval_of_bool carry in
     371    ! st ← acca_store … dacc_a v' st;
     372      let st ≝ set_carry … carry st in
     373    ! st ← next … l st ;
     374    return 〈E0, st〉
     375  | CLEAR_CARRY ⇒
     376    ! st ← next … l (set_carry … BVfalse st) ;
     377    return 〈E0, st〉
     378  | SET_CARRY ⇒
     379    ! st ← next … l (set_carry … BVtrue st) ;
     380    return 〈E0, st〉
     381  | OPACCS op dacc_a_reg dacc_b_reg sacc_a_reg sacc_b_reg ⇒
     382    ! v1 ← acca_arg_retrieve … st sacc_a_reg;
     383    ! v1 ← Byte_of_val v1;
     384    ! v2 ← accb_arg_retrieve … st sacc_b_reg;
     385    ! v2 ← Byte_of_val v2;
     386    let 〈v1',v2'〉 ≝ opaccs eval op v1 v2 in
     387    let v1' ≝ BVByte v1' in
     388    let v2' ≝ BVByte v2' in
     389    ! st ← acca_store … dacc_a_reg v1' st;
     390    ! st ← accb_store … dacc_b_reg v2' st;
     391    ! st ← next … l st ;
     392    return 〈E0, st〉
     393  | POP dst ⇒
     394    eval_pop … ge st dst l
     395  | PUSH src ⇒
     396    ! v ← acca_arg_retrieve … st src;
     397    ! st ← push … st v;
     398    ! st ← next … l st ;
     399    return 〈E0, st〉
     400  | MOVE dst_src ⇒
     401    ! st ← pair_reg_move … st dst_src ;
     402    ! st ← next … l st ;
     403    return 〈E0, st〉
     404  | CALL_ID id args dest ⇒
     405    ! ra ← succ_pc … p l (pc … st) : IO ??? ;
     406    eval_call_id … ge st id args dest ra
     407  ].
    281408
    282409definition eval_statement : ∀globals: list ident.∀p:sem_params. genv globals p →
     
    289416       return 〈E0, st〉
    290417    | RETURN ⇒
    291       ! p ← fetch_ra … st ;
    292       let 〈st,ra〉 ≝ p in
     418      ! 〈st,ra〉 ← fetch_ra … st ;
    293419      ! st ← pop_frame … ge st;
    294420      return 〈E0,set_pc … ra st〉
    295    | sequential seq l ⇒
    296       match seq with
    297       [ extension c ⇒
    298         ! 〈lbl_opt, tr, st〉 ← exec_extended … ge c st ;
    299         match lbl_opt with
    300         [ Some lbl ⇒
    301           ! st ← goto … ge lbl st ;
    302           return 〈tr, st〉
    303         | None ⇒
    304           ! st ← next … l st ;
    305           return 〈tr, st〉
    306         ]       
    307        | COST_LABEL cl ⇒
    308          ! st ← next … p l st ;
    309          return 〈Echarge cl, st〉
    310       | COMMENT c ⇒
    311          ! st ← next … p l st ;
    312          return 〈E0, st〉
    313       | LOAD dst addrl addrh ⇒
    314         ! vaddrh ← dph_arg_retrieve … st addrh ;
    315         ! vaddrl ← dpl_arg_retrieve … st addrl;
    316         ! vaddr ← pointer_of_address 〈vaddrl,vaddrh〉;
    317         ! v ← opt_to_res … (msg FailedLoad) (beloadv (m … st) vaddr);
    318         ! st ← acca_store p … dst v st ;
    319         ! st ← next … p l st ;
    320         return 〈E0, st〉
    321       | STORE addrl addrh src ⇒
    322         ! vaddrh ← dph_arg_retrieve … st addrh;
    323         ! vaddrl ← dpl_arg_retrieve … st addrl;
    324         ! vaddr ← pointer_of_address 〈vaddrl,vaddrh〉;
    325         ! v ← acca_arg_retrieve … st src;
    326         ! m' ← opt_to_res … (msg FailedStore) (bestorev (m … st) vaddr v);
    327         let st ≝ set_m … m' st in
    328         ! st ← next … p l st ;
    329         return 〈E0, st〉
    330       | COND src ltrue ⇒
    331         ! v ← acca_retrieve … st src;
    332         ! b ← bool_of_beval v;
    333         if b then
    334          ! st ← goto … p ge ltrue st ;
    335          return 〈E0, st〉
    336         else
    337          ! st ← next … p l st ;
    338          return 〈E0, st〉
    339       | ADDRESS ident prf ldest hdest ⇒
    340         eval_address … ge st ident prf ldest hdest l
    341       | OP1 op dacc_a sacc_a ⇒
    342         ! v ← acca_retrieve … st sacc_a;
    343         ! v ← Byte_of_val v;
    344         let v' ≝ BVByte (op1 eval op v) in
    345         ! st ← acca_store … dacc_a v' st;
    346         ! st ← next … l st ;
    347         return 〈E0, st〉
    348       | OP2 op dacc_a sacc_a src ⇒
    349         ! v1 ← acca_arg_retrieve … st sacc_a;
    350         ! v1 ← Byte_of_val v1;
    351         ! v2 ← snd_arg_retrieve … st src;
    352         ! v2 ← Byte_of_val v2;
    353         ! carry ← bool_of_beval (carry … st);
    354           let 〈v',carry〉 ≝ op2 eval carry op v1 v2 in
    355           let v' ≝ BVByte v' in
    356           let carry ≝ beval_of_bool carry in
    357         ! st ← acca_store … dacc_a v' st;
    358           let st ≝ set_carry … carry st in
    359         ! st ← next … l st ;
    360         return 〈E0, st〉
    361       | CLEAR_CARRY ⇒
    362         ! st ← next … l (set_carry … BVfalse st) ;
    363         return 〈E0, st〉
    364       | SET_CARRY ⇒
    365         ! st ← next … l (set_carry … BVtrue st) ;
    366         return 〈E0, st〉
    367       | OPACCS op dacc_a_reg dacc_b_reg sacc_a_reg sacc_b_reg ⇒
    368         ! v1 ← acca_arg_retrieve … st sacc_a_reg;
    369         ! v1 ← Byte_of_val v1;
    370         ! v2 ← accb_arg_retrieve … st sacc_b_reg;
    371         ! v2 ← Byte_of_val v2;
    372         let 〈v1',v2'〉 ≝ opaccs eval op v1 v2 in
    373         let v1' ≝ BVByte v1' in
    374         let v2' ≝ BVByte v2' in
    375         ! st ← acca_store … dacc_a_reg v1' st;
    376         ! st ← accb_store … dacc_b_reg v2' st;
    377         ! st ← next … l st ;
    378         return 〈E0, st〉
    379       | POP dst ⇒
    380         eval_pop … ge st dst l
    381       | PUSH src ⇒
    382         ! v ← acca_arg_retrieve … st src;
    383         ! st ← push … st v;
    384         ! st ← next … l st ;
    385         return 〈E0, st〉
    386       | MOVE dst_src ⇒
    387         ! st ← pair_reg_move … st dst_src ;
    388         ! st ← next … l st ;
    389         return 〈E0, st〉
    390       | CALL_ID id args dest ⇒
    391         eval_call_id_succ … ge st id args dest l
    392      ]
     421   | sequential seq l ⇒ eval_sequential … ge st seq l
     422   | extension_fin c ⇒ exec_fin_extended … ge c st
    393423   ].
    394424
Note: See TracChangeset for help on using the changeset viewer.