source: src/joint/semantics.ma @ 2537

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

rolled back changes on calls in joint. Now the save_frame parameter
has a switch that tells whether the call is an ident one or a pointer one.
The idea is that in the latter case, from LTL onwards, the caller address is not saved (as it is done by explicit instructions

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