source: src/joint/joint_semantics.ma @ 2645

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