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

Changelog.md

@@ -32,6 +32,8 @@ Compiler Features:
 Bugfixes:
  * SMTChecker: Fix lack of reporting potential violations when using only the CHC engine.
  * SMTChecker: Fix internal error on conversion from string literal to byte.
+ * SMTChecker: Fix internal error when using tuples of rational literals inside the conditional operator.
+ * SMTChecker: Fix internal error when assigning state variable via contract's name.
  * Code generator: Fix missing creation dependency tracking for abstract contracts.
 
 

docs/control-structures.rst

@@ -700,7 +700,13 @@ The following example shows how to use an error string together with ``revert``
         }
     }
 
-The two syntax options are equivalent, it's developer preference which to use.
+If you provide the reason string directly, then the two syntax options are equivalent, it is the developer's preference which one to use.
+
+.. note::
+    The ``require`` function is evaluated just as any other function.
+    This means that all arguments are evaluated before the function itself is executed.
+    In particular, in ``require(condition, f())`` the function ``f`` is executed even if
+    ``condition`` is true.
 
 The provided string is :ref:`abi-encoded <ABI>` as if it were a call to a function ``Error(string)``.
 In the above example, ``revert("Not enough Ether provided.");`` returns the following hexadecimal as error return data:

docs/security-considerations.rst

@@ -457,19 +457,21 @@ The SMT encoding tries to be as precise as possible, mapping Solidity types
 and expressions to their closest `SMT-LIB <http://smtlib.cs.uiowa.edu/>`_
 representation, as shown in the table below.
 
-+-----------------------+--------------+-----------------------------+
++-----------------------+--------------------------------+-----------------------------+
-|Solidity type          |SMT sort      |Theories (quantifier-free)   |
+|Solidity type          |SMT sort                        |Theories (quantifier-free)   |
-+=======================+==============+=============================+
++=======================+================================+=============================+
-|Boolean                |Bool          |Bool                         |
+|Boolean                |Bool                            |Bool                         |
-+-----------------------+--------------+-----------------------------+
++-----------------------+--------------------------------+-----------------------------+
-|intN, uintN, address,  |Integer       |LIA, NIA                     |
+|intN, uintN, address,  |Integer                         |LIA, NIA                     |
-|bytesN, enum           |              |                             |
+|bytesN, enum           |                                |                             |
-+-----------------------+--------------+-----------------------------+
++-----------------------+--------------------------------+-----------------------------+
-|array, mapping, bytes, |Array         |Arrays                       |
+|array, mapping, bytes, |Tuple                           |Datatypes, Arrays, LIA       |
-|string                 |              |                             |
+|string                 |(Array elements, Integer length)|                             |
-+-----------------------+--------------+-----------------------------+
++-----------------------+--------------------------------+-----------------------------+
-|other types            |Integer       |LIA                          |
+|struct                 |Tuple                           |Datatypes                    |
-+-----------------------+--------------+-----------------------------+
++-----------------------+--------------------------------+-----------------------------+
+|other types            |Integer                         |LIA                          |
++-----------------------+--------------------------------+-----------------------------+
 
 Types that are not yet supported are abstracted by a single 256-bit unsigned
 integer, where their unsupported operations are ignored.

libevmasm/Assembly.cpp

@@ -580,14 +580,14 @@ LinkerObject const& Assembly::assemble() const
 	multimap<size_t, size_t> subRef;
 	vector<unsigned> sizeRef; ///< Pointers to code locations where the size of the program is inserted
 	unsigned bytesPerTag = util::bytesRequired(bytesRequiredForCode);
-	uint8_t tagPush = (uint8_t)Instruction::PUSH1 - 1 + bytesPerTag;
+	uint8_t tagPush = (uint8_t)pushInstruction(bytesPerTag);
 
 	unsigned bytesRequiredIncludingData = bytesRequiredForCode + 1 + m_auxiliaryData.size();
 	for (auto const& sub: m_subs)
 		bytesRequiredIncludingData += sub->assemble().bytecode.size();
 
 	unsigned bytesPerDataRef = util::bytesRequired(bytesRequiredIncludingData);
-	uint8_t dataRefPush = (uint8_t)Instruction::PUSH1 - 1 + bytesPerDataRef;
+	uint8_t dataRefPush = (uint8_t)pushInstruction(bytesPerDataRef);
 	ret.bytecode.reserve(bytesRequiredIncludingData);
 
 	for (AssemblyItem const& i: m_items)
@@ -617,7 +617,7 @@ LinkerObject const& Assembly::assemble() const
 		case Push:
 		{
 			uint8_t b = max<unsigned>(1, util::bytesRequired(i.data()));
-			ret.bytecode.push_back((uint8_t)Instruction::PUSH1 - 1 + b);
+			ret.bytecode.push_back((uint8_t)pushInstruction(b));
 			ret.bytecode.resize(ret.bytecode.size() + b);
 			bytesRef byr(&ret.bytecode.back() + 1 - b, b);
 			toBigEndian(i.data(), byr);
@@ -647,7 +647,7 @@ LinkerObject const& Assembly::assemble() const
 			auto s = subAssemblyById(static_cast<size_t>(i.data()))->assemble().bytecode.size();
 			i.setPushedValue(u256(s));
 			uint8_t b = max<unsigned>(1, util::bytesRequired(s));
-			ret.bytecode.push_back((uint8_t)Instruction::PUSH1 - 1 + b);
+			ret.bytecode.push_back((uint8_t)pushInstruction(b));
 			ret.bytecode.resize(ret.bytecode.size() + b);
 			bytesRef byr(&ret.bytecode.back() + 1 - b, b);
 			toBigEndian(s, byr);
@@ -683,7 +683,7 @@ LinkerObject const& Assembly::assemble() const
 				}
 				// TODO: should we make use of the constant optimizer methods for pushing the offsets?
 				bytes offsetBytes = toCompactBigEndian(u256(offsets[i]));
-				ret.bytecode.push_back(uint8_t(Instruction::PUSH1) - 1 + offsetBytes.size());
+				ret.bytecode.push_back(uint8_t(pushInstruction(offsetBytes.size())));
 				ret.bytecode += offsetBytes;
 				ret.bytecode.push_back(uint8_t(Instruction::ADD));
 				ret.bytecode.push_back(uint8_t(Instruction::MSTORE));

libsmtutil/CHCSolverInterface.h

@@ -44,9 +44,7 @@ public:
 	/// Needs to bound all vars as universally quantified.
 	virtual void addRule(Expression const& _expr, std::string const& _name) = 0;
 
-	/// first: predicate name
+	using CexNode = Expression;
-	/// second: predicate arguments
-	using CexNode = std::pair<std::string, std::vector<std::string>>;
 	struct CexGraph
 	{
 		std::map<unsigned, CexNode> nodes;

libsmtutil/SolverInterface.h

@@ -60,6 +60,8 @@ class Expression
 public:
 	explicit Expression(bool _v): Expression(_v ? "true" : "false", Kind::Bool) {}
 	explicit Expression(std::shared_ptr<SortSort> _sort, std::string _name = ""): Expression(std::move(_name), {}, _sort) {}
+	explicit Expression(std::string _name, std::vector<Expression> _arguments, SortPointer _sort):
+		name(std::move(_name)), arguments(std::move(_arguments)), sort(std::move(_sort)) {}
 	Expression(size_t _number): Expression(std::to_string(_number), {}, SortProvider::sintSort) {}
 	Expression(u256 const& _number): Expression(_number.str(), {}, SortProvider::sintSort) {}
 	Expression(s256 const& _number): Expression(_number.str(), {}, SortProvider::sintSort) {}
@@ -233,14 +235,26 @@ public:
 
 	friend Expression operator!(Expression _a)
 	{
+		if (_a.sort->kind == Kind::BitVector)
+			return ~_a;
 		return Expression("not", std::move(_a), Kind::Bool);
 	}
 	friend Expression operator&&(Expression _a, Expression _b)
 	{
+		if (_a.sort->kind == Kind::BitVector)
+		{
+			smtAssert(_b.sort->kind == Kind::BitVector, "");
+			return _a & _b;
+		}
 		return Expression("and", std::move(_a), std::move(_b), Kind::Bool);
 	}
 	friend Expression operator||(Expression _a, Expression _b)
 	{
+		if (_a.sort->kind == Kind::BitVector)
+		{
+			smtAssert(_b.sort->kind == Kind::BitVector, "");
+			return _a | _b;
+		}
 		return Expression("or", std::move(_a), std::move(_b), Kind::Bool);
 	}
 	friend Expression operator==(Expression _a, Expression _b)
@@ -344,8 +358,6 @@ public:
 
 private:
 	/// Manual constructors, should only be used by SolverInterface and this class itself.
-	Expression(std::string _name, std::vector<Expression> _arguments, SortPointer _sort):
-		name(std::move(_name)), arguments(std::move(_arguments)), sort(std::move(_sort)) {}
 	Expression(std::string _name, std::vector<Expression> _arguments, Kind _kind):
 		Expression(std::move(_name), std::move(_arguments), std::make_shared<Sort>(_kind)) {}
 

libsmtutil/Z3CHCInterface.cpp

@@ -161,7 +161,7 @@ CHCSolverInterface::CexGraph Z3CHCInterface::cexGraph(z3::expr const& _proof)
 	proofStack.push(_proof.arg(0));
 
 	auto const& root = proofStack.top();
-	graph.nodes[root.id()] = {name(fact(root)), arguments(fact(root))};
+	graph.nodes.emplace(root.id(), m_z3Interface->fromZ3Expr(fact(root)));
 
 	set<unsigned> visited;
 	visited.insert(root.id());
@@ -186,7 +186,7 @@ CHCSolverInterface::CexGraph Z3CHCInterface::cexGraph(z3::expr const& _proof)
 
 				if (!graph.nodes.count(child.id()))
 				{
-					graph.nodes[child.id()] = {name(fact(child)), arguments(fact(child))};
+					graph.nodes.emplace(child.id(), m_z3Interface->fromZ3Expr(fact(child)));
 					graph.edges[child.id()] = {};
 				}
 

libsmtutil/Z3Interface.cpp

@@ -18,10 +18,14 @@
 
 #include <libsmtutil/Z3Interface.h>
 
+#include <libsolutil/CommonData.h>
 #include <libsolutil/CommonIO.h>
 
+#include <z3_api.h>
+
 using namespace std;
 using namespace solidity::smtutil;
+using namespace solidity::util;
 
 Z3Interface::Z3Interface():
 	m_solver(m_context)
@@ -243,6 +247,82 @@ z3::expr Z3Interface::toZ3Expr(Expression const& _expr)
 	smtAssert(false, "");
 }
 
+Expression Z3Interface::fromZ3Expr(z3::expr const& _expr)
+{
+	auto sort = fromZ3Sort(_expr.get_sort());
+	if (_expr.is_const() || _expr.is_var())
+		return Expression(_expr.to_string(), {}, sort);
+
+	smtAssert(_expr.is_app(), "");
+	vector<Expression> arguments;
+	for (unsigned i = 0; i < _expr.num_args(); ++i)
+		arguments.push_back(fromZ3Expr(_expr.arg(i)));
+
+	auto kind = _expr.decl().decl_kind();
+	if (_expr.is_ite())
+		return Expression::ite(arguments[0], arguments[1], arguments[2]);
+	else if (_expr.is_not())
+		return !arguments[0];
+	else if (_expr.is_and())
+		return arguments[0] && arguments[1];
+	else if (_expr.is_or())
+		return arguments[0] || arguments[1];
+	else if (_expr.is_implies())
+		return Expression::implies(arguments[0], arguments[1]);
+	else if (_expr.is_eq())
+		return arguments[0] == arguments[1];
+	else if (kind == Z3_OP_ULT || kind == Z3_OP_SLT)
+		return arguments[0] < arguments[1];
+	else if (kind == Z3_OP_ULEQ || kind == Z3_OP_SLEQ)
+		return arguments[0] <= arguments[1];
+	else if (kind == Z3_OP_GT || kind == Z3_OP_SGT)
+		return arguments[0] > arguments[1];
+	else if (kind == Z3_OP_UGEQ || kind == Z3_OP_SGEQ)
+		return arguments[0] >= arguments[1];
+	else if (kind == Z3_OP_ADD)
+		return arguments[0] + arguments[1];
+	else if (kind == Z3_OP_SUB)
+		return arguments[0] - arguments[1];
+	else if (kind == Z3_OP_MUL)
+		return arguments[0] * arguments[1];
+	else if (kind == Z3_OP_DIV)
+		return arguments[0] / arguments[1];
+	else if (kind == Z3_OP_MOD)
+		return arguments[0] % arguments[1];
+	else if (kind == Z3_OP_XOR)
+		return arguments[0] ^ arguments[1];
+	else if (kind == Z3_OP_BSHL)
+		return arguments[0] << arguments[1];
+	else if (kind == Z3_OP_BLSHR)
+		return arguments[0] >> arguments[1];
+	else if (kind == Z3_OP_BASHR)
+		return Expression::ashr(arguments[0], arguments[1]);
+	else if (kind == Z3_OP_INT2BV)
+		smtAssert(false, "");
+	else if (kind == Z3_OP_BV2INT)
+		smtAssert(false, "");
+	else if (kind == Z3_OP_SELECT)
+		return Expression::select(arguments[0], arguments[1]);
+	else if (kind == Z3_OP_STORE)
+		return Expression::store(arguments[0], arguments[1], arguments[2]);
+	else if (kind == Z3_OP_CONST_ARRAY)
+	{
+		auto sortSort = make_shared<SortSort>(fromZ3Sort(_expr.get_sort()));
+		return Expression::const_array(Expression(sortSort), arguments[0]);
+	}
+	else if (kind == Z3_OP_DT_CONSTRUCTOR)
+	{
+		auto sortSort = make_shared<SortSort>(fromZ3Sort(_expr.get_sort()));
+		return Expression::tuple_constructor(Expression(sortSort), arguments);
+	}
+	else if (kind == Z3_OP_DT_ACCESSOR)
+		smtAssert(false, "");
+	else if (kind == Z3_OP_UNINTERPRETED)
+		return Expression(_expr.decl().name().str(), arguments, fromZ3Sort(_expr.get_sort()));
+
+	smtAssert(false, "");
+}
+
 z3::sort Z3Interface::z3Sort(Sort const& _sort)
 {
 	switch (_sort.kind)
@@ -295,3 +375,35 @@ z3::sort_vector Z3Interface::z3Sort(vector<SortPointer> const& _sorts)
 		z3Sorts.push_back(z3Sort(*_sort));
 	return z3Sorts;
 }
+
+SortPointer Z3Interface::fromZ3Sort(z3::sort const& _sort)
+{
+	if (_sort.is_bool())
+		return SortProvider::boolSort;
+	if (_sort.is_int())
+		return SortProvider::sintSort;
+	if (_sort.is_bv())
+		return make_shared<BitVectorSort>(_sort.bv_size());
+	if (_sort.is_array())
+		return make_shared<ArraySort>(fromZ3Sort(_sort.array_domain()), fromZ3Sort(_sort.array_range()));
+	if (_sort.is_datatype())
+	{
+		auto name = _sort.name().str();
+		auto constructor = z3::func_decl(m_context, Z3_get_tuple_sort_mk_decl(m_context, _sort));
+		vector<string> memberNames;
+		vector<SortPointer> memberSorts;
+		for (unsigned i = 0; i < constructor.arity(); ++i)
+		{
+			auto accessor = z3::func_decl(m_context, Z3_get_tuple_sort_field_decl(m_context, _sort, i));
+			memberNames.push_back(accessor.name().str());
+			memberSorts.push_back(fromZ3Sort(accessor.range()));
+		}
+		return make_shared<TupleSort>(name, memberNames, memberSorts);
+	}
+	smtAssert(false, "");
+}
+
+vector<SortPointer> Z3Interface::fromZ3Sort(z3::sort_vector const& _sorts)
+{
+	return applyMap(_sorts, [this](auto const& sort) { return fromZ3Sort(sort); });
+}

libsmtutil/Z3Interface.h

@@ -41,6 +41,7 @@ public:
 	std::pair<CheckResult, std::vector<std::string>> check(std::vector<Expression> const& _expressionsToEvaluate) override;
 
 	z3::expr toZ3Expr(Expression const& _expr);
+	smtutil::Expression fromZ3Expr(z3::expr const& _expr);
 
 	std::map<std::string, z3::expr> constants() const { return m_constants; }
 	std::map<std::string, z3::func_decl> functions() const { return m_functions; }
@@ -56,6 +57,8 @@ private:
 
 	z3::sort z3Sort(Sort const& _sort);
 	z3::sort_vector z3Sort(std::vector<SortPointer> const& _sorts);
+	smtutil::SortPointer fromZ3Sort(z3::sort const& _sort);
+	std::vector<smtutil::SortPointer> fromZ3Sort(z3::sort_vector const& _sorts);
 
 	z3::context m_context;
 	z3::solver m_solver;

libsolidity/codegen/YulUtilFunctions.cpp

@@ -2314,7 +2314,7 @@ string YulUtilFunctions::updateStorageValueFunction(
 							structMembers[i].type->stackItems().size()
 						));
 						t("dynamicallyEncodedMember", structMembers[i].type->isDynamicallyEncoded());
-						if (structMembers[i].type->isDynamicallySized())
+						if (structMembers[i].type->isDynamicallyEncoded())
 							t("accessCalldataTail", accessCalldataTailFunction(*structMembers[i].type));
 					}
 					t("isValueType", structMembers[i].type->isValueType());

libsolidity/formal/CHC.cpp

@@ -1306,7 +1306,7 @@ optional<string> CHC::generateCounterexample(CHCSolverInterface::CexGraph const&
 {
 	optional<unsigned> rootId;
 	for (auto const& [id, node]: _graph.nodes)
-		if (node.first == _root)
+		if (node.name == _root)
 		{
 			rootId = id;
 			break;
@@ -1330,18 +1330,18 @@ optional<string> CHC::generateCounterexample(CHCSolverInterface::CexGraph const&
 		if (edges.size() == 2)
 		{
 			interfaceId = edges.at(1);
-			if (!Predicate::predicate(_graph.nodes.at(summaryId).first)->isSummary())
+			if (!Predicate::predicate(_graph.nodes.at(summaryId).name)->isSummary())
 				swap(summaryId, *interfaceId);
-			auto interfacePredicate = Predicate::predicate(_graph.nodes.at(*interfaceId).first);
+			auto interfacePredicate = Predicate::predicate(_graph.nodes.at(*interfaceId).name);
 			solAssert(interfacePredicate && interfacePredicate->isInterface(), "");
 		}
 		/// The children are unordered, so we need to check which is the summary and
 		/// which is the interface.
 
-		Predicate const* summaryPredicate = Predicate::predicate(_graph.nodes.at(summaryId).first);
+		Predicate const* summaryPredicate = Predicate::predicate(_graph.nodes.at(summaryId).name);
 		solAssert(summaryPredicate && summaryPredicate->isSummary(), "");
 		/// At this point property 2 from the function description is verified for this node.
-		auto summaryArgs = _graph.nodes.at(summaryId).second;
+		vector<smtutil::Expression> summaryArgs = _graph.nodes.at(summaryId).arguments;
 
 		FunctionDefinition const* calledFun = summaryPredicate->programFunction();
 		ContractDefinition const* calledContract = summaryPredicate->programContract();
@@ -1387,7 +1387,7 @@ optional<string> CHC::generateCounterexample(CHCSolverInterface::CexGraph const&
 		/// or stop.
 		if (interfaceId)
 		{
-			Predicate const* interfacePredicate = Predicate::predicate(_graph.nodes.at(*interfaceId).first);
+			Predicate const* interfacePredicate = Predicate::predicate(_graph.nodes.at(*interfaceId).name);
 			solAssert(interfacePredicate && interfacePredicate->isInterface(), "");
 			node = *interfaceId;
 		}
@@ -1403,7 +1403,14 @@ string CHC::cex2dot(CHCSolverInterface::CexGraph const& _cex)
 	string dot = "digraph {\n";
 
 	auto pred = [&](CHCSolverInterface::CexNode const& _node) {
-		return "\"" + _node.first + "(" + boost::algorithm::join(_node.second, ", ") + ")\"";
+		vector<string> args = applyMap(
+			_node.arguments,
+			[&](auto const& arg) {
+				solAssert(arg.arguments.empty(), "");
+				return arg.name;
+			}
+		);
+		return "\"" + _node.name + "(" + boost::algorithm::join(args, ", ") + ")\"";
 	};
 
 	for (auto const& [u, vs]: _cex.edges)

libsolidity/formal/CHC.h

@@ -203,7 +203,7 @@ private:
 
 	/// @returns a set of pairs _var = _value separated by _separator.
 	template <typename T>
-	std::string formatVariableModel(std::vector<T> const& _variables, std::vector<std::string> const& _values, std::string const& _separator) const
+	std::string formatVariableModel(std::vector<T> const& _variables, std::vector<std::optional<std::string>> const& _values, std::string const& _separator) const
 	{
 		solAssert(_variables.size() == _values.size(), "");
 
@@ -211,8 +211,8 @@ private:
 		for (unsigned i = 0; i < _values.size(); ++i)
 		{
 			auto var = _variables.at(i);
-			if (var && var->type()->isValueType())
+			if (var && _values.at(i))
-				assignments.emplace_back(var->name() + " = " + _values.at(i));
+				assignments.emplace_back(var->name() + " = " + *_values.at(i));
 		}
 
 		return boost::algorithm::join(assignments, _separator);

libsolidity/formal/Predicate.cpp

@@ -149,7 +149,7 @@ bool Predicate::isInterface() const
 	return functor().name.rfind("interface", 0) == 0;
 }
 
-string Predicate::formatSummaryCall(vector<string> const& _args) const
+string Predicate::formatSummaryCall(vector<smtutil::Expression> const& _args) const
 {
 	if (programContract())
 		return "constructor()";
@@ -163,18 +163,19 @@ string Predicate::formatSummaryCall(vector<string> const& _args) const
 
 	/// The signature of a function summary predicate is: summary(error, this, cryptoFunctions, txData, preBlockChainState, preStateVars, preInputVars, postBlockchainState, postStateVars, postInputVars, outputVars).
 	/// Here we are interested in preInputVars.
-	vector<string>::const_iterator first = _args.begin() + 5 + static_cast<int>(stateVars->size());
+	auto first = _args.begin() + 5 + static_cast<int>(stateVars->size());
-	vector<string>::const_iterator last = first + static_cast<int>(fun->parameters().size());
+	auto last = first + static_cast<int>(fun->parameters().size());
 	solAssert(first >= _args.begin() && first <= _args.end(), "");
 	solAssert(last >= _args.begin() && last <= _args.end(), "");
-	vector<string> functionArgsCex(first, last);
+	auto inTypes = FunctionType(*fun).parameterTypes();
+	vector<optional<string>> functionArgsCex = formatExpressions(vector<smtutil::Expression>(first, last), inTypes);
 	vector<string> functionArgs;
 
 	auto const& params = fun->parameters();
 	solAssert(params.size() == functionArgsCex.size(), "");
 	for (unsigned i = 0; i < params.size(); ++i)
-		if (params[i]->type()->isValueType())
+		if (params.at(i) && functionArgsCex.at(i))
-			functionArgs.emplace_back(functionArgsCex[i]);
+			functionArgs.emplace_back(*functionArgsCex.at(i));
 		else
 			functionArgs.emplace_back(params[i]->name());
 
@@ -186,7 +187,7 @@ string Predicate::formatSummaryCall(vector<string> const& _args) const
 
 }
 
-vector<string> Predicate::summaryStateValues(vector<string> const& _args) const
+vector<optional<string>> Predicate::summaryStateValues(vector<smtutil::Expression> const& _args) const
 {
 	/// The signature of a function summary predicate is: summary(error, this, cryptoFunctions, txData, preBlockchainState, preStateVars, preInputVars, postBlockchainState, postStateVars, postInputVars, outputVars).
 	/// The signature of an implicit constructor summary predicate is: summary(error, this, cryptoFunctions, txData, preBlockchainState, postBlockchainState, postStateVars).
@@ -194,8 +195,8 @@ vector<string> Predicate::summaryStateValues(vector<string> const& _args) const
 	auto stateVars = stateVariables();
 	solAssert(stateVars.has_value(), "");
 
-	vector<string>::const_iterator stateFirst;
+	vector<smtutil::Expression>::const_iterator stateFirst;
-	vector<string>::const_iterator stateLast;
+	vector<smtutil::Expression>::const_iterator stateLast;
 	if (auto const* function = programFunction())
 	{
 		stateFirst = _args.begin() + 5 + static_cast<int>(stateVars->size()) + static_cast<int>(function->parameters().size()) + 1;
@@ -212,12 +213,13 @@ vector<string> Predicate::summaryStateValues(vector<string> const& _args) const
 	solAssert(stateFirst >= _args.begin() && stateFirst <= _args.end(), "");
 	solAssert(stateLast >= _args.begin() && stateLast <= _args.end(), "");
 
-	vector<string> stateArgs(stateFirst, stateLast);
+	vector<smtutil::Expression> stateArgs(stateFirst, stateLast);
 	solAssert(stateArgs.size() == stateVars->size(), "");
-	return stateArgs;
+	auto stateTypes = applyMap(*stateVars, [&](auto const& _var) { return _var->type(); });
+	return formatExpressions(stateArgs, stateTypes);
 }
 
-vector<string> Predicate::summaryPostInputValues(vector<string> const& _args) const
+vector<optional<string>> Predicate::summaryPostInputValues(vector<smtutil::Expression> const& _args) const
 {
 	/// The signature of a function summary predicate is: summary(error, this, cryptoFunctions, txData, preBlockchainState, preStateVars, preInputVars, postBlockchainState, postStateVars, postInputVars, outputVars).
 	/// Here we are interested in postInputVars.
@@ -229,18 +231,19 @@ vector<string> Predicate::summaryPostInputValues(vector<string> const& _args) co
 
 	auto const& inParams = function->parameters();
 
-	vector<string>::const_iterator first = _args.begin() + 5 + static_cast<int>(stateVars->size()) * 2 + static_cast<int>(inParams.size()) + 1;
+	auto first = _args.begin() + 5 + static_cast<int>(stateVars->size()) * 2 + static_cast<int>(inParams.size()) + 1;
-	vector<string>::const_iterator last = first + static_cast<int>(inParams.size());
+	auto last = first + static_cast<int>(inParams.size());
 
 	solAssert(first >= _args.begin() && first <= _args.end(), "");
 	solAssert(last >= _args.begin() && last <= _args.end(), "");
 
-	vector<string> inValues(first, last);
+	vector<smtutil::Expression> inValues(first, last);
 	solAssert(inValues.size() == inParams.size(), "");
-	return inValues;
+	auto inTypes = FunctionType(*function).parameterTypes();
+	return formatExpressions(inValues, inTypes);
 }
 
-vector<string> Predicate::summaryPostOutputValues(vector<string> const& _args) const
+vector<optional<string>> Predicate::summaryPostOutputValues(vector<smtutil::Expression> const& _args) const
 {
 	/// The signature of a function summary predicate is: summary(error, this, cryptoFunctions, txData, preBlockchainState, preStateVars, preInputVars, postBlockchainState, postStateVars, postInputVars, outputVars).
 	/// Here we are interested in outputVars.
@@ -252,11 +255,116 @@ vector<string> Predicate::summaryPostOutputValues(vector<string> const& _args) c
 
 	auto const& inParams = function->parameters();
 
-	vector<string>::const_iterator first = _args.begin() + 5 + static_cast<int>(stateVars->size()) * 2 + static_cast<int>(inParams.size()) * 2 + 1;
+	auto first = _args.begin() + 5 + static_cast<int>(stateVars->size()) * 2 + static_cast<int>(inParams.size()) * 2 + 1;
 
 	solAssert(first >= _args.begin() && first <= _args.end(), "");
 
-	vector<string> outValues(first, _args.end());
+	vector<smtutil::Expression> outValues(first, _args.end());
 	solAssert(outValues.size() == function->returnParameters().size(), "");
-	return outValues;
+	auto outTypes = FunctionType(*function).returnParameterTypes();
+	return formatExpressions(outValues, outTypes);
+}
+
+vector<optional<string>> Predicate::formatExpressions(vector<smtutil::Expression> const& _exprs, vector<TypePointer> const& _types) const
+{
+	solAssert(_exprs.size() == _types.size(), "");
+	vector<optional<string>> strExprs;
+	for (unsigned i = 0; i < _exprs.size(); ++i)
+		strExprs.push_back(expressionToString(_exprs.at(i), _types.at(i)));
+	return strExprs;
+}
+
+optional<string> Predicate::expressionToString(smtutil::Expression const& _expr, TypePointer _type) const
+{
+	if (smt::isNumber(*_type))
+	{
+		solAssert(_expr.sort->kind == Kind::Int, "");
+		solAssert(_expr.arguments.empty(), "");
+		// TODO assert that _expr.name is a number.
+		return _expr.name;
+	}
+	if (smt::isBool(*_type))
+	{
+		solAssert(_expr.sort->kind == Kind::Bool, "");
+		solAssert(_expr.arguments.empty(), "");
+		solAssert(_expr.name == "true" || _expr.name == "false", "");
+		return _expr.name;
+	}
+	if (smt::isFunction(*_type))
+	{
+		solAssert(_expr.arguments.empty(), "");
+		return _expr.name;
+	}
+	if (smt::isArray(*_type))
+	{
+		auto const& arrayType = dynamic_cast<ArrayType const&>(*_type);
+		solAssert(_expr.name == "tuple_constructor", "");
+		auto const& tupleSort = dynamic_cast<TupleSort const&>(*_expr.sort);
+		solAssert(tupleSort.components.size() == 2, "");
+
+		auto length = stoul(_expr.arguments.at(1).name);
+		// Limit this counterexample size to 1k.
+		// Some OSs give you "unlimited" memory through swap and other virtual memory,
+		// so purely relying on bad_alloc being thrown is not a good idea.
+		// In that case, the array allocation might cause OOM and the program is killed.
+		if (length >= 1024)
+			return {};
+		try
+		{
+			vector<string> array(length);
+			if (!fillArray(_expr.arguments.at(0), array, arrayType))
+				return {};
+			return "[" + boost::algorithm::join(array, ", ") + "]";
+		}
+		catch (bad_alloc const&)
+		{
+			// Solver gave a concrete array but length is too large.
+		}
+	}
+
+	return {};
+}
+
+bool Predicate::fillArray(smtutil::Expression const& _expr, vector<string>& _array, ArrayType const& _type) const
+{
+	// Base case
+	if (_expr.name == "const_array")
+	{
+		auto length = _array.size();
+		optional<string> elemStr = expressionToString(_expr.arguments.at(1), _type.baseType());
+		if (!elemStr)
+			return false;
+		_array.clear();
+		_array.resize(length, *elemStr);
+		return true;
+	}
+
+	// Recursive case.
+	if (_expr.name == "store")
+	{
+		if (!fillArray(_expr.arguments.at(0), _array, _type))
+			return false;
+		optional<string> indexStr = expressionToString(_expr.arguments.at(1), TypeProvider::uint256());
+		if (!indexStr)
+			return false;
+		// Sometimes the solver assigns huge lengths that are not related,
+		// we should catch and ignore those.
+		unsigned index;
+		try
+		{
+			index = stoul(*indexStr);
+		}
+		catch (out_of_range const&)
+		{
+			return true;
+		}
+		optional<string> elemStr = expressionToString(_expr.arguments.at(2), _type.baseType());
+		if (!elemStr)
+			return false;
+		if (index < _array.size())
+			_array.at(index) = *elemStr;
+		return true;
+	}
+
+	solAssert(false, "");
 }

libsolidity/formal/Predicate.h

@@ -107,21 +107,33 @@ public:
 
 	/// @returns a formatted string representing a call to this predicate
 	/// with _args.
-	std::string formatSummaryCall(std::vector<std::string> const& _args) const;
+	std::string formatSummaryCall(std::vector<smtutil::Expression> const& _args) const;
 
 	/// @returns the values of the state variables from _args at the point
 	/// where this summary was reached.
-	std::vector<std::string> summaryStateValues(std::vector<std::string> const& _args) const;
+	std::vector<std::optional<std::string>> summaryStateValues(std::vector<smtutil::Expression> const& _args) const;
 
 	/// @returns the values of the function input variables from _args at the point
 	/// where this summary was reached.
-	std::vector<std::string> summaryPostInputValues(std::vector<std::string> const& _args) const;
+	std::vector<std::optional<std::string>> summaryPostInputValues(std::vector<smtutil::Expression> const& _args) const;
 
 	/// @returns the values of the function output variables from _args at the point
 	/// where this summary was reached.
-	std::vector<std::string> summaryPostOutputValues(std::vector<std::string> const& _args) const;
+	std::vector<std::optional<std::string>> summaryPostOutputValues(std::vector<smtutil::Expression> const& _args) const;
 
 private:
+	/// @returns the formatted version of the given SMT expressions. Those expressions must be SMT constants.
+	std::vector<std::optional<std::string>> formatExpressions(std::vector<smtutil::Expression> const& _exprs, std::vector<TypePointer> const& _types) const;
+
+	/// @returns a string representation of the SMT expression based on a Solidity type.
+	std::optional<std::string> expressionToString(smtutil::Expression const& _expr, TypePointer _type) const;
+
+	/// Recursively fills _array from _expr.
+	/// _expr should have the form `store(store(...(const_array(x_0), i_0, e_0), i_m, e_m), i_k, e_k)`.
+	/// @returns true if the construction worked,
+	/// and false if at least one element could not be built.
+	bool fillArray(smtutil::Expression const& _expr, std::vector<std::string>& _array, ArrayType const& _type) const;
+
 	/// The actual SMT expression.
 	smt::SymbolicFunctionVariable m_predicate;
 

libsolidity/formal/SMTEncoder.cpp

@@ -574,8 +574,8 @@ bool SMTEncoder::visit(Conditional const& _op)
 
 	defineExpr(_op, smtutil::Expression::ite(
 		expr(_op.condition()),
-		expr(_op.trueExpression()),
+		expr(_op.trueExpression(), _op.annotation().type),
-		expr(_op.falseExpression())
+		expr(_op.falseExpression(), _op.annotation().type)
 	));
 
 	return false;
@@ -1056,10 +1056,9 @@ bool SMTEncoder::visit(MemberAccess const& _memberAccess)
 
 	auto const& exprType = _memberAccess.expression().annotation().type;
 	solAssert(exprType, "");
-	auto identifier = dynamic_cast<Identifier const*>(&_memberAccess.expression());
 	if (exprType->category() == Type::Category::Magic)
 	{
-		if (identifier)
+		if (auto const* identifier = dynamic_cast<Identifier const*>(&_memberAccess.expression()))
 		{
 			auto const& name = identifier->name();
 			solAssert(name == "block" || name == "msg" || name == "tx", "");
@@ -1104,13 +1103,23 @@ bool SMTEncoder::visit(MemberAccess const& _memberAccess)
 	}
 	else if (exprType->category() == Type::Category::TypeType)
 	{
-		if (identifier && dynamic_cast<EnumDefinition const*>(identifier->annotation().referencedDeclaration))
+		auto const* decl = expressionToDeclaration(_memberAccess.expression());
+		if (dynamic_cast<EnumDefinition const*>(decl))
 		{
 			auto enumType = dynamic_cast<EnumType const*>(accessType);
 			solAssert(enumType, "");
 			defineExpr(_memberAccess, enumType->memberValue(_memberAccess.memberName()));
+
+			return false;
+		}
+		else if (dynamic_cast<ContractDefinition const*>(decl))
+		{
+			if (auto const* var = dynamic_cast<VariableDeclaration const*>(_memberAccess.annotation().referencedDeclaration))
+			{
+				defineExpr(_memberAccess, currentValue(*var));
+				return false;
+			}
 		}
-		return false;
 	}
 	else if (exprType->category() == Type::Category::Address)
 	{
@@ -1240,6 +1249,23 @@ void SMTEncoder::arrayAssignment()
 
 void SMTEncoder::indexOrMemberAssignment(Expression const& _expr, smtutil::Expression const& _rightHandSide)
 {
+	if (auto const* memberAccess = dynamic_cast<MemberAccess const*>(&_expr))
+	{
+		if (dynamic_cast<ContractDefinition const*>(expressionToDeclaration(memberAccess->expression())))
+		{
+			if (auto const* var = dynamic_cast<VariableDeclaration const*>(memberAccess->annotation().referencedDeclaration))
+			{
+				if (var->hasReferenceOrMappingType())
+					resetReferences(*var);
+
+				m_context.addAssertion(m_context.newValue(*var) == _rightHandSide);
+				m_context.expression(_expr)->increaseIndex();
+				defineExpr(_expr, currentValue(*var));
+				return;
+			}
+		}
+	}
+
 	auto toStore = _rightHandSide;
 	auto const* lastExpr = &_expr;
 	while (true)
@@ -1301,7 +1327,7 @@ void SMTEncoder::indexOrMemberAssignment(Expression const& _expr, smtutil::Expre
 
 			m_context.addAssertion(m_context.newValue(*varDecl) == toStore);
 			m_context.expression(*id)->increaseIndex();
-			defineExpr(*id,currentValue(*varDecl));
+			defineExpr(*id, currentValue(*varDecl));
 			break;
 		}
 		else
@@ -1622,7 +1648,8 @@ smtutil::Expression SMTEncoder::bitwiseOperation(
 			result = bvLeft << bvRight;
 			break;
 		case Token::SHR:
-			solAssert(false, "");
+			result = bvLeft >> bvRight;
+			break;
 		case Token::SAR:
 			result = isSigned ?
 				smtutil::Expression::ashr(bvLeft, bvRight) :
@@ -2282,16 +2309,25 @@ set<VariableDeclaration const*> SMTEncoder::touchedVariables(ASTNode const& _nod
 	return m_variableUsage.touchedVariables(_node, callStack);
 }
 
+Declaration const* SMTEncoder::expressionToDeclaration(Expression const& _expr)
+{
+	if (auto const* identifier = dynamic_cast<Identifier const*>(&_expr))
+		return identifier->annotation().referencedDeclaration;
+	if (auto const* outerMemberAccess = dynamic_cast<MemberAccess const*>(&_expr))
+		return outerMemberAccess->annotation().referencedDeclaration;
+	return nullptr;
+}
+
 VariableDeclaration const* SMTEncoder::identifierToVariable(Expression const& _expr)
 {
-	if (auto identifier = dynamic_cast<Identifier const*>(&_expr))
+	// We do not use `expressionToDeclaration` here because we are not interested in
-	{
+	// struct.field, for example.
-		if (auto decl = dynamic_cast<VariableDeclaration const*>(identifier->annotation().referencedDeclaration))
+	if (auto const* identifier = dynamic_cast<Identifier const*>(&_expr))
+		if (auto const* varDecl = dynamic_cast<VariableDeclaration const*>(identifier->annotation().referencedDeclaration))
 		{
-			solAssert(m_context.knownVariable(*decl), "");
+			solAssert(m_context.knownVariable(*varDecl), "");
-			return decl;
+			return varDecl;
 		}
-	}
 	return nullptr;
 }
 

libsolidity/formal/SMTEncoder.h

@@ -280,7 +280,11 @@ protected:
 	/// @returns variables that are touched in _node's subtree.
 	std::set<VariableDeclaration const*> touchedVariables(ASTNode const& _node);
 
-	/// @returns the VariableDeclaration referenced by an Identifier or nullptr.
+	/// @returns the declaration referenced by _expr, if any,
+	/// and nullptr otherwise.
+	Declaration const* expressionToDeclaration(Expression const& _expr);
+
+	/// @returns the VariableDeclaration referenced by an Expression or nullptr.
 	VariableDeclaration const* identifierToVariable(Expression const& _expr);
 
 	/// Creates symbolic expressions for the returned values

libsolidity/formal/SymbolicVariables.cpp

@@ -245,7 +245,25 @@ SymbolicTupleVariable::SymbolicTupleVariable(
 	solAssert(m_sort->kind == Kind::Tuple, "");
 }
 
-vector<SortPointer> const& SymbolicTupleVariable::components()
+smtutil::Expression SymbolicTupleVariable::currentValue(frontend::TypePointer const& _targetType) const
+{
+	if (!_targetType || sort() == smtSort(*_targetType))
+		return SymbolicVariable::currentValue();
+
+	auto thisTuple = dynamic_pointer_cast<TupleSort>(sort());
+	auto otherTuple = dynamic_pointer_cast<TupleSort>(smtSort(*_targetType));
+	solAssert(thisTuple && otherTuple, "");
+	solAssert(thisTuple->components.size() == otherTuple->components.size(), "");
+	vector<smtutil::Expression> args;
+	for (size_t i = 0; i < thisTuple->components.size(); ++i)
+		args.emplace_back(component(i, type(), _targetType));
+	return smtutil::Expression::tuple_constructor(
+		smtutil::Expression(make_shared<smtutil::SortSort>(smtSort(*_targetType)), ""),
+		args
+	);
+}
+
+vector<SortPointer> const& SymbolicTupleVariable::components() const
 {
 	auto tupleSort = dynamic_pointer_cast<TupleSort>(m_sort);
 	solAssert(tupleSort, "");
@@ -256,7 +274,7 @@ smtutil::Expression SymbolicTupleVariable::component(
 	size_t _index,
 	TypePointer _fromType,
 	TypePointer _toType
-)
+) const
 {
 	optional<smtutil::Expression> conversion = symbolicTypeConversion(_fromType, _toType);
 	if (conversion)

libsolidity/formal/SymbolicVariables.h

@@ -225,12 +225,14 @@ public:
 		EncodingContext& _context
 	);
 
-	std::vector<smtutil::SortPointer> const& components();
+	smtutil::Expression currentValue(frontend::TypePointer const& _targetType = TypePointer{}) const override;
+
+	std::vector<smtutil::SortPointer> const& components() const;
 	smtutil::Expression component(
 		size_t _index,
 		TypePointer _fromType = nullptr,
 		TypePointer _toType = nullptr
-	);
+	) const;
 };
 
 /**

libyul/AsmAnalysis.cpp

@@ -635,19 +635,18 @@ bool AsmAnalyzer::validateInstructions(evmasm::Instruction _instr, SourceLocatio
 		);
 	};
 
-	if ((
+	if (_instr == evmasm::Instruction::RETURNDATACOPY && !m_evmVersion.supportsReturndata())
-		_instr == evmasm::Instruction::RETURNDATACOPY ||
-		_instr == evmasm::Instruction::RETURNDATASIZE
-	) && !m_evmVersion.supportsReturndata())
 		errorForVM(7756_error, "only available for Byzantium-compatible");
+	else if (_instr == evmasm::Instruction::RETURNDATASIZE && !m_evmVersion.supportsReturndata())
+		errorForVM(4778_error, "only available for Byzantium-compatible");
 	else if (_instr == evmasm::Instruction::STATICCALL && !m_evmVersion.hasStaticCall())
 		errorForVM(1503_error, "only available for Byzantium-compatible");
-	else if ((
+	else if (_instr == evmasm::Instruction::SHL && !m_evmVersion.hasBitwiseShifting())
-		_instr == evmasm::Instruction::SHL ||
-		_instr == evmasm::Instruction::SHR ||
-		_instr == evmasm::Instruction::SAR
-	) && !m_evmVersion.hasBitwiseShifting())
 		errorForVM(6612_error, "only available for Constantinople-compatible");
+	else if (_instr == evmasm::Instruction::SHR && !m_evmVersion.hasBitwiseShifting())
+		errorForVM(7458_error, "only available for Constantinople-compatible");
+	else if (_instr == evmasm::Instruction::SAR && !m_evmVersion.hasBitwiseShifting())
+		errorForVM(2054_error, "only available for Constantinople-compatible");
 	else if (_instr == evmasm::Instruction::CREATE2 && !m_evmVersion.hasCreate2())
 		errorForVM(6166_error, "only available for Constantinople-compatible");
 	else if (_instr == evmasm::Instruction::EXTCODEHASH && !m_evmVersion.hasExtCodeHash())

libyul/backends/wasm/BinaryTransform.cpp

@@ -356,11 +356,15 @@ bytes BinaryTransform::operator()(BuiltinCall const& _call)
 	if (_call.functionName == "dataoffset")
 	{
 		string name = get<StringLiteral>(_call.arguments.at(0)).value;
+		// TODO: support the case where name refers to the current object
+		yulAssert(m_subModulePosAndSize.count(name), "");
 		return toBytes(Opcode::I64Const) + lebEncodeSigned(static_cast<int64_t>(m_subModulePosAndSize.at(name).first));
 	}
 	else if (_call.functionName == "datasize")
 	{
 		string name = get<StringLiteral>(_call.arguments.at(0)).value;
+		// TODO: support the case where name refers to the current object
+		yulAssert(m_subModulePosAndSize.count(name), "");
 		return toBytes(Opcode::I64Const) + lebEncodeSigned(static_cast<int64_t>(m_subModulePosAndSize.at(name).second));
 	}
 

libyul/backends/wasm/EVMToEwasmTranslator.cpp

@@ -1211,6 +1211,9 @@ function revert(x1, x2, x3, x4, y1, y2, y3, y4) {
 function invalid() {
 	unreachable()
 }
+function stop() {
+	eth.finish(0:i32, 0:i32)
+}
 function memoryguard(x:i64) -> y1, y2, y3, y4 {
 	y4 := x
 }

libyul/optimiser/SSAReverser.cpp

@@ -73,7 +73,7 @@ void SSAReverser::operator()(Block& _block)
 							VariableDeclaration{
 								std::move(varDecl->location),
 								std::move(varDecl->variables),
-								std::make_unique<Expression>(std::move(assignment->variableNames.front()))
+								std::make_unique<Expression>(assignment->variableNames.front())
 							}
 						);
 				}

test/libsolidity/semanticTests/array/copying/array_nested_calldata_to_storage.sol

@@ -1,16 +1,43 @@
 pragma experimental ABIEncoderV2;
 
 contract c {
-    uint256[][] a;
+    uint256[][] a1;
+    uint256[][2] a2;
+    uint256[2][] a3;
+    uint256[2][2] a4;
 
-    function test(uint256[][] calldata d) external returns (uint256, uint256) {
+    function test1(uint256[][] calldata c) external returns (uint256, uint256) {
-        a = d;
+        a1 = c;
-        assert(a[0][0] == d[0][0]);
+        assert(a1[0][0] == c[0][0]);
-        assert(a[0][1] == d[0][1]);
+        assert(a1[0][1] == c[0][1]);
-        return (a.length, a[1][0] + a[1][1]);
+        return (a1.length, a1[1][0] + a1[1][1]);
+    }
+
+    function test2(uint256[][2] calldata c) external returns (uint256, uint256) {
+        a2 = c;
+        assert(a2[0][0] == c[0][0]);
+        assert(a2[0][1] == c[0][1]);
+        return (a2[0].length, a2[1][0] + a2[1][1]);
+    }
+
+    function test3(uint256[2][] calldata c) external returns (uint256, uint256) {
+        a3 = c;
+        assert(a3[0][0] == c[0][0]);
+        assert(a3[0][1] == c[0][1]);
+        return (a3.length, a3[1][0] + a3[1][1]);
+    }
+
+    function test4(uint256[2][2] calldata c) external returns (uint256) {
+        a4 = c;
+        assert(a4[0][0] == c[0][0]);
+        assert(a4[0][1] == c[0][1]);
+        return (a4[1][0] + a4[1][1]);
     }
 }
 // ====
 // compileViaYul: true
 // ----
-// test(uint256[][]): 0x20, 2, 0x40, 0x40, 2, 23, 42 -> 2, 65
+// test1(uint256[][]): 0x20, 2, 0x40, 0x40, 2, 23, 42 -> 2, 65
+// test2(uint256[][2]): 0x20, 0x40, 0x40, 2, 23, 42 -> 2, 65
+// test3(uint256[2][]): 0x20, 2, 0x40, 0x40, 23, 42 -> 2, 65
+// test4(uint256[2][2]): 23, 42, 23, 42 -> 65

test/libsolidity/semanticTests/structs/calldata/calldata_struct_with_nested_array_to_storage.sol

@@ -0,0 +1,20 @@
+pragma experimental ABIEncoderV2;
+
+contract C {
+    struct S {
+        uint128 p1;
+        uint256[][2] a;
+        uint32 p2;
+    }
+    S s;
+    function f(uint32 p1, S calldata c) external returns(uint32, uint128, uint256, uint256, uint32) {
+        s = c;
+        assert(s.a[0][0] == c.a[0][0]);
+        assert(s.a[1][1] == c.a[1][1]);
+        return (p1, s.p1, s.a[0][0], s.a[1][1], s.p2);
+    }
+}
+// ====
+// compileViaYul: true
+// ----
+// f(uint32, (uint128, uint256[][2], uint32)): 55, 0x40, 77, 0x60, 88, 0x40, 0x40, 2, 1, 2 -> 55, 77, 1, 2, 88

test/libsolidity/smtCheckerTests/operators/assignment_contract_member_variable.sol

@@ -0,0 +1,30 @@
+pragma experimental SMTChecker;
+contract A {
+	int x;
+	int y;
+	function a() public {
+		require(A.x < 100);
+		A.y = A.x++;
+		assert(A.y == A.x - 1);
+		// Fails
+		assert(A.y == 0);
+		A.y = ++A.x;
+		assert(A.y == A.x);
+		delete A.x;
+		assert(A.x == 0);
+		A.y = A.x--;
+		assert(A.y == A.x + 1);
+		assert(A.y == 0);
+		A.y = --A.x;
+		assert(A.y == A.x);
+		A.x += 10;
+		// Fails
+		assert(A.y == 0);
+		assert(A.y + 10 == A.x);
+		A.x -= 10;
+		assert(A.y == A.x);
+	}
+}
+// ----
+// Warning 6328: (160-176): CHC: Assertion violation happens here.
+// Warning 6328: (373-389): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/operators/assignment_contract_member_variable_array.sol

@@ -0,0 +1,14 @@
+pragma experimental SMTChecker;
+contract A {
+	uint[] a;
+	function f() public {
+		A.a.push(2);
+		assert(A.a[A.a.length - 1] == 2);
+		A.a.pop();
+		// Fails
+		assert(A.a.length > 0);
+		assert(A.a.length == 0);
+	}
+}
+// ----
+// Warning 6328: (156-178): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/operators/assignment_module_contract_member_variable.sol

@@ -0,0 +1,31 @@
+==== Source: AASource ====
+pragma experimental SMTChecker;
+import "AASource" as AA;
+contract A {
+	int x;
+	int y;
+	function a() public {
+		require(A.x < 100);
+		AA.A.y = A.x++;
+		assert(A.y == AA.A.x - 1);
+		// Fails
+		assert(AA.A.y == 0);
+		A.y = ++AA.A.x;
+		assert(A.y == A.x);
+		delete AA.A.x;
+		assert(A.x == 0);
+		A.y = A.x--;
+		assert(AA.A.y == AA.A.x + 1);
+		A.y = --A.x;
+		assert(A.y == A.x);
+		AA.A.x += 10;
+		// Fails
+		assert(A.y == 0);
+		assert(A.y + 10 == A.x);
+		A.x -= 10;
+		assert(AA.A.y == A.x);
+	}
+}
+// ----
+// Warning 6328: (AASource:191-210): CHC: Assertion violation happens here.
+// Warning 6328: (AASource:402-418): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_uint_2.sol

@@ -7,9 +7,7 @@ contract C {
     function f(bool b) public {
         if (b)
             s.x[2] |= 1;
-        assert(s.x[2] != 1);
+		// Removed because of Spacer nondeterminism.
+        //assert(s.x[2] != 1);
     }
 }
-// ----
-// Warning 6328: (173-192): CHC: Assertion violation might happen here.
-// Warning 7812: (173-192): BMC: Assertion violation might happen here.

test/libsolidity/smtCheckerTests/operators/shifts/shr_unused.sol

@@ -0,0 +1,10 @@
+pragma experimental SMTChecker;
+
+contract C {
+	function f() public pure {
+		fixed x;
+		assert(x >>> 6 == 0);
+	}
+}
+// ----
+// UnimplementedFeatureError: Not yet implemented - FixedPointType.

test/libsolidity/smtCheckerTests/operators/tuple_rationals_conditional.sol

@@ -0,0 +1,11 @@
+pragma experimental SMTChecker;
+
+contract C {
+	function f(bool x) public pure {
+		(uint a, uint b) = x ? (10000000001, 2) : (3, 4);
+		assert(a != 0);
+		assert(b != 0);
+		assert(a % 2 == 1);
+		assert(b % 2 == 0);
+	}
+}

test/libsolidity/smtCheckerTests/types/array_static_mapping_aliasing_2.sol

@@ -17,7 +17,8 @@ contract C
 		// Should not fail since knowledge is erased only for mapping (uint => uint).
 		assert(severalMaps8[0][0] == 42);
 		// Should not fail since singleMap == severalMaps3d[0][0] is not possible.
-		assert(severalMaps3d[0][0][0] == 42);
+		// Removed because of Spacer nondeterminism.
+		//assert(severalMaps3d[0][0][0] == 42);
 		// Should fail since singleMap == map is possible.
 		assert(map[0] == 42);
 	}
@@ -26,4 +27,4 @@ contract C
 	}
 }
 // ----
-// Warning 6328: (781-801): CHC: Assertion violation happens here.
+// Warning 6328: (830-850): CHC: Assertion violation happens here.

test/libsolidity/syntaxTests/inlineAssembly/evm_byzantium_on_homestead.sol

@@ -14,7 +14,7 @@ contract C {
 // ====
 // EVMVersion: =homestead
 // ----
-// TypeError 7756: (86-100): The "returndatasize" instruction is only available for Byzantium-compatible VMs (you are currently compiling for "homestead").
+// TypeError 4778: (86-100): The "returndatasize" instruction is only available for Byzantium-compatible VMs (you are currently compiling for "homestead").
 // DeclarationError 3812: (77-102): Variable count mismatch: 1 variables and 0 values.
 // TypeError 7756: (115-129): The "returndatacopy" instruction is only available for Byzantium-compatible VMs (you are currently compiling for "homestead").
 // TypeError 1503: (245-255): The "staticcall" instruction is only available for Byzantium-compatible VMs (you are currently compiling for "homestead").

test/libsolidity/syntaxTests/inlineAssembly/evm_constantinople_on_byzantium.sol

@@ -17,9 +17,9 @@ contract C {
 // ----
 // TypeError 6612: (103-106): The "shl" instruction is only available for Constantinople-compatible VMs (you are currently compiling for "byzantium").
 // DeclarationError 8678: (96-116): Variable count does not match number of values (1 vs. 0)
-// TypeError 6612: (136-139): The "shr" instruction is only available for Constantinople-compatible VMs (you are currently compiling for "byzantium").
+// TypeError 7458: (136-139): The "shr" instruction is only available for Constantinople-compatible VMs (you are currently compiling for "byzantium").
 // DeclarationError 8678: (129-147): Variable count does not match number of values (1 vs. 0)
-// TypeError 6612: (167-170): The "sar" instruction is only available for Constantinople-compatible VMs (you are currently compiling for "byzantium").
+// TypeError 2054: (167-170): The "sar" instruction is only available for Constantinople-compatible VMs (you are currently compiling for "byzantium").
 // DeclarationError 8678: (160-178): Variable count does not match number of values (1 vs. 0)
 // TypeError 6166: (283-290): The "create2" instruction is only available for Constantinople-compatible VMs (you are currently compiling for "byzantium").
 // DeclarationError 8678: (276-302): Variable count does not match number of values (1 vs. 0)

test/libyul/ewasmTranslationTests/balance.yul

@@ -6,7 +6,7 @@
 // Trace:
 // Memory dump:
 //      0: 0000000000000000000000000000000000000000000000000000000000000001
-//     20: 0000000000000000000000000000000000000000000000000000000022222222
+//     20: 0000000000000000000000000000000022222222000000000000000000000000
 // Storage dump:
-//   0000000000000000000000000000000000000000000000000000000000000000: 0000000000000000000000000000000000000000000000000000000022222222
+//   0000000000000000000000000000000000000000000000000000000000000000: 0000000000000000000000000000000022222222000000000000000000000000
-//   0000000000000000000000000000000000000000000000000000000000000001: 0000000000000000000000000000000000000000000000000000000022222222
+//   0000000000000000000000000000000000000000000000000000000000000001: 0000000000000000000000000000000022222222000000000000000000000000

test/libyul/ewasmTranslationTests/callvalue.yul

@@ -4,6 +4,6 @@
 // ----
 // Trace:
 // Memory dump:
-//     20: 0000000000000000000000005555555500000000000000000000000000000000
+//     20: 5555555500000000000000000000000000000000000000000000000000000000
 // Storage dump:
-//   0000000000000000000000000000000000000000000000000000000000000000: 0000000000000000000000005555555500000000000000000000000000000000
+//   0000000000000000000000000000000000000000000000000000000000000000: 5555555500000000000000000000000000000000000000000000000000000000

test/libyul/ewasmTranslationTests/difficulty.yul

@@ -4,6 +4,6 @@
 // ----
 // Trace:
 // Memory dump:
-//     20: 0000000000000000000000000000000000000000000000000000000009999999
+//     20: 9999990900000000000000000000000000000000000000000000000000000000
 // Storage dump:
-//   0000000000000000000000000000000000000000000000000000000000000000: 0000000000000000000000000000000000000000000000000000000009999999
+//   0000000000000000000000000000000000000000000000000000000000000000: 9999990900000000000000000000000000000000000000000000000000000000

test/libyul/ewasmTranslationTests/extcodesize.yul

@@ -4,6 +4,6 @@
 // ----
 // Trace:
 // Memory dump:
-//     20: 000000000000000000000000000000000000000000000000000000000000077b
+//     20: 0000000000000000000000000000000000000000000000000000000000000dd6
 // Storage dump:
-//   0000000000000000000000000000000000000000000000000000000000000000: 000000000000000000000000000000000000000000000000000000000000077b
+//   0000000000000000000000000000000000000000000000000000000000000000: 0000000000000000000000000000000000000000000000000000000000000dd6

test/libyul/ewasmTranslationTests/gasprice.yul

@@ -4,6 +4,6 @@
 // ----
 // Trace:
 // Memory dump:
-//     20: 0000000000000000000000006666666600000000000000000000000000000000
+//     20: 6666666600000000000000000000000000000000000000000000000000000000
 // Storage dump:
-//   0000000000000000000000000000000000000000000000000000000000000000: 0000000000000000000000006666666600000000000000000000000000000000
+//   0000000000000000000000000000000000000000000000000000000000000000: 6666666600000000000000000000000000000000000000000000000000000000

test/tools/yulInterpreter/EwasmBuiltinInterpreter.cpp

@@ -35,6 +35,7 @@ using namespace solidity;
 using namespace solidity::yul;
 using namespace solidity::yul::test;
 
+using solidity::util::h160;
 using solidity::util::h256;
 
 namespace
@@ -297,9 +298,7 @@ u256 EwasmBuiltinInterpreter::evalEthBuiltin(string const& _fun, vector<uint64_t
 	}
 	else if (_fun == "getExternalBalance")
 	{
-		// TODO this does not read the address, but is consistent with
+		readAddress(arg[0]);
-		// EVM interpreter implementation.
-		// If we take the address into account, this needs to use readAddress.
 		writeU128(arg[1], m_state.balance);
 		return 0;
 	}
@@ -309,14 +308,15 @@ u256 EwasmBuiltinInterpreter::evalEthBuiltin(string const& _fun, vector<uint64_t
 			return 1;
 		else
 		{
-			writeU256(arg[1], 0xaaaaaaaa + u256(arg[0] - m_state.blockNumber - 256));
+			writeBytes32(arg[1], h256(0xaaaaaaaa + u256(arg[0] - m_state.blockNumber - 256)));
 			return 0;
 		}
 	}
 	else if (_fun == "call")
 	{
-		// TODO read args from memory
+		readAddress(arg[1]);
-		// TODO use readAddress to read address.
+		readU128(arg[2]);
+		accessMemory(arg[3], arg[4]);
 		logTrace(evmasm::Instruction::CALL, {});
 		return arg[0] & 1;
 	}
@@ -335,38 +335,38 @@ u256 EwasmBuiltinInterpreter::evalEthBuiltin(string const& _fun, vector<uint64_t
 		return m_state.calldata.size();
 	else if (_fun == "callCode")
 	{
-		// TODO read args from memory
+		readAddress(arg[1]);
-		// TODO use readAddress to read address.
+		readU128(arg[2]);
+		accessMemory(arg[3], arg[4]);
 		logTrace(evmasm::Instruction::CALLCODE, {});
 		return arg[0] & 1;
 	}
 	else if (_fun == "callDelegate")
 	{
-		// TODO read args from memory
+		readAddress(arg[1]);
-		// TODO use readAddress to read address.
+		accessMemory(arg[2], arg[3]);
 		logTrace(evmasm::Instruction::DELEGATECALL, {});
 		return arg[0] & 1;
 	}
 	else if (_fun == "callStatic")
 	{
-		// TODO read args from memory
+		readAddress(arg[1]);
-		// TODO use readAddress to read address.
+		accessMemory(arg[2], arg[3]);
 		logTrace(evmasm::Instruction::STATICCALL, {});
 		return arg[0] & 1;
 	}
 	else if (_fun == "storageStore")
 	{
-		m_state.storage[h256(readU256(arg[0]))] = readU256((arg[1]));
+		m_state.storage[readBytes32(arg[0])] = readBytes32(arg[1]);
 		return 0;
 	}
 	else if (_fun == "storageLoad")
 	{
-		writeU256(arg[1], m_state.storage[h256(readU256(arg[0]))]);
+		writeBytes32(arg[1], m_state.storage[readBytes32(arg[0])]);
 		return 0;
 	}
 	else if (_fun == "getCaller")
 	{
-		// TODO should this only write 20 bytes?
 		writeAddress(arg[0], m_state.caller);
 		return 0;
 	}
@@ -393,10 +393,11 @@ u256 EwasmBuiltinInterpreter::evalEthBuiltin(string const& _fun, vector<uint64_t
 	}
 	else if (_fun == "create")
 	{
-		// TODO access memory
+		readU128(arg[0]);
-		// TODO use writeAddress to store resulting address
+		accessMemory(arg[1], arg[2]);
 		logTrace(evmasm::Instruction::CREATE, {});
-		return 0xcccccc + arg[1];
+		writeAddress(arg[3], h160(h256(0xcccccc + arg[1])));
+		return 1;
 	}
 	else if (_fun == "getBlockDifficulty")
 	{
@@ -405,7 +406,7 @@ u256 EwasmBuiltinInterpreter::evalEthBuiltin(string const& _fun, vector<uint64_t
 	}
 	else if (_fun == "externalCodeCopy")
 	{
-		// TODO use readAddress to read address.
+		readAddress(arg[0]);
 		if (accessMemory(arg[1], arg[3]))
 			// TODO this way extcodecopy and codecopy do the same thing.
 			copyZeroExtended(
@@ -415,8 +416,8 @@ u256 EwasmBuiltinInterpreter::evalEthBuiltin(string const& _fun, vector<uint64_t
 		return 0;
 	}
 	else if (_fun == "getExternalCodeSize")
-		// Generate "random" code length. Make sure it fits the page size.
+		// Generate "random" code length.
-		return u256(keccak256(h256(readAddress(arg[0])))) & 0xfff;
+		return uint32_t(u256(keccak256(h256(readAddress(arg[0])))) & 0xfff);
 	else if (_fun == "getGasLeft")
 		return 0x99;
 	else if (_fun == "getBlockGasLimit")
@@ -428,9 +429,18 @@ u256 EwasmBuiltinInterpreter::evalEthBuiltin(string const& _fun, vector<uint64_t
 	}
 	else if (_fun == "log")
 	{
+		accessMemory(arg[0], arg[1]);
 		uint64_t numberOfTopics = arg[2];
 		if (numberOfTopics > 4)
 			throw ExplicitlyTerminated();
+		if (numberOfTopics > 0)
+			readBytes32(arg[3]);
+		if (numberOfTopics > 1)
+			readBytes32(arg[4]);
+		if (numberOfTopics > 2)
+			readBytes32(arg[5]);
+		if (numberOfTopics > 3)
+			readBytes32(arg[6]);
 		logTrace(evmasm::logInstruction(numberOfTopics), {});
 		return 0;
 	}
@@ -472,7 +482,7 @@ u256 EwasmBuiltinInterpreter::evalEthBuiltin(string const& _fun, vector<uint64_t
 	}
 	else if (_fun == "selfDestruct")
 	{
-		// TODO use readAddress to read address.
+		readAddress(arg[0]);
 		logTrace(evmasm::Instruction::SELFDESTRUCT, {});
 		throw ExplicitlyTerminated();
 	}
@@ -523,6 +533,12 @@ uint32_t EwasmBuiltinInterpreter::readMemoryHalfWord(uint64_t _offset)
 	return r;
 }
 
+void EwasmBuiltinInterpreter::writeMemory(uint64_t _offset, bytes const& _value)
+{
+	for (size_t i = 0; i < _value.size(); i++)
+		m_state.memory[_offset + i] = _value[i];
+}
+
 void EwasmBuiltinInterpreter::writeMemoryWord(uint64_t _offset, uint64_t _value)
 {
 	for (size_t i = 0; i < 8; i++)
@@ -545,7 +561,7 @@ void EwasmBuiltinInterpreter::writeU256(uint64_t _offset, u256 _value, size_t _c
 	accessMemory(_offset, _croppedTo);
 	for (size_t i = 0; i < _croppedTo; i++)
 	{
-		m_state.memory[_offset + _croppedTo - 1 - i] = uint8_t(_value & 0xff);
+		m_state.memory[_offset + i] = uint8_t(_value & 0xff);
 		_value >>= 8;
 	}
 }
@@ -553,9 +569,9 @@ void EwasmBuiltinInterpreter::writeU256(uint64_t _offset, u256 _value, size_t _c
 u256 EwasmBuiltinInterpreter::readU256(uint64_t _offset, size_t _croppedTo)
 {
 	accessMemory(_offset, _croppedTo);
-	u256 value;
+	u256 value{0};
 	for (size_t i = 0; i < _croppedTo; i++)
-		value = (value << 8) | m_state.memory[_offset + i];
+		value = (value << 8) | m_state.memory[_offset + _croppedTo - 1 - i];
 
 	return value;
 }

test/tools/yulInterpreter/EwasmBuiltinInterpreter.h

@@ -24,6 +24,7 @@
 #include <libyul/AsmDataForward.h>
 
 #include <libsolutil/CommonData.h>
+#include <libsolutil/FixedHash.h>
 
 #include <vector>
 
@@ -61,6 +62,8 @@ struct InterpreterState;
  *
  * The main focus is that the generated execution trace is the same for equivalent executions
  * and likely to be different for non-equivalent executions.
+ *
+ * The type names are following the Ewasm specification (https://github.com/ewasm/design/blob/master/eth_interface.md).
  */
 class EwasmBuiltinInterpreter
 {
@@ -99,6 +102,9 @@ private:
 	/// @returns the memory contents (4 bytes) at the provided address (little-endian).
 	/// Does not adjust msize, use @a accessMemory for that
 	uint32_t readMemoryHalfWord(uint64_t _offset);
+	/// Writes bytes to memory.
+	/// Does not adjust msize, use @a accessMemory for that
+	void writeMemory(uint64_t _offset, bytes const& _value);
 	/// Writes a word to memory (little-endian)
 	/// Does not adjust msize, use @a accessMemory for that
 	void writeMemoryWord(uint64_t _offset, uint64_t _value);
@@ -109,14 +115,18 @@ private:
 	/// Does not adjust msize, use @a accessMemory for that
 	void writeMemoryByte(uint64_t _offset, uint8_t _value);
 
-	/// Helper for eth.* builtins. Writes to memory (big-endian) and always returns zero.
+	/// Helper for eth.* builtins. Writes to memory (little-endian) and always returns zero.
 	void writeU256(uint64_t _offset, u256 _value, size_t _croppedTo = 32);
 	void writeU128(uint64_t _offset, u256 _value) { writeU256(_offset, std::move(_value), 16); }
-	void writeAddress(uint64_t _offset, u256 _value) { writeU256(_offset, std::move(_value), 20); }
+	/// Helper for eth.* builtins. Writes to memory (as a byte string).
-	/// Helper for eth.* builtins. Reads from memory (big-endian) and returns the value;
+	void writeBytes32(uint64_t _offset, util::h256 _value) { accessMemory(_offset, 32); writeMemory(_offset, _value.asBytes()); }
+	void writeAddress(uint64_t _offset, util::h160 _value) { accessMemory(_offset, 20); writeMemory(_offset, _value.asBytes()); }
+	/// Helper for eth.* builtins. Reads from memory (little-endian) and returns the value.
 	u256 readU256(uint64_t _offset, size_t _croppedTo = 32);
 	u256 readU128(uint64_t _offset) { return readU256(_offset, 16); }
-	u256 readAddress(uint64_t _offset) { return readU256(_offset, 20); }
+	/// Helper for eth.* builtins. Reads from memory (as a byte string).
+	util::h256 readBytes32(uint64_t _offset) { accessMemory(_offset, 32); return util::h256(readMemory(_offset, 32)); }
+	util::h160 readAddress(uint64_t _offset) { accessMemory(_offset, 20); return util::h160(readMemory(_offset, 20)); }
 
 	void logTrace(evmasm::Instruction _instruction, std::vector<u256> const& _arguments = {}, bytes const& _data = {});
 	/// Appends a log to the trace representing an instruction or similar operation by string,