From 2d8adb765194464c2d37601530a13fa043427495 Mon Sep 17 00:00:00 2001 From: Mate Soos Date: Thu, 30 Jun 2022 03:22:04 +0800 Subject: [PATCH 1/7] Adding required stuff for static compilation --- CMakeLists.txt | 8 ++++++++ libsmtutil/CMakeLists.txt | 10 +++++----- libsolidity/CMakeLists.txt | 2 +- libyul/CMakeLists.txt | 2 +- tools/CMakeLists.txt | 3 +-- 5 files changed, 16 insertions(+), 9 deletions(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index 759f69a53..27923b1b5 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -35,6 +35,14 @@ endif() option(SOLC_LINK_STATIC "Link solc executable statically on supported platforms" OFF) option(SOLC_STATIC_STDLIBS "Link solc against static versions of libgcc and libstdc++ on supported platforms" OFF) option(STRICT_Z3_VERSION "Use the latest version of Z3" ON) +option(STATICCOMPILE "Compile to static executable" OFF) +if (STATICCOMPILE) + set(BUILD_SHARED_LIBS OFF) + set(Boost_USE_STATIC_LIBS ON) + set(SOLC_STATIC_STDLIBS ON) + set(SOLC_LINK_STATIC ON) + set(CMAKE_EXE_LINKER_FLAGS "-static") +endif() # Setup cccache. include(EthCcache) diff --git a/libsmtutil/CMakeLists.txt b/libsmtutil/CMakeLists.txt index af7f47b60..f839b546e 100644 --- a/libsmtutil/CMakeLists.txt +++ b/libsmtutil/CMakeLists.txt @@ -37,15 +37,15 @@ if (${USE_Z3_DLOPEN}) endif() add_library(smtutil ${sources} ${z3_SRCS} ${cvc4_SRCS}) -target_link_libraries(smtutil PUBLIC solutil Boost::boost) +target_link_libraries(smtutil LINK_PUBLIC solutil Boost::boost) if (${USE_Z3_DLOPEN}) - target_include_directories(smtutil PUBLIC ${Z3_HEADER_PATH}) - target_link_libraries(smtutil PUBLIC ${CMAKE_DL_LIBS}) + target_include_directories(smtutil LINK_PUBLIC ${Z3_HEADER_PATH}) + target_link_libraries(smtutil LINK_PUBLIC ${CMAKE_DL_LIBS}) elseif (${Z3_FOUND}) - target_link_libraries(smtutil PUBLIC z3::libz3) + target_link_libraries(smtutil LINK_PUBLIC z3::libz3) endif() if (${CVC4_FOUND}) - target_link_libraries(smtutil PUBLIC CVC4::CVC4) + target_link_libraries(smtutil LINK_PUBLIC CVC4::CVC4) endif() diff --git a/libsolidity/CMakeLists.txt b/libsolidity/CMakeLists.txt index 3d2845463..e316837b3 100644 --- a/libsolidity/CMakeLists.txt +++ b/libsolidity/CMakeLists.txt @@ -175,4 +175,4 @@ set(sources ) add_library(solidity ${sources}) -target_link_libraries(solidity PUBLIC yul evmasm langutil smtutil solutil Boost::boost fmt::fmt-header-only) +target_link_libraries(solidity LINK_PUBLIC yul evmasm langutil smtutil solutil Boost::boost fmt::fmt-header-only) diff --git a/libyul/CMakeLists.txt b/libyul/CMakeLists.txt index 806f094fe..69a2fe85f 100644 --- a/libyul/CMakeLists.txt +++ b/libyul/CMakeLists.txt @@ -223,4 +223,4 @@ add_library(yul optimiser/VarNameCleaner.h ) -target_link_libraries(yul PUBLIC evmasm solutil langutil smtutil fmt::fmt-header-only) +target_link_libraries(yul LINK_PUBLIC evmasm solutil langutil smtutil fmt::fmt-header-only) diff --git a/tools/CMakeLists.txt b/tools/CMakeLists.txt index 7415e0d01..2230cb4ab 100644 --- a/tools/CMakeLists.txt +++ b/tools/CMakeLists.txt @@ -50,9 +50,8 @@ target_link_libraries(yul-phaser PRIVATE phaser) install(TARGETS yul-phaser DESTINATION "${CMAKE_INSTALL_BINDIR}") - add_executable(satsolver satsolver-main.cpp) target_link_libraries(satsolver PUBLIC solidity range-v3 Boost::boost Boost::program_options) add_executable(solsmt solsmt.cpp) -target_link_libraries(solsmt PRIVATE smtutil solutil range-v3 Boost::boost Boost::program_options) +target_link_libraries(solsmt LINK_PRIVATE smtutil solutil range-v3 Boost::boost Boost::program_options) From 0193a3f3155992b0e8e8feae42578810bd99fc32 Mon Sep 17 00:00:00 2001 From: Mate Soos Date: Fri, 1 Jul 2022 11:35:46 +0200 Subject: [PATCH 2/7] Making things more solidity-like --- libsolutil/CDCL.cpp | 16 ++++++++-------- libsolutil/CDCL.h | 26 +++++++++++++------------- 2 files changed, 21 insertions(+), 21 deletions(-) diff --git a/libsolutil/CDCL.cpp b/libsolutil/CDCL.cpp index 0548c1d89..14fe67961 100644 --- a/libsolutil/CDCL.cpp +++ b/libsolutil/CDCL.cpp @@ -38,7 +38,7 @@ CDCL::CDCL( m_theorySolver(_theorySolver), m_backtrackNotify(_backtrackNotify), m_variables(move(_variables)), - order(VarOrderLt(activity)) + m_order(VarOrderLt(m_activity)) { for (Clause const& clause: _clauses) addClause(clause); @@ -278,17 +278,17 @@ std::pair CDCL::analyze(Clause _conflictClause) void CDCL::addClause(Clause _clause) { - uint64_t max_var = (uint32_t)activity.size(); + uint64_t max_var = (uint32_t)m_activity.size(); uint64_t new_max_var = 0; for(auto const& l: _clause) { new_max_var = std::max(l.variable+1, max_var); } int64_t to_add = (int64_t)new_max_var - (int64_t)max_var; if (to_add > 0) { - activity.insert(activity.end(), (uint64_t)to_add, 0.0); + m_activity.insert(m_activity.end(), (uint64_t)to_add, 0.0); } for(auto const& l: _clause) { - if (!order.inHeap((int)l.variable)) order.insert((int)l.variable); + if (!m_order.inHeap((int)l.variable)) m_order.insert((int)l.variable); } m_clauses.push_back(make_unique(move(_clause))); @@ -331,8 +331,8 @@ void CDCL::cancelUntil(size_t _backtrackLevel) m_reason.erase(l); // TODO maybe could do without. m_levelForVariable.erase(l.variable); - if (!order.inHeap((int)l.variable)) { - order.insert((int)l.variable); + if (!m_order.inHeap((int)l.variable)) { + m_order.insert((int)l.variable); } } m_decisionPoints.resize(_backtrackLevel); @@ -344,8 +344,8 @@ void CDCL::cancelUntil(size_t _backtrackLevel) optional CDCL::nextDecisionVariable() { while(true) { - if (order.empty()) return nullopt; - size_t i = (size_t)order.removeMin(); + if (m_order.empty()) return nullopt; + size_t i = (size_t)m_order.removeMin(); if (!m_assignments.count(i)) return i; } return nullopt; diff --git a/libsolutil/CDCL.h b/libsolutil/CDCL.h index 6cecd1dce..04d970a1f 100644 --- a/libsolutil/CDCL.h +++ b/libsolutil/CDCL.h @@ -129,30 +129,30 @@ private: #endif // Var activity - Heap order; - std::vector activity; - double var_inc_vsids = 1; - double var_decay = 0.95; + Heap m_order; + std::vector m_activity; + double m_var_inc_vsids = 1; + double m_var_decay = 0.95; void vsids_decay_var_act() { - var_inc_vsids *= (1.0 / var_decay); + m_var_inc_vsids *= (1.0 / m_var_decay); } - void vsids_bump_var_act(uint32_t var) + void vsids_bump_var_act(const uint32_t var) { - assert(activity.size() > var); - activity[var] += var_inc_vsids; + assert(m_activity.size() > var); + m_activity[var] += m_var_inc_vsids; bool rescaled = false; - if (activity[var] > 1e100) { + if (m_activity[var] > 1e100) { // Rescale - for (auto& a: activity) a *= 1e-100; + for (auto& a: m_activity) a *= 1e-100; rescaled = true; - var_inc_vsids *= 1e-100; + m_var_inc_vsids *= 1e-100; } // Update order_heap with respect to new activity: - if (order.inHeap((int)var)) order.decrease((int)var); - if (rescaled) assert(order.heap_property()); + if (m_order.inHeap((int)var)) m_order.decrease((int)var); + if (rescaled) assert(m_order.heap_property()); } // TODO group those into a class From 6ca4979a2b70b85378e655b235725e1565b6a5e6 Mon Sep 17 00:00:00 2001 From: Mate Soos Date: Fri, 1 Jul 2022 11:39:57 +0200 Subject: [PATCH 3/7] No need for this change --- libsmtutil/CMakeLists.txt | 10 +++++----- libsolidity/CMakeLists.txt | 2 +- libyul/CMakeLists.txt | 2 +- 3 files changed, 7 insertions(+), 7 deletions(-) diff --git a/libsmtutil/CMakeLists.txt b/libsmtutil/CMakeLists.txt index f839b546e..af7f47b60 100644 --- a/libsmtutil/CMakeLists.txt +++ b/libsmtutil/CMakeLists.txt @@ -37,15 +37,15 @@ if (${USE_Z3_DLOPEN}) endif() add_library(smtutil ${sources} ${z3_SRCS} ${cvc4_SRCS}) -target_link_libraries(smtutil LINK_PUBLIC solutil Boost::boost) +target_link_libraries(smtutil PUBLIC solutil Boost::boost) if (${USE_Z3_DLOPEN}) - target_include_directories(smtutil LINK_PUBLIC ${Z3_HEADER_PATH}) - target_link_libraries(smtutil LINK_PUBLIC ${CMAKE_DL_LIBS}) + target_include_directories(smtutil PUBLIC ${Z3_HEADER_PATH}) + target_link_libraries(smtutil PUBLIC ${CMAKE_DL_LIBS}) elseif (${Z3_FOUND}) - target_link_libraries(smtutil LINK_PUBLIC z3::libz3) + target_link_libraries(smtutil PUBLIC z3::libz3) endif() if (${CVC4_FOUND}) - target_link_libraries(smtutil LINK_PUBLIC CVC4::CVC4) + target_link_libraries(smtutil PUBLIC CVC4::CVC4) endif() diff --git a/libsolidity/CMakeLists.txt b/libsolidity/CMakeLists.txt index e316837b3..3d2845463 100644 --- a/libsolidity/CMakeLists.txt +++ b/libsolidity/CMakeLists.txt @@ -175,4 +175,4 @@ set(sources ) add_library(solidity ${sources}) -target_link_libraries(solidity LINK_PUBLIC yul evmasm langutil smtutil solutil Boost::boost fmt::fmt-header-only) +target_link_libraries(solidity PUBLIC yul evmasm langutil smtutil solutil Boost::boost fmt::fmt-header-only) diff --git a/libyul/CMakeLists.txt b/libyul/CMakeLists.txt index 69a2fe85f..806f094fe 100644 --- a/libyul/CMakeLists.txt +++ b/libyul/CMakeLists.txt @@ -223,4 +223,4 @@ add_library(yul optimiser/VarNameCleaner.h ) -target_link_libraries(yul LINK_PUBLIC evmasm solutil langutil smtutil fmt::fmt-header-only) +target_link_libraries(yul PUBLIC evmasm solutil langutil smtutil fmt::fmt-header-only) From 3073def64db060fd3a92ae293f29abfbbb4be6cf Mon Sep 17 00:00:00 2001 From: Mate Soos Date: Fri, 1 Jul 2022 11:48:05 +0200 Subject: [PATCH 4/7] To remove compile issues --- cmake/EthCompilerSettings.cmake | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/cmake/EthCompilerSettings.cmake b/cmake/EthCompilerSettings.cmake index ffa825446..ac08eaf9b 100644 --- a/cmake/EthCompilerSettings.cmake +++ b/cmake/EthCompilerSettings.cmake @@ -46,7 +46,7 @@ if (("${CMAKE_CXX_COMPILER_ID}" MATCHES "GNU") OR ("${CMAKE_CXX_COMPILER_ID}" MA # to fix warnings as they arise, so they don't accumulate "to be fixed later". add_compile_options(-Wall) add_compile_options(-Wextra) - add_compile_options(-Werror) + #add_compile_options(-Werror) add_compile_options(-pedantic) add_compile_options(-Wmissing-declarations) add_compile_options(-Wno-unknown-pragmas) From ca3d8b47146ef0f352f8be51bbde9c166eddd389 Mon Sep 17 00:00:00 2001 From: Mate Soos Date: Fri, 1 Jul 2022 13:02:56 +0200 Subject: [PATCH 5/7] Better function name --- libsolutil/CDCL.cpp | 2 +- libsolutil/CDCL.h | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/libsolutil/CDCL.cpp b/libsolutil/CDCL.cpp index 14fe67961..70770420f 100644 --- a/libsolutil/CDCL.cpp +++ b/libsolutil/CDCL.cpp @@ -243,7 +243,7 @@ std::pair CDCL::analyze(Clause _conflictClause) else { //cout << " adding " << toString(literal) << " @" << variableLevel << " to learnt clause." << endl; - vsids_bump_var_act((uint32_t)literal.variable); + vsidsBumpVarAct((uint32_t)literal.variable); learntClause.push_back(literal); backtrackLevel = max(backtrackLevel, variableLevel); } diff --git a/libsolutil/CDCL.h b/libsolutil/CDCL.h index 04d970a1f..f96fe93a3 100644 --- a/libsolutil/CDCL.h +++ b/libsolutil/CDCL.h @@ -137,7 +137,7 @@ private: { m_var_inc_vsids *= (1.0 / m_var_decay); } - void vsids_bump_var_act(const uint32_t var) + void vsidsBumpVarAct(const uint32_t var) { assert(m_activity.size() > var); m_activity[var] += m_var_inc_vsids; From 0e1f7112b395c72736c209a31feaabea6cfca580 Mon Sep 17 00:00:00 2001 From: Mate Soos Date: Fri, 1 Jul 2022 14:38:57 +0200 Subject: [PATCH 6/7] Fixing it back to correct linking --- tools/CMakeLists.txt | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tools/CMakeLists.txt b/tools/CMakeLists.txt index 2230cb4ab..d5f5a0bb6 100644 --- a/tools/CMakeLists.txt +++ b/tools/CMakeLists.txt @@ -54,4 +54,4 @@ add_executable(satsolver satsolver-main.cpp) target_link_libraries(satsolver PUBLIC solidity range-v3 Boost::boost Boost::program_options) add_executable(solsmt solsmt.cpp) -target_link_libraries(solsmt LINK_PRIVATE smtutil solutil range-v3 Boost::boost Boost::program_options) +target_link_libraries(solsmt PRIVATE smtutil solutil range-v3 Boost::boost Boost::program_options) From 8cd552c8e3e8e2c680fac6743ccafc6db3f88186 Mon Sep 17 00:00:00 2001 From: Mate Soos Date: Fri, 1 Jul 2022 14:41:34 +0200 Subject: [PATCH 7/7] Don't remove emtpy line --- tools/CMakeLists.txt | 1 + 1 file changed, 1 insertion(+) diff --git a/tools/CMakeLists.txt b/tools/CMakeLists.txt index d5f5a0bb6..7415e0d01 100644 --- a/tools/CMakeLists.txt +++ b/tools/CMakeLists.txt @@ -50,6 +50,7 @@ target_link_libraries(yul-phaser PRIVATE phaser) install(TARGETS yul-phaser DESTINATION "${CMAKE_INSTALL_BINDIR}") + add_executable(satsolver satsolver-main.cpp) target_link_libraries(satsolver PUBLIC solidity range-v3 Boost::boost Boost::program_options)