source: src/joint/semantics.ma @ 2481

Last change on this file since 2481 was 2481, checked in by piccolo, 7 years ago

corrected some inconsistencies
fixed some of lineariseProof

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 ∀F.
146 ∀ge : genv_t (fundef F).
147  program_counter →
148  res (Σi.is_internal_function … ge i) ≝
149 λpars,ge,p.
150 opt_to_res … [MSG BadFunction; MSG BadPointer]
151    (int_funct_of_block … ge (pc_block p)).
152
153record sem_unserialized_params
154  (uns_pars : unserialized_params)
155  (F : list ident → Type[0]) : Type[1] ≝
156  { st_pars :> sem_state_params
157
158  ; acca_store_ : acc_a_reg uns_pars → beval → regsT st_pars → res (regsT st_pars)
159  ; acca_retrieve_ : regsT st_pars → acc_a_reg uns_pars → res beval
160  ; acca_arg_retrieve_ : regsT st_pars → acc_a_arg uns_pars → res beval
161  ; accb_store_ : acc_b_reg uns_pars → beval → regsT st_pars → res (regsT st_pars)
162  ; accb_retrieve_ : regsT st_pars → acc_b_reg uns_pars → res beval
163  ; accb_arg_retrieve_ : regsT st_pars → acc_b_arg uns_pars → res beval
164  ; dpl_store_ : dpl_reg uns_pars → beval → regsT st_pars → res (regsT st_pars)
165  ; dpl_retrieve_ : regsT st_pars → dpl_reg uns_pars → res beval
166  ; dpl_arg_retrieve_ : regsT st_pars → dpl_arg uns_pars → res beval
167  ; dph_store_ : dph_reg uns_pars → beval → regsT st_pars → res (regsT st_pars)
168  ; dph_retrieve_ : regsT st_pars → dph_reg uns_pars → res beval
169  ; dph_arg_retrieve_ : regsT st_pars → dph_arg uns_pars → res beval
170  ; snd_arg_retrieve_ : regsT st_pars → snd_arg uns_pars → res beval
171  ; pair_reg_move_ : regsT st_pars → pair_move uns_pars → res (regsT st_pars)
172  ; fetch_ra: state st_pars → res (program_counter × (state st_pars))
173
174  ; allocate_local : localsT uns_pars → regsT st_pars → regsT st_pars
175  (* Paolo: save_frame separated from call_setup to factorize tailcall code *)
176  ; save_frame: program_counter → call_dest uns_pars → state st_pars → res (state st_pars)
177   (*CSC: setup_call returns a res only because we can call a function with the wrong number and
178     type of arguments. To be fixed using a dependent type *)
179  ; setup_call : nat → paramsT … uns_pars → call_args uns_pars →
180      state st_pars → res (state st_pars)
181  ; fetch_external_args: external_function → state st_pars → call_args … uns_pars →
182      res (list val)
183  ; set_result: list val → call_dest uns_pars → state st_pars → res (state st_pars)
184  ; call_args_for_main: call_args uns_pars
185  ; call_dest_for_main: call_dest uns_pars
186
187  (* from now on, parameters that use the type of functions *)
188  ; read_result: ∀globals.genv_gen F globals → call_dest uns_pars → state st_pars → res (list beval)
189  (* change of pc must be left to *_flow execution *)
190  ; eval_ext_seq: ∀globals.∀ge : genv_gen F globals.ext_seq uns_pars →
191    (Σi.is_internal_function … ge i) (* current *) → state st_pars → IO io_out io_in (state st_pars)
192  ; pop_frame: ∀globals.∀ge : genv_gen F globals.
193    (Σi.is_internal_function … ge i) (* current *) → state st_pars → res (state st_pars)
194  }.
195
196(*coercion msu_pars_to_ss_pars nocomposites :
197∀p,F.∀msup : more_sem_unserialized_params p F.sem_state_params
198 ≝ st_pars
199on _msup : more_sem_unserialized_params ?? to sem_state_params.*)
200
201
202definition helper_def_retrieve :
203  ∀X : ? → ? → ? → Type[0].
204  (∀up,F.∀p:sem_unserialized_params up F. regsT (st_pars up F p) → X up F p → res beval) →
205  ∀up,F.∀p : sem_unserialized_params up F.state (st_pars up F p) → X up F p → res beval ≝
206    λX,f,up,F,p,st.f ?? p (regs … st).
207
208definition helper_def_store :
209  ∀X : ? → ? → ? → Type[0].
210  (∀up,F.∀p : sem_unserialized_params up F.X up F p → beval → regsT (st_pars … p) → res (regsT (st_pars … p))) →
211  ∀up,F.∀p : sem_unserialized_params up F.X up F p → beval → state (st_pars … p) → res (state (st_pars … p)) ≝
212  λX,f,up,F,p,x,v,st.! r ← f ?? p x v (regs … st) ; return set_regs … r st.
213
214definition acca_retrieve ≝ helper_def_retrieve ? acca_retrieve_.
215definition acca_store ≝ helper_def_store ? acca_store_.
216definition acca_arg_retrieve ≝ helper_def_retrieve ? acca_arg_retrieve_.
217definition accb_store ≝ helper_def_store ? accb_store_.
218definition accb_retrieve ≝ helper_def_retrieve ? accb_retrieve_.
219definition accb_arg_retrieve ≝ helper_def_retrieve ? accb_arg_retrieve_.
220definition dpl_store ≝ helper_def_store ? dpl_store_.
221definition dpl_retrieve ≝ helper_def_retrieve ? dpl_retrieve_.
222definition dpl_arg_retrieve ≝ helper_def_retrieve ? dpl_arg_retrieve_.
223definition dph_store ≝ helper_def_store ? dph_store_.
224definition dph_retrieve ≝ helper_def_retrieve ? dph_retrieve_.
225definition dph_arg_retrieve ≝ helper_def_retrieve ? dph_arg_retrieve_.
226definition snd_arg_retrieve ≝ helper_def_retrieve ? snd_arg_retrieve_.
227definition pair_reg_move ≝
228  λup,F.λp : sem_unserialized_params up F.λst : state (st_pars … p).λpm : pair_move up.
229    ! r ← pair_reg_move_ ?? p (regs ? st) pm;
230    return set_regs ? r st.
231 
232axiom FailedStore: String.
233
234definition push: ∀p.state p → beval → res (state p) ≝
235 λp,st,v.
236 ! is ← is_push (istack … st) v ;
237 return set_istack … is st.
238
239definition pop: ∀p. state p → res (beval × (state p)) ≝
240 λp,st.
241 ! 〈bv, is〉 ← is_pop (istack … st) ;
242 return 〈bv, set_istack … is st〉.
243
244definition save_ra : ∀p. state p → program_counter → res (state p) ≝
245 λp,st,l.
246  let 〈addrl,addrh〉 ≝  beval_pair_of_pc l in
247  ! st' ← push … st addrl;
248  push … st' addrh.
249
250definition load_ra : ∀p.state p → res (program_counter × (state p)) ≝
251 λp,st.
252  ! 〈addrh, st'〉 ← pop … st;
253  ! 〈addrl, st''〉 ← pop … st';
254  ! pr ← pc_of_bevals [addrh; addrl];
255  return 〈pr, st''〉.
256
257(* parameters that are defined by serialization *)
258record more_sem_params (pp : params) : Type[1] ≝
259  { msu_pars :> sem_unserialized_params pp (joint_closed_internal_function pp)
260  ; offset_of_point : code_point pp → Pos
261  ; point_of_offset : Pos → code_point pp
262  ; point_of_offset_of_point :
263    ∀pt.point_of_offset (offset_of_point pt) = pt
264  ; offset_of_point_of_offset :
265    ∀o.offset_of_point (point_of_offset o) = o
266  }.
267
268(*
269coercion ms_pars_to_msu_pars nocomposites :
270∀p : params.∀msp : more_sem_params p.more_sem_unserialized_params p (λglobals.joint_internal_function globals p)
271 ≝ msu_pars
272on _msp : more_sem_params ? to more_sem_unserialized_params ??.
273
274definition ss_pars_of_ms_pars ≝
275  λp.λpp : more_sem_params p.
276  st_pars … (msu_pars … pp).
277coercion ms_pars_to_ss_pars nocomposites :
278∀p : params.∀msp : more_sem_params p.sem_state_params ≝
279ss_pars_of_ms_pars on _msp : more_sem_params ? to sem_state_params.*)
280
281definition pc_of_point : ∀p.more_sem_params p →
282  program_counter → code_point p → program_counter ≝
283  λp,msp,ptr,pt.
284  mk_program_counter (pc_block ptr) (offset_of_point ? msp pt).
285
286definition point_of_pc :
287  ∀p.more_sem_params p → program_counter → code_point p ≝
288  λp,msp,ptr.point_of_offset p msp (pc_offset ptr).
289
290lemma point_of_pointer_of_point :
291  ∀p,msp.∀ptr,pt.
292  point_of_pc ? msp (pc_of_point p msp ptr pt) = pt.
293#p #msp #ptr #pt normalize // qed.
294
295lemma pointer_of_point_block :
296  ∀p,msp,ptr,pt.
297  pc_block (pc_of_point p msp ptr pt) = pc_block ptr.
298#p #msp #ptr #pt % qed. (* can probably do without *)
299
300lemma pointer_of_point_uses_block :
301  ∀p,msp.∀ptr1,ptr2.∀pt.pc_block ptr1 = pc_block ptr2 →
302    pc_of_point p msp ptr1 pt = pc_of_point p msp ptr2 pt.
303#p #msp #ptr1 #ptr2 #pc #EQ normalize >EQ % qed.
304
305lemma pointer_of_point_of_pointer :
306  ∀p,msp.∀ptr1,ptr2.
307    pc_block ptr1 = pc_block ptr2 →
308    pc_of_point p msp ptr1 (point_of_pc p msp ptr2) = ptr2.
309#p #msp #ptr1 * #bl2 #o2 #EQ normalize >offset_of_point_of_offset >EQ % qed.
310
311definition fetch_statement: ∀p : params.∀ msp : more_sem_params p.∀globals.
312  ∀ge : genv_t (joint_function p globals). program_counter →
313  res ((Σi.is_internal_function … ge i) × (joint_statement p globals)) ≝
314  λp,msp,globals,ge,ptr.
315  ! f ← fetch_function … ge ptr ;
316  let fn ≝ if_of_function … f in
317  let pt ≝ point_of_pc ? msp ptr in
318  ! stmt ← opt_to_res … (msg ProgramCounterOutOfCode) (stmt_at … (joint_if_code … fn) pt);
319  return 〈f, stmt〉.
320
321definition pc_of_label : ∀p : params.∀ msp : more_sem_params p.∀globals.
322  genv_t (joint_function p globals) → program_counter → label → res program_counter ≝
323  λp,msp,globals,ge,ptr,lbl.
324  ! f ← fetch_function … ge ptr ;
325  let fn ≝ if_of_function …  ge f in
326  ! pt ← opt_to_res … [MSG LabelNotFound ; CTX ? lbl]
327            (point_of_label … (joint_if_code … fn) lbl) ;
328  return pc_of_point p msp ptr pt.
329
330definition succ_pc : ∀p : params.∀ msp : more_sem_params p.
331  program_counter → succ p → program_counter ≝
332  λp,msp,ptr,nxt.
333  let curr ≝ point_of_pc p msp ptr in
334  pc_of_point p msp ptr (point_of_succ p curr nxt).
335
336record sem_params : Type[1] ≝
337  { spp :> params
338  ; more_sem_pars :> more_sem_params spp
339  }.
340
341(* definition msu_pars_of_s_pars :
342∀p : sem_params.more_sem_unserialized_params (spp p) (λglobals.joint_internal_function globals (spp p))
343≝ λp : sem_params.
344  msu_pars … (more_sem_pars p).
345coercion s_pars_to_msu_pars nocomposites :
346∀p : sem_params.more_sem_unserialized_params (spp p) (λglobals.joint_internal_function globals (spp p)) ≝
347msu_pars_of_s_pars
348on p : sem_params to more_sem_unserialized_params ??.
349
350definition ss_pars_of_s_pars :
351∀p : sem_params.sem_state_params
352≝ λp : sem_params.
353  st_pars … (msu_pars … (more_sem_pars p)).
354coercion s_pars_to_ss_pars nocomposites :
355∀p : sem_params.sem_state_params ≝
356ss_pars_of_s_pars
357on _p : sem_params to sem_state_params.
358
359definition ms_pars_of_s_pars :
360∀p : sem_params.more_sem_params (spp p)
361≝ more_sem_pars.
362coercion s_pars_to_ms_pars nocomposites :
363∀p : sem_params.more_sem_params (spp p) ≝
364ms_pars_of_s_pars
365on p : sem_params to more_sem_params ?.*)
366
367(* definition address_of_label: ∀globals. ∀p:sem_params.
368  genv globals p → pointer → label → res address ≝
369 λglobals,p,ge,ptr,l.
370  do newptr ← pointer_of_label … p ? ge … ptr l ;
371  OK … (address_of_code_pointer newptr). *)
372
373definition goto: ∀p : sem_params.∀globals.
374  genv_t (joint_function p globals) → label → state p → program_counter → res (state_pc p) ≝
375 λp,globals,ge,l,st,b.
376  ! newpc ← pc_of_label ? p … ge b l ;
377  return mk_state_pc ? st newpc.
378
379(*
380definition empty_state: ∀p. more_sem_params p → state p ≝
381 mk_state … (empty_framesT …)
382*)
383
384definition next : ∀p : sem_params.succ p → state p → program_counter → state_pc p ≝
385 λp,l,st,pc.
386 let newpc ≝ succ_pc ? p … pc l in
387 mk_state_pc … st newpc.
388
389
390definition function_of_call ≝ λp:sem_params.λglobals.
391  λge: genv_t (joint_function p globals).λst : state p.λf.
392  match f with
393  [ inl id ⇒
394    opt_to_res … [MSG BadFunction; MSG MissingSymbol; CTX ? id] (funct_of_ident … ge id)
395  | inr addr ⇒
396    ! addr_l ← dpl_arg_retrieve … st (\fst addr) ;
397    ! addr_h ← dph_arg_retrieve … st (\snd addr) ;
398    opt_to_res … [MSG BadFunction; MSG BadPointer] (funct_of_bevals … ge addr_l addr_h)
399  ].
400
401(* Paolo: why external calls do not need args?? *)
402definition eval_external_call ≝
403λp,F.λp' : sem_unserialized_params p F.λfn,args,dest,st.
404      ! params ← fetch_external_args … p' fn st args : IO ???;
405      ! evargs ← check_eventval_list params (sig_args (ef_sig fn)) : IO ???;
406      ! evres ← do_io (ef_id fn) evargs (proj_sig_res (ef_sig fn));
407      (* CSC: XXX bug here; I think I should split it into Byte-long
408         components; instead I am making a singleton out of it. To be
409         fixed once we fully implement external functions. *)
410      let vs ≝ [mk_val ? evres] in
411      set_result … p' vs dest st.
412
413definition eval_internal_call_pc ≝
414λp : sem_params.λglobals : list ident.λge : genv_t (joint_function p globals).λi.
415let fn ≝ if_of_function … ge i in
416let l' ≝ joint_if_entry ?? fn in
417mk_program_counter (block_of_funct … ge (pi1 … i)) (offset_of_point ? p … l').
418[ @block_of_funct_ident_is_code
419| cases i /2 by internal_function_is_function/
420]
421qed.
422
423definition eval_internal_call_no_pc ≝
424λp : sem_params.λglobals : list ident.λge : genv p globals.λi,args,st.
425let fn ≝ if_of_function … ge i in
426let stack_size ≝ stack_sizes … ge i in
427! st' ← setup_call … stack_size (joint_if_params … fn) args st ;
428let regs ≝ foldr ?? (allocate_local … p) (regs … st) (joint_if_locals … fn) in
429return set_regs p regs st.
430
431definition eval_seq_no_pc :
432 ∀p:sem_params.∀globals.∀ge:genv p globals. (Σi.is_internal_function … ge i) →
433  state p → program_counter → joint_seq p globals →
434  IO io_out io_in (state p) ≝
435 λp,globals,ge,curr_fn,st,next,seq.
436 match seq return λx.IO ??? with
437  [ extension_seq c ⇒
438    eval_ext_seq … ge c curr_fn st
439  | LOAD dst addrl addrh ⇒
440    ! vaddrh ← dph_arg_retrieve … st addrh ;
441    ! vaddrl ← dpl_arg_retrieve … st addrl;
442    ! vaddr ← pointer_of_address 〈vaddrl,vaddrh〉;
443    ! v ← opt_to_res … (msg FailedLoad) (beloadv (m … st) vaddr);
444    acca_store p … dst v st
445 | STORE addrl addrh src ⇒
446    ! vaddrh ← dph_arg_retrieve … st addrh;
447    ! vaddrl ← dpl_arg_retrieve … st addrl;
448    ! vaddr ← pointer_of_address 〈vaddrl,vaddrh〉;
449    ! v ← acca_arg_retrieve … st src;
450    ! m' ← opt_to_res … (msg FailedStore) (bestorev (m … st) vaddr v);
451    return set_m … m' st
452  | ADDRESS id prf ldest hdest ⇒
453    let addr_block ≝ opt_safe ? (find_symbol … ge id) ? in
454    let 〈laddr,haddr〉 ≝ beval_pair_of_pointer (mk_pointer addr_block zero_offset) in
455    ! st' ← dpl_store … ldest laddr st;
456    dph_store … hdest haddr st'
457  | OP1 op dacc_a sacc_a ⇒
458    ! v ← acca_retrieve … st sacc_a;
459    ! v' ← be_op1 op v ;
460    acca_store … dacc_a v' st
461  | OP2 op dacc_a sacc_a src ⇒
462    ! v1 ← acca_arg_retrieve … st sacc_a;
463    ! v2 ← snd_arg_retrieve … st src;
464    ! 〈v',carry〉 ← be_op2 (carry … st) op v1 v2 ;
465    ! st' ← acca_store … dacc_a v' st;
466    return set_carry … carry st'
467  | CLEAR_CARRY ⇒
468    return set_carry … (BBbit false) st
469  | SET_CARRY ⇒
470    return set_carry … (BBbit true) st
471  | OPACCS op dacc_a_reg dacc_b_reg sacc_a_reg sacc_b_reg ⇒
472    ! v1 ← acca_arg_retrieve … st sacc_a_reg;
473    ! v2 ← accb_arg_retrieve … st sacc_b_reg;
474    ! 〈v1',v2'〉 ← be_opaccs op v1 v2 ;
475    ! st' ← acca_store … dacc_a_reg v1' st;
476    accb_store … dacc_b_reg v2' st'
477  | POP dst ⇒
478    ! 〈v, st'〉 ← pop p st;
479    acca_store … p dst v st'
480  | PUSH src ⇒
481    ! v ← acca_arg_retrieve … st src;
482    push … st v
483  | MOVE dst_src ⇒
484    pair_reg_move … st dst_src
485  | CALL f args dest ⇒
486    ! fn ← function_of_call … ge st f : IO ???;
487    match description_of_function … fn return λx.description_of_function … fn = x → ? with
488    [ Internal fd ⇒ λprf.
489      ! st' ← save_frame … next dest st ;
490      eval_internal_call_no_pc … ge «fn, ?» args st'  (* only pc changes *)
491    | External fd ⇒ λ_.eval_external_call … fd args dest st
492    ] (refl …)
493  | _ ⇒ return st
494  ].
495[ @hide_prf
496  @find_symbol_in_globals
497  lapply prf
498  elim globals [*]
499  #hd #tl #IH * [@eq_identifier_elim #H * >H %1 % ]
500  #G %2 @IH @G
501| @(description_of_internal_function … prf)
502]
503qed.
504
505definition eval_seq_pc :
506 ∀p:sem_params.∀globals.∀ge:genv p globals.
507  state p → program_counter → joint_seq p globals →
508  res program_counter ≝
509  λp,globals,ge,st,next,s.
510  match s with
511  [ CALL f args dest ⇒
512    ! fn ← function_of_call … ge st f;
513    match ? return λx.description_of_function … fn = x → ? with
514    [ Internal _ ⇒ λprf.return eval_internal_call_pc … ge «fn, ?»
515    | External _ ⇒ λ_.return next
516    ] (refl …)
517  | _ ⇒ return next
518  ].
519@(description_of_internal_function … prf)
520qed.
521
522definition eval_statement :
523 ∀p:sem_params.∀globals.∀ge:genv p globals.
524 (Σi.is_internal_function … ge i) → state_pc p →
525  ∀s:joint_statement p globals.
526  IO io_out io_in (state_pc p) ≝
527  λp,g,ge,curr_fn,st,s.
528  match s with
529  [ sequential s next ⇒
530    let next_ptr ≝ succ_pc ? p (pc … st) next in
531    match s return λ_.IO ??? with
532    [ step_seq s ⇒
533      ! st' ← eval_seq_no_pc … ge curr_fn st next_ptr s ;
534      ! pc' ← eval_seq_pc … ge st next_ptr s ;
535      return mk_state_pc … st' pc'
536    | COND a l ⇒
537      ! v ← acca_retrieve … st a ;
538      ! b ← bool_of_beval … v ;
539      ! pc' ←
540        if b then
541          pc_of_label ? p … ge (pc … st) l
542        else
543          return succ_pc ? p (pc … st) next ;
544      return mk_state_pc … st pc'
545    ]
546  | final s ⇒
547    match s with
548    [ GOTO l ⇒
549      ! pc' ← pc_of_label ? p ? ge (pc … st) l ;
550      return mk_state_pc … st pc'
551    | RETURN ⇒
552      ! st' ← pop_frame … curr_fn st ;
553      ! 〈pc', st''〉 ← fetch_ra … p st' ;
554      return mk_state_pc … st'' pc'
555    | TAILCALL _ f args ⇒
556      ! fn ← function_of_call … ge st f : IO ???;
557      match ? return λx.description_of_function … fn = x → ? with
558      [ Internal _ ⇒ λprf.
559        let pc' ≝ eval_internal_call_pc … ge «fn, ?» in
560        return mk_state_pc … st pc'
561      | External fd ⇒ λ_.
562        let curr_dest ≝ joint_if_result ?? (if_of_function … curr_fn) in
563        ! st' ← eval_external_call ??? fd args curr_dest st ;
564        ! st'' ← pop_frame … curr_fn st ;
565        ! 〈pc', st'''〉 ← fetch_ra … p st'' ;
566        return mk_state_pc … st''' pc'
567      ] (refl …)
568    ]
569  ].
570@(description_of_internal_function … prf)
571qed.
572
573definition eval_state : ∀p:sem_params. ∀globals: list ident.
574  genv p globals →
575  state_pc p → IO io_out io_in (state_pc p) ≝
576  λp,globals,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: ∀p: sem_params.∀globals.
584  genv p globals → program_counter → state_pc p → option int ≝
585 λp,globals,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.