aboutsummaryrefslogtreecommitdiffstats
path: root/libsolidity/formal
diff options
context:
space:
mode:
Diffstat (limited to 'libsolidity/formal')
-rw-r--r--libsolidity/formal/SMTChecker.cpp588
-rw-r--r--libsolidity/formal/SMTChecker.h114
-rw-r--r--libsolidity/formal/SMTLib2Interface.cpp187
-rw-r--r--libsolidity/formal/SMTLib2Interface.h75
-rw-r--r--libsolidity/formal/SolverInterface.h178
-rw-r--r--libsolidity/formal/Z3Interface.cpp189
-rw-r--r--libsolidity/formal/Z3Interface.h65
7 files changed, 1396 insertions, 0 deletions
diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp
new file mode 100644
index 00000000..fd78e578
--- /dev/null
+++ b/libsolidity/formal/SMTChecker.cpp
@@ -0,0 +1,588 @@
+/*
+ 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>
+
+#ifdef HAVE_Z3
+#include <libsolidity/formal/Z3Interface.h>
+#else
+#include <libsolidity/formal/SMTLib2Interface.h>
+#endif
+
+#include <libsolidity/interface/ErrorReporter.h>
+
+#include <boost/range/adaptor/map.hpp>
+
+using namespace std;
+using namespace dev;
+using namespace dev::solidity;
+
+SMTChecker::SMTChecker(ErrorReporter& _errorReporter, ReadCallback::Callback const& _readFileCallback):
+#ifdef HAVE_Z3
+ m_interface(make_shared<smt::Z3Interface>()),
+#else
+ m_interface(make_shared<smt::SMTLib2Interface>(_readFileCallback)),
+#endif
+ m_errorReporter(_errorReporter)
+{
+ (void)_readFileCallback;
+}
+
+void SMTChecker::analyze(SourceUnit const& _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);
+}
+
+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."
+ );
+ // TODO actually we probably also have to reset all local variables and similar things.
+ m_currentFunction = &_function;
+ m_interface->push();
+ 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.
+ // If we add storage variables, those should be cleared differently.
+ m_currentSequenceCounter.clear();
+ m_nextFreeSequenceCounter.clear();
+ m_interface->pop();
+ m_currentFunction = nullptr;
+}
+
+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();
+
+ decltype(m_currentSequenceCounter) countersAtEndOfFalse;
+ 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();
+ }
+ else
+ countersAtEndOfFalse = countersAtStart;
+
+ // Reset all values that have been touched.
+
+ // TODO this should use a previously generated side-effect structure
+
+ solAssert(countersAtEndOfFalse.size() == countersAtEndOfTrue.size(), "");
+ for (auto const& declCounter: countersAtEndOfTrue)
+ {
+ 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);
+ }
+ return false;
+}
+
+bool SMTChecker::visit(WhileStatement const& _node)
+{
+ _node.condition().accept(*this);
+
+ //m_interface->push();
+ //m_interface->addAssertion(expr(_node.condition()));
+ // TDOO clear knowledge (increment sequence numbers and add bounds assertions ) apart from assertions
+
+ // TODO combine similar to if
+ return true;
+}
+
+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."
+ );
+ else if (knownVariable(*_varDecl.declarations()[0]))
+ {
+ 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()));
+ }
+ 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."
+ );
+ else if (_assignment.annotation().type->category() != Type::Category::Integer)
+ 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()))
+ {
+ 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()));
+ 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
+ m_interface->addAssertion(expr(_tuple) == expr(*_tuple.components()[0]));
+}
+
+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)
+{
+ 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");
+ m_interface->addAssertion(expr(*args[0]));
+ }
+ else if (funType.kind() == FunctionType::Kind::Require)
+ {
+ solAssert(args.size() == 1, "");
+ solAssert(args[0]->annotation().type->category() == Type::Category::Bool, "");
+ 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.
+ }
+}
+
+void SMTChecker::endVisit(Identifier const& _identifier)
+{
+ Declaration const* decl = _identifier.annotation().referencedDeclaration;
+ solAssert(decl, "");
+ if (dynamic_cast<IntegerType const*>(_identifier.annotation().type.get()))
+ {
+ m_interface->addAssertion(expr(_identifier) == currentValue(*decl));
+ return;
+ }
+ 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)
+{
+ Type const& type = *_literal.annotation().type;
+ if (type.category() == Type::Category::Integer || type.category() == Type::Category::RationalNumber)
+ {
+ if (RationalNumberType const* rational = dynamic_cast<RationalNumberType const*>(&type))
+ solAssert(!rational->isFractional(), "");
+
+ m_interface->addAssertion(expr(_literal) == smt::Expression(type.literalValue(&_literal)));
+ }
+ else
+ m_errorReporter.warning(
+ _literal.location(),
+ "Assertion checker does not yet support the type of this expression (" +
+ _literal.annotation().type->toString() +
+ ")."
+ );
+}
+
+void SMTChecker::arithmeticOperation(BinaryOperation const& _op)
+{
+ switch (_op.getOperator())
+ {
+ case Token::Add:
+ case Token::Sub:
+ case Token::Mul:
+ {
+ solAssert(_op.annotation().commonType, "");
+ solAssert(_op.annotation().commonType->category() == Type::Category::Integer, "");
+ 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 :
+ /*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
+ );
+
+ m_interface->addAssertion(expr(_op) == value);
+ 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, "");
+ if (_op.annotation().commonType->category() == Type::Category::Integer)
+ {
+ smt::Expression left(expr(_op.leftExpression()));
+ smt::Expression right(expr(_op.rightExpression()));
+ Token::Value op = _op.getOperator();
+ smt::Expression value = (
+ 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)
+ );
+ // TODO: check that other values for op are not possible.
+ m_interface->addAssertion(expr(_op) == value);
+ }
+ 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)
+ {
+ if (_op.getOperator() == Token::And)
+ m_interface->addAssertion(expr(_op) == expr(_op.leftExpression()) && expr(_op.rightExpression()));
+ else
+ m_interface->addAssertion(expr(_op) == expr(_op.leftExpression()) || expr(_op.rightExpression()));
+ }
+ else
+ m_errorReporter.warning(
+ _op.location(),
+ "Assertion checker does not yet implement the type " + _op.annotation().commonType->toString() + " for boolean operations"
+ );
+}
+
+void SMTChecker::checkCondition(
+ smt::Expression _condition,
+ SourceLocation const& _location,
+ string const& _description,
+ string const& _additionalValueName,
+ smt::Expression* _additionalValue
+)
+{
+ m_interface->push();
+ m_interface->addAssertion(_condition);
+
+ vector<smt::Expression> expressionsToEvaluate;
+ vector<string> expressionNames;
+ if (m_currentFunction)
+ {
+ if (_additionalValue)
+ {
+ expressionsToEvaluate.emplace_back(*_additionalValue);
+ expressionNames.push_back(_additionalValueName);
+ }
+ for (auto const& param: m_currentFunction->parameters())
+ if (knownVariable(*param))
+ {
+ expressionsToEvaluate.emplace_back(currentValue(*param));
+ expressionNames.push_back(param->name());
+ }
+ for (auto const& var: m_currentFunction->localVariables())
+ if (knownVariable(*var))
+ {
+ expressionsToEvaluate.emplace_back(currentValue(*var));
+ expressionNames.push_back(var->name());
+ }
+ }
+ 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;
+ }
+
+ switch (result)
+ {
+ case smt::CheckResult::SATISFIABLE:
+ {
+ std::ostringstream message;
+ message << _description << " happens here";
+ if (m_currentFunction)
+ {
+ 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";
+ }
+ }
+ else
+ message << ".";
+ m_errorReporter.warning(_location, message.str());
+ break;
+ }
+ case smt::CheckResult::UNSATISFIABLE:
+ break;
+ case smt::CheckResult::UNKNOWN:
+ m_errorReporter.warning(_location, _description + " might happen here.");
+ break;
+ case smt::CheckResult::ERROR:
+ m_errorReporter.warning(_location, "Error trying to invoke SMT solver.");
+ break;
+ default:
+ solAssert(false, "");
+ }
+ m_interface->pop();
+}
+
+void SMTChecker::createVariable(VariableDeclaration const& _varDecl, bool _setToZero)
+{
+ if (dynamic_cast<IntegerType const*>(_varDecl.type().get()))
+ {
+ solAssert(m_currentSequenceCounter.count(&_varDecl) == 0, "");
+ solAssert(m_nextFreeSequenceCounter.count(&_varDecl) == 0, "");
+ solAssert(m_Variables.count(&_varDecl) == 0, "");
+ 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);
+ }
+ else
+ m_errorReporter.warning(
+ _varDecl.location(),
+ "Assertion checker does not yet support the type of this variable."
+ );
+}
+
+string SMTChecker::uniqueSymbol(Declaration const& _decl)
+{
+ return _decl.name() + "_" + to_string(_decl.id());
+}
+
+string SMTChecker::uniqueSymbol(Expression const& _expr)
+{
+ return "expr_" + to_string(_expr.id());
+}
+
+bool SMTChecker::knownVariable(Declaration const& _decl)
+{
+ return m_currentSequenceCounter.count(&_decl);
+}
+
+smt::Expression SMTChecker::currentValue(Declaration const& _decl)
+{
+ solAssert(m_currentSequenceCounter.count(&_decl), "");
+ return valueAtSequence(_decl, m_currentSequenceCounter.at(&_decl));
+}
+
+smt::Expression SMTChecker::valueAtSequence(const Declaration& _decl, int _sequence)
+{
+ return var(_decl)(_sequence);
+}
+
+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)
+{
+ auto const& intType = dynamic_cast<IntegerType const&>(*_decl.type());
+
+ if (_setToZero)
+ m_interface->addAssertion(currentValue(_decl) == 0);
+ else
+ {
+ m_interface->addAssertion(currentValue(_decl) >= minValue(intType));
+ m_interface->addAssertion(currentValue(_decl) <= maxValue(intType));
+ }
+}
+
+smt::Expression SMTChecker::minValue(IntegerType const& _t)
+{
+ return smt::Expression(_t.minValue());
+}
+
+smt::Expression SMTChecker::maxValue(IntegerType const& _t)
+{
+ return smt::Expression(_t.maxValue());
+}
+
+smt::Expression SMTChecker::expr(Expression const& _e)
+{
+ if (!m_Expressions.count(&_e))
+ {
+ 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.");
+ }
+ }
+ return m_Expressions.at(&_e);
+}
+
+smt::Expression SMTChecker::var(Declaration const& _decl)
+{
+ solAssert(m_Variables.count(&_decl), "");
+ return m_Variables.at(&_decl);
+}
diff --git a/libsolidity/formal/SMTChecker.h b/libsolidity/formal/SMTChecker.h
new file mode 100644
index 00000000..d23fd201
--- /dev/null
+++ b/libsolidity/formal/SMTChecker.h
@@ -0,0 +1,114 @@
+/*
+ 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 <libsolidity/ast/ASTVisitor.h>
+#include <libsolidity/formal/SolverInterface.h>
+#include <libsolidity/interface/ReadFile.h>
+
+#include <map>
+#include <string>
+
+namespace dev
+{
+namespace solidity
+{
+
+class ErrorReporter;
+
+class SMTChecker: private ASTConstVisitor
+{
+public:
+ SMTChecker(ErrorReporter& _errorReporter, ReadCallback::Callback const& _readCallback);
+
+ void analyze(SourceUnit const& _sources);
+
+private:
+ // TODO: Check that we do not have concurrent reads and writes to a variable,
+ // because the order of expression evaluation is undefined
+ // TODO: or just force a certain order, but people might have a different idea about that.
+
+ virtual void endVisit(VariableDeclaration const& _node) override;
+ virtual bool visit(FunctionDefinition const& _node) override;
+ virtual void endVisit(FunctionDefinition const& _node) override;
+ virtual bool visit(IfStatement const& _node) override;
+ virtual bool visit(WhileStatement const& _node) override;
+ virtual void endVisit(VariableDeclarationStatement const& _node) override;
+ virtual void endVisit(ExpressionStatement const& _node) override;
+ virtual void endVisit(Assignment const& _node) override;
+ virtual void endVisit(TupleExpression const& _node) override;
+ virtual void endVisit(BinaryOperation const& _node) override;
+ virtual void endVisit(FunctionCall const& _node) override;
+ virtual void endVisit(Identifier const& _node) override;
+ virtual void endVisit(Literal const& _node) override;
+
+ void arithmeticOperation(BinaryOperation const& _op);
+ void compareOperation(BinaryOperation const& _op);
+ void booleanOperation(BinaryOperation const& _op);
+
+ void checkCondition(
+ smt::Expression _condition,
+ SourceLocation const& _location,
+ std::string const& _description,
+ std::string const& _additionalValueName = "",
+ smt::Expression* _additionalValue = nullptr
+ );
+
+ void createVariable(VariableDeclaration const& _varDecl, bool _setToZero);
+
+ static std::string uniqueSymbol(Declaration const& _decl);
+ static std::string uniqueSymbol(Expression const& _expr);
+
+ /// @returns true if _delc is a variable that is known at the current point, i.e.
+ /// has a valid sequence number
+ bool knownVariable(Declaration const& _decl);
+ /// @returns an expression denoting the value of the variable declared in @a _decl
+ /// at the current point.
+ smt::Expression currentValue(Declaration const& _decl);
+ /// @returns an expression denoting the value of the variable declared in @a _decl
+ /// at the given sequence point. Does not ensure that this sequence point exists.
+ smt::Expression valueAtSequence(Declaration const& _decl, int _sequence);
+ /// Allocates a new sequence number for the declaration, updates the current
+ /// 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);
+
+ static smt::Expression minValue(IntegerType const& _t);
+ static smt::Expression maxValue(IntegerType const& _t);
+
+ /// Returns the expression corresponding to the AST node. Creates a new expression
+ /// if it does not exist yet.
+ smt::Expression expr(Expression const& _e);
+ /// 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);
+
+ std::shared_ptr<smt::SolverInterface> m_interface;
+ std::map<Declaration const*, int> m_currentSequenceCounter;
+ std::map<Declaration const*, int> m_nextFreeSequenceCounter;
+ std::map<Expression const*, smt::Expression> m_Expressions;
+ std::map<Declaration const*, smt::Expression> m_Variables;
+ ErrorReporter& m_errorReporter;
+
+ FunctionDefinition const* m_currentFunction = nullptr;
+};
+
+}
+}
diff --git a/libsolidity/formal/SMTLib2Interface.cpp b/libsolidity/formal/SMTLib2Interface.cpp
new file mode 100644
index 00000000..cbd766fb
--- /dev/null
+++ b/libsolidity/formal/SMTLib2Interface.cpp
@@ -0,0 +1,187 @@
+/*
+ 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/SMTLib2Interface.h>
+
+#include <libsolidity/interface/Exceptions.h>
+#include <libsolidity/interface/ReadFile.h>
+
+#include <boost/algorithm/string/predicate.hpp>
+#include <boost/algorithm/string/join.hpp>
+#include <boost/filesystem/operations.hpp>
+
+#include <cstdio>
+#include <fstream>
+#include <iostream>
+#include <memory>
+#include <stdexcept>
+#include <string>
+#include <array>
+
+using namespace std;
+using namespace dev;
+using namespace dev::solidity;
+using namespace dev::solidity::smt;
+
+SMTLib2Interface::SMTLib2Interface(ReadCallback::Callback const& _queryCallback):
+ m_queryCallback(_queryCallback)
+{
+ reset();
+}
+
+void SMTLib2Interface::reset()
+{
+ m_accumulatedOutput.clear();
+ m_accumulatedOutput.emplace_back();
+ write("(set-option :produce-models true)");
+ write("(set-logic QF_UFLIA)");
+}
+
+void SMTLib2Interface::push()
+{
+ m_accumulatedOutput.emplace_back();
+}
+
+void SMTLib2Interface::pop()
+{
+ solAssert(!m_accumulatedOutput.empty(), "");
+ m_accumulatedOutput.pop_back();
+}
+
+Expression SMTLib2Interface::newFunction(string _name, Sort _domain, Sort _codomain)
+{
+ write(
+ "(declare-fun |" +
+ _name +
+ "| (" +
+ (_domain == Sort::Int ? "Int" : "Bool") +
+ ") " +
+ (_codomain == Sort::Int ? "Int" : "Bool") +
+ ")"
+ );
+ return SolverInterface::newFunction(move(_name), _domain, _codomain);
+}
+
+Expression SMTLib2Interface::newInteger(string _name)
+{
+ write("(declare-const |" + _name + "| Int)");
+ return SolverInterface::newInteger(move(_name));
+}
+
+Expression SMTLib2Interface::newBool(string _name)
+{
+ write("(declare-const |" + _name + "| Bool)");
+ return SolverInterface::newBool(std::move(_name));
+}
+
+void SMTLib2Interface::addAssertion(Expression const& _expr)
+{
+ write("(assert " + toSExpr(_expr) + ")");
+}
+
+pair<CheckResult, vector<string>> SMTLib2Interface::check(vector<Expression> const& _expressionsToEvaluate)
+{
+ string response = querySolver(
+ boost::algorithm::join(m_accumulatedOutput, "\n") +
+ checkSatAndGetValuesCommand(_expressionsToEvaluate)
+ );
+
+ CheckResult result;
+ // TODO proper parsing
+ if (boost::starts_with(response, "sat\n"))
+ result = CheckResult::SATISFIABLE;
+ else if (boost::starts_with(response, "unsat\n"))
+ result = CheckResult::UNSATISFIABLE;
+ else if (boost::starts_with(response, "unknown\n"))
+ result = CheckResult::UNKNOWN;
+ else
+ result = CheckResult::ERROR;
+
+ vector<string> values;
+ if (result != CheckResult::UNSATISFIABLE && result != CheckResult::ERROR)
+ values = parseValues(find(response.cbegin(), response.cend(), '\n'), response.cend());
+ return make_pair(result, values);
+}
+
+string SMTLib2Interface::toSExpr(Expression const& _expr)
+{
+ if (_expr.arguments.empty())
+ return _expr.name;
+ std::string sexpr = "(" + _expr.name;
+ for (auto const& arg: _expr.arguments)
+ sexpr += " " + toSExpr(arg);
+ sexpr += ")";
+ return sexpr;
+}
+
+void SMTLib2Interface::write(string _data)
+{
+ solAssert(!m_accumulatedOutput.empty(), "");
+ m_accumulatedOutput.back() += move(_data) + "\n";
+}
+
+string SMTLib2Interface::checkSatAndGetValuesCommand(vector<Expression> const& _expressionsToEvaluate)
+{
+ string command;
+ if (_expressionsToEvaluate.empty())
+ command = "(check-sat)\n";
+ else
+ {
+ // TODO make sure these are unique
+ for (size_t i = 0; i < _expressionsToEvaluate.size(); i++)
+ {
+ auto const& e = _expressionsToEvaluate.at(i);
+ // TODO they don't have to be ints...
+ command += "(declare-const |EVALEXPR_" + to_string(i) + "| Int)\n";
+ command += "(assert (= |EVALEXPR_" + to_string(i) + "| " + toSExpr(e) + "))\n";
+ }
+ command += "(check-sat)\n";
+ command += "(get-value (";
+ for (size_t i = 0; i < _expressionsToEvaluate.size(); i++)
+ command += "|EVALEXPR_" + to_string(i) + "| ";
+ command += "))\n";
+ }
+
+ return command;
+}
+
+vector<string> SMTLib2Interface::parseValues(string::const_iterator _start, string::const_iterator _end)
+{
+ vector<string> values;
+ while (_start < _end)
+ {
+ auto valStart = find(_start, _end, ' ');
+ if (valStart < _end)
+ ++valStart;
+ auto valEnd = find(valStart, _end, ')');
+ values.emplace_back(valStart, valEnd);
+ _start = find(valEnd, _end, '(');
+ }
+
+ return values;
+}
+
+string SMTLib2Interface::querySolver(string const& _input)
+{
+ if (!m_queryCallback)
+ BOOST_THROW_EXCEPTION(SolverError() << errinfo_comment("No SMT solver available."));
+
+ ReadCallback::Result queryResult = m_queryCallback(_input);
+ if (!queryResult.success)
+ BOOST_THROW_EXCEPTION(SolverError() << errinfo_comment(queryResult.responseOrErrorMessage));
+ return queryResult.responseOrErrorMessage;
+}
diff --git a/libsolidity/formal/SMTLib2Interface.h b/libsolidity/formal/SMTLib2Interface.h
new file mode 100644
index 00000000..b8dac366
--- /dev/null
+++ b/libsolidity/formal/SMTLib2Interface.h
@@ -0,0 +1,75 @@
+/*
+ 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 <libsolidity/formal/SolverInterface.h>
+
+#include <libsolidity/interface/Exceptions.h>
+#include <libsolidity/interface/ReadFile.h>
+
+#include <libdevcore/Common.h>
+
+#include <boost/noncopyable.hpp>
+
+#include <map>
+#include <string>
+#include <vector>
+#include <cstdio>
+
+namespace dev
+{
+namespace solidity
+{
+namespace smt
+{
+
+class SMTLib2Interface: public SolverInterface, public boost::noncopyable
+{
+public:
+ SMTLib2Interface(ReadCallback::Callback const& _queryCallback);
+
+ void reset() override;
+
+ void push() override;
+ void pop() override;
+
+ Expression newFunction(std::string _name, Sort _domain, Sort _codomain) override;
+ Expression newInteger(std::string _name) override;
+ Expression newBool(std::string _name) override;
+
+ void addAssertion(Expression const& _expr) override;
+ std::pair<CheckResult, std::vector<std::string>> check(std::vector<Expression> const& _expressionsToEvaluate) override;
+
+private:
+ std::string toSExpr(Expression const& _expr);
+
+ void write(std::string _data);
+
+ std::string checkSatAndGetValuesCommand(std::vector<Expression> const& _expressionsToEvaluate);
+ std::vector<std::string> parseValues(std::string::const_iterator _start, std::string::const_iterator _end);
+
+ /// Communicates with the solver via the callback. Throws SMTSolverError on error.
+ std::string querySolver(std::string const& _input);
+
+ ReadCallback::Callback m_queryCallback;
+ std::vector<std::string> m_accumulatedOutput;
+};
+
+}
+}
+}
diff --git a/libsolidity/formal/SolverInterface.h b/libsolidity/formal/SolverInterface.h
new file mode 100644
index 00000000..32d92a2a
--- /dev/null
+++ b/libsolidity/formal/SolverInterface.h
@@ -0,0 +1,178 @@
+/*
+ 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 <libsolidity/interface/Exceptions.h>
+#include <libsolidity/interface/ReadFile.h>
+
+#include <libdevcore/Common.h>
+#include <libdevcore/Exceptions.h>
+
+#include <boost/noncopyable.hpp>
+
+#include <map>
+#include <string>
+#include <vector>
+#include <cstdio>
+
+namespace dev
+{
+namespace solidity
+{
+namespace smt
+{
+
+enum class CheckResult
+{
+ SATISFIABLE, UNSATISFIABLE, UNKNOWN, ERROR
+};
+
+enum class Sort
+{
+ Int, Bool
+};
+
+/// C++ representation of an SMTLIB2 expression.
+class Expression
+{
+ friend class SolverInterface;
+public:
+ Expression(size_t _number): name(std::to_string(_number)) {}
+ Expression(u256 const& _number): name(_number.str()) {}
+ Expression(bigint const& _number): name(_number.str()) {}
+
+ Expression(Expression const& _other) = default;
+ Expression(Expression&& _other) = default;
+ Expression& operator=(Expression const& _other) = default;
+ Expression& operator=(Expression&& _other) = default;
+
+ static Expression ite(Expression _condition, Expression _trueValue, Expression _falseValue)
+ {
+ return Expression("ite", std::vector<Expression>{
+ std::move(_condition), std::move(_trueValue), std::move(_falseValue)
+ });
+ }
+
+ friend Expression operator!(Expression _a)
+ {
+ return Expression("not", std::move(_a));
+ }
+ friend Expression operator&&(Expression _a, Expression _b)
+ {
+ return Expression("and", std::move(_a), std::move(_b));
+ }
+ friend Expression operator||(Expression _a, Expression _b)
+ {
+ return Expression("or", std::move(_a), std::move(_b));
+ }
+ friend Expression operator==(Expression _a, Expression _b)
+ {
+ return Expression("=", std::move(_a), std::move(_b));
+ }
+ friend Expression operator!=(Expression _a, Expression _b)
+ {
+ return !(std::move(_a) == std::move(_b));
+ }
+ friend Expression operator<(Expression _a, Expression _b)
+ {
+ return Expression("<", std::move(_a), std::move(_b));
+ }
+ friend Expression operator<=(Expression _a, Expression _b)
+ {
+ return Expression("<=", std::move(_a), std::move(_b));
+ }
+ friend Expression operator>(Expression _a, Expression _b)
+ {
+ return Expression(">", std::move(_a), std::move(_b));
+ }
+ friend Expression operator>=(Expression _a, Expression _b)
+ {
+ return Expression(">=", std::move(_a), std::move(_b));
+ }
+ friend Expression operator+(Expression _a, Expression _b)
+ {
+ return Expression("+", std::move(_a), std::move(_b));
+ }
+ friend Expression operator-(Expression _a, Expression _b)
+ {
+ return Expression("-", std::move(_a), std::move(_b));
+ }
+ friend Expression operator*(Expression _a, Expression _b)
+ {
+ return Expression("*", std::move(_a), std::move(_b));
+ }
+ Expression operator()(Expression _a) const
+ {
+ solAssert(arguments.empty(), "Attempted function application to non-function.");
+ return Expression(name, _a);
+ }
+
+ std::string const name;
+ std::vector<Expression> const arguments;
+
+private:
+ /// Manual constructor, should only be used by SolverInterface and this class itself.
+ Expression(std::string _name, std::vector<Expression> _arguments):
+ name(std::move(_name)), arguments(std::move(_arguments)) {}
+
+ explicit Expression(std::string _name):
+ Expression(std::move(_name), std::vector<Expression>{}) {}
+ Expression(std::string _name, Expression _arg):
+ Expression(std::move(_name), std::vector<Expression>{std::move(_arg)}) {}
+ Expression(std::string _name, Expression _arg1, Expression _arg2):
+ Expression(std::move(_name), std::vector<Expression>{std::move(_arg1), std::move(_arg2)}) {}
+};
+
+DEV_SIMPLE_EXCEPTION(SolverError);
+
+class SolverInterface
+{
+public:
+ virtual void reset() = 0;
+
+ virtual void push() = 0;
+ virtual void pop() = 0;
+
+ virtual Expression newFunction(std::string _name, Sort /*_domain*/, Sort /*_codomain*/)
+ {
+ // Subclasses should do something here
+ return Expression(std::move(_name), {});
+ }
+ virtual Expression newInteger(std::string _name)
+ {
+ // Subclasses should do something here
+ return Expression(std::move(_name), {});
+ }
+ virtual Expression newBool(std::string _name)
+ {
+ // Subclasses should do something here
+ return Expression(std::move(_name), {});
+ }
+
+ virtual void addAssertion(Expression const& _expr) = 0;
+
+ /// Checks for satisfiability, evaluates the expressions if a model
+ /// is available. Throws SMTSolverError on error.
+ virtual std::pair<CheckResult, std::vector<std::string>>
+ check(std::vector<Expression> const& _expressionsToEvaluate) = 0;
+};
+
+
+}
+}
+}
diff --git a/libsolidity/formal/Z3Interface.cpp b/libsolidity/formal/Z3Interface.cpp
new file mode 100644
index 00000000..522928f0
--- /dev/null
+++ b/libsolidity/formal/Z3Interface.cpp
@@ -0,0 +1,189 @@
+/*
+ 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/Z3Interface.h>
+
+#include <libsolidity/interface/Exceptions.h>
+
+#include <libdevcore/CommonIO.h>
+
+using namespace std;
+using namespace dev;
+using namespace dev::solidity::smt;
+
+Z3Interface::Z3Interface():
+ m_solver(m_context)
+{
+}
+
+void Z3Interface::reset()
+{
+ m_constants.clear();
+ m_functions.clear();
+ m_solver.reset();
+}
+
+void Z3Interface::push()
+{
+ m_solver.push();
+}
+
+void Z3Interface::pop()
+{
+ m_solver.pop();
+}
+
+Expression Z3Interface::newFunction(string _name, Sort _domain, Sort _codomain)
+{
+ m_functions.insert({_name, m_context.function(_name.c_str(), z3Sort(_domain), z3Sort(_codomain))});
+ return SolverInterface::newFunction(move(_name), _domain, _codomain);
+}
+
+Expression Z3Interface::newInteger(string _name)
+{
+ m_constants.insert({_name, m_context.int_const(_name.c_str())});
+ return SolverInterface::newInteger(move(_name));
+}
+
+Expression Z3Interface::newBool(string _name)
+{
+ m_constants.insert({_name, m_context.bool_const(_name.c_str())});
+ return SolverInterface::newBool(std::move(_name));
+}
+
+void Z3Interface::addAssertion(Expression const& _expr)
+{
+ m_solver.add(toZ3Expr(_expr));
+}
+
+pair<CheckResult, vector<string>> Z3Interface::check(vector<Expression> const& _expressionsToEvaluate)
+{
+// cout << "---------------------------------" << endl;
+// cout << m_solver << endl;
+ CheckResult result;
+ switch (m_solver.check())
+ {
+ case z3::check_result::sat:
+ result = CheckResult::SATISFIABLE;
+ cout << "sat" << endl;
+ break;
+ case z3::check_result::unsat:
+ result = CheckResult::UNSATISFIABLE;
+ cout << "unsat" << endl;
+ break;
+ case z3::check_result::unknown:
+ result = CheckResult::UNKNOWN;
+ cout << "unknown" << endl;
+ break;
+ default:
+ solAssert(false, "");
+ }
+// cout << "---------------------------------" << endl;
+
+
+ vector<string> values;
+ if (result != CheckResult::UNSATISFIABLE)
+ {
+ z3::model m = m_solver.get_model();
+ for (Expression const& e: _expressionsToEvaluate)
+ values.push_back(toString(m.eval(toZ3Expr(e))));
+ }
+ return make_pair(result, values);
+}
+
+z3::expr Z3Interface::toZ3Expr(Expression const& _expr)
+{
+ if (_expr.arguments.empty() && m_constants.count(_expr.name))
+ return m_constants.at(_expr.name);
+ z3::expr_vector arguments(m_context);
+ for (auto const& arg: _expr.arguments)
+ arguments.push_back(toZ3Expr(arg));
+
+ static map<string, unsigned> arity{
+ {"ite", 3},
+ {"not", 1},
+ {"and", 2},
+ {"or", 2},
+ {"=", 2},
+ {"<", 2},
+ {"<=", 2},
+ {">", 2},
+ {">=", 2},
+ {"+", 2},
+ {"-", 2},
+ {"*", 2},
+ {">=", 2}
+ };
+ string const& n = _expr.name;
+ if (m_functions.count(n))
+ return m_functions.at(n)(arguments);
+ else if (m_constants.count(n))
+ {
+ solAssert(arguments.empty(), "");
+ return m_constants.at(n);
+ }
+ else if (arguments.empty())
+ {
+ // We assume it is an integer...
+ return m_context.int_val(n.c_str());
+ }
+
+ assert(arity.count(n) && arity.at(n) == arguments.size());
+ if (n == "ite")
+ return z3::ite(arguments[0], arguments[1], arguments[2]);
+ else if (n == "not")
+ return !arguments[0];
+ else if (n == "and")
+ return arguments[0] && arguments[1];
+ else if (n == "or")
+ return arguments[0] || arguments[1];
+ else if (n == "=")
+ return arguments[0] == arguments[1];
+ else if (n == "<")
+ return arguments[0] < arguments[1];
+ else if (n == "<=")
+ return arguments[0] <= arguments[1];
+ else if (n == ">")
+ return arguments[0] > arguments[1];
+ else if (n == ">=")
+ return arguments[0] >= arguments[1];
+ else if (n == "+")
+ 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];
+}
+
+z3::sort Z3Interface::z3Sort(Sort _sort)
+{
+ switch (_sort)
+ {
+ case Sort::Bool:
+ return m_context.bool_sort();
+ case Sort::Int:
+ return m_context.int_sort();
+ default:
+ break;
+ }
+ solAssert(false, "");
+ // Cannot be reached.
+ return m_context.int_sort();
+}
diff --git a/libsolidity/formal/Z3Interface.h b/libsolidity/formal/Z3Interface.h
new file mode 100644
index 00000000..44d4bb2f
--- /dev/null
+++ b/libsolidity/formal/Z3Interface.h
@@ -0,0 +1,65 @@
+/*
+ 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 <libsolidity/formal/SolverInterface.h>
+
+#include <boost/noncopyable.hpp>
+
+#include <z3++.h>
+
+namespace dev
+{
+namespace solidity
+{
+namespace smt
+{
+
+class Z3Interface: public SolverInterface, public boost::noncopyable
+{
+public:
+ Z3Interface();
+
+ void reset() override;
+
+ void push() override;
+ void pop() override;
+
+ Expression newFunction(std::string _name, Sort _domain, Sort _codomain) override;
+ Expression newInteger(std::string _name) override;
+ Expression newBool(std::string _name) override;
+
+ void addAssertion(Expression const& _expr) override;
+ std::pair<CheckResult, std::vector<std::string>> check(std::vector<Expression> const& _expressionsToEvaluate) override;
+
+private:
+ z3::expr toZ3Expr(Expression const& _expr);
+ z3::sort z3Sort(smt::Sort _sort);
+
+ std::string checkSatAndGetValuesCommand(std::vector<Expression> const& _expressionsToEvaluate);
+ std::vector<std::string> parseValues(std::string::const_iterator _start, std::string::const_iterator _end);
+
+ z3::context m_context;
+ z3::solver m_solver;
+ std::map<std::string, z3::expr> m_constants;
+ std::map<std::string, z3::func_decl> m_functions;
+};
+
+}
+}
+}
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-26 15:34:15 +0800