search

AliveToolkit / alive2

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

alive-tv does not respond to signals #1101

Open DaKnig opened 2 hours ago

DaKnig commented 2 hours ago

when alive-tv runs as part of my script I can't ctrl-c out of it, if it takes too long. I'd expect this program to exit immediately with non zero exit status.

nunoplopes commented 2 hours ago

That's a bug in Z3. We use Z3's ctrl-c handler, which does a soft kill of the solving algorithm. Fixing this is a mater of figuring out which algorithm in Z3 is not checking the checkpointing mechanism. I'm happy to investigate if you give me a trace (use gdb to get several traces of when it gets stuck).

DaKnig commented 2 hours ago

I am giving it a lot of constraints. in fact I am trying to use alive2 to make a simple slow superoptimizer. so I dont think I could give a small reproducer... please instruct me what info exactly you'd want :)

nunoplopes commented 2 hours ago

I don't need a reproducer. You just need to run it inside gdb and break execution a few times after ctrl-c stops working. If the stack looks similar in all cases, it's usually easy to fix it.