source: src/joint/semantics.ma @ 2437

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

generalised calls to calls with pointers

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