Ignore:
Timestamp:
Jun 26, 2013, 2:22:28 PM (6 years ago)
Author:
piccolo
Message:

Modified RTLsemantics and ERTLsemantics. Now the pop frame will set
to undef the carry bit and all RegisterCallerSaved? exept those used to
pass the return value of a function.

Added an overflow check in ERTL_semantics

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTL_semantics.ma

    r3265 r3371  
    3737record ERTL_frame : Type[0] ≝
    3838{ psd_reg_env : register_env beval
    39 ; funct_block : Σb:block.block_region b=Code
    40 ; fr_sp : xpointer (* just for correctness *)
     39; funct_pc : program_counter
     40; funct_sp : xpointer (* just for correctness *)
    4141}.
    4242
     
    6767  ! ss ← opt_to_res ? [MSG BadFunction; CTX … curr_id ] (stack_sizes … ge curr_id) ;
    6868  let o' ≝ off sp in
    69   if Zltb o' 0 ∨
    70     (Zleb (get_joint_if_local_stacksize … ge f) o' ∧
     69  if (Zleb (get_joint_if_local_stacksize … ge f) o' ∧
    7170     Zltb o' (minus ss (get_joint_if_params_stacksize … ge f))) ∨
    7271    Zleb ss o' then
     
    7574    ! frms ← opt_to_res ? (msg FrameErrorOnPop) (st_frms ? st) ;
    7675    m_fold ??? (λfr.λ_.
    77       ! 〈ign, f〉 ← fetch_internal_function … ge (funct_block fr) ;
    78       let o' ≝ off (fr_sp fr) in
    79       if Zltb o' 0 ∨
    80         (Zleb (get_joint_if_local_stacksize … ge f) o' ∧
    81          Zltb o' (minus ss (get_joint_if_params_stacksize … ge f))) ∨
    82         Zleb ss o' then
     76      ! 〈ign, f〉 ← fetch_internal_function … ge (pc_block (funct_pc fr)) ;
     77      let o' ≝ off (funct_sp fr) in
     78      if Zleb (get_joint_if_local_stacksize … ge f) o' ∧
     79         Zltb o' (minus ss (get_joint_if_params_stacksize … ge f)) then
    8380        Error … (msg BadPointer)
    8481      else return it) frms it
     
    113110  return
    114111  (set_frms ERTL_state
    115   ((mk_ERTL_frame (\fst (regs ERTL_state st')) (pc_block (pc ? st)) sp) :: frms)
     112  ((mk_ERTL_frame (\fst (regs ERTL_state st')) (pc ? st) sp) :: frms)
    116113    (set_regs ERTL_state 〈empty_map …,\snd (regs … st')〉 st')).
    117114
     
    128125       (set_frms ERTL_state tl st) in
    129126    ! 〈st'', pc〉 ← pop_ra … st' ;
    130     if eq_block (funct_block hd) (pc_block pc) then
     127    if eq_program_counter (funct_pc hd) pc then
    131128      ! sp ← sp … st'' ;
    132       ! framesize ← opt_to_res (msg FunctionNotFound) (stack_sizes … ge id);
     129      ! framesize ← opt_to_res ? (msg FunctionNotFound) (stack_sizes … ge id);
    133130      let framesize : Byte ≝ bitvector_of_nat 8 framesize in
    134131      let newsp ≝ shift_pointer … sp framesize in
    135       OK … 〈set_sp … newsp st'', pc〉
     132      let cs_regs : hw_register_env ≝
     133        foldl ?? (λregs,r.hwreg_store r BVundef regs) (\snd (regs …st''))
     134          (filter ? (λr.all … (λx.¬ eq_Register r x) RegisterRets)  RegisterCallerSaved)
     135       in
     136      OK … 〈set_sp ? newsp (set_regs ERTL_state 〈\fst (regs … st''),cs_regs〉
     137                            (set_carry ? BBundef st'')), pc〉
    136138    else Error ? [MSG BlockInFramesCorrupted]
    137139 ].
     
    159161  return set_regs ERTL_state env' st.
    160162
     163include alias "arithmetics/nat.ma".
    161164
    162165definition ertl_setup_call : ℕ → state ERTL_state → res (state ERTL_state) ≝
    163166λframesize,st.
    164167  ! sp ← sp … st ;
    165   let framesize : Byte ≝ bitvector_of_nat 8 framesize in
    166   let newsp ≝ neg_shift_pointer … sp framesize in
    167   return set_sp … newsp st.
     168  if leb (S (framesize + (stack_usage … st))) (2^16) then
     169   let framesize : Byte ≝ bitvector_of_nat 8 framesize in
     170   let newsp ≝ neg_shift_pointer … sp framesize in
     171   return set_sp … newsp st
     172  else
     173   Error … [MSG StackOverflow].
    168174@hide_prf whd in match newsp; cases sp #ptr #EQ <EQ % qed.
    169175 
Note: See TracChangeset for help on using the changeset viewer.