source: src/joint/semantics.ma @ 2443

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

changed joint's stack pointer and internal stack

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