Changeset 3265


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

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

Location:
src
Files:
6 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
  • src/LIN/joint_LTL_LIN_semantics.ma

    r3261 r3265  
    9494  λst.return map … (hwreg_retrieve (regs … st)) RegisterRets)
    9595  (* eval_ext_seq       ≝ *) (eval_LTL_LIN_ext_seq ?)
    96   (* pop_frame          ≝ *) ((λ_.λ_.λ_.λ_.λst.pop_ra … st)).
     96  (* pop_frame          ≝ *) ((λ_.λ_.λ_.λ_.λst.pop_ra … st))
     97  (* validate_pointer   ≝ *) (λ_.λ_.λ_.λ_.λ_.return it).
  • src/RTL/RTL_semantics.ma

    r3261 r3265  
    5252    (λenv.OK … (stackp env))
    5353    (λenv.mk_reg_sp env (* coercion*)).
     54
     55(* in separate stacks, when a pointer has the same block that a stack pointer
     56   in frame, either it is correct or we can immediately fire an error.
     57   If the ptr's block is not any of the stack pointer blocks, we suppose
     58   it's pointing to a global and we accept it. *)
     59definition RTL_separate_validate_pointer : ∀F. ∀globals. genv_gen F globals →
     60  ident → state RTL_state_params → pointer → res unit ≝
     61λF,globals,ge,curr_id,st,ptr.
     62! bl ← opt_to_res … [MSG BadFunction; CTX … curr_id]
     63  (! bl ← find_symbol … ge curr_id ; code_block_of_block bl) ;
     64! 〈ign, f〉 ← fetch_internal_function … ge bl ;
     65if eq_block (pblock ptr) (pblock (stackp (regs … st))) ∧
     66  leb (get_joint_if_local_stacksize … ge f)
     67    (nat_of_bitvector … (offv (poff ptr))) then
     68  Error … (msg BadPointer)
     69else
     70  ! frms ← opt_to_res ? (msg FrameErrorOnPop) (st_frms ? st) ;
     71  m_fold ??? (λfr.λ_.
     72    ! 〈ign, f〉 ← fetch_internal_function … ge (pc_block (fr_pc fr)) ;
     73    if eq_block (pblock ptr) (pblock (stackp (fr_regs fr))) ∧
     74      leb (get_joint_if_local_stacksize … ge f)
     75        (nat_of_bitvector … (offv (poff ptr))) then
     76       Error … (msg BadPointer)
     77    else return it) frms it.
     78 
     79(* when the stack is unique, the stack block is already present in the state
     80   that we are analysing.
     81   If the ptr's block is not it, we suppose
     82   it's pointing to a global and we accept it. *)
     83definition RTL_unique_validate_pointer : ∀F. ∀globals. genv_gen F globals →
     84  ident → state RTL_state_params → pointer → res unit ≝
     85λF,globals,ge,curr_id,st,ptr.
     86let sp ≝ stackp (regs … st) in
     87if eq_block (pblock ptr) (pblock sp) then
     88  let off ≝
     89    λsp : pointer.Z_of_unsigned_bitvector … (offv (poff ptr)) -
     90        Z_of_unsigned_bitvector … (offv (poff sp)) in
     91  ! bl ← opt_to_res … [MSG BadFunction; CTX … curr_id]
     92    (! bl ← find_symbol … ge curr_id ; code_block_of_block bl) ;
     93  ! 〈ign, f〉 ← fetch_internal_function … ge bl ;
     94  let o' ≝ off sp in
     95  if Zltb o' 0 ∨ Zleb (get_joint_if_local_stacksize … ge f) o' then
     96    Error … (msg BadPointer)
     97  else
     98    ! frms ← opt_to_res ? (msg FrameErrorOnPop) (st_frms ? st) ;
     99    m_fold ??? (λfr.λ_.
     100      ! 〈ign, f〉 ← fetch_internal_function … ge (pc_block (fr_pc fr)) ;
     101      let o' ≝ off (stackp (fr_regs fr)) in
     102      if Zltb o' 0 ∨ Zleb (get_joint_if_local_stacksize … ge f) o' then
     103         Error … (msg BadPointer)
     104      else return it) frms it
     105else return it.
    54106
    55107definition RTL_state ≝ state RTL_state_params.
     
    249301      (λ_.λ_.rtl_read_result) 
    250302      (λ_.λ_.eval_rtl_seq)
    251       (λ_.λ_.λ_.rtl_pop_frame_separate))
     303      (λ_.λ_.λ_.rtl_pop_frame_separate)
     304      (RTL_separate_validate_pointer …))
    252305    RTL_premain.
    253306
     
    273326      (λ_.λ_.rtl_read_result) 
    274327      (λ_.λ_.eval_rtl_seq)
    275       (λ_.λ_.λ_.rtl_pop_frame_separate))
     328      (λ_.λ_.λ_.rtl_pop_frame_separate)
     329      (RTL_separate_validate_pointer …))
    276330    RTL_premain.
    277331
     
    297351      (λ_.λ_.rtl_read_result) 
    298352      (λ_.λ_.eval_rtl_seq)
    299       (λ_.λ_.λ_.rtl_pop_frame_unique))
     353      (λ_.λ_.λ_.rtl_pop_frame_unique)
     354      (RTL_unique_validate_pointer …))
    300355    RTL_premain.
    301      
  • src/joint/joint_semantics.ma

    r3261 r3265  
    2121; pc_from_label : (Σbl.block_region bl = Code) → F globals → label →
    2222    option program_counter
     23; get_joint_if_local_stacksize : F globals → ℕ
     24; get_joint_if_params_stacksize : F globals → ℕ
    2325}.
    2426
     
    237239    ident (* current *) → call_dest uns_pars (* current ret *) →
    238240      state st_pars → res (state st_pars × program_counter)
     241  (* filter parts of the stack that are accessible *)
     242  ; validate_pointer : ∀globals.∀ge : genv_gen F globals.
     243    ident (* current *) → state st_pars → pointer → res unit
    239244  }.
    240245
     
    458463    ! vaddrl ← dpl_arg_retrieve … st addrl;
    459464    ! vaddr ← pointer_of_address 〈vaddrl,vaddrh〉;
     465    !_ validate_pointer … ge curr_id st vaddr ;
    460466    ! v ← opt_to_res … (msg FailedLoad) (beloadv (m … st) vaddr);
    461467    acca_store p … dst v st
     
    464470    ! vaddrl ← dpl_arg_retrieve … st addrl;
    465471    ! vaddr ← pointer_of_address 〈vaddrl,vaddrh〉;
     472    !_ validate_pointer … ge curr_id st vaddr ;
    466473    ! v ← acca_arg_retrieve … st src;
    467474    ! m' ← opt_to_res … (msg FailedStore) (bestorev (m … st) vaddr v);
  • src/joint/semanticsUtils.ma

    r3037 r3265  
    408408  ! pt ← point_of_label … (joint_if_code … fn) lbl ;
    409409  return mk_program_counter bl (offset_of_point … p pt) in
    410 mk_genv_gen ?? genv ? stacksizes (pre_main_generator … p prog) pc_from_lbl.
     410mk_genv_gen ?? genv ? stacksizes (pre_main_generator … p prog) pc_from_lbl
     411(joint_if_local_stacksize …) (joint_if_params_stacksize …).
    411412#s #H
    412413cases (find_symbol_exists ?? (λx.x) … prog s ?)
Note: See TracChangeset for help on using the changeset viewer.