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

@@ -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

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

src/api/dotnet/Deprecated.cs

@@ -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
-{
-    /// <summary>
-    /// The main interaction with Z3 happens via the Context.
-    /// </summary>
-    public class Deprecated 
-    {
-
-
-    }
-}

src/api/dotnet/IDecRefQueue.cs

@@ -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
-{
-    /// <summary>
-    /// DecRefQueue interface
-    /// </summary>
-    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<IntPtr> m_queue = new List<IntPtr>();
-        private uint m_move_limit;
-
-        internal IDecRefQueue(uint move_limit = 1024)
-        {
-            m_move_limit = move_limit;
-        }
-
-        /// <summary>
-        /// Sets the limit on numbers of objects that are kept back at GC collection.
-        /// </summary>
-        /// <param name="l"></param>
-        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);
-        }
-    }
-}

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