Changeset 2395 for src/Clight


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/Clight
Files:
2 added
2 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%
Note: See TracChangeset for help on using the changeset viewer.