mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

Bugfix for concurrent Context creation in Java and .NET.

Browse source 
Relates to #205 #245
This commit is contained in:
Christoph M. Wintersteiger 2015-10-14 13:58:51 +01:00
parent 2d2ec38541
commit 24532474a0
3 changed files with 44 additions and 26 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

23
src/api/dotnet/Context.cs
View file

@ -37,8 +37,11 @@ namespace Microsoft.Z3
public Context() public Context()
: base() : base()
{ {
m_ctx = Native.Z3_mk_context_rc(IntPtr.Zero); lock (creation_lock)
InitContext(); {
m_ctx = Native.Z3_mk_context_rc(IntPtr.Zero);
InitContext();
}
} }
/// <summary> /// <summary>
@ -64,12 +67,15 @@ namespace Microsoft.Z3
{ {
Contract.Requires(settings != null); Contract.Requires(settings != null);
IntPtr cfg = Native.Z3_mk_config(); lock (creation_lock)
foreach (KeyValuePair<string, string> kv in settings) {
Native.Z3_set_param_value(cfg, kv.Key, kv.Value); IntPtr cfg = Native.Z3_mk_config();
m_ctx = Native.Z3_mk_context_rc(cfg); foreach (KeyValuePair<string, string> kv in settings)
Native.Z3_del_config(cfg); Native.Z3_set_param_value(cfg, kv.Key, kv.Value);
InitContext(); m_ctx = Native.Z3_mk_context_rc(cfg);
Native.Z3_del_config(cfg);
InitContext();
}
} }
#endregion #endregion
@ -4381,6 +4387,7 @@ namespace Microsoft.Z3
#region Internal #region Internal
internal IntPtr m_ctx = IntPtr.Zero; internal IntPtr m_ctx = IntPtr.Zero;
internal Native.Z3_error_handler m_n_err_handler = null; internal Native.Z3_error_handler m_n_err_handler = null;
internal static Object creation_lock = new Object();
internal IntPtr nCtx { get { return m_ctx; } } internal IntPtr nCtx { get { return m_ctx; } }
internal void NativeErrorHandler(IntPtr ctx, Z3_error_code errorCode) internal void NativeErrorHandler(IntPtr ctx, Z3_error_code errorCode)

25
src/api/java/Context.java
View file

@ -30,10 +30,12 @@ public class Context extends IDisposable
* Constructor. * Constructor.
**/ **/
public Context() public Context()
{ {
super(); super();
m_ctx = Native.mkContextRc(0); synchronized (creation_lock) {
initContext(); m_ctx = Native.mkContextRc(0);
initContext();
}
} }
/** /**
@ -56,12 +58,14 @@ public class Context extends IDisposable
public Context(Map<String, String> settings) public Context(Map<String, String> settings)
{ {
super(); super();
long cfg = Native.mkConfig(); synchronized (creation_lock) {
for (Map.Entry<String, String> kv : settings.entrySet()) long cfg = Native.mkConfig();
Native.setParamValue(cfg, kv.getKey(), kv.getValue()); for (Map.Entry<String, String> kv : settings.entrySet())
m_ctx = Native.mkContextRc(cfg); Native.setParamValue(cfg, kv.getKey(), kv.getValue());
Native.delConfig(cfg); m_ctx = Native.mkContextRc(cfg);
initContext(); Native.delConfig(cfg);
initContext();
}
} }
/** /**
@ -3638,7 +3642,8 @@ public class Context extends IDisposable
Native.updateParamValue(nCtx(), id, value); Native.updateParamValue(nCtx(), id, value);
} }
long m_ctx = 0; protected long m_ctx = 0;
protected static Object creation_lock = new Object();
long nCtx() long nCtx()
{ {

22
src/api/java/InterpolationContext.java
View file

@ -35,8 +35,11 @@ public class InterpolationContext extends Context
**/ **/
public InterpolationContext() public InterpolationContext()
{ {
m_ctx = Native.mkInterpolationContext(0); super();
initContext(); synchronized(creation_lock) {
m_ctx = Native.mkInterpolationContext(0);
initContext();
}
} }
/** /**
@ -48,12 +51,15 @@ public class InterpolationContext extends Context
**/ **/
public InterpolationContext(Map<String, String> settings) public InterpolationContext(Map<String, String> settings)
{ {
long cfg = Native.mkConfig(); super();
for (Map.Entry<String, String> kv : settings.entrySet()) synchronized(creation_lock) {
Native.setParamValue(cfg, kv.getKey(), kv.getValue()); long cfg = Native.mkConfig();
m_ctx = Native.mkInterpolationContext(cfg); for (Map.Entry<String, String> kv : settings.entrySet())
Native.delConfig(cfg); Native.setParamValue(cfg, kv.getKey(), kv.getValue());
initContext(); m_ctx = Native.mkInterpolationContext(cfg);
Native.delConfig(cfg);
initContext();
}
} }
/** /**