cerc-io/solidity
16
0
Fork 0
mirror of https://github.com/ethereum/solidity synced 2023-10-03 13:03:40 +00:00
Code Issues Actions Packages Projects Releases Wiki Activity

Require latest Z3 by default and allow relaxing the requirement with STRICT_Z3_VERSION=OFF

Browse Source 
Signed-off-by: soroosh-sdi <soroosh.sardari@gmail.com>
This commit is contained in:
soroosh-sdi 2021-09-17 00:10:00 +04:30
parent 55467c1cca
commit 8b04ac38ab
3 changed files with 34 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
.circleci/build_win.ps1
View File

@ -18,7 +18,7 @@ else {
mkdir build
cd build
$boost_dir=(Resolve-Path $PSScriptRoot\..\deps\boost\lib\cmake\Boost-*)
..\deps\cmake\bin\cmake -G "Visual Studio 16 2019" -DBoost_DIR="$boost_dir\" -DCMAKE_MSVC_RUNTIME_LIBRARY=MultiThreaded -DCMAKE_INSTALL_PREFIX="$PSScriptRoot\..\upload" ..
..\deps\cmake\bin\cmake -G "Visual Studio 16 2019" -DBoost_DIR="$boost_dir\" -DCMAKE_MSVC_RUNTIME_LIBRARY=MultiThreaded -DCMAKE_INSTALL_PREFIX="$PSScriptRoot\..\upload" -DUSE_Z3=OFF ..
if ( -not $? ) { throw "CMake configure failed." }
msbuild solidity.sln /p:Configuration=Release /m:5 /v:minimal
if ( -not $? ) { throw "Build failed." }

24
CMakeLists.txt
View File

@ -34,6 +34,7 @@ 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)
# Setup cccache.
include(EthCcache)
@ -63,8 +64,29 @@ configure_file("${CMAKE_SOURCE_DIR}/cmake/templates/license.h.in" include/licens
include(EthOptions)
configure_project(TESTS)
set(LATEST_Z3_VERSION "4.8.12")
set(MINIMUM_Z3_VERSION "4.8.0")
find_package(Z3)
if (${Z3_FOUND})
if (${STRICT_Z3_VERSION})
if (NOT ("${Z3_VERSION_STRING}" VERSION_EQUAL ${LATEST_Z3_VERSION}))
message(
FATAL_ERROR
"SMTChecker tests require Z3 ${LATEST_Z3_VERSION} for all tests to pass.\n\
Build with -DSTRICT_Z3_VERSION=OFF if you want to use a different version. \
You can also use -DUSE_Z3=OFF to build without Z3. In both cases use --no-smt when running tests."
)
endif()
else()
if ("${Z3_VERSION_STRING}" VERSION_LESS ${MINIMUM_Z3_VERSION})
message(
FATAL_ERROR
"Solidity requires Z3 ${MINIMUM_Z3_VERSION} or newer. You can also use -DUSE_Z3=OFF to build without Z3."
)
endif()
endif()
endif()
find_package(Z3 4.8.0)
if(${USE_Z3_DLOPEN})
add_definitions(-DHAVE_Z3)
add_definitions(-DHAVE_Z3_DLOPEN)

10
docs/installing-solidity.rst
View File

@ -335,6 +335,16 @@ The following are dependencies for all builds of Solidity:
Starting from 0.5.10 linking against Boost 1.70+ should work without manual intervention.
.. note::
The default build configuration requires a specific Z3 version (the latest one at the time the
code was last updated). Changes introduced between Z3 releases often result in slightly different
(but still valid) results being returned. Our SMT tests do not account for these differences and
will likely fail with a different version than the one they were written for. This does not mean
that a build using a different version is faulty. If you pass ``-DSTRICT_Z3_VERSION=OFF`` option
to CMake, you can build with any version that satisfies the requirement given in the table above.
If you do this, however, please remember to pass the ``--no-smt`` option to ``scripts/tests.sh``
to skip the SMT tests.
Minimum Compiler Versions
^^^^^^^^^^^^^^^^^^^^^^^^^