2017-07-06 09:05:05 +00:00
|
|
|
/*
|
|
|
|
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/SMTChecker.h>
|
|
|
|
|
2018-04-20 14:56:10 +00:00
|
|
|
#include <libsolidity/formal/SMTPortfolio.h>
|
2017-07-06 09:05:05 +00:00
|
|
|
|
2018-01-17 20:02:23 +00:00
|
|
|
#include <libsolidity/formal/SSAVariable.h>
|
2018-02-17 08:34:38 +00:00
|
|
|
#include <libsolidity/formal/SymbolicIntVariable.h>
|
2017-09-28 13:24:24 +00:00
|
|
|
#include <libsolidity/formal/VariableUsage.h>
|
|
|
|
|
2017-07-06 09:05:05 +00:00
|
|
|
#include <libsolidity/interface/ErrorReporter.h>
|
|
|
|
|
2017-07-14 09:49:27 +00:00
|
|
|
#include <boost/range/adaptor/map.hpp>
|
2017-09-29 14:53:26 +00:00
|
|
|
#include <boost/algorithm/string/replace.hpp>
|
2017-07-14 09:49:27 +00:00
|
|
|
|
2017-07-06 09:05:05 +00:00
|
|
|
using namespace std;
|
|
|
|
using namespace dev;
|
|
|
|
using namespace dev::solidity;
|
|
|
|
|
2017-07-13 19:06:29 +00:00
|
|
|
SMTChecker::SMTChecker(ErrorReporter& _errorReporter, ReadCallback::Callback const& _readFileCallback):
|
2018-04-20 14:56:10 +00:00
|
|
|
m_interface(make_shared<smt::SMTPortfolio>(_readFileCallback)),
|
2017-07-11 11:26:43 +00:00
|
|
|
m_errorReporter(_errorReporter)
|
2017-07-06 09:05:05 +00:00
|
|
|
{
|
|
|
|
}
|
|
|
|
|
|
|
|
void SMTChecker::analyze(SourceUnit const& _source)
|
|
|
|
{
|
2017-09-28 13:24:24 +00:00
|
|
|
m_variableUsage = make_shared<VariableUsage>(_source);
|
2017-08-11 16:54:56 +00:00
|
|
|
if (_source.annotation().experimentalFeatures.count(ExperimentalFeature::SMTChecker))
|
2017-07-11 11:26:43 +00:00
|
|
|
_source.accept(*this);
|
|
|
|
}
|
|
|
|
|
2018-04-30 14:30:41 +00:00
|
|
|
bool SMTChecker::visit(ContractDefinition const& _contract)
|
|
|
|
{
|
|
|
|
for (auto _var : _contract.stateVariables())
|
|
|
|
if (_var->type()->isValueType())
|
|
|
|
createVariable(*_var);
|
|
|
|
return true;
|
|
|
|
}
|
|
|
|
|
|
|
|
void SMTChecker::endVisit(ContractDefinition const&)
|
|
|
|
{
|
2018-06-05 09:46:21 +00:00
|
|
|
m_variables.clear();
|
2018-04-30 14:30:41 +00:00
|
|
|
}
|
|
|
|
|
2017-07-11 11:26:43 +00:00
|
|
|
void SMTChecker::endVisit(VariableDeclaration const& _varDecl)
|
|
|
|
{
|
2017-09-28 13:24:24 +00:00
|
|
|
if (_varDecl.isLocalVariable() && _varDecl.type()->isValueType() &&_varDecl.value())
|
2017-10-05 13:23:25 +00:00
|
|
|
assignment(_varDecl, *_varDecl.value(), _varDecl.location());
|
2017-07-11 11:26:43 +00:00
|
|
|
}
|
|
|
|
|
|
|
|
bool SMTChecker::visit(FunctionDefinition const& _function)
|
|
|
|
{
|
|
|
|
if (!_function.modifiers().empty() || _function.isConstructor())
|
|
|
|
m_errorReporter.warning(
|
|
|
|
_function.location(),
|
|
|
|
"Assertion checker does not yet support constructors and functions with modifiers."
|
|
|
|
);
|
|
|
|
m_currentFunction = &_function;
|
2017-09-28 11:44:56 +00:00
|
|
|
m_interface->reset();
|
2017-12-11 19:09:17 +00:00
|
|
|
m_pathConditions.clear();
|
2018-04-19 07:28:44 +00:00
|
|
|
m_loopExecutionHappened = false;
|
2018-04-18 21:14:45 +00:00
|
|
|
resetStateVariables();
|
2018-06-05 09:46:21 +00:00
|
|
|
initializeLocalVariables(_function);
|
2017-07-11 11:26:43 +00:00
|
|
|
return true;
|
|
|
|
}
|
|
|
|
|
|
|
|
void SMTChecker::endVisit(FunctionDefinition const&)
|
|
|
|
{
|
2018-07-10 07:18:59 +00:00
|
|
|
// TODO we could check for "reachability", i.e. satisfiability here.
|
2017-09-28 11:44:56 +00:00
|
|
|
// We only handle local variables, so we clear at the beginning of the function.
|
2017-07-13 19:04:19 +00:00
|
|
|
// If we add storage variables, those should be cleared differently.
|
2018-06-06 10:11:58 +00:00
|
|
|
removeLocalVariables();
|
2017-07-11 11:26:43 +00:00
|
|
|
m_currentFunction = nullptr;
|
|
|
|
}
|
|
|
|
|
2017-07-14 09:49:27 +00:00
|
|
|
bool SMTChecker::visit(IfStatement const& _node)
|
|
|
|
{
|
|
|
|
_node.condition().accept(*this);
|
|
|
|
|
2017-09-29 14:53:26 +00:00
|
|
|
checkBooleanNotConstant(_node.condition(), "Condition is always $VALUE.");
|
2017-07-14 09:49:27 +00:00
|
|
|
|
2017-12-18 18:43:15 +00:00
|
|
|
auto countersEndTrue = visitBranch(_node.trueStatement(), expr(_node.condition()));
|
2018-06-12 08:58:24 +00:00
|
|
|
vector<VariableDeclaration const*> touchedVariables = m_variableUsage->touchedVariables(_node.trueStatement());
|
2018-01-17 20:02:23 +00:00
|
|
|
decltype(countersEndTrue) countersEndFalse;
|
2017-07-14 09:49:27 +00:00
|
|
|
if (_node.falseStatement())
|
2017-09-28 13:24:24 +00:00
|
|
|
{
|
2017-12-18 18:43:15 +00:00
|
|
|
countersEndFalse = visitBranch(*_node.falseStatement(), !expr(_node.condition()));
|
2017-09-28 13:24:24 +00:00
|
|
|
touchedVariables += m_variableUsage->touchedVariables(*_node.falseStatement());
|
|
|
|
}
|
2018-01-17 20:02:23 +00:00
|
|
|
else
|
|
|
|
{
|
|
|
|
countersEndFalse = m_variables;
|
|
|
|
}
|
2017-07-14 09:49:27 +00:00
|
|
|
|
2017-12-18 18:43:15 +00:00
|
|
|
mergeVariables(touchedVariables, expr(_node.condition()), countersEndTrue, countersEndFalse);
|
2017-07-14 09:49:27 +00:00
|
|
|
|
|
|
|
return false;
|
|
|
|
}
|
|
|
|
|
|
|
|
bool SMTChecker::visit(WhileStatement const& _node)
|
|
|
|
{
|
2017-09-28 13:24:24 +00:00
|
|
|
auto touchedVariables = m_variableUsage->touchedVariables(_node);
|
|
|
|
resetVariables(touchedVariables);
|
2017-09-28 11:44:56 +00:00
|
|
|
if (_node.isDoWhile())
|
|
|
|
{
|
2017-09-28 13:24:24 +00:00
|
|
|
visitBranch(_node.body());
|
|
|
|
// TODO the assertions generated in the body should still be active in the condition
|
2017-09-28 11:44:56 +00:00
|
|
|
_node.condition().accept(*this);
|
2017-09-29 14:53:26 +00:00
|
|
|
checkBooleanNotConstant(_node.condition(), "Do-while loop condition is always $VALUE.");
|
2017-09-28 11:44:56 +00:00
|
|
|
}
|
|
|
|
else
|
|
|
|
{
|
|
|
|
_node.condition().accept(*this);
|
2017-09-29 14:53:26 +00:00
|
|
|
checkBooleanNotConstant(_node.condition(), "While loop condition is always $VALUE.");
|
|
|
|
|
2017-09-28 13:24:24 +00:00
|
|
|
visitBranch(_node.body(), expr(_node.condition()));
|
2017-09-28 11:44:56 +00:00
|
|
|
}
|
2018-04-19 07:28:44 +00:00
|
|
|
m_loopExecutionHappened = true;
|
2017-09-28 13:24:24 +00:00
|
|
|
resetVariables(touchedVariables);
|
2017-07-14 09:49:27 +00:00
|
|
|
|
2017-09-28 11:44:56 +00:00
|
|
|
return false;
|
2017-07-14 09:49:27 +00:00
|
|
|
}
|
|
|
|
|
2017-10-04 19:45:45 +00:00
|
|
|
bool SMTChecker::visit(ForStatement const& _node)
|
|
|
|
{
|
|
|
|
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.");
|
|
|
|
}
|
|
|
|
|
2018-01-17 20:02:23 +00:00
|
|
|
VariableSequenceCounters sequenceCountersStart = m_variables;
|
2017-10-04 19:45:45 +00:00
|
|
|
m_interface->push();
|
|
|
|
if (_node.condition())
|
|
|
|
m_interface->addAssertion(expr(*_node.condition()));
|
|
|
|
_node.body().accept(*this);
|
|
|
|
if (_node.loopExpression())
|
|
|
|
_node.loopExpression()->accept(*this);
|
|
|
|
|
|
|
|
m_interface->pop();
|
|
|
|
|
2018-04-19 07:28:44 +00:00
|
|
|
m_loopExecutionHappened = true;
|
2018-01-17 20:02:23 +00:00
|
|
|
std::swap(sequenceCountersStart, m_variables);
|
2017-10-04 19:45:45 +00:00
|
|
|
|
|
|
|
resetVariables(touchedVariables);
|
|
|
|
|
|
|
|
return false;
|
|
|
|
}
|
|
|
|
|
2017-07-11 11:26:43 +00:00
|
|
|
void SMTChecker::endVisit(VariableDeclarationStatement const& _varDecl)
|
|
|
|
{
|
|
|
|
if (_varDecl.declarations().size() != 1)
|
|
|
|
m_errorReporter.warning(
|
|
|
|
_varDecl.location(),
|
|
|
|
"Assertion checker does not yet support such variable declarations."
|
|
|
|
);
|
2017-07-14 09:49:27 +00:00
|
|
|
else if (knownVariable(*_varDecl.declarations()[0]))
|
|
|
|
{
|
|
|
|
if (_varDecl.initialValue())
|
2017-10-05 13:23:25 +00:00
|
|
|
assignment(*_varDecl.declarations()[0], *_varDecl.initialValue(), _varDecl.location());
|
2017-07-14 09:49:27 +00:00
|
|
|
}
|
2017-07-11 11:26:43 +00:00
|
|
|
else
|
|
|
|
m_errorReporter.warning(
|
|
|
|
_varDecl.location(),
|
|
|
|
"Assertion checker does not yet implement such variable declarations."
|
|
|
|
);
|
|
|
|
}
|
|
|
|
|
|
|
|
void SMTChecker::endVisit(ExpressionStatement const&)
|
|
|
|
{
|
|
|
|
}
|
|
|
|
|
|
|
|
void SMTChecker::endVisit(Assignment const& _assignment)
|
|
|
|
{
|
|
|
|
if (_assignment.assignmentOperator() != Token::Value::Assign)
|
|
|
|
m_errorReporter.warning(
|
|
|
|
_assignment.location(),
|
|
|
|
"Assertion checker does not yet implement compound assignment."
|
|
|
|
);
|
2018-03-12 19:15:27 +00:00
|
|
|
else if (!SSAVariable::isSupportedType(_assignment.annotation().type->category()))
|
2017-07-11 11:26:43 +00:00
|
|
|
m_errorReporter.warning(
|
|
|
|
_assignment.location(),
|
|
|
|
"Assertion checker does not yet implement type " + _assignment.annotation().type->toString()
|
|
|
|
);
|
|
|
|
else if (Identifier const* identifier = dynamic_cast<Identifier const*>(&_assignment.leftHandSide()))
|
|
|
|
{
|
2018-06-12 08:58:24 +00:00
|
|
|
VariableDeclaration const& decl = dynamic_cast<VariableDeclaration const&>(*identifier->annotation().referencedDeclaration);
|
|
|
|
if (knownVariable(decl))
|
2017-10-05 17:39:29 +00:00
|
|
|
{
|
2018-06-12 08:58:24 +00:00
|
|
|
assignment(decl, _assignment.rightHandSide(), _assignment.location());
|
2017-10-05 17:39:29 +00:00
|
|
|
defineExpr(_assignment, expr(_assignment.rightHandSide()));
|
|
|
|
}
|
2017-07-11 11:26:43 +00:00
|
|
|
else
|
|
|
|
m_errorReporter.warning(
|
|
|
|
_assignment.location(),
|
|
|
|
"Assertion checker does not yet implement such assignments."
|
|
|
|
);
|
|
|
|
}
|
|
|
|
else
|
|
|
|
m_errorReporter.warning(
|
|
|
|
_assignment.location(),
|
|
|
|
"Assertion checker does not yet implement such assignments."
|
|
|
|
);
|
|
|
|
}
|
|
|
|
|
|
|
|
void SMTChecker::endVisit(TupleExpression const& _tuple)
|
|
|
|
{
|
|
|
|
if (_tuple.isInlineArray() || _tuple.components().size() != 1)
|
|
|
|
m_errorReporter.warning(
|
|
|
|
_tuple.location(),
|
|
|
|
"Assertion checker does not yet implement tules and inline arrays."
|
|
|
|
);
|
|
|
|
else
|
2017-10-05 13:23:25 +00:00
|
|
|
defineExpr(_tuple, expr(*_tuple.components()[0]));
|
|
|
|
}
|
|
|
|
|
|
|
|
void SMTChecker::checkUnderOverflow(smt::Expression _value, IntegerType const& _type, SourceLocation const& _location)
|
|
|
|
{
|
|
|
|
checkCondition(
|
2018-02-17 08:34:38 +00:00
|
|
|
_value < SymbolicIntVariable::minValue(_type),
|
2017-10-05 13:23:25 +00:00
|
|
|
_location,
|
|
|
|
"Underflow (resulting value less than " + formatNumber(_type.minValue()) + ")",
|
2018-08-01 21:27:11 +00:00
|
|
|
"<result>",
|
2017-10-05 13:23:25 +00:00
|
|
|
&_value
|
|
|
|
);
|
|
|
|
checkCondition(
|
2018-02-17 08:34:38 +00:00
|
|
|
_value > SymbolicIntVariable::maxValue(_type),
|
2017-10-05 13:23:25 +00:00
|
|
|
_location,
|
|
|
|
"Overflow (resulting value larger than " + formatNumber(_type.maxValue()) + ")",
|
2018-08-01 21:27:11 +00:00
|
|
|
"<result>",
|
2017-10-05 13:23:25 +00:00
|
|
|
&_value
|
|
|
|
);
|
|
|
|
}
|
|
|
|
|
|
|
|
void SMTChecker::endVisit(UnaryOperation const& _op)
|
|
|
|
{
|
|
|
|
switch (_op.getOperator())
|
|
|
|
{
|
|
|
|
case Token::Not: // !
|
|
|
|
{
|
2018-03-12 19:15:27 +00:00
|
|
|
solAssert(SSAVariable::isBool(_op.annotation().type->category()), "");
|
2017-10-05 13:23:25 +00:00
|
|
|
defineExpr(_op, !expr(_op.subExpression()));
|
|
|
|
break;
|
|
|
|
}
|
|
|
|
case Token::Inc: // ++ (pre- or postfix)
|
|
|
|
case Token::Dec: // -- (pre- or postfix)
|
|
|
|
{
|
2018-03-09 15:19:03 +00:00
|
|
|
|
2018-03-12 19:15:27 +00:00
|
|
|
solAssert(SSAVariable::isInteger(_op.annotation().type->category()), "");
|
2017-10-05 13:23:25 +00:00
|
|
|
solAssert(_op.subExpression().annotation().lValueRequested, "");
|
|
|
|
if (Identifier const* identifier = dynamic_cast<Identifier const*>(&_op.subExpression()))
|
|
|
|
{
|
2018-06-12 08:58:24 +00:00
|
|
|
VariableDeclaration const& decl = dynamic_cast<VariableDeclaration const&>(*identifier->annotation().referencedDeclaration);
|
|
|
|
if (knownVariable(decl))
|
2017-10-05 13:23:25 +00:00
|
|
|
{
|
2018-06-12 08:58:24 +00:00
|
|
|
auto innerValue = currentValue(decl);
|
2017-10-05 13:23:25 +00:00
|
|
|
auto newValue = _op.getOperator() == Token::Inc ? innerValue + 1 : innerValue - 1;
|
2018-06-12 08:58:24 +00:00
|
|
|
assignment(decl, newValue, _op.location());
|
2017-10-05 13:23:25 +00:00
|
|
|
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."
|
|
|
|
);
|
|
|
|
}
|
2017-07-11 11:26:43 +00:00
|
|
|
}
|
|
|
|
|
|
|
|
void SMTChecker::endVisit(BinaryOperation const& _op)
|
|
|
|
{
|
|
|
|
if (Token::isArithmeticOp(_op.getOperator()))
|
|
|
|
arithmeticOperation(_op);
|
|
|
|
else if (Token::isCompareOp(_op.getOperator()))
|
|
|
|
compareOperation(_op);
|
|
|
|
else if (Token::isBooleanOp(_op.getOperator()))
|
|
|
|
booleanOperation(_op);
|
|
|
|
else
|
|
|
|
m_errorReporter.warning(
|
|
|
|
_op.location(),
|
|
|
|
"Assertion checker does not yet implement this operator."
|
|
|
|
);
|
|
|
|
}
|
|
|
|
|
|
|
|
void SMTChecker::endVisit(FunctionCall const& _funCall)
|
|
|
|
{
|
2017-10-04 11:18:40 +00:00
|
|
|
solAssert(_funCall.annotation().kind != FunctionCallKind::Unset, "");
|
|
|
|
if (_funCall.annotation().kind != FunctionCallKind::FunctionCall)
|
|
|
|
{
|
|
|
|
m_errorReporter.warning(
|
|
|
|
_funCall.location(),
|
|
|
|
"Assertion checker does not yet implement this expression."
|
|
|
|
);
|
|
|
|
return;
|
|
|
|
}
|
|
|
|
|
2017-07-11 11:26:43 +00:00
|
|
|
FunctionType const& funType = dynamic_cast<FunctionType const&>(*_funCall.expression().annotation().type);
|
|
|
|
|
|
|
|
std::vector<ASTPointer<Expression const>> const args = _funCall.arguments();
|
|
|
|
if (funType.kind() == FunctionType::Kind::Assert)
|
|
|
|
{
|
|
|
|
solAssert(args.size() == 1, "");
|
|
|
|
solAssert(args[0]->annotation().type->category() == Type::Category::Bool, "");
|
|
|
|
checkCondition(!(expr(*args[0])), _funCall.location(), "Assertion violation");
|
2017-12-13 16:59:36 +00:00
|
|
|
addPathImpliedExpression(expr(*args[0]));
|
2017-07-11 11:26:43 +00:00
|
|
|
}
|
|
|
|
else if (funType.kind() == FunctionType::Kind::Require)
|
|
|
|
{
|
|
|
|
solAssert(args.size() == 1, "");
|
|
|
|
solAssert(args[0]->annotation().type->category() == Type::Category::Bool, "");
|
2017-10-05 13:23:25 +00:00
|
|
|
checkBooleanNotConstant(*args[0], "Condition is always $VALUE.");
|
2017-12-13 16:59:36 +00:00
|
|
|
addPathImpliedExpression(expr(*args[0]));
|
2017-07-11 11:26:43 +00:00
|
|
|
}
|
|
|
|
}
|
|
|
|
|
|
|
|
void SMTChecker::endVisit(Identifier const& _identifier)
|
|
|
|
{
|
2017-09-28 13:24:24 +00:00
|
|
|
if (_identifier.annotation().lValueRequested)
|
2017-07-11 11:26:43 +00:00
|
|
|
{
|
2017-09-28 13:24:24 +00:00
|
|
|
// Will be translated as part of the node that requested the lvalue.
|
2017-07-11 11:26:43 +00:00
|
|
|
}
|
2018-03-12 19:15:27 +00:00
|
|
|
else if (SSAVariable::isSupportedType(_identifier.annotation().type->category()))
|
2018-06-12 08:58:24 +00:00
|
|
|
{
|
2018-08-07 19:43:20 +00:00
|
|
|
if (VariableDeclaration const* decl = dynamic_cast<VariableDeclaration const*>(_identifier.annotation().referencedDeclaration))
|
|
|
|
defineExpr(_identifier, currentValue(*decl));
|
|
|
|
else
|
|
|
|
// TODO: handle MagicVariableDeclaration here
|
|
|
|
m_errorReporter.warning(
|
|
|
|
_identifier.location(),
|
|
|
|
"Assertion checker does not yet support the type of this variable."
|
|
|
|
);
|
2018-06-12 08:58:24 +00:00
|
|
|
}
|
2017-07-11 11:26:43 +00:00
|
|
|
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;
|
|
|
|
}
|
|
|
|
}
|
|
|
|
|
|
|
|
void SMTChecker::endVisit(Literal const& _literal)
|
|
|
|
{
|
|
|
|
Type const& type = *_literal.annotation().type;
|
2018-09-03 15:45:58 +00:00
|
|
|
if (type.category() == Type::Category::Integer || type.category() == Type::Category::Address || type.category() == Type::Category::RationalNumber)
|
2017-07-11 11:26:43 +00:00
|
|
|
{
|
|
|
|
if (RationalNumberType const* rational = dynamic_cast<RationalNumberType const*>(&type))
|
|
|
|
solAssert(!rational->isFractional(), "");
|
|
|
|
|
2017-10-05 13:23:25 +00:00
|
|
|
defineExpr(_literal, smt::Expression(type.literalValue(&_literal)));
|
2017-07-11 11:26:43 +00:00
|
|
|
}
|
2017-09-29 14:53:26 +00:00
|
|
|
else if (type.category() == Type::Category::Bool)
|
2017-10-05 13:23:25 +00:00
|
|
|
defineExpr(_literal, smt::Expression(_literal.token() == Token::TrueLiteral ? true : false));
|
2017-07-11 11:26:43 +00:00
|
|
|
else
|
|
|
|
m_errorReporter.warning(
|
|
|
|
_literal.location(),
|
2017-09-28 13:24:24 +00:00
|
|
|
"Assertion checker does not yet support the type of this literal (" +
|
2017-07-11 11:26:43 +00:00
|
|
|
_literal.annotation().type->toString() +
|
|
|
|
")."
|
|
|
|
);
|
|
|
|
}
|
|
|
|
|
|
|
|
void SMTChecker::arithmeticOperation(BinaryOperation const& _op)
|
|
|
|
{
|
|
|
|
switch (_op.getOperator())
|
|
|
|
{
|
|
|
|
case Token::Add:
|
|
|
|
case Token::Sub:
|
|
|
|
case Token::Mul:
|
2017-10-05 13:23:25 +00:00
|
|
|
case Token::Div:
|
2017-07-11 11:26:43 +00:00
|
|
|
{
|
|
|
|
solAssert(_op.annotation().commonType, "");
|
2018-07-24 22:23:54 +00:00
|
|
|
if (_op.annotation().commonType->category() != Type::Category::Integer)
|
|
|
|
{
|
|
|
|
m_errorReporter.warning(
|
|
|
|
_op.location(),
|
|
|
|
"Assertion checker does not yet implement this operator on non-integer types."
|
|
|
|
);
|
|
|
|
break;
|
|
|
|
}
|
2017-10-05 17:20:46 +00:00
|
|
|
auto const& intType = dynamic_cast<IntegerType const&>(*_op.annotation().commonType);
|
2017-07-11 11:26:43 +00:00
|
|
|
smt::Expression left(expr(_op.leftExpression()));
|
|
|
|
smt::Expression right(expr(_op.rightExpression()));
|
|
|
|
Token::Value op = _op.getOperator();
|
|
|
|
smt::Expression value(
|
|
|
|
op == Token::Add ? left + right :
|
|
|
|
op == Token::Sub ? left - right :
|
2017-10-05 17:20:46 +00:00
|
|
|
op == Token::Div ? division(left, right, intType) :
|
2017-07-11 11:26:43 +00:00
|
|
|
/*op == Token::Mul*/ left * right
|
|
|
|
);
|
|
|
|
|
2017-10-05 13:23:25 +00:00
|
|
|
if (_op.getOperator() == Token::Div)
|
|
|
|
{
|
2018-08-01 21:27:11 +00:00
|
|
|
checkCondition(right == 0, _op.location(), "Division by zero", "<result>", &right);
|
2017-10-05 13:23:25 +00:00
|
|
|
m_interface->addAssertion(right != 0);
|
|
|
|
}
|
|
|
|
|
2017-10-05 17:20:46 +00:00
|
|
|
checkUnderOverflow(value, intType, _op.location());
|
2017-07-11 11:26:43 +00:00
|
|
|
|
2017-10-05 13:23:25 +00:00
|
|
|
defineExpr(_op, value);
|
2017-07-11 11:26:43 +00:00
|
|
|
break;
|
|
|
|
}
|
|
|
|
default:
|
|
|
|
m_errorReporter.warning(
|
|
|
|
_op.location(),
|
|
|
|
"Assertion checker does not yet implement this operator."
|
|
|
|
);
|
|
|
|
}
|
|
|
|
}
|
|
|
|
|
|
|
|
void SMTChecker::compareOperation(BinaryOperation const& _op)
|
|
|
|
{
|
|
|
|
solAssert(_op.annotation().commonType, "");
|
2018-03-12 19:15:27 +00:00
|
|
|
if (SSAVariable::isSupportedType(_op.annotation().commonType->category()))
|
2017-07-11 11:26:43 +00:00
|
|
|
{
|
|
|
|
smt::Expression left(expr(_op.leftExpression()));
|
|
|
|
smt::Expression right(expr(_op.rightExpression()));
|
|
|
|
Token::Value op = _op.getOperator();
|
2018-03-09 15:19:03 +00:00
|
|
|
shared_ptr<smt::Expression> value;
|
2018-03-12 19:15:27 +00:00
|
|
|
if (SSAVariable::isInteger(_op.annotation().commonType->category()))
|
2018-03-09 15:19:03 +00:00
|
|
|
{
|
|
|
|
value = make_shared<smt::Expression>(
|
|
|
|
op == Token::Equal ? (left == right) :
|
|
|
|
op == Token::NotEqual ? (left != right) :
|
|
|
|
op == Token::LessThan ? (left < right) :
|
|
|
|
op == Token::LessThanOrEqual ? (left <= right) :
|
|
|
|
op == Token::GreaterThan ? (left > right) :
|
|
|
|
/*op == Token::GreaterThanOrEqual*/ (left >= right)
|
|
|
|
);
|
|
|
|
}
|
|
|
|
else // Bool
|
|
|
|
{
|
2018-04-18 10:52:04 +00:00
|
|
|
solUnimplementedAssert(SSAVariable::isBool(_op.annotation().commonType->category()), "Operation not yet supported");
|
2018-03-09 15:19:03 +00:00
|
|
|
value = make_shared<smt::Expression>(
|
|
|
|
op == Token::Equal ? (left == right) :
|
2018-04-27 09:35:58 +00:00
|
|
|
/*op == Token::NotEqual*/ (left != right)
|
2018-03-09 15:19:03 +00:00
|
|
|
);
|
|
|
|
}
|
2017-07-11 11:26:43 +00:00
|
|
|
// TODO: check that other values for op are not possible.
|
2018-03-09 15:19:03 +00:00
|
|
|
defineExpr(_op, *value);
|
2017-07-11 11:26:43 +00:00
|
|
|
}
|
|
|
|
else
|
|
|
|
m_errorReporter.warning(
|
|
|
|
_op.location(),
|
|
|
|
"Assertion checker does not yet implement the type " + _op.annotation().commonType->toString() + " for comparisons"
|
|
|
|
);
|
|
|
|
}
|
|
|
|
|
|
|
|
void SMTChecker::booleanOperation(BinaryOperation const& _op)
|
|
|
|
{
|
|
|
|
solAssert(_op.getOperator() == Token::And || _op.getOperator() == Token::Or, "");
|
|
|
|
solAssert(_op.annotation().commonType, "");
|
|
|
|
if (_op.annotation().commonType->category() == Type::Category::Bool)
|
|
|
|
{
|
2017-09-28 11:44:56 +00:00
|
|
|
// @TODO check that both of them are not constant
|
2017-07-11 11:26:43 +00:00
|
|
|
if (_op.getOperator() == Token::And)
|
2017-10-05 13:23:25 +00:00
|
|
|
defineExpr(_op, expr(_op.leftExpression()) && expr(_op.rightExpression()));
|
2017-07-11 11:26:43 +00:00
|
|
|
else
|
2017-10-05 13:23:25 +00:00
|
|
|
defineExpr(_op, expr(_op.leftExpression()) || expr(_op.rightExpression()));
|
2017-07-11 11:26:43 +00:00
|
|
|
}
|
|
|
|
else
|
|
|
|
m_errorReporter.warning(
|
|
|
|
_op.location(),
|
|
|
|
"Assertion checker does not yet implement the type " + _op.annotation().commonType->toString() + " for boolean operations"
|
2017-09-28 11:44:56 +00:00
|
|
|
);
|
|
|
|
}
|
|
|
|
|
2017-10-05 17:20:46 +00:00
|
|
|
smt::Expression SMTChecker::division(smt::Expression _left, smt::Expression _right, IntegerType const& _type)
|
|
|
|
{
|
|
|
|
// Signed division in SMTLIB2 rounds differently for negative division.
|
|
|
|
if (_type.isSigned())
|
|
|
|
return (smt::Expression::ite(
|
|
|
|
_left >= 0,
|
|
|
|
smt::Expression::ite(_right >= 0, _left / _right, 0 - (_left / (0 - _right))),
|
|
|
|
smt::Expression::ite(_right >= 0, 0 - ((0 - _left) / _right), (0 - _left) / (0 - _right))
|
|
|
|
));
|
|
|
|
else
|
|
|
|
return _left / _right;
|
|
|
|
}
|
|
|
|
|
2018-06-12 08:58:24 +00:00
|
|
|
void SMTChecker::assignment(VariableDeclaration const& _variable, Expression const& _value, SourceLocation const& _location)
|
2017-09-28 11:44:56 +00:00
|
|
|
{
|
2017-10-05 13:23:25 +00:00
|
|
|
assignment(_variable, expr(_value), _location);
|
|
|
|
}
|
|
|
|
|
2018-06-12 08:58:24 +00:00
|
|
|
void SMTChecker::assignment(VariableDeclaration const& _variable, smt::Expression const& _value, SourceLocation const& _location)
|
2017-10-05 13:23:25 +00:00
|
|
|
{
|
|
|
|
TypePointer type = _variable.type();
|
|
|
|
if (auto const* intType = dynamic_cast<IntegerType const*>(type.get()))
|
|
|
|
checkUnderOverflow(_value, *intType, _location);
|
2018-09-03 15:45:58 +00:00
|
|
|
else if (dynamic_cast<AddressType const*>(type.get()))
|
|
|
|
checkUnderOverflow(_value, IntegerType(160), _location);
|
2017-10-05 13:23:25 +00:00
|
|
|
m_interface->addAssertion(newValue(_variable) == _value);
|
2017-09-28 11:44:56 +00:00
|
|
|
}
|
|
|
|
|
2017-12-18 18:43:15 +00:00
|
|
|
SMTChecker::VariableSequenceCounters SMTChecker::visitBranch(Statement const& _statement, smt::Expression _condition)
|
2017-09-28 13:24:24 +00:00
|
|
|
{
|
2017-12-18 18:43:15 +00:00
|
|
|
return visitBranch(_statement, &_condition);
|
2017-09-28 13:24:24 +00:00
|
|
|
}
|
|
|
|
|
2017-12-18 18:43:15 +00:00
|
|
|
SMTChecker::VariableSequenceCounters SMTChecker::visitBranch(Statement const& _statement, smt::Expression const* _condition)
|
2017-09-28 11:44:56 +00:00
|
|
|
{
|
2018-01-17 20:02:23 +00:00
|
|
|
VariableSequenceCounters beforeVars = m_variables;
|
2017-09-28 11:44:56 +00:00
|
|
|
|
|
|
|
if (_condition)
|
2017-12-11 19:09:17 +00:00
|
|
|
pushPathCondition(*_condition);
|
2017-09-28 11:44:56 +00:00
|
|
|
_statement.accept(*this);
|
2017-12-11 19:09:17 +00:00
|
|
|
if (_condition)
|
|
|
|
popPathCondition();
|
2017-09-28 11:44:56 +00:00
|
|
|
|
2018-01-17 20:02:23 +00:00
|
|
|
std::swap(m_variables, beforeVars);
|
|
|
|
|
|
|
|
return beforeVars;
|
2017-07-11 11:26:43 +00:00
|
|
|
}
|
|
|
|
|
|
|
|
void SMTChecker::checkCondition(
|
|
|
|
smt::Expression _condition,
|
|
|
|
SourceLocation const& _location,
|
|
|
|
string const& _description,
|
|
|
|
string const& _additionalValueName,
|
|
|
|
smt::Expression* _additionalValue
|
|
|
|
)
|
|
|
|
{
|
2017-07-13 16:22:51 +00:00
|
|
|
m_interface->push();
|
2017-12-13 16:59:36 +00:00
|
|
|
addPathConjoinedExpression(_condition);
|
2017-07-11 11:26:43 +00:00
|
|
|
|
|
|
|
vector<smt::Expression> expressionsToEvaluate;
|
2017-07-13 20:07:01 +00:00
|
|
|
vector<string> expressionNames;
|
2017-07-11 11:26:43 +00:00
|
|
|
if (m_currentFunction)
|
|
|
|
{
|
|
|
|
if (_additionalValue)
|
2017-07-13 20:07:01 +00:00
|
|
|
{
|
2017-07-11 11:26:43 +00:00
|
|
|
expressionsToEvaluate.emplace_back(*_additionalValue);
|
2017-07-13 20:07:01 +00:00
|
|
|
expressionNames.push_back(_additionalValueName);
|
|
|
|
}
|
2018-06-05 09:46:21 +00:00
|
|
|
for (auto const& var: m_variables)
|
2018-04-18 21:14:45 +00:00
|
|
|
if (knownVariable(*var.first))
|
|
|
|
{
|
|
|
|
expressionsToEvaluate.emplace_back(currentValue(*var.first));
|
|
|
|
expressionNames.push_back(var.first->name());
|
|
|
|
}
|
2017-07-11 11:26:43 +00:00
|
|
|
}
|
|
|
|
smt::CheckResult result;
|
|
|
|
vector<string> values;
|
2017-12-18 16:31:27 +00:00
|
|
|
tie(result, values) = checkSatisfiableAndGenerateModel(expressionsToEvaluate);
|
2017-07-13 19:06:29 +00:00
|
|
|
|
2018-04-19 07:28:44 +00:00
|
|
|
string loopComment;
|
|
|
|
if (m_loopExecutionHappened)
|
|
|
|
loopComment =
|
|
|
|
"\nNote that some information is erased after the execution of loops.\n"
|
2017-09-28 11:44:56 +00:00
|
|
|
"You can re-introduce information using require().";
|
2017-07-11 11:26:43 +00:00
|
|
|
switch (result)
|
|
|
|
{
|
2017-08-21 15:02:47 +00:00
|
|
|
case smt::CheckResult::SATISFIABLE:
|
2017-07-11 11:26:43 +00:00
|
|
|
{
|
|
|
|
std::ostringstream message;
|
|
|
|
message << _description << " happens here";
|
|
|
|
if (m_currentFunction)
|
|
|
|
{
|
2018-08-01 21:27:46 +00:00
|
|
|
std::ostringstream modelMessage;
|
|
|
|
modelMessage << " for:\n";
|
2017-07-13 20:07:01 +00:00
|
|
|
solAssert(values.size() == expressionNames.size(), "");
|
2018-08-01 21:27:46 +00:00
|
|
|
map<string, string> sortedModel;
|
2017-07-13 20:07:01 +00:00
|
|
|
for (size_t i = 0; i < values.size(); ++i)
|
2018-04-18 21:14:45 +00:00
|
|
|
if (expressionsToEvaluate.at(i).name != values.at(i))
|
2018-08-01 21:27:46 +00:00
|
|
|
sortedModel[expressionNames.at(i)] = values.at(i);
|
|
|
|
|
|
|
|
for (auto const& eval: sortedModel)
|
|
|
|
modelMessage << " " << eval.first << " = " << eval.second << "\n";
|
|
|
|
m_errorReporter.warning(_location, message.str() + loopComment, SecondarySourceLocation().append(modelMessage.str(), SourceLocation()));
|
2017-07-11 11:26:43 +00:00
|
|
|
}
|
|
|
|
else
|
2018-08-01 21:27:46 +00:00
|
|
|
{
|
2017-07-11 11:26:43 +00:00
|
|
|
message << ".";
|
2018-08-01 21:27:46 +00:00
|
|
|
m_errorReporter.warning(_location, message.str() + loopComment);
|
|
|
|
}
|
2017-07-11 11:26:43 +00:00
|
|
|
break;
|
|
|
|
}
|
2017-08-21 15:02:47 +00:00
|
|
|
case smt::CheckResult::UNSATISFIABLE:
|
2017-07-11 11:26:43 +00:00
|
|
|
break;
|
|
|
|
case smt::CheckResult::UNKNOWN:
|
2018-04-19 07:28:44 +00:00
|
|
|
m_errorReporter.warning(_location, _description + " might happen here." + loopComment);
|
2017-07-11 11:26:43 +00:00
|
|
|
break;
|
2018-06-26 10:41:26 +00:00
|
|
|
case smt::CheckResult::CONFLICTING:
|
|
|
|
m_errorReporter.warning(_location, "At least two SMT solvers provided conflicting answers. Results might not be sound.");
|
|
|
|
break;
|
2017-07-11 11:26:43 +00:00
|
|
|
case smt::CheckResult::ERROR:
|
|
|
|
m_errorReporter.warning(_location, "Error trying to invoke SMT solver.");
|
|
|
|
break;
|
|
|
|
}
|
2017-07-13 16:22:51 +00:00
|
|
|
m_interface->pop();
|
2017-07-11 11:26:43 +00:00
|
|
|
}
|
|
|
|
|
2017-09-29 14:53:26 +00:00
|
|
|
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();
|
2017-12-13 16:59:36 +00:00
|
|
|
addPathConjoinedExpression(expr(_condition));
|
2017-12-18 16:31:27 +00:00
|
|
|
auto positiveResult = checkSatisfiable();
|
2017-09-29 14:53:26 +00:00
|
|
|
m_interface->pop();
|
|
|
|
|
|
|
|
m_interface->push();
|
2017-12-13 16:59:36 +00:00
|
|
|
addPathConjoinedExpression(!expr(_condition));
|
2017-12-18 16:31:27 +00:00
|
|
|
auto negatedResult = checkSatisfiable();
|
2017-09-29 14:53:26 +00:00
|
|
|
m_interface->pop();
|
|
|
|
|
|
|
|
if (positiveResult == smt::CheckResult::ERROR || negatedResult == smt::CheckResult::ERROR)
|
|
|
|
m_errorReporter.warning(_condition.location(), "Error trying to invoke SMT solver.");
|
2018-06-26 10:41:26 +00:00
|
|
|
else if (positiveResult == smt::CheckResult::CONFLICTING || negatedResult == smt::CheckResult::CONFLICTING)
|
|
|
|
m_errorReporter.warning(_condition.location(), "At least two SMT solvers provided conflicting answers. Results might not be sound.");
|
2017-09-29 14:53:26 +00:00
|
|
|
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>>
|
2017-12-18 16:31:27 +00:00
|
|
|
SMTChecker::checkSatisfiableAndGenerateModel(vector<smt::Expression> const& _expressionsToEvaluate)
|
2017-09-29 14:53:26 +00:00
|
|
|
{
|
|
|
|
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);
|
|
|
|
}
|
|
|
|
|
2017-12-18 16:31:27 +00:00
|
|
|
smt::CheckResult SMTChecker::checkSatisfiable()
|
2017-09-29 14:53:26 +00:00
|
|
|
{
|
2017-12-18 16:31:27 +00:00
|
|
|
return checkSatisfiableAndGenerateModel({}).first;
|
2017-09-29 14:53:26 +00:00
|
|
|
}
|
|
|
|
|
2017-09-28 13:24:24 +00:00
|
|
|
void SMTChecker::initializeLocalVariables(FunctionDefinition const& _function)
|
|
|
|
{
|
|
|
|
for (auto const& variable: _function.localVariables())
|
2017-10-05 17:31:17 +00:00
|
|
|
if (createVariable(*variable))
|
|
|
|
setZeroValue(*variable);
|
|
|
|
|
2017-09-28 13:24:24 +00:00
|
|
|
for (auto const& param: _function.parameters())
|
2017-10-05 17:31:17 +00:00
|
|
|
if (createVariable(*param))
|
|
|
|
setUnknownValue(*param);
|
|
|
|
|
2017-09-28 13:24:24 +00:00
|
|
|
if (_function.returnParameterList())
|
|
|
|
for (auto const& retParam: _function.returnParameters())
|
2017-10-05 17:31:17 +00:00
|
|
|
if (createVariable(*retParam))
|
|
|
|
setZeroValue(*retParam);
|
2017-09-28 13:24:24 +00:00
|
|
|
}
|
|
|
|
|
2018-04-18 21:14:45 +00:00
|
|
|
void SMTChecker::resetStateVariables()
|
|
|
|
{
|
2018-06-05 09:46:21 +00:00
|
|
|
for (auto const& variable: m_variables)
|
2018-04-18 21:14:45 +00:00
|
|
|
{
|
2018-06-12 08:58:24 +00:00
|
|
|
if (variable.first->isStateVariable())
|
2018-06-05 09:46:21 +00:00
|
|
|
{
|
|
|
|
newValue(*variable.first);
|
|
|
|
setUnknownValue(*variable.first);
|
|
|
|
}
|
2018-04-18 21:14:45 +00:00
|
|
|
}
|
|
|
|
}
|
|
|
|
|
2018-06-12 08:58:24 +00:00
|
|
|
void SMTChecker::resetVariables(vector<VariableDeclaration const*> _variables)
|
2017-09-28 11:44:56 +00:00
|
|
|
{
|
|
|
|
for (auto const* decl: _variables)
|
|
|
|
{
|
|
|
|
newValue(*decl);
|
2017-09-28 13:24:24 +00:00
|
|
|
setUnknownValue(*decl);
|
2017-09-28 11:44:56 +00:00
|
|
|
}
|
|
|
|
}
|
|
|
|
|
2018-06-12 08:58:24 +00:00
|
|
|
void SMTChecker::mergeVariables(vector<VariableDeclaration const*> const& _variables, smt::Expression const& _condition, VariableSequenceCounters const& _countersEndTrue, VariableSequenceCounters const& _countersEndFalse)
|
2017-12-18 18:43:15 +00:00
|
|
|
{
|
2018-06-12 08:58:24 +00:00
|
|
|
set<VariableDeclaration const*> uniqueVars(_variables.begin(), _variables.end());
|
2017-12-18 18:43:15 +00:00
|
|
|
for (auto const* decl: uniqueVars)
|
|
|
|
{
|
2018-07-24 21:43:05 +00:00
|
|
|
solAssert(_countersEndTrue.count(decl) && _countersEndFalse.count(decl), "");
|
2018-01-17 20:02:23 +00:00
|
|
|
int trueCounter = _countersEndTrue.at(decl).index();
|
|
|
|
int falseCounter = _countersEndFalse.at(decl).index();
|
2017-12-18 18:43:15 +00:00
|
|
|
solAssert(trueCounter != falseCounter, "");
|
|
|
|
m_interface->addAssertion(newValue(*decl) == smt::Expression::ite(
|
|
|
|
_condition,
|
|
|
|
valueAtSequence(*decl, trueCounter),
|
|
|
|
valueAtSequence(*decl, falseCounter))
|
|
|
|
);
|
|
|
|
}
|
|
|
|
}
|
|
|
|
|
2017-10-05 17:31:17 +00:00
|
|
|
bool SMTChecker::createVariable(VariableDeclaration const& _varDecl)
|
2017-07-11 11:26:43 +00:00
|
|
|
{
|
2018-03-12 19:15:27 +00:00
|
|
|
if (SSAVariable::isSupportedType(_varDecl.type()->category()))
|
2017-07-11 11:26:43 +00:00
|
|
|
{
|
2017-09-28 09:29:04 +00:00
|
|
|
solAssert(m_variables.count(&_varDecl) == 0, "");
|
2018-06-05 09:46:21 +00:00
|
|
|
m_variables.emplace(&_varDecl, SSAVariable(_varDecl, *m_interface));
|
2017-10-05 17:31:17 +00:00
|
|
|
return true;
|
2017-07-11 11:26:43 +00:00
|
|
|
}
|
|
|
|
else
|
2017-10-05 17:31:17 +00:00
|
|
|
{
|
2017-07-11 11:26:43 +00:00
|
|
|
m_errorReporter.warning(
|
|
|
|
_varDecl.location(),
|
|
|
|
"Assertion checker does not yet support the type of this variable."
|
|
|
|
);
|
2017-10-05 17:31:17 +00:00
|
|
|
return false;
|
|
|
|
}
|
2017-07-11 11:26:43 +00:00
|
|
|
}
|
|
|
|
|
|
|
|
string SMTChecker::uniqueSymbol(Expression const& _expr)
|
|
|
|
{
|
|
|
|
return "expr_" + to_string(_expr.id());
|
|
|
|
}
|
|
|
|
|
2018-06-12 08:58:24 +00:00
|
|
|
bool SMTChecker::knownVariable(VariableDeclaration const& _decl)
|
2017-07-11 11:26:43 +00:00
|
|
|
{
|
2018-01-17 20:02:23 +00:00
|
|
|
return m_variables.count(&_decl);
|
2017-07-11 11:26:43 +00:00
|
|
|
}
|
|
|
|
|
2018-06-12 08:58:24 +00:00
|
|
|
smt::Expression SMTChecker::currentValue(VariableDeclaration const& _decl)
|
2017-07-11 11:26:43 +00:00
|
|
|
{
|
2018-01-17 20:02:23 +00:00
|
|
|
solAssert(knownVariable(_decl), "");
|
|
|
|
return m_variables.at(&_decl)();
|
2017-07-11 11:26:43 +00:00
|
|
|
}
|
|
|
|
|
2018-06-12 08:58:24 +00:00
|
|
|
smt::Expression SMTChecker::valueAtSequence(VariableDeclaration const& _decl, int _sequence)
|
2017-07-14 09:49:27 +00:00
|
|
|
{
|
2018-01-17 20:02:23 +00:00
|
|
|
solAssert(knownVariable(_decl), "");
|
|
|
|
return m_variables.at(&_decl)(_sequence);
|
2017-07-14 09:49:27 +00:00
|
|
|
}
|
|
|
|
|
2018-06-12 08:58:24 +00:00
|
|
|
smt::Expression SMTChecker::newValue(VariableDeclaration const& _decl)
|
2017-07-11 11:26:43 +00:00
|
|
|
{
|
2018-01-17 20:02:23 +00:00
|
|
|
solAssert(knownVariable(_decl), "");
|
|
|
|
++m_variables.at(&_decl);
|
|
|
|
return m_variables.at(&_decl)();
|
2017-07-11 11:26:43 +00:00
|
|
|
}
|
|
|
|
|
2018-06-12 08:58:24 +00:00
|
|
|
void SMTChecker::setZeroValue(VariableDeclaration const& _decl)
|
2017-07-14 09:49:27 +00:00
|
|
|
{
|
2018-01-17 20:02:23 +00:00
|
|
|
solAssert(knownVariable(_decl), "");
|
|
|
|
m_variables.at(&_decl).setZeroValue();
|
2017-09-28 13:24:24 +00:00
|
|
|
}
|
2017-07-14 09:49:27 +00:00
|
|
|
|
2018-06-12 08:58:24 +00:00
|
|
|
void SMTChecker::setUnknownValue(VariableDeclaration const& _decl)
|
2017-09-28 13:24:24 +00:00
|
|
|
{
|
2018-01-17 20:02:23 +00:00
|
|
|
solAssert(knownVariable(_decl), "");
|
|
|
|
m_variables.at(&_decl).setUnknownValue();
|
2017-07-11 11:26:43 +00:00
|
|
|
}
|
|
|
|
|
|
|
|
smt::Expression SMTChecker::expr(Expression const& _e)
|
|
|
|
{
|
2017-10-05 17:39:29 +00:00
|
|
|
if (!m_expressions.count(&_e))
|
|
|
|
{
|
|
|
|
m_errorReporter.warning(_e.location(), "Internal error: Expression undefined for SMT solver." );
|
|
|
|
createExpr(_e);
|
|
|
|
}
|
2017-10-05 13:23:25 +00:00
|
|
|
return m_expressions.at(&_e);
|
|
|
|
}
|
|
|
|
|
|
|
|
void SMTChecker::createExpr(Expression const& _e)
|
|
|
|
{
|
2017-10-05 17:39:29 +00:00
|
|
|
if (m_expressions.count(&_e))
|
|
|
|
m_errorReporter.warning(_e.location(), "Internal error: Expression created twice in SMT solver." );
|
|
|
|
else
|
2017-10-05 13:23:25 +00:00
|
|
|
{
|
2017-10-05 17:39:29 +00:00
|
|
|
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;
|
|
|
|
}
|
2018-09-03 15:45:58 +00:00
|
|
|
case Type::Category::Address:
|
2017-10-05 17:39:29 +00:00
|
|
|
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:
|
2018-04-18 10:52:04 +00:00
|
|
|
solUnimplementedAssert(false, "Type not implemented.");
|
2017-10-05 17:39:29 +00:00
|
|
|
}
|
2017-10-05 13:23:25 +00:00
|
|
|
}
|
|
|
|
}
|
|
|
|
|
|
|
|
void SMTChecker::defineExpr(Expression const& _e, smt::Expression _value)
|
|
|
|
{
|
|
|
|
createExpr(_e);
|
|
|
|
m_interface->addAssertion(expr(_e) == _value);
|
2017-07-11 11:26:43 +00:00
|
|
|
}
|
|
|
|
|
2017-12-11 19:09:17 +00:00
|
|
|
void SMTChecker::popPathCondition()
|
|
|
|
{
|
|
|
|
solAssert(m_pathConditions.size() > 0, "Cannot pop path condition, empty.");
|
|
|
|
m_pathConditions.pop_back();
|
|
|
|
}
|
|
|
|
|
|
|
|
void SMTChecker::pushPathCondition(smt::Expression const& _e)
|
|
|
|
{
|
|
|
|
m_pathConditions.push_back(currentPathConditions() && _e);
|
|
|
|
}
|
|
|
|
|
|
|
|
smt::Expression SMTChecker::currentPathConditions()
|
|
|
|
{
|
|
|
|
if (m_pathConditions.size() == 0)
|
|
|
|
return smt::Expression(true);
|
|
|
|
return m_pathConditions.back();
|
|
|
|
}
|
2017-12-13 16:59:36 +00:00
|
|
|
|
|
|
|
void SMTChecker::addPathConjoinedExpression(smt::Expression const& _e)
|
|
|
|
{
|
|
|
|
m_interface->addAssertion(currentPathConditions() && _e);
|
|
|
|
}
|
|
|
|
|
|
|
|
void SMTChecker::addPathImpliedExpression(smt::Expression const& _e)
|
|
|
|
{
|
|
|
|
m_interface->addAssertion(smt::Expression::implies(currentPathConditions(), _e));
|
|
|
|
}
|
2018-06-05 09:46:21 +00:00
|
|
|
|
2018-06-06 10:11:58 +00:00
|
|
|
void SMTChecker::removeLocalVariables()
|
2018-06-05 09:46:21 +00:00
|
|
|
{
|
|
|
|
for (auto it = m_variables.begin(); it != m_variables.end(); )
|
|
|
|
{
|
2018-06-12 08:58:24 +00:00
|
|
|
if (it->first->isLocalVariable())
|
2018-06-05 09:46:21 +00:00
|
|
|
it = m_variables.erase(it);
|
|
|
|
else
|
|
|
|
++it;
|
|
|
|
}
|
|
|
|
}
|