source: src/joint/semantics_paolo.ma @ 2125

Last change on this file since 2125 was 1999, checked in by campbell, 8 years ago

Make back-end use the main global envs.

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