source: src/joint/semantics_paolo.ma @ 1993

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