diff --git a/Changelog.md b/Changelog.md index d19d08be2..40b4765cd 100644 --- a/Changelog.md +++ b/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``. diff --git a/libsmtutil/CVC4Interface.cpp b/libsmtutil/CVC4Interface.cpp index 4c1ef378a..87184714f 100644 --- a/libsmtutil/CVC4Interface.cpp +++ b/libsmtutil/CVC4Interface.cpp @@ -19,6 +19,8 @@ #include +#include + 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(_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") diff --git a/libsmtutil/SMTLib2Interface.cpp b/libsmtutil/SMTLib2Interface.cpp index 4e81444fe..bc37ffb6c 100644 --- a/libsmtutil/SMTLib2Interface.cpp +++ b/libsmtutil/SMTLib2Interface.cpp @@ -126,7 +126,7 @@ pair> SMTLib2Interface::check(vector con result = CheckResult::ERROR; vector 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(_expr.sort); + smtAssert(intSort, ""); + + auto arg = toSExpr(_expr.arguments.front()); + auto nat = "(bv2nat " + arg + ")"; + + if (!intSort->isSigned) + return nat; + + auto bvSort = dynamic_pointer_cast(_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(_expr.arguments.at(0).sort); diff --git a/libsmtutil/SolverInterface.h b/libsmtutil/SolverInterface.h index 13fcae4f2..be12c3a80 100644 --- a/libsmtutil/SolverInterface.h +++ b/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 = std::dynamic_pointer_cast(_n.sort); + smtAssert(intSort, ""); + smtAssert(_size <= 256, ""); + return Expression( + "int2bv", + std::vector{std::move(_n), Expression(_size)}, + std::make_shared(_size) + ); + } + + static Expression bv2int(Expression _bv, bool _signed = false) + { + smtAssert(_bv.sort->kind == Kind::BitVector, ""); + std::shared_ptr bvSort = std::dynamic_pointer_cast(_bv.sort); + smtAssert(bvSort, ""); + smtAssert(bvSort->size <= 256, ""); + return Expression( + "bv2int", + std::vector{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 _arguments) const { smtAssert( diff --git a/libsmtutil/Sorts.cpp b/libsmtutil/Sorts.cpp index 7a45a1746..7624cbb5b 100644 --- a/libsmtutil/Sorts.cpp +++ b/libsmtutil/Sorts.cpp @@ -24,6 +24,14 @@ namespace solidity::smtutil { shared_ptr const SortProvider::boolSort{make_shared(Kind::Bool)}; -shared_ptr const SortProvider::intSort{make_shared(Kind::Int)}; +shared_ptr const SortProvider::uintSort{make_shared(false)}; +shared_ptr const SortProvider::sintSort{make_shared(true)}; + +shared_ptr SortProvider::intSort(bool _signed) +{ + if (_signed) + return sintSort; + return uintSort; +} } diff --git a/libsmtutil/Sorts.h b/libsmtutil/Sorts.h index 228dd057b..20cbf2be5 100644 --- a/libsmtutil/Sorts.h +++ b/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; +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 _domain, SortPointer _codomain): @@ -160,7 +191,9 @@ struct TupleSort: public Sort struct SortProvider { static std::shared_ptr const boolSort; - static std::shared_ptr const intSort; + static std::shared_ptr const uintSort; + static std::shared_ptr const sintSort; + static std::shared_ptr intSort(bool _signed = false); }; } diff --git a/libsmtutil/Z3Interface.cpp b/libsmtutil/Z3Interface.cpp index b42bc4765..1337b7b20 100644 --- a/libsmtutil/Z3Interface.cpp +++ b/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(_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") diff --git a/libsolidity/formal/CHC.cpp b/libsolidity/formal/CHC.cpp index fe63c198d..f0ba6d0de 100644 --- a/libsolidity/formal/CHC.cpp +++ b/libsolidity/formal/CHC.cpp @@ -701,7 +701,7 @@ vector CHC::stateSorts(ContractDefinition const& _contract smtutil::SortPointer CHC::constructorSort() { return make_shared( - vector{smtutil::SortProvider::intSort} + m_stateSorts, + vector{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( - vector{smtutil::SortProvider::intSort} + m_stateSorts + inputSorts + m_stateSorts + inputSorts + outputSorts, + vector{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( - vector{smtutil::SortProvider::intSort} + sorts + inputSorts + sorts + outputSorts, + vector{smtutil::SortProvider::uintSort} + sorts + inputSorts + sorts + outputSorts, smtutil::SortProvider::boolSort ); } diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp index 99aa6195f..258c74bcc 100644 --- a/libsolidity/formal/SMTEncoder.cpp +++ b/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(commonType)) + { + bvSize = intType->numBits(); + isSigned = intType->isSigned(); + } + else if (auto const* fixedType = dynamic_cast(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 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. diff --git a/libsolidity/formal/SMTEncoder.h b/libsolidity/formal/SMTEncoder.h index 63bbd45df..8010ba820 100644 --- a/libsolidity/formal/SMTEncoder.h +++ b/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); diff --git a/libsolidity/formal/SymbolicState.h b/libsolidity/formal/SymbolicState.h index f33faf9f2..2b234466d 100644 --- a/libsolidity/formal/SymbolicState.h +++ b/libsolidity/formal/SymbolicState.h @@ -63,7 +63,7 @@ private: /// Symbolic balances. SymbolicArrayVariable m_balances{ - std::make_shared(smtutil::SortProvider::intSort, smtutil::SortProvider::intSort), + std::make_shared(smtutil::SortProvider::uintSort, smtutil::SortProvider::uintSort), "balances", m_context }; diff --git a/libsolidity/formal/SymbolicTypes.cpp b/libsolidity/formal/SymbolicTypes.cpp index 38f72cb66..0ed81ee31 100644 --- a/libsolidity/formal/SymbolicTypes.cpp +++ b/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(&_type)) + return SortProvider::intSort(intType->isSigned()); + if (auto const* fixedType = dynamic_cast(&_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(parameterSorts, returnSort); @@ -68,7 +72,7 @@ SortPointer smtSort(frontend::Type const& _type) { auto stringLitType = dynamic_cast(&_type); solAssert(stringLitType, ""); - array = make_shared(SortProvider::intSort, SortProvider::intSort); + array = make_shared(SortProvider::uintSort, SortProvider::uintSort); } else { @@ -81,7 +85,7 @@ SortPointer smtSort(frontend::Type const& _type) solAssert(false, ""); solAssert(arrayType, ""); - array = make_shared(SortProvider::intSort, smtSortAbstractFunction(*arrayType->baseType())); + array = make_shared(SortProvider::uintSort, smtSortAbstractFunction(*arrayType->baseType())); } string tupleName; @@ -98,7 +102,7 @@ SortPointer smtSort(frontend::Type const& _type) return make_shared( tupleName, vector{tupleName + "_accessor_array", tupleName + "_accessor_length"}, - vector{array, SortProvider::intSort} + vector{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 smtSort(vector 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 smtSortAbstractFunction(vector const& if (type) sorts.push_back(smtSortAbstractFunction(*type)); else - sorts.push_back(SortProvider::intSort); + sorts.push_back(SortProvider::uintSort); return sorts; } diff --git a/libsolidity/formal/SymbolicVariables.cpp b/libsolidity/formal/SymbolicVariables.cpp index 558e7ccd1..002df6002 100644 --- a/libsolidity/formal/SymbolicVariables.cpp +++ b/libsolidity/formal/SymbolicVariables.cpp @@ -286,7 +286,7 @@ SymbolicArrayVariable::SymbolicArrayVariable( std::make_shared( "array_length_pair", std::vector{"array", "length"}, - std::vector{m_sort, SortProvider::intSort} + std::vector{m_sort, SortProvider::uintSort} ), m_uniqueName + "_array_length_pair", m_context diff --git a/test/libsolidity/smtCheckerTests/operators/bitwise_and_int.sol b/test/libsolidity/smtCheckerTests/operators/bitwise_and_int.sol new file mode 100644 index 000000000..579702632 --- /dev/null +++ b/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 diff --git a/test/libsolidity/smtCheckerTests/operators/bitwise_and_rational.sol b/test/libsolidity/smtCheckerTests/operators/bitwise_and_rational.sol new file mode 100644 index 000000000..4efdafdeb --- /dev/null +++ b/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 diff --git a/test/libsolidity/smtCheckerTests/operators/bitwise_and_uint.sol b/test/libsolidity/smtCheckerTests/operators/bitwise_and_uint.sol new file mode 100644 index 000000000..ce8400dbe --- /dev/null +++ b/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