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] Fix ICE in CHC when function used as argument

Browse Source
This commit is contained in:
Leonardo Alt 2019-11-10 18:58:29 +01:00
parent c0cf96cbc1
commit e3652627fd
15 changed files with 215 additions and 19 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
Changelog.md
View File

@ -17,6 +17,7 @@ Bugfixes:
* Code Generator: Fixed a faulty assert that would wrongly trigger for array sizes exceeding unsigned integer
* Type Checker: Treat magic variables as unknown identifiers in inline assembly
* SMTChecker: Fix internal error when accessing indices of fixed bytes.
* SMTChecker: Fix internal error when using function pointers as arguments.

22
libsolidity/formal/CHC.cpp
View File

@ -508,7 +508,13 @@ smt::SortPointer CHC::sort(FunctionDefinition const& _function)
auto boolSort = make_shared<smt::Sort>(smt::Kind::Bool);
vector<smt::SortPointer> varSorts;
for (auto const& var: _function.parameters() + _function.returnParameters())
varSorts.push_back(smt::smtSort(*var->type()));
{
// SMT solvers do not support function types as arguments.
if (var->type()->category() == Type::Category::Function)
varSorts.push_back(make_shared<smt::Sort>(smt::Kind::Int));
else
varSorts.push_back(smt::smtSort(*var->type()));
}
return make_shared<smt::FunctionSort>(
m_stateSorts + varSorts,
boolSort
@ -526,7 +532,13 @@ smt::SortPointer CHC::sort(ASTNode const* _node)
auto boolSort = make_shared<smt::Sort>(smt::Kind::Bool);
vector<smt::SortPointer> varSorts;
for (auto const& var: m_currentFunction->localVariables())
varSorts.push_back(smt::smtSort(*var->type()));
{
// SMT solvers do not support function types as arguments.
if (var->type()->category() == Type::Category::Function)
varSorts.push_back(make_shared<smt::Sort>(smt::Kind::Int));
else
varSorts.push_back(smt::smtSort(*var->type()));
}
return make_shared<smt::FunctionSort>(
fSort->domain + varSorts,
boolSort
@ -540,7 +552,7 @@ unique_ptr<smt::SymbolicFunctionVariable> CHC::createSymbolicBlock(smt::SortPoin
_name,
m_context
);
m_interface->registerRelation(block->currentValue());
m_interface->registerRelation(block->currentFunctionValue());
return block;
}
@ -572,7 +584,7 @@ smt::Expression CHC::error()
smt::Expression CHC::error(unsigned _idx)
{
return m_errorPredicate->valueAtIndex(_idx)({});
return m_errorPredicate->functionValueAtIndex(_idx)({});
}
unique_ptr<smt::SymbolicFunctionVariable> CHC::createBlock(ASTNode const* _node, string const& _prefix)
@ -589,7 +601,7 @@ void CHC::createErrorBlock()
{
solAssert(m_errorPredicate, "");
m_errorPredicate->increaseIndex();
m_interface->registerRelation(m_errorPredicate->currentValue());
m_interface->registerRelation(m_errorPredicate->currentFunctionValue());
}
void CHC::connectBlocks(smt::Expression const& _from, smt::Expression const& _to, smt::Expression const& _constraints)

6
libsolidity/formal/CHC.h
View File

@ -154,15 +154,15 @@ private:
//@{
/// Constructor predicate.
/// Default constructor sets state vars to 0.
std::unique_ptr<smt::SymbolicVariable> m_constructorPredicate;
std::unique_ptr<smt::SymbolicFunctionVariable> m_constructorPredicate;
/// Artificial Interface predicate.
/// Single entry block for all functions.
std::unique_ptr<smt::SymbolicVariable> m_interfacePredicate;
std::unique_ptr<smt::SymbolicFunctionVariable> m_interfacePredicate;
/// Artificial Error predicate.
/// Single error block for all assertions.
std::unique_ptr<smt::SymbolicVariable> m_errorPredicate;
std::unique_ptr<smt::SymbolicFunctionVariable> m_errorPredicate;
//@}
/// Variables.

6
libsolidity/formal/SMTEncoder.cpp
View File

@ -594,10 +594,10 @@ void SMTEncoder::endVisit(Identifier const& _identifier)
{
// Will be translated as part of the node that requested the lvalue.
}
else if (_identifier.annotation().type->category() == Type::Category::Function)
visitFunctionIdentifier(_identifier);
else if (auto decl = identifierToVariable(_identifier))
defineExpr(_identifier, currentValue(*decl));
else if (_identifier.annotation().type->category() == Type::Category::Function)
visitFunctionIdentifier(_identifier);
else if (_identifier.name() == "now")
defineGlobalVariable(_identifier.name(), _identifier);
else if (_identifier.name() == "this")
@ -1343,7 +1343,7 @@ void SMTEncoder::createExpr(Expression const& _e)
void SMTEncoder::defineExpr(Expression const& _e, smt::Expression _value)
{
createExpr(_e);
solAssert(smt::smtKind(_e.annotation().type->category()) != smt::Kind::Function, "Equality operator applied to type that is not fully supported");
solAssert(_value.sort->kind != smt::Kind::Function, "Equality operator applied to type that is not fully supported");
m_context.addAssertion(expr(_e) == _value);
}

24
libsolidity/formal/SymbolicTypes.cpp
View File

@ -19,6 +19,7 @@
#include <libsolidity/ast/TypeProvider.h>
#include <libsolidity/ast/Types.h>
#include <libdevcore/CommonData.h>
#include <memory>
using namespace std;
@ -139,7 +140,28 @@ pair<bool, shared_ptr<SymbolicVariable>> newSymbolicVariable(
else if (isBool(_type.category()))
var = make_shared<SymbolicBoolVariable>(type, _uniqueName, _context);
else if (isFunction(_type.category()))
var = make_shared<SymbolicFunctionVariable>(type, _uniqueName, _context);
{
auto const& fType = dynamic_cast<FunctionType const*>(type);
auto const& paramsIn = fType->parameterTypes();
auto const& paramsOut = fType->returnParameterTypes();
auto findFunctionParam = [&](auto&& params) {
return find_if(
begin(params),
end(params),
[&](TypePointer _paramType) { return _paramType->category() == solidity::Type::Category::Function; }
);
};
if (
findFunctionParam(paramsIn) != end(paramsIn) ||
findFunctionParam(paramsOut) != end(paramsOut)
)
{
abstract = true;
var = make_shared<SymbolicIntVariable>(TypeProvider::uint256(), type, _uniqueName, _context);
}
else
var = make_shared<SymbolicFunctionVariable>(type, _uniqueName, _context);
}
else if (isInteger(_type.category()))
var = make_shared<SymbolicIntVariable>(type, type, _uniqueName, _context);
else if (isFixedBytes(_type.category()))

34
libsolidity/formal/SymbolicVariables.cpp
View File

@ -19,7 +19,6 @@
#include <libsolidity/formal/SymbolicTypes.h>
#include <libsolidity/ast/AST.h>
#include <libsolidity/ast/TypeProvider.h>
using namespace std;
using namespace dev;
@ -153,16 +152,38 @@ SymbolicFunctionVariable::SymbolicFunctionVariable(
solAssert(m_sort->kind == Kind::Function, "");
}
void SymbolicFunctionVariable::resetDeclaration()
Expression SymbolicFunctionVariable::currentValue(solidity::TypePointer const& _targetType) const
{
m_declaration = m_context.newVariable(currentName(), m_sort);
return m_abstract.currentValue(_targetType);
}
Expression SymbolicFunctionVariable::currentFunctionValue() const
{
return m_declaration;
}
Expression SymbolicFunctionVariable::valueAtIndex(int _index) const
{
return m_abstract.valueAtIndex(_index);
}
Expression SymbolicFunctionVariable::functionValueAtIndex(int _index) const
{
return SymbolicVariable::valueAtIndex(_index);
}
Expression SymbolicFunctionVariable::resetIndex()
{
SymbolicVariable::resetIndex();
return m_abstract.resetIndex();
}
Expression SymbolicFunctionVariable::increaseIndex()
{
++(*m_ssa);
resetDeclaration();
return currentValue();
m_abstract.increaseIndex();
return m_abstract.currentValue();
}
Expression SymbolicFunctionVariable::operator()(vector<Expression> _arguments) const
@ -170,6 +191,11 @@ Expression SymbolicFunctionVariable::operator()(vector<Expression> _arguments) c
return m_declaration(_arguments);
}
void SymbolicFunctionVariable::resetDeclaration()
{
m_declaration = m_context.newVariable(currentName(), m_sort);
}
SymbolicMappingVariable::SymbolicMappingVariable(
solidity::TypePointer _type,
string _uniqueName,

32
libsolidity/formal/SymbolicVariables.h
View File

@ -20,6 +20,7 @@
#include <libsolidity/formal/SolverInterface.h>
#include <libsolidity/formal/SSAVariable.h>
#include <libsolidity/ast/Types.h>
#include <libsolidity/ast/TypeProvider.h>
#include <memory>
namespace dev
@ -138,7 +139,12 @@ public:
};
/**
* Specialization of SymbolicVariable for FunctionType
* Specialization of SymbolicVariable for FunctionType.
* Besides containing a symbolic function declaration,
* it also has an integer used as abstraction.
* By default, the abstract representation is used when
* values are requested, and the function declaration is
* used when operator() is applied over arguments.
*/
class SymbolicFunctionVariable: public SymbolicVariable
{
@ -154,8 +160,20 @@ public:
EncodingContext& _context
);
Expression increaseIndex();
Expression operator()(std::vector<Expression> _arguments) const;
Expression currentValue(solidity::TypePointer const& _targetType = TypePointer{}) const override;
// Explicit request the function declaration.
Expression currentFunctionValue() const;
Expression valueAtIndex(int _index) const override;
// Explicit request the function declaration.
Expression functionValueAtIndex(int _index) const;
Expression resetIndex() override;
Expression increaseIndex() override;
Expression operator()(std::vector<Expression> _arguments) const override;
private:
/// Creates a new function declaration.
@ -163,6 +181,14 @@ private:
/// Stores the current function declaration.
Expression m_declaration;
/// Abstract representation.
SymbolicIntVariable m_abstract{
TypeProvider::uint256(),
TypeProvider::uint256(),
m_uniqueName + "_abstract",
m_context
};
};
/**

10
test/libsolidity/smtCheckerTests/typecast/function_type_to_address.sol Normal file
View File

@ -0,0 +1,10 @@
pragma experimental SMTChecker;
contract C {
function f(address a, function(uint) external g) internal pure {
address b = address(g);
assert(a == b);
}
}
// ----
// Warning: (128-138): Type conversion is not yet fully supported and might yield false positives.
// Warning: (142-156): Assertion violation happens here

8
test/libsolidity/smtCheckerTests/typecast/function_type_to_function_type_external.sol Normal file
View File

@ -0,0 +1,8 @@
pragma experimental SMTChecker;
contract C {
function f(function(uint) external returns (uint) g, function(uint) external returns (uint) h) public {
assert(g(2) == h(2));
}
}
// ----
// Warning: (155-175): Assertion violation happens here

13
test/libsolidity/smtCheckerTests/typecast/function_type_to_function_type_internal.sol Normal file
View File

@ -0,0 +1,13 @@
pragma experimental SMTChecker;
contract C {
function f(function(uint) returns (uint) g, function(uint) returns (uint) h) internal {
assert(g(2) == h(2));
assert(g == h);
}
}
// ----
// Warning: (146-150): Assertion checker does not yet implement this type of function call.
// Warning: (154-158): Assertion checker does not yet implement this type of function call.
// Warning: (170-176): Assertion checker does not yet implement the type function (uint256) returns (uint256) for comparisons
// Warning: (139-159): Assertion violation happens here
// Warning: (163-177): Assertion violation happens here

5
test/libsolidity/smtCheckerTests/types/function_type_as_argument.sol Normal file
View File

@ -0,0 +1,5 @@
pragma experimental SMTChecker;
contract C {
function f(function(uint) external g) public {
}
}

13
test/libsolidity/smtCheckerTests/types/function_type_call.sol Normal file
View File

@ -0,0 +1,13 @@
pragma experimental SMTChecker;
contract C {
function(uint) m_g;
function f(function(uint) internal g) internal {
g(2);
}
function h() public {
f(m_g);
}
}
// ----
// Warning: (121-125): Assertion checker does not yet implement this type of function call.
// Warning: (121-125): Assertion checker does not yet implement this type of function call.

11
test/libsolidity/smtCheckerTests/types/function_type_members.sol Normal file
View File

@ -0,0 +1,11 @@
pragma experimental SMTChecker;
contract C {
function f(function(uint) external payable g) internal {
g.selector;
g.gas(2).value(3)(4);
}
}
// ----
// Warning: (108-118): Assertion checker does not yet support this expression.
// Warning: (122-130): Assertion checker does not yet implement this type of function call.
// Warning: (122-139): Assertion checker does not yet implement this type of function call.

22
test/libsolidity/smtCheckerTests/types/function_type_nested.sol Normal file
View File

@ -0,0 +1,22 @@
pragma experimental SMTChecker;
contract C {
function(uint) m_g;
function f1(function(uint) internal g1) internal {
g1(2);
}
function f2(function(function(uint) internal) internal g2) internal {
g2(m_g);
}
function h() public {
f2(f1);
}
}
// ----
// Warning: (123-128): Assertion checker does not yet implement this type of function call.
// Warning: (152-197): Assertion checker does not yet support the type of this variable.
// 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: (255-257): Internal error: Expression undefined for SMT solver.
// 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.

27
test/libsolidity/smtCheckerTests/types/function_type_nested_return.sol Normal file
View File

@ -0,0 +1,27 @@
pragma experimental SMTChecker;
contract C {
function(uint) m_g;
function r() internal view returns (function(uint)) {
return m_g;
}
function f1(function(uint) internal g1) internal {
g1(2);
}
function f2(function(function(uint) internal) internal g2) internal {
g2(r());
}
function h() public {
f2(f1);
}
}
// ----
// Warning: (195-200): Assertion checker does not yet implement this type of function call.
// Warning: (224-269): Assertion checker does not yet support the type of this variable.
// 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: (327-329): Internal error: Expression undefined for SMT solver.
// 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.