cerc-io/solidity
16
0
Fork 0
mirror of https://github.com/ethereum/solidity synced 2023-10-03 13:03:40 +00:00
Code Issues Actions Packages Projects Releases Wiki Activity

Check for conditions being constant.

Browse Source
This commit is contained in:
chriseth 2017-09-29 16:53:26 +02:00 committed by Alex Beregszaszi
parent e5de4a66ed
commit 22c689d516
4 changed files with 102 additions and 27 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

113
libsolidity/formal/SMTChecker.cpp
View File

@ -28,6 +28,7 @@
#include <libsolidity/interface/ErrorReporter.h>
#include <boost/range/adaptor/map.hpp>
#include <boost/algorithm/string/replace.hpp>
using namespace std;
using namespace dev;
@ -87,7 +88,7 @@ bool SMTChecker::visit(IfStatement const& _node)
{
_node.condition().accept(*this);
// TODO Check if condition is always true
checkBooleanNotConstant(_node.condition(), "Condition is always $VALUE.");
visitBranch(_node.trueStatement(), expr(_node.condition()));
vector<Declaration const*> touchedVariables = m_variableUsage->touchedVariables(_node.trueStatement());
@ -104,8 +105,6 @@ bool SMTChecker::visit(IfStatement const& _node)
bool SMTChecker::visit(WhileStatement const& _node)
{
// TODO Check if condition is always true
auto touchedVariables = m_variableUsage->touchedVariables(_node);
resetVariables(touchedVariables);
if (_node.isDoWhile())
@ -113,10 +112,13 @@ bool SMTChecker::visit(WhileStatement const& _node)
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);
@ -264,6 +266,8 @@ 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(),
@ -426,18 +430,7 @@ 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)
@ -455,17 +448,7 @@ 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 << ".";
@ -486,6 +469,84 @@ void SMTChecker::checkCondition(
m_interface->pop();
}
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())

13
libsolidity/formal/SMTChecker.h
View File

@ -72,6 +72,7 @@ private:
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,
@ -79,6 +80,18 @@ 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);
smt::CheckResult checkSatisifable();
void initializeLocalVariables(FunctionDefinition const& _function);
void resetVariables(std::vector<Declaration const*> _variables);

1
libsolidity/formal/SolverInterface.h
View File

@ -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()) {}

2
libsolidity/formal/Z3Interface.cpp
View File

@ -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)