source: src/joint/joint_semantics.ma @ 2939

Last change on this file since 2939 was 2920, checked in by sacerdot, 7 years ago

dos2unix-ed

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