source: src/joint/semantics_paolo.ma @ 2200

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