source: src/joint/semantics.ma @ 2470

Last change on this file since 2470 was 2470, checked in by tranquil, 7 years ago

completely separated program counters from code pointers in joint languages: the advantage is program counters with an unbounded offset in Pos

File size: 30.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".
7
8(* CSC: external functions never fail (??) and always return something of the
9   size of one register, both in the frontend and in the backend.
10   Is this reasonable??? In OCaml it always return a list, but in the frontend
11   only the head is kept (or Undef if the list is empty) ??? *)
12
13definition is_function ≝ λF.λglobals : list ident.λge : genv_t (fundef (F globals)).
14  λi : ident.∃fd.
15    ! bl ← find_symbol … ge i ;
16    find_funct_ptr … ge bl = Some ? fd.
17
18definition description_of_function : ∀F,globals,ge.(Σi.is_function F globals ge i) →
19fundef (F globals) ≝
20λF,globals,ge,i.
21match ! bl ← find_symbol … ge i ;
22        find_funct_ptr … ge bl
23return λx.(∃fd.x = ?) → ?
24with
25[ Some fd ⇒ λ_.fd
26| None ⇒ λprf.⊥
27] (pi2 … i).
28cases prf #fd #ABS destruct
29qed.
30
31definition is_internal_function ≝ λF.λglobals : list ident.λge : genv_t (fundef (F globals)).
32  λi : ident.∃fd.
33    ! bl ← find_symbol … ge i ;
34    find_funct_ptr … ge bl = Some ? (Internal ? fd).
35
36lemma description_of_internal_function : ∀F,globals,ge,i,fn.
37  description_of_function F globals ge i = Internal ? fn → is_internal_function … ge i.
38#F #globals #ge * #i * #fd #EQ
39#fn whd in ⊢ (??%?→?); >EQ normalize nodelta #EQ' >EQ' in EQ; #EQ
40%{EQ}
41qed.
42
43lemma internal_function_is_function : ∀F,globals,ge,i.
44  is_internal_function F globals ge i → is_function … ge i.
45#F #globals #ge #i * #fn #prf %{prf} qed.
46
47definition if_of_function : ∀F,globals,ge.(Σi.is_internal_function F globals ge i) →
48F globals ≝
49λF,globals,ge,i.
50match ! bl ← find_symbol … ge i ;
51        find_funct_ptr … ge bl
52return λx.(∃fn.x = ?) → ?
53with
54[ Some fd ⇒
55  match fd return λx.(∃fn.Some ? x = ?) → ? with
56  [ Internal fn ⇒ λ_.fn
57  | External _ ⇒ λprf.⊥
58  ]
59| None ⇒ λprf.⊥
60] (pi2 … i).
61cases prf #fn #ABS destruct
62qed.
63
64(* Paolo: I'll put in this record the property about genv we need *)
65record genv_gen (F : list ident → Type[0]) (globals : list ident) : Type[0] ≝
66{ ge :> genv_t (fundef (F globals))
67; find_symbol_exists : ∀id.In ? globals id → find_symbol … ge id ≠ None ?
68; stack_sizes : (Σi.is_internal_function F globals ge i) → ℕ
69}.
70
71definition genv ≝ λp.genv_gen (joint_closed_internal_function p).
72coercion genv_to_genv_t :
73  ∀p,globals.∀g : genv p globals.genv_t (joint_function p globals) ≝
74  λp,globals,g.ge ?? g on _g : genv ?? to genv_t ?.
75
76record sem_state_params : Type[1] ≝
77 { framesT: Type[0]
78 ; empty_framesT: framesT
79 ; regsT : Type[0]
80 ; empty_regsT: xpointer → regsT (* initial stack pointer *)
81 ; load_sp : regsT → res xpointer
82 ; save_sp : regsT → xpointer → regsT
83 }.
84
85inductive internal_stack : Type[0] ≝
86| empty_is : internal_stack
87| one_is : beval → internal_stack
88| both_is : beval → beval → internal_stack.
89
90axiom InternalStackFull : String.
91axiom InternalStackEmpty : String.
92
93definition is_push : internal_stack → beval → res internal_stack ≝
94λis,bv.match is with
95[ empty_is ⇒ return one_is bv
96| one_is bv' ⇒ return both_is bv' bv
97| both_is _ _ ⇒ Error … [MSG … InternalStackFull]
98].
99
100definition is_pop : internal_stack → res (beval × internal_stack) ≝
101λis.match is with
102[ empty_is ⇒ Error … [MSG … InternalStackEmpty]
103| one_is bv' ⇒ return 〈bv', empty_is〉
104| both_is bv bv' ⇒ return 〈bv', one_is bv〉
105].
106
107record state (semp: sem_state_params): Type[0] ≝
108 { st_frms: framesT semp
109 ; istack : internal_stack
110 ; carry: bebit
111 ; regs: regsT semp
112 ; m: bemem
113 }.
114
115definition sp ≝ λp,st.load_sp p (regs ? st).
116
117record state_pc (semp : sem_state_params) : Type[0] ≝
118  { st_no_pc :> state semp
119  ; pc : program_counter
120  }.
121
122definition set_m: ∀p. bemem → state p → state p ≝
123 λp,m,st. mk_state p (st_frms …st) (istack … st) (carry … st) (regs … st) m.
124
125definition set_regs: ∀p:sem_state_params. regsT p → state p → state p ≝
126 λp,regs,st.mk_state p (st_frms … st) (istack … st) (carry … st) regs (m … st).
127
128definition set_sp: ∀p. ? → state p → state p ≝
129 λp,sp,st.let regs' ≝ save_sp … (regs … st) sp in
130 mk_state p (st_frms … st) (istack … st) (carry … st) regs' (m … st).
131
132definition set_carry: ∀p. bebit → state p → state p ≝
133 λp,carry,st. mk_state … (st_frms … st) (istack … st) carry (regs … st) (m … st).
134
135definition set_istack: ∀p. internal_stack → state p → state p ≝
136 λp,is,st. mk_state … (st_frms … st) is (carry … st) (regs … st) (m … st).
137
138definition set_pc: ∀p. ? → state_pc p → state_pc p ≝
139 λp,pc,st. mk_state_pc … (st_no_pc … st) pc.
140
141definition set_no_pc: ∀p. ? → state_pc p → state_pc p ≝
142 λp,s,st. mk_state_pc … s (pc … st).
143
144definition set_frms: ∀p:sem_state_params. framesT p → state p → state p ≝
145 λp,frms,st. mk_state … frms (istack … st) (carry … st) (regs … st) (m … st).
146
147axiom BadProgramCounter : String.
148
149(*
150inductive step_flow (p : unserialized_params) (F : Type[0]) : possible_flows → Type[0] ≝
151  | Redirect : ∀lbls.(Σl.In ? lbls l) → step_flow p F (Labels lbls) (* used for goto-like flow alteration *)
152  | Init     : Z → F → call_args p → call_dest p → step_flow p F Call (* call a function with given id, then proceed *)
153  | Proceed  : ∀flows.step_flow p F flows. (* go to implicit successor *)
154
155inductive fin_step_flow (p : unserialized_params) (F : Type[0]) : possible_flows → Type[0] ≝
156  | FRedirect : ∀lbls.(Σl.In ? lbls l) → fin_step_flow p F (Labels lbls)
157  | FTailInit : Z → F → call_args p → fin_step_flow p F Call
158  | FEnd1  : fin_step_flow p F (Labels [ ]) (* end flow *)
159  | FEnd2  : fin_step_flow p F Call. (* end flow *)
160*)
161
162definition funct_of_ident : ∀F,globals,ge.
163  ident → option (Σi.is_function F globals ge i)
164≝ λF,globals,ge,i.
165match ?
166return λx.! bl ← find_symbol … ge i ;
167    find_funct_ptr … ge bl = x → ?
168with
169[ Some fd ⇒ λprf.return «i, ex_intro ?? fd prf»
170| None ⇒ λ_.None ?
171] (refl …).
172
173lemma match_opt_prf_elim : ∀A,B : Type[0].∀m : option A.
174∀Q : option A → Prop.
175∀c1 : ∀a.Q (Some ? a) → B.
176∀c2 : Q (None ?) → B.
177∀P : B → Prop.
178(∀a,prf.P (c1 a prf)) →
179(∀prf.P (c2 prf)) →
180∀prf : Q m.
181P (match m return λx.Q x → ? with
182   [ Some a ⇒ λprf.c1 a prf
183   | None ⇒ λprf.c2 prf
184   ] prf).
185#A #B * [2: #a ] #Q #c1 #c2 #P #H1 #H2 #prf
186normalize [@H1 | @H2]
187qed.
188
189lemma symbol_of_function_block_ok :
190  ∀F,ge,b,prf.symbol_for_block F ge b = Some ? (symbol_of_function_block F ge b prf).
191#F #ge #b #FFP
192whd in ⊢ (???(??%));
193@match_opt_prf_elim [//] #H @⊥
194(* cut and paste from global env *)
195whd in H:(??%?);
196cases b in FFP H ⊢ %; * * -b [2,3,5,6: #b ] normalize in ⊢ (% → ?); [4: #FFP | *: * #H cases (H (refl ??)) ]
197cases (functions_inv … ge b FFP)
198#id #L lapply (find_lookup ?? (symbols F ge) (λid',b'. eq_block (mk_block Code (neg b)) b') id (mk_block Code (neg b)))
199lapply (find_none … (symbols F ge) (λid',b'. eq_block (mk_block Code (neg b)) b') id (mk_block Code (neg b)))
200cases (find ????)
201[ #H #_ #_ lapply (H (refl ??) L) @eq_block_elim [ #_ * | * #H' cases (H' (refl ??)) ]
202| * #id' #b' #_ normalize #_ #E destruct
203] qed.
204
205definition funct_of_block : ∀F,globals,ge.
206  block → option  (Σi.is_function F globals ge i) ≝
207λF,globals,ge,bl.
208   match find_funct_ptr … ge bl
209   return λx.find_funct_ptr … ge bl = x → ? with
210   [ Some fd ⇒ λprf.return mk_Sig
211        ident (λi.is_function F globals ge i)
212        (symbol_of_function_block … ge bl ?)
213        (ex_intro … fd ?)
214   | None ⇒ λ_.None ?
215   ] (refl …).
216[ >(symbol_of_block_rev … (symbol_of_function_block_ok ? ge bl ?)) @prf
217| >prf % #ABS destruct(ABS)
218]
219qed.
220
221definition int_funct_of_block : ∀F,globals,ge.
222  block → option (Σi.is_internal_function F globals ge i) ≝
223  λF,globals,ge,bl.
224  ! f ← funct_of_block … ge bl ;
225  match ?
226  return λx.description_of_function … f = x → option (Σi.is_internal_function … ge i)
227  with
228  [ Internal fn ⇒ λprf.return «pi1 … f, ?»
229  | External fn ⇒ λ_.None ?
230  ] (refl …).
231@(description_of_internal_function … prf)
232qed.
233
234(* bevals hold a function pointer (BVptr) *)
235definition funct_of_bevals : ∀F,globals,ge.
236  beval → beval → option (Σi.is_function F globals ge i) ≝
237λF,globals,ge,dpl,dph.
238! ptr ← res_to_opt … (pointer_of_address 〈dpl, dph〉) ;
239if eq_bv … (bv_zero …) (offv (poff ptr)) ∧ (* ← check this condition in front end *)
240   match ptype ptr with [ Code ⇒ true | _ ⇒ false] then
241   funct_of_block … (pblock ptr)
242else None ?.
243
244definition block_of_funct_ident ≝ λF,globals,ge.
245  λi : Σi.is_function F globals ge i.
246  match find_symbol … ge i return λx.(∃fd.!bl ← x; ? = ?) → ? with
247  [ Some bl ⇒ λ_.bl
248  | None ⇒ λprf.⊥
249  ] (pi2 … i).
250cases prf #fd normalize #ABS destruct(ABS)
251qed.
252
253axiom ProgramCounterOutOfCode : String.
254axiom PointNotFound : String.
255axiom LabelNotFound : String.
256axiom MissingSymbol : String.
257axiom FailedLoad : String.
258axiom BadFunction : String.
259axiom SuccessorNotProvided : String.
260axiom BadPointer : String.
261
262(* this can replace graph_fetch function and lin_fetch_function *)
263definition fetch_function:
264 ∀pars : params.
265 ∀globals.
266 ∀ge : genv pars globals.
267  program_counter →
268  res (Σi.is_internal_function … ge i) ≝
269 λpars,globals,ge,p.
270 opt_to_res … [MSG BadFunction; MSG BadPointer]
271    (int_funct_of_block … ge (pc_block p)).
272
273record sem_unserialized_params
274  (uns_pars : unserialized_params)
275  (F : list ident → Type[0]) : Type[1] ≝
276  { st_pars :> sem_state_params
277
278  ; acca_store_ : acc_a_reg uns_pars → beval → regsT st_pars → res (regsT st_pars)
279  ; acca_retrieve_ : regsT st_pars → acc_a_reg uns_pars → res beval
280  ; acca_arg_retrieve_ : regsT st_pars → acc_a_arg uns_pars → res beval
281  ; accb_store_ : acc_b_reg uns_pars → beval → regsT st_pars → res (regsT st_pars)
282  ; accb_retrieve_ : regsT st_pars → acc_b_reg uns_pars → res beval
283  ; accb_arg_retrieve_ : regsT st_pars → acc_b_arg uns_pars → res beval
284  ; dpl_store_ : dpl_reg uns_pars → beval → regsT st_pars → res (regsT st_pars)
285  ; dpl_retrieve_ : regsT st_pars → dpl_reg uns_pars → res beval
286  ; dpl_arg_retrieve_ : regsT st_pars → dpl_arg uns_pars → res beval
287  ; dph_store_ : dph_reg uns_pars → beval → regsT st_pars → res (regsT st_pars)
288  ; dph_retrieve_ : regsT st_pars → dph_reg uns_pars → res beval
289  ; dph_arg_retrieve_ : regsT st_pars → dph_arg uns_pars → res beval
290  ; snd_arg_retrieve_ : regsT st_pars → snd_arg uns_pars → res beval
291  ; pair_reg_move_ : regsT st_pars → pair_move uns_pars → res (regsT st_pars)
292  ; fetch_ra: state st_pars → res (program_counter × (state st_pars))
293
294  ; allocate_local : localsT uns_pars → regsT st_pars → regsT st_pars
295  (* Paolo: save_frame separated from call_setup to factorize tailcall code *)
296  ; save_frame: program_counter → call_dest uns_pars → state st_pars → res (state st_pars)
297   (*CSC: setup_call returns a res only because we can call a function with the wrong number and
298     type of arguments. To be fixed using a dependent type *)
299  ; setup_call : nat → paramsT … uns_pars → call_args uns_pars →
300      state st_pars → res (state st_pars)
301  ; fetch_external_args: external_function → state st_pars → call_args … uns_pars →
302      res (list val)
303  ; set_result: list val → call_dest uns_pars → state st_pars → res (state st_pars)
304  ; call_args_for_main: call_args uns_pars
305  ; call_dest_for_main: call_dest uns_pars
306
307  (* from now on, parameters that use the type of functions *)
308  ; read_result: ∀globals.genv_gen F globals → call_dest uns_pars → state st_pars → res (list beval)
309  (* change of pc must be left to *_flow execution *)
310  ; eval_ext_seq: ∀globals.∀ge : genv_gen F globals.ext_seq uns_pars →
311    (Σi.is_internal_function … ge i) (* current *) → state st_pars → IO io_out io_in (state st_pars)
312  ; pop_frame: ∀globals.∀ge : genv_gen F globals.
313    (Σi.is_internal_function … ge i) (* current *) → state st_pars → res (state st_pars)
314  }.
315
316(*coercion msu_pars_to_ss_pars nocomposites :
317∀p,F.∀msup : more_sem_unserialized_params p F.sem_state_params
318 ≝ st_pars
319on _msup : more_sem_unserialized_params ?? to sem_state_params.*)
320
321
322definition helper_def_retrieve :
323  ∀X : ? → ? → ? → Type[0].
324  (∀up,F.∀p:sem_unserialized_params up F. regsT (st_pars up F p) → X up F p → res beval) →
325  ∀up,F.∀p : sem_unserialized_params up F.state (st_pars up F p) → X up F p → res beval ≝
326    λX,f,up,F,p,st.f ?? p (regs … st).
327
328definition helper_def_store :
329  ∀X : ? → ? → ? → Type[0].
330  (∀up,F.∀p : sem_unserialized_params up F.X up F p → beval → regsT (st_pars … p) → res (regsT (st_pars … p))) →
331  ∀up,F.∀p : sem_unserialized_params up F.X up F p → beval → state (st_pars … p) → res (state (st_pars … p)) ≝
332  λX,f,up,F,p,x,v,st.! r ← f ?? p x v (regs … st) ; return set_regs … r st.
333
334definition acca_retrieve ≝ helper_def_retrieve ? acca_retrieve_.
335definition acca_store ≝ helper_def_store ? acca_store_.
336definition acca_arg_retrieve ≝ helper_def_retrieve ? acca_arg_retrieve_.
337definition accb_store ≝ helper_def_store ? accb_store_.
338definition accb_retrieve ≝ helper_def_retrieve ? accb_retrieve_.
339definition accb_arg_retrieve ≝ helper_def_retrieve ? accb_arg_retrieve_.
340definition dpl_store ≝ helper_def_store ? dpl_store_.
341definition dpl_retrieve ≝ helper_def_retrieve ? dpl_retrieve_.
342definition dpl_arg_retrieve ≝ helper_def_retrieve ? dpl_arg_retrieve_.
343definition dph_store ≝ helper_def_store ? dph_store_.
344definition dph_retrieve ≝ helper_def_retrieve ? dph_retrieve_.
345definition dph_arg_retrieve ≝ helper_def_retrieve ? dph_arg_retrieve_.
346definition snd_arg_retrieve ≝ helper_def_retrieve ? snd_arg_retrieve_.
347definition pair_reg_move ≝
348  λup,F.λp : sem_unserialized_params up F.λst : state (st_pars … p).λpm : pair_move up.
349    ! r ← pair_reg_move_ ?? p (regs ? st) pm;
350    return set_regs ? r st.
351 
352axiom FailedStore: String.
353
354definition push: ∀p.state p → beval → res (state p) ≝
355 λp,st,v.
356 ! is ← is_push (istack … st) v ;
357 return set_istack … is st.
358
359definition pop: ∀p. state p → res (beval × (state p)) ≝
360 λp,st.
361 ! 〈bv, is〉 ← is_pop (istack … st) ;
362 return 〈bv, set_istack … is st〉.
363
364definition save_ra : ∀p. state p → program_counter → res (state p) ≝
365 λp,st,l.
366  let 〈addrl,addrh〉 ≝  beval_pair_of_pc l in
367  ! st' ← push … st addrl;
368  push … st' addrh.
369
370definition load_ra : ∀p.state p → res (program_counter × (state p)) ≝
371 λp,st.
372  ! 〈addrh, st'〉 ← pop … st;
373  ! 〈addrl, st''〉 ← pop … st';
374  ! pr ← pc_of_bevals [addrh; addrl];
375  return 〈pr, st''〉.
376
377(* parameters that are defined by serialization *)
378record more_sem_params (pp : params) : Type[1] ≝
379  { msu_pars :> sem_unserialized_params pp (joint_closed_internal_function pp)
380  ; offset_of_point : code_point pp → Pos
381  ; point_of_offset : Pos → code_point pp
382  ; point_of_offset_of_point :
383    ∀pt.point_of_offset (offset_of_point pt) = pt
384  ; offset_of_point_of_offset :
385    ∀o.offset_of_point (point_of_offset o) = o
386  }.
387
388(*
389coercion ms_pars_to_msu_pars nocomposites :
390∀p : params.∀msp : more_sem_params p.more_sem_unserialized_params p (λglobals.joint_internal_function globals p)
391 ≝ msu_pars
392on _msp : more_sem_params ? to more_sem_unserialized_params ??.
393
394definition ss_pars_of_ms_pars ≝
395  λp.λpp : more_sem_params p.
396  st_pars … (msu_pars … pp).
397coercion ms_pars_to_ss_pars nocomposites :
398∀p : params.∀msp : more_sem_params p.sem_state_params ≝
399ss_pars_of_ms_pars on _msp : more_sem_params ? to sem_state_params.*)
400
401definition pc_of_point : ∀p.more_sem_params p →
402  program_counter → code_point p → program_counter ≝
403  λp,msp,ptr,pt.
404  mk_program_counter (pc_block ptr) (offset_of_point ? msp pt).
405
406definition point_of_pc :
407  ∀p.more_sem_params p → program_counter → code_point p ≝
408  λp,msp,ptr.point_of_offset p msp (pc_offset ptr).
409
410lemma point_of_pointer_of_point :
411  ∀p,msp.∀ptr,pt.
412  point_of_pc ? msp (pc_of_point p msp ptr pt) = pt.
413#p #msp #ptr #pt normalize // qed.
414
415lemma pointer_of_point_block :
416  ∀p,msp,ptr,pt.
417  pc_block (pc_of_point p msp ptr pt) = pc_block ptr.
418#p #msp #ptr #pt % qed. (* can probably do without *)
419
420lemma pointer_of_point_uses_block :
421  ∀p,msp.∀ptr1,ptr2.∀pt.pc_block ptr1 = pc_block ptr2 →
422    pc_of_point p msp ptr1 pt = pc_of_point p msp ptr2 pt.
423#p #msp #ptr1 #ptr2 #pc #EQ normalize >EQ % qed.
424
425lemma pointer_of_point_of_pointer :
426  ∀p,msp.∀ptr1,ptr2.
427    pc_block ptr1 = pc_block ptr2 →
428    pc_of_point p msp ptr1 (point_of_pc p msp ptr2) = ptr2.
429#p #msp #ptr1 * #bl2 #o2 #EQ normalize >offset_of_point_of_offset >EQ % qed.
430
431definition fetch_statement: ∀p : params.∀ msp : more_sem_params p.∀globals.
432  ∀ge:genv p globals. program_counter →
433  res ((Σi.is_internal_function … ge i) × (joint_statement p globals)) ≝
434  λp,msp,globals,ge,ptr.
435  ! f ← fetch_function … ge ptr ;
436  let fn ≝ if_of_function … f in
437  let pt ≝ point_of_pc ? msp ptr in
438  ! stmt ← opt_to_res … (msg ProgramCounterOutOfCode) (stmt_at … (joint_if_code … fn) pt);
439  return 〈f, stmt〉.
440
441definition pc_of_label : ∀p : params.∀ msp : more_sem_params p.∀globals.
442  genv p globals → program_counter → label → res program_counter ≝
443  λp,msp,globals,ge,ptr,lbl.
444  ! f ← fetch_function … ge ptr ;
445  let fn ≝ if_of_function …  ge f in
446  ! pt ← opt_to_res … [MSG LabelNotFound ; CTX ? lbl]
447            (point_of_label … (joint_if_code … fn) lbl) ;
448  return pc_of_point p msp ptr pt.
449
450definition succ_pc : ∀p : params.∀ msp : more_sem_params p.
451  program_counter → succ p → program_counter ≝
452  λp,msp,ptr,nxt.
453  let curr ≝ point_of_pc p msp ptr in
454  pc_of_point p msp ptr (point_of_succ p curr nxt).
455
456record sem_params : Type[1] ≝
457  { spp :> params
458  ; more_sem_pars :> more_sem_params spp
459  }.
460
461(* definition msu_pars_of_s_pars :
462∀p : sem_params.more_sem_unserialized_params (spp p) (λglobals.joint_internal_function globals (spp p))
463≝ λp : sem_params.
464  msu_pars … (more_sem_pars p).
465coercion s_pars_to_msu_pars nocomposites :
466∀p : sem_params.more_sem_unserialized_params (spp p) (λglobals.joint_internal_function globals (spp p)) ≝
467msu_pars_of_s_pars
468on p : sem_params to more_sem_unserialized_params ??.
469
470definition ss_pars_of_s_pars :
471∀p : sem_params.sem_state_params
472≝ λp : sem_params.
473  st_pars … (msu_pars … (more_sem_pars p)).
474coercion s_pars_to_ss_pars nocomposites :
475∀p : sem_params.sem_state_params ≝
476ss_pars_of_s_pars
477on _p : sem_params to sem_state_params.
478
479definition ms_pars_of_s_pars :
480∀p : sem_params.more_sem_params (spp p)
481≝ more_sem_pars.
482coercion s_pars_to_ms_pars nocomposites :
483∀p : sem_params.more_sem_params (spp p) ≝
484ms_pars_of_s_pars
485on p : sem_params to more_sem_params ?.*)
486
487(* definition address_of_label: ∀globals. ∀p:sem_params.
488  genv globals p → pointer → label → res address ≝
489 λglobals,p,ge,ptr,l.
490  do newptr ← pointer_of_label … p ? ge … ptr l ;
491  OK … (address_of_code_pointer newptr). *)
492
493definition goto: ∀globals.∀p : sem_params.
494  genv p globals → label → state p → program_counter → res (state_pc p) ≝
495 λglobals,p,ge,l,st,b.
496  ! newpc ← pc_of_label ? p … ge b l ;
497  return mk_state_pc ? st newpc.
498
499(*
500definition empty_state: ∀p. more_sem_params p → state p ≝
501 mk_state … (empty_framesT …)
502*)
503
504definition next : ∀p : sem_params.succ p → state p → program_counter → state_pc p ≝
505 λp,l,st,pc.
506 let newpc ≝ succ_pc ? p … pc l in
507 mk_state_pc … st newpc.
508
509
510definition function_of_call ≝ λp:sem_params.λglobals.
511  λge: genv p globals.λst : state p.λf.
512  match f with
513  [ inl id ⇒
514    opt_to_res … [MSG BadFunction; MSG MissingSymbol; CTX ? id] (funct_of_ident … ge id)
515  | inr addr ⇒
516    ! addr_l ← dpl_arg_retrieve … st (\fst addr) ;
517    ! addr_h ← dph_arg_retrieve … st (\snd addr) ;
518    opt_to_res … [MSG BadFunction; MSG BadPointer] (funct_of_bevals … ge addr_l addr_h)
519  ].
520
521(* Paolo: why external calls do not need args?? *)
522definition eval_external_call ≝
523λp,F.λp' : sem_unserialized_params p F.λfn,args,dest,st.
524      ! params ← fetch_external_args … p' fn st args : IO ???;
525      ! evargs ← check_eventval_list params (sig_args (ef_sig fn)) : IO ???;
526      ! evres ← do_io (ef_id fn) evargs (proj_sig_res (ef_sig fn));
527      (* CSC: XXX bug here; I think I should split it into Byte-long
528         components; instead I am making a singleton out of it. To be
529         fixed once we fully implement external functions. *)
530      let vs ≝ [mk_val ? evres] in
531      set_result … p' vs dest st.
532
533lemma block_of_funct_ident_is_code : ∀F,globals,ge,i.
534  block_region (block_of_funct_ident F globals ge i) = Code.
535#F #globals #ge * #i * #fd
536whd in ⊢ (?→??(?%)?);
537cases (find_symbol ???)
538[ #ABS normalize in ABS; destruct(ABS) ]
539#bl normalize nodelta >m_return_bind
540whd in ⊢ (??%?→?); cases (block_region bl)
541[ #ABS normalize in ABS; destruct(ABS) ]
542#_ %
543qed.
544
545definition eval_internal_call_pc ≝
546λp : sem_params.λglobals : list ident.λge : genv p globals.λi.
547let fn ≝ if_of_function … ge i in
548let l' ≝ joint_if_entry ?? fn in
549mk_program_counter (block_of_funct_ident … ge (pi1 … i)) (offset_of_point ? p … l').
550[ @block_of_funct_ident_is_code
551| cases i /2 by internal_function_is_function/
552]
553qed.
554
555definition eval_internal_call_no_pc ≝
556λp : sem_params.λglobals : list ident.λge : genv p globals.λi,args,st.
557let fn ≝ if_of_function … ge i in
558let stack_size ≝ stack_sizes … ge i in
559! st' ← setup_call … stack_size (joint_if_params … fn) args st ;
560let regs ≝ foldr ?? (allocate_local … p) (regs … st) (joint_if_locals … fn) in
561return set_regs p regs st.
562
563definition eval_seq_no_pc :
564 ∀p:sem_params.∀globals.∀ge:genv p globals. (Σi.is_internal_function … ge i) →
565  state p → program_counter → joint_seq p globals →
566  IO io_out io_in (state p) ≝
567 λp,globals,ge,curr_fn,st,next,seq.
568 match seq return λx.IO ??? with
569  [ extension_seq c ⇒
570    eval_ext_seq … ge c curr_fn st
571  | LOAD dst addrl addrh ⇒
572    ! vaddrh ← dph_arg_retrieve … st addrh ;
573    ! vaddrl ← dpl_arg_retrieve … st addrl;
574    ! vaddr ← pointer_of_address 〈vaddrl,vaddrh〉;
575    ! v ← opt_to_res … (msg FailedLoad) (beloadv (m … st) vaddr);
576    acca_store p … dst v st
577 | STORE addrl addrh src ⇒
578    ! vaddrh ← dph_arg_retrieve … st addrh;
579    ! vaddrl ← dpl_arg_retrieve … st addrl;
580    ! vaddr ← pointer_of_address 〈vaddrl,vaddrh〉;
581    ! v ← acca_arg_retrieve … st src;
582    ! m' ← opt_to_res … (msg FailedStore) (bestorev (m … st) vaddr v);
583    return set_m … m' st
584  | ADDRESS id prf ldest hdest ⇒
585    let addr_block ≝ opt_safe ? (find_symbol … ge id) ? in
586    let 〈laddr,haddr〉 ≝ beval_pair_of_pointer (mk_pointer addr_block zero_offset) in
587    ! st' ← dpl_store … ldest laddr st;
588    dph_store … hdest haddr st'
589  | OP1 op dacc_a sacc_a ⇒
590    ! v ← acca_retrieve … st sacc_a;
591    ! v' ← be_op1 op v ;
592    acca_store … dacc_a v' st
593  | OP2 op dacc_a sacc_a src ⇒
594    ! v1 ← acca_arg_retrieve … st sacc_a;
595    ! v2 ← snd_arg_retrieve … st src;
596    ! 〈v',carry〉 ← be_op2 (carry … st) op v1 v2 ;
597    ! st' ← acca_store … dacc_a v' st;
598    return set_carry … carry st'
599  | CLEAR_CARRY ⇒
600    return set_carry … (BBbit false) st
601  | SET_CARRY ⇒
602    return set_carry … (BBbit true) st
603  | OPACCS op dacc_a_reg dacc_b_reg sacc_a_reg sacc_b_reg ⇒
604    ! v1 ← acca_arg_retrieve … st sacc_a_reg;
605    ! v2 ← accb_arg_retrieve … st sacc_b_reg;
606    ! 〈v1',v2'〉 ← be_opaccs op v1 v2 ;
607    ! st' ← acca_store … dacc_a_reg v1' st;
608    accb_store … dacc_b_reg v2' st'
609  | POP dst ⇒
610    ! 〈v, st'〉 ← pop p st;
611    acca_store … p dst v st'
612  | PUSH src ⇒
613    ! v ← acca_arg_retrieve … st src;
614    push … st v
615  | MOVE dst_src ⇒
616    pair_reg_move … st dst_src
617  | CALL f args dest ⇒
618    ! fn ← function_of_call … ge st f : IO ???;
619    match description_of_function … fn return λx.description_of_function … fn = x → ? with
620    [ Internal fd ⇒ λprf.
621      ! st' ← save_frame … next dest st ;
622      eval_internal_call_no_pc … ge «fn, ?» args st'  (* only pc changes *)
623    | External fd ⇒ λ_.eval_external_call … fd args dest st
624    ] (refl …)
625  | _ ⇒ return st
626  ].
627[ @find_symbol_exists
628  lapply prf
629  elim globals [*]
630  #hd #tl #IH * [@eq_identifier_elim #H * >H %1 % ]
631  #G %2 @IH @G
632| @(description_of_internal_function … prf)
633]
634qed.
635
636definition eval_seq_pc :
637 ∀p:sem_params.∀globals.∀ge:genv p globals.
638  state p → program_counter → joint_seq p globals →
639  res program_counter ≝
640  λp,globals,ge,st,next,s.
641  match s with
642  [ CALL f args dest ⇒
643    ! fn ← function_of_call … ge st f;
644    match ? return λx.description_of_function … fn = x → ? with
645    [ Internal _ ⇒ λprf.return eval_internal_call_pc … ge «fn, ?»
646    | External _ ⇒ λ_.return next
647    ] (refl …)
648  | _ ⇒ return next
649  ].
650@(description_of_internal_function … prf)
651qed.
652
653definition eval_statement :
654 ∀p:sem_params.∀globals.∀ge:genv p globals.
655 (Σi.is_internal_function … ge i) → state_pc p →
656  ∀s:joint_statement p globals.
657  IO io_out io_in (state_pc p) ≝
658  λp,g,ge,curr_fn,st,s.
659  match s with
660  [ sequential s next ⇒
661    let next_ptr ≝ succ_pc ? p (pc … st) next in
662    match s return λ_.IO ??? with
663    [ step_seq s ⇒
664      ! st' ← eval_seq_no_pc … ge curr_fn st next_ptr s ;
665      ! pc' ← eval_seq_pc … ge st next_ptr s ;
666      return mk_state_pc … st' pc'
667    | COND a l ⇒
668      ! v ← acca_retrieve … st a ;
669      ! b ← bool_of_beval … v ;
670      ! pc' ←
671        if b then
672          pc_of_label ? p … ge (pc … st) l
673        else
674          return succ_pc ? p (pc … st) next ;
675      return mk_state_pc … st pc'
676    ]
677  | final s ⇒
678    match s with
679    [ GOTO l ⇒
680      ! pc' ← pc_of_label ? p ? ge (pc … st) l ;
681      return mk_state_pc … st pc'
682    | RETURN ⇒
683      ! st' ← pop_frame … curr_fn st ;
684      ! 〈pc', st''〉 ← fetch_ra … p st' ;
685      return mk_state_pc … st'' pc'
686    | TAILCALL _ f args ⇒
687      ! fn ← function_of_call … ge st f : IO ???;
688      match ? return λx.description_of_function … fn = x → ? with
689      [ Internal _ ⇒ λprf.
690        let pc' ≝ eval_internal_call_pc … ge «fn, ?» in
691        return mk_state_pc … st pc'
692      | External fd ⇒ λ_.
693        let curr_dest ≝ joint_if_result ?? (if_of_function … curr_fn) in
694        ! st' ← eval_external_call ??? fd args curr_dest st ;
695        ! st'' ← pop_frame … curr_fn st ;
696        ! 〈pc', st'''〉 ← fetch_ra … p st'' ;
697        return mk_state_pc … st''' pc'
698      ] (refl …)
699    ]
700  ].
701@(description_of_internal_function … prf)
702qed.
703
704definition eval_state : ∀globals: list ident.∀p:sem_params. genv p globals →
705  state_pc p → IO io_out io_in (state_pc p) ≝
706  λglobals,p,ge,st.
707  ! 〈fn,s〉 ← fetch_statement ? p … ge (pc … st) : IO ???;
708  eval_statement … ge fn st s.
709
710(* Paolo: what if in an intermediate language main finishes with an external
711  tailcall? Maybe it should rely on an FEnd flow command issued, but that's
712  not static... *)
713definition is_final: ∀globals:list ident. ∀p: sem_params.
714  genv p globals → program_counter → state_pc p → option int ≝
715 λglobals,p,ge,exit,st.res_to_opt ? (
716  do 〈f,s〉 ← fetch_statement ? p … ge (pc … st);
717  let fn ≝ if_of_function … f in
718  match s with
719  [ final s' ⇒
720    match s' with
721    [ RETURN ⇒
722      do 〈ra, st'〉 ← fetch_ra … st;
723      if eq_program_counter ra exit then
724       do vals ← read_result … ge (joint_if_result … fn) st' ;
725       Word_of_list_beval vals
726      else
727       Error ? [ ]
728   | _ ⇒ Error ? [ ]
729   ]
730 | _ ⇒ Error ? [ ]
731 ]).
732
733(*
734record evaluation_parameters : Type[1] ≝
735 { globals: list ident
736 ; sparams:> sem_params
737 ; exit: program_counter
738 ; genv2: genv globals sparams
739 }.
740
741(* Paolo: with structured traces, eval need not emit labels. However, this
742  changes trans_system. For now, just putting a dummy thing for
743  the transition. *)
744definition joint_exec: trans_system io_out io_in ≝
745  mk_trans_system … evaluation_parameters (λG. state_pc G)
746   (λG.is_final (globals G) G (genv2 G) (exit G))
747   (λG,st.! 〈flag,st'〉 ← eval_state_flag (globals G) G (genv2 G) st ; return 〈E0, st'〉).
748
749definition make_global :
750 ∀pars: sem_params.
751  joint_program pars → evaluation_parameters
752
753 λpars.
754 (* Invariant: a -1 block is unused in common/Globalenvs *)
755 let b ≝ mk_block Code (-1) in
756 let ptr ≝ mk_pointer Code b ? (mk_offset 0) in
757  (λp. mk_evaluation_parameters
758    (prog_var_names … p)
759    (mk_sem_params … pars)
760    ptr
761    (globalenv_noinit … p)
762  ).
763% qed.
764
765axiom ExternalMain: String.
766
767definition make_initial_state :
768 ∀pars: sem_params.
769 ∀p: joint_program … pars. res (state_pc pars) ≝
770λpars,p.
771  let sem_globals ≝ make_global pars p in
772  let ge ≝ genv2 sem_globals in
773  let m ≝ alloc_mem … p in
774  let 〈m,spb〉 ≝ alloc … m 0 external_ram_size XData in
775  let 〈m,ispb〉 ≝ alloc … m 0 internal_ram_size XData in
776  let dummy_pc ≝ mk_pointer Code (mk_block Code (-1)) ? (mk_offset 0) in
777  let spp ≝ mk_pointer XData spb ? (mk_offset external_ram_size) in
778  let ispp ≝ mk_pointer XData ispb ? (mk_offset 47) in
779  let main ≝ prog_main … p in
780  let st0 ≝ mk_state pars (empty_framesT …) spp ispp BVfalse (empty_regsT … spp) m in
781  (* use exit sem_globals as ra and call_dest_for_main as dest *)
782  let st0' ≝ set_frms ? (save_frame … (exit sem_globals) (call_dest_for_main … pars) st0) st0 in
783  let st_pc0 ≝ mk_state_pc ? st0' dummy_pc in
784  ! main_block ← opt_to_res … [MSG MissingSymbol; CTX ? main] (find_symbol … ge main) ;
785  ! main_fd ← opt_to_res ? [MSG BadPointer] (find_funct_ptr … ge main_block) ;
786  match main_fd with
787  [ Internal fn ⇒
788    do_call ?? ge st_pc0 (block_id main_block) fn (call_args_for_main … pars)
789  | External _ ⇒ Error … [MSG ExternalMain] (* External main not supported: why? *)
790  ]. [5: cases ispb * |6: cases spb * ] (* without try it fails! *) try //
791qed.
792
793definition joint_fullexec :
794 ∀pars:sem_params.fullexec io_out io_in ≝
795 λpars.mk_fullexec ??? joint_exec (make_global pars) (make_initial_state pars).
796*)
Note: See TracBrowser for help on using the repository browser.