aboutsummaryrefslogtreecommitdiffstats
path: root/libsolidity
diff options
context:
space:
mode:
Diffstat (limited to 'libsolidity')
-rw-r--r--libsolidity/analysis/ConstantEvaluator.cpp22
-rw-r--r--libsolidity/analysis/ConstantEvaluator.h8
-rw-r--r--libsolidity/analysis/TypeChecker.cpp8
-rw-r--r--libsolidity/ast/AST.cpp11
-rw-r--r--libsolidity/ast/AST.h2
-rw-r--r--libsolidity/formal/SMTChecker.cpp352
-rw-r--r--libsolidity/formal/SMTChecker.h43
-rw-r--r--libsolidity/formal/SolverInterface.h1
-rw-r--r--libsolidity/formal/VariableUsage.cpp80
-rw-r--r--libsolidity/formal/VariableUsage.h50
-rw-r--r--libsolidity/formal/Z3Interface.cpp11
11 files changed, 464 insertions, 124 deletions
diff --git a/libsolidity/analysis/ConstantEvaluator.cpp b/libsolidity/analysis/ConstantEvaluator.cpp
index bc3b7cf1..4d546e68 100644
--- a/libsolidity/analysis/ConstantEvaluator.cpp
+++ b/libsolidity/analysis/ConstantEvaluator.cpp
@@ -74,3 +74,25 @@ void ConstantEvaluator::endVisit(Literal const& _literal)
if (!_literal.annotation().type)
m_errorReporter.fatalTypeError(_literal.location(), "Invalid literal value.");
}
+
+void ConstantEvaluator::endVisit(Identifier const& _identifier)
+{
+ VariableDeclaration const* variableDeclaration = dynamic_cast<VariableDeclaration const*>(_identifier.annotation().referencedDeclaration);
+ if (!variableDeclaration)
+ return;
+ if (!variableDeclaration->isConstant())
+ m_errorReporter.fatalTypeError(_identifier.location(), "Identifier must be declared constant.");
+
+ ASTPointer<Expression> value = variableDeclaration->value();
+ if (!value)
+ m_errorReporter.fatalTypeError(_identifier.location(), "Constant identifier declaration must have a constant value.");
+
+ if (!value->annotation().type)
+ {
+ if (m_depth > 32)
+ m_errorReporter.fatalTypeError(_identifier.location(), "Cyclic constant definition (or maximum recursion depth exhausted).");
+ ConstantEvaluator e(*value, m_errorReporter, m_depth + 1);
+ }
+
+ _identifier.annotation().type = value->annotation().type;
+}
diff --git a/libsolidity/analysis/ConstantEvaluator.h b/libsolidity/analysis/ConstantEvaluator.h
index 90bceb5d..6725d610 100644
--- a/libsolidity/analysis/ConstantEvaluator.h
+++ b/libsolidity/analysis/ConstantEvaluator.h
@@ -38,8 +38,9 @@ class TypeChecker;
class ConstantEvaluator: private ASTConstVisitor
{
public:
- ConstantEvaluator(Expression const& _expr, ErrorReporter& _errorReporter):
- m_errorReporter(_errorReporter)
+ ConstantEvaluator(Expression const& _expr, ErrorReporter& _errorReporter, size_t _newDepth = 0):
+ m_errorReporter(_errorReporter),
+ m_depth(_newDepth)
{
_expr.accept(*this);
}
@@ -48,8 +49,11 @@ private:
virtual void endVisit(BinaryOperation const& _operation);
virtual void endVisit(UnaryOperation const& _operation);
virtual void endVisit(Literal const& _literal);
+ virtual void endVisit(Identifier const& _identifier);
ErrorReporter& m_errorReporter;
+ /// Current recursion depth.
+ size_t m_depth;
};
}
diff --git a/libsolidity/analysis/TypeChecker.cpp b/libsolidity/analysis/TypeChecker.cpp
index 746e762e..73047e76 100644
--- a/libsolidity/analysis/TypeChecker.cpp
+++ b/libsolidity/analysis/TypeChecker.cpp
@@ -1122,7 +1122,7 @@ bool TypeChecker::visit(VariableDeclarationStatement const& _statement)
var.annotation().type->toString() +
". Try converting to type " +
valueComponentType->mobileType()->toString() +
- " or use an explicit conversion."
+ " or use an explicit conversion."
);
else
m_errorReporter.typeError(
@@ -1320,7 +1320,7 @@ bool TypeChecker::visit(TupleExpression const& _tuple)
_tuple.annotation().isPure = isPure;
if (_tuple.isInlineArray())
{
- if (!inlineArrayType)
+ if (!inlineArrayType)
m_errorReporter.fatalTypeError(_tuple.location(), "Unable to deduce common type for array elements.");
_tuple.annotation().type = make_shared<ArrayType>(DataLocation::Memory, inlineArrayType, types.size());
}
@@ -2000,7 +2000,9 @@ void TypeChecker::endVisit(Literal const& _literal)
m_errorReporter.warning(
_literal.location(),
"This looks like an address but has an invalid checksum. "
- "If this is not used as an address, please prepend '00'."
+ "If this is not used as an address, please prepend '00'. " +
+ (!_literal.getChecksummedAddress().empty() ? "Correct checksummed address: '" + _literal.getChecksummedAddress() + "'. " : "") +
+ "For more information please see https://solidity.readthedocs.io/en/develop/types.html#address-literals"
);
}
if (!_literal.annotation().type)
diff --git a/libsolidity/ast/AST.cpp b/libsolidity/ast/AST.cpp
index 1048b610..8da6964e 100644
--- a/libsolidity/ast/AST.cpp
+++ b/libsolidity/ast/AST.cpp
@@ -583,3 +583,14 @@ bool Literal::passesAddressChecksum() const
solAssert(isHexNumber(), "Expected hex number");
return dev::passesAddressChecksum(value(), true);
}
+
+std::string Literal::getChecksummedAddress() const
+{
+ solAssert(isHexNumber(), "Expected hex number");
+ /// Pad literal to be a proper hex address.
+ string address = value().substr(2);
+ if (address.length() > 40)
+ return string();
+ address.insert(address.begin(), 40 - address.size(), '0');
+ return dev::getChecksummedAddress(address);
+}
diff --git a/libsolidity/ast/AST.h b/libsolidity/ast/AST.h
index 733e7c78..feffde64 100644
--- a/libsolidity/ast/AST.h
+++ b/libsolidity/ast/AST.h
@@ -1613,6 +1613,8 @@ public:
bool looksLikeAddress() const;
/// @returns true if it passes the address checksum test.
bool passesAddressChecksum() const;
+ /// @returns the checksummed version of an address (or empty string if not valid)
+ std::string getChecksummedAddress() const;
private:
Token::Value m_token;
diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp
index 2d2f05ec..1050621e 100644
--- a/libsolidity/formal/SMTChecker.cpp
+++ b/libsolidity/formal/SMTChecker.cpp
@@ -23,9 +23,12 @@
#include <libsolidity/formal/SMTLib2Interface.h>
#endif
+#include <libsolidity/formal/VariableUsage.h>
+
#include <libsolidity/interface/ErrorReporter.h>
#include <boost/range/adaptor/map.hpp>
+#include <boost/algorithm/string/replace.hpp>
using namespace std;
using namespace dev;
@@ -44,28 +47,15 @@ SMTChecker::SMTChecker(ErrorReporter& _errorReporter, ReadCallback::Callback con
void SMTChecker::analyze(SourceUnit const& _source)
{
+ m_variableUsage = make_shared<VariableUsage>(_source);
if (_source.annotation().experimentalFeatures.count(ExperimentalFeature::SMTChecker))
- {
- m_interface->reset();
- m_currentSequenceCounter.clear();
- m_nextFreeSequenceCounter.clear();
_source.accept(*this);
- }
}
void SMTChecker::endVisit(VariableDeclaration const& _varDecl)
{
- if (_varDecl.value())
- {
- m_errorReporter.warning(
- _varDecl.location(),
- "Assertion checker does not yet support this."
- );
- }
- else if (_varDecl.isLocalOrReturn())
- createVariable(_varDecl, true);
- else if (_varDecl.isCallableParameter())
- createVariable(_varDecl, false);
+ if (_varDecl.isLocalVariable() && _varDecl.type()->isValueType() &&_varDecl.value())
+ assignment(_varDecl, *_varDecl.value());
}
bool SMTChecker::visit(FunctionDefinition const& _function)
@@ -75,20 +65,22 @@ bool SMTChecker::visit(FunctionDefinition const& _function)
_function.location(),
"Assertion checker does not yet support constructors and functions with modifiers."
);
- // TODO actually we probably also have to reset all local variables and similar things.
m_currentFunction = &_function;
- m_interface->push();
+ // We only handle local variables, so we clear at the beginning of the function.
+ // If we add storage variables, those should be cleared differently.
+ m_interface->reset();
+ m_currentSequenceCounter.clear();
+ m_nextFreeSequenceCounter.clear();
+ m_conditionalExecutionHappened = false;
+ initializeLocalVariables(_function);
return true;
}
void SMTChecker::endVisit(FunctionDefinition const&)
{
// TOOD we could check for "reachability", i.e. satisfiability here.
- // We only handle local variables, so we clear everything.
+ // We only handle local variables, so we clear at the beginning of the function.
// If we add storage variables, those should be cleared differently.
- m_currentSequenceCounter.clear();
- m_nextFreeSequenceCounter.clear();
- m_interface->pop();
m_currentFunction = nullptr;
}
@@ -96,57 +88,84 @@ bool SMTChecker::visit(IfStatement const& _node)
{
_node.condition().accept(*this);
- // TODO Check if condition is always true
-
- auto countersAtStart = m_currentSequenceCounter;
- m_interface->push();
- m_interface->addAssertion(expr(_node.condition()));
- _node.trueStatement().accept(*this);
- auto countersAtEndOfTrue = m_currentSequenceCounter;
- m_interface->pop();
+ checkBooleanNotConstant(_node.condition(), "Condition is always $VALUE.");
- decltype(m_currentSequenceCounter) countersAtEndOfFalse;
+ visitBranch(_node.trueStatement(), expr(_node.condition()));
+ vector<Declaration const*> touchedVariables = m_variableUsage->touchedVariables(_node.trueStatement());
if (_node.falseStatement())
{
- m_currentSequenceCounter = countersAtStart;
- m_interface->push();
- m_interface->addAssertion(!expr(_node.condition()));
- _node.falseStatement()->accept(*this);
- countersAtEndOfFalse = m_currentSequenceCounter;
- m_interface->pop();
+ visitBranch(*_node.falseStatement(), !expr(_node.condition()));
+ touchedVariables += m_variableUsage->touchedVariables(*_node.falseStatement());
}
- else
- countersAtEndOfFalse = countersAtStart;
- // Reset all values that have been touched.
+ resetVariables(touchedVariables);
- // TODO this should use a previously generated side-effect structure
+ return false;
+}
- solAssert(countersAtEndOfFalse.size() == countersAtEndOfTrue.size(), "");
- for (auto const& declCounter: countersAtEndOfTrue)
+bool SMTChecker::visit(WhileStatement const& _node)
+{
+ auto touchedVariables = m_variableUsage->touchedVariables(_node);
+ resetVariables(touchedVariables);
+ if (_node.isDoWhile())
{
- solAssert(countersAtEndOfFalse.count(declCounter.first), "");
- auto decl = declCounter.first;
- int trueCounter = countersAtEndOfTrue.at(decl);
- int falseCounter = countersAtEndOfFalse.at(decl);
- if (trueCounter == falseCounter)
- continue; // Was not modified
- newValue(*decl);
- setValue(*decl, 0);
+ visitBranch(_node.body());
+ // TODO the assertions generated in the body should still be active in the condition
+ _node.condition().accept(*this);
+ checkBooleanNotConstant(_node.condition(), "Do-while loop condition is always $VALUE.");
}
+ else
+ {
+ _node.condition().accept(*this);
+ checkBooleanNotConstant(_node.condition(), "While loop condition is always $VALUE.");
+
+ visitBranch(_node.body(), expr(_node.condition()));
+ }
+ resetVariables(touchedVariables);
+
return false;
}
-bool SMTChecker::visit(WhileStatement const& _node)
+bool SMTChecker::visit(ForStatement const& _node)
{
- _node.condition().accept(*this);
+ if (_node.initializationExpression())
+ _node.initializationExpression()->accept(*this);
+
+ // Do not reset the init expression part.
+ auto touchedVariables =
+ m_variableUsage->touchedVariables(_node.body());
+ if (_node.condition())
+ touchedVariables += m_variableUsage->touchedVariables(*_node.condition());
+ if (_node.loopExpression())
+ touchedVariables += m_variableUsage->touchedVariables(*_node.loopExpression());
+ // Remove duplicates
+ std::sort(touchedVariables.begin(), touchedVariables.end());
+ touchedVariables.erase(std::unique(touchedVariables.begin(), touchedVariables.end()), touchedVariables.end());
+
+ resetVariables(touchedVariables);
+
+ if (_node.condition())
+ {
+ _node.condition()->accept(*this);
+ checkBooleanNotConstant(*_node.condition(), "For loop condition is always $VALUE.");
+ }
- //m_interface->push();
- //m_interface->addAssertion(expr(_node.condition()));
- // TDOO clear knowledge (increment sequence numbers and add bounds assertions ) apart from assertions
+ VariableSequenceCounters sequenceCountersStart = m_currentSequenceCounter;
+ m_interface->push();
+ if (_node.condition())
+ m_interface->addAssertion(expr(*_node.condition()));
+ _node.body().accept(*this);
+ if (_node.loopExpression())
+ _node.loopExpression()->accept(*this);
- // TODO combine similar to if
- return true;
+ m_interface->pop();
+
+ m_conditionalExecutionHappened = true;
+ m_currentSequenceCounter = sequenceCountersStart;
+
+ resetVariables(touchedVariables);
+
+ return false;
}
void SMTChecker::endVisit(VariableDeclarationStatement const& _varDecl)
@@ -160,8 +179,7 @@ void SMTChecker::endVisit(VariableDeclarationStatement const& _varDecl)
{
if (_varDecl.initialValue())
// TODO more checks?
- // TODO add restrictions about type (might be assignment from smaller type)
- m_interface->addAssertion(newValue(*_varDecl.declarations()[0]) == expr(*_varDecl.initialValue()));
+ assignment(*_varDecl.declarations()[0], *_varDecl.initialValue());
}
else
m_errorReporter.warning(
@@ -190,9 +208,7 @@ void SMTChecker::endVisit(Assignment const& _assignment)
{
Declaration const* decl = identifier->annotation().referencedDeclaration;
if (knownVariable(*decl))
- // TODO more checks?
- // TODO add restrictions about type (might be assignment from smaller type)
- m_interface->addAssertion(newValue(*decl) == expr(_assignment.rightHandSide()));
+ assignment(*decl, _assignment.rightHandSide());
else
m_errorReporter.warning(
_assignment.location(),
@@ -269,23 +285,17 @@ void SMTChecker::endVisit(Identifier const& _identifier)
{
Declaration const* decl = _identifier.annotation().referencedDeclaration;
solAssert(decl, "");
- if (dynamic_cast<IntegerType const*>(_identifier.annotation().type.get()))
+ if (_identifier.annotation().lValueRequested)
{
- m_interface->addAssertion(expr(_identifier) == currentValue(*decl));
- return;
+ // 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));
else if (FunctionType const* fun = dynamic_cast<FunctionType const*>(_identifier.annotation().type.get()))
{
if (fun->kind() == FunctionType::Kind::Assert || fun->kind() == FunctionType::Kind::Require)
return;
- // TODO for others, clear our knowledge about storage and memory
}
- m_errorReporter.warning(
- _identifier.location(),
- "Assertion checker does not yet support the type of this expression (" +
- _identifier.annotation().type->toString() +
- ")."
- );
}
void SMTChecker::endVisit(Literal const& _literal)
@@ -298,10 +308,12 @@ void SMTChecker::endVisit(Literal const& _literal)
m_interface->addAssertion(expr(_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));
else
m_errorReporter.warning(
_literal.location(),
- "Assertion checker does not yet support the type of this expression (" +
+ "Assertion checker does not yet support the type of this literal (" +
_literal.annotation().type->toString() +
")."
);
@@ -386,6 +398,7 @@ void SMTChecker::booleanOperation(BinaryOperation const& _op)
solAssert(_op.annotation().commonType, "");
if (_op.annotation().commonType->category() == Type::Category::Bool)
{
+ // @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()));
else
@@ -395,7 +408,33 @@ void SMTChecker::booleanOperation(BinaryOperation const& _op)
m_errorReporter.warning(
_op.location(),
"Assertion checker does not yet implement the type " + _op.annotation().commonType->toString() + " for boolean operations"
- );
+ );
+}
+
+void SMTChecker::assignment(Declaration const& _variable, Expression const& _value)
+{
+ // TODO more checks?
+ // TODO add restrictions about type (might be assignment from smaller type)
+ m_interface->addAssertion(newValue(_variable) == expr(_value));
+}
+
+void SMTChecker::visitBranch(Statement const& _statement, smt::Expression _condition)
+{
+ visitBranch(_statement, &_condition);
+}
+
+void SMTChecker::visitBranch(Statement const& _statement, smt::Expression const* _condition)
+{
+ VariableSequenceCounters sequenceCountersStart = m_currentSequenceCounter;
+
+ m_interface->push();
+ if (_condition)
+ m_interface->addAssertion(*_condition);
+ _statement.accept(*this);
+ m_interface->pop();
+
+ m_conditionalExecutionHappened = true;
+ m_currentSequenceCounter = sequenceCountersStart;
}
void SMTChecker::checkCondition(
@@ -433,19 +472,13 @@ void SMTChecker::checkCondition(
}
smt::CheckResult result;
vector<string> values;
- try
- {
- tie(result, values) = m_interface->check(expressionsToEvaluate);
- }
- catch (smt::SolverError const& _e)
- {
- string description("Error querying SMT solver");
- if (_e.comment())
- description += ": " + *_e.comment();
- m_errorReporter.warning(_location, description);
- return;
- }
+ tie(result, values) = checkSatisifableAndGenerateModel(expressionsToEvaluate);
+ string conditionalComment;
+ if (m_conditionalExecutionHappened)
+ conditionalComment =
+ "\nNote that some information is erased after conditional execution of parts of the code.\n"
+ "You can re-introduce information using require().";
switch (result)
{
case smt::CheckResult::SATISFIABLE:
@@ -457,27 +490,17 @@ void SMTChecker::checkCondition(
message << " for:\n";
solAssert(values.size() == expressionNames.size(), "");
for (size_t i = 0; i < values.size(); ++i)
- {
- string formattedValue = values.at(i);
- try
- {
- // Parse and re-format nicely
- formattedValue = formatNumber(bigint(formattedValue));
- }
- catch (...) { }
-
- message << " " << expressionNames.at(i) << " = " << formattedValue << "\n";
- }
+ message << " " << expressionNames.at(i) << " = " << values.at(i) << "\n";
}
else
message << ".";
- m_errorReporter.warning(_location, message.str());
+ m_errorReporter.warning(_location, message.str() + conditionalComment);
break;
}
case smt::CheckResult::UNSATISFIABLE:
break;
case smt::CheckResult::UNKNOWN:
- m_errorReporter.warning(_location, _description + " might happen here.");
+ m_errorReporter.warning(_location, _description + " might happen here." + conditionalComment);
break;
case smt::CheckResult::ERROR:
m_errorReporter.warning(_location, "Error trying to invoke SMT solver.");
@@ -488,7 +511,110 @@ void SMTChecker::checkCondition(
m_interface->pop();
}
-void SMTChecker::createVariable(VariableDeclaration const& _varDecl, bool _setToZero)
+void SMTChecker::checkBooleanNotConstant(Expression const& _condition, string const& _description)
+{
+ // Do not check for const-ness if this is a constant.
+ if (dynamic_cast<Literal const*>(&_condition))
+ return;
+
+ m_interface->push();
+ m_interface->addAssertion(expr(_condition));
+ auto positiveResult = checkSatisifable();
+ m_interface->pop();
+
+ m_interface->push();
+ m_interface->addAssertion(!expr(_condition));
+ auto negatedResult = checkSatisifable();
+ m_interface->pop();
+
+ if (positiveResult == smt::CheckResult::ERROR || negatedResult == smt::CheckResult::ERROR)
+ m_errorReporter.warning(_condition.location(), "Error trying to invoke SMT solver.");
+ else if (positiveResult == smt::CheckResult::SATISFIABLE && negatedResult == smt::CheckResult::SATISFIABLE)
+ {
+ // everything fine.
+ }
+ else if (positiveResult == smt::CheckResult::UNSATISFIABLE && negatedResult == smt::CheckResult::UNSATISFIABLE)
+ m_errorReporter.warning(_condition.location(), "Condition unreachable.");
+ else
+ {
+ string value;
+ if (positiveResult == smt::CheckResult::SATISFIABLE)
+ {
+ solAssert(negatedResult == smt::CheckResult::UNSATISFIABLE, "");
+ value = "true";
+ }
+ else
+ {
+ solAssert(positiveResult == smt::CheckResult::UNSATISFIABLE, "");
+ solAssert(negatedResult == smt::CheckResult::SATISFIABLE, "");
+ value = "false";
+ }
+ m_errorReporter.warning(_condition.location(), boost::algorithm::replace_all_copy(_description, "$VALUE", value));
+ }
+}
+
+pair<smt::CheckResult, vector<string>>
+SMTChecker::checkSatisifableAndGenerateModel(vector<smt::Expression> const& _expressionsToEvaluate)
+{
+ smt::CheckResult result;
+ vector<string> values;
+ try
+ {
+ tie(result, values) = m_interface->check(_expressionsToEvaluate);
+ }
+ catch (smt::SolverError const& _e)
+ {
+ string description("Error querying SMT solver");
+ if (_e.comment())
+ description += ": " + *_e.comment();
+ m_errorReporter.warning(description);
+ result = smt::CheckResult::ERROR;
+ }
+
+ for (string& value: values)
+ {
+ try
+ {
+ // Parse and re-format nicely
+ value = formatNumber(bigint(value));
+ }
+ catch (...) { }
+ }
+
+ return make_pair(result, values);
+}
+
+smt::CheckResult SMTChecker::checkSatisifable()
+{
+ return checkSatisifableAndGenerateModel({}).first;
+}
+
+void SMTChecker::initializeLocalVariables(FunctionDefinition const& _function)
+{
+ for (auto const& variable: _function.localVariables())
+ if (createVariable(*variable))
+ setZeroValue(*variable);
+
+ for (auto const& param: _function.parameters())
+ if (createVariable(*param))
+ setUnknownValue(*param);
+
+ if (_function.returnParameterList())
+ for (auto const& retParam: _function.returnParameters())
+ if (createVariable(*retParam))
+ setZeroValue(*retParam);
+}
+
+void SMTChecker::resetVariables(vector<Declaration const*> _variables)
+{
+ for (auto const* decl: _variables)
+ {
+ newValue(*decl);
+ setUnknownValue(*decl);
+ }
+}
+
+bool SMTChecker::createVariable(VariableDeclaration const& _varDecl)
{
if (dynamic_cast<IntegerType const*>(_varDecl.type().get()))
{
@@ -498,13 +624,16 @@ void SMTChecker::createVariable(VariableDeclaration const& _varDecl, bool _setTo
m_currentSequenceCounter[&_varDecl] = 0;
m_nextFreeSequenceCounter[&_varDecl] = 1;
m_variables.emplace(&_varDecl, m_interface->newFunction(uniqueSymbol(_varDecl), smt::Sort::Int, smt::Sort::Int));
- setValue(_varDecl, _setToZero);
+ return true;
}
else
+ {
m_errorReporter.warning(
_varDecl.location(),
"Assertion checker does not yet support the type of this variable."
);
+ return false;
+ }
}
string SMTChecker::uniqueSymbol(Declaration const& _decl)
@@ -535,23 +664,22 @@ smt::Expression SMTChecker::valueAtSequence(const Declaration& _decl, int _seque
smt::Expression SMTChecker::newValue(Declaration const& _decl)
{
- solAssert(m_currentSequenceCounter.count(&_decl), "");
solAssert(m_nextFreeSequenceCounter.count(&_decl), "");
m_currentSequenceCounter[&_decl] = m_nextFreeSequenceCounter[&_decl]++;
return currentValue(_decl);
}
-void SMTChecker::setValue(Declaration const& _decl, bool _setToZero)
+void SMTChecker::setZeroValue(Declaration const& _decl)
{
- auto const& intType = dynamic_cast<IntegerType const&>(*_decl.type());
+ solAssert(_decl.type()->category() == Type::Category::Integer, "");
+ m_interface->addAssertion(currentValue(_decl) == 0);
+}
- if (_setToZero)
- m_interface->addAssertion(currentValue(_decl) == 0);
- else
- {
- m_interface->addAssertion(currentValue(_decl) >= minValue(intType));
- m_interface->addAssertion(currentValue(_decl) <= maxValue(intType));
- }
+void SMTChecker::setUnknownValue(Declaration const& _decl)
+{
+ auto const& intType = dynamic_cast<IntegerType const&>(*_decl.type());
+ m_interface->addAssertion(currentValue(_decl) >= minValue(intType));
+ m_interface->addAssertion(currentValue(_decl) <= maxValue(intType));
}
smt::Expression SMTChecker::minValue(IntegerType const& _t)
diff --git a/libsolidity/formal/SMTChecker.h b/libsolidity/formal/SMTChecker.h
index faaac639..8e07d74d 100644
--- a/libsolidity/formal/SMTChecker.h
+++ b/libsolidity/formal/SMTChecker.h
@@ -17,8 +17,11 @@
#pragma once
-#include <libsolidity/ast/ASTVisitor.h>
+
#include <libsolidity/formal/SolverInterface.h>
+
+#include <libsolidity/ast/ASTVisitor.h>
+
#include <libsolidity/interface/ReadFile.h>
#include <map>
@@ -29,6 +32,7 @@ namespace dev
namespace solidity
{
+class VariableUsage;
class ErrorReporter;
class SMTChecker: private ASTConstVisitor
@@ -48,6 +52,7 @@ private:
virtual void endVisit(FunctionDefinition const& _node) override;
virtual bool visit(IfStatement const& _node) override;
virtual bool visit(WhileStatement const& _node) override;
+ virtual bool visit(ForStatement const& _node) override;
virtual void endVisit(VariableDeclarationStatement const& _node) override;
virtual void endVisit(ExpressionStatement const& _node) override;
virtual void endVisit(Assignment const& _node) override;
@@ -61,6 +66,14 @@ private:
void compareOperation(BinaryOperation const& _op);
void booleanOperation(BinaryOperation const& _op);
+ void assignment(Declaration const& _variable, Expression const& _value);
+
+ // 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.
+ void visitBranch(Statement const& _statement, smt::Expression const* _condition = nullptr);
+ void visitBranch(Statement const& _statement, smt::Expression _condition);
+
+ /// Check that a condition can be satisfied.
void checkCondition(
smt::Expression _condition,
SourceLocation const& _location,
@@ -68,8 +81,24 @@ private:
std::string const& _additionalValueName = "",
smt::Expression* _additionalValue = nullptr
);
+ /// Checks that a boolean condition is not constant. Do not warn if the expression
+ /// is a literal constant.
+ /// @param _description the warning string, $VALUE will be replaced by the constant value.
+ void checkBooleanNotConstant(
+ Expression const& _condition,
+ std::string const& _description
+ );
+
+ std::pair<smt::CheckResult, std::vector<std::string>>
+ checkSatisifableAndGenerateModel(std::vector<smt::Expression> const& _expressionsToEvaluate);
- void createVariable(VariableDeclaration const& _varDecl, bool _setToZero);
+ smt::CheckResult checkSatisifable();
+
+ void initializeLocalVariables(FunctionDefinition const& _function);
+ void resetVariables(std::vector<Declaration const*> _variables);
+ /// Tries to create an uninitialized variable and returns true on success.
+ /// This fails if the type is not supported.
+ bool createVariable(VariableDeclaration const& _varDecl);
static std::string uniqueSymbol(Declaration const& _decl);
static std::string uniqueSymbol(Expression const& _expr);
@@ -87,12 +116,16 @@ private:
/// sequence number to this value and returns the expression.
smt::Expression newValue(Declaration const& _decl);
- /// Sets the value of the declaration either to zero or to its intrinsic range.
- void setValue(Declaration const& _decl, bool _setToZero);
+ /// Sets the value of the declaration to zero.
+ void setZeroValue(Declaration const& _decl);
+ /// Resets the variable to an unknown value (in its range).
+ void setUnknownValue(Declaration const& decl);
static smt::Expression minValue(IntegerType const& _t);
static smt::Expression maxValue(IntegerType const& _t);
+ 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.
smt::Expression expr(Expression const& _e);
@@ -101,6 +134,8 @@ private:
smt::Expression var(Declaration const& _decl);
std::shared_ptr<smt::SolverInterface> m_interface;
+ std::shared_ptr<VariableUsage> m_variableUsage;
+ bool m_conditionalExecutionHappened = false;
std::map<Declaration const*, int> m_currentSequenceCounter;
std::map<Declaration const*, int> m_nextFreeSequenceCounter;
std::map<Expression const*, smt::Expression> m_expressions;
diff --git a/libsolidity/formal/SolverInterface.h b/libsolidity/formal/SolverInterface.h
index 70dc1585..a69d19d5 100644
--- a/libsolidity/formal/SolverInterface.h
+++ b/libsolidity/formal/SolverInterface.h
@@ -52,6 +52,7 @@ class Expression
{
friend class SolverInterface;
public:
+ explicit Expression(bool _v): name(_v ? "true" : "false") {}
Expression(size_t _number): name(std::to_string(_number)) {}
Expression(u256 const& _number): name(_number.str()) {}
Expression(bigint const& _number): name(_number.str()) {}
diff --git a/libsolidity/formal/VariableUsage.cpp b/libsolidity/formal/VariableUsage.cpp
new file mode 100644
index 00000000..4e96059d
--- /dev/null
+++ b/libsolidity/formal/VariableUsage.cpp
@@ -0,0 +1,80 @@
+/*
+ This file is part of solidity.
+
+ solidity is free software: you can redistribute it and/or modify
+ it under the terms of the GNU General Public License as published by
+ the Free Software Foundation, either version 3 of the License, or
+ (at your option) any later version.
+
+ solidity is distributed in the hope that it will be useful,
+ but WITHOUT ANY WARRANTY; without even the implied warranty of
+ MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ GNU General Public License for more details.
+
+ You should have received a copy of the GNU General Public License
+ along with solidity. If not, see <http://www.gnu.org/licenses/>.
+*/
+
+#include <libsolidity/formal/VariableUsage.h>
+
+#include <libsolidity/ast/ASTVisitor.h>
+
+using namespace std;
+using namespace dev;
+using namespace dev::solidity;
+
+VariableUsage::VariableUsage(ASTNode const& _node)
+{
+ auto nodeFun = [&](ASTNode const& n) -> bool
+ {
+ if (Identifier const* identifier = dynamic_cast<decltype(identifier)>(&n))
+ {
+ Declaration const* declaration = identifier->annotation().referencedDeclaration;
+ solAssert(declaration, "");
+ if (VariableDeclaration const* varDecl = dynamic_cast<VariableDeclaration const*>(declaration))
+ if (
+ varDecl->isLocalVariable() &&
+ identifier->annotation().lValueRequested &&
+ varDecl->annotation().type->isValueType()
+ )
+ m_touchedVariable[&n] = varDecl;
+ }
+ return true;
+ };
+ auto edgeFun = [&](ASTNode const& _parent, ASTNode const& _child)
+ {
+ if (m_touchedVariable.count(&_child) || m_children.count(&_child))
+ m_children[&_parent].push_back(&_child);
+ };
+
+ ASTReduce reducer(nodeFun, edgeFun);
+ _node.accept(reducer);
+}
+
+vector<Declaration const*> VariableUsage::touchedVariables(ASTNode const& _node) const
+{
+ if (!m_children.count(&_node) && !m_touchedVariable.count(&_node))
+ return {};
+
+ set<Declaration const*> touched;
+ vector<ASTNode const*> toVisit;
+ toVisit.push_back(&_node);
+
+ while (!toVisit.empty())
+ {
+ ASTNode const* n = toVisit.back();
+ toVisit.pop_back();
+ if (m_children.count(n))
+ {
+ solAssert(!m_touchedVariable.count(n), "");
+ toVisit += m_children.at(n);
+ }
+ else
+ {
+ solAssert(m_touchedVariable.count(n), "");
+ touched.insert(m_touchedVariable.at(n));
+ }
+ }
+
+ return {touched.begin(), touched.end()};
+}
diff --git a/libsolidity/formal/VariableUsage.h b/libsolidity/formal/VariableUsage.h
new file mode 100644
index 00000000..62561cce
--- /dev/null
+++ b/libsolidity/formal/VariableUsage.h
@@ -0,0 +1,50 @@
+/*
+ This file is part of solidity.
+
+ solidity is free software: you can redistribute it and/or modify
+ it under the terms of the GNU General Public License as published by
+ the Free Software Foundation, either version 3 of the License, or
+ (at your option) any later version.
+
+ solidity is distributed in the hope that it will be useful,
+ but WITHOUT ANY WARRANTY; without even the implied warranty of
+ MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ GNU General Public License for more details.
+
+ You should have received a copy of the GNU General Public License
+ along with solidity. If not, see <http://www.gnu.org/licenses/>.
+*/
+
+#pragma once
+
+#include <map>
+#include <set>
+#include <vector>
+
+namespace dev
+{
+namespace solidity
+{
+
+class ASTNode;
+class Declaration;
+
+/**
+ * This class collects information about which local variables of value type
+ * are modified in which parts of the AST.
+ */
+class VariableUsage
+{
+public:
+ explicit VariableUsage(ASTNode const& _node);
+
+ std::vector<Declaration const*> touchedVariables(ASTNode const& _node) const;
+
+private:
+ // Variable touched by a specific AST node.
+ std::map<ASTNode const*, Declaration const*> m_touchedVariable;
+ std::map<ASTNode const*, std::vector<ASTNode const*>> m_children;
+};
+
+}
+}
diff --git a/libsolidity/formal/Z3Interface.cpp b/libsolidity/formal/Z3Interface.cpp
index 6111b2c8..e5c1aef4 100644
--- a/libsolidity/formal/Z3Interface.cpp
+++ b/libsolidity/formal/Z3Interface.cpp
@@ -91,7 +91,7 @@ pair<CheckResult, vector<string>> Z3Interface::check(vector<Expression> const& _
solAssert(false, "");
}
- if (result != CheckResult::UNSATISFIABLE)
+ if (result != CheckResult::UNSATISFIABLE && !_expressionsToEvaluate.empty())
{
z3::model m = m_solver.get_model();
for (Expression const& e: _expressionsToEvaluate)
@@ -139,8 +139,13 @@ z3::expr Z3Interface::toZ3Expr(Expression const& _expr)
}
else if (arguments.empty())
{
- // We assume it is an integer...
- return m_context.int_val(n.c_str());
+ if (n == "true")
+ return m_context.bool_val(true);
+ else if (n == "false")
+ return m_context.bool_val(false);
+ else
+ // We assume it is an integer...
+ return m_context.int_val(n.c_str());
}
solAssert(arity.count(n) && arity.at(n) == arguments.size(), "");
generated by cgit (git 2.34.1) at 2024-09-29 22:29:45 +0800