Segfault on some command line arguments

dreal / dreal2

Please check dreal4 instead.

https://github.com/dreal/dreal4

GNU General Public License v3.0

13 stars 15 forks source link

Segfault on some command line arguments #39

Closed kini closed 10 years ago

kini commented 10 years ago

dReal / segfaults:

kkini@0143:~/src/dreal/build/release$ ./solver /
Segmentation fault (core dumped)

Sorry I can't provide any more info. I couldn't figure out how to get the build process to produce an executable with debug symbols.

soonhokong commented 10 years ago

Hi @kini, could you download and run http://dreal.cs.cmu.edu/archives/dReal ?

Also, it would be great if you provide us the version of your operating system (i.e. Ubuntu 14.04).

kini commented 10 years ago

Sure. Same result:

kkini@0143:~/src/dreal/build/release$ ./dReal /
Segmentation fault (core dumped)

This is on a Ubuntu 14.04 machine indeed. I also tried on a Debian Sid machine:

[1] fs@erdos /tmp $ ./dReal /
Segmentation fault

soonhokong commented 10 years ago

@kini, thanks for the information. We're using Ubuntu 12.04 LTS to test builds. I'll install 14.04 and check the problem.

kini commented 10 years ago

If it helps, here's a kind of useless backtrace from the Debian Sid machine using the binary you linked:

[1] fs@erdos /tmp $ gdb --quiet --args ./dReal /
Reading symbols from /tmp/dReal...done.
(gdb) r
Starting program: /tmp/./dReal /
warning: no loadable sections found in added symbol-file system-supplied DSO at 0x7ffff7ffd000

Program received signal SIGSEGV, Segmentation fault.
0x00000000006311d6 in __strcmp_sse42 ()
(gdb) bt
#0  0x00000000006311d6 in __strcmp_sse42 ()
#1  0x0000000000405610 in main ()

pzuliani commented 10 years ago

I’ve build dreal and run ctest on 14.04 with no problem (ie, the same tests fail in 12.04 and 14.04)

Paolo

soonhokong commented 10 years ago

@kini,

I see the problem now. Is there any reason you provided / as an argument to dReal? It's expecting a file. For instance,

./solver problem.smt2

Of course, the segmentation fault is a bug. I think it can be fixed easily. I will fix it and close this one soon.

kini commented 10 years ago

devReal / was just the smallest buggy example I could find. I was reading the dReal website's front page and wanted to try the SMT2 formula shown there, so I ran dReal and pasted the formula into the terminal. This worked fine. Further down on the page it is suggested that I try dReal --verbose to see the decision trace, which I did, but I was confronted with the following output:

kkini@0143:~/src/dreal/build/release$ ./solver --verbose
# Error: ./solver  extension not recognized. Please use one in { smt2, cnf } or stdin (smtlib2 is assumed) (triggered at /home/kkini/src/dreal/src/main.cpp, 119)

So I thought maybe I could avoid this message (maybe this too is a bug?) by doing dReal --verbose /dev/stdin:

kkini@0143:~/src/dreal/build/release$ ./solver --verbose /dev/stdin
Segmentation fault (core dumped)

From this point I just refined the invocation until I had a minimal instance. Thanks for taking a look!

soonhokong commented 10 years ago

@kini, I understand the context. I'm fixing the issue.

soonhokong commented 10 years ago

@kini, I fixed the problems.

If you want to take the input from terminal, you can do so by not providing a filename. For example:
```
./solver --verbose
```
If you use --proof or --visualize option without providing a filename, dReal will pick output as a default filename to save those extra information. That is, you will have output.proof, output.json respectively.
If you provide a filename, we check if it exists and is a file (not a dir). If the check fails, it generates an error.

I also updated the static binary at http://dreal.cs.cmu.edu/archives/dReal .

kini commented 10 years ago

Awesome! Thanks for fixing it so quickly! :)

soonhokong commented 10 years ago

@kini, thanks again for the report. Please let us know if you find anything strange.