z3 crashes on sys.exit in python

[cdonovick]

#!/usr/bin/env python3
import z3
import sys
s = z3.Solver()
sys.exit(1)

Nondeterministically (about %50) terminates with the following output to stderr

Exception ignored in: <object repr() failed>
Traceback (most recent call last):
 File ".../python3.5/site-packages/z3/z3.py", line 5915, in __del__
 File ".../python3.5/site-packages/z3/z3core.py", line 4060, in Z3_solver_dec_ref
TypeError: 'NoneType' object is not callable

If I declare a literal (e.g. x = z3.BitVec('x', 16)) in addition to first error I get:

Exception ignored in: <object repr() failed>
Traceback (most recent call last):
  File ".../python3.5/site-packages/z3/z3.py", line 289, in __del__
  File ".../python3.5/site-packages/z3/z3core.py", line 1302, in Z3_solver_dec_ref
TypeError: 'NoneType' object is not callable

My enviroment
Ubuntu 16.04.1 LTS (xenial)
Python 3.5.2
Z3 version 4.5.1 - 64 (commit: 69aa5ca)

[wintersteiger]

Thanks for reporting this issue! I'm able to reproduce it on Windows as well. Looks like a cleanup problem that should be easy to fix.

[NikolajBjorner]

I was never able to reproduce this and I am not sure what the bug would be.

[cdonovick]

Just rebuilt from most recent commit (e48e7ef) and it is definitely still happening for me (nondeterministic).

running the following is sufficient for me to generate the error

  1 #!/usr/bin/env python3                                                                                                                                                                                                                    
  2                                                                                                                                                                                                                                           
  3 import z3                                                                                                                                                                                                                                 
  4 import sys                                                                                                                                                                                                                                
  5 s = z3.Solver()                                                                                                                                                                                                                           
  6 x = z3.BitVec('x', 16)                                                                                                                                                                                                                    
  7 sys.exit(1)

% ./test.py
Exception ignored in: <object repr() failed>
Traceback (most recent call last):
  File ".../python3.5/site-packages/z3/z3.py", line 5999, in __del__
  File ".../python3.5/site-packages/z3/z3core.py", line 4082, in Z3_solver_dec_ref
TypeError: 'NoneType' object is not callable
Exception ignored in: <object repr() failed>
Traceback (most recent call last):
  File ".../python3.5/site-packages/z3/z3.py", line 290, in __del__
  File ".../python3.5/site-packages/z3/z3core.py", line 1302, in Z3_dec_ref
TypeError: 'NoneType' object is not callable

[wintersteiger]

Yes, I know what the problem is and what the fix is, but I haven't had time to write down the fix yet. I can reproduce it on my machine, but it's non-deterministic. The fix may also incur extra runtime overhead, so I'll have to run some tests to see how bad that is.

(The problem is that Python collects z3core._lib while some functions from z3core still need to call Z3 functions.)

[NikolajBjorner]

Not sure if I properly understood the contract with the Python GC, but here is an attempt at addressing the bug.

[wintersteiger]

Looks like a reasonable attempt to me, thanks for taking this on! Doesn't this mean we can remove def lib(): ... altogether now?

Here's my unedited repro of the original problem with multitudes of options:

#!/usr/bin/env python3

import gc
gc.disable()
# gc.set_debug(gc.DEBUG_STATS | gc.DEBUG_UNCOLLECTABLE)

import z3
import sys

ctx = z3.Context()
s = z3.Solver(ctx=ctx)
# print("past s: " + str(type(z3.z3core._lib)))
# del s
#gc.collect()
for obj in gc.garbage:
    print("GARBAGE: " + str(obj))
# print("referrers:")
# for r in gc.get_referrers(s):
#     print(r)
print("referents:")
for r in gc.get_referents(ctx):
    print(r)
# gcit = gc.is_tracked(z3.z3core._glib)
# if not gcit:
#     print("NOT TRACKED")
sys.exit(1)

It's non-determinstic but fails fairly frequently. The sys.exit(1) call at the end is necessary, because it makes Python cut all corners it's allowed to cut.

Script to make it run lots of times:

for /L %%I in (1,1,100) do (
    echo ------
    c:\Python35\python.exe gh989.py
    ...

[NikolajBjorner]

• lib() is used one place in z3.py.
• I now also added what should be 'the real' guard against this crash: to check that _lib is set in the calls that reference it.
  We could go back to the dynamic version of lib(), but I don't see any reason for this at this point.
  What remains is to double check that this is indeed a fix.

[wintersteiger]

Just checking whether _lib is still there will produce memory leaks, which may or may not matter for some applications. I think it's unlikely that there are many Python applications for which this will matter though.

[NikolajBjorner]

touché

[NikolajBjorner]

can this be closed now? I believe this addresses the problem.

[wintersteiger]

Were you able to reproduce the problem pre-fix and not able post-fix? If not, I suppose I'll have to run some tests to verify that it works as intended now.

[NikolajBjorner]

What I could observe was that the GC would collect objects in different orders and this fix is to take care of the different possible orders.

[wintersteiger]

So, that's a 'no' then, I guess? I'll need a few hours to reproduce the pre-fix state.

[NikolajBjorner]

correct, thanks

[wintersteiger]

Hmm. Sorry, but your changes only changed the GC order, they didn't fix any of the problems:

  _lib = lib()
  if _lib.Z3_qe_model_project_skolem is None:
     return

At the crucial time _lib == None; thus the "best" case is a memory leak (Z3_*_dec_ref will not be called at all). Then, "no" return value will not be expected by any of the client applications (better to throw an exception in my opinion). And, worst of all:

Exception ignored in: <object repr() failed>
Traceback (most recent call last):
  File "F:\dev\z3-master\build\python\z3\z3.py", line 5999, in __del__
  File "F:\dev\z3-master\build\python\z3\z3core.py", line 5356, in Z3_solver_dec_ref
TypeError: 'NoneType' object is not callable

Here's my repro:

import z3
import sys

ctx = z3.Context()
s = z3.Solver(ctx=ctx)
sys.exit(1)

Run it like so:

@echo off 
@setlocal

REM SET PATH=%PATH%;c:\dev\z3\bld_dbg
REM SET PYTHON=C:\Python36\python.exe
REM SET PYTHONPATH=c:\dev\z3\src\api\python

SET PATH=%PATH%;F:\dev\z3-master\build
SET PYTHON=C:\Python35_x86\python.exe
SET PYTHONPATH=F:\dev\z3-master\build\python

for /L %%I in (1,1,100) do (
    echo ------
    %PYTHON% gh989.py
    if %ERRORLEVEL% neq 0 (
       goto :end
    )
)

:end

For me it doesn't repro using Python 3.6, only 3.5 (x86) at a rate of about 9 runs out of 100.

[wintersteiger]

Took longer than expected, but now this problem should be fixed.