search

sisl / NeuralVerification.jl

Methods to soundly verify deep neural networks
MIT License
223 stars 50 forks source link

Segfault in ExactReach #131

Open castrong opened 4 years ago

castrong commented 4 years ago

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)

castrong commented 4 years ago

This seems to be an issue with LazySets. I've posted an issue to replicate it with LazySets (without going through NeuralVerification) here: https://github.com/JuliaReach/LazySets.jl/issues/2278