1 | include "basics/lists/list.ma". |
---|
2 | include "joint/BEGlobalenvs.ma". |
---|
3 | include "common/IO.ma". |
---|
4 | include "common/SmallstepExec.ma". |
---|
5 | include "joint/Joint_paolo.ma". |
---|
6 | include "ASM/I8051bis.ma". |
---|
7 | |
---|
8 | (* CSC: external functions never fail (??) and always return something of the |
---|
9 | size of one register, both in the frontend and in the backend. |
---|
10 | Is this reasonable??? In OCaml it always return a list, but in the frontend |
---|
11 | only the head is kept (or Undef if the list is empty) ??? *) |
---|
12 | |
---|
13 | definition genv ≝ λglobals.λp:params. genv_t Genv (joint_function globals p). |
---|
14 | |
---|
15 | record sem_state_params : Type[1] ≝ |
---|
16 | { framesT: Type[0] |
---|
17 | ; empty_framesT: framesT |
---|
18 | ; regsT : Type[0] |
---|
19 | ; empty_regsT: address → regsT (* Stack pointer *) |
---|
20 | }. |
---|
21 | |
---|
22 | record state (semp: sem_state_params): Type[0] ≝ |
---|
23 | { st_frms: framesT semp |
---|
24 | ; pc: address |
---|
25 | ; sp: pointer |
---|
26 | ; isp: pointer |
---|
27 | ; carry: beval |
---|
28 | ; regs: regsT semp |
---|
29 | ; m: bemem |
---|
30 | }. |
---|
31 | |
---|
32 | definition set_m: ∀p. bemem → state p → state p ≝ |
---|
33 | λp,m,st. mk_state p (st_frms … st) (pc … st) (sp … st) (isp … st) (carry … st) (regs … st) m. |
---|
34 | |
---|
35 | definition set_regs: ∀p:sem_state_params. regsT p → state p → state p ≝ |
---|
36 | λp,regs,st. mk_state p (st_frms … st) (pc … st) (sp … st) (isp … st) (carry … st) regs (m … st). |
---|
37 | |
---|
38 | definition set_sp: ∀p. pointer → state p → state p ≝ |
---|
39 | λp,sp,st. mk_state … (st_frms … st) (pc … st) sp (isp … st) (carry … st) (regs … st) (m … st). |
---|
40 | |
---|
41 | definition set_isp: ∀p. pointer → state p → state p ≝ |
---|
42 | λp,isp,st. mk_state … (st_frms … st) (pc … st) (sp … st) isp (carry … st) (regs … st) (m … st). |
---|
43 | |
---|
44 | definition set_carry: ∀p. beval → state p → state p ≝ |
---|
45 | λp,carry,st. mk_state … (st_frms … st) (pc … st) (sp … st) (isp … st) carry (regs … st) (m … st). |
---|
46 | |
---|
47 | definition set_pc: ∀p. address → state p → state p ≝ |
---|
48 | λp,pc,st. mk_state … (st_frms … st) pc (sp … st) (isp … st) (carry … st) (regs … st) (m … st). |
---|
49 | |
---|
50 | definition set_frms: ∀p:sem_state_params. framesT p → state p → state p ≝ |
---|
51 | λp,frms,st. mk_state … frms (pc … st) (sp … st) (isp … st) (carry … st) (regs … st) (m … st). |
---|
52 | |
---|
53 | axiom BadProgramCounter : String. |
---|
54 | (* this can replace graph_fetch function and lin_fetch_function *) |
---|
55 | definition fetch_function: |
---|
56 | ∀pars : params. |
---|
57 | ∀globals. |
---|
58 | genv globals pars → |
---|
59 | pointer → |
---|
60 | res (joint_internal_function … pars) ≝ |
---|
61 | λpars,globals,ge,p. |
---|
62 | let b ≝ pblock p in |
---|
63 | do def ← opt_to_res ? [MSG BadProgramCounter] (find_funct_ptr … ge b) ; |
---|
64 | match def with |
---|
65 | [ Internal def' ⇒ OK … def' |
---|
66 | | External _ ⇒ Error … [MSG BadProgramCounter]]. |
---|
67 | |
---|
68 | record more_sem_unserialized_params (uns_pars : unserialized_params) : Type[1] ≝ |
---|
69 | { st_pars :> sem_state_params |
---|
70 | ; acca_store_ : acc_a_reg uns_pars → beval → regsT st_pars → res (regsT st_pars) |
---|
71 | ; acca_retrieve_ : regsT st_pars → acc_a_reg uns_pars → res beval |
---|
72 | ; acca_arg_retrieve_ : regsT st_pars → acc_a_arg uns_pars → res beval |
---|
73 | ; accb_store_ : acc_b_reg uns_pars → beval → regsT st_pars → res (regsT st_pars) |
---|
74 | ; accb_retrieve_ : regsT st_pars → acc_b_reg uns_pars → res beval |
---|
75 | ; accb_arg_retrieve_ : regsT st_pars → acc_b_arg uns_pars → res beval |
---|
76 | ; dpl_store_ : dpl_reg uns_pars → beval → regsT st_pars → res (regsT st_pars) |
---|
77 | ; dpl_retrieve_ : regsT st_pars → dpl_reg uns_pars → res beval |
---|
78 | ; dpl_arg_retrieve_ : regsT st_pars → dpl_arg uns_pars → res beval |
---|
79 | ; dph_store_ : dph_reg uns_pars → beval → regsT st_pars → res (regsT st_pars) |
---|
80 | ; dph_retrieve_ : regsT st_pars → dph_reg uns_pars → res beval |
---|
81 | ; dph_arg_retrieve_ : regsT st_pars → dph_arg uns_pars → res beval |
---|
82 | ; snd_arg_retrieve_ : regsT st_pars → snd_arg uns_pars → res beval |
---|
83 | ; pair_reg_move_ : regsT st_pars → pair_move uns_pars → res (regsT st_pars) |
---|
84 | ; fetch_ra: state st_pars → |
---|
85 | res ((state st_pars) × address) |
---|
86 | |
---|
87 | ; init_locals : localsT uns_pars → regsT st_pars → regsT st_pars |
---|
88 | (* Paolo: save_frame separated from call_setup to factorize tailcall code *) |
---|
89 | ; save_frame: address → call_dest uns_pars → state st_pars → state st_pars |
---|
90 | (*CSC: setup_call returns a res only because we can call a function with the wrong number and |
---|
91 | type of arguments. To be fixed using a dependent type *) |
---|
92 | ; setup_call : nat → paramsT … uns_pars → call_args uns_pars → |
---|
93 | state st_pars → res (state st_pars) |
---|
94 | ; fetch_external_args: external_function → state st_pars → |
---|
95 | res (list val) |
---|
96 | ; set_result: list val → state st_pars → |
---|
97 | res (state st_pars) |
---|
98 | ; call_args_for_main: call_args uns_pars |
---|
99 | ; call_dest_for_main: call_dest uns_pars |
---|
100 | }. |
---|
101 | |
---|
102 | |
---|
103 | definition helper_def_retrieve : |
---|
104 | ∀X : ? → ? → Type[0]. |
---|
105 | (∀up.∀p:more_sem_unserialized_params up. regsT p → X up p → res beval) → |
---|
106 | ∀up.∀p : more_sem_unserialized_params up.state p → X up p → res beval ≝ |
---|
107 | λX,f,up,p,st.f ? p (regs … st). |
---|
108 | |
---|
109 | definition helper_def_store : |
---|
110 | ∀X : ? → ? → Type[0]. |
---|
111 | (∀up.∀p : more_sem_unserialized_params up.X up p → beval → regsT p → res (regsT p)) → |
---|
112 | ∀up.∀p : more_sem_unserialized_params up.X up p → beval → state p → res (state p) ≝ |
---|
113 | λX,f,up,p,x,v,st.! r ← f ? p x v (regs … st) ; return (set_regs … r st). |
---|
114 | |
---|
115 | definition acca_retrieve ≝ helper_def_retrieve ? acca_retrieve_. |
---|
116 | definition acca_store ≝ helper_def_store ? acca_store_. |
---|
117 | definition acca_arg_retrieve ≝ helper_def_retrieve ? acca_arg_retrieve_. |
---|
118 | definition accb_store ≝ helper_def_store ? accb_store_. |
---|
119 | definition accb_retrieve ≝ helper_def_retrieve ? accb_retrieve_. |
---|
120 | definition accb_arg_retrieve ≝ helper_def_retrieve ? accb_arg_retrieve_. |
---|
121 | definition dpl_store ≝ helper_def_store ? dpl_store_. |
---|
122 | definition dpl_retrieve ≝ helper_def_retrieve ? dpl_retrieve_. |
---|
123 | definition dpl_arg_retrieve ≝ helper_def_retrieve ? dpl_arg_retrieve_. |
---|
124 | definition dph_store ≝ helper_def_store ? dph_store_. |
---|
125 | definition dph_retrieve ≝ helper_def_retrieve ? dph_retrieve_. |
---|
126 | definition dph_arg_retrieve ≝ helper_def_retrieve ? dph_arg_retrieve_. |
---|
127 | definition snd_arg_retrieve ≝ helper_def_retrieve ? snd_arg_retrieve_. |
---|
128 | definition pair_reg_move : ?→?→?→?→res ? ≝ |
---|
129 | λup.λp : more_sem_unserialized_params up.λst : state p.λpm : pair_move up. |
---|
130 | ! r ← pair_reg_move_ ? p (regs ? st) pm; |
---|
131 | return (set_regs ? r st). |
---|
132 | |
---|
133 | axiom BadPointer : String. |
---|
134 | |
---|
135 | (* this is preamble to all calls (including tail ones). The optional argument in |
---|
136 | input tells the function whether it has to save the frame for internal |
---|
137 | calls. |
---|
138 | the first element of the triple is the label at the start of the function |
---|
139 | in case of an internal call, or None in case of an external one. |
---|
140 | The actual update of the pc is left to later, as it depends on |
---|
141 | serialization and on whether the call is a tail one. *) |
---|
142 | definition eval_call_block_preamble: |
---|
143 | ∀globals.∀p : params.∀p':more_sem_unserialized_params p. |
---|
144 | genv globals p → state p' → block → call_args p → option ((call_dest p) × address) → |
---|
145 | IO io_out io_in ((option label)×trace×(state p')) ≝ |
---|
146 | λglobals,p,p',ge,st,b,args,dest_ra. |
---|
147 | ! fd ← (opt_to_res ? [MSG BadPointer] (find_funct_ptr ?? ge b) : IO ? io_in ?); |
---|
148 | match fd with |
---|
149 | [ Internal fn ⇒ |
---|
150 | let st ≝ match dest_ra with |
---|
151 | [ Some p ⇒ let 〈dest, ra〉 ≝ p in save_frame … ra dest st |
---|
152 | | None ⇒ st |
---|
153 | ] in |
---|
154 | ! st ← setup_call … (joint_if_stacksize … fn) (joint_if_params … fn) |
---|
155 | args st ; |
---|
156 | let regs ≝ init_locals … (joint_if_locals … fn) (regs … st) in |
---|
157 | let l' ≝ joint_if_entry … fn in |
---|
158 | let st ≝ set_regs p' regs st in |
---|
159 | return 〈Some label l', E0, st〉 |
---|
160 | | External fn ⇒ |
---|
161 | ! params ← fetch_external_args … p' fn st : IO ???; |
---|
162 | ! evargs ← check_eventval_list params (sig_args (ef_sig fn)) : IO ???; |
---|
163 | ! evres ← do_io (ef_id fn) evargs (proj_sig_res (ef_sig fn)); |
---|
164 | (* CSC: XXX bug here; I think I should split it into Byte-long |
---|
165 | components; instead I am making a singleton out of it. To be |
---|
166 | fixed once we fully implement external functions. *) |
---|
167 | let vs ≝ [mk_val ? evres] in |
---|
168 | ! st ← set_result … p' vs st : IO ???; |
---|
169 | return 〈None ?, Eextcall (ef_id fn) evargs (mk_eventval ? evres), st〉 |
---|
170 | ]. |
---|
171 | |
---|
172 | axiom FailedStore: String. |
---|
173 | |
---|
174 | definition push: ∀p. state p → beval → res (state p) ≝ |
---|
175 | λp,st,v. |
---|
176 | let isp ≝ isp … st in |
---|
177 | do m ← opt_to_res … (msg FailedStore) (bestorev (m … st) isp v); |
---|
178 | let isp ≝ shift_pointer … isp [[false;false;false;false;false;false;false;true]] in |
---|
179 | OK … (set_m … m (set_isp … isp st)). |
---|
180 | |
---|
181 | definition pop: ∀p. state p → res (state p × beval) ≝ |
---|
182 | λp,st. |
---|
183 | let isp ≝ isp ? st in |
---|
184 | let isp ≝ neg_shift_pointer ? isp [[false;false;false;false;false;false;false;true]] in |
---|
185 | let ist ≝ set_isp … isp st in |
---|
186 | do v ← opt_to_res ? (msg FailedStore) (beloadv (m ? st) isp); |
---|
187 | OK ? 〈st,v〉. |
---|
188 | |
---|
189 | definition save_ra : ∀p. state p → address → res (state p) ≝ |
---|
190 | λp,st,l. |
---|
191 | let 〈addrl,addrh〉 ≝ l in |
---|
192 | do st ← push … st addrl; |
---|
193 | push … st addrh. |
---|
194 | |
---|
195 | definition load_ra : ∀p.state p → res (state p × address) ≝ |
---|
196 | λp,st. |
---|
197 | do 〈st,addrh〉 ← pop … st; |
---|
198 | do 〈st,addrl〉 ← pop … st; |
---|
199 | OK ? 〈st, 〈addrl,addrh〉〉. |
---|
200 | |
---|
201 | |
---|
202 | (* parameters that need full params to have type of functions, |
---|
203 | but are still independent of serialization |
---|
204 | Paolo: the first element returned by exec extended is None if flow is |
---|
205 | left to regular sequential one, otherwise a label. |
---|
206 | The address input is the address of the next statement, to be provided to |
---|
207 | accomodate extensions that make calls. *) |
---|
208 | record more_sem_genv_params (pp : params) : Type[1] ≝ |
---|
209 | { msu_pars :> more_sem_unserialized_params pp |
---|
210 | ; read_result: ∀globals.genv globals pp → state msu_pars → res (list beval) |
---|
211 | ; exec_extended: ∀globals.genv globals pp → ext_instruction pp → |
---|
212 | state msu_pars → address → IO io_out io_in ((option label)× trace × (state msu_pars)) |
---|
213 | ; exec_fin_extended: ∀globals.genv globals pp → ext_fin_instruction pp → |
---|
214 | state msu_pars → IO io_out io_in (trace × (state msu_pars)) |
---|
215 | ; pop_frame: ∀globals.genv globals pp → state msu_pars → res (state msu_pars) |
---|
216 | }. |
---|
217 | |
---|
218 | |
---|
219 | (* parameters that are defined by serialization *) |
---|
220 | record more_sem_params (pp : params) : Type[1] ≝ |
---|
221 | { msg_pars :> more_sem_genv_params pp |
---|
222 | ; succ_pc: succ pp → address → res address |
---|
223 | ; pointer_of_label: ∀globals.genv globals pp → pointer → label → res (Σp:pointer. ptype p = Code) |
---|
224 | ; fetch_statement: ∀globals.genv globals pp → state msg_pars → res (joint_statement pp globals) |
---|
225 | }. |
---|
226 | |
---|
227 | record sem_params : Type[1] ≝ |
---|
228 | { spp :> params |
---|
229 | ; more_sem_pars :> more_sem_params spp |
---|
230 | }. |
---|
231 | |
---|
232 | definition address_of_label: ∀globals. ∀p:sem_params. |
---|
233 | genv globals p → pointer → label → res address ≝ |
---|
234 | λglobals,p,ge,ptr,l. |
---|
235 | do newptr ← pointer_of_label … p ? ge … ptr l ; |
---|
236 | OK … (address_of_code_pointer newptr). |
---|
237 | |
---|
238 | definition goto: ∀globals. ∀p:sem_params. |
---|
239 | genv globals p → label → state p → res (state p) ≝ |
---|
240 | λglobals,p,ge,l,st. |
---|
241 | ! oldpc ← pointer_of_address (pc … st); |
---|
242 | ! newpc ← address_of_label … ge oldpc l ; |
---|
243 | OK (state p) (set_pc … newpc st). |
---|
244 | |
---|
245 | (* |
---|
246 | definition empty_state: ∀p. more_sem_params p → state p ≝ |
---|
247 | mk_state … (empty_framesT …) |
---|
248 | *) |
---|
249 | |
---|
250 | definition next: ∀p:sem_params. succ … p → state p → res (state p) ≝ |
---|
251 | λp,l,st. |
---|
252 | ! l' ← succ_pc … p l (pc … st) ; |
---|
253 | OK … (set_pc … l' st). |
---|
254 | |
---|
255 | axiom MissingSymbol : String. |
---|
256 | axiom FailedLoad : String. |
---|
257 | axiom BadFunction : String. |
---|
258 | |
---|
259 | definition eval_call_block: |
---|
260 | ∀globals.∀p:sem_params. genv globals p → state p → |
---|
261 | block → call_args p → call_dest p → address → IO io_out io_in (trace×(state p)) ≝ |
---|
262 | λglobals,p,ge,st,b,args,dest,ra. |
---|
263 | ! 〈next, tr, st〉 ← eval_call_block_preamble … ge st b args (Some ? 〈dest,ra〉) ; |
---|
264 | ! new_pc ← match next with |
---|
265 | [ Some lbl ⇒ |
---|
266 | let pointer_in_fn ≝ mk_pointer Code (mk_block Code (block_id b)) ? (mk_offset 0) in |
---|
267 | address_of_label globals p ge pointer_in_fn lbl |
---|
268 | | None ⇒ return ra |
---|
269 | ] ; |
---|
270 | let st ≝ set_pc … new_pc st in |
---|
271 | return 〈tr, st〉. |
---|
272 | % qed. |
---|
273 | |
---|
274 | definition eval_call_id: |
---|
275 | ∀globals.∀p:sem_params. genv globals p → state p → |
---|
276 | ident → call_args p → call_dest p → address → IO io_out io_in (trace×(state p)) ≝ |
---|
277 | λglobals,p,ge,st,id,args,dest,ra. |
---|
278 | ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol ?? ge id) : IO ???; |
---|
279 | eval_call_block … ge st b args dest ra. |
---|
280 | |
---|
281 | |
---|
282 | (* defining because otherwise typechecker stalls *) |
---|
283 | definition eval_address : ∀globals.∀p : sem_params. genv globals p → state p → |
---|
284 | ∀i : ident.member i (eq_identifier SymbolTag) globals |
---|
285 | →dpl_reg p→dph_reg p→ succ p → res (trace × (state p)) ≝ |
---|
286 | λglobals,p,ge,st,ident,prf,ldest,hdest,l. |
---|
287 | let addr ≝ opt_safe ? (find_symbol ?? ge ident) ? in |
---|
288 | ! 〈laddr,haddr〉 ← address_of_pointer (mk_pointer (block_region addr) addr ? zero_offset) ; |
---|
289 | ! st ← dpl_store … ldest laddr st; |
---|
290 | ! st ← dph_store … hdest haddr st; |
---|
291 | ! st ← next … p l st ; |
---|
292 | return 〈E0, st〉. |
---|
293 | [ cases addr // |
---|
294 | | (* TODO: to prove *) |
---|
295 | elim daemon |
---|
296 | ] qed. |
---|
297 | |
---|
298 | (* defining because otherwise typechecker stalls *) |
---|
299 | definition eval_pop : ∀globals.∀p : sem_params. genv globals p → state p → |
---|
300 | acc_a_reg p → succ p → res (trace × (state p)) ≝ |
---|
301 | λglobals,p,ge,st,dst,l. |
---|
302 | ! 〈st,v〉 ← pop p st; |
---|
303 | ! st ← acca_store p p dst v st; |
---|
304 | ! st ← next p l st ; |
---|
305 | return 〈E0, st〉. |
---|
306 | |
---|
307 | (* defining because otherwise typechecker stalls *) |
---|
308 | definition eval_sequential : |
---|
309 | ∀globals.∀p:sem_params. genv globals p → state p → |
---|
310 | joint_instruction p globals → succ p → IO io_out io_in (trace×(state p)) ≝ |
---|
311 | λglobals,p,ge,st,seq,l. |
---|
312 | match seq with |
---|
313 | [ extension c ⇒ |
---|
314 | ! next_addr ← succ_pc … p l (pc … st) : IO ? ? ? ; |
---|
315 | ! 〈next_pc, tr, st〉 ← exec_extended … ge c st next_addr; |
---|
316 | ! st ← match next_pc with |
---|
317 | [ None ⇒ next … p l st |
---|
318 | | Some lbl ⇒ goto … ge lbl st |
---|
319 | ] ; |
---|
320 | return 〈tr, st〉 |
---|
321 | | COST_LABEL cl ⇒ |
---|
322 | ! st ← next … p l st ; |
---|
323 | return 〈Echarge cl, st〉 |
---|
324 | | COMMENT c ⇒ |
---|
325 | ! st ← next … p l st ; |
---|
326 | return 〈E0, st〉 |
---|
327 | | LOAD dst addrl addrh ⇒ |
---|
328 | ! vaddrh ← dph_arg_retrieve … st addrh ; |
---|
329 | ! vaddrl ← dpl_arg_retrieve … st addrl; |
---|
330 | ! vaddr ← pointer_of_address 〈vaddrl,vaddrh〉; |
---|
331 | ! v ← opt_to_res … (msg FailedLoad) (beloadv (m … st) vaddr); |
---|
332 | ! st ← acca_store p … dst v st ; |
---|
333 | ! st ← next … p l st ; |
---|
334 | return 〈E0, st〉 |
---|
335 | | STORE addrl addrh src ⇒ |
---|
336 | ! vaddrh ← dph_arg_retrieve … st addrh; |
---|
337 | ! vaddrl ← dpl_arg_retrieve … st addrl; |
---|
338 | ! vaddr ← pointer_of_address 〈vaddrl,vaddrh〉; |
---|
339 | ! v ← acca_arg_retrieve … st src; |
---|
340 | ! m' ← opt_to_res … (msg FailedStore) (bestorev (m … st) vaddr v); |
---|
341 | let st ≝ set_m … m' st in |
---|
342 | ! st ← next … p l st ; |
---|
343 | return 〈E0, st〉 |
---|
344 | | COND src ltrue ⇒ |
---|
345 | ! v ← acca_retrieve … st src; |
---|
346 | ! b ← bool_of_beval v; |
---|
347 | if b then |
---|
348 | ! st ← goto … p ge ltrue st ; |
---|
349 | return 〈E0, st〉 |
---|
350 | else |
---|
351 | ! st ← next … p l st ; |
---|
352 | return 〈E0, st〉 |
---|
353 | | ADDRESS ident prf ldest hdest ⇒ |
---|
354 | eval_address … ge st ident prf ldest hdest l |
---|
355 | | OP1 op dacc_a sacc_a ⇒ |
---|
356 | ! v ← acca_retrieve … st sacc_a; |
---|
357 | ! v ← Byte_of_val v; |
---|
358 | let v' ≝ BVByte (op1 eval op v) in |
---|
359 | ! st ← acca_store … dacc_a v' st; |
---|
360 | ! st ← next … l st ; |
---|
361 | return 〈E0, st〉 |
---|
362 | | OP2 op dacc_a sacc_a src ⇒ |
---|
363 | ! v1 ← acca_arg_retrieve … st sacc_a; |
---|
364 | ! v1 ← Byte_of_val v1; |
---|
365 | ! v2 ← snd_arg_retrieve … st src; |
---|
366 | ! v2 ← Byte_of_val v2; |
---|
367 | ! carry ← bool_of_beval (carry … st); |
---|
368 | let 〈v',carry〉 ≝ op2 eval carry op v1 v2 in |
---|
369 | let v' ≝ BVByte v' in |
---|
370 | let carry ≝ beval_of_bool carry in |
---|
371 | ! st ← acca_store … dacc_a v' st; |
---|
372 | let st ≝ set_carry … carry st in |
---|
373 | ! st ← next … l st ; |
---|
374 | return 〈E0, st〉 |
---|
375 | | CLEAR_CARRY ⇒ |
---|
376 | ! st ← next … l (set_carry … BVfalse st) ; |
---|
377 | return 〈E0, st〉 |
---|
378 | | SET_CARRY ⇒ |
---|
379 | ! st ← next … l (set_carry … BVtrue st) ; |
---|
380 | return 〈E0, st〉 |
---|
381 | | OPACCS op dacc_a_reg dacc_b_reg sacc_a_reg sacc_b_reg ⇒ |
---|
382 | ! v1 ← acca_arg_retrieve … st sacc_a_reg; |
---|
383 | ! v1 ← Byte_of_val v1; |
---|
384 | ! v2 ← accb_arg_retrieve … st sacc_b_reg; |
---|
385 | ! v2 ← Byte_of_val v2; |
---|
386 | let 〈v1',v2'〉 ≝ opaccs eval op v1 v2 in |
---|
387 | let v1' ≝ BVByte v1' in |
---|
388 | let v2' ≝ BVByte v2' in |
---|
389 | ! st ← acca_store … dacc_a_reg v1' st; |
---|
390 | ! st ← accb_store … dacc_b_reg v2' st; |
---|
391 | ! st ← next … l st ; |
---|
392 | return 〈E0, st〉 |
---|
393 | | POP dst ⇒ |
---|
394 | eval_pop … ge st dst l |
---|
395 | | PUSH src ⇒ |
---|
396 | ! v ← acca_arg_retrieve … st src; |
---|
397 | ! st ← push … st v; |
---|
398 | ! st ← next … l st ; |
---|
399 | return 〈E0, st〉 |
---|
400 | | MOVE dst_src ⇒ |
---|
401 | ! st ← pair_reg_move … st dst_src ; |
---|
402 | ! st ← next … l st ; |
---|
403 | return 〈E0, st〉 |
---|
404 | | CALL_ID id args dest ⇒ |
---|
405 | ! ra ← succ_pc … p l (pc … st) : IO ??? ; |
---|
406 | eval_call_id … ge st id args dest ra |
---|
407 | ]. |
---|
408 | |
---|
409 | definition eval_statement : ∀globals: list ident.∀p:sem_params. genv globals p → |
---|
410 | state p → IO io_out io_in (trace × (state p)) ≝ |
---|
411 | λglobals,p,ge,st. |
---|
412 | ! s ← fetch_statement … ge st : IO ???; |
---|
413 | match s return λ_.IO io_out io_in (trace × (state p)) with |
---|
414 | [ GOTO l ⇒ |
---|
415 | ! st ← goto … ge l st ; |
---|
416 | return 〈E0, st〉 |
---|
417 | | RETURN ⇒ |
---|
418 | ! 〈st,ra〉 ← fetch_ra … st ; |
---|
419 | ! st ← pop_frame … ge st; |
---|
420 | return 〈E0,set_pc … ra st〉 |
---|
421 | | sequential seq l ⇒ eval_sequential … ge st seq l |
---|
422 | | extension_fin c ⇒ exec_fin_extended … ge c st |
---|
423 | ]. |
---|
424 | |
---|
425 | definition is_final: ∀globals:list ident. ∀p: sem_params. |
---|
426 | genv globals p → address → state p → option int ≝ |
---|
427 | λglobals,p,ge,exit,st.res_to_opt ? ( |
---|
428 | do s ← fetch_statement … ge st; |
---|
429 | match s with |
---|
430 | [ RETURN ⇒ |
---|
431 | do 〈st,ra〉 ← fetch_ra … st; |
---|
432 | if eq_address ra exit then |
---|
433 | do vals ← read_result … ge st ; |
---|
434 | Word_of_list_beval vals |
---|
435 | else |
---|
436 | Error ? [ ] |
---|
437 | | _ ⇒ Error ? [ ]]). |
---|
438 | |
---|
439 | record evaluation_parameters : Type[1] ≝ |
---|
440 | { globals: list ident |
---|
441 | ; sparams:> sem_params |
---|
442 | ; exit: address |
---|
443 | ; genv2: genv globals sparams |
---|
444 | }. |
---|
445 | |
---|
446 | definition joint_exec: trans_system io_out io_in ≝ |
---|
447 | mk_trans_system … evaluation_parameters (λG. state G) |
---|
448 | (λG.is_final (globals G) G (genv2 G) (exit G)) |
---|
449 | (λG.eval_statement (globals G) G (genv2 G)). |
---|
450 | |
---|
451 | definition make_global : |
---|
452 | ∀pars: sem_params. |
---|
453 | joint_program pars → evaluation_parameters |
---|
454 | ≝ |
---|
455 | λpars. |
---|
456 | (* Invariant: a -1 block is unused in common/Globalenvs *) |
---|
457 | let b ≝ mk_block Code (-1) in |
---|
458 | let ptr ≝ mk_pointer Code b ? (mk_offset 0) in |
---|
459 | let addr ≝ address_of_code_pointer ptr in |
---|
460 | (λp. mk_evaluation_parameters |
---|
461 | (prog_var_names … p) |
---|
462 | (mk_sem_params … pars) |
---|
463 | addr |
---|
464 | (globalenv Genv … p) |
---|
465 | ). |
---|
466 | % qed. |
---|
467 | |
---|
468 | axiom ExternalMain: String. |
---|
469 | |
---|
470 | definition make_initial_state : |
---|
471 | ∀pars: sem_params. |
---|
472 | ∀p: joint_program … pars. res (state pars) ≝ |
---|
473 | λpars,p. |
---|
474 | let sem_globals ≝ make_global pars p in |
---|
475 | let ge ≝ genv2 sem_globals in |
---|
476 | let m ≝ init_mem Genv … p in |
---|
477 | let 〈m,spb〉 ≝ alloc … m 0 external_ram_size XData in |
---|
478 | let 〈m,ispb〉 ≝ alloc … m 0 internal_ram_size XData in |
---|
479 | let dummy_pc ≝ mk_pointer Code (mk_block Code (-1)) ? (mk_offset 0) in |
---|
480 | let spp ≝ mk_pointer XData spb ? (mk_offset external_ram_size) in |
---|
481 | let ispp ≝ mk_pointer XData ispb ? (mk_offset 47) in |
---|
482 | do sp ← address_of_pointer spp ; |
---|
483 | let main ≝ prog_main … p in |
---|
484 | let st0 ≝ mk_state … (empty_framesT …) sp ispp dummy_pc BVfalse (empty_regsT … sp) m in |
---|
485 | let trace_state ≝ |
---|
486 | eval_call_id … pars ge st0 main (call_args_for_main … pars) |
---|
487 | (call_dest_for_main … pars) (exit sem_globals) in |
---|
488 | match trace_state with |
---|
489 | [ Value tr_st ⇒ OK … (\snd tr_st) (* E0 trace thrown away *) |
---|
490 | | Wrong msg ⇒ Error … msg |
---|
491 | | Interact _ _ ⇒ Error … [MSG ExternalMain] (* External main not supported: why? *) |
---|
492 | ]. |
---|
493 | [3: % | cases ispb | cases spb] * #r #off #E >E % |
---|
494 | qed. |
---|
495 | |
---|
496 | definition joint_fullexec : |
---|
497 | ∀pars:sem_params.fullexec io_out io_in ≝ |
---|
498 | λpars.mk_fullexec ??? joint_exec (make_global pars) (make_initial_state pars). |
---|