source: src/joint/semantics.ma @ 2457

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

rewritten function handling in joint
swapped call_rel with ret_rel in the definition of status_rel, and parameterised status_simulation on status_rel
renamed SemanticUtils?

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