source: src/joint/joint_semantics.ma @ 2876

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

corrected another endianess bug in joint_semantics. Switched some names in RTLToERTL.

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