Another seemingly infinite loop

[mtzguido]

This is similar to #7948, but I'm not sure if it is in fact tightly looping (with -v:9 the logs show spurious messages once in a while, at least for the first few minutes).

This file:

queries-Hacl.Spec.Bignum.ModInvLimb-14.smt2.txt

works for random seeds 1 through 9 (with some variance in time, it can take 0.16s up to 2.2s), but seems to take forever with seed=0. It ran for at least 45 minutes on my machine.

The stack trace after running for about 30 seconds is something like this:

^C
Program received signal SIGINT, Interrupt.
0x0000555556e4bfdd in mpn_manager::mul(unsigned int const*, unsigned int, unsigned int const*, unsigned int, unsigned int*) const ()
(gdb) where
#0  0x0000555556e4bfdd in mpn_manager::mul(unsigned int const*, unsigned int, unsigned int const*, unsigned int, unsigned int*) const ()
#1  0x0000555556df385d in mpz_manager<false>::big_mul(mpz const&, mpz const&, mpz&) ()
#2  0x0000555556df65d1 in mpz_manager<false>::addmul(mpz const&, mpz const&, mpz const&, mpz&) ()
#3  0x0000555556d8a8ff in void polynomial::manager::imp::som_buffer::addmul_core<polynomial::polynomial, false>(mpz const&, polynomial::monomial const*, polynomial::polynomial const*) ()
#4  0x0000555556d93261 in polynomial::manager::imp::exact_div(polynomial::polynomial const*, polynomial::polynomial const*) ()
#5  0x0000555556da5845 in polynomial::manager::imp::resultant(polynomial::polynomial const*, polynomial::polynomial const*, unsigned int, obj_ref<polynomial::polynomial, polynomial::manager>&) ()
#6  0x0000555556d839ca in polynomial::manager::discriminant(polynomial::polynomial const*, unsigned int, obj_ref<polynomial::polynomial, polynomial::manager>&) ()
#7  0x000055555671e9f2 in nlsat::explain::imp::add_lcs(ref_vector<polynomial::polynomial, polynomial::manager>&, unsigned int) ()
#8  0x0000555556723f0d in nlsat::explain::imp::project(ref_vector<polynomial::polynomial, polynomial::manager>&, unsigned int) ()
#9  0x000055555671a62e in nlsat::explain::main_operator(unsigned int, sat::literal const*, nlsat::scoped_literal_vector&) ()
#10 0x0000555556731890 in nlsat::solver::imp::search() [clone .constprop.0] ()
#11 0x00005555567330c1 in nlsat::solver::imp::search_check() [clone .constprop.0] ()
#12 0x000055555672f62f in nlsat::solver::imp::check() [clone .constprop.0] ()
#13 0x000055555662739b in nra::solver::imp::check() ()
#14 0x000055555664d272 in nla::core::check() ()
#15 0x0000555555f86c2c in smt::theory_lra::imp::final_check_eh() ()
#16 0x0000555555fd71cb in smt::context::final_check() ()
#17 0x0000555555fd99f5 in smt::context::bounded_search() ()
#18 0x0000555555fda088 in smt::context::search() ()
#19 0x0000555555fda4d8 in smt::context::check(unsigned int, expr* const*, bool) ()
#20 0x00005555563f3e5f in solver_na2as::check_sat_core(unsigned int, expr* const*) ()
#21 0x0000555556419c4e in solver::check_sat(unsigned int, expr* const*) ()
#22 0x00005555563c43e7 in cmd_context::check_sat(unsigned int, expr* const*) ()
#23 0x00005555563ab29d in smt2::parser::operator()() ()
#24 0x00005555563935f0 in parse_smt2_commands(cmd_context&, std::basic_istream<char, std::char_traits<char> >&, bool, params_ref const&, char const*) ()
#25 0x00005555557b69fc in read_smtlib2_commands(char const*) ()
#26 0x000055555579a2fe in main ()

And it seems to not exit resultant

(gdb) finish
Run till exit from #0  0x0000555556e4bfdd in mpn_manager::mul(unsigned int const*, unsigned int, unsigned int const*, unsigned int, unsigned int*) const ()
0x0000555556df385d in mpz_manager<false>::big_mul(mpz const&, mpz const&, mpz&) ()
(gdb)
Run till exit from #0  0x0000555556df385d in mpz_manager<false>::big_mul(mpz const&, mpz const&, mpz&) ()
0x0000555556df65d1 in mpz_manager<false>::addmul(mpz const&, mpz const&, mpz const&, mpz&) ()
(gdb)
Run till exit from #0  0x0000555556df65d1 in mpz_manager<false>::addmul(mpz const&, mpz const&, mpz const&, mpz&) ()
0x0000555556d8a8ff in void polynomial::manager::imp::som_buffer::addmul_core<polynomial::polynomial, false>(mpz const&, polynomial::monomial const*, polynomial::polynomial const*) ()
(gdb)
Run till exit from #0  0x0000555556d8a8ff in void polynomial::manager::imp::som_buffer::addmul_core<polynomial::polynomial, false>(mpz const&, polynomial::monomial const*, polynomial::polynomial const*) ()
0x0000555556d93261 in polynomial::manager::imp::exact_div(polynomial::polynomial const*, polynomial::polynomial const*) ()
(gdb)
Run till exit from #0  0x0000555556d93261 in polynomial::manager::imp::exact_div(polynomial::polynomial const*, polynomial::polynomial const*) ()
0x0000555556da5845 in polynomial::manager::imp::resultant(polynomial::polynomial const*, polynomial::polynomial const*, unsigned int, obj_ref<polynomial::polynomial, polynomial::manager>&) ()
(gdb)
Run till exit from #0  0x0000555556da5845 in polynomial::manager::imp::resultant(polynomial::polynomial const*, polynomial::polynomial const*, unsigned int, obj_ref<polynomial::polynomial, polynomial::manager>&) ()
# gets stuck here

This is all on master as of now (253a724), so after the fix to the previous issue.

[mtzguido]

It seems we do not exit the while(true) loop in resultant, even if it has a checkpoint. But I don't see any messages with -tr:resultant, which I don't understand (I used ./configure -t to enable them).

I did add a print statement for degA/degB in that loop, this is the output from the time it apparently gets stuck:

[00:00:36.922098] GG degA=1, degB=0
[00:00:36.924976] GG degA=4, degB=3
[00:00:36.941329] GG degA=3, degB=2
[00:00:37.518958] GG degA=2, degB=1
[00:00:56.365987] GG degA=2, degB=1
[00:00:56.366032] GG degA=2, degB=1
[00:00:56.366768] GG degA=4, degB=3
[00:00:56.368425] GG degA=3, degB=2
[00:00:56.392395] GG degA=2, degB=1
[00:00:57.726402] GG degA=2, degB=1
[00:00:57.726648] GG degA=3, degB=2
[00:00:57.726762] GG degA=2, degB=1
[00:00:57.727854] GG degA=4, degB=3
[00:00:57.728916] GG degA=3, degB=2
[00:00:57.733493] GG degA=2, degB=1
[00:00:57.746962] GG degA=2, degB=1
[00:00:57.748589] GG degA=6, degB=5
[00:00:57.754549] GG degA=5, degB=4
[00:00:57.807473] GG degA=4, degB=3
[00:00:58.136908] GG degA=3, degB=2
[00:00:58.931792] GG degA=2, degB=1
[00:00:59.791459] GG degA=3, degB=2
[00:00:59.791625] GG degA=2, degB=1
[00:01:06.406324] GG degA=2, degB=1
[00:01:06.406358] GG degA=1, degB=0
[00:01:06.406560] GG degA=7, degB=6
[00:01:06.406741] GG degA=6, degB=5
[00:01:06.407225] GG degA=5, degB=4
[00:01:06.408446] GG degA=4, degB=3
[00:01:06.410983] GG degA=3, degB=2
[00:01:06.415441] GG degA=2, degB=1
[00:01:06.420005] GG degA=4, degB=3
[00:01:06.420028] GG degA=3, degB=2
[00:01:06.420084] GG degA=2, degB=1
[00:01:06.420198] GG degA=3, degB=2
[00:01:06.420215] GG degA=2, degB=1
[00:01:06.420307] GG degA=6, degB=5
[00:01:06.420372] GG degA=5, degB=4
[00:01:06.420502] GG degA=4, degB=3
[00:01:06.420771] GG degA=3, degB=2
[00:01:06.421272] GG degA=2, degB=1
[00:01:06.421772] GG degA=4, degB=3
[00:01:06.421803] GG degA=3, degB=2
[00:01:06.421858] GG degA=2, degB=1
[00:01:06.421952] GG degA=2, degB=1
[00:01:06.422046] GG degA=6, degB=5
[00:01:06.422109] GG degA=5, degB=4
[00:01:06.422223] GG degA=4, degB=3
[00:01:06.422460] GG degA=3, degB=2
[00:01:06.422875] GG degA=2, degB=1
[00:01:06.423285] GG degA=3, degB=2
[00:01:06.423302] GG degA=2, degB=1
[00:01:06.423357] GG degA=2, degB=1
[00:01:06.423449] GG degA=6, degB=5
[00:01:06.423514] GG degA=5, degB=4
[00:01:06.423629] GG degA=4, degB=3
[00:01:06.423871] GG degA=3, degB=2
[00:01:06.424305] GG degA=2, degB=1
[00:01:06.424721] GG degA=3, degB=2
[00:01:06.424737] GG degA=2, degB=1
[00:01:06.424788] GG degA=2, degB=1
[00:01:06.424835] GG degA=2, degB=1
[00:01:06.424904] GG degA=2, degB=1
[00:01:06.424986] GG degA=2, degB=1
[00:01:06.425660] GG degA=8, degB=7
[00:01:06.426429] GG degA=7, degB=6
[00:01:06.428994] GG degA=6, degB=5
[00:01:06.437238] GG degA=5, degB=4
[00:01:06.456743] GG degA=4, degB=3
[00:01:06.495266] GG degA=3, degB=2
[00:01:06.556094] GG degA=2, degB=1
[00:01:06.615064] GG degA=4, degB=3
[00:01:06.615123] GG degA=3, degB=2
[00:01:06.615291] GG degA=2, degB=1
[00:01:06.615522] GG degA=3, degB=2
[00:01:06.615539] GG degA=2, degB=1
[00:01:06.615987] GG degA=9, degB=8
[00:01:06.616986] GG degA=8, degB=7
[00:01:06.620689] GG degA=7, degB=6
[00:01:06.633275] GG degA=6, degB=5
[00:01:06.665726] GG degA=5, degB=4
[00:01:06.734044] GG degA=4, degB=3
[00:01:06.854668] GG degA=3, degB=2
[00:01:07.028335] GG degA=2, degB=1
[00:01:07.190838] GG degA=3, degB=2
[00:01:07.190854] GG degA=2, degB=1
[00:01:07.191006] GG degA=6, degB=5
[00:01:07.191094] GG degA=5, degB=4
[00:01:07.191316] GG degA=4, degB=3
[00:01:07.191900] GG degA=3, degB=2
[00:01:07.193379] GG degA=2, degB=1
[00:01:07.195305] GG degA=4, degB=3
[00:01:07.195384] GG degA=3, degB=2
[00:01:07.195547] GG degA=2, degB=1
[00:01:07.195802] GG degA=4, degB=3
[00:01:07.195835] GG degA=3, degB=2
[00:01:07.195885] GG degA=2, degB=1
[00:01:07.196017] GG degA=6, degB=5
[00:01:07.196080] GG degA=5, degB=4
[00:01:07.196193] GG degA=4, degB=3
[00:01:07.196432] GG degA=3, degB=2
[00:01:07.196854] GG degA=2, degB=1
[00:01:07.197284] GG degA=4, degB=3
[00:01:07.197315] GG degA=3, degB=2
[00:01:07.197365] GG degA=2, degB=1
[00:01:07.197529] GG degA=6, degB=5
[00:01:07.197613] GG degA=5, degB=4
[00:01:07.197747] GG degA=4, degB=3
[00:01:07.198052] GG degA=3, degB=2
[00:01:07.198631] GG degA=2, degB=1
[00:01:07.209624] GG degA=29, degB=28
[00:01:07.227018] GG degA=28, degB=27
[00:01:07.273268] GG degA=27, degB=26
[00:01:07.407525] GG degA=26, degB=25
[00:01:07.759218] GG degA=25, degB=24
[00:01:08.610581] GG degA=24, degB=23
[00:01:10.553705] GG degA=23, degB=22
[00:01:14.688448] GG degA=22, degB=21
[00:01:22.858689] GG degA=21, degB=20
[00:01:37.984604] GG degA=20, degB=19
[00:02:04.568094] GG degA=19, degB=18
[00:02:49.277091] GG degA=18, degB=17
[00:04:01.249390] GG degA=17, degB=16
[00:05:53.076644] GG degA=16, degB=15

Note how the last few lines get progressively slower, so maybe this is just extremely slow.

[levnach]

Fixed by 887ecc0.
There was a previous fix in nlsat that moved the perf bottleneck from nlsat to grobner. I introduced a parameter that allows throttle grobner method aggressively, that seems beneficial in general as well.

[levnach]

@mtzguido, thank you for analysis! It seems the algorithm calculating a resultant was creating huge numbers. It might be worth looking if there is a more efficient algorithm in Cohen's book.

[mtzguido]

Thanks @levnach, but I think some issue still remains. By setting the random_seed to 86, this file still ran for over six hours. Attaching a log.

L.txt

[mtzguido]

The stack trace (after running for a couple of hours too) seems somewhat similar too:

(gdb) where
#0  0x0000555556e4fb17 in mpn_manager::mul(unsigned int const*, unsigned int, unsigned int const*, unsigned int, unsigned int*) const ()
#1  0x0000555556df741d in mpz_manager<false>::big_mul(mpz const&, mpz const&, mpz&) ()
#2  0x0000555556dfa191 in mpz_manager<false>::addmul(mpz const&, mpz const&, mpz const&, mpz&) ()
#3  0x0000555556d8e43f in void polynomial::manager::imp::som_buffer::addmul_core<polynomial::polynomial, false>(mpz const&, polynomial::monomial const*, polynomial::polynomial const*) ()
#4  0x0000555556d96da1 in polynomial::manager::imp::exact_div(polynomial::polynomial const*, polynomial::polynomial const*) ()
#5  0x0000555556daa274 in polynomial::manager::imp::gcd_prs(polynomial::polynomial const*, polynomial::polynomial const*, unsigned int, obj_ref<polynomial::polynomial, polynomial::manager>&) ()
#6  0x0000555556da7987 in polynomial::manager::imp::gcd(polynomial::polynomial const*, polynomial::polynomial const*, obj_ref<polynomial::polynomial, polynomial::manager>&) ()
#7  0x0000555556daf891 in polynomial::manager::imp::factor_core(polynomial::polynomial const*, polynomial::manager::factors&, polynomial::factor_params const&) ()
#8  0x0000555556dc764b in polynomial::cache::imp::factor(polynomial::polynomial*, ref_vector<polynomial::polynomial, polynomial::manager>&) ()
#9  0x0000555556721b3d in nlsat::explain::imp::insert_fresh_factors_in_todo(obj_ref<polynomial::polynomial, polynomial::manager>&) ()
#10 0x00005555567223a9 in nlsat::explain::imp::psc_discriminant(ref_vector<polynomial::polynomial, polynomial::manager>&, unsigned int) ()
#11 0x0000555556726d19 in nlsat::explain::imp::project_cdcac(ref_vector<polynomial::polynomial, polynomial::manager>&, unsigned int) ()
#12 0x000055555671d72e in nlsat::explain::main_operator(unsigned int, sat::literal const*, nlsat::scoped_literal_vector&) ()
#13 0x0000555556734c90 in nlsat::solver::imp::search() [clone .constprop.0] ()
#14 0x00005555567364c1 in nlsat::solver::imp::search_check() [clone .constprop.0] ()
#15 0x0000555556732a2f in nlsat::solver::imp::check() [clone .constprop.0] ()
#16 0x000055555662a41b in nra::solver::imp::check() ()
#17 0x00005555566502f2 in nla::core::check() ()
#18 0x0000555555f887ec in smt::theory_lra::imp::final_check_eh() ()
#19 0x0000555555fd8d4b in smt::context::final_check() ()
#20 0x0000555555fdb575 in smt::context::bounded_search() ()
#21 0x0000555555fdbc08 in smt::context::search() ()
#22 0x0000555555fdc058 in smt::context::check(unsigned int, expr* const*, bool) ()
#23 0x00005555563f6ddf in solver_na2as::check_sat_core(unsigned int, expr* const*) ()
#24 0x000055555641caae in solver::check_sat(unsigned int, expr* const*) ()
#25 0x00005555563c6467 in cmd_context::check_sat(unsigned int, expr* const*) ()
#26 0x00005555563acd0d in smt2::parser::operator()() ()
#27 0x00005555563950b0 in parse_smt2_commands(cmd_context&, std::basic_istream<char, std::char_traits<char> >&, bool, params_ref const&, char const*)
    ()
#28 0x00005555557b737c in read_smtlib2_commands(char const*) ()
#29 0x000055555579ac5e in main ()
(gdb) return
Make selected stack frame return now? (y or n)
Please answer y or n.
Make selected stack frame return now? (y or n) n
Not confirmed
(gdb) help finish
finish, fin
Execute until selected stack frame returns.
Usage: finish
Upon return, the value returned is printed and put in the value history.
(gdb) finish
Run till exit from #0  0x0000555556e4fb17 in mpn_manager::mul(unsigned int const*, unsigned int, unsigned int const*, unsigned int, unsigned int*) const ()
0x0000555556df741d in mpz_manager<false>::big_mul(mpz const&, mpz const&, mpz&) ()
(gdb)
Run till exit from #0  0x0000555556df741d in mpz_manager<false>::big_mul(mpz const&, mpz const&, mpz&) ()
0x0000555556dfa191 in mpz_manager<false>::addmul(mpz const&, mpz const&, mpz const&, mpz&) ()
(gdb)
Run till exit from #0  0x0000555556dfa191 in mpz_manager<false>::addmul(mpz const&, mpz const&, mpz const&, mpz&) ()
0x0000555556d8e43f in void polynomial::manager::imp::som_buffer::addmul_core<polynomial::polynomial, false>(mpz const&, polynomial::monomial const*, polynomial::polynomial const*) ()
(gdb)
Run till exit from #0  0x0000555556d8e43f in void polynomial::manager::imp::som_buffer::addmul_core<polynomial::polynomial, false>(mpz const&, polynomial::monomial const*, polynomial::polynomial const*) ()
0x0000555556d96da1 in polynomial::manager::imp::exact_div(polynomial::polynomial const*, polynomial::polynomial const*) ()
(gdb)
Run till exit from #0  0x0000555556d96da1 in polynomial::manager::imp::exact_div(polynomial::polynomial const*, polynomial::polynomial const*) ()

^C
Program received signal SIGINT, Interrupt.

It gets stuck at exact_div, apparently.

I guess my question is why doesn't the rlimit kick in, even if this code were to be super slow.