source: src/joint/joint_semantics.ma @ 2601

Last change on this file since 2601 was 2601, checked in by sacerdot, 8 years ago

Extraction to ocaml is now working, with a couple of bugs left.
One limitation is that it is not possible to have two files with the
same name in different directories. Therefore this commit renames files
to avoid this situation.

The extracted directory contains:

  1. a snapshot of the .ml(i) files extracted from CerCo? by running ocamlc.opt -extract_ocaml compiler.ma The files have been patched by hand to implement all strings and fix the bugs.
  2. a file PROBLEMS that describes the remaining problems, i.e. bugs and axioms to be implemented

To obtain the compiler, run ocamlbuild compiler.byte.
At the moment it fails because of the three remaining axioms.

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 : Pos →  program_counter ≝ λpos.
80    mk_program_counter «mk_block Code OZ, refl …» pos.
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
220(*
221definition allocate_locals :
222  ∀p,F.∀sup : sem_unserialized_params p F.
223  list (localsT p) → state sup → state sup ≝
224  λp,F,sup,l,st.
225  let r ≝ foldr … (allocate_locals_ … sup) (regs … st) l in
226  set_regs … r st. *)
227
228definition helper_def_retrieve :
229  ∀X : ? → ? → ? → Type[0].
230  (∀up,F.∀p:sem_unserialized_params up F. regsT (st_pars up F p) → X up F p → res beval) →
231  ∀up,F.∀p : sem_unserialized_params up F.state (st_pars up F p) → X up F p → res beval ≝
232    λX,f,up,F,p,st.f ?? p (regs … st).
233
234definition helper_def_store :
235  ∀X : ? → ? → ? → Type[0].
236  (∀up,F.∀p : sem_unserialized_params up F.X up F p → beval → regsT (st_pars … p) → res (regsT (st_pars … p))) →
237  ∀up,F.∀p : sem_unserialized_params up F.X up F p → beval → state (st_pars … p) → res (state (st_pars … p)) ≝
238  λX,f,up,F,p,x,v,st.! r ← f ?? p x v (regs … st) ; return set_regs … r st.
239
240definition acca_retrieve ≝ helper_def_retrieve ? acca_retrieve_.
241definition acca_store ≝ helper_def_store ? acca_store_.
242definition acca_arg_retrieve ≝ helper_def_retrieve ? acca_arg_retrieve_.
243definition accb_store ≝ helper_def_store ? accb_store_.
244definition accb_retrieve ≝ helper_def_retrieve ? accb_retrieve_.
245definition accb_arg_retrieve ≝ helper_def_retrieve ? accb_arg_retrieve_.
246definition dpl_store ≝ helper_def_store ? dpl_store_.
247definition dpl_retrieve ≝ helper_def_retrieve ? dpl_retrieve_.
248definition dpl_arg_retrieve ≝ helper_def_retrieve ? dpl_arg_retrieve_.
249definition dph_store ≝ helper_def_store ? dph_store_.
250definition dph_retrieve ≝ helper_def_retrieve ? dph_retrieve_.
251definition dph_arg_retrieve ≝ helper_def_retrieve ? dph_arg_retrieve_.
252definition snd_arg_retrieve ≝ helper_def_retrieve ? snd_arg_retrieve_.
253definition pair_reg_move ≝
254  λup,F.λp : sem_unserialized_params up F.λst : state (st_pars … p).λpm : pair_move up.
255    ! r ← pair_reg_move_ ?? p (regs ? st) pm;
256    return set_regs ? r st.
257 
258axiom FailedStore: String.
259
260definition push: ∀p.state p → beval → res (state p) ≝
261 λp,st,v.
262 ! is ← is_push (istack … st) v ;
263 return set_istack … is st.
264
265definition pop: ∀p. state p → res (beval × (state p)) ≝
266 λp,st.
267 ! 〈bv, is〉 ← is_pop (istack … st) ;
268 return 〈bv, set_istack … is st〉.
269
270definition push_ra : ∀p. state p → program_counter → res (state p) ≝
271 λp,st,l.
272  let 〈addrl,addrh〉 ≝  beval_pair_of_pc l in
273  ! st' ← push … st addrl;
274  push … st' addrh.
275
276definition pop_ra : ∀p.state p → res (state p × program_counter) ≝
277 λp,st.
278  ! 〈addrh, st'〉 ← pop … st;
279  ! 〈addrl, st''〉 ← pop … st';
280  ! pr ← pc_of_bevals [addrh; addrl];
281  return 〈st'',pr〉.
282
283(* parameters that are defined by serialization *)
284record sem_params : Type[1] ≝
285  { spp :> params
286  ; msu_pars :> sem_unserialized_params spp (joint_closed_internal_function spp)
287  ; offset_of_point : code_point spp → Pos
288  ; point_of_offset : Pos → code_point spp
289  ; point_of_offset_of_point :
290    ∀pt.point_of_offset (offset_of_point pt) = pt
291  ; offset_of_point_of_offset :
292    ∀o.offset_of_point (point_of_offset o) = o
293  }.
294
295(*
296coercion ms_pars_to_msu_pars nocomposites :
297∀p : params.∀msp : more_sem_params p.more_sem_unserialized_params p (λglobals.joint_internal_function globals p)
298 ≝ msu_pars
299on _msp : more_sem_params ? to more_sem_unserialized_params ??.
300
301definition ss_pars_of_ms_pars ≝
302  λp.λpp : more_sem_params p.
303  st_pars … (msu_pars … pp).
304coercion ms_pars_to_ss_pars nocomposites :
305∀p : params.∀msp : more_sem_params p.sem_state_params ≝
306ss_pars_of_ms_pars on _msp : more_sem_params ? to sem_state_params.*)
307
308definition pc_of_point : ∀p:sem_params.(Σb.block_region b = Code) →
309  code_point p → program_counter ≝
310  λp,bl,pt.
311  mk_program_counter bl (offset_of_point p pt).
312
313definition point_of_pc :
314  ∀p:sem_params.program_counter → code_point p ≝
315  λp,ptr.point_of_offset p (pc_offset ptr).
316
317lemma point_of_pc_of_point :
318  ∀p,bl,pt.
319  point_of_pc p (pc_of_point p bl pt) = pt.
320#p #bl #pt normalize // qed.
321
322lemma pc_of_point_of_pc :
323  ∀p,ptr.
324    pc_of_point p (pc_block ptr) (point_of_pc p ptr) = ptr.
325#p * #bl #off normalize >offset_of_point_of_offset % qed.
326
327definition fetch_statement: ∀p : sem_params.∀globals.
328  ∀ge : genv_t (joint_function p globals). program_counter →
329  res (ident × (joint_closed_internal_function p globals) × (joint_statement p globals)) ≝
330  λp,globals,ge,ptr.
331  ! 〈id, fn〉 ← fetch_internal_function … ge (pc_block ptr) ;
332  let pt ≝ point_of_pc p ptr in
333  ! stmt ← opt_to_res … (msg ProgramCounterOutOfCode) (stmt_at … (joint_if_code … fn) pt);
334  return 〈id, fn, stmt〉.
335
336definition pc_of_label : ∀p : sem_params.∀globals.
337  genv_t (joint_function p globals) → (Σb.block_region b = Code) → label → res program_counter ≝
338  λp,globals,ge,bl,lbl.
339  ! 〈i, fn〉 ← fetch_internal_function … ge bl ;
340  ! pt ← opt_to_res … [MSG LabelNotFound ; CTX ? lbl]
341            (point_of_label … (joint_if_code … fn) lbl) ;
342  return mk_program_counter bl (offset_of_point p pt).
343
344definition succ_pc : ∀p : sem_params.
345  program_counter → succ p → program_counter ≝
346  λp,ptr,nxt.
347  let curr ≝ point_of_pc p ptr in
348  pc_of_point p (pc_block ptr) (point_of_succ p curr nxt).
349
350(*
351record sem_params : Type[1] ≝
352  { spp :> params
353  ; more_sem_pars :> more_sem_params spp
354  }.
355*)
356(* definition msu_pars_of_s_pars :
357∀p : sem_params.more_sem_unserialized_params (spp p) (λglobals.joint_internal_function globals (spp p))
358≝ λp : sem_params.
359  msu_pars … (more_sem_pars p).
360coercion s_pars_to_msu_pars nocomposites :
361∀p : sem_params.more_sem_unserialized_params (spp p) (λglobals.joint_internal_function globals (spp p)) ≝
362msu_pars_of_s_pars
363on p : sem_params to more_sem_unserialized_params ??.
364
365definition ss_pars_of_s_pars :
366∀p : sem_params.sem_state_params
367≝ λp : sem_params.
368  st_pars … (msu_pars … (more_sem_pars p)).
369coercion s_pars_to_ss_pars nocomposites :
370∀p : sem_params.sem_state_params ≝
371ss_pars_of_s_pars
372on _p : sem_params to sem_state_params.
373
374definition ms_pars_of_s_pars :
375∀p : sem_params.more_sem_params (spp p)
376≝ more_sem_pars.
377coercion s_pars_to_ms_pars nocomposites :
378∀p : sem_params.more_sem_params (spp p) ≝
379ms_pars_of_s_pars
380on p : sem_params to more_sem_params ?.*)
381
382(* definition address_of_label: ∀globals. ∀p:sem_params.
383  genv globals p → pointer → label → res address ≝
384 λglobals,p,ge,ptr,l.
385  do newptr ← pointer_of_label … p ? ge … ptr l ;
386  OK … (address_of_code_pointer newptr). *)
387
388definition goto: ∀p : sem_params.∀globals.
389  genv_t (joint_function p globals) → label → state_pc p → res (state_pc p) ≝
390 λp,globals,ge,l,st.
391  ! newpc ← pc_of_label … ge (pc_block (pc … st)) l ;
392  return set_pc … newpc st.
393
394(*
395definition empty_state: ∀p. more_sem_params p → state p ≝
396 mk_state … (empty_framesT …)
397*)
398
399definition next : ∀p : sem_params.succ p → state_pc p → state_pc p ≝
400 λp,l,st.
401 let newpc ≝ succ_pc … (pc … st) l in
402 set_pc … newpc st.
403
404axiom NoSuccessor : String.
405definition next_of_call_pc : ∀p : sem_params.∀globals.genv_t (joint_function p globals) →
406  program_counter → res (succ p) ≝
407λp,globals,ge,pc.
408  ! 〈id_fn, stmt〉 ← fetch_statement … ge pc ;
409  match stmt with
410  [ sequential s nxt ⇒
411    match s with
412    [ CALL _ _ _ ⇒ return nxt
413    | _ ⇒ Error … [MSG NoSuccessor]
414    ]
415  | _ ⇒ Error … [MSG NoSuccessor]
416  ].
417
418definition eval_seq_no_pc :
419 ∀p:sem_params.∀globals.∀ge:genv p globals.ident →
420 joint_closed_internal_function p globals →
421  joint_seq p globals → state p →
422  res (state p) ≝
423 λp,globals,ge,curr_id,curr_fn,seq,st.
424 match seq with
425  [ extension_seq c ⇒
426    eval_ext_seq … ge c curr_id curr_fn st
427  | LOAD dst addrl addrh ⇒
428    ! vaddrh ← dph_arg_retrieve … st addrh ;
429    ! vaddrl ← dpl_arg_retrieve … st addrl;
430    ! vaddr ← pointer_of_address 〈vaddrl,vaddrh〉;
431    ! v ← opt_to_res … (msg FailedLoad) (beloadv (m … st) vaddr);
432    acca_store p … dst v st
433 | STORE addrl addrh src ⇒
434    ! vaddrh ← dph_arg_retrieve … st addrh;
435    ! vaddrl ← dpl_arg_retrieve … st addrl;
436    ! vaddr ← pointer_of_address 〈vaddrl,vaddrh〉;
437    ! v ← acca_arg_retrieve … st src;
438    ! m' ← opt_to_res … (msg FailedStore) (bestorev (m … st) vaddr v);
439    return set_m … m' st
440  | ADDRESS id prf ldest hdest ⇒
441    let addr_block ≝ opt_safe ? (find_symbol … ge id) ? in
442    let 〈laddr,haddr〉 ≝ beval_pair_of_pointer (mk_pointer addr_block zero_offset) in
443    ! st' ← dpl_store … ldest laddr st;
444    dph_store … hdest haddr st'
445  | OP1 op dacc_a sacc_a ⇒
446    ! v ← acca_retrieve … st sacc_a;
447    ! v' ← be_op1 op v ;
448    acca_store … dacc_a v' st
449  | OP2 op dacc_a sacc_a src ⇒
450    ! v1 ← acca_arg_retrieve … st sacc_a;
451    ! v2 ← snd_arg_retrieve … st src;
452    ! 〈v',carry〉 ← be_op2 (carry … st) op v1 v2 ;
453    ! st' ← acca_store … dacc_a v' st;
454    return set_carry … carry st'
455  | CLEAR_CARRY ⇒
456    return set_carry … (BBbit false) st
457  | SET_CARRY ⇒
458    return set_carry … (BBbit true) st
459  | OPACCS op dacc_a_reg dacc_b_reg sacc_a_reg sacc_b_reg ⇒
460    ! v1 ← acca_arg_retrieve … st sacc_a_reg;
461    ! v2 ← accb_arg_retrieve … st sacc_b_reg;
462    ! 〈v1',v2'〉 ← be_opaccs op v1 v2 ;
463    ! st' ← acca_store … dacc_a_reg v1' st;
464    accb_store … dacc_b_reg v2' st'
465  | POP dst ⇒
466    ! 〈v, st'〉 ← pop p st;
467    acca_store … p dst v st'
468  | PUSH src ⇒
469    ! v ← acca_arg_retrieve … st src;
470    push … st v
471  | MOVE dst_src ⇒
472    pair_reg_move … st dst_src
473  | _ ⇒ return st (* for calls do everything in eval_seq_advance *)
474  ].
475  @hide_prf
476  @find_symbol_in_globals
477  lapply prf
478  elim globals [*]
479  #hd #tl #IH #H elim (orb_Prop_true … H) -H
480  [@eq_identifier_elim #H * >H %1 % ]
481  #G %2 @IH @G
482qed.
483
484definition code_block_of_block : block → option (Σb.block_region b = Code) ≝
485λbl.match block_region bl
486  return λx.block_region bl = x → option (Σb.block_region b = Code) with
487  [ Code ⇒ λprf.Some ? «bl, prf»
488  | XData ⇒ λ_.None ?
489  ] (refl …).
490
491definition block_of_funct_id ≝  λF.λsp:sem_state_params.
492  λge: genv_t F.λid.
493  opt_to_res … [MSG BadFunction; CTX … id] (
494    ! bl ← find_symbol … ge id;
495    code_block_of_block bl).
496 
497definition block_of_call ≝ λp : sem_params.
498  λglobals.λge: genv_t (joint_function p globals).λf.λst : state p.
499  ! bl ← match f with
500    [ inl id ⇒
501      opt_to_res … [MSG BadFunction; CTX … id]
502        (find_symbol … ge id)
503    | inr addr ⇒
504      ! addr_l ← dpl_arg_retrieve … st (\fst addr) ;
505      ! addr_h ← dph_arg_retrieve … st (\snd addr) ;
506      ! ptr ← pointer_of_bevals … [addr_l ; addr_h ] ;
507      if eq_bv … (bv_zero …) (offv (poff ptr)) then
508        return pblock ptr
509      else
510        Error … [MSG BadFunction; MSG BadPointer]
511    ] ;
512  opt_to_res … [MSG BadFunction; MSG BadPointer]
513    (code_block_of_block bl).
514
515definition eval_external_call ≝
516λp : sem_params.λfn,args,dest,st.
517      ! params ← fetch_external_args … p fn st args : IO ???;
518      ! evargs ← check_eventval_list params (sig_args (ef_sig fn)) : IO ???;
519      ! evres ← do_io (ef_id fn) evargs (proj_sig_res (ef_sig fn));
520      (* CSC: XXX bug here; I think I should split it into Byte-long
521         components; instead I am making a singleton out of it. To be
522         fixed once we fully implement external functions. *)
523      let vs ≝ [mk_val ? evres] in
524      set_result … p vs dest st.
525
526axiom MissingStackSize : String.
527
528definition eval_internal_call ≝
529λp : sem_params.λglobals : list ident.λge : genv p globals.λi,fn,args.
530λst : state p.
531! stack_size ← opt_to_res … [MSG MissingStackSize; CTX … i] (stack_sizes … ge i) ;
532setup_call … stack_size (joint_if_params … globals fn) args st.
533
534definition is_inl : ∀A,B.A+B → bool ≝ λA,B,x.match x with [ inl _ ⇒ true | _ ⇒ false ].
535
536
537definition eval_call ≝
538λp : sem_params.λglobals : list ident.λge : genv p globals.λf,args,dest,nxt.
539λst : state_pc p.
540! bl ← block_of_call … ge f st : IO ???;
541! 〈i, fd〉 ← fetch_function … ge bl : IO ???;
542match fd with
543[ Internal ifd ⇒
544  let ident ≝ ? in
545  ! st' ← save_frame … (kind_of_call … f) dest ident st ;
546  ! st'' ← eval_internal_call p globals ge i ifd args st' ;
547  let pc ≝ pc_of_point p bl (joint_if_entry … ifd) in
548  return mk_state_pc … st'' pc (last_pop … st)
549| External efd ⇒
550  ! st' ← eval_external_call … efd args dest st ;
551  return mk_state_pc … st' (succ_pc p (pc … st) nxt) (last_pop … st)
552]. cases daemon qed. (*TODO*)
553
554definition eval_statement_no_pc :
555 ∀p:sem_params.∀globals.∀ge:genv p globals.
556 ident → joint_closed_internal_function p globals (* current *) →
557 joint_statement p globals → state p → res (state p) ≝
558 λp,globals,ge,curr_id,curr_fn,s,st.
559  match s with
560  [ sequential s next ⇒
561    match s with
562    [ step_seq s ⇒ eval_seq_no_pc … ge curr_id curr_fn s st
563    | _ ⇒ return st
564    ]
565  | _ ⇒ return st
566  ].
567
568definition eval_return ≝
569λp : sem_params.λglobals : list ident.λge : genv p globals.
570λcurr_id.λcurr_fn : joint_closed_internal_function ??.
571λst : state p.
572! st' ← pop_frame … ge curr_id curr_fn st ;
573! nxt ← next_of_call_pc … ge (\snd … st') ;
574return
575  next … nxt (set_last_pop … (\snd … st') st') (* now address pushed on stack are calling ones! *).
576
577definition eval_tailcall ≝
578λp : sem_params.λglobals : list ident.λge : genv p globals.λf,args,curr_f.
579λcurr_fn : joint_closed_internal_function ??.
580λst : state_pc p.
581! bl ← block_of_call … ge f st : IO ???;
582! 〈i, fd〉 ← fetch_function … ge bl : IO ???;
583match fd with
584[ Internal ifd ⇒
585  ! st' ← eval_internal_call p globals ge i ifd args st ;
586  let pc ≝ pc_of_point p bl (joint_if_entry … ifd) in
587  return mk_state_pc … st' pc (last_pop … st)
588| External efd ⇒
589  let curr_dest ≝ joint_if_result ?? curr_fn in
590  ! st' ← eval_external_call … efd args curr_dest st ;
591  eval_return … ge curr_f curr_fn st
592].
593
594definition eval_statement_advance :
595 ∀p:sem_params.∀globals.∀ge:genv p globals.
596 ident → joint_closed_internal_function p globals →
597  joint_statement p globals → state_pc p →
598  IO io_out io_in (state_pc p) ≝
599  λp,g,ge,curr_id,curr_fn,s,st.
600  match s return λ_.IO ??? with
601  [ sequential s nxt ⇒
602    match s return λ_.IO ??? with
603    [ step_seq s ⇒ return next … nxt st
604    | COND a l ⇒
605      ! v ← acca_retrieve … st a ;
606      ! b ← bool_of_beval … v ;
607      if b then
608        goto … ge l st
609      else
610        return next … nxt st
611    | CALL f args dest ⇒
612      eval_call … ge f args dest nxt st
613    ]
614  | final s ⇒
615    match s with
616    [ GOTO l ⇒ goto … ge l st
617    | RETURN ⇒ eval_return … ge curr_id curr_fn st
618    | TAILCALL _ f args ⇒
619      eval_tailcall … ge f args curr_id curr_fn st
620    ]
621  | FCOND _ a lbltrue lblfalse ⇒
622    ! v ← acca_retrieve … st a ;
623    ! b ← bool_of_beval … v ;
624    if b then
625      goto … ge lbltrue st
626    else
627      goto … ge lblfalse st
628  ].
629
630definition eval_state : ∀p:sem_params. ∀globals: list ident.
631  genv p globals →
632  state_pc p → IO io_out io_in (state_pc p) ≝
633  λp,globals,ge,st.
634  ! 〈id,fn,s〉 ← fetch_statement … ge (pc … st) : IO ???;
635  ! st' ← eval_statement_no_pc … ge id fn s st : IO ???;
636  let st'' ≝ set_no_pc … st' st in
637  eval_statement_advance … ge id fn s st''.
638
639(* Paolo: what if in an intermediate language main finishes with an external
640  tailcall? Maybe it should rely on an FEnd flow command issued, but that's
641  not static... *)
642definition is_final: ∀p: sem_params.∀globals.
643  genv p globals → program_counter → state_pc p → option int ≝
644 λp,globals,ge,exit,st.res_to_opt ? (
645  do 〈id,fn,s〉 ← fetch_statement  … ge (pc … st);
646  match s with
647  [ final s' ⇒
648    match s' with
649    [ RETURN ⇒
650      do st' ← pop_frame … ge id fn st;
651      if eq_program_counter (\snd … st') exit then
652      do vals ← read_result … ge (joint_if_result … fn) st ;
653        Word_of_list_beval vals
654      else
655        Error ? [ ]
656   | _ ⇒ Error ? [ ]
657   ]
658 | _ ⇒ Error ? [ ]
659 ]).
660
661(*
662record evaluation_parameters : Type[1] ≝
663 { globals: list ident
664 ; sparams:> sem_params
665 ; exit: program_counter
666 ; genv2: genv globals sparams
667 }.
668
669(* Paolo: with structured traces, eval need not emit labels. However, this
670  changes trans_system. For now, just putting a dummy thing for
671  the transition. *)
672definition joint_exec: trans_system io_out io_in ≝
673  mk_trans_system … evaluation_parameters (λG. state_pc G)
674   (λG.is_final (globals G) G (genv2 G) (exit G))
675   (λG,st.! 〈flag,st'〉 ← eval_state_flag (globals G) G (genv2 G) st ; return 〈E0, st'〉).
676
677definition make_global :
678 ∀pars: sem_params.
679  joint_program pars → evaluation_parameters
680
681 λpars.
682 (* Invariant: a -1 block is unused in common/Globalenvs *)
683 let b ≝ mk_block Code (-1) in
684 let ptr ≝ mk_pointer Code b ? (mk_offset 0) in
685  (λp. mk_evaluation_parameters
686    (prog_var_names … p)
687    (mk_sem_params … pars)
688    ptr
689    (globalenv_noinit … p)
690  ).
691% qed.
692
693axiom ExternalMain: String.
694
695definition make_initial_state :
696 ∀pars: sem_params.
697 ∀p: joint_program … pars. res (state_pc pars) ≝
698λpars,p.
699  let sem_globals ≝ make_global pars p in
700  let ge ≝ genv2 sem_globals in
701  let m ≝ alloc_mem … p in
702  let 〈m,spb〉 ≝ alloc … m 0 external_ram_size XData in
703  let 〈m,ispb〉 ≝ alloc … m 0 internal_ram_size XData in
704  let dummy_pc ≝ mk_pointer Code (mk_block Code (-1)) ? (mk_offset 0) in
705  let spp ≝ mk_pointer XData spb ? (mk_offset external_ram_size) in
706  let ispp ≝ mk_pointer XData ispb ? (mk_offset 47) in
707  let main ≝ prog_main … p in
708  let st0 ≝ mk_state pars (empty_framesT …) spp ispp BVfalse (empty_regsT … spp) m in
709  (* use exit sem_globals as ra and call_dest_for_main as dest *)
710  let st0' ≝ set_frms ? (save_frame … (exit sem_globals) (call_dest_for_main … pars) st0) st0 in
711  let st_pc0 ≝ mk_state_pc ? st0' dummy_pc in
712  ! main_block ← opt_to_res … [MSG MissingSymbol; CTX ? main] (find_symbol … ge main) ;
713  ! main_fd ← opt_to_res ? [MSG BadPointer] (find_funct_ptr … ge main_block) ;
714  match main_fd with
715  [ Internal fn ⇒
716    do_call ?? ge st_pc0 (block_id main_block) fn (call_args_for_main … pars)
717  | External _ ⇒ Error … [MSG ExternalMain] (* External main not supported: why? *)
718  ]. [5: cases ispb * |6: cases spb * ] (* without try it fails! *) try //
719qed.
720
721definition joint_fullexec :
722 ∀pars:sem_params.fullexec io_out io_in ≝
723 λpars.mk_fullexec ??? joint_exec (make_global pars) (make_initial_state pars).
724*)
Note: See TracBrowser for help on using the repository browser.