From ce72d7cd262478871a9dd199681a005f00f0f8bb Mon Sep 17 00:00:00 2001 From: Leo Alt Date: Wed, 6 Oct 2021 11:46:45 +0200 Subject: [PATCH] Add ExpressionFormatter which translates an smtutil::Expression into a Solidity-like expression string --- libsolidity/formal/ExpressionFormatter.cpp | 184 +++++++++++++++++++++ libsolidity/formal/ExpressionFormatter.h | 41 +++++ 2 files changed, 225 insertions(+) create mode 100644 libsolidity/formal/ExpressionFormatter.cpp create mode 100644 libsolidity/formal/ExpressionFormatter.h diff --git a/libsolidity/formal/ExpressionFormatter.cpp b/libsolidity/formal/ExpressionFormatter.cpp new file mode 100644 index 000000000..2591328f8 --- /dev/null +++ b/libsolidity/formal/ExpressionFormatter.cpp @@ -0,0 +1,184 @@ +/* + 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 . +*/ +// SPDX-License-Identifier: GPL-3.0 + +#include + +#include +#include + +#include + +#include + +#include +#include +#include + +using namespace std; +using boost::algorithm::starts_with; +using namespace solidity; +using namespace solidity::util; +using namespace solidity::smtutil; +using namespace solidity::frontend::smt; + +namespace solidity::frontend::smt +{ + +namespace +{ + +string formatDatatypeAccessor(smtutil::Expression const& _expr, vector const& _args) +{ + auto const& op = _expr.name; + + // This is the most complicated part of the translation. + // Datatype accessor means access to a field of a datatype. + // In our encoding, datatypes are used to encode: + // - arrays/mappings as the tuple (array, length) + // - structs as the tuple (, ..., ) + // - hash and signature functions as the tuple (keccak256, sha256, ripemd160, ecrecover), + // where each element is an array emulating an UF + // - abi.* functions as the tuple (, ..., ). + if (op == "dt_accessor_keccak256") + return "keccak256"; + if (op == "dt_accessor_sha256") + return "sha256"; + if (op == "dt_accessor_ripemd160") + return "ripemd160"; + if (op == "dt_accessor_ecrecover") + return "ecrecover"; + + string accessorStr = "accessor_"; + // Struct members have suffix "accessor_". + string type = op.substr(op.rfind(accessorStr) + accessorStr.size()); + solAssert(_expr.arguments.size() == 1, ""); + + if (type == "length") + return _args.at(0) + ".length"; + if (type == "array") + return _args.at(0); + + if ( + starts_with(type, "block") || + starts_with(type, "msg") || + starts_with(type, "tx") || + starts_with(type, "abi") + ) + return type; + + if (starts_with(type, "t_function_abi")) + return type; + + return _args.at(0) + "." + type; +} + +string formatGenericOp(smtutil::Expression const& _expr, vector const& _args) +{ + return _expr.name + "(" + boost::algorithm::join(_args, ", ") + ")"; +} + +string formatInfixOp(string const& _op, vector const& _args) +{ + return "(" + boost::algorithm::join(_args, " " + _op + " ") + ")"; +} + +string formatArrayOp(smtutil::Expression const& _expr, vector const& _args) +{ + if (_expr.name == "select") + { + auto const& a0 = _args.at(0); + static set const ufs{"keccak256", "sha256", "ripemd160", "ecrecover"}; + if (ufs.count(a0) || starts_with(a0, "t_function_abi")) + return _args.at(0) + "(" + _args.at(1) + ")"; + return _args.at(0) + "[" + _args.at(1) + "]"; + } + if (_expr.name == "store") + return "(" + _args.at(0) + "[" + _args.at(1) + "] := " + _args.at(2) + ")"; + return formatGenericOp(_expr, _args); +} + +string formatUnaryOp(smtutil::Expression const& _expr, vector const& _args) +{ + if (_expr.name == "not") + return "!" + _args.at(0); + // Other operators such as exists may end up here. + return formatGenericOp(_expr, _args); +} + +} + +smtutil::Expression substitute(smtutil::Expression _from, map const& _subst) +{ + // TODO For now we ignore nested quantifier expressions, + // but we should support them in the future. + if (_from.name == "forall" || _from.name == "exists") + return smtutil::Expression(true); + if (_subst.count(_from.name)) + _from.name = _subst.at(_from.name); + for (auto& arg: _from.arguments) + arg = substitute(arg, _subst); + return _from; +} + +string toSolidityStr(smtutil::Expression const& _expr) +{ + auto const& op = _expr.name; + + auto const& args = _expr.arguments; + auto strArgs = util::applyMap(args, [](auto const& _arg) { return toSolidityStr(_arg); }); + + // Constant or variable. + if (args.empty()) + return op; + + if (starts_with(op, "dt_accessor")) + return formatDatatypeAccessor(_expr, strArgs); + + // Infix operators with format replacements. + static map const infixOps{ + {"and", "&&"}, + {"or", "||"}, + {"implies", "=>"}, + {"=", "="}, + {">", ">"}, + {">=", ">="}, + {"<", "<"}, + {"<=", "<="}, + {"+", "+"}, + {"-", "-"}, + {"*", "*"}, + {"/", "/"}, + {"div", "/"}, + {"mod", "%"} + }; + // Some of these (and, or, +, *) may have >= 2 arguments from z3. + if (infixOps.count(op)) + return formatInfixOp(infixOps.at(op), strArgs); + + static set const arrayOps{"select", "store", "const_array"}; + if (arrayOps.count(op)) + return formatArrayOp(_expr, strArgs); + + if (args.size() == 1) + return formatUnaryOp(_expr, strArgs); + + // Other operators such as bv2int, int2bv may end up here. + return op + "(" + boost::algorithm::join(strArgs, ", ") + ")"; +} + +} diff --git a/libsolidity/formal/ExpressionFormatter.h b/libsolidity/formal/ExpressionFormatter.h new file mode 100644 index 000000000..3efbeb781 --- /dev/null +++ b/libsolidity/formal/ExpressionFormatter.h @@ -0,0 +1,41 @@ +/* + 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 . +*/ +// SPDX-License-Identifier: GPL-3.0 + +#pragma once + +/** + * Formats SMT expressions into Solidity-like strings. + */ + +#include + +#include +#include + +namespace solidity::frontend::smt +{ + +/// @returns another smtutil::Expressions where every term in _from +/// may be replaced if it is in the substitution map _subst. +smtutil::Expression substitute(smtutil::Expression _from, std::map const& _subst); + +/// @returns a Solidity-like expression string built from _expr. +/// This is done at best-effort and is not guaranteed to always create a perfect Solidity expression string. +std::string toSolidityStr(smtutil::Expression const& _expr); + +}