aboutsummaryrefslogtreecommitdiffstats
path: root/libsolidity
diff options
context:
space:
mode:
Diffstat (limited to 'libsolidity')
-rw-r--r--libsolidity/formal/SMTChecker.cpp447
-rw-r--r--libsolidity/formal/SMTChecker.h65
-rw-r--r--libsolidity/formal/SMTCheckerImpl.cpp469
-rw-r--r--libsolidity/formal/SMTCheckerImpl.h97
-rw-r--r--libsolidity/formal/SMTLib2Interface.cpp168
-rw-r--r--libsolidity/formal/SMTLib2Interface.h29
-rw-r--r--libsolidity/formal/SMTSolverCommunicator.cpp75
-rw-r--r--libsolidity/formal/SMTSolverCommunicator.h50
-rw-r--r--libsolidity/interface/CompilerStack.cpp2
9 files changed, 686 insertions, 716 deletions
diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp
index 0e559fae..b9e0e8f3 100644
--- a/libsolidity/formal/SMTChecker.cpp
+++ b/libsolidity/formal/SMTChecker.cpp
@@ -17,7 +17,6 @@
#include <libsolidity/formal/SMTChecker.h>
-#include <libsolidity/formal/SMTCheckerImpl.h>
#include <libsolidity/interface/ErrorReporter.h>
@@ -25,12 +24,452 @@ using namespace std;
using namespace dev;
using namespace dev::solidity;
-SMTChecker::SMTChecker(ErrorReporter& _errorReporter):
- m_impl(make_shared<SMTCheckerImpl>(_errorReporter))
+SMTChecker::SMTChecker(ErrorReporter& _errorReporter, ReadFile::Callback const& _readFileCallback):
+ m_interface(_readFileCallback),
+ m_errorReporter(_errorReporter)
{
}
void SMTChecker::analyze(SourceUnit const& _source)
{
- m_impl->analyze(_source);
+ bool pragmaFound = false;
+ for (auto const& node: _source.nodes())
+ if (auto const* pragma = dynamic_cast<PragmaDirective const*>(node.get()))
+ if (pragma->literals()[0] == "checkAssertionsZ3")
+ pragmaFound = true;
+ if (pragmaFound)
+ {
+ m_interface.reset();
+ m_currentSequenceCounter.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.
+ m_interface.pop();
+ m_currentFunction = nullptr;
+}
+
+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]) && _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 " + intType.minValue().str() + ")",
+ "value",
+ &value
+ );
+ checkCondition(
+ value > maxValue(intType),
+ _op.location(),
+ "Overflow (resulting value larger than " + intType.maxValue().str() + ")",
+ "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;
+ if (m_currentFunction)
+ {
+ if (_additionalValue)
+ expressionsToEvaluate.emplace_back(*_additionalValue);
+ for (auto const& param: m_currentFunction->parameters())
+ if (knownVariable(*param))
+ expressionsToEvaluate.emplace_back(currentValue(*param));
+ for (auto const& var: m_currentFunction->localVariables())
+ if (knownVariable(*var))
+ expressionsToEvaluate.emplace_back(currentValue(*var));
+ }
+ smt::CheckResult result;
+ vector<string> values;
+ tie(result, values) = m_interface.check(expressionsToEvaluate);
+ switch (result)
+ {
+ case smt::CheckResult::SAT:
+ {
+ std::ostringstream message;
+ message << _description << " happens here";
+ size_t i = 0;
+ if (m_currentFunction)
+ {
+ message << " for:\n";
+ if (_additionalValue)
+ message << " " << _additionalValueName << " = " << values.at(i++) << "\n";
+ for (auto const& param: m_currentFunction->parameters())
+ if (knownVariable(*param))
+ message << " " << param->name() << " = " << values.at(i++) << "\n";
+ for (auto const& var: m_currentFunction->localVariables())
+ if (knownVariable(*var))
+ message << " " << var->name() << " = " << values.at(i++) << "\n";
+ }
+ else
+ message << ".";
+ m_errorReporter.warning(_location, message.str());
+ break;
+ }
+ case smt::CheckResult::UNSAT:
+ 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 (auto intType = dynamic_cast<IntegerType const*>(_varDecl.type().get()))
+ {
+ solAssert(m_currentSequenceCounter.count(&_varDecl) == 0, "");
+ solAssert(m_z3Variables.count(&_varDecl) == 0, "");
+ m_currentSequenceCounter[&_varDecl] = 0;
+ m_z3Variables.emplace(&_varDecl, m_interface.newFunction(uniqueSymbol(_varDecl), smt::Sort::Int, smt::Sort::Int));
+ if (_setToZero)
+ m_interface.addAssertion(currentValue(_varDecl) == 0);
+ else
+ {
+ m_interface.addAssertion(currentValue(_varDecl) >= minValue(*intType));
+ m_interface.addAssertion(currentValue(_varDecl) <= maxValue(*intType));
+ }
+ }
+ 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 var(_decl)(m_currentSequenceCounter.at(&_decl));
+}
+
+smt::Expression SMTChecker::newValue(const Declaration& _decl)
+{
+ solAssert(m_currentSequenceCounter.count(&_decl), "");
+ m_currentSequenceCounter[&_decl]++;
+ return currentValue(_decl);
+}
+
+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_z3Expressions.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_z3Expressions.emplace(&_e, m_interface.newInteger(uniqueSymbol(_e)));
+ break;
+ }
+ case Type::Category::Integer:
+ m_z3Expressions.emplace(&_e, m_interface.newInteger(uniqueSymbol(_e)));
+ break;
+ case Type::Category::Bool:
+ m_z3Expressions.emplace(&_e, m_interface.newBool(uniqueSymbol(_e)));
+ break;
+ default:
+ solAssert(false, "Type not implemented.");
+ }
+ }
+ return m_z3Expressions.at(&_e);
+}
+
+smt::Expression SMTChecker::var(Declaration const& _decl)
+{
+ solAssert(m_z3Variables.count(&_decl), "");
+ return m_z3Variables.at(&_decl);
}
diff --git a/libsolidity/formal/SMTChecker.h b/libsolidity/formal/SMTChecker.h
index 7e7ee3d9..8c6a2327 100644
--- a/libsolidity/formal/SMTChecker.h
+++ b/libsolidity/formal/SMTChecker.h
@@ -17,9 +17,12 @@
#pragma once
+#include <libsolidity/ast/ASTVisitor.h>
+#include <libsolidity/formal/SMTLib2Interface.h>
+#include <libsolidity/interface/ReadFile.h>
+
#include <map>
#include <string>
-#include <memory>
namespace dev
{
@@ -27,18 +30,68 @@ namespace solidity
{
class ErrorReporter;
-class SourceUnit;
-class SMTCheckerImpl;
-class SMTChecker
+class SMTChecker: private ASTConstVisitor
{
public:
- SMTChecker(ErrorReporter& _errorReporter);
+ SMTChecker(ErrorReporter& _errorReporter, ReadFile::Callback const& _readCallback);
void analyze(SourceUnit const& _sources);
private:
- std::shared_ptr<SMTCheckerImpl> m_impl;
+ // 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 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);
+
+ std::string uniqueSymbol(Declaration const& _decl);
+ std::string uniqueSymbol(Expression const& _expr);
+ bool knownVariable(Declaration const& _decl);
+ smt::Expression currentValue(Declaration const& _decl);
+ smt::Expression newValue(Declaration const& _decl);
+
+ smt::Expression minValue(IntegerType const& _t);
+ 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);
+
+ smt::SMTLib2Interface m_interface;
+ std::map<Declaration const*, int> m_currentSequenceCounter;
+ std::map<Expression const*, smt::Expression> m_z3Expressions;
+ std::map<Declaration const*, smt::Expression> m_z3Variables;
+ ErrorReporter& m_errorReporter;
+
+ FunctionDefinition const* m_currentFunction = nullptr;
};
}
diff --git a/libsolidity/formal/SMTCheckerImpl.cpp b/libsolidity/formal/SMTCheckerImpl.cpp
deleted file mode 100644
index b86a0279..00000000
--- a/libsolidity/formal/SMTCheckerImpl.cpp
+++ /dev/null
@@ -1,469 +0,0 @@
-/*
- 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/SMTCheckerImpl.h>
-
-
-#include <libsolidity/interface/ErrorReporter.h>
-
-using namespace std;
-using namespace dev;
-using namespace dev::solidity;
-
-SMTCheckerImpl::SMTCheckerImpl(ErrorReporter& _errorReporter):
- m_errorReporter(_errorReporter)
-{
-}
-
-void SMTCheckerImpl::analyze(SourceUnit const& _source)
-{
- bool pragmaFound = false;
- for (auto const& node: _source.nodes())
- if (auto const* pragma = dynamic_cast<PragmaDirective const*>(node.get()))
- if (pragma->literals()[0] == "checkAssertionsZ3")
- pragmaFound = true;
- if (pragmaFound)
- {
- m_interface.reset();
- m_currentSequenceCounter.clear();
- _source.accept(*this);
- }
-}
-
-void SMTCheckerImpl::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 SMTCheckerImpl::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 SMTCheckerImpl::endVisit(FunctionDefinition const&)
-{
- // TOOD we could check for "reachability", i.e. satisfiability here.
- m_interface.pop();
- m_currentFunction = nullptr;
-}
-
-void SMTCheckerImpl::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]) && _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 SMTCheckerImpl::endVisit(ExpressionStatement const&)
-{
-}
-
-void SMTCheckerImpl::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 SMTCheckerImpl::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 SMTCheckerImpl::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 SMTCheckerImpl::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 SMTCheckerImpl::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 SMTCheckerImpl::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 SMTCheckerImpl::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 " + intType.minValue().str() + ")",
- "value",
- &value
- );
- checkCondition(
- value > maxValue(intType),
- _op.location(),
- "Overflow (resulting value larger than " + intType.maxValue().str() + ")",
- "value",
- &value
- );
-
- m_interface.addAssertion(expr(_op) == value);
- break;
- }
- default:
- m_errorReporter.warning(
- _op.location(),
- "Assertion checker does not yet implement this operator."
- );
- }
-}
-
-void SMTCheckerImpl::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 SMTCheckerImpl::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 SMTCheckerImpl::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;
- if (m_currentFunction)
- {
- if (_additionalValue)
- expressionsToEvaluate.emplace_back(*_additionalValue);
- for (auto const& param: m_currentFunction->parameters())
- if (knownVariable(*param))
- expressionsToEvaluate.emplace_back(currentValue(*param));
- for (auto const& var: m_currentFunction->localVariables())
- if (knownVariable(*var))
- expressionsToEvaluate.emplace_back(currentValue(*var));
- }
- smt::CheckResult result;
- vector<string> values;
- tie(result, values) = m_interface.check(expressionsToEvaluate);
- switch (result)
- {
- case smt::CheckResult::SAT:
- {
- std::ostringstream message;
- message << _description << " happens here";
- size_t i = 0;
- if (m_currentFunction)
- {
- message << " for:\n";
- if (_additionalValue)
- message << " " << _additionalValueName << " = " << values.at(i++) << "\n";
- for (auto const& param: m_currentFunction->parameters())
- if (knownVariable(*param))
- message << " " << param->name() << " = " << values.at(i++) << "\n";
- for (auto const& var: m_currentFunction->localVariables())
- if (knownVariable(*var))
- message << " " << var->name() << " = " << values.at(i++) << "\n";
- }
- else
- message << ".";
- m_errorReporter.warning(_location, message.str());
- break;
- }
- case smt::CheckResult::UNSAT:
- break;
- case smt::CheckResult::UNKNOWN:
- m_errorReporter.warning(_location, _description + " might happen here.");
- break;
- }
- m_interface.pop();
-}
-
-void SMTCheckerImpl::createVariable(VariableDeclaration const& _varDecl, bool _setToZero)
-{
- if (auto intType = dynamic_cast<IntegerType const*>(_varDecl.type().get()))
- {
- solAssert(m_currentSequenceCounter.count(&_varDecl) == 0, "");
- solAssert(m_z3Variables.count(&_varDecl) == 0, "");
- m_currentSequenceCounter[&_varDecl] = 0;
- m_z3Variables.emplace(&_varDecl, m_interface.newFunction(uniqueSymbol(_varDecl), smt::Sort::Int, smt::Sort::Int));
- if (_setToZero)
- m_interface.addAssertion(currentValue(_varDecl) == 0);
- else
- {
- m_interface.addAssertion(currentValue(_varDecl) >= minValue(*intType));
- m_interface.addAssertion(currentValue(_varDecl) <= maxValue(*intType));
- }
- }
- else
- m_errorReporter.warning(
- _varDecl.location(),
- "Assertion checker does not yet support the type of this variable."
- );
-}
-
-string SMTCheckerImpl::uniqueSymbol(Declaration const& _decl)
-{
- return _decl.name() + "_" + to_string(_decl.id());
-}
-
-string SMTCheckerImpl::uniqueSymbol(Expression const& _expr)
-{
- return "expr_" + to_string(_expr.id());
-}
-
-bool SMTCheckerImpl::knownVariable(Declaration const& _decl)
-{
- return m_currentSequenceCounter.count(&_decl);
-}
-
-smt::Expression SMTCheckerImpl::currentValue(Declaration const& _decl)
-{
- solAssert(m_currentSequenceCounter.count(&_decl), "");
- return var(_decl)(m_currentSequenceCounter.at(&_decl));
-}
-
-smt::Expression SMTCheckerImpl::newValue(const Declaration& _decl)
-{
- solAssert(m_currentSequenceCounter.count(&_decl), "");
- m_currentSequenceCounter[&_decl]++;
- return currentValue(_decl);
-}
-
-smt::Expression SMTCheckerImpl::minValue(IntegerType const& _t)
-{
- return smt::Expression(_t.minValue());
-}
-
-smt::Expression SMTCheckerImpl::maxValue(IntegerType const& _t)
-{
- return smt::Expression(_t.maxValue());
-}
-
-smt::Expression SMTCheckerImpl::expr(Expression const& _e)
-{
- if (!m_z3Expressions.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_z3Expressions.emplace(&_e, m_interface.newInteger(uniqueSymbol(_e)));
- break;
- }
- case Type::Category::Integer:
- m_z3Expressions.emplace(&_e, m_interface.newInteger(uniqueSymbol(_e)));
- break;
- case Type::Category::Bool:
- m_z3Expressions.emplace(&_e, m_interface.newBool(uniqueSymbol(_e)));
- break;
- default:
- solAssert(false, "Type not implemented.");
- }
- }
- return m_z3Expressions.at(&_e);
-}
-
-smt::Expression SMTCheckerImpl::var(Declaration const& _decl)
-{
- solAssert(m_z3Variables.count(&_decl), "");
- return m_z3Variables.at(&_decl);
-}
diff --git a/libsolidity/formal/SMTCheckerImpl.h b/libsolidity/formal/SMTCheckerImpl.h
deleted file mode 100644
index e5179440..00000000
--- a/libsolidity/formal/SMTCheckerImpl.h
+++ /dev/null
@@ -1,97 +0,0 @@
-/*
- 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/SMTLib2Interface.h>
-
-#include <map>
-#include <string>
-
-namespace dev
-{
-namespace solidity
-{
-
-class ErrorReporter;
-
-class SMTCheckerImpl: private ASTConstVisitor
-{
-public:
- SMTCheckerImpl(ErrorReporter& _errorReporter);
-
- 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 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);
-
- std::string uniqueSymbol(Declaration const& _decl);
- std::string uniqueSymbol(Expression const& _expr);
- bool knownVariable(Declaration const& _decl);
- smt::Expression currentValue(Declaration const& _decl);
- smt::Expression newValue(Declaration const& _decl);
-
- smt::Expression minValue(IntegerType const& _t);
- smt::Expression maxValue(IntegerType const& _t);
-
- /// Returns the z3 expression corresponding to the AST node. Creates a new expression
- /// if it does not exist yet.
- smt::Expression expr(Expression const& _e);
- /// Returns the z3 function declaration corresponding to the given variable.
- /// The function takes one argument which is the "sequence number".
- smt::Expression var(Declaration const& _decl);
-
- smt::SMTLib2Interface m_interface;
- std::map<Declaration const*, int> m_currentSequenceCounter;
- std::map<Expression const*, smt::Expression> m_z3Expressions;
- std::map<Declaration const*, smt::Expression> m_z3Variables;
- ErrorReporter& m_errorReporter;
-
- FunctionDefinition const* m_currentFunction = nullptr;
-};
-
-}
-}
diff --git a/libsolidity/formal/SMTLib2Interface.cpp b/libsolidity/formal/SMTLib2Interface.cpp
index 8d40c354..63ab1679 100644
--- a/libsolidity/formal/SMTLib2Interface.cpp
+++ b/libsolidity/formal/SMTLib2Interface.cpp
@@ -21,6 +21,7 @@
#include <boost/algorithm/string/predicate.hpp>
#include <boost/algorithm/string/join.hpp>
+#include <boost/filesystem/operations.hpp>
#include <cstdio>
#include <fstream>
@@ -30,99 +31,31 @@
#include <string>
#include <array>
-#include <sys/types.h>
-#include <unistd.h>
-#include <stdio.h>
-#include <stdlib.h>
-
using namespace std;
using namespace dev;
using namespace dev::solidity::smt;
-
-//namespace
-//{
-
-//void createSubprocess(FILE*& _readPipe, FILE*& _writePipe)
-//{
-// int pipe_in[2]; /* This is the pipe with wich we write to the child process. */
-// int pipe_out[2]; /* This is the pipe with wich we read from the child process. */
-
-// solAssert(!pipe(pipe_in) && !pipe(pipe_out), "");
-
-// /* Attempt to fork and check for errors */
-// pid_t pid = fork();
-// solAssert(pid != -1, "");
-
-// if (pid)
-// {
-// /* The parent has the non-zero PID. */
-// _readPipe = fdopen(pipe_out[0], "r");
-// _writePipe = fdopen(pipe_in[1], "w");
-// close(pipe_out[1]);
-// close(pipe_in[0]);
-// }
-// else
-// {
-// /* The child has the zero pid returned by fork*/
-// cout << "child" << endl;
-// solAssert(dup2(pipe_out[1], 1) != -1, "");
-// solAssert(dup2(pipe_in[0], 0) != -1, "");
-// solAssert(close(pipe_out[0]) == 0, "");
-// solAssert(close(pipe_out[1]) == 0, "");
-// solAssert(close(pipe_in[0]) == 0, "");
-// solAssert(close(pipe_in[1]) == 0, "");
-// execl("/usr/bin/z3", "z3", "-smt2", "-in", NULL);
-// exit(1); /* Only reached if execl() failed */
-// }
-//}
-
-//}
-
-SMTLib2Interface::SMTLib2Interface()
+SMTLib2Interface::SMTLib2Interface(ReadFile::Callback const& _readFileCallback):
+ m_communicator(_readFileCallback)
{
- // TODO using pipes did not really work, so trying it the hard way for now.
-// createSubprocess(m_solverWrite, m_solverRead);
-// solAssert(m_solverWrite, "Unable to start Z3");
-// solAssert(m_solverRead, "Unable to start Z3");
-// write("(set-option :produce-models true)\n(set-logic QF_LIA)\n");
reset();
}
-SMTLib2Interface::~SMTLib2Interface()
-{
-// if (m_solverWrite)
-// {
-// write("(exit)\n");
-// fflush(m_solverWrite);
-// fclose(m_solverWrite);
-// m_solverWrite = nullptr;
-// }
-// if (m_solverRead)
-// {
-// fclose(m_solverRead);
-// m_solverRead = nullptr;
-// }
-}
-
void SMTLib2Interface::reset()
{
-// write("(reset)\n");
-// write("(set-option :produce-models true)\n");
m_accumulatedOutput.clear();
m_accumulatedOutput.emplace_back();
- write("(set-option :produce-models true)\n(set-logic QF_UFLIA)\n");
+ write("(set-option :produce-models true)");
+ write("(set-logic QF_UFLIA)");
}
void SMTLib2Interface::push()
{
m_accumulatedOutput.emplace_back();
- //write("(push)\n");
}
void SMTLib2Interface::pop()
{
- //write("(pop)\n");
solAssert(!m_accumulatedOutput.empty(), "");
m_accumulatedOutput.pop_back();
}
@@ -136,50 +69,34 @@ Expression SMTLib2Interface::newFunction(string _name, Sort _domain, Sort _codom
(_domain == Sort::Int ? "Int" : "Bool") +
") " +
(_codomain == Sort::Int ? "Int" : "Bool") +
- ")\n"
+ ")"
);
- return Expression(_name, {});
+ return Expression(std::move(_name), {});
}
Expression SMTLib2Interface::newInteger(string _name)
{
- write("(declare-const |" + _name + "| Int)\n");
- return Expression(_name, {});
+ write("(declare-const |" + _name + "| Int)");
+ return Expression(std::move(_name), {});
}
Expression SMTLib2Interface::newBool(string _name)
{
- write("(declare-const |" + _name + "| Bool)\n");
- return Expression(_name, {});
+ write("(declare-const |" + _name + "| Bool)");
+ return Expression(std::move(_name), {});
}
-void SMTLib2Interface::addAssertion(Expression _expr)
+void SMTLib2Interface::addAssertion(Expression const& _expr)
{
- write("(assert " + _expr.toSExpr() + ")\n");
+ write("(assert " + _expr.toSExpr() + ")");
}
pair<CheckResult, vector<string>> SMTLib2Interface::check(vector<Expression> const& _expressionsToEvaluate)
{
- string checks;
- if (_expressionsToEvaluate.empty())
- checks = "(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...
- checks += "(declare-const |EVALEXPR_" + to_string(i) + "| Int)\n";
- checks += "(assert (= |EVALEXPR_" + to_string(i) + "| " + e.toSExpr() + "))\n";
- }
- checks += "(check-sat)\n";
- checks += "(get-value (";
- for (size_t i = 0; i < _expressionsToEvaluate.size(); i++)
- checks += "|EVALEXPR_" + to_string(i) + "| ";
- checks += "))\n";
- }
- string response = communicate(boost::algorithm::join(m_accumulatedOutput, "\n") + checks);
+ string response = m_communicator.communicate(
+ boost::algorithm::join(m_accumulatedOutput, "\n") +
+ checkSatAndGetValuesCommand(_expressionsToEvaluate)
+ );
CheckResult result;
// TODO proper parsing
if (boost::starts_with(response, "sat\n"))
@@ -189,44 +106,43 @@ pair<CheckResult, vector<string>> SMTLib2Interface::check(vector<Expression> con
else if (boost::starts_with(response, "unknown\n"))
result = CheckResult::UNKNOWN;
else
- solAssert(false, "Invalid response to check-sat: " + response);
+ result = CheckResult::ERROR;
vector<string> values;
- if (result != CheckResult::UNSAT)
+ if (result != CheckResult::UNSAT && result != CheckResult::ERROR)
values = parseValues(find(response.cbegin(), response.cend(), '\n'), response.cend());
return make_pair(result, values);
}
-//string SMTLib2Interface::eval(Expression _expr)
-//{
-// write("(get-value (" + _expr.toSExpr() + ")\n");
-// std::string reply = communicate();
-// cout << "<-- Z3: " << reply << endl;
-// // TODO parse
-// return reply;
-//}
-
void SMTLib2Interface::write(string _data)
{
-// cout << " --> Z3: " << _data << endl;
-// solAssert(m_solverWrite, "");
-// solAssert(fputs(_data.c_str(), m_solverWrite) >= 0 || true, "EOF while communicating with Z3.");
-// solAssert(fflush(m_solverWrite) == 0 || true, "");
solAssert(!m_accumulatedOutput.empty(), "");
- m_accumulatedOutput.back() += move(_data);
+ m_accumulatedOutput.back() += move(_data) + "\n";
}
-string SMTLib2Interface::communicate(std::string const& _input)
+string SMTLib2Interface::checkSatAndGetValuesCommand(vector<Expression> const& _expressionsToEvaluate)
{
- ofstream("/tmp/z3exchange.smt2") << _input << "(exit)" << endl;
- FILE* solverOutput = popen("z3 -smt2 /tmp/z3exchange.smt2", "r");
- string result;
- array<char, 128> buffer;
- while (!feof(solverOutput))
- if (fgets(buffer.data(), 127, solverOutput) != nullptr)
- result += buffer.data();
- fclose(solverOutput);
- return result;
+ 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) + "| " + e.toSExpr() + "))\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)
diff --git a/libsolidity/formal/SMTLib2Interface.h b/libsolidity/formal/SMTLib2Interface.h
index b7bab043..d8c11df9 100644
--- a/libsolidity/formal/SMTLib2Interface.h
+++ b/libsolidity/formal/SMTLib2Interface.h
@@ -17,10 +17,15 @@
#pragma once
+#include <libsolidity/formal/SMTSolverCommunicator.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>
@@ -35,7 +40,7 @@ namespace smt
enum class CheckResult
{
- SAT, UNSAT, UNKNOWN
+ SAT, UNSAT, UNKNOWN, ERROR
};
enum class Sort
@@ -43,6 +48,7 @@ enum class Sort
Int, Bool
};
+/// C++ representation of an SMTLIB2 expression.
class Expression
{
friend class SMTLib2Interface;
@@ -62,23 +68,23 @@ public:
friend Expression operator!(Expression _a)
{
- return Expression("not", _a);
+ return Expression("not", std::move(_a));
}
friend Expression operator&&(Expression _a, Expression _b)
{
- return Expression("and", _a, _b);
+ return Expression("and", std::move(_a), std::move(_b));
}
friend Expression operator||(Expression _a, Expression _b)
{
- return Expression("or", _a, _b);
+ return Expression("or", std::move(_a), std::move(_b));
}
friend Expression operator==(Expression _a, Expression _b)
{
- return Expression("=", _a, _b);
+ return Expression("=", std::move(_a), std::move(_b));
}
friend Expression operator!=(Expression _a, Expression _b)
{
- return !(_a == _b);
+ return !(std::move(_a) == std::move(_b));
}
friend Expression operator<(Expression _a, Expression _b)
{
@@ -140,8 +146,7 @@ private:
class SMTLib2Interface: public boost::noncopyable
{
public:
- SMTLib2Interface();
- ~SMTLib2Interface();
+ SMTLib2Interface(ReadFile::Callback const& _readFileCallback);
void reset();
@@ -152,19 +157,17 @@ public:
Expression newInteger(std::string _name);
Expression newBool(std::string _name);
- void addAssertion(Expression _expr);
+ void addAssertion(Expression const& _expr);
std::pair<CheckResult, std::vector<std::string>> check(std::vector<Expression> const& _expressionsToEvaluate);
-// std::string eval(Expression _expr);
private:
void write(std::string _data);
- std::string communicate(std::string const& _input);
+ std::string checkSatAndGetValuesCommand(std::vector<Expression> const& _expressionsToEvaluate);
std::vector<std::string> parseValues(std::string::const_iterator _start, std::string::const_iterator _end);
+ SMTSolverCommunicator m_communicator;
std::vector<std::string> m_accumulatedOutput;
-// FILE* m_solverWrite = nullptr;
-// FILE* m_solverRead = nullptr;
};
diff --git a/libsolidity/formal/SMTSolverCommunicator.cpp b/libsolidity/formal/SMTSolverCommunicator.cpp
new file mode 100644
index 00000000..a97e5fcc
--- /dev/null
+++ b/libsolidity/formal/SMTSolverCommunicator.cpp
@@ -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/>.
+*/
+
+#include <libsolidity/formal/SMTSolverCommunicator.h>
+
+#include <libdevcore/Common.h>
+
+#include <boost/filesystem/operations.hpp>
+
+#include <fstream>
+
+#include <stdio.h>
+
+using namespace std;
+using namespace dev;
+using namespace dev::solidity::smt;
+
+#ifdef EMSCRIPTEN
+
+string SMTSolverCommunicator::communicate(string const& _input)
+{
+ auto result = m_readFileCallback("SMTLIB2Solver>> " + _input);
+ if (result.success)
+ return result.contentsOrErrorMessage;
+ else
+ return "";
+}
+
+#else
+
+#ifndef _WIN32
+inline FILE* _popen(char const* command, char const* type)
+{
+ return popen(command, type);
+}
+inline int _pclose(FILE* file)
+{
+ return pclose(file);
+}
+#endif
+
+string SMTSolverCommunicator::communicate(string const& _input)
+{
+ namespace fs = boost::filesystem;
+ auto tempPath = fs::unique_path(fs::temp_directory_path() / "%%%%-%%%%-%%%%.smt2");
+ ScopeGuard s1([&]() { fs::remove(tempPath); });
+ ofstream(tempPath.string()) << _input << "(exit)" << endl;
+
+ // TODO Escaping might not be 100% perfect.
+ FILE* solverOutput = _popen(("z3 -smt2 \"" + tempPath.string() + "\"").c_str(), "r");
+ ScopeGuard s2([&]() { _pclose(solverOutput); });
+
+ string result;
+ array<char, 128> buffer;
+ while (!feof(solverOutput))
+ if (fgets(buffer.data(), 127, solverOutput) != nullptr)
+ result += buffer.data();
+ return result;
+}
+
+#endif
diff --git a/libsolidity/formal/SMTSolverCommunicator.h b/libsolidity/formal/SMTSolverCommunicator.h
new file mode 100644
index 00000000..25aeba61
--- /dev/null
+++ b/libsolidity/formal/SMTSolverCommunicator.h
@@ -0,0 +1,50 @@
+/*
+ This file is part of solidity.
+
+ solidity is free software: you can redistribute it and/or modify
+ it under the terms of the GNU General Public License as published by
+ the Free Software Foundation, either version 3 of the License, or
+ (at your option) any later version.
+
+ solidity is distributed in the hope that it will be useful,
+ but WITHOUT ANY WARRANTY; without even the implied warranty of
+ MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ GNU General Public License for more details.
+
+ You should have received a copy of the GNU General Public License
+ along with solidity. If not, see <http://www.gnu.org/licenses/>.
+*/
+
+#pragma once
+
+#include <libsolidity/interface/ReadFile.h>
+
+#include <string>
+
+namespace dev
+{
+namespace solidity
+{
+namespace smt
+{
+
+/// Platform-specific way to access the SMT solver.
+class SMTSolverCommunicator
+{
+public:
+ /// Creates the communicator, the read file callback is used only
+ /// on the emscripten platform.
+ SMTSolverCommunicator(ReadFile::Callback const& _readFileCallback):
+ m_readFileCallback(_readFileCallback)
+ {}
+
+ std::string communicate(std::string const& _input);
+
+private:
+ ReadFile::Callback m_readFileCallback;
+};
+
+
+}
+}
+}
diff --git a/libsolidity/interface/CompilerStack.cpp b/libsolidity/interface/CompilerStack.cpp
index 4283cd99..50e20b3d 100644
--- a/libsolidity/interface/CompilerStack.cpp
+++ b/libsolidity/interface/CompilerStack.cpp
@@ -239,7 +239,7 @@ bool CompilerStack::analyze()
if (noErrors)
{
- SMTChecker smtChecker(m_errorReporter);
+ SMTChecker smtChecker(m_errorReporter, m_readFile);
for (Source const* source: m_sourceOrder)
smtChecker.analyze(*source->ast);
}
generated by cgit (git 2.34.1) at 2024-11-18 09:04:51 +0800