source: src/ERTLptr/ERTLptr_semantics.ma

Last change on this file was 2954, checked in by tranquil, 8 years ago

resolved circular dependency for ERTLptr's semantics

File size: 2.6 KB
RevLine 
[2566]1include "joint/semanticsUtils.ma".
2include "ERTLptr/ERTLptr.ma". (* CSC: syntax.ma in RTLabs *)
[2601]3include "ERTL/ERTL_semantics.ma".
[2566]4include alias "common/Identifiers.ma".
5
6definition ertlptr_save_frame:
[2783]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')).
[2566]17
18definition eval_ertlptr_seq:
[2954]19 ∀F.∀globals. genv_gen F globals →
[2566]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
[2954]25   | LOW_ADDRESS r l ⇒  ! pc_lab ← gen_pc_from_label … ge id l;
[2590]26                        let 〈addrl,addrh〉 ≝ beval_pair_of_pc pc_lab in
[2566]27                        ps_reg_store_status r addrl st
[2954]28   | HIGH_ADDRESS r l ⇒ ! pc_lab ← gen_pc_from_label … ge id l;
[2566]29                        let 〈addrl,addrh〉 ≝  beval_pair_of_pc pc_lab in
30                        ps_reg_store_status r addrh st
31   ].
[2666]32
33definition ERTLptr_sem_uns ≝
34λF. mk_sem_unserialized_params ERTLptr ?
[2566]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)
[2796]58  (* eval_ext_seq       ≝ *) (λgl,ge,stm,id.eval_ertlptr_seq F gl ge stm id)
[2783]59  (* pop_frame          ≝ *) (λ_.λ_.λ_.λ_.ertl_pop_frame).
60 
[2666]61definition ERTLptr_semantics ≝
[2946]62  mk_sem_graph_params ERTLptr ERTLptr_sem_uns ERTLptr_premain.
Note: See TracBrowser for help on using the repository browser.