source: src/joint/joint_semantics.ma @ 2946

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

main novelties:

  • there is an in-built stack_usage nat in joint states, at the base of the new division of RTL's semantics (with separate stacks, with separate stacks but with an artificial overflow error, with a unique stack)
  • a premain is added semantically to the global env, so initial cost label and main call and return are observed
  • proper initialization is now in LINToASM (to be sure, endianess should be checked ;-)

The update breaks proofs of back end atm. compiler.ma should be okay, but I have not had time to complete its compilation.

File size: 24.9 KB
Line 
1include "common/Globalenvs.ma".
2include "common/IO.ma".
3(* include "common/SmallstepExec.ma". *)
4include "joint/BEMem.ma".
5include "joint/Joint.ma".
6include "ASM/I8051bis.ma".
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 ; stack_usage : ℕ
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 (null_pc at the start) *)
71  ; last_pop : program_counter
72  }.
73
74definition init_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 (stack_usage … st).
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) (stack_usage … 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) (stack_usage … 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) (stack_usage … 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) (stack_usage … 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,st,pc. mk_state_pc … st pc pc.
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) (stack_usage … 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 serialized_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
281record sem_params : Type[1] ≝
282  { spp' :> serialized_params
283  ; pre_main_generator : ∀p : joint_program spp'.joint_closed_internal_function spp' (prog_var_names … p)
284  }.
285
286(*
287coercion ms_pars_to_msu_pars nocomposites :
288∀p : params.∀msp : more_sem_params p.more_sem_unserialized_params p (λglobals.joint_internal_function globals p)
289 ≝ msu_pars
290on _msp : more_sem_params ? to more_sem_unserialized_params ??.
291
292definition ss_pars_of_ms_pars ≝
293  λp.λpp : more_sem_params p.
294  st_pars … (msu_pars … pp).
295coercion ms_pars_to_ss_pars nocomposites :
296∀p : params.∀msp : more_sem_params p.sem_state_params ≝
297ss_pars_of_ms_pars on _msp : more_sem_params ? to sem_state_params.*)
298
299definition pc_of_point : ∀p:sem_params.(Σb.block_region b = Code) →
300  code_point p → program_counter ≝
301  λp,bl,pt.
302  mk_program_counter bl (offset_of_point p pt).
303
304definition point_of_pc :
305  ∀p:sem_params.program_counter → code_point p ≝
306  λp,ptr.point_of_offset p (pc_offset ptr).
307
308lemma point_of_pc_of_point :
309  ∀p,bl,pt.
310  point_of_pc p (pc_of_point p bl pt) = pt.
311#p #bl #pt normalize // qed.
312
313lemma pc_of_point_of_pc :
314  ∀p,ptr.
315    pc_of_point p (pc_block ptr) (point_of_pc p ptr) = ptr.
316#p * #bl #off normalize >offset_of_point_of_offset % qed.
317
318definition fetch_statement: ∀p : sem_params.∀globals.
319  ∀ge : genv_t (joint_function p globals). program_counter →
320  res (ident × (joint_closed_internal_function p globals) × (joint_statement p globals)) ≝
321  λp,globals,ge,ptr.
322  ! 〈id, fn〉 ← fetch_internal_function … ge (pc_block ptr) ;
323  let pt ≝ point_of_pc p ptr in
324  ! stmt ← opt_to_res … (msg ProgramCounterOutOfCode) (stmt_at … (joint_if_code … fn) pt);
325  return 〈id, fn, stmt〉.
326
327definition pc_of_label : ∀p : sem_params.∀globals.
328  genv_t (joint_function p globals) → (Σb.block_region b = Code) → label → res program_counter ≝
329  λp,globals,ge,bl,lbl.
330  ! 〈i, fn〉 ← fetch_internal_function … ge bl ;
331  ! pt ← opt_to_res … [MSG LabelNotFound ; CTX ? lbl]
332            (point_of_label … (joint_if_code … fn) lbl) ;
333  return mk_program_counter bl (offset_of_point p pt).
334
335definition succ_pc : ∀p : sem_params.
336  program_counter → succ p → program_counter ≝
337  λp,ptr,nxt.
338  let curr ≝ point_of_pc p ptr in
339  pc_of_point p (pc_block ptr) (point_of_succ p curr nxt).
340
341(*
342record sem_params : Type[1] ≝
343  { spp :> params
344  ; more_sem_pars :> more_sem_params spp
345  }.
346*)
347(* definition msu_pars_of_s_pars :
348∀p : sem_params.more_sem_unserialized_params (spp p) (λglobals.joint_internal_function globals (spp p))
349≝ λp : sem_params.
350  msu_pars … (more_sem_pars p).
351coercion s_pars_to_msu_pars nocomposites :
352∀p : sem_params.more_sem_unserialized_params (spp p) (λglobals.joint_internal_function globals (spp p)) ≝
353msu_pars_of_s_pars
354on p : sem_params to more_sem_unserialized_params ??.
355
356definition ss_pars_of_s_pars :
357∀p : sem_params.sem_state_params
358≝ λp : sem_params.
359  st_pars … (msu_pars … (more_sem_pars p)).
360coercion s_pars_to_ss_pars nocomposites :
361∀p : sem_params.sem_state_params ≝
362ss_pars_of_s_pars
363on _p : sem_params to sem_state_params.
364
365definition ms_pars_of_s_pars :
366∀p : sem_params.more_sem_params (spp p)
367≝ more_sem_pars.
368coercion s_pars_to_ms_pars nocomposites :
369∀p : sem_params.more_sem_params (spp p) ≝
370ms_pars_of_s_pars
371on p : sem_params to more_sem_params ?.*)
372
373(* definition address_of_label: ∀globals. ∀p:sem_params.
374  genv globals p → pointer → label → res address ≝
375 λglobals,p,ge,ptr,l.
376  do newptr ← pointer_of_label … p ? ge … ptr l ;
377  OK … (address_of_code_pointer newptr). *)
378
379definition goto: ∀p : sem_params.∀globals.
380  genv_t (joint_function p globals) → label → state_pc p → res (state_pc p) ≝
381 λp,globals,ge,l,st.
382  ! newpc ← pc_of_label … ge (pc_block (pc … st)) l ;
383  return set_pc … newpc st.
384
385(*
386definition empty_state: ∀p. more_sem_params p → state p ≝
387 mk_state … (empty_framesT …)
388*)
389
390definition next : ∀p : sem_params.succ p → state_pc p → state_pc p ≝
391 λp,l,st.
392 let newpc ≝ succ_pc … (pc … st) l in
393 set_pc … newpc st.
394
395definition next_of_call_pc : ∀p : sem_params.∀globals.genv_t (joint_function p globals) →
396  program_counter → res (succ p) ≝
397λp,globals,ge,pc.
398  ! 〈id_fn, stmt〉 ← fetch_statement … ge pc ;
399  match stmt with
400  [ sequential s nxt ⇒
401    match s with
402    [ CALL _ _ _ ⇒ return nxt
403    | _ ⇒ Error … [MSG NoSuccessor]
404    ]
405  | _ ⇒ Error … [MSG NoSuccessor]
406  ].
407
408lemma deq_elim : ∀A : DeqSet.∀P : bool → Prop.∀x,y : A.
409(x = y → P true) → (x ≠ y → P false) → P (x == y).
410#A #P #x #y #H1 #H2 inversion (x == y) #EQ
411[ @H1 @(proj1 … (eqb_true … ) EQ) | @H2 % #EQ' destruct
412  >(proj2 … (eqb_true …) (refl …)) in EQ; #ABS destruct ] qed.
413
414definition eval_seq_no_pc :
415 ∀p:sem_params.∀globals.∀ge:genv p globals.ident →
416  joint_seq p globals → state p →
417  res (state p) ≝
418 λp,globals,ge,curr_id,seq,st.
419 match seq with
420  [ extension_seq c ⇒
421    eval_ext_seq … ge c curr_id st
422  | LOAD dst addrl addrh ⇒
423    ! vaddrh ← dph_arg_retrieve … st addrh ;
424    ! vaddrl ← dpl_arg_retrieve … st addrl;
425    ! vaddr ← pointer_of_address 〈vaddrl,vaddrh〉;
426    ! v ← opt_to_res … (msg FailedLoad) (beloadv (m … st) vaddr);
427    acca_store p … dst v st
428 | STORE addrl addrh src ⇒
429    ! vaddrh ← dph_arg_retrieve … st addrh;
430    ! vaddrl ← dpl_arg_retrieve … st addrl;
431    ! vaddr ← pointer_of_address 〈vaddrl,vaddrh〉;
432    ! v ← acca_arg_retrieve … st src;
433    ! m' ← opt_to_res … (msg FailedStore) (bestorev (m … st) vaddr v);
434    return set_m … m' st
435  | ADDRESS id prf ldest hdest ⇒
436    let addr_block ≝ opt_safe ? (find_symbol … ge id) ? in
437    let 〈laddr,haddr〉 ≝ beval_pair_of_pointer (mk_pointer addr_block zero_offset) in
438    ! st' ← dpl_store … ldest laddr st;
439    dph_store … hdest haddr st'
440  | OP1 op dacc_a sacc_a ⇒
441    ! v ← acca_retrieve … st sacc_a;
442    ! v' ← be_op1 op v ;
443    acca_store … dacc_a v' st
444  | OP2 op dacc_a sacc_a src ⇒
445    ! v1 ← acca_arg_retrieve … st sacc_a;
446    ! v2 ← snd_arg_retrieve … st src;
447    ! 〈v',carry〉 ← be_op2 (carry … st) op v1 v2 ;
448    ! st' ← acca_store … dacc_a v' st;
449    return set_carry … carry st'
450  | CLEAR_CARRY ⇒
451    return set_carry … (BBbit false) st
452  | SET_CARRY ⇒
453    return set_carry … (BBbit true) st
454  | OPACCS op dacc_a_reg dacc_b_reg sacc_a_reg sacc_b_reg ⇒
455    ! v1 ← acca_arg_retrieve … st sacc_a_reg;
456    ! v2 ← accb_arg_retrieve … st sacc_b_reg;
457    ! 〈v1',v2'〉 ← be_opaccs op v1 v2 ;
458    ! st' ← acca_store … dacc_a_reg v1' st;
459    accb_store … dacc_b_reg v2' st'
460  | POP dst ⇒
461    ! 〈v, st'〉 ← pop p st;
462    acca_store … p dst v st'
463  | PUSH src ⇒
464    ! v ← acca_arg_retrieve … st src;
465    push … st v
466  | MOVE dst_src ⇒
467    pair_reg_move … st dst_src
468  | _ ⇒ return st (* for calls do everything in eval_seq_advance *)
469  ].
470  @hide_prf
471  @find_symbol_in_globals
472  lapply prf
473  elim globals [*]
474  #hd #tl #IH #H elim (orb_Prop_true … H) -H
475  [ @deq_elim #H * destruct %1 % | #H %2{(IH … H)} ]
476qed.
477
478definition code_block_of_block : block → option (Σb.block_region b = Code) ≝
479λbl.match block_region bl
480  return λx.block_region bl = x → option (Σb.block_region b = Code) with
481  [ Code ⇒ λprf.Some ? «bl, prf»
482  | XData ⇒ λ_.None ?
483  ] (refl …).
484
485definition block_of_funct_id ≝  λF.λsp:sem_state_params.
486  λge: genv_t F.λid.
487  opt_to_res … [MSG BadFunction; CTX … id] (
488    ! bl ← find_symbol … ge id;
489    code_block_of_block bl).
490 
491definition block_of_call ≝ λp : sem_params.
492  λglobals.λge: genv_t (joint_function p globals).λf.λst : state p.
493  ! bl ← match f with
494    [ inl id ⇒
495      opt_to_res … [MSG BadFunction; CTX … id]
496        (find_symbol … ge id)
497    | inr addr ⇒
498      ! addr_l ← dpl_arg_retrieve … st (\fst addr) ;
499      ! addr_h ← dph_arg_retrieve … st (\snd addr) ;
500      ! ptr ← pointer_of_bevals … [addr_l ; addr_h ] ;
501      if eq_bv … (bv_zero …) (offv (poff ptr)) then
502        return pblock ptr
503      else
504        Error … [MSG BadFunction; MSG BadPointer]
505    ] ;
506  opt_to_res … [MSG BadFunction; MSG BadPointer]
507    (code_block_of_block bl).
508
509definition eval_external_call ≝
510λp : sem_params.λfn,args,dest,st.
511      ! params ← fetch_external_args … p fn st args : IO ???;
512      ! evargs ← check_eventval_list params (sig_args (ef_sig fn)) : IO ???;
513      ! evres ← do_io (ef_id fn) evargs (proj_sig_res (ef_sig fn));
514      (* CSC: XXX bug here; I think I should split it into Byte-long
515         components; instead I am making a singleton out of it. To be
516         fixed once we fully implement external functions. *)
517      let vs ≝ [mk_val ? evres] in
518      set_result … p vs dest st.
519
520definition increment_stack_usage : ∀p.ℕ → state p → state p ≝
521 λp,n,st.mk_state p (st_frms … st) (istack … st) (carry … st) (regs … st) (m … st)
522  (n + stack_usage … st).
523
524definition decrement_stack_usage : ∀p.ℕ → state p → state p ≝
525 λp,n,st.mk_state p (st_frms … st) (istack … st) (carry … st) (regs … st) (m … st)
526  (stack_usage … st - n).
527
528definition eval_internal_call ≝
529λp : sem_params.λglobals : list ident.λge : genv p globals.λi,fn,args.
530λst : state p.
531! stack_size ← opt_to_res … [MSG MissingStackSize; CTX … i] (stack_sizes … ge i) ;
532! st' ← setup_call … stack_size (joint_if_params … globals fn) args st ;
533return increment_stack_usage … stack_size st'.
534
535definition is_inl : ∀A,B.A+B → bool ≝ λA,B,x.match x with [ inl _ ⇒ true | _ ⇒ false ].
536
537definition eval_call ≝
538λp : sem_params.λglobals : list ident.λge : genv p globals.λf,args,dest,nxt.
539λst : state_pc p.
540! bl ← block_of_call … ge f st : IO ???;
541! 〈i, fd〉 ← fetch_function … ge bl : IO ???;
542match fd with
543[ Internal ifd ⇒
544  ! st' ← save_frame … (kind_of_call … f) dest st ;
545  ! st'' ← eval_internal_call p globals ge i ifd args st' ;
546  let pc ≝ pc_of_point p bl (joint_if_entry … ifd) in
547  return mk_state_pc … st'' pc (last_pop … st)
548| External efd ⇒
549  ! st' ← eval_external_call … efd args dest st ;
550  return mk_state_pc … st' (succ_pc p (pc … st) nxt) (last_pop … st)
551].
552
553definition eval_statement_no_pc :
554 ∀p:sem_params.∀globals.∀ge:genv p globals.
555 ident (* current *) →
556 joint_statement p globals → state p → res (state p) ≝
557 λp,globals,ge,curr_id,s,st.
558  match s with
559  [ sequential s next ⇒
560    match s with
561    [ step_seq s ⇒ eval_seq_no_pc … ge curr_id s st
562    | _ ⇒ return st
563    ]
564  | _ ⇒ return st
565  ].
566
567definition eval_return ≝
568λp : sem_params.λglobals : list ident.λge : genv p globals.
569λcurr_id.λcurr_ret : call_dest p.
570λst : state p.
571! stack_size ← opt_to_res … [MSG MissingStackSize; CTX … curr_id] (stack_sizes … ge curr_id) ;
572! 〈st', call_pc〉 ← pop_frame … ge curr_id curr_ret st ;
573! nxt ← next_of_call_pc … ge call_pc ;
574let st'' ≝ set_last_pop … (decrement_stack_usage … stack_size st') call_pc in
575return
576  next ? nxt st'' (* now address pushed on stack are calling ones! *).
577
578definition eval_tailcall ≝
579λp : sem_params.λglobals : list ident.λge : genv p globals.λf,args,curr_f.
580λcurr_ret : call_dest p.
581λst : state_pc p.
582! bl ← block_of_call … ge f st : IO ???;
583! 〈i, fd〉 ← fetch_function … ge bl : IO ???;
584match fd with
585[ Internal ifd ⇒
586  ! stack_size ← opt_to_res … [MSG MissingStackSize; CTX … curr_f] (stack_sizes … ge curr_f) ;
587  let st' ≝ decrement_stack_usage … stack_size st in
588  ! st'' ← eval_internal_call p globals ge i ifd args st' ;
589  let pc ≝ pc_of_point p bl (joint_if_entry … ifd) in
590  return mk_state_pc … st'' pc (last_pop … st)
591| External efd ⇒
592  ! st' ← eval_external_call … efd args curr_ret st ;
593  eval_return … ge curr_f curr_ret st
594].
595
596definition eval_statement_advance :
597 ∀p:sem_params.∀globals.∀ge:genv p globals.
598 ident → joint_closed_internal_function p globals →
599  joint_statement p globals → state_pc p →
600  IO io_out io_in (state_pc p) ≝
601  λp,g,ge,curr_id,curr_fn,s,st.
602  match s return λ_.IO ??? with
603  [ sequential s nxt ⇒
604    match s return λ_.IO ??? with
605    [ COND a l ⇒
606      ! v ← acca_retrieve … st a ;
607      ! b ← bool_of_beval … v ;
608      if b then
609        goto … ge l st
610      else
611        return next … nxt st
612    | CALL f args dest ⇒
613      eval_call … ge f args dest nxt st
614    | _ ⇒ return next … nxt st
615    ]
616  | final s ⇒
617    let curr_ret ≝ joint_if_result … curr_fn in
618    match s with
619    [ GOTO l ⇒ goto … ge l st
620    | RETURN ⇒ eval_return … ge curr_id curr_ret st
621    | TAILCALL _ f args ⇒
622      eval_tailcall … ge f args curr_id curr_ret st
623    ]
624  | FCOND _ a lbltrue lblfalse ⇒
625    ! v ← acca_retrieve … st a ;
626    ! b ← bool_of_beval … v ;
627    if b then
628      goto … ge lbltrue st
629    else
630      goto … ge lblfalse st
631  ].
632
633definition eval_state : ∀p:sem_params. ∀globals: list ident.
634  genv p globals →
635  state_pc p → IO io_out io_in (state_pc p) ≝
636  λp,globals,ge,st.
637  ! 〈id,fn,s〉 ← fetch_statement … ge (pc … st) : IO ???;
638  ! st' ← eval_statement_no_pc … ge id s st : IO ???;
639  let st'' ≝ set_no_pc … st' st in
640  eval_statement_advance … ge id fn s st''.
Note: See TracBrowser for help on using the repository browser.