| 1 | include "joint/semanticsUtils.ma". |
|---|
| 2 | include "ERTLptr/ERTLptr.ma". (* CSC: syntax.ma in RTLabs *) |
|---|
| 3 | include "ERTL/ERTL_semantics.ma". |
|---|
| 4 | include alias "common/Identifiers.ma". |
|---|
| 5 | |
|---|
| 6 | definition ertlptr_save_frame: |
|---|
| 7 | call_kind → unit → state_pc ERTL_state → res (state … ERTL_state) ≝ |
|---|
| 8 | λk.λ_.λst. |
|---|
| 9 | ! st' ← match k with |
|---|
| 10 | [ ID ⇒ push_ra … st (pc … st) |
|---|
| 11 | | PTR ⇒ return (st : state ?) |
|---|
| 12 | ] ; |
|---|
| 13 | ! frms ← opt_to_res ? [MSG FrameErrorOnPush] (st_frms … st'); |
|---|
| 14 | return |
|---|
| 15 | (set_frms ERTL_state (〈\fst (regs ERTL_state st'), pc_block (pc … st)〉 :: frms) |
|---|
| 16 | (set_regs ERTL_state 〈empty_map …,\snd (regs … st')〉 st')). |
|---|
| 17 | |
|---|
| 18 | definition eval_ertlptr_seq: |
|---|
| 19 | ∀F. ∀globals. genv_gen F globals → |
|---|
| 20 | ertlptr_seq → ident → state ERTL_state → |
|---|
| 21 | res (state ERTL_state) ≝ |
|---|
| 22 | λF,globals,ge,stm,id,st. |
|---|
| 23 | match stm with |
|---|
| 24 | [ ertlptr_ertl seq ⇒ eval_ertl_seq F globals ge seq id st |
|---|
| 25 | | LOW_ADDRESS r l ⇒ ! pc_lab ← get_pc_from_label … ge id l; |
|---|
| 26 | let 〈addrl,addrh〉 ≝ beval_pair_of_pc pc_lab in |
|---|
| 27 | ps_reg_store_status r addrl st |
|---|
| 28 | | HIGH_ADDRESS r l ⇒ ! pc_lab ← get_pc_from_label … ge id l; |
|---|
| 29 | let 〈addrl,addrh〉 ≝ beval_pair_of_pc pc_lab in |
|---|
| 30 | ps_reg_store_status r addrh st |
|---|
| 31 | ]. |
|---|
| 32 | |
|---|
| 33 | definition ERTLptr_sem_uns ≝ |
|---|
| 34 | λF. mk_sem_unserialized_params ERTLptr ? |
|---|
| 35 | (* st_pars ≝ *) ERTL_state |
|---|
| 36 | (* acca_store_ ≝ *) ps_reg_store |
|---|
| 37 | (* acca_retrieve_ ≝ *) ps_reg_retrieve |
|---|
| 38 | (* acca_arg_retrieve_ ≝ *) ps_arg_retrieve |
|---|
| 39 | (* accb_store_ ≝ *) ps_reg_store |
|---|
| 40 | (* accb_retrieve_ ≝ *) ps_reg_retrieve |
|---|
| 41 | (* accb_arg_retrieve_ ≝ *) ps_arg_retrieve |
|---|
| 42 | (* dpl_store_ ≝ *) ps_reg_store |
|---|
| 43 | (* dpl_retrieve_ ≝ *) ps_reg_retrieve |
|---|
| 44 | (* dpl_arg_retrieve_ ≝ *) ps_arg_retrieve |
|---|
| 45 | (* dph_store_ ≝ *) ps_reg_store |
|---|
| 46 | (* dph_retrieve_ ≝ *) ps_reg_retrieve |
|---|
| 47 | (* dph_arg_retrieve_ ≝ *) ps_arg_retrieve |
|---|
| 48 | (* snd_arg_retrieve_ ≝ *) ps_arg_retrieve |
|---|
| 49 | (* pair_reg_move_ ≝ *) ertl_eval_move |
|---|
| 50 | (* save_frame ≝ *) ertlptr_save_frame |
|---|
| 51 | (* setup_call ≝ *) (λ_.λ_.λ_.λst.return st) |
|---|
| 52 | (* fetch_external_args≝ *) ertl_fetch_external_args |
|---|
| 53 | (* set_result ≝ *) ertl_set_result |
|---|
| 54 | (* call_args_for_main ≝ *) 0 |
|---|
| 55 | (* call_dest_for_main ≝ *) it |
|---|
| 56 | (* read_result ≝ *) (λ_.λ_.λ_. |
|---|
| 57 | λst.return map ?? (hwreg_retrieve (\snd (regs … st))) RegisterRets) |
|---|
| 58 | (* eval_ext_seq ≝ *) (λgl,ge,stm,id.eval_ertlptr_seq F gl ge stm id) |
|---|
| 59 | (* pop_frame ≝ *) (λ_.λ_.λ_.λ_.ertl_pop_frame). |
|---|
| 60 | |
|---|
| 61 | definition ERTLptr_semantics ≝ |
|---|
| 62 | mk_sem_graph_params ERTLptr ERTLptr_sem_uns. |
|---|
