source: src/joint/semantics.ma @ 2462

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

separated in back end values program counters from code pointers (intended to hold function pointers only): same signature, but separation needed the proof of some passes

File size: 30.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
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 : cpointer
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  cpointer →
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 (pblock 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 (cpointer × (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: cpointer → 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 → cpointer → 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 (cpointer × (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 → option offset (* can overflow *)
381  ; point_of_offset : offset → code_point pp
382  ; point_of_offset_of_point :
383    ∀pt.opt_All ? (eq ? pt) (option_map ?? point_of_offset (offset_of_point pt))
384  ; offset_of_point_of_offset :
385    ∀o.offset_of_point (point_of_offset o) = Some ? 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
401axiom CodePointerOverflow : String.
402
403definition pointer_of_point : ∀p.more_sem_params p →
404  cpointer→ code_point p → res cpointer ≝
405  λp,msp,ptr,pt.
406  ! o ← opt_to_res ? [MSG CodePointerOverflow] (offset_of_point ? msp pt) ;
407  return «mk_pointer (pblock ptr) o, ?».
408elim ptr #ptr' #EQ <EQ % qed.
409
410definition point_of_pointer :
411  ∀p.more_sem_params p → cpointer → code_point p ≝
412  λp,msp,ptr.point_of_offset p msp (poff ptr).
413
414lemma point_of_pointer_of_point :
415  ∀p,msp.∀ptr1,ptr2 : cpointer.∀pt.
416  pointer_of_point p msp ptr1 pt = return ptr2 →
417  point_of_pointer p msp ptr2 = pt.
418#p #msp #ptr1 #ptr2 #pt normalize
419lapply (point_of_offset_of_point p msp pt)
420cases (offset_of_point ???) normalize
421[ * #ABS destruct(ABS)
422| #o #EQ1 #EQ2 destruct %
423]
424qed.
425
426lemma pointer_of_point_block :
427  ∀p,msp,ptr1,ptr2,pt.
428  pointer_of_point p msp ptr1 pt = return ptr2 →
429  pblock ptr2 = pblock ptr1.
430#p #msp #ptr1 #ptr2 #pt normalize
431cases (offset_of_point ???) normalize
432[ #ABS destruct(ABS)
433| #o #EQ destruct(EQ) %
434]
435qed.
436
437lemma pointer_of_point_uses_block :
438  ∀p,msp.∀ptr1,ptr2 : cpointer.∀pt.pblock ptr1 = pblock ptr2 → pointer_of_point p msp ptr1 pt = pointer_of_point p msp ptr2 pt.
439#p #msp ** #b1 #o1 #EQ1
440        ** #b2 #o2 #EQ2
441#pt #EQ3 destruct normalize //
442qed.
443
444lemma pointer_of_point_of_pointer :
445  ∀p,msp.∀ptr1,ptr2 : cpointer.
446    pblock ptr1 = pblock ptr2 →
447    pointer_of_point p msp ptr1 (point_of_pointer p msp ptr2) = return ptr2.
448#p #msp ** #b1 #o1 #EQ1
449        ** #b2 #o2 #EQ2
450#EQ3 destruct
451normalize >offset_of_point_of_offset normalize %
452qed.
453
454definition fetch_statement: ∀p : params.∀ msp : more_sem_params p.∀globals.
455  ∀ge:genv p globals. cpointer →
456  res ((Σi.is_internal_function … ge i) × (joint_statement p globals)) ≝
457  λp,msp,globals,ge,ptr.
458  let bl ≝ pblock ptr in
459  ! f ← opt_to_res … [MSG BadFunction; MSG BadPointer]
460    (int_funct_of_block … ge bl) ;
461  let fn ≝ if_of_function … f in
462  let pt ≝ point_of_pointer ? msp ptr in
463  ! stmt ← opt_to_res … (msg ProgramCounterOutOfCode) (stmt_at … (joint_if_code … fn) pt);
464  return 〈f, stmt〉.
465
466definition pointer_of_label : ∀p : params.∀ msp : more_sem_params p.∀globals.
467  genv p globals → cpointer → label → res cpointer ≝
468  λp,msp,globals,ge,ptr,lbl.
469  ! f ← fetch_function … ge ptr ;
470  let fn ≝ if_of_function …  ge f in
471  ! pt ← opt_to_res … [MSG LabelNotFound ; CTX ? lbl]
472            (point_of_label … (joint_if_code … fn) lbl) ;
473  pointer_of_point p msp ptr pt.
474
475definition succ_pc : ∀p : params.∀ msp : more_sem_params p.
476  cpointer → succ p → res cpointer ≝
477  λp,msp,ptr,nxt.
478  let curr ≝ point_of_pointer p msp ptr in
479  pointer_of_point p msp ptr (point_of_succ p curr nxt).
480
481record sem_params : Type[1] ≝
482  { spp :> params
483  ; more_sem_pars :> more_sem_params spp
484  }.
485
486(* definition msu_pars_of_s_pars :
487∀p : sem_params.more_sem_unserialized_params (spp p) (λglobals.joint_internal_function globals (spp p))
488≝ λp : sem_params.
489  msu_pars … (more_sem_pars p).
490coercion s_pars_to_msu_pars nocomposites :
491∀p : sem_params.more_sem_unserialized_params (spp p) (λglobals.joint_internal_function globals (spp p)) ≝
492msu_pars_of_s_pars
493on p : sem_params to more_sem_unserialized_params ??.
494
495definition ss_pars_of_s_pars :
496∀p : sem_params.sem_state_params
497≝ λp : sem_params.
498  st_pars … (msu_pars … (more_sem_pars p)).
499coercion s_pars_to_ss_pars nocomposites :
500∀p : sem_params.sem_state_params ≝
501ss_pars_of_s_pars
502on _p : sem_params to sem_state_params.
503
504definition ms_pars_of_s_pars :
505∀p : sem_params.more_sem_params (spp p)
506≝ more_sem_pars.
507coercion s_pars_to_ms_pars nocomposites :
508∀p : sem_params.more_sem_params (spp p) ≝
509ms_pars_of_s_pars
510on p : sem_params to more_sem_params ?.*)
511
512(* definition address_of_label: ∀globals. ∀p:sem_params.
513  genv globals p → pointer → label → res address ≝
514 λglobals,p,ge,ptr,l.
515  do newptr ← pointer_of_label … p ? ge … ptr l ;
516  OK … (address_of_code_pointer newptr). *)
517
518definition goto: ∀globals.∀p : sem_params.
519  genv p globals → label → state p → cpointer → res (state_pc p) ≝
520 λglobals,p,ge,l,st,b.
521  ! newpc ← pointer_of_label ? p … ge b l ;
522  return mk_state_pc ? st newpc.
523
524(*
525definition empty_state: ∀p. more_sem_params p → state p ≝
526 mk_state … (empty_framesT …)
527*)
528
529definition next : ∀p : sem_params.succ p → state p → cpointer → res (state_pc p) ≝
530 λp,l,st,pc.
531 ! newpc ← succ_pc ? p … pc l ;
532 return mk_state_pc … st newpc.
533
534
535definition function_of_call ≝ λp:sem_params.λglobals.
536  λge: genv p globals.λst : state p.λf.
537  match f with
538  [ inl id ⇒
539    opt_to_res … [MSG BadFunction; MSG MissingSymbol; CTX ? id] (funct_of_ident … ge id)
540  | inr addr ⇒
541    ! addr_l ← dpl_arg_retrieve … st (\fst addr) ;
542    ! addr_h ← dph_arg_retrieve … st (\snd addr) ;
543    opt_to_res … [MSG BadFunction; MSG BadPointer] (funct_of_bevals … ge addr_l addr_h)
544  ].
545
546(* Paolo: why external calls do not need args?? *)
547definition eval_external_call ≝
548λp,F.λp' : sem_unserialized_params p F.λfn,args,dest,st.
549      ! params ← fetch_external_args … p' fn st args : IO ???;
550      ! evargs ← check_eventval_list params (sig_args (ef_sig fn)) : IO ???;
551      ! evres ← do_io (ef_id fn) evargs (proj_sig_res (ef_sig fn));
552      (* CSC: XXX bug here; I think I should split it into Byte-long
553         components; instead I am making a singleton out of it. To be
554         fixed once we fully implement external functions. *)
555      let vs ≝ [mk_val ? evres] in
556      set_result … p' vs dest st.
557
558lemma block_of_funct_ident_is_code : ∀F,globals,ge,i.
559  block_region (block_of_funct_ident F globals ge i) = Code.
560#F #globals #ge * #i * #fd
561whd in ⊢ (?→??(?%)?);
562cases (find_symbol ???)
563[ #ABS normalize in ABS; destruct(ABS) ]
564#bl normalize nodelta >m_return_bind
565whd in ⊢ (??%?→?); cases (block_region bl)
566[ #ABS normalize in ABS; destruct(ABS) ]
567#_ %
568qed.
569
570definition eval_internal_call_pc ≝
571λp : sem_params.λglobals : list ident.λge : genv p globals.λi.
572let fn ≝ if_of_function … ge i in
573let l' ≝ joint_if_entry ?? fn in
574let pointer_in_fn ≝ mk_pointer (block_of_funct_ident … ge (pi1 … i)) (mk_offset (bv_zero …)) in
575pointer_of_point ? p … pointer_in_fn l'.
576[ @block_of_funct_ident_is_code
577| cases i /2 by internal_function_is_function/
578]
579qed.
580
581definition eval_internal_call_no_pc ≝
582λp : sem_params.λglobals : list ident.λge : genv p globals.λi,args,st.
583let fn ≝ if_of_function … ge i in
584let stack_size ≝ stack_sizes … ge i in
585! st' ← setup_call … stack_size (joint_if_params … fn) args st ;
586let regs ≝ foldr ?? (allocate_local … p) (regs … st) (joint_if_locals … fn) in
587return set_regs p regs st.
588
589definition eval_seq_no_pc :
590 ∀p:sem_params.∀globals.∀ge:genv p globals. (Σi.is_internal_function … ge i) →
591  state p → cpointer → joint_seq p globals →
592  IO io_out io_in (state p) ≝
593 λp,globals,ge,curr_fn,st,next,seq.
594 match seq return λx.IO ??? with
595  [ extension_seq c ⇒
596    eval_ext_seq … ge c curr_fn st
597  | LOAD dst addrl addrh ⇒
598    ! vaddrh ← dph_arg_retrieve … st addrh ;
599    ! vaddrl ← dpl_arg_retrieve … st addrl;
600    ! vaddr ← pointer_of_address 〈vaddrl,vaddrh〉;
601    ! v ← opt_to_res … (msg FailedLoad) (beloadv (m … st) vaddr);
602    acca_store p … dst v st
603 | STORE addrl addrh src ⇒
604    ! vaddrh ← dph_arg_retrieve … st addrh;
605    ! vaddrl ← dpl_arg_retrieve … st addrl;
606    ! vaddr ← pointer_of_address 〈vaddrl,vaddrh〉;
607    ! v ← acca_arg_retrieve … st src;
608    ! m' ← opt_to_res … (msg FailedStore) (bestorev (m … st) vaddr v);
609    return set_m … m' st
610  | ADDRESS id prf ldest hdest ⇒
611    let addr_block ≝ opt_safe ? (find_symbol … ge id) ? in
612    let 〈laddr,haddr〉 ≝ beval_pair_of_pointer (mk_pointer addr_block zero_offset) in
613    ! st' ← dpl_store … ldest laddr st;
614    dph_store … hdest haddr st'
615  | OP1 op dacc_a sacc_a ⇒
616    ! v ← acca_retrieve … st sacc_a;
617    ! v' ← be_op1 op v ;
618    acca_store … dacc_a v' st
619  | OP2 op dacc_a sacc_a src ⇒
620    ! v1 ← acca_arg_retrieve … st sacc_a;
621    ! v2 ← snd_arg_retrieve … st src;
622    ! 〈v',carry〉 ← be_op2 (carry … st) op v1 v2 ;
623    ! st' ← acca_store … dacc_a v' st;
624    return set_carry … carry st'
625  | CLEAR_CARRY ⇒
626    return set_carry … (BBbit false) st
627  | SET_CARRY ⇒
628    return set_carry … (BBbit true) st
629  | OPACCS op dacc_a_reg dacc_b_reg sacc_a_reg sacc_b_reg ⇒
630    ! v1 ← acca_arg_retrieve … st sacc_a_reg;
631    ! v2 ← accb_arg_retrieve … st sacc_b_reg;
632    ! 〈v1',v2'〉 ← be_opaccs op v1 v2 ;
633    ! st' ← acca_store … dacc_a_reg v1' st;
634    accb_store … dacc_b_reg v2' st'
635  | POP dst ⇒
636    ! 〈v, st'〉 ← pop p st;
637    acca_store … p dst v st'
638  | PUSH src ⇒
639    ! v ← acca_arg_retrieve … st src;
640    push … st v
641  | MOVE dst_src ⇒
642    pair_reg_move … st dst_src
643  | CALL f args dest ⇒
644    ! fn ← function_of_call … ge st f : IO ???;
645    match description_of_function … fn return λx.description_of_function … fn = x → ? with
646    [ Internal fd ⇒ λprf.
647      ! st' ← save_frame … next dest st ;
648      eval_internal_call_no_pc … ge «fn, ?» args st'  (* only pc changes *)
649    | External fd ⇒ λ_.eval_external_call … fd args dest st
650    ] (refl …)
651  | _ ⇒ return st
652  ].
653[ @find_symbol_exists
654  lapply prf
655  elim globals [*]
656  #hd #tl #IH * [@eq_identifier_elim #H * >H %1 % ]
657  #G %2 @IH @G
658| @(description_of_internal_function … prf)
659]
660qed.
661
662definition eval_seq_pc :
663 ∀p:sem_params.∀globals.∀ge:genv p globals.
664  state p → cpointer → joint_seq p globals →
665  res cpointer ≝
666  λp,globals,ge,st,next,s.
667  match s with
668  [ CALL f args dest ⇒
669    ! fn ← function_of_call … ge st f;
670    match ? return λx.description_of_function … fn = x → ? with
671    [ Internal _ ⇒ λprf.eval_internal_call_pc … ge «fn, ?»
672    | External _ ⇒ λ_.return next
673    ] (refl …)
674  | _ ⇒ return next
675  ].
676@(description_of_internal_function … prf)
677qed.
678
679definition eval_statement :
680 ∀p:sem_params.∀globals.∀ge:genv p globals.
681 (Σi.is_internal_function … ge i) → state_pc p →
682  ∀s:joint_statement p globals.
683  IO io_out io_in (state_pc p) ≝
684  λp,g,ge,curr_fn,st,s.
685  match s with
686  [ sequential s next ⇒
687    ! next_ptr ← succ_pc ? p (pc … st) next : IO ??? ;
688    match s return λ_.IO ??? with
689    [ step_seq s ⇒
690      ! st' ← eval_seq_no_pc … ge curr_fn st next_ptr s ;
691      ! pc' ← eval_seq_pc … ge st next_ptr s ;
692      return mk_state_pc … st' pc'
693    | COND a l ⇒
694      ! v ← acca_retrieve … st a ;
695      ! b ← bool_of_beval … v ;
696      ! pc' ←
697        if b then
698          pointer_of_label ? p … ge (pc … st) l
699        else
700          succ_pc ? p (pc … st) next ;
701      return mk_state_pc … st pc'
702    ]
703  | final s ⇒
704    match s with
705    [ GOTO l ⇒
706      ! pc' ← pointer_of_label ? p ? ge (pc … st) l ;
707      return mk_state_pc … st pc'
708    | RETURN ⇒
709      ! st' ← pop_frame … curr_fn st ;
710      ! 〈pc', st''〉 ← fetch_ra … p st' ;
711      return mk_state_pc … st'' pc'
712    | TAILCALL _ f args ⇒
713      ! fn ← function_of_call … ge st f : IO ???;
714      match ? return λx.description_of_function … fn = x → ? with
715      [ Internal _ ⇒ λprf.
716        ! pc' ← eval_internal_call_pc … ge «fn, ?» ;
717        return mk_state_pc … st pc'
718      | External fd ⇒ λ_.
719        let curr_dest ≝ joint_if_result ?? (if_of_function … curr_fn) in
720        ! st' ← eval_external_call ??? fd args curr_dest st ;
721        ! st'' ← pop_frame … curr_fn st ;
722        ! 〈pc', st'''〉 ← fetch_ra … p st'' ;
723        return mk_state_pc … st''' pc'
724      ] (refl …)
725    ]
726  ].
727@(description_of_internal_function … prf)
728qed.
729
730definition eval_state : ∀globals: list ident.∀p:sem_params. genv p globals →
731  state_pc p → IO io_out io_in (state_pc p) ≝
732  λglobals,p,ge,st.
733  ! 〈fn,s〉 ← fetch_statement ? p … ge (pc … st) : IO ???;
734  eval_statement … ge fn st s.
735
736(* Paolo: what if in an intermediate language main finishes with an external
737  tailcall? Maybe it should rely on an FEnd flow command issued, but that's
738  not static... *)
739definition is_final: ∀globals:list ident. ∀p: sem_params.
740  genv p globals → cpointer → state_pc p → option int ≝
741 λglobals,p,ge,exit,st.res_to_opt ? (
742  do 〈f,s〉 ← fetch_statement ? p … ge (pc … st);
743  let fn ≝ if_of_function … f in
744  match s with
745  [ final s' ⇒
746    match s' with
747    [ RETURN ⇒
748      do 〈ra, st'〉 ← fetch_ra … st;
749      if eq_pointer ra exit then
750       do vals ← read_result … ge (joint_if_result … fn) st' ;
751       Word_of_list_beval vals
752      else
753       Error ? [ ]
754   | _ ⇒ Error ? [ ]
755   ]
756 | _ ⇒ Error ? [ ]
757 ]).
758
759(*
760record evaluation_parameters : Type[1] ≝
761 { globals: list ident
762 ; sparams:> sem_params
763 ; exit: cpointer
764 ; genv2: genv globals sparams
765 }.
766
767(* Paolo: with structured traces, eval need not emit labels. However, this
768  changes trans_system. For now, just putting a dummy thing for
769  the transition. *)
770definition joint_exec: trans_system io_out io_in ≝
771  mk_trans_system … evaluation_parameters (λG. state_pc G)
772   (λG.is_final (globals G) G (genv2 G) (exit G))
773   (λG,st.! 〈flag,st'〉 ← eval_state_flag (globals G) G (genv2 G) st ; return 〈E0, st'〉).
774
775definition make_global :
776 ∀pars: sem_params.
777  joint_program pars → evaluation_parameters
778
779 λpars.
780 (* Invariant: a -1 block is unused in common/Globalenvs *)
781 let b ≝ mk_block Code (-1) in
782 let ptr ≝ mk_pointer Code b ? (mk_offset 0) in
783  (λp. mk_evaluation_parameters
784    (prog_var_names … p)
785    (mk_sem_params … pars)
786    ptr
787    (globalenv_noinit … p)
788  ).
789% qed.
790
791axiom ExternalMain: String.
792
793definition make_initial_state :
794 ∀pars: sem_params.
795 ∀p: joint_program … pars. res (state_pc pars) ≝
796λpars,p.
797  let sem_globals ≝ make_global pars p in
798  let ge ≝ genv2 sem_globals in
799  let m ≝ alloc_mem … p in
800  let 〈m,spb〉 ≝ alloc … m 0 external_ram_size XData in
801  let 〈m,ispb〉 ≝ alloc … m 0 internal_ram_size XData in
802  let dummy_pc ≝ mk_pointer Code (mk_block Code (-1)) ? (mk_offset 0) in
803  let spp ≝ mk_pointer XData spb ? (mk_offset external_ram_size) in
804  let ispp ≝ mk_pointer XData ispb ? (mk_offset 47) in
805  let main ≝ prog_main … p in
806  let st0 ≝ mk_state pars (empty_framesT …) spp ispp BVfalse (empty_regsT … spp) m in
807  (* use exit sem_globals as ra and call_dest_for_main as dest *)
808  let st0' ≝ set_frms ? (save_frame … (exit sem_globals) (call_dest_for_main … pars) st0) st0 in
809  let st_pc0 ≝ mk_state_pc ? st0' dummy_pc in
810  ! main_block ← opt_to_res … [MSG MissingSymbol; CTX ? main] (find_symbol … ge main) ;
811  ! main_fd ← opt_to_res ? [MSG BadPointer] (find_funct_ptr … ge main_block) ;
812  match main_fd with
813  [ Internal fn ⇒
814    do_call ?? ge st_pc0 (block_id main_block) fn (call_args_for_main … pars)
815  | External _ ⇒ Error … [MSG ExternalMain] (* External main not supported: why? *)
816  ]. [5: cases ispb * |6: cases spb * ] (* without try it fails! *) try //
817qed.
818
819definition joint_fullexec :
820 ∀pars:sem_params.fullexec io_out io_in ≝
821 λpars.mk_fullexec ??? joint_exec (make_global pars) (make_initial_state pars).
822*)
Note: See TracBrowser for help on using the repository browser.