diff --git a/libsmtutil/CHCSmtLib2Interface.cpp b/libsmtutil/CHCSmtLib2Interface.cpp index fb2423e5a..07ef19fac 100644 --- a/libsmtutil/CHCSmtLib2Interface.cpp +++ b/libsmtutil/CHCSmtLib2Interface.cpp @@ -19,6 +19,7 @@ #include #include +#include #include #include @@ -28,6 +29,7 @@ #include #include +#include #include #include @@ -116,9 +118,9 @@ tuple CHCSmtLib2Interface CheckResult result; // TODO proper parsing if (boost::starts_with(response, "sat")) - result = CheckResult::UNSATISFIABLE; + return {CheckResult::UNSATISFIABLE, parseInvariants(response), {}}; else if (boost::starts_with(response, "unsat")) - result = CheckResult::SATISFIABLE; + return {CheckResult::SATISFIABLE, Expression (true), parseCounterexample(response)}; else if (boost::starts_with(response, "unknown")) result = CheckResult::UNKNOWN; else @@ -127,6 +129,221 @@ tuple CHCSmtLib2Interface return {result, Expression(true), {}}; } +namespace +{ + +string readToken(string const& _data, size_t _pos) +{ + string r; + while (_pos < _data.size()) + { + char c = _data[_pos++]; + if (iswspace(unsigned(c)) || c == ',' || c == '(' || c == ')') + break; + r += c; + } + return r; +} + +size_t skipWhitespaces(string const& _data, size_t _pos) +{ + while (_pos < _data.size() && iswspace(unsigned(_data[_pos]))) + { + ++_pos; + } + + return _pos; +} + +/// @param _data here is always going to be either +/// - term +/// - term(args) +pair parseExpression(string const& _data) +{ + size_t pos = skipWhitespaces(_data, 0); + + string fname = readToken(_data, pos); + pos += fname.size(); + + if (pos >= _data.size() || _data[pos] != '(') + { + if (fname == "true" || fname == "false") + return {Expression(fname, {}, SortProvider::boolSort), pos}; + return {Expression(fname, {}, SortProvider::uintSort), pos}; + } + + smtAssert(_data[pos] == '('); + + vector exprArgs; + do + { + ++pos; + auto [arg, size] = parseExpression(_data.substr(pos)); + pos += size; + exprArgs.emplace_back(move(arg)); + smtAssert(_data[pos] == ',' || _data[pos] == ')'); + } while (_data[pos] == ','); + + smtAssert(_data[pos] == ')'); + ++pos; + + if (fname == "const") + fname = "const_array"; + + return {Expression(fname, move(exprArgs), SortProvider::uintSort), pos}; +} + +/// @param _data here is always going to be either +/// - term +/// - (term arg1 arg2 ... argk), where each arg is an sexpr. +pair parseSExpression(string const& _data) +{ + size_t pos = skipWhitespaces(_data, 0); + + vector exprArgs; + string fname; + if (_data[pos] != '(') + { + fname = readToken(_data, pos); + pos += fname.size(); + } + else + { + ++pos; + + string subExpr = _data.substr(pos); + string target = "(as const "; + if (boost::starts_with(subExpr, target)) + { + fname = "const_array"; + pos += target.size(); + auto [symbArg, newPos] = parseSExpression(_data.substr(pos)); + exprArgs.emplace_back(move(symbArg)); + pos += newPos; + ++pos; + } + else + { + fname = readToken(_data, pos); + pos += fname.size(); + } + + do + { + auto [symbArg, newPos] = parseSExpression(_data.substr(pos)); + exprArgs.emplace_back(move(symbArg)); + pos += newPos; + } while (_data[pos] != ')'); + ++pos; + } + + if (fname == "") + fname = "var-decl"; + else if (fname == "const") + fname = "const_array"; + + if (fname == "true" || fname == "false") + return {Expression(fname, {}, SortProvider::boolSort), pos}; + + return {Expression(fname, move(exprArgs), SortProvider::uintSort), pos}; +} + +smtutil::Expression parseDefineFun(string const& _data) +{ + auto [defineFun, pos] = parseSExpression(_data); + + vector newArgs; + Expression const& curArgs = defineFun.arguments.at(1); + smtAssert(curArgs.name == "var-decl"); + for (auto&& curArg: curArgs.arguments) + newArgs.emplace_back(move(curArg)); + + Expression predExpr{defineFun.arguments.at(0).name, move(newArgs), SortProvider::boolSort}; + + Expression& invExpr = defineFun.arguments.at(3); + + solidity::util::BreadthFirstSearch bfs{{&invExpr}}; + bfs.run([&](auto&& _expr, auto&& _addChild) { + if (_expr->name == "=") + { + smtAssert(_expr->arguments.size() == 2); + auto check = [](string const& _name) { + return boost::starts_with(_name, "mapping") && boost::ends_with(_name, "length"); + }; + if (check(_expr->arguments.at(0).name) || check(_expr->arguments.at(1).name)) + *_expr = Expression(true); + } + for (auto& arg: _expr->arguments) + _addChild(&arg); + }); + + Expression eq{"=", {move(predExpr), move(defineFun.arguments.at(3))}, SortProvider::boolSort}; + + return eq; +} + +} + +CHCSolverInterface::CexGraph CHCSmtLib2Interface::parseCounterexample(string const& _result) +{ + CHCSolverInterface::CexGraph cexGraph; + + for (auto&& line: _result | ranges::views::split('\n') | ranges::to>()) + { + string firstDelimiter = ": "; + string secondDelimiter = " -> "; + + size_t f = line.find(firstDelimiter); + if (f != string::npos) + { + string id = line.substr(0, f); + string rest = line.substr(f + firstDelimiter.size()); + + size_t s = rest.find(secondDelimiter); + string pred; + string adj; + if (s == string::npos) + pred = rest; + else + { + pred = rest.substr(0, s); + adj = rest.substr(s + secondDelimiter.size()); + } + + if (pred == "FALSE") + pred = "false"; + + unsigned iid = unsigned(stoi(id)); + + vector children; + for (auto&& v: adj | ranges::views::split(',') | ranges::to>()) + children.emplace_back(unsigned(stoi(v))); + + auto [expr, size] = parseExpression(pred); + + cexGraph.nodes.emplace(iid, move(expr)); + cexGraph.edges.emplace(iid, move(children)); + } + } + + return cexGraph; +} + +Expression CHCSmtLib2Interface::parseInvariants(string const& _result) +{ + vector eqs; + for (auto&& line: _result | ranges::views::split('\n') | ranges::to>()) + { + if (!boost::starts_with(line, "(define-fun")) + continue; + + eqs.emplace_back(parseDefineFun(line)); + } + + Expression conj{"and", move(eqs), SortProvider::boolSort}; + return conj; +} + void CHCSmtLib2Interface::declareVariable(string const& _name, SortPointer const& _sort) { smtAssert(_sort); diff --git a/libsmtutil/CHCSmtLib2Interface.h b/libsmtutil/CHCSmtLib2Interface.h index 4748af8da..d7f4c2925 100644 --- a/libsmtutil/CHCSmtLib2Interface.h +++ b/libsmtutil/CHCSmtLib2Interface.h @@ -69,6 +69,10 @@ private: /// Communicates with the solver via the callback. Throws SMTSolverError on error. std::string querySolver(std::string const& _input); + CHCSolverInterface::CexGraph parseCounterexample(std::string const& _result); + + Expression parseInvariants(std::string const& _result); + /// Used to access toSmtLibSort, SExpr, and handle variables. std::unique_ptr m_smtlib2; diff --git a/libsolidity/formal/Predicate.cpp b/libsolidity/formal/Predicate.cpp index cef6c82ae..6480eefb2 100644 --- a/libsolidity/formal/Predicate.cpp +++ b/libsolidity/formal/Predicate.cpp @@ -34,6 +34,7 @@ using namespace std; using boost::algorithm::starts_with; using namespace solidity; +using namespace solidity::util; using namespace solidity::smtutil; using namespace solidity::frontend; using namespace solidity::frontend::smt; @@ -506,7 +507,8 @@ optional Predicate::expressionToString(smtutil::Expression const& _expr, if (_expr.name == "0") return "0x0"; // For some reason the code below returns "0x" for "0". - return util::toHex(toCompactBigEndian(bigint(_expr.name)), util::HexPrefix::Add, util::HexCase::Lower); + return toHex(toCompactBigEndian(bigint(_expr.name)), HexPrefix::Add, HexCase::Lower); + //return formatNumberReadable(bigint(_expr.name)); } catch (out_of_range const&) { @@ -516,6 +518,7 @@ optional Predicate::expressionToString(smtutil::Expression const& _expr, } } + //return formatNumberReadable(bigint(_expr.name)); return _expr.name; } if (smt::isBool(*_type)) diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp index 9c7537cd0..a8d2ab04b 100644 --- a/libsolidity/formal/SMTEncoder.cpp +++ b/libsolidity/formal/SMTEncoder.cpp @@ -1070,6 +1070,7 @@ bool SMTEncoder::shouldAnalyze(ContractDefinition const& _contract) const return false; return m_settings.contracts.isDefault() || + //m_settings.contracts.has(_contract.sourceUnitName(), _contract.name()); m_settings.contracts.has(_contract.sourceUnitName()); } diff --git a/libsolidity/formal/SymbolicState.cpp b/libsolidity/formal/SymbolicState.cpp index 3b613b75f..db3bfe6c6 100644 --- a/libsolidity/formal/SymbolicState.cpp +++ b/libsolidity/formal/SymbolicState.cpp @@ -441,6 +441,15 @@ void SymbolicState::buildABIFunctions(setrichIdentifier(); + while (name.find(" => ") != string::npos) + name.replace(name.find(" => "), 4, ""); + while (name.find('(') != string::npos) + name.replace(name.find('('), 1, "$"); + while (name.find(')') != string::npos) + name.replace(name.find(')'), 1, "$"); + while (name.find(',') != string::npos) + name.replace(name.find(','), 1, "$"); + m_abiMembers[funCall] = {name, inTypes, outTypes}; if (functions.count(name)) diff --git a/libsolidity/formal/SymbolicTypes.cpp b/libsolidity/formal/SymbolicTypes.cpp index b66ff9f40..9826407f0 100644 --- a/libsolidity/formal/SymbolicTypes.cpp +++ b/libsolidity/formal/SymbolicTypes.cpp @@ -123,6 +123,15 @@ SortPointer smtSort(frontend::Type const& _type) else tupleName = _type.toString(true); + while (tupleName.find(" => ") != string::npos) + tupleName.replace(tupleName.find(" => "), 4, ""); + while (tupleName.find('(') != string::npos) + tupleName.replace(tupleName.find('('), 1, "$"); + while (tupleName.find(')') != string::npos) + tupleName.replace(tupleName.find(')'), 1, "$"); + while (tupleName.find(',') != string::npos) + tupleName.replace(tupleName.find(','), 1, "$"); + tupleName += "_tuple"; return make_shared( @@ -134,9 +143,18 @@ SortPointer smtSort(frontend::Type const& _type) case Kind::Tuple: { vector members; - auto const& tupleName = _type.toString(true); + string tupleName = _type.toString(true); vector sorts; + while (tupleName.find(" => ") != string::npos) + tupleName.replace(tupleName.find(" => "), 4, ""); + while (tupleName.find('(') != string::npos) + tupleName.replace(tupleName.find('('), 1, "$"); + while (tupleName.find(')') != string::npos) + tupleName.replace(tupleName.find(')'), 1, "$"); + while (tupleName.find(',') != string::npos) + tupleName.replace(tupleName.find(','), 1, "$"); + if (auto const* tupleType = dynamic_cast(&_type)) { auto const& components = tupleType->components(); diff --git a/libsolutil/StringUtils.h b/libsolutil/StringUtils.h index 7a48c296f..932dc8381 100644 --- a/libsolutil/StringUtils.h +++ b/libsolutil/StringUtils.h @@ -145,16 +145,32 @@ inline std::string formatNumberReadable( // when multiple trailing FF bytes, format as N * 2**x - 1 i = 0; - for (v = _value; (v & 0xff) == 0xff; v >>= 8) + std::string minus; + v = _value; + if ((v & 0xff) == 0xfe) + { + ++i; + minus = "2"; + v >>= 8; + } + else if ((v & 0xff) == 0xfd) + { + ++i; + minus = "3"; + v >>= 8; + } + else + minus = "1"; + for (; (v & 0xff) == 0xff; v >>= 8) ++i; if (i > 2) { // 0xFF yields 2**8 - 1 (v is 0 in that case) if (v == 0) - return "2**" + std::to_string(i * 8) + " - 1"; + return "2**" + std::to_string(i * 8) + " - " + minus;//1"; return toHex(toCompactBigEndian(T(v + 1)), prefix, hexcase) + " * 2**" + std::to_string(i * 8) + - " - 1"; + " - " + minus;//1"; } std::string str = toHex(toCompactBigEndian(_value), prefix, hexcase);