cerc-io/solidity
15
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 pull request #6717 from ethereum/smt_namespace

Browse Source 
Move SMT specific code into smt namespace
This commit is contained in:
chriseth 2019-05-13 12:45:34 +02:00 committed by GitHub
commit 01dd9ba2ae
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
10 changed files with 223 additions and 205 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

68
libsolidity/formal/SMTChecker.cpp
View File

@ -332,7 +332,7 @@ void SMTChecker::endVisit(VariableDeclarationStatement const& _varDecl)
{ {
if (auto init = _varDecl.initialValue()) if (auto init = _varDecl.initialValue())
{ {
auto symbTuple = dynamic_pointer_cast<SymbolicTupleVariable>(m_expressions[init]); auto symbTuple = dynamic_pointer_cast<smt::SymbolicTupleVariable>(m_expressions[init]);
/// symbTuple == nullptr if it is the return of a non-inlined function call. /// symbTuple == nullptr if it is the return of a non-inlined function call.
if (symbTuple) if (symbTuple)
{ {
@ -375,7 +375,7 @@ void SMTChecker::endVisit(Assignment const& _assignment)
_assignment.location(), _assignment.location(),
"Assertion checker does not yet implement this assignment operator." "Assertion checker does not yet implement this assignment operator."
); );
else if (!isSupportedType(_assignment.annotation().type->category())) else if (!smt::isSupportedType(_assignment.annotation().type->category()))
{ {
m_errorReporter.warning( m_errorReporter.warning(
_assignment.location(), _assignment.location(),
@ -390,7 +390,7 @@ void SMTChecker::endVisit(Assignment const& _assignment)
vector<smt::Expression> rightArguments; vector<smt::Expression> rightArguments;
if (_assignment.rightHandSide().annotation().type->category() == Type::Category::Tuple) if (_assignment.rightHandSide().annotation().type->category() == Type::Category::Tuple)
{ {
auto symbTuple = dynamic_pointer_cast<SymbolicTupleVariable>(m_expressions[&_assignment.rightHandSide()]); auto symbTuple = dynamic_pointer_cast<smt::SymbolicTupleVariable>(m_expressions[&_assignment.rightHandSide()]);
solAssert(symbTuple, ""); solAssert(symbTuple, "");
for (auto const& component: symbTuple->components()) for (auto const& component: symbTuple->components())
{ {
@ -426,7 +426,7 @@ void SMTChecker::endVisit(TupleExpression const& _tuple)
else if (_tuple.annotation().type->category() == Type::Category::Tuple) else if (_tuple.annotation().type->category() == Type::Category::Tuple)
{ {
createExpr(_tuple); createExpr(_tuple);
vector<shared_ptr<SymbolicVariable>> components; vector<shared_ptr<smt::SymbolicVariable>> components;
for (auto const& component: _tuple.components()) for (auto const& component: _tuple.components())
if (component) if (component)
{ {
@ -441,7 +441,7 @@ void SMTChecker::endVisit(TupleExpression const& _tuple)
else else
components.push_back(nullptr); components.push_back(nullptr);
solAssert(components.size() == _tuple.components().size(), ""); solAssert(components.size() == _tuple.components().size(), "");
auto const& symbTuple = dynamic_pointer_cast<SymbolicTupleVariable>(m_expressions[&_tuple]); auto const& symbTuple = dynamic_pointer_cast<smt::SymbolicTupleVariable>(m_expressions[&_tuple]);
solAssert(symbTuple, ""); solAssert(symbTuple, "");
symbTuple->setComponents(move(components)); symbTuple->setComponents(move(components));
} }
@ -450,7 +450,7 @@ void SMTChecker::endVisit(TupleExpression const& _tuple)
/// Parenthesized expressions are also TupleExpression regardless their type. /// Parenthesized expressions are also TupleExpression regardless their type.
auto const& components = _tuple.components(); auto const& components = _tuple.components();
solAssert(components.size() == 1, ""); solAssert(components.size() == 1, "");
if (isSupportedType(components.front()->annotation().type->category())) if (smt::isSupportedType(components.front()->annotation().type->category()))
defineExpr(_tuple, expr(*components.front())); defineExpr(_tuple, expr(*components.front()));
} }
} }
@ -490,7 +490,7 @@ void SMTChecker::checkUnderflow(OverflowTarget& _target)
solAssert(_target.type != OverflowTarget::Type::Overflow, ""); solAssert(_target.type != OverflowTarget::Type::Overflow, "");
auto intType = dynamic_cast<IntegerType const*>(_target.intType); auto intType = dynamic_cast<IntegerType const*>(_target.intType);
checkCondition( checkCondition(
_target.path && _target.value < minValue(*intType), _target.path && _target.value < smt::minValue(*intType),
_target.location, _target.location,
"Underflow (resulting value less than " + formatNumberReadable(intType->minValue()) + ")", "Underflow (resulting value less than " + formatNumberReadable(intType->minValue()) + ")",
"<result>", "<result>",
@ -503,7 +503,7 @@ void SMTChecker::checkOverflow(OverflowTarget& _target)
solAssert(_target.type != OverflowTarget::Type::Underflow, ""); solAssert(_target.type != OverflowTarget::Type::Underflow, "");
auto intType = dynamic_cast<IntegerType const*>(_target.intType); auto intType = dynamic_cast<IntegerType const*>(_target.intType);
checkCondition( checkCondition(
_target.path && _target.value > maxValue(*intType), _target.path && _target.value > smt::maxValue(*intType),
_target.location, _target.location,
"Overflow (resulting value larger than " + formatNumberReadable(intType->maxValue()) + ")", "Overflow (resulting value larger than " + formatNumberReadable(intType->maxValue()) + ")",
"<result>", "<result>",
@ -520,7 +520,7 @@ void SMTChecker::endVisit(UnaryOperation const& _op)
{ {
case Token::Not: // ! case Token::Not: // !
{ {
solAssert(isBool(_op.annotation().type->category()), ""); solAssert(smt::isBool(_op.annotation().type->category()), "");
defineExpr(_op, !expr(_op.subExpression())); defineExpr(_op, !expr(_op.subExpression()));
break; break;
} }
@ -528,7 +528,7 @@ void SMTChecker::endVisit(UnaryOperation const& _op)
case Token::Dec: // -- (pre- or postfix) case Token::Dec: // -- (pre- or postfix)
{ {
solAssert(isInteger(_op.annotation().type->category()), ""); solAssert(smt::isInteger(_op.annotation().type->category()), "");
solAssert(_op.subExpression().annotation().lValueRequested, ""); solAssert(_op.subExpression().annotation().lValueRequested, "");
if (auto identifier = dynamic_cast<Identifier const*>(&_op.subExpression())) if (auto identifier = dynamic_cast<Identifier const*>(&_op.subExpression()))
{ {
@ -785,13 +785,13 @@ void SMTChecker::inlineFunctionCall(FunctionCall const& _funCall)
auto const& returnParams = funDef->returnParameters(); auto const& returnParams = funDef->returnParameters();
if (returnParams.size() > 1) if (returnParams.size() > 1)
{ {
vector<shared_ptr<SymbolicVariable>> components; vector<shared_ptr<smt::SymbolicVariable>> components;
for (auto param: returnParams) for (auto param: returnParams)
{ {
solAssert(m_variables[param.get()], ""); solAssert(m_variables[param.get()], "");
components.push_back(m_variables[param.get()]); components.push_back(m_variables[param.get()]);
} }
auto const& symbTuple = dynamic_pointer_cast<SymbolicTupleVariable>(m_expressions[&_funCall]); auto const& symbTuple = dynamic_pointer_cast<smt::SymbolicTupleVariable>(m_expressions[&_funCall]);
solAssert(symbTuple, ""); solAssert(symbTuple, "");
symbTuple->setComponents(move(components)); symbTuple->setComponents(move(components));
} }
@ -837,7 +837,7 @@ void SMTChecker::endVisit(Identifier const& _identifier)
} }
else if (_identifier.annotation().type->category() == Type::Category::Function) else if (_identifier.annotation().type->category() == Type::Category::Function)
visitFunctionIdentifier(_identifier); visitFunctionIdentifier(_identifier);
else if (isSupportedType(_identifier.annotation().type->category())) else if (smt::isSupportedType(_identifier.annotation().type->category()))
{ {
if (auto decl = identifierToVariable(_identifier)) if (auto decl = identifierToVariable(_identifier))
defineExpr(_identifier, currentValue(*decl)); defineExpr(_identifier, currentValue(*decl));
@ -880,7 +880,7 @@ void SMTChecker::visitTypeConversion(FunctionCall const& _funCall)
{ {
auto const& intType = dynamic_cast<IntegerType const&>(*m_expressions.at(&_funCall)->type()); auto const& intType = dynamic_cast<IntegerType const&>(*m_expressions.at(&_funCall)->type());
defineExpr(_funCall, smt::Expression::ite( defineExpr(_funCall, smt::Expression::ite(
expr(*argument) >= minValue(intType) && expr(*argument) <= maxValue(intType), expr(*argument) >= smt::minValue(intType) && expr(*argument) <= smt::maxValue(intType),
expr(*argument), expr(*argument),
expr(_funCall) expr(_funCall)
)); ));
@ -908,9 +908,9 @@ void SMTChecker::endVisit(Literal const& _literal)
{ {
solAssert(_literal.annotation().type, "Expected type for AST node"); solAssert(_literal.annotation().type, "Expected type for AST node");
Type const& type = *_literal.annotation().type; Type const& type = *_literal.annotation().type;
if (isNumber(type.category())) if (smt::isNumber(type.category()))
defineExpr(_literal, smt::Expression(type.literalValue(&_literal))); defineExpr(_literal, smt::Expression(type.literalValue(&_literal)));
else if (isBool(type.category())) else if (smt::isBool(type.category()))
defineExpr(_literal, smt::Expression(_literal.token() == Token::TrueLiteral ? true : false)); defineExpr(_literal, smt::Expression(_literal.token() == Token::TrueLiteral ? true : false));
else else
{ {
@ -919,7 +919,7 @@ void SMTChecker::endVisit(Literal const& _literal)
auto stringType = TypeProvider::stringMemory(); auto stringType = TypeProvider::stringMemory();
auto stringLit = dynamic_cast<StringLiteralType const*>(_literal.annotation().type); auto stringLit = dynamic_cast<StringLiteralType const*>(_literal.annotation().type);
solAssert(stringLit, ""); solAssert(stringLit, "");
auto result = newSymbolicVariable(*stringType, stringLit->richIdentifier(), *m_interface); auto result = smt::newSymbolicVariable(*stringType, stringLit->richIdentifier(), *m_interface);
m_expressions.emplace(&_literal, result.second); m_expressions.emplace(&_literal, result.second);
} }
m_errorReporter.warning( m_errorReporter.warning(
@ -1006,7 +1006,7 @@ bool SMTChecker::visit(MemberAccess const& _memberAccess)
void SMTChecker::endVisit(IndexAccess const& _indexAccess) void SMTChecker::endVisit(IndexAccess const& _indexAccess)
{ {
shared_ptr<SymbolicVariable> array; shared_ptr<smt::SymbolicVariable> array;
if (auto const& id = dynamic_cast<Identifier const*>(&_indexAccess.baseExpression())) if (auto const& id = dynamic_cast<Identifier const*>(&_indexAccess.baseExpression()))
{ {
auto varDecl = identifierToVariable(*id); auto varDecl = identifierToVariable(*id);
@ -1121,7 +1121,7 @@ void SMTChecker::defineGlobalVariable(string const& _name, Expression const& _ex
{ {
if (!knownGlobalSymbol(_name)) if (!knownGlobalSymbol(_name))
{ {
auto result = newSymbolicVariable(*_expr.annotation().type, _name, *m_interface); auto result = smt::newSymbolicVariable(*_expr.annotation().type, _name, *m_interface);
m_globalContext.emplace(_name, result.second); m_globalContext.emplace(_name, result.second);
setUnknownValue(*result.second); setUnknownValue(*result.second);
if (result.first) if (result.first)
@ -1134,7 +1134,7 @@ void SMTChecker::defineGlobalVariable(string const& _name, Expression const& _ex
m_globalContext.at(_name)->increaseIndex(); m_globalContext.at(_name)->increaseIndex();
// The default behavior is not to increase the index since // The default behavior is not to increase the index since
// most of the global values stay the same throughout a tx. // most of the global values stay the same throughout a tx.
if (isSupportedType(_expr.annotation().type->category())) if (smt::isSupportedType(_expr.annotation().type->category()))
defineExpr(_expr, m_globalContext.at(_name)->currentValue()); defineExpr(_expr, m_globalContext.at(_name)->currentValue());
} }
@ -1142,7 +1142,7 @@ void SMTChecker::defineGlobalFunction(string const& _name, Expression const& _ex
{ {
if (!knownGlobalSymbol(_name)) if (!knownGlobalSymbol(_name))
{ {
auto result = newSymbolicVariable(*_expr.annotation().type, _name, *m_interface); auto result = smt::newSymbolicVariable(*_expr.annotation().type, _name, *m_interface);
m_globalContext.emplace(_name, result.second); m_globalContext.emplace(_name, result.second);
if (result.first) if (result.first)
m_errorReporter.warning( m_errorReporter.warning(
@ -1245,16 +1245,16 @@ smt::Expression SMTChecker::arithmeticOperation(
_location _location
); );
smt::Expression intValueRange = (0 - minValue(intType)) + maxValue(intType) + 1; smt::Expression intValueRange = (0 - smt::minValue(intType)) + smt::maxValue(intType) + 1;
value = smt::Expression::ite( value = smt::Expression::ite(
value > maxValue(intType) || value < minValue(intType), value > smt::maxValue(intType) || value < smt::minValue(intType),
value % intValueRange, value % intValueRange,
value value
); );
if (intType.isSigned()) if (intType.isSigned())
{ {
value = smt::Expression::ite( value = smt::Expression::ite(
value > maxValue(intType), value > smt::maxValue(intType),
value - intValueRange, value - intValueRange,
value value
); );
@ -1266,13 +1266,13 @@ smt::Expression SMTChecker::arithmeticOperation(
void SMTChecker::compareOperation(BinaryOperation const& _op) void SMTChecker::compareOperation(BinaryOperation const& _op)
{ {
solAssert(_op.annotation().commonType, ""); solAssert(_op.annotation().commonType, "");
if (isSupportedType(_op.annotation().commonType->category())) if (smt::isSupportedType(_op.annotation().commonType->category()))
{ {
smt::Expression left(expr(_op.leftExpression())); smt::Expression left(expr(_op.leftExpression()));
smt::Expression right(expr(_op.rightExpression())); smt::Expression right(expr(_op.rightExpression()));
Token op = _op.getOperator(); Token op = _op.getOperator();
shared_ptr<smt::Expression> value; shared_ptr<smt::Expression> value;
if (isNumber(_op.annotation().commonType->category())) if (smt::isNumber(_op.annotation().commonType->category()))
{ {
value = make_shared<smt::Expression>( value = make_shared<smt::Expression>(
op == Token::Equal ? (left == right) : op == Token::Equal ? (left == right) :
@ -1285,7 +1285,7 @@ void SMTChecker::compareOperation(BinaryOperation const& _op)
} }
else // Bool else // Bool
{ {
solUnimplementedAssert(isBool(_op.annotation().commonType->category()), "Operation not yet supported"); solUnimplementedAssert(smt::isBool(_op.annotation().commonType->category()), "Operation not yet supported");
value = make_shared<smt::Expression>( value = make_shared<smt::Expression>(
op == Token::Equal ? (left == right) : op == Token::Equal ? (left == right) :
/*op == Token::NotEqual*/ (left != right) /*op == Token::NotEqual*/ (left != right)
@ -1349,7 +1349,7 @@ void SMTChecker::assignment(
langutil::SourceLocation const& _location langutil::SourceLocation const& _location
) )
{ {
if (!isSupportedType(_type->category())) if (!smt::isSupportedType(_type->category()))
m_errorReporter.warning( m_errorReporter.warning(
_location, _location,
"Assertion checker does not yet implement type " + _type->toString() "Assertion checker does not yet implement type " + _type->toString()
@ -1469,7 +1469,7 @@ void SMTChecker::checkCondition(
auto const& type = var.second->type(); auto const& type = var.second->type();
if ( if (
type->isValueType() && type->isValueType() &&
smtKind(type->category()) != smt::Kind::Function smt::smtKind(type->category()) != smt::Kind::Function
) )
{ {
expressionsToEvaluate.emplace_back(var.second->currentValue()); expressionsToEvaluate.emplace_back(var.second->currentValue());
@ -1766,7 +1766,7 @@ bool SMTChecker::createVariable(VariableDeclaration const& _varDecl)
return true; return true;
auto const& type = _varDecl.type(); auto const& type = _varDecl.type();
solAssert(m_variables.count(&_varDecl) == 0, ""); solAssert(m_variables.count(&_varDecl) == 0, "");
auto result = newSymbolicVariable(*type, _varDecl.name() + "_" + to_string(_varDecl.id()), *m_interface); auto result = smt::newSymbolicVariable(*type, _varDecl.name() + "_" + to_string(_varDecl.id()), *m_interface);
m_variables.emplace(&_varDecl, result.second); m_variables.emplace(&_varDecl, result.second);
if (result.first) if (result.first)
{ {
@ -1808,7 +1808,7 @@ void SMTChecker::setZeroValue(VariableDeclaration const& _decl)
setZeroValue(*m_variables.at(&_decl)); setZeroValue(*m_variables.at(&_decl));
} }
void SMTChecker::setZeroValue(SymbolicVariable& _variable) void SMTChecker::setZeroValue(smt::SymbolicVariable& _variable)
{ {
smt::setSymbolicZeroValue(_variable, *m_interface); smt::setSymbolicZeroValue(_variable, *m_interface);
} }
@ -1819,7 +1819,7 @@ void SMTChecker::setUnknownValue(VariableDeclaration const& _decl)
setUnknownValue(*m_variables.at(&_decl)); setUnknownValue(*m_variables.at(&_decl));
} }
void SMTChecker::setUnknownValue(SymbolicVariable& _variable) void SMTChecker::setUnknownValue(smt::SymbolicVariable& _variable)
{ {
smt::setSymbolicUnknownValue(_variable, *m_interface); smt::setSymbolicUnknownValue(_variable, *m_interface);
} }
@ -1851,7 +1851,7 @@ void SMTChecker::createExpr(Expression const& _e)
m_expressions.at(&_e)->increaseIndex(); m_expressions.at(&_e)->increaseIndex();
else else
{ {
auto result = newSymbolicVariable(*_e.annotation().type, "expr_" + to_string(_e.id()), *m_interface); auto result = smt::newSymbolicVariable(*_e.annotation().type, "expr_" + to_string(_e.id()), *m_interface);
m_expressions.emplace(&_e, result.second); m_expressions.emplace(&_e, result.second);
if (result.first) if (result.first)
m_errorReporter.warning( m_errorReporter.warning(
@ -1864,7 +1864,7 @@ void SMTChecker::createExpr(Expression const& _e)
void SMTChecker::defineExpr(Expression const& _e, smt::Expression _value) void SMTChecker::defineExpr(Expression const& _e, smt::Expression _value)
{ {
createExpr(_e); createExpr(_e);
solAssert(smtKind(_e.annotation().type->category()) != smt::Kind::Function, "Equality operator applied to type that is not fully supported"); solAssert(smt::smtKind(_e.annotation().type->category()) != smt::Kind::Function, "Equality operator applied to type that is not fully supported");
m_interface->addAssertion(expr(_e) == _value); m_interface->addAssertion(expr(_e) == _value);
} }

12
libsolidity/formal/SMTChecker.h
View File

@ -247,10 +247,10 @@ private:
/// Sets the value of the declaration to zero. /// Sets the value of the declaration to zero.
void setZeroValue(VariableDeclaration const& _decl); void setZeroValue(VariableDeclaration const& _decl);
void setZeroValue(SymbolicVariable& _variable); void setZeroValue(smt::SymbolicVariable& _variable);
/// Resets the variable to an unknown value (in its range). /// Resets the variable to an unknown value (in its range).
void setUnknownValue(VariableDeclaration const& decl); void setUnknownValue(VariableDeclaration const& decl);
void setUnknownValue(SymbolicVariable& _variable); void setUnknownValue(smt::SymbolicVariable& _variable);
/// Returns the expression corresponding to the AST node. Throws if the expression does not exist. /// Returns the expression corresponding to the AST node. Throws if the expression does not exist.
smt::Expression expr(Expression const& _e); smt::Expression expr(Expression const& _e);
@ -296,7 +296,7 @@ private:
VariableDeclaration const* identifierToVariable(Expression const& _expr); VariableDeclaration const* identifierToVariable(Expression const& _expr);
std::unique_ptr<smt::SolverInterface> m_interface; std::unique_ptr<smt::SolverInterface> m_interface;
VariableUsage m_variableUsage; smt::VariableUsage m_variableUsage;
bool m_loopExecutionHappened = false; bool m_loopExecutionHappened = false;
bool m_arrayAssignmentHappened = false; bool m_arrayAssignmentHappened = false;
bool m_externalFunctionCallHappened = false; bool m_externalFunctionCallHappened = false;
@ -304,9 +304,9 @@ private:
bool m_noSolverWarning = false; bool m_noSolverWarning = false;
/// An Expression may have multiple smt::Expression due to /// An Expression may have multiple smt::Expression due to
/// repeated calls to the same function. /// repeated calls to the same function.
std::unordered_map<Expression const*, std::shared_ptr<SymbolicVariable>> m_expressions; std::unordered_map<Expression const*, std::shared_ptr<smt::SymbolicVariable>> m_expressions;
std::unordered_map<VariableDeclaration const*, std::shared_ptr<SymbolicVariable>> m_variables; std::unordered_map<VariableDeclaration const*, std::shared_ptr<smt::SymbolicVariable>> m_variables;
std::unordered_map<std::string, std::shared_ptr<SymbolicVariable>> m_globalContext; std::unordered_map<std::string, std::shared_ptr<smt::SymbolicVariable>> m_globalContext;
/// Stores the instances of an Uninterpreted Function applied to arguments. /// Stores the instances of an Uninterpreted Function applied to arguments.
/// These may be direct application of UFs or Array index access. /// These may be direct application of UFs or Array index access.

2
libsolidity/formal/SSAVariable.cpp
View File

@ -18,7 +18,7 @@
#include <libsolidity/formal/SSAVariable.h> #include <libsolidity/formal/SSAVariable.h>
using namespace std; using namespace std;
using namespace dev::solidity; using namespace dev::solidity::smt;
SSAVariable::SSAVariable() SSAVariable::SSAVariable()
{ {

3
libsolidity/formal/SSAVariable.h
View File

@ -23,6 +23,8 @@ namespace dev
{ {
namespace solidity namespace solidity
{ {
namespace smt
{
/** /**
* This class represents the SSA representation of a program variable. * This class represents the SSA representation of a program variable.
@ -49,3 +51,4 @@ private:
} }
} }
}

156
libsolidity/formal/SymbolicTypes.cpp
View File

@ -22,79 +22,85 @@
#include <memory> #include <memory>
using namespace std; using namespace std;
using namespace dev::solidity;
smt::SortPointer dev::solidity::smtSort(Type const& _type) namespace dev
{
namespace solidity
{
namespace smt
{
SortPointer smtSort(solidity::Type const& _type)
{ {
switch (smtKind(_type.category())) switch (smtKind(_type.category()))
{ {
case smt::Kind::Int: case Kind::Int:
return make_shared<smt::Sort>(smt::Kind::Int); return make_shared<Sort>(Kind::Int);
case smt::Kind::Bool: case Kind::Bool:
return make_shared<smt::Sort>(smt::Kind::Bool); return make_shared<Sort>(Kind::Bool);
case smt::Kind::Function: case Kind::Function:
{ {
auto fType = dynamic_cast<FunctionType const*>(&_type); auto fType = dynamic_cast<solidity::FunctionType const*>(&_type);
solAssert(fType, ""); solAssert(fType, "");
vector<smt::SortPointer> parameterSorts = smtSort(fType->parameterTypes()); vector<SortPointer> parameterSorts = smtSort(fType->parameterTypes());
auto returnTypes = fType->returnParameterTypes(); auto returnTypes = fType->returnParameterTypes();
smt::SortPointer returnSort; SortPointer returnSort;
// TODO change this when we support tuples. // TODO change this when we support tuples.
if (returnTypes.size() == 0) if (returnTypes.size() == 0)
// We cannot declare functions without a return sort, so we use the smallest. // We cannot declare functions without a return sort, so we use the smallest.
returnSort = make_shared<smt::Sort>(smt::Kind::Bool); returnSort = make_shared<Sort>(Kind::Bool);
else if (returnTypes.size() > 1) else if (returnTypes.size() > 1)
// Abstract sort. // Abstract sort.
returnSort = make_shared<smt::Sort>(smt::Kind::Int); returnSort = make_shared<Sort>(Kind::Int);
else else
returnSort = smtSort(*returnTypes.front()); returnSort = smtSort(*returnTypes.front());
return make_shared<smt::FunctionSort>(parameterSorts, returnSort); return make_shared<FunctionSort>(parameterSorts, returnSort);
} }
case smt::Kind::Array: case Kind::Array:
{ {
if (isMapping(_type.category())) if (isMapping(_type.category()))
{ {
auto mapType = dynamic_cast<MappingType const*>(&_type); auto mapType = dynamic_cast<solidity::MappingType const*>(&_type);
solAssert(mapType, ""); solAssert(mapType, "");
return make_shared<smt::ArraySort>(smtSort(*mapType->keyType()), smtSort(*mapType->valueType())); return make_shared<ArraySort>(smtSort(*mapType->keyType()), smtSort(*mapType->valueType()));
} }
else else
{ {
solAssert(isArray(_type.category()), ""); solAssert(isArray(_type.category()), "");
auto arrayType = dynamic_cast<ArrayType const*>(&_type); auto arrayType = dynamic_cast<solidity::ArrayType const*>(&_type);
solAssert(arrayType, ""); solAssert(arrayType, "");
return make_shared<smt::ArraySort>(make_shared<smt::Sort>(smt::Kind::Int), smtSort(*arrayType->baseType())); return make_shared<ArraySort>(make_shared<Sort>(Kind::Int), smtSort(*arrayType->baseType()));
} }
} }
default: default:
// Abstract case. // Abstract case.
return make_shared<smt::Sort>(smt::Kind::Int); return make_shared<Sort>(Kind::Int);
} }
} }
vector<smt::SortPointer> dev::solidity::smtSort(vector<TypePointer> const& _types) vector<SortPointer> smtSort(vector<solidity::TypePointer> const& _types)
{ {
vector<smt::SortPointer> sorts; vector<SortPointer> sorts;
for (auto const& type: _types) for (auto const& type: _types)
sorts.push_back(smtSort(*type)); sorts.push_back(smtSort(*type));
return sorts; return sorts;
} }
smt::Kind dev::solidity::smtKind(Type::Category _category) Kind smtKind(solidity::Type::Category _category)
{ {
if (isNumber(_category)) if (isNumber(_category))
return smt::Kind::Int; return Kind::Int;
else if (isBool(_category)) else if (isBool(_category))
return smt::Kind::Bool; return Kind::Bool;
else if (isFunction(_category)) else if (isFunction(_category))
return smt::Kind::Function; return Kind::Function;
else if (isMapping(_category) || isArray(_category)) else if (isMapping(_category) || isArray(_category))
return smt::Kind::Array; return Kind::Array;
// Abstract case. // Abstract case.
return smt::Kind::Int; return Kind::Int;
} }
bool dev::solidity::isSupportedType(Type::Category _category) bool isSupportedType(solidity::Type::Category _category)
{ {
return isNumber(_category) || return isNumber(_category) ||
isBool(_category) || isBool(_category) ||
@ -103,25 +109,25 @@ bool dev::solidity::isSupportedType(Type::Category _category)
isTuple(_category); isTuple(_category);
} }
bool dev::solidity::isSupportedTypeDeclaration(Type::Category _category) bool isSupportedTypeDeclaration(solidity::Type::Category _category)
{ {
return isSupportedType(_category) || return isSupportedType(_category) ||
isFunction(_category); isFunction(_category);
} }
pair<bool, shared_ptr<SymbolicVariable>> dev::solidity::newSymbolicVariable( pair<bool, shared_ptr<SymbolicVariable>> newSymbolicVariable(
Type const& _type, solidity::Type const& _type,
std::string const& _uniqueName, std::string const& _uniqueName,
smt::SolverInterface& _solver SolverInterface& _solver
) )
{ {
bool abstract = false; bool abstract = false;
shared_ptr<SymbolicVariable> var; shared_ptr<SymbolicVariable> var;
TypePointer type = &_type; solidity::TypePointer type = &_type;
if (!isSupportedTypeDeclaration(_type)) if (!isSupportedTypeDeclaration(_type))
{ {
abstract = true; abstract = true;
var = make_shared<SymbolicIntVariable>(TypeProvider::uint256(), _uniqueName, _solver); var = make_shared<SymbolicIntVariable>(solidity::TypeProvider::uint256(), _uniqueName, _solver);
} }
else if (isBool(_type.category())) else if (isBool(_type.category()))
var = make_shared<SymbolicBoolVariable>(type, _uniqueName, _solver); var = make_shared<SymbolicBoolVariable>(type, _uniqueName, _solver);
@ -131,7 +137,7 @@ pair<bool, shared_ptr<SymbolicVariable>> dev::solidity::newSymbolicVariable(
var = make_shared<SymbolicIntVariable>(type, _uniqueName, _solver); var = make_shared<SymbolicIntVariable>(type, _uniqueName, _solver);
else if (isFixedBytes(_type.category())) else if (isFixedBytes(_type.category()))
{ {
auto fixedBytesType = dynamic_cast<FixedBytesType const*>(type); auto fixedBytesType = dynamic_cast<solidity::FixedBytesType const*>(type);
solAssert(fixedBytesType, ""); solAssert(fixedBytesType, "");
var = make_shared<SymbolicFixedBytesVariable>(fixedBytesType->numBytes(), _uniqueName, _solver); var = make_shared<SymbolicFixedBytesVariable>(fixedBytesType->numBytes(), _uniqueName, _solver);
} }
@ -141,10 +147,10 @@ pair<bool, shared_ptr<SymbolicVariable>> dev::solidity::newSymbolicVariable(
var = make_shared<SymbolicEnumVariable>(type, _uniqueName, _solver); var = make_shared<SymbolicEnumVariable>(type, _uniqueName, _solver);
else if (isRational(_type.category())) else if (isRational(_type.category()))
{ {
auto rational = dynamic_cast<RationalNumberType const*>(&_type); auto rational = dynamic_cast<solidity::RationalNumberType const*>(&_type);
solAssert(rational, ""); solAssert(rational, "");
if (rational->isFractional()) if (rational->isFractional())
var = make_shared<SymbolicIntVariable>(TypeProvider::uint256(), _uniqueName, _solver); var = make_shared<SymbolicIntVariable>(solidity::TypeProvider::uint256(), _uniqueName, _solver);
else else
var = make_shared<SymbolicIntVariable>(type, _uniqueName, _solver); var = make_shared<SymbolicIntVariable>(type, _uniqueName, _solver);
} }
@ -159,47 +165,47 @@ pair<bool, shared_ptr<SymbolicVariable>> dev::solidity::newSymbolicVariable(
return make_pair(abstract, var); return make_pair(abstract, var);
} }
bool dev::solidity::isSupportedType(Type const& _type) bool isSupportedType(solidity::Type const& _type)
{ {
return isSupportedType(_type.category()); return isSupportedType(_type.category());
} }
bool dev::solidity::isSupportedTypeDeclaration(Type const& _type) bool isSupportedTypeDeclaration(solidity::Type const& _type)
{ {
return isSupportedTypeDeclaration(_type.category()); return isSupportedTypeDeclaration(_type.category());
} }
bool dev::solidity::isInteger(Type::Category _category) bool isInteger(solidity::Type::Category _category)
{ {
return _category == Type::Category::Integer; return _category == solidity::Type::Category::Integer;
} }
bool dev::solidity::isRational(Type::Category _category) bool isRational(solidity::Type::Category _category)
{ {
return _category == Type::Category::RationalNumber; return _category == solidity::Type::Category::RationalNumber;
} }
bool dev::solidity::isFixedBytes(Type::Category _category) bool isFixedBytes(solidity::Type::Category _category)
{ {
return _category == Type::Category::FixedBytes; return _category == solidity::Type::Category::FixedBytes;
} }
bool dev::solidity::isAddress(Type::Category _category) bool isAddress(solidity::Type::Category _category)
{ {
return _category == Type::Category::Address; return _category == solidity::Type::Category::Address;
} }
bool dev::solidity::isContract(Type::Category _category) bool isContract(solidity::Type::Category _category)
{ {
return _category == Type::Category::Contract; return _category == solidity::Type::Category::Contract;
} }
bool dev::solidity::isEnum(Type::Category _category) bool isEnum(solidity::Type::Category _category)
{ {
return _category == Type::Category::Enum; return _category == solidity::Type::Category::Enum;
} }
bool dev::solidity::isNumber(Type::Category _category) bool isNumber(solidity::Type::Category _category)
{ {
return isInteger(_category) || return isInteger(_category) ||
isRational(_category) || isRational(_category) ||
@ -209,75 +215,79 @@ bool dev::solidity::isNumber(Type::Category _category)
isEnum(_category); isEnum(_category);
} }
bool dev::solidity::isBool(Type::Category _category) bool isBool(solidity::Type::Category _category)
{ {
return _category == Type::Category::Bool; return _category == solidity::Type::Category::Bool;
} }
bool dev::solidity::isFunction(Type::Category _category) bool isFunction(solidity::Type::Category _category)
{ {
return _category == Type::Category::Function; return _category == solidity::Type::Category::Function;
} }
bool dev::solidity::isMapping(Type::Category _category) bool isMapping(solidity::Type::Category _category)
{ {
return _category == Type::Category::Mapping; return _category == solidity::Type::Category::Mapping;
} }
bool dev::solidity::isArray(Type::Category _category) bool isArray(solidity::Type::Category _category)
{ {
return _category == Type::Category::Array; return _category == solidity::Type::Category::Array;
} }
bool dev::solidity::isTuple(Type::Category _category) bool isTuple(solidity::Type::Category _category)
{ {
return _category == Type::Category::Tuple; return _category == solidity::Type::Category::Tuple;
} }
smt::Expression dev::solidity::minValue(IntegerType const& _type) Expression minValue(solidity::IntegerType const& _type)
{ {
return smt::Expression(_type.minValue()); return Expression(_type.minValue());
} }
smt::Expression dev::solidity::maxValue(IntegerType const& _type) Expression maxValue(solidity::IntegerType const& _type)
{ {
return smt::Expression(_type.maxValue()); return Expression(_type.maxValue());
} }
void dev::solidity::smt::setSymbolicZeroValue(SymbolicVariable const& _variable, smt::SolverInterface& _interface) void setSymbolicZeroValue(SymbolicVariable const& _variable, SolverInterface& _interface)
{ {
setSymbolicZeroValue(_variable.currentValue(), _variable.type(), _interface); setSymbolicZeroValue(_variable.currentValue(), _variable.type(), _interface);
} }
void dev::solidity::smt::setSymbolicZeroValue(smt::Expression _expr, TypePointer const& _type, smt::SolverInterface& _interface) void setSymbolicZeroValue(Expression _expr, solidity::TypePointer const& _type, SolverInterface& _interface)
{ {
solAssert(_type, ""); solAssert(_type, "");
if (isInteger(_type->category())) if (isInteger(_type->category()))
_interface.addAssertion(_expr == 0); _interface.addAssertion(_expr == 0);
else if (isBool(_type->category())) else if (isBool(_type->category()))
_interface.addAssertion(_expr == smt::Expression(false)); _interface.addAssertion(_expr == Expression(false));
} }
void dev::solidity::smt::setSymbolicUnknownValue(SymbolicVariable const& _variable, smt::SolverInterface& _interface) void setSymbolicUnknownValue(SymbolicVariable const& _variable, SolverInterface& _interface)
{ {
setSymbolicUnknownValue(_variable.currentValue(), _variable.type(), _interface); setSymbolicUnknownValue(_variable.currentValue(), _variable.type(), _interface);
} }
void dev::solidity::smt::setSymbolicUnknownValue(smt::Expression _expr, TypePointer const& _type, smt::SolverInterface& _interface) void setSymbolicUnknownValue(Expression _expr, solidity::TypePointer const& _type, SolverInterface& _interface)
{ {
solAssert(_type, ""); solAssert(_type, "");
if (isEnum(_type->category())) if (isEnum(_type->category()))
{ {
auto enumType = dynamic_cast<EnumType const*>(_type); auto enumType = dynamic_cast<solidity::EnumType const*>(_type);
solAssert(enumType, ""); solAssert(enumType, "");
_interface.addAssertion(_expr >= 0); _interface.addAssertion(_expr >= 0);
_interface.addAssertion(_expr < enumType->numberOfMembers()); _interface.addAssertion(_expr < enumType->numberOfMembers());
} }
else if (isInteger(_type->category())) else if (isInteger(_type->category()))
{ {
auto intType = dynamic_cast<IntegerType const*>(_type); auto intType = dynamic_cast<solidity::IntegerType const*>(_type);
solAssert(intType, ""); solAssert(intType, "");
_interface.addAssertion(_expr >= minValue(*intType)); _interface.addAssertion(_expr >= minValue(*intType));
_interface.addAssertion(_expr <= maxValue(*intType)); _interface.addAssertion(_expr <= maxValue(*intType));
} }
} }
}
}
}

60
libsolidity/formal/SymbolicTypes.h
View File

@ -26,50 +26,48 @@ namespace dev
{ {
namespace solidity namespace solidity
{ {
namespace smt
{
/// Returns the SMT sort that models the Solidity type _type. /// Returns the SMT sort that models the Solidity type _type.
smt::SortPointer smtSort(Type const& _type); SortPointer smtSort(solidity::Type const& _type);
std::vector<smt::SortPointer> smtSort(std::vector<TypePointer> const& _types); std::vector<SortPointer> smtSort(std::vector<solidity::TypePointer> const& _types);
/// Returns the SMT kind that models the Solidity type type category _category. /// Returns the SMT kind that models the Solidity type type category _category.
smt::Kind smtKind(Type::Category _category); Kind smtKind(solidity::Type::Category _category);
/// Returns true if type is fully supported (declaration and operations). /// Returns true if type is fully supported (declaration and operations).
bool isSupportedType(Type::Category _category); bool isSupportedType(solidity::Type::Category _category);
bool isSupportedType(Type const& _type); bool isSupportedType(solidity::Type const& _type);
/// Returns true if type is partially supported (declaration). /// Returns true if type is partially supported (declaration).
bool isSupportedTypeDeclaration(Type::Category _category); bool isSupportedTypeDeclaration(solidity::Type::Category _category);
bool isSupportedTypeDeclaration(Type const& _type); bool isSupportedTypeDeclaration(solidity::Type const& _type);
bool isInteger(Type::Category _category); bool isInteger(solidity::Type::Category _category);
bool isRational(Type::Category _category); bool isRational(solidity::Type::Category _category);
bool isFixedBytes(Type::Category _category); bool isFixedBytes(solidity::Type::Category _category);
bool isAddress(Type::Category _category); bool isAddress(solidity::Type::Category _category);
bool isContract(Type::Category _category); bool isContract(solidity::Type::Category _category);
bool isEnum(Type::Category _category); bool isEnum(solidity::Type::Category _category);
bool isNumber(Type::Category _category); bool isNumber(solidity::Type::Category _category);
bool isBool(Type::Category _category); bool isBool(solidity::Type::Category _category);
bool isFunction(Type::Category _category); bool isFunction(solidity::Type::Category _category);
bool isMapping(Type::Category _category); bool isMapping(solidity::Type::Category _category);
bool isArray(Type::Category _category); bool isArray(solidity::Type::Category _category);
bool isTuple(Type::Category _category); bool isTuple(solidity::Type::Category _category);
/// Returns a new symbolic variable, according to _type. /// Returns a new symbolic variable, according to _type.
/// Also returns whether the type is abstract or not, /// Also returns whether the type is abstract or not,
/// which is true for unsupported types. /// which is true for unsupported types.
std::pair<bool, std::shared_ptr<SymbolicVariable>> newSymbolicVariable(Type const& _type, std::string const& _uniqueName, smt::SolverInterface& _solver); std::pair<bool, std::shared_ptr<SymbolicVariable>> newSymbolicVariable(solidity::Type const& _type, std::string const& _uniqueName, SolverInterface& _solver);
smt::Expression minValue(IntegerType const& _type); Expression minValue(solidity::IntegerType const& _type);
smt::Expression maxValue(IntegerType const& _type); Expression maxValue(solidity::IntegerType const& _type);
namespace smt void setSymbolicZeroValue(SymbolicVariable const& _variable, SolverInterface& _interface);
{ void setSymbolicZeroValue(Expression _expr, solidity::TypePointer const& _type, SolverInterface& _interface);
void setSymbolicUnknownValue(SymbolicVariable const& _variable, SolverInterface& _interface);
void setSymbolicZeroValue(SymbolicVariable const& _variable, smt::SolverInterface& _interface); void setSymbolicUnknownValue(Expression _expr, solidity::TypePointer const& _type, SolverInterface& _interface);
void setSymbolicZeroValue(smt::Expression _expr, TypePointer const& _type, smt::SolverInterface& _interface);
void setSymbolicUnknownValue(SymbolicVariable const& _variable, smt::SolverInterface& _interface);
void setSymbolicUnknownValue(smt::Expression _expr, TypePointer const& _type, smt::SolverInterface& _interface);
}
} }
} }
}

58
libsolidity/formal/SymbolicVariables.cpp
View File

@ -23,12 +23,12 @@
using namespace std; using namespace std;
using namespace dev; using namespace dev;
using namespace dev::solidity; using namespace dev::solidity::smt;
SymbolicVariable::SymbolicVariable( SymbolicVariable::SymbolicVariable(
TypePointer _type, solidity::TypePointer _type,
string _uniqueName, string _uniqueName,
smt::SolverInterface& _interface SolverInterface& _interface
): ):
m_type(move(_type)), m_type(move(_type)),
m_uniqueName(move(_uniqueName)), m_uniqueName(move(_uniqueName)),
@ -41,9 +41,9 @@ SymbolicVariable::SymbolicVariable(
} }
SymbolicVariable::SymbolicVariable( SymbolicVariable::SymbolicVariable(
smt::SortPointer _sort, SortPointer _sort,
string _uniqueName, string _uniqueName,
smt::SolverInterface& _interface SolverInterface& _interface
): ):
m_sort(move(_sort)), m_sort(move(_sort)),
m_uniqueName(move(_uniqueName)), m_uniqueName(move(_uniqueName)),
@ -53,7 +53,7 @@ SymbolicVariable::SymbolicVariable(
solAssert(m_sort, ""); solAssert(m_sort, "");
} }
smt::Expression SymbolicVariable::currentValue() const Expression SymbolicVariable::currentValue() const
{ {
return valueAtIndex(m_ssa->index()); return valueAtIndex(m_ssa->index());
} }
@ -63,7 +63,7 @@ string SymbolicVariable::currentName() const
return uniqueSymbol(m_ssa->index()); return uniqueSymbol(m_ssa->index());
} }
smt::Expression SymbolicVariable::valueAtIndex(int _index) const Expression SymbolicVariable::valueAtIndex(int _index) const
{ {
return m_interface.newVariable(uniqueSymbol(_index), m_sort); return m_interface.newVariable(uniqueSymbol(_index), m_sort);
} }
@ -73,26 +73,26 @@ string SymbolicVariable::uniqueSymbol(unsigned _index) const
return m_uniqueName + "_" + to_string(_index); return m_uniqueName + "_" + to_string(_index);
} }
smt::Expression SymbolicVariable::increaseIndex() Expression SymbolicVariable::increaseIndex()
{ {
++(*m_ssa); ++(*m_ssa);
return currentValue(); return currentValue();
} }
SymbolicBoolVariable::SymbolicBoolVariable( SymbolicBoolVariable::SymbolicBoolVariable(
TypePointer _type, solidity::TypePointer _type,
string _uniqueName, string _uniqueName,
smt::SolverInterface& _interface SolverInterface& _interface
): ):
SymbolicVariable(move(_type), move(_uniqueName), _interface) SymbolicVariable(move(_type), move(_uniqueName), _interface)
{ {
solAssert(m_type->category() == Type::Category::Bool, ""); solAssert(m_type->category() == solidity::Type::Category::Bool, "");
} }
SymbolicIntVariable::SymbolicIntVariable( SymbolicIntVariable::SymbolicIntVariable(
TypePointer _type, solidity::TypePointer _type,
string _uniqueName, string _uniqueName,
smt::SolverInterface& _interface SolverInterface& _interface
): ):
SymbolicVariable(move(_type), move(_uniqueName), _interface) SymbolicVariable(move(_type), move(_uniqueName), _interface)
{ {
@ -101,7 +101,7 @@ SymbolicIntVariable::SymbolicIntVariable(
SymbolicAddressVariable::SymbolicAddressVariable( SymbolicAddressVariable::SymbolicAddressVariable(
string _uniqueName, string _uniqueName,
smt::SolverInterface& _interface SolverInterface& _interface
): ):
SymbolicIntVariable(TypeProvider::uint(160), move(_uniqueName), _interface) SymbolicIntVariable(TypeProvider::uint(160), move(_uniqueName), _interface)
{ {
@ -110,21 +110,21 @@ SymbolicAddressVariable::SymbolicAddressVariable(
SymbolicFixedBytesVariable::SymbolicFixedBytesVariable( SymbolicFixedBytesVariable::SymbolicFixedBytesVariable(
unsigned _numBytes, unsigned _numBytes,
string _uniqueName, string _uniqueName,
smt::SolverInterface& _interface SolverInterface& _interface
): ):
SymbolicIntVariable(TypeProvider::uint(_numBytes * 8), move(_uniqueName), _interface) SymbolicIntVariable(TypeProvider::uint(_numBytes * 8), move(_uniqueName), _interface)
{ {
} }
SymbolicFunctionVariable::SymbolicFunctionVariable( SymbolicFunctionVariable::SymbolicFunctionVariable(
TypePointer _type, solidity::TypePointer _type,
string _uniqueName, string _uniqueName,
smt::SolverInterface& _interface SolverInterface& _interface
): ):
SymbolicVariable(move(_type), move(_uniqueName), _interface), SymbolicVariable(move(_type), move(_uniqueName), _interface),
m_declaration(m_interface.newVariable(currentName(), m_sort)) m_declaration(m_interface.newVariable(currentName(), m_sort))
{ {
solAssert(m_type->category() == Type::Category::Function, ""); solAssert(m_type->category() == solidity::Type::Category::Function, "");
} }
void SymbolicFunctionVariable::resetDeclaration() void SymbolicFunctionVariable::resetDeclaration()
@ -132,22 +132,22 @@ void SymbolicFunctionVariable::resetDeclaration()
m_declaration = m_interface.newVariable(currentName(), m_sort); m_declaration = m_interface.newVariable(currentName(), m_sort);
} }
smt::Expression SymbolicFunctionVariable::increaseIndex() Expression SymbolicFunctionVariable::increaseIndex()
{ {
++(*m_ssa); ++(*m_ssa);
resetDeclaration(); resetDeclaration();
return currentValue(); return currentValue();
} }
smt::Expression SymbolicFunctionVariable::operator()(vector<smt::Expression> _arguments) const Expression SymbolicFunctionVariable::operator()(vector<Expression> _arguments) const
{ {
return m_declaration(_arguments); return m_declaration(_arguments);
} }
SymbolicMappingVariable::SymbolicMappingVariable( SymbolicMappingVariable::SymbolicMappingVariable(
TypePointer _type, solidity::TypePointer _type,
string _uniqueName, string _uniqueName,
smt::SolverInterface& _interface SolverInterface& _interface
): ):
SymbolicVariable(move(_type), move(_uniqueName), _interface) SymbolicVariable(move(_type), move(_uniqueName), _interface)
{ {
@ -155,9 +155,9 @@ SymbolicMappingVariable::SymbolicMappingVariable(
} }
SymbolicArrayVariable::SymbolicArrayVariable( SymbolicArrayVariable::SymbolicArrayVariable(
TypePointer _type, solidity::TypePointer _type,
string _uniqueName, string _uniqueName,
smt::SolverInterface& _interface SolverInterface& _interface
): ):
SymbolicVariable(move(_type), move(_uniqueName), _interface) SymbolicVariable(move(_type), move(_uniqueName), _interface)
{ {
@ -165,9 +165,9 @@ SymbolicArrayVariable::SymbolicArrayVariable(
} }
SymbolicEnumVariable::SymbolicEnumVariable( SymbolicEnumVariable::SymbolicEnumVariable(
TypePointer _type, solidity::TypePointer _type,
string _uniqueName, string _uniqueName,
smt::SolverInterface& _interface SolverInterface& _interface
): ):
SymbolicVariable(move(_type), move(_uniqueName), _interface) SymbolicVariable(move(_type), move(_uniqueName), _interface)
{ {
@ -175,9 +175,9 @@ SymbolicEnumVariable::SymbolicEnumVariable(
} }
SymbolicTupleVariable::SymbolicTupleVariable( SymbolicTupleVariable::SymbolicTupleVariable(
TypePointer _type, solidity::TypePointer _type,
string _uniqueName, string _uniqueName,
smt::SolverInterface& _interface SolverInterface& _interface
): ):
SymbolicVariable(move(_type), move(_uniqueName), _interface) SymbolicVariable(move(_type), move(_uniqueName), _interface)
{ {
@ -187,7 +187,7 @@ SymbolicTupleVariable::SymbolicTupleVariable(
void SymbolicTupleVariable::setComponents(vector<shared_ptr<SymbolicVariable>> _components) void SymbolicTupleVariable::setComponents(vector<shared_ptr<SymbolicVariable>> _components)
{ {
solAssert(m_components.empty(), ""); solAssert(m_components.empty(), "");
auto const& tupleType = dynamic_cast<TupleType const*>(m_type); auto const& tupleType = dynamic_cast<solidity::TupleType const*>(m_type);
solAssert(_components.size() == tupleType->components().size(), ""); solAssert(_components.size() == tupleType->components().size(), "");
m_components = move(_components); m_components = move(_components);
} }

65
libsolidity/formal/SymbolicVariables.h
View File

@ -26,6 +26,8 @@ namespace dev
{ {
namespace solidity namespace solidity
{ {
namespace smt
{
class Type; class Type;
@ -36,23 +38,23 @@ class SymbolicVariable
{ {
public: public:
SymbolicVariable( SymbolicVariable(
TypePointer _type, solidity::TypePointer _type,
std::string _uniqueName, std::string _uniqueName,
smt::SolverInterface& _interface SolverInterface& _interface
); );
SymbolicVariable( SymbolicVariable(
smt::SortPointer _sort, SortPointer _sort,
std::string _uniqueName, std::string _uniqueName,
smt::SolverInterface& _interface SolverInterface& _interface
); );
virtual ~SymbolicVariable() = default; virtual ~SymbolicVariable() = default;
smt::Expression currentValue() const; Expression currentValue() const;
std::string currentName() const; std::string currentName() const;
virtual smt::Expression valueAtIndex(int _index) const; virtual Expression valueAtIndex(int _index) const;
virtual smt::Expression increaseIndex(); virtual Expression increaseIndex();
virtual smt::Expression operator()(std::vector<smt::Expression> /*_arguments*/) const virtual Expression operator()(std::vector<Expression> /*_arguments*/) const
{ {
solAssert(false, "Function application to non-function."); solAssert(false, "Function application to non-function.");
} }
@ -60,17 +62,17 @@ public:
unsigned index() const { return m_ssa->index(); } unsigned index() const { return m_ssa->index(); }
unsigned& index() { return m_ssa->index(); } unsigned& index() { return m_ssa->index(); }
TypePointer const& type() const { return m_type; } solidity::TypePointer const& type() const { return m_type; }
protected: protected:
std::string uniqueSymbol(unsigned _index) const; std::string uniqueSymbol(unsigned _index) const;
/// SMT sort. /// SMT sort.
smt::SortPointer m_sort; SortPointer m_sort;
/// Solidity type, used for size and range in number types. /// Solidity type, used for size and range in number types.
TypePointer m_type; solidity::TypePointer m_type;
std::string m_uniqueName; std::string m_uniqueName;
smt::SolverInterface& m_interface; SolverInterface& m_interface;
std::unique_ptr<SSAVariable> m_ssa; std::unique_ptr<SSAVariable> m_ssa;
}; };
@ -81,9 +83,9 @@ class SymbolicBoolVariable: public SymbolicVariable
{ {
public: public:
SymbolicBoolVariable( SymbolicBoolVariable(
TypePointer _type, solidity::TypePointer _type,
std::string _uniqueName, std::string _uniqueName,
smt::SolverInterface& _interface SolverInterface& _interface
); );
}; };
@ -94,9 +96,9 @@ class SymbolicIntVariable: public SymbolicVariable
{ {
public: public:
SymbolicIntVariable( SymbolicIntVariable(
TypePointer _type, solidity::TypePointer _type,
std::string _uniqueName, std::string _uniqueName,
smt::SolverInterface& _interface SolverInterface& _interface
); );
}; };
@ -108,7 +110,7 @@ class SymbolicAddressVariable: public SymbolicIntVariable
public: public:
SymbolicAddressVariable( SymbolicAddressVariable(
std::string _uniqueName, std::string _uniqueName,
smt::SolverInterface& _interface SolverInterface& _interface
); );
}; };
@ -121,7 +123,7 @@ public:
SymbolicFixedBytesVariable( SymbolicFixedBytesVariable(
unsigned _numBytes, unsigned _numBytes,
std::string _uniqueName, std::string _uniqueName,
smt::SolverInterface& _interface SolverInterface& _interface
); );
}; };
@ -132,20 +134,20 @@ class SymbolicFunctionVariable: public SymbolicVariable
{ {
public: public:
SymbolicFunctionVariable( SymbolicFunctionVariable(
TypePointer _type, solidity::TypePointer _type,
std::string _uniqueName, std::string _uniqueName,
smt::SolverInterface& _interface SolverInterface& _interface
); );
smt::Expression increaseIndex(); Expression increaseIndex();
smt::Expression operator()(std::vector<smt::Expression> _arguments) const; Expression operator()(std::vector<Expression> _arguments) const;
private: private:
/// Creates a new function declaration. /// Creates a new function declaration.
void resetDeclaration(); void resetDeclaration();
/// Stores the current function declaration. /// Stores the current function declaration.
smt::Expression m_declaration; Expression m_declaration;
}; };
/** /**
@ -155,9 +157,9 @@ class SymbolicMappingVariable: public SymbolicVariable
{ {
public: public:
SymbolicMappingVariable( SymbolicMappingVariable(
TypePointer _type, solidity::TypePointer _type,
std::string _uniqueName, std::string _uniqueName,
smt::SolverInterface& _interface SolverInterface& _interface
); );
}; };
@ -168,9 +170,9 @@ class SymbolicArrayVariable: public SymbolicVariable
{ {
public: public:
SymbolicArrayVariable( SymbolicArrayVariable(
TypePointer _type, solidity::TypePointer _type,
std::string _uniqueName, std::string _uniqueName,
smt::SolverInterface& _interface SolverInterface& _interface
); );
}; };
@ -181,9 +183,9 @@ class SymbolicEnumVariable: public SymbolicVariable
{ {
public: public:
SymbolicEnumVariable( SymbolicEnumVariable(
TypePointer _type, solidity::TypePointer _type,
std::string _uniqueName, std::string _uniqueName,
smt::SolverInterface& _interface SolverInterface& _interface
); );
}; };
@ -194,9 +196,9 @@ class SymbolicTupleVariable: public SymbolicVariable
{ {
public: public:
SymbolicTupleVariable( SymbolicTupleVariable(
TypePointer _type, solidity::TypePointer _type,
std::string _uniqueName, std::string _uniqueName,
smt::SolverInterface& _interface SolverInterface& _interface
); );
std::vector<std::shared_ptr<SymbolicVariable>> const& components() std::vector<std::shared_ptr<SymbolicVariable>> const& components()
@ -212,3 +214,4 @@ private:
} }
} }
}

1
libsolidity/formal/VariableUsage.cpp
View File

@ -24,6 +24,7 @@
using namespace std; using namespace std;
using namespace dev; using namespace dev;
using namespace dev::solidity; using namespace dev::solidity;
using namespace dev::solidity::smt;
set<VariableDeclaration const*> VariableUsage::touchedVariables(ASTNode const& _node, vector<CallableDeclaration const*> const& _outerCallstack) set<VariableDeclaration const*> VariableUsage::touchedVariables(ASTNode const& _node, vector<CallableDeclaration const*> const& _outerCallstack)
{ {

3
libsolidity/formal/VariableUsage.h
View File

@ -26,6 +26,8 @@ namespace dev
{ {
namespace solidity namespace solidity
{ {
namespace smt
{
/** /**
* This class computes information about which variables are modified in a certain subtree. * This class computes information about which variables are modified in a certain subtree.
@ -55,3 +57,4 @@ private:
} }
} }
}