Fix coupling (#123)

* Fix coupling

* WIP

* WIP

* WIP

* WIP

* Add pcg-macros crate with DisplayWithCtxt derive macro

Co-authored-by: zgrannan <zgrannan@protonmail.com>

* Add DisplayWithCtxt derive to enums, remove impl from edgedata_enum macro

- Update pcg-macros derive macro to add bounds based on field types
- Add derive macro to FunctionCallOrLoop, BorrowPcgExpansion, BorrowPcgEdgeKind
- Remove DisplayWithCtxt impl generation from edgedata_enum! macro

Co-authored-by: zgrannan <zgrannan@protonmail.com>

* Fix rustfmt formatting issues in pcg-macros

Co-authored-by: zgrannan <zgrannan@protonmail.com>

* WIP

* WIP

* WIP

* Simple union-find based coupling

* Update tests

* small fixes

* small fixes

* remove usage of global settings

* Appease rustfmt

* whoops

---------

Co-authored-by: Cursor Agent <cursoragent@cursor.com>

Author: zgrannan

.github/workflows/test.yml

@@ -12,8 +12,8 @@ env:
   IMAGE_NAME: ${{ github.repository }}/pcg-server
   MUTATION_TESTS_REF: zgrannan/update-pcg
   FLOWISTRY_REF: zgrannan/pcg-next4
-  SYMBOLIC_EXECUTION_REF: zgrannan/pcg-fix-nested
-  PURIFICATION_PRUSTI_REF: zgrannan/next5
+  SYMBOLIC_EXECUTION_REF: main
+  PURIFICATION_PRUSTI_REF: zgrannan/old-purification
 
 jobs:
   check_warnings:

.vscode/settings.json

@@ -1,4 +1,4 @@
 {
     "rust-analyzer.rustc.source": "discover",
-    "rust-analyzer.cargo.features": ["visualization", "coupling"]
+    "rust-analyzer.cargo.features": ["visualization"]
 }

Cargo.lock

@@ -8,11 +8,11 @@ edition = "2024"
 custom-rust-toolchain = []
 visualization = []
 debug_info = []
-coupling = []
 type-export = ["specta"]
-default = ["visualization", "coupling"]
+default = ["visualization"]
 
 [dependencies]
+pcg-macros = { path = "pcg-macros" }
 bit-set = "0.8.0"
 bumpalo = {version = "3.16.0", features = ["allocator_api"]}
 derive_more = { version = "2.0.1", features = ["full"] }
@@ -30,6 +30,7 @@ strum = "0.26"
 strum_macros = "0.26"
 tracing = "0.1"
 tracing-subscriber = "0.3.20"
+union-find = "0.4"
 
 [dev-dependencies]
 reqwest = { version = "^0.11", features = ["blocking"] }

Cargo.toml

@@ -9,7 +9,7 @@ authors = ["Prusti Devs <prusti_developers@sympa.ethz.ch>"]
 edition = "2024"
 
 [dependencies]
-pcg = { path = "..", features = ["visualization", "coupling"] }
+pcg = { path = "..", features = ["visualization"] }
 borrowck-body-storage = { path = "../borrowck-body-storage" }
 shell-escape = "0.1.5"
 tracing = "0.1"

pcg-bin/Cargo.lock

@@ -0,0 +1,12 @@
+[package]
+name = "pcg-macros"
+version = "0.1.0"
+edition = "2024"
+
+[lib]
+proc-macro = true
+
+[dependencies]
+proc-macro2 = "1.0"
+quote = "1.0"
+syn = { version = "2.0", features = ["full", "extra-traits"] }

pcg-bin/Cargo.toml

@@ -0,0 +1,118 @@
+use proc_macro::TokenStream;
+use quote::{ToTokens, quote};
+use syn::{Data, DeriveInput, Fields, GenericParam, Type, parse_macro_input};
+
+/// Derive macro for `DisplayWithCtxt` on enums where each variant has a single field.
+///
+/// This generates an implementation that requires a context type `Ctxt` where
+/// `Ctxt: Copy` and each variant's inner type implements `DisplayWithCtxt<Ctxt>`.
+///
+/// Example:
+/// ```ignore
+/// #[derive(DisplayWithCtxt)]
+/// pub enum FunctionCallOrLoop<FunctionCallData, LoopData> {
+///     FunctionCall(FunctionCallData),
+///     Loop(LoopData),
+/// }
+/// ```
+///
+/// Generates:
+/// ```ignore
+/// impl<FunctionCallData, LoopData, Ctxt: Copy> DisplayWithCtxt<Ctxt>
+///     for FunctionCallOrLoop<FunctionCallData, LoopData>
+/// where
+///     FunctionCallData: DisplayWithCtxt<Ctxt>,
+///     LoopData: DisplayWithCtxt<Ctxt>,
+/// {
+///     fn display_output(&self, ctxt: Ctxt, mode: OutputMode) -> DisplayOutput {
+///         match self {
+///             FunctionCallOrLoop::FunctionCall(inner) => inner.display_output(ctxt, mode),
+///             FunctionCallOrLoop::Loop(inner) => inner.display_output(ctxt, mode),
+///         }
+///     }
+/// }
+/// ```
+#[proc_macro_derive(DisplayWithCtxt)]
+pub fn derive_display_with_ctxt(input: TokenStream) -> TokenStream {
+    let input = parse_macro_input!(input as DeriveInput);
+
+    let name = &input.ident;
+    let generics = &input.generics;
+
+    let Data::Enum(data_enum) = &input.data else {
+        return syn::Error::new_spanned(&input, "DisplayWithCtxt can only be derived for enums")
+            .to_compile_error()
+            .into();
+    };
+
+    let mut variant_arms = Vec::new();
+    let mut field_types: Vec<&Type> = Vec::new();
+
+    for variant in &data_enum.variants {
+        let variant_name = &variant.ident;
+
+        match &variant.fields {
+            Fields::Unnamed(fields) if fields.unnamed.len() == 1 => {
+                let field = fields.unnamed.first().unwrap();
+                field_types.push(&field.ty);
+                variant_arms.push(quote! {
+                    #name::#variant_name(inner) => inner.display_output(ctxt, mode)
+                });
+            }
+            _ => {
+                return syn::Error::new_spanned(
+                    variant,
+                    "DisplayWithCtxt requires each variant to have exactly one unnamed field",
+                )
+                .to_compile_error()
+                .into();
+            }
+        }
+    }
+
+    let (_impl_generics, ty_generics, where_clause) = generics.split_for_impl();
+
+    let existing_where_predicates = where_clause.map(|w| &w.predicates);
+
+    let where_bounds = field_types.iter().map(|ty| {
+        quote! { #ty: crate::utils::display::DisplayWithCtxt<Ctxt> }
+    });
+
+    let existing_impl_params: Vec<_> = generics
+        .params
+        .iter()
+        .map(|param| match param {
+            GenericParam::Type(ty) => {
+                let ident = &ty.ident;
+                let bounds = &ty.bounds;
+                if bounds.is_empty() {
+                    quote! { #ident }
+                } else {
+                    quote! { #ident: #bounds }
+                }
+            }
+            other => other.to_token_stream(),
+        })
+        .collect();
+
+    let expanded = quote! {
+        impl<#(#existing_impl_params,)* Ctxt: Copy> crate::utils::display::DisplayWithCtxt<Ctxt>
+            for #name #ty_generics
+        where
+            #(#where_bounds,)*
+            #existing_where_predicates
+        {
+            fn display_output(
+                &self,
+                ctxt: Ctxt,
+                mode: crate::utils::display::OutputMode,
+            ) -> crate::utils::display::DisplayOutput {
+                match self {
+                    #(#variant_arms,)*
+                }
+            }
+        }
+    };
+
+    TokenStream::from(expanded)
+}

pcg-macros/Cargo.toml

@@ -5,12 +5,13 @@ authors = ["Prusti Devs <prusti_developers@sympa.ethz.ch>"]
 edition = "2024"
 
 [dependencies]
-pcg = { path = "..", features = ["visualization", "coupling"] }
+pcg = { path = "..", features = ["visualization"] }
 borrowck-body-storage = { path = "../borrowck-body-storage" }
 chrono = "0.4"
 derive_more = { version = "2.0.1", features = ["full"] }
 itertools = "0.12.0"
 rayon = "1.8"
+regex = "1"
 reqwest = { version = "^0.11", features = ["blocking"] }
 rustversion = "1.0"
 serde = "1.0"