source: src/ERTLptr/ERTLptr_semantics.ma @ 2638

Last change on this file since 2638 was 2604, checked in by piccolo, 7 years ago

ERTLtoERTLptr in place.

File size: 2.5 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 → ident → state_pc ERTL_state → res (state … ERTL_state) ≝
8 λk.λ_.λid.λst.
9 do st ← match k with [ID ⇒ push_ra … st (pc … st) |
10 PTR ⇒ return (st_no_pc … st)] ; OK …
11   (set_frms ERTL_state (〈\fst (regs ERTL_state st),id〉 :: (st_frms … st))
12    (set_regs ERTL_state 〈empty_map …,\snd (regs … st)〉 st)).
13
14definition eval_ertlptr_seq:
15 ∀F. ∀globals. genv_gen F globals →
16  ertlptr_seq → ident → state ERTL_state →
17   res (state ERTL_state) ≝
18 λF,globals,ge,stm,id,st.
19  match stm with
20   [ ertlptr_ertl seq ⇒ eval_ertl_seq F globals ge seq id st
21   | LOW_ADDRESS r l ⇒  ! pc_lab ← get_pc_from_label … ge id l;
22                        let 〈addrl,addrh〉 ≝ beval_pair_of_pc pc_lab in
23                        ps_reg_store_status r addrl st
24   | HIGH_ADDRESS r l ⇒ ! pc_lab ← get_pc_from_label … ge id l;
25                        let 〈addrl,addrh〉 ≝  beval_pair_of_pc pc_lab in
26                        ps_reg_store_status r addrh st
27   ].
28   
29definition ERTLptr_semantics ≝
30  make_sem_graph_params ERTLptr
31  (λF. mk_sem_unserialized_params ??
32  (* st_pars            ≝ *) ERTL_state
33  (* acca_store_        ≝ *) ps_reg_store
34  (* acca_retrieve_     ≝ *) ps_reg_retrieve
35  (* acca_arg_retrieve_ ≝ *) ps_arg_retrieve
36  (* accb_store_        ≝ *) ps_reg_store
37  (* accb_retrieve_     ≝ *) ps_reg_retrieve
38  (* accb_arg_retrieve_ ≝ *) ps_arg_retrieve
39  (* dpl_store_         ≝ *) ps_reg_store
40  (* dpl_retrieve_      ≝ *) ps_reg_retrieve
41  (* dpl_arg_retrieve_  ≝ *) ps_arg_retrieve
42  (* dph_store_         ≝ *) ps_reg_store
43  (* dph_retrieve_      ≝ *) ps_reg_retrieve
44  (* dph_arg_retrieve_  ≝ *) ps_arg_retrieve
45  (* snd_arg_retrieve_  ≝ *) ps_arg_retrieve
46  (* pair_reg_move_     ≝ *) ertl_eval_move
47  (* save_frame         ≝ *) ertlptr_save_frame
48  (* setup_call         ≝ *) (λ_.λ_.λ_.λst.return st)
49  (* fetch_external_args≝ *) ertl_fetch_external_args
50  (* set_result         ≝ *) ertl_set_result
51  (* call_args_for_main ≝ *) 0
52  (* call_dest_for_main ≝ *) it
53  (* read_result        ≝ *) (λ_.λ_.λ_.
54     λst.return map ?? (hwreg_retrieve (\snd (regs … st))) RegisterRets)
55  (* eval_ext_seq       ≝ *) (λgl,ge,stm,id.λ_.eval_ertlptr_seq F gl ge stm id)
56  (* pop_frame          ≝ *) (λ_.λ_.λ_.λ_.pop_ra …)).
Note: See TracBrowser for help on using the repository browser.