/* This file is part of solidity. solidity is free software: you can redistribute it and/or modify it under the terms of the GNU General Public License as published by the Free Software Foundation, either version 3 of the License, or (at your option) any later version. solidity is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License for more details. You should have received a copy of the GNU General Public License along with solidity. If not, see . */ // SPDX-License-Identifier: GPL-3.0 #include #include #include #include #include #include #include #include #include #include #include #include #include #include using namespace std; using namespace solidity; using namespace solidity::util; using namespace solidity::langutil; using namespace solidity::frontend; SMTEncoder::SMTEncoder( smt::EncodingContext& _context, ModelCheckerSettings _settings, UniqueErrorReporter& _errorReporter, UniqueErrorReporter& _unsupportedErrorReporter, langutil::CharStreamProvider const& _charStreamProvider ): m_errorReporter(_errorReporter), m_unsupportedErrors(_unsupportedErrorReporter), m_context(_context), m_settings(std::move(_settings)), m_charStreamProvider(_charStreamProvider) { } void SMTEncoder::resetSourceAnalysis() { m_freeFunctions.clear(); } bool SMTEncoder::visit(ContractDefinition const& _contract) { solAssert(m_currentContract, ""); for (auto const& node: _contract.subNodes()) if ( !dynamic_pointer_cast(node) && !dynamic_pointer_cast(node) ) node->accept(*this); for (auto const& base: _contract.annotation().linearizedBaseContracts) { // Look for all the constructor invocations bottom up. if (auto const& constructor = base->constructor()) for (auto const& invocation: constructor->modifiers()) { auto refDecl = invocation->name().annotation().referencedDeclaration; if (auto const& baseContract = dynamic_cast(refDecl)) { solAssert(!m_baseConstructorCalls.count(baseContract), ""); m_baseConstructorCalls[baseContract] = invocation.get(); } } } // Functions are visited first since they might be used // for state variable initialization which is part of // the constructor. // Constructors are visited as part of the constructor // hierarchy inlining. for (auto const* function: contractFunctionsWithoutVirtual(_contract) + allFreeFunctions()) if (!function->isConstructor()) function->accept(*this); // Constructors need to be handled by the engines separately. return false; } void SMTEncoder::endVisit(ContractDefinition const& _contract) { m_context.resetAllVariables(); m_baseConstructorCalls.clear(); solAssert(m_currentContract == &_contract, ""); m_currentContract = nullptr; if (m_callStack.empty()) m_context.popSolver(); } bool SMTEncoder::visit(ImportDirective const&) { // do not visit because the identifier therein will confuse us. return false; } void SMTEncoder::endVisit(VariableDeclaration const& _varDecl) { // State variables are handled by the constructor. if (_varDecl.isLocalVariable() &&_varDecl.value()) assignment(_varDecl, *_varDecl.value()); } bool SMTEncoder::visit(ModifierDefinition const&) { return false; } bool SMTEncoder::visit(FunctionDefinition const& _function) { solAssert(m_currentContract, ""); m_modifierDepthStack.push_back(-1); initializeLocalVariables(_function); _function.parameterList().accept(*this); if (_function.returnParameterList()) _function.returnParameterList()->accept(*this); visitFunctionOrModifier(); return false; } void SMTEncoder::visitFunctionOrModifier() { solAssert(!m_callStack.empty(), ""); solAssert(!m_modifierDepthStack.empty(), ""); ++m_modifierDepthStack.back(); FunctionDefinition const& function = dynamic_cast(*m_callStack.back().first); if (m_modifierDepthStack.back() == static_cast(function.modifiers().size())) { if (function.isImplemented()) { pushInlineFrame(function); function.body().accept(*this); popInlineFrame(function); } } else { solAssert(m_modifierDepthStack.back() < static_cast(function.modifiers().size()), ""); ASTPointer const& modifierInvocation = function.modifiers()[static_cast(m_modifierDepthStack.back())]; solAssert(modifierInvocation, ""); auto refDecl = modifierInvocation->name().annotation().referencedDeclaration; if (dynamic_cast(refDecl)) visitFunctionOrModifier(); else if (auto modifier = resolveModifierInvocation(*modifierInvocation, m_currentContract)) { m_scopes.push_back(modifier); inlineModifierInvocation(modifierInvocation.get(), modifier); solAssert(m_scopes.back() == modifier, ""); m_scopes.pop_back(); } else solAssert(false, ""); } --m_modifierDepthStack.back(); } void SMTEncoder::inlineModifierInvocation(ModifierInvocation const* _invocation, CallableDeclaration const* _definition) { solAssert(_invocation, ""); _invocation->accept(*this); vector args; if (auto const* arguments = _invocation->arguments()) { auto const& modifierParams = _definition->parameters(); solAssert(modifierParams.size() == arguments->size(), ""); for (unsigned i = 0; i < arguments->size(); ++i) args.push_back(expr(*arguments->at(i), modifierParams.at(i)->type())); } initializeFunctionCallParameters(*_definition, args); pushCallStack({_definition, _invocation}); pushInlineFrame(*_definition); if (auto modifier = dynamic_cast(_definition)) { if (modifier->isImplemented()) modifier->body().accept(*this); popCallStack(); } else if (auto function = dynamic_cast(_definition)) { if (function->isImplemented()) function->accept(*this); // Functions are popped from the callstack in endVisit(FunctionDefinition) } popInlineFrame(*_definition); } void SMTEncoder::inlineConstructorHierarchy(ContractDefinition const& _contract) { auto const& hierarchy = m_currentContract->annotation().linearizedBaseContracts; auto it = find(begin(hierarchy), end(hierarchy), &_contract); solAssert(it != end(hierarchy), ""); auto nextBase = it + 1; // Initialize the base contracts here as long as their constructors are implicit, // stop when the first explicit constructor is found. while (nextBase != end(hierarchy)) { if (auto baseConstructor = (*nextBase)->constructor()) { createLocalVariables(*baseConstructor); // If any subcontract explicitly called baseConstructor, use those arguments. if (m_baseConstructorCalls.count(*nextBase)) inlineModifierInvocation(m_baseConstructorCalls.at(*nextBase), baseConstructor); else if (baseConstructor->isImplemented()) { // The first constructor found is handled like a function // and its pushed into the callstack there. // This if avoids duplication in the callstack. if (!m_callStack.empty()) pushCallStack({baseConstructor, nullptr}); baseConstructor->accept(*this); // popped by endVisit(FunctionDefinition) } break; } else { initializeStateVariables(**nextBase); ++nextBase; } } initializeStateVariables(_contract); } bool SMTEncoder::visit(PlaceholderStatement const&) { solAssert(!m_callStack.empty(), ""); auto lastCall = popCallStack(); visitFunctionOrModifier(); pushCallStack(lastCall); return true; } void SMTEncoder::endVisit(FunctionDefinition const&) { solAssert(m_currentContract, ""); popCallStack(); solAssert(m_modifierDepthStack.back() == -1, ""); m_modifierDepthStack.pop_back(); if (m_callStack.empty()) m_context.popSolver(); } bool SMTEncoder::visit(Block const& _block) { if (_block.unchecked()) { solAssert(m_checked, ""); m_checked = false; } return true; } void SMTEncoder::endVisit(Block const& _block) { if (_block.unchecked()) { solAssert(!m_checked, ""); m_checked = true; } } bool SMTEncoder::visit(InlineAssembly const& _inlineAsm) { /// This is very similar to `yul::Assignments`, except I need to collect `Identifier`s and not just names as `YulString`s. struct AssignedExternalsCollector: public yul::ASTWalker { AssignedExternalsCollector(InlineAssembly const& _inlineAsm): externalReferences(_inlineAsm.annotation().externalReferences) { this->operator()(_inlineAsm.operations()); } map const& externalReferences; set assignedVars; using yul::ASTWalker::operator(); void operator()(yul::Assignment const& _assignment) { auto const& vars = _assignment.variableNames; for (auto const& identifier: vars) if (auto externalInfo = util::valueOrNullptr(externalReferences, &identifier)) if (auto varDecl = dynamic_cast(externalInfo->declaration)) assignedVars.insert(varDecl); } }; yul::SideEffectsCollector sideEffectsCollector(_inlineAsm.dialect(), _inlineAsm.operations()); if (sideEffectsCollector.invalidatesMemory()) resetMemoryVariables(); if (sideEffectsCollector.invalidatesStorage()) resetStorageVariables(); auto assignedVars = AssignedExternalsCollector(_inlineAsm).assignedVars; for (auto const* var: assignedVars) { solAssert(var, ""); solAssert(var->isLocalVariable(), "Non-local variable assigned in inlined assembly"); m_context.resetVariable(*var); } m_unsupportedErrors.warning( 7737_error, _inlineAsm.location(), "Inline assembly may cause SMTChecker to produce spurious warnings (false positives)." ); return false; } void SMTEncoder::pushInlineFrame(CallableDeclaration const&) { pushPathCondition(currentPathConditions()); } void SMTEncoder::popInlineFrame(CallableDeclaration const&) { popPathCondition(); } void SMTEncoder::endVisit(VariableDeclarationStatement const& _varDecl) { if (auto init = _varDecl.initialValue()) expressionToTupleAssignment(_varDecl.declarations(), *init); } bool SMTEncoder::visit(Assignment const& _assignment) { // RHS must be visited before LHS; as opposed to what Assignment::accept does _assignment.rightHandSide().accept(*this); _assignment.leftHandSide().accept(*this); return false; } void SMTEncoder::endVisit(Assignment const& _assignment) { createExpr(_assignment); Token op = _assignment.assignmentOperator(); solAssert(TokenTraits::isAssignmentOp(op), ""); if (!isSupportedType(*_assignment.annotation().type)) { // Give it a new index anyway to keep the SSA scheme sound. Expression const* base = &_assignment.leftHandSide(); if (auto const* indexAccess = dynamic_cast(base)) base = leftmostBase(*indexAccess); if (auto varDecl = identifierToVariable(*base)) m_context.newValue(*varDecl); } else { if (dynamic_cast(_assignment.rightHandSide().annotation().type)) tupleAssignment(_assignment.leftHandSide(), _assignment.rightHandSide()); else { auto const& type = _assignment.annotation().type; auto rightHandSide = op == Token::Assign ? expr(_assignment.rightHandSide(), type) : compoundAssignment(_assignment); defineExpr(_assignment, rightHandSide); assignment( _assignment.leftHandSide(), expr(_assignment, type), type ); } } } void SMTEncoder::endVisit(TupleExpression const& _tuple) { if (_tuple.annotation().type->category() == Type::Category::Function) return; if (_tuple.annotation().type->category() == Type::Category::TypeType) return; createExpr(_tuple); if (_tuple.isInlineArray()) { // Add constraints for the length and values as it is known. auto symbArray = dynamic_pointer_cast(m_context.expression(_tuple)); solAssert(symbArray, ""); addArrayLiteralAssertions(*symbArray, applyMap(_tuple.components(), [&](auto const& c) { return expr(*c); })); } else { auto values = applyMap(_tuple.components(), [this](auto const& component) -> optional { if (component) { if (!m_context.knownExpression(*component)) createExpr(*component); return expr(*component); } return {}; }); defineExpr(_tuple, values); } } void SMTEncoder::endVisit(UnaryOperation const& _op) { /// We need to shortcut here due to potentially unknown /// rational number sizes. if (_op.annotation().type->category() == Type::Category::RationalNumber) return; if (TokenTraits::isBitOp(_op.getOperator()) && !*_op.annotation().userDefinedFunction) return bitwiseNotOperation(_op); createExpr(_op); // User-defined operators are essentially function calls. if (*_op.annotation().userDefinedFunction) { // TODO: Implement user-defined operators properly. m_unsupportedErrors.warning( 6156_error, _op.location(), "User-defined operators are not yet supported by SMTChecker. "s + "This invocation of operator " + TokenTraits::friendlyName(_op.getOperator()) + " has been ignored, which may lead to incorrect results." ); return; } auto const* subExpr = innermostTuple(_op.subExpression()); auto type = _op.annotation().type; switch (_op.getOperator()) { case Token::Not: // ! { solAssert(smt::isBool(*type), ""); defineExpr(_op, !expr(*subExpr)); break; } case Token::Inc: // ++ (pre- or postfix) case Token::Dec: // -- (pre- or postfix) { solAssert(smt::isInteger(*type) || smt::isFixedPoint(*type), ""); solAssert(subExpr->annotation().willBeWrittenTo, ""); auto innerValue = expr(*subExpr); auto newValue = arithmeticOperation( _op.getOperator() == Token::Inc ? Token::Add : Token::Sub, innerValue, smtutil::Expression(size_t(1)), _op.annotation().type, _op ).first; defineExpr(_op, _op.isPrefixOperation() ? newValue : innerValue); assignment(*subExpr, newValue); break; } case Token::Sub: // - { defineExpr(_op, 0 - expr(*subExpr)); break; } case Token::Delete: { if (auto decl = identifierToVariable(*subExpr)) { m_context.newValue(*decl); m_context.setZeroValue(*decl); } else { solAssert(m_context.knownExpression(*subExpr), ""); auto const& symbVar = m_context.expression(*subExpr); symbVar->increaseIndex(); m_context.setZeroValue(*symbVar); if ( dynamic_cast(subExpr) || dynamic_cast(subExpr) ) indexOrMemberAssignment(*subExpr, symbVar->currentValue()); // Empty push added a zero value anyway, so no need to delete extra. else if (!isEmptyPush(*subExpr)) solAssert(false, ""); } break; } default: solAssert(false, ""); } } bool SMTEncoder::visit(UnaryOperation const& _op) { return !shortcutRationalNumber(_op); } bool SMTEncoder::visit(BinaryOperation const& _op) { if (shortcutRationalNumber(_op)) return false; if (TokenTraits::isBooleanOp(_op.getOperator()) && !*_op.annotation().userDefinedFunction) { booleanOperation(_op); return false; } return true; } void SMTEncoder::endVisit(BinaryOperation const& _op) { /// If _op is const evaluated the RationalNumber shortcut was taken. if (isConstant(_op)) return; if (TokenTraits::isBooleanOp(_op.getOperator()) && !*_op.annotation().userDefinedFunction) return; createExpr(_op); // User-defined operators are essentially function calls. if (*_op.annotation().userDefinedFunction) { // TODO: Implement user-defined operators properly. m_unsupportedErrors.warning( 6756_error, _op.location(), "User-defined operators are not yet supported by SMTChecker. "s + "This invocation of operator " + TokenTraits::friendlyName(_op.getOperator()) + " has been ignored, which may lead to incorrect results." ); return; } if (TokenTraits::isArithmeticOp(_op.getOperator())) arithmeticOperation(_op); else if (TokenTraits::isCompareOp(_op.getOperator())) compareOperation(_op); else if (TokenTraits::isBitOp(_op.getOperator()) || TokenTraits::isShiftOp(_op.getOperator())) bitwiseOperation(_op); else solAssert(false, ""); } bool SMTEncoder::visit(Conditional const& _op) { _op.condition().accept(*this); auto indicesEndTrue = visitBranch(&_op.trueExpression(), expr(_op.condition())).first; auto indicesEndFalse = visitBranch(&_op.falseExpression(), !expr(_op.condition())).first; mergeVariables(expr(_op.condition()), indicesEndTrue, indicesEndFalse); defineExpr(_op, smtutil::Expression::ite( expr(_op.condition()), expr(_op.trueExpression(), _op.annotation().type), expr(_op.falseExpression(), _op.annotation().type) )); return false; } bool SMTEncoder::visit(FunctionCall const& _funCall) { auto functionCallKind = *_funCall.annotation().kind; if (functionCallKind != FunctionCallKind::FunctionCall) return true; FunctionType const& funType = dynamic_cast(*_funCall.expression().annotation().type); // We do not want to visit the TypeTypes in the second argument of `abi.decode`. // Those types are checked/used in SymbolicState::buildABIFunctions. if (funType.kind() == FunctionType::Kind::ABIDecode) { if (auto arg = _funCall.arguments().front()) arg->accept(*this); return false; } // We do not really need to visit the expression in a wrap/unwrap no-op call, // so we just ignore the function call expression to avoid "unsupported" warnings. else if ( funType.kind() == FunctionType::Kind::Wrap || funType.kind() == FunctionType::Kind::Unwrap ) { if (auto arg = _funCall.arguments().front()) arg->accept(*this); return false; } return true; } void SMTEncoder::endVisit(FunctionCall const& _funCall) { auto functionCallKind = *_funCall.annotation().kind; createExpr(_funCall); if (functionCallKind == FunctionCallKind::StructConstructorCall) { visitStructConstructorCall(_funCall); return; } if (functionCallKind == FunctionCallKind::TypeConversion) { visitTypeConversion(_funCall); return; } FunctionType const& funType = dynamic_cast(*_funCall.expression().annotation().type); std::vector> const args = _funCall.arguments(); switch (funType.kind()) { case FunctionType::Kind::Assert: visitAssert(_funCall); break; case FunctionType::Kind::Require: visitRequire(_funCall); break; case FunctionType::Kind::Revert: // Revert is a special case of require and equals to `require(false)` addPathImpliedExpression(smtutil::Expression(false)); break; case FunctionType::Kind::GasLeft: visitGasLeft(_funCall); break; case FunctionType::Kind::External: if (publicGetter(_funCall.expression())) visitPublicGetter(_funCall); break; case FunctionType::Kind::ABIDecode: case FunctionType::Kind::ABIEncode: case FunctionType::Kind::ABIEncodePacked: case FunctionType::Kind::ABIEncodeWithSelector: case FunctionType::Kind::ABIEncodeCall: case FunctionType::Kind::ABIEncodeWithSignature: visitABIFunction(_funCall); break; case FunctionType::Kind::Internal: case FunctionType::Kind::BareStaticCall: case FunctionType::Kind::BareCall: break; case FunctionType::Kind::KECCAK256: case FunctionType::Kind::ECRecover: case FunctionType::Kind::SHA256: case FunctionType::Kind::RIPEMD160: visitCryptoFunction(_funCall); break; case FunctionType::Kind::BlockHash: defineExpr(_funCall, state().blockhash(expr(*_funCall.arguments().at(0)))); break; case FunctionType::Kind::AddMod: case FunctionType::Kind::MulMod: visitAddMulMod(_funCall); break; case FunctionType::Kind::Unwrap: case FunctionType::Kind::Wrap: visitWrapUnwrap(_funCall); break; case FunctionType::Kind::Send: case FunctionType::Kind::Transfer: { auto const& memberAccess = dynamic_cast(_funCall.expression()); auto const& address = memberAccess.expression(); auto const& value = args.front(); solAssert(value, ""); smtutil::Expression thisBalance = state().balance(); setSymbolicUnknownValue(thisBalance, TypeProvider::uint256(), m_context); state().transfer(state().thisAddress(), expr(address), expr(*value)); break; } case FunctionType::Kind::ArrayPush: arrayPush(_funCall); break; case FunctionType::Kind::ArrayPop: arrayPop(_funCall); break; case FunctionType::Kind::Event: case FunctionType::Kind::Error: // This can be safely ignored. break; case FunctionType::Kind::ObjectCreation: visitObjectCreation(_funCall); return; case FunctionType::Kind::Creation: if (!m_settings.engine.chc || !m_settings.externalCalls.isTrusted()) m_unsupportedErrors.warning( 8729_error, _funCall.location(), "Contract deployment is only supported in the trusted mode for external calls" " with the CHC engine." ); break; case FunctionType::Kind::DelegateCall: case FunctionType::Kind::BareCallCode: case FunctionType::Kind::BareDelegateCall: default: m_unsupportedErrors.warning( 4588_error, _funCall.location(), "Assertion checker does not yet implement this type of function call." ); } } bool SMTEncoder::visit(ModifierInvocation const& _node) { if (auto const* args = _node.arguments()) for (auto const& arg: *args) if (arg) arg->accept(*this); return false; } void SMTEncoder::initContract(ContractDefinition const& _contract) { solAssert(m_currentContract == nullptr, ""); m_currentContract = &_contract; m_context.reset(); m_context.pushSolver(); createStateVariables(_contract); clearIndices(m_currentContract, nullptr); m_variableUsage.setCurrentContract(_contract); m_checked = true; } void SMTEncoder::initFunction(FunctionDefinition const& _function) { solAssert(m_callStack.empty(), ""); solAssert(m_currentContract, ""); m_context.pushSolver(); m_pathConditions.clear(); pushCallStack({&_function, nullptr}); m_uninterpretedTerms.clear(); createStateVariables(*m_currentContract); createLocalVariables(_function); m_arrayAssignmentHappened = false; clearIndices(m_currentContract, &_function); m_checked = true; } void SMTEncoder::visitAssert(FunctionCall const& _funCall) { auto const& args = _funCall.arguments(); solAssert(args.size() == 1, ""); solAssert(args.front()->annotation().type->category() == Type::Category::Bool, ""); } void SMTEncoder::visitRequire(FunctionCall const& _funCall) { auto const& args = _funCall.arguments(); solAssert(args.size() >= 1, ""); solAssert(args.front()->annotation().type->category() == Type::Category::Bool, ""); addPathImpliedExpression(expr(*args.front())); } void SMTEncoder::visitABIFunction(FunctionCall const& _funCall) { auto symbFunction = state().abiFunction(&_funCall); auto const& [name, inTypes, outTypes] = state().abiFunctionTypes(&_funCall); auto const& funType = dynamic_cast(*_funCall.expression().annotation().type); auto kind = funType.kind(); auto const& args = _funCall.sortedArguments(); auto argsActualLength = kind == FunctionType::Kind::ABIDecode ? 1 : args.size(); solAssert(inTypes.size() == argsActualLength, ""); if (argsActualLength == 0) { defineExpr(_funCall, smt::zeroValue(TypeProvider::bytesMemory())); return; } vector symbArgs; for (unsigned i = 0; i < argsActualLength; ++i) if (args.at(i)) symbArgs.emplace_back(expr(*args.at(i), inTypes.at(i))); optional arg; if (inTypes.size() == 1) arg = expr(*args.at(0), inTypes.at(0)); else { auto inputSort = dynamic_cast(*symbFunction.sort).domain; arg = smtutil::Expression::tuple_constructor( smtutil::Expression(make_shared(inputSort), ""), symbArgs ); } auto out = smtutil::Expression::select(symbFunction, *arg); if (outTypes.size() == 1) defineExpr(_funCall, out); else { auto symbTuple = dynamic_pointer_cast(m_context.expression(_funCall)); solAssert(symbTuple, ""); solAssert(symbTuple->components().size() == outTypes.size(), ""); solAssert(out.sort->kind == smtutil::Kind::Tuple, ""); symbTuple->increaseIndex(); for (unsigned i = 0; i < symbTuple->components().size(); ++i) m_context.addAssertion(symbTuple->component(i) == smtutil::Expression::tuple_get(out, i)); } } void SMTEncoder::visitCryptoFunction(FunctionCall const& _funCall) { auto const& funType = dynamic_cast(*_funCall.expression().annotation().type); auto kind = funType.kind(); auto arg0 = expr(*_funCall.arguments().at(0)); optional result; if (kind == FunctionType::Kind::KECCAK256) result = smtutil::Expression::select(state().cryptoFunction("keccak256"), arg0); else if (kind == FunctionType::Kind::SHA256) result = smtutil::Expression::select(state().cryptoFunction("sha256"), arg0); else if (kind == FunctionType::Kind::RIPEMD160) result = smtutil::Expression::select(state().cryptoFunction("ripemd160"), arg0); else if (kind == FunctionType::Kind::ECRecover) { auto e = state().cryptoFunction("ecrecover"); auto arg0 = expr(*_funCall.arguments().at(0)); auto arg1 = expr(*_funCall.arguments().at(1)); auto arg2 = expr(*_funCall.arguments().at(2)); auto arg3 = expr(*_funCall.arguments().at(3)); auto inputSort = dynamic_cast(*e.sort).domain; auto ecrecoverInput = smtutil::Expression::tuple_constructor( smtutil::Expression(make_shared(inputSort), ""), {arg0, arg1, arg2, arg3} ); result = smtutil::Expression::select(e, ecrecoverInput); } else solAssert(false, ""); defineExpr(_funCall, *result); } void SMTEncoder::visitGasLeft(FunctionCall const& _funCall) { string gasLeft = "gasleft"; // We increase the variable index since gasleft changes // inside a tx. defineGlobalVariable(gasLeft, _funCall, true); auto const& symbolicVar = m_context.globalSymbol(gasLeft); unsigned index = symbolicVar->index(); // We set the current value to unknown anyway to add type constraints. m_context.setUnknownValue(*symbolicVar); if (index > 0) m_context.addAssertion(symbolicVar->currentValue() <= symbolicVar->valueAtIndex(index - 1)); } void SMTEncoder::visitAddMulMod(FunctionCall const& _funCall) { auto const& funType = dynamic_cast(*_funCall.expression().annotation().type); auto kind = funType.kind(); solAssert(kind == FunctionType::Kind::AddMod || kind == FunctionType::Kind::MulMod, ""); auto const& args = _funCall.arguments(); solAssert(args.at(0) && args.at(1) && args.at(2), ""); auto x = expr(*args.at(0)); auto y = expr(*args.at(1)); auto k = expr(*args.at(2)); auto const& intType = dynamic_cast(*_funCall.annotation().type); if (kind == FunctionType::Kind::AddMod) defineExpr(_funCall, divModWithSlacks(x + y, k, intType).second); else defineExpr(_funCall, divModWithSlacks(x * y, k, intType).second); } void SMTEncoder::visitWrapUnwrap(FunctionCall const& _funCall) { auto const& args = _funCall.arguments(); solAssert(args.size() == 1, ""); defineExpr(_funCall, expr(*args.front())); } void SMTEncoder::visitObjectCreation(FunctionCall const& _funCall) { auto const& args = _funCall.arguments(); solAssert(args.size() >= 1, ""); auto argType = args.front()->annotation().type->category(); solAssert(argType == Type::Category::Integer || argType == Type::Category::RationalNumber, ""); smtutil::Expression arraySize = expr(*args.front()); setSymbolicUnknownValue(arraySize, TypeProvider::uint256(), m_context); auto symbArray = dynamic_pointer_cast(m_context.expression(_funCall)); solAssert(symbArray, ""); smt::setSymbolicZeroValue(*symbArray, m_context); auto zeroElements = symbArray->elements(); symbArray->increaseIndex(); m_context.addAssertion(symbArray->length() == arraySize); m_context.addAssertion(symbArray->elements() == zeroElements); } void SMTEncoder::endVisit(Identifier const& _identifier) { if (auto decl = identifierToVariable(_identifier)) { if (decl->isConstant()) defineExpr(_identifier, constantExpr(_identifier, *decl)); else defineExpr(_identifier, currentValue(*decl)); } else if (_identifier.annotation().type->category() == Type::Category::Function) visitFunctionIdentifier(_identifier); else if (_identifier.name() == "now") defineGlobalVariable(_identifier.name(), _identifier); else if (_identifier.name() == "this") { defineExpr(_identifier, state().thisAddress()); m_uninterpretedTerms.insert(&_identifier); } // Ignore type identifiers else if (dynamic_cast(_identifier.annotation().type)) return; // Ignore module identifiers else if (dynamic_cast(_identifier.annotation().type)) return; // Ignore user defined value type identifiers else if (dynamic_cast(_identifier.annotation().type)) return; // Ignore the builtin abi, it is handled in FunctionCall. // TODO: ignore MagicType in general (abi, block, msg, tx, type) else if (auto magicType = dynamic_cast(_identifier.annotation().type); magicType && magicType->kind() == MagicType::Kind::ABI) { solAssert(_identifier.name() == "abi", ""); return; } else createExpr(_identifier); } void SMTEncoder::endVisit(ElementaryTypeNameExpression const& _typeName) { auto const& typeType = dynamic_cast(*_typeName.annotation().type); auto result = smt::newSymbolicVariable( *TypeProvider::uint256(), typeType.actualType()->toString(false), m_context ); solAssert(!result.first && result.second, ""); m_context.createExpression(_typeName, result.second); } namespace // helpers for SMTEncoder::visitPublicGetter { bool isReturnedFromStructGetter(Type const* _type) { // So far it seems that only Mappings and ordinary Arrays are not returned. auto category = _type->category(); if (category == Type::Category::Mapping) return false; if (category == Type::Category::Array) return dynamic_cast(*_type).isByteArrayOrString(); // default return true; } vector structGetterReturnedMembers(StructType const& _structType) { vector returnedMembers; for (auto const& member: _structType.nativeMembers(nullptr)) if (isReturnedFromStructGetter(member.type)) returnedMembers.push_back(member.name); return returnedMembers; } } void SMTEncoder::visitPublicGetter(FunctionCall const& _funCall) { auto var = publicGetter(_funCall.expression()); solAssert(var && var->isStateVariable(), ""); solAssert(m_context.knownExpression(_funCall), ""); auto paramExpectedTypes = replaceUserTypes(FunctionType(*var).parameterTypes()); auto actualArguments = _funCall.arguments(); solAssert(actualArguments.size() == paramExpectedTypes.size(), ""); deque symbArguments; for (unsigned i = 0; i < paramExpectedTypes.size(); ++i) symbArguments.push_back(expr(*actualArguments[i], paramExpectedTypes[i])); // See FunctionType::FunctionType(VariableDeclaration const& _varDecl) // to understand the return types of public getters. Type const* type = var->type(); smtutil::Expression currentExpr = currentValue(*var); while (true) { if ( type->isValueType() || (type->category() == Type::Category::Array && dynamic_cast(*type).isByteArrayOrString()) ) { solAssert(symbArguments.empty(), ""); defineExpr(_funCall, currentExpr); return; } switch (type->category()) { case Type::Category::Array: case Type::Category::Mapping: { solAssert(!symbArguments.empty(), ""); // For nested arrays/mappings, each argument in the call is an index to the next layer. // We mirror this with `select` after unpacking the SMT-LIB array expression. currentExpr = smtutil::Expression::select(smtutil::Expression::tuple_get(currentExpr, 0), symbArguments.front()); symbArguments.pop_front(); if (auto arrayType = dynamic_cast(type)) type = arrayType->baseType(); else if (auto mappingType = dynamic_cast(type)) type = mappingType->valueType(); else solAssert(false, ""); break; } case Type::Category::Struct: { solAssert(symbArguments.empty(), ""); smt::SymbolicStructVariable structVar(dynamic_cast(type), "struct_temp_" + to_string(_funCall.id()), m_context); m_context.addAssertion(structVar.currentValue() == currentExpr); auto returnedMembers = structGetterReturnedMembers(dynamic_cast(*structVar.type())); solAssert(!returnedMembers.empty(), ""); auto returnedValues = applyMap(returnedMembers, [&](string const& memberName) -> optional { return structVar.member(memberName); }); defineExpr(_funCall, returnedValues); return; } default: { // Unsupported cases, do nothing and the getter will be abstracted. return; } } } } bool SMTEncoder::shouldAnalyze(SourceUnit const& _source) const { return m_settings.contracts.isDefault() || m_settings.contracts.has(*_source.annotation().path); } bool SMTEncoder::shouldAnalyze(ContractDefinition const& _contract) const { if (!_contract.canBeDeployed()) return false; return m_settings.contracts.isDefault() || m_settings.contracts.has(_contract.sourceUnitName()); } void SMTEncoder::visitTypeConversion(FunctionCall const& _funCall) { solAssert(*_funCall.annotation().kind == FunctionCallKind::TypeConversion, ""); solAssert(_funCall.arguments().size() == 1, ""); auto argument = _funCall.arguments().front(); auto const argType = argument->annotation().type; auto const funCallType = _funCall.annotation().type; auto symbArg = expr(*argument, funCallType); if (smt::isStringLiteral(*argType) && smt::isFixedBytes(*funCallType)) { defineExpr(_funCall, symbArg); return; } ArrayType const* arrayType = dynamic_cast(argType); if (auto sliceType = dynamic_cast(argType)) arrayType = &sliceType->arrayType(); if (arrayType && arrayType->isByteArrayOrString() && smt::isFixedBytes(*funCallType)) { auto array = dynamic_pointer_cast(m_context.expression(*argument)); bytesToFixedBytesAssertions(*array, _funCall); return; } // TODO Simplify this whole thing for 0.8.0 where weird casts are disallowed. unsigned argSize = argType->storageBytes(); unsigned castSize = funCallType->storageBytes(); bool castIsSigned = smt::isNumber(*funCallType) && smt::isSigned(funCallType); bool argIsSigned = smt::isNumber(*argType) && smt::isSigned(argType); optional symbMin; optional symbMax; if (smt::isNumber(*funCallType)) { symbMin = smt::minValue(funCallType); symbMax = smt::maxValue(funCallType); } if (argSize == castSize) { // If sizes are the same, it's possible that the signs are different. if (smt::isNumber(*funCallType) && smt::isNumber(*argType)) { // castIsSigned && !argIsSigned => might overflow if arg > castType.max // !castIsSigned && argIsSigned => might underflow if arg < castType.min // !castIsSigned && !argIsSigned => ok // castIsSigned && argIsSigned => ok if (castIsSigned && !argIsSigned) { auto wrap = smtutil::Expression::ite( symbArg > *symbMax, symbArg - (*symbMax - *symbMin + 1), symbArg ); defineExpr(_funCall, wrap); } else if (!castIsSigned && argIsSigned) { auto wrap = smtutil::Expression::ite( symbArg < *symbMin, symbArg + (*symbMax + 1), symbArg ); defineExpr(_funCall, wrap); } else defineExpr(_funCall, symbArg); } else defineExpr(_funCall, symbArg); } else if (castSize > argSize) { solAssert(smt::isNumber(*funCallType), ""); // RationalNumbers have size 32. solAssert(argType->category() != Type::Category::RationalNumber, ""); // castIsSigned && !argIsSigned => ok // castIsSigned && argIsSigned => ok // !castIsSigned && !argIsSigned => ok except for FixedBytesType, need to adjust padding // !castIsSigned && argIsSigned => might underflow if arg < castType.min if (!castIsSigned && argIsSigned) { auto wrap = smtutil::Expression::ite( symbArg < *symbMin, symbArg + (*symbMax + 1), symbArg ); defineExpr(_funCall, wrap); } else if (!castIsSigned && !argIsSigned) { if (auto const* fixedCast = dynamic_cast(funCallType)) { auto const* fixedArg = dynamic_cast(argType); solAssert(fixedArg, ""); auto diff = fixedCast->numBytes() - fixedArg->numBytes(); solAssert(diff > 0, ""); auto bvSize = fixedCast->numBytes() * 8; defineExpr( _funCall, smtutil::Expression::bv2int(smtutil::Expression::int2bv(symbArg, bvSize) << smtutil::Expression::int2bv(diff * 8, bvSize)) ); } else defineExpr(_funCall, symbArg); } else defineExpr(_funCall, symbArg); } else // castSize < argSize { solAssert(smt::isNumber(*funCallType), ""); RationalNumberType const* rationalType = isConstant(*argument); if (rationalType) { // The TypeChecker guarantees that a constant fits in the cast size. defineExpr(_funCall, symbArg); return; } auto const* fixedCast = dynamic_cast(funCallType); auto const* fixedArg = dynamic_cast(argType); if (fixedCast && fixedArg) { createExpr(_funCall); auto diff = argSize - castSize; solAssert(fixedArg->numBytes() - fixedCast->numBytes() == diff, ""); auto argValueBV = smtutil::Expression::int2bv(symbArg, argSize * 8); auto shr = smtutil::Expression::int2bv(diff * 8, argSize * 8); solAssert(!castIsSigned, ""); defineExpr(_funCall, smtutil::Expression::bv2int(argValueBV >> shr)); } else { auto argValueBV = smtutil::Expression::int2bv(symbArg, castSize * 8); defineExpr(_funCall, smtutil::Expression::bv2int(argValueBV, castIsSigned)); } } } void SMTEncoder::visitFunctionIdentifier(Identifier const& _identifier) { auto const& fType = dynamic_cast(*_identifier.annotation().type); if (replaceUserTypes(fType.returnParameterTypes()).size() == 1) { defineGlobalVariable(fType.identifier(), _identifier); m_context.createExpression(_identifier, m_context.globalSymbol(fType.identifier())); } } void SMTEncoder::visitStructConstructorCall(FunctionCall const& _funCall) { solAssert(*_funCall.annotation().kind == FunctionCallKind::StructConstructorCall, ""); if (smt::isNonRecursiveStruct(*_funCall.annotation().type)) { auto& structSymbolicVar = dynamic_cast(*m_context.expression(_funCall)); auto structType = dynamic_cast(structSymbolicVar.type()); solAssert(structType, ""); auto const& structMembers = structType->structDefinition().members(); solAssert(structMembers.size() == _funCall.sortedArguments().size(), ""); auto args = _funCall.sortedArguments(); structSymbolicVar.assignAllMembers(applyMap( ranges::views::zip(args, structMembers), [this] (auto const& argMemberPair) { return expr(*argMemberPair.first, argMemberPair.second->type()); } )); } } void SMTEncoder::endVisit(Literal const& _literal) { solAssert(_literal.annotation().type, "Expected type for AST node"); Type const& type = *_literal.annotation().type; if (smt::isNumber(type)) defineExpr(_literal, smtutil::Expression(type.literalValue(&_literal))); else if (smt::isBool(type)) defineExpr(_literal, smtutil::Expression(_literal.token() == Token::TrueLiteral ? true : false)); else if (smt::isStringLiteral(type)) { createExpr(_literal); // Add constraints for the length and values as it is known. auto symbArray = dynamic_pointer_cast(m_context.expression(_literal)); solAssert(symbArray, ""); addArrayLiteralAssertions( *symbArray, applyMap(_literal.value(), [](unsigned char c) { return smtutil::Expression{size_t(c)}; }) ); } else solAssert(false, ""); } void SMTEncoder::addArrayLiteralAssertions( smt::SymbolicArrayVariable& _symArray, vector const& _elementValues ) { m_context.addAssertion(_symArray.length() == _elementValues.size()); for (size_t i = 0; i < _elementValues.size(); i++) m_context.addAssertion(smtutil::Expression::select(_symArray.elements(), i) == _elementValues[i]); } void SMTEncoder::bytesToFixedBytesAssertions( smt::SymbolicArrayVariable& _symArray, Expression const& _fixedBytes ) { auto const& fixed = dynamic_cast(*_fixedBytes.annotation().type); auto intType = TypeProvider::uint256(); string suffix = to_string(_fixedBytes.id()) + "_" + to_string(m_context.newUniqueId()); smt::SymbolicIntVariable k(intType, intType, "k_" + suffix, m_context); m_context.addAssertion(k.currentValue() == 0); size_t n = fixed.numBytes(); for (size_t i = 0; i < n; i++) { auto kPrev = k.currentValue(); m_context.addAssertion((smtutil::Expression::select(_symArray.elements(), i) * (u256(1) << ((n - i - 1) * 8))) + kPrev == k.increaseIndex()); } m_context.addAssertion(expr(_fixedBytes) == k.currentValue()); } void SMTEncoder::endVisit(Return const& _return) { if (_return.expression() && m_context.knownExpression(*_return.expression())) { auto returnParams = m_callStack.back().first->returnParameters(); if (returnParams.size() > 1) { auto const& symbTuple = dynamic_pointer_cast(m_context.expression(*_return.expression())); solAssert(symbTuple, ""); solAssert(symbTuple->components().size() == returnParams.size(), ""); auto const* tupleType = dynamic_cast(_return.expression()->annotation().type); solAssert(tupleType, ""); auto const& types = tupleType->components(); solAssert(types.size() == returnParams.size(), ""); for (unsigned i = 0; i < returnParams.size(); ++i) assignment(*returnParams.at(i), symbTuple->component(i, types.at(i), returnParams.at(i)->type())); } else if (returnParams.size() == 1) assignment(*returnParams.front(), expr(*_return.expression(), returnParams.front()->type())); } } bool SMTEncoder::visit(MemberAccess const& _memberAccess) { createExpr(_memberAccess); auto const& accessType = _memberAccess.annotation().type; if (accessType->category() == Type::Category::Function) { auto const* functionType = dynamic_cast(_memberAccess.annotation().type); if (functionType && functionType->hasDeclaration()) defineExpr(_memberAccess, functionType->externalIdentifier()); return true; } Expression const* memberExpr = innermostTuple(_memberAccess.expression()); auto const& exprType = memberExpr->annotation().type; solAssert(exprType, ""); if (exprType->category() == Type::Category::Magic) { if (auto const* identifier = dynamic_cast(memberExpr)) { auto const& name = identifier->name(); solAssert(name == "block" || name == "msg" || name == "tx", ""); auto memberName = _memberAccess.memberName(); // TODO remove this for 0.9.0 if (name == "block" && memberName == "difficulty") memberName = "prevrandao"; defineExpr(_memberAccess, state().txMember(name + "." + memberName)); } else if (auto magicType = dynamic_cast(exprType)) { if (magicType->kind() == MagicType::Kind::Block) defineExpr(_memberAccess, state().txMember("block." + _memberAccess.memberName())); else if (magicType->kind() == MagicType::Kind::Message) defineExpr(_memberAccess, state().txMember("msg." + _memberAccess.memberName())); else if (magicType->kind() == MagicType::Kind::Transaction) defineExpr(_memberAccess, state().txMember("tx." + _memberAccess.memberName())); else if (magicType->kind() == MagicType::Kind::MetaType) { auto const& memberName = _memberAccess.memberName(); if (memberName == "min" || memberName == "max") { if (IntegerType const* integerType = dynamic_cast(magicType->typeArgument())) defineExpr(_memberAccess, memberName == "min" ? integerType->minValue() : integerType->maxValue()); else if (EnumType const* enumType = dynamic_cast(magicType->typeArgument())) defineExpr(_memberAccess, memberName == "min" ? enumType->minValue() : enumType->maxValue()); } else if (memberName == "interfaceId") { ContractDefinition const& contract = dynamic_cast(*magicType->typeArgument()).contractDefinition(); defineExpr(_memberAccess, contract.interfaceId()); } else // NOTE: supporting name, creationCode, runtimeCode would be easy enough, but the bytes/string they return are not // at all usable in the SMT checker currently m_unsupportedErrors.warning( 7507_error, _memberAccess.location(), "Assertion checker does not yet support this expression." ); } } else solAssert(false, ""); return false; } else if (smt::isNonRecursiveStruct(*exprType)) { memberExpr->accept(*this); auto const& symbStruct = dynamic_pointer_cast(m_context.expression(*memberExpr)); defineExpr(_memberAccess, symbStruct->member(_memberAccess.memberName())); return false; } else if (exprType->category() == Type::Category::TypeType) { auto const* decl = expressionToDeclaration(*memberExpr); if (dynamic_cast(decl)) { auto enumType = dynamic_cast(accessType); solAssert(enumType, ""); defineExpr(_memberAccess, enumType->memberValue(_memberAccess.memberName())); return false; } else if (dynamic_cast(decl)) { if (auto const* var = dynamic_cast(_memberAccess.annotation().referencedDeclaration)) { if (var->isConstant()) defineExpr(_memberAccess, constantExpr(_memberAccess, *var)); else defineExpr(_memberAccess, currentValue(*var)); return false; } } } else if (exprType->category() == Type::Category::Address) { memberExpr->accept(*this); if (_memberAccess.memberName() == "balance") { defineExpr(_memberAccess, state().balance(expr(*memberExpr))); setSymbolicUnknownValue(*m_context.expression(_memberAccess), m_context); m_uninterpretedTerms.insert(&_memberAccess); return false; } } else if (exprType->category() == Type::Category::Array) { memberExpr->accept(*this); if (_memberAccess.memberName() == "length") { auto symbArray = dynamic_pointer_cast(m_context.expression(*memberExpr)); solAssert(symbArray, ""); defineExpr(_memberAccess, symbArray->length()); m_uninterpretedTerms.insert(&_memberAccess); setSymbolicUnknownValue( expr(_memberAccess), _memberAccess.annotation().type, m_context ); } return false; } else if ( auto const* functionType = dynamic_cast(exprType); functionType && _memberAccess.memberName() == "selector" && functionType->hasDeclaration() ) { defineExpr(_memberAccess, functionType->externalIdentifier()); return false; } else if (exprType->category() == Type::Category::Module) { if (auto const* var = dynamic_cast(_memberAccess.annotation().referencedDeclaration)) { solAssert(var->isConstant(), ""); defineExpr(_memberAccess, constantExpr(_memberAccess, *var)); return false; } } m_unsupportedErrors.warning( 7650_error, _memberAccess.location(), "Assertion checker does not yet support this expression." ); return true; } void SMTEncoder::endVisit(IndexAccess const& _indexAccess) { createExpr(_indexAccess); if (_indexAccess.annotation().type->category() == Type::Category::TypeType) return; makeOutOfBoundsVerificationTarget(_indexAccess); if (auto const* type = dynamic_cast(_indexAccess.baseExpression().annotation().type)) { smtutil::Expression base = expr(_indexAccess.baseExpression()); if (type->numBytes() == 1) defineExpr(_indexAccess, base); else { auto [bvSize, isSigned] = smt::typeBvSizeAndSignedness(_indexAccess.baseExpression().annotation().type); solAssert(!isSigned, ""); solAssert(bvSize >= 16, ""); solAssert(bvSize % 8 == 0, ""); smtutil::Expression idx = expr(*_indexAccess.indexExpression()); auto bvBase = smtutil::Expression::int2bv(base, bvSize); auto bvShl = smtutil::Expression::int2bv(idx * 8, bvSize); auto bvShr = smtutil::Expression::int2bv(bvSize - 8, bvSize); auto result = (bvBase << bvShl) >> bvShr; auto anyValue = expr(_indexAccess); m_context.expression(_indexAccess)->increaseIndex(); unsigned numBytes = bvSize / 8; auto withBound = smtutil::Expression::ite( idx < numBytes, smtutil::Expression::bv2int(result, false), anyValue ); defineExpr(_indexAccess, withBound); } return; } shared_ptr array; if (auto const* id = dynamic_cast(&_indexAccess.baseExpression())) { auto varDecl = identifierToVariable(*id); solAssert(varDecl, ""); array = m_context.variable(*varDecl); if (varDecl && varDecl->isConstant()) m_context.addAssertion(currentValue(*varDecl) == expr(*id)); } else { solAssert(m_context.knownExpression(_indexAccess.baseExpression()), ""); array = m_context.expression(_indexAccess.baseExpression()); } auto arrayVar = dynamic_pointer_cast(array); solAssert(arrayVar, ""); Type const* baseType = _indexAccess.baseExpression().annotation().type; defineExpr(_indexAccess, smtutil::Expression::select( arrayVar->elements(), expr(*_indexAccess.indexExpression(), keyType(baseType)) )); setSymbolicUnknownValue( expr(_indexAccess), _indexAccess.annotation().type, m_context ); m_uninterpretedTerms.insert(&_indexAccess); } void SMTEncoder::endVisit(IndexRangeAccess const& _indexRangeAccess) { createExpr(_indexRangeAccess); /// The actual slice is created by CHC which also assigns the length. } void SMTEncoder::arrayAssignment() { m_arrayAssignmentHappened = true; } void SMTEncoder::indexOrMemberAssignment(Expression const& _expr, smtutil::Expression const& _rightHandSide) { auto toStore = _rightHandSide; auto const* lastExpr = &_expr; while (true) { if (auto const* indexAccess = dynamic_cast(lastExpr)) { auto const& base = indexAccess->baseExpression(); if (dynamic_cast(&base)) base.accept(*this); Type const* baseType = base.annotation().type; auto indexExpr = expr(*indexAccess->indexExpression(), keyType(baseType)); auto symbArray = dynamic_pointer_cast(m_context.expression(base)); solAssert(symbArray, ""); toStore = smtutil::Expression::tuple_constructor( smtutil::Expression(make_shared(smt::smtSort(*baseType)), baseType->toString(true)), {smtutil::Expression::store(symbArray->elements(), indexExpr, toStore), symbArray->length()} ); defineExpr(*indexAccess, smtutil::Expression::select( symbArray->elements(), indexExpr )); lastExpr = &indexAccess->baseExpression(); } else if (auto const* memberAccess = dynamic_cast(lastExpr)) { auto const& base = memberAccess->expression(); if (dynamic_cast(&base)) base.accept(*this); if ( auto const* structType = dynamic_cast(base.annotation().type); structType && structType->recursive() ) { m_unsupportedErrors.warning( 4375_error, memberAccess->location(), "Assertion checker does not support recursive structs." ); return; } if (auto varDecl = identifierToVariable(*memberAccess)) { if (varDecl->hasReferenceOrMappingType()) resetReferences(*varDecl); assignment(*varDecl, toStore); break; } auto symbStruct = dynamic_pointer_cast(m_context.expression(base)); solAssert(symbStruct, ""); symbStruct->assignMember(memberAccess->memberName(), toStore); toStore = symbStruct->currentValue(); defineExpr(*memberAccess, symbStruct->member(memberAccess->memberName())); lastExpr = &memberAccess->expression(); } else if (auto const& id = dynamic_cast(lastExpr)) { auto varDecl = identifierToVariable(*id); solAssert(varDecl, ""); if (varDecl->hasReferenceOrMappingType()) resetReferences(*varDecl); assignment(*varDecl, toStore); defineExpr(*id, currentValue(*varDecl)); break; } else { auto type = lastExpr->annotation().type; if ( dynamic_cast(type) || dynamic_cast(type) ) resetReferences(type); assignment(*m_context.expression(*lastExpr), toStore); break; } } } void SMTEncoder::arrayPush(FunctionCall const& _funCall) { auto memberAccess = dynamic_cast(&_funCall.expression()); solAssert(memberAccess, ""); auto symbArray = dynamic_pointer_cast(m_context.expression(memberAccess->expression())); solAssert(symbArray, ""); auto oldLength = symbArray->length(); m_context.addAssertion(oldLength >= 0); // Real world assumption: the array length is assumed to not overflow. // This assertion guarantees that both the current and updated lengths have the above property. m_context.addAssertion(oldLength + 1 < (smt::maxValue(*TypeProvider::uint256()) - 1)); auto const& arguments = _funCall.arguments(); auto arrayType = dynamic_cast(symbArray->type()); solAssert(arrayType, ""); auto elementType = arrayType->baseType(); smtutil::Expression element = arguments.empty() ? smt::zeroValue(elementType) : expr(*arguments.front(), elementType); smtutil::Expression store = smtutil::Expression::store( symbArray->elements(), oldLength, element ); symbArray->increaseIndex(); m_context.addAssertion(symbArray->elements() == store); m_context.addAssertion(symbArray->length() == oldLength + 1); if (arguments.empty()) defineExpr(_funCall, element); assignment(memberAccess->expression(), symbArray->currentValue()); } void SMTEncoder::arrayPop(FunctionCall const& _funCall) { auto memberAccess = dynamic_cast(cleanExpression(_funCall.expression())); solAssert(memberAccess, ""); auto symbArray = dynamic_pointer_cast(m_context.expression(memberAccess->expression())); solAssert(symbArray, ""); makeArrayPopVerificationTarget(_funCall); auto oldElements = symbArray->elements(); auto oldLength = symbArray->length(); symbArray->increaseIndex(); m_context.addAssertion(symbArray->elements() == oldElements); auto newLength = smtutil::Expression::ite( oldLength > 0, oldLength - 1, 0 ); m_context.addAssertion(symbArray->length() == newLength); assignment(memberAccess->expression(), symbArray->currentValue()); } void SMTEncoder::defineGlobalVariable(string const& _name, Expression const& _expr, bool _increaseIndex) { if (!m_context.knownGlobalSymbol(_name)) { bool abstract = m_context.createGlobalSymbol(_name, _expr); if (abstract) m_unsupportedErrors.warning( 1695_error, _expr.location(), "Assertion checker does not yet support this global variable." ); } else if (_increaseIndex) m_context.globalSymbol(_name)->increaseIndex(); // The default behavior is not to increase the index since // most of the global values stay the same throughout a tx. if (isSupportedType(*_expr.annotation().type)) defineExpr(_expr, m_context.globalSymbol(_name)->currentValue()); } bool SMTEncoder::shortcutRationalNumber(Expression const& _expr) { RationalNumberType const* rationalType = isConstant(_expr); if (!rationalType) return false; if (rationalType->isNegative()) defineExpr(_expr, smtutil::Expression(u2s(rationalType->literalValue(nullptr)))); else defineExpr(_expr, smtutil::Expression(rationalType->literalValue(nullptr))); return true; } void SMTEncoder::arithmeticOperation(BinaryOperation const& _op) { auto type = _op.annotation().commonType; solAssert(type, ""); solAssert(type->category() == Type::Category::Integer || type->category() == Type::Category::FixedPoint, ""); switch (_op.getOperator()) { case Token::Add: case Token::Sub: case Token::Mul: case Token::Div: case Token::Mod: { auto values = arithmeticOperation( _op.getOperator(), expr(_op.leftExpression()), expr(_op.rightExpression()), _op.annotation().commonType, _op ); defineExpr(_op, values.first); break; } default: m_unsupportedErrors.warning( 5188_error, _op.location(), "Assertion checker does not yet implement this operator." ); } } pair SMTEncoder::arithmeticOperation( Token _op, smtutil::Expression const& _left, smtutil::Expression const& _right, Type const* _commonType, Expression const& _operation ) { static set validOperators{ Token::Add, Token::Sub, Token::Mul, Token::Div, Token::Mod }; solAssert(validOperators.count(_op), ""); solAssert(_commonType, ""); solAssert( _commonType->category() == Type::Category::Integer || _commonType->category() == Type::Category::FixedPoint, "" ); IntegerType const* intType = nullptr; if (auto type = dynamic_cast(_commonType)) intType = type; else intType = TypeProvider::uint256(); auto valueUnbounded = [&]() -> smtutil::Expression { switch (_op) { case Token::Add: return _left + _right; case Token::Sub: return _left - _right; case Token::Mul: return _left * _right; case Token::Div: return divModWithSlacks(_left, _right, *intType).first; case Token::Mod: return divModWithSlacks(_left, _right, *intType).second; default: solAssert(false, ""); } }(); if (m_checked) return {valueUnbounded, valueUnbounded}; if (_op == Token::Div || _op == Token::Mod) { // mod and unsigned division never underflow/overflow if (_op == Token::Mod || !intType->isSigned()) return {valueUnbounded, valueUnbounded}; // The only case where division overflows is // - type is signed // - LHS is type.min // - RHS is -1 // the result is then -(type.min), which wraps back to type.min smtutil::Expression maxLeft = _left == smt::minValue(*intType); smtutil::Expression minusOneRight = _right == numeric_limits::max(); smtutil::Expression wrap = smtutil::Expression::ite(maxLeft && minusOneRight, smt::minValue(*intType), valueUnbounded); return {wrap, valueUnbounded}; } auto symbMin = smt::minValue(*intType); auto symbMax = smt::maxValue(*intType); smtutil::Expression intValueRange = (0 - symbMin) + symbMax + 1; string suffix = to_string(_operation.id()) + "_" + to_string(m_context.newUniqueId()); smt::SymbolicIntVariable k(intType, intType, "k_" + suffix, m_context); smt::SymbolicIntVariable m(intType, intType, "m_" + suffix, m_context); // To wrap around valueUnbounded in case of overflow or underflow, we replace it with a k, given: // 1. k + m * intValueRange = valueUnbounded // 2. k is in range of the desired integer type auto wrap = k.currentValue(); m_context.addAssertion(valueUnbounded == (k.currentValue() + intValueRange * m.currentValue())); m_context.addAssertion(k.currentValue() >= symbMin); m_context.addAssertion(k.currentValue() <= symbMax); // TODO this could be refined: // for unsigned types it's enough to check only the upper bound. auto value = smtutil::Expression::ite( valueUnbounded > symbMax, wrap, smtutil::Expression::ite( valueUnbounded < symbMin, wrap, valueUnbounded ) ); return {value, valueUnbounded}; } smtutil::Expression SMTEncoder::bitwiseOperation( Token _op, smtutil::Expression const& _left, smtutil::Expression const& _right, Type const* _commonType ) { static set validOperators{ Token::BitAnd, Token::BitOr, Token::BitXor, Token::SHL, Token::SHR, Token::SAR }; solAssert(validOperators.count(_op), ""); solAssert(_commonType, ""); auto [bvSize, isSigned] = smt::typeBvSizeAndSignedness(_commonType); auto bvLeft = smtutil::Expression::int2bv(_left, bvSize); auto bvRight = smtutil::Expression::int2bv(_right, bvSize); optional result; switch (_op) { case Token::BitAnd: result = bvLeft & bvRight; break; case Token::BitOr: result = bvLeft | bvRight; break; case Token::BitXor: result = bvLeft ^ bvRight; break; case Token::SHL: result = bvLeft << bvRight; break; case Token::SHR: result = bvLeft >> bvRight; break; case Token::SAR: result = isSigned ? smtutil::Expression::ashr(bvLeft, bvRight) : bvLeft >> bvRight; break; default: solAssert(false, ""); } solAssert(result.has_value(), ""); return smtutil::Expression::bv2int(*result, isSigned); } void SMTEncoder::compareOperation(BinaryOperation const& _op) { auto commonType = _op.annotation().commonType; solAssert(commonType, ""); if (isSupportedType(*commonType)) { smtutil::Expression left(expr(_op.leftExpression(), commonType)); smtutil::Expression right(expr(_op.rightExpression(), commonType)); Token op = _op.getOperator(); shared_ptr value; if (smt::isNumber(*commonType)) { value = make_shared( op == Token::Equal ? (left == right) : op == Token::NotEqual ? (left != right) : op == Token::LessThan ? (left < right) : op == Token::LessThanOrEqual ? (left <= right) : op == Token::GreaterThan ? (left > right) : /*op == Token::GreaterThanOrEqual*/ (left >= right) ); } else // Bool { solUnimplementedAssert(smt::isBool(*commonType), "Operation not yet supported"); value = make_shared( op == Token::Equal ? (left == right) : /*op == Token::NotEqual*/ (left != right) ); } // TODO: check that other values for op are not possible. defineExpr(_op, *value); } else m_unsupportedErrors.warning( 7229_error, _op.location(), "Assertion checker does not yet implement the type " + _op.annotation().commonType->toString() + " for comparisons" ); } void SMTEncoder::booleanOperation(BinaryOperation const& _op) { solAssert(_op.getOperator() == Token::And || _op.getOperator() == Token::Or, ""); solAssert(_op.annotation().commonType, ""); solAssert(_op.annotation().commonType->category() == Type::Category::Bool, ""); // @TODO check that both of them are not constant _op.leftExpression().accept(*this); if (_op.getOperator() == Token::And) { auto indicesAfterSecond = visitBranch(&_op.rightExpression(), expr(_op.leftExpression())).first; mergeVariables(!expr(_op.leftExpression()), copyVariableIndices(), indicesAfterSecond); defineExpr(_op, expr(_op.leftExpression()) && expr(_op.rightExpression())); } else { auto indicesAfterSecond = visitBranch(&_op.rightExpression(), !expr(_op.leftExpression())).first; mergeVariables(expr(_op.leftExpression()), copyVariableIndices(), indicesAfterSecond); defineExpr(_op, expr(_op.leftExpression()) || expr(_op.rightExpression())); } } void SMTEncoder::bitwiseOperation(BinaryOperation const& _op) { auto op = _op.getOperator(); solAssert(TokenTraits::isBitOp(op) || TokenTraits::isShiftOp(op), ""); auto commonType = _op.annotation().commonType; solAssert(commonType, ""); defineExpr(_op, bitwiseOperation( _op.getOperator(), expr(_op.leftExpression(), commonType), expr(_op.rightExpression(), commonType), commonType )); } void SMTEncoder::bitwiseNotOperation(UnaryOperation const& _op) { solAssert(_op.getOperator() == Token::BitNot, ""); auto [bvSize, isSigned] = smt::typeBvSizeAndSignedness(_op.annotation().type); auto bvOperand = smtutil::Expression::int2bv(expr(_op.subExpression(), _op.annotation().type), bvSize); defineExpr(_op, smtutil::Expression::bv2int(~bvOperand, isSigned)); } pair SMTEncoder::divModWithSlacks( smtutil::Expression _left, smtutil::Expression _right, IntegerType const& _type ) { if (m_settings.divModNoSlacks) return {_left / _right, _left % _right}; IntegerType const* intType = &_type; string suffix = "div_mod_" + to_string(m_context.newUniqueId()); smt::SymbolicIntVariable dSymb(intType, intType, "d_" + suffix, m_context); smt::SymbolicIntVariable rSymb(intType, intType, "r_" + suffix, m_context); auto d = dSymb.currentValue(); auto r = rSymb.currentValue(); // x / y = d and x % y = r iff d * y + r = x and // either x >= 0 and 0 <= r < abs(y) (or just 0 <= r < y for unsigned) // or x < 0 and -abs(y) < r <= 0 m_context.addAssertion(((d * _right) + r) == _left); if (_type.isSigned()) m_context.addAssertion( (_left >= 0 && 0 <= r && (_right == 0 || r < smtutil::abs(_right))) || (_left < 0 && ((_right == 0 || 0 - smtutil::abs(_right) < r) && r <= 0)) ); else // unsigned version m_context.addAssertion(0 <= r && (_right == 0 || r < _right)); auto divResult = smtutil::Expression::ite(_right == 0, 0, d); auto modResult = smtutil::Expression::ite(_right == 0, 0, r); return {divResult, modResult}; } void SMTEncoder::assignment(Expression const& _left, smtutil::Expression const& _right) { assignment(_left, _right, _left.annotation().type); } void SMTEncoder::assignment( Expression const& _left, smtutil::Expression const& _right, Type const* _type ) { solAssert( _left.annotation().type->category() != Type::Category::Tuple, "Tuple assignments should be handled by tupleAssignment." ); Expression const* left = cleanExpression(_left); if (!isSupportedType(*_type)) { // Give it a new index anyway to keep the SSA scheme sound. if (auto varDecl = identifierToVariable(*left)) m_context.newValue(*varDecl); } else if (auto varDecl = identifierToVariable(*left)) { if (varDecl->hasReferenceOrMappingType()) resetReferences(*varDecl); assignment(*varDecl, _right); } else if ( dynamic_cast(left) || dynamic_cast(left) ) indexOrMemberAssignment(*left, _right); else if (auto const* funCall = dynamic_cast(left)) { if (auto funType = dynamic_cast(funCall->expression().annotation().type)) { if (funType->kind() == FunctionType::Kind::ArrayPush) { auto memberAccess = dynamic_cast(&funCall->expression()); solAssert(memberAccess, ""); auto symbArray = dynamic_pointer_cast(m_context.expression(memberAccess->expression())); solAssert(symbArray, ""); auto oldLength = symbArray->length(); auto store = smtutil::Expression::store( symbArray->elements(), symbArray->length() - 1, _right ); symbArray->increaseIndex(); m_context.addAssertion(symbArray->elements() == store); m_context.addAssertion(symbArray->length() == oldLength); assignment(memberAccess->expression(), symbArray->currentValue()); } else if (funType->kind() == FunctionType::Kind::Internal) { for (auto type: replaceUserTypes(funType->returnParameterTypes())) if (type->category() == Type::Category::Mapping || dynamic_cast(type)) resetReferences(type); } } } else solAssert(false, ""); } void SMTEncoder::tupleAssignment(Expression const& _left, Expression const& _right) { auto lTuple = dynamic_cast(innermostTuple(_left)); solAssert(lTuple, ""); Expression const* right = innermostTuple(_right); auto const& lComponents = lTuple->components(); // If both sides are tuple expressions, we individually and potentially // recursively assign each pair of components. // This is because of potential type conversion. if (auto rTuple = dynamic_cast(right)) { auto const& rComponents = rTuple->components(); solAssert(lComponents.size() == rComponents.size(), ""); for (unsigned i = 0; i < lComponents.size(); ++i) { if (!lComponents.at(i) || !rComponents.at(i)) continue; auto const& lExpr = *lComponents.at(i); auto const& rExpr = *rComponents.at(i); if (lExpr.annotation().type->category() == Type::Category::Tuple) tupleAssignment(lExpr, rExpr); else { auto type = lExpr.annotation().type; assignment(lExpr, expr(rExpr, type), type); } } } else { auto rType = dynamic_cast(right->annotation().type); solAssert(rType, ""); auto const& rComponents = rType->components(); solAssert(lComponents.size() == rComponents.size(), ""); auto symbRight = expr(*right); solAssert(symbRight.sort->kind == smtutil::Kind::Tuple, ""); for (unsigned i = 0; i < lComponents.size(); ++i) if (auto component = lComponents.at(i); component && rComponents.at(i)) assignment(*component, smtutil::Expression::tuple_get(symbRight, i), component->annotation().type); } } smtutil::Expression SMTEncoder::compoundAssignment(Assignment const& _assignment) { static map const compoundToArithmetic{ {Token::AssignAdd, Token::Add}, {Token::AssignSub, Token::Sub}, {Token::AssignMul, Token::Mul}, {Token::AssignDiv, Token::Div}, {Token::AssignMod, Token::Mod} }; static map const compoundToBitwise{ {Token::AssignBitAnd, Token::BitAnd}, {Token::AssignBitOr, Token::BitOr}, {Token::AssignBitXor, Token::BitXor}, {Token::AssignShl, Token::SHL}, {Token::AssignShr, Token::SHR}, {Token::AssignSar, Token::SAR} }; Token op = _assignment.assignmentOperator(); solAssert(compoundToArithmetic.count(op) || compoundToBitwise.count(op), ""); auto decl = identifierToVariable(_assignment.leftHandSide()); if (compoundToBitwise.count(op)) return bitwiseOperation( compoundToBitwise.at(op), decl ? currentValue(*decl) : expr(_assignment.leftHandSide(), _assignment.annotation().type), expr(_assignment.rightHandSide(), _assignment.annotation().type), _assignment.annotation().type ); auto values = arithmeticOperation( compoundToArithmetic.at(op), decl ? currentValue(*decl) : expr(_assignment.leftHandSide(), _assignment.annotation().type), expr(_assignment.rightHandSide(), _assignment.annotation().type), _assignment.annotation().type, _assignment ); return values.first; } void SMTEncoder::expressionToTupleAssignment(vector> const& _variables, Expression const& _rhs) { auto symbolicVar = m_context.expression(_rhs); if (_variables.size() > 1) { auto symbTuple = dynamic_pointer_cast(symbolicVar); solAssert(symbTuple, ""); auto const& symbComponents = symbTuple->components(); solAssert(symbComponents.size() == _variables.size(), ""); auto tupleType = dynamic_cast(_rhs.annotation().type); solAssert(tupleType, ""); auto const& typeComponents = tupleType->components(); solAssert(typeComponents.size() == symbComponents.size(), ""); for (unsigned i = 0; i < symbComponents.size(); ++i) { auto param = _variables.at(i); if (param) { solAssert(m_context.knownVariable(*param), ""); assignment(*param, symbTuple->component(i, typeComponents[i], param->type())); } } } else if (_variables.size() == 1) { auto const& var = *_variables.front(); solAssert(m_context.knownVariable(var), ""); assignment(var, _rhs); } } void SMTEncoder::assignment(VariableDeclaration const& _variable, Expression const& _value) { // 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. assignment(_variable, expr(_value, _variable.type())); } void SMTEncoder::assignment(VariableDeclaration const& _variable, smtutil::Expression const& _value) { Type const* type = _variable.type(); if (type->category() == Type::Category::Mapping) arrayAssignment(); assignment(*m_context.variable(_variable), _value); } void SMTEncoder::assignment(smt::SymbolicVariable& _symVar, smtutil::Expression const& _value) { m_context.addAssertion(_symVar.increaseIndex() == _value); } pair SMTEncoder::visitBranch( ASTNode const* _statement, smtutil::Expression _condition ) { return visitBranch(_statement, &_condition); } pair SMTEncoder::visitBranch( ASTNode const* _statement, smtutil::Expression const* _condition ) { auto indicesBeforeBranch = copyVariableIndices(); if (_condition) pushPathCondition(*_condition); _statement->accept(*this); auto pathConditionOnExit = currentPathConditions(); if (_condition) popPathCondition(); auto indicesAfterBranch = copyVariableIndices(); resetVariableIndices(indicesBeforeBranch); return {indicesAfterBranch, pathConditionOnExit}; } void SMTEncoder::initializeFunctionCallParameters(CallableDeclaration const& _function, vector const& _callArgs) { auto const& funParams = _function.parameters(); solAssert(funParams.size() == _callArgs.size(), ""); for (unsigned i = 0; i < funParams.size(); ++i) if (createVariable(*funParams[i])) { m_context.addAssertion(_callArgs[i] == m_context.newValue(*funParams[i])); if (funParams[i]->annotation().type->category() == Type::Category::Mapping) m_arrayAssignmentHappened = true; } vector localVars; if (auto const* fun = dynamic_cast(&_function)) localVars = localVariablesIncludingModifiers(*fun, m_currentContract); else localVars = _function.localVariables(); for (auto const& variable: localVars) if (createVariable(*variable)) { m_context.newValue(*variable); m_context.setZeroValue(*variable); } if (_function.returnParameterList()) for (auto const& retParam: _function.returnParameters()) if (createVariable(*retParam)) { m_context.newValue(*retParam); m_context.setZeroValue(*retParam); } } void SMTEncoder::createStateVariables(ContractDefinition const& _contract) { for (auto var: stateVariablesIncludingInheritedAndPrivate(_contract)) createVariable(*var); } void SMTEncoder::initializeStateVariables(ContractDefinition const& _contract) { for (auto var: _contract.stateVariables()) { solAssert(m_context.knownVariable(*var), ""); m_context.setZeroValue(*var); } for (auto var: _contract.stateVariables()) if (var->value()) { var->value()->accept(*this); assignment(*var, *var->value()); } } void SMTEncoder::createLocalVariables(FunctionDefinition const& _function) { for (auto const& variable: localVariablesIncludingModifiers(_function, m_currentContract)) createVariable(*variable); for (auto const& param: _function.parameters()) createVariable(*param); if (_function.returnParameterList()) for (auto const& retParam: _function.returnParameters()) createVariable(*retParam); } void SMTEncoder::initializeLocalVariables(FunctionDefinition const& _function) { for (auto const& variable: localVariablesIncludingModifiers(_function, m_currentContract)) { solAssert(m_context.knownVariable(*variable), ""); m_context.setZeroValue(*variable); } for (auto const& param: _function.parameters()) { solAssert(m_context.knownVariable(*param), ""); m_context.setUnknownValue(*param); } if (_function.returnParameterList()) for (auto const& retParam: _function.returnParameters()) { solAssert(m_context.knownVariable(*retParam), ""); m_context.setZeroValue(*retParam); } } void SMTEncoder::resetStateVariables() { m_context.resetVariables([&](VariableDeclaration const& _variable) { return _variable.isStateVariable(); }); } void SMTEncoder::resetMemoryVariables() { m_context.resetVariables([&](VariableDeclaration const& _variable) { return _variable.referenceLocation() == VariableDeclaration::Location::Memory; }); } void SMTEncoder::resetStorageVariables() { m_context.resetVariables([&](VariableDeclaration const& _variable) { return _variable.referenceLocation() == VariableDeclaration::Location::Storage || _variable.isStateVariable(); }); } void SMTEncoder::resetBalances() { state().newBalances(); } void SMTEncoder::resetReferences(VariableDeclaration const& _varDecl) { m_context.resetVariables([&](VariableDeclaration const& _var) { if (_var == _varDecl) return false; // If both are state variables no need to clear knowledge. if (_var.isStateVariable() && _varDecl.isStateVariable()) return false; return sameTypeOrSubtype(_var.type(), _varDecl.type()); }); } void SMTEncoder::resetReferences(Type const* _type) { m_context.resetVariables([&](VariableDeclaration const& _var) { return sameTypeOrSubtype(_var.type(), _type); }); } bool SMTEncoder::sameTypeOrSubtype(Type const* _a, Type const* _b) { bool foundSame = false; solidity::util::BreadthFirstSearch bfs{{_a}}; bfs.run([&](auto _type, auto&& _addChild) { if (*typeWithoutPointer(_b) == *typeWithoutPointer(_type)) { foundSame = true; bfs.abort(); } if (auto const* mapType = dynamic_cast(_type)) _addChild(mapType->valueType()); else if (auto const* arrayType = dynamic_cast(_type)) _addChild(arrayType->baseType()); else if (auto const* structType = dynamic_cast(_type)) for (auto const& member: structType->nativeMembers(nullptr)) _addChild(member.type); }); return foundSame; } bool SMTEncoder::isSupportedType(Type const& _type) const { return smt::isSupportedType(*underlyingType(&_type)); } Type const* SMTEncoder::typeWithoutPointer(Type const* _type) { if (auto refType = dynamic_cast(_type)) return TypeProvider::withLocationIfReference(refType->location(), _type); return _type; } void SMTEncoder::mergeVariables(smtutil::Expression const& _condition, VariableIndices const& _indicesEndTrue, VariableIndices const& _indicesEndFalse) { for (auto const& entry: _indicesEndTrue) { VariableDeclaration const* var = entry.first; auto trueIndex = entry.second; if (_indicesEndFalse.count(var) && _indicesEndFalse.at(var) != trueIndex) { m_context.addAssertion(m_context.newValue(*var) == smtutil::Expression::ite( _condition, valueAtIndex(*var, trueIndex), valueAtIndex(*var, _indicesEndFalse.at(var))) ); } } } smtutil::Expression SMTEncoder::currentValue(VariableDeclaration const& _decl) const { solAssert(m_context.knownVariable(_decl), ""); return m_context.variable(_decl)->currentValue(); } smtutil::Expression SMTEncoder::valueAtIndex(VariableDeclaration const& _decl, unsigned _index) const { solAssert(m_context.knownVariable(_decl), ""); return m_context.variable(_decl)->valueAtIndex(_index); } bool SMTEncoder::createVariable(VariableDeclaration const& _varDecl) { if (m_context.knownVariable(_varDecl)) return true; bool abstract = m_context.createVariable(_varDecl); if (abstract) { m_unsupportedErrors.warning( 8115_error, _varDecl.location(), "Assertion checker does not yet support the type of this variable." ); return false; } return true; } smtutil::Expression SMTEncoder::expr(Expression const& _e, Type const* _targetType) { if (!m_context.knownExpression(_e)) { m_unsupportedErrors.warning(6031_error, _e.location(), "Internal error: Expression undefined for SMT solver." ); createExpr(_e); } return m_context.expression(_e)->currentValue(underlyingType(_targetType)); } void SMTEncoder::createExpr(Expression const& _e) { bool abstract = m_context.createExpression(_e); if (abstract) m_unsupportedErrors.warning( 8364_error, _e.location(), "Assertion checker does not yet implement type " + _e.annotation().type->toString() ); } void SMTEncoder::defineExpr(Expression const& _e, smtutil::Expression _value) { auto type = _e.annotation().type; createExpr(_e); solAssert(_value.sort->kind != smtutil::Kind::Function, "Equality operator applied to type that is not fully supported"); if (!smt::isInaccessibleDynamic(*type)) m_context.addAssertion(expr(_e) == _value); if (m_checked && smt::isNumber(*type)) m_context.addAssertion(smtutil::Expression::implies( currentPathConditions(), smt::symbolicUnknownConstraints(expr(_e), type) )); } void SMTEncoder::defineExpr(Expression const& _e, vector> const& _values) { if (_values.size() == 1 && _values.front()) { defineExpr(_e, *_values.front()); return; } auto const& symbTuple = dynamic_pointer_cast(m_context.expression(_e)); solAssert(symbTuple, ""); symbTuple->increaseIndex(); auto const& symbComponents = symbTuple->components(); solAssert(symbComponents.size() == _values.size(), ""); auto tupleType = dynamic_cast(_e.annotation().type); solAssert(tupleType, ""); solAssert(tupleType->components().size() == symbComponents.size(), ""); for (unsigned i = 0; i < symbComponents.size(); ++i) if (_values[i] && !smt::isInaccessibleDynamic(*tupleType->components()[i])) m_context.addAssertion(symbTuple->component(i) == *_values[i]); } void SMTEncoder::popPathCondition() { solAssert(m_pathConditions.size() > 0, "Cannot pop path condition, empty."); m_pathConditions.pop_back(); } void SMTEncoder::pushPathCondition(smtutil::Expression const& _e) { m_pathConditions.push_back(currentPathConditions() && _e); } void SMTEncoder::setPathCondition(smtutil::Expression const& _e) { if (m_pathConditions.empty()) m_pathConditions.push_back(_e); else m_pathConditions.back() = _e; } smtutil::Expression SMTEncoder::currentPathConditions() { if (m_pathConditions.empty()) return smtutil::Expression(true); return m_pathConditions.back(); } SecondarySourceLocation SMTEncoder::callStackMessage(vector const& _callStack) { SecondarySourceLocation callStackLocation; solAssert(!_callStack.empty(), ""); callStackLocation.append("Callstack:", SourceLocation()); for (auto const& call: _callStack | ranges::views::reverse) if (call.second) callStackLocation.append("", call.second->location()); return callStackLocation; } pair SMTEncoder::popCallStack() { solAssert(!m_callStack.empty(), ""); auto lastCalled = m_callStack.back(); m_callStack.pop_back(); return lastCalled; } void SMTEncoder::pushCallStack(CallStackEntry _entry) { m_callStack.push_back(_entry); } void SMTEncoder::addPathImpliedExpression(smtutil::Expression const& _e) { m_context.addAssertion(smtutil::Expression::implies(currentPathConditions(), _e)); } bool SMTEncoder::isRootFunction() { return m_callStack.size() == 1; } bool SMTEncoder::visitedFunction(FunctionDefinition const* _funDef) { for (auto const& call: m_callStack) if (call.first == _funDef) return true; return false; } ContractDefinition const* SMTEncoder::currentScopeContract() { for (auto&& f: m_callStack | ranges::views::reverse | ranges::views::keys) if (auto fun = dynamic_cast(f)) return fun->annotation().contract; return nullptr; } SMTEncoder::VariableIndices SMTEncoder::copyVariableIndices() { VariableIndices indices; for (auto const& var: m_context.variables()) indices.emplace(var.first, var.second->index()); return indices; } void SMTEncoder::resetVariableIndices(VariableIndices const& _indices) { for (auto const& var: _indices) m_context.variable(*var.first)->setIndex(var.second); } void SMTEncoder::clearIndices(ContractDefinition const* _contract, FunctionDefinition const* _function) { solAssert(_contract, ""); for (auto var: stateVariablesIncludingInheritedAndPrivate(*_contract)) m_context.variable(*var)->resetIndex(); if (_function) { for (auto const& var: _function->parameters() + _function->returnParameters()) m_context.variable(*var)->resetIndex(); for (auto const& var: localVariablesIncludingModifiers(*_function, _contract)) m_context.variable(*var)->resetIndex(); } state().reset(); } Expression const* SMTEncoder::leftmostBase(IndexAccess const& _indexAccess) { Expression const* base = &_indexAccess.baseExpression(); while (auto access = dynamic_cast(base)) base = &access->baseExpression(); return base; } Type const* SMTEncoder::keyType(Type const* _type) { if (auto const* mappingType = dynamic_cast(_type)) return mappingType->keyType(); if ( dynamic_cast(_type) || dynamic_cast(_type) ) return TypeProvider::uint256(); else solAssert(false, ""); } Expression const* SMTEncoder::innermostTuple(Expression const& _expr) { auto const* tuple = dynamic_cast(&_expr); if (!tuple || tuple->isInlineArray()) return &_expr; Expression const* expr = tuple; while (tuple && !tuple->isInlineArray() && tuple->components().size() == 1) { expr = tuple->components().front().get(); tuple = dynamic_cast(expr); } solAssert(expr, ""); return expr; } Type const* SMTEncoder::underlyingType(Type const* _type) { if (auto userType = dynamic_cast(_type)) _type = &userType->underlyingType(); return _type; } TypePointers SMTEncoder::replaceUserTypes(TypePointers const& _types) { return applyMap(_types, [](auto _type) { if (auto userType = dynamic_cast(_type)) return &userType->underlyingType(); return _type; }); } pair SMTEncoder::functionCallExpression(FunctionCall const& _funCall) { Expression const* callExpr = &_funCall.expression(); auto const* callOptions = dynamic_cast(callExpr); if (callOptions) callExpr = &callOptions->expression(); return {callExpr, callOptions}; } Expression const* SMTEncoder::cleanExpression(Expression const& _expr) { auto const* expr = &_expr; if (auto const* tuple = dynamic_cast(expr)) return cleanExpression(*innermostTuple(*tuple)); if (auto const* functionCall = dynamic_cast(expr)) if (*functionCall->annotation().kind == FunctionCallKind::TypeConversion) { auto typeType = dynamic_cast(functionCall->expression().annotation().type); solAssert(typeType, ""); if (auto const* arrayType = dynamic_cast(typeType->actualType())) if (arrayType->isByteArrayOrString()) { // this is a cast to `bytes` solAssert(functionCall->arguments().size() == 1, ""); Expression const& arg = *functionCall->arguments()[0]; if ( auto const* argArrayType = dynamic_cast(arg.annotation().type); argArrayType && argArrayType->isByteArrayOrString() ) return cleanExpression(arg); } } solAssert(expr, ""); return expr; } set SMTEncoder::touchedVariables(ASTNode const& _node) { vector callStack; for (auto const& call: m_callStack) callStack.push_back(call.first); return m_variableUsage.touchedVariables(_node, callStack); } Declaration const* SMTEncoder::expressionToDeclaration(Expression const& _expr) const { if (auto const* identifier = dynamic_cast(&_expr)) return identifier->annotation().referencedDeclaration; if (auto const* outerMemberAccess = dynamic_cast(&_expr)) return outerMemberAccess->annotation().referencedDeclaration; return nullptr; } VariableDeclaration const* SMTEncoder::identifierToVariable(Expression const& _expr) const { // We do not use `expressionToDeclaration` here because we are not interested in // struct.field, for example. if (auto const* identifier = dynamic_cast(&_expr)) if (auto const* varDecl = dynamic_cast(identifier->annotation().referencedDeclaration)) { solAssert(m_context.knownVariable(*varDecl), ""); return varDecl; } // But we are interested in "contract.var", because that is the same as just "var". if (auto const* memberAccess = dynamic_cast(&_expr)) if (dynamic_cast(expressionToDeclaration( *cleanExpression(memberAccess->expression()) ))) if (auto const* varDecl = dynamic_cast(memberAccess->annotation().referencedDeclaration)) { solAssert(m_context.knownVariable(*varDecl), ""); return varDecl; } return nullptr; } MemberAccess const* SMTEncoder::isEmptyPush(Expression const& _expr) const { if ( auto const* funCall = dynamic_cast(&_expr); funCall && funCall->arguments().empty() ) { auto const& funType = dynamic_cast(*funCall->expression().annotation().type); if (funType.kind() == FunctionType::Kind::ArrayPush) return &dynamic_cast(funCall->expression()); } return nullptr; } smtutil::Expression SMTEncoder::contractAddressValue(FunctionCall const& _f) { FunctionType const& funType = dynamic_cast(*_f.expression().annotation().type); if (funType.kind() == FunctionType::Kind::Internal) return state().thisAddress(); auto [funExpr, funOptions] = functionCallExpression(_f); if (MemberAccess const* callBase = dynamic_cast(funExpr)) return expr(callBase->expression()); solAssert(false, "Unreachable!"); } VariableDeclaration const* SMTEncoder::publicGetter(Expression const& _expr) const { if (auto memberAccess = dynamic_cast(&_expr)) return dynamic_cast(memberAccess->annotation().referencedDeclaration); return nullptr; } bool SMTEncoder::isExternalCallToThis(Expression const* _expr) { auto memberAccess = dynamic_cast(_expr); if (!memberAccess) return false; auto identifier = dynamic_cast(&memberAccess->expression()); return identifier && identifier->name() == "this" && identifier->annotation().referencedDeclaration && dynamic_cast(identifier->annotation().referencedDeclaration) ; } string SMTEncoder::extraComment() { string extra; if (m_arrayAssignmentHappened) extra += "\nNote that array aliasing is not supported," " therefore all mapping information is erased after" " a mapping local variable/parameter is assigned.\n" "You can re-introduce information using require()."; return extra; } FunctionDefinition const* SMTEncoder::functionCallToDefinition( FunctionCall const& _funCall, ContractDefinition const* _scopeContract, ContractDefinition const* _contextContract ) { if (*_funCall.annotation().kind != FunctionCallKind::FunctionCall) return {}; auto [calledExpr, callOptions] = functionCallExpression(_funCall); if (TupleExpression const* fun = dynamic_cast(calledExpr)) { solAssert(fun->components().size() == 1, ""); calledExpr = innermostTuple(*calledExpr); } auto resolveVirtual = [&](auto const* _ref) -> FunctionDefinition const* { VirtualLookup lookup = *_ref->annotation().requiredLookup; solAssert(_contextContract || lookup == VirtualLookup::Static, "No contract context provided for function lookup resolution!"); auto funDef = dynamic_cast(_ref->annotation().referencedDeclaration); if (!funDef) return funDef; switch (lookup) { case VirtualLookup::Virtual: return &(funDef->resolveVirtual(*_contextContract)); case VirtualLookup::Super: { solAssert(_scopeContract, ""); auto super = _scopeContract->superContract(*_contextContract); solAssert(super, "Super contract not available."); return &funDef->resolveVirtual(*_contextContract, super); } case VirtualLookup::Static: return funDef; } solAssert(false, ""); }; if (Identifier const* fun = dynamic_cast(calledExpr)) return resolveVirtual(fun); else if (MemberAccess const* fun = dynamic_cast(calledExpr)) return resolveVirtual(fun); return {}; } vector SMTEncoder::stateVariablesIncludingInheritedAndPrivate(ContractDefinition const& _contract) { return fold( _contract.annotation().linearizedBaseContracts, vector{}, [](auto&& _acc, auto _contract) { return _acc + _contract->stateVariables(); } ); } vector SMTEncoder::stateVariablesIncludingInheritedAndPrivate(FunctionDefinition const& _function) { if (auto contract = dynamic_cast(_function.scope())) return stateVariablesIncludingInheritedAndPrivate(*contract); return {}; } vector SMTEncoder::localVariablesIncludingModifiers(FunctionDefinition const& _function, ContractDefinition const* _contract) { return _function.localVariables() + tryCatchVariables(_function) + modifiersVariables(_function, _contract); } vector SMTEncoder::tryCatchVariables(FunctionDefinition const& _function) { struct TryCatchVarsVisitor : public ASTConstVisitor { bool visit(TryCatchClause const& _catchClause) override { if (_catchClause.parameters()) { auto const& params = _catchClause.parameters()->parameters(); for (auto param: params) vars.push_back(param.get()); } return true; } vector vars; } tryCatchVarsVisitor; _function.accept(tryCatchVarsVisitor); return tryCatchVarsVisitor.vars; } vector SMTEncoder::modifiersVariables(FunctionDefinition const& _function, ContractDefinition const* _contract) { struct BlockVars: ASTConstVisitor { BlockVars(Block const& _block) { _block.accept(*this); } void endVisit(VariableDeclaration const& _var) { vars.push_back(&_var); } vector vars; }; vector vars; set visited; for (auto invok: _function.modifiers()) { if (!invok) continue; auto const* modifier = resolveModifierInvocation(*invok, _contract); if (!modifier || visited.count(modifier)) continue; visited.insert(modifier); if (modifier->isImplemented()) { vars += applyMap(modifier->parameters(), [](auto _var) { return _var.get(); }); vars += BlockVars(modifier->body()).vars; } } return vars; } ModifierDefinition const* SMTEncoder::resolveModifierInvocation(ModifierInvocation const& _invocation, ContractDefinition const* _contract) { auto const* modifier = dynamic_cast(_invocation.name().annotation().referencedDeclaration); if (modifier) { VirtualLookup lookup = *_invocation.name().annotation().requiredLookup; solAssert(lookup == VirtualLookup::Virtual || lookup == VirtualLookup::Static, ""); solAssert(_contract || lookup == VirtualLookup::Static, "No contract context provided for modifier lookup resolution!"); if (lookup == VirtualLookup::Virtual) modifier = &modifier->resolveVirtual(*_contract); } return modifier; } set const& SMTEncoder::contractFunctions(ContractDefinition const& _contract) { if (!m_contractFunctions.count(&_contract)) { auto const& functions = _contract.definedFunctions(); set resolvedFunctions(begin(functions), end(functions)); for (auto const* base: _contract.annotation().linearizedBaseContracts) { if (base == &_contract) continue; for (auto const* baseFunction: base->definedFunctions()) { if (baseFunction->isConstructor()) // We don't want to include constructors of parent contracts continue; bool overridden = false; for (auto const* function: resolvedFunctions) if ( function->name() == baseFunction->name() && function->kind() == baseFunction->kind() && FunctionType(*function).asExternallyCallableFunction(false)-> hasEqualParameterTypes(*FunctionType(*baseFunction).asExternallyCallableFunction(false)) ) { overridden = true; break; } if (!overridden) resolvedFunctions.insert(baseFunction); } } m_contractFunctions.emplace(&_contract, std::move(resolvedFunctions)); } return m_contractFunctions.at(&_contract); } set const& SMTEncoder::contractFunctionsWithoutVirtual(ContractDefinition const& _contract) { if (!m_contractFunctionsWithoutVirtual.count(&_contract)) { auto allFunctions = contractFunctions(_contract); for (auto const* base: _contract.annotation().linearizedBaseContracts) for (auto const* baseFun: base->definedFunctions()) allFunctions.insert(baseFun); m_contractFunctionsWithoutVirtual.emplace(&_contract, std::move(allFunctions)); } return m_contractFunctionsWithoutVirtual.at(&_contract); } map>> SMTEncoder::baseArguments(ContractDefinition const& _contract) { map>> baseArgs; for (auto contract: _contract.annotation().linearizedBaseContracts) { /// Collect base contracts and potential constructor arguments. for (auto specifier: contract->baseContracts()) { solAssert(specifier, ""); auto const& base = dynamic_cast(*specifier->name().annotation().referencedDeclaration); if (auto args = specifier->arguments()) baseArgs[&base] = *args; } /// Collect base constructor arguments given as constructor modifiers. if (auto constructor = contract->constructor()) for (auto mod: constructor->modifiers()) { auto decl = mod->name().annotation().referencedDeclaration; if (auto base = dynamic_cast(decl)) { solAssert(!baseArgs.count(base), ""); if (auto args = mod->arguments()) baseArgs[base] = *args; } } } return baseArgs; } RationalNumberType const* SMTEncoder::isConstant(Expression const& _expr) { if (auto type = dynamic_cast(_expr.annotation().type)) return type; // _expr may not be constant evaluable. // In that case we ignore any warnings emitted by the constant evaluator, // as it will return nullptr in case of failure. ErrorList l; ErrorReporter e(l); if (auto t = ConstantEvaluator::evaluate(e, _expr)) return TypeProvider::rationalNumber(t->value); return nullptr; } set> SMTEncoder::collectABICalls(ASTNode const* _node) { struct ABIFunctions: public ASTConstVisitor { ABIFunctions(ASTNode const* _node) { _node->accept(*this); } void endVisit(FunctionCall const& _funCall) { if (*_funCall.annotation().kind == FunctionCallKind::FunctionCall) switch (dynamic_cast(*_funCall.expression().annotation().type).kind()) { case FunctionType::Kind::ABIEncode: case FunctionType::Kind::ABIEncodePacked: case FunctionType::Kind::ABIEncodeWithSelector: case FunctionType::Kind::ABIEncodeCall: case FunctionType::Kind::ABIEncodeWithSignature: case FunctionType::Kind::ABIDecode: abiCalls.insert(&_funCall); break; default: {} } } set> abiCalls; }; return ABIFunctions(_node).abiCalls; } set SMTEncoder::sourceDependencies(SourceUnit const& _source) { set sources; sources.insert(&_source); for (auto const& source: _source.referencedSourceUnits(true)) sources.insert(source); return sources; } void SMTEncoder::createReturnedExpressions(FunctionCall const& _funCall, ContractDefinition const* _contextContract) { auto funDef = functionCallToDefinition(_funCall, currentScopeContract(), _contextContract); if (!funDef) return; auto const& returnParams = funDef->returnParameters(); for (auto param: returnParams) createVariable(*param); auto returnValues = applyMap(returnParams, [this](auto const& param) -> optional { solAssert(param && m_context.knownVariable(*param), ""); return currentValue(*param); }); defineExpr(_funCall, returnValues); } vector SMTEncoder::symbolicArguments(FunctionCall const& _funCall, ContractDefinition const* _contextContract) { auto funDef = functionCallToDefinition(_funCall, currentScopeContract(), _contextContract); solAssert(funDef, ""); vector args; Expression const* calledExpr = &_funCall.expression(); auto funType = dynamic_cast(calledExpr->annotation().type); solAssert(funType, ""); vector> arguments = _funCall.sortedArguments(); auto functionParams = funDef->parameters(); unsigned firstParam = 0; if (funType->hasBoundFirstArgument()) { calledExpr = innermostTuple(*calledExpr); auto const& attachedFunction = dynamic_cast(calledExpr); solAssert(attachedFunction, ""); args.push_back(expr(attachedFunction->expression(), functionParams.front()->type())); firstParam = 1; } solAssert((arguments.size() + firstParam) == functionParams.size(), ""); for (unsigned i = 0; i < arguments.size(); ++i) args.push_back(expr(*arguments.at(i), functionParams.at(i + firstParam)->type())); return args; } smtutil::Expression SMTEncoder::constantExpr(Expression const& _expr, VariableDeclaration const& _var) { if (RationalNumberType const* rationalType = isConstant(_expr)) { if (rationalType->isNegative()) return smtutil::Expression(u2s(rationalType->literalValue(nullptr))); else return smtutil::Expression(rationalType->literalValue(nullptr)); } else { solAssert(_var.value(), ""); _var.value()->accept(*this); return expr(*_var.value(), _expr.annotation().type); } solAssert(false, ""); } void SMTEncoder::collectFreeFunctions(set const& _sources) { for (auto source: _sources) for (auto node: source->nodes()) if (auto function = dynamic_cast(node.get())) m_freeFunctions.insert(function); else if ( auto contract = dynamic_cast(node.get()); contract && contract->isLibrary() ) for (auto function: contract->definedFunctions()) // We need to add public library functions too because they can be called // internally by internal library functions that are considered free functions. m_freeFunctions.insert(function); } void SMTEncoder::createFreeConstants(set const& _sources) { for (auto source: _sources) for (auto node: source->nodes()) if (auto var = dynamic_cast(node.get())) createVariable(*var); else if ( auto contract = dynamic_cast(node.get()); contract && contract->isLibrary() ) for (auto var: contract->stateVariables()) { solAssert(var->isConstant(), ""); createVariable(*var); } } smt::SymbolicState& SMTEncoder::state() { return m_context.state(); }