Re: Hampi build problems
Elnatan Reisner
help.
I first tried to compile on a Mac, which I knew would require some
work. Eventually I got stuck, and I'll come back to that. In the
meantime, though, I tried to build on a Linux machine, where I
expected things would just work, but they didn't.
First of all, the INSTALL.txt file says to run ./configure and make.
(The Makefile actually calls configure, so that's not necessary, but
that's a minor point.) But that's not all you have to do: You need to
set 2 paths in lib/cfganalyzer-2007-12-03/Makefile: one to your C++
compiler (although 'g++' is probably right) and one to your OCaml
library directory. You seem *not* to have to set the path to libstp.a,
despite what the Makefile says, because it's location is fixed.
Having set these paths, 'make' worked, but 'make verify' died with
this message:
.java: symbol lookup error: /path/to/hampi-read-only/lib/stp-jni/
64bit/libSTPJNI.so: undefined symbol:
_ZSt16__ostream_insertIcSt11char_traitsIcEERSt13basic_ostreamIT_T0_ES6_PKS3_l
If anyone knows how to diagnose this, please let me know.
Now, back to the Mac
I compiled STP myself and tweaked lib/stp-jni/Makefile as needed to
make 'make' work. However, I get a
java.lang.UnsatisfiedLinkError: no STPJNI in java.library.path
error when doing 'make verify' or when trying to run hampi.sh on one
of the test files. 'make verify' also gives me a bunch of
java.lang.NoClassDefFoundError: Could not initialize class stp.STPJNI
errors.
I'm attaching my build log and a patch containing my changes to Hampi.
STP doesn't compile with my machine's default gcc:
elnatan$ gcc --version
i686-apple-darwin9-gcc-4.2.1 (GCC) 4.2.1 (Apple Inc. build 5577)
so I specified a different one, hence the CXX=... you'll see in the
build log. This issue also led to me change cfganalyzer's and zchaff's
Makefiles, which used nonstandard variable names for the C++ compiler.
By the way, I'm sure my changes to lib/stp-jni/Makefile break things
for Linux builds, but I do think that some of the reorganization is
worthwhile to prevent duplicate work. (For example, the Makefile as it
was would recompile the Java source every time.)
Oh, my patch also includes some additions to expose an STP function
via the JNI.
If any my changes are helpful, please make use of them. But, more
directly for my benefit, if anyone has any advice on how to fix my
build problems, I'd really appreciate it.
Elnatan
Elnatan Reisner
> <builds.log><hampi.patch>
Playing around a bit more, I found that the main problem was that
Mac's require JNI files to be named with the suffix .jnilib, not .so .
After that, I had to deal with some 32-bit versus 64-bit problems, but
I eventually got Hampi running. (I'm running Leopard, which only has
64-bit Java, so I had to compile STP in 64-bit, which itself required
a small amount of tweaking.)
However, Hampi still isn't entirely working. 'make verify' now fails
with the message:
> BUILD SUCCESSFUL
> Total time: 36 seconds
> make -C lib teststp
> make -C stp-jni teststp
> java -Djava.library.path=mac -cp .:../junit.jar stp.examples.AllTests
> .Invalid memory access of location 0x6e rip=0x1165f03ea
>
> make[2]: *** [teststp] Segmentation fault
> make[1]: *** [teststp] Error 2
> make: *** [verify] Error 2
I ran all of the tests (that is, the .hmp files) in the tests/hampi/
tests/ directory and, of the 379 files there, 81 returned UNSAT while
the other 298 returned essentially the same 'Invalid memory access'
error as above, although with slightly different 'rip' values. Are
these 81 the only unsatisfiable tests, suggesting that the unsat
instances work fine but the satisfiable ones do not? Why might this be?
Elnatan
Elnatan Reisner
Continuing to push on this, I found that the segmentation fault
happened in src/hampi/stp/STPSolver.java, at a call to
VC.setFlags('a'), which turns off STP's optimizations. Just commenting
out this line got rid of the segmentation fault when running the tests
directly, although running 'make verify' still gives the same error.
I did have to make one other change, though: I guess STP's output
changed, because it now prints hex values starting with '0x' rather
than '0hex', so Hampi has to deal with this.
These two changes made all the tests in tests/hampi/tests/ run fine.
It looks like the 81 that returned UNSAT before were simplified away
before ever creating an STP VC; other unsat cases *did* require calls
to STP. (In total, I got that 135 tests were unsatisfiable and 244
were satisfiable; is that right?)
Elnatan
Devdatta Akhawe
usually needed for STP.
I suggest not turning on the optimization. STP sometimes doesn't print
out the answer with optimizations turned on (I am guessing its because
the constraint is so trivial that it goes away in the optimization
phase).
HTH
cheers
devdatta
On 28 December 2010 20:16, Elnatan Reisner <elnat...@gmail.com> wrote:
> On Dec 28, 2010, at 5:40 PM, Elnatan Reisner wrote:
>
>> On Dec 22, 2010, at 11:38 PM, Elnatan Reisner wrote:
>>
>>> It took me this long to look back and realize that I forgot the
>>> attachments. Here they are.
>>>
>>> Elnatan
>>>
>>> <builds.log><hampi.patch>
>>>
>>> On Dec 21, 2010, at 3:23 PM, Elnatan Reisner wrote:
>>>
>>>> I've been having trouble compiling Hampi, and I wonder if anyone can
>>>> help.
>>>>
>>>> I first tried to compile on a Mac, which I knew would require some work.
>>>> Eventually I got stuck, and I'll come back to that. In the meantime, though,
>>>> I tried to build on a Linux machine, where I expected things would just
>>>> work, but they didn't.
>>>>
>>>> First of all, the INSTALL.txt file says to run ./configure and make.
>>>> (The Makefile actually calls configure, so that's not necessary, but that's
>>>> a minor point.) But that's not all you have to do: You need to set 2 paths
>>>> in lib/cfganalyzer-2007-12-03/Makefile: one to your C++ compiler (although
>>>> 'g++' is probably right) and one to your OCaml library directory. You seem
>>>> *not* to have to set the path to libstp.a, despite what the Makefile says,
>>>> because it's location is fixed.
>>>>
>>>> Having set these paths, 'make' worked, but 'make verify' died with this
>>>> message:
>>>> .java: symbol lookup error:
>>>> /path/to/hampi-read-only/lib/stp-jni/64bit/libSTPJNI.so: undefined symbol:
>>>> _ZSt16__ostream_insertIcSt11char_traitsIcEERSt13basic_ostreamIT_T0_ES6_PKS3_l
>>>>
>>>> If anyone knows how to diagnose this, please let me know.
>>>>
>>>> Now, back to the Mac
>>>> I compiled STP myself and tweaked lib/stp-jni/Makefile as needed to make
>>>> 'make' work. However, I get a
>>>> java.lang.UnsatisfiedLinkError: no STPJNI in java.library.path
>>>> error when doing 'make verify' or when trying to run hampi.sh on one of
>>>> the test files. 'make verify' also gives me a bunch of
>>>> java.lang.NoClassDefFoundError: Could not initialize class stp.STPJNI
>>>> errors.
>>>>
>>>> I'm attaching my build log and a patch containing my changes to Hampi.
>>>> STP doesn't compile with my machine's default gcc:
>>>> elnatan$ gcc --version
>>>> i686-apple-darwin9-gcc-4.2.1 (GCC) 4.2.1 (Apple Inc. build 5577)
>>>> so I specified a different one, hence the CXX=... you'll see in the
>>>> build log. This issue also led to me change cfganalyzer's and zchaff's
>>>> Makefiles, which used nonstandard variable names for the C++ compiler.
Adam Kiezun
> out the answer with optimizations turned on (I am guessing its because
> the constraint is so trivial that it goes away in the optimization
> phase).
I concur. Hampi is actually slower with STP optimizations on. The
constraints generated by Hampi are fairly easy from the point of view
of the STP logic (only conjunctions and disjunctions, substring
extractions, equalities and disequalities), so they mostly map 1-1 to
a SAT formula and it's seems not worth spending time optimizing them.
Besides, Hampi spends most of its time in _creating_ the STP formula,
and not in solving it.
./adam
Adam Kiezun
> satisfiable ones do not? Why might this be?
the simplest error scenario leading to this behavior would be that
*all* instances return UNSAT.
./adam
Elnatan Reisner
> Continuing to push on this, I found that the segmentation fault
> happened in src/hampi/stp/STPSolver.java, at a call to
> VC.setFlags('a'), which turns off STP's optimizations. Just
> commenting out this line got rid of the segmentation fault when
> running the tests directly, although running 'make verify' still
> gives the same error.
On Dec 29, 2010, at 10:58 AM, Adam Kiezun wrote:
>> I suggest not turning on the optimization. STP sometimes doesn't
>> print
>> out the answer with optimizations turned on (I am guessing its
>> because
>> the constraint is so trivial that it goes away in the optimization
>> phase).
>
> I concur. Hampi is actually slower with STP optimizations on. The
> constraints generated by Hampi are fairly easy from the point of view
> of the STP logic (only conjunctions and disjunctions, substring
> extractions, equalities and disequalities), so they mostly map 1-1 to
> a SAT formula and it's seems not worth spending time optimizing them.
Maybe I didn't make myself clear. I got a segmentation fault when the
code tried to turn off optimizations. So, just to get Hampi to be able
to invoke STP, I *have* to leave optimizations on. I understand that
it might be less efficient, but I haven't run into STP not printing a
result as Devdatta thought might happen, and if my options are have a
working (but not blazing-fast) Hampi or a broken Hampi, I choose the
former.
If anyone else has had success using Hampi on a Mac and has surmounted
this problem, please let me know.
Elnatan
Elnatan Reisner
On Dec 28, 2010, at 11:16 PM, Elnatan Reisner wrote:
> These two changes made all the tests in tests/hampi/tests/ run fine.
> It looks like the 81 that returned UNSAT before were simplified away
> before ever creating an STP VC; other unsat cases *did* require
> calls to STP. (In total, I got that 135 tests were unsatisfiable and
> 244 were satisfiable; is that right?)
I'm not sure I entirely understand your response, but I think my later
email explained what happened: the 81 instances that returned UNSAT at
first (before I got Hampi working) were the ones that Hampi was able
to discover were UNSAT without ever invoking STP. There were a lot of
other tests that were also UNSAT, but Hampi needed to ask STP about
those in order to determine that; until I fixed the segmentation fault
problem, I only saw the answers from the ones that didn't require STP.
Also, apparently, none of the tests in tests/hampi/tests/ are found to
be satisfiable without consulting STP. (A brief perusal of Hampi's
code suggests to me that the only time Hampi would return SAT without
consulting STP is if the empty string is a valid solution, which I
guess never happens in those tests.)
Elnatan