source: src/joint/semantics_paolo.ma @ 1971

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