From 7a068d3cd0231c36e5a38e740e9740ee088a48c1 Mon Sep 17 00:00:00 2001
From: Stuart Pernsteiner <spernsteiner@galois.com>
Date: Mon, 3 Jun 2024 11:45:02 -0700
Subject: [PATCH] analyze: add test case for C null pointer projection special
 cases

---
 .../tests/filecheck/non_null_rewrites.rs      | 43 +++++++++++++++++++
 1 file changed, 43 insertions(+)

diff --git a/c2rust-analyze/tests/filecheck/non_null_rewrites.rs b/c2rust-analyze/tests/filecheck/non_null_rewrites.rs
index 4c3e9e69a..380c421bb 100644
--- a/c2rust-analyze/tests/filecheck/non_null_rewrites.rs
+++ b/c2rust-analyze/tests/filecheck/non_null_rewrites.rs
@@ -146,3 +146,46 @@ unsafe fn local_field_projection(cond: bool) -> i32 {
     }
     *p
 }
+
+// CHECK-LABEL: unsafe fn null_ptr_special_cases{{[<(]}}
+unsafe fn null_ptr_special_cases(cond: bool, p: *const i32, i: isize) -> *const i32 {
+    // In C, `*NULL` is usually undefined behavior, even in cases like `sizeof(*(char*)0)` that
+    // don't involve an actual memory access.  However, there are two special cases in the
+    // standard:
+    //
+    // 1. `&*p == p` for all `p`, even if `p == NULL`.
+    // 2. `&p[i] == p + i` for all `p`, even if `p == NULL`.  Note that `NULL + 0 == NULL`, but
+    //    `NULL + i` with nonzero `i` is undefined.
+    //
+    // Here we test these two cases to see if rewriting introduces a panic even in cases where the
+    // C operation is valid.
+
+    // Make `p` nullable.
+    let mut p = p;
+    if cond {
+        p = ptr::null();
+    }
+
+    // Currently, `&*p` rewrites to `Some(&*p.unwrap())`, which panics when `p` is null.
+    //
+    // CHECK: Some(&(*(p).unwrap()));
+    let q = ptr::addr_of!(*p);
+
+    // `offset(i)` rewrites to `map`, which passes null/`None` through unchanged.
+    //
+    // CHECK: let (arr, idx, ) = ((q), (0) as usize, );
+    // CHECK-NEXT: arr.map(|arr| &arr[idx ..])
+    let r = q.offset(0);
+
+    // Because we use `Option::map` for this rewrite, it returns `None` if `p` is `None`, even when
+    // `i != 0`.  This is different from the concrete behavior of most C compilers, where `NULL + i
+    // != NULL`.  Adding `NULL + i` (with nonzero `i`) is undefined behavior in C, so it's legal
+    // for us to define it this way, though it may produce surprising results in some cases like
+    // handrolled `offsetof` macros.
+    //
+    // CHECK: let (arr, idx, ) = ((r), (i) as usize, );
+    // CHECK-NEXT: arr.map(|arr| &arr[idx ..])
+    let s = r.offset(i);
+
+    s
+}