source: src/joint/semantics_paolo.ma @ 2233

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