RafaelTupynamba / GuidedSampler

GuidedSampler: Coverage-guided Sampling of SMT Solutions
BSD 3-Clause "New" or "Revised" License
12 stars 2 forks source link

Error trying to make GuidedSampler #2

Open EZL1190 opened 2 years ago

EZL1190 commented 2 years ago

Hello

I'm following the Readme guide, and when i'm running "make" in GuidedSampler it's exiting with error 1.

─$ make
g++ -g -O3 -o guidedsampler guidedsampler.cpp -lz3
/usr/bin/ld: /tmp/ccOBzSlY.o: warning: relocation against `coverage_all_bv' in read-only section `.text._ZN13GuidedSampler11print_statsEv[_ZN13GuidedSampler11print_statsEv]'
/usr/bin/ld: /tmp/ccOBzSlY.o: in function `GuidedSampler::print_stats()':
/home/kali/Desktop/stuff/guided_sampler/GuidedSampler/guidedsampler.cpp:297: undefined reference to `coverage_bool'
/usr/bin/ld: /home/kali/Desktop/stuff/guided_sampler/GuidedSampler/guidedsampler.cpp:297: undefined reference to `coverage_all_bool'
/usr/bin/ld: /home/kali/Desktop/stuff/guided_sampler/GuidedSampler/guidedsampler.cpp:297: undefined reference to `coverage_all_bool'
/usr/bin/ld: /home/kali/Desktop/stuff/guided_sampler/GuidedSampler/guidedsampler.cpp:297: undefined reference to `coverage_bv'
/usr/bin/ld: /home/kali/Desktop/stuff/guided_sampler/GuidedSampler/guidedsampler.cpp:297: undefined reference to `coverage_all_bv'
/usr/bin/ld: /home/kali/Desktop/stuff/guided_sampler/GuidedSampler/guidedsampler.cpp:297: undefined reference to `coverage_all_bv'
/usr/bin/ld: /tmp/ccOBzSlY.o: in function `GuidedSampler::value(char const*, z3::sort)':
/home/kali/Desktop/stuff/guided_sampler/GuidedSampler/guidedsampler.cpp:638: undefined reference to `parse_bv(char const*, _Z3_sort*, _Z3_context*)'
/usr/bin/ld: /home/kali/Desktop/stuff/guided_sampler/GuidedSampler/guidedsampler.cpp:638: undefined reference to `parse_bv(char const*, _Z3_sort*, _Z3_context*)'
/usr/bin/ld: /home/kali/Desktop/stuff/guided_sampler/GuidedSampler/guidedsampler.cpp:638: undefined reference to `parse_bv(char const*, _Z3_sort*, _Z3_context*)'
/usr/bin/ld: /home/kali/Desktop/stuff/guided_sampler/GuidedSampler/guidedsampler.cpp:638: undefined reference to `parse_bv(char const*, _Z3_sort*, _Z3_context*)'
/usr/bin/ld: /home/kali/Desktop/stuff/guided_sampler/GuidedSampler/guidedsampler.cpp:638: undefined reference to `parse_bv(char const*, _Z3_sort*, _Z3_context*)'
/usr/bin/ld: /tmp/ccOBzSlY.o: in function `GuidedSampler::model_string[abi:cxx11](z3::model, std::vector<z3::func_decl, std::allocator<z3::func_decl> >)':
/home/kali/Desktop/stuff/guided_sampler/GuidedSampler/guidedsampler.cpp:1260: undefined reference to `bv_string[abi:cxx11](_Z3_ast*, _Z3_context*)'
/usr/bin/ld: /home/kali/Desktop/stuff/guided_sampler/GuidedSampler/guidedsampler.cpp:1263: undefined reference to `bv_string[abi:cxx11](_Z3_ast*, _Z3_context*)'
/usr/bin/ld: /home/kali/Desktop/stuff/guided_sampler/GuidedSampler/guidedsampler.cpp:1264: undefined reference to `bv_string[abi:cxx11](_Z3_ast*, _Z3_context*)'
/usr/bin/ld: /home/kali/Desktop/stuff/guided_sampler/GuidedSampler/guidedsampler.cpp:1302: undefined reference to `bv_string[abi:cxx11](_Z3_ast*, _Z3_context*)'
/usr/bin/ld: /home/kali/Desktop/stuff/guided_sampler/GuidedSampler/guidedsampler.cpp:1324: undefined reference to `bv_string[abi:cxx11](_Z3_ast*, _Z3_context*)'
/usr/bin/ld: /tmp/ccOBzSlY.o:/home/kali/Desktop/stuff/guided_sampler/GuidedSampler/guidedsampler.cpp:1328: more undefined references to `bv_string[abi:cxx11](_Z3_ast*, _Z3_context*)' follow
/usr/bin/ld: /tmp/ccOBzSlY.o: in function `GuidedSampler::GuidedSampler(std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >, int, double, int, bool, bool, bool, bool)':
/home/kali/Desktop/stuff/guided_sampler/GuidedSampler/guidedsampler.cpp:152: undefined reference to `get_coverage_vector'
/usr/bin/ld: /tmp/ccOBzSlY.o: in function `__gnu_cxx::__normal_iterator<coverage_count_struct*, std::vector<coverage_count_struct, std::allocator<coverage_count_struct> > >::__normal_iterator(coverage_count_struct* const&)':
/usr/include/c++/12/bits/stl_iterator.h:1073: undefined reference to `coverage_vector'
/usr/bin/ld: /tmp/ccOBzSlY.o: in function `GuidedSampler::finish()':
/home/kali/Desktop/stuff/guided_sampler/GuidedSampler/guidedsampler.cpp:1176: undefined reference to `coverage_vector'
/usr/bin/ld: /tmp/ccOBzSlY.o: in function `std::_Hashtable<std::pair<int, int>, std::pair<int, int>, std::allocator<std::pair<int, int> >, std::__detail::_Identity, std::equal_to<std::pair<int, int> >, pair_hash, std::__detail::_Mod_range_hashing, std::__detail::_Default_ranged_hash, std::__detail::_Prime_rehash_policy, std::__detail::_Hashtable_traits<true, true, true> >::_Hashtable()':
/usr/include/c++/12/bits/hashtable.h:531: undefined reference to `covered'
/usr/bin/ld: /tmp/ccOBzSlY.o: in function `std::_Hashtable<_Z3_ast*, std::pair<_Z3_ast* const, coverage_struct>, std::allocator<std::pair<_Z3_ast* const, coverage_struct> >, std::__detail::_Select1st, std::equal_to<_Z3_ast*>, std::hash<_Z3_ast*>, std::__detail::_Mod_range_hashing, std::__detail::_Default_ranged_hash, std::__detail::_Prime_rehash_policy, std::__detail::_Hashtable_traits<false, false, true> >::_M_bucket_index(unsigned long) const':
/usr/include/c++/12/bits/hashtable.h:798: undefined reference to `covered'
/usr/bin/ld: /tmp/ccOBzSlY.o: in function `std::vector<coverage_count_struct, std::allocator<coverage_count_struct> >::operator[](unsigned long)':
/usr/include/c++/12/bits/stl_vector.h:1124: undefined reference to `coverage_vector'
/usr/bin/ld: /tmp/ccOBzSlY.o: in function `GuidedSampler::evaluate(z3::model, z3::expr, bool, int)':
/home/kali/Desktop/stuff/guided_sampler/GuidedSampler/guidedsampler.cpp:574: undefined reference to `coverage_enable'
/usr/bin/ld: /home/kali/Desktop/stuff/guided_sampler/GuidedSampler/guidedsampler.cpp:576: undefined reference to `coverage_enable'
/usr/bin/ld: /home/kali/Desktop/stuff/guided_sampler/GuidedSampler/guidedsampler.cpp:574: undefined reference to `coverage_enable'
/usr/bin/ld: /home/kali/Desktop/stuff/guided_sampler/GuidedSampler/guidedsampler.cpp:576: undefined reference to `coverage_enable'
/usr/bin/ld: /tmp/ccOBzSlY.o: in function `z3::apply_result::convert_model(z3::model const&, unsigned int) const':
/usr/include/z3++.h:2100: undefined reference to `Z3_apply_result_convert_model'
/usr/bin/ld: /tmp/ccOBzSlY.o: in function `GuidedSampler::value(char const*, z3::sort)':
/home/kali/Desktop/stuff/guided_sampler/GuidedSampler/guidedsampler.cpp:638: undefined reference to `parse_bv(char const*, _Z3_sort*, _Z3_context*)'
/usr/bin/ld: /home/kali/Desktop/stuff/guided_sampler/GuidedSampler/guidedsampler.cpp:638: undefined reference to `parse_bv(char const*, _Z3_sort*, _Z3_context*)'
/usr/bin/ld: /home/kali/Desktop/stuff/guided_sampler/GuidedSampler/guidedsampler.cpp:638: undefined reference to `parse_bv(char const*, _Z3_sort*, _Z3_context*)'
/usr/bin/ld: /home/kali/Desktop/stuff/guided_sampler/GuidedSampler/guidedsampler.cpp:638: undefined reference to `parse_bv(char const*, _Z3_sort*, _Z3_context*)'
/usr/bin/ld: /tmp/ccOBzSlY.o: in function `std::vector<coverage_count_struct, std::allocator<coverage_count_struct> >::size() const':
/usr/include/c++/12/bits/stl_vector.h:988: undefined reference to `coverage_vector'
/usr/bin/ld: /usr/include/c++/12/bits/stl_vector.h:988: undefined reference to `coverage_vector'
/usr/bin/ld: /tmp/ccOBzSlY.o: in function `std::vector<coverage_count_struct, std::allocator<coverage_count_struct> >::push_back(coverage_count_struct const&)':
/usr/include/c++/12/bits/stl_vector.h:1278: undefined reference to `coverage_vector'
/usr/bin/ld: /usr/include/c++/12/bits/stl_vector.h:1283: undefined reference to `coverage_vector'
/usr/bin/ld: /tmp/ccOBzSlY.o: in function `std::pair<std::__detail::_Node_iterator<std::pair<_Z3_ast* const, coverage_struct>, false, false>, bool> std::_Hashtable<_Z3_ast*, std::pair<_Z3_ast* const, coverage_struct>, std::allocator<std::pair<_Z3_ast* const, coverage_struct> >, std::__detail::_Select1st, std::equal_to<_Z3_ast*>, std::hash<_Z3_ast*>, std::__detail::_Mod_range_hashing, std::__detail::_Default_ranged_hash, std::__detail::_Prime_rehash_policy, std::__detail::_Hashtable_traits<false, false, true> >::emplace<z3::expr&, coverage_struct&>(z3::expr&, coverage_struct&)':
/usr/include/c++/12/bits/hashtable.h:950: undefined reference to `covered'
/usr/bin/ld: /tmp/ccOBzSlY.o: in function `std::vector<coverage_count_struct, std::allocator<coverage_count_struct> >::push_back(coverage_count_struct const&)':
/usr/include/c++/12/bits/stl_vector.h:1287: undefined reference to `coverage_vector'
/usr/bin/ld: /tmp/ccOBzSlY.o: in function `std::vector<coverage_count_struct, std::allocator<coverage_count_struct> >::size() const':
/usr/include/c++/12/bits/stl_vector.h:988: undefined reference to `coverage_vector'
/usr/bin/ld: /usr/include/c++/12/bits/stl_vector.h:988: undefined reference to `coverage_vector'
/usr/bin/ld: /tmp/ccOBzSlY.o: in function `std::vector<coverage_count_struct, std::allocator<coverage_count_struct> >::push_back(coverage_count_struct const&)':
/usr/include/c++/12/bits/stl_vector.h:1278: undefined reference to `coverage_vector'
/usr/bin/ld: /usr/include/c++/12/bits/stl_vector.h:1283: undefined reference to `coverage_vector'
/usr/bin/ld: /tmp/ccOBzSlY.o: in function `std::pair<std::__detail::_Node_iterator<std::pair<_Z3_ast* const, coverage_struct>, false, false>, bool> std::_Hashtable<_Z3_ast*, std::pair<_Z3_ast* const, coverage_struct>, std::allocator<std::pair<_Z3_ast* const, coverage_struct> >, std::__detail::_Select1st, std::equal_to<_Z3_ast*>, std::hash<_Z3_ast*>, std::__detail::_Mod_range_hashing, std::__detail::_Default_ranged_hash, std::__detail::_Prime_rehash_policy, std::__detail::_Hashtable_traits<false, false, true> >::emplace<z3::expr&, coverage_struct&>(z3::expr&, coverage_struct&)':
/usr/include/c++/12/bits/hashtable.h:950: undefined reference to `covered'
/usr/bin/ld: /tmp/ccOBzSlY.o: in function `std::vector<coverage_count_struct, std::allocator<coverage_count_struct> >::size() const':
/usr/include/c++/12/bits/stl_vector.h:988: undefined reference to `coverage_vector'
/usr/bin/ld: /usr/include/c++/12/bits/stl_vector.h:988: undefined reference to `coverage_vector'
/usr/bin/ld: /tmp/ccOBzSlY.o: in function `std::vector<coverage_count_struct, std::allocator<coverage_count_struct> >::push_back(coverage_count_struct const&)':
/usr/include/c++/12/bits/stl_vector.h:1278: undefined reference to `coverage_vector'
/usr/bin/ld: /usr/include/c++/12/bits/stl_vector.h:1283: undefined reference to `coverage_vector'
/usr/bin/ld: /tmp/ccOBzSlY.o: in function `std::pair<std::__detail::_Node_iterator<std::pair<_Z3_ast* const, coverage_struct>, false, false>, bool> std::_Hashtable<_Z3_ast*, std::pair<_Z3_ast* const, coverage_struct>, std::allocator<std::pair<_Z3_ast* const, coverage_struct> >, std::__detail::_Select1st, std::equal_to<_Z3_ast*>, std::hash<_Z3_ast*>, std::__detail::_Mod_range_hashing, std::__detail::_Default_ranged_hash, std::__detail::_Prime_rehash_policy, std::__detail::_Hashtable_traits<false, false, true> >::emplace<z3::expr&, coverage_struct&>(z3::expr&, coverage_struct&)':
/usr/include/c++/12/bits/hashtable.h:950: undefined reference to `covered'
/usr/bin/ld: /tmp/ccOBzSlY.o: in function `std::vector<coverage_count_struct, std::allocator<coverage_count_struct> >::size() const':
/usr/include/c++/12/bits/stl_vector.h:988: undefined reference to `coverage_vector'
/usr/bin/ld: /usr/include/c++/12/bits/stl_vector.h:988: undefined reference to `coverage_vector'
/usr/bin/ld: /tmp/ccOBzSlY.o: in function `std::vector<coverage_count_struct, std::allocator<coverage_count_struct> >::push_back(coverage_count_struct const&)':
/usr/include/c++/12/bits/stl_vector.h:1278: undefined reference to `coverage_vector'
/usr/bin/ld: /usr/include/c++/12/bits/stl_vector.h:1283: undefined reference to `coverage_vector'
/usr/bin/ld: /tmp/ccOBzSlY.o: in function `std::pair<std::__detail::_Node_iterator<std::pair<_Z3_ast* const, coverage_struct>, false, false>, bool> std::_Hashtable<_Z3_ast*, std::pair<_Z3_ast* const, coverage_struct>, std::allocator<std::pair<_Z3_ast* const, coverage_struct> >, std::__detail::_Select1st, std::equal_to<_Z3_ast*>, std::hash<_Z3_ast*>, std::__detail::_Mod_range_hashing, std::__detail::_Default_ranged_hash, std::__detail::_Prime_rehash_policy, std::__detail::_Hashtable_traits<false, false, true> >::emplace<z3::expr&, coverage_struct&>(z3::expr&, coverage_struct&)':
/usr/include/c++/12/bits/hashtable.h:950: undefined reference to `covered'
/usr/bin/ld: /tmp/ccOBzSlY.o: in function `std::vector<coverage_count_struct, std::allocator<coverage_count_struct> >::push_back(coverage_count_struct const&)':
/usr/include/c++/12/bits/stl_vector.h:1287: undefined reference to `coverage_vector'
/usr/bin/ld: /usr/include/c++/12/bits/stl_vector.h:1287: undefined reference to `coverage_vector'
/usr/bin/ld: /usr/include/c++/12/bits/stl_vector.h:1287: undefined reference to `coverage_vector'
/usr/bin/ld: /tmp/ccOBzSlY.o: in function `GuidedSampler::evaluate(z3::model, z3::expr, bool, int)':
/home/kali/Desktop/stuff/guided_sampler/GuidedSampler/guidedsampler.cpp:574: undefined reference to `coverage_enable'
/usr/bin/ld: /home/kali/Desktop/stuff/guided_sampler/GuidedSampler/guidedsampler.cpp:576: undefined reference to `coverage_enable'
/usr/bin/ld: /tmp/ccOBzSlY.o: in function `z3::context::check_parser_error() const':
/usr/include/z3++.h:180: undefined reference to `Z3_get_parser_error'
/usr/bin/ld: /tmp/ccOBzSlY.o: in function `z3::apply_result::convert_model(z3::model const&, unsigned int) const':
/usr/include/z3++.h:2100: undefined reference to `Z3_apply_result_convert_model'
/usr/bin/ld: /tmp/ccOBzSlY.o: in function `GuidedSampler::evaluate(z3::model, z3::expr, bool, int)':
/home/kali/Desktop/stuff/guided_sampler/GuidedSampler/guidedsampler.cpp:574: undefined reference to `coverage_enable'
/usr/bin/ld: /home/kali/Desktop/stuff/guided_sampler/GuidedSampler/guidedsampler.cpp:576: undefined reference to `coverage_enable'
/usr/bin/ld: /tmp/ccOBzSlY.o: in function `z3::context::check_parser_error() const':
/usr/include/z3++.h:180: undefined reference to `Z3_get_parser_error'
/usr/bin/ld: /tmp/ccOBzSlY.o: in function `GuidedSampler::run()':
/home/kali/Desktop/stuff/guided_sampler/GuidedSampler/guidedsampler.cpp:244: undefined reference to `parse_bv(char const*, _Z3_sort*, _Z3_context*)'
/usr/bin/ld: warning: creating DT_TEXTREL in a PIE
collect2: error: ld returned 1 exit status
make: *** [Makefile:2: all] Error 1
lahiri-phdworks commented 1 year ago

Specify the path explicitly. g++ -g -O3 guidedsampler.cpp -Wall -Wpedantic -o guidedsampler -L../z3/build -lz3 to the z3 build dir and also export it like wise export LD_LIBRARY_PATH=$HOME/SMTSampler_code/z3/build/:$LD_LIBRARY_PATH