source: src/joint/semantics.ma @ 2473

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

put some generic stuff we need in the back end in extraGlobalenvs (with some axioms that are
in the commented section of Globalenvs)
linearise now has a full spec

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