From a86f6567046d1a5781208b52d41ca5dbbd9b9ff3 Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Mon, 7 Sep 2020 16:45:14 +0200 Subject: [PATCH 1/3] Refactor state as tuple --- libsolidity/formal/SymbolicState.cpp | 76 ++++++++++++++++++++++------ libsolidity/formal/SymbolicState.h | 46 +++++++++++------ 2 files changed, 91 insertions(+), 31 deletions(-) diff --git a/libsolidity/formal/SymbolicState.cpp b/libsolidity/formal/SymbolicState.cpp index 40fac322d..d51d68162 100644 --- a/libsolidity/formal/SymbolicState.cpp +++ b/libsolidity/formal/SymbolicState.cpp @@ -16,24 +16,42 @@ */ // SPDX-License-Identifier: GPL-3.0 +#include "libsmtutil/SolverInterface.h" #include +#include #include using namespace std; using namespace solidity; +using namespace solidity::smtutil; using namespace solidity::frontend::smt; SymbolicState::SymbolicState(EncodingContext& _context): m_context(_context) { + m_stateMembers.emplace("balances", make_shared(smtutil::SortProvider::uintSort, smtutil::SortProvider::uintSort)); + + vector members; + vector sorts; + for (auto const& [component, sort]: m_stateMembers) + { + members.emplace_back(component); + sorts.emplace_back(sort); + m_componentIndices[component] = members.size() - 1; + } + m_stateTuple = make_unique( + make_shared("state_type", members, sorts), + "state", + m_context + ); } void SymbolicState::reset() { - m_thisAddress.resetIndex(); - m_balances.resetIndex(); m_error.resetIndex(); + m_thisAddress.resetIndex(); + m_stateTuple->resetIndex(); } // Blockchain @@ -43,14 +61,19 @@ smtutil::Expression SymbolicState::thisAddress() return m_thisAddress.currentValue(); } +smtutil::Expression SymbolicState::balances() +{ + return m_stateTuple->component(m_componentIndices.at("balances")); +} + smtutil::Expression SymbolicState::balance() { - return balance(m_thisAddress.currentValue()); + return balance(thisAddress()); } smtutil::Expression SymbolicState::balance(smtutil::Expression _address) { - return smtutil::Expression::select(m_balances.elements(), move(_address)); + return smtutil::Expression::select(balances(), move(_address)); } SymbolicIntVariable& SymbolicState::errorFlag() @@ -58,21 +81,31 @@ SymbolicIntVariable& SymbolicState::errorFlag() return m_error; } +smtutil::Expression SymbolicState::state() +{ + return m_stateTuple->currentValue(); +} + +SortPointer SymbolicState::stateSort() +{ + return m_stateTuple->sort(); +} + void SymbolicState::transfer(smtutil::Expression _from, smtutil::Expression _to, smtutil::Expression _value) { - unsigned indexBefore = m_balances.index(); + unsigned indexBefore = m_stateTuple->index(); addBalance(_from, 0 - _value); addBalance(_to, move(_value)); - unsigned indexAfter = m_balances.index(); + unsigned indexAfter = m_stateTuple->index(); solAssert(indexAfter > indexBefore, ""); - m_balances.increaseIndex(); + m_stateTuple->increaseIndex(); /// Do not apply the transfer operation if _from == _to. - auto newBalances = smtutil::Expression::ite( + auto newState = smtutil::Expression::ite( move(_from) == move(_to), - m_balances.valueAtIndex(indexBefore), - m_balances.valueAtIndex(indexAfter) + m_stateTuple->valueAtIndex(indexBefore), + m_stateTuple->valueAtIndex(indexAfter) ); - m_context.addAssertion(m_balances.currentValue() == newBalances); + m_context.addAssertion(m_stateTuple->currentValue() == newState); } /// Private helpers. @@ -80,13 +113,24 @@ void SymbolicState::transfer(smtutil::Expression _from, smtutil::Expression _to, void SymbolicState::addBalance(smtutil::Expression _address, smtutil::Expression _value) { auto newBalances = smtutil::Expression::store( - m_balances.elements(), + balances(), _address, balance(_address) + move(_value) ); - auto oldLength = m_balances.length(); - m_balances.increaseIndex(); - m_context.addAssertion(m_balances.elements() == newBalances); - m_context.addAssertion(m_balances.length() == oldLength); + assignStateMember("balances", newBalances); } +smtutil::Expression SymbolicState::assignStateMember(string const& _member, smtutil::Expression const& _value) +{ + vector args; + for (auto const& member: m_stateMembers) + if (member.first == _member) + args.emplace_back(_value); + else + args.emplace_back(m_stateTuple->component(m_componentIndices.at(member.first))); + m_stateTuple->increaseIndex(); + auto tuple = m_stateTuple->currentValue(); + auto sortExpr = smtutil::Expression(make_shared(tuple.sort), tuple.name); + m_context.addAssertion(tuple == smtutil::Expression::tuple_constructor(sortExpr, args)); + return m_stateTuple->currentValue(); +} diff --git a/libsolidity/formal/SymbolicState.h b/libsolidity/formal/SymbolicState.h index e11dc3840..9878e1926 100644 --- a/libsolidity/formal/SymbolicState.h +++ b/libsolidity/formal/SymbolicState.h @@ -27,9 +27,17 @@ namespace solidity::frontend::smt { class EncodingContext; +class SymbolicAddressVariable; +class SymbolicArrayVariable; /** - * Symbolic representation of the blockchain state. + * Symbolic representation of the blockchain context: + * - error flag + * - this (the address of the currently executing contract) + * - state, represented as a tuple of: + * - balances + * - TODO: potentially storage of contracts + * - TODO transaction variables */ class SymbolicState { @@ -42,6 +50,8 @@ public: //@{ /// Value of `this` address. smtutil::Expression thisAddress(); + /// @returns the symbolic balances. + smtutil::Expression balances(); /// @returns the symbolic balance of address `this`. smtutil::Expression balance(); /// @returns the symbolic balance of an address. @@ -49,6 +59,12 @@ public: SymbolicIntVariable& errorFlag(); + /// @returns the state as a tuple. + smtutil::Expression state(); + + /// @returns the state sort. + smtutil::SortPointer stateSort(); + /// Transfer _value from _from to _to. void transfer(smtutil::Expression _from, smtutil::Expression _to, smtutil::Expression _value); //@} @@ -57,27 +73,27 @@ private: /// Adds _value to _account's balance. void addBalance(smtutil::Expression _account, smtutil::Expression _value); + /// Generates a new tuple where _member is assigned _value. + smtutil::Expression assignStateMember(std::string const& _member, smtutil::Expression const& _value); + EncodingContext& m_context; - /// Symbolic `this` address. - SymbolicAddressVariable m_thisAddress{ - "this", - m_context - }; - - /// Symbolic balances. - SymbolicArrayVariable m_balances{ - std::make_shared(smtutil::SortProvider::uintSort, smtutil::SortProvider::uintSort), - "balances", - m_context - }; - - smt::SymbolicIntVariable m_error{ + SymbolicIntVariable m_error{ TypeProvider::uint256(), TypeProvider::uint256(), "error", m_context }; + + SymbolicAddressVariable m_thisAddress{ + "this", + m_context + }; + + std::map m_componentIndices; + /// balances, TODO storage of other contracts + std::map m_stateMembers; + std::unique_ptr m_stateTuple; }; } From 18cf01c1872143f0f9857abcec8d2b952d990943 Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Fri, 18 Sep 2020 18:55:23 +0200 Subject: [PATCH 2/3] Add this and state to CHC --- libsolidity/formal/BMC.cpp | 3 +- libsolidity/formal/CHC.cpp | 69 ++++++++++++------- libsolidity/formal/CHC.h | 1 + libsolidity/formal/Predicate.cpp | 20 +++--- libsolidity/formal/PredicateInstance.cpp | 44 ++++++++---- libsolidity/formal/PredicateInstance.h | 4 ++ libsolidity/formal/PredicateSort.cpp | 31 +++++---- libsolidity/formal/PredicateSort.h | 26 +++---- libsolidity/formal/SMTEncoder.cpp | 1 + libsolidity/formal/SymbolicState.cpp | 56 ++++++++++----- libsolidity/formal/SymbolicState.h | 22 +++--- ...rray_struct_array_struct_memory_unsafe.sol | 2 - 12 files changed, 180 insertions(+), 99 deletions(-) diff --git a/libsolidity/formal/BMC.cpp b/libsolidity/formal/BMC.cpp index 158b3301d..eb552545d 100644 --- a/libsolidity/formal/BMC.cpp +++ b/libsolidity/formal/BMC.cpp @@ -396,7 +396,6 @@ void BMC::endVisit(FunctionCall const& _funCall) case FunctionType::Kind::Send: case FunctionType::Kind::Transfer: { - SMTEncoder::endVisit(_funCall); auto value = _funCall.arguments().front(); solAssert(value, ""); smtutil::Expression thisBalance = m_context.state().balance(); @@ -406,6 +405,8 @@ void BMC::endVisit(FunctionCall const& _funCall) thisBalance < expr(*value), &_funCall ); + + SMTEncoder::endVisit(_funCall); break; } case FunctionType::Kind::AddMod: diff --git a/libsolidity/formal/CHC.cpp b/libsolidity/formal/CHC.cpp index bb7382565..f959c0fed 100644 --- a/libsolidity/formal/CHC.cpp +++ b/libsolidity/formal/CHC.cpp @@ -101,7 +101,7 @@ bool CHC::visit(ContractDefinition const& _contract) solAssert(m_currentContract, ""); m_constructorSummaryPredicate = createSymbolicBlock( - constructorSort(*m_currentContract), + constructorSort(*m_currentContract, state()), "summary_constructor_" + contractSuffix(_contract), PredicateType::ConstructorSummary, &_contract @@ -114,15 +114,16 @@ bool CHC::visit(ContractDefinition const& _contract) void CHC::endVisit(ContractDefinition const& _contract) { auto implicitConstructorPredicate = createSymbolicBlock( - implicitConstructorSort(), + implicitConstructorSort(state()), "implicit_constructor_" + contractSuffix(_contract), PredicateType::ImplicitConstructor, &_contract ); - auto implicitConstructor = (*implicitConstructorPredicate)({}); - addRule(implicitConstructor, implicitConstructor.name); - m_currentBlock = implicitConstructor; - m_context.addAssertion(errorFlag().currentValue() == 0); + addRule( + (*implicitConstructorPredicate)({0, state().thisAddress(), state().state()}), + implicitConstructorPredicate->functor().name + ); + setCurrentBlock(*implicitConstructorPredicate); if (auto constructor = _contract.constructor()) constructor->accept(*this); @@ -178,6 +179,7 @@ bool CHC::visit(FunctionDefinition const& _function) m_context.addAssertion(m_context.variable(*var)->valueAtIndex(0) == currentValue(*var)); for (auto const& var: _function.parameters()) m_context.addAssertion(m_context.variable(*var)->valueAtIndex(0) == currentValue(*var)); + m_context.addAssertion(state().state(0) == state().state()); connectBlocks(functionPred, bodyPred); @@ -215,7 +217,7 @@ void CHC::endVisit(FunctionDefinition const& _function) string suffix = m_currentContract->name() + "_" + to_string(m_currentContract->id()); solAssert(m_currentContract, ""); auto constructorExit = createSymbolicBlock( - constructorSort(*m_currentContract), + constructorSort(*m_currentContract, state()), "constructor_exit_" + suffix, PredicateType::ConstructorSummary, m_currentContract @@ -234,7 +236,7 @@ void CHC::endVisit(FunctionDefinition const& _function) setCurrentBlock(*m_interfaces.at(m_currentContract)); - auto ifacePre = (*m_interfaces.at(m_currentContract))(initialStateVariables()); + auto ifacePre = smt::interfacePre(*m_interfaces.at(m_currentContract), *m_currentContract, m_context); if (_function.isPublic()) { addAssertVerificationTarget(&_function, ifacePre, sum, assertionError); @@ -598,15 +600,21 @@ void CHC::externalFunctionCall(FunctionCall const& _funCall) for (auto var: function->returnParameters()) m_context.variable(*var)->increaseIndex(); - auto preCallState = currentStateVariables(); + auto preCallState = vector{state().state()} + currentStateVariables(); bool usesStaticCall = kind == FunctionType::Kind::BareStaticCall || function->stateMutability() == StateMutability::Pure || function->stateMutability() == StateMutability::View; if (!usesStaticCall) + { + state().newState(); for (auto const* var: m_stateVariables) m_context.variable(*var)->increaseIndex(); + } - auto nondet = (*m_nondetInterfaces.at(m_currentContract))(preCallState + currentStateVariables()); + auto postCallState = vector{state().state()} + currentStateVariables(); + auto nondet = (*m_nondetInterfaces.at(m_currentContract))(preCallState + postCallState); + // TODO this could instead add the summary of the called function, where that summary + // basically has the nondet interface of this summary as a constraint. m_context.addAssertion(nondet); m_context.addAssertion(errorFlag().currentValue() == 0); @@ -775,6 +783,8 @@ void CHC::clearIndices(ContractDefinition const* _contract, FunctionDefinition c for (auto const& var: _function->localVariables()) m_context.variable(*var)->increaseIndex(); } + + state().newState(); } void CHC::setCurrentBlock(Predicate const& _block) @@ -800,7 +810,7 @@ set CHC::transactionAssertions(ASTN SortPointer CHC::sort(FunctionDefinition const& _function) { - return functionSort(_function, m_currentContract); + return functionSort(_function, m_currentContract, state()); } SortPointer CHC::sort(ASTNode const* _node) @@ -809,7 +819,7 @@ SortPointer CHC::sort(ASTNode const* _node) return sort(*funDef); solAssert(m_currentFunction, ""); - return functionBodySort(*m_currentFunction, m_currentContract); + return functionBodySort(*m_currentFunction, m_currentContract, state()); } Predicate const* CHC::createSymbolicBlock(SortPointer _sort, string const& _name, PredicateType _predType, ASTNode const* _node) @@ -825,8 +835,8 @@ void CHC::defineInterfacesAndSummaries(SourceUnit const& _source) if (auto const* contract = dynamic_cast(node.get())) { string suffix = contract->name() + "_" + to_string(contract->id()); - m_interfaces[contract] = createSymbolicBlock(interfaceSort(*contract), "interface_" + suffix, PredicateType::Interface, contract); - m_nondetInterfaces[contract] = createSymbolicBlock(nondetInterfaceSort(*contract), "nondet_interface_" + suffix, PredicateType::NondetInterface, contract); + m_interfaces[contract] = createSymbolicBlock(interfaceSort(*contract, state()), "interface_" + suffix, PredicateType::Interface, contract); + m_nondetInterfaces[contract] = createSymbolicBlock(nondetInterfaceSort(*contract, state()), "nondet_interface_" + suffix, PredicateType::NondetInterface, contract); for (auto const* var: stateVariablesIncludingInheritedAndPrivate(*contract)) if (!m_context.knownVariable(*var)) @@ -836,8 +846,7 @@ void CHC::defineInterfacesAndSummaries(SourceUnit const& _source) /// 0 steps to be taken, used as base for the inductive /// rule for each function. auto const& iface = *m_nondetInterfaces.at(contract); - auto state0 = stateVariablesAtIndex(0, *contract); - addRule(iface(state0 + state0), "base_nondet"); + addRule(smt::nondetInterface(iface, *contract, m_context, 0, 0), "base_nondet"); for (auto const* base: contract->annotation().linearizedBaseContracts) for (auto const* function: base->definedFunctions()) @@ -861,12 +870,13 @@ void CHC::defineInterfacesAndSummaries(SourceUnit const& _source) auto state1 = stateVariablesAtIndex(1, *contract); auto state2 = stateVariablesAtIndex(2, *contract); - auto nondetPre = iface(state0 + state1); - auto nondetPost = iface(state0 + state2); + auto nondetPre = smt::nondetInterface(iface, *contract, m_context, 0, 1); + auto nondetPost = smt::nondetInterface(iface, *contract, m_context, 0, 2); - vector args{errorFlag().currentValue()}; + vector args{errorFlag().currentValue(), state().thisAddress(), state().state(1)}; args += state1 + applyMap(function->parameters(), [this](auto _var) { return valueAtIndex(*_var, 0); }) + + vector{state().state(2)} + state2 + applyMap(function->parameters(), [this](auto _var) { return valueAtIndex(*_var, 1); }) + applyMap(function->returnParameters(), [this](auto _var) { return valueAtIndex(*_var, 1); }); @@ -930,7 +940,7 @@ Predicate const* CHC::createBlock(ASTNode const* _node, PredicateType _predType, Predicate const* CHC::createSummaryBlock(FunctionDefinition const& _function, ContractDefinition const& _contract) { auto block = createSymbolicBlock( - functionSort(_function, &_contract), + functionSort(_function, &_contract, state()), "summary_" + uniquePrefix() + "_" + predicateName(&_function, &_contract), PredicateType::FunctionSummary, &_function @@ -1042,7 +1052,7 @@ smtutil::Expression CHC::predicate(FunctionCall const& _funCall) return smtutil::Expression(true); errorFlag().increaseIndex(); - vector args{errorFlag().currentValue()}; + vector args{errorFlag().currentValue(), state().thisAddress(), state().state()}; FunctionType const& funType = dynamic_cast(*_funCall.expression().annotation().type); solAssert(funType.kind() == FunctionType::Kind::Internal, ""); @@ -1058,11 +1068,17 @@ smtutil::Expression CHC::predicate(FunctionCall const& _funCall) auto const* calledContract = contract->isLibrary() ? contract : m_currentContract; solAssert(calledContract, ""); + bool usesStaticCall = function->stateMutability() == StateMutability::Pure || function->stateMutability() == StateMutability::View; + args += currentStateVariables(*calledContract); args += symbolicArguments(_funCall); - if (!calledContract->isLibrary()) + if (!calledContract->isLibrary() && !usesStaticCall) + { + state().newState(); for (auto const& var: m_stateVariables) m_context.variable(*var)->increaseIndex(); + } + args += vector{state().state()}; args += currentStateVariables(*calledContract); for (auto var: function->parameters() + function->returnParameters()) @@ -1152,7 +1168,7 @@ void CHC::addVerificationTarget(ASTNode const* _scope, VerificationTarget::Type addVerificationTarget(_scope, _type, summary(*m_currentContract), smtutil::Expression(true), _errorId); else { - auto iface = (*m_interfaces.at(m_currentContract))(initialStateVariables()); + auto iface = smt::interfacePre(*m_interfaces.at(m_currentContract), *m_currentContract, m_context); auto sum = summary(*m_currentFunction); addVerificationTarget(_scope, _type, iface, sum, _errorId); } @@ -1444,7 +1460,12 @@ unsigned CHC::newErrorId(frontend::Expression const& _expr) return errorId; } +SymbolicState& CHC::state() +{ + return m_context.state(); +} + SymbolicIntVariable& CHC::errorFlag() { - return m_context.state().errorFlag(); + return state().errorFlag(); } diff --git a/libsolidity/formal/CHC.h b/libsolidity/formal/CHC.h index e76f75c89..b47043781 100644 --- a/libsolidity/formal/CHC.h +++ b/libsolidity/formal/CHC.h @@ -235,6 +235,7 @@ private: /// it into m_errorIds. unsigned newErrorId(Expression const& _expr); + smt::SymbolicState& state(); smt::SymbolicIntVariable& errorFlag(); //@} diff --git a/libsolidity/formal/Predicate.cpp b/libsolidity/formal/Predicate.cpp index 9d3f856ce..ca77c3d8d 100644 --- a/libsolidity/formal/Predicate.cpp +++ b/libsolidity/formal/Predicate.cpp @@ -161,9 +161,9 @@ string Predicate::formatSummaryCall(vector const& _args) const auto const* fun = programFunction(); solAssert(fun, ""); - /// The signature of a function summary predicate is: summary(error, preStateVars, preInputVars, postStateVars, postInputVars, outputVars). + /// The signature of a function summary predicate is: summary(error, this, preBlockChainState, preStateVars, preInputVars, postBlockchainState, postStateVars, postInputVars, outputVars). /// Here we are interested in preInputVars. - vector::const_iterator first = _args.begin() + static_cast(stateVars->size()) + 1; + vector::const_iterator first = _args.begin() + 3 + static_cast(stateVars->size()); vector::const_iterator last = first + static_cast(fun->parameters().size()); solAssert(first >= _args.begin() && first <= _args.end(), ""); solAssert(last >= _args.begin() && last <= _args.end(), ""); @@ -188,8 +188,8 @@ string Predicate::formatSummaryCall(vector const& _args) const vector Predicate::summaryStateValues(vector const& _args) const { - /// The signature of a function summary predicate is: summary(error, preStateVars, preInputVars, postStateVars, postInputVars, outputVars). - /// The signature of an implicit constructor summary predicate is: summary(error, postStateVars). + /// The signature of a function summary predicate is: summary(error, this, preBlockchainState, preStateVars, preInputVars, postBlockchainState, postStateVars, postInputVars, outputVars). + /// The signature of an implicit constructor summary predicate is: summary(error, this, postBlockchainState, postStateVars). /// Here we are interested in postStateVars. auto stateVars = stateVariables(); @@ -199,12 +199,12 @@ vector Predicate::summaryStateValues(vector const& _args) const vector::const_iterator stateLast; if (auto const* function = programFunction()) { - stateFirst = _args.begin() + 1 + static_cast(stateVars->size()) + static_cast(function->parameters().size()); + stateFirst = _args.begin() + 3 + static_cast(stateVars->size()) + static_cast(function->parameters().size()) + 1; stateLast = stateFirst + static_cast(stateVars->size()); } else if (programContract()) { - stateFirst = _args.begin() + 1; + stateFirst = _args.begin() + 3; stateLast = stateFirst + static_cast(stateVars->size()); } else @@ -220,7 +220,7 @@ vector Predicate::summaryStateValues(vector const& _args) const vector Predicate::summaryPostInputValues(vector const& _args) const { - /// The signature of a function summary predicate is: summary(error, preStateVars, preInputVars, postStateVars, postInputVars, outputVars). + /// The signature of a function summary predicate is: summary(error, this, preBlockchainState, preStateVars, preInputVars, postBlockchainState, postStateVars, postInputVars, outputVars). /// Here we are interested in postInputVars. auto const* function = programFunction(); solAssert(function, ""); @@ -230,7 +230,7 @@ vector Predicate::summaryPostInputValues(vector const& _args) co auto const& inParams = function->parameters(); - vector::const_iterator first = _args.begin() + 1 + static_cast(stateVars->size()) * 2 + static_cast(inParams.size()); + vector::const_iterator first = _args.begin() + 3 + static_cast(stateVars->size()) * 2 + static_cast(inParams.size()) + 1; vector::const_iterator last = first + static_cast(inParams.size()); solAssert(first >= _args.begin() && first <= _args.end(), ""); @@ -243,7 +243,7 @@ vector Predicate::summaryPostInputValues(vector const& _args) co vector Predicate::summaryPostOutputValues(vector const& _args) const { - /// The signature of a function summary predicate is: summary(error, preStateVars, preInputVars, postStateVars, postInputVars, outputVars). + /// The signature of a function summary predicate is: summary(error, this, preBlockchainState, preStateVars, preInputVars, postBlockchainState, postStateVars, postInputVars, outputVars). /// Here we are interested in outputVars. auto const* function = programFunction(); solAssert(function, ""); @@ -253,7 +253,7 @@ vector Predicate::summaryPostOutputValues(vector const& _args) c auto const& inParams = function->parameters(); - vector::const_iterator first = _args.begin() + 1 + static_cast(stateVars->size()) * 2 + static_cast(inParams.size()) * 2; + vector::const_iterator first = _args.begin() + 3 + static_cast(stateVars->size()) * 2 + static_cast(inParams.size()) * 2 + 1; solAssert(first >= _args.begin() && first <= _args.end(), ""); diff --git a/libsolidity/formal/PredicateInstance.cpp b/libsolidity/formal/PredicateInstance.cpp index 8bece398e..601891c5a 100644 --- a/libsolidity/formal/PredicateInstance.cpp +++ b/libsolidity/formal/PredicateInstance.cpp @@ -27,10 +27,35 @@ using namespace solidity::smtutil; namespace solidity::frontend::smt { +smtutil::Expression interfacePre(Predicate const& _pred, ContractDefinition const& _contract, EncodingContext& _context) +{ + auto& state = _context.state(); + vector stateExprs{state.thisAddress(0), state.state(0)}; + return _pred(stateExprs + initialStateVariables(_contract, _context)); +} smtutil::Expression interface(Predicate const& _pred, ContractDefinition const& _contract, EncodingContext& _context) { - return _pred(currentStateVariables(_contract, _context)); + auto& state = _context.state(); + vector stateExprs{state.thisAddress(0), state.state()}; + return _pred(stateExprs + currentStateVariables(_contract, _context)); +} + +smtutil::Expression nondetInterface(Predicate const& _pred, ContractDefinition const& _contract, EncodingContext& _context, unsigned _preIdx, unsigned _postIdx) +{ + return _pred( + vector{_context.state().state(_preIdx)} + + stateVariablesAtIndex(_preIdx, _contract, _context) + + vector{_context.state().state(_postIdx)} + + stateVariablesAtIndex(_postIdx, _contract, _context) + ); +} + +smtutil::Expression implicitConstructor(Predicate const& _pred, ContractDefinition const&, EncodingContext& _context) +{ + auto& state = _context.state(); + vector stateExprs{state.errorFlag().currentValue(), state.thisAddress(0), state.state(0)}; + return _pred(stateExprs); } smtutil::Expression constructor(Predicate const& _pred, ContractDefinition const& _contract, EncodingContext& _context) @@ -38,16 +63,9 @@ smtutil::Expression constructor(Predicate const& _pred, ContractDefinition const if (auto const* constructor = _contract.constructor()) return _pred(currentFunctionVariables(*constructor, &_contract, _context)); - return _pred( - vector{_context.state().errorFlag().currentValue()} + - currentStateVariables(_contract, _context) - ); -} - -/// Currently it does not have arguments but it will have tx data in the future. -smtutil::Expression implicitConstructor(Predicate const& _pred, ContractDefinition const&, EncodingContext&) -{ - return _pred({}); + auto& state = _context.state(); + vector stateExprs{state.errorFlag().currentValue(), state.thisAddress(0), state.state()}; + return _pred(stateExprs + currentStateVariables(_contract, _context)); } smtutil::Expression function( @@ -99,9 +117,11 @@ vector currentFunctionVariables( EncodingContext& _context ) { - vector exprs{_context.state().errorFlag().currentValue()}; + auto& state = _context.state(); + vector exprs{_context.state().errorFlag().currentValue(), state.thisAddress(0), state.state(0)}; exprs += _contract ? initialStateVariables(*_contract, _context) : vector{}; exprs += applyMap(_function.parameters(), [&](auto _var) { return _context.variable(*_var)->valueAtIndex(0); }); + exprs += vector{state.state()}; exprs += _contract ? currentStateVariables(*_contract, _context) : vector{}; exprs += applyMap(_function.parameters(), [&](auto _var) { return _context.variable(*_var)->currentValue(); }); exprs += applyMap(_function.returnParameters(), [&](auto _var) { return _context.variable(*_var)->currentValue(); }); diff --git a/libsolidity/formal/PredicateInstance.h b/libsolidity/formal/PredicateInstance.h index 185807e5e..6e287eac8 100644 --- a/libsolidity/formal/PredicateInstance.h +++ b/libsolidity/formal/PredicateInstance.h @@ -30,8 +30,12 @@ class EncodingContext; * The predicates follow the specification in PredicateSort.h. * */ +smtutil::Expression interfacePre(Predicate const& _pred, ContractDefinition const& _contract, EncodingContext& _context); + smtutil::Expression interface(Predicate const& _pred, ContractDefinition const& _contract, EncodingContext& _context); +smtutil::Expression nondetInterface(Predicate const& _pred, ContractDefinition const& _contract, EncodingContext& _context, unsigned _preIdx, unsigned _postIdx); + smtutil::Expression constructor(Predicate const& _pred, ContractDefinition const& _contract, EncodingContext& _context); smtutil::Expression implicitConstructor(Predicate const& _pred, ContractDefinition const& _contract, EncodingContext& _context); diff --git a/libsolidity/formal/PredicateSort.cpp b/libsolidity/formal/PredicateSort.cpp index ffef00f0c..5bcc5efcb 100644 --- a/libsolidity/formal/PredicateSort.cpp +++ b/libsolidity/formal/PredicateSort.cpp @@ -28,49 +28,54 @@ using namespace solidity::smtutil; namespace solidity::frontend::smt { -SortPointer interfaceSort(ContractDefinition const& _contract) +SortPointer interfaceSort(ContractDefinition const& _contract, SymbolicState& _state) { return make_shared( - stateSorts(_contract), + vector{_state.thisAddressSort(), _state.stateSort()} + stateSorts(_contract), SortProvider::boolSort ); } -SortPointer nondetInterfaceSort(ContractDefinition const& _contract) +SortPointer nondetInterfaceSort(ContractDefinition const& _contract, SymbolicState& _state) { auto varSorts = stateSorts(_contract); + vector stateSort{_state.stateSort()}; return make_shared( - varSorts + varSorts, + stateSort + varSorts + stateSort + varSorts, SortProvider::boolSort ); } -SortPointer implicitConstructorSort() +SortPointer implicitConstructorSort(SymbolicState& _state) { - return arity0FunctionSort(); + return make_shared( + vector{_state.errorFlagSort(), _state.thisAddressSort(), _state.stateSort()}, + SortProvider::boolSort + ); } -SortPointer constructorSort(ContractDefinition const& _contract) +SortPointer constructorSort(ContractDefinition const& _contract, SymbolicState& _state) { if (auto const* constructor = _contract.constructor()) - return functionSort(*constructor, &_contract); + return functionSort(*constructor, &_contract, _state); return make_shared( - vector{SortProvider::uintSort} + stateSorts(_contract), + vector{_state.errorFlagSort(), _state.thisAddressSort(), _state.stateSort()} + stateSorts(_contract), SortProvider::boolSort ); } -SortPointer functionSort(FunctionDefinition const& _function, ContractDefinition const* _contract) +SortPointer functionSort(FunctionDefinition const& _function, ContractDefinition const* _contract, SymbolicState& _state) { auto smtSort = [](auto _var) { return smt::smtSortAbstractFunction(*_var->type()); }; auto varSorts = _contract ? stateSorts(*_contract) : vector{}; auto inputSorts = applyMap(_function.parameters(), smtSort); auto outputSorts = applyMap(_function.returnParameters(), smtSort); return make_shared( - vector{SortProvider::uintSort} + + vector{_state.errorFlagSort(), _state.thisAddressSort(), _state.stateSort()} + varSorts + inputSorts + + vector{_state.stateSort()} + varSorts + inputSorts + outputSorts, @@ -78,9 +83,9 @@ SortPointer functionSort(FunctionDefinition const& _function, ContractDefinition ); } -SortPointer functionBodySort(FunctionDefinition const& _function, ContractDefinition const* _contract) +SortPointer functionBodySort(FunctionDefinition const& _function, ContractDefinition const* _contract, SymbolicState& _state) { - auto fSort = dynamic_pointer_cast(functionSort(_function, _contract)); + auto fSort = dynamic_pointer_cast(functionSort(_function, _contract, _state)); solAssert(fSort, ""); auto smtSort = [](auto _var) { return smt::smtSortAbstractFunction(*_var->type()); }; diff --git a/libsolidity/formal/PredicateSort.h b/libsolidity/formal/PredicateSort.h index 04d5226c6..a2f25e7e4 100644 --- a/libsolidity/formal/PredicateSort.h +++ b/libsolidity/formal/PredicateSort.h @@ -20,6 +20,8 @@ #include +#include + #include namespace solidity::frontend::smt @@ -31,46 +33,46 @@ namespace solidity::frontend::smt * * 1. Interface * The idle state of a contract. Signature: - * interface(stateVariables). + * interface(this, blockchainState, stateVariables). * * 2. Nondet interface * The nondeterminism behavior of a contract. Signature: - * nondet_interface(stateVariables, stateVariables'). + * nondet_interface(blockchainState, stateVariables, blockchainState', stateVariables'). * * 3. Implicit constructor * The implicit constructor of a contract, that is, without input parameters. Signature: - * implicit_constructor(). + * implicit_constructor(error, this, blockchainState). * * 4. Constructor entry/summary * The summary of an implicit constructor. Signature: - * constructor_summary(error, stateVariables'). + * constructor_summary(error, this, blockchainState, blockchainState', stateVariables'). * * 5. Function entry/summary * The entry point of a function definition. Signature: - * function_entry(error, stateVariables, inputVariables, stateVariables', inputVariables', outputVariables'). + * function_entry(error, this, blockchainState, stateVariables, inputVariables, blockchainState', stateVariables', inputVariables', outputVariables'). * * 6. Function body * Use for any predicate within a function. Signature: - * function_body(error, stateVariables, inputVariables, stateVariables', inputVariables', outputVariables', localVariables). + * function_body(error, this, blockchainState, stateVariables, inputVariables, blockchainState' ,stateVariables', inputVariables', outputVariables', localVariables). */ /// @returns the interface predicate sort for _contract. -smtutil::SortPointer interfaceSort(ContractDefinition const& _contract); +smtutil::SortPointer interfaceSort(ContractDefinition const& _contract, SymbolicState& _state); /// @returns the nondeterminisc interface predicate sort for _contract. -smtutil::SortPointer nondetInterfaceSort(ContractDefinition const& _contract); +smtutil::SortPointer nondetInterfaceSort(ContractDefinition const& _contract, SymbolicState& _state); /// @returns the implicit constructor predicate sort. -smtutil::SortPointer implicitConstructorSort(); +smtutil::SortPointer implicitConstructorSort(SymbolicState& _state); /// @returns the constructor entry/summary predicate sort for _contract. -smtutil::SortPointer constructorSort(ContractDefinition const& _contract); +smtutil::SortPointer constructorSort(ContractDefinition const& _contract, SymbolicState& _state); /// @returns the function entry/summary predicate sort for _function contained in _contract. -smtutil::SortPointer functionSort(FunctionDefinition const& _function, ContractDefinition const* _contract); +smtutil::SortPointer functionSort(FunctionDefinition const& _function, ContractDefinition const* _contract, SymbolicState& _state); /// @returns the function body predicate sort for _function contained in _contract. -smtutil::SortPointer functionBodySort(FunctionDefinition const& _function, ContractDefinition const* _contract); +smtutil::SortPointer functionBodySort(FunctionDefinition const& _function, ContractDefinition const* _contract, SymbolicState& _state); /// @returns the sort of a predicate without parameters. smtutil::SortPointer arity0FunctionSort(); diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp index 2b42b6c79..118cb5308 100644 --- a/libsolidity/formal/SMTEncoder.cpp +++ b/libsolidity/formal/SMTEncoder.cpp @@ -2162,6 +2162,7 @@ void SMTEncoder::clearIndices(ContractDefinition const* _contract, FunctionDefin for (auto const& var: _function->localVariables()) m_context.variable(*var)->resetIndex(); } + m_context.state().reset(); } Expression const* SMTEncoder::leftmostBase(IndexAccess const& _indexAccess) diff --git a/libsolidity/formal/SymbolicState.cpp b/libsolidity/formal/SymbolicState.cpp index d51d68162..9f4dfe5c7 100644 --- a/libsolidity/formal/SymbolicState.cpp +++ b/libsolidity/formal/SymbolicState.cpp @@ -16,7 +16,6 @@ */ // SPDX-License-Identifier: GPL-3.0 -#include "libsmtutil/SolverInterface.h" #include #include @@ -56,11 +55,51 @@ void SymbolicState::reset() // Blockchain +SymbolicIntVariable& SymbolicState::errorFlag() +{ + return m_error; +} + +SortPointer SymbolicState::errorFlagSort() +{ + return m_error.sort(); +} + smtutil::Expression SymbolicState::thisAddress() { return m_thisAddress.currentValue(); } +smtutil::Expression SymbolicState::thisAddress(unsigned _idx) +{ + return m_thisAddress.valueAtIndex(_idx); +} + +SortPointer SymbolicState::thisAddressSort() +{ + return m_thisAddress.sort(); +} + +smtutil::Expression SymbolicState::state() +{ + return m_stateTuple->currentValue(); +} + +smtutil::Expression SymbolicState::state(unsigned _idx) +{ + return m_stateTuple->valueAtIndex(_idx); +} + +SortPointer SymbolicState::stateSort() +{ + return m_stateTuple->sort(); +} + +void SymbolicState::newState() +{ + m_stateTuple->increaseIndex(); +} + smtutil::Expression SymbolicState::balances() { return m_stateTuple->component(m_componentIndices.at("balances")); @@ -76,21 +115,6 @@ smtutil::Expression SymbolicState::balance(smtutil::Expression _address) return smtutil::Expression::select(balances(), move(_address)); } -SymbolicIntVariable& SymbolicState::errorFlag() -{ - return m_error; -} - -smtutil::Expression SymbolicState::state() -{ - return m_stateTuple->currentValue(); -} - -SortPointer SymbolicState::stateSort() -{ - return m_stateTuple->sort(); -} - void SymbolicState::transfer(smtutil::Expression _from, smtutil::Expression _to, smtutil::Expression _value) { unsigned indexBefore = m_stateTuple->index(); diff --git a/libsolidity/formal/SymbolicState.h b/libsolidity/formal/SymbolicState.h index 9878e1926..fe3233b1e 100644 --- a/libsolidity/formal/SymbolicState.h +++ b/libsolidity/formal/SymbolicState.h @@ -48,8 +48,20 @@ public: /// Blockchain. //@{ - /// Value of `this` address. + SymbolicIntVariable& errorFlag(); + smtutil::SortPointer errorFlagSort(); + + /// @returns the symbolic value of the currently executing contract's address. smtutil::Expression thisAddress(); + smtutil::Expression thisAddress(unsigned _idx); + smtutil::SortPointer thisAddressSort(); + + /// @returns the state as a tuple. + smtutil::Expression state(); + smtutil::Expression state(unsigned _idx); + smtutil::SortPointer stateSort(); + void newState(); + /// @returns the symbolic balances. smtutil::Expression balances(); /// @returns the symbolic balance of address `this`. @@ -57,14 +69,6 @@ public: /// @returns the symbolic balance of an address. smtutil::Expression balance(smtutil::Expression _address); - SymbolicIntVariable& errorFlag(); - - /// @returns the state as a tuple. - smtutil::Expression state(); - - /// @returns the state sort. - smtutil::SortPointer stateSort(); - /// Transfer _value from _from to _to. void transfer(smtutil::Expression _from, smtutil::Expression _to, smtutil::Expression _value); //@} diff --git a/test/libsolidity/smtCheckerTests/types/struct/array_struct_array_struct_memory_unsafe.sol b/test/libsolidity/smtCheckerTests/types/struct/array_struct_array_struct_memory_unsafe.sol index 6ade5f038..0273f17d0 100644 --- a/test/libsolidity/smtCheckerTests/types/struct/array_struct_array_struct_memory_unsafe.sol +++ b/test/libsolidity/smtCheckerTests/types/struct/array_struct_array_struct_memory_unsafe.sol @@ -23,8 +23,6 @@ contract C { assert(s1[2].a[2] == s2.a[2]); s1[0].ts[3].y = 5; assert(s1[0].ts[3].y == s2.ts[3].y); - s1[1].ts[4].a[5] = 6; - assert(s1[1].ts[4].a[5] == s2.ts[4].a[5]); } } // ---- From 3d2e6252f01cffa99b65989f5749e4b0271e3dac Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Fri, 18 Sep 2020 19:07:58 +0200 Subject: [PATCH 3/3] Add/update tests --- .../blockchain_state/decreasing_balance.sol | 20 +++++++++++++++++++ .../blockchain_state/this_does_not_change.sol | 12 +++++++++++ .../this_does_not_change_external_call.sol | 18 +++++++++++++++++ .../this_does_not_change_internal_call.sol | 15 ++++++++++++++ .../blockchain_state/transfer.sol | 13 ++++++++++++ .../functions/functions_external_2.sol | 1 - .../loops/for_1_false_positive.sol | 1 + ...rray_struct_array_struct_memory_unsafe.sol | 1 - 8 files changed, 79 insertions(+), 2 deletions(-) create mode 100644 test/libsolidity/smtCheckerTests/blockchain_state/decreasing_balance.sol create mode 100644 test/libsolidity/smtCheckerTests/blockchain_state/this_does_not_change.sol create mode 100644 test/libsolidity/smtCheckerTests/blockchain_state/this_does_not_change_external_call.sol create mode 100644 test/libsolidity/smtCheckerTests/blockchain_state/this_does_not_change_internal_call.sol create mode 100644 test/libsolidity/smtCheckerTests/blockchain_state/transfer.sol diff --git a/test/libsolidity/smtCheckerTests/blockchain_state/decreasing_balance.sol b/test/libsolidity/smtCheckerTests/blockchain_state/decreasing_balance.sol new file mode 100644 index 000000000..792029433 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/blockchain_state/decreasing_balance.sol @@ -0,0 +1,20 @@ +pragma experimental SMTChecker; + +contract C { + uint t; + constructor() { + t = address(this).balance; + } + function f(address payable a, uint x) public { + require(address(this).balance >= x); + a.transfer(x); + } + function inv() public view { + // If only looking at `f`, it looks like this.balance always decreases. + // However, the edge case of a contract `selfdestruct` sending its remaining balance + // to this contract should make the claim false (since there's no fallback/receive here). + assert(address(this).balance == t); + } +} +// ---- +// Warning 6328: (496-530): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/blockchain_state/this_does_not_change.sol b/test/libsolidity/smtCheckerTests/blockchain_state/this_does_not_change.sol new file mode 100644 index 000000000..816b9af32 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/blockchain_state/this_does_not_change.sol @@ -0,0 +1,12 @@ +pragma experimental SMTChecker; + +contract C { + address t; + constructor() { + t = address(this); + } + function inv() public view { + assert(address(this) == t); + } +} +// ---- diff --git a/test/libsolidity/smtCheckerTests/blockchain_state/this_does_not_change_external_call.sol b/test/libsolidity/smtCheckerTests/blockchain_state/this_does_not_change_external_call.sol new file mode 100644 index 000000000..c0adb1fe9 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/blockchain_state/this_does_not_change_external_call.sol @@ -0,0 +1,18 @@ +pragma experimental SMTChecker; + +abstract contract D { + function d() external virtual; +} + +contract C { + address t; + constructor() { + t = address(this); + } + function f(D d) public { + address a = address(this); + d.d(); + assert(address(this) == t); + assert(a == t); + } +} diff --git a/test/libsolidity/smtCheckerTests/blockchain_state/this_does_not_change_internal_call.sol b/test/libsolidity/smtCheckerTests/blockchain_state/this_does_not_change_internal_call.sol new file mode 100644 index 000000000..70feedc3e --- /dev/null +++ b/test/libsolidity/smtCheckerTests/blockchain_state/this_does_not_change_internal_call.sol @@ -0,0 +1,15 @@ +pragma experimental SMTChecker; + +contract C { + address t; + constructor() { + t = address(this); + } + function f() public view { + g(address(this)); + } + function g(address a) internal view { + assert(a == t); + assert(a == address(this)); + } +} diff --git a/test/libsolidity/smtCheckerTests/blockchain_state/transfer.sol b/test/libsolidity/smtCheckerTests/blockchain_state/transfer.sol new file mode 100644 index 000000000..90dc1e957 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/blockchain_state/transfer.sol @@ -0,0 +1,13 @@ +pragma experimental SMTChecker; + +contract C { + function f(address payable a) public { + require(address(this).balance > 1000); + a.transfer(666); + assert(address(this).balance > 100); + // Fails. + assert(address(this).balance > 500); + } +} +// ---- +// Warning 6328: (199-234): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/functions/functions_external_2.sol b/test/libsolidity/smtCheckerTests/functions/functions_external_2.sol index 5ac741522..402c3dbd3 100644 --- a/test/libsolidity/smtCheckerTests/functions/functions_external_2.sol +++ b/test/libsolidity/smtCheckerTests/functions/functions_external_2.sol @@ -17,4 +17,3 @@ contract C } } // ---- -// Warning 4661: (297-321): BMC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/loops/for_1_false_positive.sol b/test/libsolidity/smtCheckerTests/loops/for_1_false_positive.sol index f4176588e..6ca91ce94 100644 --- a/test/libsolidity/smtCheckerTests/loops/for_1_false_positive.sol +++ b/test/libsolidity/smtCheckerTests/loops/for_1_false_positive.sol @@ -15,3 +15,4 @@ contract C } // ---- // Warning 2661: (176-181): BMC: Overflow (resulting value larger than 2**256 - 1) happens here. +// Warning 4661: (296-309): BMC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/types/struct/array_struct_array_struct_memory_unsafe.sol b/test/libsolidity/smtCheckerTests/types/struct/array_struct_array_struct_memory_unsafe.sol index 0273f17d0..4b97dd2fb 100644 --- a/test/libsolidity/smtCheckerTests/types/struct/array_struct_array_struct_memory_unsafe.sol +++ b/test/libsolidity/smtCheckerTests/types/struct/array_struct_array_struct_memory_unsafe.sol @@ -30,4 +30,3 @@ contract C { // Warning 6328: (327-354): CHC: Assertion violation happens here. // Warning 6328: (376-405): CHC: Assertion violation happens here. // Warning 6328: (430-465): CHC: Assertion violation happens here. -// Warning 6328: (493-534): CHC: Assertion violation happens here.