From 637546850fb9b1d83e68755c31a67cbe41ba85e0 Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Tue, 22 Jan 2019 14:34:29 +0100 Subject: [PATCH 1/3] [SMTChecker] Add mod operator --- libsolidity/formal/CVC4Interface.cpp | 2 ++ libsolidity/formal/SolverInterface.h | 5 +++++ libsolidity/formal/Z3Interface.cpp | 2 ++ 3 files changed, 9 insertions(+) diff --git a/libsolidity/formal/CVC4Interface.cpp b/libsolidity/formal/CVC4Interface.cpp index e7c8f0159..71f657471 100644 --- a/libsolidity/formal/CVC4Interface.cpp +++ b/libsolidity/formal/CVC4Interface.cpp @@ -163,6 +163,8 @@ CVC4::Expr CVC4Interface::toCVC4Expr(Expression const& _expr) return m_context.mkExpr(CVC4::kind::MULT, arguments[0], arguments[1]); else if (n == "/") return m_context.mkExpr(CVC4::kind::INTS_DIVISION_TOTAL, arguments[0], arguments[1]); + else if (n == "mod") + return m_context.mkExpr(CVC4::kind::INTS_MODULUS, arguments[0], arguments[1]); else if (n == "select") return m_context.mkExpr(CVC4::kind::SELECT, arguments[0], arguments[1]); else if (n == "store") diff --git a/libsolidity/formal/SolverInterface.h b/libsolidity/formal/SolverInterface.h index 76991a58f..80b48e0f6 100644 --- a/libsolidity/formal/SolverInterface.h +++ b/libsolidity/formal/SolverInterface.h @@ -141,6 +141,7 @@ public: {"-", 2}, {"*", 2}, {"/", 2}, + {"mod", 2}, {"select", 2}, {"store", 3} }; @@ -246,6 +247,10 @@ public: { return Expression("/", std::move(_a), std::move(_b), Kind::Int); } + friend Expression operator%(Expression _a, Expression _b) + { + return Expression("mod", std::move(_a), std::move(_b), Kind::Int); + } Expression operator()(std::vector _arguments) const { solAssert( diff --git a/libsolidity/formal/Z3Interface.cpp b/libsolidity/formal/Z3Interface.cpp index 4cbc32719..4d7ea8347 100644 --- a/libsolidity/formal/Z3Interface.cpp +++ b/libsolidity/formal/Z3Interface.cpp @@ -162,6 +162,8 @@ z3::expr Z3Interface::toZ3Expr(Expression const& _expr) return arguments[0] * arguments[1]; else if (n == "/") return arguments[0] / arguments[1]; + else if (n == "mod") + return z3::mod(arguments[0], arguments[1]); else if (n == "select") return z3::select(arguments[0], arguments[1]); else if (n == "store") From 4058978b3ba12ea1cb66f6364b1b6bc85958b032 Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Mon, 4 Feb 2019 14:39:45 +0100 Subject: [PATCH 2/3] Require Z3 >= 4.6.0 --- cmake/FindZ3.cmake | 18 +++++++++++++++++- libsolidity/CMakeLists.txt | 2 +- 2 files changed, 18 insertions(+), 2 deletions(-) diff --git a/cmake/FindZ3.cmake b/cmake/FindZ3.cmake index ad34cbc3b..bdd8ce72f 100644 --- a/cmake/FindZ3.cmake +++ b/cmake/FindZ3.cmake @@ -1,8 +1,24 @@ if (USE_Z3) find_path(Z3_INCLUDE_DIR NAMES z3++.h PATH_SUFFIXES z3) find_library(Z3_LIBRARY NAMES z3) + find_program(Z3_EXECUTABLE z3 PATH_SUFFIXES bin) + + if(Z3_INCLUDE_DIR AND Z3_LIBRARY AND Z3_EXECUTABLE) + execute_process (COMMAND ${Z3_EXECUTABLE} -version + OUTPUT_VARIABLE libz3_version_str + ERROR_QUIET + OUTPUT_STRIP_TRAILING_WHITESPACE) + + string(REGEX REPLACE "^Z3 version ([0-9.]+).*" "\\1" + Z3_VERSION_STRING "${libz3_version_str}") + unset(libz3_version_str) + endif() + mark_as_advanced(Z3_VERSION_STRING z3_DIR) + include(FindPackageHandleStandardArgs) - find_package_handle_standard_args(Z3 DEFAULT_MSG Z3_LIBRARY Z3_INCLUDE_DIR) + find_package_handle_standard_args(Z3 + REQUIRED_VARS Z3_LIBRARY Z3_INCLUDE_DIR + VERSION_VAR Z3_VERSION_STRING) if (NOT TARGET Z3::Z3) add_library(Z3::Z3 UNKNOWN IMPORTED) diff --git a/libsolidity/CMakeLists.txt b/libsolidity/CMakeLists.txt index 8c2ab3475..6cc77c4e3 100644 --- a/libsolidity/CMakeLists.txt +++ b/libsolidity/CMakeLists.txt @@ -102,7 +102,7 @@ set(sources parsing/Token.h ) -find_package(Z3 QUIET) +find_package(Z3 4.6.0) if (${Z3_FOUND}) add_definitions(-DHAVE_Z3) message("Z3 SMT solver found. This enables optional SMT checking with Z3.") From bea695f3fc661b48e1a5929fe4af8fedb615ede4 Mon Sep 17 00:00:00 2001 From: chriseth Date: Wed, 6 Feb 2019 15:50:36 +0100 Subject: [PATCH 3/3] Changelog entry for Z3 version. --- Changelog.md | 1 + 1 file changed, 1 insertion(+) diff --git a/Changelog.md b/Changelog.md index 89143ee59..a08d22ecb 100644 --- a/Changelog.md +++ b/Changelog.md @@ -21,6 +21,7 @@ Bugfixes: Build System: * Add support for continuous fuzzing via Google oss-fuzz + * SMT: If using Z3, require version 4.6.0 or newer. * Ubuntu PPA Packages: Use CVC4 as SMT solver instead of Z3