source: src/joint/joint_semantics.ma @ 2783

Last change on this file since 2783 was 2783, checked in by piccolo, 7 years ago

modified joint_closed_internal_function definition (added condition on pseudo-registers)
added new record for parameters
modified state definition with option for framesT

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