source: src/joint/semantics_paolo.ma @ 2214

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