From a0c605aa85c0a18c2d3e9f614d120d6a089c460b Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Tue, 14 Apr 2020 11:09:38 +0200 Subject: [PATCH] [SMTChecker] Support array length --- Changelog.md | 1 + libsolidity/formal/CVC4Interface.cpp | 9 ++ libsolidity/formal/SMTEncoder.cpp | 60 ++++++++-- libsolidity/formal/SMTLib2Interface.cpp | 21 +++- libsolidity/formal/SSAVariable.cpp | 9 +- libsolidity/formal/SSAVariable.h | 7 +- libsolidity/formal/SolverInterface.h | 28 ++++- libsolidity/formal/SymbolicState.cpp | 8 +- libsolidity/formal/SymbolicTypes.cpp | 52 ++++++-- libsolidity/formal/SymbolicVariables.cpp | 111 +++++++++++------- libsolidity/formal/SymbolicVariables.h | 72 ++++++------ libsolidity/formal/Z3Interface.cpp | 9 ++ ...ngth_1d_assignment_2d_memory_to_memory.sol | 10 ++ ...th_1d_assignment_2d_storage_to_storage.sol | 11 ++ .../length_1d_copy_2d_memory_to_storage.sol | 11 ++ .../length_1d_copy_2d_storage_to_memory.sol | 11 ++ .../length_1d_mapping_array_1.sol | 8 ++ .../length_1d_mapping_array_2.sol | 9 ++ .../length_1d_mapping_array_2d_1.sol | 9 ++ .../length_1d_struct_array_1.sol | 20 ++++ .../length_1d_struct_array_2d_1.sol | 22 ++++ .../length_assignment_2d_memory_to_memory.sol | 9 ++ .../length_assignment_memory_to_memory.sol | 8 ++ .../length_assignment_storage_to_storage.sol | 10 ++ .../array_members/length_basic.sol | 13 ++ .../length_copy_memory_to_storage.sol | 9 ++ .../length_copy_storage_to_memory.sol | 9 ++ .../array_members/length_function_call.sol | 10 ++ .../length_same_after_assignment.sol | 10 ++ .../length_same_after_assignment_2.sol | 15 +++ .../length_same_after_assignment_2_fail.sol | 19 +++ .../length_same_after_assignment_3.sol | 17 +++ .../length_same_after_assignment_3_fail.sol | 22 ++++ .../smtCheckerTests/complex/MerkleProof.sol | 2 - .../compound_assignment_division_2.sol | 1 - .../compound_assignment_division_3.sol | 1 - .../operators/compound_mul_array_index.sol | 1 + .../operators/compound_mul_mapping.sol | 1 + .../operators/delete_array_index_2d.sol | 2 + .../smtCheckerTests/special/msg_data.sol | 1 - .../types/mapping_aliasing_2.sol | 1 + .../smtCheckerTests/types/string_1.sol | 2 - .../smtCheckerTestsJSON/multi.json | 4 +- .../smtCheckerTestsJSON/simple.json | 2 +- 44 files changed, 548 insertions(+), 119 deletions(-) create mode 100644 test/libsolidity/smtCheckerTests/array_members/length_1d_assignment_2d_memory_to_memory.sol create mode 100644 test/libsolidity/smtCheckerTests/array_members/length_1d_assignment_2d_storage_to_storage.sol create mode 100644 test/libsolidity/smtCheckerTests/array_members/length_1d_copy_2d_memory_to_storage.sol create mode 100644 test/libsolidity/smtCheckerTests/array_members/length_1d_copy_2d_storage_to_memory.sol create mode 100644 test/libsolidity/smtCheckerTests/array_members/length_1d_mapping_array_1.sol create mode 100644 test/libsolidity/smtCheckerTests/array_members/length_1d_mapping_array_2.sol create mode 100644 test/libsolidity/smtCheckerTests/array_members/length_1d_mapping_array_2d_1.sol create mode 100644 test/libsolidity/smtCheckerTests/array_members/length_1d_struct_array_1.sol create mode 100644 test/libsolidity/smtCheckerTests/array_members/length_1d_struct_array_2d_1.sol create mode 100644 test/libsolidity/smtCheckerTests/array_members/length_assignment_2d_memory_to_memory.sol create mode 100644 test/libsolidity/smtCheckerTests/array_members/length_assignment_memory_to_memory.sol create mode 100644 test/libsolidity/smtCheckerTests/array_members/length_assignment_storage_to_storage.sol create mode 100644 test/libsolidity/smtCheckerTests/array_members/length_basic.sol create mode 100644 test/libsolidity/smtCheckerTests/array_members/length_copy_memory_to_storage.sol create mode 100644 test/libsolidity/smtCheckerTests/array_members/length_copy_storage_to_memory.sol create mode 100644 test/libsolidity/smtCheckerTests/array_members/length_function_call.sol create mode 100644 test/libsolidity/smtCheckerTests/array_members/length_same_after_assignment.sol create mode 100644 test/libsolidity/smtCheckerTests/array_members/length_same_after_assignment_2.sol create mode 100644 test/libsolidity/smtCheckerTests/array_members/length_same_after_assignment_2_fail.sol create mode 100644 test/libsolidity/smtCheckerTests/array_members/length_same_after_assignment_3.sol create mode 100644 test/libsolidity/smtCheckerTests/array_members/length_same_after_assignment_3_fail.sol diff --git a/Changelog.md b/Changelog.md index e2bfde110..cf1565913 100644 --- a/Changelog.md +++ b/Changelog.md @@ -5,6 +5,7 @@ Language Features: 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``. Bugfixes: diff --git a/libsolidity/formal/CVC4Interface.cpp b/libsolidity/formal/CVC4Interface.cpp index 067786061..86688e0b1 100644 --- a/libsolidity/formal/CVC4Interface.cpp +++ b/libsolidity/formal/CVC4Interface.cpp @@ -206,6 +206,15 @@ CVC4::Expr CVC4Interface::toCVC4Expr(Expression const& _expr) CVC4::Expr s = dt[0][index].getSelector(); return m_context.mkExpr(CVC4::kind::APPLY_SELECTOR, s, arguments[0]); } + else if (n == "tuple_constructor") + { + shared_ptr tupleSort = std::dynamic_pointer_cast(_expr.sort); + solAssert(tupleSort, ""); + CVC4::DatatypeType tt = m_context.mkTupleType(cvc4Sort(tupleSort->components)); + CVC4::Datatype const& dt = tt.getDatatype(); + CVC4::Expr c = dt[0].getConstructor(); + return m_context.mkExpr(CVC4::kind::APPLY_CONSTRUCTOR, c, arguments); + } solAssert(false, ""); } diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp index 8760c7b6b..09c188435 100644 --- a/libsolidity/formal/SMTEncoder.cpp +++ b/libsolidity/formal/SMTEncoder.cpp @@ -890,6 +890,33 @@ bool SMTEncoder::visit(MemberAccess const& _memberAccess) return false; } } + else if (exprType->category() == Type::Category::Array) + { + _memberAccess.expression().accept(*this); + if (_memberAccess.memberName() == "length") + { + auto symbArray = dynamic_pointer_cast(m_context.expression(_memberAccess.expression())); + solAssert(symbArray, ""); + defineExpr(_memberAccess, symbArray->length()); + m_uninterpretedTerms.insert(&_memberAccess); + setSymbolicUnknownValue( + expr(_memberAccess), + _memberAccess.annotation().type, + m_context + ); + } + else + { + auto const& name = _memberAccess.memberName(); + solAssert(name == "push" || name == "pop", ""); + m_errorReporter.warning( + 9098_error, + _memberAccess.location(), + "Assertion checker does not yet support array member \"" + name + "\"." + ); + } + return false; + } else m_errorReporter.warning( 7650_error, @@ -939,9 +966,10 @@ void SMTEncoder::endVisit(IndexAccess const& _indexAccess) return; } - solAssert(array, ""); + auto arrayVar = dynamic_pointer_cast(array); + solAssert(arrayVar, ""); defineExpr(_indexAccess, smt::Expression::select( - array->currentValue(), + arrayVar->elements(), expr(*_indexAccess.indexExpression()) )); setSymbolicUnknownValue( @@ -1013,16 +1041,20 @@ void SMTEncoder::arrayIndexAssignment(Expression const& _expr, smt::Expression c return false; }); + auto symbArray = dynamic_pointer_cast(m_context.variable(*varDecl)); smt::Expression store = smt::Expression::store( - m_context.variable(*varDecl)->currentValue(), + symbArray->elements(), expr(*indexAccess->indexExpression()), toStore ); - m_context.addAssertion(m_context.newValue(*varDecl) == store); + auto oldLength = symbArray->length(); + symbArray->increaseIndex(); + m_context.addAssertion(symbArray->elements() == store); + m_context.addAssertion(symbArray->length() == oldLength); // Update the SMT select value after the assignment, // necessary for sound models. defineExpr(*indexAccess, smt::Expression::select( - m_context.variable(*varDecl)->currentValue(), + symbArray->elements(), expr(*indexAccess->indexExpression()) )); @@ -1030,7 +1062,12 @@ void SMTEncoder::arrayIndexAssignment(Expression const& _expr, smt::Expression c } else if (auto base = dynamic_cast(&indexAccess->baseExpression())) { - toStore = smt::Expression::store(expr(*base), expr(*indexAccess->indexExpression()), toStore); + auto symbArray = dynamic_pointer_cast(m_context.expression(*base)); + solAssert(symbArray, ""); + toStore = smt::Expression::tuple_constructor( + smt::Expression(base->annotation().type), + {smt::Expression::store(symbArray->elements(), expr(*indexAccess->indexExpression()), toStore), symbArray->length()} + ); indexAccess = base; } else @@ -1326,7 +1363,14 @@ smt::Expression SMTEncoder::compoundAssignment(Assignment const& _assignment) void SMTEncoder::assignment(VariableDeclaration const& _variable, Expression const& _value) { - assignment(_variable, expr(_value, _variable.type())); + // In general, at this point, the SMT sorts of _variable and _value are the same, + // even if there is implicit conversion. + // This is a special case where the SMT sorts are different. + // For now we are unaware of other cases where this happens, but if they do appear + // we should extract this into an `implicitConversion` function. + if (_variable.type()->category() != Type::Category::Array || _value.annotation().type->category() != Type::Category::StringLiteral) + assignment(_variable, expr(_value, _variable.type())); + // TODO else { store each string literal byte into the array } } void SMTEncoder::assignment(VariableDeclaration const& _variable, smt::Expression const& _value) @@ -1616,7 +1660,7 @@ SMTEncoder::VariableIndices SMTEncoder::copyVariableIndices() void SMTEncoder::resetVariableIndices(VariableIndices const& _indices) { for (auto const& var: _indices) - m_context.variable(*var.first)->index() = var.second; + m_context.variable(*var.first)->setIndex(var.second); } void SMTEncoder::clearIndices(ContractDefinition const* _contract, FunctionDefinition const* _function) diff --git a/libsolidity/formal/SMTLib2Interface.cpp b/libsolidity/formal/SMTLib2Interface.cpp index 339a0a8ad..97ccc2c91 100644 --- a/libsolidity/formal/SMTLib2Interface.cpp +++ b/libsolidity/formal/SMTLib2Interface.cpp @@ -153,7 +153,15 @@ string SMTLib2Interface::toSExpr(smt::Expression const& _expr) auto tupleSort = dynamic_pointer_cast(_expr.arguments.at(0).sort); unsigned index = std::stoi(_expr.arguments.at(1).name); solAssert(index < tupleSort->members.size(), ""); - sexpr += tupleSort->members.at(index) + " " + toSExpr(_expr.arguments.at(0)); + sexpr += "|" + tupleSort->members.at(index) + "| " + toSExpr(_expr.arguments.at(0)); + } + else if (_expr.name == "tuple_constructor") + { + auto tupleSort = dynamic_pointer_cast(_expr.sort); + solAssert(tupleSort, ""); + sexpr += "|" + tupleSort->name + "|"; + for (auto const& arg: _expr.arguments) + sexpr += " " + toSExpr(arg); } else { @@ -182,18 +190,19 @@ string SMTLib2Interface::toSmtLibSort(Sort const& _sort) case Kind::Tuple: { auto const& tupleSort = dynamic_cast(_sort); - if (!m_userSorts.count(tupleSort.name)) + string tupleName = "|" + tupleSort.name + "|"; + if (!m_userSorts.count(tupleName)) { - m_userSorts.insert(tupleSort.name); - string decl("(declare-datatypes ((" + tupleSort.name + " 0)) (((" + tupleSort.name); + m_userSorts.insert(tupleName); + string decl("(declare-datatypes ((" + tupleName + " 0)) (((" + tupleName); solAssert(tupleSort.members.size() == tupleSort.components.size(), ""); for (unsigned i = 0; i < tupleSort.members.size(); ++i) - decl += " (" + tupleSort.members.at(i) + " " + toSmtLibSort(*tupleSort.components.at(i)) + ")"; + decl += " (|" + tupleSort.members.at(i) + "| " + toSmtLibSort(*tupleSort.components.at(i)) + ")"; decl += "))))"; write(decl); } - return tupleSort.name; + return tupleName; } default: solAssert(false, "Invalid SMT sort"); diff --git a/libsolidity/formal/SSAVariable.cpp b/libsolidity/formal/SSAVariable.cpp index 90e77a050..5569d8f36 100644 --- a/libsolidity/formal/SSAVariable.cpp +++ b/libsolidity/formal/SSAVariable.cpp @@ -29,5 +29,12 @@ SSAVariable::SSAVariable() void SSAVariable::resetIndex() { m_currentIndex = 0; - m_nextFreeIndex = make_unique(1); + m_nextFreeIndex = 1; +} + +void SSAVariable::setIndex(unsigned _index) +{ + m_currentIndex = _index; + if (m_nextFreeIndex <= _index) + m_nextFreeIndex = _index + 1; } diff --git a/libsolidity/formal/SSAVariable.h b/libsolidity/formal/SSAVariable.h index 9c86af40b..bad6fa80c 100644 --- a/libsolidity/formal/SSAVariable.h +++ b/libsolidity/formal/SSAVariable.h @@ -29,7 +29,10 @@ class SSAVariable { public: SSAVariable(); + /// Resets index to 0 and next index to 1. void resetIndex(); + /// Sets index to _index and only adjusts next if next <= _index. + void setIndex(unsigned _index); /// This function returns the current index of this SSA variable. unsigned index() const { return m_currentIndex; } @@ -37,12 +40,12 @@ public: unsigned operator++() { - return m_currentIndex = (*m_nextFreeIndex)++; + return m_currentIndex = m_nextFreeIndex++; } private: unsigned m_currentIndex; - std::unique_ptr m_nextFreeIndex; + unsigned m_nextFreeIndex; }; } diff --git a/libsolidity/formal/SolverInterface.h b/libsolidity/formal/SolverInterface.h index cac412c4b..4532c1b3e 100644 --- a/libsolidity/formal/SolverInterface.h +++ b/libsolidity/formal/SolverInterface.h @@ -28,6 +28,7 @@ #include #include #include +#include #include #include @@ -63,7 +64,8 @@ class Expression friend class SolverInterface; public: explicit Expression(bool _v): Expression(_v ? "true" : "false", Kind::Bool) {} - explicit Expression(frontend::TypePointer _type): Expression(_type->toString(), {}, std::make_shared(smtSort(*_type))) {} + explicit Expression(frontend::TypePointer _type): Expression(_type->toString(true), {}, std::make_shared(smtSort(*_type))) {} + explicit Expression(std::shared_ptr _sort): Expression("", {}, _sort) {} Expression(size_t _number): Expression(std::to_string(_number), Kind::Int) {} Expression(u256 const& _number): Expression(_number.str(), Kind::Int) {} Expression(s256 const& _number): Expression(_number.str(), Kind::Int) {} @@ -76,6 +78,13 @@ public: bool hasCorrectArity() const { + if (name == "tuple_constructor") + { + auto tupleSort = std::dynamic_pointer_cast(sort); + solAssert(tupleSort, ""); + return arguments.size() == tupleSort->components.size(); + } + static std::map const operatorsArity{ {"ite", 3}, {"not", 1}, @@ -138,8 +147,7 @@ public: /// The function is pure and returns the modified array. static Expression store(Expression _array, Expression _index, Expression _element) { - solAssert(_array.sort->kind == Kind::Array, ""); - std::shared_ptr arraySort = std::dynamic_pointer_cast(_array.sort); + auto arraySort = std::dynamic_pointer_cast(_array.sort); solAssert(arraySort, ""); solAssert(_index.sort, ""); solAssert(_element.sort, ""); @@ -180,6 +188,20 @@ public: ); } + static Expression tuple_constructor(Expression _tuple, std::vector _arguments) + { + solAssert(_tuple.sort->kind == Kind::Sort, ""); + auto sortSort = std::dynamic_pointer_cast(_tuple.sort); + auto tupleSort = std::dynamic_pointer_cast(sortSort->inner); + solAssert(tupleSort, ""); + solAssert(_arguments.size() == tupleSort->components.size(), ""); + return Expression( + "tuple_constructor", + std::move(_arguments), + tupleSort + ); + } + friend Expression operator!(Expression _a) { return Expression("not", std::move(_a), Kind::Bool); diff --git a/libsolidity/formal/SymbolicState.cpp b/libsolidity/formal/SymbolicState.cpp index d38e79c54..5ae8922fb 100644 --- a/libsolidity/formal/SymbolicState.cpp +++ b/libsolidity/formal/SymbolicState.cpp @@ -47,7 +47,7 @@ Expression SymbolicState::balance() Expression SymbolicState::balance(Expression _address) { - return Expression::select(m_balances.currentValue(), move(_address)); + return Expression::select(m_balances.elements(), move(_address)); } void SymbolicState::transfer(Expression _from, Expression _to, Expression _value) @@ -72,11 +72,13 @@ void SymbolicState::transfer(Expression _from, Expression _to, Expression _value void SymbolicState::addBalance(Expression _address, Expression _value) { auto newBalances = Expression::store( - m_balances.currentValue(), + m_balances.elements(), _address, balance(_address) + move(_value) ); + auto oldLength = m_balances.length(); m_balances.increaseIndex(); - m_context.addAssertion(newBalances == m_balances.currentValue()); + m_context.addAssertion(m_balances.elements() == newBalances); + m_context.addAssertion(m_balances.length() == oldLength); } diff --git a/libsolidity/formal/SymbolicTypes.cpp b/libsolidity/formal/SymbolicTypes.cpp index b8da5da0c..be6cc1b37 100644 --- a/libsolidity/formal/SymbolicTypes.cpp +++ b/libsolidity/formal/SymbolicTypes.cpp @@ -21,6 +21,7 @@ #include #include #include +#include using namespace std; @@ -55,17 +56,18 @@ SortPointer smtSort(frontend::Type const& _type) } case Kind::Array: { + shared_ptr array; if (isMapping(_type.category())) { auto mapType = dynamic_cast(&_type); solAssert(mapType, ""); - return make_shared(smtSortAbstractFunction(*mapType->keyType()), smtSortAbstractFunction(*mapType->valueType())); + array = make_shared(smtSortAbstractFunction(*mapType->keyType()), smtSortAbstractFunction(*mapType->valueType())); } else if (isStringLiteral(_type.category())) { auto stringLitType = dynamic_cast(&_type); solAssert(stringLitType, ""); - return make_shared(SortProvider::intSort, SortProvider::intSort); + array = make_shared(SortProvider::intSort, SortProvider::intSort); } else { @@ -78,8 +80,25 @@ SortPointer smtSort(frontend::Type const& _type) solAssert(false, ""); solAssert(arrayType, ""); - return make_shared(SortProvider::intSort, smtSortAbstractFunction(*arrayType->baseType())); + array = make_shared(SortProvider::intSort, smtSortAbstractFunction(*arrayType->baseType())); } + + string tupleName; + if ( + auto arrayType = dynamic_cast(&_type); + (arrayType && arrayType->isString()) || + _type.category() == frontend::Type::Category::ArraySlice || + _type.category() == frontend::Type::Category::StringLiteral + ) + tupleName = "bytes_tuple"; + else + tupleName = _type.toString(true) + "_tuple"; + + return make_shared( + tupleName, + vector{tupleName + "_accessor_array", tupleName + "_accessor_length"}, + vector{array, SortProvider::intSort} + ); } case Kind::Tuple: { @@ -219,9 +238,7 @@ pair> newSymbolicVariable( else var = make_shared(type, type, _uniqueName, _context); } - else if (isMapping(_type.category())) - var = make_shared(type, _uniqueName, _context); - else if (isArray(_type.category())) + else if (isMapping(_type.category()) || isArray(_type.category())) var = make_shared(type, type, _uniqueName, _context); else if (isTuple(_type.category())) var = make_shared(type, _uniqueName, _context); @@ -349,11 +366,26 @@ Expression zeroValue(frontend::TypePointer const& _type) return Expression(false); if (isArray(_type->category()) || isMapping(_type->category())) { + auto tupleSort = dynamic_pointer_cast(smtSort(*_type)); + solAssert(tupleSort, ""); + auto sortSort = make_shared(tupleSort->components.front()); + + std::optional zeroArray; + auto length = bigint(0); if (auto arrayType = dynamic_cast(_type)) - return Expression::const_array(Expression(arrayType), zeroValue(arrayType->baseType())); - auto mappingType = dynamic_cast(_type); - solAssert(mappingType, ""); - return Expression::const_array(Expression(mappingType), zeroValue(mappingType->valueType())); + { + zeroArray = Expression::const_array(Expression(sortSort), zeroValue(arrayType->baseType())); + if (!arrayType->isDynamicallySized()) + length = bigint(arrayType->length()); + } + else if (auto mappingType = dynamic_cast(_type)) + zeroArray = Expression::const_array(Expression(sortSort), zeroValue(mappingType->valueType())); + else + solAssert(false, ""); + + solAssert(zeroArray, ""); + return Expression::tuple_constructor(Expression(_type), vector{*zeroArray, length}); + } solAssert(false, ""); } diff --git a/libsolidity/formal/SymbolicVariables.cpp b/libsolidity/formal/SymbolicVariables.cpp index 35cd4f9c2..519588abd 100644 --- a/libsolidity/formal/SymbolicVariables.cpp +++ b/libsolidity/formal/SymbolicVariables.cpp @@ -86,6 +86,12 @@ smt::Expression SymbolicVariable::resetIndex() return currentValue(); } +smt::Expression SymbolicVariable::setIndex(unsigned _index) +{ + m_ssa->setIndex(_index); + return currentValue(); +} + smt::Expression SymbolicVariable::increaseIndex() { ++(*m_ssa); @@ -179,6 +185,12 @@ smt::Expression SymbolicFunctionVariable::resetIndex() return m_abstract.resetIndex(); } +smt::Expression SymbolicFunctionVariable::setIndex(unsigned _index) +{ + SymbolicVariable::setIndex(_index); + return m_abstract.setIndex(_index); +} + smt::Expression SymbolicFunctionVariable::increaseIndex() { ++(*m_ssa); @@ -197,46 +209,6 @@ void SymbolicFunctionVariable::resetDeclaration() m_declaration = m_context.newVariable(currentName(), m_sort); } -SymbolicMappingVariable::SymbolicMappingVariable( - frontend::TypePointer _type, - string _uniqueName, - EncodingContext& _context -): - SymbolicVariable(_type, _type, move(_uniqueName), _context) -{ - solAssert(isMapping(m_type->category()), ""); -} - -SymbolicArrayVariable::SymbolicArrayVariable( - frontend::TypePointer _type, - frontend::TypePointer _originalType, - string _uniqueName, - EncodingContext& _context -): - SymbolicVariable(_type, _originalType, move(_uniqueName), _context) -{ - solAssert(isArray(m_type->category()), ""); -} - -SymbolicArrayVariable::SymbolicArrayVariable( - SortPointer _sort, - string _uniqueName, - EncodingContext& _context -): - SymbolicVariable(move(_sort), move(_uniqueName), _context) -{ - solAssert(m_sort->kind == Kind::Array, ""); -} - -smt::Expression SymbolicArrayVariable::currentValue(frontend::TypePointer const& _targetType) const -{ - optional conversion = symbolicTypeConversion(m_originalType, _targetType); - if (conversion) - return *conversion; - - return SymbolicVariable::currentValue(_targetType); -} - SymbolicEnumVariable::SymbolicEnumVariable( frontend::TypePointer _type, string _uniqueName, @@ -286,3 +258,62 @@ smt::Expression SymbolicTupleVariable::component( return smt::Expression::tuple_get(currentValue(), _index); } + +SymbolicArrayVariable::SymbolicArrayVariable( + frontend::TypePointer _type, + frontend::TypePointer _originalType, + string _uniqueName, + EncodingContext& _context +): + SymbolicVariable(_type, _originalType, move(_uniqueName), _context), + m_pair( + smtSort(*_type), + m_uniqueName + "_length_pair", + m_context + ) +{ + solAssert(isArray(m_type->category()) || isMapping(m_type->category()), ""); +} + +SymbolicArrayVariable::SymbolicArrayVariable( + SortPointer _sort, + string _uniqueName, + EncodingContext& _context +): + SymbolicVariable(move(_sort), move(_uniqueName), _context), + m_pair( + std::make_shared( + "array_length_pair", + std::vector{"array", "length"}, + std::vector{m_sort, SortProvider::intSort} + ), + m_uniqueName + "_array_length_pair", + m_context + ) +{ + solAssert(m_sort->kind == Kind::Array, ""); +} + +smt::Expression SymbolicArrayVariable::currentValue(frontend::TypePointer const& _targetType) const +{ + optional conversion = symbolicTypeConversion(m_originalType, _targetType); + if (conversion) + return *conversion; + + return m_pair.currentValue(); +} + +smt::Expression SymbolicArrayVariable::valueAtIndex(int _index) const +{ + return m_pair.valueAtIndex(_index); +} + +smt::Expression SymbolicArrayVariable::elements() +{ + return m_pair.component(0); +} + +smt::Expression SymbolicArrayVariable::length() +{ + return m_pair.component(1); +} diff --git a/libsolidity/formal/SymbolicVariables.h b/libsolidity/formal/SymbolicVariables.h index 6f7ad6ec4..3f5379d9b 100644 --- a/libsolidity/formal/SymbolicVariables.h +++ b/libsolidity/formal/SymbolicVariables.h @@ -56,6 +56,7 @@ public: virtual Expression valueAtIndex(int _index) const; virtual std::string nameAtIndex(int _index) const; virtual Expression resetIndex(); + virtual Expression setIndex(unsigned _index); virtual Expression increaseIndex(); virtual Expression operator()(std::vector /*_arguments*/) const { @@ -169,6 +170,7 @@ public: Expression functionValueAtIndex(int _index) const; Expression resetIndex() override; + Expression setIndex(unsigned _index) override; Expression increaseIndex() override; Expression operator()(std::vector _arguments) const override; @@ -189,42 +191,6 @@ private: }; }; -/** - * Specialization of SymbolicVariable for Mapping - */ -class SymbolicMappingVariable: public SymbolicVariable -{ -public: - SymbolicMappingVariable( - frontend::TypePointer _type, - std::string _uniqueName, - EncodingContext& _context - ); -}; - -/** - * Specialization of SymbolicVariable for Array - */ -class SymbolicArrayVariable: public SymbolicVariable -{ -public: - SymbolicArrayVariable( - frontend::TypePointer _type, - frontend::TypePointer _originalTtype, - std::string _uniqueName, - EncodingContext& _context - ); - SymbolicArrayVariable( - SortPointer _sort, - std::string _uniqueName, - EncodingContext& _context - ); - - SymbolicArrayVariable(SymbolicArrayVariable&&) = default; - - Expression currentValue(frontend::TypePointer const& _targetType = TypePointer{}) const override; -}; - /** * Specialization of SymbolicVariable for Enum */ @@ -263,4 +229,38 @@ public: ); }; +/** + * Specialization of SymbolicVariable for Array + */ +class SymbolicArrayVariable: public SymbolicVariable +{ +public: + SymbolicArrayVariable( + frontend::TypePointer _type, + frontend::TypePointer _originalTtype, + std::string _uniqueName, + EncodingContext& _context + ); + SymbolicArrayVariable( + SortPointer _sort, + std::string _uniqueName, + EncodingContext& _context + ); + + SymbolicArrayVariable(SymbolicArrayVariable&&) = default; + + Expression currentValue(frontend::TypePointer const& _targetType = TypePointer{}) const override; + Expression valueAtIndex(int _index) const override; + Expression resetIndex() override { SymbolicVariable::resetIndex(); return m_pair.resetIndex(); } + Expression setIndex(unsigned _index) override { SymbolicVariable::setIndex(_index); return m_pair.setIndex(_index); } + Expression increaseIndex() override { SymbolicVariable::increaseIndex(); return m_pair.increaseIndex(); } + Expression elements(); + Expression length(); + + SortPointer tupleSort() { return m_pair.sort(); } + +private: + SymbolicTupleVariable m_pair; +}; + } diff --git a/libsolidity/formal/Z3Interface.cpp b/libsolidity/formal/Z3Interface.cpp index a84f39bb1..d49314b6c 100644 --- a/libsolidity/formal/Z3Interface.cpp +++ b/libsolidity/formal/Z3Interface.cpp @@ -198,6 +198,15 @@ z3::expr Z3Interface::toZ3Expr(Expression const& _expr) size_t index = std::stoi(_expr.arguments[1].name); return z3::func_decl(m_context, Z3_get_tuple_sort_field_decl(m_context, z3Sort(*_expr.arguments[0].sort), index))(arguments[0]); } + else if (n == "tuple_constructor") + { + auto constructor = z3::func_decl(m_context, Z3_get_tuple_sort_mk_decl(m_context, z3Sort(*_expr.sort))); + solAssert(constructor.arity() == arguments.size(), ""); + z3::expr_vector args(m_context); + for (auto const& arg: arguments) + args.push_back(arg); + return constructor(args); + } solAssert(false, ""); } diff --git a/test/libsolidity/smtCheckerTests/array_members/length_1d_assignment_2d_memory_to_memory.sol b/test/libsolidity/smtCheckerTests/array_members/length_1d_assignment_2d_memory_to_memory.sol new file mode 100644 index 000000000..2e3ef86fd --- /dev/null +++ b/test/libsolidity/smtCheckerTests/array_members/length_1d_assignment_2d_memory_to_memory.sol @@ -0,0 +1,10 @@ +pragma experimental SMTChecker; +pragma experimental ABIEncoderV2; + +contract C { + function f(uint[][] memory arr) public pure { + uint[][] memory arr2 = arr; + assert(arr2[0].length == arr[0].length); + assert(arr.length == arr2.length); + } +} diff --git a/test/libsolidity/smtCheckerTests/array_members/length_1d_assignment_2d_storage_to_storage.sol b/test/libsolidity/smtCheckerTests/array_members/length_1d_assignment_2d_storage_to_storage.sol new file mode 100644 index 000000000..acf6a1e1d --- /dev/null +++ b/test/libsolidity/smtCheckerTests/array_members/length_1d_assignment_2d_storage_to_storage.sol @@ -0,0 +1,11 @@ +pragma experimental SMTChecker; +pragma experimental ABIEncoderV2; + +contract C { + uint[][] arr; + uint[][] arr2; + function f() public view { + assert(arr2[0].length == arr[0].length); + assert(arr2.length == arr.length); + } +} diff --git a/test/libsolidity/smtCheckerTests/array_members/length_1d_copy_2d_memory_to_storage.sol b/test/libsolidity/smtCheckerTests/array_members/length_1d_copy_2d_memory_to_storage.sol new file mode 100644 index 000000000..ce0d9ef5d --- /dev/null +++ b/test/libsolidity/smtCheckerTests/array_members/length_1d_copy_2d_memory_to_storage.sol @@ -0,0 +1,11 @@ +pragma experimental SMTChecker; +pragma experimental ABIEncoderV2; + +contract C { + uint[][] arr; + function f(uint[][] memory arr2) public { + arr = arr2; + assert(arr2[0].length == arr[0].length); + assert(arr2.length == arr.length); + } +} diff --git a/test/libsolidity/smtCheckerTests/array_members/length_1d_copy_2d_storage_to_memory.sol b/test/libsolidity/smtCheckerTests/array_members/length_1d_copy_2d_storage_to_memory.sol new file mode 100644 index 000000000..4aa03c222 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/array_members/length_1d_copy_2d_storage_to_memory.sol @@ -0,0 +1,11 @@ +pragma experimental SMTChecker; +pragma experimental ABIEncoderV2; + +contract C { + uint[][] arr; + function f() public view { + uint[][] memory arr2 = arr; + assert(arr2[0].length == arr[0].length); + assert(arr2.length == arr.length); + } +} diff --git a/test/libsolidity/smtCheckerTests/array_members/length_1d_mapping_array_1.sol b/test/libsolidity/smtCheckerTests/array_members/length_1d_mapping_array_1.sol new file mode 100644 index 000000000..dbce0665c --- /dev/null +++ b/test/libsolidity/smtCheckerTests/array_members/length_1d_mapping_array_1.sol @@ -0,0 +1,8 @@ +pragma experimental SMTChecker; + +contract C { + mapping (uint => uint[]) map; + function f() public view { + assert(map[0].length == map[1].length); + } +} diff --git a/test/libsolidity/smtCheckerTests/array_members/length_1d_mapping_array_2.sol b/test/libsolidity/smtCheckerTests/array_members/length_1d_mapping_array_2.sol new file mode 100644 index 000000000..dc2305f79 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/array_members/length_1d_mapping_array_2.sol @@ -0,0 +1,9 @@ +pragma experimental SMTChecker; + +contract C { + mapping (uint => uint[]) map; + function f(uint x, uint y) public view { + require(x == y); + assert(map[x].length == map[y].length); + } +} diff --git a/test/libsolidity/smtCheckerTests/array_members/length_1d_mapping_array_2d_1.sol b/test/libsolidity/smtCheckerTests/array_members/length_1d_mapping_array_2d_1.sol new file mode 100644 index 000000000..bdc24df30 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/array_members/length_1d_mapping_array_2d_1.sol @@ -0,0 +1,9 @@ +pragma experimental SMTChecker; + +contract C { + mapping (uint => uint[][]) map; + function f(uint x, uint y) public view { + require(x == y); + assert(map[x][0].length == map[y][0].length); + } +} diff --git a/test/libsolidity/smtCheckerTests/array_members/length_1d_struct_array_1.sol b/test/libsolidity/smtCheckerTests/array_members/length_1d_struct_array_1.sol new file mode 100644 index 000000000..68be993a8 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/array_members/length_1d_struct_array_1.sol @@ -0,0 +1,20 @@ +pragma experimental SMTChecker; + +contract C { + struct S { + uint[] arr; + } + S s1; + S s2; + function f() public view { + assert(s1.arr.length == s2.arr.length); + } +} +// ---- +// Warning: (76-80): Assertion checker does not yet support the type of this variable. +// Warning: (83-87): Assertion checker does not yet support the type of this variable. +// Warning: (126-132): Assertion checker does not yet support this expression. +// Warning: (126-128): Assertion checker does not yet implement type struct C.S storage ref +// Warning: (143-149): Assertion checker does not yet support this expression. +// Warning: (143-145): Assertion checker does not yet implement type struct C.S storage ref +// Warning: (119-157): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/array_members/length_1d_struct_array_2d_1.sol b/test/libsolidity/smtCheckerTests/array_members/length_1d_struct_array_2d_1.sol new file mode 100644 index 000000000..bb248c43e --- /dev/null +++ b/test/libsolidity/smtCheckerTests/array_members/length_1d_struct_array_2d_1.sol @@ -0,0 +1,22 @@ +pragma experimental SMTChecker; + +contract C { + struct S { + uint[][] arr; + } + S s1; + S s2; + function f() public view { + assert(s1.arr[0].length == s2.arr[0].length); + } +} +// ---- +// Warning: (78-82): Assertion checker does not yet support the type of this variable. +// Warning: (85-89): Assertion checker does not yet support the type of this variable. +// Warning: (128-134): Assertion checker does not yet support this expression. +// Warning: (128-130): Assertion checker does not yet implement type struct C.S storage ref +// Warning: (128-137): Assertion checker does not yet implement this expression. +// Warning: (148-154): Assertion checker does not yet support this expression. +// Warning: (148-150): Assertion checker does not yet implement type struct C.S storage ref +// Warning: (148-157): Assertion checker does not yet implement this expression. +// Warning: (121-165): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/array_members/length_assignment_2d_memory_to_memory.sol b/test/libsolidity/smtCheckerTests/array_members/length_assignment_2d_memory_to_memory.sol new file mode 100644 index 000000000..d85f01104 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/array_members/length_assignment_2d_memory_to_memory.sol @@ -0,0 +1,9 @@ +pragma experimental SMTChecker; +pragma experimental ABIEncoderV2; + +contract C { + function f(uint[][] memory arr) public pure { + uint[][] memory arr2 = arr; + assert(arr2.length == arr.length); + } +} diff --git a/test/libsolidity/smtCheckerTests/array_members/length_assignment_memory_to_memory.sol b/test/libsolidity/smtCheckerTests/array_members/length_assignment_memory_to_memory.sol new file mode 100644 index 000000000..66f6d1067 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/array_members/length_assignment_memory_to_memory.sol @@ -0,0 +1,8 @@ +pragma experimental SMTChecker; + +contract C { + function f(uint[] memory arr) public pure { + uint[] memory arr2 = arr; + assert(arr2.length == arr.length); + } +} diff --git a/test/libsolidity/smtCheckerTests/array_members/length_assignment_storage_to_storage.sol b/test/libsolidity/smtCheckerTests/array_members/length_assignment_storage_to_storage.sol new file mode 100644 index 000000000..c379f3381 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/array_members/length_assignment_storage_to_storage.sol @@ -0,0 +1,10 @@ +pragma experimental SMTChecker; + +contract C { + uint[] arr; + uint[] arr2; + function f() public { + arr2 = arr; + assert(arr2.length == arr.length); + } +} diff --git a/test/libsolidity/smtCheckerTests/array_members/length_basic.sol b/test/libsolidity/smtCheckerTests/array_members/length_basic.sol new file mode 100644 index 000000000..cd1041f7c --- /dev/null +++ b/test/libsolidity/smtCheckerTests/array_members/length_basic.sol @@ -0,0 +1,13 @@ +pragma experimental SMTChecker; + +contract C { + uint[] arr; + function f() public view { + uint x = arr.length; + uint y = x; + assert(arr.length == y); + assert(arr.length != y); + } +} +// ---- +// Warning: (153-176): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/array_members/length_copy_memory_to_storage.sol b/test/libsolidity/smtCheckerTests/array_members/length_copy_memory_to_storage.sol new file mode 100644 index 000000000..ec6c2a2f2 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/array_members/length_copy_memory_to_storage.sol @@ -0,0 +1,9 @@ +pragma experimental SMTChecker; + +contract C { + uint[] arr; + function f(uint[] memory marr) public { + arr = marr; + assert(marr.length == arr.length); + } +} diff --git a/test/libsolidity/smtCheckerTests/array_members/length_copy_storage_to_memory.sol b/test/libsolidity/smtCheckerTests/array_members/length_copy_storage_to_memory.sol new file mode 100644 index 000000000..20e83c908 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/array_members/length_copy_storage_to_memory.sol @@ -0,0 +1,9 @@ +pragma experimental SMTChecker; + +contract C { + uint[] arr; + function f() public view { + uint[] memory marr = arr; + assert(marr.length == arr.length); + } +} diff --git a/test/libsolidity/smtCheckerTests/array_members/length_function_call.sol b/test/libsolidity/smtCheckerTests/array_members/length_function_call.sol new file mode 100644 index 000000000..250c88666 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/array_members/length_function_call.sol @@ -0,0 +1,10 @@ +pragma experimental SMTChecker; + +contract C { + uint[] arr; + function f() public view { + assert(arr.length == g().length); + } + function g() internal pure returns (uint[] memory) { + } +} diff --git a/test/libsolidity/smtCheckerTests/array_members/length_same_after_assignment.sol b/test/libsolidity/smtCheckerTests/array_members/length_same_after_assignment.sol new file mode 100644 index 000000000..e0d13b35a --- /dev/null +++ b/test/libsolidity/smtCheckerTests/array_members/length_same_after_assignment.sol @@ -0,0 +1,10 @@ +pragma experimental SMTChecker; + +contract C { + uint[] arr; + function f() public view { + uint[] memory arr2 = arr; + arr2[2] = 3; + assert(arr.length == arr2.length); + } +} diff --git a/test/libsolidity/smtCheckerTests/array_members/length_same_after_assignment_2.sol b/test/libsolidity/smtCheckerTests/array_members/length_same_after_assignment_2.sol new file mode 100644 index 000000000..9665c0317 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/array_members/length_same_after_assignment_2.sol @@ -0,0 +1,15 @@ +pragma experimental SMTChecker; + +contract C { + uint[][] arr; + uint[][] arr2; + function f() public { + uint x = arr[2].length; + uint y = arr[3].length; + uint z = arr.length; + arr[2][333] = 444; + assert(arr[2].length == x); + assert(arr[3].length == y); + assert(arr.length == z); + } +} diff --git a/test/libsolidity/smtCheckerTests/array_members/length_same_after_assignment_2_fail.sol b/test/libsolidity/smtCheckerTests/array_members/length_same_after_assignment_2_fail.sol new file mode 100644 index 000000000..e5356d240 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/array_members/length_same_after_assignment_2_fail.sol @@ -0,0 +1,19 @@ +pragma experimental SMTChecker; + +contract C { + uint[][] arr; + uint[][] arr2; + function f() public { + uint x = arr[2].length; + uint y = arr[3].length; + uint z = arr.length; + arr[2][333] = 444; + assert(arr[2].length != x); + assert(arr[3].length != y); + assert(arr.length != z); + } +} +// ---- +// Warning: (198-224): Assertion violation happens here +// Warning: (228-254): Assertion violation happens here +// Warning: (258-281): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/array_members/length_same_after_assignment_3.sol b/test/libsolidity/smtCheckerTests/array_members/length_same_after_assignment_3.sol new file mode 100644 index 000000000..c36d55e76 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/array_members/length_same_after_assignment_3.sol @@ -0,0 +1,17 @@ +pragma experimental SMTChecker; + +contract C { + uint[][] arr; + uint[][] arr2; + function f() public { + uint x = arr[2].length; + uint y = arr[3].length; + uint z = arr.length; + uint t = arr[5].length; + arr[5] = arr[8]; + assert(arr[2].length == x); + assert(arr[3].length == y); + assert(arr.length == z); + assert(arr[5].length == t); + } +} diff --git a/test/libsolidity/smtCheckerTests/array_members/length_same_after_assignment_3_fail.sol b/test/libsolidity/smtCheckerTests/array_members/length_same_after_assignment_3_fail.sol new file mode 100644 index 000000000..92da0cf61 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/array_members/length_same_after_assignment_3_fail.sol @@ -0,0 +1,22 @@ +pragma experimental SMTChecker; + +contract C { + uint[][] arr; + uint[][] arr2; + function f() public { + uint x = arr[2].length; + uint y = arr[3].length; + uint z = arr.length; + uint t = arr[5].length; + arr[5] = arr[8]; + assert(arr[2].length != x); + assert(arr[3].length != y); + assert(arr.length != z); + assert(arr[5].length != t); + } +} +// ---- +// Warning: (222-248): Assertion violation happens here +// Warning: (252-278): Assertion violation happens here +// Warning: (282-305): Assertion violation happens here +// Warning: (309-335): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/complex/MerkleProof.sol b/test/libsolidity/smtCheckerTests/complex/MerkleProof.sol index 955d5fd1e..aa69285ba 100644 --- a/test/libsolidity/smtCheckerTests/complex/MerkleProof.sol +++ b/test/libsolidity/smtCheckerTests/complex/MerkleProof.sol @@ -34,9 +34,7 @@ library MerkleProof { } // ---- -// Warning: (755-767): Assertion checker does not yet support this expression. // Warning: (988-991): Assertion checker does not yet implement type abi // Warning: (988-1032): Assertion checker does not yet implement this type of function call. // Warning: (1175-1178): Assertion checker does not yet implement type abi // Warning: (1175-1219): Assertion checker does not yet implement this type of function call. -// Warning: (755-767): Assertion checker does not yet support this expression. diff --git a/test/libsolidity/smtCheckerTests/operators/compound_assignment_division_2.sol b/test/libsolidity/smtCheckerTests/operators/compound_assignment_division_2.sol index 83bd7cb6b..230d5f33c 100644 --- a/test/libsolidity/smtCheckerTests/operators/compound_assignment_division_2.sol +++ b/test/libsolidity/smtCheckerTests/operators/compound_assignment_division_2.sol @@ -10,6 +10,5 @@ contract C { } } // ---- -// Warning: (163-184): Error trying to invoke SMT solver. // Warning: (188-209): Error trying to invoke SMT solver. // Warning: (188-209): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/operators/compound_assignment_division_3.sol b/test/libsolidity/smtCheckerTests/operators/compound_assignment_division_3.sol index b941a5767..6449db84c 100644 --- a/test/libsolidity/smtCheckerTests/operators/compound_assignment_division_3.sol +++ b/test/libsolidity/smtCheckerTests/operators/compound_assignment_division_3.sol @@ -10,6 +10,5 @@ contract C { } } // ---- -// Warning: (171-190): Error trying to invoke SMT solver. // Warning: (194-213): Error trying to invoke SMT solver. // Warning: (194-213): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/operators/compound_mul_array_index.sol b/test/libsolidity/smtCheckerTests/operators/compound_mul_array_index.sol index 110eb868e..0c4fc0876 100644 --- a/test/libsolidity/smtCheckerTests/operators/compound_mul_array_index.sol +++ b/test/libsolidity/smtCheckerTests/operators/compound_mul_array_index.sol @@ -12,4 +12,5 @@ contract C } } // ---- +// Warning: (191-212): Error trying to invoke SMT solver. // Warning: (191-212): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/operators/compound_mul_mapping.sol b/test/libsolidity/smtCheckerTests/operators/compound_mul_mapping.sol index cd73bc687..f7dcd1469 100644 --- a/test/libsolidity/smtCheckerTests/operators/compound_mul_mapping.sol +++ b/test/libsolidity/smtCheckerTests/operators/compound_mul_mapping.sol @@ -12,4 +12,5 @@ contract C } } // ---- +// Warning: (197-216): Error trying to invoke SMT solver. // Warning: (197-216): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/operators/delete_array_index_2d.sol b/test/libsolidity/smtCheckerTests/operators/delete_array_index_2d.sol index a47763c03..1892441ca 100644 --- a/test/libsolidity/smtCheckerTests/operators/delete_array_index_2d.sol +++ b/test/libsolidity/smtCheckerTests/operators/delete_array_index_2d.sol @@ -4,6 +4,7 @@ contract C { uint[][] a; function f(bool b) public { + a[1][1] = 512; a[2][3] = 4; if (b) delete a; @@ -16,3 +17,4 @@ contract C // ==== // SMTSolvers: z3 // ---- +// Warning: (191-211): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/special/msg_data.sol b/test/libsolidity/smtCheckerTests/special/msg_data.sol index dff997395..9db24dbcb 100644 --- a/test/libsolidity/smtCheckerTests/special/msg_data.sol +++ b/test/libsolidity/smtCheckerTests/special/msg_data.sol @@ -7,5 +7,4 @@ contract C } } // ---- -// Warning: (86-101): Assertion checker does not yet support this expression. // Warning: (79-106): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/types/mapping_aliasing_2.sol b/test/libsolidity/smtCheckerTests/types/mapping_aliasing_2.sol index f31192b3a..6bf521749 100644 --- a/test/libsolidity/smtCheckerTests/types/mapping_aliasing_2.sol +++ b/test/libsolidity/smtCheckerTests/types/mapping_aliasing_2.sol @@ -30,6 +30,7 @@ contract C } } // ---- +// Warning: (670-690): Error trying to invoke SMT solver. // Warning: (397-417): Assertion violation happens here // Warning: (463-481): Assertion violation happens here // Warning: (533-557): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/types/string_1.sol b/test/libsolidity/smtCheckerTests/types/string_1.sol index 7f03c29da..2f2f64488 100644 --- a/test/libsolidity/smtCheckerTests/types/string_1.sol +++ b/test/libsolidity/smtCheckerTests/types/string_1.sol @@ -7,6 +7,4 @@ contract C } } // ---- -// Warning: (117-133): Assertion checker does not yet support this expression. -// Warning: (137-153): Assertion checker does not yet support this expression. // Warning: (110-154): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTestsJSON/multi.json b/test/libsolidity/smtCheckerTestsJSON/multi.json index b1be75073..986429dac 100644 --- a/test/libsolidity/smtCheckerTestsJSON/multi.json +++ b/test/libsolidity/smtCheckerTestsJSON/multi.json @@ -3,8 +3,8 @@ { "smtlib2responses": { - "0x9c50514d749eabf3c13d97ad7d787e682dd99a114bad652b10a01b8c6ad6c1fb": "sat\n((|EVALEXPR_0| 1))\n", - "0xb524e7c577188e2e36f0e67fead51269fa0f8b8fb41bff2d973dcf584d38cd1e": "sat\n((|EVALEXPR_0| 0))\n" + "0x45598870c7c0bc4c4f61acad7e0dd9399fb28aa3df198379dd36a95d70814ef8": "sat\n((|EVALEXPR_0| 1))\n", + "0xee335f8104fdb81b6e5fb418725923b81f7d78ffbd6bf95fb82e5593a1ac366a": "sat\n((|EVALEXPR_0| 0))\n" } } } diff --git a/test/libsolidity/smtCheckerTestsJSON/simple.json b/test/libsolidity/smtCheckerTestsJSON/simple.json index 89eac1b80..0b70ea24b 100644 --- a/test/libsolidity/smtCheckerTestsJSON/simple.json +++ b/test/libsolidity/smtCheckerTestsJSON/simple.json @@ -3,7 +3,7 @@ { "smtlib2responses": { - "0x45c37a9829e623d7838d82b547d297cd446d6b5faff36c53a56862fcee50fb41": "sat\n((|EVALEXPR_0| 0))\n" + "0x535c76d6b87d14bd4b4bf1014d14b8e91b648f073a68f9f267c4fe1df570bc14": "sat\n((|EVALEXPR_0| 0))\n" } } }