1 | include "common/Globalenvs.ma". |
---|
2 | include "common/IO.ma". |
---|
3 | (* include "common/SmallstepExec.ma". *) |
---|
4 | include "joint/BEMem.ma". |
---|
5 | include "joint/Joint.ma". |
---|
6 | include "ASM/I8051bis.ma". |
---|
7 | include "common/extraGlobalenvs.ma". |
---|
8 | |
---|
9 | (* CSC: external functions never fail (??) and always return something of the |
---|
10 | size of one register, both in the frontend and in the backend. |
---|
11 | Is this reasonable??? In OCaml it always return a list, but in the frontend |
---|
12 | only the head is kept (or Undef if the list is empty) ??? *) |
---|
13 | |
---|
14 | (* Paolo: I'll put in this record the property about genv we need *) |
---|
15 | record genv_gen (F : list ident → Type[0]) (globals : list ident) : Type[0] ≝ |
---|
16 | { ge :> genv_t (fundef (F globals)) |
---|
17 | ; find_symbol_in_globals : ∀s.In … globals s → find_symbol … ge s ≠ None ? |
---|
18 | ; stack_sizes : ident → option ℕ |
---|
19 | ; get_pc_from_label : ident (* current function *) → label → res program_counter |
---|
20 | }. |
---|
21 | |
---|
22 | definition genv ≝ λp.genv_gen (joint_closed_internal_function p). |
---|
23 | coercion genv_to_genv_t : |
---|
24 | ∀p,globals.∀g : genv p globals.genv_t (joint_function p globals) ≝ |
---|
25 | λp,globals,g.ge ?? g on _g : genv ?? to genv_t ?. |
---|
26 | |
---|
27 | record sem_state_params : Type[1] ≝ |
---|
28 | { framesT: Type[0] |
---|
29 | ; empty_framesT: framesT |
---|
30 | ; regsT : Type[0] |
---|
31 | (* empty_regsT called at the start of each function call *) |
---|
32 | ; empty_regsT: xpointer → regsT (* initial stack pointer *) |
---|
33 | ; load_sp : regsT → res xpointer |
---|
34 | ; save_sp : regsT → xpointer → regsT |
---|
35 | }. |
---|
36 | |
---|
37 | inductive internal_stack : Type[0] ≝ |
---|
38 | | empty_is : internal_stack |
---|
39 | | one_is : beval → internal_stack |
---|
40 | | both_is : beval → beval → internal_stack. |
---|
41 | |
---|
42 | definition is_push : internal_stack → beval → res internal_stack ≝ |
---|
43 | λis,bv.match is with |
---|
44 | [ empty_is ⇒ return one_is bv |
---|
45 | | one_is bv' ⇒ return both_is bv' bv |
---|
46 | | both_is _ _ ⇒ Error … [MSG … InternalStackFull] |
---|
47 | ]. |
---|
48 | |
---|
49 | definition is_pop : internal_stack → res (beval × internal_stack) ≝ |
---|
50 | λis.match is with |
---|
51 | [ empty_is ⇒ Error … [MSG … InternalStackEmpty] |
---|
52 | | one_is bv' ⇒ return 〈bv', empty_is〉 |
---|
53 | | both_is bv bv' ⇒ return 〈bv', one_is bv〉 |
---|
54 | ]. |
---|
55 | |
---|
56 | record state (semp: sem_state_params): Type[0] ≝ |
---|
57 | { st_frms: option(framesT semp) |
---|
58 | ; istack : internal_stack |
---|
59 | ; carry: bebit |
---|
60 | ; regs: regsT semp |
---|
61 | ; m: bemem |
---|
62 | ; stack_usage : ℕ |
---|
63 | }. |
---|
64 | |
---|
65 | definition sp ≝ λp,st.load_sp p (regs ? st). |
---|
66 | |
---|
67 | record state_pc (semp : sem_state_params) : Type[0] ≝ |
---|
68 | { st_no_pc :> state semp |
---|
69 | ; pc : program_counter |
---|
70 | (* for correctness reasons: pc of last popped calling address (null_pc at the start) *) |
---|
71 | ; last_pop : program_counter |
---|
72 | }. |
---|
73 | |
---|
74 | definition init_pc : program_counter ≝ |
---|
75 | mk_program_counter «mk_block (-1), refl …» one. |
---|
76 | |
---|
77 | definition null_pc : Pos → program_counter ≝ λpos. |
---|
78 | mk_program_counter «dummy_block_code, refl …» pos. |
---|
79 | |
---|
80 | definition set_m: ∀p. bemem → state p → state p ≝ |
---|
81 | λp,m,st. mk_state p (st_frms …st) (istack … st) (carry … st) (regs … st) m (stack_usage … st). |
---|
82 | |
---|
83 | definition set_regs: ∀p:sem_state_params. regsT p → state p → state p ≝ |
---|
84 | λp,regs,st.mk_state p (st_frms … st) (istack … st) (carry … st) regs (m … st) (stack_usage … st). |
---|
85 | |
---|
86 | definition set_sp: ∀p. ? → state p → state p ≝ |
---|
87 | λp,sp,st.let regs' ≝ save_sp … (regs … st) sp in |
---|
88 | mk_state p (st_frms … st) (istack … st) (carry … st) regs' (m … st) (stack_usage … st). |
---|
89 | |
---|
90 | definition set_carry: ∀p. bebit → state p → state p ≝ |
---|
91 | λp,carry,st. mk_state … (st_frms … st) (istack … st) carry (regs … st) (m … st) (stack_usage … st). |
---|
92 | |
---|
93 | definition set_istack: ∀p. internal_stack → state p → state p ≝ |
---|
94 | λp,is,st. mk_state … (st_frms … st) is (carry … st) (regs … st) (m … st) (stack_usage … st). |
---|
95 | |
---|
96 | definition set_pc: ∀p. ? → state_pc p → state_pc p ≝ |
---|
97 | λp,pc,st. mk_state_pc … (st_no_pc … st) pc (last_pop … st). |
---|
98 | |
---|
99 | definition set_no_pc: ∀p. ? → state_pc p → state_pc p ≝ |
---|
100 | λp,s,st. mk_state_pc … s (pc … st) (last_pop … st). |
---|
101 | |
---|
102 | definition set_last_pop: ∀p.state p → program_counter → state_pc p ≝ |
---|
103 | λp,st,pc. mk_state_pc … st pc pc. |
---|
104 | |
---|
105 | definition set_frms: ∀p:sem_state_params. framesT p → state p → state p ≝ |
---|
106 | λp,frms,st. mk_state … (Some ? (frms)) (istack … st) (carry … st) (regs … st) (m … st) (stack_usage … st). |
---|
107 | |
---|
108 | (* |
---|
109 | inductive step_flow (p : unserialized_params) (F : Type[0]) : possible_flows → Type[0] ≝ |
---|
110 | | Redirect : ∀lbls.(Σl.In ? lbls l) → step_flow p F (Labels lbls) (* used for goto-like flow alteration *) |
---|
111 | | Init : Z → F → call_args p → call_dest p → step_flow p F Call (* call a function with given id, then proceed *) |
---|
112 | | Proceed : ∀flows.step_flow p F flows. (* go to implicit successor *) |
---|
113 | |
---|
114 | inductive fin_step_flow (p : unserialized_params) (F : Type[0]) : possible_flows → Type[0] ≝ |
---|
115 | | FRedirect : ∀lbls.(Σl.In ? lbls l) → fin_step_flow p F (Labels lbls) |
---|
116 | | FTailInit : Z → F → call_args p → fin_step_flow p F Call |
---|
117 | | FEnd1 : fin_step_flow p F (Labels [ ]) (* end flow *) |
---|
118 | | FEnd2 : fin_step_flow p F Call. (* end flow *) |
---|
119 | *) |
---|
120 | |
---|
121 | (* this can replace graph_fetch function and lin_fetch_function *) |
---|
122 | definition fetch_function: |
---|
123 | ∀F. |
---|
124 | ∀ge : genv_t F. |
---|
125 | (Σb.block_region b = Code) → |
---|
126 | res (ident×F) ≝ |
---|
127 | λF,ge,bl. |
---|
128 | opt_to_res … [MSG BadFunction] |
---|
129 | (! id ← symbol_for_block … ge bl ; |
---|
130 | ! fd ← find_funct_ptr … ge bl ; |
---|
131 | return 〈id, fd〉). |
---|
132 | |
---|
133 | definition fetch_internal_function : |
---|
134 | ∀F. |
---|
135 | ∀ge : genv_t (fundef F). |
---|
136 | (Σb.block_region b = Code) → |
---|
137 | res (ident×F) ≝ |
---|
138 | λF,ge,bl. |
---|
139 | ! 〈id, fd〉 ← fetch_function … ge bl ; |
---|
140 | match fd with |
---|
141 | [ Internal ifd ⇒ return 〈id, ifd〉 |
---|
142 | | _ ⇒ Error … [MSG BadFunction] |
---|
143 | ]. |
---|
144 | |
---|
145 | lemma fetch_internal_function_no_minus_one : |
---|
146 | ∀F,V,i,p,bl. |
---|
147 | block_id (pi1 … bl) = -1 → |
---|
148 | fetch_internal_function … (globalenv (λvars.fundef (F vars)) V i p) |
---|
149 | bl = Error … [MSG BadFunction]. |
---|
150 | #F#V#i#p ** #id #EQ1 #EQ2 destruct |
---|
151 | whd in match fetch_internal_function; |
---|
152 | whd in match fetch_function; normalize nodelta |
---|
153 | >globalenv_no_minus_one |
---|
154 | cases (symbol_for_block ???) normalize // |
---|
155 | qed. |
---|
156 | |
---|
157 | inductive call_kind : Type[0] ≝ |
---|
158 | | PTR : call_kind |
---|
159 | | ID : call_kind. |
---|
160 | |
---|
161 | definition kind_of_call : |
---|
162 | ∀p.(ident + (dpl_arg p × (dph_arg p))) → call_kind ≝ |
---|
163 | λp,f.match f with [ inl _ ⇒ ID | inr _ ⇒ PTR ]. |
---|
164 | |
---|
165 | record sem_unserialized_params |
---|
166 | (uns_pars : unserialized_params) |
---|
167 | (F : list ident → Type[0]) : Type[1] ≝ |
---|
168 | { st_pars :> sem_state_params |
---|
169 | |
---|
170 | ; acca_store_ : acc_a_reg uns_pars → beval → regsT st_pars → res (regsT st_pars) |
---|
171 | ; acca_retrieve_ : regsT st_pars → acc_a_reg uns_pars → res beval |
---|
172 | ; acca_arg_retrieve_ : regsT st_pars → acc_a_arg uns_pars → res beval |
---|
173 | ; accb_store_ : acc_b_reg uns_pars → beval → regsT st_pars → res (regsT st_pars) |
---|
174 | ; accb_retrieve_ : regsT st_pars → acc_b_reg uns_pars → res beval |
---|
175 | ; accb_arg_retrieve_ : regsT st_pars → acc_b_arg uns_pars → res beval |
---|
176 | ; dpl_store_ : dpl_reg uns_pars → beval → regsT st_pars → res (regsT st_pars) |
---|
177 | ; dpl_retrieve_ : regsT st_pars → dpl_reg uns_pars → res beval |
---|
178 | ; dpl_arg_retrieve_ : regsT st_pars → dpl_arg uns_pars → res beval |
---|
179 | ; dph_store_ : dph_reg uns_pars → beval → regsT st_pars → res (regsT st_pars) |
---|
180 | ; dph_retrieve_ : regsT st_pars → dph_reg uns_pars → res beval |
---|
181 | ; dph_arg_retrieve_ : regsT st_pars → dph_arg uns_pars → res beval |
---|
182 | ; snd_arg_retrieve_ : regsT st_pars → snd_arg uns_pars → res beval |
---|
183 | ; pair_reg_move_ : regsT st_pars → pair_move uns_pars → res (regsT st_pars) |
---|
184 | |
---|
185 | (* Paolo: save_frame separated from call_setup to factorize tailcall code *) |
---|
186 | (* ; allocate_locals_ : localsT uns_pars → regsT st_pars → regsT st_pars *) |
---|
187 | ; save_frame: call_kind → call_dest uns_pars → state_pc st_pars → res (state st_pars) |
---|
188 | (*CSC: setup_call returns a res only because we can call a function with the wrong number and |
---|
189 | type of arguments. To be fixed using a dependent type *) |
---|
190 | ; setup_call : nat → paramsT … uns_pars → call_args uns_pars → |
---|
191 | state st_pars → res (state st_pars) |
---|
192 | ; fetch_external_args: external_function → state st_pars → call_args … uns_pars → |
---|
193 | res (list val) |
---|
194 | ; set_result: list val → call_dest uns_pars → state st_pars → res (state st_pars) |
---|
195 | ; call_args_for_main: call_args uns_pars |
---|
196 | ; call_dest_for_main: call_dest uns_pars |
---|
197 | |
---|
198 | (* from now on, parameters that use the type of functions *) |
---|
199 | ; read_result: ∀globals.genv_t (fundef (F globals)) → call_dest uns_pars → |
---|
200 | state st_pars → res (list beval) |
---|
201 | ; eval_ext_seq: ∀globals.∀ge : genv_gen F globals.ext_seq uns_pars → |
---|
202 | ident (* current *) → state st_pars → res (state st_pars) |
---|
203 | ; pop_frame: ∀globals.∀ge : genv_gen F globals. |
---|
204 | ident (* current *) → call_dest uns_pars (* current ret *) → |
---|
205 | state st_pars → res (state st_pars × program_counter) |
---|
206 | }. |
---|
207 | |
---|
208 | (* |
---|
209 | definition allocate_locals : |
---|
210 | ∀p,F.∀sup : sem_unserialized_params p F. |
---|
211 | list (localsT p) → state sup → state sup ≝ |
---|
212 | λp,F,sup,l,st. |
---|
213 | let r ≝ foldr … (allocate_locals_ … sup) (regs … st) l in |
---|
214 | set_regs … r st. *) |
---|
215 | |
---|
216 | definition helper_def_retrieve : |
---|
217 | ∀X : ? → ? → ? → Type[0]. |
---|
218 | (∀up,F.∀p:sem_unserialized_params up F. regsT (st_pars up F p) → X up F p → res beval) → |
---|
219 | ∀up,F.∀p : sem_unserialized_params up F.state (st_pars up F p) → X up F p → res beval ≝ |
---|
220 | λX,f,up,F,p,st.f ?? p (regs … st). |
---|
221 | |
---|
222 | definition helper_def_store : |
---|
223 | ∀X : ? → ? → ? → Type[0]. |
---|
224 | (∀up,F.∀p : sem_unserialized_params up F.X up F p → beval → regsT (st_pars … p) → res (regsT (st_pars … p))) → |
---|
225 | ∀up,F.∀p : sem_unserialized_params up F.X up F p → beval → state (st_pars … p) → res (state (st_pars … p)) ≝ |
---|
226 | λX,f,up,F,p,x,v,st.! r ← f ?? p x v (regs … st) ; return set_regs … r st. |
---|
227 | |
---|
228 | definition acca_retrieve ≝ helper_def_retrieve ? acca_retrieve_. |
---|
229 | definition acca_store ≝ helper_def_store ? acca_store_. |
---|
230 | definition acca_arg_retrieve ≝ helper_def_retrieve ? acca_arg_retrieve_. |
---|
231 | definition accb_store ≝ helper_def_store ? accb_store_. |
---|
232 | definition accb_retrieve ≝ helper_def_retrieve ? accb_retrieve_. |
---|
233 | definition accb_arg_retrieve ≝ helper_def_retrieve ? accb_arg_retrieve_. |
---|
234 | definition dpl_store ≝ helper_def_store ? dpl_store_. |
---|
235 | definition dpl_retrieve ≝ helper_def_retrieve ? dpl_retrieve_. |
---|
236 | definition dpl_arg_retrieve ≝ helper_def_retrieve ? dpl_arg_retrieve_. |
---|
237 | definition dph_store ≝ helper_def_store ? dph_store_. |
---|
238 | definition dph_retrieve ≝ helper_def_retrieve ? dph_retrieve_. |
---|
239 | definition dph_arg_retrieve ≝ helper_def_retrieve ? dph_arg_retrieve_. |
---|
240 | definition snd_arg_retrieve ≝ helper_def_retrieve ? snd_arg_retrieve_. |
---|
241 | definition pair_reg_move ≝ |
---|
242 | λup,F.λp : sem_unserialized_params up F.λst : state (st_pars … p).λpm : pair_move up. |
---|
243 | ! r ← pair_reg_move_ ?? p (regs ? st) pm; |
---|
244 | return set_regs ? r st. |
---|
245 | |
---|
246 | definition push: ∀p.state p → beval → res (state p) ≝ |
---|
247 | λp,st,v. |
---|
248 | ! is ← is_push (istack … st) v ; |
---|
249 | return set_istack … is st. |
---|
250 | |
---|
251 | definition pop: ∀p. state p → res (beval × (state p)) ≝ |
---|
252 | λp,st. |
---|
253 | ! 〈bv, is〉 ← is_pop (istack … st) ; |
---|
254 | return 〈bv, set_istack … is st〉. |
---|
255 | |
---|
256 | definition push_ra : ∀p. state p → program_counter → res (state p) ≝ |
---|
257 | λp,st,l. |
---|
258 | let 〈addrl,addrh〉 ≝ beval_pair_of_pc l in |
---|
259 | ! st' ← push … st addrl; |
---|
260 | push … st' addrh. |
---|
261 | |
---|
262 | definition pop_ra : ∀p.state p → res (state p × program_counter) ≝ |
---|
263 | λp,st. |
---|
264 | ! 〈addrh, st'〉 ← pop … st; |
---|
265 | ! 〈addrl, st''〉 ← pop … st'; |
---|
266 | ! pr ← pc_of_bevals [addrl; addrh]; |
---|
267 | return 〈st'',pr〉. |
---|
268 | |
---|
269 | (* parameters that are defined by serialization *) |
---|
270 | record serialized_params : Type[1] ≝ |
---|
271 | { spp :> params |
---|
272 | ; msu_pars :> sem_unserialized_params spp (joint_closed_internal_function spp) |
---|
273 | ; offset_of_point : code_point spp → Pos |
---|
274 | ; point_of_offset : Pos → code_point spp |
---|
275 | ; point_of_offset_of_point : |
---|
276 | ∀pt.point_of_offset (offset_of_point pt) = pt |
---|
277 | ; offset_of_point_of_offset : |
---|
278 | ∀o.offset_of_point (point_of_offset o) = o |
---|
279 | }. |
---|
280 | |
---|
281 | record sem_params : Type[1] ≝ |
---|
282 | { spp' :> serialized_params |
---|
283 | ; pre_main_generator : ∀p : joint_program spp'.joint_closed_internal_function spp' (prog_var_names … p) |
---|
284 | }. |
---|
285 | |
---|
286 | (* |
---|
287 | coercion ms_pars_to_msu_pars nocomposites : |
---|
288 | ∀p : params.∀msp : more_sem_params p.more_sem_unserialized_params p (λglobals.joint_internal_function globals p) |
---|
289 | ≝ msu_pars |
---|
290 | on _msp : more_sem_params ? to more_sem_unserialized_params ??. |
---|
291 | |
---|
292 | definition ss_pars_of_ms_pars ≝ |
---|
293 | λp.λpp : more_sem_params p. |
---|
294 | st_pars … (msu_pars … pp). |
---|
295 | coercion ms_pars_to_ss_pars nocomposites : |
---|
296 | ∀p : params.∀msp : more_sem_params p.sem_state_params ≝ |
---|
297 | ss_pars_of_ms_pars on _msp : more_sem_params ? to sem_state_params.*) |
---|
298 | |
---|
299 | definition pc_of_point : ∀p:sem_params.(Σb.block_region b = Code) → |
---|
300 | code_point p → program_counter ≝ |
---|
301 | λp,bl,pt. |
---|
302 | mk_program_counter bl (offset_of_point p pt). |
---|
303 | |
---|
304 | definition point_of_pc : |
---|
305 | ∀p:sem_params.program_counter → code_point p ≝ |
---|
306 | λp,ptr.point_of_offset p (pc_offset ptr). |
---|
307 | |
---|
308 | lemma point_of_pc_of_point : |
---|
309 | ∀p,bl,pt. |
---|
310 | point_of_pc p (pc_of_point p bl pt) = pt. |
---|
311 | #p #bl #pt normalize // qed. |
---|
312 | |
---|
313 | lemma pc_of_point_of_pc : |
---|
314 | ∀p,ptr. |
---|
315 | pc_of_point p (pc_block ptr) (point_of_pc p ptr) = ptr. |
---|
316 | #p * #bl #off normalize >offset_of_point_of_offset % qed. |
---|
317 | |
---|
318 | definition fetch_statement: ∀p : sem_params.∀globals. |
---|
319 | ∀ge : genv_t (joint_function p globals). program_counter → |
---|
320 | res (ident × (joint_closed_internal_function p globals) × (joint_statement p globals)) ≝ |
---|
321 | λp,globals,ge,ptr. |
---|
322 | ! 〈id, fn〉 ← fetch_internal_function … ge (pc_block ptr) ; |
---|
323 | let pt ≝ point_of_pc p ptr in |
---|
324 | ! stmt ← opt_to_res … (msg ProgramCounterOutOfCode) (stmt_at … (joint_if_code … fn) pt); |
---|
325 | return 〈id, fn, stmt〉. |
---|
326 | |
---|
327 | definition pc_of_label : ∀p : sem_params.∀globals. |
---|
328 | genv_t (joint_function p globals) → (Σb.block_region b = Code) → label → res program_counter ≝ |
---|
329 | λp,globals,ge,bl,lbl. |
---|
330 | ! 〈i, fn〉 ← fetch_internal_function … ge bl ; |
---|
331 | ! pt ← opt_to_res … [MSG LabelNotFound ; CTX ? lbl] |
---|
332 | (point_of_label … (joint_if_code … fn) lbl) ; |
---|
333 | return mk_program_counter bl (offset_of_point p pt). |
---|
334 | |
---|
335 | definition succ_pc : ∀p : sem_params. |
---|
336 | program_counter → succ p → program_counter ≝ |
---|
337 | λp,ptr,nxt. |
---|
338 | let curr ≝ point_of_pc p ptr in |
---|
339 | pc_of_point p (pc_block ptr) (point_of_succ p curr nxt). |
---|
340 | |
---|
341 | (* |
---|
342 | record sem_params : Type[1] ≝ |
---|
343 | { spp :> params |
---|
344 | ; more_sem_pars :> more_sem_params spp |
---|
345 | }. |
---|
346 | *) |
---|
347 | (* definition msu_pars_of_s_pars : |
---|
348 | ∀p : sem_params.more_sem_unserialized_params (spp p) (λglobals.joint_internal_function globals (spp p)) |
---|
349 | ≝ λp : sem_params. |
---|
350 | msu_pars … (more_sem_pars p). |
---|
351 | coercion s_pars_to_msu_pars nocomposites : |
---|
352 | ∀p : sem_params.more_sem_unserialized_params (spp p) (λglobals.joint_internal_function globals (spp p)) ≝ |
---|
353 | msu_pars_of_s_pars |
---|
354 | on p : sem_params to more_sem_unserialized_params ??. |
---|
355 | |
---|
356 | definition ss_pars_of_s_pars : |
---|
357 | ∀p : sem_params.sem_state_params |
---|
358 | ≝ λp : sem_params. |
---|
359 | st_pars … (msu_pars … (more_sem_pars p)). |
---|
360 | coercion s_pars_to_ss_pars nocomposites : |
---|
361 | ∀p : sem_params.sem_state_params ≝ |
---|
362 | ss_pars_of_s_pars |
---|
363 | on _p : sem_params to sem_state_params. |
---|
364 | |
---|
365 | definition ms_pars_of_s_pars : |
---|
366 | ∀p : sem_params.more_sem_params (spp p) |
---|
367 | ≝ more_sem_pars. |
---|
368 | coercion s_pars_to_ms_pars nocomposites : |
---|
369 | ∀p : sem_params.more_sem_params (spp p) ≝ |
---|
370 | ms_pars_of_s_pars |
---|
371 | on p : sem_params to more_sem_params ?.*) |
---|
372 | |
---|
373 | (* definition address_of_label: ∀globals. ∀p:sem_params. |
---|
374 | genv globals p → pointer → label → res address ≝ |
---|
375 | λglobals,p,ge,ptr,l. |
---|
376 | do newptr ← pointer_of_label … p ? ge … ptr l ; |
---|
377 | OK … (address_of_code_pointer newptr). *) |
---|
378 | |
---|
379 | definition goto: ∀p : sem_params.∀globals. |
---|
380 | genv_t (joint_function p globals) → label → state_pc p → res (state_pc p) ≝ |
---|
381 | λp,globals,ge,l,st. |
---|
382 | ! newpc ← pc_of_label … ge (pc_block (pc … st)) l ; |
---|
383 | return set_pc … newpc st. |
---|
384 | |
---|
385 | (* |
---|
386 | definition empty_state: ∀p. more_sem_params p → state p ≝ |
---|
387 | mk_state … (empty_framesT …) |
---|
388 | *) |
---|
389 | |
---|
390 | definition next : ∀p : sem_params.succ p → state_pc p → state_pc p ≝ |
---|
391 | λp,l,st. |
---|
392 | let newpc ≝ succ_pc … (pc … st) l in |
---|
393 | set_pc … newpc st. |
---|
394 | |
---|
395 | definition next_of_call_pc : ∀p : sem_params.∀globals.genv_t (joint_function p globals) → |
---|
396 | program_counter → res (succ p) ≝ |
---|
397 | λp,globals,ge,pc. |
---|
398 | ! 〈id_fn, stmt〉 ← fetch_statement … ge pc ; |
---|
399 | match stmt with |
---|
400 | [ sequential s nxt ⇒ |
---|
401 | match s with |
---|
402 | [ CALL _ _ _ ⇒ return nxt |
---|
403 | | _ ⇒ Error … [MSG NoSuccessor] |
---|
404 | ] |
---|
405 | | _ ⇒ Error … [MSG NoSuccessor] |
---|
406 | ]. |
---|
407 | |
---|
408 | lemma deq_elim : ∀A : DeqSet.∀P : bool → Prop.∀x,y : A. |
---|
409 | (x = y → P true) → (x ≠ y → P false) → P (x == y). |
---|
410 | #A #P #x #y #H1 #H2 inversion (x == y) #EQ |
---|
411 | [ @H1 @(proj1 … (eqb_true … ) EQ) | @H2 % #EQ' destruct |
---|
412 | >(proj2 … (eqb_true …) (refl …)) in EQ; #ABS destruct ] qed. |
---|
413 | |
---|
414 | definition eval_seq_no_pc : |
---|
415 | ∀p:sem_params.∀globals.∀ge:genv p globals.ident → |
---|
416 | joint_seq p globals → state p → |
---|
417 | res (state p) ≝ |
---|
418 | λp,globals,ge,curr_id,seq,st. |
---|
419 | match seq with |
---|
420 | [ extension_seq c ⇒ |
---|
421 | eval_ext_seq … ge c curr_id st |
---|
422 | | LOAD dst addrl addrh ⇒ |
---|
423 | ! vaddrh ← dph_arg_retrieve … st addrh ; |
---|
424 | ! vaddrl ← dpl_arg_retrieve … st addrl; |
---|
425 | ! vaddr ← pointer_of_address 〈vaddrl,vaddrh〉; |
---|
426 | ! v ← opt_to_res … (msg FailedLoad) (beloadv (m … st) vaddr); |
---|
427 | acca_store p … dst v st |
---|
428 | | STORE addrl addrh src ⇒ |
---|
429 | ! vaddrh ← dph_arg_retrieve … st addrh; |
---|
430 | ! vaddrl ← dpl_arg_retrieve … st addrl; |
---|
431 | ! vaddr ← pointer_of_address 〈vaddrl,vaddrh〉; |
---|
432 | ! v ← acca_arg_retrieve … st src; |
---|
433 | ! m' ← opt_to_res … (msg FailedStore) (bestorev (m … st) vaddr v); |
---|
434 | return set_m … m' st |
---|
435 | | ADDRESS id prf ldest hdest ⇒ |
---|
436 | let addr_block ≝ opt_safe ? (find_symbol … ge id) ? in |
---|
437 | let 〈laddr,haddr〉 ≝ beval_pair_of_pointer (mk_pointer addr_block zero_offset) in |
---|
438 | ! st' ← dpl_store … ldest laddr st; |
---|
439 | dph_store … hdest haddr st' |
---|
440 | | OP1 op dacc_a sacc_a ⇒ |
---|
441 | ! v ← acca_retrieve … st sacc_a; |
---|
442 | ! v' ← be_op1 op v ; |
---|
443 | acca_store … dacc_a v' st |
---|
444 | | OP2 op dacc_a sacc_a src ⇒ |
---|
445 | ! v1 ← acca_arg_retrieve … st sacc_a; |
---|
446 | ! v2 ← snd_arg_retrieve … st src; |
---|
447 | ! 〈v',carry〉 ← be_op2 (carry … st) op v1 v2 ; |
---|
448 | ! st' ← acca_store … dacc_a v' st; |
---|
449 | return set_carry … carry st' |
---|
450 | | CLEAR_CARRY ⇒ |
---|
451 | return set_carry … (BBbit false) st |
---|
452 | | SET_CARRY ⇒ |
---|
453 | return set_carry … (BBbit true) st |
---|
454 | | OPACCS op dacc_a_reg dacc_b_reg sacc_a_reg sacc_b_reg ⇒ |
---|
455 | ! v1 ← acca_arg_retrieve … st sacc_a_reg; |
---|
456 | ! v2 ← accb_arg_retrieve … st sacc_b_reg; |
---|
457 | ! 〈v1',v2'〉 ← be_opaccs op v1 v2 ; |
---|
458 | ! st' ← acca_store … dacc_a_reg v1' st; |
---|
459 | accb_store … dacc_b_reg v2' st' |
---|
460 | | POP dst ⇒ |
---|
461 | ! 〈v, st'〉 ← pop p st; |
---|
462 | acca_store … p dst v st' |
---|
463 | | PUSH src ⇒ |
---|
464 | ! v ← acca_arg_retrieve … st src; |
---|
465 | push … st v |
---|
466 | | MOVE dst_src ⇒ |
---|
467 | pair_reg_move … st dst_src |
---|
468 | | _ ⇒ return st (* for calls do everything in eval_seq_advance *) |
---|
469 | ]. |
---|
470 | @hide_prf |
---|
471 | @find_symbol_in_globals |
---|
472 | lapply prf |
---|
473 | elim globals [*] |
---|
474 | #hd #tl #IH #H elim (orb_Prop_true … H) -H |
---|
475 | [ @deq_elim #H * destruct %1 % | #H %2{(IH … H)} ] |
---|
476 | qed. |
---|
477 | |
---|
478 | definition code_block_of_block : block → option (Σb.block_region b = Code) ≝ |
---|
479 | λbl.match block_region bl |
---|
480 | return λx.block_region bl = x → option (Σb.block_region b = Code) with |
---|
481 | [ Code ⇒ λprf.Some ? «bl, prf» |
---|
482 | | XData ⇒ λ_.None ? |
---|
483 | ] (refl …). |
---|
484 | |
---|
485 | definition block_of_funct_id ≝ λF.λsp:sem_state_params. |
---|
486 | λge: genv_t F.λid. |
---|
487 | opt_to_res … [MSG BadFunction; CTX … id] ( |
---|
488 | ! bl ← find_symbol … ge id; |
---|
489 | code_block_of_block bl). |
---|
490 | |
---|
491 | definition block_of_call ≝ λp : sem_params. |
---|
492 | λglobals.λge: genv_t (joint_function p globals).λf.λst : state p. |
---|
493 | ! bl ← match f with |
---|
494 | [ inl id ⇒ |
---|
495 | opt_to_res … [MSG BadFunction; CTX … id] |
---|
496 | (find_symbol … ge id) |
---|
497 | | inr addr ⇒ |
---|
498 | ! addr_l ← dpl_arg_retrieve … st (\fst addr) ; |
---|
499 | ! addr_h ← dph_arg_retrieve … st (\snd addr) ; |
---|
500 | ! ptr ← pointer_of_bevals … [addr_l ; addr_h ] ; |
---|
501 | if eq_bv … (bv_zero …) (offv (poff ptr)) then |
---|
502 | return pblock ptr |
---|
503 | else |
---|
504 | Error … [MSG BadFunction; MSG BadPointer] |
---|
505 | ] ; |
---|
506 | opt_to_res … [MSG BadFunction; MSG BadPointer] |
---|
507 | (code_block_of_block bl). |
---|
508 | |
---|
509 | definition eval_external_call ≝ |
---|
510 | λp : sem_params.λfn,args,dest,st. |
---|
511 | ! params ← fetch_external_args … p fn st args : IO ???; |
---|
512 | ! evargs ← check_eventval_list params (sig_args (ef_sig fn)) : IO ???; |
---|
513 | ! evres ← do_io (ef_id fn) evargs (proj_sig_res (ef_sig fn)); |
---|
514 | (* CSC: XXX bug here; I think I should split it into Byte-long |
---|
515 | components; instead I am making a singleton out of it. To be |
---|
516 | fixed once we fully implement external functions. *) |
---|
517 | let vs ≝ [mk_val ? evres] in |
---|
518 | set_result … p vs dest st. |
---|
519 | |
---|
520 | definition increment_stack_usage : ∀p.ℕ → state p → state p ≝ |
---|
521 | λp,n,st.mk_state p (st_frms … st) (istack … st) (carry … st) (regs … st) (m … st) |
---|
522 | (n + stack_usage … st). |
---|
523 | |
---|
524 | definition decrement_stack_usage : ∀p.ℕ → state p → state p ≝ |
---|
525 | λp,n,st.mk_state p (st_frms … st) (istack … st) (carry … st) (regs … st) (m … st) |
---|
526 | (stack_usage … st - n). |
---|
527 | |
---|
528 | definition eval_internal_call ≝ |
---|
529 | λp : sem_params.λglobals : list ident.λge : genv p globals.λi,fn,args. |
---|
530 | λst : state p. |
---|
531 | ! stack_size ← opt_to_res … [MSG MissingStackSize; CTX … i] (stack_sizes … ge i) ; |
---|
532 | ! st' ← setup_call … stack_size (joint_if_params … globals fn) args st ; |
---|
533 | return increment_stack_usage … stack_size st'. |
---|
534 | |
---|
535 | definition is_inl : ∀A,B.A+B → bool ≝ λA,B,x.match x with [ inl _ ⇒ true | _ ⇒ false ]. |
---|
536 | |
---|
537 | definition eval_call ≝ |
---|
538 | λp : sem_params.λglobals : list ident.λge : genv p globals.λf,args,dest,nxt. |
---|
539 | λst : state_pc p. |
---|
540 | ! bl ← block_of_call … ge f st : IO ???; |
---|
541 | ! 〈i, fd〉 ← fetch_function … ge bl : IO ???; |
---|
542 | match fd with |
---|
543 | [ Internal ifd ⇒ |
---|
544 | ! st' ← save_frame … (kind_of_call … f) dest st ; |
---|
545 | ! st'' ← eval_internal_call p globals ge i ifd args st' ; |
---|
546 | let pc ≝ pc_of_point p bl (joint_if_entry … ifd) in |
---|
547 | return mk_state_pc … st'' pc (last_pop … st) |
---|
548 | | External efd ⇒ |
---|
549 | ! st' ← eval_external_call … efd args dest st ; |
---|
550 | return mk_state_pc … st' (succ_pc p (pc … st) nxt) (last_pop … st) |
---|
551 | ]. |
---|
552 | |
---|
553 | definition eval_statement_no_pc : |
---|
554 | ∀p:sem_params.∀globals.∀ge:genv p globals. |
---|
555 | ident (* current *) → |
---|
556 | joint_statement p globals → state p → res (state p) ≝ |
---|
557 | λp,globals,ge,curr_id,s,st. |
---|
558 | match s with |
---|
559 | [ sequential s next ⇒ |
---|
560 | match s with |
---|
561 | [ step_seq s ⇒ eval_seq_no_pc … ge curr_id s st |
---|
562 | | _ ⇒ return st |
---|
563 | ] |
---|
564 | | _ ⇒ return st |
---|
565 | ]. |
---|
566 | |
---|
567 | definition eval_return ≝ |
---|
568 | λp : sem_params.λglobals : list ident.λge : genv p globals. |
---|
569 | λcurr_id.λcurr_ret : call_dest p. |
---|
570 | λst : state p. |
---|
571 | ! stack_size ← opt_to_res … [MSG MissingStackSize; CTX … curr_id] (stack_sizes … ge curr_id) ; |
---|
572 | ! 〈st', call_pc〉 ← pop_frame … ge curr_id curr_ret st ; |
---|
573 | ! nxt ← next_of_call_pc … ge call_pc ; |
---|
574 | let st'' ≝ set_last_pop … (decrement_stack_usage … stack_size st') call_pc in |
---|
575 | return |
---|
576 | next ? nxt st'' (* now address pushed on stack are calling ones! *). |
---|
577 | |
---|
578 | definition eval_tailcall ≝ |
---|
579 | λp : sem_params.λglobals : list ident.λge : genv p globals.λf,args,curr_f. |
---|
580 | λcurr_ret : call_dest p. |
---|
581 | λst : state_pc p. |
---|
582 | ! bl ← block_of_call … ge f st : IO ???; |
---|
583 | ! 〈i, fd〉 ← fetch_function … ge bl : IO ???; |
---|
584 | match fd with |
---|
585 | [ Internal ifd ⇒ |
---|
586 | ! stack_size ← opt_to_res … [MSG MissingStackSize; CTX … curr_f] (stack_sizes … ge curr_f) ; |
---|
587 | let st' ≝ decrement_stack_usage … stack_size st in |
---|
588 | ! st'' ← eval_internal_call p globals ge i ifd args st' ; |
---|
589 | let pc ≝ pc_of_point p bl (joint_if_entry … ifd) in |
---|
590 | return mk_state_pc … st'' pc (last_pop … st) |
---|
591 | | External efd ⇒ |
---|
592 | ! st' ← eval_external_call … efd args curr_ret st ; |
---|
593 | eval_return … ge curr_f curr_ret st |
---|
594 | ]. |
---|
595 | |
---|
596 | definition eval_statement_advance : |
---|
597 | ∀p:sem_params.∀globals.∀ge:genv p globals. |
---|
598 | ident → joint_closed_internal_function p globals → |
---|
599 | joint_statement p globals → state_pc p → |
---|
600 | IO io_out io_in (state_pc p) ≝ |
---|
601 | λp,g,ge,curr_id,curr_fn,s,st. |
---|
602 | match s return λ_.IO ??? with |
---|
603 | [ sequential s nxt ⇒ |
---|
604 | match s return λ_.IO ??? with |
---|
605 | [ COND a l ⇒ |
---|
606 | ! v ← acca_retrieve … st a ; |
---|
607 | ! b ← bool_of_beval … v ; |
---|
608 | if b then |
---|
609 | goto … ge l st |
---|
610 | else |
---|
611 | return next … nxt st |
---|
612 | | CALL f args dest ⇒ |
---|
613 | eval_call … ge f args dest nxt st |
---|
614 | | _ ⇒ return next … nxt st |
---|
615 | ] |
---|
616 | | final s ⇒ |
---|
617 | let curr_ret ≝ joint_if_result … curr_fn in |
---|
618 | match s with |
---|
619 | [ GOTO l ⇒ goto … ge l st |
---|
620 | | RETURN ⇒ eval_return … ge curr_id curr_ret st |
---|
621 | | TAILCALL _ f args ⇒ |
---|
622 | eval_tailcall … ge f args curr_id curr_ret st |
---|
623 | ] |
---|
624 | | FCOND _ a lbltrue lblfalse ⇒ |
---|
625 | ! v ← acca_retrieve … st a ; |
---|
626 | ! b ← bool_of_beval … v ; |
---|
627 | if b then |
---|
628 | goto … ge lbltrue st |
---|
629 | else |
---|
630 | goto … ge lblfalse st |
---|
631 | ]. |
---|
632 | |
---|
633 | definition eval_state : ∀p:sem_params. ∀globals: list ident. |
---|
634 | genv p globals → |
---|
635 | state_pc p → IO io_out io_in (state_pc p) ≝ |
---|
636 | λp,globals,ge,st. |
---|
637 | ! 〈id,fn,s〉 ← fetch_statement … ge (pc … st) : IO ???; |
---|
638 | ! st' ← eval_statement_no_pc … ge id s st : IO ???; |
---|
639 | let st'' ≝ set_no_pc … st' st in |
---|
640 | eval_statement_advance … ge id fn s st''. |
---|