Open anithag opened 9 years ago
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.)
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
(2) How do I disable tests?
(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).
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?
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.
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.
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:
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.
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).
@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?
To implement a new language several steps are required:
tags
directory.frontend
directory. This is based in boost.proto and rather obscure at times.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.
@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)
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.
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.