aboutsummaryrefslogtreecommitdiffstats
path: root/libsolidity/formal
diff options
context:
space:
mode:
Diffstat (limited to 'libsolidity/formal')
-rw-r--r--libsolidity/formal/CVC4Interface.cpp200
-rw-r--r--libsolidity/formal/CVC4Interface.h62
-rw-r--r--libsolidity/formal/SMTChecker.cpp8
-rw-r--r--libsolidity/formal/SolverInterface.h20
-rw-r--r--libsolidity/formal/Z3Interface.cpp17
-rw-r--r--libsolidity/formal/Z3Interface.h3
6 files changed, 289 insertions, 21 deletions
diff --git a/libsolidity/formal/CVC4Interface.cpp b/libsolidity/formal/CVC4Interface.cpp
new file mode 100644
index 00000000..dba5823a
--- /dev/null
+++ b/libsolidity/formal/CVC4Interface.cpp
@@ -0,0 +1,200 @@
+/*
+ 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/CVC4Interface.h>
+
+#include <libsolidity/interface/Exceptions.h>
+
+#include <libdevcore/CommonIO.h>
+
+using namespace std;
+using namespace dev;
+using namespace dev::solidity::smt;
+
+CVC4Interface::CVC4Interface():
+ m_solver(&m_context)
+{
+ reset();
+}
+
+void CVC4Interface::reset()
+{
+ m_constants.clear();
+ m_functions.clear();
+ m_solver.reset();
+ m_solver.setOption("produce-models", true);
+}
+
+void CVC4Interface::push()
+{
+ m_solver.push();
+}
+
+void CVC4Interface::pop()
+{
+ m_solver.pop();
+}
+
+Expression CVC4Interface::newFunction(string _name, Sort _domain, Sort _codomain)
+{
+ CVC4::Type fType = m_context.mkFunctionType(cvc4Sort(_domain), cvc4Sort(_codomain));
+ m_functions.insert({_name, m_context.mkVar(_name.c_str(), fType)});
+ return SolverInterface::newFunction(move(_name), _domain, _codomain);
+}
+
+Expression CVC4Interface::newInteger(string _name)
+{
+ m_constants.insert({_name, m_context.mkVar(_name.c_str(), m_context.integerType())});
+ return SolverInterface::newInteger(move(_name));
+}
+
+Expression CVC4Interface::newBool(string _name)
+{
+ m_constants.insert({_name, m_context.mkVar(_name.c_str(), m_context.booleanType())});
+ return SolverInterface::newBool(std::move(_name));
+}
+
+void CVC4Interface::addAssertion(Expression const& _expr)
+{
+ try
+ {
+ m_solver.assertFormula(toCVC4Expr(_expr));
+ }
+ catch (CVC4::TypeCheckingException const&)
+ {
+ solAssert(false, "");
+ }
+ catch (CVC4::LogicException const&)
+ {
+ solAssert(false, "");
+ }
+ catch (CVC4::UnsafeInterruptException const&)
+ {
+ solAssert(false, "");
+ }
+}
+
+pair<CheckResult, vector<string>> CVC4Interface::check(vector<Expression> const& _expressionsToEvaluate)
+{
+ CheckResult result;
+ vector<string> values;
+ try
+ {
+ switch (m_solver.checkSat().isSat())
+ {
+ case CVC4::Result::SAT:
+ result = CheckResult::SATISFIABLE;
+ break;
+ case CVC4::Result::UNSAT:
+ result = CheckResult::UNSATISFIABLE;
+ break;
+ case CVC4::Result::SAT_UNKNOWN:
+ result = CheckResult::UNKNOWN;
+ break;
+ default:
+ solAssert(false, "");
+ }
+
+ if (result != CheckResult::UNSATISFIABLE && !_expressionsToEvaluate.empty())
+ {
+ for (Expression const& e: _expressionsToEvaluate)
+ values.push_back(toString(m_solver.getValue(toCVC4Expr(e))));
+ }
+ }
+ catch (CVC4::Exception & e)
+ {
+ result = CheckResult::ERROR;
+ values.clear();
+ }
+
+ return make_pair(result, values);
+}
+
+CVC4::Expr CVC4Interface::toCVC4Expr(Expression const& _expr)
+{
+ if (_expr.arguments.empty() && m_constants.count(_expr.name))
+ return m_constants.at(_expr.name);
+ vector<CVC4::Expr> arguments;
+ for (auto const& arg: _expr.arguments)
+ arguments.push_back(toCVC4Expr(arg));
+
+ string const& n = _expr.name;
+ if (m_functions.count(n))
+ return m_context.mkExpr(CVC4::kind::APPLY_UF, m_functions[n], arguments);
+ else if (m_constants.count(n))
+ {
+ solAssert(arguments.empty(), "");
+ return m_constants.at(n);
+ }
+ else if (arguments.empty())
+ {
+ if (n == "true")
+ return m_context.mkConst(true);
+ else if (n == "false")
+ return m_context.mkConst(false);
+ else
+ // We assume it is an integer...
+ return m_context.mkConst(CVC4::Rational(n));
+ }
+
+ solAssert(_expr.hasCorrectArity(), "");
+ if (n == "ite")
+ return arguments[0].iteExpr(arguments[1], arguments[2]);
+ else if (n == "not")
+ return arguments[0].notExpr();
+ else if (n == "and")
+ return arguments[0].andExpr(arguments[1]);
+ else if (n == "or")
+ return arguments[0].orExpr(arguments[1]);
+ else if (n == "=")
+ return m_context.mkExpr(CVC4::kind::EQUAL, arguments[0], arguments[1]);
+ else if (n == "<")
+ return m_context.mkExpr(CVC4::kind::LT, arguments[0], arguments[1]);
+ else if (n == "<=")
+ return m_context.mkExpr(CVC4::kind::LEQ, arguments[0], arguments[1]);
+ else if (n == ">")
+ return m_context.mkExpr(CVC4::kind::GT, arguments[0], arguments[1]);
+ else if (n == ">=")
+ return m_context.mkExpr(CVC4::kind::GEQ, arguments[0], arguments[1]);
+ else if (n == "+")
+ return m_context.mkExpr(CVC4::kind::PLUS, arguments[0], arguments[1]);
+ else if (n == "-")
+ return m_context.mkExpr(CVC4::kind::MINUS, arguments[0], arguments[1]);
+ else if (n == "*")
+ return m_context.mkExpr(CVC4::kind::MULT, arguments[0], arguments[1]);
+ else if (n == "/")
+ return m_context.mkExpr(CVC4::kind::INTS_DIVISION_TOTAL, arguments[0], arguments[1]);
+ // Cannot reach here.
+ solAssert(false, "");
+ return arguments[0];
+}
+
+CVC4::Type CVC4Interface::cvc4Sort(Sort _sort)
+{
+ switch (_sort)
+ {
+ case Sort::Bool:
+ return m_context.booleanType();
+ case Sort::Int:
+ return m_context.integerType();
+ default:
+ break;
+ }
+ solAssert(false, "");
+ // Cannot be reached.
+ return m_context.integerType();
+}
diff --git a/libsolidity/formal/CVC4Interface.h b/libsolidity/formal/CVC4Interface.h
new file mode 100644
index 00000000..cfaeb412
--- /dev/null
+++ b/libsolidity/formal/CVC4Interface.h
@@ -0,0 +1,62 @@
+/*
+ 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 <cvc4/cvc4.h>
+
+namespace dev
+{
+namespace solidity
+{
+namespace smt
+{
+
+class CVC4Interface: public SolverInterface, public boost::noncopyable
+{
+public:
+ CVC4Interface();
+
+ 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:
+ CVC4::Expr toCVC4Expr(Expression const& _expr);
+ CVC4::Type cvc4Sort(smt::Sort _sort);
+
+ CVC4::ExprManager m_context;
+ CVC4::SmtEngine m_solver;
+ std::map<std::string, CVC4::Expr> m_constants;
+ std::map<std::string, CVC4::Expr> m_functions;
+};
+
+}
+}
+}
diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp
index 8f4abdc2..777e57c3 100644
--- a/libsolidity/formal/SMTChecker.cpp
+++ b/libsolidity/formal/SMTChecker.cpp
@@ -19,6 +19,8 @@
#ifdef HAVE_Z3
#include <libsolidity/formal/Z3Interface.h>
+#elif HAVE_CVC4
+#include <libsolidity/formal/CVC4Interface.h>
#else
#include <libsolidity/formal/SMTLib2Interface.h>
#endif
@@ -39,6 +41,8 @@ using namespace dev::solidity;
SMTChecker::SMTChecker(ErrorReporter& _errorReporter, ReadCallback::Callback const& _readFileCallback):
#ifdef HAVE_Z3
m_interface(make_shared<smt::Z3Interface>()),
+#elif HAVE_CVC4
+ m_interface(make_shared<smt::CVC4Interface>()),
#else
m_interface(make_shared<smt::SMTLib2Interface>(_readFileCallback)),
#endif
@@ -464,7 +468,7 @@ void SMTChecker::compareOperation(BinaryOperation const& _op)
}
else // Bool
{
- solAssert(SSAVariable::isBool(_op.annotation().commonType->category()), "");
+ solUnimplementedAssert(SSAVariable::isBool(_op.annotation().commonType->category()), "Operation not yet supported");
value = make_shared<smt::Expression>(
op == Token::Equal ? (left == right) :
op == Token::NotEqual ? (left != right) :
@@ -835,7 +839,7 @@ void SMTChecker::createExpr(Expression const& _e)
m_expressions.emplace(&_e, m_interface->newBool(uniqueSymbol(_e)));
break;
default:
- solAssert(false, "Type not implemented.");
+ solUnimplementedAssert(false, "Type not implemented.");
}
}
}
diff --git a/libsolidity/formal/SolverInterface.h b/libsolidity/formal/SolverInterface.h
index 0bdebb6c..e127bb55 100644
--- a/libsolidity/formal/SolverInterface.h
+++ b/libsolidity/formal/SolverInterface.h
@@ -65,6 +65,26 @@ public:
Expression& operator=(Expression const&) = default;
Expression& operator=(Expression&&) = default;
+ bool hasCorrectArity() const
+ {
+ static std::map<std::string, unsigned> const operatorsArity{
+ {"ite", 3},
+ {"not", 1},
+ {"and", 2},
+ {"or", 2},
+ {"=", 2},
+ {"<", 2},
+ {"<=", 2},
+ {">", 2},
+ {">=", 2},
+ {"+", 2},
+ {"-", 2},
+ {"*", 2},
+ {"/", 2}
+ };
+ return operatorsArity.count(name) && operatorsArity.at(name) == arguments.size();
+ }
+
static Expression ite(Expression _condition, Expression _trueValue, Expression _falseValue)
{
solAssert(_trueValue.sort == _falseValue.sort, "");
diff --git a/libsolidity/formal/Z3Interface.cpp b/libsolidity/formal/Z3Interface.cpp
index 125da00d..41943c92 100644
--- a/libsolidity/formal/Z3Interface.cpp
+++ b/libsolidity/formal/Z3Interface.cpp
@@ -116,21 +116,6 @@ z3::expr Z3Interface::toZ3Expr(Expression const& _expr)
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);
@@ -150,7 +135,7 @@ z3::expr Z3Interface::toZ3Expr(Expression const& _expr)
return m_context.int_val(n.c_str());
}
- solAssert(arity.count(n) && arity.at(n) == arguments.size(), "");
+ solAssert(_expr.hasCorrectArity(), "");
if (n == "ite")
return z3::ite(arguments[0], arguments[1], arguments[2]);
else if (n == "not")
diff --git a/libsolidity/formal/Z3Interface.h b/libsolidity/formal/Z3Interface.h
index 44d4bb2f..354ded25 100644
--- a/libsolidity/formal/Z3Interface.h
+++ b/libsolidity/formal/Z3Interface.h
@@ -51,9 +51,6 @@ 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;
generated by cgit (git 2.34.1) at 2024-11-18 07:26:42 +0800