CN VIP: Add bounds checks for ptr relops

This commit implements the VIP typing rules for pointer relational (<,
>, >=, <=) operators, for which both operands must be of the same live
allocation.

backend/cn/lib/check.ml

@@ -451,7 +451,7 @@ let check_alloc_bounds loc ~ptr ub_unspec =
     return ()
 
 
-let check_both_eq_alloc loc arg1 arg2 ub_unspec =
+let check_both_eq_alloc loc arg1 arg2 ub =
   let here = Locations.other __FUNCTION__ in
   let both_alloc =
     and_
@@ -461,7 +461,6 @@ let check_both_eq_alloc loc arg1 arg2 ub_unspec =
       ]
       here
   in
-  let ub = CF.Undefined.(UB_CERB004_unspecified ub_unspec) in
   let@ provable = provable loc in
   match provable @@ LC.T both_alloc with
   | `False ->
@@ -470,8 +469,8 @@ let check_both_eq_alloc loc arg1 arg2 ub_unspec =
   | `True -> return ()
 
 
-let check_live_alloc_bounds loc arg ub_unspec constr =
-  let@ base_size = RI.Special.get_live_alloc loc Ptr_diff arg in
+let check_live_alloc_bounds loc arg ub constr =
+  let@ base_size = RI.Special.get_live_alloc loc Ptr_diff_or_compare arg in
   let here = Locations.other __FUNCTION__ in
   let base, size = Alloc.History.get_base_size base_size here in
   if !use_vip then (
@@ -481,7 +480,6 @@ let check_live_alloc_bounds loc arg ub_unspec constr =
     | `True -> return ()
     | `False ->
       let@ model = model () in
-      let ub = CF.Undefined.(UB_CERB004_unspecified ub_unspec) in
       fail (fun ctxt -> { loc; msg = Undefined_behaviour { ub; ctxt; model } }))
   else
     return ()
@@ -1372,10 +1370,15 @@ let rec check_expr labels (e : BT.t Mu.mu_expr) (k : IT.t -> unit m) : unit m =
          and_ [ lower1; lower2; upper1; upper2 ] here
        in
        let pointer_op op pe1 pe2 =
+         let ub = CF.Undefined.UB053_distinct_aggregate_union_pointer_comparison in
          let@ () = ensure_base_type loc ~expect Bool in
          let@ () = ensure_base_type loc ~expect:(Loc ()) (Mu.bt_of_pexpr pe1) in
          let@ () = ensure_base_type loc ~expect:(Loc ()) (Mu.bt_of_pexpr pe2) in
-         check_pexpr pe1 (fun arg1 -> check_pexpr pe2 (fun arg2 -> k (op (arg1, arg2))))
+         check_pexpr pe1 (fun arg1 ->
+           check_pexpr pe2 (fun arg2 ->
+             let@ () = check_both_eq_alloc loc arg1 arg2 ub in
+             let@ () = check_live_alloc_bounds loc arg1 ub (both_in_bounds arg1 arg2) in
+             k (op (arg1, arg2))))
        in
        (match memop with
         | M_PtrEq (pe1, pe2) -> pointer_eq pe1 pe2
@@ -1398,10 +1401,9 @@ let rec check_expr labels (e : BT.t Mu.mu_expr) (k : IT.t -> unit m) : unit m =
                 | ct -> Memory.size_of_ctype ct
               in
               let ub_unspec = CF.Undefined.UB_unspec_pointer_sub in
-              let@ () = check_both_eq_alloc loc arg1 arg2 ub_unspec in
-              let@ () =
-                check_live_alloc_bounds loc arg1 ub_unspec (both_in_bounds arg1 arg2)
-              in
+              let ub = CF.Undefined.(UB_CERB004_unspecified ub_unspec) in
+              let@ () = check_both_eq_alloc loc arg1 arg2 ub in
+              let@ () = check_live_alloc_bounds loc arg1 ub (both_in_bounds arg1 arg2) in
               let ptr_diff_bt = Memory.bt_of_sct (Integer Ptrdiff_t) in
               let value =
                 (* TODO: confirm that the cast from uintptr_t to ptrdiff_t
@@ -1477,11 +1479,12 @@ let rec check_expr labels (e : BT.t Mu.mu_expr) (k : IT.t -> unit m) : unit m =
               let result =
                 arrayShift_ ~base:vt1 ~index:(cast_ Memory.uintptr_bt vt2 loc) act.ct loc
               in
-              let unspec = CF.Undefined.UB_unspec_pointer_add in
-              let@ () = check_has_alloc_id loc vt1 unspec in
+              let ub_unspec = CF.Undefined.UB_unspec_pointer_add in
+              let ub = CF.Undefined.(UB_CERB004_unspecified ub_unspec) in
+              let@ () = check_has_alloc_id loc vt1 ub_unspec in
               let here = Locations.other __FUNCTION__ in
               let@ () =
-                check_live_alloc_bounds loc vt1 unspec (fun ~base ~size ->
+                check_live_alloc_bounds loc vt1 ub (fun ~base ~size ->
                   let addr = addr_ result here in
                   let lower = le_ (base, addr) here in
                   let upper = le_ (addr, add_ (base, size) here) here in

backend/cn/lib/typeErrors.ml

@@ -37,7 +37,7 @@ let call_prefix = function
 
 
 type situation =
-  | Ptr_diff
+  | Ptr_diff_or_compare
   | Access of access
   | Call of call_situation
 
@@ -59,7 +59,7 @@ let call_situation = function
 
 let checking_situation = function
   | Access _ -> !^"checking access"
-  | Ptr_diff -> !^"checking pointer difference"
+  | Ptr_diff_or_compare -> !^"checking pointer difference or comparison"
   | Call s -> call_situation s
 
 
@@ -73,7 +73,7 @@ let for_access = function
 
 let for_situation = function
   | Access access -> for_access access
-  | Ptr_diff -> !^"for subtracting pointers"
+  | Ptr_diff_or_compare -> !^"for subtracting or comparing pointers"
   | Call s ->
     (match s with
      | FunctionCall fsym -> !^"for calling function" ^^^ Sym.pp fsym

tests/cn/ptr_relop.c

@@ -0,0 +1,85 @@
+int live_owned_footprint(char *p, char *q)
+/*@
+ requires
+    take P = Owned<int[11]>(array_shift<char>(p, -2i64));
+    ptr_eq(q, array_shift<char>(p, 12i64));
+ensures
+    take P2 = Owned<int[11]>(array_shift<char>(p, -2i64));
+    P == P2;
+    return == 0i32;
+@*/
+{
+  /*@ extract Owned<int>, 7u64; @*/
+  // NOTE: neither argument needs to be in the footprint of the Owned
+  // The bounds check for the allocation are done separately to the resource
+  // lookup
+  return q < p;
+}
+
+// Here, only one ownership is required to establish the that the allocation is
+// live, but both are required to ensure that the bounds check succeeds
+int live_owned_both(int *p, int *q)
+/*@
+ requires
+    take P = Owned(p);
+    take Q = Owned(q);
+    (u64) p < (u64) q;
+    ptr_eq(q, array_shift(p, 10i32));
+ensures
+    take P2 = Owned(p);
+    P == P2;
+    take Q2 = Owned(q);
+    Q == Q2;
+    return == 0i32;
+@*/
+{
+  return p > q;
+}
+
+int live_owned_one(int *p, int *q)
+/*@
+ requires
+    take P = Owned(p);
+    ptr_eq(q, array_shift(p, 10i32));
+    let A = allocs[(alloc_id)p];
+    (u64) p <= (u64) q;
+    (u64) q <= A.base + A.size;
+ensures
+    take P2 = Owned(p);
+    P == P2;
+    return == 1i32;
+@*/
+{
+  return p <= q;
+}
+
+int live_alloc(int *p, int *q)
+/*@
+ requires
+    !is_null(p);
+    ptr_eq(q, array_shift(p, 10i32));
+    take A = Alloc(p);
+    A.base <= (u64) p;
+    (u64) p <= (u64) q;
+    (u64) q <= A.base + A.size;
+ensures
+    return == 0i32;
+    take A2 = Alloc(p);
+    A == A2;
+@*/
+{
+  /*@ assert(allocs[(alloc_id)p] == A); @*/
+  return p >= q;
+}
+
+int main(void)
+{
+    int arr[11] = { 0 };
+    live_alloc(&arr[0], &arr[10]);
+    /*@ extract Owned<int>, 0u64; @*/
+    /*@ extract Owned<int>, 10u64; @*/
+    live_owned_one(&arr[0], &arr[10]);
+    live_owned_both(&arr[0], &arr[10]);
+    char *p = (char*) arr;
+    live_owned_footprint(p + 2, p + 14);
+}

tests/cn/ptr_relop.error.c

@@ -0,0 +1,21 @@
+int live_owned_footprint(char *p, char *q)
+/*@
+ requires
+    take P = Owned<int[11]>(array_shift<char>(p, -2i64));
+    ptr_eq(q, array_shift<char>(p, 12i64));
+ensures
+    take P2 = Owned<int[11]>(array_shift<char>(p, -2i64));
+    P == P2;
+    return == 1i32;
+@*/
+{
+  // will fail without -- /*@ extract Owned<int>, 7u64; @*/
+  return q > p;
+}
+
+int main(void)
+{
+    int arr[11] = { 0 };
+    char *p = (char*) arr;
+    live_owned_footprint(p + 2, p + 14);
+}

tests/run-cn-exec.sh

@@ -95,6 +95,8 @@ SUCCESS=$(find cn -name '*.c' \
     ! -name "mask_ptr.c" \
     ! -name "previously_inconsistent_assumptions1.c" \
     ! -name "previously_inconsistent_assumptions2.c" \
+    ! -name "ptr_relop.c" \
+    ! -name "ptr_relop.error.c" \
 )
 
 # Include files which cause error for proof but not testing
@@ -154,6 +156,8 @@ BUGGY="cn/division_casting.c \
        cn/mask_ptr.c \
        cn/previously_inconsistent_assumptions1.c \
        cn/previously_inconsistent_assumptions2.c \
+       cn/ptr_relop.c \
+       cn/ptr_relop.error.c \
        "
 
 # Exclude files which cause error for proof but not testing