analyze: add Callee::Null for ptr::{null,null_mut}

immunant · Apr 12, 2024 · a5ffd1e · a5ffd1e
1 parent 90442f8
commit a5ffd1e
Show file tree

Hide file tree

Showing 5 changed files with 43 additions and 2 deletions.
diff --git a/c2rust-analyze/src/borrowck/type_check.rs b/c2rust-analyze/src/borrowck/type_check.rs
@@ -602,6 +602,9 @@ impl<'tcx> TypeChecker<'tcx, '_> {
                             self.visit_operand(p)
                         });
                     }
+                    Callee::Null { .. } => {
+                        // TODO: do we need to do anything here?
+                    }
                 }
             }
             // TODO(spernsteiner): handle other `TerminatorKind`s

diff --git a/c2rust-analyze/src/dataflow/mod.rs b/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));
     }
 

diff --git a/c2rust-analyze/src/dataflow/type_check.rs b/c2rust-analyze/src/dataflow/type_check.rs
@@ -599,6 +599,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);
+            }
         }
     }
 

diff --git a/c2rust-analyze/src/pointee_type/type_check.rs b/c2rust-analyze/src/pointee_type/type_check.rs
@@ -332,6 +332,9 @@ impl<'tcx> TypeChecker<'tcx, '_> {
             Callee::IsNull => {
                 // No constraints.
             }
+            Callee::Null { .. } => {
+                // No constraints.
+            }
         }
     }
 }

diff --git a/c2rust-analyze/src/util.rs b/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::mem::size_of` 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);