Changeset 2395 for src/common


Ignore:
Timestamp:
Oct 12, 2012, 3:33:53 PM (7 years ago)
Author:
campbell
Message:

Proper handling of comparison of pointers off-the-end of an object.
We might need to drop this if the proofs/back-end work is too involved.

Location:
src/common
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/common/FrontEndMem.ma

    r2185 r2395  
    4646  | _ ⇒ None ? ].
    4747
    48 (* Only used by Clight semantics for pointer comparisons.  So in contrast to
    49    CompCert, we allow a pointer-to-one-off-the-end. *)
     48(* A pointer that can be dereferenced.  Only used for front-end pointer
     49   comparison at present. *)
    5050
    5151definition valid_pointer : mem → pointer → bool ≝
     
    5454  Zltb (block_id (pblock ptr)) (nextblock m) ∧
    5555  Zleb (low_bound m (pblock ptr)) off ∧
    56   Zleb off (high_bound m (pblock ptr)).
     56  Zltb off (high_bound m (pblock ptr)).
    5757
     58(* In contrast to CompCert, we also allow a pointer-to-one-off-the-end.  This is
     59   not entirely straightforward, as comparisons of an off-the-end pointer with a
     60   pointer from another block cannot be defined; if we did then we might change
     61   the result when coalescing blocks. *)
     62
     63definition end_pointer : mem → pointer → bool ≝
     64λm,ptr.
     65  let off ≝ Z_of_unsigned_bitvector … (offv (poff ptr)) in
     66  eqZb off (high_bound m (pblock ptr)).
     67
     68
  • src/common/FrontEndOps.ma

    r2177 r2395  
    1919
    2020include "common/Values.ma".
     21include "common/FrontEndMem.ma".
    2122
    2223inductive constant : typ → Type[0] ≝
     
    404405  | _ ⇒ None ? ].
    405406
    406 definition ev_cmpp ≝ λc: comparison. λv1,v2: val.
     407definition ev_cmpp ≝ λm. λc: comparison. λv1,v2: val.
    407408  match v1 with
    408409  [ Vptr ptr1 ⇒ match v2 with
    409410    [ Vptr ptr2 ⇒
    410         if eq_block (pblock ptr1) (pblock ptr2)
    411         then Some ? (FE_of_bool (cmp_offset c (poff ptr1) (poff ptr2)))
    412         else ev_cmp_mismatch c
     411        if eq_block (pblock ptr1) (pblock ptr2) then
     412          if (valid_pointer m ptr1 ∨ end_pointer m ptr1) ∧
     413             (valid_pointer m ptr2 ∨ end_pointer m ptr2)
     414          then Some ? (FE_of_bool (cmp_offset c (poff ptr1) (poff ptr2)))
     415          else None ?
     416        else
     417          if valid_pointer m ptr1 ∧
     418             valid_pointer m ptr2
     419          then ev_cmp_mismatch c
     420          else None ?
    413421    | Vnull  ⇒ ev_cmp_mismatch c
    414422    | _ ⇒ None ? ]
     
    437445  | _ ⇒ None ? ].
    438446
    439 definition eval_binop : ∀t1,t2,t'. binary_operation t1 t2 t' → val → val → option val ≝
    440 λt1,t2,t',op.
     447definition eval_binop : mem → ∀t1,t2,t'. binary_operation t1 t2 t' → val → val → option val ≝
     448λm,t1,t2,t',op.
    441449  match op with
    442450  [ Oadd _ _ ⇒ ev_add
     
    463471  | Osubpi _ ⇒ ev_subpi
    464472  | Osubpp sz ⇒ ev_subpp sz
    465   | Ocmpp _ c ⇒ ev_cmpp c
    466   ].
    467 
    468 lemma eval_binop_typ_correct : ∀t1,t2,t',op,v1,v2,v'.
     473  | Ocmpp _ c ⇒ ev_cmpp m c
     474  ].
     475
     476lemma eval_binop_typ_correct : ∀m,t1,t2,t',op,v1,v2,v'.
    469477  val_typ v1 t1 → val_typ v2 t2 →
    470   eval_binop t1 t2 t' op v1 v2 = Some ? v' →
     478  eval_binop m t1 t2 t' op v1 v2 = Some ? v' →
    471479  val_typ v' t'.
    472 #t1x #t2x #tx' *
     480#m #t1x #t2x #tx' *
    473481[ 1,2,3,8,9,10:
    474482  #sz #sg #v1 #v2 #v' #V1 #V2 @(elim_val_typ … V1) #i1 @(elim_val_typ … V2) #i2
     
    501509  whd in ⊢ (??%? → ?); [ 2: cases (eq_block ??) whd in ⊢ (??%? → ?); | ] #E destruct //
    502510| #sg' #c #v1 #v2 #v' #V1 #V2 @(elim_val_typ … V1) % [ 2: #b1 #o1 ] @(elim_val_typ … V2) % [ 2,4: #b2 #o2 ]
    503   whd in ⊢ (??%? → ?); [ cases (eq_block ??) cases (cmp_offset ???) ] cases c whd in ⊢ (??%? → ?); #E destruct //
     511  whd in ⊢ (??%? → ?); [ cases (andb ??) cases (andb ??) cases (eq_block ??) cases (cmp_offset ???) ] cases c whd in ⊢ (??%? → ?); #E destruct //
    504512] qed.
    505513
Note: See TracChangeset for help on using the changeset viewer.