source: src/joint/semantics_paolo.ma @ 1949

Last change on this file since 1949 was 1949, checked in by tranquil, 8 years ago
  • lemma trace rel to eq flatten trace
  • some more properties of generic monad relations and predicates
  • removed 'iff notation from extralib as already there
File size: 25.0 KB
RevLine 
[1640]1include "basics/lists/list.ma".
2include "joint/BEGlobalenvs.ma".
3include "common/IO.ma".
4include "common/SmallstepExec.ma".
5include "joint/Joint_paolo.ma".
6include "ASM/I8051bis.ma".
7
8(* CSC: external functions never fail (??) and always return something of the
9   size of one register, both in the frontend and in the backend.
10   Is this reasonable??? In OCaml it always return a list, but in the frontend
11   only the head is kept (or Undef if the list is empty) ??? *)
12
13definition genv ≝ λglobals.λp:params. genv_t Genv (joint_function globals p).
[1882]14definition cpointer ≝ Σp.ptype p = Code.
15definition xpointer ≝ Σp.ptype p = XData.
16unification hint 0 ≔ ⊢ cpointer ≡ Sig pointer (λp.ptype p = Code).
17unification hint 0 ≔ ⊢ xpointer ≡ Sig pointer (λp.ptype p = XData).
[1640]18
19record sem_state_params : Type[1] ≝
[1641]20 { framesT: Type[0]
[1640]21 ; empty_framesT: framesT
[1641]22 ; regsT : Type[0]
[1882]23 ; empty_regsT: xpointer → regsT (* Stack pointer *)
[1640]24 }.
25 
26record state (semp: sem_state_params): Type[0] ≝
27 { st_frms: framesT semp
[1882]28 ; sp: xpointer
29 ; isp: xpointer
[1640]30 ; carry: beval
31 ; regs: regsT semp
32 ; m: bemem
33 }.
[1882]34
35record state_pc (semp : sem_state_params) : Type[0] ≝
36  { st_no_pc :> state semp
37  ; pc : cpointer
38  }.
39
[1640]40definition set_m: ∀p. bemem → state p → state p ≝
[1882]41 λp,m,st. mk_state p (st_frms ?…st) (sp … st) (isp … st) (carry … st) (regs … st) m.
[1640]42
43definition set_regs: ∀p:sem_state_params. regsT p → state p → state p ≝
[1882]44 λp,regs,st. mk_state p (st_frms … st) (sp … st) (isp … st) (carry … st) regs (m … st).
[1640]45
[1882]46definition set_sp: ∀p. ? → state p → state p ≝
47 λp,sp,st. mk_state … (st_frms … st) sp (isp … st) (carry … st) (regs … st) (m … st).
[1640]48
[1882]49definition set_isp: ∀p. ? → state p → state p ≝
50 λp,isp,st. mk_state … (st_frms … st) (sp … st) isp (carry … st) (regs … st) (m … st).
[1640]51
52definition set_carry: ∀p. beval → state p → state p ≝
[1882]53 λp,carry,st. mk_state … (st_frms … st) (sp … st) (isp … st) carry (regs … st) (m … st).
[1640]54
[1882]55definition set_pc: ∀p. ? → state_pc p → state_pc p ≝
56 λp,pc,st. mk_state_pc … (st_no_pc … st) pc.
[1640]57
[1882]58definition set_no_pc: ∀p. ? → state_pc p → state_pc p ≝
59 λp,s,st. mk_state_pc … s (pc … st).
60
[1640]61definition set_frms: ∀p:sem_state_params. framesT p → state p → state p ≝
[1882]62 λp,frms,st. mk_state … frms (sp … st) (isp … st) (carry … st) (regs … st) (m … st).
[1640]63
[1641]64axiom BadProgramCounter : String.
[1949]65
66definition function_of_block :
[1641]67 ∀pars : params.
68 ∀globals.
69  genv globals pars →
[1949]70  block →
[1641]71  res (joint_internal_function … pars) ≝
[1949]72  λpars,blobals,ge,b.
[1641]73  do def ← opt_to_res ? [MSG BadProgramCounter] (find_funct_ptr … ge b) ;
74  match def with
75  [ Internal def' ⇒ OK … def'
76  | External _ ⇒ Error … [MSG BadProgramCounter]].
[1949]77 
78(* this can replace graph_fetch function and lin_fetch_function *)
79definition fetch_function:
80 ∀pars : params.
81 ∀globals.
82  genv globals pars →
83  cpointer →
84  res (joint_internal_function … pars) ≝
85 λpars,globals,ge,p.function_of_block pars globals ge (pblock p).
[1882]86
[1949]87inductive step_flow (p : params) (globals : list ident) (labels : list label) : Type[0] ≝
88  | Redirect : (Σl.In ? labels l) → step_flow p globals labels (* used for goto-like flow alteration *)
89  | Init     : Z → joint_internal_function globals p → call_args p → call_dest p → step_flow p globals labels (* call a function with given id, then proceed *)
90  | Proceed  : step_flow p globals labels. (* go to implicit successor *)
[1882]91
[1949]92inductive fin_step_flow (p : params) (globals : list ident) (labels : list label): Type[0] ≝
93  | FRedirect : (Σl.In ? labels l) → fin_step_flow p globals labels
94  | FTailInit : Z → joint_internal_function globals p → call_args p → fin_step_flow p globals labels
95  | FEnd  : fin_step_flow p globals labels. (* end flow *)
[1882]96
[1640]97record more_sem_unserialized_params (uns_pars : unserialized_params) : Type[1] ≝
98  { st_pars :> sem_state_params
99  ; acca_store_ : acc_a_reg uns_pars → beval → regsT st_pars → res (regsT st_pars)
100  ; acca_retrieve_ : regsT st_pars → acc_a_reg uns_pars → res beval
101  ; acca_arg_retrieve_ : regsT st_pars → acc_a_arg uns_pars → res beval
102  ; accb_store_ : acc_b_reg uns_pars → beval → regsT st_pars → res (regsT st_pars)
103  ; accb_retrieve_ : regsT st_pars → acc_b_reg uns_pars → res beval
104  ; accb_arg_retrieve_ : regsT st_pars → acc_b_arg uns_pars → res beval
105  ; dpl_store_ : dpl_reg uns_pars → beval → regsT st_pars → res (regsT st_pars)
106  ; dpl_retrieve_ : regsT st_pars → dpl_reg uns_pars → res beval
107  ; dpl_arg_retrieve_ : regsT st_pars → dpl_arg uns_pars → res beval
108  ; dph_store_ : dph_reg uns_pars → beval → regsT st_pars → res (regsT st_pars)
109  ; dph_retrieve_ : regsT st_pars → dph_reg uns_pars → res beval
110  ; dph_arg_retrieve_ : regsT st_pars → dph_arg uns_pars → res beval
111  ; snd_arg_retrieve_ : regsT st_pars → snd_arg uns_pars → res beval
112  ; pair_reg_move_ : regsT st_pars → pair_move uns_pars → res (regsT st_pars)
[1882]113  ; fetch_ra: state st_pars → res ((state st_pars) × cpointer)
[1640]114
[1882]115  ; allocate_local : localsT uns_pars → regsT st_pars → regsT st_pars
[1643]116  (* Paolo: save_frame separated from call_setup to factorize tailcall code *)
[1882]117  ; save_frame: cpointer → call_dest uns_pars → state st_pars → framesT st_pars
[1643]118   (*CSC: setup_call returns a res only because we can call a function with the wrong number and
[1640]119     type of arguments. To be fixed using a dependent type *)
[1643]120  ; setup_call : nat → paramsT … uns_pars → call_args uns_pars →
[1640]121      state st_pars → res (state st_pars)
122  ; fetch_external_args: external_function → state st_pars →
123      res (list val)
[1882]124  ; set_result: list val → state st_pars → res (state st_pars)
[1640]125  ; call_args_for_main: call_args uns_pars
126  ; call_dest_for_main: call_dest uns_pars
127 }.
128
129
130definition helper_def_retrieve :
131  ∀X : ? → ? → Type[0].
132  (∀up.∀p:more_sem_unserialized_params up. regsT p → X up p → res beval) →
133  ∀up.∀p : more_sem_unserialized_params up.state p → X up p → res beval ≝
134    λX,f,up,p,st.f ? p (regs … st).
135
136definition helper_def_store :
137  ∀X : ? → ? → Type[0].
138  (∀up.∀p : more_sem_unserialized_params up.X up p → beval → regsT p → res (regsT p)) →
139  ∀up.∀p : more_sem_unserialized_params up.X up p → beval → state p → res (state p) ≝
[1882]140  λX,f,up,p,x,v,st.! r ← f ? p x v (regs … st) ; return set_regs … r st.
[1640]141
142definition acca_retrieve ≝ helper_def_retrieve ? acca_retrieve_.
143definition acca_store ≝ helper_def_store ? acca_store_.
144definition acca_arg_retrieve ≝ helper_def_retrieve ? acca_arg_retrieve_.
145definition accb_store ≝ helper_def_store ? accb_store_.
146definition accb_retrieve ≝ helper_def_retrieve ? accb_retrieve_.
147definition accb_arg_retrieve ≝ helper_def_retrieve ? accb_arg_retrieve_.
148definition dpl_store ≝ helper_def_store ? dpl_store_.
149definition dpl_retrieve ≝ helper_def_retrieve ? dpl_retrieve_.
150definition dpl_arg_retrieve ≝ helper_def_retrieve ? dpl_arg_retrieve_.
151definition dph_store ≝ helper_def_store ? dph_store_.
152definition dph_retrieve ≝ helper_def_retrieve ? dph_retrieve_.
153definition dph_arg_retrieve ≝ helper_def_retrieve ? dph_arg_retrieve_.
154definition snd_arg_retrieve ≝ helper_def_retrieve ? snd_arg_retrieve_.
[1882]155definition pair_reg_move : ?→?→?→?→?  ≝
[1640]156  λup.λp : more_sem_unserialized_params up.λst : state p.λpm : pair_move up.
157    ! r ← pair_reg_move_ ? p (regs ? st) pm;
[1882]158    return set_regs ? r st.
[1640]159
[1882]160 
[1643]161axiom BadPointer : String.
[1882]162 
[1643]163(* this is preamble to all calls (including tail ones). The optional argument in
164   input tells the function whether it has to save the frame for internal
165   calls.
[1882]166   the first element of the triple is the entry point of the function if
167   it is an internal one, or false in case of an external one.
[1643]168   The actual update of the pc is left to later, as it depends on
169   serialization and on whether the call is a tail one. *)
[1882]170definition eval_call_block:
[1949]171 ∀globals.∀p : params.∀p':more_sem_unserialized_params p.∀lbls.
[1882]172  genv globals p → state p' → block → call_args p → call_dest p →
[1949]173    IO io_out io_in ((step_flow p globals lbls)×(state p')) ≝
174 λglobals,p,p',lbls,ge,st,b,args,dest.
[1643]175  ! fd ← (opt_to_res ? [MSG BadPointer] (find_funct_ptr ?? ge b) : IO ? io_in ?);
176    match fd with
177    [ Internal fn ⇒
[1949]178      return 〈Init … (block_id b) fn args dest, st〉
[1643]179    | External fn ⇒
180      ! params ← fetch_external_args … p' fn st : IO ???;
181      ! evargs ← check_eventval_list params (sig_args (ef_sig fn)) : IO ???;
182      ! evres ← do_io (ef_id fn) evargs (proj_sig_res (ef_sig fn));
183      (* CSC: XXX bug here; I think I should split it into Byte-long
184         components; instead I am making a singleton out of it. To be
185         fixed once we fully implement external functions. *)
186      let vs ≝ [mk_val ? evres] in
187      ! st ← set_result … p' vs st : IO ???;
[1949]188      return 〈Proceed ???, st〉
[1643]189      ].
190
191axiom FailedStore: String.
192
[1882]193definition push: ∀p.state p → beval → res (state p) ≝
[1643]194 λp,st,v.
[1882]195  let isp' ≝ isp ? st in
196  do m ← opt_to_res ? (msg FailedStore) (bestorev (m … st) isp' v);
197  let isp'' ≝ shift_pointer … isp' [[false;false;false;false;false;false;false;true]] in
198  return set_m … m (set_isp … isp'' st).
199  normalize elim (isp p st) //
200qed.
[1643]201
[1882]202definition pop: ∀p. state p → res ((state p ) × beval) ≝
[1643]203 λp,st.
[1882]204  let isp' ≝ isp ? st in
205  let isp'' ≝ neg_shift_pointer ? isp' [[false;false;false;false;false;false;false;true]] in
206  let ist ≝ set_isp … isp'' st in
207  do v ← opt_to_res ? (msg FailedStore) (beloadv (m ? st) isp'');
208  OK ? 〈ist,v〉.
209  normalize elim (isp p st) //
210qed.
211 
212definition save_ra : ∀p. state p → cpointer → res (state p) ≝
[1643]213 λp,st,l.
[1882]214  let 〈addrl,addrh〉 ≝ address_of_code_pointer l in
215  ! st' ← push … st addrl;
216  push … st' addrh.
[1643]217
[1882]218definition load_ra : ∀p.state p → res ((state p) × cpointer) ≝
[1643]219 λp,st.
[1882]220  do 〈st',addrh〉 ← pop … st;
221  do 〈st'',addrl〉 ← pop … st';
222  do pr ← code_pointer_of_address 〈addrh, addrl〉;
223  return 〈st'', pr〉.
[1643]224
[1641]225(* parameters that need full params to have type of functions,
[1882]226   but are still independent of serialization *)
[1641]227record more_sem_genv_params (pp : params) : Type[1] ≝
[1640]228  { msu_pars :> more_sem_unserialized_params pp
229  ; read_result: ∀globals.genv globals pp → state msu_pars → res (list beval)
[1882]230  (* change of pc must be left to *_flow execution *)
[1949]231  ; exec_extended: ∀globals.genv globals pp → ∀s : ext_step pp.
[1882]232      state msu_pars →
[1949]233      IO io_out io_in ((step_flow pp globals (ext_step_labels … s))× (state msu_pars))
234  ; exec_fin_extended: ∀globals.genv globals pp → ∀s : ext_fin_stmt pp.
[1882]235      state msu_pars →
[1949]236      IO io_out io_in ((fin_step_flow pp globals (ext_fin_stmt_labels … s))×(state msu_pars))
[1641]237  ; pop_frame: ∀globals.genv globals pp → state msu_pars → res (state msu_pars)
238  }.
[1640]239
[1641]240(* parameters that are defined by serialization *)
241record more_sem_params (pp : params) : Type[1] ≝
242  { msg_pars :> more_sem_genv_params pp
[1882]243  ; offset_of_point : code_point pp → offset
244  ; point_of_offset : offset → option (code_point pp)
245  ; point_of_offset_of_point : ∀pt.point_of_offset (offset_of_point pt) = Some ? pt
246  ; offset_of_point_of_offset : ∀o.opt_All ? (eq ? o) (! pt ← point_of_offset o ; return offset_of_point pt)
[1640]247  }.
248
[1882]249definition pointer_of_point : ∀p.more_sem_params p →
250  cpointer→ code_point p → cpointer ≝
251  λp,msp,ptr,pt.
252    mk_pointer Code (pblock ptr) ? (offset_of_point p msp pt).
253[ elim ptr #ptr' #EQ <EQ @pok
254| %] qed.
255
256axiom BadOffsetForCodePoint : String.
257
258definition point_of_pointer :
259  ∀p.more_sem_params p → cpointer → res (code_point p) ≝
260  λp,msp,ptr.opt_to_res … (msg BadOffsetForCodePoint)
261    (point_of_offset p msp (poff ptr)).
262
263lemma point_of_pointer_of_point :
264  ∀p,msp.∀ptr : cpointer.∀pt.point_of_pointer p msp (pointer_of_point p msp ptr pt) = return pt.
265#p #msp #ptr #pt normalize
266>point_of_offset_of_point %
267qed.
268
269lemma pointer_of_point_block :
270  ∀p,msp,ptr,pt.pblock (pointer_of_point p msp ptr pt) = pblock ptr.
271/ by refl/
272qed.
273
274lemma pointer_of_point_uses_block :
275  ∀p,msp.∀ptr1,ptr2 : cpointer.∀pt.pblock ptr1 = pblock ptr2 → pointer_of_point p msp ptr1 pt = pointer_of_point p msp ptr2 pt.
276#p #msp ** #ty1 #bl1 #H1 #o1 #EQ1
277        ** #ty2 #bl2 #H2 #o2 #EQ2
278#pt #EQ3 destruct normalize //
279qed.
280
281lemma pointer_of_point_of_pointer :
282  ∀p,msp.∀ptr1,ptr2 : cpointer.∀pt.
283    pblock ptr1 = pblock ptr2 → point_of_pointer p msp ptr1 = OK … pt →
284    pointer_of_point p msp ptr2 pt = ptr1.
285#p #msp ** #ty1 #bl1 #H1 #o1 #EQ1
286        ** #ty2 #bl2 #H2 #o2 #EQ2 #pt #EQ
287destruct
288lapply (offset_of_point_of_offset p msp o1)
289normalize
290elim (point_of_offset ???) normalize [* #ABS destruct(ABS)]
291#pt' #EQ #EQ' destruct %
292qed.
293
294
295axiom ProgramCounterOutOfCode : String.
296axiom PointNotFound : String.
297axiom LabelNotFound : String.
298
299definition fetch_statement: ∀p : params.∀ msp : more_sem_params p.∀globals.
300  genv globals p → cpointer → res (joint_statement p globals) ≝
301  λp,msp,globals,ge,ptr.
302  ! pt ← point_of_pointer ? msp ptr ;
303  ! fn ← fetch_function … ge ptr ;
304  opt_to_res … (msg ProgramCounterOutOfCode) (stmt_at … (joint_if_code … fn) pt).
[1949]305 
306definition pointer_of_label_in_block : ∀p : params.∀ msp : more_sem_params p.∀globals.
307  genv globals p → block → label → res cpointer ≝
308  λp,msp,globals,ge,b,lbl.
309  ! fn ← function_of_block … ge b ;
310  ! pt ← opt_to_res … [MSG LabelNotFound ; CTX ? lbl]
311            (point_of_label … (joint_if_code … fn) lbl) ;
312  return (mk_pointer Code (mk_block Code (block_id b)) ? (offset_of_point p msp pt) : Σp.?). // qed.
[1882]313
314definition pointer_of_label : ∀p : params.∀ msp : more_sem_params p.∀globals.
315  genv globals p → cpointer → label → res cpointer ≝
[1949]316  λp,msp,globals,ge,ptr.
317  pointer_of_label_in_block p msp globals ge (pblock ptr).
[1882]318
319definition succ_pc : ∀p : params.∀ msp : more_sem_params p.
320  cpointer → succ p → res cpointer ≝
321  λp,msp,ptr,nxt.
322  ! curr ← point_of_pointer p msp ptr ;
323  return pointer_of_point p msp ptr (point_of_succ p curr nxt). 
324
[1640]325record sem_params : Type[1] ≝
326  { spp :> params
327  ; more_sem_pars :> more_sem_params spp
328  }.
329
[1882]330(* definition address_of_label: ∀globals. ∀p:sem_params.
[1640]331  genv globals p → pointer → label → res address ≝
332 λglobals,p,ge,ptr,l.
333  do newptr ← pointer_of_label … p ? ge … ptr l ;
[1882]334  OK … (address_of_code_pointer newptr). *)
[1640]335
336definition goto: ∀globals. ∀p:sem_params.
[1949]337  genv globals p → label → state p → block → res (state_pc p) ≝
338 λglobals,p,ge,l,st,b.
339  ! newpc ← pointer_of_label_in_block ? p … ge b l ;
340  return mk_state_pc ? st newpc.
[1640]341
342(*
343definition empty_state: ∀p. more_sem_params p → state p ≝
344 mk_state … (empty_framesT …)
345*)
346
[1949]347definition next : ∀p : sem_params.succ p → state p → cpointer → res (state_pc p) ≝
348 λp,l,st,pc.
349 ! newpc ← succ_pc ? p … pc l ;
350 return mk_state_pc … st newpc.
[1640]351
352axiom MissingSymbol : String.
353axiom FailedLoad : String.
354axiom BadFunction : String.
[1882]355axiom SuccessorNotProvided : String.
[1640]356
[1882]357(* the optional point must be given only for calls *)
358definition eval_step :
[1640]359 ∀globals.∀p:sem_params. genv globals p → state p →
[1949]360  ∀s:joint_step p globals.
361  IO io_out io_in ((step_flow p globals (step_labels … s))×(state p)) ≝
[1882]362 λglobals,p,ge,st,seq.
[1949]363  match seq return λx.IO ?? ((step_flow ?? (step_labels … x) × ?)) with
[1643]364  [ extension c ⇒
[1882]365    exec_extended … ge c st
[1643]366  | COST_LABEL cl ⇒
[1949]367    return 〈Proceed ???, st〉
[1643]368  | COMMENT c ⇒
[1949]369    return 〈Proceed ???, st〉
[1643]370  | LOAD dst addrl addrh ⇒
371    ! vaddrh ← dph_arg_retrieve … st addrh ;
372    ! vaddrl ← dpl_arg_retrieve … st addrl;
373    ! vaddr ← pointer_of_address 〈vaddrl,vaddrh〉;
374    ! v ← opt_to_res … (msg FailedLoad) (beloadv (m … st) vaddr);
375    ! st ← acca_store p … dst v st ;
[1949]376    return 〈Proceed ???, st〉
[1643]377  | STORE addrl addrh src ⇒
378    ! vaddrh ← dph_arg_retrieve … st addrh;
379    ! vaddrl ← dpl_arg_retrieve … st addrl;
380    ! vaddr ← pointer_of_address 〈vaddrl,vaddrh〉;
381    ! v ← acca_arg_retrieve … st src;
382    ! m' ← opt_to_res … (msg FailedStore) (bestorev (m … st) vaddr v);
[1949]383    return 〈Proceed ???, set_m … m' st〉
[1643]384  | COND src ltrue ⇒
385    ! v ← acca_retrieve … st src;
386    ! b ← bool_of_beval v;
387    if b then
[1949]388      return 〈Redirect ??? ltrue, st〉
[1643]389    else
[1949]390      return 〈Proceed ???, st〉
[1643]391  | ADDRESS ident prf ldest hdest ⇒
[1882]392    let addr ≝ opt_safe ? (find_symbol ?? ge ident) ? in
393    ! 〈laddr,haddr〉 ← address_of_pointer (mk_pointer (block_region addr) addr ? zero_offset) ;
394    ! st' ← dpl_store … ldest laddr st;
395    ! st'' ← dph_store … hdest haddr st';
[1949]396    return 〈Proceed ???, st''〉
[1643]397  | OP1 op dacc_a sacc_a ⇒
398    ! v ← acca_retrieve … st sacc_a;
399    ! v ← Byte_of_val v;
400    let v' ≝ BVByte (op1 eval op v) in
401    ! st ← acca_store … dacc_a v' st;
[1949]402    return 〈Proceed ???, st〉
[1643]403  | OP2 op dacc_a sacc_a src ⇒
404    ! v1 ← acca_arg_retrieve … st sacc_a;
405    ! v1 ← Byte_of_val v1;
406    ! v2 ← snd_arg_retrieve … st src;
407    ! v2 ← Byte_of_val v2;
408    ! carry ← bool_of_beval (carry … st);
409      let 〈v',carry〉 ≝ op2 eval carry op v1 v2 in
410      let v' ≝ BVByte v' in
411      let carry ≝ beval_of_bool carry in
[1882]412    ! st' ← acca_store … dacc_a v' st;
413      let st'' ≝ set_carry … carry st' in
[1949]414    return 〈Proceed ???, st''〉
[1643]415  | CLEAR_CARRY ⇒
[1882]416    let st' ≝ set_carry … BVfalse st in
[1949]417    return 〈Proceed ???, st'〉
[1643]418  | SET_CARRY ⇒
[1882]419    let st' ≝ set_carry … BVtrue st in
[1949]420    return 〈Proceed ???, st'〉
[1643]421  | OPACCS op dacc_a_reg dacc_b_reg sacc_a_reg sacc_b_reg ⇒
422    ! v1 ← acca_arg_retrieve … st sacc_a_reg;
423    ! v1 ← Byte_of_val v1;
424    ! v2 ← accb_arg_retrieve … st sacc_b_reg;
425    ! v2 ← Byte_of_val v2;
426    let 〈v1',v2'〉 ≝ opaccs eval op v1 v2 in
427    let v1' ≝ BVByte v1' in
428    let v2' ≝ BVByte v2' in
[1882]429    ! st' ← acca_store … dacc_a_reg v1' st;
430    ! st'' ← accb_store … dacc_b_reg v2' st';
[1949]431    return 〈Proceed ???, st''〉
[1643]432  | POP dst ⇒
[1882]433    ! 〈st',v〉 ← pop p st;
434    ! st'' ← acca_store p p dst v st';
[1949]435    return 〈Proceed ???, st''〉
[1643]436  | PUSH src ⇒
437    ! v ← acca_arg_retrieve … st src;
438    ! st ← push … st v;
[1949]439    return 〈Proceed ???, st〉
[1643]440  | MOVE dst_src ⇒
441    ! st ← pair_reg_move … st dst_src ;
[1949]442    return 〈Proceed ???, st〉
[1643]443  | CALL_ID id args dest ⇒
[1882]444    ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol ?? ge id) : IO ???;
445    eval_call_block … ge st b args dest
[1643]446  ].
[1882]447  [ cases addr //
448  | (* TODO: to prove *)
449    elim daemon
[1949]450  | %1 %
[1882]451  ] qed.
[1640]452
[1949]453definition eval_fin_step : ∀globals: list ident.∀p:sem_params. genv globals p →
454  state p → ∀s : joint_fin_step … p globals.
455  IO io_out io_in ((fin_step_flow p globals (fin_step_labels … s))×(state p)) ≝
[1882]456 λglobals,p,ge,st,s.
[1949]457  match s return λx.IO ?? ((fin_step_flow ?? (fin_step_labels … x)) × ?) with
458    [ GOTO l ⇒ return 〈FRedirect ??? l, st〉
459    | RETURN ⇒ return 〈FEnd ???, st〉
460    | extension_fin c ⇒ exec_fin_extended … ge c st
461    ]. %1 % qed.
[1882]462
463
464definition do_call : ∀globals: list ident.∀p:sem_params. genv globals p →
465  state p → Z → joint_internal_function globals p → call_args p →
466  res (state_pc p) ≝
467  λglobals,p,ge,st,id,fn,args.
468    ! st' ← setup_call … (joint_if_stacksize … fn) (joint_if_params … fn)
469              args st ;
470    let regs ≝ foldr ?? (allocate_local p p) (regs … st) (joint_if_locals … fn) in
471    let l' ≝ joint_if_entry … fn in
472    let st' ≝ set_regs p regs st in
473    let pointer_in_fn ≝ mk_pointer Code (mk_block Code id) ? (mk_offset 0) in
474    let pc ≝ pointer_of_point ? p … pointer_in_fn l' in
475    return mk_state_pc ? st' pc. % qed.
476
[1949]477(* The pointer provided is the one to the *next* instruction.
478   The boolean tells wether a flow changement has occurred (i.e.
479   a non Proceed cmd was issued). Used in linking block evaluation
480   with regular one *)
481definition eval_step_flow :
482 ∀globals.∀p:sem_params.∀lbls.genv globals p →
483  state p → cpointer → step_flow p globals lbls →
484    res (bool × (state_pc p)) ≝
485 λglobals,p,lbls,ge,st,nxt,cmd.
486 match cmd with
487  [ Redirect l ⇒
488    ! st ← goto … ge l st (pblock nxt) ; return 〈true, st〉
489  | Init id fn args dest ⇒
490    let st' ≝ set_frms … (save_frame … nxt dest st) st in
491    ! st ← do_call ?? ge st' id fn args ;
492    return 〈true, st〉
493  | Proceed ⇒
494    return 〈false, mk_state_pc ? st nxt〉
495  ].
496
497definition eval_fin_step_flow : ∀globals: list ident.∀p:sem_params.∀lbls. genv globals p →
498  state p → block → fin_step_flow p globals lbls → res (state_pc p) ≝
499  λglobals,p,lbls,ge,st,b,cmd.
500  match cmd with
501  [ FRedirect l ⇒ goto … ge l st b
502  | FTailInit id fn args ⇒
[1882]503    do_call … ge st id fn args
[1949]504  | FEnd ⇒
505    ! 〈st',ra〉 ← fetch_ra … st ;
506    ! st'' ← pop_frame … ge st;
507    return mk_state_pc ? st'' ra
[1882]508  ].
509
[1949]510definition eval_statement :
511 ∀globals.∀p:sem_params.genv globals p →
512  state_pc p → joint_statement p globals →
513    IO io_out io_in (bool × (state_pc p)) ≝
514 λglobals,p,ge,st,stmt.
515 match stmt with
516 [ sequential s nxt ⇒
517   ! 〈flow, st'〉 ← eval_step … ge st s ;
518   ! nxtptr ← succ_pc ? p (pc … st) nxt ;
519   eval_step_flow … ge st' nxtptr flow
520 | final s ⇒
521   ! 〈flow, st'〉 ← eval_fin_step … ge st s ;
522   ! st ← eval_fin_step_flow … ge st' (pblock … (pc … st)) flow ;
523   return 〈true, st〉
524 ].
[1640]525
[1949]526definition eval_state_flag : ∀globals: list ident.∀p:sem_params. genv globals p →
527  state_pc p → IO io_out io_in (bool × (state_pc p)) ≝
528  λglobals,p,ge,st.
529  ! s ← fetch_statement ? p … ge (pc … st) : IO ???;
530  eval_statement … ge st s.
[1882]531
532definition eval_state : ∀globals: list ident.∀p:sem_params. genv globals p →
[1949]533  state_pc p → IO io_out io_in (state_pc p) ≝
[1882]534  λglobals,p,ge,st.
[1949]535  ! 〈flag,st'〉 ← eval_state_flag … ge st ;
536  return st'.
[1882]537
[1949]538(* Paolo: what if in an intermediate language main finishes with an external
539  tailcall? Maybe it should rely on an FEnd flow command issued, but that's
540  not static... *)
[1640]541definition is_final: ∀globals:list ident. ∀p: sem_params.
[1882]542  genv globals p → cpointer → state_pc p → option int ≝
[1640]543 λglobals,p,ge,exit,st.res_to_opt ? (
[1882]544  do s ← fetch_statement ? p … ge (pc … st);
[1640]545  match s with
[1949]546  [ final s' ⇒
547    match s' with
548    [ RETURN ⇒
[1640]549      do 〈st,ra〉 ← fetch_ra … st;
[1882]550      if eq_pointer ra exit then
[1640]551       do vals ← read_result … ge st ;
552       Word_of_list_beval vals
553      else
554       Error ? [ ]
[1949]555   | _ ⇒ Error ? [ ]
556   ]
557 | _ ⇒ Error ? [ ]
558 ]).
[1882]559 
[1640]560record evaluation_parameters : Type[1] ≝
561 { globals: list ident
562 ; sparams:> sem_params
[1882]563 ; exit: cpointer
[1640]564 ; genv2: genv globals sparams
565 }.
566
[1949]567(* Paolo: with structured traces, eval need not emit labels. However, this
568  changes trans_system. For now, just putting a dummy thing for
569  the transition. *)
[1640]570definition joint_exec: trans_system io_out io_in ≝
[1882]571  mk_trans_system … evaluation_parameters (λG. state_pc G)
[1640]572   (λG.is_final (globals G) G (genv2 G) (exit G))
[1949]573   (λG,st.! 〈flag,st'〉 ← eval_state_flag (globals G) G (genv2 G) st ; return 〈E0, st'〉).
[1640]574
575definition make_global :
576 ∀pars: sem_params.
577  joint_program pars → evaluation_parameters
578
579 λpars.
580 (* Invariant: a -1 block is unused in common/Globalenvs *)
581 let b ≝ mk_block Code (-1) in
582 let ptr ≝ mk_pointer Code b ? (mk_offset 0) in
583  (λp. mk_evaluation_parameters
584    (prog_var_names … p)
585    (mk_sem_params … pars)
[1882]586    ptr
[1640]587    (globalenv Genv … p)
588  ).
589% qed.
590
591axiom ExternalMain: String.
592
593definition make_initial_state :
594 ∀pars: sem_params.
[1882]595 ∀p: joint_program … pars. res (state_pc pars) ≝
[1640]596λpars,p.
597  let sem_globals ≝ make_global pars p in
598  let ge ≝ genv2 sem_globals in
599  let m ≝ init_mem Genv … p in
600  let 〈m,spb〉 ≝ alloc … m 0 external_ram_size XData in
601  let 〈m,ispb〉 ≝ alloc … m 0 internal_ram_size XData in
602  let dummy_pc ≝ mk_pointer Code (mk_block Code (-1)) ? (mk_offset 0) in
603  let spp ≝ mk_pointer XData spb ? (mk_offset external_ram_size) in
604  let ispp ≝ mk_pointer XData ispb ? (mk_offset 47) in
605  let main ≝ prog_main … p in
[1882]606  let st0 ≝ mk_state pars (empty_framesT …) spp ispp BVfalse (empty_regsT … spp) m in
607  (* use exit sem_globals as ra and call_dest_for_main as dest *)
608  let st0' ≝ set_frms ? (save_frame … (exit sem_globals) (call_dest_for_main … pars) st0) st0 in
609  let st_pc0 ≝ mk_state_pc ? st0' dummy_pc in
610  ! main_block ← opt_to_res … [MSG MissingSymbol; CTX ? main] (find_symbol ?? ge main) ;
611  ! main_fd ← opt_to_res ? [MSG BadPointer] (find_funct_ptr ?? ge main_block) ;
612  match main_fd with
613  [ Internal fn ⇒
614    do_call ?? ge st_pc0 (block_id main_block) fn (call_args_for_main … pars)
615  | External _ ⇒ Error … [MSG ExternalMain] (* External main not supported: why? *)
616  ]. [5: cases ispb * |6: cases spb * ] (* without try it fails! *) try //
[1640]617qed.
618
619definition joint_fullexec :
620 ∀pars:sem_params.fullexec io_out io_in ≝
621 λpars.mk_fullexec ??? joint_exec (make_global pars) (make_initial_state pars).
Note: See TracBrowser for help on using the repository browser.