search

AliveToolkit / alive2

Automatic verification of LLVM optimizations
MIT License
789 stars 99 forks source link

Z3 doesn't respect memory limit with QI & FPA formula #785

Closed nunoplopes closed 2 years ago

nunoplopes commented 2 years ago

So this doesn't get lost. This command consumes a lot of memory as it doesn't respect the memory limit.

$ alive-tv ~/llvm/llvm/test/Transforms/InstCombine/fast-math.ll -disable-undef-input -disable-poison-input -func=sqrt_intrinsic_three_args1

The trace looks like:

#158 0x00007f112ff9bd61 smt::context::internalize_formula_core(app*, bool)
#159 0x00007f11301deac8 smt::theory_fpa::assert_cnstr(expr*)
#160 0x00007f11301df0d1 smt::theory_fpa::internalize_atom(app*, bool)
#161 0x00007f112ff967d1 smt::context::internalize_theory_atom(app*, bool)
#162 0x00007f112ff9c226 smt::context::internalize_formula(expr*, bool)
#163 0x00007f112ff9bd61 smt::context::internalize_formula_core(app*, bool)
#164 0x00007f112ff9e115 smt::context::internalize_assertion(expr*, app*, unsigned int)
#165 0x00007f1130070184 smt::qi_queue::instantiate(smt::qi_queue::entry&)
#166 0x00007f1130070932 smt::qi_queue::instantiate()
#167 0x00007f113015cac1 smt::context::propagate()

The formula seems very DNF-iy. Something is odd.

nunoplopes commented 2 years ago

QI doesn't seem at fault. I tried to pre-process the formula to remove all quantified variables (booleans), and had to kill it after 8 GBs of RAM consumption (limit=2 GBs).