-
Notifications
You must be signed in to change notification settings - Fork 10
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
VR: use fixed and refactored version #65
base: master
Are you sure you want to change the base?
Conversation
8498726
to
0246a28
Compare
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Remarks:
- Some files do not end with a newline.
- Format the changes files using the
clang-format
config file fromdg
.
tests/CMakeLists.txt
Outdated
../src/jsoncpp.cpp | ||
${CMAKE_SOURCE_DIR}/analyses/value_relations_plugin.cpp |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
../src/jsoncpp.cpp
-- What ifjsoncpp
installed by a package manager is used?${CMAKE_SOURCE_DIR}/analyses/value_relations_plugin.cpp
- Link with the corresponding plug-in so that the code that's actually going to be used by the instrumenter is tested.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I was not able to test the fix as the libjsoncpp-dev on Ubuntu 20.04 contains version 1.7.4, but at least 1.9.2 is required (or at least I hope I interpret the problem correctly).
As for linking ValueRelationsPlugin directly, when I tried the naive solution of dropping the value_relations_plugin.cpp and linking ValueRelationsPlugin as library instead, I got the following error:
CMake Error at tests/CMakeLists.txt:39 (target_link_libraries):
Target "ValueRelationsPlugin" of type MODULE_LIBRARY may not be linked into
another target. One may link only to INTERFACE, OBJECT, STATIC or SHARED
libraries, or to executables with the ENABLE_EXPORTS property set.
I do not feel like it's my call to change the ValueRelationsPlugin library's type and no attempt to set ENABLE_EXPORTS helped.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Yeah, sorry. I forgot that the plug-ins are not meant to be directly linked to other targets. You can re-use the libdl
-like machinery of Analyzer::analyse
(OT: This is a really deceitful name for a method that just loads and initializes a dynamic library on-demand...):
sbt-instrumentation/src/instr_analyzer.cpp
Lines 13 to 41 in ad75851
unique_ptr<InstrPlugin> Analyzer::analyze(const string &path, | |
llvm::Module* module) | |
{ | |
if (path.empty()) | |
return nullptr; | |
string err; | |
auto DL = llvm::sys::DynamicLibrary::getPermanentLibrary(path.c_str(), | |
&err); | |
if (!DL.isValid()) { | |
cerr << "Cannot open library: " << path << "\n"; | |
cerr << err << endl; | |
return nullptr; | |
} | |
InstrPlugin* (*create)(llvm::Module*); | |
void *symbol = DL.getAddressOfSymbol("create_object"); | |
if (!symbol) { | |
cerr << "Cannot load symbol 'create_object' from " << path << endl; | |
return nullptr; | |
} | |
create = reinterpret_cast<InstrPlugin *(*)(llvm::Module*)>(symbol); | |
unique_ptr<InstrPlugin> plugin(create(module)); | |
return plugin; | |
} |
tests/tests.cpp
Outdated
std::string targetFile = "tmp/" + benchmark + ".ll"; | ||
|
||
if (! fileExists(targetFile)) { | ||
std::string command = "clang-10 -S -emit-llvm " + path + "/" + benchmark + ".i -o " + targetFile; |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Clang version should be configured by the build system to use version compatible with LLVM that this project was compiled with.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Well, I solved this, but the solution feels pretty hacked.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I haven't went through the commits, but I have tested them repeatedly (and they ran in SV-COMP'22), so once all cosmetic issues are solved, I think they are good to be merged.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This is quite big PR. I will need some assistance to fully understand the changes.
Dismissing because I'm no longer associated with this project in any way for few last months..
Known issues:
.h
and.cpp
, I changed the way the resulting libraries are linked to the ValueRelationsPlugin and also to the new vr_tests; the way is probably not the desired one, since it requires the variable CMAKE_INSTALL_LIBDIR to be set with the path to the dg install directory (which probably misuses the CMake in several ways that I know little about)Related PR to dg:
mchalupa/dg#403