mzn2fzn SEGFAULT: Infinite recursion in parsing of recursive function.

[stian-svedenborg]

Parsing the following example using mzn2fzn will trigger a segfault caused by a stack overflow.

function var int:
ilog2( var int: x ) =
  let { constraint x > 0 } in
  if  x > 1 then
     1 + ilog2(x div 2)
  else
     0
  endif
;

var 1..256: x;
var int: y;

constraint( y == ilog2(x) );

solve ::int_search( [x, y], first_fail, indomain_random, complete ) satisfy;

Stack trace (with increased stack size):

> # 0  0x000000000062eff1 in MiniZinc::bind(MiniZinc::EnvI&, MiniZinc::Ctx, MiniZinc::VarDecl_, MiniZinc::Expression_) ()
> # 1  0x0000000000639867 in MiniZinc::flat_exp(MiniZinc::EnvI&, MiniZinc::Ctx, MiniZinc::Expression_, MiniZinc::VarDecl_, MiniZinc::VarDecl*) ()
> # 2  0x000000000064f21a in MiniZinc::flat_exp(MiniZinc::EnvI&, MiniZinc::Ctx, MiniZinc::Expression_, MiniZinc::VarDecl_, MiniZinc::VarDecl*) ()
> # 3  0x000000000065869e in MiniZinc::EnvI::flat_addItem(MiniZinc::Item*) ()
> # 4  0x000000000063028f in MiniZinc::bind(MiniZinc::EnvI&, MiniZinc::Ctx, MiniZinc::VarDecl_, MiniZinc::Expression_) ()
> # 5  0x0000000000654f2e in MiniZinc::flat_exp(MiniZinc::EnvI&, MiniZinc::Ctx, MiniZinc::Expression_, MiniZinc::VarDecl_, MiniZinc::VarDecl*) ()
> # 6  0x000000000065763b in MiniZinc::flat_exp(MiniZinc::EnvI&, MiniZinc::Ctx, MiniZinc::Expression_, MiniZinc::VarDecl_, MiniZinc::VarDecl*) ()
> # 7  0x0000000000655779 in MiniZinc::flat_exp(MiniZinc::EnvI&, MiniZinc::Ctx, MiniZinc::Expression_, MiniZinc::VarDecl_, MiniZinc::VarDecl*) ()
> # 8  0x0000000000662dcd in MiniZinc::flat_ite(MiniZinc::EnvI&, MiniZinc::Ctx, MiniZinc::ITE_, MiniZinc::VarDecl_, MiniZinc::VarDecl*) ()
> # 9  0x0000000000643378 in MiniZinc::flat_exp(MiniZinc::EnvI&, MiniZinc::Ctx, MiniZinc::Expression_, MiniZinc::VarDecl_, MiniZinc::VarDecl*) ()
> # 10 0x00000000006558da in MiniZinc::flat_exp(MiniZinc::EnvI&, MiniZinc::Ctx, MiniZinc::Expression_, MiniZinc::VarDecl_, MiniZinc::VarDecl*) ()
> # 11 0x0000000000646776 in MiniZinc::flat_exp(MiniZinc::EnvI&, MiniZinc::Ctx, MiniZinc::Expression_, MiniZinc::VarDecl_, MiniZinc::VarDecl*) ()
> # 12 0x000000000064f21a in MiniZinc::flat_exp(MiniZinc::EnvI&, MiniZinc::Ctx, MiniZinc::Expression_, MiniZinc::VarDecl_, MiniZinc::VarDecl*) ()
> # 13 0x000000000063b659 in MiniZinc::flat_exp(MiniZinc::EnvI&, MiniZinc::Ctx, MiniZinc::Expression_, MiniZinc::VarDecl_, MiniZinc::VarDecl*) ()
> # 14 0x000000000064f21a in MiniZinc::flat_exp(MiniZinc::EnvI&, MiniZinc::Ctx, MiniZinc::Expression_, MiniZinc::VarDecl_, MiniZinc::VarDecl*) ()
> # 15 0x0000000000644d74 in MiniZinc::flat_exp(MiniZinc::EnvI&, MiniZinc::Ctx, MiniZinc::Expression_, MiniZinc::VarDecl_, MiniZinc::VarDecl*) ()
> # 16 0x00000000006637b5 in MiniZinc::flat_ite(MiniZinc::EnvI&, MiniZinc::Ctx, MiniZinc::ITE_, MiniZinc::VarDecl_, MiniZinc::VarDecl*) ()
> 
> (...)
>  #2844 0x00000000006637b5 in MiniZinc::flat_ite(MiniZinc::EnvI&, MiniZinc::Ctx, MiniZinc::ITE_, MiniZinc::VarDecl_, MiniZinc::VarDecl*) ()
> # 2845 0x0000000000643378 in MiniZinc::flat_exp(MiniZinc::EnvI&, MiniZinc::Ctx, MiniZinc::Expression_, MiniZinc::VarDecl_, MiniZinc::VarDecl*) ()
> # 2846 0x0000000000657a20 in MiniZinc::flat_exp(MiniZinc::EnvI&, MiniZinc::Ctx, MiniZinc::Expression_, MiniZinc::VarDecl_, MiniZinc::VarDecl*) ()
> # 2847 0x00000000006558da in MiniZinc::flat_exp(MiniZinc::EnvI&, MiniZinc::Ctx, MiniZinc::Expression_, MiniZinc::VarDecl_, MiniZinc::VarDecl*) ()
> # 2848 0x000000000063b659 in MiniZinc::flat_exp(MiniZinc::EnvI&, MiniZinc::Ctx, MiniZinc::Expression_, MiniZinc::VarDecl_, MiniZinc::VarDecl*) ()
> # 2849 0x000000000064f21a in MiniZinc::flat_exp(MiniZinc::EnvI&, MiniZinc::Ctx, MiniZinc::Expression_, MiniZinc::VarDecl_, MiniZinc::VarDecl*) ()
> # 2850 0x0000000000644d74 in MiniZinc::flat_exp(MiniZinc::EnvI&, MiniZinc::Ctx, MiniZinc::Expression_, MiniZinc::VarDecl_, MiniZinc::VarDecl*) ()
> # 2851 0x00000000006637b5 in MiniZinc::flat_ite(MiniZinc::EnvI&, MiniZinc::Ctx, MiniZinc::ITE_, MiniZinc::VarDecl_, MiniZinc::VarDecl*) ()
> # 2852 0x0000000000643378 in MiniZinc::flat_exp(MiniZinc::EnvI&, MiniZinc::Ctx, MiniZinc::Expression_, MiniZinc::VarDecl_, MiniZinc::VarDecl*) ()
> # 2853 0x0000000000657a20 in MiniZinc::flat_exp(MiniZinc::EnvI&, MiniZinc::Ctx, MiniZinc::Expression_, MiniZinc::VarDecl_, MiniZinc::VarDecl*) ()
> # 2854 0x00000000006558da in MiniZinc::flat_exp(MiniZinc::EnvI&, MiniZinc::Ctx, MiniZinc::Expression_, MiniZinc::VarDecl_, MiniZinc::VarDecl*) ()
> # 2855 0x00000000006499cc in MiniZinc::flat_exp(MiniZinc::EnvI&, MiniZinc::Ctx, MiniZinc::Expression_, MiniZinc::VarDecl_, MiniZinc::VarDecl*) ()
> # 2856 0x000000000067ffb3 in MiniZinc::flatten(MiniZinc::Env&, MiniZinc::FlatteningOptions)::FV::vConstraintI(MiniZinc::ConstraintI*) ()
> # 2857 0x000000000067f196 in MiniZinc::ItemIter<MiniZinc::flatten(MiniZinc::Env&, MiniZinc::FlatteningOptions)::FV>::run(MiniZinc::Model*) ()
> # 2858 0x00000000006762ad in void MiniZinc::iterItems<MiniZinc::flatten(MiniZinc::Env&, MiniZinc::FlatteningOptions)::FV>(MiniZinc::flatten(MiniZinc::Env&, MiniZinc::FlatteningOptions)::FV&, MiniZinc::Model*) ()
> # 2859 0x000000000066ef07 in MiniZinc::flatten(MiniZinc::Env&, MiniZinc::FlatteningOptions) ()
> # 2860 0x000000000053443c in main ()

[guidotack]

Unfortunately this is the “expected” behaviour here. You can’t do recursion through a variable argument in MiniZinc, since the if condition cannot be evaluated at compile time. MiniZinc should fail with a better error message though, I’ll see if we can implement some check there.

[stian-svedenborg]

That's a bummer. Ok, I have a workaround that will work. Thanks for the quick response as always Guido.

[guidotack]

You can often simulate a var function by turning a par function into an array lookup like this:

function int: ilog2(int: x) =
  if x > 1 then 1 + ilog2(x div 2)
  else 0 endif;

var 1..256: x;
var int: y;

constraint y = [ilog2(i) | i in dom(x)][x];

solve ::int_search( [x, y], first_fail, indomain_random, complete ) satisfy;

output ["x = \(x), y=\(y)\n"];

[stian-svedenborg]

Thanks, I ended up writing a very very long conditional instead as I need it to work on a large domain. If performance becomes an issue I'll revise the domain and change it to the lookup table you describe.