Segfault in dd_blockelimination

[castrong]

I've been running into a Segfault in CDDLib while using Lazy sets (mentioned in a LazySets.jl issue JuliaReach/LazySets.jl#2278 and NeuralVerification.jl issue sisl/NeuralVerification.jl#131). I've reproduced the issue below, which arises when trying to perform an affine map on a polytope.

Code to reproduce the error:

using LazySets
using Polyhedra
using CDDLib
using LinearAlgebra

# Setup an affine map of a polytope. Create a weight, bias, and polytope to map.
weight = [0.9115126809261311 0.4138440851467826 -0.33913105667038046 0.16700640073917672 -0.235120928568453; 0.6708292278443739 0.7576636017826068 0.8258791757476476 -0.17354379680520315 0.05393765869881095]
bias = [0.9457155975714278, 0.8338760871488544]


x_b = [0.0, 0.0, 48.84693391113945, -0.0, -0.0, -48.84693391113945, 1.8836929121889678, -185.48981164918555, -10.462945198060497, -1720.1125639313502, 30.8157991272438, 2.0328182777903794, -187.72706748216493, 31.333402600081193, 0.8311564016891444, -22.109210103545358, -1.5090925356292428, 24.84987253171124, 22.723250162485456, 46.839496529983926, -3.0989868675615497, 22.996310337995876, 7.619279109784628, -95.3486713467225, -7.854896717148563, 11.076982623957505, 13.357831143154556, 7.571546154878658, -103.47921230520559, 14.32831285002315, 8.135529620293468, 48.79574944863249, 19.26331941987261, 136.7074646969065, 737.0385026793365, 386.7092569137319, 35.510763078591076, 19.326340234088597, 19.984549508693096, 81.48499516064464, -13.09506164510387, -22.242599379716452, -16.602786452793474, -54.966447910936374, -66.1493435694213, -8.126647179260214, -72.17519884364094, -125.60015735472614, 0.0, 0.0, 0.0]
x_A = [-1.0 -0.0 -0.0 -0.0 -0.0; 0.0 0.0 -1.0 0.0 0.0; 0.0 8.076118521420486 0.0 35.19332258166109 13.837840646860146; 1.0 0.0 0.0 0.0 0.0; -0.0 -0.0 1.0 -0.0 -0.0; -0.0 -8.076118521420486 -0.0 -35.19332258166109 -13.837840646860146; -0.0 -3.183853894999074 -0.0 1.2556482650995342 -1.335269967575815; -0.0 -123.48562349701186 -0.0 12.461527940546762 -191.56298093458574; -0.0 -5.8754081576777555 -0.0 -1.0 -9.192156091705593; -0.0 -3954.019716077408 -0.0 516.3823227731308 1.0; -0.0 -2.020421677653688 -0.0 33.13501964692841 -1.5290182089446205; -0.0 -2.9367563418673024 -0.0 1.234074373666857 -1.3523486586045974; -0.0 -124.77068430216175 -0.0 12.582671668841833 -194.00279187884; -0.0 -1.7585066999570298 -0.0 33.51946010990651 -1.5485644695561085; -0.0 -7.218099737090482 -0.0 1.2632052067877908 1.0; -0.0 -15.488240849079062 -0.0 1.5412692709140638 -22.419938049751448; -0.0 -13.01835813695014 -0.0 1.0 4.926303512727481; -0.0 -7.412162155296751 -0.0 27.784232793846485 1.0; -0.0 13.01835813695014 -0.0 -1.0 -4.926303512727481; -0.0 15.488240849079062 -0.0 -1.5412692709140638 22.419938049751448; -0.0 7.412162155296751 -0.0 -27.784232793846485 -1.0; -0.0 13.401396607174302 -0.0 -1.0 -5.278131656113089; -0.0 7.243060544078956 -0.0 1.0 -6.770502738425847; -0.0 19.403024419575345 -0.0 1.0 -188.7132194712973; -0.0 -1.0 -0.0 -5.021202289034041 -3.6682709246498715; -0.0 34.39532800581566 -0.0 1.0 -38.624071876237714; -0.0 3.56454827656787 -0.0 12.19995345388215 -2.282505496082628; -0.0 6.8682285340371765 -0.0 1.0 -6.330770131793407; -0.0 18.257665816436887 -0.0 1.0 -200.17949584749525; -0.0 3.681583201082492 -0.0 13.127471771939016 -2.2825054960826288; -0.0 1.0 -0.0 5.021202289034041 3.6682709246498715; -0.0 8.076118521420485 -0.0 34.85346029447396 14.267156457625715; -0.0 5.8754081576777555 -0.0 1.0 9.192156091705593; -0.0 -18.257665816436887 -0.0 -1.0 200.17949584749525; -0.0 136.66235756616274 -0.0 1.0 985.1793220116999; -0.0 124.77068430216175 -0.0 -12.582671668841833 194.00279187884; -0.0 4.356246013730709 -0.0 1.0 36.423283339663975; -0.0 5.662649285509967 -0.0 1.0 14.188241938928781; -0.0 5.78278828756762 -0.0 1.0 15.078731703355606; -0.0 26.217307003486123 -0.0 -2.4420919880667333 41.45623389823421; -0.0 -3.681583201082492 -0.0 -13.127471771939016 2.2825054960826288; -0.0 -3.538269036057601 -0.0 -21.009712955831077 1.0; -0.0 1.7585066999570298 -0.0 -33.51946010990651 1.5485644695561085; -0.0 -6.767275556297155 -0.0 -60.347490188260586 1.0; -0.0 -5.913573386014781 -0.0 -73.97201065550148 -1.0; -0.0 -1.0 -0.0 -7.655047108966467 -1.0887090115595073; -0.0 -6.557924359755801 -0.0 -80.44710443760286 -1.0; -0.0 -6.004865949367552 -0.0 -164.54018450234872 1.0; -0.0 -1.0 -0.0 -0.0 -0.0; -0.0 -0.0 -0.0 -1.0 -0.0; -0.0 -0.0 -0.0 -0.0 -1.0]
P = LazySets.HPolytope(x_A, x_b)

# Setup the call to eliminate (matching the setup in LazySets._linear_map_hrep)
m, n = size(weight)
N = Float64
₋Id_m = Matrix(-one(N)*I, m, m)
Ax_leq_b = [Polyhedra.HalfSpace(vcat(zeros(N, m), Vector(c.a)), c.b) for c in constraints_list(P)]
y_eq_Mx = [Polyhedra.HyperPlane(vcat(₋Id_m[i, :], Vector(weight[i, :])), zero(N)) for i in 1:m]

# Create the Phrep and then call CDDLib.eliminate
Phrep = Polyhedra.hrep(y_eq_Mx, Ax_leq_b)
Phrep = polyhedron(Phrep, CDDLib.Library(:float)) # define concrete subtype
Peli_block = CDDLib.eliminate(Phrep, (m+1):(m+n), BlockElimination())

Leads to the following stacktrace:

signal (11): Segmentation fault: 11
in expression starting at /Users/castrong/Desktop/Research/NV_Fork/NeuralVerification.jl/examples/SimpleProblem.jl:24
ddf_BlockElimination at /Users/castrong/.julia/dev/CDDLib/deps/usr/lib/libcddgmp.0.dylib (unknown line)
dd_blockelimination at /Users/castrong/.julia/dev/CDDLib/src/CDDLib.jl:22 [inlined]
blockelimination at /Users/castrong/.julia/dev/CDDLib/src/operations.jl:272
unknown function (ip: 0x12588db99)
eliminate at /Users/castrong/.julia/dev/CDDLib/src/polyhedron.jl:187
unknown function (ip: 0x12588d7a9)
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]

[mengyuest]

Hi, any update on this thread? I encountered similar SegFault problem for reachability analysis when doing BlockElimination. Thanks.

[blegat]

This is a bug in cddlib, see #65 (comment)

[odow]

Close in favor of #65

[odow]

Closing in favor of #65