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/SymbolicState.h>
20
21 #include <libsolidity/formal/SymbolicTypes.h>
22 #include <libsolidity/formal/EncodingContext.h>
23 #include <libsolidity/formal/SMTEncoder.h>
24
25 using namespace std;
26 using namespace solidity;
27 using namespace solidity::smtutil;
28 using namespace solidity::frontend::smt;
29
BlockchainVariable(string _name,map<string,smtutil::SortPointer> _members,EncodingContext & _context)30 BlockchainVariable::BlockchainVariable(
31 string _name,
32 map<string, smtutil::SortPointer> _members,
33 EncodingContext& _context
34 ):
35 m_name(move(_name)),
36 m_members(move(_members)),
37 m_context(_context)
38 {
39 vector<string> members;
40 vector<SortPointer> sorts;
41 for (auto const& [component, sort]: m_members)
42 {
43 members.emplace_back(component);
44 sorts.emplace_back(sort);
45 m_componentIndices[component] = static_cast<unsigned>(members.size() - 1);
46 }
47 m_tuple = make_unique<SymbolicTupleVariable>(
48 make_shared<smtutil::TupleSort>(m_name + "_type", members, sorts),
49 m_name,
50 m_context
51 );
52 }
53
member(string const & _member) const54 smtutil::Expression BlockchainVariable::member(string const& _member) const
55 {
56 return m_tuple->component(m_componentIndices.at(_member));
57 }
58
assignMember(string const & _member,smtutil::Expression const & _value)59 smtutil::Expression BlockchainVariable::assignMember(string const& _member, smtutil::Expression const& _value)
60 {
61 vector<smtutil::Expression> args;
62 for (auto const& m: m_members)
63 if (m.first == _member)
64 args.emplace_back(_value);
65 else
66 args.emplace_back(member(m.first));
67 m_tuple->increaseIndex();
68 auto tuple = m_tuple->currentValue();
69 auto sortExpr = smtutil::Expression(make_shared<smtutil::SortSort>(tuple.sort), tuple.name);
70 m_context.addAssertion(tuple == smtutil::Expression::tuple_constructor(sortExpr, args));
71 return m_tuple->currentValue();
72 }
73
reset()74 void SymbolicState::reset()
75 {
76 m_error.resetIndex();
77 m_thisAddress.resetIndex();
78 m_state.reset();
79 m_tx.reset();
80 m_crypto.reset();
81 if (m_abi)
82 m_abi->reset();
83 }
84
balances() const85 smtutil::Expression SymbolicState::balances() const
86 {
87 return m_state.member("balances");
88 }
89
balance() const90 smtutil::Expression SymbolicState::balance() const
91 {
92 return balance(thisAddress());
93 }
94
balance(smtutil::Expression _address) const95 smtutil::Expression SymbolicState::balance(smtutil::Expression _address) const
96 {
97 return smtutil::Expression::select(balances(), move(_address));
98 }
99
blockhash(smtutil::Expression _blockNumber) const100 smtutil::Expression SymbolicState::blockhash(smtutil::Expression _blockNumber) const
101 {
102 return smtutil::Expression::select(m_tx.member("blockhash"), move(_blockNumber));
103 }
104
newBalances()105 void SymbolicState::newBalances()
106 {
107 auto tupleSort = dynamic_pointer_cast<TupleSort>(stateSort());
108 auto balanceSort = tupleSort->components.at(tupleSort->memberToIndex.at("balances"));
109 SymbolicVariable newBalances(balanceSort, "fresh_balances_" + to_string(m_context.newUniqueId()), m_context);
110 m_state.assignMember("balances", newBalances.currentValue());
111 }
112
transfer(smtutil::Expression _from,smtutil::Expression _to,smtutil::Expression _value)113 void SymbolicState::transfer(smtutil::Expression _from, smtutil::Expression _to, smtutil::Expression _value)
114 {
115 unsigned indexBefore = m_state.index();
116 addBalance(_from, 0 - _value);
117 addBalance(_to, move(_value));
118 unsigned indexAfter = m_state.index();
119 solAssert(indexAfter > indexBefore, "");
120 m_state.newVar();
121 /// Do not apply the transfer operation if _from == _to.
122 auto newState = smtutil::Expression::ite(
123 move(_from) == move(_to),
124 m_state.value(indexBefore),
125 m_state.value(indexAfter)
126 );
127 m_context.addAssertion(m_state.value() == newState);
128 }
129
addBalance(smtutil::Expression _address,smtutil::Expression _value)130 void SymbolicState::addBalance(smtutil::Expression _address, smtutil::Expression _value)
131 {
132 auto newBalances = smtutil::Expression::store(
133 balances(),
134 _address,
135 balance(_address) + move(_value)
136 );
137 m_state.assignMember("balances", newBalances);
138 }
139
txMember(string const & _member) const140 smtutil::Expression SymbolicState::txMember(string const& _member) const
141 {
142 return m_tx.member(_member);
143 }
144
txTypeConstraints() const145 smtutil::Expression SymbolicState::txTypeConstraints() const
146 {
147 return
148 smt::symbolicUnknownConstraints(m_tx.member("block.basefee"), TypeProvider::uint256()) &&
149 smt::symbolicUnknownConstraints(m_tx.member("block.chainid"), TypeProvider::uint256()) &&
150 smt::symbolicUnknownConstraints(m_tx.member("block.coinbase"), TypeProvider::address()) &&
151 smt::symbolicUnknownConstraints(m_tx.member("block.difficulty"), TypeProvider::uint256()) &&
152 smt::symbolicUnknownConstraints(m_tx.member("block.gaslimit"), TypeProvider::uint256()) &&
153 smt::symbolicUnknownConstraints(m_tx.member("block.number"), TypeProvider::uint256()) &&
154 smt::symbolicUnknownConstraints(m_tx.member("block.timestamp"), TypeProvider::uint256()) &&
155 smt::symbolicUnknownConstraints(m_tx.member("msg.sender"), TypeProvider::address()) &&
156 smt::symbolicUnknownConstraints(m_tx.member("msg.value"), TypeProvider::uint256()) &&
157 smt::symbolicUnknownConstraints(m_tx.member("tx.origin"), TypeProvider::address()) &&
158 smt::symbolicUnknownConstraints(m_tx.member("tx.gasprice"), TypeProvider::uint256());
159 }
160
txNonPayableConstraint() const161 smtutil::Expression SymbolicState::txNonPayableConstraint() const
162 {
163 return m_tx.member("msg.value") == 0;
164 }
165
txFunctionConstraints(FunctionDefinition const & _function) const166 smtutil::Expression SymbolicState::txFunctionConstraints(FunctionDefinition const& _function) const
167 {
168 smtutil::Expression conj = _function.isPayable() ? smtutil::Expression(true) : txNonPayableConstraint();
169 if (_function.isPartOfExternalInterface())
170 {
171 auto sig = TypeProvider::function(_function)->externalIdentifier();
172 conj = conj && m_tx.member("msg.sig") == sig;
173 auto b0 = sig >> (3 * 8);
174 auto b1 = (sig & 0x00ff0000) >> (2 * 8);
175 auto b2 = (sig & 0x0000ff00) >> (1 * 8);
176 auto b3 = (sig & 0x000000ff);
177 auto data = smtutil::Expression::tuple_get(m_tx.member("msg.data"), 0);
178 conj = conj && smtutil::Expression::select(data, 0) == b0;
179 conj = conj && smtutil::Expression::select(data, 1) == b1;
180 conj = conj && smtutil::Expression::select(data, 2) == b2;
181 conj = conj && smtutil::Expression::select(data, 3) == b3;
182 auto length = smtutil::Expression::tuple_get(m_tx.member("msg.data"), 1);
183 // TODO add ABI size of function input parameters here \/
184 conj = conj && length >= 4;
185 }
186
187 return conj;
188 }
189
prepareForSourceUnit(SourceUnit const & _source)190 void SymbolicState::prepareForSourceUnit(SourceUnit const& _source)
191 {
192 set<FunctionCall const*> abiCalls = SMTEncoder::collectABICalls(&_source);
193 for (auto const& source: _source.referencedSourceUnits(true))
194 abiCalls += SMTEncoder::collectABICalls(source);
195 buildABIFunctions(abiCalls);
196 }
197
198 /// Private helpers.
199
buildABIFunctions(set<FunctionCall const * > const & _abiFunctions)200 void SymbolicState::buildABIFunctions(set<FunctionCall const*> const& _abiFunctions)
201 {
202 map<string, SortPointer> functions;
203
204 for (auto const* funCall: _abiFunctions)
205 {
206 auto t = dynamic_cast<FunctionType const*>(funCall->expression().annotation().type);
207
208 auto const& args = funCall->sortedArguments();
209 auto const& paramTypes = t->parameterTypes();
210 auto const& returnTypes = t->returnParameterTypes();
211
212
213 auto argTypes = [](auto const& _args) {
214 return applyMap(_args, [](auto arg) { return arg->annotation().type; });
215 };
216
217 /// Since each abi.* function may have a different number of input/output parameters,
218 /// we generically compute those types.
219 vector<frontend::Type const*> inTypes;
220 vector<frontend::Type const*> outTypes;
221 if (t->kind() == FunctionType::Kind::ABIDecode)
222 {
223 /// abi.decode : (bytes, tuple_of_types(return_types)) -> (return_types)
224 solAssert(args.size() == 2, "Unexpected number of arguments for abi.decode");
225 inTypes.emplace_back(TypeProvider::bytesMemory());
226 auto argType = args.at(1)->annotation().type;
227 if (auto const* tupleType = dynamic_cast<TupleType const*>(argType))
228 for (auto componentType: tupleType->components())
229 {
230 auto typeType = dynamic_cast<TypeType const*>(componentType);
231 solAssert(typeType, "");
232 outTypes.emplace_back(typeType->actualType());
233 }
234 else if (auto const* typeType = dynamic_cast<TypeType const*>(argType))
235 outTypes.emplace_back(typeType->actualType());
236 else
237 solAssert(false, "Unexpected argument of abi.decode");
238 }
239 else if (t->kind() == FunctionType::Kind::ABIEncodeCall)
240 {
241 // abi.encodeCall : (functionPointer, tuple_of_args_or_one_non_tuple_arg(arguments)) -> bytes
242 solAssert(args.size() == 2, "Unexpected number of arguments for abi.encodeCall");
243
244 outTypes.emplace_back(TypeProvider::bytesMemory());
245 inTypes.emplace_back(args.at(0)->annotation().type);
246 inTypes.emplace_back(args.at(1)->annotation().type);
247 }
248 else
249 {
250 outTypes = returnTypes;
251 if (
252 t->kind() == FunctionType::Kind::ABIEncodeWithSelector ||
253 t->kind() == FunctionType::Kind::ABIEncodeWithSignature
254 )
255 {
256 /// abi.encodeWithSelector : (bytes4, one_or_more_types) -> bytes
257 /// abi.encodeWithSignature : (string, one_or_more_types) -> bytes
258 inTypes.emplace_back(paramTypes.front());
259 inTypes += argTypes(vector<ASTPointer<Expression const>>(args.begin() + 1, args.end()));
260 }
261 else
262 {
263 /// abi.encode/abi.encodePacked : one_or_more_types -> bytes
264 solAssert(
265 t->kind() == FunctionType::Kind::ABIEncode ||
266 t->kind() == FunctionType::Kind::ABIEncodePacked,
267 ""
268 );
269 inTypes = argTypes(args);
270 }
271 }
272
273 /// Rational numbers and string literals add the concrete values to the type name,
274 /// so we replace them by uint256 and bytes since those are the same as their SMT types.
275 /// TODO we could also replace all types by their ABI type.
276 auto replaceTypes = [](auto& _types) {
277 for (auto& t: _types)
278 if (t->category() == frontend::Type::Category::RationalNumber)
279 t = TypeProvider::uint256();
280 else if (t->category() == frontend::Type::Category::StringLiteral)
281 t = TypeProvider::bytesMemory();
282 else if (auto userType = dynamic_cast<UserDefinedValueType const*>(t))
283 t = &userType->underlyingType();
284 };
285 replaceTypes(inTypes);
286 replaceTypes(outTypes);
287
288 auto name = t->richIdentifier();
289 for (auto paramType: inTypes + outTypes)
290 name += "_" + paramType->richIdentifier();
291
292 m_abiMembers[funCall] = {name, inTypes, outTypes};
293
294 if (functions.count(name))
295 continue;
296
297 /// If there is only one input or output parameter, we use that type directly.
298 /// Otherwise we create a tuple wrapping the necessary input or output types.
299 auto typesToSort = [](auto const& _types, string const& _name) -> shared_ptr<Sort> {
300 if (_types.size() == 1)
301 return smtSortAbstractFunction(*_types.front());
302
303 vector<string> inNames;
304 vector<SortPointer> sorts;
305 for (unsigned i = 0; i < _types.size(); ++i)
306 {
307 inNames.emplace_back(_name + "_input_" + to_string(i));
308 sorts.emplace_back(smtSortAbstractFunction(*_types.at(i)));
309 }
310 return make_shared<smtutil::TupleSort>(
311 _name + "_input",
312 inNames,
313 sorts
314 );
315 };
316
317 auto functionSort = make_shared<smtutil::ArraySort>(
318 typesToSort(inTypes, name),
319 typesToSort(outTypes, name)
320 );
321
322 functions[name] = functionSort;
323 }
324
325 m_abi = make_unique<BlockchainVariable>("abi", move(functions), m_context);
326 }
327
abiFunction(frontend::FunctionCall const * _funCall)328 smtutil::Expression SymbolicState::abiFunction(frontend::FunctionCall const* _funCall)
329 {
330 solAssert(m_abi, "");
331 return m_abi->member(get<0>(m_abiMembers.at(_funCall)));
332 }
333
abiFunctionTypes(FunctionCall const * _funCall) const334 SymbolicState::SymbolicABIFunction const& SymbolicState::abiFunctionTypes(FunctionCall const* _funCall) const
335 {
336 return m_abiMembers.at(_funCall);
337 }
338