2017-07-06 09:05:05 +00:00
|
|
|
/*
|
|
|
|
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/>.
|
|
|
|
*/
|
2020-07-17 14:54:12 +00:00
|
|
|
// SPDX-License-Identifier: GPL-3.0
|
2017-07-06 09:05:05 +00:00
|
|
|
|
2019-06-25 10:46:17 +00:00
|
|
|
#include <libsolidity/formal/SMTEncoder.h>
|
2017-07-06 09:05:05 +00:00
|
|
|
|
2019-04-15 13:33:39 +00:00
|
|
|
#include <libsolidity/ast/TypeProvider.h>
|
2020-03-24 19:15:15 +00:00
|
|
|
#include <libsolidity/formal/SymbolicState.h>
|
2018-10-15 15:32:17 +00:00
|
|
|
#include <libsolidity/formal/SymbolicTypes.h>
|
2017-09-28 13:24:24 +00:00
|
|
|
|
2020-12-16 10:27:56 +00:00
|
|
|
#include <libsolidity/analysis/ConstantEvaluator.h>
|
|
|
|
|
2021-01-18 09:37:09 +00:00
|
|
|
#include <libyul/AST.h>
|
|
|
|
#include <libyul/optimiser/Semantics.h>
|
|
|
|
|
2020-05-18 15:42:24 +00:00
|
|
|
#include <libsmtutil/SMTPortfolio.h>
|
2020-05-11 17:56:29 +00:00
|
|
|
#include <libsmtutil/Helpers.h>
|
2020-05-18 15:42:24 +00:00
|
|
|
|
2021-07-01 15:28:06 +00:00
|
|
|
#include <liblangutil/CharStreamProvider.h>
|
|
|
|
|
2021-01-25 17:17:56 +00:00
|
|
|
#include <range/v3/view.hpp>
|
|
|
|
|
2017-07-14 09:49:27 +00:00
|
|
|
|
2021-03-04 13:23:41 +00:00
|
|
|
#include <deque>
|
|
|
|
|
2017-07-06 09:05:05 +00:00
|
|
|
using namespace std;
|
2019-12-11 16:31:36 +00:00
|
|
|
using namespace solidity;
|
|
|
|
using namespace solidity::util;
|
|
|
|
using namespace solidity::langutil;
|
|
|
|
using namespace solidity::frontend;
|
2017-07-06 09:05:05 +00:00
|
|
|
|
2021-04-15 10:31:45 +00:00
|
|
|
SMTEncoder::SMTEncoder(
|
|
|
|
smt::EncodingContext& _context,
|
2021-07-01 15:28:06 +00:00
|
|
|
ModelCheckerSettings const& _settings,
|
2021-08-27 09:40:20 +00:00
|
|
|
UniqueErrorReporter& _errorReporter,
|
2021-07-01 15:28:06 +00:00
|
|
|
langutil::CharStreamProvider const& _charStreamProvider
|
2021-04-15 10:31:45 +00:00
|
|
|
):
|
2021-08-27 09:40:20 +00:00
|
|
|
m_errorReporter(_errorReporter),
|
2021-04-15 10:31:45 +00:00
|
|
|
m_context(_context),
|
2021-07-01 15:28:06 +00:00
|
|
|
m_settings(_settings),
|
|
|
|
m_charStreamProvider(_charStreamProvider)
|
2017-07-06 09:05:05 +00:00
|
|
|
{
|
|
|
|
}
|
|
|
|
|
2021-08-27 14:45:41 +00:00
|
|
|
void SMTEncoder::resetSourceAnalysis()
|
2020-12-09 09:52:49 +00:00
|
|
|
{
|
2021-08-27 14:45:41 +00:00
|
|
|
m_freeFunctions.clear();
|
2020-12-09 09:52:49 +00:00
|
|
|
}
|
|
|
|
|
2019-06-25 10:46:17 +00:00
|
|
|
bool SMTEncoder::visit(ContractDefinition const& _contract)
|
2018-04-30 14:30:41 +00:00
|
|
|
{
|
2019-09-28 19:04:49 +00:00
|
|
|
solAssert(m_currentContract, "");
|
2019-08-02 16:36:26 +00:00
|
|
|
|
2019-09-28 19:04:49 +00:00
|
|
|
for (auto const& node: _contract.subNodes())
|
2019-09-26 14:12:27 +00:00
|
|
|
if (
|
|
|
|
!dynamic_pointer_cast<FunctionDefinition>(node) &&
|
|
|
|
!dynamic_pointer_cast<VariableDeclaration>(node)
|
|
|
|
)
|
2019-09-28 19:04:49 +00:00
|
|
|
node->accept(*this);
|
2019-07-09 14:39:30 +00:00
|
|
|
|
2019-09-28 19:04:49 +00:00
|
|
|
for (auto const& base: _contract.annotation().linearizedBaseContracts)
|
2019-09-26 14:12:27 +00:00
|
|
|
{
|
|
|
|
// Look for all the constructor invocations bottom up.
|
|
|
|
if (auto const& constructor = base->constructor())
|
|
|
|
for (auto const& invocation: constructor->modifiers())
|
|
|
|
{
|
2020-08-11 09:18:22 +00:00
|
|
|
auto refDecl = invocation->name().annotation().referencedDeclaration;
|
2019-09-26 14:12:27 +00:00
|
|
|
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.
|
2021-04-07 12:52:56 +00:00
|
|
|
for (auto const* function: contractFunctionsWithoutVirtual(_contract) + allFreeFunctions())
|
2019-09-26 14:12:27 +00:00
|
|
|
if (!function->isConstructor())
|
|
|
|
function->accept(*this);
|
|
|
|
|
|
|
|
// Constructors need to be handled by the engines separately.
|
2019-09-28 19:04:49 +00:00
|
|
|
|
|
|
|
return false;
|
2018-04-30 14:30:41 +00:00
|
|
|
}
|
|
|
|
|
2019-08-02 16:36:26 +00:00
|
|
|
void SMTEncoder::endVisit(ContractDefinition const& _contract)
|
2018-04-30 14:30:41 +00:00
|
|
|
{
|
2019-05-10 14:28:29 +00:00
|
|
|
m_context.resetAllVariables();
|
2019-08-02 16:36:26 +00:00
|
|
|
|
2019-09-26 14:12:27 +00:00
|
|
|
m_baseConstructorCalls.clear();
|
|
|
|
|
2019-08-02 16:36:26 +00:00
|
|
|
solAssert(m_currentContract == &_contract, "");
|
|
|
|
m_currentContract = nullptr;
|
2020-04-14 21:25:56 +00:00
|
|
|
|
|
|
|
if (m_callStack.empty())
|
|
|
|
m_context.popSolver();
|
2018-04-30 14:30:41 +00:00
|
|
|
}
|
|
|
|
|
2019-06-25 10:46:17 +00:00
|
|
|
void SMTEncoder::endVisit(VariableDeclaration const& _varDecl)
|
2017-07-11 11:26:43 +00:00
|
|
|
{
|
2019-09-26 14:12:27 +00:00
|
|
|
// State variables are handled by the constructor.
|
|
|
|
if (_varDecl.isLocalVariable() &&_varDecl.value())
|
2019-06-24 15:58:56 +00:00
|
|
|
assignment(_varDecl, *_varDecl.value());
|
2017-07-11 11:26:43 +00:00
|
|
|
}
|
|
|
|
|
2019-06-25 10:46:17 +00:00
|
|
|
bool SMTEncoder::visit(ModifierDefinition const&)
|
2019-03-11 20:06:28 +00:00
|
|
|
{
|
|
|
|
return false;
|
|
|
|
}
|
|
|
|
|
2019-06-25 10:46:17 +00:00
|
|
|
bool SMTEncoder::visit(FunctionDefinition const& _function)
|
2017-07-11 11:26:43 +00:00
|
|
|
{
|
2021-04-07 12:52:56 +00:00
|
|
|
solAssert(m_currentContract, "");
|
|
|
|
|
2019-05-06 18:03:11 +00:00
|
|
|
m_modifierDepthStack.push_back(-1);
|
2019-09-26 14:12:27 +00:00
|
|
|
|
2020-09-02 08:45:47 +00:00
|
|
|
initializeLocalVariables(_function);
|
2019-09-26 14:12:27 +00:00
|
|
|
|
|
|
|
_function.parameterList().accept(*this);
|
|
|
|
if (_function.returnParameterList())
|
|
|
|
_function.returnParameterList()->accept(*this);
|
|
|
|
|
|
|
|
visitFunctionOrModifier();
|
|
|
|
|
2019-03-11 20:06:28 +00:00
|
|
|
return false;
|
|
|
|
}
|
|
|
|
|
2019-06-25 10:46:17 +00:00
|
|
|
void SMTEncoder::visitFunctionOrModifier()
|
2019-03-11 20:06:28 +00:00
|
|
|
{
|
2019-05-06 18:03:11 +00:00
|
|
|
solAssert(!m_callStack.empty(), "");
|
2019-03-11 20:06:28 +00:00
|
|
|
solAssert(!m_modifierDepthStack.empty(), "");
|
|
|
|
|
|
|
|
++m_modifierDepthStack.back();
|
2019-05-06 18:03:11 +00:00
|
|
|
FunctionDefinition const& function = dynamic_cast<FunctionDefinition const&>(*m_callStack.back().first);
|
2019-03-11 20:06:28 +00:00
|
|
|
|
2020-06-02 13:42:46 +00:00
|
|
|
if (m_modifierDepthStack.back() == static_cast<int>(function.modifiers().size()))
|
2019-03-11 20:06:28 +00:00
|
|
|
{
|
|
|
|
if (function.isImplemented())
|
2020-07-27 17:39:17 +00:00
|
|
|
{
|
|
|
|
pushInlineFrame(function);
|
2019-03-11 20:06:28 +00:00
|
|
|
function.body().accept(*this);
|
2020-07-27 17:39:17 +00:00
|
|
|
popInlineFrame(function);
|
|
|
|
}
|
2019-03-11 20:06:28 +00:00
|
|
|
}
|
|
|
|
else
|
|
|
|
{
|
2020-06-02 13:42:46 +00:00
|
|
|
solAssert(m_modifierDepthStack.back() < static_cast<int>(function.modifiers().size()), "");
|
|
|
|
ASTPointer<ModifierInvocation> const& modifierInvocation =
|
|
|
|
function.modifiers()[static_cast<size_t>(m_modifierDepthStack.back())];
|
2019-03-11 20:06:28 +00:00
|
|
|
solAssert(modifierInvocation, "");
|
2020-08-11 09:18:22 +00:00
|
|
|
auto refDecl = modifierInvocation->name().annotation().referencedDeclaration;
|
2019-09-26 14:12:27 +00:00
|
|
|
if (dynamic_cast<ContractDefinition const*>(refDecl))
|
|
|
|
visitFunctionOrModifier();
|
2020-12-21 10:41:35 +00:00
|
|
|
else if (auto modifier = resolveModifierInvocation(*modifierInvocation, m_currentContract))
|
2021-01-21 18:04:34 +00:00
|
|
|
{
|
|
|
|
m_scopes.push_back(modifier);
|
2020-12-21 10:41:35 +00:00
|
|
|
inlineModifierInvocation(modifierInvocation.get(), modifier);
|
2021-01-21 18:04:34 +00:00
|
|
|
solAssert(m_scopes.back() == modifier, "");
|
|
|
|
m_scopes.pop_back();
|
|
|
|
}
|
2019-09-26 14:12:27 +00:00
|
|
|
else
|
|
|
|
solAssert(false, "");
|
|
|
|
}
|
|
|
|
|
|
|
|
--m_modifierDepthStack.back();
|
|
|
|
}
|
|
|
|
|
|
|
|
void SMTEncoder::inlineModifierInvocation(ModifierInvocation const* _invocation, CallableDeclaration const* _definition)
|
|
|
|
{
|
|
|
|
solAssert(_invocation, "");
|
|
|
|
_invocation->accept(*this);
|
|
|
|
|
2020-05-19 12:14:46 +00:00
|
|
|
vector<smtutil::Expression> args;
|
2019-09-26 14:12:27 +00:00
|
|
|
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});
|
2020-07-27 17:39:17 +00:00
|
|
|
pushInlineFrame(*_definition);
|
2019-09-26 14:12:27 +00:00
|
|
|
if (auto modifier = dynamic_cast<ModifierDefinition const*>(_definition))
|
|
|
|
{
|
2020-04-15 10:42:15 +00:00
|
|
|
if (modifier->isImplemented())
|
|
|
|
modifier->body().accept(*this);
|
2019-09-26 14:12:27 +00:00
|
|
|
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)
|
|
|
|
}
|
2020-07-27 17:39:17 +00:00
|
|
|
popInlineFrame(*_definition);
|
2019-09-26 14:12:27 +00:00
|
|
|
}
|
|
|
|
|
|
|
|
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())
|
2019-11-13 11:21:37 +00:00
|
|
|
{
|
2019-09-26 14:12:27 +00:00
|
|
|
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;
|
2019-11-13 11:21:37 +00:00
|
|
|
}
|
2019-03-11 20:06:28 +00:00
|
|
|
}
|
2018-10-10 12:31:49 +00:00
|
|
|
|
2019-09-26 14:12:27 +00:00
|
|
|
initializeStateVariables(_contract);
|
2019-03-11 20:06:28 +00:00
|
|
|
}
|
|
|
|
|
2019-06-25 10:46:17 +00:00
|
|
|
bool SMTEncoder::visit(PlaceholderStatement const&)
|
2019-03-11 20:06:28 +00:00
|
|
|
{
|
2019-05-06 18:03:11 +00:00
|
|
|
solAssert(!m_callStack.empty(), "");
|
|
|
|
auto lastCall = popCallStack();
|
2019-03-11 20:06:28 +00:00
|
|
|
visitFunctionOrModifier();
|
|
|
|
pushCallStack(lastCall);
|
2017-07-11 11:26:43 +00:00
|
|
|
return true;
|
|
|
|
}
|
|
|
|
|
2019-06-25 10:46:17 +00:00
|
|
|
void SMTEncoder::endVisit(FunctionDefinition const&)
|
2017-07-11 11:26:43 +00:00
|
|
|
{
|
2021-04-07 12:52:56 +00:00
|
|
|
solAssert(m_currentContract, "");
|
|
|
|
|
2019-06-24 15:37:03 +00:00
|
|
|
popCallStack();
|
2019-05-06 18:03:11 +00:00
|
|
|
solAssert(m_modifierDepthStack.back() == -1, "");
|
|
|
|
m_modifierDepthStack.pop_back();
|
|
|
|
if (m_callStack.empty())
|
2019-06-24 15:37:03 +00:00
|
|
|
m_context.popSolver();
|
2017-07-11 11:26:43 +00:00
|
|
|
}
|
|
|
|
|
2020-12-16 17:32:34 +00:00
|
|
|
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;
|
|
|
|
}
|
|
|
|
}
|
|
|
|
|
2019-06-25 10:46:17 +00:00
|
|
|
bool SMTEncoder::visit(InlineAssembly const& _inlineAsm)
|
2019-04-05 14:41:05 +00:00
|
|
|
{
|
2021-01-18 09:37:09 +00:00
|
|
|
/// This is very similar to `yul::Assignments`, except I need to collect `Identifier`s and not just names as `YulString`s.
|
|
|
|
struct AssignedExternalsCollector: public yul::ASTWalker
|
|
|
|
{
|
|
|
|
AssignedExternalsCollector(InlineAssembly const& _inlineAsm): externalReferences(_inlineAsm.annotation().externalReferences)
|
|
|
|
{
|
|
|
|
this->operator()(_inlineAsm.operations());
|
|
|
|
}
|
|
|
|
|
|
|
|
map<yul::Identifier const*, InlineAssemblyAnnotation::ExternalIdentifierInfo> const& externalReferences;
|
|
|
|
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 = valueOrNullptr(externalReferences, &identifier))
|
|
|
|
if (auto varDecl = dynamic_cast<VariableDeclaration const*>(externalInfo->declaration))
|
|
|
|
assignedVars.insert(varDecl);
|
|
|
|
}
|
|
|
|
};
|
|
|
|
|
|
|
|
yul::SideEffectsCollector sideEffectsCollector(_inlineAsm.dialect(), _inlineAsm.operations());
|
|
|
|
if (sideEffectsCollector.invalidatesMemory())
|
|
|
|
resetMemoryVariables();
|
|
|
|
if (sideEffectsCollector.invalidatesStorage())
|
|
|
|
resetStorageVariables();
|
|
|
|
|
|
|
|
auto assignedVars = AssignedExternalsCollector(_inlineAsm).assignedVars;
|
|
|
|
for (auto const* var: assignedVars)
|
|
|
|
{
|
|
|
|
solAssert(var, "");
|
|
|
|
solAssert(var->isLocalVariable(), "Non-local variable assigned in inlined assembly");
|
|
|
|
m_context.resetVariable(*var);
|
|
|
|
}
|
|
|
|
|
2019-04-05 14:41:05 +00:00
|
|
|
m_errorReporter.warning(
|
2020-05-05 22:38:28 +00:00
|
|
|
7737_error,
|
2019-04-05 14:41:05 +00:00
|
|
|
_inlineAsm.location(),
|
2021-01-18 09:37:09 +00:00
|
|
|
"Inline assembly may cause SMTChecker to produce spurious warnings (false positives)."
|
2019-04-05 14:41:05 +00:00
|
|
|
);
|
|
|
|
return false;
|
|
|
|
}
|
|
|
|
|
2020-07-27 17:39:17 +00:00
|
|
|
void SMTEncoder::pushInlineFrame(CallableDeclaration const&)
|
|
|
|
{
|
|
|
|
pushPathCondition(currentPathConditions());
|
|
|
|
}
|
|
|
|
|
|
|
|
void SMTEncoder::popInlineFrame(CallableDeclaration const&)
|
|
|
|
{
|
|
|
|
popPathCondition();
|
|
|
|
}
|
|
|
|
|
2019-06-25 10:46:17 +00:00
|
|
|
void SMTEncoder::endVisit(VariableDeclarationStatement const& _varDecl)
|
2017-07-11 11:26:43 +00:00
|
|
|
{
|
2021-01-12 14:07:30 +00:00
|
|
|
if (auto init = _varDecl.initialValue())
|
|
|
|
expressionToTupleAssignment(_varDecl.declarations(), *init);
|
2017-07-11 11:26:43 +00:00
|
|
|
}
|
|
|
|
|
2020-10-26 16:16:27 +00:00
|
|
|
bool SMTEncoder::visit(Assignment const& _assignment)
|
|
|
|
{
|
2021-03-23 18:34:46 +00:00
|
|
|
// RHS must be visited before LHS; as opposed to what Assignment::accept does
|
|
|
|
_assignment.rightHandSide().accept(*this);
|
|
|
|
_assignment.leftHandSide().accept(*this);
|
|
|
|
return false;
|
2020-10-26 16:16:27 +00:00
|
|
|
}
|
|
|
|
|
2019-06-25 10:46:17 +00:00
|
|
|
void SMTEncoder::endVisit(Assignment const& _assignment)
|
2017-07-11 11:26:43 +00:00
|
|
|
{
|
2019-07-01 14:25:33 +00:00
|
|
|
createExpr(_assignment);
|
|
|
|
|
2019-03-28 11:43:20 +00:00
|
|
|
Token op = _assignment.assignmentOperator();
|
2020-09-22 09:15:56 +00:00
|
|
|
solAssert(TokenTraits::isAssignmentOp(op), "");
|
2019-08-02 17:46:06 +00:00
|
|
|
|
2020-09-22 09:15:56 +00:00
|
|
|
if (!smt::isSupportedType(*_assignment.annotation().type))
|
2019-05-08 12:05:23 +00:00
|
|
|
{
|
|
|
|
// Give it a new index anyway to keep the SSA scheme sound.
|
2020-05-28 09:26:32 +00:00
|
|
|
|
|
|
|
Expression const* base = &_assignment.leftHandSide();
|
|
|
|
if (auto const* indexAccess = dynamic_cast<IndexAccess const*>(base))
|
|
|
|
base = leftmostBase(*indexAccess);
|
|
|
|
|
|
|
|
if (auto varDecl = identifierToVariable(*base))
|
2019-05-10 14:28:29 +00:00
|
|
|
m_context.newValue(*varDecl);
|
2019-05-08 12:05:23 +00:00
|
|
|
}
|
2019-04-29 09:39:24 +00:00
|
|
|
else
|
2018-11-09 16:06:30 +00:00
|
|
|
{
|
2020-05-27 17:24:48 +00:00
|
|
|
if (dynamic_cast<TupleType const*>(_assignment.rightHandSide().annotation().type))
|
|
|
|
tupleAssignment(_assignment.leftHandSide(), _assignment.rightHandSide());
|
2019-04-29 11:02:27 +00:00
|
|
|
else
|
|
|
|
{
|
2020-05-27 17:24:48 +00:00
|
|
|
auto const& type = _assignment.annotation().type;
|
2020-09-22 09:15:56 +00:00
|
|
|
auto rightHandSide = op == Token::Assign ?
|
|
|
|
expr(_assignment.rightHandSide(), type) :
|
|
|
|
compoundAssignment(_assignment);
|
2019-04-29 11:02:27 +00:00
|
|
|
defineExpr(_assignment, rightHandSide);
|
2020-05-27 17:24:48 +00:00
|
|
|
assignment(
|
|
|
|
_assignment.leftHandSide(),
|
|
|
|
expr(_assignment, type),
|
2020-08-25 17:28:31 +00:00
|
|
|
type
|
2020-05-27 17:24:48 +00:00
|
|
|
);
|
2019-04-29 11:02:27 +00:00
|
|
|
}
|
2019-04-29 09:39:24 +00:00
|
|
|
}
|
2017-07-11 11:26:43 +00:00
|
|
|
}
|
|
|
|
|
2019-06-25 10:46:17 +00:00
|
|
|
void SMTEncoder::endVisit(TupleExpression const& _tuple)
|
2017-07-11 11:26:43 +00:00
|
|
|
{
|
2021-03-09 19:00:51 +00:00
|
|
|
if (_tuple.annotation().type->category() == Type::Category::Function)
|
|
|
|
return;
|
|
|
|
|
2019-07-01 14:25:33 +00:00
|
|
|
createExpr(_tuple);
|
|
|
|
|
2019-04-26 12:57:29 +00:00
|
|
|
if (_tuple.isInlineArray())
|
2020-10-07 11:28:35 +00:00
|
|
|
{
|
|
|
|
// Add constraints for the length and values as it is known.
|
|
|
|
auto symbArray = dynamic_pointer_cast<smt::SymbolicArrayVariable>(m_context.expression(_tuple));
|
|
|
|
solAssert(symbArray, "");
|
|
|
|
|
|
|
|
addArrayLiteralAssertions(*symbArray, applyMap(_tuple.components(), [&](auto const& c) { return expr(*c); }));
|
|
|
|
}
|
2020-08-31 14:45:52 +00:00
|
|
|
else
|
2019-04-26 12:57:29 +00:00
|
|
|
{
|
2021-03-16 12:11:24 +00:00
|
|
|
auto values = applyMap(_tuple.components(), [this](auto const& component) -> optional<smtutil::Expression> {
|
|
|
|
if (component)
|
2019-11-15 13:48:11 +00:00
|
|
|
{
|
2021-04-07 16:53:56 +00:00
|
|
|
if (!m_context.knownExpression(*component))
|
2021-03-16 12:11:24 +00:00
|
|
|
createExpr(*component);
|
2021-04-07 16:53:56 +00:00
|
|
|
return expr(*component);
|
2019-11-15 13:48:11 +00:00
|
|
|
}
|
2021-03-16 12:11:24 +00:00
|
|
|
return {};
|
|
|
|
});
|
|
|
|
defineExpr(_tuple, values);
|
2019-04-26 12:57:29 +00:00
|
|
|
}
|
2017-10-05 13:23:25 +00:00
|
|
|
}
|
|
|
|
|
2019-06-25 10:46:17 +00:00
|
|
|
void SMTEncoder::endVisit(UnaryOperation const& _op)
|
2017-10-05 13:23:25 +00:00
|
|
|
{
|
2020-09-01 09:35:25 +00:00
|
|
|
/// We need to shortcut here due to potentially unknown
|
|
|
|
/// rational number sizes.
|
2019-03-11 10:56:08 +00:00
|
|
|
if (_op.annotation().type->category() == Type::Category::RationalNumber)
|
|
|
|
return;
|
|
|
|
|
2020-09-01 09:35:25 +00:00
|
|
|
if (TokenTraits::isBitOp(_op.getOperator()))
|
|
|
|
return bitwiseNotOperation(_op);
|
|
|
|
|
2019-07-01 14:25:33 +00:00
|
|
|
createExpr(_op);
|
|
|
|
|
2020-08-31 10:59:11 +00:00
|
|
|
auto const* subExpr = innermostTuple(_op.subExpression());
|
2020-08-27 13:16:02 +00:00
|
|
|
auto type = _op.annotation().type;
|
2017-10-05 13:23:25 +00:00
|
|
|
switch (_op.getOperator())
|
|
|
|
{
|
|
|
|
case Token::Not: // !
|
|
|
|
{
|
2020-08-27 13:16:02 +00:00
|
|
|
solAssert(smt::isBool(*type), "");
|
2020-08-31 10:59:11 +00:00
|
|
|
defineExpr(_op, !expr(*subExpr));
|
2017-10-05 13:23:25 +00:00
|
|
|
break;
|
|
|
|
}
|
|
|
|
case Token::Inc: // ++ (pre- or postfix)
|
|
|
|
case Token::Dec: // -- (pre- or postfix)
|
|
|
|
{
|
2020-08-27 13:16:02 +00:00
|
|
|
solAssert(smt::isInteger(*type) || smt::isFixedPoint(*type), "");
|
2020-08-31 10:59:11 +00:00
|
|
|
solAssert(subExpr->annotation().willBeWrittenTo, "");
|
2021-03-26 09:31:58 +00:00
|
|
|
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);
|
2017-10-05 13:23:25 +00:00
|
|
|
break;
|
|
|
|
}
|
|
|
|
case Token::Sub: // -
|
|
|
|
{
|
2020-08-31 10:59:11 +00:00
|
|
|
defineExpr(_op, 0 - expr(*subExpr));
|
2017-10-05 13:23:25 +00:00
|
|
|
break;
|
|
|
|
}
|
2019-05-06 16:24:15 +00:00
|
|
|
case Token::Delete:
|
|
|
|
{
|
2020-08-31 10:59:11 +00:00
|
|
|
if (auto decl = identifierToVariable(*subExpr))
|
2019-05-06 16:24:15 +00:00
|
|
|
{
|
2019-05-10 14:28:29 +00:00
|
|
|
m_context.newValue(*decl);
|
|
|
|
m_context.setZeroValue(*decl);
|
2019-05-06 16:24:15 +00:00
|
|
|
}
|
|
|
|
else
|
|
|
|
{
|
2020-08-31 10:59:11 +00:00
|
|
|
solAssert(m_context.knownExpression(*subExpr), "");
|
|
|
|
auto const& symbVar = m_context.expression(*subExpr);
|
2019-05-06 16:24:15 +00:00
|
|
|
symbVar->increaseIndex();
|
2019-05-10 14:28:29 +00:00
|
|
|
m_context.setZeroValue(*symbVar);
|
2020-08-25 14:58:09 +00:00
|
|
|
if (
|
2020-10-26 16:16:27 +00:00
|
|
|
dynamic_cast<IndexAccess const*>(subExpr) ||
|
|
|
|
dynamic_cast<MemberAccess const*>(subExpr)
|
2020-08-25 14:58:09 +00:00
|
|
|
)
|
2020-10-26 16:16:27 +00:00
|
|
|
indexOrMemberAssignment(*subExpr, symbVar->currentValue());
|
|
|
|
// Empty push added a zero value anyway, so no need to delete extra.
|
|
|
|
else if (!isEmptyPush(*subExpr))
|
2020-08-25 17:28:31 +00:00
|
|
|
solAssert(false, "");
|
2019-05-06 16:24:15 +00:00
|
|
|
}
|
|
|
|
break;
|
|
|
|
}
|
2017-10-05 13:23:25 +00:00
|
|
|
default:
|
2020-11-05 13:25:15 +00:00
|
|
|
solAssert(false, "");
|
2017-10-05 13:23:25 +00:00
|
|
|
}
|
2017-07-11 11:26:43 +00:00
|
|
|
}
|
|
|
|
|
2019-06-25 10:46:17 +00:00
|
|
|
bool SMTEncoder::visit(UnaryOperation const& _op)
|
2019-03-11 10:56:08 +00:00
|
|
|
{
|
|
|
|
return !shortcutRationalNumber(_op);
|
|
|
|
}
|
|
|
|
|
2019-06-25 10:46:17 +00:00
|
|
|
bool SMTEncoder::visit(BinaryOperation const& _op)
|
2019-03-11 10:56:08 +00:00
|
|
|
{
|
2019-03-22 16:05:58 +00:00
|
|
|
if (shortcutRationalNumber(_op))
|
|
|
|
return false;
|
|
|
|
if (TokenTraits::isBooleanOp(_op.getOperator()))
|
|
|
|
{
|
|
|
|
booleanOperation(_op);
|
|
|
|
return false;
|
|
|
|
}
|
|
|
|
return true;
|
2019-03-11 10:56:08 +00:00
|
|
|
}
|
|
|
|
|
2019-06-25 10:46:17 +00:00
|
|
|
void SMTEncoder::endVisit(BinaryOperation const& _op)
|
2017-07-11 11:26:43 +00:00
|
|
|
{
|
2020-12-16 10:27:56 +00:00
|
|
|
/// If _op is const evaluated the RationalNumber shortcut was taken.
|
|
|
|
if (isConstant(_op))
|
2019-03-11 10:56:08 +00:00
|
|
|
return;
|
2019-03-22 16:05:58 +00:00
|
|
|
if (TokenTraits::isBooleanOp(_op.getOperator()))
|
|
|
|
return;
|
2019-03-11 10:56:08 +00:00
|
|
|
|
2019-07-01 14:25:33 +00:00
|
|
|
createExpr(_op);
|
|
|
|
|
2018-10-22 14:48:21 +00:00
|
|
|
if (TokenTraits::isArithmeticOp(_op.getOperator()))
|
2017-07-11 11:26:43 +00:00
|
|
|
arithmeticOperation(_op);
|
2018-10-22 14:48:21 +00:00
|
|
|
else if (TokenTraits::isCompareOp(_op.getOperator()))
|
2017-07-11 11:26:43 +00:00
|
|
|
compareOperation(_op);
|
2020-09-04 14:55:45 +00:00
|
|
|
else if (TokenTraits::isBitOp(_op.getOperator()) || TokenTraits::isShiftOp(_op.getOperator()))
|
2020-05-13 11:08:48 +00:00
|
|
|
bitwiseOperation(_op);
|
2017-07-11 11:26:43 +00:00
|
|
|
else
|
2020-11-05 13:25:15 +00:00
|
|
|
solAssert(false, "");
|
2017-07-11 11:26:43 +00:00
|
|
|
}
|
|
|
|
|
2020-08-18 17:25:36 +00:00
|
|
|
bool SMTEncoder::visit(Conditional const& _op)
|
|
|
|
{
|
|
|
|
_op.condition().accept(*this);
|
|
|
|
|
2020-11-14 14:42:32 +00:00
|
|
|
auto indicesEndTrue = visitBranch(&_op.trueExpression(), expr(_op.condition())).first;
|
2020-08-18 17:25:36 +00:00
|
|
|
|
2020-11-14 14:42:32 +00:00
|
|
|
auto indicesEndFalse = visitBranch(&_op.falseExpression(), !expr(_op.condition())).first;
|
2020-08-18 17:25:36 +00:00
|
|
|
|
2021-03-29 12:44:33 +00:00
|
|
|
mergeVariables(expr(_op.condition()), indicesEndTrue, indicesEndFalse);
|
2020-08-18 17:25:36 +00:00
|
|
|
|
|
|
|
defineExpr(_op, smtutil::Expression::ite(
|
|
|
|
expr(_op.condition()),
|
2020-10-21 21:04:34 +00:00
|
|
|
expr(_op.trueExpression(), _op.annotation().type),
|
|
|
|
expr(_op.falseExpression(), _op.annotation().type)
|
2020-08-18 17:25:36 +00:00
|
|
|
));
|
|
|
|
|
|
|
|
return false;
|
|
|
|
}
|
|
|
|
|
2019-06-25 10:46:17 +00:00
|
|
|
void SMTEncoder::endVisit(FunctionCall const& _funCall)
|
2017-07-11 11:26:43 +00:00
|
|
|
{
|
2020-04-08 17:38:30 +00:00
|
|
|
auto functionCallKind = *_funCall.annotation().kind;
|
|
|
|
|
2019-05-14 21:10:56 +00:00
|
|
|
createExpr(_funCall);
|
2020-04-08 17:38:30 +00:00
|
|
|
if (functionCallKind == FunctionCallKind::StructConstructorCall)
|
2017-10-04 11:18:40 +00:00
|
|
|
{
|
2020-11-12 09:09:43 +00:00
|
|
|
visitStructConstructorCall(_funCall);
|
2017-10-04 11:18:40 +00:00
|
|
|
return;
|
|
|
|
}
|
|
|
|
|
2020-04-08 17:38:30 +00:00
|
|
|
if (functionCallKind == FunctionCallKind::TypeConversion)
|
2018-12-20 12:20:07 +00:00
|
|
|
{
|
|
|
|
visitTypeConversion(_funCall);
|
|
|
|
return;
|
|
|
|
}
|
|
|
|
|
2017-07-11 11:26:43 +00:00
|
|
|
FunctionType const& funType = dynamic_cast<FunctionType const&>(*_funCall.expression().annotation().type);
|
|
|
|
|
|
|
|
std::vector<ASTPointer<Expression const>> const args = _funCall.arguments();
|
2018-12-10 16:23:36 +00:00
|
|
|
switch (funType.kind())
|
|
|
|
{
|
|
|
|
case FunctionType::Kind::Assert:
|
2018-10-10 12:31:49 +00:00
|
|
|
visitAssert(_funCall);
|
2018-12-10 16:23:36 +00:00
|
|
|
break;
|
|
|
|
case FunctionType::Kind::Require:
|
2018-10-10 12:31:49 +00:00
|
|
|
visitRequire(_funCall);
|
2018-12-10 16:23:36 +00:00
|
|
|
break;
|
2020-09-11 19:49:04 +00:00
|
|
|
case FunctionType::Kind::Revert:
|
|
|
|
// Revert is a special case of require and equals to `require(false)`
|
|
|
|
addPathImpliedExpression(smtutil::Expression(false));
|
|
|
|
break;
|
2018-12-10 16:23:36 +00:00
|
|
|
case FunctionType::Kind::GasLeft:
|
2018-10-18 13:03:52 +00:00
|
|
|
visitGasLeft(_funCall);
|
2018-12-10 16:23:36 +00:00
|
|
|
break;
|
2018-12-20 17:11:20 +00:00
|
|
|
case FunctionType::Kind::External:
|
2020-11-26 16:14:58 +00:00
|
|
|
if (isPublicGetter(_funCall.expression()))
|
|
|
|
visitPublicGetter(_funCall);
|
|
|
|
break;
|
2020-12-08 20:14:18 +00:00
|
|
|
case FunctionType::Kind::ABIDecode:
|
|
|
|
case FunctionType::Kind::ABIEncode:
|
|
|
|
case FunctionType::Kind::ABIEncodePacked:
|
|
|
|
case FunctionType::Kind::ABIEncodeWithSelector:
|
|
|
|
case FunctionType::Kind::ABIEncodeWithSignature:
|
|
|
|
visitABIFunction(_funCall);
|
|
|
|
break;
|
2020-11-26 16:14:58 +00:00
|
|
|
case FunctionType::Kind::Internal:
|
2019-04-11 16:14:48 +00:00
|
|
|
case FunctionType::Kind::BareStaticCall:
|
2021-08-11 16:10:21 +00:00
|
|
|
case FunctionType::Kind::BareCall:
|
2018-12-20 17:11:20 +00:00
|
|
|
break;
|
2018-12-10 16:23:36 +00:00
|
|
|
case FunctionType::Kind::KECCAK256:
|
|
|
|
case FunctionType::Kind::ECRecover:
|
|
|
|
case FunctionType::Kind::SHA256:
|
|
|
|
case FunctionType::Kind::RIPEMD160:
|
2020-10-13 16:00:26 +00:00
|
|
|
visitCryptoFunction(_funCall);
|
2020-09-29 08:36:20 +00:00
|
|
|
break;
|
2018-12-10 16:23:36 +00:00
|
|
|
case FunctionType::Kind::BlockHash:
|
2021-02-03 10:31:17 +00:00
|
|
|
defineExpr(_funCall, state().blockhash(expr(*_funCall.arguments().at(0))));
|
2020-09-28 10:09:40 +00:00
|
|
|
break;
|
2018-12-10 16:23:36 +00:00
|
|
|
case FunctionType::Kind::AddMod:
|
|
|
|
case FunctionType::Kind::MulMod:
|
2020-09-28 10:09:40 +00:00
|
|
|
visitAddMulMod(_funCall);
|
2018-12-10 16:23:36 +00:00
|
|
|
break;
|
2019-04-11 16:14:48 +00:00
|
|
|
case FunctionType::Kind::Send:
|
|
|
|
case FunctionType::Kind::Transfer:
|
|
|
|
{
|
|
|
|
auto const& memberAccess = dynamic_cast<MemberAccess const&>(_funCall.expression());
|
|
|
|
auto const& address = memberAccess.expression();
|
2019-05-09 11:17:00 +00:00
|
|
|
auto const& value = args.front();
|
2019-04-11 16:14:48 +00:00
|
|
|
solAssert(value, "");
|
|
|
|
|
2021-02-03 10:31:17 +00:00
|
|
|
smtutil::Expression thisBalance = state().balance();
|
2019-07-03 14:05:56 +00:00
|
|
|
setSymbolicUnknownValue(thisBalance, TypeProvider::uint256(), m_context);
|
2019-06-24 15:37:03 +00:00
|
|
|
|
2021-02-03 10:31:17 +00:00
|
|
|
state().transfer(state().thisAddress(), expr(address), expr(*value));
|
2019-04-11 16:14:48 +00:00
|
|
|
break;
|
|
|
|
}
|
2020-05-11 22:39:00 +00:00
|
|
|
case FunctionType::Kind::ArrayPush:
|
|
|
|
arrayPush(_funCall);
|
|
|
|
break;
|
|
|
|
case FunctionType::Kind::ArrayPop:
|
|
|
|
arrayPop(_funCall);
|
|
|
|
break;
|
2020-09-12 11:22:03 +00:00
|
|
|
case FunctionType::Kind::Event:
|
2021-01-28 11:56:22 +00:00
|
|
|
case FunctionType::Kind::Error:
|
2020-10-21 16:57:10 +00:00
|
|
|
// This can be safely ignored.
|
2020-09-12 11:22:03 +00:00
|
|
|
break;
|
2020-09-25 12:00:32 +00:00
|
|
|
case FunctionType::Kind::ObjectCreation:
|
|
|
|
visitObjectCreation(_funCall);
|
|
|
|
return;
|
2020-12-08 20:14:18 +00:00
|
|
|
case FunctionType::Kind::DelegateCall:
|
|
|
|
case FunctionType::Kind::BareCallCode:
|
|
|
|
case FunctionType::Kind::BareDelegateCall:
|
|
|
|
case FunctionType::Kind::Creation:
|
2018-12-10 16:23:36 +00:00
|
|
|
default:
|
2018-10-10 12:31:49 +00:00
|
|
|
m_errorReporter.warning(
|
2020-05-05 22:38:28 +00:00
|
|
|
4588_error,
|
2018-10-10 12:31:49 +00:00
|
|
|
_funCall.location(),
|
|
|
|
"Assertion checker does not yet implement this type of function call."
|
|
|
|
);
|
|
|
|
}
|
|
|
|
}
|
|
|
|
|
2019-11-27 21:34:33 +00:00
|
|
|
bool SMTEncoder::visit(ModifierInvocation const& _node)
|
|
|
|
{
|
|
|
|
if (auto const* args = _node.arguments())
|
|
|
|
for (auto const& arg: *args)
|
|
|
|
if (arg)
|
|
|
|
arg->accept(*this);
|
|
|
|
return false;
|
|
|
|
}
|
|
|
|
|
2019-09-28 19:04:49 +00:00
|
|
|
void SMTEncoder::initContract(ContractDefinition const& _contract)
|
|
|
|
{
|
|
|
|
solAssert(m_currentContract == nullptr, "");
|
|
|
|
m_currentContract = &_contract;
|
|
|
|
|
2019-09-26 14:12:27 +00:00
|
|
|
m_context.reset();
|
|
|
|
m_context.pushSolver();
|
|
|
|
createStateVariables(_contract);
|
|
|
|
clearIndices(m_currentContract, nullptr);
|
2020-12-22 19:25:31 +00:00
|
|
|
m_variableUsage.setCurrentContract(_contract);
|
2020-12-16 17:32:34 +00:00
|
|
|
m_checked = true;
|
2019-09-28 19:04:49 +00:00
|
|
|
}
|
|
|
|
|
2019-06-25 10:46:17 +00:00
|
|
|
void SMTEncoder::initFunction(FunctionDefinition const& _function)
|
|
|
|
{
|
|
|
|
solAssert(m_callStack.empty(), "");
|
2019-09-26 14:12:27 +00:00
|
|
|
solAssert(m_currentContract, "");
|
2019-06-25 10:46:17 +00:00
|
|
|
m_context.pushSolver();
|
|
|
|
m_pathConditions.clear();
|
|
|
|
pushCallStack({&_function, nullptr});
|
|
|
|
m_uninterpretedTerms.clear();
|
2019-09-26 14:12:27 +00:00
|
|
|
createStateVariables(*m_currentContract);
|
|
|
|
createLocalVariables(_function);
|
2019-06-25 10:46:17 +00:00
|
|
|
m_arrayAssignmentHappened = false;
|
2019-09-26 14:12:27 +00:00
|
|
|
clearIndices(m_currentContract, &_function);
|
2020-12-16 17:32:34 +00:00
|
|
|
m_checked = true;
|
2019-06-25 10:46:17 +00:00
|
|
|
}
|
|
|
|
|
|
|
|
void SMTEncoder::visitAssert(FunctionCall const& _funCall)
|
2018-10-10 12:31:49 +00:00
|
|
|
{
|
|
|
|
auto const& args = _funCall.arguments();
|
|
|
|
solAssert(args.size() == 1, "");
|
2019-07-01 14:11:29 +00:00
|
|
|
solAssert(args.front()->annotation().type->category() == Type::Category::Bool, "");
|
2018-10-10 12:31:49 +00:00
|
|
|
}
|
|
|
|
|
2019-06-25 10:46:17 +00:00
|
|
|
void SMTEncoder::visitRequire(FunctionCall const& _funCall)
|
2018-10-10 12:31:49 +00:00
|
|
|
{
|
|
|
|
auto const& args = _funCall.arguments();
|
2019-07-01 14:11:29 +00:00
|
|
|
solAssert(args.size() >= 1, "");
|
|
|
|
solAssert(args.front()->annotation().type->category() == Type::Category::Bool, "");
|
|
|
|
addPathImpliedExpression(expr(*args.front()));
|
2018-10-10 12:31:49 +00:00
|
|
|
}
|
|
|
|
|
2020-12-08 20:14:18 +00:00
|
|
|
void SMTEncoder::visitABIFunction(FunctionCall const& _funCall)
|
|
|
|
{
|
2021-02-03 10:31:17 +00:00
|
|
|
auto symbFunction = state().abiFunction(&_funCall);
|
|
|
|
auto const& [name, inTypes, outTypes] = state().abiFunctionTypes(&_funCall);
|
2020-12-08 20:14:18 +00:00
|
|
|
|
|
|
|
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, "");
|
2021-03-25 11:24:37 +00:00
|
|
|
if (argsActualLength == 0)
|
|
|
|
{
|
|
|
|
defineExpr(_funCall, smt::zeroValue(TypeProvider::bytesMemory()));
|
|
|
|
return;
|
|
|
|
}
|
|
|
|
vector<smtutil::Expression> symbArgs;
|
2020-12-08 20:14:18 +00:00
|
|
|
for (unsigned i = 0; i < argsActualLength; ++i)
|
|
|
|
if (args.at(i))
|
|
|
|
symbArgs.emplace_back(expr(*args.at(i), inTypes.at(i)));
|
|
|
|
|
|
|
|
optional<smtutil::Expression> arg;
|
|
|
|
if (inTypes.size() == 1)
|
2021-01-14 12:54:52 +00:00
|
|
|
arg = expr(*args.at(0), inTypes.at(0));
|
2020-12-08 20:14:18 +00:00
|
|
|
else
|
|
|
|
{
|
|
|
|
auto inputSort = dynamic_cast<smtutil::ArraySort&>(*symbFunction.sort).domain;
|
|
|
|
arg = smtutil::Expression::tuple_constructor(
|
|
|
|
smtutil::Expression(make_shared<smtutil::SortSort>(inputSort), ""),
|
|
|
|
symbArgs
|
|
|
|
);
|
|
|
|
}
|
|
|
|
|
|
|
|
auto out = smtutil::Expression::select(symbFunction, *arg);
|
|
|
|
if (outTypes.size() == 1)
|
|
|
|
defineExpr(_funCall, out);
|
|
|
|
else
|
|
|
|
{
|
|
|
|
auto symbTuple = 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));
|
|
|
|
}
|
|
|
|
}
|
|
|
|
|
2020-10-13 16:00:26 +00:00
|
|
|
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));
|
|
|
|
optional<smtutil::Expression> result;
|
|
|
|
if (kind == FunctionType::Kind::KECCAK256)
|
2021-02-03 10:31:17 +00:00
|
|
|
result = smtutil::Expression::select(state().cryptoFunction("keccak256"), arg0);
|
2020-10-13 16:00:26 +00:00
|
|
|
else if (kind == FunctionType::Kind::SHA256)
|
2021-02-03 10:31:17 +00:00
|
|
|
result = smtutil::Expression::select(state().cryptoFunction("sha256"), arg0);
|
2020-10-13 16:00:26 +00:00
|
|
|
else if (kind == FunctionType::Kind::RIPEMD160)
|
2021-02-03 10:31:17 +00:00
|
|
|
result = smtutil::Expression::select(state().cryptoFunction("ripemd160"), arg0);
|
2020-10-13 16:00:26 +00:00
|
|
|
else if (kind == FunctionType::Kind::ECRecover)
|
|
|
|
{
|
2021-02-03 10:31:17 +00:00
|
|
|
auto e = state().cryptoFunction("ecrecover");
|
2020-10-13 16:00:26 +00:00
|
|
|
auto arg0 = expr(*_funCall.arguments().at(0));
|
|
|
|
auto arg1 = expr(*_funCall.arguments().at(1));
|
|
|
|
auto arg2 = expr(*_funCall.arguments().at(2));
|
|
|
|
auto arg3 = expr(*_funCall.arguments().at(3));
|
|
|
|
auto inputSort = dynamic_cast<smtutil::ArraySort&>(*e.sort).domain;
|
|
|
|
auto ecrecoverInput = smtutil::Expression::tuple_constructor(
|
|
|
|
smtutil::Expression(make_shared<smtutil::SortSort>(inputSort), ""),
|
|
|
|
{arg0, arg1, arg2, arg3}
|
|
|
|
);
|
|
|
|
result = smtutil::Expression::select(e, ecrecoverInput);
|
|
|
|
}
|
|
|
|
else
|
|
|
|
solAssert(false, "");
|
|
|
|
|
|
|
|
defineExpr(_funCall, *result);
|
|
|
|
}
|
|
|
|
|
2019-06-25 10:46:17 +00:00
|
|
|
void SMTEncoder::visitGasLeft(FunctionCall const& _funCall)
|
2018-10-18 13:03:52 +00:00
|
|
|
{
|
2021-05-18 20:23:36 +00:00
|
|
|
string gasLeft = "gasleft";
|
2018-10-18 13:03:52 +00:00
|
|
|
// We increase the variable index since gasleft changes
|
|
|
|
// inside a tx.
|
2018-12-10 16:23:36 +00:00
|
|
|
defineGlobalVariable(gasLeft, _funCall, true);
|
2019-05-14 16:57:34 +00:00
|
|
|
auto const& symbolicVar = m_context.globalSymbol(gasLeft);
|
2018-10-22 16:19:11 +00:00
|
|
|
unsigned index = symbolicVar->index();
|
|
|
|
// We set the current value to unknown anyway to add type constraints.
|
2019-05-10 14:28:29 +00:00
|
|
|
m_context.setUnknownValue(*symbolicVar);
|
2018-10-22 16:19:11 +00:00
|
|
|
if (index > 0)
|
2019-06-24 15:37:03 +00:00
|
|
|
m_context.addAssertion(symbolicVar->currentValue() <= symbolicVar->valueAtIndex(index - 1));
|
2018-10-18 13:03:52 +00:00
|
|
|
}
|
|
|
|
|
2020-09-28 10:09:40 +00:00
|
|
|
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));
|
2020-10-14 14:26:50 +00:00
|
|
|
auto const& intType = dynamic_cast<IntegerType const&>(*_funCall.annotation().type);
|
2020-09-28 10:09:40 +00:00
|
|
|
|
|
|
|
if (kind == FunctionType::Kind::AddMod)
|
2020-10-14 14:26:50 +00:00
|
|
|
defineExpr(_funCall, divModWithSlacks(x + y, k, intType).second);
|
2020-09-28 10:09:40 +00:00
|
|
|
else
|
2020-10-14 14:26:50 +00:00
|
|
|
defineExpr(_funCall, divModWithSlacks(x * y, k, intType).second);
|
2020-09-28 10:09:40 +00:00
|
|
|
}
|
|
|
|
|
2020-09-25 12:00:32 +00:00
|
|
|
void SMTEncoder::visitObjectCreation(FunctionCall const& _funCall)
|
|
|
|
{
|
|
|
|
auto const& args = _funCall.arguments();
|
|
|
|
solAssert(args.size() >= 1, "");
|
|
|
|
auto argType = args.front()->annotation().type->category();
|
|
|
|
solAssert(argType == Type::Category::Integer || argType == Type::Category::RationalNumber, "");
|
|
|
|
|
|
|
|
smtutil::Expression arraySize = expr(*args.front());
|
|
|
|
setSymbolicUnknownValue(arraySize, TypeProvider::uint256(), m_context);
|
|
|
|
|
|
|
|
auto symbArray = dynamic_pointer_cast<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);
|
|
|
|
}
|
|
|
|
|
2019-06-25 10:46:17 +00:00
|
|
|
void SMTEncoder::endVisit(Identifier const& _identifier)
|
2017-07-11 11:26:43 +00:00
|
|
|
{
|
2020-07-15 16:56:28 +00:00
|
|
|
if (auto decl = identifierToVariable(_identifier))
|
2020-12-18 12:39:43 +00:00
|
|
|
{
|
|
|
|
if (decl->isConstant())
|
|
|
|
{
|
|
|
|
if (RationalNumberType const* rationalType = isConstant(_identifier))
|
|
|
|
{
|
|
|
|
if (rationalType->isNegative())
|
|
|
|
defineExpr(_identifier, smtutil::Expression(u2s(rationalType->literalValue(nullptr))));
|
|
|
|
else
|
|
|
|
defineExpr(_identifier, smtutil::Expression(rationalType->literalValue(nullptr)));
|
|
|
|
}
|
|
|
|
else
|
|
|
|
{
|
|
|
|
solAssert(decl->value(), "");
|
|
|
|
decl->value()->accept(*this);
|
2021-03-03 15:48:32 +00:00
|
|
|
defineExpr(_identifier, expr(*decl->value(), _identifier.annotation().type));
|
2020-12-18 12:39:43 +00:00
|
|
|
}
|
|
|
|
}
|
|
|
|
else
|
|
|
|
defineExpr(_identifier, currentValue(*decl));
|
|
|
|
}
|
2019-11-10 17:58:29 +00:00
|
|
|
else if (_identifier.annotation().type->category() == Type::Category::Function)
|
|
|
|
visitFunctionIdentifier(_identifier);
|
2019-07-01 14:25:33 +00:00
|
|
|
else if (_identifier.name() == "now")
|
|
|
|
defineGlobalVariable(_identifier.name(), _identifier);
|
|
|
|
else if (_identifier.name() == "this")
|
2018-06-12 08:58:24 +00:00
|
|
|
{
|
2021-02-03 10:31:17 +00:00
|
|
|
defineExpr(_identifier, state().thisAddress());
|
2019-07-01 14:25:33 +00:00
|
|
|
m_uninterpretedTerms.insert(&_identifier);
|
2018-06-12 08:58:24 +00:00
|
|
|
}
|
2020-11-23 14:41:57 +00:00
|
|
|
// Ignore type identifiers
|
|
|
|
else if (dynamic_cast<TypeType const*>(_identifier.annotation().type))
|
2020-11-12 09:09:43 +00:00
|
|
|
return;
|
2020-09-24 09:32:56 +00:00
|
|
|
// 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;
|
|
|
|
}
|
2019-11-27 21:34:33 +00:00
|
|
|
else
|
2019-11-15 13:48:11 +00:00
|
|
|
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);
|
2017-07-11 11:26:43 +00:00
|
|
|
}
|
|
|
|
|
2020-11-26 16:14:58 +00:00
|
|
|
namespace // helpers for SMTEncoder::visitPublicGetter
|
|
|
|
{
|
|
|
|
|
2021-03-22 16:12:05 +00:00
|
|
|
bool isReturnedFromStructGetter(Type const* _type)
|
2020-11-26 16:14:58 +00:00
|
|
|
{
|
|
|
|
// 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).isByteArray();
|
|
|
|
// default
|
|
|
|
return true;
|
|
|
|
}
|
|
|
|
|
|
|
|
vector<string> structGetterReturnedMembers(StructType const& _structType)
|
|
|
|
{
|
|
|
|
vector<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)
|
|
|
|
{
|
|
|
|
MemberAccess const& access = dynamic_cast<MemberAccess const&>(_funCall.expression());
|
|
|
|
auto var = dynamic_cast<VariableDeclaration const*>(access.annotation().referencedDeclaration);
|
|
|
|
solAssert(var, "");
|
|
|
|
solAssert(m_context.knownExpression(_funCall), "");
|
|
|
|
auto paramExpectedTypes = FunctionType(*var).parameterTypes();
|
|
|
|
auto actualArguments = _funCall.arguments();
|
|
|
|
solAssert(actualArguments.size() == paramExpectedTypes.size(), "");
|
2021-03-04 13:23:41 +00:00
|
|
|
deque<smtutil::Expression> symbArguments;
|
2020-11-26 16:14:58 +00:00
|
|
|
for (unsigned i = 0; i < paramExpectedTypes.size(); ++i)
|
|
|
|
symbArguments.push_back(expr(*actualArguments[i], paramExpectedTypes[i]));
|
|
|
|
|
2021-03-04 13:23:41 +00:00
|
|
|
// See FunctionType::FunctionType(VariableDeclaration const& _varDecl)
|
|
|
|
// to understand the return types of public getters.
|
2021-03-22 16:12:05 +00:00
|
|
|
Type const* type = var->type();
|
2021-03-04 13:23:41 +00:00
|
|
|
smtutil::Expression currentExpr = currentValue(*var);
|
|
|
|
while (true)
|
2020-11-26 16:14:58 +00:00
|
|
|
{
|
2021-03-04 13:23:41 +00:00
|
|
|
if (
|
|
|
|
type->isValueType() ||
|
|
|
|
(type->category() == Type::Category::Array && dynamic_cast<ArrayType const&>(*type).isByteArray())
|
|
|
|
)
|
2020-11-26 16:14:58 +00:00
|
|
|
{
|
2021-03-04 13:23:41 +00:00
|
|
|
solAssert(symbArguments.empty(), "");
|
|
|
|
defineExpr(_funCall, currentExpr);
|
|
|
|
return;
|
2020-11-26 16:14:58 +00:00
|
|
|
}
|
2021-03-04 13:23:41 +00:00
|
|
|
switch (type->category())
|
2020-11-26 16:14:58 +00:00
|
|
|
{
|
2021-03-04 13:23:41 +00:00
|
|
|
case Type::Category::Array:
|
|
|
|
case Type::Category::Mapping:
|
2020-11-26 16:14:58 +00:00
|
|
|
{
|
2021-03-04 13:23:41 +00:00
|
|
|
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_" + to_string(_funCall.id()), m_context);
|
|
|
|
m_context.addAssertion(structVar.currentValue() == currentExpr);
|
|
|
|
auto returnedMembers = structGetterReturnedMembers(dynamic_cast<StructType const&>(*structVar.type()));
|
|
|
|
solAssert(!returnedMembers.empty(), "");
|
2021-03-16 12:11:24 +00:00
|
|
|
auto returnedValues = applyMap(returnedMembers, [&](string const& memberName) -> optional<smtutil::Expression> { return structVar.member(memberName); });
|
|
|
|
defineExpr(_funCall, returnedValues);
|
2021-03-04 13:23:41 +00:00
|
|
|
return;
|
|
|
|
}
|
|
|
|
default:
|
|
|
|
{
|
|
|
|
// Unsupported cases, do nothing and the getter will be abstracted.
|
|
|
|
return;
|
2020-11-26 16:14:58 +00:00
|
|
|
}
|
|
|
|
}
|
|
|
|
}
|
|
|
|
}
|
|
|
|
|
2021-04-15 10:31:45 +00:00
|
|
|
bool SMTEncoder::shouldAnalyze(ContractDefinition const& _contract) const
|
|
|
|
{
|
|
|
|
if (!_contract.canBeDeployed())
|
|
|
|
return false;
|
|
|
|
|
|
|
|
return m_settings.contracts.isDefault() ||
|
|
|
|
m_settings.contracts.has(_contract.sourceUnitName(), _contract.name());
|
|
|
|
}
|
|
|
|
|
2019-06-25 10:46:17 +00:00
|
|
|
void SMTEncoder::visitTypeConversion(FunctionCall const& _funCall)
|
2018-12-20 12:20:07 +00:00
|
|
|
{
|
2020-04-08 17:38:30 +00:00
|
|
|
solAssert(*_funCall.annotation().kind == FunctionCallKind::TypeConversion, "");
|
2018-12-20 12:20:07 +00:00
|
|
|
solAssert(_funCall.arguments().size() == 1, "");
|
2020-09-14 19:22:50 +00:00
|
|
|
|
2019-05-09 11:17:00 +00:00
|
|
|
auto argument = _funCall.arguments().front();
|
2020-12-03 17:22:45 +00:00
|
|
|
auto const argType = argument->annotation().type;
|
|
|
|
auto const funCallType = _funCall.annotation().type;
|
2020-09-14 19:22:50 +00:00
|
|
|
|
2020-12-03 17:22:45 +00:00
|
|
|
auto symbArg = expr(*argument, funCallType);
|
2020-09-14 19:22:50 +00:00
|
|
|
|
2020-12-03 17:22:45 +00:00
|
|
|
if (smt::isStringLiteral(*argType) && smt::isFixedBytes(*funCallType))
|
|
|
|
{
|
|
|
|
defineExpr(_funCall, symbArg);
|
|
|
|
return;
|
|
|
|
}
|
2020-09-14 19:22:50 +00:00
|
|
|
|
2021-06-01 15:28:41 +00:00
|
|
|
ArrayType const* arrayType = dynamic_cast<ArrayType const*>(argType);
|
|
|
|
if (auto sliceType = dynamic_cast<ArraySliceType const*>(argType))
|
|
|
|
arrayType = &sliceType->arrayType();
|
|
|
|
|
|
|
|
if (arrayType && arrayType->isByteArray() && smt::isFixedBytes(*funCallType))
|
|
|
|
{
|
|
|
|
auto array = dynamic_pointer_cast<smt::SymbolicArrayVariable>(m_context.expression(*argument));
|
|
|
|
bytesToFixedBytesAssertions(*array, _funCall);
|
|
|
|
return;
|
|
|
|
}
|
|
|
|
|
2020-09-14 19:22:50 +00:00
|
|
|
// TODO Simplify this whole thing for 0.8.0 where weird casts are disallowed.
|
|
|
|
|
2020-12-03 17:22:45 +00:00
|
|
|
unsigned argSize = argType->storageBytes();
|
|
|
|
unsigned castSize = funCallType->storageBytes();
|
2020-09-14 19:22:50 +00:00
|
|
|
bool castIsSigned = smt::isNumber(*funCallType) && smt::isSigned(funCallType);
|
|
|
|
bool argIsSigned = smt::isNumber(*argType) && smt::isSigned(argType);
|
|
|
|
optional<smtutil::Expression> symbMin;
|
|
|
|
optional<smtutil::Expression> symbMax;
|
|
|
|
if (smt::isNumber(*funCallType))
|
|
|
|
{
|
|
|
|
symbMin = smt::minValue(funCallType);
|
|
|
|
symbMax = smt::maxValue(funCallType);
|
|
|
|
}
|
|
|
|
if (argSize == castSize)
|
2018-12-20 12:20:07 +00:00
|
|
|
{
|
2020-09-14 19:22:50 +00:00
|
|
|
// If sizes are the same, it's possible that the signs are different.
|
2020-10-19 20:46:15 +00:00
|
|
|
if (smt::isNumber(*funCallType) && smt::isNumber(*argType))
|
2018-12-20 12:20:07 +00:00
|
|
|
{
|
2020-09-14 19:22:50 +00:00
|
|
|
// 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);
|
|
|
|
}
|
2018-12-20 12:20:07 +00:00
|
|
|
else
|
2020-09-14 19:22:50 +00:00
|
|
|
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))
|
2018-12-20 12:20:07 +00:00
|
|
|
{
|
2020-09-14 19:22:50 +00:00
|
|
|
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))
|
|
|
|
);
|
2018-12-20 12:20:07 +00:00
|
|
|
}
|
2020-09-14 19:22:50 +00:00
|
|
|
else
|
|
|
|
defineExpr(_funCall, symbArg);
|
2018-12-20 12:20:07 +00:00
|
|
|
}
|
2020-09-14 19:22:50 +00:00
|
|
|
else
|
|
|
|
defineExpr(_funCall, symbArg);
|
|
|
|
}
|
|
|
|
else // castSize < argSize
|
|
|
|
{
|
|
|
|
solAssert(smt::isNumber(*funCallType), "");
|
2018-12-20 12:20:07 +00:00
|
|
|
|
2021-05-11 12:07:02 +00:00
|
|
|
RationalNumberType const* rationalType = isConstant(*argument);
|
|
|
|
if (rationalType)
|
|
|
|
{
|
|
|
|
// The TypeChecker guarantees that a constant fits in the cast size.
|
|
|
|
defineExpr(_funCall, symbArg);
|
|
|
|
return;
|
|
|
|
}
|
|
|
|
|
2020-09-14 19:22:50 +00:00
|
|
|
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));
|
|
|
|
}
|
2018-12-20 12:20:07 +00:00
|
|
|
}
|
|
|
|
}
|
|
|
|
|
2019-06-25 10:46:17 +00:00
|
|
|
void SMTEncoder::visitFunctionIdentifier(Identifier const& _identifier)
|
2018-12-10 16:23:36 +00:00
|
|
|
{
|
|
|
|
auto const& fType = dynamic_cast<FunctionType const&>(*_identifier.annotation().type);
|
2019-04-30 06:58:08 +00:00
|
|
|
if (fType.returnParameterTypes().size() == 1)
|
2018-12-10 16:23:36 +00:00
|
|
|
{
|
2019-09-18 20:19:35 +00:00
|
|
|
defineGlobalVariable(fType.identifier(), _identifier);
|
|
|
|
m_context.createExpression(_identifier, m_context.globalSymbol(fType.identifier()));
|
2018-12-10 16:23:36 +00:00
|
|
|
}
|
|
|
|
}
|
|
|
|
|
2020-11-12 09:09:43 +00:00
|
|
|
void SMTEncoder::visitStructConstructorCall(FunctionCall const& _funCall)
|
|
|
|
{
|
|
|
|
solAssert(*_funCall.annotation().kind == FunctionCallKind::StructConstructorCall, "");
|
2020-12-15 08:15:59 +00:00
|
|
|
if (smt::isNonRecursiveStruct(*_funCall.annotation().type))
|
|
|
|
{
|
|
|
|
auto& structSymbolicVar = dynamic_cast<smt::SymbolicStructVariable&>(*m_context.expression(_funCall));
|
2021-05-16 10:56:33 +00:00
|
|
|
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()); }
|
|
|
|
));
|
2020-12-15 08:15:59 +00:00
|
|
|
}
|
|
|
|
|
2020-11-12 09:09:43 +00:00
|
|
|
}
|
|
|
|
|
2019-06-25 10:46:17 +00:00
|
|
|
void SMTEncoder::endVisit(Literal const& _literal)
|
2017-07-11 11:26:43 +00:00
|
|
|
{
|
2019-02-27 10:55:59 +00:00
|
|
|
solAssert(_literal.annotation().type, "Expected type for AST node");
|
2017-07-11 11:26:43 +00:00
|
|
|
Type const& type = *_literal.annotation().type;
|
2020-08-27 13:16:02 +00:00
|
|
|
if (smt::isNumber(type))
|
2020-05-19 12:14:46 +00:00
|
|
|
defineExpr(_literal, smtutil::Expression(type.literalValue(&_literal)));
|
2020-08-27 13:16:02 +00:00
|
|
|
else if (smt::isBool(type))
|
2020-05-19 12:14:46 +00:00
|
|
|
defineExpr(_literal, smtutil::Expression(_literal.token() == Token::TrueLiteral ? true : false));
|
2020-08-27 13:16:02 +00:00
|
|
|
else if (smt::isStringLiteral(type))
|
2020-09-24 11:16:38 +00:00
|
|
|
{
|
2019-08-07 08:48:09 +00:00
|
|
|
createExpr(_literal);
|
2020-09-24 11:16:38 +00:00
|
|
|
|
|
|
|
// Add constraints for the length and values as it is known.
|
|
|
|
auto symbArray = dynamic_pointer_cast<smt::SymbolicArrayVariable>(m_context.expression(_literal));
|
|
|
|
solAssert(symbArray, "");
|
|
|
|
|
2020-10-07 11:28:35 +00:00
|
|
|
addArrayLiteralAssertions(
|
|
|
|
*symbArray,
|
2020-12-03 17:22:45 +00:00
|
|
|
applyMap(_literal.value(), [](unsigned char c) { return smtutil::Expression{size_t(c)}; })
|
2020-10-07 11:28:35 +00:00
|
|
|
);
|
2020-09-24 11:16:38 +00:00
|
|
|
}
|
2017-07-11 11:26:43 +00:00
|
|
|
else
|
2020-11-05 13:25:15 +00:00
|
|
|
solAssert(false, "");
|
2017-07-11 11:26:43 +00:00
|
|
|
}
|
|
|
|
|
2020-10-07 11:28:35 +00:00
|
|
|
void SMTEncoder::addArrayLiteralAssertions(
|
|
|
|
smt::SymbolicArrayVariable& _symArray,
|
|
|
|
vector<smtutil::Expression> const& _elementValues
|
|
|
|
)
|
|
|
|
{
|
|
|
|
m_context.addAssertion(_symArray.length() == _elementValues.size());
|
|
|
|
for (size_t i = 0; i < _elementValues.size(); i++)
|
|
|
|
m_context.addAssertion(smtutil::Expression::select(_symArray.elements(), i) == _elementValues[i]);
|
|
|
|
}
|
|
|
|
|
2021-06-01 15:28:41 +00:00
|
|
|
void SMTEncoder::bytesToFixedBytesAssertions(
|
|
|
|
smt::SymbolicArrayVariable& _symArray,
|
|
|
|
Expression const& _fixedBytes
|
|
|
|
)
|
|
|
|
{
|
|
|
|
auto const& fixed = dynamic_cast<FixedBytesType const&>(*_fixedBytes.annotation().type);
|
|
|
|
auto intType = TypeProvider::uint256();
|
|
|
|
string suffix = to_string(_fixedBytes.id()) + "_" + to_string(m_context.newUniqueId());
|
|
|
|
smt::SymbolicIntVariable k(intType, intType, "k_" + suffix, m_context);
|
|
|
|
m_context.addAssertion(k.currentValue() == 0);
|
|
|
|
size_t n = fixed.numBytes();
|
|
|
|
for (size_t i = 0; i < n; i++)
|
|
|
|
{
|
|
|
|
auto kPrev = k.currentValue();
|
|
|
|
m_context.addAssertion((smtutil::Expression::select(_symArray.elements(), i) * (u256(1) << ((n - i - 1) * 8))) + kPrev == k.increaseIndex());
|
|
|
|
}
|
|
|
|
m_context.addAssertion(expr(_fixedBytes) == k.currentValue());
|
|
|
|
}
|
|
|
|
|
2019-06-25 10:46:17 +00:00
|
|
|
void SMTEncoder::endVisit(Return const& _return)
|
2018-10-10 12:31:49 +00:00
|
|
|
{
|
2019-05-13 14:53:38 +00:00
|
|
|
if (_return.expression() && m_context.knownExpression(*_return.expression()))
|
2018-10-10 12:31:49 +00:00
|
|
|
{
|
2019-05-06 18:03:11 +00:00
|
|
|
auto returnParams = m_callStack.back().first->returnParameters();
|
2018-10-10 12:31:49 +00:00
|
|
|
if (returnParams.size() > 1)
|
2019-04-30 06:58:08 +00:00
|
|
|
{
|
2019-08-02 18:43:54 +00:00
|
|
|
auto const& symbTuple = dynamic_pointer_cast<smt::SymbolicTupleVariable>(m_context.expression(*_return.expression()));
|
|
|
|
solAssert(symbTuple, "");
|
2020-04-03 13:10:16 +00:00
|
|
|
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(), "");
|
|
|
|
|
2019-04-30 06:58:08 +00:00
|
|
|
for (unsigned i = 0; i < returnParams.size(); ++i)
|
2020-11-19 16:11:02 +00:00
|
|
|
assignment(*returnParams.at(i), symbTuple->component(i, types.at(i), returnParams.at(i)->type()));
|
2019-04-30 06:58:08 +00:00
|
|
|
}
|
2018-10-10 12:31:49 +00:00
|
|
|
else if (returnParams.size() == 1)
|
2020-11-19 16:11:02 +00:00
|
|
|
assignment(*returnParams.front(), expr(*_return.expression(), returnParams.front()->type()));
|
2018-10-10 12:31:49 +00:00
|
|
|
}
|
|
|
|
}
|
|
|
|
|
2019-06-25 10:46:17 +00:00
|
|
|
bool SMTEncoder::visit(MemberAccess const& _memberAccess)
|
2018-10-18 13:03:52 +00:00
|
|
|
{
|
2018-10-25 15:50:31 +00:00
|
|
|
auto const& accessType = _memberAccess.annotation().type;
|
|
|
|
if (accessType->category() == Type::Category::Function)
|
|
|
|
return true;
|
|
|
|
|
2019-07-01 14:25:33 +00:00
|
|
|
createExpr(_memberAccess);
|
|
|
|
|
2018-10-18 13:03:52 +00:00
|
|
|
auto const& exprType = _memberAccess.expression().annotation().type;
|
|
|
|
solAssert(exprType, "");
|
|
|
|
if (exprType->category() == Type::Category::Magic)
|
|
|
|
{
|
2020-10-23 10:44:04 +00:00
|
|
|
if (auto const* identifier = dynamic_cast<Identifier const*>(&_memberAccess.expression()))
|
2020-09-29 08:36:20 +00:00
|
|
|
{
|
|
|
|
auto const& name = identifier->name();
|
|
|
|
solAssert(name == "block" || name == "msg" || name == "tx", "");
|
2021-02-03 10:31:17 +00:00
|
|
|
defineExpr(_memberAccess, state().txMember(name + "." + _memberAccess.memberName()));
|
2020-09-29 08:36:20 +00:00
|
|
|
}
|
2020-09-11 18:28:01 +00:00
|
|
|
else if (auto magicType = dynamic_cast<MagicType const*>(exprType); magicType->kind() == MagicType::Kind::MetaType)
|
|
|
|
{
|
|
|
|
auto const& memberName = _memberAccess.memberName();
|
|
|
|
if (memberName == "min" || memberName == "max")
|
|
|
|
{
|
2021-08-26 16:03:16 +00:00
|
|
|
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());
|
2020-09-11 18:28:01 +00:00
|
|
|
}
|
2020-09-11 18:37:34 +00:00
|
|
|
else if (memberName == "interfaceId")
|
|
|
|
{
|
|
|
|
ContractDefinition const& contract = dynamic_cast<ContractType const&>(*magicType->typeArgument()).contractDefinition();
|
2020-09-14 10:39:38 +00:00
|
|
|
defineExpr(_memberAccess, contract.interfaceId());
|
2020-09-11 18:37:34 +00:00
|
|
|
}
|
2020-09-11 18:28:01 +00:00
|
|
|
else
|
|
|
|
// NOTE: supporting name, creationCode, runtimeCode would be easy enough, but the bytes/string they return are not
|
2020-11-23 18:40:29 +00:00
|
|
|
// at all usable in the SMT checker currently
|
2020-09-11 18:28:01 +00:00
|
|
|
m_errorReporter.warning(
|
|
|
|
7507_error,
|
|
|
|
_memberAccess.location(),
|
|
|
|
"Assertion checker does not yet support this expression."
|
|
|
|
);
|
|
|
|
}
|
2018-10-22 16:19:11 +00:00
|
|
|
else
|
2020-11-05 13:25:15 +00:00
|
|
|
solUnimplementedAssert(false, "");
|
|
|
|
|
2018-10-18 13:03:52 +00:00
|
|
|
return false;
|
|
|
|
}
|
2020-08-27 13:16:02 +00:00
|
|
|
else if (smt::isNonRecursiveStruct(*exprType))
|
2020-08-25 14:58:09 +00:00
|
|
|
{
|
|
|
|
_memberAccess.expression().accept(*this);
|
|
|
|
auto const& symbStruct = dynamic_pointer_cast<smt::SymbolicStructVariable>(m_context.expression(_memberAccess.expression()));
|
|
|
|
defineExpr(_memberAccess, symbStruct->member(_memberAccess.memberName()));
|
|
|
|
return false;
|
|
|
|
}
|
2019-03-06 00:10:43 +00:00
|
|
|
else if (exprType->category() == Type::Category::TypeType)
|
|
|
|
{
|
2020-10-23 10:44:04 +00:00
|
|
|
auto const* decl = expressionToDeclaration(_memberAccess.expression());
|
|
|
|
if (dynamic_cast<EnumDefinition const*>(decl))
|
2019-03-06 00:10:43 +00:00
|
|
|
{
|
2019-04-15 13:33:39 +00:00
|
|
|
auto enumType = dynamic_cast<EnumType const*>(accessType);
|
2019-03-06 00:10:43 +00:00
|
|
|
solAssert(enumType, "");
|
|
|
|
defineExpr(_memberAccess, enumType->memberValue(_memberAccess.memberName()));
|
2020-10-23 10:44:04 +00:00
|
|
|
|
|
|
|
return false;
|
|
|
|
}
|
|
|
|
else if (dynamic_cast<ContractDefinition const*>(decl))
|
|
|
|
{
|
|
|
|
if (auto const* var = dynamic_cast<VariableDeclaration const*>(_memberAccess.annotation().referencedDeclaration))
|
|
|
|
{
|
|
|
|
defineExpr(_memberAccess, currentValue(*var));
|
|
|
|
return false;
|
|
|
|
}
|
2019-03-06 00:10:43 +00:00
|
|
|
}
|
|
|
|
}
|
2019-04-11 16:14:48 +00:00
|
|
|
else if (exprType->category() == Type::Category::Address)
|
|
|
|
{
|
|
|
|
_memberAccess.expression().accept(*this);
|
|
|
|
if (_memberAccess.memberName() == "balance")
|
|
|
|
{
|
2021-02-03 10:31:17 +00:00
|
|
|
defineExpr(_memberAccess, state().balance(expr(_memberAccess.expression())));
|
2019-07-03 14:05:56 +00:00
|
|
|
setSymbolicUnknownValue(*m_context.expression(_memberAccess), m_context);
|
2019-04-11 16:14:48 +00:00
|
|
|
m_uninterpretedTerms.insert(&_memberAccess);
|
|
|
|
return false;
|
|
|
|
}
|
|
|
|
}
|
2020-04-14 09:09:38 +00:00
|
|
|
else if (exprType->category() == Type::Category::Array)
|
|
|
|
{
|
|
|
|
_memberAccess.expression().accept(*this);
|
|
|
|
if (_memberAccess.memberName() == "length")
|
|
|
|
{
|
|
|
|
auto symbArray = dynamic_pointer_cast<smt::SymbolicArrayVariable>(m_context.expression(_memberAccess.expression()));
|
|
|
|
solAssert(symbArray, "");
|
|
|
|
defineExpr(_memberAccess, symbArray->length());
|
|
|
|
m_uninterpretedTerms.insert(&_memberAccess);
|
|
|
|
setSymbolicUnknownValue(
|
|
|
|
expr(_memberAccess),
|
|
|
|
_memberAccess.annotation().type,
|
|
|
|
m_context
|
|
|
|
);
|
|
|
|
}
|
|
|
|
return false;
|
|
|
|
}
|
2020-10-21 15:57:34 +00:00
|
|
|
else if (
|
|
|
|
auto const* functionType = dynamic_cast<FunctionType const*>(exprType);
|
|
|
|
functionType &&
|
|
|
|
_memberAccess.memberName() == "selector" &&
|
|
|
|
functionType->hasDeclaration()
|
|
|
|
)
|
|
|
|
{
|
|
|
|
defineExpr(_memberAccess, functionType->externalIdentifier());
|
|
|
|
return false;
|
|
|
|
}
|
2018-10-18 13:03:52 +00:00
|
|
|
else
|
|
|
|
m_errorReporter.warning(
|
2020-05-05 22:38:28 +00:00
|
|
|
7650_error,
|
2018-10-18 13:03:52 +00:00
|
|
|
_memberAccess.location(),
|
|
|
|
"Assertion checker does not yet support this expression."
|
|
|
|
);
|
|
|
|
|
|
|
|
return true;
|
|
|
|
}
|
|
|
|
|
2019-06-25 10:46:17 +00:00
|
|
|
void SMTEncoder::endVisit(IndexAccess const& _indexAccess)
|
2018-11-09 16:06:30 +00:00
|
|
|
{
|
2019-07-01 14:25:33 +00:00
|
|
|
createExpr(_indexAccess);
|
|
|
|
|
2019-12-02 23:00:13 +00:00
|
|
|
if (_indexAccess.annotation().type->category() == Type::Category::TypeType)
|
|
|
|
return;
|
2021-03-23 18:15:14 +00:00
|
|
|
|
|
|
|
makeOutOfBoundsVerificationTarget(_indexAccess);
|
|
|
|
|
2020-09-24 13:27:56 +00:00
|
|
|
if (auto const* type = dynamic_cast<FixedBytesType const*>(_indexAccess.baseExpression().annotation().type))
|
2020-07-27 10:11:10 +00:00
|
|
|
{
|
2020-09-24 13:27:56 +00:00
|
|
|
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);
|
|
|
|
}
|
2020-07-27 10:11:10 +00:00
|
|
|
return;
|
|
|
|
}
|
2019-12-02 23:00:13 +00:00
|
|
|
|
2019-05-09 10:16:52 +00:00
|
|
|
shared_ptr<smt::SymbolicVariable> array;
|
2019-12-02 23:00:13 +00:00
|
|
|
if (auto const* id = dynamic_cast<Identifier const*>(&_indexAccess.baseExpression()))
|
2018-11-09 16:06:30 +00:00
|
|
|
{
|
2019-04-29 09:44:32 +00:00
|
|
|
auto varDecl = identifierToVariable(*id);
|
|
|
|
solAssert(varDecl, "");
|
2019-05-10 14:28:29 +00:00
|
|
|
array = m_context.variable(*varDecl);
|
2021-04-07 16:53:56 +00:00
|
|
|
|
|
|
|
if (varDecl && varDecl->isConstant())
|
|
|
|
m_context.addAssertion(currentValue(*varDecl) == expr(*id));
|
2018-11-09 16:06:30 +00:00
|
|
|
}
|
|
|
|
else
|
|
|
|
{
|
2020-08-25 14:58:09 +00:00
|
|
|
solAssert(m_context.knownExpression(_indexAccess.baseExpression()), "");
|
|
|
|
array = m_context.expression(_indexAccess.baseExpression());
|
2018-11-09 16:06:30 +00:00
|
|
|
}
|
|
|
|
|
2020-04-14 09:09:38 +00:00
|
|
|
auto arrayVar = dynamic_pointer_cast<smt::SymbolicArrayVariable>(array);
|
|
|
|
solAssert(arrayVar, "");
|
2021-03-23 18:15:14 +00:00
|
|
|
|
2021-03-22 16:12:05 +00:00
|
|
|
Type const* baseType = _indexAccess.baseExpression().annotation().type;
|
2020-05-19 12:14:46 +00:00
|
|
|
defineExpr(_indexAccess, smtutil::Expression::select(
|
2020-04-14 09:09:38 +00:00
|
|
|
arrayVar->elements(),
|
2020-10-19 20:46:15 +00:00
|
|
|
expr(*_indexAccess.indexExpression(), keyType(baseType))
|
2018-11-09 16:06:30 +00:00
|
|
|
));
|
|
|
|
setSymbolicUnknownValue(
|
|
|
|
expr(_indexAccess),
|
|
|
|
_indexAccess.annotation().type,
|
2019-07-03 14:05:56 +00:00
|
|
|
m_context
|
2018-11-09 16:06:30 +00:00
|
|
|
);
|
|
|
|
m_uninterpretedTerms.insert(&_indexAccess);
|
|
|
|
}
|
|
|
|
|
2019-09-03 16:30:00 +00:00
|
|
|
void SMTEncoder::endVisit(IndexRangeAccess const& _indexRangeAccess)
|
|
|
|
{
|
|
|
|
createExpr(_indexRangeAccess);
|
2020-09-24 17:24:33 +00:00
|
|
|
/// The actual slice is created by CHC which also assigns the length.
|
2019-09-03 16:30:00 +00:00
|
|
|
}
|
|
|
|
|
2019-06-25 10:46:17 +00:00
|
|
|
void SMTEncoder::arrayAssignment()
|
2018-12-14 11:21:43 +00:00
|
|
|
{
|
|
|
|
m_arrayAssignmentHappened = true;
|
|
|
|
}
|
|
|
|
|
2020-08-25 14:58:09 +00:00
|
|
|
void SMTEncoder::indexOrMemberAssignment(Expression const& _expr, smtutil::Expression const& _rightHandSide)
|
2018-11-09 16:06:30 +00:00
|
|
|
{
|
2019-10-28 16:27:39 +00:00
|
|
|
auto toStore = _rightHandSide;
|
2020-08-25 14:58:09 +00:00
|
|
|
auto const* lastExpr = &_expr;
|
2019-10-28 16:27:39 +00:00
|
|
|
while (true)
|
2018-11-09 16:06:30 +00:00
|
|
|
{
|
2020-08-25 14:58:09 +00:00
|
|
|
if (auto const* indexAccess = dynamic_cast<IndexAccess const*>(lastExpr))
|
2019-10-28 16:27:39 +00:00
|
|
|
{
|
2020-08-25 14:58:09 +00:00
|
|
|
auto const& base = indexAccess->baseExpression();
|
|
|
|
if (dynamic_cast<Identifier const*>(&base))
|
|
|
|
base.accept(*this);
|
2020-10-19 20:46:15 +00:00
|
|
|
|
2021-03-22 16:12:05 +00:00
|
|
|
Type const* baseType = base.annotation().type;
|
2020-10-19 20:46:15 +00:00
|
|
|
auto indexExpr = expr(*indexAccess->indexExpression(), keyType(baseType));
|
2020-08-25 14:58:09 +00:00
|
|
|
auto symbArray = dynamic_pointer_cast<smt::SymbolicArrayVariable>(m_context.expression(base));
|
|
|
|
solAssert(symbArray, "");
|
|
|
|
toStore = smtutil::Expression::tuple_constructor(
|
|
|
|
smtutil::Expression(make_shared<smtutil::SortSort>(smt::smtSort(*baseType)), baseType->toString(true)),
|
2020-10-19 20:46:15 +00:00
|
|
|
{smtutil::Expression::store(symbArray->elements(), indexExpr, toStore), symbArray->length()}
|
2019-10-28 16:27:39 +00:00
|
|
|
);
|
2020-05-19 12:14:46 +00:00
|
|
|
defineExpr(*indexAccess, smtutil::Expression::select(
|
2020-04-14 09:09:38 +00:00
|
|
|
symbArray->elements(),
|
2020-10-19 20:46:15 +00:00
|
|
|
indexExpr
|
2019-10-28 16:27:39 +00:00
|
|
|
));
|
2020-08-25 14:58:09 +00:00
|
|
|
lastExpr = &indexAccess->baseExpression();
|
2019-10-28 16:27:39 +00:00
|
|
|
}
|
2020-08-25 14:58:09 +00:00
|
|
|
else if (auto const* memberAccess = dynamic_cast<MemberAccess const*>(lastExpr))
|
2019-05-09 14:06:13 +00:00
|
|
|
{
|
2020-08-25 14:58:09 +00:00
|
|
|
auto const& base = memberAccess->expression();
|
|
|
|
if (dynamic_cast<Identifier const*>(&base))
|
|
|
|
base.accept(*this);
|
2020-08-27 13:16:02 +00:00
|
|
|
|
|
|
|
if (
|
|
|
|
auto const* structType = dynamic_cast<StructType const*>(base.annotation().type);
|
|
|
|
structType && structType->recursive()
|
|
|
|
)
|
|
|
|
{
|
|
|
|
m_errorReporter.warning(
|
|
|
|
4375_error,
|
|
|
|
memberAccess->location(),
|
|
|
|
"Assertion checker does not support recursive structs."
|
|
|
|
);
|
|
|
|
return;
|
|
|
|
}
|
2021-03-12 13:01:07 +00:00
|
|
|
if (auto varDecl = identifierToVariable(*memberAccess))
|
|
|
|
{
|
|
|
|
if (varDecl->hasReferenceOrMappingType())
|
|
|
|
resetReferences(*varDecl);
|
|
|
|
|
|
|
|
assignment(*varDecl, toStore);
|
|
|
|
break;
|
|
|
|
}
|
2020-08-27 13:16:02 +00:00
|
|
|
|
2020-08-25 14:58:09 +00:00
|
|
|
auto symbStruct = 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);
|
|
|
|
|
2020-11-19 16:11:02 +00:00
|
|
|
assignment(*varDecl, toStore);
|
2020-10-23 10:44:04 +00:00
|
|
|
defineExpr(*id, currentValue(*varDecl));
|
2020-08-25 14:58:09 +00:00
|
|
|
break;
|
2019-10-28 16:27:39 +00:00
|
|
|
}
|
|
|
|
else
|
|
|
|
{
|
2020-08-25 17:28:31 +00:00
|
|
|
auto type = lastExpr->annotation().type;
|
|
|
|
if (
|
|
|
|
dynamic_cast<ReferenceType const*>(type) ||
|
|
|
|
dynamic_cast<MappingType const*>(type)
|
|
|
|
)
|
|
|
|
resetReferences(type);
|
|
|
|
|
2020-11-19 16:11:02 +00:00
|
|
|
assignment(*m_context.expression(*lastExpr), toStore);
|
2019-10-28 16:27:39 +00:00
|
|
|
break;
|
2019-05-09 14:06:13 +00:00
|
|
|
}
|
|
|
|
}
|
2018-11-09 16:06:30 +00:00
|
|
|
}
|
|
|
|
|
2020-05-11 22:39:00 +00:00
|
|
|
void SMTEncoder::arrayPush(FunctionCall const& _funCall)
|
|
|
|
{
|
|
|
|
auto memberAccess = dynamic_cast<MemberAccess const*>(&_funCall.expression());
|
|
|
|
solAssert(memberAccess, "");
|
|
|
|
auto symbArray = dynamic_pointer_cast<smt::SymbolicArrayVariable>(m_context.expression(memberAccess->expression()));
|
|
|
|
solAssert(symbArray, "");
|
|
|
|
auto oldLength = symbArray->length();
|
2020-05-17 18:20:17 +00:00
|
|
|
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));
|
|
|
|
|
2020-05-11 22:39:00 +00:00
|
|
|
auto const& arguments = _funCall.arguments();
|
2021-01-12 17:52:14 +00:00
|
|
|
auto arrayType = dynamic_cast<ArrayType const*>(symbArray->type());
|
|
|
|
solAssert(arrayType, "");
|
|
|
|
auto elementType = arrayType->baseType();
|
2020-05-19 12:14:46 +00:00
|
|
|
smtutil::Expression element = arguments.empty() ?
|
2021-01-12 17:52:14 +00:00
|
|
|
smt::zeroValue(elementType) :
|
|
|
|
expr(*arguments.front(), elementType);
|
2020-05-19 12:14:46 +00:00
|
|
|
smtutil::Expression store = smtutil::Expression::store(
|
2020-05-11 22:39:00 +00:00
|
|
|
symbArray->elements(),
|
|
|
|
oldLength,
|
|
|
|
element
|
|
|
|
);
|
|
|
|
symbArray->increaseIndex();
|
|
|
|
m_context.addAssertion(symbArray->elements() == store);
|
2020-05-17 18:20:17 +00:00
|
|
|
m_context.addAssertion(symbArray->length() == oldLength + 1);
|
2020-05-11 22:39:00 +00:00
|
|
|
|
|
|
|
if (arguments.empty())
|
2021-03-26 09:31:58 +00:00
|
|
|
defineExpr(_funCall, element);
|
2020-05-11 22:39:00 +00:00
|
|
|
|
2021-03-26 09:31:58 +00:00
|
|
|
assignment(memberAccess->expression(), symbArray->currentValue());
|
2020-05-11 22:39:00 +00:00
|
|
|
}
|
|
|
|
|
|
|
|
void SMTEncoder::arrayPop(FunctionCall const& _funCall)
|
|
|
|
{
|
2021-03-09 19:00:51 +00:00
|
|
|
auto memberAccess = dynamic_cast<MemberAccess const*>(cleanExpression(_funCall.expression()));
|
2020-05-11 22:39:00 +00:00
|
|
|
solAssert(memberAccess, "");
|
|
|
|
auto symbArray = dynamic_pointer_cast<smt::SymbolicArrayVariable>(m_context.expression(memberAccess->expression()));
|
|
|
|
solAssert(symbArray, "");
|
2020-05-17 21:21:08 +00:00
|
|
|
|
|
|
|
makeArrayPopVerificationTarget(_funCall);
|
|
|
|
|
2020-05-11 22:39:00 +00:00
|
|
|
auto oldElements = symbArray->elements();
|
|
|
|
auto oldLength = symbArray->length();
|
2020-05-17 21:21:08 +00:00
|
|
|
|
2020-05-11 22:39:00 +00:00
|
|
|
symbArray->increaseIndex();
|
|
|
|
m_context.addAssertion(symbArray->elements() == oldElements);
|
2020-05-19 12:14:46 +00:00
|
|
|
auto newLength = smtutil::Expression::ite(
|
2020-08-28 09:59:15 +00:00
|
|
|
oldLength > 0,
|
|
|
|
oldLength - 1,
|
|
|
|
0
|
2020-05-11 22:39:00 +00:00
|
|
|
);
|
2020-08-28 09:59:15 +00:00
|
|
|
m_context.addAssertion(symbArray->length() == newLength);
|
2020-05-11 22:39:00 +00:00
|
|
|
|
2021-03-26 09:31:58 +00:00
|
|
|
assignment(memberAccess->expression(), symbArray->currentValue());
|
2020-05-11 22:39:00 +00:00
|
|
|
}
|
|
|
|
|
2019-06-25 10:46:17 +00:00
|
|
|
void SMTEncoder::defineGlobalVariable(string const& _name, Expression const& _expr, bool _increaseIndex)
|
2018-10-18 13:03:52 +00:00
|
|
|
{
|
2019-05-14 16:57:34 +00:00
|
|
|
if (!m_context.knownGlobalSymbol(_name))
|
2018-10-18 13:03:52 +00:00
|
|
|
{
|
2019-05-14 16:57:34 +00:00
|
|
|
bool abstract = m_context.createGlobalSymbol(_name, _expr);
|
|
|
|
if (abstract)
|
2018-10-18 13:03:52 +00:00
|
|
|
m_errorReporter.warning(
|
2020-05-05 22:38:28 +00:00
|
|
|
1695_error,
|
2018-10-18 13:03:52 +00:00
|
|
|
_expr.location(),
|
2018-12-10 16:23:36 +00:00
|
|
|
"Assertion checker does not yet support this global variable."
|
2018-10-18 13:03:52 +00:00
|
|
|
);
|
|
|
|
}
|
|
|
|
else if (_increaseIndex)
|
2019-05-14 16:57:34 +00:00
|
|
|
m_context.globalSymbol(_name)->increaseIndex();
|
2018-10-18 13:03:52 +00:00
|
|
|
// The default behavior is not to increase the index since
|
2018-12-10 16:23:36 +00:00
|
|
|
// most of the global values stay the same throughout a tx.
|
2020-08-27 13:16:02 +00:00
|
|
|
if (smt::isSupportedType(*_expr.annotation().type))
|
2019-05-14 16:57:34 +00:00
|
|
|
defineExpr(_expr, m_context.globalSymbol(_name)->currentValue());
|
2018-10-25 14:00:09 +00:00
|
|
|
}
|
2018-10-18 13:03:52 +00:00
|
|
|
|
2019-06-25 10:46:17 +00:00
|
|
|
bool SMTEncoder::shortcutRationalNumber(Expression const& _expr)
|
2019-03-11 10:56:08 +00:00
|
|
|
{
|
2020-12-16 16:58:49 +00:00
|
|
|
RationalNumberType const* rationalType = isConstant(_expr);
|
|
|
|
if (!rationalType)
|
2020-12-16 10:27:56 +00:00
|
|
|
return false;
|
|
|
|
|
2020-12-16 16:58:49 +00:00
|
|
|
if (rationalType->isNegative())
|
|
|
|
defineExpr(_expr, smtutil::Expression(u2s(rationalType->literalValue(nullptr))));
|
2020-12-16 10:27:56 +00:00
|
|
|
else
|
2020-12-16 16:58:49 +00:00
|
|
|
defineExpr(_expr, smtutil::Expression(rationalType->literalValue(nullptr)));
|
2020-12-16 10:27:56 +00:00
|
|
|
return true;
|
2019-03-11 10:56:08 +00:00
|
|
|
}
|
|
|
|
|
2019-06-25 10:46:17 +00:00
|
|
|
void SMTEncoder::arithmeticOperation(BinaryOperation const& _op)
|
2017-07-11 11:26:43 +00:00
|
|
|
{
|
2019-04-30 15:45:28 +00:00
|
|
|
auto type = _op.annotation().commonType;
|
|
|
|
solAssert(type, "");
|
2020-11-05 13:25:15 +00:00
|
|
|
solAssert(type->category() == Type::Category::Integer || type->category() == Type::Category::FixedPoint, "");
|
|
|
|
switch (_op.getOperator())
|
2017-07-11 11:26:43 +00:00
|
|
|
{
|
2020-11-05 13:25:15 +00:00
|
|
|
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;
|
2017-07-11 11:26:43 +00:00
|
|
|
}
|
2020-11-05 13:25:15 +00:00
|
|
|
default:
|
2017-07-11 11:26:43 +00:00
|
|
|
m_errorReporter.warning(
|
2020-11-05 13:25:15 +00:00
|
|
|
5188_error,
|
2017-07-11 11:26:43 +00:00
|
|
|
_op.location(),
|
2020-11-05 13:25:15 +00:00
|
|
|
"Assertion checker does not yet implement this operator."
|
2017-07-11 11:26:43 +00:00
|
|
|
);
|
2020-11-05 13:25:15 +00:00
|
|
|
}
|
2017-07-11 11:26:43 +00:00
|
|
|
}
|
|
|
|
|
2020-05-19 12:14:46 +00:00
|
|
|
pair<smtutil::Expression, smtutil::Expression> SMTEncoder::arithmeticOperation(
|
2019-03-28 11:42:32 +00:00
|
|
|
Token _op,
|
2020-05-19 12:14:46 +00:00
|
|
|
smtutil::Expression const& _left,
|
|
|
|
smtutil::Expression const& _right,
|
2021-03-22 16:12:05 +00:00
|
|
|
Type const* _commonType,
|
2020-06-09 11:07:40 +00:00
|
|
|
Expression const& _operation
|
2019-03-28 11:42:32 +00:00
|
|
|
)
|
|
|
|
{
|
|
|
|
static set<Token> validOperators{
|
|
|
|
Token::Add,
|
|
|
|
Token::Sub,
|
|
|
|
Token::Mul,
|
2019-04-05 15:07:08 +00:00
|
|
|
Token::Div,
|
|
|
|
Token::Mod
|
2019-03-28 11:42:32 +00:00
|
|
|
};
|
|
|
|
solAssert(validOperators.count(_op), "");
|
|
|
|
solAssert(_commonType, "");
|
2020-05-29 16:13:03 +00:00
|
|
|
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();
|
2019-03-28 11:42:32 +00:00
|
|
|
|
2020-06-09 11:07:40 +00:00
|
|
|
auto valueUnbounded = [&]() -> smtutil::Expression {
|
|
|
|
switch (_op)
|
|
|
|
{
|
|
|
|
case Token::Add: return _left + _right;
|
|
|
|
case Token::Sub: return _left - _right;
|
|
|
|
case Token::Mul: return _left * _right;
|
2020-10-14 14:26:50 +00:00
|
|
|
case Token::Div: return divModWithSlacks(_left, _right, *intType).first;
|
|
|
|
case Token::Mod: return divModWithSlacks(_left, _right, *intType).second;
|
2020-06-09 11:07:40 +00:00
|
|
|
default: solAssert(false, "");
|
|
|
|
}
|
|
|
|
}();
|
2019-03-28 11:42:32 +00:00
|
|
|
|
2020-12-16 17:32:34 +00:00
|
|
|
if (m_checked)
|
|
|
|
return {valueUnbounded, valueUnbounded};
|
|
|
|
|
2019-04-05 15:07:08 +00:00
|
|
|
if (_op == Token::Div || _op == Token::Mod)
|
2020-06-09 11:07:40 +00:00
|
|
|
{
|
|
|
|
// 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);
|
2020-06-15 10:51:58 +00:00
|
|
|
smtutil::Expression minusOneRight = _right == numeric_limits<size_t >::max();
|
2020-06-09 11:07:40 +00:00
|
|
|
smtutil::Expression wrap = smtutil::Expression::ite(maxLeft && minusOneRight, smt::minValue(*intType), valueUnbounded);
|
|
|
|
return {wrap, valueUnbounded};
|
|
|
|
}
|
|
|
|
|
2020-05-29 16:13:03 +00:00
|
|
|
auto symbMin = smt::minValue(*intType);
|
|
|
|
auto symbMax = smt::maxValue(*intType);
|
|
|
|
|
|
|
|
smtutil::Expression intValueRange = (0 - symbMin) + symbMax + 1;
|
2020-07-10 08:28:49 +00:00
|
|
|
string suffix = to_string(_operation.id()) + "_" + to_string(m_context.newUniqueId());
|
2020-06-09 11:07:40 +00:00
|
|
|
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.
|
2020-05-19 12:14:46 +00:00
|
|
|
auto value = smtutil::Expression::ite(
|
2020-06-09 11:07:40 +00:00
|
|
|
valueUnbounded > symbMax,
|
|
|
|
wrap,
|
2020-05-19 12:14:46 +00:00
|
|
|
smtutil::Expression::ite(
|
2020-06-09 11:07:40 +00:00
|
|
|
valueUnbounded < symbMin,
|
|
|
|
wrap,
|
|
|
|
valueUnbounded
|
2019-08-20 13:03:45 +00:00
|
|
|
)
|
2019-03-28 11:42:32 +00:00
|
|
|
);
|
2019-08-20 13:03:45 +00:00
|
|
|
|
2020-06-09 11:07:40 +00:00
|
|
|
return {value, valueUnbounded};
|
2019-03-28 11:42:32 +00:00
|
|
|
}
|
|
|
|
|
2020-09-21 14:54:58 +00:00
|
|
|
smtutil::Expression SMTEncoder::bitwiseOperation(
|
|
|
|
Token _op,
|
|
|
|
smtutil::Expression const& _left,
|
|
|
|
smtutil::Expression const& _right,
|
2021-03-22 16:12:05 +00:00
|
|
|
Type const* _commonType
|
2020-09-21 14:54:58 +00:00
|
|
|
)
|
|
|
|
{
|
|
|
|
static 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);
|
|
|
|
|
|
|
|
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:
|
2020-10-28 08:25:14 +00:00
|
|
|
result = bvLeft >> bvRight;
|
|
|
|
break;
|
2020-09-21 14:54:58 +00:00
|
|
|
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);
|
|
|
|
}
|
|
|
|
|
2019-06-25 10:46:17 +00:00
|
|
|
void SMTEncoder::compareOperation(BinaryOperation const& _op)
|
2017-07-11 11:26:43 +00:00
|
|
|
{
|
2019-08-07 08:48:09 +00:00
|
|
|
auto const& commonType = _op.annotation().commonType;
|
|
|
|
solAssert(commonType, "");
|
2020-08-27 13:16:02 +00:00
|
|
|
if (smt::isSupportedType(*commonType))
|
2017-07-11 11:26:43 +00:00
|
|
|
{
|
2020-05-19 12:14:46 +00:00
|
|
|
smtutil::Expression left(expr(_op.leftExpression(), commonType));
|
|
|
|
smtutil::Expression right(expr(_op.rightExpression(), commonType));
|
2018-10-22 14:48:21 +00:00
|
|
|
Token op = _op.getOperator();
|
2020-05-19 12:14:46 +00:00
|
|
|
shared_ptr<smtutil::Expression> value;
|
2020-08-27 13:16:02 +00:00
|
|
|
if (smt::isNumber(*commonType))
|
2018-03-09 15:19:03 +00:00
|
|
|
{
|
2020-05-19 12:14:46 +00:00
|
|
|
value = make_shared<smtutil::Expression>(
|
2018-03-09 15:19:03 +00:00
|
|
|
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
|
|
|
|
{
|
2020-08-27 13:16:02 +00:00
|
|
|
solUnimplementedAssert(smt::isBool(*commonType), "Operation not yet supported");
|
2020-05-19 12:14:46 +00:00
|
|
|
value = make_shared<smtutil::Expression>(
|
2018-03-09 15:19:03 +00:00
|
|
|
op == Token::Equal ? (left == right) :
|
2018-04-27 09:35:58 +00:00
|
|
|
/*op == Token::NotEqual*/ (left != right)
|
2018-03-09 15:19:03 +00:00
|
|
|
);
|
|
|
|
}
|
2017-07-11 11:26:43 +00:00
|
|
|
// TODO: check that other values for op are not possible.
|
2018-03-09 15:19:03 +00:00
|
|
|
defineExpr(_op, *value);
|
2017-07-11 11:26:43 +00:00
|
|
|
}
|
|
|
|
else
|
|
|
|
m_errorReporter.warning(
|
2020-05-05 22:38:28 +00:00
|
|
|
7229_error,
|
2017-07-11 11:26:43 +00:00
|
|
|
_op.location(),
|
|
|
|
"Assertion checker does not yet implement the type " + _op.annotation().commonType->toString() + " for comparisons"
|
|
|
|
);
|
|
|
|
}
|
|
|
|
|
2019-06-25 10:46:17 +00:00
|
|
|
void SMTEncoder::booleanOperation(BinaryOperation const& _op)
|
2017-07-11 11:26:43 +00:00
|
|
|
{
|
|
|
|
solAssert(_op.getOperator() == Token::And || _op.getOperator() == Token::Or, "");
|
|
|
|
solAssert(_op.annotation().commonType, "");
|
2020-11-05 13:25:15 +00:00
|
|
|
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)
|
2017-07-11 11:26:43 +00:00
|
|
|
{
|
2020-11-05 13:25:15 +00:00
|
|
|
auto indicesAfterSecond = visitBranch(&_op.rightExpression(), expr(_op.leftExpression())).first;
|
2021-03-29 12:44:33 +00:00
|
|
|
mergeVariables(!expr(_op.leftExpression()), copyVariableIndices(), indicesAfterSecond);
|
2020-11-05 13:25:15 +00:00
|
|
|
defineExpr(_op, expr(_op.leftExpression()) && expr(_op.rightExpression()));
|
2017-07-11 11:26:43 +00:00
|
|
|
}
|
|
|
|
else
|
2020-11-05 13:25:15 +00:00
|
|
|
{
|
|
|
|
auto indicesAfterSecond = visitBranch(&_op.rightExpression(), !expr(_op.leftExpression())).first;
|
2021-03-29 12:44:33 +00:00
|
|
|
mergeVariables(expr(_op.leftExpression()), copyVariableIndices(), indicesAfterSecond);
|
2020-11-05 13:25:15 +00:00
|
|
|
defineExpr(_op, expr(_op.leftExpression()) || expr(_op.rightExpression()));
|
|
|
|
}
|
2017-09-28 11:44:56 +00:00
|
|
|
}
|
|
|
|
|
2020-05-13 11:08:48 +00:00
|
|
|
void SMTEncoder::bitwiseOperation(BinaryOperation const& _op)
|
|
|
|
{
|
2020-09-04 14:55:45 +00:00
|
|
|
auto op = _op.getOperator();
|
|
|
|
solAssert(TokenTraits::isBitOp(op) || TokenTraits::isShiftOp(op), "");
|
2020-05-13 11:08:48 +00:00
|
|
|
auto commonType = _op.annotation().commonType;
|
|
|
|
solAssert(commonType, "");
|
|
|
|
|
2020-09-21 14:54:58 +00:00
|
|
|
defineExpr(_op, bitwiseOperation(
|
|
|
|
_op.getOperator(),
|
|
|
|
expr(_op.leftExpression(), commonType),
|
|
|
|
expr(_op.rightExpression(), commonType),
|
|
|
|
commonType
|
|
|
|
));
|
2020-05-13 11:08:48 +00:00
|
|
|
}
|
|
|
|
|
2020-08-23 19:21:45 +00:00
|
|
|
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));
|
|
|
|
}
|
|
|
|
|
2020-10-14 14:26:50 +00:00
|
|
|
pair<smtutil::Expression, smtutil::Expression> SMTEncoder::divModWithSlacks(
|
|
|
|
smtutil::Expression _left,
|
|
|
|
smtutil::Expression _right,
|
|
|
|
IntegerType const& _type
|
|
|
|
)
|
2017-10-05 17:20:46 +00:00
|
|
|
{
|
2021-07-15 15:39:01 +00:00
|
|
|
if (m_settings.divModNoSlacks)
|
|
|
|
return {_left / _right, _left % _right};
|
|
|
|
|
2020-10-14 14:26:50 +00:00
|
|
|
IntegerType const* intType = &_type;
|
|
|
|
string suffix = "div_mod_" + to_string(m_context.newUniqueId());
|
2020-11-06 11:51:01 +00:00
|
|
|
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();
|
2020-10-14 14:26:50 +00:00
|
|
|
|
|
|
|
// 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
|
2020-11-06 11:51:01 +00:00
|
|
|
m_context.addAssertion(((d * _right) + r) == _left);
|
2017-10-05 17:20:46 +00:00
|
|
|
if (_type.isSigned())
|
2020-10-14 14:26:50 +00:00
|
|
|
m_context.addAssertion(
|
2020-11-06 11:51:01 +00:00
|
|
|
(_left >= 0 && 0 <= r && (_right == 0 || r < smtutil::abs(_right))) ||
|
|
|
|
(_left < 0 && ((_right == 0 || 0 - smtutil::abs(_right) < r) && r <= 0))
|
2020-10-14 14:26:50 +00:00
|
|
|
);
|
|
|
|
else // unsigned version
|
2020-11-06 11:51:01 +00:00
|
|
|
m_context.addAssertion(0 <= r && (_right == 0 || r < _right));
|
2020-10-14 14:26:50 +00:00
|
|
|
|
2020-11-06 11:51:01 +00:00
|
|
|
auto divResult = smtutil::Expression::ite(_right == 0, 0, d);
|
|
|
|
auto modResult = smtutil::Expression::ite(_right == 0, 0, r);
|
2020-10-19 16:54:42 +00:00
|
|
|
return {divResult, modResult};
|
2017-10-05 17:20:46 +00:00
|
|
|
}
|
|
|
|
|
2021-03-26 09:31:58 +00:00
|
|
|
void SMTEncoder::assignment(Expression const& _left, smtutil::Expression const& _right)
|
|
|
|
{
|
|
|
|
assignment(_left, _right, _left.annotation().type);
|
|
|
|
}
|
|
|
|
|
2019-06-25 10:46:17 +00:00
|
|
|
void SMTEncoder::assignment(
|
2019-04-29 09:39:24 +00:00
|
|
|
Expression const& _left,
|
2020-05-27 17:24:48 +00:00
|
|
|
smtutil::Expression const& _right,
|
2021-03-22 16:12:05 +00:00
|
|
|
Type const* _type
|
2019-04-29 09:39:24 +00:00
|
|
|
)
|
|
|
|
{
|
2020-05-27 17:24:48 +00:00
|
|
|
solAssert(
|
|
|
|
_left.annotation().type->category() != Type::Category::Tuple,
|
|
|
|
"Tuple assignments should be handled by tupleAssignment."
|
|
|
|
);
|
|
|
|
|
2021-03-26 09:31:58 +00:00
|
|
|
Expression const* left = cleanExpression(_left);
|
2020-07-15 16:56:28 +00:00
|
|
|
|
2020-08-27 13:16:02 +00:00
|
|
|
if (!smt::isSupportedType(*_type))
|
2019-08-02 17:46:06 +00:00
|
|
|
{
|
|
|
|
// Give it a new index anyway to keep the SSA scheme sound.
|
2020-07-15 16:56:28 +00:00
|
|
|
if (auto varDecl = identifierToVariable(*left))
|
2019-08-02 17:46:06 +00:00
|
|
|
m_context.newValue(*varDecl);
|
|
|
|
}
|
2020-07-15 16:56:28 +00:00
|
|
|
else if (auto varDecl = identifierToVariable(*left))
|
2021-03-12 18:33:45 +00:00
|
|
|
{
|
|
|
|
if (varDecl->hasReferenceOrMappingType())
|
|
|
|
resetReferences(*varDecl);
|
2020-05-27 17:24:48 +00:00
|
|
|
assignment(*varDecl, _right);
|
2021-03-12 18:33:45 +00:00
|
|
|
}
|
2020-08-25 14:58:09 +00:00
|
|
|
else if (
|
|
|
|
dynamic_cast<IndexAccess const*>(left) ||
|
|
|
|
dynamic_cast<MemberAccess const*>(left)
|
|
|
|
)
|
|
|
|
indexOrMemberAssignment(*left, _right);
|
2021-03-26 09:31:58 +00:00
|
|
|
else if (auto const* funCall = dynamic_cast<FunctionCall const*>(left))
|
|
|
|
{
|
2021-08-27 16:53:15 +00:00
|
|
|
if (auto funType = dynamic_cast<FunctionType const*>(funCall->expression().annotation().type))
|
2021-03-26 09:31:58 +00:00
|
|
|
{
|
2021-08-27 16:53:15 +00:00
|
|
|
if (funType->kind() == FunctionType::Kind::ArrayPush)
|
|
|
|
{
|
|
|
|
auto memberAccess = dynamic_cast<MemberAccess const*>(&funCall->expression());
|
|
|
|
solAssert(memberAccess, "");
|
|
|
|
auto symbArray = 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: funType->returnParameterTypes())
|
|
|
|
if (type->category() == Type::Category::Mapping || dynamic_cast<ReferenceType const*>(type))
|
|
|
|
resetReferences(type);
|
|
|
|
}
|
2021-03-26 09:31:58 +00:00
|
|
|
}
|
|
|
|
}
|
2019-04-29 09:39:24 +00:00
|
|
|
else
|
2020-08-25 17:28:31 +00:00
|
|
|
solAssert(false, "");
|
2019-04-29 09:39:24 +00:00
|
|
|
}
|
|
|
|
|
2020-05-27 17:24:48 +00:00
|
|
|
void SMTEncoder::tupleAssignment(Expression const& _left, Expression const& _right)
|
|
|
|
{
|
2020-08-31 10:59:11 +00:00
|
|
|
auto lTuple = dynamic_cast<TupleExpression const*>(innermostTuple(_left));
|
2020-05-27 17:24:48 +00:00
|
|
|
solAssert(lTuple, "");
|
2020-08-31 14:12:38 +00:00
|
|
|
Expression const* right = innermostTuple(_right);
|
2020-05-27 17:24:48 +00:00
|
|
|
|
|
|
|
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.
|
2020-08-31 14:12:38 +00:00
|
|
|
if (auto rTuple = dynamic_cast<TupleExpression const*>(right))
|
2020-05-27 17:24:48 +00:00
|
|
|
{
|
|
|
|
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;
|
2020-08-25 17:28:31 +00:00
|
|
|
assignment(lExpr, expr(rExpr, type), type);
|
2020-05-27 17:24:48 +00:00
|
|
|
}
|
|
|
|
}
|
|
|
|
}
|
|
|
|
else
|
|
|
|
{
|
2020-08-31 14:12:38 +00:00
|
|
|
auto rType = dynamic_cast<TupleType const*>(right->annotation().type);
|
2020-05-27 17:24:48 +00:00
|
|
|
solAssert(rType, "");
|
|
|
|
|
|
|
|
auto const& rComponents = rType->components();
|
|
|
|
solAssert(lComponents.size() == rComponents.size(), "");
|
|
|
|
|
2020-08-31 14:12:38 +00:00
|
|
|
auto symbRight = expr(*right);
|
2020-05-27 17:24:48 +00:00
|
|
|
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))
|
2020-08-25 17:28:31 +00:00
|
|
|
assignment(*component, smtutil::Expression::tuple_get(symbRight, i), component->annotation().type);
|
2020-05-27 17:24:48 +00:00
|
|
|
}
|
|
|
|
}
|
|
|
|
|
2020-05-19 12:14:46 +00:00
|
|
|
smtutil::Expression SMTEncoder::compoundAssignment(Assignment const& _assignment)
|
2019-04-29 09:39:24 +00:00
|
|
|
{
|
|
|
|
static 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}
|
|
|
|
};
|
2020-09-21 14:54:58 +00:00
|
|
|
static map<Token, Token> const compoundToBitwise{
|
|
|
|
{Token::AssignBitAnd, Token::BitAnd},
|
|
|
|
{Token::AssignBitOr, Token::BitOr},
|
2020-09-22 09:15:56 +00:00
|
|
|
{Token::AssignBitXor, Token::BitXor},
|
|
|
|
{Token::AssignShl, Token::SHL},
|
|
|
|
{Token::AssignShr, Token::SHR},
|
|
|
|
{Token::AssignSar, Token::SAR}
|
2020-09-21 14:54:58 +00:00
|
|
|
};
|
2019-04-29 09:39:24 +00:00
|
|
|
Token op = _assignment.assignmentOperator();
|
2020-09-21 14:54:58 +00:00
|
|
|
solAssert(compoundToArithmetic.count(op) || compoundToBitwise.count(op), "");
|
|
|
|
|
2019-04-29 09:39:24 +00:00
|
|
|
auto decl = identifierToVariable(_assignment.leftHandSide());
|
2020-09-21 14:54:58 +00:00
|
|
|
|
|
|
|
if (compoundToBitwise.count(op))
|
|
|
|
return bitwiseOperation(
|
|
|
|
compoundToBitwise.at(op),
|
2020-11-24 18:14:15 +00:00
|
|
|
decl ? currentValue(*decl) : expr(_assignment.leftHandSide(), _assignment.annotation().type),
|
|
|
|
expr(_assignment.rightHandSide(), _assignment.annotation().type),
|
2020-09-21 14:54:58 +00:00
|
|
|
_assignment.annotation().type
|
|
|
|
);
|
|
|
|
|
2019-06-25 10:46:17 +00:00
|
|
|
auto values = arithmeticOperation(
|
2019-04-29 09:39:24 +00:00
|
|
|
compoundToArithmetic.at(op),
|
2020-11-24 18:14:15 +00:00
|
|
|
decl ? currentValue(*decl) : expr(_assignment.leftHandSide(), _assignment.annotation().type),
|
|
|
|
expr(_assignment.rightHandSide(), _assignment.annotation().type),
|
2019-04-29 09:39:24 +00:00
|
|
|
_assignment.annotation().type,
|
2019-06-24 15:37:03 +00:00
|
|
|
_assignment
|
2019-04-29 09:39:24 +00:00
|
|
|
);
|
2019-06-25 10:46:17 +00:00
|
|
|
return values.first;
|
2019-04-29 09:39:24 +00:00
|
|
|
}
|
|
|
|
|
2021-01-12 14:07:30 +00:00
|
|
|
void SMTEncoder::expressionToTupleAssignment(vector<shared_ptr<VariableDeclaration>> const& _variables, Expression const& _rhs)
|
2021-01-09 15:35:21 +00:00
|
|
|
{
|
2021-01-12 14:07:30 +00:00
|
|
|
auto symbolicVar = m_context.expression(_rhs);
|
2021-01-09 15:35:21 +00:00
|
|
|
if (_variables.size() > 1)
|
|
|
|
{
|
2021-01-12 14:07:30 +00:00
|
|
|
auto symbTuple = dynamic_pointer_cast<smt::SymbolicTupleVariable>(symbolicVar);
|
2021-01-09 15:35:21 +00:00
|
|
|
solAssert(symbTuple, "");
|
|
|
|
auto const& symbComponents = symbTuple->components();
|
|
|
|
solAssert(symbComponents.size() == _variables.size(), "");
|
2021-01-12 14:07:30 +00:00
|
|
|
auto tupleType = dynamic_cast<TupleType const*>(_rhs.annotation().type);
|
|
|
|
solAssert(tupleType, "");
|
|
|
|
auto const& typeComponents = tupleType->components();
|
|
|
|
solAssert(typeComponents.size() == symbComponents.size(), "");
|
2021-01-09 15:35:21 +00:00
|
|
|
for (unsigned i = 0; i < symbComponents.size(); ++i)
|
|
|
|
{
|
|
|
|
auto param = _variables.at(i);
|
2021-01-12 14:07:30 +00:00
|
|
|
if (param)
|
|
|
|
{
|
|
|
|
solAssert(m_context.knownVariable(*param), "");
|
|
|
|
assignment(*param, symbTuple->component(i, typeComponents[i], param->type()));
|
|
|
|
}
|
2021-01-09 15:35:21 +00:00
|
|
|
}
|
|
|
|
}
|
|
|
|
else if (_variables.size() == 1)
|
2021-01-12 14:07:30 +00:00
|
|
|
{
|
|
|
|
auto const& var = *_variables.front();
|
|
|
|
solAssert(m_context.knownVariable(var), "");
|
|
|
|
assignment(var, _rhs);
|
|
|
|
}
|
2021-01-09 15:35:21 +00:00
|
|
|
}
|
|
|
|
|
2019-06-25 10:46:17 +00:00
|
|
|
void SMTEncoder::assignment(VariableDeclaration const& _variable, Expression const& _value)
|
2017-09-28 11:44:56 +00:00
|
|
|
{
|
2020-04-14 09:09:38 +00:00
|
|
|
// 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.
|
2020-09-25 09:34:18 +00:00
|
|
|
assignment(_variable, expr(_value, _variable.type()));
|
2017-10-05 13:23:25 +00:00
|
|
|
}
|
|
|
|
|
2020-05-19 12:14:46 +00:00
|
|
|
void SMTEncoder::assignment(VariableDeclaration const& _variable, smtutil::Expression const& _value)
|
2017-10-05 13:23:25 +00:00
|
|
|
{
|
2021-03-22 16:12:05 +00:00
|
|
|
Type const* type = _variable.type();
|
2019-06-24 15:58:56 +00:00
|
|
|
if (type->category() == Type::Category::Mapping)
|
2018-12-14 11:21:43 +00:00
|
|
|
arrayAssignment();
|
2020-11-19 16:11:02 +00:00
|
|
|
assignment(*m_context.variable(_variable), _value);
|
|
|
|
}
|
|
|
|
|
|
|
|
void SMTEncoder::assignment(smt::SymbolicVariable& _symVar, smtutil::Expression const& _value)
|
|
|
|
{
|
|
|
|
m_context.addAssertion(_symVar.increaseIndex() == _value);
|
2017-09-28 11:44:56 +00:00
|
|
|
}
|
|
|
|
|
2020-11-14 14:42:32 +00:00
|
|
|
pair<SMTEncoder::VariableIndices, smtutil::Expression> SMTEncoder::visitBranch(
|
|
|
|
ASTNode const* _statement,
|
|
|
|
smtutil::Expression _condition
|
|
|
|
)
|
2017-09-28 13:24:24 +00:00
|
|
|
{
|
2017-12-18 18:43:15 +00:00
|
|
|
return visitBranch(_statement, &_condition);
|
2017-09-28 13:24:24 +00:00
|
|
|
}
|
|
|
|
|
2020-11-14 14:42:32 +00:00
|
|
|
pair<SMTEncoder::VariableIndices, smtutil::Expression> SMTEncoder::visitBranch(
|
|
|
|
ASTNode const* _statement,
|
|
|
|
smtutil::Expression const* _condition
|
|
|
|
)
|
2017-09-28 11:44:56 +00:00
|
|
|
{
|
2018-10-17 09:32:01 +00:00
|
|
|
auto indicesBeforeBranch = copyVariableIndices();
|
2017-09-28 11:44:56 +00:00
|
|
|
if (_condition)
|
2017-12-11 19:09:17 +00:00
|
|
|
pushPathCondition(*_condition);
|
2019-03-22 16:05:58 +00:00
|
|
|
_statement->accept(*this);
|
2020-11-14 14:42:32 +00:00
|
|
|
auto pathConditionOnExit = currentPathConditions();
|
2017-12-11 19:09:17 +00:00
|
|
|
if (_condition)
|
|
|
|
popPathCondition();
|
2018-10-17 09:32:01 +00:00
|
|
|
auto indicesAfterBranch = copyVariableIndices();
|
|
|
|
resetVariableIndices(indicesBeforeBranch);
|
2020-11-14 14:42:32 +00:00
|
|
|
return {indicesAfterBranch, pathConditionOnExit};
|
2017-07-11 11:26:43 +00:00
|
|
|
}
|
|
|
|
|
2020-05-19 12:14:46 +00:00
|
|
|
void SMTEncoder::initializeFunctionCallParameters(CallableDeclaration const& _function, vector<smtutil::Expression> const& _callArgs)
|
2018-10-10 12:31:49 +00:00
|
|
|
{
|
|
|
|
auto const& funParams = _function.parameters();
|
|
|
|
solAssert(funParams.size() == _callArgs.size(), "");
|
|
|
|
for (unsigned i = 0; i < funParams.size(); ++i)
|
|
|
|
if (createVariable(*funParams[i]))
|
2018-12-14 11:21:43 +00:00
|
|
|
{
|
2019-06-24 15:37:03 +00:00
|
|
|
m_context.addAssertion(_callArgs[i] == m_context.newValue(*funParams[i]));
|
2018-12-14 11:21:43 +00:00
|
|
|
if (funParams[i]->annotation().type->category() == Type::Category::Mapping)
|
|
|
|
m_arrayAssignmentHappened = true;
|
|
|
|
}
|
2018-10-10 12:31:49 +00:00
|
|
|
|
2020-11-04 21:06:30 +00:00
|
|
|
vector<VariableDeclaration const*> localVars;
|
|
|
|
if (auto const* fun = dynamic_cast<FunctionDefinition const*>(&_function))
|
2020-12-15 14:50:02 +00:00
|
|
|
localVars = localVariablesIncludingModifiers(*fun, m_currentContract);
|
2020-11-04 21:06:30 +00:00
|
|
|
else
|
|
|
|
localVars = _function.localVariables();
|
|
|
|
for (auto const& variable: localVars)
|
2018-10-10 12:31:49 +00:00
|
|
|
if (createVariable(*variable))
|
|
|
|
{
|
2019-05-10 14:28:29 +00:00
|
|
|
m_context.newValue(*variable);
|
|
|
|
m_context.setZeroValue(*variable);
|
2018-10-10 12:31:49 +00:00
|
|
|
}
|
|
|
|
|
|
|
|
if (_function.returnParameterList())
|
|
|
|
for (auto const& retParam: _function.returnParameters())
|
|
|
|
if (createVariable(*retParam))
|
|
|
|
{
|
2019-05-10 14:28:29 +00:00
|
|
|
m_context.newValue(*retParam);
|
|
|
|
m_context.setZeroValue(*retParam);
|
2018-10-10 12:31:49 +00:00
|
|
|
}
|
|
|
|
}
|
|
|
|
|
2019-09-26 14:12:27 +00:00
|
|
|
void SMTEncoder::createStateVariables(ContractDefinition const& _contract)
|
2019-08-02 16:36:26 +00:00
|
|
|
{
|
2020-10-28 18:13:40 +00:00
|
|
|
for (auto var: stateVariablesIncludingInheritedAndPrivate(_contract))
|
2019-08-02 16:36:26 +00:00
|
|
|
createVariable(*var);
|
|
|
|
}
|
|
|
|
|
2019-09-26 14:12:27 +00:00
|
|
|
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)
|
|
|
|
{
|
2020-12-15 14:50:02 +00:00
|
|
|
for (auto const& variable: localVariablesIncludingModifiers(_function, m_currentContract))
|
2019-09-26 14:12:27 +00:00
|
|
|
createVariable(*variable);
|
|
|
|
|
|
|
|
for (auto const& param: _function.parameters())
|
|
|
|
createVariable(*param);
|
|
|
|
|
|
|
|
if (_function.returnParameterList())
|
|
|
|
for (auto const& retParam: _function.returnParameters())
|
|
|
|
createVariable(*retParam);
|
|
|
|
}
|
|
|
|
|
2019-06-25 10:46:17 +00:00
|
|
|
void SMTEncoder::initializeLocalVariables(FunctionDefinition const& _function)
|
2017-09-28 13:24:24 +00:00
|
|
|
{
|
2020-12-15 14:50:02 +00:00
|
|
|
for (auto const& variable: localVariablesIncludingModifiers(_function, m_currentContract))
|
2019-09-26 14:12:27 +00:00
|
|
|
{
|
|
|
|
solAssert(m_context.knownVariable(*variable), "");
|
|
|
|
m_context.setZeroValue(*variable);
|
|
|
|
}
|
2017-10-05 17:31:17 +00:00
|
|
|
|
2017-09-28 13:24:24 +00:00
|
|
|
for (auto const& param: _function.parameters())
|
2019-09-26 14:12:27 +00:00
|
|
|
{
|
|
|
|
solAssert(m_context.knownVariable(*param), "");
|
|
|
|
m_context.setUnknownValue(*param);
|
|
|
|
}
|
2017-10-05 17:31:17 +00:00
|
|
|
|
2017-09-28 13:24:24 +00:00
|
|
|
if (_function.returnParameterList())
|
|
|
|
for (auto const& retParam: _function.returnParameters())
|
2019-09-26 14:12:27 +00:00
|
|
|
{
|
|
|
|
solAssert(m_context.knownVariable(*retParam), "");
|
|
|
|
m_context.setZeroValue(*retParam);
|
|
|
|
}
|
2018-12-20 17:11:20 +00:00
|
|
|
}
|
|
|
|
|
2019-06-25 10:46:17 +00:00
|
|
|
void SMTEncoder::resetStateVariables()
|
2018-04-18 21:14:45 +00:00
|
|
|
{
|
2019-05-10 14:28:29 +00:00
|
|
|
m_context.resetVariables([&](VariableDeclaration const& _variable) { return _variable.isStateVariable(); });
|
2018-12-20 17:11:20 +00:00
|
|
|
}
|
|
|
|
|
2021-01-18 09:37:09 +00:00
|
|
|
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();
|
|
|
|
});
|
|
|
|
}
|
|
|
|
|
2021-08-25 09:29:42 +00:00
|
|
|
void SMTEncoder::resetBalances()
|
|
|
|
{
|
2021-08-20 13:49:36 +00:00
|
|
|
state().newBalances();
|
2021-08-25 09:29:42 +00:00
|
|
|
}
|
|
|
|
|
2020-06-05 12:54:52 +00:00
|
|
|
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;
|
|
|
|
|
2020-08-25 17:28:31 +00:00
|
|
|
return sameTypeOrSubtype(_var.type(), _varDecl.type());
|
|
|
|
});
|
|
|
|
}
|
|
|
|
|
2021-03-22 16:12:05 +00:00
|
|
|
void SMTEncoder::resetReferences(Type const* _type)
|
2020-08-25 17:28:31 +00:00
|
|
|
{
|
|
|
|
m_context.resetVariables([&](VariableDeclaration const& _var) {
|
|
|
|
return sameTypeOrSubtype(_var.type(), _type);
|
|
|
|
});
|
|
|
|
}
|
|
|
|
|
2021-03-22 16:12:05 +00:00
|
|
|
bool SMTEncoder::sameTypeOrSubtype(Type const* _a, Type const* _b)
|
2020-08-25 17:28:31 +00:00
|
|
|
{
|
2021-03-22 16:12:05 +00:00
|
|
|
Type const* prefix = _a;
|
2020-08-25 17:28:31 +00:00
|
|
|
while (
|
|
|
|
prefix->category() == Type::Category::Mapping ||
|
|
|
|
prefix->category() == Type::Category::Array
|
|
|
|
)
|
|
|
|
{
|
|
|
|
if (*typeWithoutPointer(_b) == *typeWithoutPointer(prefix))
|
|
|
|
return true;
|
|
|
|
if (prefix->category() == Type::Category::Mapping)
|
2020-06-05 12:54:52 +00:00
|
|
|
{
|
2020-08-25 17:28:31 +00:00
|
|
|
auto mapPrefix = dynamic_cast<MappingType const*>(prefix);
|
|
|
|
solAssert(mapPrefix, "");
|
|
|
|
prefix = mapPrefix->valueType();
|
2020-06-05 12:54:52 +00:00
|
|
|
}
|
2020-08-25 17:28:31 +00:00
|
|
|
else
|
|
|
|
{
|
|
|
|
auto arrayPrefix = dynamic_cast<ArrayType const*>(prefix);
|
|
|
|
solAssert(arrayPrefix, "");
|
|
|
|
prefix = arrayPrefix->baseType();
|
|
|
|
}
|
|
|
|
}
|
|
|
|
return false;
|
2020-06-05 12:54:52 +00:00
|
|
|
}
|
|
|
|
|
2021-03-22 16:12:05 +00:00
|
|
|
Type const* SMTEncoder::typeWithoutPointer(Type const* _type)
|
2019-02-21 12:01:58 +00:00
|
|
|
{
|
2019-04-15 13:33:39 +00:00
|
|
|
if (auto refType = dynamic_cast<ReferenceType const*>(_type))
|
2019-04-17 11:25:03 +00:00
|
|
|
return TypeProvider::withLocationIfReference(refType->location(), _type);
|
2019-02-21 12:01:58 +00:00
|
|
|
return _type;
|
|
|
|
}
|
|
|
|
|
2021-03-29 12:44:33 +00:00
|
|
|
void SMTEncoder::mergeVariables(smtutil::Expression const& _condition, VariableIndices const& _indicesEndTrue, VariableIndices const& _indicesEndFalse)
|
2019-03-22 16:05:58 +00:00
|
|
|
{
|
2021-03-29 12:44:33 +00:00
|
|
|
for (auto const& entry: _indicesEndTrue)
|
2019-07-30 10:18:03 +00:00
|
|
|
{
|
2021-03-29 12:44:33 +00:00
|
|
|
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)))
|
|
|
|
);
|
|
|
|
}
|
2017-12-18 18:43:15 +00:00
|
|
|
}
|
|
|
|
}
|
|
|
|
|
2021-04-27 11:30:19 +00:00
|
|
|
smtutil::Expression SMTEncoder::currentValue(VariableDeclaration const& _decl) const
|
2019-05-10 14:28:29 +00:00
|
|
|
{
|
|
|
|
solAssert(m_context.knownVariable(_decl), "");
|
|
|
|
return m_context.variable(_decl)->currentValue();
|
|
|
|
}
|
|
|
|
|
2021-04-27 11:30:19 +00:00
|
|
|
smtutil::Expression SMTEncoder::valueAtIndex(VariableDeclaration const& _decl, unsigned _index) const
|
2019-05-10 14:28:29 +00:00
|
|
|
{
|
|
|
|
solAssert(m_context.knownVariable(_decl), "");
|
|
|
|
return m_context.variable(_decl)->valueAtIndex(_index);
|
|
|
|
}
|
|
|
|
|
2019-06-25 10:46:17 +00:00
|
|
|
bool SMTEncoder::createVariable(VariableDeclaration const& _varDecl)
|
2017-07-11 11:26:43 +00:00
|
|
|
{
|
2019-05-10 14:28:29 +00:00
|
|
|
if (m_context.knownVariable(_varDecl))
|
2018-10-10 12:31:49 +00:00
|
|
|
return true;
|
2019-05-10 14:28:29 +00:00
|
|
|
bool abstract = m_context.createVariable(_varDecl);
|
|
|
|
if (abstract)
|
2017-10-05 17:31:17 +00:00
|
|
|
{
|
2017-07-11 11:26:43 +00:00
|
|
|
m_errorReporter.warning(
|
2020-05-05 22:38:28 +00:00
|
|
|
8115_error,
|
2017-07-11 11:26:43 +00:00
|
|
|
_varDecl.location(),
|
|
|
|
"Assertion checker does not yet support the type of this variable."
|
|
|
|
);
|
2017-10-05 17:31:17 +00:00
|
|
|
return false;
|
|
|
|
}
|
2018-10-17 16:00:42 +00:00
|
|
|
return true;
|
2017-07-11 11:26:43 +00:00
|
|
|
}
|
|
|
|
|
2021-03-22 16:12:05 +00:00
|
|
|
smtutil::Expression SMTEncoder::expr(Expression const& _e, Type const* _targetType)
|
2017-07-11 11:26:43 +00:00
|
|
|
{
|
2019-05-13 14:53:38 +00:00
|
|
|
if (!m_context.knownExpression(_e))
|
2017-10-05 17:39:29 +00:00
|
|
|
{
|
2020-05-05 22:38:28 +00:00
|
|
|
m_errorReporter.warning(6031_error, _e.location(), "Internal error: Expression undefined for SMT solver." );
|
2017-10-05 17:39:29 +00:00
|
|
|
createExpr(_e);
|
|
|
|
}
|
2019-08-07 08:48:09 +00:00
|
|
|
|
|
|
|
return m_context.expression(_e)->currentValue(_targetType);
|
2018-10-10 12:31:49 +00:00
|
|
|
}
|
|
|
|
|
2019-06-25 10:46:17 +00:00
|
|
|
void SMTEncoder::createExpr(Expression const& _e)
|
2017-10-05 13:23:25 +00:00
|
|
|
{
|
2019-05-13 14:53:38 +00:00
|
|
|
bool abstract = m_context.createExpression(_e);
|
|
|
|
if (abstract)
|
|
|
|
m_errorReporter.warning(
|
2020-05-05 22:38:28 +00:00
|
|
|
8364_error,
|
2019-05-13 14:53:38 +00:00
|
|
|
_e.location(),
|
2019-07-01 14:25:33 +00:00
|
|
|
"Assertion checker does not yet implement type " + _e.annotation().type->toString()
|
2019-05-13 14:53:38 +00:00
|
|
|
);
|
2017-10-05 13:23:25 +00:00
|
|
|
}
|
|
|
|
|
2020-05-19 12:14:46 +00:00
|
|
|
void SMTEncoder::defineExpr(Expression const& _e, smtutil::Expression _value)
|
2017-10-05 13:23:25 +00:00
|
|
|
{
|
2021-03-16 20:55:45 +00:00
|
|
|
auto type = _e.annotation().type;
|
2017-10-05 13:23:25 +00:00
|
|
|
createExpr(_e);
|
2020-05-19 12:14:46 +00:00
|
|
|
solAssert(_value.sort->kind != smtutil::Kind::Function, "Equality operator applied to type that is not fully supported");
|
2021-03-16 20:55:45 +00:00
|
|
|
if (!smt::isInaccessibleDynamic(*type))
|
|
|
|
m_context.addAssertion(expr(_e) == _value);
|
2020-12-16 17:32:34 +00:00
|
|
|
|
2021-03-16 20:55:45 +00:00
|
|
|
if (m_checked && smt::isNumber(*type))
|
2020-12-16 17:32:34 +00:00
|
|
|
m_context.addAssertion(smtutil::Expression::implies(
|
|
|
|
currentPathConditions(),
|
|
|
|
smt::symbolicUnknownConstraints(expr(_e), type)
|
|
|
|
));
|
2021-03-16 12:11:24 +00:00
|
|
|
}
|
2020-12-16 17:32:34 +00:00
|
|
|
|
2021-03-16 12:11:24 +00:00
|
|
|
void SMTEncoder::defineExpr(Expression const& _e, vector<optional<smtutil::Expression>> const& _values)
|
|
|
|
{
|
|
|
|
if (_values.size() == 1 && _values.front())
|
|
|
|
{
|
|
|
|
defineExpr(_e, *_values.front());
|
|
|
|
return;
|
|
|
|
}
|
|
|
|
auto const& symbTuple = dynamic_pointer_cast<smt::SymbolicTupleVariable>(m_context.expression(_e));
|
|
|
|
solAssert(symbTuple, "");
|
|
|
|
symbTuple->increaseIndex();
|
|
|
|
auto const& symbComponents = symbTuple->components();
|
|
|
|
solAssert(symbComponents.size() == _values.size(), "");
|
2021-03-16 20:55:45 +00:00
|
|
|
auto tupleType = dynamic_cast<TupleType const*>(_e.annotation().type);
|
|
|
|
solAssert(tupleType, "");
|
|
|
|
solAssert(tupleType->components().size() == symbComponents.size(), "");
|
2021-03-16 12:11:24 +00:00
|
|
|
for (unsigned i = 0; i < symbComponents.size(); ++i)
|
2021-03-16 20:55:45 +00:00
|
|
|
if (_values[i] && !smt::isInaccessibleDynamic(*tupleType->components()[i]))
|
2021-03-16 12:11:24 +00:00
|
|
|
m_context.addAssertion(symbTuple->component(i) == *_values[i]);
|
2017-07-11 11:26:43 +00:00
|
|
|
}
|
|
|
|
|
2019-06-25 10:46:17 +00:00
|
|
|
void SMTEncoder::popPathCondition()
|
2017-12-11 19:09:17 +00:00
|
|
|
{
|
|
|
|
solAssert(m_pathConditions.size() > 0, "Cannot pop path condition, empty.");
|
|
|
|
m_pathConditions.pop_back();
|
|
|
|
}
|
|
|
|
|
2020-05-19 12:14:46 +00:00
|
|
|
void SMTEncoder::pushPathCondition(smtutil::Expression const& _e)
|
2017-12-11 19:09:17 +00:00
|
|
|
{
|
|
|
|
m_pathConditions.push_back(currentPathConditions() && _e);
|
|
|
|
}
|
|
|
|
|
2020-11-14 14:42:32 +00:00
|
|
|
void SMTEncoder::setPathCondition(smtutil::Expression const& _e)
|
|
|
|
{
|
|
|
|
if (m_pathConditions.empty())
|
|
|
|
m_pathConditions.push_back(_e);
|
|
|
|
else
|
|
|
|
m_pathConditions.back() = _e;
|
|
|
|
}
|
|
|
|
|
2020-05-19 12:14:46 +00:00
|
|
|
smtutil::Expression SMTEncoder::currentPathConditions()
|
2017-12-11 19:09:17 +00:00
|
|
|
{
|
2018-10-09 03:29:37 +00:00
|
|
|
if (m_pathConditions.empty())
|
2020-05-19 12:14:46 +00:00
|
|
|
return smtutil::Expression(true);
|
2017-12-11 19:09:17 +00:00
|
|
|
return m_pathConditions.back();
|
|
|
|
}
|
2017-12-13 16:59:36 +00:00
|
|
|
|
2019-06-25 10:46:17 +00:00
|
|
|
SecondarySourceLocation SMTEncoder::callStackMessage(vector<CallStackEntry> const& _callStack)
|
2019-03-18 12:04:08 +00:00
|
|
|
{
|
|
|
|
SecondarySourceLocation callStackLocation;
|
2019-06-24 15:37:03 +00:00
|
|
|
solAssert(!_callStack.empty(), "");
|
2020-10-14 15:44:40 +00:00
|
|
|
callStackLocation.append("Callstack:", SourceLocation());
|
2021-03-31 18:03:04 +00:00
|
|
|
for (auto const& call: _callStack | ranges::views::reverse)
|
2019-05-06 18:03:11 +00:00
|
|
|
if (call.second)
|
|
|
|
callStackLocation.append("", call.second->location());
|
2019-03-18 12:04:08 +00:00
|
|
|
return callStackLocation;
|
|
|
|
}
|
|
|
|
|
2019-06-25 10:46:17 +00:00
|
|
|
pair<CallableDeclaration const*, ASTNode const*> SMTEncoder::popCallStack()
|
2019-03-11 20:06:28 +00:00
|
|
|
{
|
|
|
|
solAssert(!m_callStack.empty(), "");
|
2019-05-06 18:03:11 +00:00
|
|
|
auto lastCalled = m_callStack.back();
|
2019-03-11 20:06:28 +00:00
|
|
|
m_callStack.pop_back();
|
|
|
|
return lastCalled;
|
|
|
|
}
|
|
|
|
|
2019-06-25 10:46:17 +00:00
|
|
|
void SMTEncoder::pushCallStack(CallStackEntry _entry)
|
2019-03-11 20:06:28 +00:00
|
|
|
{
|
2019-05-06 18:03:11 +00:00
|
|
|
m_callStack.push_back(_entry);
|
2019-03-11 20:06:28 +00:00
|
|
|
}
|
|
|
|
|
2020-05-19 12:14:46 +00:00
|
|
|
void SMTEncoder::addPathImpliedExpression(smtutil::Expression const& _e)
|
2017-12-13 16:59:36 +00:00
|
|
|
{
|
2020-05-19 12:14:46 +00:00
|
|
|
m_context.addAssertion(smtutil::Expression::implies(currentPathConditions(), _e));
|
2017-12-13 16:59:36 +00:00
|
|
|
}
|
2018-06-05 09:46:21 +00:00
|
|
|
|
2019-06-25 10:46:17 +00:00
|
|
|
bool SMTEncoder::isRootFunction()
|
2018-06-05 09:46:21 +00:00
|
|
|
{
|
2019-05-06 18:03:11 +00:00
|
|
|
return m_callStack.size() == 1;
|
2018-10-10 12:31:49 +00:00
|
|
|
}
|
|
|
|
|
2019-06-25 10:46:17 +00:00
|
|
|
bool SMTEncoder::visitedFunction(FunctionDefinition const* _funDef)
|
2018-10-10 12:31:49 +00:00
|
|
|
{
|
2019-05-06 18:03:11 +00:00
|
|
|
for (auto const& call: m_callStack)
|
|
|
|
if (call.first == _funDef)
|
|
|
|
return true;
|
|
|
|
return false;
|
2018-06-05 09:46:21 +00:00
|
|
|
}
|
2018-10-15 15:32:17 +00:00
|
|
|
|
2021-01-25 17:17:56 +00:00
|
|
|
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;
|
|
|
|
}
|
|
|
|
|
2019-06-25 10:46:17 +00:00
|
|
|
SMTEncoder::VariableIndices SMTEncoder::copyVariableIndices()
|
2018-10-15 15:32:17 +00:00
|
|
|
{
|
2018-10-17 09:32:01 +00:00
|
|
|
VariableIndices indices;
|
2019-05-10 14:28:29 +00:00
|
|
|
for (auto const& var: m_context.variables())
|
2018-10-17 09:32:01 +00:00
|
|
|
indices.emplace(var.first, var.second->index());
|
|
|
|
return indices;
|
2018-10-15 15:32:17 +00:00
|
|
|
}
|
|
|
|
|
2019-06-25 10:46:17 +00:00
|
|
|
void SMTEncoder::resetVariableIndices(VariableIndices const& _indices)
|
2018-10-15 15:32:17 +00:00
|
|
|
{
|
2018-10-17 09:32:01 +00:00
|
|
|
for (auto const& var: _indices)
|
2021-03-29 12:44:33 +00:00
|
|
|
m_context.variable(*var.first)->setIndex(var.second);
|
2018-10-15 15:32:17 +00:00
|
|
|
}
|
2019-03-25 12:58:22 +00:00
|
|
|
|
2019-09-26 14:12:27 +00:00
|
|
|
void SMTEncoder::clearIndices(ContractDefinition const* _contract, FunctionDefinition const* _function)
|
|
|
|
{
|
|
|
|
solAssert(_contract, "");
|
2020-10-28 18:13:40 +00:00
|
|
|
for (auto var: stateVariablesIncludingInheritedAndPrivate(*_contract))
|
2019-09-26 14:12:27 +00:00
|
|
|
m_context.variable(*var)->resetIndex();
|
|
|
|
if (_function)
|
|
|
|
{
|
|
|
|
for (auto const& var: _function->parameters() + _function->returnParameters())
|
|
|
|
m_context.variable(*var)->resetIndex();
|
2020-12-15 14:50:02 +00:00
|
|
|
for (auto const& var: localVariablesIncludingModifiers(*_function, _contract))
|
2019-09-26 14:12:27 +00:00
|
|
|
m_context.variable(*var)->resetIndex();
|
|
|
|
}
|
2021-02-03 10:31:17 +00:00
|
|
|
state().reset();
|
2019-09-26 14:12:27 +00:00
|
|
|
}
|
|
|
|
|
2019-06-25 10:46:17 +00:00
|
|
|
Expression const* SMTEncoder::leftmostBase(IndexAccess const& _indexAccess)
|
2019-05-09 14:06:13 +00:00
|
|
|
{
|
|
|
|
Expression const* base = &_indexAccess.baseExpression();
|
|
|
|
while (auto access = dynamic_cast<IndexAccess const*>(base))
|
|
|
|
base = &access->baseExpression();
|
|
|
|
return base;
|
|
|
|
}
|
|
|
|
|
2021-03-22 16:12:05 +00:00
|
|
|
Type const* SMTEncoder::keyType(Type const* _type)
|
2020-10-19 20:46:15 +00:00
|
|
|
{
|
|
|
|
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, "");
|
|
|
|
}
|
|
|
|
|
2020-08-31 10:59:11 +00:00
|
|
|
Expression const* SMTEncoder::innermostTuple(Expression const& _expr)
|
2020-07-15 16:56:28 +00:00
|
|
|
{
|
2020-08-31 10:59:11 +00:00
|
|
|
auto const* tuple = dynamic_cast<TupleExpression const*>(&_expr);
|
|
|
|
if (!tuple || tuple->isInlineArray())
|
|
|
|
return &_expr;
|
|
|
|
|
2020-07-15 16:56:28 +00:00
|
|
|
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;
|
|
|
|
}
|
|
|
|
|
2021-08-30 16:21:22 +00:00
|
|
|
pair<Expression const*, FunctionCallOptions const*> SMTEncoder::functionCallExpression(FunctionCall const& _funCall)
|
|
|
|
{
|
|
|
|
Expression const* callExpr = &_funCall.expression();
|
|
|
|
auto const* callOptions = dynamic_cast<FunctionCallOptions const*>(callExpr);
|
|
|
|
if (callOptions)
|
|
|
|
callExpr = &callOptions->expression();
|
|
|
|
|
|
|
|
return {callExpr, callOptions};
|
|
|
|
}
|
|
|
|
|
2021-03-02 17:29:52 +00:00
|
|
|
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->isByteArray())
|
|
|
|
{
|
|
|
|
// 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->isByteArray()
|
|
|
|
)
|
|
|
|
return cleanExpression(arg);
|
|
|
|
}
|
|
|
|
}
|
|
|
|
solAssert(expr, "");
|
|
|
|
return expr;
|
|
|
|
}
|
|
|
|
|
2019-06-25 10:46:17 +00:00
|
|
|
set<VariableDeclaration const*> SMTEncoder::touchedVariables(ASTNode const& _node)
|
2019-04-01 09:10:28 +00:00
|
|
|
{
|
2019-05-06 18:03:11 +00:00
|
|
|
vector<CallableDeclaration const*> callStack;
|
|
|
|
for (auto const& call: m_callStack)
|
|
|
|
callStack.push_back(call.first);
|
|
|
|
return m_variableUsage.touchedVariables(_node, callStack);
|
2019-04-01 09:10:28 +00:00
|
|
|
}
|
2019-04-29 09:39:24 +00:00
|
|
|
|
2020-10-26 16:16:27 +00:00
|
|
|
Declaration const* SMTEncoder::expressionToDeclaration(Expression const& _expr) const
|
2020-10-23 10:44:04 +00:00
|
|
|
{
|
|
|
|
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;
|
|
|
|
}
|
|
|
|
|
2020-10-26 16:16:27 +00:00
|
|
|
VariableDeclaration const* SMTEncoder::identifierToVariable(Expression const& _expr) const
|
2019-04-29 09:39:24 +00:00
|
|
|
{
|
2020-10-23 10:44:04 +00:00
|
|
|
// 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))
|
2019-04-29 09:39:24 +00:00
|
|
|
{
|
2020-10-23 10:44:04 +00:00
|
|
|
solAssert(m_context.knownVariable(*varDecl), "");
|
|
|
|
return varDecl;
|
2019-04-29 09:39:24 +00:00
|
|
|
}
|
2021-03-12 13:01:07 +00:00
|
|
|
// 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(memberAccess->expression())))
|
|
|
|
if (auto const* varDecl = dynamic_cast<VariableDeclaration const*>(memberAccess->annotation().referencedDeclaration))
|
|
|
|
{
|
|
|
|
solAssert(m_context.knownVariable(*varDecl), "");
|
|
|
|
return varDecl;
|
|
|
|
}
|
2021-04-07 16:53:56 +00:00
|
|
|
|
2019-04-29 09:39:24 +00:00
|
|
|
return nullptr;
|
|
|
|
}
|
2019-06-25 10:46:17 +00:00
|
|
|
|
2020-10-26 16:16:27 +00:00
|
|
|
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);
|
2021-02-03 20:48:45 +00:00
|
|
|
if (funType.kind() == FunctionType::Kind::ArrayPush)
|
2020-10-26 16:16:27 +00:00
|
|
|
return &dynamic_cast<MemberAccess const&>(funCall->expression());
|
|
|
|
}
|
|
|
|
return nullptr;
|
|
|
|
}
|
|
|
|
|
2020-11-26 16:14:58 +00:00
|
|
|
bool SMTEncoder::isPublicGetter(Expression const& _expr) {
|
|
|
|
if (!isTrustedExternalCall(&_expr))
|
|
|
|
return false;
|
|
|
|
auto varDecl = dynamic_cast<VariableDeclaration const*>(
|
|
|
|
dynamic_cast<MemberAccess const&>(_expr).annotation().referencedDeclaration
|
|
|
|
);
|
|
|
|
return varDecl != nullptr;
|
|
|
|
}
|
|
|
|
|
2020-11-09 13:50:41 +00:00
|
|
|
bool SMTEncoder::isTrustedExternalCall(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)
|
|
|
|
;
|
|
|
|
}
|
|
|
|
|
2019-06-25 10:46:17 +00:00
|
|
|
string SMTEncoder::extraComment()
|
|
|
|
{
|
|
|
|
string extra;
|
|
|
|
if (m_arrayAssignmentHappened)
|
|
|
|
extra +=
|
|
|
|
"\nNote that array aliasing is not supported,"
|
|
|
|
" therefore all mapping information is erased after"
|
|
|
|
" a mapping local variable/parameter is assigned.\n"
|
|
|
|
"You can re-introduce information using require().";
|
|
|
|
return extra;
|
|
|
|
}
|
2019-07-17 15:54:48 +00:00
|
|
|
|
2021-01-25 17:17:56 +00:00
|
|
|
FunctionDefinition const* SMTEncoder::functionCallToDefinition(
|
|
|
|
FunctionCall const& _funCall,
|
|
|
|
ContractDefinition const* _scopeContract,
|
|
|
|
ContractDefinition const* _contextContract
|
|
|
|
)
|
2019-07-17 15:54:48 +00:00
|
|
|
{
|
2020-04-08 17:38:30 +00:00
|
|
|
if (*_funCall.annotation().kind != FunctionCallKind::FunctionCall)
|
2020-12-22 19:25:31 +00:00
|
|
|
return {};
|
2019-07-17 15:54:48 +00:00
|
|
|
|
2021-08-30 16:21:22 +00:00
|
|
|
auto [calledExpr, callOptions] = functionCallExpression(_funCall);
|
|
|
|
|
2020-12-11 17:59:03 +00:00
|
|
|
if (TupleExpression const* fun = dynamic_cast<TupleExpression const*>(calledExpr))
|
2019-07-17 15:54:48 +00:00
|
|
|
{
|
|
|
|
solAssert(fun->components().size() == 1, "");
|
2020-12-11 17:59:03 +00:00
|
|
|
calledExpr = innermostTuple(*calledExpr);
|
2019-07-17 15:54:48 +00:00
|
|
|
}
|
|
|
|
|
2021-01-25 17:17:56 +00:00
|
|
|
auto resolveVirtual = [&](auto const* _ref) -> FunctionDefinition const* {
|
2020-12-22 19:25:31 +00:00
|
|
|
VirtualLookup lookup = *_ref->annotation().requiredLookup;
|
2021-01-25 17:17:56 +00:00
|
|
|
solAssert(_contextContract || lookup == VirtualLookup::Static, "No contract context provided for function lookup resolution!");
|
2020-12-22 19:25:31 +00:00
|
|
|
auto funDef = dynamic_cast<FunctionDefinition const*>(_ref->annotation().referencedDeclaration);
|
|
|
|
if (!funDef)
|
2021-01-25 17:17:56 +00:00
|
|
|
return funDef;
|
2021-01-18 10:40:04 +00:00
|
|
|
switch (lookup)
|
|
|
|
{
|
|
|
|
case VirtualLookup::Virtual:
|
2021-01-25 17:17:56 +00:00
|
|
|
return &(funDef->resolveVirtual(*_contextContract));
|
2021-01-18 10:40:04 +00:00
|
|
|
case VirtualLookup::Super:
|
2020-12-22 19:25:31 +00:00
|
|
|
{
|
2021-01-25 17:17:56 +00:00
|
|
|
solAssert(_scopeContract, "");
|
|
|
|
auto super = _scopeContract->superContract(*_contextContract);
|
2020-12-22 19:25:31 +00:00
|
|
|
solAssert(super, "Super contract not available.");
|
2021-01-25 17:17:56 +00:00
|
|
|
return &funDef->resolveVirtual(*_contextContract, super);
|
2021-01-18 10:40:04 +00:00
|
|
|
}
|
|
|
|
case VirtualLookup::Static:
|
2021-01-25 17:17:56 +00:00
|
|
|
return funDef;
|
2020-12-22 19:25:31 +00:00
|
|
|
}
|
2021-01-25 17:17:56 +00:00
|
|
|
solAssert(false, "");
|
2020-12-22 19:25:31 +00:00
|
|
|
};
|
|
|
|
|
2019-07-17 15:54:48 +00:00
|
|
|
if (Identifier const* fun = dynamic_cast<Identifier const*>(calledExpr))
|
2020-12-22 19:25:31 +00:00
|
|
|
return resolveVirtual(fun);
|
2019-07-17 15:54:48 +00:00
|
|
|
else if (MemberAccess const* fun = dynamic_cast<MemberAccess const*>(calledExpr))
|
2020-12-22 19:25:31 +00:00
|
|
|
return resolveVirtual(fun);
|
2019-07-17 15:54:48 +00:00
|
|
|
|
2020-12-22 19:25:31 +00:00
|
|
|
return {};
|
2019-07-17 15:54:48 +00:00
|
|
|
}
|
2019-08-02 18:43:54 +00:00
|
|
|
|
2020-08-19 11:51:58 +00:00
|
|
|
vector<VariableDeclaration const*> SMTEncoder::stateVariablesIncludingInheritedAndPrivate(ContractDefinition const& _contract)
|
|
|
|
{
|
|
|
|
return fold(
|
|
|
|
_contract.annotation().linearizedBaseContracts,
|
|
|
|
vector<VariableDeclaration const*>{},
|
|
|
|
[](auto&& _acc, auto _contract) { return _acc + _contract->stateVariables(); }
|
|
|
|
);
|
|
|
|
}
|
|
|
|
|
|
|
|
vector<VariableDeclaration const*> SMTEncoder::stateVariablesIncludingInheritedAndPrivate(FunctionDefinition const& _function)
|
|
|
|
{
|
|
|
|
return stateVariablesIncludingInheritedAndPrivate(dynamic_cast<ContractDefinition const&>(*_function.scope()));
|
|
|
|
}
|
|
|
|
|
2020-12-15 14:50:02 +00:00
|
|
|
vector<VariableDeclaration const*> SMTEncoder::localVariablesIncludingModifiers(FunctionDefinition const& _function, ContractDefinition const* _contract)
|
2020-11-04 21:06:30 +00:00
|
|
|
{
|
2021-01-04 18:33:07 +00:00
|
|
|
return _function.localVariables() + tryCatchVariables(_function) + modifiersVariables(_function, _contract);
|
|
|
|
}
|
|
|
|
|
|
|
|
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());
|
|
|
|
}
|
|
|
|
|
2021-01-18 10:24:39 +00:00
|
|
|
return true;
|
2021-01-04 18:33:07 +00:00
|
|
|
}
|
|
|
|
|
|
|
|
vector<VariableDeclaration const*> vars;
|
|
|
|
} tryCatchVarsVisitor;
|
|
|
|
_function.accept(tryCatchVarsVisitor);
|
|
|
|
return tryCatchVarsVisitor.vars;
|
2020-11-04 21:06:30 +00:00
|
|
|
}
|
|
|
|
|
2020-12-15 14:50:02 +00:00
|
|
|
vector<VariableDeclaration const*> SMTEncoder::modifiersVariables(FunctionDefinition const& _function, ContractDefinition const* _contract)
|
2020-11-04 21:06:30 +00:00
|
|
|
{
|
|
|
|
struct BlockVars: ASTConstVisitor
|
|
|
|
{
|
|
|
|
BlockVars(Block const& _block) { _block.accept(*this); }
|
|
|
|
void endVisit(VariableDeclaration const& _var) { vars.push_back(&_var); }
|
|
|
|
vector<VariableDeclaration const*> vars;
|
|
|
|
};
|
|
|
|
|
|
|
|
vector<VariableDeclaration const*> vars;
|
|
|
|
set<ModifierDefinition const*> visited;
|
|
|
|
for (auto invok: _function.modifiers())
|
|
|
|
{
|
|
|
|
if (!invok)
|
|
|
|
continue;
|
2020-12-21 10:41:35 +00:00
|
|
|
auto const* modifier = resolveModifierInvocation(*invok, _contract);
|
2020-11-04 21:06:30 +00:00
|
|
|
if (!modifier || visited.count(modifier))
|
|
|
|
continue;
|
|
|
|
|
|
|
|
visited.insert(modifier);
|
2020-12-21 10:41:35 +00:00
|
|
|
if (modifier->isImplemented())
|
2020-12-14 17:23:07 +00:00
|
|
|
{
|
2020-12-21 10:41:35 +00:00
|
|
|
vars += applyMap(modifier->parameters(), [](auto _var) { return _var.get(); });
|
|
|
|
vars += BlockVars(modifier->body()).vars;
|
2020-12-14 17:23:07 +00:00
|
|
|
}
|
2020-11-04 21:06:30 +00:00
|
|
|
}
|
|
|
|
return vars;
|
|
|
|
}
|
|
|
|
|
2020-12-21 10:41:35 +00:00
|
|
|
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;
|
|
|
|
}
|
|
|
|
|
2021-01-25 17:17:56 +00:00
|
|
|
set<FunctionDefinition const*, ASTNode::CompareByID> const& SMTEncoder::contractFunctions(ContractDefinition const& _contract)
|
2020-12-21 17:17:56 +00:00
|
|
|
{
|
|
|
|
if (!m_contractFunctions.count(&_contract))
|
|
|
|
{
|
2021-01-25 17:17:56 +00:00
|
|
|
auto const& functions = _contract.definedFunctions();
|
|
|
|
set<FunctionDefinition const*, ASTNode::CompareByID> resolvedFunctions(begin(functions), end(functions));
|
2020-12-21 17:17:56 +00:00
|
|
|
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)
|
2021-01-25 17:17:56 +00:00
|
|
|
resolvedFunctions.insert(baseFunction);
|
2020-12-21 17:17:56 +00:00
|
|
|
}
|
|
|
|
}
|
|
|
|
m_contractFunctions.emplace(&_contract, move(resolvedFunctions));
|
|
|
|
}
|
|
|
|
return m_contractFunctions.at(&_contract);
|
|
|
|
}
|
|
|
|
|
2021-01-25 17:17:56 +00:00
|
|
|
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())
|
2021-03-03 19:24:05 +00:00
|
|
|
allFunctions.insert(baseFun);
|
2021-01-25 17:17:56 +00:00
|
|
|
|
|
|
|
m_contractFunctionsWithoutVirtual.emplace(&_contract, move(allFunctions));
|
|
|
|
|
|
|
|
}
|
|
|
|
return m_contractFunctionsWithoutVirtual.at(&_contract);
|
|
|
|
}
|
|
|
|
|
2020-09-02 08:45:47 +00:00
|
|
|
SourceUnit const* SMTEncoder::sourceUnitContaining(Scopable const& _scopable)
|
|
|
|
{
|
|
|
|
for (auto const* s = &_scopable; s; s = dynamic_cast<Scopable const*>(s->scope()))
|
|
|
|
if (auto const* source = dynamic_cast<SourceUnit const*>(s->scope()))
|
|
|
|
return source;
|
|
|
|
solAssert(false, "");
|
|
|
|
}
|
|
|
|
|
2020-11-09 15:37:08 +00:00
|
|
|
map<ContractDefinition const*, vector<ASTPointer<frontend::Expression>>> SMTEncoder::baseArguments(ContractDefinition const& _contract)
|
|
|
|
{
|
|
|
|
map<ContractDefinition const*, 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())
|
|
|
|
{
|
2020-12-07 12:30:09 +00:00
|
|
|
auto decl = mod->name().annotation().referencedDeclaration;
|
2020-11-09 15:37:08 +00:00
|
|
|
if (auto base = dynamic_cast<ContractDefinition const*>(decl))
|
|
|
|
{
|
|
|
|
solAssert(!baseArgs.count(base), "");
|
|
|
|
if (auto args = mod->arguments())
|
|
|
|
baseArgs[base] = *args;
|
|
|
|
}
|
|
|
|
}
|
|
|
|
}
|
|
|
|
|
|
|
|
return baseArgs;
|
|
|
|
}
|
|
|
|
|
2020-12-16 16:58:49 +00:00
|
|
|
RationalNumberType const* SMTEncoder::isConstant(Expression const& _expr)
|
2020-12-16 10:27:56 +00:00
|
|
|
{
|
2020-12-16 16:58:49 +00:00
|
|
|
if (auto type = dynamic_cast<RationalNumberType const*>(_expr.annotation().type))
|
2020-12-16 10:27:56 +00:00
|
|
|
return type;
|
|
|
|
|
|
|
|
// _expr may not be constant evaluable.
|
|
|
|
// In that case we ignore any warnings emitted by the constant evaluator,
|
|
|
|
// as it will return nullptr in case of failure.
|
|
|
|
ErrorList l;
|
|
|
|
ErrorReporter e(l);
|
2020-12-16 16:58:49 +00:00
|
|
|
if (auto t = ConstantEvaluator::evaluate(e, _expr))
|
|
|
|
return TypeProvider::rationalNumber(t->value);
|
|
|
|
|
|
|
|
return nullptr;
|
2020-12-16 10:27:56 +00:00
|
|
|
}
|
|
|
|
|
2020-12-08 20:14:18 +00:00
|
|
|
set<FunctionCall const*> 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::ABIEncodeWithSignature:
|
|
|
|
case FunctionType::Kind::ABIDecode:
|
|
|
|
abiCalls.insert(&_funCall);
|
|
|
|
break;
|
|
|
|
default: {}
|
|
|
|
}
|
|
|
|
}
|
|
|
|
|
|
|
|
set<FunctionCall const*> abiCalls;
|
|
|
|
};
|
|
|
|
|
|
|
|
return ABIFunctions(_node).abiCalls;
|
|
|
|
}
|
|
|
|
|
2021-04-07 16:53:56 +00:00
|
|
|
set<SourceUnit const*, ASTNode::CompareByID> SMTEncoder::sourceDependencies(SourceUnit const& _source)
|
|
|
|
{
|
|
|
|
set<SourceUnit const*, ASTNode::CompareByID> sources;
|
|
|
|
sources.insert(&_source);
|
|
|
|
for (auto const& source: _source.referencedSourceUnits(true))
|
|
|
|
sources.insert(source);
|
|
|
|
return sources;
|
|
|
|
}
|
|
|
|
|
2021-01-25 17:17:56 +00:00
|
|
|
void SMTEncoder::createReturnedExpressions(FunctionCall const& _funCall, ContractDefinition const* _contextContract)
|
2019-08-02 18:43:54 +00:00
|
|
|
{
|
2021-01-25 17:17:56 +00:00
|
|
|
auto funDef = functionCallToDefinition(_funCall, currentScopeContract(), _contextContract);
|
2019-08-02 18:43:54 +00:00
|
|
|
if (!funDef)
|
|
|
|
return;
|
|
|
|
|
|
|
|
auto const& returnParams = funDef->returnParameters();
|
|
|
|
for (auto param: returnParams)
|
|
|
|
createVariable(*param);
|
2021-03-16 12:11:24 +00:00
|
|
|
auto returnValues = applyMap(returnParams, [this](auto const& param) -> optional<smtutil::Expression> {
|
|
|
|
solAssert(param && m_context.knownVariable(*param), "");
|
|
|
|
return currentValue(*param);
|
|
|
|
});
|
|
|
|
defineExpr(_funCall, returnValues);
|
2019-08-02 18:43:54 +00:00
|
|
|
}
|
2020-02-12 01:11:28 +00:00
|
|
|
|
2021-01-25 17:17:56 +00:00
|
|
|
vector<smtutil::Expression> SMTEncoder::symbolicArguments(FunctionCall const& _funCall, ContractDefinition const* _contextContract)
|
2020-02-12 01:11:28 +00:00
|
|
|
{
|
2021-01-25 17:17:56 +00:00
|
|
|
auto funDef = functionCallToDefinition(_funCall, currentScopeContract(), _contextContract);
|
2020-12-22 19:25:31 +00:00
|
|
|
solAssert(funDef, "");
|
2020-02-12 01:11:28 +00:00
|
|
|
|
2020-05-19 12:14:46 +00:00
|
|
|
vector<smtutil::Expression> args;
|
2020-02-12 01:11:28 +00:00
|
|
|
Expression const* calledExpr = &_funCall.expression();
|
2020-12-22 19:25:31 +00:00
|
|
|
auto funType = dynamic_cast<FunctionType const*>(calledExpr->annotation().type);
|
2020-02-12 01:11:28 +00:00
|
|
|
solAssert(funType, "");
|
|
|
|
|
2020-11-09 13:09:34 +00:00
|
|
|
vector<ASTPointer<Expression const>> arguments = _funCall.sortedArguments();
|
2020-12-22 19:25:31 +00:00
|
|
|
auto functionParams = funDef->parameters();
|
2020-02-12 01:11:28 +00:00
|
|
|
unsigned firstParam = 0;
|
|
|
|
if (funType->bound())
|
|
|
|
{
|
2020-12-11 17:59:03 +00:00
|
|
|
calledExpr = innermostTuple(*calledExpr);
|
2020-02-12 01:11:28 +00:00
|
|
|
auto const& boundFunction = dynamic_cast<MemberAccess const*>(calledExpr);
|
|
|
|
solAssert(boundFunction, "");
|
|
|
|
args.push_back(expr(boundFunction->expression(), functionParams.front()->type()));
|
|
|
|
firstParam = 1;
|
|
|
|
}
|
|
|
|
|
|
|
|
solAssert((arguments.size() + firstParam) == functionParams.size(), "");
|
|
|
|
for (unsigned i = 0; i < arguments.size(); ++i)
|
|
|
|
args.push_back(expr(*arguments.at(i), functionParams.at(i + firstParam)->type()));
|
|
|
|
|
|
|
|
return args;
|
|
|
|
}
|
2021-02-03 10:31:17 +00:00
|
|
|
|
2021-04-07 12:52:56 +00:00
|
|
|
void SMTEncoder::collectFreeFunctions(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())
|
|
|
|
if (!function->isPublic())
|
|
|
|
m_freeFunctions.insert(function);
|
|
|
|
}
|
|
|
|
}
|
|
|
|
|
2021-04-07 16:53:56 +00:00
|
|
|
void SMTEncoder::createFreeConstants(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);
|
2021-08-10 16:30:11 +00:00
|
|
|
else if (
|
|
|
|
auto contract = dynamic_cast<ContractDefinition const*>(node.get());
|
|
|
|
contract && contract->isLibrary()
|
|
|
|
)
|
|
|
|
for (auto var: contract->stateVariables())
|
|
|
|
{
|
|
|
|
solAssert(var->isConstant(), "");
|
|
|
|
createVariable(*var);
|
|
|
|
}
|
2021-04-07 16:53:56 +00:00
|
|
|
}
|
|
|
|
|
2021-02-03 10:31:17 +00:00
|
|
|
smt::SymbolicState& SMTEncoder::state()
|
|
|
|
{
|
|
|
|
return m_context.state();
|
|
|
|
}
|