source: src/joint/joint_semantics.ma @ 3259

Last change on this file since 3259 was 3259, checked in by piccolo, 6 years ago

changed ERTL semantics:
1) added manipulation of stack pointer directly in the semantics
2) added values of Callee Saved in frames

File size: 27.1 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])
16  (globals : list ident) : Type[0] ≝
17{ ge :> genv_t (fundef (F globals))
18; find_symbol_in_globals : ∀s.In … globals s → find_symbol … ge s ≠ None ?
19; stack_sizes : ident → option ℕ
20; premain : F globals
21; pc_from_label : (Σbl.block_region bl = Code) → F globals → label →
22    option program_counter
23}.
24
25definition pre_main_id : ident ≝ an_identifier … one.
26
27(* this can replace graph_fetch function and lin_fetch_function *)
28definition fetch_function:
29 ∀F,globals.
30 ∀ge : genv_gen F globals.
31  (Σb.block_region b = Code) →
32  res (ident×(fundef (F globals))) ≝
33 λF,g,ge,bl.
34 if eqZb (block_id bl) (-1) then
35   return 〈pre_main_id, Internal ? (premain … ge)〉
36 else
37   opt_to_res … [MSG BadFunction]
38    (! id ← symbol_for_block … ge bl ;
39     ! fd ← find_funct_ptr … ge bl ;
40     return 〈id, fd〉).
41
42definition fetch_internal_function :
43 ∀F,globals.
44 ∀ge : genv_gen F globals.
45  (Σb.block_region b = Code) →
46  res (ident×(F globals)) ≝
47 λF,g,ge,bl.
48 ! 〈id, fd〉 ← fetch_function … ge bl ;
49 match fd with
50 [ Internal ifd ⇒ return 〈id, ifd〉
51 | _ ⇒ Error … [MSG BadFunction]
52 ].
53
54definition code_block_of_block : block → option (Σb.block_region b = Code) ≝
55λbl.match block_region bl
56  return λx.block_region bl = x → option (Σb.block_region b = Code) with
57  [ Code ⇒ λprf.Some ? «bl, prf»
58  | XData ⇒ λ_.None ?
59  ] (refl …).
60
61definition block_of_funct_id ≝  λF.
62  λge: genv_t F.λid.
63  opt_to_res … [MSG BadFunction; CTX … id] (
64    ! bl ← find_symbol … ge id;
65    code_block_of_block bl).
66
67(* this is equal to pc_of_label defined later, but can be used in
68   generic definitions of mk_sem_unserialised_params *)
69definition gen_pc_from_label :
70  ∀F.∀globals.
71  genv_gen F globals →
72  ident (* current function *) → label → res program_counter ≝
73  λF,g,ge,id,lbl.
74  ! bl ← block_of_funct_id … ge id ;
75  ! 〈ignore, f_def〉 ← fetch_internal_function … ge bl ;
76  opt_to_res … [MSG LabelNotFound ; CTX ? lbl]
77    (pc_from_label … ge bl f_def lbl).
78
79definition genv ≝ λp.genv_gen (joint_closed_internal_function p).
80unification hint 0 ≔ p, globals ⊢
81genv p globals ≡ genv_gen (joint_closed_internal_function p) globals.
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 : ∀globals.∀ge : genv_gen F globals.nat → paramsT … uns_pars → call_args uns_pars → ident →
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_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 off ldest hdest ⇒
470    (* to be changed when globals will be already in stack? *)
471    let addr_block ≝ opt_safe ? (find_symbol … ge id) ? in
472    let 〈laddr,haddr〉 ≝ beval_pair_of_pointer (mk_pointer addr_block (mk_offset off)) in
473    ! st' ← dpl_store … ldest laddr st;
474    dph_store … hdest haddr st'
475  | OP1 op dacc_a sacc_a ⇒
476    ! v ← acca_retrieve … st sacc_a;
477    ! v' ← be_op1 op v ;
478    acca_store … dacc_a v' st
479  | OP2 op dacc_a sacc_a src ⇒
480    ! v1 ← acca_arg_retrieve … st sacc_a;
481    ! v2 ← snd_arg_retrieve … st src;
482    ! 〈v',carry〉 ← be_op2 (carry … st) op v1 v2 ;
483    ! st' ← acca_store … dacc_a v' st;
484    return set_carry … carry st'
485  | CLEAR_CARRY ⇒
486    return set_carry … (BBbit false) st
487  | SET_CARRY ⇒
488    return set_carry … (BBbit true) st
489  | OPACCS op dacc_a_reg dacc_b_reg sacc_a_reg sacc_b_reg ⇒
490    ! v1 ← acca_arg_retrieve … st sacc_a_reg;
491    ! v2 ← accb_arg_retrieve … st sacc_b_reg;
492    ! 〈v1',v2'〉 ← be_opaccs op v1 v2 ;
493    ! st' ← acca_store … dacc_a_reg v1' st;
494    accb_store … dacc_b_reg v2' st'
495  | POP dst ⇒
496    ! 〈v, st'〉 ← pop p st;
497    acca_store … p dst v st'
498  | PUSH src ⇒
499    ! v ← acca_arg_retrieve … st src;
500    push … st v
501  | MOVE dst_src ⇒
502    pair_reg_move … st dst_src
503  | _ ⇒ return st (* for calls do everything in eval_seq_advance *)
504  ].
505  @hide_prf
506  @find_symbol_in_globals
507  lapply prf
508  elim globals [*]
509  #hd #tl #IH #H elim (orb_Prop_true … H) -H
510  [ @deq_elim #H * destruct %1 % | #H %2{(IH … H)} ]
511qed.
512
513definition block_of_call ≝ λp : sem_params.
514  λglobals.λge: genv p globals.
515    λf.λst : state p.
516  ! bl ← match f with
517    [ inl id ⇒
518      !bl ← opt_to_res … [MSG BadFunction; CTX … id] (find_symbol … ge id) ;
519      if eqZb (block_id bl) (-1) then
520        Error … [MSG BadFunction; CTX … id]
521      else return bl
522    | inr addr ⇒
523      ! addr_l ← dpl_arg_retrieve … st (\fst addr) ;
524      ! addr_h ← dph_arg_retrieve … st (\snd addr) ;
525      ! ptr ← pointer_of_bevals … [addr_l ; addr_h ] ;
526      if eq_bv … (bv_zero …) (offv (poff ptr)) ∧
527         (notb (eqZb (block_id (pblock ptr)) (-1))) then
528        return pblock ptr
529      else
530        Error … [MSG BadFunction; MSG BadPointer]
531    ] ;
532  opt_to_res … [MSG BadFunction; MSG BadPointer]
533    (code_block_of_block bl).
534
535lemma match_reg_elim : ∀ A : Type[0]. ∀ P : A → Prop. ∀ r : region.
536∀f : (r = XData) → A. ∀g : (r = Code) → A. (∀ prf : r = XData.P (f prf)) →
537(∀ prf : r = Code.P (g prf)) →
538P ((match r return λx.(r = x → ?) with
539    [XData ⇒ f | Code ⇒ g])(refl ? r)).
540#A #P * #f #g #H1 #H2 normalize nodelta [ @H1 | @H2]
541qed.
542
543lemma block_of_call_no_minus_one : ∀p,globals,ge,f,st,bl.
544block_of_call p globals ge f st = return bl →
545block_id bl ≠ -1.
546#p #globals #ge #f #st #bl whd in match block_of_call; normalize nodelta
547#H cases(bind_inversion ????? H) #bl1 cases f -f normalize nodelta
548[ #id * #H cases(bind_inversion ????? H) -H #bl2 * #_ @eqZb_elim #EQbl2
549  normalize nodelta whd in ⊢ (??%% → ?); #EQ destruct(EQ)
550  #H lapply(opt_eq_from_res ???? H) -H whd in match code_block_of_block;
551  normalize nodelta @match_reg_elim [ #_ #EQ destruct] #prf #EQ destruct(EQ)
552  assumption
553| * #dpl #dph * #H cases(bind_inversion ????? H) -H #bv1 * #_ #H
554  cases(bind_inversion ????? H) -H #bv2 * #_ #H cases(bind_inversion ????? H) -H
555  #ptr * #_ @eq_bv_elim #_ normalize nodelta [2: whd in ⊢ (??%% → ?); #EQ destruct]
556  @eqZb_elim #EQptr normalize nodelta whd in ⊢ (??%% → ?); #EQ destruct
557  #H lapply(opt_eq_from_res ???? H) -H whd in match code_block_of_block;
558  normalize nodelta @match_reg_elim [#_ #EQ destruct] #prf #EQ destruct
559  assumption
560]
561qed.
562
563
564definition eval_external_call ≝
565λp : sem_params.λfn,args,dest,st.
566      ! params ← fetch_external_args … p fn st args : IO ???;
567      ! evargs ← check_eventval_list params (sig_args (ef_sig fn)) : IO ???;
568      ! evres ← do_io (ef_id fn) evargs (proj_sig_res (ef_sig fn));
569      (* CSC: XXX bug here; I think I should split it into Byte-long
570         components; instead I am making a singleton out of it. To be
571         fixed once we fully implement external functions. *)
572      let vs ≝ [mk_val ? evres] in
573      set_result … p vs dest st.
574
575definition increment_stack_usage : ∀p.ℕ → state p → state p ≝
576 λp,n,st.mk_state p (st_frms … st) (istack … st) (carry … st) (regs … st) (m … st)
577  (n + stack_usage … st).
578
579definition decrement_stack_usage : ∀p.ℕ → state p → state p ≝
580 λp,n,st.mk_state p (st_frms … st) (istack … st) (carry … st) (regs … st) (m … st)
581  (stack_usage … st - n).
582
583definition eval_internal_call ≝
584λp : sem_params.λglobals : list ident.λge : genv p globals.λi,fn,args.
585λst : state p.
586! stack_size ← opt_to_res … [MSG MissingStackSize; CTX … i] (stack_sizes … ge i) ;
587! st' ← setup_call … ge … stack_size (joint_if_params … globals fn) args i st ;
588return increment_stack_usage … stack_size st'.
589
590definition is_inl : ∀A,B.A+B → bool ≝ λA,B,x.match x with [ inl _ ⇒ true | _ ⇒ false ].
591
592definition eval_call ≝
593λp : sem_params.λglobals : list ident.λge : genv p globals.λf,args,dest,nxt.
594λst : state_pc p.
595! bl ← block_of_call … ge f st : IO ???;
596! 〈i, fd〉 ← fetch_function … ge bl : IO ???;
597match fd with
598[ Internal ifd ⇒
599  ! st' ← save_frame … (kind_of_call … f) dest st ;
600  ! st'' ← eval_internal_call p globals ge i ifd args st' ;
601  let pc ≝ pc_of_point p bl (joint_if_entry … ifd) in
602  return mk_state_pc … st'' pc (last_pop … st)
603| External efd ⇒
604  ! st' ← eval_external_call … efd args dest st ;
605  return mk_state_pc … st' (succ_pc p (pc … st) nxt) (last_pop … st)
606].
607
608definition eval_statement_no_pc :
609 ∀p:sem_params.∀globals.∀ge:genv p globals.
610 ident (* current *) →
611 joint_statement p globals → state p → res (state p) ≝
612 λp,globals,ge,curr_id,s,st.
613  match s with
614  [ sequential s next ⇒
615    match s with
616    [ step_seq s ⇒ eval_seq_no_pc … ge curr_id s st
617    | _ ⇒ return st
618    ]
619  | _ ⇒ return st
620  ].
621
622definition eval_return ≝
623λp : sem_params.λglobals : list ident.λge : genv p globals.
624λcurr_id.λcurr_ret : call_dest p.
625λst : state p.
626! stack_size ← opt_to_res … [MSG MissingStackSize; CTX … curr_id] (stack_sizes … ge curr_id) ;
627! 〈st', call_pc〉 ← pop_frame … ge curr_id curr_ret st ;
628! nxt ← next_of_call_pc … ge call_pc ;
629let st'' ≝ set_last_pop … (decrement_stack_usage … stack_size st') call_pc in
630return
631  next ? nxt st'' (* now address pushed on stack are calling ones! *).
632
633definition eval_tailcall ≝
634λp : sem_params.λglobals : list ident.λge : genv p globals.λf,args,curr_f.
635λcurr_ret : call_dest p.
636λst : state_pc p.
637! bl ← block_of_call … ge f st : IO ???;
638! 〈i, fd〉 ← fetch_function … ge bl : IO ???;
639match fd with
640[ Internal ifd ⇒
641  ! stack_size ← opt_to_res … [MSG MissingStackSize; CTX … curr_f] (stack_sizes … ge curr_f) ;
642  let st' ≝ decrement_stack_usage … stack_size st in
643  ! st'' ← eval_internal_call p globals ge i ifd args st' ;
644  let pc ≝ pc_of_point p bl (joint_if_entry … ifd) in
645  return mk_state_pc … st'' pc (last_pop … st)
646| External efd ⇒
647  ! st' ← eval_external_call … efd args curr_ret st ;
648  eval_return … ge curr_f curr_ret st
649].
650
651definition eval_statement_advance :
652 ∀p:sem_params.∀globals.∀ge:genv p globals.
653 ident → joint_closed_internal_function p globals →
654  joint_statement p globals → state_pc p →
655  IO io_out io_in (state_pc p) ≝
656  λp,g,ge,curr_id,curr_fn,s,st.
657  match s return λ_.IO ??? with
658  [ sequential s nxt ⇒
659    match s return λ_.IO ??? with
660    [ COND a l ⇒
661      ! v ← acca_retrieve … st a ;
662      ! b ← bool_of_beval … v ;
663      if b then
664        goto … ge l st
665      else
666        return next … nxt st
667    | CALL f args dest ⇒
668      eval_call … ge f args dest nxt st
669    | _ ⇒ return next … nxt st
670    ]
671  | final s ⇒
672    let curr_ret ≝ joint_if_result … curr_fn in
673    match s with
674    [ GOTO l ⇒ goto … ge l st
675    | RETURN ⇒ eval_return … ge curr_id curr_ret st
676    | TAILCALL _ f args ⇒
677      eval_tailcall … ge f args curr_id curr_ret st
678    ]
679  | FCOND _ a lbltrue lblfalse ⇒
680    ! v ← acca_retrieve … st a ;
681    ! b ← bool_of_beval … v ;
682    if b then
683      goto … ge lbltrue st
684    else
685      goto … ge lblfalse st
686  ].
687
688definition eval_state : ∀p:sem_params. ∀globals: list ident.
689  genv p globals →
690  state_pc p → IO io_out io_in (state_pc p) ≝
691  λp,globals,ge,st.
692  ! 〈id,fn,s〉 ← fetch_statement … ge (pc … st) : IO ???;
693  ! st' ← eval_statement_no_pc … ge id s st : IO ???;
694  let st'' ≝ set_no_pc … st' st in
695  eval_statement_advance … ge id fn s st''.
Note: See TracBrowser for help on using the repository browser.