source: src/joint/semantics.ma @ 2529

Last change on this file since 2529 was 2529, checked in by tranquil, 7 years ago

rewritten function handling in joint
swapped call_rel with ret_rel in the definition of status_rel, and parameterised status_simulation on status_rel
renamed SemanticUtils?

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