Enum type with no values causes segmentation fault in typecheck.cpp, introduced in commit 05afaf2e174b29c3993466988f8dc150b09f6638

[agentydragon]

In my project I use Minizinc to solve an optimization/scheduling problem. I run tests to test my integration with Minizinc and that my model produces correct solutions.

The tests break somewhere between 2.4.3 and HEAD. I tried running minizinc simple-planning.mzn input.dzn --solver gecode with the attached files. Here's what minizinc --help says about available solvers:

Available solvers (get help using --help <solver id>):
  Gecode 6.2.0 (org.gecode.gecode, cp, int, float, set, restart)
  Gecode Gist 6.2.0 (org.gecode.gist, cp, int, float, set, restart)

OK on Minizinc 2.4.3

On Minizinc 2.4.3, I get an OK output on my test:

stock = array2d(0..2, Ingredients, [2, 2, 1, 2, 1, 1]);
recipe_cooked = array1d(0..1, [R2_Raw_apple, R0_Raw_egg]);
recipe_cooked_idx = array1d(0..1, [3, 1]);
products_bought = array2d(0..1, Products, []);
products_bought_overall = array1d(Products, []);
used_directly = array2d(0..1, Ingredients, [1, 0, 0, 1]);
as_used_by_recipe = array2d(0..1, Ingredients, [1, 0, 0, 1]);
as_thrown_in = array2d(0..1, Ingredients, [1, 0, 0, 1]);
using_diet_bit = array2d(0..1, DietBits, [false, false, false, false, false, false, false, false, false, false]);
obtain_externally = array1d(Ingredients, [0, 0]);
total_ingredient_use = array1d(Ingredients, [1, 1]);
recipe_ever_cooked = array1d(Recipes, [true, false, true]);
generalization_to_from = array3d(0..1, Ingredients, Ingredients, [0, 0, 0, 0, 0, 0, 0, 0]);
total_products_bought = 0;
----------
==========

Failure in HEAD

I just uninstalled the Minizinc package on my system (Pop!_OS 20.10 if relevant), installed libgecode-dev, updated my clone of libminizinc to commit e385f96, and used cmake . && make, then sudo make install.

$ minizinc --version
MiniZinc to FlatZinc converter, version 2.5.3

I passed this json-config.msc:

{
"id": "org.gecode.gecode",
"name": "Gecode",
"description": "Gecode FlatZinc executable",
"version": "6.2.0",
"mznlib": "/usr/share/minizinc/gecode",
"executable": "/usr/bin/fzn-gecode",
"tags": ["cp", "int", "float", "set", "restart"],
"stdFlags": ["-a", "-f", "-n", "-p", "-r", "-s", "-t"],
"supportsMzn": false,
"supportsFzn": true,
"needsSolns2Out": true,
"needsMznExecutable": false,
"needsStdlibDir": false,
"isGUIApplication": false
}

And I run: minizinc simple-planning.mzn input.dzn --solver json-config.msc --stdlib-dir /usr/local/share/minizinc and get a segmentation fault:

[1]    2698470 segmentation fault (core dumped)  minizinc simple-planning.mzn input.dzn --solver json-config.msc --stdlib-dir 

I didn't yet build minizinc with debug symbol, but I get this backtrace from gdb:

#0  0x000055555579d81f in MiniZinc::create_enum_mapper(MiniZinc::EnvI&, MiniZinc::Model*, unsigned int, MiniZinc::VarDecl*, MiniZinc::Model*) ()
#1  0x00005555557b229e in MiniZinc::typecheck(MiniZinc::Env&, MiniZinc::Model*, std::vector<MiniZinc::TypeError, std::allocator<MiniZinc::TypeError> >&, bool, bool, bool) ()
#2  0x000055555576b936 in MiniZinc::CompilePass::run(MiniZinc::Env*, std::ostream&) ()
#3  0x0000555555707493 in MiniZinc::Flattener::multiPassFlatten(std::vector<std::unique_ptr<MiniZinc::Pass, std::default_delete<MiniZinc::Pass> >, std::allocator<std::unique_ptr<MiniZinc::Pass, std::default_delete<MiniZinc::Pass> > > > const&) ()
#4  0x000055555570cfc5 in MiniZinc::Flattener::flatten(std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&) ()
#5  0x00005555555caebd in MiniZinc::MznSolver::run(std::vector<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >, std::allocator<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > > > const&, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&) ()
#6  0x00005555555bc79d in main ()

I faintly remember that there were some changes in Minizinc related to enums between 2.4.3 and now, so maybe they might have some bug in them.

[agentydragon]

input.dzn: https://pastebin.ubuntu.com/p/XXgghC6Pfg/
simple-planning.mzn: https://pastebin.ubuntu.com/p/DYfXnGKzdY/

[agentydragon]

Made a debug build and got a nicer backtrace:

(gdb) r simple-planning.mzn input.dzn --solver json-config.msc --stdlib-dir /usr/local/share/minizinc
Starting program: /usr/local/bin/minizinc simple-planning.mzn input.dzn --solver json-config.msc --stdlib-dir /usr/local/share/minizinc
[Thread debugging using libthread_db enabled]
Using host libthread_db library "/lib/x86_64-linux-gnu/libthread_db.so.1".

Program received signal SIGSEGV, Segmentation fault.
MiniZinc::create_enum_mapper (env=..., m=0x555555bd5930, enumId=3, vd=0x555555bcc2e8, 
    enumItems=0x555555c12b80) at /home/agentydragon/repos/libminizinc/lib/typecheck.cpp:764
764	  auto* rhs = new BinOp(vd->loc(), IntLit::a(1), BOT_DOTDOT, partCardinality.back());
(gdb) bt
#0  MiniZinc::create_enum_mapper (env=..., m=0x555555bd5930, enumId=3, vd=0x555555bcc2e8, 
    enumItems=0x555555c12b80) at /home/agentydragon/repos/libminizinc/lib/typecheck.cpp:764
#1  0x000055555581d203 in MiniZinc::typecheck (env=..., origModel=0x555555b05ae0, 
    typeErrors=std::vector of length 0, capacity 0, ignoreUndefinedParameters=false, 
    allowMultiAssignment=false, isFlatZinc=false)
    at /home/agentydragon/repos/libminizinc/lib/typecheck.cpp:2748
#2  0x00005555557cd657 in MiniZinc::CompilePass::run (this=0x555555bd58b0, store=0x555555b06550, 
    log=...) at /home/agentydragon/repos/libminizinc/lib/passes/compile_pass.cpp:121
#3  0x0000555555747e12 in MiniZinc::Flattener::multiPassFlatten (this=0x7fffffffd330, 
    passes=std::vector of length 1, capacity 1 = {...})
    at /home/agentydragon/repos/libminizinc/lib/flattener.cpp:427
#4  0x000055555574b36d in MiniZinc::Flattener::flatten (this=0x7fffffffd330, modelString="", 
    modelName="stdin") at /home/agentydragon/repos/libminizinc/lib/flattener.cpp:782
#5  0x0000555555577f90 in MiniZinc::MznSolver::flatten (this=0x7fffffffd210, modelString="", 
    modelName="stdin") at /home/agentydragon/repos/libminizinc/lib/solver.cpp:844
#6  0x00005555555786c8 in MiniZinc::MznSolver::run (this=0x7fffffffd210, 
    args0=std::vector of length 6, capacity 6 = {...}, model="", exeName="/usr/local/bin/minizinc", 
    modelName="stdin") at /home/agentydragon/repos/libminizinc/lib/solver.cpp:912
#7  0x000055555556e31c in main (argc=7, argv=0x7fffffffda08)
    at /home/agentydragon/repos/libminizinc/minizinc.cpp:57
(gdb) 

[agentydragon]

The crash happens here:

// Create set literal for overall enum
auto* rhs = new BinOp(vd->loc(), IntLit::a(1), BOT_DOTDOT, partCardinality.back()); // <-- here
vd->e(rhs);

I set up an assert(partCardinality.size() > 0); on the previous line, and with that compiled in, the assertion failed. Looks like the previous for-loop is supposed to populate partCardinality, but the case when it doesn't get populated is not handled.

[agentydragon]

Used git checkout lib/typecheck.cpp 3a7874d1c3570603c5ea82989bb8918c51019c41 to roll back to earlier version of typecheck.cpp. The bug is already present in that commit. On the previous commit changing typecheck.cpp, 4e019c9, changing typecheck.cpp only does not build.

[agentydragon]

git bisect with gdb --args minizinc simple-planning.mzn input.dzn --solver json-config.msc --stdlib-dir /usr/local/share/minizinc:

git bisect good 2.4.3
git bisect bad e385f96afad3c1c3a361a0378e7e24898dcef14d
git bisect bad 23da0ef8193b7d7ebb82d3a0c54798f0bdba82e3
git bisect good f8fd967208e5c01a1ca0f0269dc05f2ec1f199b3
git bisect bad 90707faaba41589220a4a53448d9046db68d67ad
git bisect good 74d09c8437793aa31755bdb5633b349153e5d6db
git bisect bad 07a3ac4dab88cfeba49ba7843481b4303f0bffb3
git bisect bad ab01dfb4fa836e1ff5f270da54ee1526f38e7e54
git bisect bad 987d91d3c7e66f432494b1e77790503ed9d91bab
git bisect bad f5f1e119e7f5db7ba7de6b36e15dcaca7a944b64
git bisect bad b2bcdcb7096320e9cb2a6279f62bd174b08de8f2
git bisect bad 05afaf2e174b29c3993466988f8dc150b09f6638

Identified 05afaf2 as the first bad commit.

[agentydragon]

@guidotack Hi, looks like your commit 05afaf2 fails to work on my testcase (described above). Could you take a look?

[agentydragon]

I minimized my failing input to just:

enum EmptyEnum;
EmptyEnum = {  };
solve satisfy;

[agentydragon]

My attempt at fixing is in PR #444.