diff --git a/CMakeLists.txt b/CMakeLists.txt index 29ca63fe0..da14ddb77 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -16,7 +16,6 @@ option(SOLC_LINK_STATIC "Link solc executable statically on supported platforms" # Let's find our dependencies include(EthDependencies) include(deps/jsoncpp.cmake) -include(deps/z3.cmake) find_package(Threads) diff --git a/deps b/deps index cd9c6ff69..e5c8316db 160000 --- a/deps +++ b/deps @@ -1 +1 @@ -Subproject commit cd9c6ff69134e8f53bde70d92cce12ad294752de +Subproject commit e5c8316db8d3daa0abc3b5af8545ce330057608c diff --git a/libsolidity/formal/SMTCheckerImpl.cpp b/libsolidity/formal/SMTCheckerImpl.cpp index 028e4400a..b86a0279b 100644 --- a/libsolidity/formal/SMTCheckerImpl.cpp +++ b/libsolidity/formal/SMTCheckerImpl.cpp @@ -325,25 +325,40 @@ void SMTCheckerImpl::checkCondition( { m_interface.push(); m_interface.addAssertion(_condition); - switch (m_interface.check()) + + vector 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 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 << " = " << m_interface.eval(*_additionalValue) << "\n"; + message << " " << _additionalValueName << " = " << values.at(i++) << "\n"; for (auto const& param: m_currentFunction->parameters()) if (knownVariable(*param)) - message << " " << param->name() << " = " << m_interface.eval(currentValue(*param)) << "\n"; + message << " " << param->name() << " = " << values.at(i++) << "\n"; for (auto const& var: m_currentFunction->localVariables()) if (knownVariable(*var)) - message << " " << var->name() << " = " << m_interface.eval(currentValue(*var)) << "\n"; -// message << m << endl; -// message << m_solver << endl; + message << " " << var->name() << " = " << values.at(i++) << "\n"; } else message << "."; @@ -412,12 +427,12 @@ smt::Expression SMTCheckerImpl::newValue(const Declaration& _decl) smt::Expression SMTCheckerImpl::minValue(IntegerType const& _t) { - return m_interface.newInteger(_t.minValue()); + return smt::Expression(_t.minValue()); } smt::Expression SMTCheckerImpl::maxValue(IntegerType const& _t) { - return m_interface.newInteger(_t.maxValue()); + return smt::Expression(_t.maxValue()); } smt::Expression SMTCheckerImpl::expr(Expression const& _e) diff --git a/libsolidity/formal/SMTLib2Interface.cpp b/libsolidity/formal/SMTLib2Interface.cpp index c736ed2a3..8d40c3545 100644 --- a/libsolidity/formal/SMTLib2Interface.cpp +++ b/libsolidity/formal/SMTLib2Interface.cpp @@ -17,8 +17,230 @@ #include +#include + +#include +#include + +#include +#include +#include +#include +#include +#include +#include + +#include +#include +#include +#include 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() +{ + // 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"); +} + +void SMTLib2Interface::push() +{ + m_accumulatedOutput.emplace_back(); + //write("(push)\n"); +} + +void SMTLib2Interface::pop() +{ + //write("(pop)\n"); + 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") + + ")\n" + ); + return Expression(_name, {}); +} + +Expression SMTLib2Interface::newInteger(string _name) +{ + write("(declare-const |" + _name + "| Int)\n"); + return Expression(_name, {}); +} + +Expression SMTLib2Interface::newBool(string _name) +{ + write("(declare-const |" + _name + "| Bool)\n"); + return Expression(_name, {}); +} + +void SMTLib2Interface::addAssertion(Expression _expr) +{ + write("(assert " + _expr.toSExpr() + ")\n"); +} + +pair> SMTLib2Interface::check(vector 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); + CheckResult result; + // TODO proper parsing + if (boost::starts_with(response, "sat\n")) + result = CheckResult::SAT; + else if (boost::starts_with(response, "unsat\n")) + result = CheckResult::UNSAT; + else if (boost::starts_with(response, "unknown\n")) + result = CheckResult::UNKNOWN; + else + solAssert(false, "Invalid response to check-sat: " + response); + + vector values; + if (result != CheckResult::UNSAT) + 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); +} + +string SMTLib2Interface::communicate(std::string const& _input) +{ + ofstream("/tmp/z3exchange.smt2") << _input << "(exit)" << endl; + FILE* solverOutput = popen("z3 -smt2 /tmp/z3exchange.smt2", "r"); + string result; + array buffer; + while (!feof(solverOutput)) + if (fgets(buffer.data(), 127, solverOutput) != nullptr) + result += buffer.data(); + fclose(solverOutput); + return result; +} + +vector SMTLib2Interface::parseValues(string::const_iterator _start, string::const_iterator _end) +{ + vector 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; +} diff --git a/libsolidity/formal/SMTLib2Interface.h b/libsolidity/formal/SMTLib2Interface.h index f984cfb50..b7bab0437 100644 --- a/libsolidity/formal/SMTLib2Interface.h +++ b/libsolidity/formal/SMTLib2Interface.h @@ -17,11 +17,14 @@ #pragma once +#include + +#include + #include #include #include - -#include +#include namespace dev { @@ -49,7 +52,8 @@ class Expression public: Expression(size_t _number): m_name(std::to_string(_number)) {} - Expression(u256 const& _number): m_name(std::to_string(_number)) {} + Expression(u256 const& _number): m_name(_number.str()) {} + Expression(bigint const& _number): m_name(_number.str()) {} Expression(Expression const& _other) = default; Expression(Expression&& _other) = default; @@ -104,9 +108,16 @@ public: { return Expression("*", std::move(_a), std::move(_b)); } + Expression operator()(Expression _a) const + { + solAssert(m_arguments.empty(), "Attempted function application to non-function."); + return Expression(m_name, _a); + } std::string toSExpr() const { + if (m_arguments.empty()) + return m_name; std::string sexpr = "(" + m_name; for (auto const& arg: m_arguments) sexpr += " " + arg.toSExpr(); @@ -126,9 +137,11 @@ private: std::vector const m_arguments; }; -class SMTLib2Interface +class SMTLib2Interface: public boost::noncopyable { public: + SMTLib2Interface(); + ~SMTLib2Interface(); void reset(); @@ -140,8 +153,18 @@ public: Expression newBool(std::string _name); void addAssertion(Expression _expr); - CheckResult check(); - std::string eval(Expression _expr); + std::pair> check(std::vector const& _expressionsToEvaluate); +// std::string eval(Expression _expr); + +private: + void write(std::string _data); + std::string communicate(std::string const& _input); + + std::vector parseValues(std::string::const_iterator _start, std::string::const_iterator _end); + + std::vector m_accumulatedOutput; +// FILE* m_solverWrite = nullptr; +// FILE* m_solverRead = nullptr; };