Merge pull request #5841 from ethereum/smt_mod

[SMTChecker] Add mod operator

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
 
 

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)

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.")

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")

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<Expression> _arguments) const
 	{
 		solAssert(

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")