From d2f65ea8b11f3be7281347390d739b9fec3c61ce Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Tue, 24 Mar 2020 20:51:52 +0100 Subject: [PATCH] [SMTChecker] Add SortProvider --- libsolidity/CMakeLists.txt | 2 + libsolidity/formal/CHC.cpp | 35 +++---- libsolidity/formal/EncodingContext.cpp | 4 +- libsolidity/formal/SolverInterface.h | 90 +----------------- libsolidity/formal/Sorts.cpp | 29 ++++++ libsolidity/formal/Sorts.h | 125 +++++++++++++++++++++++++ libsolidity/formal/SymbolicTypes.cpp | 17 ++-- 7 files changed, 179 insertions(+), 123 deletions(-) create mode 100644 libsolidity/formal/Sorts.cpp create mode 100644 libsolidity/formal/Sorts.h diff --git a/libsolidity/CMakeLists.txt b/libsolidity/CMakeLists.txt index bb54c836f..ba2651e94 100644 --- a/libsolidity/CMakeLists.txt +++ b/libsolidity/CMakeLists.txt @@ -100,6 +100,8 @@ set(sources formal/SMTPortfolio.cpp formal/SMTPortfolio.h formal/SolverInterface.h + formal/Sorts.cpp + formal/Sorts.h formal/SSAVariable.cpp formal/SSAVariable.h formal/SymbolicTypes.cpp diff --git a/libsolidity/formal/CHC.cpp b/libsolidity/formal/CHC.cpp index 1e851937c..e10c16d39 100644 --- a/libsolidity/formal/CHC.cpp +++ b/libsolidity/formal/CHC.cpp @@ -79,10 +79,9 @@ void CHC::analyze(SourceUnit const& _source) resetSourceAnalysis(); - auto boolSort = make_shared(smt::Kind::Bool); auto genesisSort = make_shared( vector(), - boolSort + smt::SortProvider::boolSort ); m_genesisPredicate = createSymbolicBlock(genesisSort, "genesis"); addRule(genesis(), "genesis"); @@ -131,12 +130,9 @@ bool CHC::visit(ContractDefinition const& _contract) clearIndices(&_contract); - - // TODO create static instances for Bool/Int sorts in SolverInterface. - auto boolSort = make_shared(smt::Kind::Bool); auto errorFunctionSort = make_shared( vector(), - boolSort + smt::SortProvider::boolSort ); string suffix = _contract.name() + "_" + to_string(_contract.id()); @@ -664,29 +660,25 @@ vector CHC::stateSorts(ContractDefinition const& _contract) smt::SortPointer CHC::constructorSort() { - auto boolSort = make_shared(smt::Kind::Bool); - auto intSort = make_shared(smt::Kind::Int); return make_shared( - vector{intSort} + m_stateSorts, - boolSort + vector{smt::SortProvider::intSort} + m_stateSorts, + smt::SortProvider::boolSort ); } smt::SortPointer CHC::interfaceSort() { - auto boolSort = make_shared(smt::Kind::Bool); return make_shared( m_stateSorts, - boolSort + smt::SortProvider::boolSort ); } smt::SortPointer CHC::interfaceSort(ContractDefinition const& _contract) { - auto boolSort = make_shared(smt::Kind::Bool); return make_shared( stateSorts(_contract), - boolSort + smt::SortProvider::boolSort ); } @@ -703,8 +695,6 @@ smt::SortPointer CHC::interfaceSort(ContractDefinition const& _contract) /// - 1 set of output variables smt::SortPointer CHC::sort(FunctionDefinition const& _function) { - auto boolSort = make_shared(smt::Kind::Bool); - auto intSort = make_shared(smt::Kind::Int); vector inputSorts; for (auto const& var: _function.parameters()) inputSorts.push_back(smt::smtSortAbstractFunction(*var->type())); @@ -712,8 +702,8 @@ smt::SortPointer CHC::sort(FunctionDefinition const& _function) for (auto const& var: _function.returnParameters()) outputSorts.push_back(smt::smtSortAbstractFunction(*var->type())); return make_shared( - vector{intSort} + m_stateSorts + inputSorts + m_stateSorts + inputSorts + outputSorts, - boolSort + vector{smt::SortProvider::intSort} + m_stateSorts + inputSorts + m_stateSorts + inputSorts + outputSorts, + smt::SortProvider::boolSort ); } @@ -725,13 +715,12 @@ smt::SortPointer CHC::sort(ASTNode const* _node) auto fSort = dynamic_pointer_cast(sort(*m_currentFunction)); solAssert(fSort, ""); - auto boolSort = make_shared(smt::Kind::Bool); vector varSorts; for (auto const& var: m_currentFunction->localVariables()) varSorts.push_back(smt::smtSortAbstractFunction(*var->type())); return make_shared( fSort->domain + varSorts, - boolSort + smt::SortProvider::boolSort ); } @@ -740,16 +729,14 @@ smt::SortPointer CHC::summarySort(FunctionDefinition const& _function, ContractD auto stateVariables = stateVariablesIncludingInheritedAndPrivate(_contract); auto sorts = stateSorts(_contract); - auto boolSort = make_shared(smt::Kind::Bool); - auto intSort = make_shared(smt::Kind::Int); vector inputSorts, outputSorts; for (auto const& var: _function.parameters()) inputSorts.push_back(smt::smtSortAbstractFunction(*var->type())); for (auto const& var: _function.returnParameters()) outputSorts.push_back(smt::smtSortAbstractFunction(*var->type())); return make_shared( - vector{intSort} + sorts + inputSorts + sorts + outputSorts, - boolSort + vector{smt::SortProvider::intSort} + sorts + inputSorts + sorts + outputSorts, + smt::SortProvider::boolSort ); } diff --git a/libsolidity/formal/EncodingContext.cpp b/libsolidity/formal/EncodingContext.cpp index ff193d2e2..1f7b7a5e0 100644 --- a/libsolidity/formal/EncodingContext.cpp +++ b/libsolidity/formal/EncodingContext.cpp @@ -28,8 +28,8 @@ EncodingContext::EncodingContext(): m_thisAddress(make_unique("this", *this)) { auto sort = make_shared( - make_shared(Kind::Int), - make_shared(Kind::Int) + SortProvider::intSort, + SortProvider::intSort ); m_balances = make_unique(sort, "balances", *this); } diff --git a/libsolidity/formal/SolverInterface.h b/libsolidity/formal/SolverInterface.h index 512be65bb..106ada820 100644 --- a/libsolidity/formal/SolverInterface.h +++ b/libsolidity/formal/SolverInterface.h @@ -17,6 +17,8 @@ #pragma once +#include + #include #include #include @@ -52,94 +54,6 @@ enum class CheckResult SATISFIABLE, UNSATISFIABLE, UNKNOWN, CONFLICTING, ERROR }; -enum class Kind -{ - Int, - Bool, - Function, - Array, - Sort -}; - -struct Sort -{ - Sort(Kind _kind): - kind(_kind) {} - virtual ~Sort() = default; - virtual bool operator==(Sort const& _other) const { return kind == _other.kind; } - - Kind const kind; -}; -using SortPointer = std::shared_ptr; - -struct FunctionSort: public Sort -{ - FunctionSort(std::vector _domain, SortPointer _codomain): - Sort(Kind::Function), domain(std::move(_domain)), codomain(std::move(_codomain)) {} - bool operator==(Sort const& _other) const override - { - if (!Sort::operator==(_other)) - return false; - auto _otherFunction = dynamic_cast(&_other); - solAssert(_otherFunction, ""); - if (domain.size() != _otherFunction->domain.size()) - return false; - if (!std::equal( - domain.begin(), - domain.end(), - _otherFunction->domain.begin(), - [&](SortPointer _a, SortPointer _b) { return *_a == *_b; } - )) - return false; - solAssert(codomain, ""); - solAssert(_otherFunction->codomain, ""); - return *codomain == *_otherFunction->codomain; - } - - std::vector domain; - SortPointer codomain; -}; - -struct ArraySort: public Sort -{ - /// _domain is the sort of the indices - /// _range is the sort of the values - ArraySort(SortPointer _domain, SortPointer _range): - Sort(Kind::Array), domain(std::move(_domain)), range(std::move(_range)) {} - bool operator==(Sort const& _other) const override - { - if (!Sort::operator==(_other)) - return false; - auto _otherArray = dynamic_cast(&_other); - solAssert(_otherArray, ""); - solAssert(_otherArray->domain, ""); - solAssert(_otherArray->range, ""); - solAssert(domain, ""); - solAssert(range, ""); - return *domain == *_otherArray->domain && *range == *_otherArray->range; - } - - SortPointer domain; - SortPointer range; -}; - -struct SortSort: public Sort -{ - SortSort(SortPointer _inner): Sort(Kind::Sort), inner(std::move(_inner)) {} - bool operator==(Sort const& _other) const override - { - if (!Sort::operator==(_other)) - return false; - auto _otherSort = dynamic_cast(&_other); - solAssert(_otherSort, ""); - solAssert(_otherSort->inner, ""); - solAssert(inner, ""); - return *inner == *_otherSort->inner; - } - - SortPointer inner; -}; - // Forward declaration. SortPointer smtSort(Type const& _type); diff --git a/libsolidity/formal/Sorts.cpp b/libsolidity/formal/Sorts.cpp new file mode 100644 index 000000000..195048e56 --- /dev/null +++ b/libsolidity/formal/Sorts.cpp @@ -0,0 +1,29 @@ +/* + 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 . +*/ + + +#include + +using namespace std; + +namespace solidity::frontend::smt +{ + +shared_ptr const SortProvider::boolSort{make_shared(Kind::Bool)}; +shared_ptr const SortProvider::intSort{make_shared(Kind::Int)}; + +} diff --git a/libsolidity/formal/Sorts.h b/libsolidity/formal/Sorts.h new file mode 100644 index 000000000..d26644462 --- /dev/null +++ b/libsolidity/formal/Sorts.h @@ -0,0 +1,125 @@ +/* + 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 . +*/ + +#pragma once + +#include +#include +#include + +#include +#include + +namespace solidity::frontend::smt +{ + +enum class Kind +{ + Int, + Bool, + Function, + Array, + Sort +}; + +struct Sort +{ + Sort(Kind _kind): + kind(_kind) {} + virtual ~Sort() = default; + virtual bool operator==(Sort const& _other) const { return kind == _other.kind; } + + Kind const kind; +}; +using SortPointer = std::shared_ptr; + +struct FunctionSort: public Sort +{ + FunctionSort(std::vector _domain, SortPointer _codomain): + Sort(Kind::Function), domain(std::move(_domain)), codomain(std::move(_codomain)) {} + bool operator==(Sort const& _other) const override + { + if (!Sort::operator==(_other)) + return false; + auto _otherFunction = dynamic_cast(&_other); + solAssert(_otherFunction, ""); + if (domain.size() != _otherFunction->domain.size()) + return false; + if (!std::equal( + domain.begin(), + domain.end(), + _otherFunction->domain.begin(), + [&](SortPointer _a, SortPointer _b) { return *_a == *_b; } + )) + return false; + solAssert(codomain, ""); + solAssert(_otherFunction->codomain, ""); + return *codomain == *_otherFunction->codomain; + } + + std::vector domain; + SortPointer codomain; +}; + +struct ArraySort: public Sort +{ + /// _domain is the sort of the indices + /// _range is the sort of the values + ArraySort(SortPointer _domain, SortPointer _range): + Sort(Kind::Array), domain(std::move(_domain)), range(std::move(_range)) {} + bool operator==(Sort const& _other) const override + { + if (!Sort::operator==(_other)) + return false; + auto _otherArray = dynamic_cast(&_other); + solAssert(_otherArray, ""); + solAssert(_otherArray->domain, ""); + solAssert(_otherArray->range, ""); + solAssert(domain, ""); + solAssert(range, ""); + return *domain == *_otherArray->domain && *range == *_otherArray->range; + } + + SortPointer domain; + SortPointer range; +}; + +struct SortSort: public Sort +{ + SortSort(SortPointer _inner): Sort(Kind::Sort), inner(std::move(_inner)) {} + bool operator==(Sort const& _other) const override + { + if (!Sort::operator==(_other)) + return false; + auto _otherSort = dynamic_cast(&_other); + solAssert(_otherSort, ""); + solAssert(_otherSort->inner, ""); + solAssert(inner, ""); + return *inner == *_otherSort->inner; + } + + SortPointer inner; +}; + +/** Frequently used sorts.*/ +struct SortProvider +{ + static std::shared_ptr const boolSort; + static std::shared_ptr const intSort; +}; + +} diff --git a/libsolidity/formal/SymbolicTypes.cpp b/libsolidity/formal/SymbolicTypes.cpp index a2475b337..1d9655a9c 100644 --- a/libsolidity/formal/SymbolicTypes.cpp +++ b/libsolidity/formal/SymbolicTypes.cpp @@ -32,9 +32,9 @@ SortPointer smtSort(frontend::Type const& _type) switch (smtKind(_type.category())) { case Kind::Int: - return make_shared(Kind::Int); + return SortProvider::intSort; case Kind::Bool: - return make_shared(Kind::Bool); + return SortProvider::boolSort; case Kind::Function: { auto fType = dynamic_cast(&_type); @@ -45,10 +45,10 @@ SortPointer smtSort(frontend::Type const& _type) // TODO change this when we support tuples. if (returnTypes.size() == 0) // We cannot declare functions without a return sort, so we use the smallest. - returnSort = make_shared(Kind::Bool); + returnSort = SortProvider::boolSort; else if (returnTypes.size() > 1) // Abstract sort. - returnSort = make_shared(Kind::Int); + returnSort = SortProvider::intSort; else returnSort = smtSort(*returnTypes.front()); return make_shared(parameterSorts, returnSort); @@ -65,20 +65,19 @@ SortPointer smtSort(frontend::Type const& _type) { auto stringLitType = dynamic_cast(&_type); solAssert(stringLitType, ""); - auto intSort = make_shared(Kind::Int); - return make_shared(intSort, intSort); + return make_shared(SortProvider::intSort, SortProvider::intSort); } else { solAssert(isArray(_type.category()), ""); auto arrayType = dynamic_cast(&_type); solAssert(arrayType, ""); - return make_shared(make_shared(Kind::Int), smtSortAbstractFunction(*arrayType->baseType())); + return make_shared(SortProvider::intSort, smtSortAbstractFunction(*arrayType->baseType())); } } default: // Abstract case. - return make_shared(Kind::Int); + return SortProvider::intSort; } } @@ -93,7 +92,7 @@ vector smtSort(vector const& _types) SortPointer smtSortAbstractFunction(frontend::Type const& _type) { if (isFunction(_type.category())) - return make_shared(Kind::Int); + return SortProvider::intSort; return smtSort(_type); }