Format array cex

libsolidity/formal/CHC.h

@@ -211,11 +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))
-			{
-				solAssert(_values.at(i), "");
 				assignments.emplace_back(var->name() + " = " + *_values.at(i));
-			}
 		}
 
 		return boost::algorithm::join(assignments, _separator);

libsolidity/formal/Predicate.cpp

@@ -174,11 +174,8 @@ string Predicate::formatSummaryCall(vector<smtutil::Expression> const& _args) co
 	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))
-		{
-			solAssert(functionArgsCex.at(i), "");
 			functionArgs.emplace_back(*functionArgsCex.at(i));
-		}
 		else
 			functionArgs.emplace_back(params[i]->name());
 
@@ -298,6 +295,68 @@ optional<string> Predicate::expressionToString(smtutil::Expression const& _expr,
 		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, "");
+		try
+		{
+			vector<string> array(stoul(_expr.arguments.at(1).name));
+			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

@@ -128,6 +128,12 @@ private:
 	/// @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;