/src/solidity/libsolidity/formal/SMTEncoder.cpp

Source
/*
  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 <http://www.gnu.org/licenses/>.
*/
// SPDX-License-Identifier: GPL-3.0

#include <libsolidity/formal/SMTEncoder.h>

#include <libsolidity/ast/TypeProvider.h>
#include <libsolidity/formal/SymbolicState.h>
#include <libsolidity/formal/SymbolicTypes.h>

#include <libsolidity/analysis/ConstantEvaluator.h>

#include <libyul/AST.h>
#include <libyul/optimiser/Semantics.h>

#include <libsmtutil/SMTPortfolio.h>
#include <libsmtutil/Helpers.h>

#include <liblangutil/CharStreamProvider.h>

#include <libsolutil/Algorithms.h>
#include <libsolutil/FunctionSelector.h>

#include <range/v3/view.hpp>

#include <limits>
#include <deque>

using namespace solidity;
using namespace solidity::util;
using namespace solidity::langutil;
using namespace solidity::frontend;
using namespace std::string_literals;

SMTEncoder::SMTEncoder(
  smt::EncodingContext& _context,
  ModelCheckerSettings _settings,
  UniqueErrorReporter& _errorReporter,
  UniqueErrorReporter& _unsupportedErrorReporter,
  ErrorReporter& _provedSafeReporter,
  langutil::CharStreamProvider const& _charStreamProvider
):
  m_errorReporter(_errorReporter),
  m_unsupportedErrors(_unsupportedErrorReporter),
  m_provedSafeReporter(_provedSafeReporter),
  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 (
      !std::dynamic_pointer_cast<FunctionDefinition>(node) &&
      !std::dynamic_pointer_cast<VariableDeclaration>(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<ContractDefinition const*>(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<FunctionDefinition const&>(*m_callStack.back().first);

  if (m_modifierDepthStack.back() == static_cast<int>(function.modifiers().size()))
  {
    if (function.isImplemented())
    {
      pushInlineFrame(function);
      function.body().accept(*this);
      popInlineFrame(function);
    }
  }
  else
  {
    solAssert(m_modifierDepthStack.back() < static_cast<int>(function.modifiers().size()), "");
    ASTPointer<ModifierInvocation> const& modifierInvocation =
      function.modifiers()[static_cast<size_t>(m_modifierDepthStack.back())];
    solAssert(modifierInvocation, "");
    auto refDecl = modifierInvocation->name().annotation().referencedDeclaration;
    if (dynamic_cast<ContractDefinition const*>(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);

  std::vector<smtutil::Expression> 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<ModifierDefinition const*>(_definition))
  {
    if (modifier->isImplemented())
      modifier->body().accept(*this);
    popCallStack();
  }
  else if (auto function = dynamic_cast<FunctionDefinition const*>(_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().root());
    }

    std::map<yul::Identifier const*, InlineAssemblyAnnotation::ExternalIdentifierInfo> const& externalReferences;
    std::set<VariableDeclaration const*> 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<VariableDeclaration const*>(externalInfo->declaration))
            assignedVars.insert(varDecl);
    }
  };

  yul::SideEffectsCollector sideEffectsCollector(_inlineAsm.dialect(), _inlineAsm.operations().root());
  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<IndexAccess const*>(base))
      base = leftmostBase(*indexAccess);

    if (auto varDecl = identifierToVariable(*base))
      m_context.newValue(*varDecl);
  }
  else
  {
    if (dynamic_cast<TupleType const*>(_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 = std::dynamic_pointer_cast<smt::SymbolicArrayVariable>(m_context.expression(_tuple));
    smtAssert(symbArray, "Inline array must be represented with SymbolicArrayVariable");
    auto originalType = symbArray->originalType();
    auto arrayType = dynamic_cast<ArrayType const*>(originalType);
    smtAssert(arrayType, "Type of inline array must be ArrayType");
    addArrayLiteralAssertions(*symbArray, applyMap(_tuple.components(), [&](auto const& c) { return expr(*c, arrayType->baseType()); }));
  }
  else
  {
    auto values = applyMap(_tuple.components(), [this](auto const& component) -> std::optional<smtutil::Expression> {
      if (component)
      {
        if (!m_context.knownExpression(*component))
            createExpr(*component);
        return expr(*component);
      }
      return {};
    });
    defineExpr(_tuple, values);
  }
}

void SMTEncoder::endVisit(UnaryOperation const& _op)
{
  /// For constant expressions, we need to shortcut here
  /// due to potentially unknown rational number sizes that
  /// can appear in intermediary operations, e.g., ~(2**256 - 1).
  if (isConstant(_op))
    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)
    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<IndexAccess const*>(&subExpr) ||
        dynamic_cast<MemberAccess const*>(&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)
    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<FunctionType const&>(*_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<FunctionType const&>(*_funCall.expression().annotation().type);

  std::vector<ASTPointer<Expression const>> 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::BytesConcat:
    visitBytesConcat(_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::BlobHash:
    visitBlobHash(_funCall);
    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<MemberAccess const&>(_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_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::visitBytesConcat(FunctionCall const& _funCall)
{
  auto const& args = _funCall.sortedArguments();

  // bytes.concat call with no arguments returns an empty array
  if (args.size() == 0)
  {
    defineExpr(_funCall, smt::zeroValue(TypeProvider::bytesMemory()));
    return;
  }

  // bytes.concat with single argument of type bytes memory
  if (args.size() == 1 && args.front()->annotation().type->category() == frontend::Type::Category::Array)
  {
    defineExpr(_funCall, expr(*args.front(), TypeProvider::bytesMemory()));
    return;
  }

  auto const& [name, inTypes, outType] = state().bytesConcatFunctionTypes(&_funCall);
  solAssert(inTypes.size() == args.size(), "");

  auto symbFunction = state().bytesConcatFunction(&_funCall);
  auto out = createSelectExpressionForFunction(symbFunction, args, inTypes, args.size());

  defineExpr(_funCall, out);
}

void SMTEncoder::visitABIFunction(FunctionCall const& _funCall)
{
  auto symbFunction = state().abiFunction(&_funCall);
  auto const& [name, inTypes, outTypes] = state().abiFunctionTypes(&_funCall);

  auto const& funType = dynamic_cast<FunctionType const&>(*_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;
  }

  auto out = createSelectExpressionForFunction(symbFunction, args, inTypes, argsActualLength);
  if (outTypes.size() == 1)
    defineExpr(_funCall, out);
  else
  {
    auto symbTuple = std::dynamic_pointer_cast<smt::SymbolicTupleVariable>(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<FunctionType const&>(*_funCall.expression().annotation().type);
  auto kind = funType.kind();
  auto arg0 = expr(*_funCall.arguments().at(0), TypeProvider::bytesStorage());
  std::optional<smtutil::Expression> 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), TypeProvider::fixedBytes(32));
    auto arg1 = expr(*_funCall.arguments().at(1), TypeProvider::uint(8));
    auto arg2 = expr(*_funCall.arguments().at(2), TypeProvider::fixedBytes(32));
    auto arg3 = expr(*_funCall.arguments().at(3), TypeProvider::fixedBytes(32));
    auto inputSort = dynamic_cast<smtutil::ArraySort&>(*e.sort).domain;
    auto ecrecoverInput = smtutil::Expression::tuple_constructor(
      smtutil::Expression(std::make_shared<smtutil::SortSort>(inputSort), ""),
      {arg0, arg1, arg2, arg3}
    );
    result = smtutil::Expression::select(e, ecrecoverInput);
  }
  else
    solAssert(false, "");

  defineExpr(_funCall, *result);
}

void SMTEncoder::visitGasLeft(FunctionCall const& _funCall)
{
  std::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::visitBlobHash(FunctionCall const& _funCall)
{
  constexpr unsigned BLOB_TRANSACTION_LIMIT = 9; // Since pectra
  auto indexExpr = expr(*_funCall.arguments().at(0));
  auto valueExpr = smtutil::Expression::ite(
    indexExpr >= BLOB_TRANSACTION_LIMIT,
    smtutil::Expression(u256(0)),
    state().blobhash(indexExpr)
  );
  defineExpr(_funCall, std::move(valueExpr));
}

void SMTEncoder::visitAddMulMod(FunctionCall const& _funCall)
{
  auto const& funType = dynamic_cast<FunctionType const&>(*_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<IntegerType const&>(*_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();
  smtAssert(args.size() == 1, "Expected exactly one argument to wrap/unwrap");
  auto const& funType = dynamic_cast<FunctionType const&>(*_funCall.expression().annotation().type);
  auto const* argType = funType.parameterTypes().front();
  defineExpr(_funCall, expr(*args.front(), argType));
}

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 = std::dynamic_pointer_cast<smt::SymbolicArrayVariable>(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<TypeType const*>(_identifier.annotation().type))
    return;
  // Ignore module identifiers
  else if (dynamic_cast<ModuleType const*>(_identifier.annotation().type))
    return;
  // Ignore user defined value type identifiers
  else if (dynamic_cast<UserDefinedValueType const*>(_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<MagicType const*>(_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<TypeType const&>(*_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<ArrayType const&>(*_type).isByteArrayOrString();
  // default
  return true;
}

std::vector<std::string> structGetterReturnedMembers(StructType const& _structType)
{
  std::vector<std::string> 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(), "");
  std::deque<smtutil::Expression> 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<ArrayType const&>(*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<ArrayType const*>(type))
          type = arrayType->baseType();
        else if (auto mappingType = dynamic_cast<MappingType const*>(type))
          type = mappingType->valueType();
        else
          solAssert(false, "");
        break;
      }
      case Type::Category::Struct:
      {
        solAssert(symbArguments.empty(), "");
        smt::SymbolicStructVariable structVar(dynamic_cast<StructType const*>(type), "struct_temp_" + std::to_string(_funCall.id()), m_context);
        m_context.addAssertion(structVar.currentValue() == currentExpr);
        auto returnedMembers = structGetterReturnedMembers(dynamic_cast<StructType const&>(*structVar.type()));
        solAssert(!returnedMembers.empty(), "");
        auto returnedValues = applyMap(returnedMembers, [&](std::string const& memberName) -> std::optional<smtutil::Expression> { return structVar.member(memberName); });
        defineExpr(_funCall, returnedValues);
        return;
      }
      default:
      {
        // Unsupported cases, do nothing and the getter will be abstracted.
        return;
      }
    }
  }
}

bool SMTEncoder::shouldEncode(ContractDefinition const& _contract) const
{
  return _contract.canBeDeployed();
}

bool SMTEncoder::shouldAnalyzeVerificationTargetsFor(SourceUnit const& _source) const
{
  return m_settings.contracts.isDefault() ||
    m_settings.contracts.has(*_source.annotation().path);
}

bool SMTEncoder::shouldAnalyzeVerificationTargetsFor(ContractDefinition const& _contract) const
{
  if (!shouldEncode(_contract))
    return false;

  return m_settings.contracts.isDefault() ||
    m_settings.contracts.has(_contract.sourceUnitName(), _contract.name());
}

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<ArrayType const*>(argType);
  if (auto sliceType = dynamic_cast<ArraySliceType const*>(argType))
    arrayType = &sliceType->arrayType();

  if (arrayType && arrayType->isByteArrayOrString() && smt::isFixedBytes(*funCallType))
  {
    auto array = std::dynamic_pointer_cast<smt::SymbolicArrayVariable>(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);
  std::optional<smtutil::Expression> symbMin;
  std::optional<smtutil::Expression> 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<FixedBytesType const*>(funCallType))
      {
        auto const* fixedArg = dynamic_cast<FixedBytesType const*>(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<FixedBytesType const*>(funCallType);
    auto const* fixedArg = dynamic_cast<FixedBytesType const*>(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<FunctionType const&>(*_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<smt::SymbolicStructVariable&>(*m_context.expression(_funCall));
    auto structType = dynamic_cast<StructType const*>(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 = std::dynamic_pointer_cast<smt::SymbolicArrayVariable>(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,
  std::vector<smtutil::Expression> const& _elementValues
)
{
  m_context.addAssertion(_symArray.length() == _elementValues.size());

  // Assert to the solver that _elementValues are exactly the elements at the beginning of the array.
  // Since we create new symbolic representation for every array literal in the source file, we want to ensure that
  // representations of two equal literals are also equal. For this reason we always start from constant-zero array.
  // This ensures SMT-LIB arrays (which are infinite) are also equal beyond the length of the Solidity array literal.
  auto type = _symArray.type();
  smtAssert(type);
  auto valueType = [&]() {
    if (auto const* arrayType = dynamic_cast<ArrayType const*>(type))
      return arrayType->baseType();
    if (smt::isStringLiteral(*type))
      return TypeProvider::stringMemory()->baseType();
    smtAssert(false);
  }();
  auto tupleSort = std::dynamic_pointer_cast<smtutil::TupleSort>(smt::smtSort(*type));
  auto sortSort = std::make_shared<smtutil::SortSort>(tupleSort->components.front());
  smtutil::Expression arrayExpr = smtutil::Expression::const_array(smtutil::Expression(sortSort), smt::zeroValue(valueType));
  smtAssert(arrayExpr.sort->kind == smtutil::Kind::Array);
  for (size_t i = 0; i < _elementValues.size(); i++)
    arrayExpr = smtutil::Expression::store(arrayExpr, smtutil::Expression(i), _elementValues[i]);
  m_context.addAssertion(_symArray.elements() == arrayExpr);
}

void SMTEncoder::bytesToFixedBytesAssertions(
  smt::SymbolicArrayVariable& _symArray,
  Expression const& _fixedBytes
)
{
  auto const& fixed = dynamic_cast<FixedBytesType const&>(*_fixedBytes.annotation().type);
  auto intType = TypeProvider::uint256();
  std::string suffix = std::to_string(_fixedBytes.id()) + "_" + std::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 = std::dynamic_pointer_cast<smt::SymbolicTupleVariable>(m_context.expression(*_return.expression()));
      solAssert(symbTuple, "");
      solAssert(symbTuple->components().size() == returnParams.size(), "");

      auto const* tupleType = dynamic_cast<TupleType const*>(_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<FunctionType const*>(_memberAccess.annotation().type);
    if (functionType && functionType->hasDeclaration())
      defineExpr(
        _memberAccess,
        util::selectorFromSignatureU32(functionType->richIdentifier())
      );

    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<Identifier const*>(&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<MagicType const*>(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<IntegerType const*>(magicType->typeArgument()))
            defineExpr(_memberAccess, memberName == "min" ? integerType->minValue() : integerType->maxValue());
          else if (EnumType const* enumType = dynamic_cast<EnumType const*>(magicType->typeArgument()))
            defineExpr(_memberAccess, memberName == "min" ? enumType->minValue() : enumType->maxValue());
        }
        else if (memberName == "interfaceId")
        {
          ContractDefinition const& contract = dynamic_cast<ContractType const&>(*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 = std::dynamic_pointer_cast<smt::SymbolicStructVariable>(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<EnumDefinition const*>(decl))
    {
      auto enumType = dynamic_cast<EnumType const*>(accessType);
      solAssert(enumType, "");
      defineExpr(_memberAccess, enumType->memberValue(_memberAccess.memberName()));

      return false;
    }
    else if (dynamic_cast<ContractDefinition const*>(decl))
    {
      if (auto const* var = dynamic_cast<VariableDeclaration const*>(_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 = std::dynamic_pointer_cast<smt::SymbolicArrayVariable>(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<FunctionType const*>(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<VariableDeclaration const*>(_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<FixedBytesType const*>(_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;
  }

  std::shared_ptr<smt::SymbolicVariable> array;
  if (auto const* id = dynamic_cast<Identifier const*>(&_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 = std::dynamic_pointer_cast<smt::SymbolicArrayVariable>(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<IndexAccess const*>(lastExpr))
    {
      auto const& base = indexAccess->baseExpression();
      if (dynamic_cast<Identifier const*>(&base))
        base.accept(*this);

      Type const* baseType = base.annotation().type;
      auto indexExpr = expr(*indexAccess->indexExpression(), keyType(baseType));
      auto symbArray = std::dynamic_pointer_cast<smt::SymbolicArrayVariable>(m_context.expression(base));
      solAssert(symbArray, "");
      toStore = smtutil::Expression::tuple_constructor(
        smtutil::Expression(std::make_shared<smtutil::SortSort>(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<MemberAccess const*>(lastExpr))
    {
      auto const& base = memberAccess->expression();
      if (dynamic_cast<Identifier const*>(&base))
        base.accept(*this);

      if (
        auto const* structType = dynamic_cast<StructType const*>(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 = std::dynamic_pointer_cast<smt::SymbolicStructVariable>(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<Identifier const*>(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<ReferenceType const*>(type) ||
        dynamic_cast<MappingType const*>(type)
      )
        resetReferences(type);

      assignment(*m_context.expression(*lastExpr), toStore);
      break;
    }
  }
}

void SMTEncoder::arrayPush(FunctionCall const& _funCall)
{
  auto memberAccess = dynamic_cast<MemberAccess const*>(&_funCall.expression());
  solAssert(memberAccess, "");
  auto symbArray = std::dynamic_pointer_cast<smt::SymbolicArrayVariable>(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<ArrayType const*>(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<MemberAccess const*>(cleanExpression(_funCall.expression()));
  solAssert(memberAccess, "");
  auto symbArray = std::dynamic_pointer_cast<smt::SymbolicArrayVariable>(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(std::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."
    );
  }
}

std::pair<smtutil::Expression, smtutil::Expression> SMTEncoder::arithmeticOperation(
  Token _op,
  smtutil::Expression const& _left,
  smtutil::Expression const& _right,
  Type const* _commonType,
  Expression const& _operation
)
{
  static std::set<Token> 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<IntegerType const*>(_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 == std::numeric_limits<size_t >::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;
  std::string suffix = std::to_string(_operation.id()) + "_" + std::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 std::set<Token> 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);

  std::optional<smtutil::Expression> 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();
    std::shared_ptr<smtutil::Expression> value;
    if (smt::isNumber(*commonType))
    {
      value = std::make_shared<smtutil::Expression>(
        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 = std::make_shared<smtutil::Expression>(
        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));
}

std::pair<smtutil::Expression, smtutil::Expression> SMTEncoder::divModWithSlacks(
  smtutil::Expression _left,
  smtutil::Expression _right,
  IntegerType const& _type
)
{
  if (m_settings.divModNoSlacks)
    return {_left / _right, _left % _right};

  IntegerType const* intType = &_type;
  std::string suffix = "div_mod_" + std::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<IndexAccess const*>(left) ||
    dynamic_cast<MemberAccess const*>(left)
  )
    indexOrMemberAssignment(*left, _right);
  else if (auto const* funCall = dynamic_cast<FunctionCall const*>(left))
  {
    if (auto funType = dynamic_cast<FunctionType const*>(funCall->expression().annotation().type))
    {
      if (funType->kind() == FunctionType::Kind::ArrayPush)
      {
        auto memberAccess = dynamic_cast<MemberAccess const*>(&funCall->expression());
        solAssert(memberAccess, "");
        auto symbArray = std::dynamic_pointer_cast<smt::SymbolicArrayVariable>(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<ReferenceType const*>(type))
            resetReferences(type);
      }
    }
  }
  else
    solAssert(false, "");
}

void SMTEncoder::tupleAssignment(Expression const& _left, Expression const& _right)
{
  auto lTuple = dynamic_cast<TupleExpression const*>(&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<TupleExpression const*>(&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<TupleType const*>(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 std::map<Token, Token> const compoundToArithmetic{
    {Token::AssignAdd, Token::Add},
    {Token::AssignSub, Token::Sub},
    {Token::AssignMul, Token::Mul},
    {Token::AssignDiv, Token::Div},
    {Token::AssignMod, Token::Mod}
  };
  static std::map<Token, Token> 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(std::vector<std::shared_ptr<VariableDeclaration>> const& _variables, Expression const& _rhs)
{
  auto symbolicVar = m_context.expression(_rhs);
  if (_variables.size() > 1)
  {
    auto symbTuple = std::dynamic_pointer_cast<smt::SymbolicTupleVariable>(symbolicVar);
    solAssert(symbTuple, "");
    auto const& symbComponents = symbTuple->components();
    solAssert(symbComponents.size() == _variables.size(), "");
    auto tupleType = dynamic_cast<TupleType const*>(_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);
}

std::pair<SMTEncoder::VariableIndices, smtutil::Expression> SMTEncoder::visitBranch(
  ASTNode const* _statement,
  smtutil::Expression _condition
)
{
  return visitBranch(_statement, &_condition);
}

std::pair<SMTEncoder::VariableIndices, smtutil::Expression> 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, std::vector<smtutil::Expression> 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;
    }

  std::vector<VariableDeclaration const*> localVars;
  if (auto const* fun = dynamic_cast<FunctionDefinition const*>(&_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<Type const*> bfs{{_a}};
  bfs.run([&](auto _type, auto&& _addChild) {
    if (*typeWithoutPointer(_b) == *typeWithoutPointer(_type))
    {
      foundSame = true;
      bfs.abort();
    }
    if (auto const* mapType = dynamic_cast<MappingType const*>(_type))
      _addChild(mapType->valueType());
    else if (auto const* arrayType = dynamic_cast<ArrayType const*>(_type))
      _addChild(arrayType->baseType());
    else if (auto const* structType = dynamic_cast<StructType const*>(_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<ReferenceType const*>(_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, std::vector<std::optional<smtutil::Expression>> const& _values)
{
  if (_values.size() == 1 && _values.front())
  {
    defineExpr(_e, *_values.front());
    return;
  }
  auto const& symbTuple = std::dynamic_pointer_cast<smt::SymbolicTupleVariable>(m_context.expression(_e));
  solAssert(symbTuple, "");
  symbTuple->increaseIndex();
  auto const& symbComponents = symbTuple->components();
  solAssert(symbComponents.size() == _values.size(), "");
  auto tupleType = dynamic_cast<TupleType const*>(_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(std::vector<CallStackEntry> 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;
}

std::pair<CallableDeclaration const*, ASTNode const*> 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<FunctionDefinition const*>(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<IndexAccess const*>(base))
    base = &access->baseExpression();
  return base;
}

Type const* SMTEncoder::keyType(Type const* _type)
{
  if (auto const* mappingType = dynamic_cast<MappingType const*>(_type))
    return mappingType->keyType();
  if (
    dynamic_cast<ArrayType const*>(_type) ||
    dynamic_cast<ArraySliceType const*>(_type)
  )
    return TypeProvider::uint256();
  else
    solAssert(false, "");
}

Expression const& SMTEncoder::innermostTuple(Expression const& _expr)
{
  auto const* tuple = dynamic_cast<TupleExpression const*>(&_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<TupleExpression const*>(expr);
  }
  solAssert(expr, "");
  return *expr;
}

Type const* SMTEncoder::underlyingType(Type const* _type)
{
  if (auto userType = dynamic_cast<UserDefinedValueType const*>(_type))
    _type = &userType->underlyingType();
  return _type;
}

TypePointers SMTEncoder::replaceUserTypes(TypePointers const& _types)
{
  return applyMap(_types, [](auto _type) {
    if (auto userType = dynamic_cast<UserDefinedValueType const*>(_type))
      return &userType->underlyingType();
    return _type;
  });
}

std::pair<Expression const*, FunctionCallOptions const*> SMTEncoder::functionCallExpression(FunctionCall const& _funCall)
{
  Expression const* callExpr = &innermostTuple(_funCall.expression());
  auto const* callOptions = dynamic_cast<FunctionCallOptions const*>(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<TupleExpression const*>(expr))
    return cleanExpression(innermostTuple(*tuple));
  if (auto const* functionCall = dynamic_cast<FunctionCall const*>(expr))
    if (*functionCall->annotation().kind == FunctionCallKind::TypeConversion)
    {
      auto typeType = dynamic_cast<TypeType const*>(functionCall->expression().annotation().type);
      solAssert(typeType, "");
      if (auto const* arrayType = dynamic_cast<ArrayType const*>(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<ArrayType const*>(arg.annotation().type);
            argArrayType && argArrayType->isByteArrayOrString()
          )
            return cleanExpression(arg);
        }
    }
  solAssert(expr, "");
  return expr;
}

Declaration const* SMTEncoder::expressionToDeclaration(Expression const& _expr) const
{
  if (auto const* identifier = dynamic_cast<Identifier const*>(&_expr))
    return identifier->annotation().referencedDeclaration;
  if (auto const* outerMemberAccess = dynamic_cast<MemberAccess const*>(&_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<Identifier const*>(&_expr))
    if (auto const* varDecl = dynamic_cast<VariableDeclaration const*>(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<MemberAccess const*>(&_expr))
    if (dynamic_cast<ContractDefinition const*>(expressionToDeclaration(
      *cleanExpression(memberAccess->expression())
    )))
      if (auto const* varDecl = dynamic_cast<VariableDeclaration const*>(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<FunctionCall const*>(&_expr);
    funCall && funCall->arguments().empty()
  )
  {
    auto const& funType = dynamic_cast<FunctionType const&>(*funCall->expression().annotation().type);
    if (funType.kind() == FunctionType::Kind::ArrayPush)
      return &dynamic_cast<MemberAccess const&>(funCall->expression());
  }
  return nullptr;
}

smtutil::Expression SMTEncoder::contractAddressValue(FunctionCall const& _f)
{
  FunctionType const& funType = dynamic_cast<FunctionType const&>(*_f.expression().annotation().type);
  if (funType.kind() == FunctionType::Kind::Internal)
    return state().thisAddress();
  auto [funExpr, funOptions] = functionCallExpression(_f);
  if (MemberAccess const* callBase = dynamic_cast<MemberAccess const*>(funExpr))
    return expr(callBase->expression());
  smtAssert(false, "Unexpected function call type encountered while getting contract address!");
}

VariableDeclaration const* SMTEncoder::publicGetter(Expression const& _expr) const {
  if (auto memberAccess = dynamic_cast<MemberAccess const*>(&_expr))
    if (auto variableDeclaration = dynamic_cast<VariableDeclaration const*>(memberAccess->annotation().referencedDeclaration))
      return variableDeclaration->isStateVariable() ? variableDeclaration : nullptr;
  return nullptr;
}

bool SMTEncoder::isExternalCallToThis(Expression const* _expr) {
  auto memberAccess = dynamic_cast<MemberAccess const*>(_expr);
  if (!memberAccess)
    return false;

  auto identifier = dynamic_cast<Identifier const*>(&memberAccess->expression());
  return identifier &&
    identifier->name() == "this" &&
    identifier->annotation().referencedDeclaration &&
    dynamic_cast<MagicVariableDeclaration const*>(identifier->annotation().referencedDeclaration)
  ;
}

std::string SMTEncoder::extraComment()
{
  std::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<TupleExpression const*>(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<FunctionDefinition const*>(_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<Identifier const*>(calledExpr))
    return resolveVirtual(fun);
  else if (MemberAccess const* fun = dynamic_cast<MemberAccess const*>(calledExpr))
    return resolveVirtual(fun);

  return {};
}

std::vector<VariableDeclaration const*> SMTEncoder::stateVariablesIncludingInheritedAndPrivate(ContractDefinition const& _contract)
{
  return fold(
    _contract.annotation().linearizedBaseContracts,
    std::vector<VariableDeclaration const*>{},
    [](auto&& _acc, auto _contract) { return _acc + _contract->stateVariables(); }
  );
}

std::vector<VariableDeclaration const*> SMTEncoder::stateVariablesIncludingInheritedAndPrivate(FunctionDefinition const& _function)
{
  if (auto contract = dynamic_cast<ContractDefinition const*>(_function.scope()))
    return stateVariablesIncludingInheritedAndPrivate(*contract);
  return {};
}

std::vector<VariableDeclaration const*> SMTEncoder::localVariablesIncludingModifiers(FunctionDefinition const& _function, ContractDefinition const* _contract)
{
  return _function.localVariables() + tryCatchVariables(_function) + modifiersVariables(_function, _contract);
}

std::vector<VariableDeclaration const*> 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;
    }

    std::vector<VariableDeclaration const*> vars;
  } tryCatchVarsVisitor;
  _function.accept(tryCatchVarsVisitor);
  return tryCatchVarsVisitor.vars;
}

std::vector<VariableDeclaration const*> 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); }
    std::vector<VariableDeclaration const*> vars;
  };

  std::vector<VariableDeclaration const*> vars;
  std::set<ModifierDefinition const*> 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<ModifierDefinition const*>(_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;
}

std::set<FunctionDefinition const*, ASTNode::CompareByID> const& SMTEncoder::contractFunctions(ContractDefinition const& _contract)
{
  if (!m_contractFunctions.count(&_contract))
  {
    auto const& functions = _contract.definedFunctions();
    std::set<FunctionDefinition const*, ASTNode::CompareByID> 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);
}

std::set<FunctionDefinition const*, ASTNode::CompareByID> 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);
}

std::map<ContractDefinition const*, std::vector<ASTPointer<frontend::Expression>>> SMTEncoder::baseArguments(ContractDefinition const& _contract)
{
  std::map<ContractDefinition const*, std::vector<ASTPointer<Expression>>> 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<ContractDefinition const&>(*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<ContractDefinition const*>(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<RationalNumberType const*>(_expr.annotation().type))
    return type;

  if (
    auto typedValue = ConstantEvaluator::tryEvaluate(_expr);
    std::holds_alternative<rational>(typedValue.value)
  )
    return TypeProvider::rationalNumber(std::get<rational>(typedValue.value));

  return nullptr;
}

std::set<FunctionCall const*, ASTCompareByID<FunctionCall>> 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<FunctionType const&>(*_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: {}
        }
    }

    std::set<FunctionCall const*, ASTCompareByID<FunctionCall>> abiCalls;
  };

  return ABIFunctions(_node).abiCalls;
}

std::set<FunctionCall const*, ASTCompareByID<FunctionCall>> SMTEncoder::collectBytesConcatCalls(ASTNode const* _node)
{
  struct BytesConcatFunctions: public ASTConstVisitor
  {
    BytesConcatFunctions(ASTNode const* _node) { _node->accept(*this); }
    void endVisit(FunctionCall const& _funCall)
    {
      if (*_funCall.annotation().kind == FunctionCallKind::FunctionCall)
        switch (dynamic_cast<FunctionType const&>(*_funCall.expression().annotation().type).kind())
        {
        case FunctionType::Kind::BytesConcat:
          bytesConcatCalls.insert(&_funCall);
          break;
        default: {}
        }
    }

    std::set<FunctionCall const*, ASTCompareByID<FunctionCall>> bytesConcatCalls;
  };

  return BytesConcatFunctions(_node).bytesConcatCalls;
}

std::set<SourceUnit const*, ASTNode::CompareByID> SMTEncoder::sourceDependencies(SourceUnit const& _source)
{
  std::set<SourceUnit const*, ASTNode::CompareByID> sources;
  sources.insert(&_source);
  for (auto const& source: _source.referencedSourceUnits(true))
    sources.insert(source);
  return sources;
}

void SMTEncoder::createReturnedExpressions(FunctionDefinition const* _funDef, Expression const& _callStackExpr)
{
  if (!_funDef)
    return;

  auto const& returnParams = _funDef->returnParameters();
  for (auto param: returnParams)
    createVariable(*param);
  auto returnValues = applyMap(returnParams, [this](auto const& param) -> std::optional<smtutil::Expression> {
    solAssert(param && m_context.knownVariable(*param), "");
    return currentValue(*param);
  });
  defineExpr(_callStackExpr, returnValues);
}

std::vector<smtutil::Expression> SMTEncoder::symbolicArguments(
  std::vector<ASTPointer<VariableDeclaration>> const& _funParameters,
  std::vector<Expression const*> const& _arguments,
  std::optional<Expression const*> _boundArgumentCall
)
{
  std::vector<smtutil::Expression> args;
  unsigned firstParam = 0;
  if (_boundArgumentCall)
  {
    Expression const& calledExpr = innermostTuple(*_boundArgumentCall.value());
    auto const& attachedFunction = dynamic_cast<MemberAccess const*>(&calledExpr);
    solAssert(attachedFunction, "");
    args.push_back(expr(attachedFunction->expression(), _funParameters.front()->type()));
    firstParam = 1;
  }

  solAssert((_arguments.size() + firstParam) == _funParameters.size(), "");

  for (unsigned i = 0; i < _arguments.size(); ++i)
    args.push_back(expr(*_arguments.at(i), _funParameters.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(std::set<SourceUnit const*, ASTNode::CompareByID> const& _sources)
{
  for (auto source: _sources)
    for (auto node: source->nodes())
      if (auto function = dynamic_cast<FunctionDefinition const*>(node.get()))
        m_freeFunctions.insert(function);
      else if (
        auto contract = dynamic_cast<ContractDefinition const*>(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(std::set<SourceUnit const*, ASTNode::CompareByID> const& _sources)
{
  for (auto source: _sources)
    for (auto node: source->nodes())
      if (auto var = dynamic_cast<VariableDeclaration const*>(node.get()))
        createVariable(*var);
      else if (
        auto contract = dynamic_cast<ContractDefinition const*>(node.get());
        contract && contract->isLibrary()
      )
        for (auto var: contract->stateVariables())
        {
          solAssert(var->isConstant(), "");
          createVariable(*var);
        }
}

void SMTEncoder::createStateVariables(std::set<SourceUnit const*, ASTNode::CompareByID> const& _sources)
{
  for (auto const& source: _sources)
    for (auto const& node: source->nodes())
      if (auto contract = dynamic_cast<ContractDefinition const*>(node.get()))
        createStateVariables(*contract);
}

smt::SymbolicState& SMTEncoder::state()
{
  return m_context.state();
}

smtutil::Expression SMTEncoder::createSelectExpressionForFunction(
  smtutil::Expression symbFunction,
  std::vector<frontend::ASTPointer<frontend::Expression const>> const& args,
  frontend::TypePointers const& inTypes,
  unsigned long argsActualLength
)
{
  solAssert(argsActualLength <= args.size() && inTypes.size() == argsActualLength);
  if (inTypes.size() == 1)
  {
    smtutil::Expression arg = expr(*args.at(0), inTypes.at(0));
    return smtutil::Expression::select(symbFunction, arg);
  }

  std::vector<smtutil::Expression> symbArgs;
  for (unsigned i = 0; i < argsActualLength; ++i)
    if (args.at(i))
      symbArgs.emplace_back(expr(*args.at(i), inTypes.at(i)));

  auto inputSort = dynamic_cast<smtutil::ArraySort&>(*symbFunction.sort).domain;
  smtutil::Expression arg = smtutil::Expression::tuple_constructor(
    smtutil::Expression(std::make_shared<smtutil::SortSort>(inputSort), ""),
    symbArgs
  );
  return smtutil::Expression::select(symbFunction, arg);
}

Coverage Report

Created: 2026-06-30 07:08