{"action":"created","issue":{"url":"https://api.github.com/repos/stp/stp/issues/296","repository_url":"https://api.github.com/repos/stp/stp","labels_url":"https://api.github.com/repos/stp/stp/issues/296/labels{/name}","comments_url":"https://api.github.com/repos/stp/stp/issues/296/comments","events_url":"https://api.github.com/repos/stp/stp/issues/296/events","html_url":"https://github.com/stp/stp/issues/296","id":383166018,"node_id":"MDU6SXNzdWUzODMxNjYwMTg=","number":296,"title":"Building with MinGW leads to SIGSEGV during application close","user":{"login":"andrewvaughanj","id":14277540,"node_id":"MDQ6VXNlcjE0Mjc3NTQw","avatar_url":"https://avatars1.githubusercontent.com/u/14277540?v=4","gravatar_id":"","url":"https://api.github.com/users/andrewvaughanj","html_url":"https://github.com/andrewvaughanj","followers_url":"https://api.github.com/users/andrewvaughanj/followers","following_url":"https://api.github.com/users/andrewvaughanj/following{/other_user}","gists_url":"https://api.github.com/users/andrewvaughanj/gists{/gist_id}","starred_url":"https://api.github.com/users/andrewvaughanj/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/andrewvaughanj/subscriptions","organizations_url":"https://api.github.com/users/andrewvaughanj/orgs","repos_url":"https://api.github.com/users/andrewvaughanj/repos","events_url":"https://api.github.com/users/andrewvaughanj/events{/privacy}","received_events_url":"https://api.github.com/users/andrewvaughanj/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":3,"created_at":"2018-11-21T15:18:54Z","updated_at":"2018-11-22T15:08:18Z","closed_at":null,"author_association":"NONE","body":"Hi,\r\n\r\nI wrote up the Windows build instructions for Boolector here: <https://github.com/andrewvaughanj/boolector/blob/windows_build/COMPILING_WIN32.md>.\r\n\r\nThese instructions work to allow me to build Boolector binaries on Windows, such that they are compatible with \"official\" Windows Python 2.7. I have also used the same steps and setup (albeit with a different version of MinGW) to build Z3 on Windows, such that the Python bindings also work with the official Python 2.7. These instructions are also for building a _32-bit_ version of these libraries.\r\n\r\nThese build steps have been written to assist in creating DLLs that are free from Cygwin altogether (i.e., the builds can be performed without Cygwin at all) -- this means the resulting DLLs (if statically linked) are extremely portable between hosts.\r\n\r\nWith some slight modifications (e.g., installing Bison, Flex and Perl with MSys: `pacman -S --needed bison flex perl`), I have also been able to _build_ STP using a very similar setup. Here's an automated script to build it all, once the necessary prerequisites have been installed:\r\n\r\n```bash\r\n#!/bin/bash\r\n\r\nset -x\r\nset -u\r\nset -e\r\nset -v\r\n\r\nfunction cleanup()\r\n{\r\n    rm -rf \"${INSTALL_DIR}\"\r\n    mkdir \"${INSTALL_DIR}\"\r\n    mkdir \"${INSTALL_DIR}/python\"\r\n    mkdir \"${INSTALL_DIR}/lib\"\r\n    mkdir \"${INSTALL_DIR}/bin\"\r\n}\r\n\r\nfunction setenv()\r\n{\r\n    cmd /c \"subst /D n:\"\r\n    # cmd /c \"subst n: \\\"C:\\Program Files\\mingw-w64\\x86_64-6.4.0-posix-seh-rt_v5-rev0\\mingw64\\\"\"\r\n    cmd /c \"subst n: \\\"C:\\Program Files (x86)\\mingw-w64\\i686-6.4.0-posix-dwarf-rt_v5-rev0\\mingw32\\\"\"\r\n    # cmd /c \"subst n: \\\"C:\\Program Files (x86)\\mingw-w64\\i686-8.1.0-win32-dwarf-rt_v6-rev0\\mingw32\\\"\"\r\n\r\n    export PYTHON_DIR=$(cygpath -u \"C:\\Python27\")\r\n    export CMAKE_DIR=$(cygpath -u \"C:\\cmake-3.12.4-win32-x86\")\r\n    export MINGW_DIR=$(cygpath -u $(cygpath -d \"$(cygpath -u 'N:\\')\"))\r\n\r\n    export PATH=\"${PYTHON_DIR}:${PATH}\"\r\n    export PATH=\"${PYTHON_DIR}/Scripts:${PATH}\"\r\n    export PATH=\"${CMAKE_DIR}/bin:${PATH}\"\r\n    export PATH=\"${MINGW_DIR}/bin:${PATH}\"\r\n\r\n    export PATH=\"${INSTALL_DIR}/lib:${INSTALL_DIR}/bin:${PATH}\"\r\n\r\n    export DEBUG_FLAG=\"-ggdb3\"\r\n    export COMPARCH=32   # for a 32-bit build!\r\n    # export COMPARCH=64   # for a 64-bit build!\r\n\r\n    #\r\n    # Force a static build on Win32\r\n    #\r\n    export EXTRA_FLAGS=\"-static-libstdc++ -static-libgcc\"\r\n    export COMPFLAGS=\"${EXTRA_FLAGS} -I${PYTHON_DIR}/include -m${COMPARCH}\"\r\n\r\n    #\r\n    # Disable all optimisations\r\n    #\r\n    export COMPFLAGS=\"-O0 ${COMPFLAGS}\"\r\n\r\n    #\r\n    # STP enables the following define if MSVC, which we don't have\r\n    #\r\n    export COMPFLAGS=\"-DSTP_SHARED_LIB ${COMPFLAGS}\"\r\n\r\n    export CFLAGS=\"${COMPFLAGS}\"\r\n    export CXXFLAGS=\"${COMPFLAGS}\"\r\n    export LDFLAGS=\"${EXTRA_FLAGS} -L${PYTHON_DIR}/lib\"\r\n\r\n    export CC=\"gcc\"\r\n    export CXX=\"g++\"\r\n    export AR=\"ar\"\r\n}\r\n\r\nfunction build_zlib()\r\n{\r\n    cd \"${ROOT}\"\r\n    rm -rf zlib\r\n    git clone https://github.com/madler/zlib\r\n    cd zlib\r\n    git checkout v1.2.8\r\n    mkdir build\r\n    cd build\r\n    cmake -DCMAKE_INSTALL_PREFIX=\"../../${INSTALL_DIR}\" -G \"MSYS Makefiles\" ..\r\n    cmake --build .\r\n    cmake --build . --target install\r\n}\r\n\r\nfunction build_minisat()\r\n{\r\n    cd \"${ROOT}\"\r\n    rm -rf minisat\r\n\r\n    git clone https://github.com/stp/minisat\r\n    cd minisat\r\n    git checkout a259927\r\n    mkdir build\r\n    cd build\r\n    cmake -DCMAKE_INSTALL_PREFIX=\"../../${INSTALL_DIR}\" -DZLIB_ROOT=\"../../${INSTALL_DIR}\" -G \"MSYS Makefiles\" ..\r\n    cmake --build .\r\n    cmake --build . --target install\r\n}\r\n\r\nfunction build_stp()\r\n{\r\n    cd \"${ROOT}\"\r\n\r\n    export EXTRA_FLAGS=\"-Wl,-allow-multiple-definition -Wl,-Bstatic,--whole-archive -lwinpthread -Wl,--no-whole-archive -Wl,-Bdynamic\"\r\n    export CFLAGS=\"${EXTRA_FLAGS} ${CFLAGS}\"\r\n    export CXXFLAGS=\"${EXTRA_FLAGS} ${CXXFLAGS}\"\r\n    export LDFLAGS=\"${EXTRA_FLAGS} ${LDFLAGS}\"\r\n\r\n    rm -rf stp\r\n\r\n    git clone https://github.com/stp/stp\r\n    cd stp\r\n    git checkout 15943d7\r\n    git submodule update --init --recursive\r\n    rm -rf build\r\n    mkdir build\r\n    cd build\r\n    cmake -DCMAKE_BUILD_TYPE=Debug -DBoost_USE_STATIC_LIBS=ON -DENABLE_TESTING=ON -DENABLE_PYTHON_INTERFACE=ON -DPYTHON_EXECUTABLE=\"$(cygpath -d $(which python))\" -DLIT_TOOL=\"$(cygpath -d $(which lit))\" -DMINISAT_LIBDIR=\"../../${INSTALL_DIR}/lib\" -DMINISAT_INCLUDE_DIR=\"../../${INSTALL_DIR}/include\" -DMINISAT_LIBRARY=\"../../${INSTALL_DIR}/lib/libminisat.a\" -DZLIB_INCLUDE_DIR=\"../../${INSTALL_DIR}/include\" -DZLIB_LIBRARY=\"../../${INSTALL_DIR}/lib/libzlibstatic.a\" -DCMAKE_INSTALL_PREFIX=\"../../${INSTALL_DIR}\" -DPYTHON_LIB_INSTALL_DIR=\"../../${INSTALL_DIR}/python\" -G \"MSYS Makefiles\" ..\r\n    cmake --build .\r\n    cmake --build . --target install\r\n    cmake --build . --target test || true\r\n}\r\n\r\nfunction copy_files()\r\n{\r\n    cd \"${ROOT}\"\r\n\r\n    #\r\n    # If you don't build statically, you need these\r\n    #\r\n    # cp /n/bin/libstdc++-6.dll $INSTALL_DIR/bin\r\n    # cp /n/bin/libgcc_s_dw2-1.dll $INSTALL_DIR/bin\r\n    #\r\n    cp ./stp/build/bin/libstp.dll \"${INSTALL_DIR}\"\r\n    cp ./stp/build/bin/libstp.dll \"${INSTALL_DIR}/bin\"\r\n}\r\n\r\nfunction test_simple()\r\n{\r\n    cd \"${ROOT}\"\r\n\r\n    cd \"${INSTALL_DIR}/bin\"\r\n\r\n    cat << EOF > test.smt2\r\n(set-info :status unknown)\r\n(declare-fun y () (_ BitVec 32))\r\n(declare-fun x () (_ BitVec 32))\r\n(assert (= (bvadd x y) #x0000000a))\r\n(assert (distinct x #x0000000a))\r\n(assert (distinct y #x0000000a))\r\n(check-sat)\r\n(get-model)\r\nEOF\r\n\r\n    ./stp_simple.exe test.smt2 || true\r\n}\r\n\r\nfunction test_python()\r\n{\r\n    cd \"${ROOT}\"\r\n\r\n    cd \"${INSTALL_DIR}/python\"\r\n\r\n    cat << EOF > test.py\r\nfrom stp import stp, Solver\r\n\r\ns = Solver()\r\nx = s.bitvec('x', 32)\r\ny = s.bitvec('y', 32)\r\nv10 = s.bitvecval(32, 10)\r\ns.add(x.add(y).eq(v10))\r\ns.add(x.ne(v10))\r\ns.add(y.ne(v10))\r\nprint s.check()\r\nprint s.model()\r\nEOF\r\n\r\n    python test.py || true\r\n}\r\n\r\nexport INSTALL_DIR=\"myinstall\"\r\nexport ROOT=$(pwd)\r\n\r\ncleanup\r\nsetenv\r\nbuild_zlib\r\nbuild_minisat\r\nbuild_stp\r\ncopy_files\r\ntest_simple\r\ntest_python\r\n\r\n# EOF\r\n```\r\n\r\nSome important notes:\r\n\r\n* These steps \"force\" MinGW to compile statically, such that the resulting DLLs do not depend on the MinGW runtime (i.e., `libstdc++-6.dll` and `libgcc_s_dw2-1.dll`)\r\n* They also do some (semi) magic to force GCC to statically link `winpthread`, for the same kind of reason\r\n\r\nHowever, despite being able to build STP, the resulting binaries do not seem happy at all.\r\n\r\nThe interesting finding is that, actually, STP has been built \"enough\" such that core functionality works (see `test_simple` and `test_python`), however it is during application close (i.e., when the C runtime automatically clears up the heap, calling deconstructors, etc.) that the crash occurs.\r\n\r\nI guess this can't be stressed enough: in the examples above, you _do_ get a correct SMT2 model out of the solver, it is just when the process terminates that everything dies.\r\n\r\nFor running `stp_simple.exe`, here is the backtrace:\r\n\r\n```bash\r\n#0  0x66c36434 in std::_Hashtable<stp::ASTNode, stp::ASTNode, std::allocator<stp::ASTNode>, std::__detail::_Identity, stp::ASTNode::ASTNodeEqual, stp::ASTNode::ASTNodeHasher, std::__detail::_Mod_range_hashing, std::__detail::_Default_ranged_hash, std::__detail::_Prime_rehash_policy, std::__detail::_Hashtable_traits<true, true, true> >::_M_begin (this=0x59f39f45)\r\n    at N:/lib/gcc/i686-w64-mingw32/6.4.0/include/c++/bits/hashtable.h:369\r\n#1  0x66c86e1b in std::_Hashtable<stp::ASTNode, stp::ASTNode, std::allocator<stp::ASTNode>, std::__detail::_Identity, stp::ASTNode::ASTNodeEqual, stp::ASTNode::ASTNodeHasher, std::__detail::_Mod_range_hashing, std::__detail::_Default_ranged_hash, std::__detail::_Prime_rehash_policy, std::__detail::_Hashtable_traits<true, true, true> >::clear (this=0x59f39f45)\r\n    at N:/lib/gcc/i686-w64-mingw32/6.4.0/include/c++/bits/hashtable.h:1901\r\n#2  0x66c87533 in std::_Hashtable<stp::ASTNode, stp::ASTNode, std::allocator<stp::ASTNode>, std::__detail::_Identity, stp::ASTNode::ASTNodeEqual, stp::ASTNode::ASTNodeHasher, std::__detail::_Mod_range_hashing, std::__detail::_Default_ranged_hash, std::__detail::_Prime_rehash_policy, std::__detail::_Hashtable_traits<true, true, true> >::~_Hashtable (this=0x59f39f45, __in_chrg=<optimized out>)\r\n    at N:/lib/gcc/i686-w64-mingw32/6.4.0/include/c++/bits/hashtable.h:1227\r\n#3  0x66cadd5b in std::unordered_set<stp::ASTNode, stp::ASTNode::ASTNodeHasher, stp::ASTNode::ASTNodeEqual, std::allocator<stp::ASTNode> >::~unordered_set (\r\n    this=0x59f39f45, __in_chrg=<optimized out>)\r\n    at N:/lib/gcc/i686-w64-mingw32/6.4.0/include/c++/bits/unordered_set.h:93\r\n#4  0x66bf8d2a in (anonymous namespace)::run(void*) ()\r\n   from C:\\msys32\\home\\avj\\Desktop\\stp\\myinstall\\bin\\libstp.dll\r\n#5  0x66bf8d80 in (anonymous namespace)::run() ()\r\n   from C:\\msys32\\home\\avj\\Desktop\\stp\\myinstall\\bin\\libstp.dll\r\n#6  0x66b011b4 in _CRT_INIT@12 ()\r\n   from C:\\msys32\\home\\avj\\Desktop\\stp\\myinstall\\bin\\libstp.dll\r\n#7  0x66b012dc in __DllMainCRTStartup ()\r\n   from C:\\msys32\\home\\avj\\Desktop\\stp\\myinstall\\bin\\libstp.dll\r\n#8  0x66b01423 in DllMainCRTStartup@12 ()\r\n   from C:\\msys32\\home\\avj\\Desktop\\stp\\myinstall\\bin\\libstp.dll\r\n#9  0x7773a1f6 in ntdll!RtlCheckTokenCapability ()\r\n   from C:\\Windows\\SYSTEM32\\ntdll.dll\r\n#10 0x7770eca6 in ntdll!RtlHashUnicodeString ()\r\n   from C:\\Windows\\SYSTEM32\\ntdll.dll\r\n#11 0x776ffe4d in ntdll!LdrShutdownProcess ()\r\n   from C:\\Windows\\SYSTEM32\\ntdll.dll\r\n#12 0x00000000 in ?? ()\r\n```\r\n\r\nFor running Python and using the STP API, here is the backtrace:\r\n\r\n```bash\r\n#0  0x02cb2db8 in std::vector<stp::MutableASTNode*, std::allocator<stp::MutableASTNode*> >::~vector (this=0x1c2ebb8c, __in_chrg=<optimized out>)\r\n    at N:/lib/gcc/i686-w64-mingw32/6.4.0/include/c++/bits/stl_vector.h:426\r\n#1  0x02bd8d2a in (anonymous namespace)::run(void*) ()\r\n   from C:\\msys32\\home\\avj\\Desktop\\stp\\myinstall\\libstp.dll\r\n#2  0x02bd8d80 in (anonymous namespace)::run() ()\r\n   from C:\\msys32\\home\\avj\\Desktop\\stp\\myinstall\\libstp.dll\r\n#3  0x02ae11b4 in _CRT_INIT@12 ()\r\n   from C:\\msys32\\home\\avj\\Desktop\\stp\\myinstall\\libstp.dll\r\n#4  0x02ae12dc in __DllMainCRTStartup ()\r\n   from C:\\msys32\\home\\avj\\Desktop\\stp\\myinstall\\libstp.dll\r\n#5  0x02ae1423 in DllMainCRTStartup@12 ()\r\n   from C:\\msys32\\home\\avj\\Desktop\\stp\\myinstall\\libstp.dll\r\n#6  0x7773a1f6 in ntdll!RtlCheckTokenCapability ()\r\n   from C:\\Windows\\SYSTEM32\\ntdll.dll\r\n#7  0x7770eca6 in ntdll!RtlHashUnicodeString ()\r\n   from C:\\Windows\\SYSTEM32\\ntdll.dll\r\n#8  0x776ffe4d in ntdll!LdrShutdownProcess ()\r\n   from C:\\Windows\\SYSTEM32\\ntdll.dll\r\n#9  0x00000000 in ?? ()\r\n```\r\n\r\nSome further points:\r\n\r\n* If you don't statically link all of the C runtime files, then you get slightly different backtraces, but the final \"crash\" is the same (i.e., the stack refers to `libstdc++-6.dll` rather than `libstp.dll`), so I don't blame that aspect of the compilation\r\n* I initially wanted to \"blame\" mixing C runtimes between the MinGW compiled applications and how Python 2.7 is compiled (I believe this is with Visual Studio 2008) -- however, the fact you get similar crashes when running standalone `stp_simple.exe` seems to discredit this theory\r\n* All of STP's automated tests also \"fail\", but only because they have SIGSEGV at the end -- looking at the output, seems to suggest they have run correctly up until application close\r\n* I have tried multiple versions of the MinGW toolchain (e.g., 6.4.0 and 8.1.0, but these all have the same resulting crashes)\r\n* Statically linking or not doesn't make any difference in the results (e.g., if you comment out `EXTRA_FLAGS`, which sets the static linking), you get the same crashes\r\n\r\nI am aware that compiling STP on Windows, with MinGW, is probably an extreme edge-case, but I'd love to be able to get STP up and running, as both Z3 and Boolector can be compiled and work very well in this way!\r\n\r\nIf I can provide any further detail, please don't hesitate to let me know, and I am happy to try some other steps. Also, not that I necessarily advocate sharing binaries, but I am happy to provide my pre-compiled versions, if that helps with further diagnosis."},"comment":{"url":"https://api.github.com/repos/stp/stp/issues/comments/441057554","html_url":"https://github.com/stp/stp/issues/296#issuecomment-441057554","issue_url":"https://api.github.com/repos/stp/stp/issues/296","id":441057554,"node_id":"MDEyOklzc3VlQ29tbWVudDQ0MTA1NzU1NA==","user":{"login":"andrewvaughanj","id":14277540,"node_id":"MDQ6VXNlcjE0Mjc3NTQw","avatar_url":"https://avatars1.githubusercontent.com/u/14277540?v=4","gravatar_id":"","url":"https://api.github.com/users/andrewvaughanj","html_url":"https://github.com/andrewvaughanj","followers_url":"https://api.github.com/users/andrewvaughanj/followers","following_url":"https://api.github.com/users/andrewvaughanj/following{/other_user}","gists_url":"https://api.github.com/users/andrewvaughanj/gists{/gist_id}","starred_url":"https://api.github.com/users/andrewvaughanj/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/andrewvaughanj/subscriptions","organizations_url":"https://api.github.com/users/andrewvaughanj/orgs","repos_url":"https://api.github.com/users/andrewvaughanj/repos","events_url":"https://api.github.com/users/andrewvaughanj/events{/privacy}","received_events_url":"https://api.github.com/users/andrewvaughanj/received_events","type":"User","site_admin":false},"created_at":"2018-11-22T15:08:18Z","updated_at":"2018-11-22T15:08:18Z","author_association":"NONE","body":"When compiling with `-DUSE_THREAD_LOCAL=OFF`:\r\n\r\n```\r\n95% tests passed, 2 tests failed out of 38\r\n\r\nTotal Test time (real) =  20.72 sec\r\n\r\nThe following tests FAILED:\r\n          1 - query-files (Failed)\r\n         38 - python-interface-tests (Failed)\r\n```"}}
{"actor":{"display_login":"andrewvaughanj"}}