source: src/joint/semantics.ma @ 2556

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

in joint semantics and traces: added a last popped calling address to state_pc, in order to have a strong enough as_after_return in joint (due to graph languages having one-to-many predecessors)
in lineariseProof: one axiom left (tailcall case)

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