Counterexamples from Eldarica

libsmtutil/CHCSmtLib2Interface.cpp

@@ -19,6 +19,7 @@
 #include <boost/filesystem/operations.hpp>
 #include <libsmtutil/CHCSmtLib2Interface.h>
 
+#include <libsolutil/Algorithms.h>
 #include <libsolutil/Keccak256.h>
 
 #include <boost/algorithm/string/join.hpp>
@@ -28,6 +29,7 @@
 #include <boost/process.hpp>
 
 #include <range/v3/view.hpp>
+#include <range/v3/algorithm/for_each.hpp>
 
 #include <array>
 #include <fstream>
@@ -116,9 +118,9 @@ tuple<CheckResult, Expression, CHCSolverInterface::CexGraph> CHCSmtLib2Interface
 	CheckResult result;
 	// TODO proper parsing
 	if (boost::starts_with(response, "sat"))
-		result = CheckResult::UNSATISFIABLE;
+		return {CheckResult::UNSATISFIABLE, parseInvariants(response), {}};
 	else if (boost::starts_with(response, "unsat"))
-		result = CheckResult::SATISFIABLE;
+		return {CheckResult::SATISFIABLE, Expression (true), parseCounterexample(response)};
 	else if (boost::starts_with(response, "unknown"))
 		result = CheckResult::UNKNOWN;
 	else
@@ -127,6 +129,221 @@ tuple<CheckResult, Expression, CHCSolverInterface::CexGraph> CHCSmtLib2Interface
 	return {result, Expression(true), {}};
 }
 
+namespace
+{
+
+string readToken(string const& _data, size_t _pos)
+{
+	string r;
+	while (_pos < _data.size())
+	{
+		char c = _data[_pos++];
+		if (iswspace(unsigned(c)) || c == ',' || c == '(' || c == ')')
+			break;
+		r += c;
+	}
+	return r;
+}
+
+size_t skipWhitespaces(string const& _data, size_t _pos)
+{
+	while (_pos < _data.size() && iswspace(unsigned(_data[_pos])))
+	{
+		++_pos;
+	}
+
+	return _pos;
+}
+
+/// @param _data here is always going to be either
+/// - term
+/// - term(args)
+pair<smtutil::Expression, size_t> parseExpression(string const& _data)
+{
+	size_t pos = skipWhitespaces(_data, 0);
+
+	string fname = readToken(_data, pos);
+	pos += fname.size();
+
+	if (pos >= _data.size() || _data[pos] != '(')
+	{
+		if (fname == "true" || fname == "false")
+			return {Expression(fname, {}, SortProvider::boolSort), pos};
+		return {Expression(fname, {}, SortProvider::uintSort), pos};
+	}
+
+	smtAssert(_data[pos] == '(');
+
+	vector<Expression> exprArgs;
+	do
+	{
+		++pos;
+		auto [arg, size] = parseExpression(_data.substr(pos));
+		pos += size;
+		exprArgs.emplace_back(move(arg));
+		smtAssert(_data[pos] == ',' || _data[pos] == ')');
+	} while (_data[pos] == ',');
+
+	smtAssert(_data[pos] == ')');
+	++pos;
+
+	if (fname == "const")
+		fname = "const_array";
+
+	return {Expression(fname, move(exprArgs), SortProvider::uintSort), pos};
+}
+
+/// @param _data here is always going to be either
+/// - term
+/// - (term arg1 arg2 ... argk), where each arg is an sexpr.
+pair<smtutil::Expression, size_t> parseSExpression(string const& _data)
+{
+	size_t pos = skipWhitespaces(_data, 0);
+
+	vector<Expression> exprArgs;
+	string fname;
+	if (_data[pos] != '(')
+	{
+		fname = readToken(_data, pos);
+		pos += fname.size();
+	}
+	else
+	{
+		++pos;
+
+		string subExpr = _data.substr(pos);
+		string target = "(as const ";
+		if (boost::starts_with(subExpr, target))
+		{
+			fname = "const_array";
+			pos += target.size();
+			auto [symbArg, newPos] = parseSExpression(_data.substr(pos));
+			exprArgs.emplace_back(move(symbArg));
+			pos += newPos;
+			++pos;
+		}
+		else
+		{
+			fname = readToken(_data, pos);
+			pos += fname.size();
+		}
+
+		do
+		{
+			auto [symbArg, newPos] = parseSExpression(_data.substr(pos));
+			exprArgs.emplace_back(move(symbArg));
+			pos += newPos;
+		} while (_data[pos] != ')');
+		++pos;
+	}
+
+	if (fname == "")
+		fname = "var-decl";
+	else if (fname == "const")
+		fname = "const_array";
+
+	if (fname == "true" || fname == "false")
+		return {Expression(fname, {}, SortProvider::boolSort), pos};
+
+	return {Expression(fname, move(exprArgs), SortProvider::uintSort), pos};
+}
+
+smtutil::Expression parseDefineFun(string const& _data)
+{
+	auto [defineFun, pos] = parseSExpression(_data);
+
+	vector<Expression> newArgs;
+	Expression const& curArgs = defineFun.arguments.at(1);
+	smtAssert(curArgs.name == "var-decl");
+	for (auto&& curArg: curArgs.arguments)
+		newArgs.emplace_back(move(curArg));
+
+	Expression predExpr{defineFun.arguments.at(0).name, move(newArgs), SortProvider::boolSort};
+
+	Expression& invExpr = defineFun.arguments.at(3);
+
+	solidity::util::BreadthFirstSearch<Expression*> bfs{{&invExpr}};
+	bfs.run([&](auto&& _expr, auto&& _addChild) {
+		if (_expr->name == "=")
+		{
+			smtAssert(_expr->arguments.size() == 2);
+			auto check = [](string const& _name) {
+				return boost::starts_with(_name, "mapping") && boost::ends_with(_name, "length");
+			};
+			if (check(_expr->arguments.at(0).name) || check(_expr->arguments.at(1).name))
+				*_expr = Expression(true);
+		}
+		for (auto& arg: _expr->arguments)
+			_addChild(&arg);
+	});
+
+	Expression eq{"=", {move(predExpr), move(defineFun.arguments.at(3))}, SortProvider::boolSort};
+
+	return eq;
+}
+
+}
+
+CHCSolverInterface::CexGraph CHCSmtLib2Interface::parseCounterexample(string const& _result)
+{
+	CHCSolverInterface::CexGraph cexGraph;
+
+	for (auto&& line: _result | ranges::views::split('\n') | ranges::to<vector<string>>())
+	{
+		string firstDelimiter = ": ";
+		string secondDelimiter = " -> ";
+
+		size_t f = line.find(firstDelimiter);
+		if (f != string::npos)
+		{
+			string id = line.substr(0, f);
+			string rest = line.substr(f + firstDelimiter.size());
+
+			size_t s = rest.find(secondDelimiter);
+			string pred;
+			string adj;
+			if (s == string::npos)
+				pred = rest;
+			else
+			{
+				pred = rest.substr(0, s);
+				adj = rest.substr(s + secondDelimiter.size());
+			}
+
+			if (pred == "FALSE")
+				pred = "false";
+
+			unsigned iid = unsigned(stoi(id));
+
+			vector<unsigned> children;
+			for (auto&& v: adj | ranges::views::split(',') | ranges::to<vector<string>>())
+				children.emplace_back(unsigned(stoi(v)));
+
+			auto [expr, size] = parseExpression(pred);
+
+			cexGraph.nodes.emplace(iid, move(expr));
+			cexGraph.edges.emplace(iid, move(children));
+		}
+	}
+
+	return cexGraph;
+}
+
+Expression CHCSmtLib2Interface::parseInvariants(string const& _result)
+{
+	vector<Expression> eqs;
+	for (auto&& line: _result | ranges::views::split('\n') | ranges::to<vector<string>>())
+	{
+		if (!boost::starts_with(line, "(define-fun"))
+			continue;
+
+		eqs.emplace_back(parseDefineFun(line));
+	}
+
+	Expression conj{"and", move(eqs), SortProvider::boolSort};
+	return conj;
+}
+
 void CHCSmtLib2Interface::declareVariable(string const& _name, SortPointer const& _sort)
 {
 	smtAssert(_sort);

libsmtutil/CHCSmtLib2Interface.h

@@ -69,6 +69,10 @@ private:
 	/// Communicates with the solver via the callback. Throws SMTSolverError on error.
 	std::string querySolver(std::string const& _input);
 
+	CHCSolverInterface::CexGraph parseCounterexample(std::string const& _result);
+
+	Expression parseInvariants(std::string const& _result);
+
 	/// Used to access toSmtLibSort, SExpr, and handle variables.
 	std::unique_ptr<SMTLib2Interface> m_smtlib2;
 

libsolidity/formal/Predicate.cpp

@@ -34,6 +34,7 @@
 using namespace std;
 using boost::algorithm::starts_with;
 using namespace solidity;
+using namespace solidity::util;
 using namespace solidity::smtutil;
 using namespace solidity::frontend;
 using namespace solidity::frontend::smt;
@@ -506,7 +507,8 @@ optional<string> Predicate::expressionToString(smtutil::Expression const& _expr,
 				if (_expr.name == "0")
 					return "0x0";
 				// For some reason the code below returns "0x" for "0".
-				return util::toHex(toCompactBigEndian(bigint(_expr.name)), util::HexPrefix::Add, util::HexCase::Lower);
+				return toHex(toCompactBigEndian(bigint(_expr.name)), HexPrefix::Add, HexCase::Lower);
+				//return formatNumberReadable(bigint(_expr.name));
 			}
 			catch (out_of_range const&)
 			{
@@ -516,6 +518,7 @@ optional<string> Predicate::expressionToString(smtutil::Expression const& _expr,
 			}
 		}
 
+		//return formatNumberReadable(bigint(_expr.name));
 		return _expr.name;
 	}
 	if (smt::isBool(*_type))

libsolidity/formal/SMTEncoder.cpp

@@ -1070,6 +1070,7 @@ bool SMTEncoder::shouldAnalyze(ContractDefinition const& _contract) const
 		return false;
 
 	return m_settings.contracts.isDefault() ||
+		//m_settings.contracts.has(_contract.sourceUnitName(), _contract.name());
 		m_settings.contracts.has(_contract.sourceUnitName());
 }
 

libsolidity/formal/SymbolicState.cpp

@@ -441,6 +441,15 @@ void SymbolicState::buildABIFunctions(set<FunctionCall const*, ASTCompareByID<Fu
 		for (auto paramType: inTypes + outTypes)
 			name += "_" + paramType->richIdentifier();
 
+		while (name.find(" => ") != string::npos)
+			name.replace(name.find(" => "), 4, "");
+		while (name.find('(') != string::npos)
+			name.replace(name.find('('), 1, "$");
+		while (name.find(')') != string::npos)
+			name.replace(name.find(')'), 1, "$");
+		while (name.find(',') != string::npos)
+			name.replace(name.find(','), 1, "$");
+
 		m_abiMembers[funCall] = {name, inTypes, outTypes};
 
 		if (functions.count(name))

libsolidity/formal/SymbolicTypes.cpp

@@ -123,6 +123,15 @@ SortPointer smtSort(frontend::Type const& _type)
 		else
 			tupleName = _type.toString(true);
 
+		while (tupleName.find(" => ") != string::npos)
+			tupleName.replace(tupleName.find(" => "), 4, "");
+		while (tupleName.find('(') != string::npos)
+			tupleName.replace(tupleName.find('('), 1, "$");
+		while (tupleName.find(')') != string::npos)
+			tupleName.replace(tupleName.find(')'), 1, "$");
+		while (tupleName.find(',') != string::npos)
+			tupleName.replace(tupleName.find(','), 1, "$");
+
 		tupleName += "_tuple";
 
 		return make_shared<TupleSort>(
@@ -134,9 +143,18 @@ SortPointer smtSort(frontend::Type const& _type)
 	case Kind::Tuple:
 	{
 		vector<string> members;
-		auto const& tupleName = _type.toString(true);
+		string tupleName = _type.toString(true);
 		vector<SortPointer> sorts;
 
+		while (tupleName.find(" => ") != string::npos)
+			tupleName.replace(tupleName.find(" => "), 4, "");
+		while (tupleName.find('(') != string::npos)
+			tupleName.replace(tupleName.find('('), 1, "$");
+		while (tupleName.find(')') != string::npos)
+			tupleName.replace(tupleName.find(')'), 1, "$");
+		while (tupleName.find(',') != string::npos)
+			tupleName.replace(tupleName.find(','), 1, "$");
+
 		if (auto const* tupleType = dynamic_cast<frontend::TupleType const*>(&_type))
 		{
 			auto const& components = tupleType->components();

libsolutil/StringUtils.h

@@ -145,16 +145,32 @@ inline std::string formatNumberReadable(
 
 	// when multiple trailing FF bytes, format as N * 2**x - 1
 	i = 0;
-	for (v = _value; (v & 0xff) == 0xff; v >>= 8)
+	std::string minus;
+	v = _value;
+	if ((v & 0xff) == 0xfe)
+	{
+		++i;
+		minus = "2";
+		v >>= 8;
+	}
+	else if ((v & 0xff) == 0xfd)
+	{
+		++i;
+		minus = "3";
+		v >>= 8;
+	}
+	else
+		minus = "1";
+	for (; (v & 0xff) == 0xff; v >>= 8)
 		++i;
 	if (i > 2)
 	{
 		// 0xFF yields 2**8 - 1 (v is 0 in that case)
 		if (v == 0)
-			return "2**" + std::to_string(i * 8) + " - 1";
+			return "2**" + std::to_string(i * 8) + " - " + minus;//1";
 		return toHex(toCompactBigEndian(T(v + 1)), prefix, hexcase) +
 			" * 2**" + std::to_string(i * 8) +
-			" - 1";
+			" - " + minus;//1";
 	}
 
 	std::string str = toHex(toCompactBigEndian(_value), prefix, hexcase);