crash

[regehr]

cc @Hatsunespica

seen on Ubuntu 22.04 with very recent Z3 and LLVM:

regehr@john-home:~/test/log1580/out$ cat reduced.ll 

define i32 @test(ptr %isec) {
entry:
  %mul16 = fmul nsz float 0.000000e+00, 0.000000e+00
  %mul55 = fmul nsz arcp contract float 0.000000e+00, 0.000000e+00
  %cmp63 = fcmp nnan ogt float %mul55, %mul16
  br i1 %cmp63, label %cleanup, label %if.end

if.end:                                           ; preds = %entry
  br label %cleanup

cleanup:                                          ; preds = %if.end, %entry
  ret i32 0
}
regehr@john-home:~/test/log1580/out$ ~/alive2-regehr/build/alive-tv --smt-to=60000 --disable-undef-input --disable-poison-input reduced.ll 

----------------------------------------
define i32 @test(ptr %isec) {
entry:
  %mul16 = fmul nsz float 0.000000, 0.000000
  %mul55 = fmul nsz arcp contract float 0.000000, 0.000000
  %cmp63 = fcmp nnan ogt float %mul55, %mul16
  br i1 %cmp63, label %cleanup, label %if.end

if.end:
  br label %cleanup

cleanup:
  ret i32 0
}
=>
define i32 @test(ptr nocapture noread nowrite %isec) nofree willreturn memory(none) {
entry:
  ret i32 0
}
 #0 0x00007f2e663fe950 llvm::sys::PrintStackTrace(llvm::raw_ostream&, int) (/home/regehr/llvm-project/for-alive/lib/libLLVMSupport.so.18git+0x1fe950)
 #1 0x00007f2e663fb95f llvm::sys::RunSignalHandlers() (/home/regehr/llvm-project/for-alive/lib/libLLVMSupport.so.18git+0x1fb95f)
 #2 0x00007f2e663fbab5 SignalHandler(int) Signals.cpp:0:0
 #3 0x00007f2e65a42520 (/lib/x86_64-linux-gnu/libc.so.6+0x42520)
 #4 0x00007f2e688e031c smt::context::undo_mk_enode() /home/regehr/z3/src/smt/smt_internalizer.cpp:1071:45
 #5 0x00007f2e688c04e6 undo_trail_stack(ptr_vector<trail>&, unsigned int) /home/regehr/z3/src/util/trail.h:387:15
 #6 0x00007f2e688c04e6 smt::context::undo_trail_stack(unsigned int) /home/regehr/z3/src/smt/smt_context.cpp:1963:27
 #7 0x00007f2e688c04e6 smt::context::flush() /home/regehr/z3/src/smt/smt_context.cpp:3015:25
 #8 0x00007f2e688c0624 smt::context::~context() /home/regehr/z3/src/smt/smt_context.cpp:186:37
 #9 0x00007f2e688ebeb1 void dealloc<smt::kernel::imp>(smt::kernel::imp*) /home/regehr/z3/src/util/memory_manager.h:97:23
#10 0x00007f2e688ebeb1 void dealloc<smt::kernel::imp>(smt::kernel::imp*) /home/regehr/z3/src/util/memory_manager.h:94:6
#11 0x00007f2e688ebeb1 smt::kernel::~kernel() /home/regehr/z3/src/smt/smt_kernel.cpp:59:16
#12 0x00007f2e68bb8083 void dealloc<smt::kernel>(smt::kernel*) /home/regehr/z3/src/util/memory_manager.h:97:23
#13 0x00007f2e68bb8083 void dealloc<smt::kernel>(smt::kernel*) /home/regehr/z3/src/util/memory_manager.h:94:6
#14 0x00007f2e68bb8083 smt_tactic::scoped_init_ctx::~scoped_init_ctx() /home/regehr/z3/src/smt/tactic/smt_tactic_core.cpp:148:24
#15 0x00007f2e68bb8083 smt_tactic::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) /home/regehr/z3/src/smt/tactic/smt_tactic_core.cpp:310:9
#16 0x00007f2e68318e17 ref<goal>::dec_ref() /home/regehr/z3/src/util/ref.h:33:13
#17 0x00007f2e68318e17 ref<goal>::~ref() /home/regehr/z3/src/util/ref.h:58:16
#18 0x00007f2e68318e17 and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) /home/regehr/z3/src/tactic/tactical.cpp:123:9
#19 0x00007f2e6831cd29 exec(tactic&, ref<goal> const&, sref_buffer<goal, 16u>&) /home/regehr/z3/src/tactic/tactic.cpp:166:18
#20 0x00007f2e6831d51c check_sat(tactic&, ref<goal>&, ref<model>&, labels_vec&, obj_ref<app, ast_manager>&, obj_ref<dependency_manager<ast_manager::expr_dependency_config>::dependency, ast_manager>&, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char>>&) /home/regehr/z3/src/tactic/tactic.cpp:196:5
#21 0x00007f2e6859f36a (anonymous namespace)::tactic2solver::check_sat_core2(unsigned int, expr* const*) /home/regehr/z3/src/solver/tactic2solver.cpp:241:28
#22 0x00007f2e6858b43e solver_na2as::check_sat_core(unsigned int, expr* const*) /home/regehr/z3/src/solver/solver_na2as.cpp:67:27
#23 0x00007f2e68589851 solver::check_sat(unsigned int, expr* const*) /home/regehr/z3/src/solver/solver.cpp:318:27
#24 0x00007f2e68fa5d8c scoped_rlimit::~scoped_rlimit() /home/regehr/z3/src/util/rlimit.h:70:35
#25 0x00007f2e68fa5d8c _solver_check /home/regehr/z3/src/api/api_solver.cpp:669:9
#26 0x00007f2e68fa6a3b z3_log_ctx::~z3_log_ctx() /home/regehr/z3/build/src/api/api_log_macros.h:11:124
#27 0x00007f2e68fa6a3b Z3_solver_check /home/regehr/z3/src/api/api_solver.cpp:683:9
#28 0x000055868109f05d smt::Solver::check() const (/home/regehr/alive2-regehr/build/alive-tv+0x12a05d)
#29 0x00005586810a9dd2 check_refinement(util::Errors&, tools::Transform const&, IR::State&, IR::State&, IR::Value const*, IR::Type const&, IR::State::ValTy const&, IR::State::ValTy const&, bool) transform.cpp:0:0
#30 0x00005586810afaad tools::TransformVerify::verify() const (/home/regehr/alive2-regehr/build/alive-tv+0x13aaad)
#31 0x0000558680fb4417 (anonymous namespace)::verify(llvm::Function&, llvm::Function&, llvm::TargetLibraryInfoWrapperPass&, smt::smt_initializer&, std::ostream&, bool, bool) compare.cpp:0:0
#32 0x0000558680fb66c4 llvm_util::Verifier::compareFunctions(llvm::Function&, llvm::Function&) (/home/regehr/alive2-regehr/build/alive-tv+0x416c4)
#33 0x0000558680faa908 main (/home/regehr/alive2-regehr/build/alive-tv+0x35908)
#34 0x00007f2e65a29d90 __libc_start_call_main ./csu/../sysdeps/nptl/libc_start_call_main.h:58:16
#35 0x00007f2e65a29e40 call_init ./csu/../csu/libc-start.c:128:20
#36 0x00007f2e65a29e40 __libc_start_main ./csu/../csu/libc-start.c:379:5
#37 0x0000558680faba55 _start (/home/regehr/alive2-regehr/build/alive-tv+0x36a55)
PLEASE submit a bug report to https://github.com/llvm/llvm-project/issues/ and include the crash backtrace.
Stack dump:
0.  Program arguments: /home/regehr/alive2-regehr/build/alive-tv --smt-to=60000 --disable-undef-input --disable-poison-input reduced.ll
Segmentation fault (core dumped)
regehr@john-home:~/test/log1580/out$ 

[nunoplopes]

I can't repro this with a 2 weeks old Z3. It may be related with https://github.com/Z3Prover/z3/issues/6972 Essentially, floats are broken in Z3 right now.

[regehr]

please let me know when this is better -- I'll wait until then to update the compiler explorer instance.

I guess it's probably silly to bump Z3 at the same time I bump LLVM and Alive2. should I just start using the most recent Z3 release on our CE node?

[nunoplopes]

Z3 should be fixed now. Can you try again pls?

[regehr]

works now thx!