cerc-io/solidity
16
0
Fork 0
mirror of https://github.com/ethereum/solidity synced 2023-10-03 13:03:40 +00:00
Code Issues Actions Packages Projects Releases Wiki Activity

[SMTChecker] Remove redundant CHC constraints

Browse Source
This commit is contained in:
Leonardo Alt 2020-04-14 23:25:56 +02:00
parent 10879bcae6
commit bca43586c6
6 changed files with 15 additions and 22 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

27
libsolidity/formal/CHC.cpp
View File

@ -130,15 +130,10 @@ bool CHC::visit(ContractDefinition const& _contract)
clearIndices(&_contract); clearIndices(&_contract);
auto errorFunctionSort = make_shared<smt::FunctionSort>(
vector<smt::SortPointer>(),
smt::SortProvider::boolSort
);
string suffix = _contract.name() + "_" + to_string(_contract.id()); string suffix = _contract.name() + "_" + to_string(_contract.id());
m_errorPredicate = createSymbolicBlock(errorFunctionSort, "error_" + suffix); m_errorPredicate = createSymbolicBlock(arity0FunctionSort(), "error_" + suffix);
m_constructorSummaryPredicate = createSymbolicBlock(constructorSort(), "summary_constructor_" + suffix); m_constructorSummaryPredicate = createSymbolicBlock(constructorSort(), "summary_constructor_" + suffix);
m_implicitConstructorPredicate = createSymbolicBlock(interfaceSort(), "implicit_constructor_" + suffix); m_implicitConstructorPredicate = createSymbolicBlock(arity0FunctionSort(), "implicit_constructor_" + suffix);
auto stateExprs = currentStateVariables(); auto stateExprs = currentStateVariables();
setCurrentBlock(*m_interfaces.at(m_currentContract), &stateExprs); setCurrentBlock(*m_interfaces.at(m_currentContract), &stateExprs);
@ -148,15 +143,7 @@ bool CHC::visit(ContractDefinition const& _contract)
void CHC::endVisit(ContractDefinition const& _contract) void CHC::endVisit(ContractDefinition const& _contract)
{ {
for (auto const& var: m_stateVariables) auto implicitConstructor = (*m_implicitConstructorPredicate)({});
{
solAssert(m_context.knownVariable(*var), "");
auto const& symbVar = m_context.variable(*var);
symbVar->resetIndex();
m_context.setZeroValue(*var);
symbVar->increaseIndex();
}
auto implicitConstructor = (*m_implicitConstructorPredicate)(initialStateVariables());
connectBlocks(genesis(), implicitConstructor); connectBlocks(genesis(), implicitConstructor);
m_currentBlock = implicitConstructor; m_currentBlock = implicitConstructor;
m_context.addAssertion(m_error.currentValue() == 0); m_context.addAssertion(m_error.currentValue() == 0);
@ -682,6 +669,14 @@ smt::SortPointer CHC::interfaceSort(ContractDefinition const& _contract)
); );
} }
smt::SortPointer CHC::arity0FunctionSort()
{
return make_shared<smt::FunctionSort>(
vector<smt::SortPointer>(),
smt::SortProvider::boolSort
);
}
/// A function in the symbolic CFG requires: /// A function in the symbolic CFG requires:
/// - Index of failed assertion. 0 means no assertion failed. /// - Index of failed assertion. 0 means no assertion failed.
/// - 2 sets of state variables: /// - 2 sets of state variables:

1
libsolidity/formal/CHC.h
View File

@ -106,6 +106,7 @@ private:
smt::SortPointer constructorSort(); smt::SortPointer constructorSort();
smt::SortPointer interfaceSort(); smt::SortPointer interfaceSort();
static smt::SortPointer interfaceSort(ContractDefinition const& _const); static smt::SortPointer interfaceSort(ContractDefinition const& _const);
smt::SortPointer arity0FunctionSort();
smt::SortPointer sort(FunctionDefinition const& _function); smt::SortPointer sort(FunctionDefinition const& _function);
smt::SortPointer sort(ASTNode const* _block); smt::SortPointer sort(ASTNode const* _block);
/// @returns the sort of a predicate that represents the summary of _function in the scope of _contract. /// @returns the sort of a predicate that represents the summary of _function in the scope of _contract.

4
libsolidity/formal/SMTEncoder.cpp
View File

@ -107,6 +107,9 @@ void SMTEncoder::endVisit(ContractDefinition const& _contract)
solAssert(m_currentContract == &_contract, ""); solAssert(m_currentContract == &_contract, "");
m_currentContract = nullptr; m_currentContract = nullptr;
if (m_callStack.empty())
m_context.popSolver();
} }
void SMTEncoder::endVisit(VariableDeclaration const& _varDecl) void SMTEncoder::endVisit(VariableDeclaration const& _varDecl)
@ -662,7 +665,6 @@ void SMTEncoder::initFunction(FunctionDefinition const& _function)
{ {
solAssert(m_callStack.empty(), ""); solAssert(m_callStack.empty(), "");
solAssert(m_currentContract, ""); solAssert(m_currentContract, "");
m_context.reset();
m_context.pushSolver(); m_context.pushSolver();
m_pathConditions.clear(); m_pathConditions.clear();
pushCallStack({&_function, nullptr}); pushCallStack({&_function, nullptr});

1
test/libsolidity/smtCheckerTests/types/function_type_nested.sol
View File

@ -18,5 +18,4 @@ contract C {
// Warning: (212-219): Assertion checker does not yet implement this type of function call. // Warning: (212-219): Assertion checker does not yet implement this type of function call.
// Warning: (255-257): Internal error: Expression undefined for SMT solver. // Warning: (255-257): Internal error: Expression undefined for SMT solver.
// Warning: (255-257): Assertion checker does not yet implement type function (function (uint256)) // Warning: (255-257): Assertion checker does not yet implement type function (function (uint256))
// Warning: (212-214): Assertion checker does not yet implement type function (function (uint256))
// Warning: (212-219): Assertion checker does not yet implement this type of function call. // Warning: (212-219): Assertion checker does not yet implement this type of function call.

2
test/libsolidity/smtCheckerTests/types/function_type_nested_return.sol
View File

@ -22,6 +22,4 @@ contract C {
// Warning: (284-291): Assertion checker does not yet implement this type of function call. // Warning: (284-291): Assertion checker does not yet implement this type of function call.
// Warning: (327-329): Internal error: Expression undefined for SMT solver. // Warning: (327-329): Internal error: Expression undefined for SMT solver.
// Warning: (327-329): Assertion checker does not yet implement type function (function (uint256)) // Warning: (327-329): Assertion checker does not yet implement type function (function (uint256))
// Warning: (284-286): Assertion checker does not yet implement type function (function (uint256))
// Warning: (287-288): Assertion checker does not yet support this global variable.
// Warning: (284-291): Assertion checker does not yet implement this type of function call. // Warning: (284-291): Assertion checker does not yet implement this type of function call.

2
test/libsolidity/smtCheckerTests/types/tuple_return_branch.sol
View File

@ -19,7 +19,5 @@ contract C {
// Warning: (137-141): Assertion checker does not yet implement type struct C.S memory // Warning: (137-141): Assertion checker does not yet implement type struct C.S memory
// Warning: (137-141): Assertion checker does not yet implement this expression. // Warning: (137-141): Assertion checker does not yet implement this expression.
// Warning: (193-203): Assertion checker does not yet support the type of this variable. // Warning: (193-203): Assertion checker does not yet support the type of this variable.
// Warning: (137-138): Assertion checker does not yet implement type type(struct C.S storage pointer)
// Warning: (137-141): Assertion checker does not yet implement type struct C.S memory
// Warning: (137-141): Assertion checker does not yet implement this expression. // Warning: (137-141): Assertion checker does not yet implement this expression.
// Warning: (227-228): Assertion checker does not yet implement type struct C.S memory // Warning: (227-228): Assertion checker does not yet implement type struct C.S memory