Changeset 3265 for src/ERTL


Ignore:
Timestamp:
May 10, 2013, 6:21:46 PM (7 years ago)
Author:
tranquil
Message:

added validate_pointer filter
in Interference added that intereference only fires on non eliminable
statements

Location:
src/ERTL
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTL_semantics.ma

    r3262 r3265  
    3838{ psd_reg_env : register_env beval
    3939; funct_block : Σb:block.block_region b=Code
    40 ; callee_values : list beval
     40; fr_sp : xpointer (* just for correctness *)
    4141}.
    4242
     
    4949 (*load_sp ≝ *) get_hwsp
    5050 (*save_sp ≝ *) set_hwsp.
     51 
     52(* when the stack is unique, the stack block is already present in the state
     53   that we are analysing.
     54   If the ptr's block is not it, we suppose
     55   it's pointing to a global and we accept it. *)
     56definition ERTL_validate_pointer : ∀F. ∀globals. genv_gen F globals →
     57  ident → state ERTL_state → pointer → res unit ≝
     58λF,globals,ge,curr_id,st,ptr.
     59! sp ← sp … st ;
     60if eq_block (pblock ptr) (pblock sp) then
     61  let off ≝
     62    λsp : pointer.Z_of_unsigned_bitvector … (offv (poff ptr)) -
     63        Z_of_unsigned_bitvector … (offv (poff sp)) in
     64  ! bl ← opt_to_res … [MSG BadFunction; CTX … curr_id]
     65    (! bl ← find_symbol … ge curr_id ; code_block_of_block bl) ;
     66  ! 〈ign, f〉 ← fetch_internal_function … ge bl ;
     67  ! ss ← opt_to_res ? [MSG BadFunction; CTX … curr_id ] (stack_sizes … ge curr_id) ;
     68  let o' ≝ off sp in
     69  if Zltb o' 0 ∨
     70    (Zleb (get_joint_if_local_stacksize … ge f) o' ∧
     71     Zltb o' (minus ss (get_joint_if_params_stacksize … ge f))) ∨
     72    Zleb ss o' then
     73    Error … (msg BadPointer)
     74  else
     75    ! frms ← opt_to_res ? (msg FrameErrorOnPop) (st_frms ? st) ;
     76    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
     83        Error … (msg BadPointer)
     84      else return it) frms it
     85else return it.
    5186
    5287(* we ignore need_spilled_no as we never move framesize based values around in the
     
    75110  ! st' ← push_ra … st (pc … st) ;
    76111  ! frms ← opt_to_res ? [MSG FrameErrorOnPush] (st_frms … st');
    77   let callee_val ≝ map … (λr.hwreg_retrieve (\snd (regs …  st')) r)
    78                     RegisterCalleeSaved in
     112  ! sp ← sp … st ;
    79113  return
    80114  (set_frms ERTL_state
    81   ((mk_ERTL_frame (\fst (regs ERTL_state st')) (pc_block (pc ? st))
    82      callee_val) :: frms)
     115  ((mk_ERTL_frame (\fst (regs ERTL_state st')) (pc_block (pc ? st)) sp) :: frms)
    83116    (set_regs ERTL_state 〈empty_map …,\snd (regs … st')〉 st')).
    84117
    85 definition callee_values_ok : hw_register_env → list beval → bool ≝
    86 λregs,l.true (*waiting for Paolo's function*).
    87 
    88 
     118(* Paolo: maybe insert a check that stack pointer is restored after return? *)
    89119definition ertl_pop_frame:
    90120 ∀F. ∀globals. genv_gen F globals → ident →  state ERTL_state →
     
    95125 [ nil ⇒ Error ? [MSG FramesEmptyOnPop]
    96126 | cons hd tl ⇒
    97    if callee_values_ok (\snd (regs … st)) (callee_values hd) then
    98127    let st' ≝ set_regs ERTL_state 〈(psd_reg_env hd), \snd (regs … st)〉
    99128       (set_frms ERTL_state tl st) in
     
    106135      OK … 〈set_sp … newsp st'', pc〉
    107136    else Error ? [MSG BlockInFramesCorrupted]
    108    else Error ? [MSG BadRegister]
    109137 ].
    110138@hide_prf whd in match newsp; cases sp #ptr #EQ <EQ % qed.
     
    196224     λst.return map ?? (hwreg_retrieve (\snd (regs … st))) RegisterRets)
    197225  (* eval_ext_seq       ≝ *) (λgl,ge,stm,id.eval_ertl_seq F gl ge stm id)
    198   (* pop_frame          ≝ *) (λglobals,ge,id.λ_.λst.ertl_pop_frame F globals ge id st).
     226  (* pop_frame          ≝ *) (λglobals,ge,id.λ_.λst.ertl_pop_frame F globals ge id st)
     227  (* validate_pointer   ≝ *) (ERTL_validate_pointer …).
    199228
    200229definition ERTL_semantics ≝
  • src/ERTL/Interference.ma

    r3263 r3265  
    5050[ None ⇒ false
    5151| Some s ⇒
     52  ¬eliminable … (liveafter l) s ∧
    5253  in_lattice v1 (defined … s) ∧ in_lattice v2 (liveafter l) ∧
    5354  ¬is_src_of_move … s v2
Note: See TracChangeset for help on using the changeset viewer.