Check / emit annotations based on env vars

zgrannan · zgrannan · commit ad4d2f0c1c40 · 2025-02-04T10:08:47.000-08:00
diff --git a/README.md b/README.md
@@ -3,9 +3,9 @@ To run:
 
 `cargo run [FILENAME].rs`
 
-To view the visualization 
+To view the visualization
 
-1. `PCS_VISUALIZATION=true cargo run [FILENAME.rs]`
+1. `PCG_VISUALIZATION=true cargo run [FILENAME.rs]`
 2. `cd visualization && ./serve`
 3. Go to http://localhost:8080 and select the function you wish to view
 
diff --git a/src/borrows/borrow_pcg_capabilities.rs b/src/borrows/borrow_pcg_capabilities.rs
@@ -1,6 +1,9 @@
 use std::collections::HashMap;
 
-use crate::free_pcs::CapabilityKind;
+use crate::{
+    free_pcs::CapabilityKind,
+    utils::{display::DisplayWithRepacker, PlaceRepacker},
+};
 
 use super::borrow_pcg_edge::PCGNode;
 
@@ -16,9 +19,11 @@ impl<'tcx> BorrowPCGCapabilities<'tcx> {
         Self(HashMap::new())
     }
 
-    pub(crate) fn debug_capability_lines(&self) -> Vec<String> {
+    pub(crate) fn debug_capability_lines(&self, repacker: PlaceRepacker<'_, 'tcx>) -> Vec<String> {
         self.iter()
-            .map(|(node, capability)| format!("{}: {:?}", node, capability))
+            .map(|(node, capability)| {
+                format!("{}: {:?}", node.to_short_string(repacker), capability)
+            })
             .collect()
     }
 
diff --git a/src/borrows/borrows_state.rs b/src/borrows/borrows_state.rs
@@ -91,8 +91,8 @@ impl<'tcx> Default for BorrowsState<'tcx> {
 }
 
 impl<'tcx> BorrowsState<'tcx> {
-    pub(crate) fn debug_capability_lines(&self) -> Vec<String> {
-        self.capabilities.debug_capability_lines()
+    pub(crate) fn debug_capability_lines(&self, repacker: PlaceRepacker<'_, 'tcx>) -> Vec<String> {
+        self.capabilities.debug_capability_lines(repacker)
     }
     pub(crate) fn insert(&mut self, edge: BorrowPCGEdge<'tcx>) -> bool {
         self.graph.insert(edge)
diff --git a/src/borrows/domain.rs b/src/borrows/domain.rs
@@ -19,7 +19,7 @@ pub struct LoopAbstraction<'tcx> {
 }
 
 impl<'tcx> DisplayWithRepacker<'tcx> for LoopAbstraction<'tcx> {
-    fn to_short_string(&self, repacker: PlaceRepacker<'_, 'tcx>) -> String {
+    fn to_short_string(&self, _repacker: PlaceRepacker<'_, 'tcx>) -> String {
         format!("Loop({:?})", self.block)
     }
 }
@@ -73,7 +73,7 @@ pub struct FunctionCallAbstraction<'tcx> {
 }
 
 impl<'tcx> DisplayWithRepacker<'tcx> for FunctionCallAbstraction<'tcx> {
-    fn to_short_string(&self, repacker: PlaceRepacker<'_, 'tcx>) -> String {
+    fn to_short_string(&self, _repacker: PlaceRepacker<'_, 'tcx>) -> String {
         format!("FunctionCall({:?}, {:?})", self.def_id, self.substs)
     }
 }
diff --git a/src/free_pcs/impl/fpcs.rs b/src/free_pcs/impl/fpcs.rs
@@ -150,10 +150,10 @@ impl<'tcx> Debug for CapabilitySummary<'tcx> {
 }
 
 impl<'tcx> CapabilitySummary<'tcx> {
-    pub(crate) fn debug_lines(&self) -> Vec<String> {
+    pub(crate) fn debug_lines(&self, repacker: PlaceRepacker<'_, 'tcx>) -> Vec<String> {
         self.0
             .iter()
-            .map(|c| c.debug_lines())
+            .map(|c| c.debug_lines(repacker))
             .collect::<Vec<_>>()
             .concat()
     }
diff --git a/src/free_pcs/impl/local.rs b/src/free_pcs/impl/local.rs
@@ -15,7 +15,7 @@ use rustc_interface::{
 use crate::{
     free_pcs::{CapabilityKind, RelatedSet, RepackOp},
     rustc_interface,
-    utils::{Place, PlaceOrdering, PlaceRepacker},
+    utils::{display::DisplayWithRepacker, Place, PlaceOrdering, PlaceRepacker},
 };
 
 #[derive(Clone, PartialEq, Eq)]
@@ -42,10 +42,10 @@ impl Default for CapabilityLocal<'_> {
 }
 
 impl<'tcx> CapabilityLocal<'tcx> {
-    pub(crate) fn debug_lines(&self) -> Vec<String> {
+    pub(crate) fn debug_lines(&self, repacker: PlaceRepacker<'_, 'tcx>) -> Vec<String> {
         match self {
             Self::Unallocated => vec![],
-            Self::Allocated(cps) => cps.debug_lines(),
+            Self::Allocated(cps) => cps.debug_lines(repacker),
         }
     }
 
@@ -81,9 +81,9 @@ impl<'tcx> Debug for CapabilityProjections<'tcx> {
 }
 
 impl<'tcx> CapabilityProjections<'tcx> {
-    pub(crate) fn debug_lines(&self) -> Vec<String> {
+    pub(crate) fn debug_lines(&self, repacker: PlaceRepacker<'_, 'tcx>) -> Vec<String> {
         self.iter()
-            .map(|(p, k)| format!("{p:?}: {k:?}"))
+            .map(|(p, k)| format!("{}: {:?}", p.to_short_string(repacker), k))
             .collect()
     }
 
diff --git a/src/free_pcs/results/cursor.rs b/src/free_pcs/results/cursor.rs
@@ -140,6 +140,7 @@ impl<'mir, 'tcx, D: HasPcg<'mir, 'tcx>, E: Analysis<'tcx, Domain = D>>
                     repacks_start: state.post_main().bridge(&to.post_main(), rp),
                     repacks_middle: Vec::new(),
                     borrows: entry_set.get_curr_borrow_pcg().states.clone(),
+                    // TODO: It seems like extra_start should be similar to repacks_start
                     extra_start: BorrowsBridge::new(),
                     extra_middle: BorrowsBridge::new(),
                 }
@@ -171,11 +172,11 @@ pub struct FreePcsBasicBlock<'tcx> {
 }
 
 impl<'tcx> FreePcsBasicBlock<'tcx> {
-    pub fn debug_lines(&self) -> Vec<String> {
+    pub fn debug_lines(&self, repacker: PlaceRepacker<'_, 'tcx>) -> Vec<String> {
         let mut result = Vec::new();
         for stmt in self.statements.iter() {
             for phase in EvalStmtPhase::phases() {
-                for line in stmt.debug_lines(phase) {
+                for line in stmt.debug_lines(phase, repacker) {
                     result.push(format!("{:?} {}: {}", stmt.location, phase, line));
                 }
             }
@@ -201,9 +202,16 @@ pub struct FreePcsLocation<'tcx> {
 }
 
 impl<'tcx> FreePcsLocation<'tcx> {
-    pub(crate) fn debug_lines(&self, phase: EvalStmtPhase) -> Vec<String> {
-        let mut result = self.states[phase].debug_lines();
-        result.extend(self.borrows[phase].debug_capability_lines());
+    pub(crate) fn debug_lines(
+        &self,
+        phase: EvalStmtPhase,
+        repacker: PlaceRepacker<'_, 'tcx>,
+    ) -> Vec<String> {
+        let mut result = self.states[phase].debug_lines(repacker);
+        for action in self.actions[phase].iter() {
+            result.push(action.debug_line(repacker));
+        }
+        result.extend(self.borrows[phase].debug_capability_lines(repacker));
         result
     }
 }
diff --git a/src/main.rs b/src/main.rs
@@ -3,6 +3,7 @@
 use std::fs::File;
 use std::io::Write;
 
+use pcs::utils::PlaceRepacker;
 use std::cell::RefCell;
 use tracing::{debug, info, trace, warn};
 use tracing_subscriber;
@@ -65,15 +66,22 @@ fn should_check_body(body: &BodyWithBorrowckFacts<'_>) -> bool {
     // true
 }
 
-fn run_pcs_on_all_fns<'tcx>(tcx: TyCtxt<'tcx>) {
+fn env_feature_enabled(feature: &str) -> bool {
+    ["true", "1"].contains(&std::env::var(feature).unwrap_or_default().as_str())
+}
+
+fn run_pcg_on_all_fns<'tcx>(tcx: TyCtxt<'tcx>) {
     let mut item_names = vec![];
 
-    let vis_dir = if std::env::var("PCS_VISUALIZATION").unwrap_or_default() == "true" {
+    let vis_dir = if env_feature_enabled("PCG_VISUALIZATION") {
         Some("visualization/data")
     } else {
         None
     };
 
+    let emit_pcg_annotations = env_feature_enabled("PCG_EMIT_ANNOTATIONS");
+    let check_pcg_annotations = env_feature_enabled("PCG_CHECK_ANNOTATIONS");
+
     if let Some(path) = &vis_dir {
         if std::path::Path::new(path).exists() {
             std::fs::remove_dir_all(path)
@@ -109,30 +117,39 @@ fn run_pcs_on_all_fns<'tcx>(tcx: TyCtxt<'tcx>) {
                         tcx,
                         vis_dir.map(|dir| format!("{}/{}", dir, item_name)),
                     );
-                    if let Ok(source) = tcx.sess.source_map().span_to_snippet(body.body.span) {
-                        let expected_annotations = source
-                            .lines()
-                            .flat_map(|l| l.split("// PCG: ").nth(1))
-                            .map(|l| l.trim())
-                            .collect::<Vec<_>>();
-                        if !expected_annotations.is_empty() {
-                            eprintln!("Expected annotations: {:?}", expected_annotations);
-                            let mut debug_lines = Vec::new();
-                            for (idx, _) in body.body.basic_blocks.iter_enumerated() {
-                                let block = output.get_all_for_bb(idx);
-                                debug_lines.extend(block.debug_lines());
+                    if emit_pcg_annotations || check_pcg_annotations {
+                        let mut debug_lines = Vec::new();
+                        for (idx, _) in body.body.basic_blocks.iter_enumerated() {
+                            let block = output.get_all_for_bb(idx);
+                            debug_lines
+                                .extend(block.debug_lines(PlaceRepacker::new(&body.body, tcx)));
+                        }
+                        if emit_pcg_annotations {
+                            for line in debug_lines.iter() {
+                                eprintln!("// PCG: {}", line);
                             }
-                            let missing_annotations = expected_annotations
-                                .iter()
-                                .filter(|a| !debug_lines.contains(&a.to_string()))
-                                .collect::<Vec<_>>();
-                            if !missing_annotations.is_empty() {
-                                panic!("Missing annotations: {:?}", missing_annotations);
+                        }
+                        if check_pcg_annotations {
+                            if let Ok(source) =
+                                tcx.sess.source_map().span_to_snippet(body.body.span)
+                            {
+                                let expected_annotations = source
+                                    .lines()
+                                    .flat_map(|l| l.split("// PCG: ").nth(1))
+                                    .map(|l| l.trim())
+                                    .collect::<Vec<_>>();
+                                if !expected_annotations.is_empty() {
+                                    let missing_annotations = expected_annotations
+                                        .iter()
+                                        .filter(|a| !debug_lines.contains(&a.to_string()))
+                                        .collect::<Vec<_>>();
+                                    if !missing_annotations.is_empty() {
+                                        panic!("Missing annotations: {:?}", missing_annotations);
+                                    }
+                                }
+                            } else {
+                                tracing::warn!("No source for function: {}", item_name);
                             }
-                            // eprintln!("Debug lines:");
-                            // for line in debug_lines {
-                            //     eprintln!("{}", line);
-                            // }
                         }
                     }
                 }
@@ -175,7 +192,7 @@ impl driver::Callbacks for PcsCallbacks {
         _compiler: &Compiler,
         queries: &'tcx Queries<'tcx>,
     ) -> Compilation {
-        queries.global_ctxt().unwrap().enter(run_pcs_on_all_fns);
+        queries.global_ctxt().unwrap().enter(run_pcg_on_all_fns);
         if std::env::var("CARGO").is_ok() {
             Compilation::Continue
         } else {
diff --git a/tests/19_lifetime_projection.rs b/tests/19_lifetime_projection.rs
@@ -7,8 +7,8 @@ struct S<'a> {
 }
 
 fn f<'a>(s: S<'a>) {
-    let x = s.x; // PCG: bb0[1] pre_operands: _1.1: E
-                 // PCG: bb0[1] pre_operands: _1.1↓'?6: E
+    let x = s.x; // PCG: bb0[1] pre_operands: s.y: E
+                 // PCG: bb0[1] pre_operands: s.y↓'?6: E
     let y = s.y.a;
 
 }
diff --git a/tests/27_aurel.rs b/tests/27_aurel.rs
@@ -1,5 +1,5 @@
 struct X<'a> { a: &'a mut i32 }
 fn foo_ref_struct<'a>(x: X<'a>) {
-    *x.a = 42;
+    *x.a = 42; // PCG: bb0[0] pre_main: Weaken *x.a from E to W
 }
 fn main(){}
diff --git a/tests/run_all_tests.rs b/tests/run_all_tests.rs
@@ -36,6 +36,7 @@ fn run_all_tests() {
 
         let status = Command::new(&pcs_exe)
             .arg(&test_file)
+            .env("PCG_CHECK_ANNOTATIONS", "true")
             .status()
             .unwrap_or_else(|e| panic!("Failed to execute test {}: {}", test_file.display(), e));
 

Original file line number	Diff line number	Diff line change
`@@ -91,8 +91,8 @@ impl<'tcx> Default for BorrowsState<'tcx> {`
`91`	`91`	`}`
`92`	`92`
`93`	`93`	`impl<'tcx> BorrowsState<'tcx> {`
`94`		`- pub(crate) fn debug_capability_lines(&self) -> Vec<String> {`
`95`		`- self.capabilities.debug_capability_lines()`
	`94`	`+ pub(crate) fn debug_capability_lines(&self, repacker: PlaceRepacker<'_, 'tcx>) -> Vec<String> {`
	`95`	`+ self.capabilities.debug_capability_lines(repacker)`
`96`	`96`	`}`
`97`	`97`	`pub(crate) fn insert(&mut self, edge: BorrowPCGEdge<'tcx>) -> bool {`
`98`	`98`	`self.graph.insert(edge)`
Original file line number	Diff line number	Diff line change
`@@ -19,7 +19,7 @@ pub struct LoopAbstraction<'tcx> {`
`19`	`19`	`}`
`20`	`20`
`21`	`21`	`impl<'tcx> DisplayWithRepacker<'tcx> for LoopAbstraction<'tcx> {`
`22`		`- fn to_short_string(&self, repacker: PlaceRepacker<'_, 'tcx>) -> String {`
	`22`	`+ fn to_short_string(&self, _repacker: PlaceRepacker<'_, 'tcx>) -> String {`
`23`	`23`	`format!("Loop({:?})", self.block)`
`24`	`24`	`}`
`25`	`25`	`}`
`@@ -73,7 +73,7 @@ pub struct FunctionCallAbstraction<'tcx> {`
`73`	`73`	`}`
`74`	`74`
`75`	`75`	`impl<'tcx> DisplayWithRepacker<'tcx> for FunctionCallAbstraction<'tcx> {`
`76`		`- fn to_short_string(&self, repacker: PlaceRepacker<'_, 'tcx>) -> String {`
	`76`	`+ fn to_short_string(&self, _repacker: PlaceRepacker<'_, 'tcx>) -> String {`
`77`	`77`	`format!("FunctionCall({:?}, {:?})", self.def_id, self.substs)`
`78`	`78`	`}`
`79`	`79`	`}`
Original file line number	Diff line number	Diff line change
`@@ -150,10 +150,10 @@ impl<'tcx> Debug for CapabilitySummary<'tcx> {`
`150`	`150`	`}`
`151`	`151`
`152`	`152`	`impl<'tcx> CapabilitySummary<'tcx> {`
`153`		`- pub(crate) fn debug_lines(&self) -> Vec<String> {`
	`153`	`+ pub(crate) fn debug_lines(&self, repacker: PlaceRepacker<'_, 'tcx>) -> Vec<String> {`
`154`	`154`	`self.0`
`155`	`155`	`.iter()`
`156`		`- .map(\|c\| c.debug_lines())`
	`156`	`+ .map(\|c\| c.debug_lines(repacker))`
`157`	`157`	`.collect::<Vec<_>>()`
`158`	`158`	`.concat()`
`159`	`159`	`}`
Original file line number	Diff line number	Diff line change
`@@ -15,7 +15,7 @@ use rustc_interface::{`
`15`	`15`	`use crate::{`
`16`	`16`	`free_pcs::{CapabilityKind, RelatedSet, RepackOp},`
`17`	`17`	`rustc_interface,`
`18`		`- utils::{Place, PlaceOrdering, PlaceRepacker},`
	`18`	`+ utils::{display::DisplayWithRepacker, Place, PlaceOrdering, PlaceRepacker},`
`19`	`19`	`};`
`20`	`20`
`21`	`21`	`#[derive(Clone, PartialEq, Eq)]`
`@@ -42,10 +42,10 @@ impl Default for CapabilityLocal<'_> {`
`42`	`42`	`}`
`43`	`43`
`44`	`44`	`impl<'tcx> CapabilityLocal<'tcx> {`
`45`		`- pub(crate) fn debug_lines(&self) -> Vec<String> {`
	`45`	`+ pub(crate) fn debug_lines(&self, repacker: PlaceRepacker<'_, 'tcx>) -> Vec<String> {`
`46`	`46`	`match self {`
`47`	`47`	`Self::Unallocated => vec![],`
`48`		`- Self::Allocated(cps) => cps.debug_lines(),`
	`48`	`+ Self::Allocated(cps) => cps.debug_lines(repacker),`
`49`	`49`	`}`
`50`	`50`	`}`
`51`	`51`
`@@ -81,9 +81,9 @@ impl<'tcx> Debug for CapabilityProjections<'tcx> {`
`81`	`81`	`}`
`82`	`82`
`83`	`83`	`impl<'tcx> CapabilityProjections<'tcx> {`
`84`		`- pub(crate) fn debug_lines(&self) -> Vec<String> {`
	`84`	`+ pub(crate) fn debug_lines(&self, repacker: PlaceRepacker<'_, 'tcx>) -> Vec<String> {`
`85`	`85`	`self.iter()`
`86`		`- .map(\|(p, k)\| format!("{p:?}: {k:?}"))`
	`86`	`+ .map(\|(p, k)\| format!("{}: {:?}", p.to_short_string(repacker), k))`
`87`	`87`	`.collect()`
`88`	`88`	`}`
`89`	`89`
Original file line number	Diff line number	Diff line change
`@@ -140,6 +140,7 @@ impl<'mir, 'tcx, D: HasPcg<'mir, 'tcx>, E: Analysis<'tcx, Domain = D>>`
`140`	`140`	`repacks_start: state.post_main().bridge(&to.post_main(), rp),`
`141`	`141`	`repacks_middle: Vec::new(),`
`142`	`142`	`borrows: entry_set.get_curr_borrow_pcg().states.clone(),`
	`143`	`+ // TODO: It seems like extra_start should be similar to repacks_start`
`143`	`144`	`extra_start: BorrowsBridge::new(),`
`144`	`145`	`extra_middle: BorrowsBridge::new(),`
`145`	`146`	`}`
`@@ -171,11 +172,11 @@ pub struct FreePcsBasicBlock<'tcx> {`
`171`	`172`	`}`
`172`	`173`
`173`	`174`	`impl<'tcx> FreePcsBasicBlock<'tcx> {`
`174`		`- pub fn debug_lines(&self) -> Vec<String> {`
	`175`	`+ pub fn debug_lines(&self, repacker: PlaceRepacker<'_, 'tcx>) -> Vec<String> {`
`175`	`176`	`let mut result = Vec::new();`
`176`	`177`	`for stmt in self.statements.iter() {`
`177`	`178`	`for phase in EvalStmtPhase::phases() {`
`178`		`- for line in stmt.debug_lines(phase) {`
	`179`	`+ for line in stmt.debug_lines(phase, repacker) {`
`179`	`180`	`result.push(format!("{:?} {}: {}", stmt.location, phase, line));`
`180`	`181`	`}`
`181`	`182`	`}`
`@@ -201,9 +202,16 @@ pub struct FreePcsLocation<'tcx> {`
`201`	`202`	`}`
`202`	`203`
`203`	`204`	`impl<'tcx> FreePcsLocation<'tcx> {`
`204`		`- pub(crate) fn debug_lines(&self, phase: EvalStmtPhase) -> Vec<String> {`
`205`		`- let mut result = self.states[phase].debug_lines();`
`206`		`- result.extend(self.borrows[phase].debug_capability_lines());`
	`205`	`+ pub(crate) fn debug_lines(`
	`206`	`+ &self,`
	`207`	`+ phase: EvalStmtPhase,`
	`208`	`+ repacker: PlaceRepacker<'_, 'tcx>,`
	`209`	`+ ) -> Vec<String> {`
	`210`	`+ let mut result = self.states[phase].debug_lines(repacker);`
	`211`	`+ for action in self.actions[phase].iter() {`
	`212`	`+ result.push(action.debug_line(repacker));`
	`213`	`+ }`
	`214`	`+ result.extend(self.borrows[phase].debug_capability_lines(repacker));`
`207`	`215`	`result`
`208`	`216`	`}`
`209`	`217`	`}`
Original file line number	Diff line number	Diff line change
`@@ -7,8 +7,8 @@ struct S<'a> {`
`7`	`7`	`}`
`8`	`8`
`9`	`9`	`fn f<'a>(s: S<'a>) {`
`10`		`- let x = s.x; // PCG: bb0[1] pre_operands: _1.1: E`
`11`		`- // PCG: bb0[1] pre_operands: _1.1↓'?6: E`
	`10`	`+ let x = s.x; // PCG: bb0[1] pre_operands: s.y: E`
	`11`	`+ // PCG: bb0[1] pre_operands: s.y↓'?6: E`
`12`	`12`	`let y = s.y.a;`
`13`	`13`
`14`	`14`	`}`
Original file line number	Diff line number	Diff line change
`@@ -1,5 +1,5 @@`
`1`	`1`	`struct X<'a> { a: &'a mut i32 }`
`2`	`2`	`fn foo_ref_struct<'a>(x: X<'a>) {`
`3`		`- *x.a = 42;`
	`3`	`+ x.a = 42; // PCG: bb0[0] pre_main: Weaken x.a from E to W`
`4`	`4`	`}`
`5`	`5`	`fn main(){}`