diff options
| -rw-r--r-- | cmake/FindZ3.cmake | 9 | ||||
| -rw-r--r-- | libsolidity/CMakeLists.txt | 16 | ||||
| -rw-r--r-- | libsolidity/formal/SMTChecker.cpp | 3 | ||||
| -rwxr-xr-x | scripts/install_deps.sh | 54 |
4 files changed, 57 insertions, 25 deletions
diff --git a/cmake/FindZ3.cmake b/cmake/FindZ3.cmake new file mode 100644 index 00000000..8f3f9ee1 --- /dev/null +++ b/cmake/FindZ3.cmake @@ -0,0 +1,9 @@ +find_path(Z3_INCLUDE_DIR z3++.h) +find_library(Z3_LIBRARY NAMES z3 ) +include(${CMAKE_CURRENT_LIST_DIR}/FindPackageHandleStandardArgs.cmake) +FIND_PACKAGE_HANDLE_STANDARD_ARGS(Z3 DEFAULT_MSG Z3_LIBRARY Z3_INCLUDE_DIR) + +if(Z3_FOUND) + set(Z3_LIBRARIES ${Z3_LIBRARY}) +endif() + diff --git a/libsolidity/CMakeLists.txt b/libsolidity/CMakeLists.txt index a88d16b8..f7c1a390 100644 --- a/libsolidity/CMakeLists.txt +++ b/libsolidity/CMakeLists.txt @@ -2,5 +2,19 @@ file(GLOB_RECURSE sources "*.cpp" "../libjulia/*.cpp") file(GLOB_RECURSE headers "*.h" "../libjulia/*.h") +find_package(Z3 QUIET) +if (${Z3_FOUND}) + include_directories(${Z3_INCLUDE_DIR}) + add_definitions(-DHAVE_Z3) + message("Z3 SMT solver FOUND.") +else() + message("Z3 SMT solver NOT found.") + list(REMOVE_ITEM sources "${CMAKE_CURRENT_SOURCE_DIR}/formal/Z3Interface.cpp") +endif() + add_library(solidity ${sources} ${headers}) -target_link_libraries(solidity PUBLIC evmasm devcore z3) +target_link_libraries(solidity PUBLIC evmasm devcore) + +if (${Z3_FOUND}) + target_link_libraries(solidity PUBLIC ${Z3_LIBRARY}) +endif()
\ No newline at end of file diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp index b9e0e8f3..76232c2e 100644 --- a/libsolidity/formal/SMTChecker.cpp +++ b/libsolidity/formal/SMTChecker.cpp @@ -76,6 +76,9 @@ bool SMTChecker::visit(FunctionDefinition const& _function) void SMTChecker::endVisit(FunctionDefinition const&) { // TOOD we could check for "reachability", i.e. satisfiability here. + // We only handle local variables, so we clear everything. + // If we add storage variables, those should be cleared differently. + m_currentSequenceCounter.clear(); m_interface.pop(); m_currentFunction = nullptr; } diff --git a/scripts/install_deps.sh b/scripts/install_deps.sh index 24cf49d5..760e4b80 100755 --- a/scripts/install_deps.sh +++ b/scripts/install_deps.sh @@ -115,7 +115,7 @@ case $(uname -s) in echo "Installing solidity dependencies on FreeBSD." echo "ERROR - 'install_deps.sh' doesn't have FreeBSD support yet." echo "Please let us know if you see this error message, and we can work out what is missing." - echo "Drop us a message at https://gitter.im/ethereum/solidity." + echo "Drop us a message at https://gitter.im/ethereum/solidity-dev." exit 1 ;; @@ -167,6 +167,7 @@ case $(uname -s) in Debian) #Debian + install_z3="" case $(lsb_release -cs) in wheezy) #wheezy @@ -174,7 +175,7 @@ case $(uname -s) in echo "ERROR - 'install_deps.sh' doesn't have Debian Wheezy support yet." echo "See http://solidity.readthedocs.io/en/latest/installing-solidity.html for manual instructions." echo "If you would like to get 'install_deps.sh' working for Debian Wheezy, that would be fantastic." - echo "Drop us a message at https://gitter.im/ethereum/solidity." + echo "Drop us a message at https://gitter.im/ethereum/solidity-dev." echo "See also https://github.com/ethereum/webthree-umbrella/issues/495 where we are working through Alpine support." exit 1 ;; @@ -185,20 +186,19 @@ case $(uname -s) in stretch) #stretch echo "Installing solidity dependencies on Debian Stretch (9.x)." - echo "ERROR - 'install_deps.sh' doesn't have Debian Stretch support yet." - echo "See http://solidity.readthedocs.io/en/latest/installing-solidity.html for manual instructions." - echo "If you would like to get 'install_deps.sh' working for Debian Stretch, that would be fantastic." - echo "Drop us a message at https://gitter.im/ethereum/solidity." - exit 1 + install_z3="libz3-dev" + ;; + buster) + #buster + echo "Installing solidity dependencies on Debian Buster (10.x)." + install_z3="libz3-dev" ;; *) #other Debian echo "Installing solidity dependencies on unknown Debian version." - echo "ERROR - Debian Jessie is the only Debian version which solidity has been tested on." - echo "If you are using a different release and would like to get 'install_deps.sh'" - echo "working for that release that would be fantastic." - echo "Drop us a message at https://gitter.im/ethereum/solidity." - exit 1 + echo "ERROR - This might not work, but we are trying anyway." + echo "Drop us a message at https://gitter.im/ethereum/solidity-dev" + install_z3="libz3-dev" ;; esac @@ -211,7 +211,9 @@ case $(uname -s) in gcc \ git \ libboost-all-dev \ - unzip + unzip \ + "$install_z3" + ;; @@ -267,6 +269,7 @@ case $(uname -s) in Ubuntu) #Ubuntu + install_z3="" case $(lsb_release -cs) in trusty) #trusty @@ -287,22 +290,25 @@ case $(uname -s) in xenial) #xenial echo "Installing solidity dependencies on Ubuntu Xenial Xerus (16.04)." + install_z3="libz3-dev" ;; yakkety) #yakkety echo "Installing solidity dependencies on Ubuntu Yakkety Yak (16.10)." - echo "" - echo "NOTE - You are in unknown territory with this preview OS." - echo "We will need to update the Ethereum PPAs, work through build and runtime breaks, etc." - echo "See https://github.com/ethereum/webthree-umbrella/issues/624." - echo "If you would like to partner with us to work through these, that" - echo "would be fantastic. Please just comment on that issue. Thanks!" + install_z3="libz3-dev" + ;; + zesty) + #zesty + echo "Installing solidity dependencies on Ubuntu Zesty (17.04)." + install_z3="libz3-dev" ;; *) #other Ubuntu echo "ERROR - Unknown or unsupported Ubuntu version (" $(lsb_release -cs) ")" - echo "We only support Trusty, Utopic, Vivid, Wily and Xenial, with work-in-progress on Yakkety." - exit 1 + echo "ERROR - This might not work, but we are trying anyway." + echo "Please drop us a message at https://gitter.im/ethereum/solidity-dev." + echo "We only support Trusty, Utopic, Vivid, Wily, Xenial and Yakkety." + install_z3="libz3-dev" ;; esac @@ -311,7 +317,7 @@ case $(uname -s) in build-essential \ cmake \ git \ - libboost-all-dev + libboost-all-dev "$install_z3" if [ "$CI" = true ]; then # Install 'eth', for use in the Solidity Tests-over-IPC. # We will not use this 'eth', but its dependencies @@ -375,7 +381,7 @@ case $(uname -s) in echo "ERROR - Unsupported or unidentified Linux distro." echo "See http://solidity.readthedocs.io/en/latest/installing-solidity.html for manual instructions." echo "If you would like to get your distro working, that would be fantastic." - echo "Drop us a message at https://gitter.im/ethereum/solidity." + echo "Drop us a message at https://gitter.im/ethereum/solidity-dev." exit 1 ;; esac @@ -392,6 +398,6 @@ case $(uname -s) in echo "ERROR - Unsupported or unidentified operating system." echo "See http://solidity.readthedocs.io/en/latest/installing-solidity.html for manual instructions." echo "If you would like to get your operating system working, that would be fantastic." - echo "Drop us a message at https://gitter.im/ethereum/solidity." + echo "Drop us a message at https://gitter.im/ethereum/solidity-dev." ;; esac |