source: src/joint/joint_semantics.ma @ 2638

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

Back-end fixes for last Garnier's commit that removes the regions from
the blocks. Only part of the back-end has been fixed.

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