source: src/joint/semantics_paolo.ma @ 2186

Last change on this file since 2186 was 2186, checked in by tranquil, 8 years ago

updated joint semantics

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