cerc-io/solidity
11
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

Merge remote-tracking branch 'origin/develop' into develop_060

Browse Source
This commit is contained in:
chriseth
2019-11-14 13:42:46 +01:00
parent 8569fe7764 42338a5964
commit 216e1749f4
85 changed files with 1406 additions and 110 deletions
Download Patch File Download Diff File Expand all files Collapse all files
libsolidity/formal/BMC.cpp
+8 -3
View File
@@ -428,15 +428,20 @@ void BMC::inlineFunctionCall(FunctionCall const& _funCall)
auto const& funType = dynamic_cast<FunctionType const*>(calledExpr->annotation().type);
solAssert(funType, "");
auto const& functionParams = funDef->parameters();
auto const& arguments = _funCall.arguments();
unsigned firstParam = 0;
if (funType->bound())
{
auto const& boundFunction = dynamic_cast<MemberAccess const*>(calledExpr);
solAssert(boundFunction, "");
funArgs.push_back(expr(boundFunction->expression()));
funArgs.push_back(expr(boundFunction->expression(), functionParams.front()->type()));
firstParam = 1;
}
for (auto arg: _funCall.arguments())
funArgs.push_back(expr(*arg));
solAssert((arguments.size() + firstParam) == functionParams.size(), "");
for (unsigned i = 0; i < arguments.size(); ++i)
funArgs.push_back(expr(*arguments.at(i), functionParams.at(i + firstParam)->type()));
initializeFunctionCallParameters(*funDef, funArgs);
// The reason why we need to pushCallStack here instead of visit(FunctionDefinition)
libsolidity/formal/CHC.cpp
+17 -5
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)
libsolidity/formal/CHC.h
+3 -3
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.
libsolidity/formal/SMTEncoder.cpp
+11 -7
View File
@@ -136,9 +136,13 @@ void SMTEncoder::visitFunctionOrModifier()
*modifierInvocation->name()->annotation().referencedDeclaration
);
vector<smt::Expression> modifierArgsExpr;
if (modifierInvocation->arguments())
for (auto arg: *modifierInvocation->arguments())
modifierArgsExpr.push_back(expr(*arg));
if (auto const* arguments = modifierInvocation->arguments())
{
auto const& modifierParams = modifierDef.parameters();
solAssert(modifierParams.size() == arguments->size(), "");
for (unsigned i = 0; i < arguments->size(); ++i)
modifierArgsExpr.push_back(expr(*arguments->at(i), modifierParams.at(i)->type()));
}
initializeFunctionCallParameters(modifierDef, modifierArgsExpr);
pushCallStack({&modifierDef, modifierInvocation.get()});
modifierDef.body().accept(*this);
@@ -595,10 +599,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")
@@ -699,7 +703,7 @@ void SMTEncoder::endVisit(Return const& _return)
}
}
else if (returnParams.size() == 1)
m_context.addAssertion(expr(*_return.expression()) == m_context.newValue(*returnParams.front()));
m_context.addAssertion(expr(*_return.expression(), returnParams.front()->type()) == m_context.newValue(*returnParams.front()));
}
}
@@ -1353,7 +1357,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);
}
libsolidity/formal/SymbolicTypes.cpp
+23 -1
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()))
libsolidity/formal/SymbolicVariables.cpp
+30 -4
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,
libsolidity/formal/SymbolicVariables.h
+29 -3
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
};
};
/**