source: src/joint/semantics_paolo.ma @ 2217

Last change on this file since 2217 was 2217, checked in by tranquil, 7 years ago
  • collapsed step_params, unserialized_params, funct_params and local_params into one (unserialized_params)
  • completed update of RTL, LTL and LIN semantics
File size: 27.4 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 : unserialized_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 : unserialized_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 → call_dest uns_pars → 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)) → call_dest uns_pars → 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      call_dest uns_pars → 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)) → call_dest uns_pars → 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 dest 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 →
329  res ((joint_internal_function p globals) × (joint_statement p globals)) ≝
330  λp,msp,globals,ge,ptr.
331  let pt ≝ point_of_pointer ? msp ptr in
332  ! fn ← fetch_function … ge ptr ;
333  ! stmt ← opt_to_res … (msg ProgramCounterOutOfCode) (stmt_at … (joint_if_code … fn) pt);
334  return 〈fn, stmt〉.
335 
336definition pointer_of_label : ∀p : params.∀ msp : more_sem_params p.∀globals.
337  genv p globals → cpointer → label → res cpointer ≝
338  λp,msp,globals,ge,ptr,lbl.
339  ! fn ← fetch_function … ge ptr ;
340  ! pt ← opt_to_res … [MSG LabelNotFound ; CTX ? lbl]
341            (point_of_label … (joint_if_code … fn) lbl) ;
342  pointer_of_point p msp ptr pt.
343
344definition succ_pc : ∀p : params.∀ msp : more_sem_params p.
345  cpointer → succ p → res cpointer ≝
346  λp,msp,ptr,nxt.
347  let curr ≝ point_of_pointer p msp ptr in
348  pointer_of_point p msp ptr (point_of_succ p curr nxt).
349
350record sem_params : Type[1] ≝
351  { spp :> params
352  ; more_sem_pars :> more_sem_params spp
353  }.
354
355(* definition msu_pars_of_s_pars :
356∀p : sem_params.more_sem_unserialized_params (spp p) (λglobals.joint_internal_function globals (spp p))
357≝ λp : sem_params.
358  msu_pars … (more_sem_pars p).
359coercion s_pars_to_msu_pars nocomposites :
360∀p : sem_params.more_sem_unserialized_params (spp p) (λglobals.joint_internal_function globals (spp p)) ≝
361msu_pars_of_s_pars
362on p : sem_params to more_sem_unserialized_params ??.
363
364definition ss_pars_of_s_pars :
365∀p : sem_params.sem_state_params
366≝ λp : sem_params.
367  st_pars … (msu_pars … (more_sem_pars p)).
368coercion s_pars_to_ss_pars nocomposites :
369∀p : sem_params.sem_state_params ≝
370ss_pars_of_s_pars
371on _p : sem_params to sem_state_params.
372
373definition ms_pars_of_s_pars :
374∀p : sem_params.more_sem_params (spp p)
375≝ more_sem_pars.
376coercion s_pars_to_ms_pars nocomposites :
377∀p : sem_params.more_sem_params (spp p) ≝
378ms_pars_of_s_pars
379on p : sem_params to more_sem_params ?.*)
380
381(* definition address_of_label: ∀globals. ∀p:sem_params.
382  genv globals p → pointer → label → res address ≝
383 λglobals,p,ge,ptr,l.
384  do newptr ← pointer_of_label … p ? ge … ptr l ;
385  OK … (address_of_code_pointer newptr). *)
386
387definition goto: ∀globals.∀p : sem_params.
388  genv p globals → label → state p → cpointer → res (state_pc p) ≝
389 λglobals,p,ge,l,st,b.
390  ! newpc ← pointer_of_label ? p … ge b l ;
391  return mk_state_pc ? st newpc.
392
393(*
394definition empty_state: ∀p. more_sem_params p → state p ≝
395 mk_state … (empty_framesT …)
396*)
397
398definition next : ∀p : sem_params.succ p → state p → cpointer → res (state_pc p) ≝
399 λp,l,st,pc.
400 ! newpc ← succ_pc ? p … pc l ;
401 return mk_state_pc … st newpc.
402
403axiom MissingSymbol : String.
404axiom FailedLoad : String.
405axiom BadFunction : String.
406axiom SuccessorNotProvided : String.
407
408definition eval_seq_no_pc :
409 ∀globals.∀p:sem_params. genv p globals → state p →
410  ∀s:joint_seq p globals.
411  IO io_out io_in (state p) ≝
412 λglobals,p,ge,st,seq.
413  match seq return λx.IO ??? with
414  [ extension_seq c ⇒
415    eval_ext_seq … ge c st
416  | LOAD dst addrl addrh ⇒
417    ! vaddrh ← dph_arg_retrieve … st addrh ;
418    ! vaddrl ← dpl_arg_retrieve … st addrl;
419    ! vaddr ← pointer_of_address 〈vaddrl,vaddrh〉;
420    ! v ← opt_to_res … (msg FailedLoad) (beloadv (m … st) vaddr);
421    acca_store p … dst v st
422  | STORE addrl addrh src ⇒
423    ! vaddrh ← dph_arg_retrieve … st addrh;
424    ! vaddrl ← dpl_arg_retrieve … st addrl;
425    ! vaddr ← pointer_of_address 〈vaddrl,vaddrh〉;
426    ! v ← acca_arg_retrieve … st src;
427    ! m' ← opt_to_res … (msg FailedStore) (bestorev (m … st) vaddr v);
428    return set_m … m' st
429  | ADDRESS ident prf ldest hdest ⇒
430    let addr ≝ opt_safe ? (find_symbol … ge ident) ? in
431    ! 〈laddr,haddr〉 ← address_of_pointer (mk_pointer addr zero_offset) ;
432    ! st' ← dpl_store … ldest laddr st;
433    dph_store … hdest haddr st'
434  | OP1 op dacc_a sacc_a ⇒
435    ! v ← acca_retrieve … st sacc_a;
436    ! v ← Byte_of_val v;
437    let v' ≝ BVByte (op1 eval op v) in
438    acca_store … dacc_a v' st
439  | OP2 op dacc_a sacc_a src ⇒
440    ! v1 ← acca_arg_retrieve … st sacc_a;
441    ! v1 ← Byte_of_val v1;
442    ! v2 ← snd_arg_retrieve … st src;
443    ! v2 ← Byte_of_val v2;
444    ! carry ← bool_of_beval (carry … st);
445      let 〈v',carry〉 ≝ op2 eval carry op v1 v2 in
446      let v' ≝ BVByte v' in
447      let carry ≝ beval_of_bool carry in
448    ! st' ← acca_store … dacc_a v' st;
449    return set_carry … carry st'
450  | CLEAR_CARRY ⇒
451    return set_carry … BVfalse st
452  | SET_CARRY ⇒
453    return set_carry … BVtrue st
454  | OPACCS op dacc_a_reg dacc_b_reg sacc_a_reg sacc_b_reg ⇒
455    ! v1 ← acca_arg_retrieve … st sacc_a_reg;
456    ! v1 ← Byte_of_val v1;
457    ! v2 ← accb_arg_retrieve … st sacc_b_reg;
458    ! v2 ← Byte_of_val v2;
459    let 〈v1',v2'〉 ≝ opaccs eval op v1 v2 in
460    let v1' ≝ BVByte v1' in
461    let v2' ≝ BVByte v2' in
462    ! st' ← acca_store … dacc_a_reg v1' st;
463    accb_store … dacc_b_reg v2' st'
464  | POP dst ⇒
465    ! 〈st',v〉 ← pop p st;
466    acca_store … p dst v st'
467  | PUSH src ⇒
468    ! v ← acca_arg_retrieve … st src;
469    push … st v
470  | MOVE dst_src ⇒
471    pair_reg_move … st dst_src
472  | CALL_ID id args dest ⇒
473    ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol … ge id) : IO ???;
474    ! 〈flow, st'〉 ← eval_call_block … ge st b args dest ;
475    return st'
476  | extension_call s ⇒
477    !〈flow, st'〉 ← eval_ext_call … ge s st ;
478    return st'
479  | _ ⇒ return st
480  ].
481  (* TODO: to prove *)
482  elim daemon
483  qed.
484
485definition eval_seq_pc :
486 ∀globals.∀p:sem_params. genv p globals → state p →
487  ∀s:joint_seq p globals.
488  IO io_out io_in (step_flow p ? (step_flows … s)) ≝
489  λg,p,ge,st,s.match s return λx : joint_seq ??.IO ?? (step_flow ?? (step_flows … x)) with
490  [ CALL_ID id args dest ⇒
491    ! b ← opt_to_res \ldots  [MSG MissingSymbol; CTX ? id] (find_symbol … ge id) : IO ???;
492    ! 〈flow, st'〉 ← eval_call_block … ge st b args dest ;
493    return flow
494  | extension_call s ⇒
495    !〈flow, st'〉 ← eval_ext_call … ge s st ;
496    return flow
497  | _ ⇒ return Proceed ???
498  ].
499
500definition eval_step :
501 ∀globals.∀p:sem_params. genv p globals → state p →
502  ∀s:joint_step p globals.
503  IO io_out io_in ((step_flow p ? (step_flows … s))×(state p)) ≝
504  λglobals,p,ge,st,s.
505  match s return λx.IO ?? ((step_flow ?? (step_flows … x))×?) with
506  [ step_seq s ⇒
507    ! flow ← eval_seq_pc ?? ge st s ;
508    ! st' ← eval_seq_no_pc ?? ge st s ;
509    return 〈flow,st'〉
510  | COND src ltrue ⇒
511    ! v ← acca_retrieve … st src;
512    ! b ← bool_of_beval v;
513    if b then
514      return 〈Redirect ??? ltrue, st〉
515    else
516      return 〈Proceed ???, st〉
517  ].
518  %1 % qed.
519
520definition eval_fin_step_no_pc : ∀globals: list ident.∀p:sem_params. genv p globals →
521  (* result registers of current function *) call_dest p → state p → ∀s : joint_fin_step p.
522  IO io_out io_in (state p) ≝
523 λglobals,p,ge,ret,st,s.
524  match s return λx.IO ??? with
525    [ tailcall c ⇒
526      !〈flow,st'〉 ← eval_ext_tailcall … ge c ret st ;
527      return st'
528    | _ ⇒ return st
529    ].
530
531definition eval_fin_step_pc :
532 ∀globals.∀p:sem_params. genv p globals → call_dest p → state p →
533  ∀s:joint_fin_step p.
534  IO io_out io_in (fin_step_flow p ? (fin_step_flows … s)) ≝
535  λg,p,ge,ret,st,s.
536  match s return λx.IO ?? (fin_step_flow ?? (fin_step_flows … x)) with
537  [ tailcall c ⇒
538    !〈flow,st'〉 ← eval_ext_tailcall … ge c ret st ;
539    return flow 
540  | GOTO l ⇒ return FRedirect … l
541  | RETURN ⇒ return FEnd1 ??
542  ]. %1 % qed.
543
544definition do_call : ∀globals: list ident.∀p:sem_params. genv p globals →
545  state p → Z → joint_internal_function p globals → call_args p →
546  res (state_pc p) ≝
547  λglobals,p,ge,st,id,fn,args.
548    ! st' ← setup_call … (joint_if_stacksize … fn) (joint_if_params … fn)
549              args st ;
550    let regs ≝ foldr ?? (allocate_local … p) (regs … st) (joint_if_locals … fn) in
551    let l' ≝ joint_if_entry … fn in
552    let st' ≝ set_regs p regs st in
553    let pointer_in_fn ≝ mk_pointer (mk_block Code id) (mk_offset (bv_zero …)) in
554    ! pc ← pointer_of_point ? p … pointer_in_fn l' ;
555    return mk_state_pc ? st' pc. % qed.
556
557(* The pointer provided is the one to the *next* instruction. *)
558definition eval_step_flow :
559 ∀globals.∀p:sem_params.∀flows.genv p globals →
560 state p → cpointer → step_flow p ? flows → res (state_pc p) ≝
561 λglobals,p,flows,ge,st,nxt,cmd.
562 match cmd with
563  [ Redirect _ l ⇒
564    goto … ge l st nxt
565  | Init id fn args dest ⇒
566    ! st' ← save_frame … nxt dest st ;
567    do_call ?? ge st' id fn args
568  | Proceed _ ⇒
569    return mk_state_pc ? st nxt
570  ].
571
572definition eval_fin_step_flow : ∀globals: list ident.∀p:sem_params.∀flows. genv p globals →
573  state p → cpointer → fin_step_flow p ? flows → res (state_pc p) ≝
574  λglobals,p,lbls,ge,st,curr,cmd.
575  match cmd with
576  [ FRedirect _ l ⇒ goto … ge l st curr
577  | FTailInit id fn args ⇒
578    do_call … ge st id fn args
579  | _ ⇒
580    ! 〈st',ra〉 ← fetch_ra … st ;
581    ! fn ← fetch_function … ge curr ;
582    ! st'' ← pop_frame … ge (joint_if_result … fn) st';
583    return mk_state_pc ? st'' ra
584  ].
585
586definition eval_statement :
587 ∀globals.∀p:sem_params.genv p globals →
588  state_pc p → joint_internal_function p globals → joint_statement p globals →
589    IO io_out io_in (state_pc p) ≝
590 λglobals,p,ge,st,curr_fn,stmt.
591 match stmt with
592 [ sequential s nxt ⇒
593   ! 〈flow,st'〉 ← eval_step … ge st s ;
594   ! nxtptr ← succ_pc ? p (pc … st) nxt ;
595   eval_step_flow … ge st' nxtptr flow
596 | final s ⇒
597   let ret ≝ joint_if_result … curr_fn in
598   ! st' ← eval_fin_step_no_pc … ge ret st s ;
599   ! flow ← eval_fin_step_pc … ge ret st s ;
600   eval_fin_step_flow … ge st' (pc … st) flow
601 ].
602
603definition eval_state : ∀globals: list ident.∀p:sem_params. genv p globals →
604  state_pc p → IO io_out io_in (state_pc p) ≝
605  λglobals,p,ge,st.
606  ! 〈fn,s〉 ← fetch_statement ? p … ge (pc … st) : IO ???;
607  eval_statement … ge st fn s.
608
609(* Paolo: what if in an intermediate language main finishes with an external
610  tailcall? Maybe it should rely on an FEnd flow command issued, but that's
611  not static... *)
612definition is_final: ∀globals:list ident. ∀p: sem_params.
613  genv p globals → cpointer → state_pc p → option int ≝
614 λglobals,p,ge,exit,st.res_to_opt ? (
615  do 〈fn,s〉 ← fetch_statement ? p … ge (pc … st);
616  match s with
617  [ final s' ⇒
618    match s' with
619    [ RETURN ⇒
620      do 〈st',ra〉 ← fetch_ra … st;
621      if eq_pointer ra exit then
622       do vals ← read_result … ge (joint_if_result … fn) st' ;
623       Word_of_list_beval vals
624      else
625       Error ? [ ]
626   | _ ⇒ Error ? [ ]
627   ]
628 | _ ⇒ Error ? [ ]
629 ]).
630
631(*
632record evaluation_parameters : Type[1] ≝
633 { globals: list ident
634 ; sparams:> sem_params
635 ; exit: cpointer
636 ; genv2: genv globals sparams
637 }.
638
639(* Paolo: with structured traces, eval need not emit labels. However, this
640  changes trans_system. For now, just putting a dummy thing for
641  the transition. *)
642definition joint_exec: trans_system io_out io_in ≝
643  mk_trans_system … evaluation_parameters (λG. state_pc G)
644   (λG.is_final (globals G) G (genv2 G) (exit G))
645   (λG,st.! 〈flag,st'〉 ← eval_state_flag (globals G) G (genv2 G) st ; return 〈E0, st'〉).
646
647definition make_global :
648 ∀pars: sem_params.
649  joint_program pars → evaluation_parameters
650
651 λpars.
652 (* Invariant: a -1 block is unused in common/Globalenvs *)
653 let b ≝ mk_block Code (-1) in
654 let ptr ≝ mk_pointer Code b ? (mk_offset 0) in
655  (λp. mk_evaluation_parameters
656    (prog_var_names … p)
657    (mk_sem_params … pars)
658    ptr
659    (globalenv_noinit … p)
660  ).
661% qed.
662
663axiom ExternalMain: String.
664
665definition make_initial_state :
666 ∀pars: sem_params.
667 ∀p: joint_program … pars. res (state_pc pars) ≝
668λpars,p.
669  let sem_globals ≝ make_global pars p in
670  let ge ≝ genv2 sem_globals in
671  let m ≝ alloc_mem … p in
672  let 〈m,spb〉 ≝ alloc … m 0 external_ram_size XData in
673  let 〈m,ispb〉 ≝ alloc … m 0 internal_ram_size XData in
674  let dummy_pc ≝ mk_pointer Code (mk_block Code (-1)) ? (mk_offset 0) in
675  let spp ≝ mk_pointer XData spb ? (mk_offset external_ram_size) in
676  let ispp ≝ mk_pointer XData ispb ? (mk_offset 47) in
677  let main ≝ prog_main … p in
678  let st0 ≝ mk_state pars (empty_framesT …) spp ispp BVfalse (empty_regsT … spp) m in
679  (* use exit sem_globals as ra and call_dest_for_main as dest *)
680  let st0' ≝ set_frms ? (save_frame … (exit sem_globals) (call_dest_for_main … pars) st0) st0 in
681  let st_pc0 ≝ mk_state_pc ? st0' dummy_pc in
682  ! main_block ← opt_to_res … [MSG MissingSymbol; CTX ? main] (find_symbol … ge main) ;
683  ! main_fd ← opt_to_res ? [MSG BadPointer] (find_funct_ptr … ge main_block) ;
684  match main_fd with
685  [ Internal fn ⇒
686    do_call ?? ge st_pc0 (block_id main_block) fn (call_args_for_main … pars)
687  | External _ ⇒ Error … [MSG ExternalMain] (* External main not supported: why? *)
688  ]. [5: cases ispb * |6: cases spb * ] (* without try it fails! *) try //
689qed.
690
691definition joint_fullexec :
692 ∀pars:sem_params.fullexec io_out io_in ≝
693 λpars.mk_fullexec ??? joint_exec (make_global pars) (make_initial_state pars).
694*)
Note: See TracBrowser for help on using the repository browser.