Segfault in small SMT problem involving 'let'

[sdthompson1]

I've been experimenting with Vampire, using the SMT-LIB input format, and found a crash. I managed to reduce the input file down to the following:

(define-fun foo ((b Bool)) Int (let ((b2 b)) 123))
(check-sat)

For me, running vampire --input_syntax smtlib2 with that file as input produces a SIGSEGV error.

Using --traceback on I get the following stack trace:

#0  0x00007f011424742f in __GI___wait4 (pid=13643, stat_loc=stat_loc@entry=0x7ffcc63ff7b8, options=options@entry=0, usage=usage@entry=0x0) at ../sysdeps/unix/sysv/linux/wait4.c:30
#1  0x00007f01142473ab in __GI___waitpid (pid=<optimised out>, stat_loc=stat_loc@entry=0x7ffcc63ff7b8, options=options@entry=0) at ./posix/waitpid.c:38
#2  0x00007f01141adbdb in do_system (line=<optimised out>) at ../sysdeps/posix/system.c:171
#3  0x000055ed7a2c4a43 in try_gdb (pid=13641) at /home/stephen/solvers/vampire/Debug/Tracer.cpp:47
#4  0x000055ed7a2c4cd2 in Debug::Tracer::printStack () at /home/stephen/solvers/vampire/Debug/Tracer.cpp:73
#5  0x000055ed7a2c2622 in Debug::Assertion::violated (file=0x55ed7aa9ca40 "/home/stephen/solvers/vampire/Lib/Stack.hpp", line=202, cond=0x55ed7aa9ca6c "_stack+n < _cursor") at /home/stephen/solvers/vampire/Debug/Assertion.cpp:49
#6  0x000055ed7a2b95b4 in Lib::Stack<Kernel::Signature::Symbol*>::operator[] (this=0x55eda61bb968, n=1) at /home/stephen/solvers/vampire/Lib/Stack.hpp:202
#7  0x000055ed7a2b592d in Kernel::Signature::functionArity (this=0x55eda61bb910, number=1) at /home/stephen/solvers/vampire/Kernel/Signature.hpp:516
#8  0x000055ed7a419892 in Kernel::Term::createLet (functor=1, variables=0x0, binding=..., body=..., bodySort=...) at /home/stephen/solvers/vampire/Kernel/Term.cpp:1037
#9  0x000055ed7a9150ae in Parse::SMTLIB2::parseLetEnd (this=0x7ffcc6400830, exp=0x55eda61da5e0) at /home/stephen/solvers/vampire/Parse/SMTLIB2.cpp:1525
#10 0x000055ed7a921a7b in Parse::SMTLIB2::parseTermOrFormula (this=0x7ffcc6400830, body=0x55eda61da5e0, isSort=false) at /home/stephen/solvers/vampire/Parse/SMTLIB2.cpp:2887
#11 0x000055ed7a90cba6 in Parse::SMTLIB2::readDefineFun (this=0x7ffcc6400830, name="foo", iArgs=0x55eda61c43d0, oSort=0x55eda61da610, body=0x55eda61da5e0, typeArgs=..., recursive=false) at /home/stephen/solvers/vampire/Parse/SMTLIB2.cpp:771
#12 0x000055ed7a908993 in Parse::SMTLIB2::readBenchmark (this=0x7ffcc6400830, bench=0x55eda61c4410) at /home/stephen/solvers/vampire/Parse/SMTLIB2.cpp:273
#13 0x000055ed7a9070e6 in Parse::SMTLIB2::parse (this=0x7ffcc6400830, bench=0x55eda61da790) at /home/stephen/solvers/vampire/Parse/SMTLIB2.cpp:84
#14 0x000055ed7a907044 in Parse::SMTLIB2::parse (this=0x7ffcc6400830, str=...) at /home/stephen/solvers/vampire/Parse/SMTLIB2.cpp:78
#15 0x000055ed7a901246 in Shell::UIHelper::tryParseSMTLIB2 (input=...) at /home/stephen/solvers/vampire/Shell/UIHelper.cpp:221
#16 0x000055ed7a90180e in Shell::UIHelper::parseStream (input=..., inputSyntax=Shell::Options::InputSyntax::SMTLIB2, verbose=true, preferSMTonAuto=true) at /home/stephen/solvers/vampire/Shell/UIHelper.cpp:315
#17 0x000055ed7a901e01 in Shell::UIHelper::parseFile (inputFile="/home/stephen/projects/b-notes/smt-bugs/vampire-segfault.smt", inputSyntax=Shell::Options::InputSyntax::SMTLIB2, verbose=true) at /home/stephen/solvers/vampire/Shell/UIHelper.cpp:355
#18 0x000055ed7a2b3d3f in main (argc=6, argv=0x7ffcc6400f18) at /home/stephen/solvers/vampire/vampire.cpp:781

I'm not really sure what any of that means, but hopefully this report will be helpful to someone :)

[MichaelRawson]

Thanks for the report!

@mezpusz regrettably I think you touched the SMT-LIB parser most recently. Any ideas?

[mezpusz]

The issue seems to be that we assume the let-bound term to be a proper term here:
https://github.com/vprover/vampire/blob/master/Kernel/Term.cpp#L1035
In this case it's a boolean variable, so we do something we shouldn't. Maybe pass the binding sort as well?

[MichaelRawson]

Yeah, if not too painful I guess this should be a TypedTermList. I'll try and fix it now.

[MichaelRawson]

The crashing code turns out to be debug checks that can be skipped in this thorny case, but there is another crash stemming from the same logic in SortHelper. @quickbeam123 would you be able to have a look? I think the fix is to look up the sort of the binding in map if it's a variable, but I'm not 100% sure what's going on in the machinery.

[mezpusz]

Could we just use TypedTermList everywhere in the parser? I can also have a look at some point later this week.

[MichaelRawson]

In principle yes, it was just a big diff and SortHelper turned out to also be broken - go for it if feeling inspired.

IMO the whole let special term design is a bit broken, I think it could just be a regular polymorphic term $let : !>[Bind: $tType, $In: $tType]: (Bind * Bind * In) > In, like lambda-expressions, but maybe I didn't think about this carefully enough yet. There's also the weird let-tuple thing.