From ba7b12c18c0d52a7683d89c0c42f08f3f8bc544d Mon Sep 17 00:00:00 2001
From: Copilot <198982749+Copilot@users.noreply.github.com>
Date: Sat, 11 Jul 2026 21:15:36 -0700
Subject: [PATCH] Fix .NET API memory leak: NativeContext finalizer, delegate
lifetime, GC memory pressure (#10090)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit
Creating and disposing `Context` instances causes unbounded native
memory growth (~12 GB for 100k contexts) because `NativeContext` had no
finalizer — if `Dispose()` was never called, the native Z3 context
leaked permanently. Additionally, both `Context` and `NativeContext` had
delegate lifetime and thread-safety issues in their disposal paths.
## `NativeContext.cs`
- **Add missing finalizer** `~NativeContext() { Dispose(); }` — the root
cause of permanent leaks when callers don't explicitly dispose
- **Atomic disposal** via `Interlocked.Exchange(ref m_ctx, IntPtr.Zero)`
— prevents double-free when `Dispose()` is called concurrently (e.g.
user code + finalizer race)
- **Delegate lifetime** — capture `errHandler` locally +
`GC.KeepAlive(errHandler)` after `Z3_del_context`; the GC could
otherwise collect the error handler callback before the native
destructor finishes
- **Remove dead code** — `GC.SuppressFinalize` in `InitContext()` and
`GC.ReRegisterForFinalize` in `Dispose()` were both no-ops (no finalizer
existed); the latter would have caused infinite finalization with the
new finalizer
- **GC memory pressure** — `GC.AddMemoryPressure(8MB)` on init /
`GC.RemoveMemoryPressure(8MB)` on dispose, guarded by
`m_memPressureAdded` flag, so the GC schedules finalizers promptly when
contexts accumulate
## `Context.cs`
- **Thread-safe disposal** — capture `ctx` and `errHandler` inside the
existing `lock(this)` block; previously both were read outside the lock,
allowing two concurrent callers to both capture the same non-zero `ctx`
and double-free it
- **Delegate lifetime** — same `errHandler` + `GC.KeepAlive` pattern as
`NativeContext`
- **`GC.SuppressFinalize` placement** — moved inside the `if (m_ctx !=
IntPtr.Zero)` block, before cleanup, per .NET best practice
- **GC memory pressure** — same add/remove pattern, conditioned on
`!is_external` via `m_memPressureAdded` flag
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
---
src/api/dotnet/Context.cs | 41 +++++++++++++++++++++++++++++----
src/api/dotnet/NativeContext.cs | 38 ++++++++++++++++++++++++------
2 files changed, 67 insertions(+), 12 deletions(-)
diff --git a/src/api/dotnet/Context.cs b/src/api/dotnet/Context.cs
index cba223f149..715c81626c 100644
--- a/src/api/dotnet/Context.cs
+++ b/src/api/dotnet/Context.cs
@@ -5256,6 +5256,11 @@ namespace Microsoft.Z3
internal IntPtr nCtx { get { return m_ctx; } }
private Z3_ast_print_mode m_print_mode = Z3_ast_print_mode.Z3_PRINT_SMTLIB2_COMPLIANT;
+ // Estimated native memory used per context, for GC memory pressure hints.
+ // The value is a conservative lower bound; actual usage may exceed this.
+ private const long NativeMemoryPressureEstimate = 8 * 1024 * 1024; // 8 MB
+ private bool m_memPressureAdded = false;
+
internal void NativeErrorHandler(IntPtr ctx, Z3_error_code errorCode)
{
// Do-nothing error handler. The wrappers in Z3.Native will throw exceptions upon errors.
@@ -5266,6 +5271,11 @@ namespace Microsoft.Z3
PrintMode = Z3_ast_print_mode.Z3_PRINT_SMTLIB2_COMPLIANT;
m_n_err_handler = new Native.Z3_error_handler(NativeErrorHandler); // keep reference so it doesn't get collected.
Native.Z3_set_error_handler(m_ctx, m_n_err_handler);
+ if (!is_external)
+ {
+ GC.AddMemoryPressure(NativeMemoryPressureEstimate);
+ m_memPressureAdded = true;
+ }
}
internal void CheckContextMatch(Z3Object other)
@@ -5355,17 +5365,38 @@ namespace Microsoft.Z3
m_charSort = null;
if (m_ctx != IntPtr.Zero)
{
- IntPtr ctx = m_ctx;
+ // Suppress the finalizer before performing cleanup so that it cannot
+ // run concurrently or redundantly if cleanup raises an exception.
+ GC.SuppressFinalize(this);
+ IntPtr ctx;
+ // Keep a local reference to the error handler delegate to ensure it stays
+ // alive throughout Z3_del_context. Setting m_n_err_handler = null releases
+ // the field reference; without the local variable the GC could collect the
+ // delegate before the native destructor finishes using the handler.
+ Native.Z3_error_handler errHandler;
lock (this)
{
+ ctx = m_ctx;
+ errHandler = m_n_err_handler;
m_n_err_handler = null;
m_ctx = IntPtr.Zero;
}
- if (!is_external)
- Native.Z3_del_context(ctx);
+ // ctx is non-zero only for the thread that wins the lock and zeros m_ctx,
+ // preventing double-free when Dispose() is called concurrently.
+ if (ctx != IntPtr.Zero)
+ {
+ if (!is_external)
+ {
+ Native.Z3_del_context(ctx);
+ GC.KeepAlive(errHandler);
+ }
+ if (m_memPressureAdded)
+ {
+ GC.RemoveMemoryPressure(NativeMemoryPressureEstimate);
+ m_memPressureAdded = false;
+ }
+ }
}
-
- GC.SuppressFinalize(this);
}
diff --git a/src/api/dotnet/NativeContext.cs b/src/api/dotnet/NativeContext.cs
index afae66e468..0b0b71f73f 100644
--- a/src/api/dotnet/NativeContext.cs
+++ b/src/api/dotnet/NativeContext.cs
@@ -1334,6 +1334,11 @@ namespace Microsoft.Z3
internal Native.Z3_error_handler m_n_err_handler = null;
internal IntPtr nCtx { get { return m_ctx; } }
+ // Estimated native memory used per context, for GC memory pressure hints.
+ // The value is a conservative lower bound; actual usage may exceed this.
+ private const long NativeMemoryPressureEstimate = 8 * 1024 * 1024; // 8 MB
+ private bool m_memPressureAdded = false;
+
internal void NativeErrorHandler(IntPtr ctx, Z3_error_code errorCode)
{
// Do-nothing error handler. The wrappers in Z3.Native will throw exceptions upon errors.
@@ -1344,8 +1349,8 @@ namespace Microsoft.Z3
PrintMode = Z3_ast_print_mode.Z3_PRINT_SMTLIB2_COMPLIANT;
m_n_err_handler = new Native.Z3_error_handler(NativeErrorHandler); // keep reference so it doesn't get collected.
Native.Z3_set_error_handler(m_ctx, m_n_err_handler);
-
- GC.SuppressFinalize(this);
+ GC.AddMemoryPressure(NativeMemoryPressureEstimate);
+ m_memPressureAdded = true;
}
#endregion
@@ -1365,20 +1370,39 @@ namespace Microsoft.Z3
#region Dispose
+ ///
+ /// Finalizer.
+ ///
+ ~NativeContext()
+ {
+ Dispose();
+ }
+
///
/// Disposes of the context.
///
public void Dispose()
{
- if (m_ctx != IntPtr.Zero)
+ IntPtr ctx = System.Threading.Interlocked.Exchange(ref m_ctx, IntPtr.Zero);
+ if (ctx != IntPtr.Zero)
{
+ // Suppress the finalizer before performing cleanup so that it cannot
+ // run concurrently or redundantly if cleanup raises an exception.
+ GC.SuppressFinalize(this);
+ // Keep a local reference to the error handler delegate to ensure it stays
+ // alive throughout Z3_del_context. Setting m_n_err_handler = null releases
+ // the field reference; without the local variable the GC could collect the
+ // delegate before the native destructor finishes using the handler.
+ var errHandler = m_n_err_handler;
m_n_err_handler = null;
- IntPtr ctx = m_ctx;
- m_ctx = IntPtr.Zero;
Native.Z3_del_context(ctx);
+ GC.KeepAlive(errHandler);
+ if (m_memPressureAdded)
+ {
+ GC.RemoveMemoryPressure(NativeMemoryPressureEstimate);
+ m_memPressureAdded = false;
+ }
}
- else
- GC.ReRegisterForFinalize(this);
}
#endregion