source: src/joint/semantics.ma @ 2491

Last change on this file since 2491 was 2491, checked in by tranquil, 7 years ago

fixed wrt change of list member definition

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