CN VIP: Add int to pointer rules

0 addresses are mapped to NULL, otherwise mapped to a pointer with an
unconstrained provenance.

backend/cn/lib/check.ml

@@ -1407,7 +1407,8 @@ let rec check_expr labels (e : BT.t Mu.mu_expr) (k : IT.t -> unit m) : unit m =
               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
-                   yields the expected result. *)
+                   yields the expected result, or signal
+                   UB050_pointers_subtraction_not_representable *)
                 div_
                   ( cast_ ptr_diff_bt (sub_ (addr_ arg1 loc, addr_ arg2 loc) loc) loc,
                     int_lit_ divisor ptr_diff_bt loc )
@@ -1448,9 +1449,17 @@ let rec check_expr labels (e : BT.t Mu.mu_expr) (k : IT.t -> unit m) : unit m =
           in
           let@ _bt_info = ensure_bitvector_type loc ~expect:(Mu.bt_of_pexpr pe) in
           check_pexpr pe (fun arg ->
-            (* TODO (DCM, VIP): check for UB050_pointers_subtraction_not_representable *)
-            let value = integerToPointerCast_ arg loc in
-            k value)
+            let sym, result = IT.fresh_named (BT.Loc ()) "intToPtr" loc in
+            let@ _ = add_a sym (Loc ()) (here, lazy (Sym.pp sym)) in
+            let cond = eq_ (arg, int_lit_ 0 (bt arg) here) here in
+            let null_case = eq_ (result, null_ here) here in
+            (* NOTE: the allocation ID is intentionally left unconstrained *)
+            let alloc_case =
+              and_ [ hasAllocId_ result here; eq_ (arg, addr_ result here) here ] here
+            in
+            let constr = ite_ (cond, null_case, alloc_case) here in
+            let@ () = add_c loc (LC.T constr) in
+            k result)
         | M_PtrValidForDeref (act, pe) ->
           (* TODO (DCM, VIP) *)
           let@ () = WellTyped.WCT.is_ct act.loc act.ct in

backend/cn/lib/indexTerms.ml

@@ -719,8 +719,6 @@ let gePointer_ (it, it') loc = lePointer_ (it', it) loc
 
 let cast_ bt it loc = IT (Cast (bt, it), bt, loc)
 
-let integerToPointerCast_ it loc = cast_ (Loc ()) it loc
-
 let uintptr_const_ n loc = num_lit_ n Memory.uintptr_bt loc
 
 let uintptr_int_ n loc = uintptr_const_ (Z.of_int n) loc

tests/cn/int_to_ptr.c

@@ -0,0 +1,15 @@
+void* cast(unsigned long long addr)
+/*@
+ensures
+    addr == 0u64 && is_null(return) || addr != 0u64 && has_alloc_id(return) && (u64) return == addr;
+@*/
+{
+    return (void*)addr;
+}
+
+int main()
+{
+    int x = 0;
+    void* p = cast((unsigned long long)&x);
+    /*@ assert ((u64) &x == 0u64 || has_alloc_id(p) && (u64) p == (u64) &x); @*/
+}

tests/cn/int_to_ptr.error.c

@@ -0,0 +1,17 @@
+int* cast(unsigned long long addr)
+/*@
+ensures
+    addr == 0u64 && is_null(return) || addr != 0u64 && has_alloc_id(return) && (u64) return == addr;
+@*/
+{
+    return (void*)addr;
+}
+
+int main()
+{
+    int x = 0;
+    int* p = cast((unsigned long long)&x);
+    // The cast is successful, but has an unconstrained allocation ID, and so
+    // can't be used
+    return *p == 0;
+}

tests/cn/null_to_int.c

@@ -0,0 +1,15 @@
+unsigned long long f(int *p)
+/*@
+requires
+    ptr_eq(p, NULL);
+ensures
+    return == 0u64;
+@*/
+{
+    return (unsigned long long)p;
+}
+
+int main()
+{
+    return f((int*)0);
+}

tests/run-cn-exec.sh

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