diff --git a/backend/cn/lib/check.ml b/backend/cn/lib/check.ml index 1aa8b8141..a8cafba96 100644 --- a/backend/cn/lib/check.ml +++ b/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 diff --git a/backend/cn/lib/typeErrors.ml b/backend/cn/lib/typeErrors.ml index 628f605f5..689db40c9 100644 --- a/backend/cn/lib/typeErrors.ml +++ b/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 diff --git a/tests/cn/ptr_relop.c b/tests/cn/ptr_relop.c new file mode 100644 index 000000000..cf80ff5b2 --- /dev/null +++ b/tests/cn/ptr_relop.c @@ -0,0 +1,85 @@ +int live_owned_footprint(char *p, char *q) +/*@ + requires + take P = Owned(array_shift(p, -2i64)); + ptr_eq(q, array_shift(p, 12i64)); +ensures + take P2 = Owned(array_shift(p, -2i64)); + P == P2; + return == 0i32; +@*/ +{ + /*@ extract Owned, 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, 0u64; @*/ + /*@ extract Owned, 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); +} diff --git a/tests/cn/ptr_relop.error.c b/tests/cn/ptr_relop.error.c new file mode 100644 index 000000000..d80e79914 --- /dev/null +++ b/tests/cn/ptr_relop.error.c @@ -0,0 +1,21 @@ +int live_owned_footprint(char *p, char *q) +/*@ + requires + take P = Owned(array_shift(p, -2i64)); + ptr_eq(q, array_shift(p, 12i64)); +ensures + take P2 = Owned(array_shift(p, -2i64)); + P == P2; + return == 1i32; +@*/ +{ + // will fail without -- /*@ extract Owned, 7u64; @*/ + return q > p; +} + +int main(void) +{ + int arr[11] = { 0 }; + char *p = (char*) arr; + live_owned_footprint(p + 2, p + 14); +} diff --git a/tests/run-cn-exec.sh b/tests/run-cn-exec.sh index 27ff31131..dcf1f70d9 100755 --- a/tests/run-cn-exec.sh +++ b/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