source: src/ERTLptr/ERTLptr_semantics.ma @ 3362

Last change on this file since 3362 was 2954, checked in by tranquil, 7 years ago

resolved circular dependency for ERTLptr's semantics

File size: 2.6 KB
Line 
1include "joint/semanticsUtils.ma".
2include "ERTLptr/ERTLptr.ma". (* CSC: syntax.ma in RTLabs *)
3include "ERTL/ERTL_semantics.ma".
4include alias "common/Identifiers.ma".
5
6definition 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
18definition 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 ← gen_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 ← gen_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
33definition 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 
61definition ERTLptr_semantics ≝
62  mk_sem_graph_params ERTLptr ERTLptr_sem_uns ERTLptr_premain.
Note: See TracBrowser for help on using the repository browser.