Ignore:
Timestamp:
Nov 13, 2012, 11:30:23 AM (8 years ago)
Author:
tranquil
Message:

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:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/semantics.ma

    r2443 r2457  
    1111   only the head is kept (or Undef if the list is empty) ??? *)
    1212
     13definition is_function ≝ λF.λglobals : list ident.λge : genv_t (fundef (F globals)).
     14  λi : ident.∃fd.
     15    ! bl ← find_symbol … ge i ;
     16    find_funct_ptr … ge bl = Some ? fd.
     17
     18definition description_of_function : ∀F,globals,ge.(Σi.is_function F globals ge i) →
     19fundef (F globals) ≝
     20λF,globals,ge,i.
     21match ! bl ← find_symbol … ge i ;
     22        find_funct_ptr … ge bl
     23return λx.(∃fd.x = ?) → ?
     24with
     25[ Some fd ⇒ λ_.fd
     26| None ⇒ λprf.⊥
     27] (pi2 … i).
     28cases prf #fd #ABS destruct
     29qed.
     30
     31definition is_internal_function ≝ λF.λglobals : list ident.λge : genv_t (fundef (F globals)).
     32  λi : ident.∃fd.
     33    ! bl ← find_symbol … ge i ;
     34    find_funct_ptr … ge bl = Some ? (Internal ? fd).
     35
     36lemma description_of_internal_function : ∀F,globals,ge,i,fn.
     37  description_of_function F globals ge i = Internal ? fn → is_internal_function … ge i.
     38#F #globals #ge * #i * #fd #EQ
     39#fn whd in ⊢ (??%?→?); >EQ normalize nodelta #EQ' >EQ' in EQ; #EQ
     40%{EQ}
     41qed.
     42
     43lemma internal_function_is_function : ∀F,globals,ge,i.
     44  is_internal_function F globals ge i → is_function … ge i.
     45#F #globals #ge #i * #fn #prf %{prf} qed.
     46
     47definition if_of_function : ∀F,globals,ge.(Σi.is_internal_function F globals ge i) →
     48F globals ≝
     49λF,globals,ge,i.
     50match ! bl ← find_symbol … ge i ;
     51        find_funct_ptr … ge bl
     52return λx.(∃fn.x = ?) → ?
     53with
     54[ Some fd ⇒
     55  match fd return λx.(∃fn.Some ? x = ?) → ? with
     56  [ Internal fn ⇒ λ_.fn
     57  | External _ ⇒ λprf.⊥
     58  ]
     59| None ⇒ λprf.⊥
     60] (pi2 … i).
     61cases prf #fn #ABS destruct
     62qed.
     63
    1364(* Paolo: I'll put in this record the property about genv we need *)
    1465record genv_gen (F : list ident → Type[0]) (globals : list ident) : Type[0] ≝
    1566{ ge :> genv_t (fundef (F globals))
    1667; find_symbol_exists : ∀id.In ? globals id → find_symbol … ge id ≠ None ?
     68; stack_sizes : (Σi.is_internal_function F globals ge i) → ℕ
    1769}.
    1870
     
    102154axiom BadProgramCounter : String.
    103155
    104 definition function_of_block :
    105  ∀pars : params.
    106  ∀globals.
    107   genv pars globals →
    108   block →
    109   res (joint_closed_internal_function pars globals) ≝
    110   λpars,globals,ge,b.
    111   do def ← opt_to_res ? [MSG BadProgramCounter] (find_funct_ptr … ge b) ;
    112   match def with
    113   [ Internal def' ⇒ OK … def'
    114   | External _ ⇒ Error … [MSG BadProgramCounter]].
    115  
    116 (* this can replace graph_fetch function and lin_fetch_function *)
    117 definition fetch_function:
    118  ∀pars : params.
    119  ∀globals.
    120   genv pars globals →
    121   cpointer →
    122   res (joint_closed_internal_function pars globals) ≝
    123  λpars,globals,ge,p.function_of_block pars globals ge (pblock p).
    124 
     156(*
    125157inductive step_flow (p : unserialized_params) (F : Type[0]) : possible_flows → Type[0] ≝
    126158  | Redirect : ∀lbls.(Σl.In ? lbls l) → step_flow p F (Labels lbls) (* used for goto-like flow alteration *)
     
    133165  | FEnd1  : fin_step_flow p F (Labels [ ]) (* end flow *)
    134166  | FEnd2  : fin_step_flow p F Call. (* end flow *)
     167*)
     168
     169definition funct_of_ident : ∀F,globals,ge.
     170  ident → option (Σi.is_function F globals ge i)
     171≝ λF,globals,ge,i.
     172match ?
     173return λx.! bl ← find_symbol … ge i ;
     174    find_funct_ptr … ge bl = x → ?
     175with
     176[ Some fd ⇒ λprf.return «i, ex_intro ?? fd prf»
     177| None ⇒ λ_.None ?
     178] (refl …).
     179
     180lemma match_opt_prf_elim : ∀A,B : Type[0].∀m : option A.
     181∀Q : option A → Prop.
     182∀c1 : ∀a.Q (Some ? a) → B.
     183∀c2 : Q (None ?) → B.
     184∀P : B → Prop.
     185(∀a,prf.P (c1 a prf)) →
     186(∀prf.P (c2 prf)) →
     187∀prf : Q m.
     188P (match m return λx.Q x → ? with
     189   [ Some a ⇒ λprf.c1 a prf
     190   | None ⇒ λprf.c2 prf
     191   ] prf).
     192#A #B * [2: #a ] #Q #c1 #c2 #P #H1 #H2 #prf
     193normalize [@H1 | @H2]
     194qed.
     195
     196lemma symbol_of_function_block_ok :
     197  ∀F,ge,b,prf.symbol_for_block F ge b = Some ? (symbol_of_function_block F ge b prf).
     198#F #ge #b #FFP
     199whd in ⊢ (???(??%));
     200@match_opt_prf_elim [//] #H @⊥
     201(* cut and paste from global env *)
     202whd in H:(??%?);
     203cases b in FFP H ⊢ %; * * -b [2,3,5,6: #b ] normalize in ⊢ (% → ?); [4: #FFP | *: * #H cases (H (refl ??)) ]
     204cases (functions_inv … ge b FFP)
     205#id #L lapply (find_lookup ?? (symbols F ge) (λid',b'. eq_block (mk_block Code (neg b)) b') id (mk_block Code (neg b)))
     206lapply (find_none … (symbols F ge) (λid',b'. eq_block (mk_block Code (neg b)) b') id (mk_block Code (neg b)))
     207cases (find ????)
     208[ #H #_ #_ lapply (H (refl ??) L) @eq_block_elim [ #_ * | * #H' cases (H' (refl ??)) ]
     209| * #id' #b' #_ normalize #_ #E destruct
     210] qed.
     211
     212definition funct_of_block : ∀F,globals,ge.
     213  block → option  (Σi.is_function F globals ge i) ≝
     214λF,globals,ge,bl.
     215   match find_funct_ptr … ge bl
     216   return λx.find_funct_ptr … ge bl = x → ? with
     217   [ Some fd ⇒ λprf.return mk_Sig
     218        ident (λi.is_function F globals ge i)
     219        (symbol_of_function_block … ge bl ?)
     220        (ex_intro … fd ?)
     221   | None ⇒ λ_.None ?
     222   ] (refl …).
     223[ >(symbol_of_block_rev … (symbol_of_function_block_ok ? ge bl ?)) @prf
     224| >prf % #ABS destruct(ABS)
     225]
     226qed.
     227
     228definition int_funct_of_block : ∀F,globals,ge.
     229  block → option (Σi.is_internal_function F globals ge i) ≝
     230  λF,globals,ge,bl.
     231  ! f ← funct_of_block … ge bl ;
     232  match ?
     233  return λx.description_of_function … f = x → option (Σi.is_internal_function … ge i)
     234  with
     235  [ Internal fn ⇒ λprf.return «pi1 … f, ?»
     236  | External fn ⇒ λ_.None ?
     237  ] (refl …).
     238@(description_of_internal_function … prf)
     239qed.
     240
     241definition funct_of_bevals : ∀F,globals,ge.
     242  beval → beval → option (Σi.is_function F globals ge i) ≝
     243λF,globals,ge,dpl,dph.
     244! ptr ← res_to_opt … (pointer_of_address 〈dpl, dph〉) ;
     245if eq_bv … (bv_zero …) (offv (poff ptr)) ∧
     246   match ptype ptr with [ Code ⇒ true | _ ⇒ false] then
     247   funct_of_block … (pblock ptr)
     248else None ?.
     249
     250definition block_of_funct_ident ≝ λF,globals,ge.
     251  λi : Σi.is_function F globals ge i.
     252  match find_symbol … ge i return λx.(∃fd.!bl ← x; ? = ?) → ? with
     253  [ Some bl ⇒ λ_.bl
     254  | None ⇒ λprf.⊥
     255  ] (pi2 … i).
     256cases prf #fd normalize #ABS destruct(ABS)
     257qed.
     258
     259axiom ProgramCounterOutOfCode : String.
     260axiom PointNotFound : String.
     261axiom LabelNotFound : String.
     262axiom MissingSymbol : String.
     263axiom FailedLoad : String.
     264axiom BadFunction : String.
     265axiom SuccessorNotProvided : String.
     266axiom BadPointer : String.
     267
     268(* this can replace graph_fetch function and lin_fetch_function *)
     269definition fetch_function:
     270 ∀pars : params.
     271 ∀globals.
     272 ∀ge : genv pars globals.
     273  cpointer →
     274  res (Σi.is_internal_function … ge i) ≝
     275 λpars,globals,ge,p.
     276 opt_to_res … [MSG BadFunction; MSG BadPointer]
     277    (int_funct_of_block … ge (pblock p)).
    135278
    136279record sem_unserialized_params
     
    138281  (F : list ident → Type[0]) : Type[1] ≝
    139282  { st_pars :> sem_state_params
     283
    140284  ; acca_store_ : acc_a_reg uns_pars → beval → regsT st_pars → res (regsT st_pars)
    141285  ; acca_retrieve_ : regsT st_pars → acc_a_reg uns_pars → res beval
     
    161305  ; setup_call : nat → paramsT … uns_pars → call_args uns_pars →
    162306      state st_pars → res (state st_pars)
    163   ; fetch_external_args: external_function → state st_pars →
     307  ; fetch_external_args: external_function → state st_pars → call_args … uns_pars →
    164308      res (list val)
    165309  ; set_result: list val → call_dest uns_pars → state st_pars → res (state st_pars)
     
    170314  ; read_result: ∀globals.genv_gen F globals → call_dest uns_pars → state st_pars → res (list beval)
    171315  (* change of pc must be left to *_flow execution *)
    172   ; eval_ext_seq: ∀globals.genv_gen F globals → ext_seq uns_pars →
    173       F globals → state st_pars → IO io_out io_in (state st_pars)
    174   ; eval_ext_tailcall : ∀globals.genv_gen F globals → ext_tailcall uns_pars →
    175       F globals → state st_pars → IO io_out io_in ((fin_step_flow uns_pars (F globals) Call)×(state st_pars))
    176   ; ext_tailcall_id : ∀globals.genv_gen F globals → ext_tailcall uns_pars →
    177       state st_pars → IO io_out io_in ident
    178   ; pop_frame: ∀globals.genv_gen F globals → F globals → state st_pars → res (state st_pars)
    179   (* do something more in some op2 calculations (e.g. mark a register for correction
    180      with spilled_no in ERTL) *)
    181   ; post_op2 : ∀globals.genv_gen F globals →
    182     Op2 → acc_a_reg uns_pars → acc_a_arg uns_pars → snd_arg uns_pars →
    183     state st_pars → state st_pars
     316  ; eval_ext_seq: ∀globals.∀ge : genv_gen F globals.ext_seq uns_pars →
     317    (Σi.is_internal_function … ge i) (* current *) → state st_pars → IO io_out io_in (state st_pars)
     318  ; pop_frame: ∀globals.∀ge : genv_gen F globals.
     319    (Σi.is_internal_function … ge i) (* current *) → state st_pars → res (state st_pars)
    184320  }.
    185321
     
    220356    return set_regs ? r st.
    221357 
    222 axiom BadPointer : String.
    223 
    224 (* this is preamble to all calls (including tail ones). The optional argument in
    225    input tells the function whether it has to save the frame for internal
    226    calls.
    227    the first element of the triple is the entry point of the function if
    228    it is an internal one, or false in case of an external one.
    229    The actual update of the pc is left to later, as it depends on
    230    serialization and on whether the call is a tail one. *)
    231 definition eval_call_block:
    232  ∀p,F.∀p':sem_unserialized_params p F.∀globals.
    233   genv_t (fundef (F globals)) → state (st_pars ?? p') → block → call_args p → call_dest p →
    234     IO io_out io_in ((step_flow p (F globals) Call)×(state (st_pars ?? p'))) ≝
    235  λp,F,p',globals,ge,st,b,args,dest.
    236   ! fd ← (opt_to_res ? [MSG BadPointer] (find_funct_ptr ? ge b) : IO ? io_in ?);
    237     match fd with
    238     [ Internal fd ⇒
    239       return 〈Init ?? (block_id b) fd args dest, st〉
    240     | External fn ⇒
    241       ! params ← fetch_external_args … p' fn st : IO ???;
    242       ! evargs ← check_eventval_list params (sig_args (ef_sig fn)) : IO ???;
    243       ! evres ← do_io (ef_id fn) evargs (proj_sig_res (ef_sig fn));
    244       (* CSC: XXX bug here; I think I should split it into Byte-long
    245          components; instead I am making a singleton out of it. To be
    246          fixed once we fully implement external functions. *)
    247       let vs ≝ [mk_val ? evres] in
    248       ! st ← set_result … p' vs dest st : IO ???;
    249       return 〈Proceed ???, st〉
    250       ].
    251 
    252358axiom FailedStore: String.
    253359
     
    355461qed.
    356462
    357 axiom ProgramCounterOutOfCode : String.
    358 axiom PointNotFound : String.
    359 axiom LabelNotFound : String.
    360 
    361463definition fetch_statement: ∀p : params.∀ msp : more_sem_params p.∀globals.
    362   genv p globals → cpointer →
    363   res ((joint_closed_internal_function p globals) × (joint_statement p globals)) ≝
     464  ∀ge:genv p globals. cpointer →
     465  res ((Σi.is_internal_function … ge i) × (joint_statement p globals)) ≝
    364466  λp,msp,globals,ge,ptr.
     467  let bl ≝ pblock ptr in
     468  ! f ← opt_to_res … [MSG BadFunction; MSG BadPointer]
     469    (int_funct_of_block … ge bl) ;
     470  let fn ≝ if_of_function … f in
    365471  let pt ≝ point_of_pointer ? msp ptr in
    366   ! fn ← fetch_function … ge ptr ;
    367472  ! stmt ← opt_to_res … (msg ProgramCounterOutOfCode) (stmt_at … (joint_if_code … fn) pt);
    368   return 〈fn, stmt〉.
    369  
     473  return 〈f, stmt〉.
     474
    370475definition pointer_of_label : ∀p : params.∀ msp : more_sem_params p.∀globals.
    371476  genv p globals → cpointer → label → res cpointer ≝
    372477  λp,msp,globals,ge,ptr,lbl.
    373   ! fn ← fetch_function … ge ptr ;
     478  ! f ← fetch_function … ge ptr ;
     479  let fn ≝ if_of_function …  ge f in
    374480  ! pt ← opt_to_res … [MSG LabelNotFound ; CTX ? lbl]
    375481            (point_of_label … (joint_if_code … fn) lbl) ;
     
    435541 return mk_state_pc … st newpc.
    436542
    437 axiom MissingSymbol : String.
    438 axiom FailedLoad : String.
    439 axiom BadFunction : String.
    440 axiom SuccessorNotProvided : String.
    441 
    442 definition block_of_call ≝ λp:sem_params.λglobals.
     543
     544definition function_of_call ≝ λp:sem_params.λglobals.
    443545  λge: genv p globals.λst : state p.λf.
    444546  match f with
    445547  [ inl id ⇒
    446     opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol … ge id)
     548    opt_to_res … [MSG BadFunction; MSG MissingSymbol; CTX ? id] (funct_of_ident … ge id)
    447549  | inr addr ⇒
    448550    ! addr_l ← dpl_arg_retrieve … st (\fst addr) ;
    449551    ! addr_h ← dph_arg_retrieve … st (\snd addr) ;
    450     ! ptr ← pointer_of_bevals [addr_l ; addr_h] ;
    451     if eq_bv … (bv_zero …) (offv (poff … ptr)) then
    452       return pblock ptr
    453     else Error … [MSG BadFunction]
     552    opt_to_res … [MSG BadFunction; MSG BadPointer] (funct_of_bevals … ge addr_l addr_h)
    454553  ].
    455554
     555(* Paolo: why external calls do not need args?? *)
     556definition eval_external_call ≝
     557λp,F.λp' : sem_unserialized_params p F.λfn,args,dest,st.
     558      ! params ← fetch_external_args … p' fn st args : IO ???;
     559      ! evargs ← check_eventval_list params (sig_args (ef_sig fn)) : IO ???;
     560      ! evres ← do_io (ef_id fn) evargs (proj_sig_res (ef_sig fn));
     561      (* CSC: XXX bug here; I think I should split it into Byte-long
     562         components; instead I am making a singleton out of it. To be
     563         fixed once we fully implement external functions. *)
     564      let vs ≝ [mk_val ? evres] in
     565      set_result … p' vs dest st.
     566
     567lemma block_of_funct_ident_is_code : ∀F,globals,ge,i.
     568  block_region (block_of_funct_ident F globals ge i) = Code.
     569#F #globals #ge * #i * #fd
     570whd in ⊢ (?→??(?%)?);
     571cases (find_symbol ???)
     572[ #ABS normalize in ABS; destruct(ABS) ]
     573#bl normalize nodelta >m_return_bind
     574whd in ⊢ (??%?→?); cases (block_region bl)
     575[ #ABS normalize in ABS; destruct(ABS) ]
     576#_ %
     577qed.
     578
     579definition eval_internal_call_pc ≝
     580λp : sem_params.λglobals : list ident.λge : genv p globals.λi.
     581let fn ≝ if_of_function … ge i in
     582let l' ≝ joint_if_entry ?? fn in
     583let pointer_in_fn ≝ mk_pointer (block_of_funct_ident … ge (pi1 … i)) (mk_offset (bv_zero …)) in
     584pointer_of_point ? p … pointer_in_fn l'.
     585[ @block_of_funct_ident_is_code
     586| cases i /2 by internal_function_is_function/
     587]
     588qed.
     589
     590definition eval_internal_call_no_pc ≝
     591λp : sem_params.λglobals : list ident.λge : genv p globals.λi,args,st.
     592let fn ≝ if_of_function … ge i in
     593let stack_size ≝ stack_sizes … ge i in
     594! st' ← setup_call … stack_size (joint_if_params … fn) args st ;
     595let regs ≝ foldr ?? (allocate_local … p) (regs … st) (joint_if_locals … fn) in
     596return set_regs p regs st.
     597
    456598definition eval_seq_no_pc :
    457  ∀p:sem_params.∀globals. genv p globals → joint_closed_internal_function p globals
    458   state p → ∀s:joint_seq p globals.
     599 ∀p:sem_params.∀globals.∀ge:genv p globals. (Σi.is_internal_function … ge i)
     600  state p → cpointer → joint_seq p globals →
    459601  IO io_out io_in (state p) ≝
    460  λp,globals,ge,curr_fn,st,seq.
     602 λp,globals,ge,curr_fn,st,next,seq.
    461603 match seq return λx.IO ??? with
    462604  [ extension_seq c ⇒
     
    489631    ! 〈v',carry〉 ← be_op2 (carry … st) op v1 v2 ;
    490632    ! st' ← acca_store … dacc_a v' st;
    491     return set_carry … carry (post_op2 … p … ge op dacc_a sacc_a src st')
     633    return set_carry … carry st'
    492634  | CLEAR_CARRY ⇒
    493635    return set_carry … (BBbit false) st
     
    509651    pair_reg_move … st dst_src
    510652  | CALL f args dest ⇒
    511     ! b ← block_of_call … ge st f : IO ???;
    512     ! 〈flow, st'〉 ← eval_call_block … ge st b args dest ;
    513     return st'
     653    ! fn ← function_of_call … ge st f : IO ???;
     654    match description_of_function … fn return λx.description_of_function … fn = x → ? with
     655    [ Internal fd ⇒ λprf.
     656      ! st' ← save_frame … next dest st ;
     657      eval_internal_call_no_pc … ge «fn, ?» args st'  (* only pc changes *)
     658    | External fd ⇒ λ_.eval_external_call … fd args dest st
     659    ] (refl …)
    514660  | _ ⇒ return st
    515661  ].
    516   @find_symbol_exists
     662[ @find_symbol_exists
    517663  lapply prf
    518664  elim globals [*]
    519665  #hd #tl #IH * [@eq_identifier_elim #H * >H %1 % ]
    520666  #G %2 @IH @G
    521   qed.
    522 
    523 definition eval_seq_pc :
    524  ∀p:sem_params.∀globals. genv p globals → state p →
    525   ∀s:joint_seq p globals.
    526   IO io_out io_in (step_flow p ? (step_flows … s)) ≝
    527   λp,g,ge,st,s.match s return λx : joint_seq ??.IO ?? (step_flow ?? (step_flows … x)) with
     667| @(description_of_internal_function … prf)
     668]
     669qed.
     670
     671definition eval_seq_pc :
     672 ∀p:sem_params.∀globals.∀ge:genv p globals.
     673  state p → cpointer → joint_seq p globals →
     674  res cpointer ≝
     675  λp,globals,ge,st,next,s.
     676  match s with
    528677  [ CALL f args dest ⇒
    529     ! b ← block_of_call … ge st f : IO ???;
    530     ! 〈flow, st'〉 ← eval_call_block … ge st b args dest ;
    531     return flow
    532   | _ ⇒ return Proceed ???
     678    ! fn ← function_of_call … ge st f;
     679    match ? return λx.description_of_function … fn = x → ? with
     680    [ Internal _ ⇒ λprf.eval_internal_call_pc … ge «fn, ?»
     681    | External _ ⇒ λ_.return next
     682    ] (refl …)
     683  | _ ⇒ return next
    533684  ].
    534 
    535 definition eval_step :
    536  ∀p:sem_params.∀globals. genv p globals →
    537   joint_closed_internal_function p globals → state p →
    538   ∀s:joint_step p globals.
    539   IO io_out io_in ((step_flow p ? (step_flows … s))×(state p)) ≝
    540   λp,globals,ge,curr_fn,st,s.
    541   match s return λx.IO ?? ((step_flow ?? (step_flows … x))×?) with
    542   [ step_seq s ⇒
    543     ! flow ← eval_seq_pc ?? ge st s ;
    544     ! st' ← eval_seq_no_pc ?? ge curr_fn st s ;
    545     return 〈flow,st'〉
    546   | COND src ltrue ⇒
    547     ! v ← acca_retrieve … st src;
    548     ! b ← bool_of_beval v;
    549     if b then
    550       return 〈Redirect ??? ltrue, st〉
    551     else
    552       return 〈Proceed ???, st〉
     685@(description_of_internal_function … prf)
     686qed.
     687
     688definition eval_statement :
     689 ∀p:sem_params.∀globals.∀ge:genv p globals.
     690 (Σi.is_internal_function … ge i) → state_pc p →
     691  ∀s:joint_statement p globals.
     692  IO io_out io_in (state_pc p) ≝
     693  λp,g,ge,curr_fn,st,s.
     694  match s with
     695  [ sequential s next ⇒
     696    ! next_ptr ← succ_pc ? p (pc … st) next : IO ??? ;
     697    match s return λ_.IO ??? with
     698    [ step_seq s ⇒
     699      ! st' ← eval_seq_no_pc … ge curr_fn st next_ptr s ;
     700      ! pc' ← eval_seq_pc … ge st next_ptr s ;
     701      return mk_state_pc … st' pc'
     702    | COND a l ⇒
     703      ! v ← acca_retrieve … st a ;
     704      ! b ← bool_of_beval … v ;
     705      ! pc' ←
     706        if b then
     707          pointer_of_label ? p … ge (pc … st) l
     708        else
     709          succ_pc ? p (pc … st) next ;
     710      return mk_state_pc … st pc'
     711    ]
     712  | final s ⇒
     713    match s with
     714    [ GOTO l ⇒
     715      ! pc' ← pointer_of_label ? p ? ge (pc … st) l ;
     716      return mk_state_pc … st pc'
     717    | RETURN ⇒
     718      ! st' ← pop_frame … curr_fn st ;
     719      ! 〈pc', st''〉 ← fetch_ra … p st' ;
     720      return mk_state_pc … st'' pc'
     721    | TAILCALL _ f args ⇒
     722      ! fn ← function_of_call … ge st f : IO ???;
     723      match ? return λx.description_of_function … fn = x → ? with
     724      [ Internal _ ⇒ λprf.
     725        ! pc' ← eval_internal_call_pc … ge «fn, ?» ;
     726        return mk_state_pc … st pc'
     727      | External fd ⇒ λ_.
     728        let curr_dest ≝ joint_if_result ?? (if_of_function … curr_fn) in
     729        ! st' ← eval_external_call ??? fd args curr_dest st ;
     730        ! st'' ← pop_frame … curr_fn st ;
     731        ! 〈pc', st'''〉 ← fetch_ra … p st'' ;
     732        return mk_state_pc … st''' pc'
     733      ] (refl …)
     734    ]
    553735  ].
    554   %1 % qed.
    555 
    556 definition eval_fin_step_no_pc : ∀p:sem_params.∀globals. genv p globals →
    557   (* current function *) joint_closed_internal_function p globals → state p → ∀s : joint_fin_step p.
    558   IO io_out io_in (state p) ≝
    559  λp,globals,ge,curr_fn,st,s.
    560   match s return λx.IO ??? with
    561     [ tailcall c ⇒
    562       !〈flow,st'〉 ← eval_ext_tailcall … ge c curr_fn st ;
    563       return st'
    564     | _ ⇒ return st
    565     ].
    566 
    567 definition eval_fin_step_pc :
    568  ∀p:sem_params.∀globals. genv p globals → joint_closed_internal_function p globals → state p →
    569   ∀s:joint_fin_step p.
    570   IO io_out io_in (fin_step_flow p ? (fin_step_flows … s)) ≝
    571   λp,g,ge,curr_fn,st,s.
    572   match s return λx.IO ?? (fin_step_flow ?? (fin_step_flows … x)) with
    573   [ tailcall c ⇒
    574     !〈flow,st'〉 ← eval_ext_tailcall … ge c curr_fn st ;
    575     return flow 
    576   | GOTO l ⇒ return FRedirect … l
    577   | RETURN ⇒ return FEnd1 ??
    578   ]. %1 % qed.
    579 
    580 definition do_call : ∀p:sem_params.∀globals: list ident. genv p globals →
    581   state p → Z → joint_closed_internal_function p globals → call_args p →
    582   res (state_pc p) ≝
    583   λp,globals,ge,st,id,fn,args.
    584     ! st' ← setup_call … (joint_if_stacksize … fn) (joint_if_params … fn)
    585               args st ;
    586     let regs ≝ foldr ?? (allocate_local … p) (regs … st) (joint_if_locals … fn) in
    587     let l' ≝ joint_if_entry … fn in
    588     let st' ≝ set_regs p regs st in
    589     let pointer_in_fn ≝ mk_pointer (mk_block Code id) (mk_offset (bv_zero …)) in
    590     ! pc ← pointer_of_point ? p … pointer_in_fn l' ;
    591     return mk_state_pc ? st' pc. % qed.
    592 
    593 (* The pointer provided is the one to the *next* instruction. *)
    594 definition eval_step_flow :
    595  ∀p:sem_params.∀globals.∀flows.genv p globals →
    596  state p → cpointer → step_flow p ? flows → res (state_pc p) ≝
    597  λp,globals,flows,ge,st,nxt,cmd.
    598  match cmd with
    599   [ Redirect _ l ⇒
    600     goto … ge l st nxt
    601   | Init id fn args dest ⇒
    602     ! st' ← save_frame … nxt dest st ;
    603     do_call ?? ge st' id fn args
    604   | Proceed _ ⇒
    605     return mk_state_pc ? st nxt
    606   ].
    607 
    608 definition eval_fin_step_flow : ∀p:sem_params.∀globals: list ident.∀flows. genv p globals →
    609   state p → cpointer → fin_step_flow p ? flows → res (state_pc p) ≝
    610   λp,globals,lbls,ge,st,curr,cmd.
    611   match cmd with
    612   [ FRedirect _ l ⇒ goto … ge l st curr
    613   | FTailInit id fn args ⇒
    614     do_call … ge st id fn args
    615   | _ ⇒
    616     ! 〈ra, st'〉 ← fetch_ra … st ;
    617     ! fn ← fetch_function … ge curr ;
    618     ! st'' ← pop_frame … ge fn st';
    619     return mk_state_pc ? st'' ra
    620   ].
    621 
    622 definition eval_statement :
    623  ∀globals.∀p:sem_params.genv p globals →
    624   state_pc p → joint_closed_internal_function p globals → joint_statement p globals →
    625     IO io_out io_in (state_pc p) ≝
    626  λglobals,p,ge,st,curr_fn,stmt.
    627  match stmt with
    628  [ sequential s nxt ⇒
    629    ! 〈flow,st'〉 ← eval_step … ge curr_fn st s ;
    630    ! nxtptr ← succ_pc ? p (pc … st) nxt ;
    631    eval_step_flow … ge st' nxtptr flow
    632  | final s ⇒
    633    ! st' ← eval_fin_step_no_pc … ge curr_fn st s ;
    634    ! flow ← eval_fin_step_pc … ge curr_fn st s ;
    635    eval_fin_step_flow … ge st' (pc … st) flow
    636  ].
     736@(description_of_internal_function … prf)
     737qed.
    637738
    638739definition eval_state : ∀globals: list ident.∀p:sem_params. genv p globals →
     
    640741  λglobals,p,ge,st.
    641742  ! 〈fn,s〉 ← fetch_statement ? p … ge (pc … st) : IO ???;
    642   eval_statement … ge st fn s.
     743  eval_statement … ge fn st s.
    643744
    644745(* Paolo: what if in an intermediate language main finishes with an external
     
    648749  genv p globals → cpointer → state_pc p → option int ≝
    649750 λglobals,p,ge,exit,st.res_to_opt ? (
    650   do 〈fn,s〉 ← fetch_statement ? p … ge (pc … st);
     751  do 〈f,s〉 ← fetch_statement ? p … ge (pc … st);
     752  let fn ≝ if_of_function … f in
    651753  match s with
    652754  [ final s' ⇒
Note: See TracChangeset for help on using the changeset viewer.