Skip to content
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.

Sign up for GitHub

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

Plugin Support #59

Closed
wants to merge 6 commits into from
Closed

Plugin Support #59

Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
3a05f1a
fix: leanc: use cc when compiling a .c file
Kha Nov 7, 2019
47c8184
chore: remove outdated macOS cmake setup
Kha Nov 7, 2019
7e95669
feat: add --plugin for loading shared libraries
Kha Nov 9, 2019
6641d10
feat: simplistic linter framework
Kha Nov 9, 2019
083fb9a
feat: call linters on non-mutual definitions
Kha Nov 9, 2019
0865fd2
test: trivial linter test
Kha Nov 6, 2019
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
9 changes: 5 additions & 4 deletions bin/leanc.in
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,10 +16,13 @@ bindir=$(dirname $0)
# Final linking still has to be done by a C++ compiler because we need to link against the
# Lean runtime written in C++ (https://isocpp.org/wiki/faq/mixing-c-and-cpp#overview-mixing-langs).
use_c=maybe
# NOTE: leanstatic and leanstdlib are cyclically dependent
linker_flags="-lleanstatic -lleanstdlib -lleanstatic -lleanstdlib"
for arg in "$@"; do
[[ $use_c == maybe && $arg == "-c" ]] && use_c=yes
[[ $arg == *.c ]] && use_c=yes
[[ $arg == *.cpp ]] && use_c=no
[[ $arg == "-shared" ]] && linker_flags="@LEANC_SHARED_LINKER_FLAGS@"
done

if [[ $use_c == yes ]]; then
Expand All @@ -31,8 +34,7 @@ if [[ $use_c == yes ]]; then
done
[ -f $LEAN_CC ] || command -v $LEAN_CC || error "no suitable C compiler found!"

# NOTE: leanstatic and leanstdlib are cyclically dependent
$LEAN_CC -D LEAN_MULTI_THREAD "-I$bindir/../src" "-I$bindir/../include" "$@" "-L$bindir" "-L$bindir/../lib" -lleanstatic -lleanstdlib -lleanstatic -lleanstdlib -lgmp @LEANC_EXTRA_FLAGS@ -Wno-unused-command-line-argument
$LEAN_CC -D LEAN_MULTI_THREAD "-I$bindir/../src" "-I$bindir/../include" "$@" "-L$bindir" "-L$bindir/../lib" $linker_flags -lgmp @LEANC_EXTRA_FLAGS@ -Wno-unused-command-line-argument
else
# Check C++ compiler
for cxx in $LEAN_CXX @CMAKE_CXX_COMPILER@ /usr/bin/g++; do
Expand All @@ -42,6 +44,5 @@ else
done
[ -f $LEAN_CXX ] || command -v $LEAN_CXX || error "no suitable C++ compiler found!"

# NOTE: leanstatic and leanstdlib are cyclically dependent
$LEAN_CXX -std=c++14 -D LEAN_MULTI_THREAD "-I$bindir/../src" "-I$bindir/../include" "$@" "-L$bindir" "-L$bindir/../lib" -lleanstatic -lleanstdlib -lleanstatic -lleanstdlib -lgmp @LEANC_EXTRA_FLAGS@ -Wno-unused-command-line-argument
$LEAN_CXX -std=c++14 -D LEAN_MULTI_THREAD "-I$bindir/../src" "-I$bindir/../include" "$@" "-L$bindir" "-L$bindir/../lib" $linker_flags -lgmp @LEANC_EXTRA_FLAGS@ -Wno-unused-command-line-argument
fi
16 changes: 13 additions & 3 deletions src/CMakeLists.txt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -427,18 +427,28 @@ include_directories(${LEAN_SOURCE_DIR})
# export all symbols for the interpreter
if(${CMAKE_SYSTEM_NAME} MATCHES "Windows")
set(CMAKE_EXE_LINKER_FLAGS "${CMAKE_EXE_LINKER_FLAGS} ${LEAN_EXTRA_LINKER_FLAGS} -Wl,--export-all")
set(CMAKE_SHARED_LINKER_FLAGS "${CMAKE_SHARED_LINKER_FLAGS} -Wl,--export-all")
set(LEANC_SHARED_LINKER_FLAGS "${LEANC_SHARED_LINKER_FLAGS} -Wl,--export-all")
else()
set(CMAKE_EXE_LINKER_FLAGS "${CMAKE_EXE_LINKER_FLAGS} ${LEAN_EXTRA_LINKER_FLAGS} -rdynamic")
set(LEANC_EXTRA_FLAGS "${LEANC_EXTRA_FLAGS} -ldl")
endif()

# Allow `lean` symbols in plugins without linking directly against it. If we linked against the
# executable or `leanshared`, plugins would try to look them up at load time (even though they
# are already loaded) and probably fail unless we set up LD_LIBRARY_PATH.
if(${CMAKE_SYSTEM_NAME} MATCHES "Windows")
# import library created by the `lean` target (and copied by `bin_lean`)
set(LEANC_SHARED_LINKER_FLAGS "$bindir/liblean.dll.a")
elseif("${CMAKE_SYSTEM_NAME}" MATCHES "Darwin")
set(LEANC_SHARED_LINKER_FLAGS "${LEANC_EXTRA_FLAGS} -Wl,-undefined,dynamic_lookup")
endif()
# Linux ignores undefined symbols in shared libraries by default

if(MULTI_THREAD AND NOT MSVC AND (NOT ("${CMAKE_SYSTEM_NAME}" MATCHES "Darwin")))
set(CMAKE_EXE_LINKER_FLAGS "${CMAKE_EXE_LINKER_FLAGS} -pthread")
endif()
set(CMAKE_EXE_LINKER_FLAGS_TESTCOV "${CMAKE_EXE_LINKER_FLAGS} -fprofile-arcs -ftest-coverage")
if ((${CYGWIN} EQUAL "1") OR (${CMAKE_SYSTEM_NAME} MATCHES "Windows"))
set(CMAKE_SHARED_LINKER_FLAGS "${CMAKE_SHARED_LINKER_FLAGS} -Wl,--export-all")
endif()

# Git HASH
set(LEAN_PACKAGE_VERSION "NOT-FOUND")
Expand Down
8 changes: 7 additions & 1 deletion src/shell/CMakeLists.txt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -33,6 +33,12 @@ add_custom_target(update-stage0

add_executable(lean lean.cpp)
target_link_libraries(lean leanstatic)
# create import library on Windows to link plugins against
set_target_properties(lean PROPERTIES ENABLE_EXPORTS ON)
if(${CMAKE_SYSTEM_NAME} MATCHES "Windows")
# https://github.com/msys2/MINGW-packages/issues/5952
target_link_options(lean PRIVATE "-Wl,--out-implib,$<TARGET_LINKER_FILE:lean>")
endif()
install(TARGETS lean DESTINATION bin)

if(${EMSCRIPTEN})
Expand Down Expand Up @@ -76,7 +82,7 @@ else()
)
else()
ADD_CUSTOM_TARGET(bin_lean ALL
COMMAND "${CMAKE_COMMAND}" -E copy_if_different "$<TARGET_FILE:lean>" "${LEAN_SOURCE_DIR}/../bin/"
COMMAND "${CMAKE_COMMAND}" -E copy_if_different "$<TARGET_FILE:lean>" "$<TARGET_LINKER_FILE:lean>" "${LEAN_SOURCE_DIR}/../bin/"
DEPENDS bin_lean_stage0 lean
)
endif()
Expand Down
44 changes: 43 additions & 1 deletion src/shell/lean.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -56,6 +56,13 @@ Author: Leonardo de Moura
#endif
#include "githash.h" // NOLINT

#ifdef LEAN_WINDOWS
#include <windows.h>
#undef ERROR // thanks, wingdi.h
#else
#include <dlfcn.h>
#endif

#if defined(LEAN_LLVM)
#include <llvm/Support/TargetSelect.h>
#endif
Expand Down Expand Up @@ -201,6 +208,7 @@ static void display_help(std::ostream & out) {
std::cout << " --threads=num -j number of threads used to process lean files\n";
std::cout << " --tstack=num -s thread stack size in Kb\n";
#endif
std::cout << " --plugin=file load and initialize shared library for registering linters etc.";
std::cout << " --deps just print dependencies of a Lean input\n";
#if defined(LEAN_JSON)
std::cout << " --json print JSON-formatted structured error messages\n";
Expand Down Expand Up @@ -241,14 +249,15 @@ static struct option g_long_options[] = {
#if defined(LEAN_MULTI_THREAD)
{"tstack", required_argument, 0, 's'},
#endif
{"plugin", required_argument, 0, 'p'},
#ifdef LEAN_DEBUG
{"debug", required_argument, 0, 'B'},
#endif
{0, 0, 0, 0}
};

static char const * g_opt_str =
"PdD:c:C:qgvht:012j:012rM:012T:012a"
"PdD:c:C:qgvht:012j:012rM:012T:012ap:"
#if defined(LEAN_MULTI_THREAD)
"s:012"
#endif
Expand Down Expand Up @@ -289,6 +298,32 @@ options set_config_option(options const & opts, char const * in) {
}
}

void load_plugin(std::string path) {
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

We should move this function to a different folder since we need it to implement the import plugin <plugin-name> command

void * init;
// we never want to look up plugins using the system library search
path = lrealpath(path);
#ifdef LEAN_WINDOWS
HMODULE h = LoadLibrary(path.c_str());
if (!h) {
throw exception(sstream() << "error loading plugin " << path);
}
init = reinterpret_cast<void *>(GetProcAddress(h, "initialize_Default"));
#else
void *handle = dlopen(path.c_str(), RTLD_LAZY);
if (!handle) {
throw exception(sstream() << "error loading plugin, " << dlerror());
}
init = dlsym(handle, "initialize_Default");
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It seems every plugin must define initialize_Default. Is this a problem?
https://stackoverflow.com/questions/6538501/linking-two-shared-libraries-with-some-of-the-same-symbols
I am assuming it should work since you are using dlsym.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes, objects loaded by dlsym are independent by default.

      RTLD_LOCAL
              This is the converse of RTLD_GLOBAL, and the default if neither flag is specified.  Symbols  defined  in  this
              shared object are not made available to resolve references in subsequently loaded shared objects.

As far as I could find out, this is actually the only behavior supported on Windows, so we should be fine.

Btw, note that if we ever do prefix import paths with the package name as we once discussed, this would be initialize_SnakeLinter_Default anyway (which --plugin should derive from the library filename).

Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Should this try calling dlopen with RTLD_NOLOAD (if available) first, to check if the shared library is actually loaded already,
to avoid opening the same library twice?

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

If the same shared object is opened again with dlopen(), the same object handle is returned. And Lean initializers are idempotent.

Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks I had missed the section describing that in the docs, needed to read further.

#endif
if (!init) {
throw exception(sstream() << "error, plugin " << path << " does not seem to contain a module 'Default'");
}
auto init_fn = reinterpret_cast<object *(*)(object *)>(init);
object *r = init_fn(io_mk_world());
consume_io_result(r);
// NOTE: we never unload plugins
}

class initializer {
private:
lean::initializer m_init;
Expand Down Expand Up @@ -344,6 +379,10 @@ int main(int argc, char ** argv) {
} catch (e) {
console.log(e);
});
#endif
#if LEAN_WINDOWS
// "best practice" according to https://docs.microsoft.com/en-us/windows/win32/api/errhandlingapi/nf-errhandlingapi-seterrormode
SetErrorMode(SEM_FAILCRITICALERRORS);
#endif
auto init_start = std::chrono::steady_clock::now();
::initializer init;
Expand Down Expand Up @@ -454,6 +493,9 @@ int main(int argc, char ** argv) {
case 'n':
new_frontend = true;
break;
case 'p':
load_plugin(optarg);
break;
default:
std::cerr << "Unknown command line option\n";
display_help(std::cerr);
Expand Down