source: src/joint/joint_semantics.ma @ 2952

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