source: src/joint/joint_semantics.ma @ 2954

Last change on this file since 2954 was 2954, checked in by tranquil, 7 years ago

resolved circular dependency for ERTLptr's semantics

File size: 25.5 KB
Line 
1include "common/Globalenvs.ma".
2include "common/IO.ma".
3(* include "common/SmallstepExec.ma". *)
4include "joint/BEMem.ma".
5include "joint/Joint.ma".
6include "ASM/I8051bis.ma".
7include "common/extraGlobalenvs.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
14(* Paolo: I'll put in this record the property about genv we need *)
15record genv_gen (F : list ident → Type[0]) (globals : list ident) : Type[0] ≝
16{ ge :> genv_t (fundef (F globals))
17; find_symbol_in_globals : ∀s.In … globals s → find_symbol … ge s ≠ None ?
18; stack_sizes : ident → option ℕ
19; premain : F globals
20; pc_from_label : (Σbl.block_region bl = Code) → F globals → label →
21    option program_counter
22}.
23
24definition pre_main_id : ident ≝ an_identifier … one.
25
26(* this can replace graph_fetch function and lin_fetch_function *)
27definition fetch_function:
28 ∀F,globals.
29 ∀ge : genv_gen F globals.
30  (Σb.block_region b = Code) →
31  res (ident×(fundef (F globals))) ≝
32 λF,g,ge,bl.
33 if eqZb (block_id bl) (-1) then
34   return 〈pre_main_id, Internal ? (premain … ge)〉
35 else
36   opt_to_res … [MSG BadFunction]
37    (! id ← symbol_for_block … ge bl ;
38     ! fd ← find_funct_ptr … ge bl ;
39     return 〈id, fd〉).
40
41definition fetch_internal_function :
42 ∀F,globals.
43 ∀ge : genv_gen F globals.
44  (Σb.block_region b = Code) →
45  res (ident×(F globals)) ≝
46 λF,g,ge,bl.
47 ! 〈id, fd〉 ← fetch_function … ge bl ;
48 match fd with
49 [ Internal ifd ⇒ return 〈id, ifd〉
50 | _ ⇒ Error … [MSG BadFunction]
51 ].
52
53definition code_block_of_block : block → option (Σb.block_region b = Code) ≝
54λbl.match block_region bl
55  return λx.block_region bl = x → option (Σb.block_region b = Code) with
56  [ Code ⇒ λprf.Some ? «bl, prf»
57  | XData ⇒ λ_.None ?
58  ] (refl …).
59
60definition block_of_funct_id ≝  λF.
61  λge: genv_t F.λid.
62  opt_to_res … [MSG BadFunction; CTX … id] (
63    ! bl ← find_symbol … ge id;
64    code_block_of_block bl).
65
66(* this is equal to pc_of_label defined later, but can be used in
67   generic definitions of mk_sem_unserialised_params *)
68definition gen_pc_from_label :
69  ∀F.∀globals.
70  genv_gen F globals →
71  ident (* current function *) → label → res program_counter ≝
72  λF,g,ge,id,lbl.
73  ! bl ← block_of_funct_id … ge id ;
74  ! 〈ignore, f_def〉 ← fetch_internal_function … ge bl ;
75  opt_to_res … [MSG LabelNotFound ; CTX ? lbl]
76    (pc_from_label … ge bl f_def lbl).
77
78definition genv ≝ λp.genv_gen (joint_closed_internal_function p).
79coercion genv_to_genv_t :
80  ∀p,globals.∀g : genv p globals.genv_t (joint_function p globals) ≝
81  λp,globals,g.ge ?? g on _g : genv ?? to genv_t ?.
82
83record sem_state_params : Type[1] ≝
84 { framesT: Type[0]
85 ; empty_framesT: framesT
86 ; regsT : Type[0]
87 (* empty_regsT called at the start of each function call *)
88 ; empty_regsT: xpointer → regsT (* initial stack pointer *)
89 ; load_sp : regsT → res xpointer
90 ; save_sp : regsT → xpointer → regsT
91 }.
92
93inductive internal_stack : Type[0] ≝
94| empty_is : internal_stack
95| one_is : beval → internal_stack
96| both_is : beval → beval → internal_stack.
97
98definition is_push : internal_stack → beval → res internal_stack ≝
99λis,bv.match is with
100[ empty_is ⇒ return one_is bv
101| one_is bv' ⇒ return both_is bv' bv
102| both_is _ _ ⇒ Error … [MSG … InternalStackFull]
103].
104
105definition is_pop : internal_stack → res (beval × internal_stack) ≝
106λis.match is with
107[ empty_is ⇒ Error … [MSG … InternalStackEmpty]
108| one_is bv' ⇒ return 〈bv', empty_is〉
109| both_is bv bv' ⇒ return 〈bv', one_is bv〉
110].
111
112record state (semp: sem_state_params): Type[0] ≝
113 { st_frms: option(framesT semp)
114 ; istack : internal_stack
115 ; carry: bebit
116 ; regs: regsT semp
117 ; m: bemem
118 ; stack_usage : ℕ
119 }.
120
121definition sp ≝ λp,st.load_sp p (regs ? st).
122
123record state_pc (semp : sem_state_params) : Type[0] ≝
124  { st_no_pc :> state semp
125  ; pc : program_counter
126  (* for correctness reasons: pc of last popped calling address (null_pc at the start) *)
127  ; last_pop : program_counter
128  }.
129
130definition init_pc : program_counter ≝
131  mk_program_counter «mk_block (-1), refl …» one.
132
133definition null_pc : Pos →  program_counter ≝ λpos.
134    mk_program_counter «dummy_block_code, refl …» pos.
135
136definition set_m: ∀p. bemem → state p → state p ≝
137 λp,m,st. mk_state p (st_frms …st) (istack … st) (carry … st) (regs … st) m (stack_usage … st).
138
139definition set_regs: ∀p:sem_state_params. regsT p → state p → state p ≝
140 λp,regs,st.mk_state p (st_frms … st) (istack … st) (carry … st) regs (m … st) (stack_usage … st).
141
142definition set_sp: ∀p. ? → state p → state p ≝
143 λp,sp,st.let regs' ≝ save_sp … (regs … st) sp in
144 mk_state p (st_frms … st) (istack … st) (carry … st) regs' (m … st) (stack_usage … st).
145
146definition set_carry: ∀p. bebit → state p → state p ≝
147 λp,carry,st. mk_state … (st_frms … st) (istack … st) carry (regs … st) (m … st) (stack_usage … st).
148
149definition set_istack: ∀p. internal_stack → state p → state p ≝
150 λp,is,st. mk_state … (st_frms … st) is (carry … st) (regs … st) (m … st) (stack_usage … st).
151
152definition set_pc: ∀p. ? → state_pc p → state_pc p ≝
153 λp,pc,st. mk_state_pc … (st_no_pc … st) pc (last_pop … st).
154
155definition set_no_pc: ∀p. ? → state_pc p → state_pc p ≝
156 λp,s,st. mk_state_pc … s (pc … st) (last_pop … st).
157
158definition set_last_pop: ∀p.state p → program_counter → state_pc p ≝
159 λp,st,pc. mk_state_pc … st pc pc.
160
161definition set_frms: ∀p:sem_state_params. framesT p → state p → state p ≝
162 λp,frms,st. mk_state … (Some ? (frms)) (istack … st) (carry … st) (regs … st) (m … st) (stack_usage … st).
163
164(*
165inductive step_flow (p : unserialized_params) (F : Type[0]) : possible_flows → Type[0] ≝
166  | Redirect : ∀lbls.(Σl.In ? lbls l) → step_flow p F (Labels lbls) (* used for goto-like flow alteration *)
167  | Init     : Z → F → call_args p → call_dest p → step_flow p F Call (* call a function with given id, then proceed *)
168  | Proceed  : ∀flows.step_flow p F flows. (* go to implicit successor *)
169
170inductive fin_step_flow (p : unserialized_params) (F : Type[0]) : possible_flows → Type[0] ≝
171  | FRedirect : ∀lbls.(Σl.In ? lbls l) → fin_step_flow p F (Labels lbls)
172  | FTailInit : Z → F → call_args p → fin_step_flow p F Call
173  | FEnd1  : fin_step_flow p F (Labels [ ]) (* end flow *)
174  | FEnd2  : fin_step_flow p F Call. (* end flow *)
175*)
176
177(* lemma fetch_internal_function_minus_one :
178  ∀F,V,i,p,bl.
179  block_id (pi1 … bl) = -1 →
180  fetch_internal_function … (globalenv (λvars.fundef (F vars)) V i p)
181    bl = Error … [MSG BadFunction].
182 #F#V#i#p ** #id #EQ1 #EQ2 destruct
183 whd in match fetch_internal_function;
184  whd in match fetch_function; normalize nodelta
185  >globalenv_no_minus_one
186  cases (symbol_for_block ???) normalize //
187qed.
188*)
189
190inductive call_kind : Type[0] ≝
191| PTR : call_kind
192| ID : call_kind.
193
194definition kind_of_call :
195  ∀p.(ident + (dpl_arg p × (dph_arg p))) → call_kind ≝
196  λp,f.match f with [ inl _ ⇒ ID | inr _ ⇒ PTR ].
197
198record sem_unserialized_params
199  (uns_pars : unserialized_params)
200  (F : list ident → Type[0]) : Type[1] ≝
201  { st_pars :> sem_state_params
202
203  ; acca_store_ : acc_a_reg uns_pars → beval → regsT st_pars → res (regsT st_pars)
204  ; acca_retrieve_ : regsT st_pars → acc_a_reg uns_pars → res beval
205  ; acca_arg_retrieve_ : regsT st_pars → acc_a_arg uns_pars → res beval
206  ; accb_store_ : acc_b_reg uns_pars → beval → regsT st_pars → res (regsT st_pars)
207  ; accb_retrieve_ : regsT st_pars → acc_b_reg uns_pars → res beval
208  ; accb_arg_retrieve_ : regsT st_pars → acc_b_arg uns_pars → res beval
209  ; dpl_store_ : dpl_reg uns_pars → beval → regsT st_pars → res (regsT st_pars)
210  ; dpl_retrieve_ : regsT st_pars → dpl_reg uns_pars → res beval
211  ; dpl_arg_retrieve_ : regsT st_pars → dpl_arg uns_pars → res beval
212  ; dph_store_ : dph_reg uns_pars → beval → regsT st_pars → res (regsT st_pars)
213  ; dph_retrieve_ : regsT st_pars → dph_reg uns_pars → res beval
214  ; dph_arg_retrieve_ : regsT st_pars → dph_arg uns_pars → res beval
215  ; snd_arg_retrieve_ : regsT st_pars → snd_arg uns_pars → res beval
216  ; pair_reg_move_ : regsT st_pars → pair_move uns_pars → res (regsT st_pars)
217 
218  (* Paolo: save_frame separated from call_setup to factorize tailcall code *)
219  (* ; allocate_locals_ : localsT uns_pars → regsT st_pars → regsT st_pars *)
220  ; save_frame: call_kind → call_dest uns_pars → state_pc st_pars → res (state st_pars)
221   (*CSC: setup_call returns a res only because we can call a function with the wrong number and
222     type of arguments. To be fixed using a dependent type *)
223  ; setup_call : nat → paramsT … uns_pars → call_args uns_pars →
224      state st_pars → res (state st_pars)
225  ; fetch_external_args: external_function → state st_pars → call_args … uns_pars →
226      res (list val)
227  ; set_result: list val → call_dest uns_pars → state st_pars → res (state st_pars)
228  ; call_args_for_main: call_args uns_pars
229  ; call_dest_for_main: call_dest uns_pars
230
231  (* from now on, parameters that use the type of functions *)
232  ; read_result: ∀globals.genv_t (fundef (F globals)) → call_dest uns_pars →
233      state st_pars → res (list beval)
234  ; eval_ext_seq: ∀globals.∀ge : genv_gen F globals.ext_seq uns_pars →
235    ident (* current *) → state st_pars → res (state st_pars)
236  ; pop_frame: ∀globals.∀ge : genv_gen F globals.
237    ident (* current *) → call_dest uns_pars (* current ret *) →
238      state st_pars → res (state st_pars × program_counter)
239  }.
240
241(*
242definition allocate_locals :
243  ∀p,F.∀sup : sem_unserialized_params p F.
244  list (localsT p) → state sup → state sup ≝
245  λp,F,sup,l,st.
246  let r ≝ foldr … (allocate_locals_ … sup) (regs … st) l in
247  set_regs … r st. *)
248
249definition helper_def_retrieve :
250  ∀X : ? → ? → ? → Type[0].
251  (∀up,F.∀p:sem_unserialized_params up F. regsT (st_pars up F p) → X up F p → res beval) →
252  ∀up,F.∀p : sem_unserialized_params up F.state (st_pars up F p) → X up F p → res beval ≝
253    λX,f,up,F,p,st.f ?? p (regs … st).
254
255definition helper_def_store :
256  ∀X : ? → ? → ? → Type[0].
257  (∀up,F.∀p : sem_unserialized_params up F.X up F p → beval → regsT (st_pars … p) → res (regsT (st_pars … p))) →
258  ∀up,F.∀p : sem_unserialized_params up F.X up F p → beval → state (st_pars … p) → res (state (st_pars … p)) ≝
259  λX,f,up,F,p,x,v,st.! r ← f ?? p x v (regs … st) ; return set_regs … r st.
260
261definition acca_retrieve ≝ helper_def_retrieve ? acca_retrieve_.
262definition acca_store ≝ helper_def_store ? acca_store_.
263definition acca_arg_retrieve ≝ helper_def_retrieve ? acca_arg_retrieve_.
264definition accb_store ≝ helper_def_store ? accb_store_.
265definition accb_retrieve ≝ helper_def_retrieve ? accb_retrieve_.
266definition accb_arg_retrieve ≝ helper_def_retrieve ? accb_arg_retrieve_.
267definition dpl_store ≝ helper_def_store ? dpl_store_.
268definition dpl_retrieve ≝ helper_def_retrieve ? dpl_retrieve_.
269definition dpl_arg_retrieve ≝ helper_def_retrieve ? dpl_arg_retrieve_.
270definition dph_store ≝ helper_def_store ? dph_store_.
271definition dph_retrieve ≝ helper_def_retrieve ? dph_retrieve_.
272definition dph_arg_retrieve ≝ helper_def_retrieve ? dph_arg_retrieve_.
273definition snd_arg_retrieve ≝ helper_def_retrieve ? snd_arg_retrieve_.
274definition pair_reg_move ≝
275  λup,F.λp : sem_unserialized_params up F.λst : state (st_pars … p).λpm : pair_move up.
276    ! r ← pair_reg_move_ ?? p (regs ? st) pm;
277    return set_regs ? r st.
278 
279definition push: ∀p.state p → beval → res (state p) ≝
280 λp,st,v.
281 ! is ← is_push (istack … st) v ;
282 return set_istack … is st.
283
284definition pop: ∀p. state p → res (beval × (state p)) ≝
285 λp,st.
286 ! 〈bv, is〉 ← is_pop (istack … st) ;
287 return 〈bv, set_istack … is st〉.
288
289definition push_ra : ∀p. state p → program_counter → res (state p) ≝
290 λp,st,l.
291  let 〈addrl,addrh〉 ≝  beval_pair_of_pc l in
292  ! st' ← push … st addrl;
293  push … st' addrh.
294
295definition pop_ra : ∀p.state p → res (state p × program_counter) ≝
296 λp,st.
297  ! 〈addrh, st'〉 ← pop … st;
298  ! 〈addrl, st''〉 ← pop … st';
299  ! pr ← pc_of_bevals [addrl; addrh];
300  return 〈st'',pr〉.
301
302(* parameters that are defined by serialization *)
303record serialized_params : Type[1] ≝
304  { spp :> params
305  ; msu_pars :> sem_unserialized_params spp (joint_closed_internal_function spp)
306  ; offset_of_point : code_point spp → Pos
307  ; point_of_offset : Pos → code_point spp
308  ; point_of_offset_of_point :
309    ∀pt.point_of_offset (offset_of_point pt) = pt
310  ; offset_of_point_of_offset :
311    ∀o.offset_of_point (point_of_offset o) = o
312  }.
313
314record sem_params : Type[1] ≝
315  { spp' :> serialized_params
316  ; pre_main_generator : ∀p : joint_program spp'.joint_closed_internal_function spp' (prog_var_names … p)
317  }.
318
319(*
320coercion ms_pars_to_msu_pars nocomposites :
321∀p : params.∀msp : more_sem_params p.more_sem_unserialized_params p (λglobals.joint_internal_function globals p)
322 ≝ msu_pars
323on _msp : more_sem_params ? to more_sem_unserialized_params ??.
324
325definition ss_pars_of_ms_pars ≝
326  λp.λpp : more_sem_params p.
327  st_pars … (msu_pars … pp).
328coercion ms_pars_to_ss_pars nocomposites :
329∀p : params.∀msp : more_sem_params p.sem_state_params ≝
330ss_pars_of_ms_pars on _msp : more_sem_params ? to sem_state_params.*)
331
332definition pc_of_point : ∀p:sem_params.(Σb.block_region b = Code) →
333  code_point p → program_counter ≝
334  λp,bl,pt.
335  mk_program_counter bl (offset_of_point p pt).
336
337definition point_of_pc :
338  ∀p:sem_params.program_counter → code_point p ≝
339  λp,ptr.point_of_offset p (pc_offset ptr).
340
341lemma point_of_pc_of_point :
342  ∀p,bl,pt.
343  point_of_pc p (pc_of_point p bl pt) = pt.
344#p #bl #pt normalize // qed.
345
346lemma pc_of_point_of_pc :
347  ∀p,ptr.
348    pc_of_point p (pc_block ptr) (point_of_pc p ptr) = ptr.
349#p * #bl #off normalize >offset_of_point_of_offset % qed.
350
351definition fetch_statement: ∀p : sem_params.∀globals.
352  ∀ge : genv p globals. program_counter →
353  res (ident × (joint_closed_internal_function p globals) × (joint_statement p globals)) ≝
354  λp,globals,ge,ptr.
355  ! 〈id, fn〉 ← fetch_internal_function … ge (pc_block ptr) ;
356  let pt ≝ point_of_pc p ptr in
357  ! stmt ← opt_to_res … (msg ProgramCounterOutOfCode) (stmt_at … (joint_if_code … fn) pt);
358  return 〈id, fn, stmt〉.
359
360definition pc_of_label : ∀p : sem_params.∀globals.
361  genv p globals → (Σb.block_region b = Code) → label → res program_counter ≝
362  λp,globals,ge,bl,lbl.
363  ! 〈i, fn〉 ← fetch_internal_function … ge bl ;
364  ! pt ← opt_to_res … [MSG LabelNotFound ; CTX ? lbl]
365            (point_of_label … (joint_if_code … fn) lbl) ;
366  return mk_program_counter bl (offset_of_point p pt).
367
368definition succ_pc : ∀p : sem_params.
369  program_counter → succ p → program_counter ≝
370  λp,ptr,nxt.
371  let curr ≝ point_of_pc p ptr in
372  pc_of_point p (pc_block ptr) (point_of_succ p curr nxt).
373
374(*
375record sem_params : Type[1] ≝
376  { spp :> params
377  ; more_sem_pars :> more_sem_params spp
378  }.
379*)
380(* definition msu_pars_of_s_pars :
381∀p : sem_params.more_sem_unserialized_params (spp p) (λglobals.joint_internal_function globals (spp p))
382≝ λp : sem_params.
383  msu_pars … (more_sem_pars p).
384coercion s_pars_to_msu_pars nocomposites :
385∀p : sem_params.more_sem_unserialized_params (spp p) (λglobals.joint_internal_function globals (spp p)) ≝
386msu_pars_of_s_pars
387on p : sem_params to more_sem_unserialized_params ??.
388
389definition ss_pars_of_s_pars :
390∀p : sem_params.sem_state_params
391≝ λp : sem_params.
392  st_pars … (msu_pars … (more_sem_pars p)).
393coercion s_pars_to_ss_pars nocomposites :
394∀p : sem_params.sem_state_params ≝
395ss_pars_of_s_pars
396on _p : sem_params to sem_state_params.
397
398definition ms_pars_of_s_pars :
399∀p : sem_params.more_sem_params (spp p)
400≝ more_sem_pars.
401coercion s_pars_to_ms_pars nocomposites :
402∀p : sem_params.more_sem_params (spp p) ≝
403ms_pars_of_s_pars
404on p : sem_params to more_sem_params ?.*)
405
406(* definition address_of_label: ∀globals. ∀p:sem_params.
407  genv globals p → pointer → label → res address ≝
408 λglobals,p,ge,ptr,l.
409  do newptr ← pointer_of_label … p ? ge … ptr l ;
410  OK … (address_of_code_pointer newptr). *)
411
412definition goto: ∀p : sem_params.∀globals.
413  genv p globals → label → state_pc p → res (state_pc p) ≝
414 λp,globals,ge,l,st.
415  ! newpc ← pc_of_label … ge (pc_block (pc … st)) l ;
416  return set_pc … newpc st.
417
418(*
419definition empty_state: ∀p. more_sem_params p → state p ≝
420 mk_state … (empty_framesT …)
421*)
422
423definition next : ∀p : sem_params.succ p → state_pc p → state_pc p ≝
424 λp,l,st.
425 let newpc ≝ succ_pc … (pc … st) l in
426 set_pc … newpc st.
427
428definition next_of_call_pc : ∀p : sem_params.∀globals.
429  genv p globals →
430  program_counter → res (succ p) ≝
431λp,globals,ge,pc.
432  ! 〈id_fn, stmt〉 ← fetch_statement … ge pc ;
433  match stmt with
434  [ sequential s nxt ⇒
435    match s with
436    [ CALL _ _ _ ⇒ return nxt
437    | _ ⇒ Error … [MSG NoSuccessor]
438    ]
439  | _ ⇒ Error … [MSG NoSuccessor]
440  ].
441
442lemma deq_elim : ∀A : DeqSet.∀P : bool → Prop.∀x,y : A.
443(x = y → P true) → (x ≠ y → P false) → P (x == y).
444#A #P #x #y #H1 #H2 inversion (x == y) #EQ
445[ @H1 @(proj1 … (eqb_true … ) EQ) | @H2 % #EQ' destruct
446  >(proj2 … (eqb_true …) (refl …)) in EQ; #ABS destruct ] qed.
447
448definition eval_seq_no_pc :
449 ∀p:sem_params.∀globals.∀ge:genv p globals.ident →
450  joint_seq p globals → state p →
451  res (state p) ≝
452 λp,globals,ge,curr_id,seq,st.
453 match seq with
454  [ extension_seq c ⇒
455    eval_ext_seq … ge c curr_id st
456  | LOAD dst addrl addrh ⇒
457    ! vaddrh ← dph_arg_retrieve … st addrh ;
458    ! vaddrl ← dpl_arg_retrieve … st addrl;
459    ! vaddr ← pointer_of_address 〈vaddrl,vaddrh〉;
460    ! v ← opt_to_res … (msg FailedLoad) (beloadv (m … st) vaddr);
461    acca_store p … dst v st
462 | STORE addrl addrh src ⇒
463    ! vaddrh ← dph_arg_retrieve … st addrh;
464    ! vaddrl ← dpl_arg_retrieve … st addrl;
465    ! vaddr ← pointer_of_address 〈vaddrl,vaddrh〉;
466    ! v ← acca_arg_retrieve … st src;
467    ! m' ← opt_to_res … (msg FailedStore) (bestorev (m … st) vaddr v);
468    return set_m … m' st
469  | ADDRESS id prf ldest hdest ⇒
470    let addr_block ≝ opt_safe ? (find_symbol … ge id) ? in
471    let 〈laddr,haddr〉 ≝ beval_pair_of_pointer (mk_pointer addr_block zero_offset) in
472    ! st' ← dpl_store … ldest laddr st;
473    dph_store … hdest haddr st'
474  | OP1 op dacc_a sacc_a ⇒
475    ! v ← acca_retrieve … st sacc_a;
476    ! v' ← be_op1 op v ;
477    acca_store … dacc_a v' st
478  | OP2 op dacc_a sacc_a src ⇒
479    ! v1 ← acca_arg_retrieve … st sacc_a;
480    ! v2 ← snd_arg_retrieve … st src;
481    ! 〈v',carry〉 ← be_op2 (carry … st) op v1 v2 ;
482    ! st' ← acca_store … dacc_a v' st;
483    return set_carry … carry st'
484  | CLEAR_CARRY ⇒
485    return set_carry … (BBbit false) st
486  | SET_CARRY ⇒
487    return set_carry … (BBbit true) st
488  | OPACCS op dacc_a_reg dacc_b_reg sacc_a_reg sacc_b_reg ⇒
489    ! v1 ← acca_arg_retrieve … st sacc_a_reg;
490    ! v2 ← accb_arg_retrieve … st sacc_b_reg;
491    ! 〈v1',v2'〉 ← be_opaccs op v1 v2 ;
492    ! st' ← acca_store … dacc_a_reg v1' st;
493    accb_store … dacc_b_reg v2' st'
494  | POP dst ⇒
495    ! 〈v, st'〉 ← pop p st;
496    acca_store … p dst v st'
497  | PUSH src ⇒
498    ! v ← acca_arg_retrieve … st src;
499    push … st v
500  | MOVE dst_src ⇒
501    pair_reg_move … st dst_src
502  | _ ⇒ return st (* for calls do everything in eval_seq_advance *)
503  ].
504  @hide_prf
505  @find_symbol_in_globals
506  lapply prf
507  elim globals [*]
508  #hd #tl #IH #H elim (orb_Prop_true … H) -H
509  [ @deq_elim #H * destruct %1 % | #H %2{(IH … H)} ]
510qed.
511
512definition block_of_call ≝ λp : sem_params.
513  λglobals.λge: genv_t (joint_function p globals).λf.λst : state p.
514  ! bl ← match f with
515    [ inl id ⇒
516      opt_to_res … [MSG BadFunction; CTX … id]
517        (find_symbol … ge id)
518    | inr addr ⇒
519      ! addr_l ← dpl_arg_retrieve … st (\fst addr) ;
520      ! addr_h ← dph_arg_retrieve … st (\snd addr) ;
521      ! ptr ← pointer_of_bevals … [addr_l ; addr_h ] ;
522      if eq_bv … (bv_zero …) (offv (poff ptr)) then
523        return pblock ptr
524      else
525        Error … [MSG BadFunction; MSG BadPointer]
526    ] ;
527  opt_to_res … [MSG BadFunction; MSG BadPointer]
528    (code_block_of_block bl).
529
530definition eval_external_call ≝
531λp : sem_params.λfn,args,dest,st.
532      ! params ← fetch_external_args … p fn st args : IO ???;
533      ! evargs ← check_eventval_list params (sig_args (ef_sig fn)) : IO ???;
534      ! evres ← do_io (ef_id fn) evargs (proj_sig_res (ef_sig fn));
535      (* CSC: XXX bug here; I think I should split it into Byte-long
536         components; instead I am making a singleton out of it. To be
537         fixed once we fully implement external functions. *)
538      let vs ≝ [mk_val ? evres] in
539      set_result … p vs dest st.
540
541definition increment_stack_usage : ∀p.ℕ → state p → state p ≝
542 λp,n,st.mk_state p (st_frms … st) (istack … st) (carry … st) (regs … st) (m … st)
543  (n + stack_usage … st).
544
545definition decrement_stack_usage : ∀p.ℕ → state p → state p ≝
546 λp,n,st.mk_state p (st_frms … st) (istack … st) (carry … st) (regs … st) (m … st)
547  (stack_usage … st - n).
548
549definition eval_internal_call ≝
550λp : sem_params.λglobals : list ident.λge : genv p globals.λi,fn,args.
551λst : state p.
552! stack_size ← opt_to_res … [MSG MissingStackSize; CTX … i] (stack_sizes … ge i) ;
553! st' ← setup_call … stack_size (joint_if_params … globals fn) args st ;
554return increment_stack_usage … stack_size st'.
555
556definition is_inl : ∀A,B.A+B → bool ≝ λA,B,x.match x with [ inl _ ⇒ true | _ ⇒ false ].
557
558definition eval_call ≝
559λp : sem_params.λglobals : list ident.λge : genv p globals.λf,args,dest,nxt.
560λst : state_pc p.
561! bl ← block_of_call … ge f st : IO ???;
562! 〈i, fd〉 ← fetch_function … ge bl : IO ???;
563match fd with
564[ Internal ifd ⇒
565  ! st' ← save_frame … (kind_of_call … f) dest st ;
566  ! st'' ← eval_internal_call p globals ge i ifd args st' ;
567  let pc ≝ pc_of_point p bl (joint_if_entry … ifd) in
568  return mk_state_pc … st'' pc (last_pop … st)
569| External efd ⇒
570  ! st' ← eval_external_call … efd args dest st ;
571  return mk_state_pc … st' (succ_pc p (pc … st) nxt) (last_pop … st)
572].
573
574definition eval_statement_no_pc :
575 ∀p:sem_params.∀globals.∀ge:genv p globals.
576 ident (* current *) →
577 joint_statement p globals → state p → res (state p) ≝
578 λp,globals,ge,curr_id,s,st.
579  match s with
580  [ sequential s next ⇒
581    match s with
582    [ step_seq s ⇒ eval_seq_no_pc … ge curr_id s st
583    | _ ⇒ return st
584    ]
585  | _ ⇒ return st
586  ].
587
588definition eval_return ≝
589λp : sem_params.λglobals : list ident.λge : genv p globals.
590λcurr_id.λcurr_ret : call_dest p.
591λst : state p.
592! stack_size ← opt_to_res … [MSG MissingStackSize; CTX … curr_id] (stack_sizes … ge curr_id) ;
593! 〈st', call_pc〉 ← pop_frame … ge curr_id curr_ret st ;
594! nxt ← next_of_call_pc … ge call_pc ;
595let st'' ≝ set_last_pop … (decrement_stack_usage … stack_size st') call_pc in
596return
597  next ? nxt st'' (* now address pushed on stack are calling ones! *).
598
599definition eval_tailcall ≝
600λp : sem_params.λglobals : list ident.λge : genv p globals.λf,args,curr_f.
601λcurr_ret : call_dest p.
602λst : state_pc p.
603! bl ← block_of_call … ge f st : IO ???;
604! 〈i, fd〉 ← fetch_function … ge bl : IO ???;
605match fd with
606[ Internal ifd ⇒
607  ! stack_size ← opt_to_res … [MSG MissingStackSize; CTX … curr_f] (stack_sizes … ge curr_f) ;
608  let st' ≝ decrement_stack_usage … stack_size st in
609  ! st'' ← eval_internal_call p globals ge i ifd args st' ;
610  let pc ≝ pc_of_point p bl (joint_if_entry … ifd) in
611  return mk_state_pc … st'' pc (last_pop … st)
612| External efd ⇒
613  ! st' ← eval_external_call … efd args curr_ret st ;
614  eval_return … ge curr_f curr_ret st
615].
616
617definition eval_statement_advance :
618 ∀p:sem_params.∀globals.∀ge:genv p globals.
619 ident → joint_closed_internal_function p globals →
620  joint_statement p globals → state_pc p →
621  IO io_out io_in (state_pc p) ≝
622  λp,g,ge,curr_id,curr_fn,s,st.
623  match s return λ_.IO ??? with
624  [ sequential s nxt ⇒
625    match s return λ_.IO ??? with
626    [ COND a l ⇒
627      ! v ← acca_retrieve … st a ;
628      ! b ← bool_of_beval … v ;
629      if b then
630        goto … ge l st
631      else
632        return next … nxt st
633    | CALL f args dest ⇒
634      eval_call … ge f args dest nxt st
635    | _ ⇒ return next … nxt st
636    ]
637  | final s ⇒
638    let curr_ret ≝ joint_if_result … curr_fn in
639    match s with
640    [ GOTO l ⇒ goto … ge l st
641    | RETURN ⇒ eval_return … ge curr_id curr_ret st
642    | TAILCALL _ f args ⇒
643      eval_tailcall … ge f args curr_id curr_ret st
644    ]
645  | FCOND _ a lbltrue lblfalse ⇒
646    ! v ← acca_retrieve … st a ;
647    ! b ← bool_of_beval … v ;
648    if b then
649      goto … ge lbltrue st
650    else
651      goto … ge lblfalse st
652  ].
653
654definition eval_state : ∀p:sem_params. ∀globals: list ident.
655  genv p globals →
656  state_pc p → IO io_out io_in (state_pc p) ≝
657  λp,globals,ge,st.
658  ! 〈id,fn,s〉 ← fetch_statement … ge (pc … st) : IO ???;
659  ! st' ← eval_statement_no_pc … ge id s st : IO ???;
660  let st'' ≝ set_no_pc … st' st in
661  eval_statement_advance … ge id fn s st''.
Note: See TracBrowser for help on using the repository browser.