source: src/joint/joint_semantics.ma

Last change on this file was 3265, checked in by tranquil, 6 years ago

added validate_pointer filter
in Interference added that intereference only fires on non eliminable
statements

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