Segfault in ExactReach
castrong opened this issue · 1 comments
The following code:
using LazySets
# Setup problem
network = NeuralVerification.read_nnet("./examples/networks/issue_net.nnet")
input_set = LazySets.HPolytope([LazySets.HalfSpace([1.0, 0.0], 0.3255948352202567), LazySets.HalfSpace([0.0, 1.0], 0.0063660927344990625), LazySets.HalfSpace([-1.0, 0.0], 1.2657708462240773), LazySets.HalfSpace([0.0, -1.0], 0.2352976132029676)])
output_set = LazySets.HPolytope([LazySets.HalfSpace([1.0, 0.0], 1.152247437385072), LazySets.HalfSpace([0.0, 1.0], 0.824396693498243), LazySets.HalfSpace([-1.0, 0.0], 0.27530728609343824), LazySets.HalfSpace([0.0, -1.0], -0.05687606354374264)])
problem = NeuralVerification.Problem(network, input_set, output_set)
# Solve on ExactReach
println(NeuralVerification.solve(NeuralVerification.ExactReach(), problem))
With network:
//Neural Network File Format by Kyle Julian, Stanford 2016.
2, 2, 2, 5,
2, 5, 2,
This line extraneous
-6.55e4,-6.55e4,
6.55e4,6.55e4,
0.0,0.0,0.0,
1.0,1.0,1.0,
-0.7365114899510892, -0.41154368275566355,
-0.8591329390595495, 0.9370977185855476,
-0.11047670316300051, -0.2654135126870667,
0.227516004509706, 0.021382971813836527,
-0.07722192536896744, -0.6012968553830342,
-0.5395494005121688,
0.9689132574915664,
0.0008503521368683487,
0.9240786368047944,
0.6142922344389037,
0.9115126809261311, 0.4138440851467826, -0.33913105667038046, 0.16700640073917672, -0.235120928568453,
0.6708292278443739, 0.7576636017826068, 0.8258791757476476, -0.17354379680520315, 0.05393765869881095,
0.9457155975714278,
0.8338760871488544,
Leads to the following Segfault and stack trace:
signal (11): Segmentation fault: 11
in expression starting at /Users/castrong/Desktop/Research/NV_Fork/NeuralVerification.jl/examples/SimpleProblem.jl:13
ddf_BlockElimination at /Users/castrong/.julia/packages/CDDLib/Y6ywi/deps/usr/lib/libcddgmp.0.dylib (unknown line)
dd_blockelimination at /Users/castrong/.julia/packages/CDDLib/Y6ywi/src/CDDLib.jl:22 [inlined]
blockelimination at /Users/castrong/.julia/packages/CDDLib/Y6ywi/src/operations.jl:259
unknown function (ip: 0x1331a9179)
eliminate at /Users/castrong/.julia/packages/CDDLib/Y6ywi/src/polyhedron.jl:181
unknown function (ip: 0x1331a88d9)
_linear_map_hrep at /Users/castrong/.julia/packages/LazySets/FwmiZ/src/Interfaces/AbstractPolyhedron_functions.jl:768
_linear_map_hrep_helper at /Users/castrong/.julia/packages/LazySets/FwmiZ/src/Sets/HPolytope.jl:132
#linear_map#35 at /Users/castrong/.julia/packages/LazySets/FwmiZ/src/Interfaces/AbstractPolyhedron_functions.jl:622
linear_map at /Users/castrong/.julia/packages/LazySets/FwmiZ/src/Interfaces/AbstractPolyhedron_functions.jl:593 [inlined]
affine_map at /Users/castrong/.julia/packages/LazySets/FwmiZ/src/Interfaces/LazySet.jl:396
affine_map at /Users/castrong/Desktop/Research/NV_Fork/NeuralVerification.jl/src/utils/util.jl:367
forward_layer at /Users/castrong/Desktop/Research/NV_Fork/NeuralVerification.jl/src/reachability/exactReach.jl:37
forward_network at /Users/castrong/Desktop/Research/NV_Fork/NeuralVerification.jl/src/reachability/utils/reachability.jl:9
solve at /Users/castrong/Desktop/Research/NV_Fork/NeuralVerification.jl/src/reachability/exactReach.jl:28
do_call at /Users/sabae/buildbot/worker/package_macos64/build/src/interpreter.c:323
eval_stmt_value at /Users/sabae/buildbot/worker/package_macos64/build/src/interpreter.c:362 [inlined]
eval_body at /Users/sabae/buildbot/worker/package_macos64/build/src/interpreter.c:758
jl_interpret_toplevel_thunk_callback at /Users/sabae/buildbot/worker/package_macos64/build/src/interpreter.c:884
unknown function (ip: 0xfffffffffffffffe)
This seems to be an issue with LazySets. I've posted an issue to replicate it with LazySets (without going through NeuralVerification) here: JuliaReach/LazySets.jl#2278