source: src/joint/joint_semantics.ma @ 2821

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