From 3519b380550d32281a81380ee1d5babed15c1841 Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Wed, 16 Sep 2020 11:47:54 +0200 Subject: [PATCH] Move predicate functions from CHC to PredicateInstance --- libsolidity/CMakeLists.txt | 2 + libsolidity/formal/CHC.cpp | 186 ++++++++--------------- libsolidity/formal/CHC.h | 21 +-- libsolidity/formal/Predicate.cpp | 5 +- libsolidity/formal/Predicate.h | 19 +++ libsolidity/formal/PredicateInstance.cpp | 120 +++++++++++++++ libsolidity/formal/PredicateInstance.h | 73 +++++++++ 7 files changed, 288 insertions(+), 138 deletions(-) create mode 100644 libsolidity/formal/PredicateInstance.cpp create mode 100644 libsolidity/formal/PredicateInstance.h diff --git a/libsolidity/CMakeLists.txt b/libsolidity/CMakeLists.txt index 091c87cd4..a6ea34c29 100644 --- a/libsolidity/CMakeLists.txt +++ b/libsolidity/CMakeLists.txt @@ -104,6 +104,8 @@ set(sources formal/ModelChecker.h formal/Predicate.cpp formal/Predicate.h + formal/PredicateInstance.cpp + formal/PredicateInstance.h formal/PredicateSort.cpp formal/PredicateSort.h formal/SMTEncoder.cpp diff --git a/libsolidity/formal/CHC.cpp b/libsolidity/formal/CHC.cpp index 710cc0aa8..bdca72fd0 100644 --- a/libsolidity/formal/CHC.cpp +++ b/libsolidity/formal/CHC.cpp @@ -22,6 +22,7 @@ #include #endif +#include #include #include @@ -101,10 +102,9 @@ bool CHC::visit(ContractDefinition const& _contract) m_constructorSummaryPredicate = createSymbolicBlock( constructorSort(*m_currentContract), "summary_constructor_" + contractSuffix(_contract), + PredicateType::ConstructorSummary, &_contract ); - auto stateExprs = currentStateVariables(); - setCurrentBlock(*m_interfaces.at(m_currentContract), &stateExprs); SMTEncoder::visit(_contract); return false; @@ -130,9 +130,7 @@ void CHC::endVisit(ContractDefinition const& _contract) connectBlocks(m_currentBlock, summary(_contract)); - clearIndices(m_currentContract, nullptr); - vector symbArgs = currentFunctionVariables(*m_currentContract); - setCurrentBlock(*m_constructorSummaryPredicate, &symbArgs); + setCurrentBlock(*m_constructorSummaryPredicate); addAssertVerificationTarget(m_currentContract, m_currentBlock, smtutil::Expression(true), errorFlag().currentValue()); connectBlocks(m_currentBlock, interface(), errorFlag().currentValue() == 0); @@ -163,10 +161,10 @@ bool CHC::visit(FunctionDefinition const& _function) initFunction(_function); - auto functionEntryBlock = createBlock(m_currentFunction); - auto bodyBlock = createBlock(&m_currentFunction->body()); + auto functionEntryBlock = createBlock(m_currentFunction, PredicateType::FunctionEntry); + auto bodyBlock = createBlock(&m_currentFunction->body(), PredicateType::FunctionBlock); - auto functionPred = predicate(*functionEntryBlock, currentFunctionVariables()); + auto functionPred = predicate(*functionEntryBlock); auto bodyPred = predicate(*bodyBlock); if (_function.isConstructor()) @@ -218,13 +216,12 @@ void CHC::endVisit(FunctionDefinition const& _function) auto constructorExit = createSymbolicBlock( constructorSort(*m_currentContract), "constructor_exit_" + suffix, + PredicateType::ConstructorSummary, m_currentContract ); - connectBlocks(m_currentBlock, predicate(*constructorExit, currentFunctionVariables(*m_currentContract))); + connectBlocks(m_currentBlock, predicate(*constructorExit)); - clearIndices(m_currentContract, m_currentFunction); - auto stateExprs = currentFunctionVariables(*m_currentContract); - setCurrentBlock(*constructorExit, &stateExprs); + setCurrentBlock(*constructorExit); } else { @@ -234,13 +231,13 @@ void CHC::endVisit(FunctionDefinition const& _function) auto iface = interface(); - auto stateExprs = initialStateVariables(); - setCurrentBlock(*m_interfaces.at(m_currentContract), &stateExprs); + setCurrentBlock(*m_interfaces.at(m_currentContract)); + auto ifacePre = (*m_interfaces.at(m_currentContract))(initialStateVariables()); if (_function.isPublic()) { - addAssertVerificationTarget(&_function, m_currentBlock, sum, assertionError); - connectBlocks(m_currentBlock, iface, sum && (assertionError == 0)); + addAssertVerificationTarget(&_function, ifacePre, sum, assertionError); + connectBlocks(ifacePre, iface, sum && (assertionError == 0)); } } m_currentFunction = nullptr; @@ -259,10 +256,10 @@ bool CHC::visit(IfStatement const& _if) solAssert(m_currentFunction, ""); auto const& functionBody = m_currentFunction->body(); - auto ifHeaderBlock = createBlock(&_if, "if_header_"); - auto trueBlock = createBlock(&_if.trueStatement(), "if_true_"); - auto falseBlock = _if.falseStatement() ? createBlock(_if.falseStatement(), "if_false_") : nullptr; - auto afterIfBlock = createBlock(&functionBody); + auto ifHeaderBlock = createBlock(&_if, PredicateType::FunctionBlock, "if_header_"); + auto trueBlock = createBlock(&_if.trueStatement(), PredicateType::FunctionBlock, "if_true_"); + auto falseBlock = _if.falseStatement() ? createBlock(_if.falseStatement(), PredicateType::FunctionBlock, "if_false_") : nullptr; + auto afterIfBlock = createBlock(&functionBody, PredicateType::FunctionBlock); connectBlocks(m_currentBlock, predicate(*ifHeaderBlock)); @@ -306,9 +303,9 @@ bool CHC::visit(WhileStatement const& _while) auto const& functionBody = m_currentFunction->body(); auto namePrefix = string(_while.isDoWhile() ? "do_" : "") + "while"; - auto loopHeaderBlock = createBlock(&_while, namePrefix + "_header_"); - auto loopBodyBlock = createBlock(&_while.body(), namePrefix + "_body_"); - auto afterLoopBlock = createBlock(&functionBody); + auto loopHeaderBlock = createBlock(&_while, PredicateType::FunctionBlock, namePrefix + "_header_"); + auto loopBodyBlock = createBlock(&_while.body(), PredicateType::FunctionBlock, namePrefix + "_body_"); + auto afterLoopBlock = createBlock(&functionBody, PredicateType::FunctionBlock); auto outerBreakDest = m_breakDest; auto outerContinueDest = m_continueDest; @@ -355,11 +352,11 @@ bool CHC::visit(ForStatement const& _for) solAssert(m_currentFunction, ""); auto const& functionBody = m_currentFunction->body(); - auto loopHeaderBlock = createBlock(&_for, "for_header_"); - auto loopBodyBlock = createBlock(&_for.body(), "for_body_"); - auto afterLoopBlock = createBlock(&functionBody); + auto loopHeaderBlock = createBlock(&_for, PredicateType::FunctionBlock, "for_header_"); + auto loopBodyBlock = createBlock(&_for.body(), PredicateType::FunctionBlock, "for_body_"); + auto afterLoopBlock = createBlock(&functionBody, PredicateType::FunctionBlock); auto postLoop = _for.loopExpression(); - auto postLoopBlock = postLoop ? createBlock(postLoop, "for_post_") : nullptr; + auto postLoopBlock = postLoop ? createBlock(postLoop, PredicateType::FunctionBlock, "for_post_") : nullptr; auto outerBreakDest = m_breakDest; auto outerContinueDest = m_continueDest; @@ -461,7 +458,7 @@ void CHC::endVisit(Break const& _break) { solAssert(m_breakDest, ""); connectBlocks(m_currentBlock, predicate(*m_breakDest)); - auto breakGhost = createBlock(&_break, "break_ghost_"); + auto breakGhost = createBlock(&_break, PredicateType::FunctionBlock, "break_ghost_"); m_currentBlock = predicate(*breakGhost); } @@ -469,7 +466,7 @@ void CHC::endVisit(Continue const& _continue) { solAssert(m_continueDest, ""); connectBlocks(m_currentBlock, predicate(*m_continueDest)); - auto continueGhost = createBlock(&_continue, "continue_ghost_"); + auto continueGhost = createBlock(&_continue, PredicateType::FunctionBlock, "continue_ghost_"); m_currentBlock = predicate(*continueGhost); } @@ -726,20 +723,14 @@ void CHC::clearIndices(ContractDefinition const* _contract, FunctionDefinition c } } -void CHC::setCurrentBlock( - Predicate const& _block, - vector const* _arguments -) +void CHC::setCurrentBlock(Predicate const& _block) { if (m_context.solverStackHeigh() > 0) m_context.popSolver(); solAssert(m_currentContract, ""); clearIndices(m_currentContract, m_currentFunction); m_context.pushSolver(); - if (_arguments) - m_currentBlock = predicate(_block, *_arguments); - else - m_currentBlock = predicate(_block); + m_currentBlock = predicate(_block); } set CHC::transactionAssertions(ASTNode const* _txRoot) @@ -767,9 +758,9 @@ SortPointer CHC::sort(ASTNode const* _node) return functionBodySort(*m_currentFunction, m_currentContract); } -Predicate const* CHC::createSymbolicBlock(SortPointer _sort, string const& _name, ASTNode const* _node) +Predicate const* CHC::createSymbolicBlock(SortPointer _sort, string const& _name, PredicateType _predType, ASTNode const* _node) { - auto const* block = Predicate::create(_sort, _name, m_context, _node); + auto const* block = Predicate::create(_sort, _name, _predType, m_context, _node); m_interface->registerRelation(block->functor()); return block; } @@ -780,8 +771,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); - m_nondetInterfaces[contract] = createSymbolicBlock(nondetInterfaceSort(*contract), "nondet_interface_" + suffix); + m_interfaces[contract] = createSymbolicBlock(interfaceSort(*contract), "interface_" + suffix, PredicateType::Interface, contract); + m_nondetInterfaces[contract] = createSymbolicBlock(nondetInterfaceSort(*contract), "nondet_interface_" + suffix, PredicateType::NondetInterface, contract); for (auto const* var: stateVariablesIncludingInheritedAndPrivate(*contract)) if (!m_context.knownVariable(*var)) @@ -834,16 +825,13 @@ void CHC::defineInterfacesAndSummaries(SourceUnit const& _source) smtutil::Expression CHC::interface() { - auto paramExprs = applyMap( - m_stateVariables, - [this](auto _var) { return m_context.variable(*_var)->currentValue(); } - ); - return (*m_interfaces.at(m_currentContract))(paramExprs); + solAssert(m_currentContract, ""); + return interface(*m_currentContract); } smtutil::Expression CHC::interface(ContractDefinition const& _contract) { - return (*m_interfaces.at(&_contract))(stateVariablesAtIndex(0, _contract)); + return ::interface(*m_interfaces.at(&_contract), _contract, m_context); } smtutil::Expression CHC::error() @@ -858,27 +846,12 @@ smtutil::Expression CHC::error(unsigned _idx) smtutil::Expression CHC::summary(ContractDefinition const& _contract) { - if (auto const* constructor = _contract.constructor()) - return (*m_constructorSummaryPredicate)( - currentFunctionVariables(*constructor) - ); - - return (*m_constructorSummaryPredicate)( - vector{m_error.currentValue()} + - currentStateVariables() - ); + return constructor(*m_constructorSummaryPredicate, _contract, m_context); } smtutil::Expression CHC::summary(FunctionDefinition const& _function, ContractDefinition const& _contract) { - vector args{m_error.currentValue()}; - auto contract = _function.annotation().contract; - args += contract->isLibrary() ? stateVariablesAtIndex(0, *contract) : initialStateVariables(_contract); - args += applyMap(_function.parameters(), [this](auto _var) { return valueAtIndex(*_var, 0); }); - args += contract->isLibrary() ? stateVariablesAtIndex(1, *contract) : currentStateVariables(_contract); - args += applyMap(_function.parameters(), [this](auto _var) { return currentValue(*_var); }); - args += applyMap(_function.returnParameters(), [this](auto _var) { return currentValue(*_var); }); - return (*m_summaries.at(&_contract).at(&_function))(args); + return smt::function(*m_summaries.at(&_contract).at(&_function), _function, &_contract, m_context); } smtutil::Expression CHC::summary(FunctionDefinition const& _function) @@ -887,11 +860,12 @@ smtutil::Expression CHC::summary(FunctionDefinition const& _function) return summary(_function, *m_currentContract); } -Predicate const* CHC::createBlock(ASTNode const* _node, string const& _prefix) +Predicate const* CHC::createBlock(ASTNode const* _node, PredicateType _predType, string const& _prefix) { auto block = createSymbolicBlock( sort(_node), "block_" + uniquePrefix() + "_" + _prefix + predicateName(_node), + _predType, _node ); @@ -904,6 +878,7 @@ Predicate const* CHC::createSummaryBlock(FunctionDefinition const& _function, Co auto block = createSymbolicBlock( functionSort(_function, &_contract), "summary_" + uniquePrefix() + "_" + predicateName(&_function, &_contract), + PredicateType::FunctionSummary, &_function ); @@ -912,7 +887,7 @@ Predicate const* CHC::createSummaryBlock(FunctionDefinition const& _function, Co void CHC::createErrorBlock() { - m_errorPredicate = createSymbolicBlock(arity0FunctionSort(), "error_target_" + to_string(m_context.newUniqueId())); + m_errorPredicate = createSymbolicBlock(arity0FunctionSort(), "error_target_" + to_string(m_context.newUniqueId()), PredicateType::Error); m_interface->registerRelation(m_errorPredicate->functor()); } @@ -930,11 +905,6 @@ vector CHC::initialStateVariables() return stateVariablesAtIndex(0); } -vector CHC::initialStateVariables(ContractDefinition const& _contract) -{ - return stateVariablesAtIndex(0, _contract); -} - vector CHC::stateVariablesAtIndex(unsigned _index) { solAssert(m_currentContract, ""); @@ -960,46 +930,6 @@ vector CHC::currentStateVariables(ContractDefinition const& return applyMap(SMTEncoder::stateVariablesIncludingInheritedAndPrivate(_contract), [this](auto _var) { return currentValue(*_var); }); } -vector CHC::currentFunctionVariables() -{ - solAssert(m_currentFunction, ""); - return currentFunctionVariables(*m_currentFunction); -} - -vector CHC::currentFunctionVariables(FunctionDefinition const& _function) -{ - vector initInputExprs; - vector mutableInputExprs; - for (auto const& var: _function.parameters()) - { - initInputExprs.push_back(m_context.variable(*var)->valueAtIndex(0)); - mutableInputExprs.push_back(m_context.variable(*var)->currentValue()); - } - auto returnExprs = applyMap(_function.returnParameters(), [this](auto _var) { return currentValue(*_var); }); - return vector{m_error.currentValue()} + - initialStateVariables() + - initInputExprs + - currentStateVariables() + - mutableInputExprs + - returnExprs; -} - -vector CHC::currentFunctionVariables(ContractDefinition const& _contract) -{ - if (auto const* constructor = _contract.constructor()) - return currentFunctionVariables(*constructor); - - return vector{m_error.currentValue()} + currentStateVariables(); -} - -vector CHC::currentBlockVariables() -{ - if (m_currentFunction) - return currentFunctionVariables() + applyMap(m_currentFunction->localVariables(), [this](auto _var) { return currentValue(*_var); }); - - return currentFunctionVariables(); -} - string CHC::predicateName(ASTNode const* _node, ContractDefinition const* _contract) { string prefix; @@ -1019,15 +949,31 @@ string CHC::predicateName(ASTNode const* _node, ContractDefinition const* _contr smtutil::Expression CHC::predicate(Predicate const& _block) { - return _block(currentBlockVariables()); -} - -smtutil::Expression CHC::predicate( - Predicate const& _block, - vector const& _arguments -) -{ - return _block(_arguments); + switch (_block.type()) + { + case PredicateType::Interface: + solAssert(m_currentContract, ""); + return ::interface(_block, *m_currentContract, m_context); + case PredicateType::ImplicitConstructor: + solAssert(m_currentContract, ""); + return implicitConstructor(_block, *m_currentContract, m_context); + case PredicateType::ConstructorSummary: + solAssert(m_currentContract, ""); + return constructor(_block, *m_currentContract, m_context); + case PredicateType::FunctionEntry: + case PredicateType::FunctionSummary: + solAssert(m_currentFunction, ""); + return smt::function(_block, *m_currentFunction, m_currentContract, m_context); + case PredicateType::FunctionBlock: + solAssert(m_currentFunction, ""); + return functionBlock(_block, *m_currentFunction, m_currentContract, m_context); + case PredicateType::Error: + return _block({}); + case PredicateType::NondetInterface: + // Nondeterministic interface predicates are handled differently. + solAssert(false, ""); + } + solAssert(false, ""); } smtutil::Expression CHC::predicate(FunctionCall const& _funCall) diff --git a/libsolidity/formal/CHC.h b/libsolidity/formal/CHC.h index 328d4cfda..bd6ab3888 100644 --- a/libsolidity/formal/CHC.h +++ b/libsolidity/formal/CHC.h @@ -111,7 +111,7 @@ private: void resetContractAnalysis(); void eraseKnowledge(); void clearIndices(ContractDefinition const* _contract, FunctionDefinition const* _function = nullptr) override; - void setCurrentBlock(Predicate const& _block, std::vector const* _arguments = nullptr); + void setCurrentBlock(Predicate const& _block); std::set transactionAssertions(ASTNode const* _txRoot); //@} @@ -124,7 +124,7 @@ private: /// Predicate helpers. //@{ /// @returns a new block of given _sort and _name. - Predicate const* createSymbolicBlock(smtutil::SortPointer _sort, std::string const& _name, ASTNode const* _node = nullptr); + Predicate const* createSymbolicBlock(smtutil::SortPointer _sort, std::string const& _name, PredicateType _predType, ASTNode const* _node = nullptr); /// Creates summary predicates for all functions of all contracts /// in a given _source. @@ -138,7 +138,7 @@ private: smtutil::Expression error(unsigned _idx); /// Creates a block for the given _node. - Predicate const* createBlock(ASTNode const* _node, std::string const& _prefix = ""); + Predicate const* createBlock(ASTNode const* _node, PredicateType _predType, std::string const& _prefix = ""); /// Creates a call block for the given function _function from contract _contract. /// The contract is needed here because of inheritance. Predicate const* createSummaryBlock(FunctionDefinition const& _function, ContractDefinition const& _contract); @@ -152,29 +152,16 @@ private: /// @returns the symbolic values of the state variables at the beginning /// of the current transaction. std::vector initialStateVariables(); - std::vector initialStateVariables(ContractDefinition const& _contract); std::vector stateVariablesAtIndex(unsigned _index); std::vector stateVariablesAtIndex(unsigned _index, ContractDefinition const& _contract); /// @returns the current symbolic values of the current state variables. std::vector currentStateVariables(); std::vector currentStateVariables(ContractDefinition const& _contract); - /// @returns the current symbolic values of the current function's - /// input and output parameters. - std::vector currentFunctionVariables(); - std::vector currentFunctionVariables(FunctionDefinition const& _function); - std::vector currentFunctionVariables(ContractDefinition const& _contract); - - /// @returns the same as currentFunctionVariables plus - /// local variables. - std::vector currentBlockVariables(); - /// @returns the predicate name for a given node. std::string predicateName(ASTNode const* _node, ContractDefinition const* _contract = nullptr); - /// @returns a predicate application over the current scoped variables. + /// @returns a predicate application after checking the predicate's type. smtutil::Expression predicate(Predicate const& _block); - /// @returns a predicate application over @param _arguments. - smtutil::Expression predicate(Predicate const& _block, std::vector const& _arguments); /// @returns the summary predicate for the called function. smtutil::Expression predicate(FunctionCall const& _funCall); /// @returns a predicate that defines a constructor summary. diff --git a/libsolidity/formal/Predicate.cpp b/libsolidity/formal/Predicate.cpp index 9f897d63f..9d3f856ce 100644 --- a/libsolidity/formal/Predicate.cpp +++ b/libsolidity/formal/Predicate.cpp @@ -36,6 +36,7 @@ map Predicate::m_predicates; Predicate const* Predicate::create( SortPointer _sort, string _name, + PredicateType _type, EncodingContext& _context, ASTNode const* _node ) @@ -46,15 +47,17 @@ Predicate const* Predicate::create( return &m_predicates.emplace( std::piecewise_construct, std::forward_as_tuple(functorName), - std::forward_as_tuple(move(predicate), _node) + std::forward_as_tuple(move(predicate), _type, _node) ).first->second; } Predicate::Predicate( smt::SymbolicFunctionVariable&& _predicate, + PredicateType _type, ASTNode const* _node ): m_predicate(move(_predicate)), + m_type(_type), m_node(_node) { } diff --git a/libsolidity/formal/Predicate.h b/libsolidity/formal/Predicate.h index 3da5ad453..addf5ea32 100644 --- a/libsolidity/formal/Predicate.h +++ b/libsolidity/formal/Predicate.h @@ -30,6 +30,18 @@ namespace solidity::frontend { +enum class PredicateType +{ + Interface, + NondetInterface, + ImplicitConstructor, + ConstructorSummary, + FunctionEntry, + FunctionSummary, + FunctionBlock, + Error +}; + /** * Represents a predicate used by the CHC engine. */ @@ -39,12 +51,14 @@ public: static Predicate const* create( smtutil::SortPointer _sort, std::string _name, + PredicateType _type, smt::EncodingContext& _context, ASTNode const* _node = nullptr ); Predicate( smt::SymbolicFunctionVariable&& _predicate, + PredicateType _type, ASTNode const* _node = nullptr ); @@ -88,6 +102,8 @@ public: /// @returns true if this predicate represents an interface. bool isInterface() const; + PredicateType type() const { return m_type; } + /// @returns a formatted string representing a call to this predicate /// with _args. std::string formatSummaryCall(std::vector const& _args) const; @@ -108,6 +124,9 @@ private: /// The actual SMT expression. smt::SymbolicFunctionVariable m_predicate; + /// The type of this predicate. + PredicateType m_type; + /// The ASTNode that this predicate represents. /// nullptr if this predicate is not associated with a specific program AST node. ASTNode const* m_node = nullptr; diff --git a/libsolidity/formal/PredicateInstance.cpp b/libsolidity/formal/PredicateInstance.cpp new file mode 100644 index 000000000..8bece398e --- /dev/null +++ b/libsolidity/formal/PredicateInstance.cpp @@ -0,0 +1,120 @@ +/* + 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 . +*/ +// SPDX-License-Identifier: GPL-3.0 + +#include + +#include +#include + +using namespace std; +using namespace solidity::util; +using namespace solidity::smtutil; + +namespace solidity::frontend::smt +{ + +smtutil::Expression interface(Predicate const& _pred, ContractDefinition const& _contract, EncodingContext& _context) +{ + return _pred(currentStateVariables(_contract, _context)); +} + +smtutil::Expression constructor(Predicate const& _pred, ContractDefinition const& _contract, EncodingContext& _context) +{ + 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({}); +} + +smtutil::Expression function( + Predicate const& _pred, + FunctionDefinition const& _function, + ContractDefinition const* _contract, + EncodingContext& _context +) +{ + return _pred(currentFunctionVariables(_function, _contract, _context)); +} + +smtutil::Expression functionBlock( + Predicate const& _pred, + FunctionDefinition const& _function, + ContractDefinition const* _contract, + EncodingContext& _context +) +{ + return _pred(currentBlockVariables(_function, _contract, _context)); +} + +/// Helpers + +vector initialStateVariables(ContractDefinition const& _contract, EncodingContext& _context) +{ + return stateVariablesAtIndex(0, _contract, _context); +} + +vector stateVariablesAtIndex(unsigned _index, ContractDefinition const& _contract, EncodingContext& _context) +{ + return applyMap( + SMTEncoder::stateVariablesIncludingInheritedAndPrivate(_contract), + [&](auto _var) { return _context.variable(*_var)->valueAtIndex(_index); } + ); +} + +vector currentStateVariables(ContractDefinition const& _contract, EncodingContext& _context) +{ + return applyMap( + SMTEncoder::stateVariablesIncludingInheritedAndPrivate(_contract), + [&](auto _var) { return _context.variable(*_var)->currentValue(); } + ); +} + +vector currentFunctionVariables( + FunctionDefinition const& _function, + ContractDefinition const* _contract, + EncodingContext& _context +) +{ + vector exprs{_context.state().errorFlag().currentValue()}; + exprs += _contract ? initialStateVariables(*_contract, _context) : vector{}; + exprs += applyMap(_function.parameters(), [&](auto _var) { return _context.variable(*_var)->valueAtIndex(0); }); + 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(); }); + return exprs; +} + +vector currentBlockVariables(FunctionDefinition const& _function, ContractDefinition const* _contract, EncodingContext& _context) +{ + return currentFunctionVariables(_function, _contract, _context) + + applyMap( + _function.localVariables(), + [&](auto _var) { return _context.variable(*_var)->currentValue(); } + ); +} + +} diff --git a/libsolidity/formal/PredicateInstance.h b/libsolidity/formal/PredicateInstance.h new file mode 100644 index 000000000..185807e5e --- /dev/null +++ b/libsolidity/formal/PredicateInstance.h @@ -0,0 +1,73 @@ +/* + 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 . +*/ +// SPDX-License-Identifier: GPL-3.0 + +#pragma once + +#include + +namespace solidity::frontend::smt +{ + +class EncodingContext; + +/** + * This file represents the specification for building CHC predicate instances. + * The predicates follow the specification in PredicateSort.h. + * */ + +smtutil::Expression interface(Predicate const& _pred, ContractDefinition const& _contract, EncodingContext& _context); + +smtutil::Expression constructor(Predicate const& _pred, ContractDefinition const& _contract, EncodingContext& _context); + +smtutil::Expression implicitConstructor(Predicate const& _pred, ContractDefinition const& _contract, EncodingContext& _context); + +smtutil::Expression function( + Predicate const& _pred, + FunctionDefinition const& _function, + ContractDefinition const* _contract, + EncodingContext& _context +); + +smtutil::Expression functionBlock( + Predicate const& _pred, + FunctionDefinition const& _function, + ContractDefinition const* _contract, + EncodingContext& _context +); + +/// Helpers + +std::vector initialStateVariables(ContractDefinition const& _contract, EncodingContext& _context); + +std::vector stateVariablesAtIndex(unsigned _index, ContractDefinition const& _contract, EncodingContext& _context); + +std::vector currentStateVariables(ContractDefinition const& _contract, EncodingContext& _context); + +std::vector currentFunctionVariables( + FunctionDefinition const& _function, + ContractDefinition const* _contract, + EncodingContext& _context +); + +std::vector currentBlockVariables( + FunctionDefinition const& _function, + ContractDefinition const* _contract, + EncodingContext& _context +); + +}