search

ahumenberger / Z3.jl

Julia interface to Z3
MIT License
57 stars 7 forks source link

segfault #12

Closed goretkin closed 9 months ago

goretkin commented 3 years ago

This snippet of code reliably segfaults:

using Z3

function fun()
    println("1")
    ctx = Context()
    println("2")
    solver = Solver(ctx, "QF_NRA")
    println("3")
    c = real_const(ctx, "c")
    s = real_const(ctx, "s")
    println("4")

    R = [
        c s;
    ]
    # @show typeof(R) prevents segfault
    println("5")
    add(solver, c == 1)
    println("6")
end

sols = fun()

Sometimes with

1
2
3
4
5
Segmentation fault: 11

or

ASSERTION VIOLATION
File: /workspace/srcdir/z3/src/ast/ast.cpp
Line: 431
UNREACHABLE CODE WAS REACHED.
4.8.8.0

or

signal (11): Segmentation fault: 11
in expression starting at /Users/goretkin/projects/MakeJuliaZ3Segfault/z3-segfault.jl:22
_Z8get_sortPK4expr at /Users/goretkin/.julia/artifacts/71bdd8cf754f971d6fc3f9b42d2856330bb2e5b4/lib/libz3.4.8.8.0.dylib (unknown line)
Z3_get_sort at /Users/goretkin/.julia/artifacts/71bdd8cf754f971d6fc3f9b42d2856330bb2e5b4/lib/libz3.4.8.8.0.dylib (unknown line)
_ZNK2z34expr8get_sortEv at /Users/goretkin/.julia/artifacts/71bdd8cf754f971d6fc3f9b42d2856330bb2e5b4/lib/libz3jl.dylib (unknown line)
_ZNSt3__110__function6__funcIZN5jlcxx11TypeWrapperIN2z34exprEE6methodINS4_4sortES5_JEEERS6_RKNS_12basic_stringIcNS_11char_traitsIcEENS_9allocatorIcEEEEMT0_KFT_DpT1_EEUlRKS5_E_NSD_ISQ_EEFS8_SP_EEclESP_ at /Users/goretkin/.julia/artifacts/71bdd8cf754f971d6fc3f9b42d2856330bb2e5b4/lib/libz3jl.dylib (unknown line)
_ZN5jlcxx6detail17ReturnTypeAdapterIN2z34sortEJRKNS2_4exprEEEclEPKvNS_13WrappedCppPtrE at /Users/goretkin/.julia/artifacts/71bdd8cf754f971d6fc3f9b42d2856330bb2e5b4/lib/libz3jl.dylib (unknown line)
_ZN5jlcxx6detail11CallFunctorIN2z34sortEJRKNS2_4exprEEE5applyEPKvNS_13WrappedCppPtrE at /Users/goretkin/.julia/artifacts/71bdd8cf754f971d6fc3f9b42d2856330bb2e5b4/lib/libz3jl.dylib (unknown line)
get_sort at /Users/goretkin/.julia/packages/CxxWrap/94t40/src/CxxWrap.jl:590
promote at /Users/goretkin/.julia/packages/Z3/MnUlr/src/Z3.jl:71 [inlined]
== at /Users/goretkin/.julia/packages/Z3/MnUlr/src/Z3.jl:78
fun at /Users/goretkin/projects/MakeJuliaZ3Segfault/z3-segfault.jl:18

I reproduced the segfault in the CI of this repo:

https://github.com/goretkin/MakeJuliaZ3Segfault/runs/1410898097#step:4:51

Errors seem to point to: https://github.com/Z3Prover/z3/blob/e16acd0965bcb679e54c451eba61a4a8ed474a03/src/ast/ast.cpp#L423-L435

ahumenberger commented 3 years ago

It seems as some objects are garbage collected before they are used within the call to add(solver, c == 1). For me it works if I expand the lifetime of the object ctx with GC.@preserve. That is, using GC.@preserve ctx add(solver, c == 1) instead of add(solver, c == 1) works in my case. I'm however not yet sure if this is really the solution, I need to investigate a bit further. Let me know if that works for you.

goretkin commented 3 years ago

Yup, that fixes it for me! Thanks for taking a look at it!

I tried to learn a bit more about CxxWrap.jlto see if this is expected behavior, or to see if there's a fix regarding whether being used, but I didn't learn enough. I hope it's okay to ping @barche to offer some advice.

goretkin commented 3 years ago

It seems this segfault is caused by https://github.com/JuliaInterop/CxxWrap.jl/issues/256

shashi commented 1 year ago

Just an update -- this actually works now! :-)