source: src/joint/semantics.ma @ 2570

Last change on this file since 2570 was 2570, checked in by piccolo, 7 years ago

ERTLtoERTLptr in place

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