mirror of
https://github.com/Z3Prover/z3
synced 2026-08-09 23:42:21 +00:00
ba7b12c18c
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>
|
||
|---|---|---|
| .. | ||
| Properties | ||
| AlgebraicNum.cs | ||
| ApplyResult.cs | ||
| ArithExpr.cs | ||
| ArithSort.cs | ||
| ArrayExpr.cs | ||
| ArraySort.cs | ||
| AST.cs | ||
| ASTMap.cs | ||
| ASTVector.cs | ||
| BitVecExpr.cs | ||
| BitVecNum.cs | ||
| BitVecSort.cs | ||
| BoolExpr.cs | ||
| BoolSort.cs | ||
| CharSort.cs | ||
| cmake_install_gac.cmake.in | ||
| cmake_uninstall_gac.cmake.in | ||
| CMakeLists.txt | ||
| Constructor.cs | ||
| ConstructorList.cs | ||
| Context.cs | ||
| DatatypeExpr.cs | ||
| DatatypeSort.cs | ||
| EnumSort.cs | ||
| Expr.cs | ||
| FiniteDomainExpr.cs | ||
| FiniteDomainNum.cs | ||
| FiniteDomainSort.cs | ||
| FiniteSetSort.cs | ||
| Fixedpoint.cs | ||
| FPExpr.cs | ||
| FPNum.cs | ||
| FPRMExpr.cs | ||
| FPRMNum.cs | ||
| FPRMSort.cs | ||
| FPSort.cs | ||
| FuncDecl.cs | ||
| FuncInterp.cs | ||
| Global.cs | ||
| Goal.cs | ||
| IntExpr.cs | ||
| IntNum.cs | ||
| IntSort.cs | ||
| IntSymbol.cs | ||
| Lambda.cs | ||
| ListSort.cs | ||
| Log.cs | ||
| Microsoft.Z3.csproj.in | ||
| Microsoft.Z3.props | ||
| Microsoft.Z3.Sharp.pc.in | ||
| Microsoft.Z3.snk | ||
| Microsoft.Z3.targets | ||
| Microsoft.Z3.targets.in | ||
| Model.cs | ||
| NativeContext.cs | ||
| NativeFuncInterp.cs | ||
| NativeModel.cs | ||
| NativeSolver.cs | ||
| OnClause.cs | ||
| Optimize.cs | ||
| ParamDescrs.cs | ||
| Params.cs | ||
| Pattern.cs | ||
| Probe.cs | ||
| Quantifier.cs | ||
| RatNum.cs | ||
| RCFNum.cs | ||
| README.md | ||
| RealExpr.cs | ||
| RealSort.cs | ||
| ReExpr.cs | ||
| RelationSort.cs | ||
| ReSort.cs | ||
| SeqExpr.cs | ||
| SeqSort.cs | ||
| SetSort.cs | ||
| Simplifiers.cs | ||
| Solver.cs | ||
| Sort.cs | ||
| Statistics.cs | ||
| Status.cs | ||
| StringSymbol.cs | ||
| Symbol.cs | ||
| Tactic.cs | ||
| TupleSort.cs | ||
| UninterpretedSort.cs | ||
| UserPropagator.cs | ||
| Version.cs | ||
| Z3Exception.cs | ||
| Z3Object.cs | ||
Z3 Nuget Package
For more information see the Z3 github page