solidity/libsolidity/formal/PredicateSort.cpp

115 lines
3.8 KiB
C++
Raw Normal View History

2020-09-08 14:52:58 +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/>.
*/
// SPDX-License-Identifier: GPL-3.0
#include <libsolidity/formal/PredicateSort.h>
#include <libsolidity/formal/SMTEncoder.h>
#include <libsolidity/formal/SymbolicTypes.h>
using namespace std;
using namespace solidity::util;
using namespace solidity::smtutil;
namespace solidity::frontend::smt
{
2020-09-18 16:55:23 +00:00
SortPointer interfaceSort(ContractDefinition const& _contract, SymbolicState& _state)
2020-09-08 14:52:58 +00:00
{
return make_shared<FunctionSort>(
vector<SortPointer>{_state.thisAddressSort(), _state.abiSort(), _state.cryptoSort(), _state.stateSort()} + stateSorts(_contract),
2020-09-08 14:52:58 +00:00
SortProvider::boolSort
);
}
2020-09-18 16:55:23 +00:00
SortPointer nondetInterfaceSort(ContractDefinition const& _contract, SymbolicState& _state)
2020-09-08 14:52:58 +00:00
{
auto varSorts = stateSorts(_contract);
2020-09-18 16:55:23 +00:00
vector<SortPointer> stateSort{_state.stateSort()};
2020-09-08 14:52:58 +00:00
return make_shared<FunctionSort>(
vector<SortPointer>{_state.errorFlagSort(), _state.thisAddressSort(), _state.abiSort(), _state.cryptoSort()} +
stateSort +
varSorts +
stateSort +
varSorts,
2020-09-08 14:52:58 +00:00
SortProvider::boolSort
);
}
2020-09-18 16:55:23 +00:00
SortPointer constructorSort(ContractDefinition const& _contract, SymbolicState& _state)
2020-09-08 14:52:58 +00:00
{
if (auto const* constructor = _contract.constructor())
2020-09-18 16:55:23 +00:00
return functionSort(*constructor, &_contract, _state);
2020-09-08 14:52:58 +00:00
auto varSorts = stateSorts(_contract);
vector<SortPointer> stateSort{_state.stateSort()};
2020-09-08 14:52:58 +00:00
return make_shared<FunctionSort>(
vector<SortPointer>{_state.errorFlagSort(), _state.thisAddressSort(), _state.abiSort(), _state.cryptoSort(), _state.txSort(), _state.stateSort(), _state.stateSort()} + varSorts + varSorts,
2020-09-08 14:52:58 +00:00
SortProvider::boolSort
);
}
2020-09-18 16:55:23 +00:00
SortPointer functionSort(FunctionDefinition const& _function, ContractDefinition const* _contract, SymbolicState& _state)
2020-09-08 14:52:58 +00:00
{
auto smtSort = [](auto _var) { return smt::smtSortAbstractFunction(*_var->type()); };
auto varSorts = _contract ? stateSorts(*_contract) : vector<SortPointer>{};
auto inputSorts = applyMap(_function.parameters(), smtSort);
auto outputSorts = applyMap(_function.returnParameters(), smtSort);
return make_shared<FunctionSort>(
vector<SortPointer>{_state.errorFlagSort(), _state.thisAddressSort(), _state.abiSort(), _state.cryptoSort(), _state.txSort(), _state.stateSort()} +
2020-09-08 14:52:58 +00:00
varSorts +
inputSorts +
2020-09-18 16:55:23 +00:00
vector<SortPointer>{_state.stateSort()} +
2020-09-08 14:52:58 +00:00
varSorts +
inputSorts +
outputSorts,
SortProvider::boolSort
);
}
2020-09-18 16:55:23 +00:00
SortPointer functionBodySort(FunctionDefinition const& _function, ContractDefinition const* _contract, SymbolicState& _state)
2020-09-08 14:52:58 +00:00
{
2020-09-18 16:55:23 +00:00
auto fSort = dynamic_pointer_cast<FunctionSort>(functionSort(_function, _contract, _state));
2020-09-08 14:52:58 +00:00
solAssert(fSort, "");
auto smtSort = [](auto _var) { return smt::smtSortAbstractFunction(*_var->type()); };
return make_shared<FunctionSort>(
fSort->domain + applyMap(SMTEncoder::localVariablesIncludingModifiers(_function, _contract), smtSort),
2020-09-08 14:52:58 +00:00
SortProvider::boolSort
);
}
SortPointer arity0FunctionSort()
{
return make_shared<FunctionSort>(
vector<SortPointer>(),
SortProvider::boolSort
);
}
/// Helpers
vector<SortPointer> stateSorts(ContractDefinition const& _contract)
{
return applyMap(
SMTEncoder::stateVariablesIncludingInheritedAndPrivate(_contract),
[](auto _var) { return smt::smtSortAbstractFunction(*_var->type()); }
);
}
}