solidity/libsolidity/formal/ExpressionFormatter.cpp

185 lines
5.1 KiB
C++
Raw Normal View History

/*
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/>.
*/
// SPDX-License-Identifier: GPL-3.0
#include <libsolidity/formal/ExpressionFormatter.h>
#include <libsolutil/Algorithms.h>
#include <libsolutil/CommonData.h>
#include <boost/algorithm/string.hpp>
#include <range/v3/algorithm/for_each.hpp>
#include <map>
#include <vector>
#include <string>
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<string> 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 (<member1>, ..., <memberK>)
// - 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 (<abiCall1>, ..., <abiCallK>).
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_<memberName>".
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<string> const& _args)
{
return _expr.name + "(" + boost::algorithm::join(_args, ", ") + ")";
}
string formatInfixOp(string const& _op, vector<string> const& _args)
{
return "(" + boost::algorithm::join(_args, " " + _op + " ") + ")";
}
string formatArrayOp(smtutil::Expression const& _expr, vector<string> const& _args)
{
if (_expr.name == "select")
{
auto const& a0 = _args.at(0);
static set<string> 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<string> 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<string, string> 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<string, string> 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<string> 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, ", ") + ")";
}
}