From 58fad41dfa34df10b69b0b5969f84e9db61f3d5f Mon Sep 17 00:00:00 2001 From: Peter Bruch <582627+ptr1120@users.noreply.github.com> Date: Thu, 22 Sep 2022 20:25:17 +0200 Subject: [PATCH] Dotnet Api: Fix infinite finalization of Context (#6361) * Dotnet Api: suppress GC finalization of dotnet context in favor of re-registering finalization * Dotnet Api: enable concurrent dec-ref even if context is created without parameters. * Dotnet Api: removed dead code. --- src/api/dotnet/CMakeLists.txt | 2 - src/api/dotnet/Context.cs | 6 +- src/api/dotnet/Deprecated.cs | 35 ----------- src/api/dotnet/IDecRefQueue.cs | 103 --------------------------------- src/api/dotnet/Z3Object.cs | 9 +-- 5 files changed, 6 insertions(+), 149 deletions(-) delete mode 100644 src/api/dotnet/Deprecated.cs delete mode 100644 src/api/dotnet/IDecRefQueue.cs diff --git a/src/api/dotnet/CMakeLists.txt b/src/api/dotnet/CMakeLists.txt index 82abfbf09..b2ba590ce 100644 --- a/src/api/dotnet/CMakeLists.txt +++ b/src/api/dotnet/CMakeLists.txt @@ -59,7 +59,6 @@ set(Z3_DOTNET_ASSEMBLY_SOURCES_IN_SRC_TREE Context.cs DatatypeExpr.cs DatatypeSort.cs - Deprecated.cs EnumSort.cs Expr.cs FiniteDomainExpr.cs @@ -76,7 +75,6 @@ set(Z3_DOTNET_ASSEMBLY_SOURCES_IN_SRC_TREE FuncInterp.cs Global.cs Goal.cs - IDecRefQueue.cs IntExpr.cs IntNum.cs IntSort.cs diff --git a/src/api/dotnet/Context.cs b/src/api/dotnet/Context.cs index 5aabcbc39..80b5a95f1 100644 --- a/src/api/dotnet/Context.cs +++ b/src/api/dotnet/Context.cs @@ -42,6 +42,7 @@ namespace Microsoft.Z3 lock (creation_lock) { m_ctx = Native.Z3_mk_context_rc(IntPtr.Zero); + Native.Z3_enable_concurrent_dec_ref(m_ctx); InitContext(); } } @@ -4794,7 +4795,6 @@ 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); } internal void CheckContextMatch(Z3Object other) @@ -4893,8 +4893,8 @@ namespace Microsoft.Z3 if (!is_external) Native.Z3_del_context(ctx); } - else - GC.ReRegisterForFinalize(this); + + GC.SuppressFinalize(this); } diff --git a/src/api/dotnet/Deprecated.cs b/src/api/dotnet/Deprecated.cs deleted file mode 100644 index 64255cea2..000000000 --- a/src/api/dotnet/Deprecated.cs +++ /dev/null @@ -1,35 +0,0 @@ -/*++ -Copyright (c) 2012 Microsoft Corporation - -Module Name: - - Deprecated.cs - -Abstract: - - Expose deprecated features for use from the managed API - those who use them for experiments. - -Author: - - Christoph Wintersteiger (cwinter) 2012-03-15 - -Notes: - ---*/ -using System.Diagnostics; -using System; -using System.Collections.Generic; -using System.Runtime.InteropServices; - -namespace Microsoft.Z3 -{ - /// - /// The main interaction with Z3 happens via the Context. - /// - public class Deprecated - { - - - } -} \ No newline at end of file diff --git a/src/api/dotnet/IDecRefQueue.cs b/src/api/dotnet/IDecRefQueue.cs deleted file mode 100644 index 8af0973d6..000000000 --- a/src/api/dotnet/IDecRefQueue.cs +++ /dev/null @@ -1,103 +0,0 @@ -/*++ -Copyright (c) 2012 Microsoft Corporation - -Module Name: - - DecRefQueue.cs - -Abstract: - - Z3 Managed API: DecRef Queues - -Author: - - Christoph Wintersteiger (cwinter) 2012-03-16 - -Notes: - ---*/ - -using System.Diagnostics; -using System; -using System.Collections; -using System.Collections.Generic; -using System.Threading; - -namespace Microsoft.Z3 -{ - /// - /// DecRefQueue interface - /// - public abstract class IDecRefQueue - { - #region Object invariant - - private void ObjectInvariant() - { - Debug.Assert(this.m_queue != null); - } - - #endregion - - readonly private Object m_lock = new Object(); - readonly private List m_queue = new List(); - private uint m_move_limit; - - internal IDecRefQueue(uint move_limit = 1024) - { - m_move_limit = move_limit; - } - - /// - /// Sets the limit on numbers of objects that are kept back at GC collection. - /// - /// - public void SetLimit(uint l) { m_move_limit = l; } - - internal abstract void IncRef(Context ctx, IntPtr obj); - internal abstract void DecRef(Context ctx, IntPtr obj); - - internal void IncAndClear(Context ctx, IntPtr o) - { - Debug.Assert(ctx != null); - - IncRef(ctx, o); - if (m_queue.Count >= m_move_limit) Clear(ctx); - } - - internal void Add(IntPtr o) - { - if (o == IntPtr.Zero) return; - - lock (m_lock) - { - m_queue.Add(o); - } - } - - internal void Clear(Context ctx) - { - Debug.Assert(ctx != null); - - lock (m_lock) - { - foreach (IntPtr o in m_queue) - DecRef(ctx, o); - m_queue.Clear(); - } - } - } - - abstract class DecRefQueueContracts : IDecRefQueue - { - internal override void IncRef(Context ctx, IntPtr obj) - { - Debug.Assert(ctx != null); - } - - internal override void DecRef(Context ctx, IntPtr obj) - { - Debug.Assert(ctx != null); - } - } -} diff --git a/src/api/dotnet/Z3Object.cs b/src/api/dotnet/Z3Object.cs index 1affa9d17..4295ef054 100644 --- a/src/api/dotnet/Z3Object.cs +++ b/src/api/dotnet/Z3Object.cs @@ -50,10 +50,7 @@ namespace Microsoft.Z3 m_n_obj = IntPtr.Zero; } - if (m_ctx != null) - { - m_ctx = null; - } + m_ctx = null; GC.SuppressFinalize(this); } @@ -81,8 +78,8 @@ namespace Microsoft.Z3 { Debug.Assert(ctx != null); m_ctx = ctx; - IncRef(obj); m_n_obj = obj; + IncRef(obj); } internal virtual void IncRef(IntPtr o) { } @@ -103,7 +100,7 @@ namespace Microsoft.Z3 internal static IntPtr GetNativeObject(Z3Object s) { - if (s == null) return new IntPtr(); + if (s == null) return IntPtr.Zero; return s.NativeObject; }