source: src/joint/semantics.ma @ 2286

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

Big update!

  • merge of all _paolo variants
  • reorganised some depends (in particular, Register and thus back-end laguages no longer have fake ASM dependency)
  • split I8051.ma spawning new BackEndOps?.ma

compiler.ma broken at the moment, but not by these changes as far as I can tell

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