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/Predicate.h>
20
21 #include <libsolidity/formal/SMTEncoder.h>
22
23 #include <liblangutil/CharStreamProvider.h>
24 #include <liblangutil/CharStream.h>
25 #include <libsolidity/ast/AST.h>
26 #include <libsolidity/ast/TypeProvider.h>
27
28 #include <boost/algorithm/string/join.hpp>
29 #include <boost/algorithm/string.hpp>
30
31 #include <range/v3/view.hpp>
32 #include <utility>
33
34 using namespace std;
35 using boost::algorithm::starts_with;
36 using namespace solidity;
37 using namespace solidity::smtutil;
38 using namespace solidity::frontend;
39 using namespace solidity::frontend::smt;
40
41 map<string, Predicate> Predicate::m_predicates;
42
create(SortPointer _sort,string _name,PredicateType _type,EncodingContext & _context,ASTNode const * _node,ContractDefinition const * _contractContext,vector<ScopeOpener const * > _scopeStack)43 Predicate const* Predicate::create(
44 SortPointer _sort,
45 string _name,
46 PredicateType _type,
47 EncodingContext& _context,
48 ASTNode const* _node,
49 ContractDefinition const* _contractContext,
50 vector<ScopeOpener const*> _scopeStack
51 )
52 {
53 smt::SymbolicFunctionVariable predicate{_sort, move(_name), _context};
54 string functorName = predicate.currentName();
55 solAssert(!m_predicates.count(functorName), "");
56 return &m_predicates.emplace(
57 std::piecewise_construct,
58 std::forward_as_tuple(functorName),
59 std::forward_as_tuple(move(predicate), _type, _node, _contractContext, move(_scopeStack))
60 ).first->second;
61 }
62
Predicate(smt::SymbolicFunctionVariable && _predicate,PredicateType _type,ASTNode const * _node,ContractDefinition const * _contractContext,vector<ScopeOpener const * > _scopeStack)63 Predicate::Predicate(
64 smt::SymbolicFunctionVariable&& _predicate,
65 PredicateType _type,
66 ASTNode const* _node,
67 ContractDefinition const* _contractContext,
68 vector<ScopeOpener const*> _scopeStack
69 ):
70 m_predicate(move(_predicate)),
71 m_type(_type),
72 m_node(_node),
73 m_contractContext(_contractContext),
74 m_scopeStack(_scopeStack)
75 {
76 }
77
predicate(string const & _name)78 Predicate const* Predicate::predicate(string const& _name)
79 {
80 return &m_predicates.at(_name);
81 }
82
reset()83 void Predicate::reset()
84 {
85 m_predicates.clear();
86 }
87
operator ()(vector<smtutil::Expression> const & _args) const88 smtutil::Expression Predicate::operator()(vector<smtutil::Expression> const& _args) const
89 {
90 return m_predicate(_args);
91 }
92
functor() const93 smtutil::Expression Predicate::functor() const
94 {
95 return m_predicate.currentFunctionValue();
96 }
97
functor(unsigned _idx) const98 smtutil::Expression Predicate::functor(unsigned _idx) const
99 {
100 return m_predicate.functionValueAtIndex(_idx);
101 }
102
newFunctor()103 void Predicate::newFunctor()
104 {
105 m_predicate.increaseIndex();
106 }
107
programNode() const108 ASTNode const* Predicate::programNode() const
109 {
110 return m_node;
111 }
112
contextContract() const113 ContractDefinition const* Predicate::contextContract() const
114 {
115 return m_contractContext;
116 }
117
programContract() const118 ContractDefinition const* Predicate::programContract() const
119 {
120 if (auto const* contract = dynamic_cast<ContractDefinition const*>(m_node))
121 if (!contract->constructor())
122 return contract;
123
124 return nullptr;
125 }
126
programFunction() const127 FunctionDefinition const* Predicate::programFunction() const
128 {
129 if (auto const* contract = dynamic_cast<ContractDefinition const*>(m_node))
130 {
131 if (contract->constructor())
132 return contract->constructor();
133 return nullptr;
134 }
135
136 if (auto const* fun = dynamic_cast<FunctionDefinition const*>(m_node))
137 return fun;
138
139 return nullptr;
140 }
141
programFunctionCall() const142 FunctionCall const* Predicate::programFunctionCall() const
143 {
144 return dynamic_cast<FunctionCall const*>(m_node);
145 }
146
stateVariables() const147 optional<vector<VariableDeclaration const*>> Predicate::stateVariables() const
148 {
149 if (m_contractContext)
150 return SMTEncoder::stateVariablesIncludingInheritedAndPrivate(*m_contractContext);
151
152 return nullopt;
153 }
154
isSummary() const155 bool Predicate::isSummary() const
156 {
157 return isFunctionSummary() ||
158 isInternalCall() ||
159 isExternalCallTrusted() ||
160 isExternalCallUntrusted() ||
161 isConstructorSummary();
162 }
163
isFunctionSummary() const164 bool Predicate::isFunctionSummary() const
165 {
166 return m_type == PredicateType::FunctionSummary;
167 }
168
isFunctionBlock() const169 bool Predicate::isFunctionBlock() const
170 {
171 return m_type == PredicateType::FunctionBlock;
172 }
173
isFunctionErrorBlock() const174 bool Predicate::isFunctionErrorBlock() const
175 {
176 return m_type == PredicateType::FunctionErrorBlock;
177 }
178
isInternalCall() const179 bool Predicate::isInternalCall() const
180 {
181 return m_type == PredicateType::InternalCall;
182 }
183
isExternalCallTrusted() const184 bool Predicate::isExternalCallTrusted() const
185 {
186 return m_type == PredicateType::ExternalCallTrusted;
187 }
188
isExternalCallUntrusted() const189 bool Predicate::isExternalCallUntrusted() const
190 {
191 return m_type == PredicateType::ExternalCallUntrusted;
192 }
193
isConstructorSummary() const194 bool Predicate::isConstructorSummary() const
195 {
196 return m_type == PredicateType::ConstructorSummary;
197 }
198
isInterface() const199 bool Predicate::isInterface() const
200 {
201 return m_type == PredicateType::Interface;
202 }
203
isNondetInterface() const204 bool Predicate::isNondetInterface() const
205 {
206 return m_type == PredicateType::NondetInterface;
207 }
208
formatSummaryCall(vector<smtutil::Expression> const & _args,langutil::CharStreamProvider const & _charStreamProvider,bool _appendTxVars) const209 string Predicate::formatSummaryCall(
210 vector<smtutil::Expression> const& _args,
211 langutil::CharStreamProvider const& _charStreamProvider,
212 bool _appendTxVars
213 ) const
214 {
215 solAssert(isSummary(), "");
216
217 if (auto funCall = programFunctionCall())
218 {
219 if (funCall->location().hasText())
220 return string(_charStreamProvider.charStream(*funCall->location().sourceName).text(funCall->location()));
221 else
222 return {};
223 }
224
225 /// The signature of a function summary predicate is: summary(error, this, abiFunctions, cryptoFunctions, txData, preBlockChainState, preStateVars, preInputVars, postBlockchainState, postStateVars, postInputVars, outputVars).
226 /// Here we are interested in preInputVars to format the function call.
227
228 string txModel;
229
230 if (_appendTxVars)
231 {
232 set<string> txVars;
233 if (isFunctionSummary())
234 {
235 solAssert(programFunction(), "");
236 if (programFunction()->isPayable())
237 txVars.insert("msg.value");
238 }
239 else if (isConstructorSummary())
240 {
241 FunctionDefinition const* fun = programFunction();
242 if (fun && fun->isPayable())
243 txVars.insert("msg.value");
244 }
245
246 struct TxVarsVisitor: public ASTConstVisitor
247 {
248 bool visit(MemberAccess const& _memberAccess)
249 {
250 Expression const* memberExpr = SMTEncoder::innermostTuple(_memberAccess.expression());
251
252 Type const* exprType = memberExpr->annotation().type;
253 solAssert(exprType, "");
254 if (exprType->category() == Type::Category::Magic)
255 if (auto const* identifier = dynamic_cast<Identifier const*>(memberExpr))
256 {
257 ASTString const& name = identifier->name();
258 if (name == "block" || name == "msg" || name == "tx")
259 txVars.insert(name + "." + _memberAccess.memberName());
260 }
261
262 return true;
263 }
264
265 set<string> txVars;
266 } txVarsVisitor;
267
268 if (auto fun = programFunction())
269 {
270 fun->accept(txVarsVisitor);
271 txVars += txVarsVisitor.txVars;
272 }
273
274 // Here we are interested in txData from the summary predicate.
275 auto txValues = readTxVars(_args.at(4));
276 vector<string> values;
277 for (auto const& _var: txVars)
278 if (auto v = txValues.at(_var))
279 values.push_back(_var + ": " + *v);
280
281 if (!values.empty())
282 txModel = "{ " + boost::algorithm::join(values, ", ") + " }";
283 }
284
285 if (auto contract = programContract())
286 return contract->name() + ".constructor()" + txModel;
287
288 auto stateVars = stateVariables();
289 solAssert(stateVars.has_value(), "");
290 auto const* fun = programFunction();
291 solAssert(fun, "");
292
293 auto first = _args.begin() + 6 + static_cast<int>(stateVars->size());
294 auto last = first + static_cast<int>(fun->parameters().size());
295 solAssert(first >= _args.begin() && first <= _args.end(), "");
296 solAssert(last >= _args.begin() && last <= _args.end(), "");
297 auto inTypes = SMTEncoder::replaceUserTypes(FunctionType(*fun).parameterTypes());
298 vector<optional<string>> functionArgsCex = formatExpressions(vector<smtutil::Expression>(first, last), inTypes);
299 vector<string> functionArgs;
300
301 auto const& params = fun->parameters();
302 solAssert(params.size() == functionArgsCex.size(), "");
303 for (unsigned i = 0; i < params.size(); ++i)
304 if (params.at(i) && functionArgsCex.at(i))
305 functionArgs.emplace_back(*functionArgsCex.at(i));
306 else
307 functionArgs.emplace_back(params[i]->name());
308
309 string fName = fun->isConstructor() ? "constructor" :
310 fun->isFallback() ? "fallback" :
311 fun->isReceive() ? "receive" :
312 fun->name();
313
314 string prefix;
315 if (fun->isFree())
316 prefix = !fun->sourceUnitName().empty() ? (fun->sourceUnitName() + ":") : "";
317 else
318 {
319 solAssert(fun->annotation().contract, "");
320 prefix = fun->annotation().contract->name() + ".";
321 }
322 return prefix + fName + "(" + boost::algorithm::join(functionArgs, ", ") + ")" + txModel;
323 }
324
summaryStateValues(vector<smtutil::Expression> const & _args) const325 vector<optional<string>> Predicate::summaryStateValues(vector<smtutil::Expression> const& _args) const
326 {
327 /// The signature of a function summary predicate is: summary(error, this, abiFunctions, cryptoFunctions, txData, preBlockchainState, preStateVars, preInputVars, postBlockchainState, postStateVars, postInputVars, outputVars).
328 /// The signature of the summary predicate of a contract without constructor is: summary(error, this, abiFunctions, cryptoFunctions, txData, preBlockchainState, postBlockchainState, preStateVars, postStateVars).
329 /// Here we are interested in postStateVars.
330 auto stateVars = stateVariables();
331 solAssert(stateVars.has_value(), "");
332
333 vector<smtutil::Expression>::const_iterator stateFirst;
334 vector<smtutil::Expression>::const_iterator stateLast;
335 if (auto const* function = programFunction())
336 {
337 stateFirst = _args.begin() + 6 + static_cast<int>(stateVars->size()) + static_cast<int>(function->parameters().size()) + 1;
338 stateLast = stateFirst + static_cast<int>(stateVars->size());
339 }
340 else if (programContract())
341 {
342 stateFirst = _args.begin() + 7 + static_cast<int>(stateVars->size());
343 stateLast = stateFirst + static_cast<int>(stateVars->size());
344 }
345 else
346 solAssert(false, "");
347
348 solAssert(stateFirst >= _args.begin() && stateFirst <= _args.end(), "");
349 solAssert(stateLast >= _args.begin() && stateLast <= _args.end(), "");
350
351 vector<smtutil::Expression> stateArgs(stateFirst, stateLast);
352 solAssert(stateArgs.size() == stateVars->size(), "");
353 auto stateTypes = applyMap(*stateVars, [&](auto const& _var) { return _var->type(); });
354 return formatExpressions(stateArgs, stateTypes);
355 }
356
summaryPostInputValues(vector<smtutil::Expression> const & _args) const357 vector<optional<string>> Predicate::summaryPostInputValues(vector<smtutil::Expression> const& _args) const
358 {
359 /// The signature of a function summary predicate is: summary(error, this, abiFunctions, cryptoFunctions, txData, preBlockchainState, preStateVars, preInputVars, postBlockchainState, postStateVars, postInputVars, outputVars).
360 /// Here we are interested in postInputVars.
361 auto const* function = programFunction();
362 solAssert(function, "");
363
364 auto stateVars = stateVariables();
365 solAssert(stateVars.has_value(), "");
366
367 auto const& inParams = function->parameters();
368
369 auto first = _args.begin() + 6 + static_cast<int>(stateVars->size()) * 2 + static_cast<int>(inParams.size()) + 1;
370 auto last = first + static_cast<int>(inParams.size());
371
372 solAssert(first >= _args.begin() && first <= _args.end(), "");
373 solAssert(last >= _args.begin() && last <= _args.end(), "");
374
375 vector<smtutil::Expression> inValues(first, last);
376 solAssert(inValues.size() == inParams.size(), "");
377 auto inTypes = SMTEncoder::replaceUserTypes(FunctionType(*function).parameterTypes());
378 return formatExpressions(inValues, inTypes);
379 }
380
summaryPostOutputValues(vector<smtutil::Expression> const & _args) const381 vector<optional<string>> Predicate::summaryPostOutputValues(vector<smtutil::Expression> const& _args) const
382 {
383 /// The signature of a function summary predicate is: summary(error, this, abiFunctions, cryptoFunctions, txData, preBlockchainState, preStateVars, preInputVars, postBlockchainState, postStateVars, postInputVars, outputVars).
384 /// Here we are interested in outputVars.
385 auto const* function = programFunction();
386 solAssert(function, "");
387
388 auto stateVars = stateVariables();
389 solAssert(stateVars.has_value(), "");
390
391 auto const& inParams = function->parameters();
392
393 auto first = _args.begin() + 6 + static_cast<int>(stateVars->size()) * 2 + static_cast<int>(inParams.size()) * 2 + 1;
394
395 solAssert(first >= _args.begin() && first <= _args.end(), "");
396
397 vector<smtutil::Expression> outValues(first, _args.end());
398 solAssert(outValues.size() == function->returnParameters().size(), "");
399 auto outTypes = SMTEncoder::replaceUserTypes(FunctionType(*function).returnParameterTypes());
400 return formatExpressions(outValues, outTypes);
401 }
402
localVariableValues(vector<smtutil::Expression> const & _args) const403 pair<vector<optional<string>>, vector<VariableDeclaration const*>> Predicate::localVariableValues(vector<smtutil::Expression> const& _args) const
404 {
405 /// The signature of a local block predicate is:
406 /// block(error, this, abiFunctions, cryptoFunctions, txData, preBlockchainState, preStateVars, preInputVars, postBlockchainState, postStateVars, postInputVars, outputVars, localVars).
407 /// Here we are interested in localVars.
408 auto const* function = programFunction();
409 solAssert(function, "");
410
411 auto const& localVars = SMTEncoder::localVariablesIncludingModifiers(*function, m_contractContext);
412 auto first = _args.end() - static_cast<int>(localVars.size());
413 vector<smtutil::Expression> outValues(first, _args.end());
414
415 auto mask = applyMap(
416 localVars,
417 [this](auto _var) {
418 auto varScope = dynamic_cast<ScopeOpener const*>(_var->scope());
419 return find(begin(m_scopeStack), end(m_scopeStack), varScope) != end(m_scopeStack);
420 }
421 );
422 auto localVarsInScope = util::filter(localVars, mask);
423 auto outValuesInScope = util::filter(outValues, mask);
424
425 auto outTypes = applyMap(localVarsInScope, [](auto _var) { return _var->type(); });
426 return {formatExpressions(outValuesInScope, outTypes), localVarsInScope};
427 }
428
expressionSubstitution(smtutil::Expression const & _predExpr) const429 map<string, string> Predicate::expressionSubstitution(smtutil::Expression const& _predExpr) const
430 {
431 map<string, string> subst;
432 string predName = functor().name;
433
434 solAssert(contextContract(), "");
435 auto const& stateVars = SMTEncoder::stateVariablesIncludingInheritedAndPrivate(*contextContract());
436
437 auto nArgs = _predExpr.arguments.size();
438
439 // The signature of an interface predicate is
440 // interface(this, abiFunctions, cryptoFunctions, blockchainState, stateVariables).
441 // An invariant for an interface predicate is a contract
442 // invariant over its state, for example `x <= 0`.
443 if (isInterface())
444 {
445 solAssert(starts_with(predName, "interface"), "");
446 subst[_predExpr.arguments.at(0).name] = "address(this)";
447 solAssert(nArgs == stateVars.size() + 4, "");
448 for (size_t i = nArgs - stateVars.size(); i < nArgs; ++i)
449 subst[_predExpr.arguments.at(i).name] = stateVars.at(i - 4)->name();
450 }
451 // The signature of a nondet interface predicate is
452 // nondet_interface(error, this, abiFunctions, cryptoFunctions, blockchainState, stateVariables, blockchainState', stateVariables').
453 // An invariant for a nondet interface predicate is a reentrancy property
454 // over the pre and post state variables of a contract, where pre state vars
455 // are represented by the variable's name and post state vars are represented
456 // by the primed variable's name, for example
457 // `(x <= 0) => (x' <= 100)`.
458 else if (isNondetInterface())
459 {
460 solAssert(starts_with(predName, "nondet_interface"), "");
461 subst[_predExpr.arguments.at(0).name] = "<errorCode>";
462 subst[_predExpr.arguments.at(1).name] = "address(this)";
463 solAssert(nArgs == stateVars.size() * 2 + 6, "");
464 for (size_t i = nArgs - stateVars.size(), s = 0; i < nArgs; ++i, ++s)
465 subst[_predExpr.arguments.at(i).name] = stateVars.at(s)->name() + "'";
466 for (size_t i = nArgs - (stateVars.size() * 2 + 1), s = 0; i < nArgs - (stateVars.size() + 1); ++i, ++s)
467 subst[_predExpr.arguments.at(i).name] = stateVars.at(s)->name();
468 }
469
470 return subst;
471 }
472
formatExpressions(vector<smtutil::Expression> const & _exprs,vector<Type const * > const & _types) const473 vector<optional<string>> Predicate::formatExpressions(vector<smtutil::Expression> const& _exprs, vector<Type const*> const& _types) const
474 {
475 solAssert(_exprs.size() == _types.size(), "");
476 vector<optional<string>> strExprs;
477 for (unsigned i = 0; i < _exprs.size(); ++i)
478 strExprs.push_back(expressionToString(_exprs.at(i), _types.at(i)));
479 return strExprs;
480 }
481
expressionToString(smtutil::Expression const & _expr,Type const * _type) const482 optional<string> Predicate::expressionToString(smtutil::Expression const& _expr, Type const* _type) const
483 {
484 if (smt::isNumber(*_type))
485 {
486 solAssert(_expr.sort->kind == Kind::Int, "");
487 solAssert(_expr.arguments.empty(), "");
488
489 if (
490 _type->category() == Type::Category::Address ||
491 _type->category() == Type::Category::FixedBytes
492 )
493 {
494 try
495 {
496 if (_expr.name == "0")
497 return "0x0";
498 // For some reason the code below returns "0x" for "0".
499 return toHex(toCompactBigEndian(bigint(_expr.name)), HexPrefix::Add, HexCase::Lower);
500 }
501 catch (out_of_range const&)
502 {
503 }
504 catch (invalid_argument const&)
505 {
506 }
507 }
508
509 return _expr.name;
510 }
511 if (smt::isBool(*_type))
512 {
513 solAssert(_expr.sort->kind == Kind::Bool, "");
514 solAssert(_expr.arguments.empty(), "");
515 solAssert(_expr.name == "true" || _expr.name == "false", "");
516 return _expr.name;
517 }
518 if (smt::isFunction(*_type))
519 {
520 solAssert(_expr.arguments.empty(), "");
521 return _expr.name;
522 }
523 if (smt::isArray(*_type))
524 {
525 auto const& arrayType = dynamic_cast<ArrayType const&>(*_type);
526 if (_expr.name != "tuple_constructor")
527 return {};
528
529 auto const& tupleSort = dynamic_cast<TupleSort const&>(*_expr.sort);
530 solAssert(tupleSort.components.size() == 2, "");
531
532 unsigned long length;
533 try
534 {
535 length = stoul(_expr.arguments.at(1).name);
536 }
537 catch(out_of_range const&)
538 {
539 return {};
540 }
541 catch(invalid_argument const&)
542 {
543 return {};
544 }
545
546 // Limit this counterexample size to 1k.
547 // Some OSs give you "unlimited" memory through swap and other virtual memory,
548 // so purely relying on bad_alloc being thrown is not a good idea.
549 // In that case, the array allocation might cause OOM and the program is killed.
550 if (length >= 1024)
551 return {};
552 try
553 {
554 vector<string> array(length);
555 if (!fillArray(_expr.arguments.at(0), array, arrayType))
556 return {};
557 return "[" + boost::algorithm::join(array, ", ") + "]";
558 }
559 catch (bad_alloc const&)
560 {
561 // Solver gave a concrete array but length is too large.
562 }
563 }
564 if (smt::isNonRecursiveStruct(*_type))
565 {
566 auto const& structType = dynamic_cast<StructType const&>(*_type);
567 solAssert(_expr.name == "tuple_constructor", "");
568 auto const& tupleSort = dynamic_cast<TupleSort const&>(*_expr.sort);
569 auto members = structType.structDefinition().members();
570 solAssert(tupleSort.components.size() == members.size(), "");
571 solAssert(_expr.arguments.size() == members.size(), "");
572 vector<string> elements;
573 for (unsigned i = 0; i < members.size(); ++i)
574 {
575 optional<string> elementStr = expressionToString(_expr.arguments.at(i), members[i]->type());
576 elements.push_back(members[i]->name() + (elementStr.has_value() ? ": " + elementStr.value() : ""));
577 }
578 return "{" + boost::algorithm::join(elements, ", ") + "}";
579 }
580
581 return {};
582 }
583
fillArray(smtutil::Expression const & _expr,vector<string> & _array,ArrayType const & _type) const584 bool Predicate::fillArray(smtutil::Expression const& _expr, vector<string>& _array, ArrayType const& _type) const
585 {
586 // Base case
587 if (_expr.name == "const_array")
588 {
589 auto length = _array.size();
590 optional<string> elemStr = expressionToString(_expr.arguments.at(1), _type.baseType());
591 if (!elemStr)
592 return false;
593 _array.clear();
594 _array.resize(length, *elemStr);
595 return true;
596 }
597
598 // Recursive case.
599 if (_expr.name == "store")
600 {
601 if (!fillArray(_expr.arguments.at(0), _array, _type))
602 return false;
603 optional<string> indexStr = expressionToString(_expr.arguments.at(1), TypeProvider::uint256());
604 if (!indexStr)
605 return false;
606 // Sometimes the solver assigns huge lengths that are not related,
607 // we should catch and ignore those.
608 unsigned long index;
609 try
610 {
611 index = stoul(*indexStr);
612 }
613 catch (out_of_range const&)
614 {
615 return true;
616 }
617 catch (invalid_argument const&)
618 {
619 return true;
620 }
621 optional<string> elemStr = expressionToString(_expr.arguments.at(2), _type.baseType());
622 if (!elemStr)
623 return false;
624 if (index < _array.size())
625 _array.at(index) = *elemStr;
626 return true;
627 }
628
629 // Special base case, not supported yet.
630 if (_expr.name.rfind("(_ as-array") == 0)
631 {
632 // Z3 expression representing reinterpretation of a different term as an array
633 return false;
634 }
635
636 solAssert(false, "");
637 }
638
readTxVars(smtutil::Expression const & _tx) const639 map<string, optional<string>> Predicate::readTxVars(smtutil::Expression const& _tx) const
640 {
641 map<string, Type const*> const txVars{
642 {"block.basefee", TypeProvider::uint256()},
643 {"block.chainid", TypeProvider::uint256()},
644 {"block.coinbase", TypeProvider::address()},
645 {"block.difficulty", TypeProvider::uint256()},
646 {"block.gaslimit", TypeProvider::uint256()},
647 {"block.number", TypeProvider::uint256()},
648 {"block.timestamp", TypeProvider::uint256()},
649 {"blockhash", TypeProvider::array(DataLocation::Memory, TypeProvider::uint256())},
650 {"msg.data", TypeProvider::array(DataLocation::CallData)},
651 {"msg.sender", TypeProvider::address()},
652 {"msg.sig", TypeProvider::fixedBytes(4)},
653 {"msg.value", TypeProvider::uint256()},
654 {"tx.gasprice", TypeProvider::uint256()},
655 {"tx.origin", TypeProvider::address()}
656 };
657 map<string, optional<string>> vars;
658 for (auto&& [i, v]: txVars | ranges::views::enumerate)
659 vars.emplace(v.first, expressionToString(_tx.arguments.at(i), v.second));
660 return vars;
661 }
662