source: src/joint/semantics.ma @ 2564

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

ERTL fully repaired, useless part of return value of pop_ra
removed.

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