aboutsummaryrefslogtreecommitdiffstats
path: root/libsolidity
diff options
context:
space:
mode:
authorchriseth <chris@ethereum.org>2017-10-05 21:23:25 +0800
committerchriseth <chris@ethereum.org>2017-11-30 08:20:21 +0800
commit19e067465a058ca9f40238cb3a928a1113531c9d (patch)
tree6b4f83892d5fd76194bd3794669cc59f02e86d37 /libsolidity
parentffb3a3c06c4d436aaf03efccf31301b472cd8137 (diff)
downloaddexon-solidity-19e067465a058ca9f40238cb3a928a1113531c9d.tar.gz
dexon-solidity-19e067465a058ca9f40238cb3a928a1113531c9d.tar.zst
dexon-solidity-19e067465a058ca9f40238cb3a928a1113531c9d.zip
Unary operators and division.
Diffstat (limited to 'libsolidity')
-rw-r--r--libsolidity/analysis/TypeChecker.cpp2
-rw-r--r--libsolidity/formal/SMTChecker.cpp191
-rw-r--r--libsolidity/formal/SMTChecker.h14
-rw-r--r--libsolidity/formal/SolverInterface.h4
-rw-r--r--libsolidity/formal/Z3Interface.cpp5
5 files changed, 155 insertions, 61 deletions
diff --git a/libsolidity/analysis/TypeChecker.cpp b/libsolidity/analysis/TypeChecker.cpp
index 73047e76..96160a75 100644
--- a/libsolidity/analysis/TypeChecker.cpp
+++ b/libsolidity/analysis/TypeChecker.cpp
@@ -1060,7 +1060,7 @@ bool TypeChecker::visit(VariableDeclarationStatement const& _statement)
_statement.initialValue()->location(),
"Invalid rational " +
valueComponentType->toString() +
- " (absolute value too large or divison by zero)."
+ " (absolute value too large or division by zero)."
);
else
solAssert(false, "");
diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp
index 1050621e..9e2cf908 100644
--- a/libsolidity/formal/SMTChecker.cpp
+++ b/libsolidity/formal/SMTChecker.cpp
@@ -55,7 +55,7 @@ void SMTChecker::analyze(SourceUnit const& _source)
void SMTChecker::endVisit(VariableDeclaration const& _varDecl)
{
if (_varDecl.isLocalVariable() && _varDecl.type()->isValueType() &&_varDecl.value())
- assignment(_varDecl, *_varDecl.value());
+ assignment(_varDecl, *_varDecl.value(), _varDecl.location());
}
bool SMTChecker::visit(FunctionDefinition const& _function)
@@ -178,8 +178,7 @@ void SMTChecker::endVisit(VariableDeclarationStatement const& _varDecl)
else if (knownVariable(*_varDecl.declarations()[0]))
{
if (_varDecl.initialValue())
- // TODO more checks?
- assignment(*_varDecl.declarations()[0], *_varDecl.initialValue());
+ assignment(*_varDecl.declarations()[0], *_varDecl.initialValue(), _varDecl.location());
}
else
m_errorReporter.warning(
@@ -208,7 +207,7 @@ void SMTChecker::endVisit(Assignment const& _assignment)
{
Declaration const* decl = identifier->annotation().referencedDeclaration;
if (knownVariable(*decl))
- assignment(*decl, _assignment.rightHandSide());
+ assignment(*decl, _assignment.rightHandSide(), _assignment.location());
else
m_errorReporter.warning(
_assignment.location(),
@@ -230,7 +229,81 @@ void SMTChecker::endVisit(TupleExpression const& _tuple)
"Assertion checker does not yet implement tules and inline arrays."
);
else
- m_interface->addAssertion(expr(_tuple) == expr(*_tuple.components()[0]));
+ defineExpr(_tuple, expr(*_tuple.components()[0]));
+}
+
+void SMTChecker::checkUnderOverflow(smt::Expression _value, IntegerType const& _type, SourceLocation const& _location)
+{
+ checkCondition(
+ _value < minValue(_type),
+ _location,
+ "Underflow (resulting value less than " + formatNumber(_type.minValue()) + ")",
+ "value",
+ &_value
+ );
+ checkCondition(
+ _value > maxValue(_type),
+ _location,
+ "Overflow (resulting value larger than " + formatNumber(_type.maxValue()) + ")",
+ "value",
+ &_value
+ );
+}
+
+void SMTChecker::endVisit(UnaryOperation const& _op)
+{
+ switch (_op.getOperator())
+ {
+ case Token::Not: // !
+ {
+ solAssert(_op.annotation().type->category() == Type::Category::Bool, "");
+ defineExpr(_op, !expr(_op.subExpression()));
+ break;
+ }
+ case Token::Inc: // ++ (pre- or postfix)
+ case Token::Dec: // -- (pre- or postfix)
+ {
+ solAssert(_op.annotation().type->category() == Type::Category::Integer, "");
+ solAssert(_op.subExpression().annotation().lValueRequested, "");
+ if (Identifier const* identifier = dynamic_cast<Identifier const*>(&_op.subExpression()))
+ {
+ Declaration const* decl = identifier->annotation().referencedDeclaration;
+ if (knownVariable(*decl))
+ {
+ auto innerValue = currentValue(*decl);
+ auto newValue = _op.getOperator() == Token::Inc ? innerValue + 1 : innerValue - 1;
+ assignment(*decl, newValue, _op.location());
+ defineExpr(_op, _op.isPrefixOperation() ? newValue : innerValue);
+ }
+ else
+ m_errorReporter.warning(
+ _op.location(),
+ "Assertion checker does not yet implement such assignments."
+ );
+ }
+ else
+ m_errorReporter.warning(
+ _op.location(),
+ "Assertion checker does not yet implement such increments / decrements."
+ );
+ break;
+ }
+ case Token::Add: // +
+ defineExpr(_op, expr(_op.subExpression()));
+ break;
+ case Token::Sub: // -
+ {
+ defineExpr(_op, 0 - expr(_op.subExpression()));
+ if (auto intType = dynamic_cast<IntegerType const*>(_op.annotation().type.get()))
+ checkUnderOverflow(expr(_op), *intType, _op.location());
+ break;
+ }
+ default:
+ m_errorReporter.warning(
+ _op.location(),
+ "Assertion checker does not yet implement this operator."
+ );
+ }
}
void SMTChecker::endVisit(BinaryOperation const& _op)
@@ -274,10 +347,8 @@ void SMTChecker::endVisit(FunctionCall const& _funCall)
{
solAssert(args.size() == 1, "");
solAssert(args[0]->annotation().type->category() == Type::Category::Bool, "");
+ checkBooleanNotConstant(*args[0], "Condition is always $VALUE.");
m_interface->addAssertion(expr(*args[0]));
- checkCondition(!(expr(*args[0])), _funCall.location(), "Unreachable code");
- // TODO is there something meaningful we can check here?
- // We can check whether the condition is always fulfilled or never fulfilled.
}
}
@@ -290,7 +361,7 @@ void SMTChecker::endVisit(Identifier const& _identifier)
// Will be translated as part of the node that requested the lvalue.
}
else if (dynamic_cast<IntegerType const*>(_identifier.annotation().type.get()))
- m_interface->addAssertion(expr(_identifier) == currentValue(*decl));
+ defineExpr(_identifier, currentValue(*decl));
else if (FunctionType const* fun = dynamic_cast<FunctionType const*>(_identifier.annotation().type.get()))
{
if (fun->kind() == FunctionType::Kind::Assert || fun->kind() == FunctionType::Kind::Require)
@@ -306,10 +377,10 @@ void SMTChecker::endVisit(Literal const& _literal)
if (RationalNumberType const* rational = dynamic_cast<RationalNumberType const*>(&type))
solAssert(!rational->isFractional(), "");
- m_interface->addAssertion(expr(_literal) == smt::Expression(type.literalValue(&_literal)));
+ defineExpr(_literal, smt::Expression(type.literalValue(&_literal)));
}
else if (type.category() == Type::Category::Bool)
- m_interface->addAssertion(expr(_literal) == smt::Expression(_literal.token() == Token::TrueLiteral ? true : false));
+ defineExpr(_literal, smt::Expression(_literal.token() == Token::TrueLiteral ? true : false));
else
m_errorReporter.warning(
_literal.location(),
@@ -326,6 +397,7 @@ void SMTChecker::arithmeticOperation(BinaryOperation const& _op)
case Token::Add:
case Token::Sub:
case Token::Mul:
+ case Token::Div:
{
solAssert(_op.annotation().commonType, "");
solAssert(_op.annotation().commonType->category() == Type::Category::Integer, "");
@@ -335,27 +407,19 @@ void SMTChecker::arithmeticOperation(BinaryOperation const& _op)
smt::Expression value(
op == Token::Add ? left + right :
op == Token::Sub ? left - right :
+ op == Token::Div ? left / right :
/*op == Token::Mul*/ left * right
);
- // Overflow check
- auto const& intType = dynamic_cast<IntegerType const&>(*_op.annotation().commonType);
- checkCondition(
- value < minValue(intType),
- _op.location(),
- "Underflow (resulting value less than " + formatNumber(intType.minValue()) + ")",
- "value",
- &value
- );
- checkCondition(
- value > maxValue(intType),
- _op.location(),
- "Overflow (resulting value larger than " + formatNumber(intType.maxValue()) + ")",
- "value",
- &value
- );
+ if (_op.getOperator() == Token::Div)
+ {
+ checkCondition(right == 0, _op.location(), "Division by zero", "value", &right);
+ m_interface->addAssertion(right != 0);
+ }
+
+ checkUnderOverflow(value, dynamic_cast<IntegerType const&>(*_op.annotation().commonType), _op.location());
- m_interface->addAssertion(expr(_op) == value);
+ defineExpr(_op, value);
break;
}
default:
@@ -383,7 +447,7 @@ void SMTChecker::compareOperation(BinaryOperation const& _op)
/*op == Token::GreaterThanOrEqual*/ (left >= right)
);
// TODO: check that other values for op are not possible.
- m_interface->addAssertion(expr(_op) == value);
+ defineExpr(_op, value);
}
else
m_errorReporter.warning(
@@ -400,9 +464,9 @@ void SMTChecker::booleanOperation(BinaryOperation const& _op)
{
// @TODO check that both of them are not constant
if (_op.getOperator() == Token::And)
- m_interface->addAssertion(expr(_op) == expr(_op.leftExpression()) && expr(_op.rightExpression()));
+ defineExpr(_op, expr(_op.leftExpression()) && expr(_op.rightExpression()));
else
- m_interface->addAssertion(expr(_op) == expr(_op.leftExpression()) || expr(_op.rightExpression()));
+ defineExpr(_op, expr(_op.leftExpression()) || expr(_op.rightExpression()));
}
else
m_errorReporter.warning(
@@ -411,11 +475,17 @@ void SMTChecker::booleanOperation(BinaryOperation const& _op)
);
}
-void SMTChecker::assignment(Declaration const& _variable, Expression const& _value)
+void SMTChecker::assignment(Declaration const& _variable, Expression const& _value, SourceLocation const& _location)
{
- // TODO more checks?
- // TODO add restrictions about type (might be assignment from smaller type)
- m_interface->addAssertion(newValue(_variable) == expr(_value));
+ assignment(_variable, expr(_value), _location);
+}
+
+void SMTChecker::assignment(Declaration const& _variable, smt::Expression const& _value, SourceLocation const& _location)
+{
+ TypePointer type = _variable.type();
+ if (auto const* intType = dynamic_cast<IntegerType const*>(type.get()))
+ checkUnderOverflow(_value, *intType, _location);
+ m_interface->addAssertion(newValue(_variable) == _value);
}
void SMTChecker::visitBranch(Statement const& _statement, smt::Expression _condition)
@@ -694,29 +764,38 @@ smt::Expression SMTChecker::maxValue(IntegerType const& _t)
smt::Expression SMTChecker::expr(Expression const& _e)
{
- if (!m_expressions.count(&_e))
+ solAssert(m_expressions.count(&_e), "");
+ return m_expressions.at(&_e);
+}
+
+void SMTChecker::createExpr(Expression const& _e)
+{
+ solAssert(!m_expressions.count(&_e), "");
+ solAssert(_e.annotation().type, "");
+ switch (_e.annotation().type->category())
{
- solAssert(_e.annotation().type, "");
- switch (_e.annotation().type->category())
- {
- case Type::Category::RationalNumber:
- {
- if (RationalNumberType const* rational = dynamic_cast<RationalNumberType const*>(_e.annotation().type.get()))
- solAssert(!rational->isFractional(), "");
- m_expressions.emplace(&_e, m_interface->newInteger(uniqueSymbol(_e)));
- break;
- }
- case Type::Category::Integer:
- m_expressions.emplace(&_e, m_interface->newInteger(uniqueSymbol(_e)));
- break;
- case Type::Category::Bool:
- m_expressions.emplace(&_e, m_interface->newBool(uniqueSymbol(_e)));
- break;
- default:
- solAssert(false, "Type not implemented.");
- }
+ case Type::Category::RationalNumber:
+ {
+ if (RationalNumberType const* rational = dynamic_cast<RationalNumberType const*>(_e.annotation().type.get()))
+ solAssert(!rational->isFractional(), "");
+ m_expressions.emplace(&_e, m_interface->newInteger(uniqueSymbol(_e)));
+ break;
}
- return m_expressions.at(&_e);
+ case Type::Category::Integer:
+ m_expressions.emplace(&_e, m_interface->newInteger(uniqueSymbol(_e)));
+ break;
+ case Type::Category::Bool:
+ m_expressions.emplace(&_e, m_interface->newBool(uniqueSymbol(_e)));
+ break;
+ default:
+ solAssert(false, "Type not implemented.");
+ }
+}
+
+void SMTChecker::defineExpr(Expression const& _e, smt::Expression _value)
+{
+ createExpr(_e);
+ m_interface->addAssertion(expr(_e) == _value);
}
smt::Expression SMTChecker::var(Declaration const& _decl)
diff --git a/libsolidity/formal/SMTChecker.h b/libsolidity/formal/SMTChecker.h
index 8e07d74d..cc3aca81 100644
--- a/libsolidity/formal/SMTChecker.h
+++ b/libsolidity/formal/SMTChecker.h
@@ -57,6 +57,7 @@ private:
virtual void endVisit(ExpressionStatement const& _node) override;
virtual void endVisit(Assignment const& _node) override;
virtual void endVisit(TupleExpression const& _node) override;
+ virtual void endVisit(UnaryOperation const& _node) override;
virtual void endVisit(BinaryOperation const& _node) override;
virtual void endVisit(FunctionCall const& _node) override;
virtual void endVisit(Identifier const& _node) override;
@@ -66,7 +67,8 @@ private:
void compareOperation(BinaryOperation const& _op);
void booleanOperation(BinaryOperation const& _op);
- void assignment(Declaration const& _variable, Expression const& _value);
+ void assignment(Declaration const& _variable, Expression const& _value, SourceLocation const& _location);
+ void assignment(Declaration const& _variable, smt::Expression const& _value, SourceLocation const& _location);
// Visits the branch given by the statement, pushes and pops the SMT checker.
// @param _condition if present, asserts that this condition is true within the branch.
@@ -88,6 +90,9 @@ private:
Expression const& _condition,
std::string const& _description
);
+ /// Checks that the value is in the range given by the type.
+ void checkUnderOverflow(smt::Expression _value, IntegerType const& _Type, SourceLocation const& _location);
+
std::pair<smt::CheckResult, std::vector<std::string>>
checkSatisifableAndGenerateModel(std::vector<smt::Expression> const& _expressionsToEvaluate);
@@ -126,9 +131,12 @@ private:
using VariableSequenceCounters = std::map<Declaration const*, int>;
- /// Returns the expression corresponding to the AST node. Creates a new expression
- /// if it does not exist yet.
+ /// Returns the expression corresponding to the AST node. Throws if the expression does not exist.
smt::Expression expr(Expression const& _e);
+ /// Creates the expression (value can be arbitrary)
+ void createExpr(Expression const& _e);
+ /// Creates the expression and sets its value.
+ void defineExpr(Expression const& _e, smt::Expression _value);
/// Returns the function declaration corresponding to the given variable.
/// The function takes one argument which is the "sequence number".
smt::Expression var(Declaration const& _decl);
diff --git a/libsolidity/formal/SolverInterface.h b/libsolidity/formal/SolverInterface.h
index c9adf863..74c993e8 100644
--- a/libsolidity/formal/SolverInterface.h
+++ b/libsolidity/formal/SolverInterface.h
@@ -120,6 +120,10 @@ public:
{
return Expression("*", std::move(_a), std::move(_b), Sort::Int);
}
+ friend Expression operator/(Expression _a, Expression _b)
+ {
+ return Expression("/", std::move(_a), std::move(_b), Sort::Int);
+ }
Expression operator()(Expression _a) const
{
solAssert(
diff --git a/libsolidity/formal/Z3Interface.cpp b/libsolidity/formal/Z3Interface.cpp
index e5c1aef4..769e6edb 100644
--- a/libsolidity/formal/Z3Interface.cpp
+++ b/libsolidity/formal/Z3Interface.cpp
@@ -127,7 +127,8 @@ z3::expr Z3Interface::toZ3Expr(Expression const& _expr)
{">=", 2},
{"+", 2},
{"-", 2},
- {"*", 2}
+ {"*", 2},
+ {"/", 2}
};
string const& n = _expr.name;
if (m_functions.count(n))
@@ -173,6 +174,8 @@ z3::expr Z3Interface::toZ3Expr(Expression const& _expr)
return arguments[0] - arguments[1];
else if (n == "*")
return arguments[0] * arguments[1];
+ else if (n == "/")
+ return arguments[0] / arguments[1];
// Cannot reach here.
solAssert(false, "");
return arguments[0];