From 34ddf68d39e1af65da442b2148564a412426274c Mon Sep 17 00:00:00 2001
From: Andrei Homescu <ah@immunant.com>
Date: Mon, 5 Aug 2024 16:20:11 -0700
Subject: [PATCH] Unsound: add non-null pointers from PDG to updates_forbidden

If the dynamic analysis tells us a pointer is never NULL
(i.e. it never shows up in an is_null graph), then
force the NON_NULL permission on it using updates_forbidden.
This is potentially an unsound transformation because the
pointer may actually be NULL on other inputs not covered
by the sample ones.
---
 c2rust-analyze/src/analyze.rs | 33 ++++++++++++++++++++++++++++++++-
 1 file changed, 32 insertions(+), 1 deletion(-)

diff --git a/c2rust-analyze/src/analyze.rs b/c2rust-analyze/src/analyze.rs
index f4eddf544..15f390d79 100644
--- a/c2rust-analyze/src/analyze.rs
+++ b/c2rust-analyze/src/analyze.rs
@@ -943,6 +943,29 @@ fn run(tcx: TyCtxt) {
         let f = std::fs::File::open(pdg_file_path).unwrap();
         let graphs: Graphs = bincode::deserialize_from(f).unwrap();
 
+        let mut known_nulls = HashSet::new();
+        for g in &graphs.graphs {
+            for n in &g.nodes {
+                let dest_pl = match n.dest.as_ref() {
+                    Some(x) => x,
+                    None => {
+                        continue;
+                    }
+                };
+                if !dest_pl.projection.is_empty() {
+                    continue;
+                }
+                let dest = dest_pl.local;
+                let dest = Local::from_u32(dest.index);
+                if g.is_null {
+                    known_nulls.insert((n.function.id, dest));
+                }
+            }
+        }
+
+        let allow_unsound =
+            env::var("C2RUST_ANALYZE_PDG_ALLOW_UNSOUND").map_or(false, |val| &val == "1");
+
         for g in &graphs.graphs {
             for n in &g.nodes {
                 let def_path_hash: (u64, u64) = n.function.id.0.into();
@@ -962,6 +985,8 @@ fn run(tcx: TyCtxt) {
                 let mir = mir.borrow();
                 let acx = gacx.function_context_with_data(&mir, info.acx_data.take());
                 let mut asn = gasn.and(&mut info.lasn);
+                let mut updates_forbidden =
+                    g_updates_forbidden.and_mut(&mut info.l_updates_forbidden);
 
                 let dest_pl = match n.dest.as_ref() {
                     Some(x) => x,
@@ -999,8 +1024,14 @@ fn run(tcx: TyCtxt) {
 
                 let old_perms = asn.perms()[ptr];
                 let mut perms = old_perms;
-                if g.is_null {
+                if known_nulls.contains(&(n.function.id, dest)) {
                     perms.remove(PermissionSet::NON_NULL);
+                } else if allow_unsound {
+                    perms.insert(PermissionSet::NON_NULL);
+                    // Unsound update: if we have never seen a NULL for
+                    // this local in the PDG, prevent the static analysis
+                    // from changing that permission.
+                    updates_forbidden[ptr].insert(PermissionSet::NON_NULL);
                 }
 
                 if let Some(node_info) = n.info.as_ref() {