1
Vote

Parser Segfault

description

I encountered a segmentation fault in Z3 when parsing the following smtlib2 input (already minimized with ddsmt):
(set-logic QF_UFBV)
(declare-fun f ((_ BitVec 1)) (_ BitVec 1))
(assert (= (_ bv0 1) (f (_ bv0 1))))
(check-sat)
(exit)
If the logic is set to e.g. QF_AUFBV the segmentation fault does not occur. I am currently using the version from the master branch commit cee7dd39444c9060186df79c2a2c7f8845de415b.

I also tried it with the current unstable branch version commit 882dbfc706db6e7f83b0673906983d21404b8a19, which has the same behaviour.

file attachments

comments

NBjorner wrote Dec 16, 2014 at 12:33 AM

What platform does this manifest itself on?

MPreiner wrote Dec 16, 2014 at 9:27 AM

It's Linux 64 Bit.

wintersteiger wrote Dec 16, 2014 at 2:43 PM

Thanks or reporting this issue! I'm unable to reproduce this behavior; could you tell us what exact flavor of Linux you're using?

MPreiner wrote Dec 16, 2014 at 4:00 PM

I am running the current version of Archlinux with the following gcc version:

$ gcc -v
Using built-in specs.
COLLECT_GCC=gcc
COLLECT_LTO_WRAPPER=/usr/lib/gcc/x86_64-unknown-linux-gnu/4.9.2/lto-wrapper
Target: x86_64-unknown-linux-gnu
Configured with: /build/gcc/src/gcc-4.9.2/configure --prefix=/usr --libdir=/usr/lib --libexecdir=/usr/lib --mandir=/usr/share/man --infodir=/usr/share/info --with-bugurl=https://bugs.archlinux.org/ --enable-languages=c,c++,ada,fortran,go,lto,objc,obj-c++ --enable-shared --enable-threads=posix --with-system-zlib --enable-__cxa_atexit --disable-libunwind-exceptions --enable-clocale=gnu --disable-libstdcxx-pch --disable-libssp --enable-gnu-unique-object --enable-linker-build-id --enable-cloog-backend=isl --disable-isl-version-check --disable-cloog-version-check --enable-lto --enable-plugin --enable-install-libiberty --with-linker-hash-style=gnu --disable-multilib --disable-werror --enable-checking=release
Thread model: posix
gcc version 4.9.2 (GCC)

When I compile z3 in debug mode (configure -d) the segfault does not happen. I also tried a different box running Gentoo Linux with gcc version 4.7.3 and I couldn't reproduce the behaviour.

I can reproduce the segfault on the Archlinux machine with the following steps:

PYTHON="python2.7" ./configure
cd build && make
./z3 segfault.smt2


I attached info.tar.gz, which contains valgrind output and a list of all installed library versions on my system.

wintersteiger wrote Dec 17, 2014 at 7:14 PM

Alright, I'm finally able to reproduce this problem. I had to install archlinux though, the problem does not occur on any other system. No ETA on a fix though.

MPreiner wrote Dec 17, 2014 at 8:12 PM

I also was only able to reproduce it on Archlinux. Archlinux is a cutting-edge distribution, so there might be still some problem in a software package. I think the segfault is related to some newer versions of libraries and/or gcc that do not play along well yet. I'll keep you posted if the behavior changes on my system .

nunoplopes wrote Apr 29, 2015 at 3:57 PM

AFAICT this is a bug in gcc. I traced the generated assembly code and it's wrong.
I've used gcc 4.9.2 on Cygwin 64 bits.