metaSMT build error on Mac OSX

[anithag]

After building dependencies, I proceeded to build metaSMT. (cd $metaSMT/build; make). This gives me the following error. How to fix this issue? My compiler specs are also given below.

Compiler Specs

/usr/bin/c++ -v
Apple LLVM version 6.0 (clang-600.0.57) (based on LLVM 3.5svn)
Target: x86_64-apple-darwin14.1.0
Thread model: posix

---

Error

/usr/bin/c++ -O3 -DNDEBUG -I/Users/anithagollamudi/cs260r/project/metaSMT/deps/boost-1_52_0/include -I/Users/anithagollamudi/cs260r/project/metaSMT/tests/../src -I/Users/anithagollamudi/cs260r/project/metaSMT/deps/SWORD-1.1/include -o CMakeFiles/direct_ExprSolver_SMT2.dir/direct_ExprSolver_SMT2.cpp.o -c /Users/anithagollamudi/cs260r/project/metaSMT/tests/direct_ExprSolver_SMT2.cpp
In file included from /Users/anithagollamudi/cs260r/project/metaSMT/tests/direct_ExprSolver_SMT2.cpp:17:
/Users/anithagollamudi/cs260r/project/metaSMT/tests/test_Array.cpp:163:42: warning: operator '<<' has lower precedence than '-'; '-' will be evaluated first
[-Wshift-op-parentheses]
unsigned const size = 1 << index_width - 1;
~~ ~~~~~~~~~~~~^~~
/Users/anithagollamudi/cs260r/project/metaSMT/tests/test_Array.cpp:163:42: note: place parentheses around the '-' expression to silence this warning
unsigned const size = 1 << index_width - 1;
^
( )
In file included from /Users/anithagollamudi/cs260r/project/metaSMT/tests/direct_ExprSolver_SMT2.cpp:18:
/Users/anithagollamudi/cs260r/project/metaSMT/tests/test_stack.cpp:15:26: error: redefinition of 'stack_t' as different kind of symbol
BOOST_FIXTURE_TEST_SUITE(stack_t, Solver_Fixture )
^
/Users/anithagollamudi/cs260r/project/metaSMT/deps/boost-1_52_0/include/boost/test/unit_test_suite.hpp:54:24: note: expanded from macro 'BOOST_FIXTURE_TEST_SUITE'
BOOST_AUTO_TEST_SUITE( suite_name )
^
/Users/anithagollamudi/cs260r/project/metaSMT/deps/boost-1_52_0/include/boost/test/unit_test_suite.hpp:45:11: note: expanded from macro '
BOOST_AUTO_TEST_SUITE'
namespace suite_name {
^
/usr/include/sys/_types/_sigaltstack.h:42:29: note: previous definition is here
typedef _STRUCT_SIGALTSTACK stack_t; /* [???] signal stack */
^
1 warning and 1 error generated.

[hriener]

Thank you for reporting this issue.

Looks like the name ''stack_t'' is already taken on MacOS. I cannot reproduce the error on my system, however, I guess it's enough to assign a different name to the test suite for metaSMT's stack API, e.g., ''stack_test''.

As a quick fix, please edit file /Users/anithagollamudi/cs260r/project/metaSMT/tests/test_stack.cpp and change in line 15 ''stack_t'' to ''stack_test'' and re-build with make.

Further, notice that building metaSMT's test suites is optional. (Disabling the test suites saves you a lot of time when building metaSMT.)

[anithag]

Thanks. I renamed it and the build progressed. I have two questions at this point.

(1) I am getting error linking direct_ExprSolver_SMT2. I could build boost-1.52 successfully though. I am confused as I am using same toolchain for building metaSMT and boost-1.52.0 (For boost-1.52.0 I changed script shared.sh to use toolset=darwin to get build through). I am confused. All boost libraries are present and seem to be correctly installed. Any idea why?

---

/usr/bin/c++ -O3 -DNDEBUG -Wl,-search_paths_first -Wl,-headerpad_max_install_names CMakeFiles/direct_ExprSolver_SMT2.dir/direct_ExprSolver_SMT2.cpp.o -o direct_ExprSolver_SMT2 libboost_test.a ../src/lib/libmetaSMT.a ../src/lib/libmetaSMT.a ../../deps/boost-1_52_0/lib/libboost_iostreams.dylib ../../deps/boost-1_52_0/lib/libboost_thread.dylib ../../deps/boost-1_52_0/lib/libboost_system.dylib

[ 20%] Built target metaSMT
[ 26%] Built target boost_test
Linking CXX executable direct_ExprSolver_SMT2
Undefined symbols for architecture x86_64:
"boost::iostreams::file_descriptor::seek(long, std::_Ios_Seekdir)", referenced from:
boost::iostreams::detail::indirect_streambuf<boost::iostreams::file_descriptor_source, std::char_traits, std::allocator, boost::iostreams::input_seekable>::seekpos(std::fpos<__mbstate_t>, std::_Ios_Openmode) in direct_ExprSolver_SMT2.cpp.o
...
ld: symbol(s) not found for architecture x86_64
clang: error: linker command failed with exit code 1 (use -v to see invocation)
make[2]: *** [tests/direct_ExprSolver_SMT2] Error 1
make[1]: *** [tests/CMakeFiles/direct_ExprSolver_SMT2.dir/all] Error 2

---

(2) How do I disable tests?

[hriener]

(1) I'm only guessing: maybe you mixed up architectures --- a part is compiled for 32bit and another part for 64bit. Then, you will not be able to link them together.

On Linux I can check the architecture of a library, e.g., by utilizing ''file''.
$ file boost-1_52_0/lib/libboost_iostreams.so.1.52.0
boost-1_52_0/lib/libboost_iostreams.so.1.52.0: ELF 64-bit LSB shared object, x86-64, [...]

(2) For instance, you could use the tool ''ccmake''. (Note that you may have to install additional packages on your system.) Enter the build directory and type ''ccmake .''. You will see a dialog menu in which you can customize the build, e.g., to set the variable ''metaSMT_ENABLE_TESTS'' to ''OFF''. Then type ''c'' (configure), followed by ''g'' (generate) and re-build with ''make''. You may want to search the web for details on ''ccmake''. Notice also that there is the option ''t'' (toggle advance mode). In advanced mode, you will have the ability to control/change also Boost-related variables and paths, e.g., ''Boost_IOSTREAMS_LIBRARY_RELEASE'' (which could be interesting for the first issue).

[anithag]

I think I figured the reason. I need to configure -stdlib=libstdc++ in LDFLAGS and/or CXXFLAGS to build metaSMT. How do I configure this in bootstrap.sh?

[anithag]

I just manually edited link.txt files in build directories. So the above error got fixed. However python bindings gave a new error:

/Users/anithagollamudi/cs260r/project/metaSMT/bindings/python/../../src/metaSMT/backend/../support/GoTmp.hpp:11:16: error: use of undeclared identifier 'get_current_dir_name'
: prevPath(get_current_dir_name())

I am wondering if building python bindings can be suppressed. I tried to find the option in 'ccmake .' I did not find it though.

[finnhaedicke]

Hi @anithag

you can disable the python bindings by setting metaSMT_ENABLE_BINDINGS, in ccmake or

cd build 
cmake -DmetaSMT_ENABLE_BINDINGS=off

Other parts of metaSMT also use it so I rewrote it to work on OS X. Would you mind to try the changes from my personal repository:

git remote add finnhaedicke https://github.com/finnhaedicke/metaSMT.git
git fetch finnhaedicke
git checkout osx-support

(does anybody know an easier way?)

Furthermore I noticed SWORD appeared in one of your error messages. Sadly SWORD is only available as a linux binary. So I disabled it for OS X. So was the Z3 version we used. In the support-osx version I switched to the git version of Z3. Please pull your dependencies repository to get the current version of Z3 from https://github.com/Z3Prover/z3

If you want to set the compiler and linker flags you can use CMAKE_CXX_FLAGS, CMAKE_EXE_LINKER_FLAGS and CMAKE_SHARED_LINKER_FLAGS. However in metaSMT we do not use SHARED. As @hriener said, your can set them in the ccmake advanced mode (t).
I am not sure why you need -stdlib=libstdc++ I assumed when you compile everything from source (exclduing SWORD and using the new Z3), then libc++ should work. However, like @hriener I do not have a machine with OS X to test it myself.

Thanks for trying metaSMT on OS X and reporting the issues.

[anithag]

I could finally get Z3-4.3.1 built and installed on Mac OSX. I have not tried other solvers. Main changes for Mac OSX are:

1. Changes to all 'sed -i' commands. On Mac 'sed -i' requires additional operand. I just set it to null though.
2. For tests to work, need to modify test_stack.cpp to use a different stack_t (#comment 1)
3. Turn off python bindings as get_current_dir() is not supported
4. To build boost, "toolset=darwin" in dependencies/boost-1_46_0/shared.sh
5. Change extension to dynamic libraries. On Mac, they come with extension .dylib. For example, set(Z3_LIBRARIES ${Z3_DIR}/lib/libz3.so ) should be set(Z3_LIBRARIES ${Z3_DIR}/lib/libz3.dylib )
6. Though Z3 installation is working for me when I tried manually, for some reason bootstrap.sh says "Disabling Z3. A version of Z3 >= 4.0 is required."
7. No SWORD sources to get it built on Mac OS.

---

Now, the other issue I faced was linking libstdc++. I am not sure why the build passes when all libraries are linked with libstdc++. This must be due to my setup. I'll debug on this more when I have time.

@finnhaedicke I tried building your repo. Boost build failed. I checked the scripts. As I mentioned in my points above, toolset needs to be darwin. I have not thoroughly debugged the failures.
Inittially, it took me lot of time to understand the scripts in dependencies. Am new to cmake ( I am home with autoconf stuff). So tweaking things took me a while. Many thanks for the prompt support. I am now reasonably comfortable with the repo.

I am hoping to fork a branch with all my mac specific changes soon.

EDIT: I am trying this for one of my course projects. The plan is to make KLEE use Z3 for testing string operations (eventually target SQL injections). If you have any suggestions on better string solvers, please let me know. I'll be happy to explore.

[finnhaedicke]

For the .so/.dynlyb you can use the cmake variable CMAKE_SHARED_LINKER_SUFFIX, which resolves to .so on linux.

As for your edit: As I understand, you plan to use string theory. I am sorry to say, metaSMT only supports Core, BitVector and Array theory.
I have not worked with string theory, so I do not know which solvers support it (well).

[anithag]

@finnhaedicke

I am sorry to say, metaSMT only supports Core, BitVector and Array theory.

:-(

I have not worked with string theory, so I do not know which solvers support it (well).

There is Z3-str which I am hoping to use in place of Z3. https://github.com/z3str/Z3-str
How hard is it to get started with support for basic string theory?

[finnhaedicke]

To implement a new language several steps are required:

1. Define tags for the variables, constants and operations in the theory, see tags directory.
2. Define the input language for the theory. See frontend directory. This is based in boost.proto and rather obscure at times.
3. Write Tests for the logic. Using each of the defined operations. Usually a set of simple satisfiable or unsatisfiable assertion.
4. Implement support for the new theory in one vor more backends.

I have found that CVC4 has documentation for their implementation. http://cvc4.cs.nyu.edu/wiki/Strings

Sorry for any typos, written on Android with auto-correction.

[anithag]

@finnhaedicke

Regarding string theory support,

Do we also need to change DirectSolver_Context.hpp to handle string tags? (I have not yet debugged its detailed purpose other than as a framework for underlying solvers)

[finnhaedicke]

Essentially, DirectSolver is only a framework component, but also does some pre-processing before the expressions are passed to the backend. It contains a cache of already evaluated variable 1, does the variable lookup for read_value 2 and does packaging of parameters for constants and operations that require special handling 3, 4.

We introduced DirectSolver as a customization point for intermediate representations. DirectSolver has none, but GraphSolver has an intermediate representation to identify identical sub-expressions.