Changeset 2564


Ignore:
Timestamp:
Dec 19, 2012, 12:46:59 PM (7 years ago)
Author:
piccolo
Message:

ERTL fully repaired, useless part of return value of pop_ra
removed.

Location:
src
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/semantics.ma

    r2563 r2564  
    117117  set_regs ERTL_state 〈\fst (regs … st),hwregs〉 st.
    118118
     119axiom FunctionNotFound: errmsg.
     120
    119121definition eval_ertl_seq:
    120  ∀globals. genv ERTL globals →
    121   ertl_seq → ident → joint_internal_function ERTL globals → state ERTL_state →
    122    IO io_out io_in (state ERTL_state) ≝
    123  λglobals,ge,stm,id,curr_fn,st.
    124  let framesize : Byte ≝ bitvector_of_nat 8 (joint_if_stacksize … curr_fn) in
     122 ∀F. ∀globals. genv_gen F globals →
     123  ertl_seq → ident → state ERTL_state →
     124   res (state ERTL_state) ≝
     125 λF,globals,ge,stm,id,st.
     126 ! framesize ← opt_to_res … FunctionNotFound  (stack_sizes … ge id);
     127 let framesize : Byte ≝ bitvector_of_nat 8 framesize in
    125128  match stm with
    126129   [ ertl_new_frame ⇒
     
    174177  (* snd_arg_retrieve_  ≝ *) ps_arg_retrieve
    175178  (* pair_reg_move_     ≝ *) ertl_eval_move
    176 (*  (* fetch_ra           ≝ *) ?(*(pop_ra …)*) *)
    177179  (* allocate_local     ≝ *) ertl_allocate_local
    178180  (* save_frame         ≝ *) ertl_save_frame
     
    184186  (* read_result        ≝ *) (λ_.λ_.λ_.
    185187     λst.return map ?? (hwreg_retrieve (\snd (regs … st))) RegisterRets)
    186   (* eval_ext_seq       ≝ *) ?(*eval_ertl_seq*)
    187 (*  (* eval_ext_tailcall  ≝ *) (λ_.λ_.λabs.match abs in void with [ ])
    188   (* eval_ext_call      ≝ *) (λ_.λ_.λabs.match abs in void with [ ]) *)
    189   (* pop_frame          ≝ *) ?(*(λ_.λ_.?(*return st_no_pc ? st*))*)
    190 (*  (* post_op2           ≝ *) (λ_.λ_.ertl_post_op2)) *)).
    191 [ (* pop_frame *) cases daemon (* Handle last-popped correctly *)
    192 | @eval_ertl_seq (* Handle type of call *)
    193 ]
     188  (* eval_ext_seq       ≝ *) (λgl,ge,stm,id.λ_.eval_ertl_seq F gl ge stm id)
     189  (* pop_frame          ≝ *) (λ_.λ_.λ_.λ_.pop_ra …)).
  • src/joint/semantics.ma

    r2562 r2564  
    9898 λp,s,st. mk_state_pc … s (pc … st) (last_pop … st).
    9999
    100 definition set_last_pop: ∀p. ? → state_pc p → state_pc p ≝
    101  λp,s,st. mk_state_pc … (st_no_pc … st) (pc … st) s.
     100definition set_last_pop: ∀p. ? → state p × program_counter → state_pc p ≝
     101 λp,s,st. mk_state_pc … (\fst … st) (\snd … st) s.
    102102
    103103definition set_frms: ∀p:sem_state_params. framesT p → state p → state p ≝
     
    199199    ident → F globals (* current *) → state st_pars → res (state st_pars)
    200200  ; pop_frame: ∀globals.∀ge : genv_gen F globals.
    201     ident → F globals (* current *) → state st_pars → res (state_pc st_pars)
     201    ident → F globals (* current *) → state st_pars → res (state st_pars × program_counter)
    202202  }.
    203203
     
    257257  push … st' addrh.
    258258
    259 definition pop_ra : ∀p.state p → res (program_counter × (state p)) ≝
     259definition pop_ra : ∀p.state p → res (state p × program_counter) ≝
    260260 λp,st.
    261261  ! 〈addrh, st'〉 ← pop … st;
    262262  ! 〈addrl, st''〉 ← pop … st';
    263263  ! pr ← pc_of_bevals [addrh; addrl];
    264   return 〈pr, st''〉.
     264  return 〈st'',pr〉.
    265265
    266266(* parameters that are defined by serialization *)
     
    553553λst : state p.
    554554! st' ← pop_frame … ge curr_id curr_fn st ;
    555 ! nxt ← next_of_call_pc … ge (pc … st') ;
     555! nxt ← next_of_call_pc … ge (\snd … st') ;
    556556return
    557   set_last_pop … (pc … st') (next … nxt st') (* now address pushed on stack are calling ones! *).
     557  next … nxt (set_last_pop … (\snd … st') st') (* now address pushed on stack are calling ones! *).
    558558
    559559definition eval_tailcall ≝
     
    631631    [ RETURN ⇒
    632632      do st' ← pop_frame … ge id fn st;
    633       if eq_program_counter (pc … st') exit then
     633      if eq_program_counter (\snd … st') exit then
    634634      do vals ← read_result … ge (joint_if_result … fn) st ;
    635635        Word_of_list_beval vals
Note: See TracChangeset for help on using the changeset viewer.