Ignore:
Timestamp:
Apr 17, 2013, 2:53:45 PM (7 years ago)
Author:
piccolo
Message:

1) changed block_of_call in order to prevent pre-main calls
2) StatusSimulationHelper? in place

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/joint_semantics.ma

    r3037 r3154  
    516516  ! bl ← match f with
    517517    [ inl id ⇒
    518       opt_to_res … [MSG BadFunction; CTX … id]
    519         (find_symbol … ge id)
     518      !bl ← opt_to_res … [MSG BadFunction; CTX … id] (find_symbol … ge id) ;
     519      if eqZb (block_id bl) (-1) then
     520        Error … [MSG BadFunction; CTX … id]
     521      else return bl
    520522    | inr addr ⇒
    521523      ! addr_l ← dpl_arg_retrieve … st (\fst addr) ;
    522524      ! addr_h ← dph_arg_retrieve … st (\snd addr) ;
    523525      ! ptr ← pointer_of_bevals … [addr_l ; addr_h ] ;
    524       if eq_bv … (bv_zero …) (offv (poff ptr)) then
     526      if eq_bv … (bv_zero …) (offv (poff ptr)) ∧
     527         (notb (eqZb (block_id (pblock ptr)) (-1))) then
    525528        return pblock ptr
    526529      else
     
    529532  opt_to_res … [MSG BadFunction; MSG BadPointer]
    530533    (code_block_of_block bl).
     534
     535lemma match_reg_elim : ∀ A : Type[0]. ∀ P : A → Prop. ∀ r : region.
     536∀f : (r = XData) → A. ∀g : (r = Code) → A. (∀ prf : r = XData.P (f prf)) →
     537(∀ prf : r = Code.P (g prf)) →
     538P ((match r return λx.(r = x → ?) with
     539    [XData ⇒ f | Code ⇒ g])(refl ? r)).
     540#A #P * #f #g #H1 #H2 normalize nodelta [ @H1 | @H2]
     541qed.
     542
     543lemma block_of_call_no_minus_one : ∀p,globals,ge,f,st,bl.
     544block_of_call p globals ge f st = return bl →
     545block_id bl ≠ -1.
     546#p #globals #ge #f #st #bl whd in match block_of_call; normalize nodelta
     547#H cases(bind_inversion ????? H) #bl1 cases f -f normalize nodelta
     548[ #id * #H cases(bind_inversion ????? H) -H #bl2 * #_ @eqZb_elim #EQbl2
     549  normalize nodelta whd in ⊢ (??%% → ?); #EQ destruct(EQ)
     550  #H lapply(opt_eq_from_res ???? H) -H whd in match code_block_of_block;
     551  normalize nodelta @match_reg_elim [ #_ #EQ destruct] #prf #EQ destruct(EQ)
     552  assumption
     553| * #dpl #dph * #H cases(bind_inversion ????? H) -H #bv1 * #_ #H
     554  cases(bind_inversion ????? H) -H #bv2 * #_ #H cases(bind_inversion ????? H) -H
     555  #ptr * #_ @eq_bv_elim #_ normalize nodelta [2: whd in ⊢ (??%% → ?); #EQ destruct]
     556  @eqZb_elim #EQptr normalize nodelta whd in ⊢ (??%% → ?); #EQ destruct
     557  #H lapply(opt_eq_from_res ???? H) -H whd in match code_block_of_block;
     558  normalize nodelta @match_reg_elim [#_ #EQ destruct] #prf #EQ destruct
     559  assumption
     560]
     561qed.
     562
    531563
    532564definition eval_external_call ≝
Note: See TracChangeset for help on using the changeset viewer.