[SMTChecker] Support to bitwise

Changelog.md

@@ -9,8 +9,10 @@ Compiler Features:
  * Build system: Update the soljson.js build to emscripten 1.39.15 and boost 1.73.0 and include Z3 for integrated SMTChecker support without the callback mechanism.
  * SMTChecker: Support array ``length``.
  * SMTChecker: Support array ``push`` and ``pop``.
+ * SMTChecker: General support to BitVectors and the bitwise ``and`` operator.
  * Add support for natspec comments on state variables.
 
+
 Bugfixes:
  * Optimizer: Fixed a bug in BlockDeDuplicator.
  * Type Checker: Disallow assignments to storage variables of type ``mapping``.

libsmtutil/CVC4Interface.cpp

@@ -19,6 +19,8 @@
 
 #include <libsolutil/CommonIO.h>
 
+#include <cvc4/util/bitvector.h>
+
 using namespace std;
 using namespace solidity;
 using namespace solidity::util;
@@ -185,6 +187,49 @@ CVC4::Expr CVC4Interface::toCVC4Expr(Expression const& _expr)
 			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 == "bvand")
+			return m_context.mkExpr(CVC4::kind::BITVECTOR_AND, arguments[0], arguments[1]);
+		else if (n == "int2bv")
+		{
+			size_t size = std::stoi(_expr.arguments[1].name);
+			auto i2bvOp = m_context.mkConst(CVC4::IntToBitVector(size));
+			// CVC4 treats all BVs as unsigned, so we need to manually apply 2's complement if needed.
+			return m_context.mkExpr(
+				CVC4::kind::ITE,
+				m_context.mkExpr(CVC4::kind::GEQ, arguments[0], m_context.mkConst(CVC4::Rational(0))),
+				m_context.mkExpr(CVC4::kind::INT_TO_BITVECTOR, i2bvOp, arguments[0]),
+				m_context.mkExpr(
+					CVC4::kind::BITVECTOR_NEG,
+					m_context.mkExpr(CVC4::kind::INT_TO_BITVECTOR, i2bvOp, m_context.mkExpr(CVC4::kind::UMINUS, arguments[0]))
+				)
+			);
+		}
+		else if (n == "bv2int")
+		{
+			auto intSort = dynamic_pointer_cast<IntSort>(_expr.sort);
+			smtAssert(intSort, "");
+			auto nat = m_context.mkExpr(CVC4::kind::BITVECTOR_TO_NAT, arguments[0]);
+			if (!intSort->isSigned)
+				return nat;
+
+			auto type = arguments[0].getType();
+			smtAssert(type.isBitVector(), "");
+			auto size = CVC4::BitVectorType(type).getSize();
+			// CVC4 treats all BVs as unsigned, so we need to manually apply 2's complement if needed.
+			auto extractOp = m_context.mkConst(CVC4::BitVectorExtract(size - 1, size - 1));
+			return m_context.mkExpr(CVC4::kind::ITE,
+				m_context.mkExpr(
+					CVC4::kind::EQUAL,
+					m_context.mkExpr(CVC4::kind::BITVECTOR_EXTRACT, extractOp, arguments[0]),
+					m_context.mkConst(CVC4::BitVector(1, size_t(0)))
+				),
+				nat,
+				m_context.mkExpr(
+					CVC4::kind::UMINUS,
+					m_context.mkExpr(CVC4::kind::BITVECTOR_TO_NAT, m_context.mkExpr(CVC4::kind::BITVECTOR_NEG, arguments[0]))
+				)
+			);
+		}
 		else if (n == "select")
 			return m_context.mkExpr(CVC4::kind::SELECT, arguments[0], arguments[1]);
 		else if (n == "store")

libsmtutil/SMTLib2Interface.cpp

@@ -126,7 +126,7 @@ pair<CheckResult, vector<string>> SMTLib2Interface::check(vector<Expression> con
 		result = CheckResult::ERROR;
 
 	vector<string> values;
-	if (result == CheckResult::SATISFIABLE && result != CheckResult::ERROR)
+	if (result == CheckResult::SATISFIABLE && !_expressionsToEvaluate.empty())
 		values = parseValues(find(response.cbegin(), response.cend(), '\n'), response.cend());
 	return make_pair(result, values);
 }
@@ -137,7 +137,40 @@ string SMTLib2Interface::toSExpr(Expression const& _expr)
 		return _expr.name;
 
 	std::string sexpr = "(";
-	if (_expr.name == "const_array")
+	if (_expr.name == "int2bv")
+	{
+		size_t size = std::stoi(_expr.arguments[1].name);
+		auto arg = toSExpr(_expr.arguments.front());
+		auto int2bv = "(_ int2bv " + to_string(size) + ")";
+		// Some solvers treat all BVs as unsigned, so we need to manually apply 2's complement if needed.
+		sexpr += string("ite ") +
+			"(>= " + arg + " 0) " +
+			"(" + int2bv + " " + arg + ") " +
+			"(bvneg (" + int2bv + " (- " + arg + ")))";
+	}
+	else if (_expr.name == "bv2int")
+	{
+		auto intSort = dynamic_pointer_cast<IntSort>(_expr.sort);
+		smtAssert(intSort, "");
+
+		auto arg = toSExpr(_expr.arguments.front());
+		auto nat = "(bv2nat " + arg + ")";
+
+		if (!intSort->isSigned)
+			return nat;
+
+		auto bvSort = dynamic_pointer_cast<BitVectorSort>(_expr.arguments.front().sort);
+		smtAssert(bvSort, "");
+		auto size = to_string(bvSort->size);
+		auto pos = to_string(bvSort->size - 1);
+
+		// Some solvers treat all BVs as unsigned, so we need to manually apply 2's complement if needed.
+		sexpr += string("ite ") +
+			"(= ((_ extract " + pos + " " + pos + ")" + arg + ") #b0) " +
+			nat + " " +
+			"(- (bvneg " + arg + "))";
+	}
+	else if (_expr.name == "const_array")
 	{
 		smtAssert(_expr.arguments.size() == 2, "");
 		auto sortSort = std::dynamic_pointer_cast<SortSort>(_expr.arguments.at(0).sort);

libsmtutil/SolverInterface.h

@@ -94,6 +94,9 @@ public:
 			{"*", 2},
 			{"/", 2},
 			{"mod", 2},
+			{"bvand", 2},
+			{"int2bv", 2},
+			{"bv2int", 1},
 			{"select", 2},
 			{"store", 3},
 			{"const_array", 2},
@@ -195,6 +198,32 @@ public:
 		);
 	}
 
+	static Expression int2bv(Expression _n, size_t _size)
+	{
+		smtAssert(_n.sort->kind == Kind::Int, "");
+		std::shared_ptr<IntSort> intSort = std::dynamic_pointer_cast<IntSort>(_n.sort);
+		smtAssert(intSort, "");
+		smtAssert(_size <= 256, "");
+		return Expression(
+			"int2bv",
+			std::vector<Expression>{std::move(_n), Expression(_size)},
+			std::make_shared<BitVectorSort>(_size)
+		);
+	}
+
+	static Expression bv2int(Expression _bv, bool _signed = false)
+	{
+		smtAssert(_bv.sort->kind == Kind::BitVector, "");
+		std::shared_ptr<BitVectorSort> bvSort = std::dynamic_pointer_cast<BitVectorSort>(_bv.sort);
+		smtAssert(bvSort, "");
+		smtAssert(bvSort->size <= 256, "");
+		return Expression(
+			"bv2int",
+			std::vector<Expression>{std::move(_bv)},
+			SortProvider::intSort(_signed)
+		);
+	}
+
 	friend Expression operator!(Expression _a)
 	{
 		return Expression("not", std::move(_a), Kind::Bool);
@@ -251,6 +280,11 @@ public:
 	{
 		return Expression("mod", std::move(_a), std::move(_b), Kind::Int);
 	}
+	friend Expression operator&(Expression _a, Expression _b)
+	{
+		auto bvSort = _a.sort;
+		return Expression("bvand", {std::move(_a), std::move(_b)}, bvSort);
+	}
 	Expression operator()(std::vector<Expression> _arguments) const
 	{
 		smtAssert(

libsmtutil/Sorts.cpp

@@ -24,6 +24,14 @@ namespace solidity::smtutil
 {
 
 shared_ptr<Sort> const SortProvider::boolSort{make_shared<Sort>(Kind::Bool)};
-shared_ptr<Sort> const SortProvider::intSort{make_shared<Sort>(Kind::Int)};
+shared_ptr<IntSort> const SortProvider::uintSort{make_shared<IntSort>(false)};
+shared_ptr<IntSort> const SortProvider::sintSort{make_shared<IntSort>(true)};
+
+shared_ptr<IntSort> SortProvider::intSort(bool _signed)
+{
+	if (_signed)
+		return sintSort;
+	return uintSort;
+}
 
 }

libsmtutil/Sorts.h

@@ -31,6 +31,7 @@ enum class Kind
 {
 	Int,
 	Bool,
+	BitVector,
 	Function,
 	Array,
 	Sort,
@@ -48,6 +49,36 @@ struct Sort
 };
 using SortPointer = std::shared_ptr<Sort>;
 
+struct IntSort: public Sort
+{
+	IntSort(bool _signed):
+		Sort(Kind::Int),
+		isSigned(_signed)
+	{}
+
+	bool operator==(IntSort const& _other) const
+	{
+		return Sort::operator==(_other) && isSigned == _other.isSigned;
+	}
+
+	bool isSigned;
+};
+
+struct BitVectorSort: public Sort
+{
+	BitVectorSort(unsigned _size):
+		Sort(Kind::BitVector),
+		size(_size)
+	{}
+
+	bool operator==(BitVectorSort const& _other) const
+	{
+		return Sort::operator==(_other) && size == _other.size;
+	}
+
+	unsigned size;
+};
+
 struct FunctionSort: public Sort
 {
 	FunctionSort(std::vector<SortPointer> _domain, SortPointer _codomain):
@@ -160,7 +191,9 @@ struct TupleSort: public Sort
 struct SortProvider
 {
 	static std::shared_ptr<Sort> const boolSort;
-	static std::shared_ptr<Sort> const intSort;
+	static std::shared_ptr<IntSort> const uintSort;
+	static std::shared_ptr<IntSort> const sintSort;
+	static std::shared_ptr<IntSort> intSort(bool _signed = false);
 };
 
 }

libsmtutil/Z3Interface.cpp

@@ -180,6 +180,19 @@ z3::expr Z3Interface::toZ3Expr(Expression const& _expr)
 			return arguments[0] / arguments[1];
 		else if (n == "mod")
 			return z3::mod(arguments[0], arguments[1]);
+		else if (n == "bvand")
+			return arguments[0] & arguments[1];
+		else if (n == "int2bv")
+		{
+			size_t size = std::stoi(_expr.arguments[1].name);
+			return z3::int2bv(size, arguments[0]);
+		}
+		else if (n == "bv2int")
+		{
+			auto intSort = dynamic_pointer_cast<IntSort>(_expr.sort);
+			smtAssert(intSort, "");
+			return z3::bv2int(arguments[0], intSort->isSigned);
+		}
 		else if (n == "select")
 			return z3::select(arguments[0], arguments[1]);
 		else if (n == "store")

libsolidity/formal/CHC.cpp

@@ -701,7 +701,7 @@ vector<smtutil::SortPointer> CHC::stateSorts(ContractDefinition const& _contract
 smtutil::SortPointer CHC::constructorSort()
 {
 	return make_shared<smtutil::FunctionSort>(
-		vector<smtutil::SortPointer>{smtutil::SortProvider::intSort} + m_stateSorts,
+		vector<smtutil::SortPointer>{smtutil::SortProvider::uintSort} + m_stateSorts,
 		smtutil::SortProvider::boolSort
 	);
 }
@@ -747,7 +747,7 @@ smtutil::SortPointer CHC::sort(FunctionDefinition const& _function)
 	auto inputSorts = applyMap(_function.parameters(), smtSort);
 	auto outputSorts = applyMap(_function.returnParameters(), smtSort);
 	return make_shared<smtutil::FunctionSort>(
-		vector<smtutil::SortPointer>{smtutil::SortProvider::intSort} + m_stateSorts + inputSorts + m_stateSorts + inputSorts + outputSorts,
+		vector<smtutil::SortPointer>{smtutil::SortProvider::uintSort} + m_stateSorts + inputSorts + m_stateSorts + inputSorts + outputSorts,
 		smtutil::SortProvider::boolSort
 	);
 }
@@ -776,7 +776,7 @@ smtutil::SortPointer CHC::summarySort(FunctionDefinition const& _function, Contr
 	auto inputSorts = applyMap(_function.parameters(), smtSort);
 	auto outputSorts = applyMap(_function.returnParameters(), smtSort);
 	return make_shared<smtutil::FunctionSort>(
-		vector<smtutil::SortPointer>{smtutil::SortProvider::intSort} + sorts + inputSorts + sorts + outputSorts,
+		vector<smtutil::SortPointer>{smtutil::SortProvider::uintSort} + sorts + inputSorts + sorts + outputSorts,
 		smtutil::SortProvider::boolSort
 	);
 }

libsolidity/formal/SMTEncoder.cpp

@@ -574,6 +574,8 @@ void SMTEncoder::endVisit(BinaryOperation const& _op)
 		arithmeticOperation(_op);
 	else if (TokenTraits::isCompareOp(_op.getOperator()))
 		compareOperation(_op);
+	else if (TokenTraits::isBitOp(_op.getOperator()))
+		bitwiseOperation(_op);
 	else
 		m_errorReporter.warning(
 			3876_error,
@@ -1346,6 +1348,43 @@ void SMTEncoder::booleanOperation(BinaryOperation const& _op)
 		);
 }
 
+void SMTEncoder::bitwiseOperation(BinaryOperation const& _op)
+{
+	solAssert(TokenTraits::isBitOp(_op.getOperator()), "");
+	auto commonType = _op.annotation().commonType;
+	solAssert(commonType, "");
+
+	unsigned bvSize = 256;
+	bool isSigned = false;
+	if (auto const* intType = dynamic_cast<IntegerType const*>(commonType))
+	{
+		bvSize = intType->numBits();
+		isSigned = intType->isSigned();
+	}
+	else if (auto const* fixedType = dynamic_cast<FixedPointType const*>(commonType))
+	{
+		bvSize = fixedType->numBits();
+		isSigned = fixedType->isSigned();
+	}
+
+	auto bvLeft = smtutil::Expression::int2bv(expr(_op.leftExpression()), bvSize);
+	auto bvRight = smtutil::Expression::int2bv(expr(_op.rightExpression()), bvSize);
+
+	optional<smtutil::Expression> result;
+	if (_op.getOperator() == Token::BitAnd)
+		result = bvLeft & bvRight;
+	// TODO implement the other operators
+	else
+		m_errorReporter.warning(
+			1093_error,
+			_op.location(),
+			"Assertion checker does not yet implement this bitwise operator."
+		);
+
+	if (result)
+		defineExpr(_op, smtutil::Expression::bv2int(*result, isSigned));
+}
+
 smtutil::Expression SMTEncoder::division(smtutil::Expression _left, smtutil::Expression _right, IntegerType const& _type)
 {
 	// Signed division in SMTLIB2 rounds differently for negative division.

libsolidity/formal/SMTEncoder.h

@@ -108,6 +108,7 @@ protected:
 	);
 	void compareOperation(BinaryOperation const& _op);
 	void booleanOperation(BinaryOperation const& _op);
+	void bitwiseOperation(BinaryOperation const& _op);
 
 	void initContract(ContractDefinition const& _contract);
 	void initFunction(FunctionDefinition const& _function);

libsolidity/formal/SymbolicState.h

@@ -63,7 +63,7 @@ private:
 
 	/// Symbolic balances.
 	SymbolicArrayVariable m_balances{
-		std::make_shared<smtutil::ArraySort>(smtutil::SortProvider::intSort, smtutil::SortProvider::intSort),
+		std::make_shared<smtutil::ArraySort>(smtutil::SortProvider::uintSort, smtutil::SortProvider::uintSort),
 		"balances",
 		m_context
 	};

libsolidity/formal/SymbolicTypes.cpp

@@ -34,7 +34,11 @@ SortPointer smtSort(frontend::Type const& _type)
 	switch (smtKind(_type.category()))
 	{
 	case Kind::Int:
-		return SortProvider::intSort;
+		if (auto const* intType = dynamic_cast<IntegerType const*>(&_type))
+			return SortProvider::intSort(intType->isSigned());
+		if (auto const* fixedType = dynamic_cast<FixedPointType const*>(&_type))
+			return SortProvider::intSort(fixedType->isSigned());
+		return SortProvider::uintSort;
 	case Kind::Bool:
 		return SortProvider::boolSort;
 	case Kind::Function:
@@ -50,7 +54,7 @@ SortPointer smtSort(frontend::Type const& _type)
 			returnSort = SortProvider::boolSort;
 		else if (returnTypes.size() > 1)
 			// Abstract sort.
-			returnSort = SortProvider::intSort;
+			returnSort = SortProvider::uintSort;
 		else
 			returnSort = smtSort(*returnTypes.front());
 		return make_shared<FunctionSort>(parameterSorts, returnSort);
@@ -68,7 +72,7 @@ SortPointer smtSort(frontend::Type const& _type)
 		{
 			auto stringLitType = dynamic_cast<frontend::StringLiteralType const*>(&_type);
 			solAssert(stringLitType, "");
-			array = make_shared<ArraySort>(SortProvider::intSort, SortProvider::intSort);
+			array = make_shared<ArraySort>(SortProvider::uintSort, SortProvider::uintSort);
 		}
 		else
 		{
@@ -81,7 +85,7 @@ SortPointer smtSort(frontend::Type const& _type)
 				solAssert(false, "");
 
 			solAssert(arrayType, "");
-			array = make_shared<ArraySort>(SortProvider::intSort, smtSortAbstractFunction(*arrayType->baseType()));
+			array = make_shared<ArraySort>(SortProvider::uintSort, smtSortAbstractFunction(*arrayType->baseType()));
 		}
 
 		string tupleName;
@@ -98,7 +102,7 @@ SortPointer smtSort(frontend::Type const& _type)
 		return make_shared<TupleSort>(
 			tupleName,
 			vector<string>{tupleName + "_accessor_array", tupleName + "_accessor_length"},
-			vector<SortPointer>{array, SortProvider::intSort}
+			vector<SortPointer>{array, SortProvider::uintSort}
 		);
 	}
 	case Kind::Tuple:
@@ -118,7 +122,7 @@ SortPointer smtSort(frontend::Type const& _type)
 	}
 	default:
 		// Abstract case.
-		return SortProvider::intSort;
+		return SortProvider::uintSort;
 	}
 }
 
@@ -133,7 +137,7 @@ vector<SortPointer> smtSort(vector<frontend::TypePointer> const& _types)
 SortPointer smtSortAbstractFunction(frontend::Type const& _type)
 {
 	if (isFunction(_type.category()))
-		return SortProvider::intSort;
+		return SortProvider::uintSort;
 	return smtSort(_type);
 }
 
@@ -144,7 +148,7 @@ vector<SortPointer> smtSortAbstractFunction(vector<frontend::TypePointer> const&
 		if (type)
 			sorts.push_back(smtSortAbstractFunction(*type));
 		else
-			sorts.push_back(SortProvider::intSort);
+			sorts.push_back(SortProvider::uintSort);
 	return sorts;
 }
 

libsolidity/formal/SymbolicVariables.cpp

@@ -286,7 +286,7 @@ SymbolicArrayVariable::SymbolicArrayVariable(
 		std::make_shared<TupleSort>(
 			"array_length_pair",
 			std::vector<std::string>{"array", "length"},
-			std::vector<SortPointer>{m_sort, SortProvider::intSort}
+			std::vector<SortPointer>{m_sort, SortProvider::uintSort}
 		),
 		m_uniqueName + "_array_length_pair",
 		m_context

test/libsolidity/smtCheckerTests/operators/bitwise_and_int.sol

@@ -0,0 +1,18 @@
+pragma experimental SMTChecker;
+
+contract C {
+	function f() public pure {
+		int8 x = 1;
+		int8 y = 0;
+		assert(x & y != 0);
+		x = -1; y = 3;
+		assert(x & y == 3);
+		y = -1;
+		int8 z = x & y;
+		assert(z == -1);
+		y = 127;
+		assert(x & y == 127);
+	}
+}
+// ----
+// Warning: (104-122): Assertion violation happens here

test/libsolidity/smtCheckerTests/operators/bitwise_and_rational.sol

@@ -0,0 +1,12 @@
+pragma experimental SMTChecker;
+
+contract C {
+	function f() public pure {
+		assert(1 & 0 != 0);
+		assert(-1 & 3 == 3);
+		assert(-1 & -1 == -1);
+		assert(-1 & 127 == 127);
+	}
+}
+// ----
+// Warning: (76-94): Assertion violation happens here

test/libsolidity/smtCheckerTests/operators/bitwise_and_uint.sol

@@ -0,0 +1,18 @@
+pragma experimental SMTChecker;
+
+contract C {
+	function f() public pure {
+		uint8 x = 1;
+		uint16 y = 0;
+		assert(x & y != 0);
+		x = 0xff;
+		y = 0xffff;
+		assert(x & y == 0xff);
+		assert(x & y == 0xffff);
+		assert(x & y == 0x0000);
+	}
+}
+// ----
+// Warning: (107-125): Assertion violation happens here
+// Warning: (180-203): Assertion violation happens here
+// Warning: (207-230): Assertion violation happens here