source: src/joint/joint_semantics.ma @ 2757

Last change on this file since 2757 was 2688, checked in by tranquil, 8 years ago
  • in Arithmeticcs.ma: commented include that breaks script in latest matita
  • moved COST_LABEL out of joint_seq
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: 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 … 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 → ident → 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  let ident ≝ ? in
531  ! st' ← save_frame … (kind_of_call … f) dest ident st ;
532  ! st'' ← eval_internal_call p globals ge i ifd args st' ;
533  let pc ≝ pc_of_point p bl (joint_if_entry … ifd) in
534  return mk_state_pc … st'' pc (last_pop … st)
535| External efd ⇒
536  ! st' ← eval_external_call … efd args dest st ;
537  return mk_state_pc … st' (succ_pc p (pc … st) nxt) (last_pop … st)
538]. cases daemon qed. (*TODO*)
539
540definition eval_statement_no_pc :
541 ∀p:sem_params.∀globals.∀ge:genv p globals.
542 ident → joint_closed_internal_function p globals (* current *) →
543 joint_statement p globals → state p → res (state p) ≝
544 λp,globals,ge,curr_id,curr_fn,s,st.
545  match s with
546  [ sequential s next ⇒
547    match s with
548    [ step_seq s ⇒ eval_seq_no_pc … ge curr_id curr_fn s st
549    | _ ⇒ return st
550    ]
551  | _ ⇒ return st
552  ].
553
554definition eval_return ≝
555λp : sem_params.λglobals : list ident.λge : genv p globals.
556λcurr_id.λcurr_fn : joint_closed_internal_function ??.
557λst : state p.
558! st' ← pop_frame … ge curr_id curr_fn st ;
559! nxt ← next_of_call_pc … ge (\snd … st') ;
560return
561  next … nxt (set_last_pop … (\snd … st') st') (* now address pushed on stack are calling ones! *).
562
563definition eval_tailcall ≝
564λp : sem_params.λglobals : list ident.λge : genv p globals.λf,args,curr_f.
565λcurr_fn : joint_closed_internal_function ??.
566λst : state_pc p.
567! bl ← block_of_call … ge f st : IO ???;
568! 〈i, fd〉 ← fetch_function … ge bl : IO ???;
569match fd with
570[ Internal ifd ⇒
571  ! st' ← eval_internal_call p globals ge i ifd args st ;
572  let pc ≝ pc_of_point p bl (joint_if_entry … ifd) in
573  return mk_state_pc … st' pc (last_pop … st)
574| External efd ⇒
575  let curr_dest ≝ joint_if_result ?? curr_fn in
576  ! st' ← eval_external_call … efd args curr_dest st ;
577  eval_return … ge curr_f curr_fn st
578].
579
580definition eval_statement_advance :
581 ∀p:sem_params.∀globals.∀ge:genv p globals.
582 ident → joint_closed_internal_function p globals →
583  joint_statement p globals → state_pc p →
584  IO io_out io_in (state_pc p) ≝
585  λp,g,ge,curr_id,curr_fn,s,st.
586  match s return λ_.IO ??? with
587  [ sequential s nxt ⇒
588    match s return λ_.IO ??? with
589    [ COND a l ⇒
590      ! v ← acca_retrieve … st a ;
591      ! b ← bool_of_beval … v ;
592      if b then
593        goto … ge l st
594      else
595        return next … nxt st
596    | CALL f args dest ⇒
597      eval_call … ge f args dest nxt st
598    | _ ⇒ return next … nxt st
599    ]
600  | final s ⇒
601    match s with
602    [ GOTO l ⇒ goto … ge l st
603    | RETURN ⇒ eval_return … ge curr_id curr_fn st
604    | TAILCALL _ f args ⇒
605      eval_tailcall … ge f args curr_id curr_fn st
606    ]
607  | FCOND _ a lbltrue lblfalse ⇒
608    ! v ← acca_retrieve … st a ;
609    ! b ← bool_of_beval … v ;
610    if b then
611      goto … ge lbltrue st
612    else
613      goto … ge lblfalse st
614  ].
615
616definition eval_state : ∀p:sem_params. ∀globals: list ident.
617  genv p globals →
618  state_pc p → IO io_out io_in (state_pc p) ≝
619  λp,globals,ge,st.
620  ! 〈id,fn,s〉 ← fetch_statement … ge (pc … st) : IO ???;
621  ! st' ← eval_statement_no_pc … ge id fn s st : IO ???;
622  let st'' ≝ set_no_pc … st' st in
623  eval_statement_advance … ge id fn s st''.
624
625(* Paolo: what if in an intermediate language main finishes with an external
626  tailcall? Maybe it should rely on an FEnd flow command issued, but that's
627  not static... *)
628definition is_final: ∀p: sem_params.∀globals.
629  genv p globals → program_counter → state_pc p → option int ≝
630 λp,globals,ge,exit,st.res_to_opt ? (
631  do 〈id,fn,s〉 ← fetch_statement  … ge (pc … st);
632  match s with
633  [ final s' ⇒
634    match s' with
635    [ RETURN ⇒
636      do st' ← pop_frame … ge id fn st;
637      if eq_program_counter (\snd … st') exit then
638      do vals ← read_result … ge (joint_if_result … fn) st ;
639        Word_of_list_beval vals
640      else
641        Error ? [ ]
642   | _ ⇒ Error ? [ ]
643   ]
644 | _ ⇒ Error ? [ ]
645 ]).
646
647(*
648record evaluation_parameters : Type[1] ≝
649 { globals: list ident
650 ; sparams:> sem_params
651 ; exit: program_counter
652 ; genv2: genv globals sparams
653 }.
654
655(* Paolo: with structured traces, eval need not emit labels. However, this
656  changes trans_system. For now, just putting a dummy thing for
657  the transition. *)
658definition joint_exec: trans_system io_out io_in ≝
659  mk_trans_system … evaluation_parameters (λG. state_pc G)
660   (λG.is_final (globals G) G (genv2 G) (exit G))
661   (λG,st.! 〈flag,st'〉 ← eval_state_flag (globals G) G (genv2 G) st ; return 〈E0, st'〉).
662
663definition make_global :
664 ∀pars: sem_params.
665  joint_program pars → evaluation_parameters
666
667 λpars.
668 (* Invariant: a -1 block is unused in common/Globalenvs *)
669 let b ≝ mk_block Code (-1) in
670 let ptr ≝ mk_pointer Code b ? (mk_offset 0) in
671  (λp. mk_evaluation_parameters
672    (prog_var_names … p)
673    (mk_sem_params … pars)
674    ptr
675    (globalenv_noinit … p)
676  ).
677% qed.
678
679definition make_initial_state :
680 ∀pars: sem_params.
681 ∀p: joint_program … pars. res (state_pc pars) ≝
682λpars,p.
683  let sem_globals ≝ make_global pars p in
684  let ge ≝ genv2 sem_globals in
685  let m ≝ alloc_mem … p in
686  let 〈m,spb〉 ≝ alloc … m 0 external_ram_size XData in
687  let 〈m,ispb〉 ≝ alloc … m 0 internal_ram_size XData in
688  let dummy_pc ≝ mk_pointer Code (mk_block Code (-1)) ? (mk_offset 0) in
689  let spp ≝ mk_pointer XData spb ? (mk_offset external_ram_size) in
690  let ispp ≝ mk_pointer XData ispb ? (mk_offset 47) in
691  let main ≝ prog_main … p in
692  let st0 ≝ mk_state pars (empty_framesT …) spp ispp BVfalse (empty_regsT … spp) m in
693  (* use exit sem_globals as ra and call_dest_for_main as dest *)
694  let st0' ≝ set_frms ? (save_frame … (exit sem_globals) (call_dest_for_main … pars) st0) st0 in
695  let st_pc0 ≝ mk_state_pc ? st0' dummy_pc in
696  ! main_block ← opt_to_res … [MSG MissingSymbol; CTX ? main] (find_symbol … ge main) ;
697  ! main_fd ← opt_to_res ? [MSG BadPointer] (find_funct_ptr … ge main_block) ;
698  match main_fd with
699  [ Internal fn ⇒
700    do_call ?? ge st_pc0 (block_id main_block) fn (call_args_for_main … pars)
701  | External _ ⇒ Error … [MSG ExternalMain] (* External main not supported: why? *)
702  ]. [5: cases ispb * |6: cases spb * ] (* without try it fails! *) try //
703qed.
704
705definition joint_fullexec :
706 ∀pars:sem_params.fullexec io_out io_in ≝
707 λpars.mk_fullexec ??? joint_exec (make_global pars) (make_initial_state pars).
708*)
Note: See TracBrowser for help on using the repository browser.