1 /*
2 This file is part of solidity.
3
4 solidity is free software: you can redistribute it and/or modify
5 it under the terms of the GNU General Public License as published by
6 the Free Software Foundation, either version 3 of the License, or
7 (at your option) any later version.
8
9 solidity is distributed in the hope that it will be useful,
10 but WITHOUT ANY WARRANTY; without even the implied warranty of
11 MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
12 GNU General Public License for more details.
13
14 You should have received a copy of the GNU General Public License
15 along with solidity. If not, see <http://www.gnu.org/licenses/>.
16 */
17 // SPDX-License-Identifier: GPL-3.0
18
19 #include <libsolidity/formal/ExpressionFormatter.h>
20
21 #include <libsolutil/Algorithms.h>
22 #include <libsolutil/CommonData.h>
23
24 #include <boost/algorithm/string.hpp>
25
26 #include <range/v3/algorithm/for_each.hpp>
27
28 #include <map>
29 #include <vector>
30 #include <string>
31
32 using namespace std;
33 using boost::algorithm::starts_with;
34 using namespace solidity;
35 using namespace solidity::util;
36 using namespace solidity::smtutil;
37 using namespace solidity::frontend::smt;
38
39 namespace solidity::frontend::smt
40 {
41
42 namespace
43 {
44
formatDatatypeAccessor(smtutil::Expression const & _expr,vector<string> const & _args)45 string formatDatatypeAccessor(smtutil::Expression const& _expr, vector<string> const& _args)
46 {
47 auto const& op = _expr.name;
48
49 // This is the most complicated part of the translation.
50 // Datatype accessor means access to a field of a datatype.
51 // In our encoding, datatypes are used to encode:
52 // - arrays/mappings as the tuple (array, length)
53 // - structs as the tuple (<member1>, ..., <memberK>)
54 // - hash and signature functions as the tuple (keccak256, sha256, ripemd160, ecrecover),
55 // where each element is an array emulating an UF
56 // - abi.* functions as the tuple (<abiCall1>, ..., <abiCallK>).
57 if (op == "dt_accessor_keccak256")
58 return "keccak256";
59 if (op == "dt_accessor_sha256")
60 return "sha256";
61 if (op == "dt_accessor_ripemd160")
62 return "ripemd160";
63 if (op == "dt_accessor_ecrecover")
64 return "ecrecover";
65
66 string accessorStr = "accessor_";
67 // Struct members have suffix "accessor_<memberName>".
68 string type = op.substr(op.rfind(accessorStr) + accessorStr.size());
69 solAssert(_expr.arguments.size() == 1, "");
70
71 if (type == "length")
72 return _args.at(0) + ".length";
73 if (type == "array")
74 return _args.at(0);
75
76 if (
77 starts_with(type, "block") ||
78 starts_with(type, "msg") ||
79 starts_with(type, "tx") ||
80 starts_with(type, "abi")
81 )
82 return type;
83
84 if (starts_with(type, "t_function_abi"))
85 return type;
86
87 return _args.at(0) + "." + type;
88 }
89
formatGenericOp(smtutil::Expression const & _expr,vector<string> const & _args)90 string formatGenericOp(smtutil::Expression const& _expr, vector<string> const& _args)
91 {
92 return _expr.name + "(" + boost::algorithm::join(_args, ", ") + ")";
93 }
94
formatInfixOp(string const & _op,vector<string> const & _args)95 string formatInfixOp(string const& _op, vector<string> const& _args)
96 {
97 return "(" + boost::algorithm::join(_args, " " + _op + " ") + ")";
98 }
99
formatArrayOp(smtutil::Expression const & _expr,vector<string> const & _args)100 string formatArrayOp(smtutil::Expression const& _expr, vector<string> const& _args)
101 {
102 if (_expr.name == "select")
103 {
104 auto const& a0 = _args.at(0);
105 static set<string> const ufs{"keccak256", "sha256", "ripemd160", "ecrecover"};
106 if (ufs.count(a0) || starts_with(a0, "t_function_abi"))
107 return _args.at(0) + "(" + _args.at(1) + ")";
108 return _args.at(0) + "[" + _args.at(1) + "]";
109 }
110 if (_expr.name == "store")
111 return "(" + _args.at(0) + "[" + _args.at(1) + "] := " + _args.at(2) + ")";
112 return formatGenericOp(_expr, _args);
113 }
114
formatUnaryOp(smtutil::Expression const & _expr,vector<string> const & _args)115 string formatUnaryOp(smtutil::Expression const& _expr, vector<string> const& _args)
116 {
117 if (_expr.name == "not")
118 return "!" + _args.at(0);
119 // Other operators such as exists may end up here.
120 return formatGenericOp(_expr, _args);
121 }
122
123 }
124
substitute(smtutil::Expression _from,map<string,string> const & _subst)125 smtutil::Expression substitute(smtutil::Expression _from, map<string, string> const& _subst)
126 {
127 // TODO For now we ignore nested quantifier expressions,
128 // but we should support them in the future.
129 if (_from.name == "forall" || _from.name == "exists")
130 return smtutil::Expression(true);
131 if (_subst.count(_from.name))
132 _from.name = _subst.at(_from.name);
133 for (auto& arg: _from.arguments)
134 arg = substitute(arg, _subst);
135 return _from;
136 }
137
toSolidityStr(smtutil::Expression const & _expr)138 string toSolidityStr(smtutil::Expression const& _expr)
139 {
140 auto const& op = _expr.name;
141
142 auto const& args = _expr.arguments;
143 auto strArgs = util::applyMap(args, [](auto const& _arg) { return toSolidityStr(_arg); });
144
145 // Constant or variable.
146 if (args.empty())
147 return op;
148
149 if (starts_with(op, "dt_accessor"))
150 return formatDatatypeAccessor(_expr, strArgs);
151
152 // Infix operators with format replacements.
153 static map<string, string> const infixOps{
154 {"and", "&&"},
155 {"or", "||"},
156 {"implies", "=>"},
157 {"=", "="},
158 {">", ">"},
159 {">=", ">="},
160 {"<", "<"},
161 {"<=", "<="},
162 {"+", "+"},
163 {"-", "-"},
164 {"*", "*"},
165 {"/", "/"},
166 {"div", "/"},
167 {"mod", "%"}
168 };
169 // Some of these (and, or, +, *) may have >= 2 arguments from z3.
170 if (infixOps.count(op))
171 return formatInfixOp(infixOps.at(op), strArgs);
172
173 static set<string> const arrayOps{"select", "store", "const_array"};
174 if (arrayOps.count(op))
175 return formatArrayOp(_expr, strArgs);
176
177 if (args.size() == 1)
178 return formatUnaryOp(_expr, strArgs);
179
180 // Other operators such as bv2int, int2bv may end up here.
181 return op + "(" + boost::algorithm::join(strArgs, ", ") + ")";
182 }
183
184 }
185