1 | include "joint/SemanticUtils.ma". |
---|
2 | include "ERTL/ERTL.ma". (* CSC: syntax.ma in RTLabs *) |
---|
3 | include alias "common/Identifiers.ma". |
---|
4 | |
---|
5 | definition ps_reg_store ≝ |
---|
6 | λr,v.λlocal_env:(register_env beval) × hw_register_env. |
---|
7 | do res ← reg_store r v (\fst local_env) ; |
---|
8 | OK … 〈res, \snd local_env〉. |
---|
9 | |
---|
10 | definition ps_reg_retrieve ≝ |
---|
11 | λlocal_env:(register_env beval) × hw_register_env. reg_retrieve … (\fst local_env). |
---|
12 | |
---|
13 | definition hw_reg_store ≝ |
---|
14 | λr,v.λlocal_env:(register_env beval) × hw_register_env. |
---|
15 | do res ← hwreg_store r v (\snd local_env) ; |
---|
16 | OK … 〈\fst local_env,res〉. |
---|
17 | |
---|
18 | definition hw_reg_retrieve ≝ |
---|
19 | λlocal_env:(register_env beval) × hw_register_env. hwreg_retrieve … (\snd local_env). |
---|
20 | |
---|
21 | definition ertl_more_sem_params: more_sem_params ertl_params_ := |
---|
22 | mk_more_sem_params ertl_params_ |
---|
23 | (list (register_env beval)) [] ((register_env beval) × hw_register_env) |
---|
24 | 〈empty_map …,empty_hw_register_env〉 0 it |
---|
25 | graph_succ_p |
---|
26 | ps_reg_store ps_reg_retrieve ps_reg_store ps_reg_retrieve ps_reg_store ps_reg_retrieve |
---|
27 | ps_reg_store ps_reg_retrieve ps_reg_store ps_reg_retrieve |
---|
28 | (λlocals,dest_src. |
---|
29 | do v ← |
---|
30 | match \snd dest_src with |
---|
31 | [ pseudo reg ⇒ ps_reg_retrieve locals reg |
---|
32 | | hardware reg ⇒ hw_reg_retrieve locals reg] ; |
---|
33 | match \fst dest_src with |
---|
34 | [ pseudo reg ⇒ ps_reg_store reg v locals |
---|
35 | | hardware reg ⇒ hw_reg_store reg v locals]) |
---|
36 | pointer_of_label. |
---|
37 | definition ertl_sem_params: sem_params ≝ mk_sem_params … ertl_more_sem_params. |
---|
38 | |
---|
39 | definition ertl_init_locals : |
---|
40 | list register → |
---|
41 | (register_env beval) × hw_register_env → (register_env beval) × hw_register_env ≝ |
---|
42 | λlocals,lenv. |
---|
43 | 〈foldl … (λlenv,reg. add … lenv reg BVundef) (empty_map …) locals, \snd lenv〉. |
---|
44 | |
---|
45 | (*CSC: could we use here a dependent type to avoid the Error case? *) |
---|
46 | axiom EmptyStack: String. |
---|
47 | definition ertl_pop_frame: |
---|
48 | ∀globals. genv … (ertl_params globals) → state … ertl_sem_params → res (state … ertl_sem_params) ≝ |
---|
49 | λglobals,ge,st. |
---|
50 | let frms ≝ st_frms ? st in |
---|
51 | match frms with |
---|
52 | [ nil ⇒ Error ? [MSG EmptyStack] |
---|
53 | | cons hd tl ⇒ |
---|
54 | OK … (set_frms ertl_sem_params tl (set_regs ertl_sem_params 〈hd, \snd (regs … st)〉 st)) ]. |
---|
55 | |
---|
56 | definition ertl_save_frame: |
---|
57 | address → nat → nat → nat → unit → state … ertl_sem_params → res (state … ertl_sem_params) ≝ |
---|
58 | λl.λ_.λ_.λ_.λ_.λst. |
---|
59 | do st ← save_ra … st l ; |
---|
60 | OK … |
---|
61 | (set_frms ertl_sem_params (\fst (regs … st) :: (st_frms … st)) |
---|
62 | (set_regs ertl_sem_params 〈empty_map …,\snd (regs … st)〉 st)). |
---|
63 | |
---|
64 | definition ertl_result_regs: |
---|
65 | ∀globals. genv … (ertl_params globals) → state ertl_sem_params → res (list register) ≝ |
---|
66 | λglobals,ge,st. |
---|
67 | do fn ← graph_fetch_function … globals ge st ; |
---|
68 | OK … (joint_if_result … fn). |
---|
69 | |
---|
70 | (*CSC: XXXX, for external functions only*) |
---|
71 | axiom ertl_fetch_external_args: external_function → state ertl_sem_params → res (list val). |
---|
72 | axiom ertl_set_result: list val → state ertl_sem_params → res (state ertl_sem_params). |
---|
73 | |
---|
74 | definition framesize: |
---|
75 | ∀globals. genv … (ertl_params globals) → state ertl_sem_params → res nat ≝ |
---|
76 | λglobals,ge,st. |
---|
77 | do f ← graph_fetch_function … ge st ; |
---|
78 | OK ? (joint_if_stacksize globals … f). |
---|
79 | |
---|
80 | definition get_hwsp : state ertl_sem_params → res address ≝ |
---|
81 | λst. |
---|
82 | do spl ← hwreg_retrieve (\snd (regs … st)) RegisterSPL ; |
---|
83 | do sph ← hwreg_retrieve (\snd (regs … st)) RegisterSPH ; |
---|
84 | OK ? 〈spl,sph〉. |
---|
85 | |
---|
86 | definition set_hwsp : address → state ertl_sem_params → res (state ertl_sem_params) ≝ |
---|
87 | λsp,st. |
---|
88 | let 〈spl,sph〉 ≝ sp in |
---|
89 | do hwregs ← hwreg_store RegisterSPL spl (\snd (regs … st)) ; |
---|
90 | do hwregs ← hwreg_store RegisterSPH sph hwregs ; |
---|
91 | OK ? (set_regs ertl_sem_params 〈\fst (regs … st),hwregs〉 st). |
---|
92 | |
---|
93 | definition ertl_exec_extended: |
---|
94 | ∀globals. genv globals (ertl_params globals) → |
---|
95 | ertl_statement_extension → label → state ertl_sem_params → |
---|
96 | IO io_out io_in (trace × (state ertl_sem_params)) ≝ |
---|
97 | λglobals,ge,stm,l,st. |
---|
98 | match stm with |
---|
99 | [ ertl_st_ext_new_frame ⇒ |
---|
100 | ! v ← framesize globals … ge st; |
---|
101 | ! sp ← get_hwsp st; |
---|
102 | ! newsp ← addr_sub sp v; |
---|
103 | ! st ← set_hwsp newsp st; |
---|
104 | ret ? 〈E0,goto … l st〉 |
---|
105 | | ertl_st_ext_del_frame ⇒ |
---|
106 | ! v ← framesize … ge st; |
---|
107 | ! sp ← get_hwsp st; |
---|
108 | ! newsp ← addr_add sp v; |
---|
109 | ! st ← set_hwsp newsp st; |
---|
110 | ret ? 〈E0,goto … l st〉 |
---|
111 | | ertl_st_ext_frame_size dst ⇒ |
---|
112 | ! v ← framesize … ge st; |
---|
113 | ! st ← greg_store ertl_sem_params dst (BVByte (bitvector_of_nat … v)) st; |
---|
114 | ret ? 〈E0, goto … l st〉 |
---|
115 | ]. |
---|
116 | |
---|
117 | definition ertl_more_sem_params2: ∀globals. more_sem_params2 … (ertl_params globals) ≝ |
---|
118 | λglobals. |
---|
119 | mk_more_sem_params2 … ertl_more_sem_params |
---|
120 | (graph_fetch_statement …) (load_ra …) (ertl_result_regs …) |
---|
121 | ertl_init_locals ertl_save_frame (ertl_pop_frame …) |
---|
122 | ertl_fetch_external_args ertl_set_result (ertl_exec_extended …). |
---|
123 | |
---|
124 | definition ertl_fullexec ≝ |
---|
125 | joint_fullexec … (λp. ertl_more_sem_params2 (prog_var_names … p)). |
---|