source: src/joint/semantics.ma @ 2590

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

added monad machineary for ERTL to ERTLptr translation
eval_seq_no_pc case in place in ERTLptr translation

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