analyze: initial implementation of NON_NULL static analysis (#1081)

This adds a very basic static analysis for `NON_NULL` within the current
`dataflow` framework. It starts by optimistically assuming that all
pointers are `NON_NULL`, and removes the permission from pointers into
which a `ptr::null()` or equivalent might flow. This branch just
implements the static analysis, not rewriting.

I'm actually not a huge fan of this design - I think we'd probably get
much better results with a path-sensitive analysis that can handle
common patterns from C like `if !p.is_null() { let q = (&p).field; /*
use q... */ }` by detecting null checks in the CFG. But the simple
path-insensitive version is sufficient for now, and gives us somewhere
to plug in the dynamic analysis results.

c2rust-analyze/src/analyze.rs

@@ -867,8 +867,11 @@ fn run(tcx: TyCtxt) {
     // don't want to rewrite those
     gacx.foreign_mentioned_tys = foreign_mentioned_tys(tcx);
 
-    let mut gasn =
-        GlobalAssignment::new(gacx.num_pointers(), PermissionSet::UNIQUE, FlagSet::empty());
+    const INITIAL_PERMS: PermissionSet =
+        PermissionSet::union_all([PermissionSet::UNIQUE, PermissionSet::NON_NULL]);
+    const INITIAL_FLAGS: FlagSet = FlagSet::empty();
+
+    let mut gasn = GlobalAssignment::new(gacx.num_pointers(), INITIAL_PERMS, INITIAL_FLAGS);
     for (ptr, &info) in gacx.ptr_info().iter() {
         if should_make_fixed(info) {
             gasn.flags[ptr].insert(FlagSet::FIXED);
@@ -886,14 +889,14 @@ fn run(tcx: TyCtxt) {
 
     for (ptr, perms) in gacx.known_fn_ptr_perms() {
         let existing_perms = &mut gasn.perms[ptr];
-        existing_perms.remove(PermissionSet::UNIQUE);
+        existing_perms.remove(INITIAL_PERMS);
         assert_eq!(*existing_perms, PermissionSet::empty());
         *existing_perms = perms;
     }
 
     for info in func_info.values_mut() {
         let num_pointers = info.acx_data.num_pointers();
-        let mut lasn = LocalAssignment::new(num_pointers, PermissionSet::UNIQUE, FlagSet::empty());
+        let mut lasn = LocalAssignment::new(num_pointers, INITIAL_PERMS, INITIAL_FLAGS);
 
         for (ptr, &info) in info.acx_data.local_ptr_info().iter() {
             if should_make_fixed(info) {
@@ -990,6 +993,7 @@ fn run(tcx: TyCtxt) {
                 if !node_info.unique {
                     perms.remove(PermissionSet::UNIQUE);
                 }
+                // TODO: PermissionSet::NON_NULL
 
                 if perms != old_perms {
                     let added = perms & !old_perms;

c2rust-analyze/src/borrowck/type_check.rs

@@ -602,6 +602,11 @@ impl<'tcx> TypeChecker<'tcx, '_> {
                             self.visit_operand(p)
                         });
                     }
+                    Callee::Null { .. } => {
+                        // Just visit the place.  The null pointer returned here has no origin, so
+                        // there's no need to call `do_assign` to set up subset relations.
+                        let _pl_lty = self.visit_place(destination);
+                    }
                 }
             }
             // TODO(spernsteiner): handle other `TerminatorKind`s

c2rust-analyze/src/context.rs

@@ -166,7 +166,7 @@ impl PermissionSet {
 
     /// The permissions for a (byte-)string literal.
     //
-    // `.union` is used here since it's a `const fn`, unlike `BitOr::bitor`.
+    // `union_all` is used here since it's a `const fn`, unlike `BitOr::bitor`.
     pub const STRING_LITERAL: Self = Self::union_all([Self::READ, Self::OFFSET_ADD]);
 }
 
@@ -456,10 +456,11 @@ impl<'a, 'tcx> AnalysisCtxt<'_, 'tcx> {
             let ptr = lty.label;
             let expected_perms = PermissionSet::STRING_LITERAL;
             let mut actual_perms = asn.perms()[ptr];
-            // Ignore `UNIQUE` as it gets automatically added to all permissions
-            // and then removed later if it can't apply.
-            // We don't care about `UNIQUE` for const refs, so just unset it here.
+            // Ignore `UNIQUE` and `NON_NULL` as they get automatically added to all permissions
+            // and then removed later if it can't apply.  We don't care about `UNIQUE` or
+            // `NON_NULL` for const refs, so just unset it here.
             actual_perms.set(PermissionSet::UNIQUE, false);
+            actual_perms.set(PermissionSet::NON_NULL, false);
             assert_eq!(expected_perms, actual_perms);
         }
     }

c2rust-analyze/src/dataflow/mod.rs

@@ -40,8 +40,7 @@ impl DataflowConstraints {
         self.constraints.push(Constraint::AllPerms(ptr, perms));
     }
 
-    #[allow(dead_code)]
-    fn _add_no_perms(&mut self, ptr: PointerId, perms: PermissionSet) {
+    fn add_no_perms(&mut self, ptr: PointerId, perms: PermissionSet) {
         self.constraints.push(Constraint::NoPerms(ptr, perms));
     }
 
@@ -86,7 +85,7 @@ impl DataflowConstraints {
                 // Permissions that should be propagated "down": if the superset (`b`)
                 // doesn't have it, then the subset (`a`) should have it removed.
                 #[allow(bad_style)]
-                let PROPAGATE_DOWN = PermissionSet::UNIQUE;
+                let PROPAGATE_DOWN = PermissionSet::UNIQUE | PermissionSet::NON_NULL;
                 // Permissions that should be propagated "up": if the subset (`a`) has it,
                 // then the superset (`b`) should be given it.
                 #[allow(bad_style)]

c2rust-analyze/src/dataflow/type_check.rs

@@ -123,6 +123,9 @@ impl<'tcx> TypeChecker<'tcx, '_> {
                 if !op.constant().copied().map(is_null_const).unwrap_or(false) {
                     panic!("Creating non-null pointers from exposed addresses not supported");
                 }
+                // The target type of the cast must not have `NON_NULL` permission.
+                self.constraints
+                    .add_no_perms(to_lty.label, PermissionSet::NON_NULL);
             }
             CastKind::PointerExposeAddress => {
                 // Allow, as [`CastKind::PointerFromExposedAddress`] is the dangerous one,
@@ -599,6 +602,15 @@ impl<'tcx> TypeChecker<'tcx, '_> {
                 assert!(args.len() == 1);
                 self.visit_operand(&args[0]);
             }
+            Callee::Null { .. } => {
+                assert!(args.len() == 0);
+                self.visit_place(destination, Mutability::Mut);
+                let pl_lty = self.acx.type_of(destination);
+                // We are assigning a null pointer to `destination`, so it must not have the
+                // `NON_NULL` flag.
+                self.constraints
+                    .add_no_perms(pl_lty.label, PermissionSet::NON_NULL);
+            }
         }
     }
 

c2rust-analyze/src/pointee_type/type_check.rs

@@ -332,6 +332,9 @@ impl<'tcx> TypeChecker<'tcx, '_> {
             Callee::IsNull => {
                 // No constraints.
             }
+            Callee::Null { .. } => {
+                // No constraints.
+            }
         }
     }
 }

c2rust-analyze/src/util.rs

@@ -191,6 +191,9 @@ pub enum Callee<'tcx> {
     /// core::ptr::is_null
     IsNull,
 
+    /// core::ptr::null or core::ptr::null_mut
+    Null { mutbl: Mutability },
+
     /// `core::mem::size_of<T>`
     SizeOf { ty: Ty<'tcx> },
 }
@@ -342,6 +345,30 @@ fn builtin_callee<'tcx>(tcx: TyCtxt<'tcx>, did: DefId, substs: SubstsRef<'tcx>)
             Some(Callee::IsNull)
         }
 
+        "null" | "null_mut" => {
+            // The `core::ptr::null/null_mut` function.
+            let parent_did = tcx.parent(did);
+            if tcx.def_kind(parent_did) != DefKind::Mod {
+                return None;
+            }
+            if tcx.item_name(parent_did).as_str() != "ptr" {
+                return None;
+            }
+            let grandparent_did = tcx.parent(parent_did);
+            if grandparent_did.index != CRATE_DEF_INDEX {
+                return None;
+            }
+            if tcx.crate_name(grandparent_did.krate).as_str() != "core" {
+                return None;
+            }
+            let mutbl = match name.as_str() {
+                "null" => Mutability::Not,
+                "null_mut" => Mutability::Mut,
+                _ => unreachable!(),
+            };
+            Some(Callee::Null { mutbl })
+        }
+
         "size_of" => {
             // The `core::mem::size_of` function.
             let parent_did = tcx.parent(did);

c2rust-analyze/tests/filecheck.rs

@@ -55,6 +55,7 @@ define_tests! {
     insertion_sort_driver,
     insertion_sort_rewrites,
     known_fn,
+    non_null,
     offset1,
     offset2,
     pointee,

c2rust-analyze/tests/filecheck/alias1.rs

@@ -2,23 +2,23 @@ use std::ptr;
 
 // CHECK-LABEL: final labeling for "alias1_good"
 pub unsafe fn alias1_good() {
-    // CHECK-DAG: ([[@LINE+1]]: mut x): addr_of = READ | WRITE | UNIQUE,
+    // CHECK-DAG: ([[@LINE+1]]: mut x): addr_of = READ | WRITE | UNIQUE | NON_NULL,
     let mut x = 0;
-    // CHECK-DAG: ([[@LINE+1]]: p): {{.*}}type = UNIQUE#
+    // CHECK-DAG: ([[@LINE+1]]: p): {{.*}}type = UNIQUE | NON_NULL#
     let p = ptr::addr_of_mut!(x);
-    // CHECK-DAG: ([[@LINE+1]]: q): {{.*}}type = READ | WRITE | UNIQUE#
+    // CHECK-DAG: ([[@LINE+1]]: q): {{.*}}type = READ | WRITE | UNIQUE | NON_NULL#
     let q = ptr::addr_of_mut!(x);
     *q = 1;
 }
 
 // CHECK-LABEL: final labeling for "alias1_bad"
 pub unsafe fn alias1_bad() {
-    // CHECK-DAG: ([[@LINE+2]]: mut x): addr_of = READ | WRITE,
+    // CHECK-DAG: ([[@LINE+2]]: mut x): addr_of = READ | WRITE | NON_NULL,
     // CHECK-DAG: ([[@LINE+1]]: mut x): addr_of flags = CELL,
     let mut x = 0;
-    // CHECK-DAG: ([[@LINE+1]]: p): {{.*}}type = READ | WRITE#
+    // CHECK-DAG: ([[@LINE+1]]: p): {{.*}}type = READ | WRITE | NON_NULL#
     let p = ptr::addr_of_mut!(x);
-    // CHECK-DAG: ([[@LINE+2]]: q): {{.*}}type = (empty)#
+    // CHECK-DAG: ([[@LINE+2]]: q): {{.*}}type = NON_NULL#
     // CHECK-DAG: ([[@LINE+1]]: q): {{.*}}type flags = CELL#
     let q = ptr::addr_of_mut!(x);
     *p = 1;

c2rust-analyze/tests/filecheck/alias2.rs

@@ -1,43 +1,43 @@
 use std::ptr;
 
 // CHECK-LABEL: final labeling for "alias2_copy_good"
-// CHECK-DAG: ([[@LINE+1]]: x): {{.*}}type = READ | WRITE | UNIQUE#
+// CHECK-DAG: ([[@LINE+1]]: x): {{.*}}type = READ | WRITE | UNIQUE | NON_NULL#
 pub unsafe fn alias2_copy_good(x: *mut i32) {
-    // CHECK-DAG: ([[@LINE+1]]: p): {{.*}}type = UNIQUE#
+    // CHECK-DAG: ([[@LINE+1]]: p): {{.*}}type = UNIQUE | NON_NULL#
     let p = x;
-    // CHECK-DAG: ([[@LINE+1]]: q): {{.*}}type = READ | WRITE | UNIQUE#
+    // CHECK-DAG: ([[@LINE+1]]: q): {{.*}}type = READ | WRITE | UNIQUE | NON_NULL#
     let q = x;
     *q = 1;
 }
 
 // CHECK-LABEL: final labeling for "alias2_addr_of_good"
-// CHECK-DAG: ([[@LINE+1]]: x): {{.*}}type = READ | WRITE | UNIQUE#
+// CHECK-DAG: ([[@LINE+1]]: x): {{.*}}type = READ | WRITE | UNIQUE | NON_NULL#
 pub unsafe fn alias2_addr_of_good(x: *mut i32) {
-    // CHECK-DAG: ([[@LINE+1]]: p): {{.*}}type = UNIQUE#
+    // CHECK-DAG: ([[@LINE+1]]: p): {{.*}}type = UNIQUE | NON_NULL#
     let p = ptr::addr_of_mut!(*x);
-    // CHECK-DAG: ([[@LINE+1]]: q): {{.*}}type = READ | WRITE | UNIQUE#
+    // CHECK-DAG: ([[@LINE+1]]: q): {{.*}}type = READ | WRITE | UNIQUE | NON_NULL#
     let q = ptr::addr_of_mut!(*x);
     *q = 1;
 }
 
 // CHECK-LABEL: final labeling for "alias2_copy_bad"
-// CHECK-DAG: ([[@LINE+2]]: x): {{.*}}type = READ | WRITE#
+// CHECK-DAG: ([[@LINE+2]]: x): {{.*}}type = READ | WRITE | NON_NULL#
 // CHECK-DAG: ([[@LINE+1]]: x): {{.*}}type flags = CELL#
 pub unsafe fn alias2_copy_bad(x: *mut i32) {
-    // CHECK-DAG: ([[@LINE+1]]: p): {{.*}}type = READ | WRITE#
+    // CHECK-DAG: ([[@LINE+1]]: p): {{.*}}type = READ | WRITE | NON_NULL#
     let p = x;
-    // CHECK-DAG: ([[@LINE+1]]: q): {{.*}}type = (empty)#
+    // CHECK-DAG: ([[@LINE+1]]: q): {{.*}}type = NON_NULL#
     let q = x;
     *p = 1;
 }
 
 // CHECK-LABEL: final labeling for "alias2_addr_of_bad"
-// CHECK-DAG: ([[@LINE+2]]: x): {{.*}}type = READ | WRITE#
+// CHECK-DAG: ([[@LINE+2]]: x): {{.*}}type = READ | WRITE | NON_NULL#
 // CHECK-DAG: ([[@LINE+1]]: x): {{.*}}type flags = CELL#
 pub unsafe fn alias2_addr_of_bad(x: *mut i32) {
-    // CHECK-DAG: ([[@LINE+1]]: p): {{.*}}type = READ | WRITE#
+    // CHECK-DAG: ([[@LINE+1]]: p): {{.*}}type = READ | WRITE | NON_NULL#
     let p = ptr::addr_of_mut!(*x);
-    // CHECK-DAG: ([[@LINE+1]]: q): {{.*}}type = (empty)#
+    // CHECK-DAG: ([[@LINE+1]]: q): {{.*}}type = NON_NULL#
     let q = ptr::addr_of_mut!(*x);
     *p = 1;
 }

c2rust-analyze/tests/filecheck/alias3.rs

@@ -1,26 +1,26 @@
 use std::ptr;
 
 // CHECK-LABEL: final labeling for "alias3_copy_bad1"
-// CHECK-DAG: ([[@LINE+2]]: x): {{.*}}type = READ | WRITE#
+// CHECK-DAG: ([[@LINE+2]]: x): {{.*}}type = READ | WRITE | NON_NULL#
 // CHECK-DAG: ([[@LINE+1]]: x): {{.*}}type flags = CELL#
 pub unsafe fn alias3_copy_bad1(x: *mut i32) {
-    // CHECK-DAG: ([[@LINE+2]]: p): {{.*}}type = READ#
+    // CHECK-DAG: ([[@LINE+2]]: p): {{.*}}type = READ | NON_NULL#
     // CHECK-DAG: ([[@LINE+1]]: p): {{.*}}type flags = CELL#
     let p = x;
-    // CHECK-DAG: ([[@LINE+2]]: q): {{.*}}type = READ | WRITE#
+    // CHECK-DAG: ([[@LINE+2]]: q): {{.*}}type = READ | WRITE | NON_NULL#
     // CHECK-DAG: ([[@LINE+1]]: q): {{.*}}type flags = CELL#
     let q = x;
     *q = *p;
 }
 
 // CHECK-LABEL: final labeling for "alias3_copy_bad2"
-// CHECK-DAG: ([[@LINE+2]]: x): {{.*}}type = READ | WRITE#
+// CHECK-DAG: ([[@LINE+2]]: x): {{.*}}type = READ | WRITE | NON_NULL#
 // CHECK-DAG: ([[@LINE+1]]: x): {{.*}}type flags = CELL#
 pub unsafe fn alias3_copy_bad2(x: *mut i32) {
-    // CHECK-DAG: ([[@LINE+2]]: p): {{.*}}type = READ | WRITE#
+    // CHECK-DAG: ([[@LINE+2]]: p): {{.*}}type = READ | WRITE | NON_NULL#
     // CHECK-DAG: ([[@LINE+1]]: p): {{.*}}type flags = CELL#
     let p = x;
-    // CHECK-DAG: ([[@LINE+2]]: q): {{.*}}type = READ#
+    // CHECK-DAG: ([[@LINE+2]]: q): {{.*}}type = READ | NON_NULL#
     // CHECK-DAG: ([[@LINE+1]]: q): {{.*}}type flags = CELL#
     let q = x;
     *p = *q;

c2rust-analyze/tests/filecheck/alloc.rs

@@ -38,28 +38,28 @@ unsafe extern "C" fn calloc1() -> *mut i32 {
 
 // CHECK-LABEL: final labeling for "malloc1"
 pub unsafe extern "C" fn malloc1(mut cnt: libc::c_int) -> *mut i32 {
-    // CHECK-DAG: ([[@LINE+1]]: i): addr_of = UNIQUE, type = READ
+    // CHECK-DAG: ([[@LINE+1]]: i): addr_of = UNIQUE | NON_NULL, type = READ | NON_NULL
     let i = malloc(::std::mem::size_of::<i32>() as libc::c_ulong) as *mut i32;
     let x = *i;
     return i;
 }
 
 // CHECK-LABEL: final labeling for "free1"
 unsafe extern "C" fn free1(mut i: *mut i32) {
-    // CHECK-DAG: ([[@LINE+1]]: i{{.*}}): {{.*}}type = UNIQUE | FREE#
+    // CHECK-DAG: ([[@LINE+1]]: i{{.*}}): {{.*}}type = UNIQUE | FREE | NON_NULL#
     free(i as *mut libc::c_void);
 }
 
 // CHECK-LABEL: final labeling for "realloc1"
 unsafe extern "C" fn realloc1(mut i: *mut i32, len: libc::c_ulong) {
     let mut capacity = 1;
     let mut x = 1;
-    // CHECK-DAG: ([[@LINE+1]]: mut elem): addr_of = UNIQUE, type = READ | WRITE | OFFSET_ADD | OFFSET_SUB
+    // CHECK-DAG: ([[@LINE+1]]: mut elem): addr_of = UNIQUE | NON_NULL, type = READ | WRITE | OFFSET_ADD | OFFSET_SUB | NON_NULL
     let mut elem = i;
     loop {
         if x == capacity {
             capacity *= 2;
-            // CHECK-DAG: ([[@LINE+2]]: i{{.*}}): addr_of = UNIQUE, type = FREE
+            // CHECK-DAG: ([[@LINE+2]]: i{{.*}}): addr_of = UNIQUE | NON_NULL, type = FREE | NON_NULL
             i = realloc(
                 i as *mut libc::c_void,
                 4 as libc::c_ulong,
@@ -76,22 +76,22 @@ unsafe extern "C" fn realloc1(mut i: *mut i32, len: libc::c_ulong) {
 
 // CHECK-LABEL: final labeling for "alloc_and_free1"
 pub unsafe extern "C" fn alloc_and_free1(mut cnt: libc::c_int) {
-    // CHECK-DAG: ([[@LINE+1]]: i): addr_of = UNIQUE, type = UNIQUE | FREE#
+    // CHECK-DAG: ([[@LINE+1]]: i): addr_of = UNIQUE | NON_NULL, type = UNIQUE | FREE | NON_NULL#
     let i = malloc(::std::mem::size_of::<i32>() as libc::c_ulong) as *mut i32;
-    // CHECK-DAG: ([[@LINE+1]]: i{{.*}}): {{.*}}type = UNIQUE | FREE#
+    // CHECK-DAG: ([[@LINE+1]]: i{{.*}}): {{.*}}type = UNIQUE | FREE | NON_NULL#
     free(i as *mut libc::c_void);
 }
 
 
 // CHECK-LABEL: final labeling for "alloc_and_free2"
 pub unsafe extern "C" fn alloc_and_free2(mut cnt: libc::c_int) {
-    // CHECK-DAG: ([[@LINE+1]]: i): addr_of = UNIQUE, type = READ | WRITE | UNIQUE | FREE#
+    // CHECK-DAG: ([[@LINE+1]]: i): addr_of = UNIQUE | NON_NULL, type = READ | WRITE | UNIQUE | FREE | NON_NULL#
     let i = malloc(::std::mem::size_of::<i32>() as libc::c_ulong) as *mut i32;
     if !i.is_null() {
-        // CHECK-DAG: ([[@LINE+1]]: mut b): addr_of = UNIQUE, type = READ | WRITE | UNIQUE#
+        // CHECK-DAG: ([[@LINE+1]]: mut b): addr_of = UNIQUE | NON_NULL, type = READ | WRITE | UNIQUE | NON_NULL#
         let mut b = i;
         *b = 2;
-        // CHECK-DAG: ([[@LINE+1]]: i): {{.*}}type = UNIQUE | FREE#
+        // CHECK-DAG: ([[@LINE+1]]: i): {{.*}}type = UNIQUE | FREE | NON_NULL#
         free(i as *mut libc::c_void);
     }
 }

c2rust-analyze/tests/filecheck/cast.rs

@@ -10,7 +10,7 @@ struct S {
 
 // CHECK-LABEL: final labeling for "null_ptr"
 pub unsafe fn null_ptr() {
-    // CHECK-DAG: ([[@LINE+3]]: s): addr_of = UNIQUE, type = READ | WRITE | UNIQUE#
+    // CHECK-DAG: ([[@LINE+3]]: s): addr_of = UNIQUE | NON_NULL, type = READ | WRITE | UNIQUE#
     // CHECK-LABEL: type assignment for "null_ptr":
     // CHECK-DAG: ([[@LINE+1]]: s): &mut S
     let s = 0 as *mut S;

c2rust-analyze/tests/filecheck/fields.rs

@@ -60,15 +60,15 @@ struct HypoWrapper {
 // CHECK-DAG: assign Label { origin: Some(Origin([[P_REF_A_ORIGIN]]))
 
 // CHECK-LABEL: final labeling for "_field_access"
-// CHECK-DAG: ([[@LINE+3]]: ppd): addr_of = UNIQUE, type = READ | WRITE | UNIQUE
+// CHECK-DAG: ([[@LINE+3]]: ppd): addr_of = UNIQUE | NON_NULL, type = READ | WRITE | UNIQUE | NON_NULL
 // CHECK-DAG: ([[@LINE+2]]: ra): &'d mut A<'d>
 // CHECK-DAG: ([[@LINE+1]]: ppd): &mut &mut Data
 unsafe fn _field_access<'d, 'a: 'd, T: Clone + Copy>(ra: &'d mut A<'d>, ppd: *mut *mut Data<'d>) {
-    // CHECK-DAG: ([[@LINE+2]]: rd): addr_of = UNIQUE, type = READ | UNIQUE
+    // CHECK-DAG: ([[@LINE+2]]: rd): addr_of = UNIQUE | NON_NULL, type = READ | UNIQUE | NON_NULL
     // CHECK-DAG: ([[@LINE+1]]: rd): &Data
     let rd = (*(**ppd).a.pra).rd;
 
-    // CHECK-DAG: ([[@LINE+2]]: pi): addr_of = UNIQUE, type = READ | WRITE | UNIQUE
+    // CHECK-DAG: ([[@LINE+2]]: pi): addr_of = UNIQUE | NON_NULL, type = READ | WRITE | UNIQUE | NON_NULL
     // CHECK-DAG: ([[@LINE+1]]: pi): &mut i32
     let pi = rd.pi;
     *pi = 3;