Fix .NET API memory leak: NativeContext finalizer, delegate lifetime, GC memory pressure (#10090)

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

@@ -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);
         }
 
 

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
 
+        /// <summary>
+        /// Finalizer.
+        /// </summary>
+        ~NativeContext()
+        {
+            Dispose();
+        }
+
         /// <summary>
         /// Disposes of the context.
         /// </summary>
         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