Changeset 2395 for src/Clight

Timestamp:

Oct 12, 2012, 3:33:53 PM (9 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:

• Csem.ma (modified) (1 diff)
• test/endptr.test.ma (modified) (2 diffs)
• test/endptr2.c (added)
• test/endptr2.c.ma (added)
• test/endptr2.test.ma (copied) (copied from src/Clight/test/endptr.test.ma) (3 diffs)

src/Clight/Csem.ma

@@ -348 +348 @@
         match v2 with
         [ Vptr ptr2 ⇒
-          if valid_pointer m ptr1
-          ∧ valid_pointer m ptr2 then
-            if eq_block (pblock ptr1) (pblock ptr2)
+          (* Pointers one-off-the-end require careful treatment - they may end
+             up equal to a pointer to another object.  I don't think we have
+             the corresponding definitions in the back-end, so we may need to
+             compromise on this; if so, the pointer comparison in FrontEndOps
+             will need changed too. *)
+          if eq_block (pblock ptr1) (pblock ptr2) then
+            if (valid_pointer m ptr1 ∨ end_pointer m ptr1) ∧
+               (valid_pointer m ptr2 ∨ end_pointer m ptr2)
             then Some ? (of_bool (cmp_offset c (poff ptr1) (poff ptr2)))
-            else sem_cmp_mismatch c
-          else None ?
+            else None ?
+          else
+            if valid_pointer m ptr1 ∧
+               valid_pointer m ptr2
+            then sem_cmp_mismatch c
+            else None ?
         | Vnull ⇒ sem_cmp_mismatch c
         | _ ⇒ None ? ]

src/Clight/test/endptr.test.ma

@@ -1 +1 @@
 include "Clight/test/endptr.c.ma".
 
-example exec: result ? (exec_up_to clight_fullexec myprog 1000 [ ]).
+example exec: exec_up_to clight_fullexec myprog 1000 [ ] = Error ? (msg FailedOp).
 normalize  (* you can examine the result here *)
 %
@@ -9 +9 @@
 include "Clight/toCminor.ma".
 include "Cminor/semantics.ma".
+
+(* This succeeds because the variables have been arranged in the stack frame. *)
 
 example e1: result ?

src/Clight/test/endptr2.test.ma

@@ -1 @@
-include "Clight/test/endptr.c.ma".
+include "Clight/test/endptr2.c.ma".
 
-example exec: result ? (exec_up_to clight_fullexec myprog 1000 [ ]).
+example exec: exec_up_to clight_fullexec myprog 1000 [ ] = Error ? (msg FailedOp).
 normalize  (* you can examine the result here *)
 %
@@ -10 +10 @@
 include "Cminor/semantics.ma".
 
-example e1: result ?
+example e1: 
   (bind ? (snapshot state) (clight_to_cminor (simplify_program myprog))
-   (λp. exec_up_to Cminor_fullexec p 1000 [ ])).
+   (λp. exec_up_to Cminor_fullexec p 1000 [ ]))
+  = Error ? (msg FailedOp).
 normalize
 %
@@ -21 +22 @@
 include "Clight/label.ma".
 
-example e2: result ? (
+example e2: 
 let 〈p0,init〉 ≝ clight_label myprog in
 bind ? (snapshot state) (clight_to_cminor (simplify_program p0))
 (λp1. let p2 ≝ cminor_to_rtlabs init p1 in
-  exec_up_to RTLabs_fullexec p2 1000 [ ])).
+  exec_up_to RTLabs_fullexec p2 1000 [ ])
+= Error ? (msg FailedOp).
 normalize
 %