source: src/joint/semantics.ma @ 2536

Last change on this file since 2536 was 2532, checked in by tranquil, 8 years ago

added FCOND in LIN, and rewritten linearise so that it never adds a GOTO after a COND (writes in FCOND instead)
LIN to ASM is broken atm

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