source: src/joint/semantics.ma @ 2491

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

fixed wrt change of list member definition

File size: 26.0 KB
Line 
1include "common/Globalenvs.ma".
2include "common/IO.ma".
3(* include "common/SmallstepExec.ma". *)
4include "joint/BEMem.ma".
5include "joint/Joint.ma".
6include "ASM/I8051bis.ma".
7include "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 *)
15record 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 : (Σi.is_internal_function ? ge i) → ℕ
19}.
20
21definition stack_sizes_lift :
22∀pars_in, pars_out : params.
23∀trans : ∀globals.joint_closed_internal_function pars_in globals →
24                  joint_closed_internal_function pars_out globals.
25∀prog_in : program (joint_function pars_in) ℕ.
26let prog_out ≝
27  transform_program … prog_in (λglobals.transf_fundef ?? (trans globals)) in
28((Σi.is_internal_function_of_program … prog_out i) → ℕ) →
29((Σi.is_internal_function_of_program … prog_in i) → ℕ) ≝
30λpars_in,pars_out,prog_in,trans,stack_sizes.
31λi.stack_sizes «i, if_propagate … (pi2 … i)».
32
33definition genv ≝ λp.genv_gen (joint_closed_internal_function p).
34coercion genv_to_genv_t :
35  ∀p,globals.∀g : genv p globals.genv_t (joint_function p globals) ≝
36  λp,globals,g.ge ?? g on _g : genv ?? to genv_t ?.
37
38record sem_state_params : Type[1] ≝
39 { framesT: Type[0]
40 ; empty_framesT: framesT
41 ; regsT : Type[0]
42 ; empty_regsT: xpointer → regsT (* initial stack pointer *)
43 ; load_sp : regsT → res xpointer
44 ; save_sp : regsT → xpointer → regsT
45 }.
46
47inductive internal_stack : Type[0] ≝
48| empty_is : internal_stack
49| one_is : beval → internal_stack
50| both_is : beval → beval → internal_stack.
51
52axiom InternalStackFull : String.
53axiom InternalStackEmpty : String.
54
55definition is_push : internal_stack → beval → res internal_stack ≝
56λis,bv.match is with
57[ empty_is ⇒ return one_is bv
58| one_is bv' ⇒ return both_is bv' bv
59| both_is _ _ ⇒ Error … [MSG … InternalStackFull]
60].
61
62definition is_pop : internal_stack → res (beval × internal_stack) ≝
63λis.match is with
64[ empty_is ⇒ Error … [MSG … InternalStackEmpty]
65| one_is bv' ⇒ return 〈bv', empty_is〉
66| both_is bv bv' ⇒ return 〈bv', one_is bv〉
67].
68
69record state (semp: sem_state_params): Type[0] ≝
70 { st_frms: framesT semp
71 ; istack : internal_stack
72 ; carry: bebit
73 ; regs: regsT semp
74 ; m: bemem
75 }.
76
77definition sp ≝ λp,st.load_sp p (regs ? st).
78
79record state_pc (semp : sem_state_params) : Type[0] ≝
80  { st_no_pc :> state semp
81  ; pc : program_counter
82  }.
83
84definition set_m: ∀p. bemem → state p → state p ≝
85 λp,m,st. mk_state p (st_frms …st) (istack … st) (carry … st) (regs … st) m.
86
87definition set_regs: ∀p:sem_state_params. regsT p → state p → state p ≝
88 λp,regs,st.mk_state p (st_frms … st) (istack … st) (carry … st) regs (m … st).
89
90definition set_sp: ∀p. ? → state p → state p ≝
91 λp,sp,st.let regs' ≝ save_sp … (regs … st) sp in
92 mk_state p (st_frms … st) (istack … st) (carry … st) regs' (m … st).
93
94definition set_carry: ∀p. bebit → state p → state p ≝
95 λp,carry,st. mk_state … (st_frms … st) (istack … st) carry (regs … st) (m … st).
96
97definition set_istack: ∀p. internal_stack → state p → state p ≝
98 λp,is,st. mk_state … (st_frms … st) is (carry … st) (regs … st) (m … st).
99
100definition set_pc: ∀p. ? → state_pc p → state_pc p ≝
101 λp,pc,st. mk_state_pc … (st_no_pc … st) pc.
102
103definition set_no_pc: ∀p. ? → state_pc p → state_pc p ≝
104 λp,s,st. mk_state_pc … s (pc … st).
105
106definition set_frms: ∀p:sem_state_params. framesT p → state p → state p ≝
107 λp,frms,st. mk_state … frms (istack … st) (carry … st) (regs … st) (m … st).
108
109axiom BadProgramCounter : String.
110
111(*
112inductive step_flow (p : unserialized_params) (F : Type[0]) : possible_flows → Type[0] ≝
113  | Redirect : ∀lbls.(Σl.In ? lbls l) → step_flow p F (Labels lbls) (* used for goto-like flow alteration *)
114  | Init     : Z → F → call_args p → call_dest p → step_flow p F Call (* call a function with given id, then proceed *)
115  | Proceed  : ∀flows.step_flow p F flows. (* go to implicit successor *)
116
117inductive fin_step_flow (p : unserialized_params) (F : Type[0]) : possible_flows → Type[0] ≝
118  | FRedirect : ∀lbls.(Σl.In ? lbls l) → fin_step_flow p F (Labels lbls)
119  | FTailInit : Z → F → call_args p → fin_step_flow p F Call
120  | FEnd1  : fin_step_flow p F (Labels [ ]) (* end flow *)
121  | FEnd2  : fin_step_flow p F Call. (* end flow *)
122*)
123
124(* bevals hold a function pointer (BVptr) *)
125definition funct_of_bevals : ∀F,ge.
126  beval → beval → option (Σi.is_function F ge i) ≝
127λF,ge,dpl,dph.
128! ptr ← res_to_opt … (pointer_of_address 〈dpl, dph〉) ;
129if eq_bv … (bv_zero …) (offv (poff ptr)) ∧ (* ← check this condition in front end *)
130   match ptype ptr with [ Code ⇒ true | _ ⇒ false] then (* ← already checked in funct_of_block? *)
131   funct_of_block … (pblock ptr)
132else None ?.
133
134axiom ProgramCounterOutOfCode : String.
135axiom PointNotFound : String.
136axiom LabelNotFound : String.
137axiom MissingSymbol : String.
138axiom FailedLoad : String.
139axiom BadFunction : String.
140axiom SuccessorNotProvided : String.
141axiom BadPointer : String.
142
143(* this can replace graph_fetch function and lin_fetch_function *)
144definition fetch_function:
145 ∀F.
146 ∀ge : genv_t (fundef F).
147  program_counter →
148  res (Σi.is_internal_function … ge i) ≝
149 λpars,ge,p.
150 opt_to_res … [MSG BadFunction; MSG BadPointer]
151    (int_funct_of_block … ge (pc_block p)).
152
153record sem_unserialized_params
154  (uns_pars : unserialized_params)
155  (F : list ident → Type[0]) : Type[1] ≝
156  { st_pars :> sem_state_params
157
158  ; acca_store_ : acc_a_reg uns_pars → beval → regsT st_pars → res (regsT st_pars)
159  ; acca_retrieve_ : regsT st_pars → acc_a_reg uns_pars → res beval
160  ; acca_arg_retrieve_ : regsT st_pars → acc_a_arg uns_pars → res beval
161  ; accb_store_ : acc_b_reg uns_pars → beval → regsT st_pars → res (regsT st_pars)
162  ; accb_retrieve_ : regsT st_pars → acc_b_reg uns_pars → res beval
163  ; accb_arg_retrieve_ : regsT st_pars → acc_b_arg uns_pars → res beval
164  ; dpl_store_ : dpl_reg uns_pars → beval → regsT st_pars → res (regsT st_pars)
165  ; dpl_retrieve_ : regsT st_pars → dpl_reg uns_pars → res beval
166  ; dpl_arg_retrieve_ : regsT st_pars → dpl_arg uns_pars → res beval
167  ; dph_store_ : dph_reg uns_pars → beval → regsT st_pars → res (regsT st_pars)
168  ; dph_retrieve_ : regsT st_pars → dph_reg uns_pars → res beval
169  ; dph_arg_retrieve_ : regsT st_pars → dph_arg uns_pars → res beval
170  ; snd_arg_retrieve_ : regsT st_pars → snd_arg uns_pars → res beval
171  ; pair_reg_move_ : regsT st_pars → pair_move uns_pars → res (regsT st_pars)
172
173  ; allocate_locals_ : localsT uns_pars → regsT st_pars → regsT st_pars
174  (* Paolo: save_frame separated from call_setup to factorize tailcall code *)
175  ; save_frame: call_dest uns_pars → state_pc st_pars → res (state st_pars)
176   (*CSC: setup_call returns a res only because we can call a function with the wrong number and
177     type of arguments. To be fixed using a dependent type *)
178  ; setup_call : nat → paramsT … uns_pars → call_args uns_pars →
179      state st_pars → res (state st_pars)
180  ; fetch_external_args: external_function → state st_pars → call_args … uns_pars →
181      res (list val)
182  ; set_result: list val → call_dest uns_pars → state st_pars → res (state st_pars)
183  ; call_args_for_main: call_args uns_pars
184  ; call_dest_for_main: call_dest uns_pars
185
186  (* from now on, parameters that use the type of functions *)
187  ; read_result: ∀globals.genv_gen F globals → call_dest uns_pars → state st_pars → res (list beval)
188  ; eval_ext_seq: ∀globals.∀ge : genv_gen F globals.ext_seq uns_pars →
189    (Σi.is_internal_function … ge i) (* current *) → state st_pars → IO io_out io_in (state st_pars)
190  ; pop_frame: ∀globals.∀ge : genv_gen F globals.
191    (Σi.is_internal_function … ge i) (* current *) → state st_pars → res (state_pc st_pars)
192  }.
193
194definition allocate_locals :
195  ∀p,F.∀sup : sem_unserialized_params p F.
196  list (localsT p) → state sup → state sup ≝
197  λp,F,sup,l,st.
198  let r ≝ foldr … (allocate_locals_ … sup) (regs … st) l in
199  set_regs … r st.
200
201definition helper_def_retrieve :
202  ∀X : ? → ? → ? → Type[0].
203  (∀up,F.∀p:sem_unserialized_params up F. regsT (st_pars up F p) → X up F p → res beval) →
204  ∀up,F.∀p : sem_unserialized_params up F.state (st_pars up F p) → X up F p → res beval ≝
205    λX,f,up,F,p,st.f ?? p (regs … st).
206
207definition helper_def_store :
208  ∀X : ? → ? → ? → Type[0].
209  (∀up,F.∀p : sem_unserialized_params up F.X up F p → beval → regsT (st_pars … p) → res (regsT (st_pars … p))) →
210  ∀up,F.∀p : sem_unserialized_params up F.X up F p → beval → state (st_pars … p) → res (state (st_pars … p)) ≝
211  λX,f,up,F,p,x,v,st.! r ← f ?? p x v (regs … st) ; return set_regs … r st.
212
213definition acca_retrieve ≝ helper_def_retrieve ? acca_retrieve_.
214definition acca_store ≝ helper_def_store ? acca_store_.
215definition acca_arg_retrieve ≝ helper_def_retrieve ? acca_arg_retrieve_.
216definition accb_store ≝ helper_def_store ? accb_store_.
217definition accb_retrieve ≝ helper_def_retrieve ? accb_retrieve_.
218definition accb_arg_retrieve ≝ helper_def_retrieve ? accb_arg_retrieve_.
219definition dpl_store ≝ helper_def_store ? dpl_store_.
220definition dpl_retrieve ≝ helper_def_retrieve ? dpl_retrieve_.
221definition dpl_arg_retrieve ≝ helper_def_retrieve ? dpl_arg_retrieve_.
222definition dph_store ≝ helper_def_store ? dph_store_.
223definition dph_retrieve ≝ helper_def_retrieve ? dph_retrieve_.
224definition dph_arg_retrieve ≝ helper_def_retrieve ? dph_arg_retrieve_.
225definition snd_arg_retrieve ≝ helper_def_retrieve ? snd_arg_retrieve_.
226definition pair_reg_move ≝
227  λup,F.λp : sem_unserialized_params up F.λst : state (st_pars … p).λpm : pair_move up.
228    ! r ← pair_reg_move_ ?? p (regs ? st) pm;
229    return set_regs ? r st.
230 
231axiom FailedStore: String.
232
233definition push: ∀p.state p → beval → res (state p) ≝
234 λp,st,v.
235 ! is ← is_push (istack … st) v ;
236 return set_istack … is st.
237
238definition pop: ∀p. state p → res (beval × (state p)) ≝
239 λp,st.
240 ! 〈bv, is〉 ← is_pop (istack … st) ;
241 return 〈bv, set_istack … is st〉.
242
243definition save_ra : ∀p. state p → program_counter → res (state p) ≝
244 λp,st,l.
245  let 〈addrl,addrh〉 ≝  beval_pair_of_pc l in
246  ! st' ← push … st addrl;
247  push … st' addrh.
248
249definition load_ra : ∀p.state p → res (program_counter × (state p)) ≝
250 λp,st.
251  ! 〈addrh, st'〉 ← pop … st;
252  ! 〈addrl, st''〉 ← pop … st';
253  ! pr ← pc_of_bevals [addrh; addrl];
254  return 〈pr, st''〉.
255
256(* parameters that are defined by serialization *)
257record more_sem_params (pp : params) : Type[1] ≝
258  { msu_pars :> sem_unserialized_params pp (joint_closed_internal_function pp)
259  ; offset_of_point : code_point pp → Pos
260  ; point_of_offset : Pos → code_point pp
261  ; point_of_offset_of_point :
262    ∀pt.point_of_offset (offset_of_point pt) = pt
263  ; offset_of_point_of_offset :
264    ∀o.offset_of_point (point_of_offset o) = o
265  }.
266
267(*
268coercion ms_pars_to_msu_pars nocomposites :
269∀p : params.∀msp : more_sem_params p.more_sem_unserialized_params p (λglobals.joint_internal_function globals p)
270 ≝ msu_pars
271on _msp : more_sem_params ? to more_sem_unserialized_params ??.
272
273definition ss_pars_of_ms_pars ≝
274  λp.λpp : more_sem_params p.
275  st_pars … (msu_pars … pp).
276coercion ms_pars_to_ss_pars nocomposites :
277∀p : params.∀msp : more_sem_params p.sem_state_params ≝
278ss_pars_of_ms_pars on _msp : more_sem_params ? to sem_state_params.*)
279
280definition pc_of_point : ∀p.more_sem_params p →
281  program_counter → code_point p → program_counter ≝
282  λp,msp,ptr,pt.
283  mk_program_counter (pc_block ptr) (offset_of_point ? msp pt).
284
285definition point_of_pc :
286  ∀p.more_sem_params p → program_counter → code_point p ≝
287  λp,msp,ptr.point_of_offset p msp (pc_offset ptr).
288
289lemma point_of_pointer_of_point :
290  ∀p,msp.∀ptr,pt.
291  point_of_pc ? msp (pc_of_point p msp ptr pt) = pt.
292#p #msp #ptr #pt normalize // qed.
293
294lemma pointer_of_point_block :
295  ∀p,msp,ptr,pt.
296  pc_block (pc_of_point p msp ptr pt) = pc_block ptr.
297#p #msp #ptr #pt % qed. (* can probably do without *)
298
299lemma pointer_of_point_uses_block :
300  ∀p,msp.∀ptr1,ptr2.∀pt.pc_block ptr1 = pc_block ptr2 →
301    pc_of_point p msp ptr1 pt = pc_of_point p msp ptr2 pt.
302#p #msp #ptr1 #ptr2 #pc #EQ normalize >EQ % qed.
303
304lemma pointer_of_point_of_pointer :
305  ∀p,msp.∀ptr1,ptr2.
306    pc_block ptr1 = pc_block ptr2 →
307    pc_of_point p msp ptr1 (point_of_pc p msp ptr2) = ptr2.
308#p #msp #ptr1 * #bl2 #o2 #EQ normalize >offset_of_point_of_offset >EQ % qed.
309
310definition fetch_statement: ∀p : params.∀ msp : more_sem_params p.∀globals.
311  ∀ge : genv_t (joint_function p globals). program_counter →
312  res ((Σi.is_internal_function … ge i) × (joint_statement p globals)) ≝
313  λp,msp,globals,ge,ptr.
314  ! f ← fetch_function … ge ptr ;
315  let fn ≝ if_of_function … f in
316  let pt ≝ point_of_pc ? msp ptr in
317  ! stmt ← opt_to_res … (msg ProgramCounterOutOfCode) (stmt_at … (joint_if_code … fn) pt);
318  return 〈f, stmt〉.
319
320definition pc_of_label : ∀p : params.∀ msp : more_sem_params p.∀globals.
321  genv_t (joint_function p globals) → program_counter → label → res program_counter ≝
322  λp,msp,globals,ge,ptr,lbl.
323  ! f ← fetch_function … ge ptr ;
324  let fn ≝ if_of_function …  ge f in
325  ! pt ← opt_to_res … [MSG LabelNotFound ; CTX ? lbl]
326            (point_of_label … (joint_if_code … fn) lbl) ;
327  return pc_of_point p msp ptr pt.
328
329definition succ_pc : ∀p : params.∀ msp : more_sem_params p.
330  program_counter → succ p → program_counter ≝
331  λp,msp,ptr,nxt.
332  let curr ≝ point_of_pc p msp ptr in
333  pc_of_point p msp ptr (point_of_succ p curr nxt).
334
335record sem_params : Type[1] ≝
336  { spp :> params
337  ; more_sem_pars :> more_sem_params spp
338  }.
339
340(* definition msu_pars_of_s_pars :
341∀p : sem_params.more_sem_unserialized_params (spp p) (λglobals.joint_internal_function globals (spp p))
342≝ λp : sem_params.
343  msu_pars … (more_sem_pars p).
344coercion s_pars_to_msu_pars nocomposites :
345∀p : sem_params.more_sem_unserialized_params (spp p) (λglobals.joint_internal_function globals (spp p)) ≝
346msu_pars_of_s_pars
347on p : sem_params to more_sem_unserialized_params ??.
348
349definition ss_pars_of_s_pars :
350∀p : sem_params.sem_state_params
351≝ λp : sem_params.
352  st_pars … (msu_pars … (more_sem_pars p)).
353coercion s_pars_to_ss_pars nocomposites :
354∀p : sem_params.sem_state_params ≝
355ss_pars_of_s_pars
356on _p : sem_params to sem_state_params.
357
358definition ms_pars_of_s_pars :
359∀p : sem_params.more_sem_params (spp p)
360≝ more_sem_pars.
361coercion s_pars_to_ms_pars nocomposites :
362∀p : sem_params.more_sem_params (spp p) ≝
363ms_pars_of_s_pars
364on p : sem_params to more_sem_params ?.*)
365
366(* definition address_of_label: ∀globals. ∀p:sem_params.
367  genv globals p → pointer → label → res address ≝
368 λglobals,p,ge,ptr,l.
369  do newptr ← pointer_of_label … p ? ge … ptr l ;
370  OK … (address_of_code_pointer newptr). *)
371
372definition goto: ∀p : sem_params.∀globals.
373  genv_t (joint_function p globals) → label → state p → program_counter → res (state_pc p) ≝
374 λp,globals,ge,l,st,b.
375  ! newpc ← pc_of_label ? p … ge b l ;
376  return mk_state_pc ? st newpc.
377
378(*
379definition empty_state: ∀p. more_sem_params p → state p ≝
380 mk_state … (empty_framesT …)
381*)
382
383definition next : ∀p : sem_params.succ p → state_pc p → state_pc p ≝
384 λp,l,st.
385 let newpc ≝ succ_pc ? p … (pc … st) l in
386 mk_state_pc … st newpc.
387
388
389definition function_of_call ≝ λp:sem_params.λglobals.
390  λge: genv_t (joint_function p globals).λst : state p.λf.
391  match f with
392  [ inl id ⇒
393    opt_to_res … [MSG BadFunction; MSG MissingSymbol; CTX ? id] (funct_of_ident … ge id)
394  | inr addr ⇒
395    ! addr_l ← dpl_arg_retrieve … st (\fst addr) ;
396    ! addr_h ← dph_arg_retrieve … st (\snd addr) ;
397    opt_to_res … [MSG BadFunction; MSG BadPointer] (funct_of_bevals … ge addr_l addr_h)
398  ].
399
400(* Paolo: why external calls do not need args?? *)
401definition eval_external_call ≝
402λp,F.λp' : sem_unserialized_params p F.λfn,args,dest,st.
403      ! params ← fetch_external_args … p' fn st args : IO ???;
404      ! evargs ← check_eventval_list params (sig_args (ef_sig fn)) : IO ???;
405      ! evres ← do_io (ef_id fn) evargs (proj_sig_res (ef_sig fn));
406      (* CSC: XXX bug here; I think I should split it into Byte-long
407         components; instead I am making a singleton out of it. To be
408         fixed once we fully implement external functions. *)
409      let vs ≝ [mk_val ? evres] in
410      set_result … p' vs dest st.
411
412definition eval_internal_call_pc ≝
413λp : sem_params.λglobals : list ident.λge : genv_t (joint_function p globals).λi.
414let fn ≝ if_of_function … ge i in
415let l' ≝ joint_if_entry ?? fn in
416mk_program_counter (block_of_funct … ge (pi1 … i)) (offset_of_point ? p … l').
417[ @block_of_funct_ident_is_code
418| cases i /2 by internal_function_is_function/
419]
420qed.
421
422definition eval_internal_call_no_pc ≝
423λp : sem_params.λglobals : list ident.λge : genv p globals.λi,args,st.
424let fn ≝ if_of_function … ge i in
425let stack_size ≝ stack_sizes … ge i in
426! st' ← setup_call … stack_size (joint_if_params … fn) args st ;
427return allocate_locals … p (joint_if_locals … fn) st.
428
429definition eval_seq_no_pc :
430 ∀p:sem_params.∀globals.∀ge:genv p globals. (Σi.is_internal_function … ge i) →
431  state p → joint_seq p globals →
432  IO io_out io_in (state p) ≝
433 λp,globals,ge,curr_fn,st,seq.
434 match seq return λx.IO ??? with
435  [ extension_seq c ⇒
436    eval_ext_seq … ge c curr_fn st
437  | LOAD dst addrl addrh ⇒
438    ! vaddrh ← dph_arg_retrieve … st addrh ;
439    ! vaddrl ← dpl_arg_retrieve … st addrl;
440    ! vaddr ← pointer_of_address 〈vaddrl,vaddrh〉;
441    ! v ← opt_to_res … (msg FailedLoad) (beloadv (m … st) vaddr);
442    acca_store p … dst v st
443 | STORE addrl addrh src ⇒
444    ! vaddrh ← dph_arg_retrieve … st addrh;
445    ! vaddrl ← dpl_arg_retrieve … st addrl;
446    ! vaddr ← pointer_of_address 〈vaddrl,vaddrh〉;
447    ! v ← acca_arg_retrieve … st src;
448    ! m' ← opt_to_res … (msg FailedStore) (bestorev (m … st) vaddr v);
449    return set_m … m' st
450  | ADDRESS id prf ldest hdest ⇒
451    let addr_block ≝ opt_safe ? (find_symbol … ge id) ? in
452    let 〈laddr,haddr〉 ≝ beval_pair_of_pointer (mk_pointer addr_block zero_offset) in
453    ! st' ← dpl_store … ldest laddr st;
454    dph_store … hdest haddr st'
455  | OP1 op dacc_a sacc_a ⇒
456    ! v ← acca_retrieve … st sacc_a;
457    ! v' ← be_op1 op v ;
458    acca_store … dacc_a v' st
459  | OP2 op dacc_a sacc_a src ⇒
460    ! v1 ← acca_arg_retrieve … st sacc_a;
461    ! v2 ← snd_arg_retrieve … st src;
462    ! 〈v',carry〉 ← be_op2 (carry … st) op v1 v2 ;
463    ! st' ← acca_store … dacc_a v' st;
464    return set_carry … carry st'
465  | CLEAR_CARRY ⇒
466    return set_carry … (BBbit false) st
467  | SET_CARRY ⇒
468    return set_carry … (BBbit true) st
469  | OPACCS op dacc_a_reg dacc_b_reg sacc_a_reg sacc_b_reg ⇒
470    ! v1 ← acca_arg_retrieve … st sacc_a_reg;
471    ! v2 ← accb_arg_retrieve … st sacc_b_reg;
472    ! 〈v1',v2'〉 ← be_opaccs op v1 v2 ;
473    ! st' ← acca_store … dacc_a_reg v1' st;
474    accb_store … dacc_b_reg v2' st'
475  | POP dst ⇒
476    ! 〈v, st'〉 ← pop p st;
477    acca_store … p dst v st'
478  | PUSH src ⇒
479    ! v ← acca_arg_retrieve … st src;
480    push … st v
481  | MOVE dst_src ⇒
482    pair_reg_move … st dst_src
483  | CALL f args dest ⇒
484    ! fn ← function_of_call … ge st f : IO ???;
485    match description_of_function … fn return λx.description_of_function … fn = x → ? with
486    [ Internal fd ⇒ λprf.
487      eval_internal_call_no_pc … ge «fn, ?» args st  (* only pc changes *)
488    | External fd ⇒ λ_.eval_external_call … fd args dest st
489    ] (refl …)
490  | _ ⇒ return st
491  ].
492[ @hide_prf
493  @find_symbol_in_globals
494  lapply prf
495  elim globals [*]
496  #hd #tl #IH #H elim (orb_Prop_true … H) -H
497  [@eq_identifier_elim #H * >H %1 % ]
498  #G %2 @IH @G
499| @(description_of_internal_function … prf)
500]
501qed.
502
503definition eval_seq_pc :
504 ∀p:sem_params.∀globals.∀ge:genv p globals.
505  state_pc p → ? → joint_seq p globals →
506  res (state_pc p) ≝
507  λp,globals,ge,st,nxt,s.
508  match s with
509  [ CALL f args dest ⇒
510    ! fn ← function_of_call … ge st f;
511    match ? return λx.description_of_function … fn = x → ? with
512    [ Internal _ ⇒ λprf.
513      let pc ≝ eval_internal_call_pc … ge «fn, ?» in
514      ! st' ← save_frame … dest st ;
515      return mk_state_pc … st' pc
516    | External _ ⇒ λ_.return next p nxt st
517    ] (refl …)
518  | _ ⇒ return next p nxt st
519  ].
520@(description_of_internal_function … prf)
521qed.
522
523definition eval_statement :
524 ∀p:sem_params.∀globals.∀ge:genv p globals.
525 (Σi.is_internal_function … ge i) → state_pc p →
526  ∀s:joint_statement p globals.
527  IO io_out io_in (state_pc p) ≝
528  λp,g,ge,curr_fn,st,s.
529  match s with
530  [ sequential s next ⇒
531    match s return λ_.IO ??? with
532    [ step_seq s ⇒
533      ! st' ← eval_seq_no_pc … ge curr_fn st s ;
534      let st'' ≝ mk_state_pc … st' (pc … st) in
535      eval_seq_pc ?? ge st'' next s
536    | COND a l ⇒
537      ! v ← acca_retrieve … st a ;
538      ! b ← bool_of_beval … v ;
539      ! pc' ←
540        if b then
541          pc_of_label ? p … ge (pc … st) l
542        else
543          return succ_pc ? p (pc … st) next ;
544      return mk_state_pc … st pc'
545    ]
546  | final s ⇒
547    match s with
548    [ GOTO l ⇒
549      ! pc' ← pc_of_label ? p ? ge (pc … st) l ;
550      return mk_state_pc … st pc'
551    | RETURN ⇒ pop_frame … curr_fn st
552    | TAILCALL _ f args ⇒
553      ! fn ← function_of_call … ge st f : IO ???;
554      match ? return λx.description_of_function … fn = x → ? with
555      [ Internal _ ⇒ λprf.
556        let pc' ≝ eval_internal_call_pc … ge «fn, ?» in
557        return mk_state_pc … st pc'
558      | External fd ⇒ λ_.
559        let curr_dest ≝ joint_if_result ?? (if_of_function … curr_fn) in
560        ! st' ← eval_external_call ??? fd args curr_dest st ;
561        pop_frame … curr_fn st'
562      ] (refl …)
563    ]
564  ].
565@(description_of_internal_function … prf)
566qed.
567
568definition eval_state : ∀p:sem_params. ∀globals: list ident.
569  genv p globals →
570  state_pc p → IO io_out io_in (state_pc p) ≝
571  λp,globals,ge,st.
572  ! 〈fn,s〉 ← fetch_statement ? p … ge (pc … st) : IO ???;
573  eval_statement … ge fn st s.
574
575(* Paolo: what if in an intermediate language main finishes with an external
576  tailcall? Maybe it should rely on an FEnd flow command issued, but that's
577  not static... *)
578definition is_final: ∀p: sem_params.∀globals.
579  genv p globals → program_counter → state_pc p → option int ≝
580 λp,globals,ge,exit,st.res_to_opt ? (
581  do 〈f,s〉 ← fetch_statement ? p … ge (pc … st);
582  let fn ≝ if_of_function … f in
583  match s with
584  [ final s' ⇒
585    match s' with
586    [ RETURN ⇒
587      do st' ← pop_frame … ge f st;
588      if eq_program_counter (pc … st') exit then
589       do vals ← read_result … ge (joint_if_result … fn) st' ;
590       Word_of_list_beval vals
591      else
592       Error ? [ ]
593   | _ ⇒ Error ? [ ]
594   ]
595 | _ ⇒ Error ? [ ]
596 ]).
597
598(*
599record evaluation_parameters : Type[1] ≝
600 { globals: list ident
601 ; sparams:> sem_params
602 ; exit: program_counter
603 ; genv2: genv globals sparams
604 }.
605
606(* Paolo: with structured traces, eval need not emit labels. However, this
607  changes trans_system. For now, just putting a dummy thing for
608  the transition. *)
609definition joint_exec: trans_system io_out io_in ≝
610  mk_trans_system … evaluation_parameters (λG. state_pc G)
611   (λG.is_final (globals G) G (genv2 G) (exit G))
612   (λG,st.! 〈flag,st'〉 ← eval_state_flag (globals G) G (genv2 G) st ; return 〈E0, st'〉).
613
614definition make_global :
615 ∀pars: sem_params.
616  joint_program pars → evaluation_parameters
617
618 λpars.
619 (* Invariant: a -1 block is unused in common/Globalenvs *)
620 let b ≝ mk_block Code (-1) in
621 let ptr ≝ mk_pointer Code b ? (mk_offset 0) in
622  (λp. mk_evaluation_parameters
623    (prog_var_names … p)
624    (mk_sem_params … pars)
625    ptr
626    (globalenv_noinit … p)
627  ).
628% qed.
629
630axiom ExternalMain: String.
631
632definition make_initial_state :
633 ∀pars: sem_params.
634 ∀p: joint_program … pars. res (state_pc pars) ≝
635λpars,p.
636  let sem_globals ≝ make_global pars p in
637  let ge ≝ genv2 sem_globals in
638  let m ≝ alloc_mem … p in
639  let 〈m,spb〉 ≝ alloc … m 0 external_ram_size XData in
640  let 〈m,ispb〉 ≝ alloc … m 0 internal_ram_size XData in
641  let dummy_pc ≝ mk_pointer Code (mk_block Code (-1)) ? (mk_offset 0) in
642  let spp ≝ mk_pointer XData spb ? (mk_offset external_ram_size) in
643  let ispp ≝ mk_pointer XData ispb ? (mk_offset 47) in
644  let main ≝ prog_main … p in
645  let st0 ≝ mk_state pars (empty_framesT …) spp ispp BVfalse (empty_regsT … spp) m in
646  (* use exit sem_globals as ra and call_dest_for_main as dest *)
647  let st0' ≝ set_frms ? (save_frame … (exit sem_globals) (call_dest_for_main … pars) st0) st0 in
648  let st_pc0 ≝ mk_state_pc ? st0' dummy_pc in
649  ! main_block ← opt_to_res … [MSG MissingSymbol; CTX ? main] (find_symbol … ge main) ;
650  ! main_fd ← opt_to_res ? [MSG BadPointer] (find_funct_ptr … ge main_block) ;
651  match main_fd with
652  [ Internal fn ⇒
653    do_call ?? ge st_pc0 (block_id main_block) fn (call_args_for_main … pars)
654  | External _ ⇒ Error … [MSG ExternalMain] (* External main not supported: why? *)
655  ]. [5: cases ispb * |6: cases spb * ] (* without try it fails! *) try //
656qed.
657
658definition joint_fullexec :
659 ∀pars:sem_params.fullexec io_out io_in ≝
660 λpars.mk_fullexec ??? joint_exec (make_global pars) (make_initial_state pars).
661*)
Note: See TracBrowser for help on using the repository browser.