Merge remote-tracking branch 'origin/develop' into breaking

libsolidity/codegen/YulUtilFunctions.cpp

@@ -1437,19 +1437,27 @@ string YulUtilFunctions::storageArrayPushZeroFunction(ArrayType const& _type)
 {
 	solAssert(_type.location() == DataLocation::Storage, "");
 	solAssert(_type.isDynamicallySized(), "");
-	solUnimplementedAssert(!_type.isByteArray(), "Byte Arrays not yet implemented!");
 	solUnimplementedAssert(_type.baseType()->storageBytes() <= 32, "Base type is not yet implemented.");
 
 	string functionName = "array_push_zero_" + _type.identifier();
 	return m_functionCollector.createFunction(functionName, [&]() {
 		return Whiskers(R"(
 			function <functionName>(array) -> slot, offset {
-				let oldLen := <fetchLength>(array)
-				if iszero(lt(oldLen, <maxArrayLength>)) { <panic>() }
-				sstore(array, add(oldLen, 1))
+				<?isBytes>
+					let data := sload(array)
+					let oldLen := <extractLength>(data)
+					<increaseBytesSize>(array, data, oldLen, add(oldLen, 1))
+				<!isBytes>
+					let oldLen := <fetchLength>(array)
+					if iszero(lt(oldLen, <maxArrayLength>)) { <panic>() }
+					sstore(array, add(oldLen, 1))
+				</isBytes>
 				slot, offset := <indexAccess>(array, oldLen)
 			})")
 			("functionName", functionName)
+			("isBytes", _type.isByteArray())
+			("increaseBytesSize", _type.isByteArray() ? increaseByteArraySizeFunction(_type) : "")
+			("extractLength", _type.isByteArray() ? extractByteArrayLengthFunction() : "")
 			("panic", panicFunction(PanicCode::ResourceError))
 			("fetchLength", arrayLengthFunction(_type))
 			("indexAccess", storageArrayIndexAccessFunction(_type))

libsolidity/formal/BMC.cpp

@@ -23,6 +23,10 @@
 
 #include <libsmtutil/SMTPortfolio.h>
 
+#ifdef HAVE_Z3_DLOPEN
+#include <z3_version.h>
+#endif
+
 using namespace std;
 using namespace solidity;
 using namespace solidity::util;
@@ -83,7 +87,10 @@ void BMC::analyze(SourceUnit const& _source, map<ASTNode const*, set<Verificatio
 			m_outerErrorReporter.warning(
 				8084_error,
 				SourceLocation(),
-				"BMC analysis was not possible since no integrated SMT solver (Z3 or CVC4) was found."
+				"BMC analysis was not possible since no SMT solver (Z3 or CVC4) was found."
+#ifdef HAVE_Z3_DLOPEN
+				" Install libz3.so." + to_string(Z3_MAJOR_VERSION) + "." + to_string(Z3_MINOR_VERSION) + " to enable Z3."
+#endif
 			);
 		}
 	}

libsolidity/formal/CHC.cpp

@@ -34,6 +34,10 @@
 
 #include <boost/range/adaptor/reversed.hpp>
 
+#ifdef HAVE_Z3_DLOPEN
+#include <z3_version.h>
+#endif
+
 #include <queue>
 
 using namespace std;
@@ -58,7 +62,9 @@ CHC::CHC(
 	m_queryTimeout(_timeout)
 {
 	bool usesZ3 = _enabledSolvers.z3;
-#ifndef HAVE_Z3
+#ifdef HAVE_Z3
+	usesZ3 = usesZ3 && Z3Interface::available();
+#else
 	usesZ3 = false;
 #endif
 	if (!usesZ3)
@@ -88,16 +94,19 @@ void CHC::analyze(SourceUnit const& _source)
 	}
 
 	bool ranSolver = true;
-#ifndef HAVE_Z3
-	ranSolver = dynamic_cast<CHCSmtLib2Interface const*>(m_interface.get())->unhandledQueries().empty();
-#endif
+	if (auto const* smtLibInterface = dynamic_cast<CHCSmtLib2Interface const*>(m_interface.get()))
+		ranSolver = smtLibInterface->unhandledQueries().empty();
 	if (!ranSolver && !m_noSolverWarning)
 	{
 		m_noSolverWarning = true;
 		m_outerErrorReporter.warning(
 			3996_error,
 			SourceLocation(),
+#ifdef HAVE_Z3_DLOPEN
+			"CHC analysis was not possible since libz3.so." + to_string(Z3_MAJOR_VERSION) + "." + to_string(Z3_MINOR_VERSION) + " was not found."
+#else
 			"CHC analysis was not possible since no integrated z3 SMT solver was found."
+#endif
 		);
 	}
 	else
@@ -762,7 +771,7 @@ void CHC::resetSourceAnalysis()
 
 	bool usesZ3 = false;
 #ifdef HAVE_Z3
-	usesZ3 = m_enabledSolvers.z3;
+	usesZ3 = m_enabledSolvers.z3 && Z3Interface::available();
 	if (usesZ3)
 	{
 		/// z3::fixedpoint does not have a reset mechanism, so we need to create another.

libsolidity/formal/ModelChecker.cpp

@@ -17,6 +17,9 @@
 // SPDX-License-Identifier: GPL-3.0
 
 #include <libsolidity/formal/ModelChecker.h>
+#ifdef HAVE_Z3
+#include <libsmtutil/Z3Interface.h>
+#endif
 
 using namespace std;
 using namespace solidity;
@@ -63,7 +66,7 @@ solidity::smtutil::SMTSolverChoice ModelChecker::availableSolvers()
 {
 	smtutil::SMTSolverChoice available = smtutil::SMTSolverChoice::None();
 #ifdef HAVE_Z3
-	available.z3 = true;
+	available.z3 = solidity::smtutil::Z3Interface::available();
 #endif
 #ifdef HAVE_CVC4
 	available.cvc4 = true;