Changeset 2395


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
Files:
2 added
6 edited
1 copied

Legend:

Unmodified
Added
Removed
  • src/Clight/Csem.ma

    r2391 r2395  
    348348        match v2 with
    349349        [ Vptr ptr2 ⇒
    350           if valid_pointer m ptr1
    351           ∧ valid_pointer m ptr2 then
    352             if eq_block (pblock ptr1) (pblock ptr2)
     350          (* Pointers one-off-the-end require careful treatment - they may end
     351             up equal to a pointer to another object.  I don't think we have
     352             the corresponding definitions in the back-end, so we may need to
     353             compromise on this; if so, the pointer comparison in FrontEndOps
     354             will need changed too. *)
     355          if eq_block (pblock ptr1) (pblock ptr2) then
     356            if (valid_pointer m ptr1 ∨ end_pointer m ptr1) ∧
     357               (valid_pointer m ptr2 ∨ end_pointer m ptr2)
    353358            then Some ? (of_bool (cmp_offset c (poff ptr1) (poff ptr2)))
    354             else sem_cmp_mismatch c
    355           else None ?
     359            else None ?
     360          else
     361            if valid_pointer m ptr1 ∧
     362               valid_pointer m ptr2
     363            then sem_cmp_mismatch c
     364            else None ?
    356365        | Vnull ⇒ sem_cmp_mismatch c
    357366        | _ ⇒ None ? ]
  • src/Clight/test/endptr.test.ma

    r2393 r2395  
    11include "Clight/test/endptr.c.ma".
    22
    3 example exec: result ? (exec_up_to clight_fullexec myprog 1000 [ ]).
     3example exec: exec_up_to clight_fullexec myprog 1000 [ ] = Error ? (msg FailedOp).
    44normalize  (* you can examine the result here *)
    55%
     
    99include "Clight/toCminor.ma".
    1010include "Cminor/semantics.ma".
     11
     12(* This succeeds because the variables have been arranged in the stack frame. *)
    1113
    1214example e1: result ?
  • src/Clight/test/endptr2.test.ma

    r2393 r2395  
    1 include "Clight/test/endptr.c.ma".
     1include "Clight/test/endptr2.c.ma".
    22
    3 example exec: result ? (exec_up_to clight_fullexec myprog 1000 [ ]).
     3example exec: exec_up_to clight_fullexec myprog 1000 [ ] = Error ? (msg FailedOp).
    44normalize  (* you can examine the result here *)
    55%
     
    1010include "Cminor/semantics.ma".
    1111
    12 example e1: result ?
     12example e1:
    1313  (bind ? (snapshot state) (clight_to_cminor (simplify_program myprog))
    14    (λp. exec_up_to Cminor_fullexec p 1000 [ ])).
     14   (λp. exec_up_to Cminor_fullexec p 1000 [ ]))
     15  = Error ? (msg FailedOp).
    1516normalize
    1617%
     
    2122include "Clight/label.ma".
    2223
    23 example e2: result ? (
     24example e2:
    2425let 〈p0,init〉 ≝ clight_label myprog in
    2526bind ? (snapshot state) (clight_to_cminor (simplify_program p0))
    2627(λp1. let p2 ≝ cminor_to_rtlabs init p1 in
    27   exec_up_to RTLabs_fullexec p2 1000 [ ])).
     28  exec_up_to RTLabs_fullexec p2 1000 [ ])
     29= Error ? (msg FailedOp).
    2830normalize
    2931%
  • src/Cminor/semantics.ma

    r2254 r2395  
    104104    do 〈tr1,v1〉 ← eval_expr ge ? e1 en ? sp m;
    105105    do 〈tr2,v2〉 ← eval_expr ge ? e2 en ? sp m;
    106     do r ← opt_to_res … (msg FailedOp) (eval_binop ??? op v1 v2);
     106    do r ← opt_to_res … (msg FailedOp) (eval_binop m ??? op v1 v2);
    107107    OK ? 〈tr1 ⧺ tr2, r〉
    108108| Mem ty e ⇒ λEnv.
  • src/RTLabs/semantics.ma

    r2296 r2395  
    105105      ! v1 ← reg_retrieve (locals f) src1;
    106106      ! v2 ← reg_retrieve (locals f) src2;
    107       ! v' ← opt_to_res … (msg FailedOp) (eval_binop ??? op v1 v2);
     107      ! v' ← opt_to_res … (msg FailedOp) (eval_binop m ??? op v1 v2);
    108108      ! locals ← reg_store dst v' (locals f);
    109109      return 〈E0, State (mk_frame (func f) locals l ? (sp f) (retdst f)) fs m〉
  • 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.