source: src/joint/semantics.ma @ 2422

Last change on this file since 2422 was 2422, checked in by tranquil, 8 years ago

adapted joint to cl_call f

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