source: src/joint/semantics.ma @ 2529

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

rewritten function handling in joint
swapped call_rel with ret_rel in the definition of status_rel, and parameterised status_simulation on status_rel
renamed SemanticUtils?

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