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/SMTEncoder.h>
20
21 #include <libsolidity/ast/TypeProvider.h>
22 #include <libsolidity/formal/SymbolicState.h>
23 #include <libsolidity/formal/SymbolicTypes.h>
24
25 #include <libsolidity/analysis/ConstantEvaluator.h>
26
27 #include <libyul/AST.h>
28 #include <libyul/optimiser/Semantics.h>
29
30 #include <libsmtutil/SMTPortfolio.h>
31 #include <libsmtutil/Helpers.h>
32
33 #include <liblangutil/CharStreamProvider.h>
34
35 #include <libsolutil/Algorithms.h>
36
37 #include <range/v3/view.hpp>
38
39 #include <limits>
40 #include <deque>
41
42 using namespace std;
43 using namespace solidity;
44 using namespace solidity::util;
45 using namespace solidity::langutil;
46 using namespace solidity::frontend;
47
SMTEncoder(smt::EncodingContext & _context,ModelCheckerSettings const & _settings,UniqueErrorReporter & _errorReporter,langutil::CharStreamProvider const & _charStreamProvider)48 SMTEncoder::SMTEncoder(
49 smt::EncodingContext& _context,
50 ModelCheckerSettings const& _settings,
51 UniqueErrorReporter& _errorReporter,
52 langutil::CharStreamProvider const& _charStreamProvider
53 ):
54 m_errorReporter(_errorReporter),
55 m_context(_context),
56 m_settings(_settings),
57 m_charStreamProvider(_charStreamProvider)
58 {
59 }
60
resetSourceAnalysis()61 void SMTEncoder::resetSourceAnalysis()
62 {
63 m_freeFunctions.clear();
64 }
65
visit(ContractDefinition const & _contract)66 bool SMTEncoder::visit(ContractDefinition const& _contract)
67 {
68 solAssert(m_currentContract, "");
69
70 for (auto const& node: _contract.subNodes())
71 if (
72 !dynamic_pointer_cast<FunctionDefinition>(node) &&
73 !dynamic_pointer_cast<VariableDeclaration>(node)
74 )
75 node->accept(*this);
76
77 for (auto const& base: _contract.annotation().linearizedBaseContracts)
78 {
79 // Look for all the constructor invocations bottom up.
80 if (auto const& constructor = base->constructor())
81 for (auto const& invocation: constructor->modifiers())
82 {
83 auto refDecl = invocation->name().annotation().referencedDeclaration;
84 if (auto const& baseContract = dynamic_cast<ContractDefinition const*>(refDecl))
85 {
86 solAssert(!m_baseConstructorCalls.count(baseContract), "");
87 m_baseConstructorCalls[baseContract] = invocation.get();
88 }
89 }
90 }
91 // Functions are visited first since they might be used
92 // for state variable initialization which is part of
93 // the constructor.
94 // Constructors are visited as part of the constructor
95 // hierarchy inlining.
96 for (auto const* function: contractFunctionsWithoutVirtual(_contract) + allFreeFunctions())
97 if (!function->isConstructor())
98 function->accept(*this);
99
100 // Constructors need to be handled by the engines separately.
101
102 return false;
103 }
104
endVisit(ContractDefinition const & _contract)105 void SMTEncoder::endVisit(ContractDefinition const& _contract)
106 {
107 m_context.resetAllVariables();
108
109 m_baseConstructorCalls.clear();
110
111 solAssert(m_currentContract == &_contract, "");
112 m_currentContract = nullptr;
113
114 if (m_callStack.empty())
115 m_context.popSolver();
116 }
117
endVisit(VariableDeclaration const & _varDecl)118 void SMTEncoder::endVisit(VariableDeclaration const& _varDecl)
119 {
120 // State variables are handled by the constructor.
121 if (_varDecl.isLocalVariable() &&_varDecl.value())
122 assignment(_varDecl, *_varDecl.value());
123 }
124
visit(ModifierDefinition const &)125 bool SMTEncoder::visit(ModifierDefinition const&)
126 {
127 return false;
128 }
129
visit(FunctionDefinition const & _function)130 bool SMTEncoder::visit(FunctionDefinition const& _function)
131 {
132 solAssert(m_currentContract, "");
133
134 m_modifierDepthStack.push_back(-1);
135
136 initializeLocalVariables(_function);
137
138 _function.parameterList().accept(*this);
139 if (_function.returnParameterList())
140 _function.returnParameterList()->accept(*this);
141
142 visitFunctionOrModifier();
143
144 return false;
145 }
146
visitFunctionOrModifier()147 void SMTEncoder::visitFunctionOrModifier()
148 {
149 solAssert(!m_callStack.empty(), "");
150 solAssert(!m_modifierDepthStack.empty(), "");
151
152 ++m_modifierDepthStack.back();
153 FunctionDefinition const& function = dynamic_cast<FunctionDefinition const&>(*m_callStack.back().first);
154
155 if (m_modifierDepthStack.back() == static_cast<int>(function.modifiers().size()))
156 {
157 if (function.isImplemented())
158 {
159 pushInlineFrame(function);
160 function.body().accept(*this);
161 popInlineFrame(function);
162 }
163 }
164 else
165 {
166 solAssert(m_modifierDepthStack.back() < static_cast<int>(function.modifiers().size()), "");
167 ASTPointer<ModifierInvocation> const& modifierInvocation =
168 function.modifiers()[static_cast<size_t>(m_modifierDepthStack.back())];
169 solAssert(modifierInvocation, "");
170 auto refDecl = modifierInvocation->name().annotation().referencedDeclaration;
171 if (dynamic_cast<ContractDefinition const*>(refDecl))
172 visitFunctionOrModifier();
173 else if (auto modifier = resolveModifierInvocation(*modifierInvocation, m_currentContract))
174 {
175 m_scopes.push_back(modifier);
176 inlineModifierInvocation(modifierInvocation.get(), modifier);
177 solAssert(m_scopes.back() == modifier, "");
178 m_scopes.pop_back();
179 }
180 else
181 solAssert(false, "");
182 }
183
184 --m_modifierDepthStack.back();
185 }
186
inlineModifierInvocation(ModifierInvocation const * _invocation,CallableDeclaration const * _definition)187 void SMTEncoder::inlineModifierInvocation(ModifierInvocation const* _invocation, CallableDeclaration const* _definition)
188 {
189 solAssert(_invocation, "");
190 _invocation->accept(*this);
191
192 vector<smtutil::Expression> args;
193 if (auto const* arguments = _invocation->arguments())
194 {
195 auto const& modifierParams = _definition->parameters();
196 solAssert(modifierParams.size() == arguments->size(), "");
197 for (unsigned i = 0; i < arguments->size(); ++i)
198 args.push_back(expr(*arguments->at(i), modifierParams.at(i)->type()));
199 }
200
201 initializeFunctionCallParameters(*_definition, args);
202
203 pushCallStack({_definition, _invocation});
204 pushInlineFrame(*_definition);
205 if (auto modifier = dynamic_cast<ModifierDefinition const*>(_definition))
206 {
207 if (modifier->isImplemented())
208 modifier->body().accept(*this);
209 popCallStack();
210 }
211 else if (auto function = dynamic_cast<FunctionDefinition const*>(_definition))
212 {
213 if (function->isImplemented())
214 function->accept(*this);
215 // Functions are popped from the callstack in endVisit(FunctionDefinition)
216 }
217 popInlineFrame(*_definition);
218 }
219
inlineConstructorHierarchy(ContractDefinition const & _contract)220 void SMTEncoder::inlineConstructorHierarchy(ContractDefinition const& _contract)
221 {
222 auto const& hierarchy = m_currentContract->annotation().linearizedBaseContracts;
223 auto it = find(begin(hierarchy), end(hierarchy), &_contract);
224 solAssert(it != end(hierarchy), "");
225
226 auto nextBase = it + 1;
227 // Initialize the base contracts here as long as their constructors are implicit,
228 // stop when the first explicit constructor is found.
229 while (nextBase != end(hierarchy))
230 {
231 if (auto baseConstructor = (*nextBase)->constructor())
232 {
233 createLocalVariables(*baseConstructor);
234 // If any subcontract explicitly called baseConstructor, use those arguments.
235 if (m_baseConstructorCalls.count(*nextBase))
236 inlineModifierInvocation(m_baseConstructorCalls.at(*nextBase), baseConstructor);
237 else if (baseConstructor->isImplemented())
238 {
239 // The first constructor found is handled like a function
240 // and its pushed into the callstack there.
241 // This if avoids duplication in the callstack.
242 if (!m_callStack.empty())
243 pushCallStack({baseConstructor, nullptr});
244 baseConstructor->accept(*this);
245 // popped by endVisit(FunctionDefinition)
246 }
247 break;
248 }
249 else
250 {
251 initializeStateVariables(**nextBase);
252 ++nextBase;
253 }
254 }
255
256 initializeStateVariables(_contract);
257 }
258
visit(PlaceholderStatement const &)259 bool SMTEncoder::visit(PlaceholderStatement const&)
260 {
261 solAssert(!m_callStack.empty(), "");
262 auto lastCall = popCallStack();
263 visitFunctionOrModifier();
264 pushCallStack(lastCall);
265 return true;
266 }
267
endVisit(FunctionDefinition const &)268 void SMTEncoder::endVisit(FunctionDefinition const&)
269 {
270 solAssert(m_currentContract, "");
271
272 popCallStack();
273 solAssert(m_modifierDepthStack.back() == -1, "");
274 m_modifierDepthStack.pop_back();
275 if (m_callStack.empty())
276 m_context.popSolver();
277 }
278
visit(Block const & _block)279 bool SMTEncoder::visit(Block const& _block)
280 {
281 if (_block.unchecked())
282 {
283 solAssert(m_checked, "");
284 m_checked = false;
285 }
286 return true;
287 }
288
endVisit(Block const & _block)289 void SMTEncoder::endVisit(Block const& _block)
290 {
291 if (_block.unchecked())
292 {
293 solAssert(!m_checked, "");
294 m_checked = true;
295 }
296 }
297
visit(InlineAssembly const & _inlineAsm)298 bool SMTEncoder::visit(InlineAssembly const& _inlineAsm)
299 {
300 /// This is very similar to `yul::Assignments`, except I need to collect `Identifier`s and not just names as `YulString`s.
301 struct AssignedExternalsCollector: public yul::ASTWalker
302 {
303 AssignedExternalsCollector(InlineAssembly const& _inlineAsm): externalReferences(_inlineAsm.annotation().externalReferences)
304 {
305 this->operator()(_inlineAsm.operations());
306 }
307
308 map<yul::Identifier const*, InlineAssemblyAnnotation::ExternalIdentifierInfo> const& externalReferences;
309 set<VariableDeclaration const*> assignedVars;
310
311 using yul::ASTWalker::operator();
312 void operator()(yul::Assignment const& _assignment)
313 {
314 auto const& vars = _assignment.variableNames;
315 for (auto const& identifier: vars)
316 if (auto externalInfo = valueOrNullptr(externalReferences, &identifier))
317 if (auto varDecl = dynamic_cast<VariableDeclaration const*>(externalInfo->declaration))
318 assignedVars.insert(varDecl);
319 }
320 };
321
322 yul::SideEffectsCollector sideEffectsCollector(_inlineAsm.dialect(), _inlineAsm.operations());
323 if (sideEffectsCollector.invalidatesMemory())
324 resetMemoryVariables();
325 if (sideEffectsCollector.invalidatesStorage())
326 resetStorageVariables();
327
328 auto assignedVars = AssignedExternalsCollector(_inlineAsm).assignedVars;
329 for (auto const* var: assignedVars)
330 {
331 solAssert(var, "");
332 solAssert(var->isLocalVariable(), "Non-local variable assigned in inlined assembly");
333 m_context.resetVariable(*var);
334 }
335
336 m_errorReporter.warning(
337 7737_error,
338 _inlineAsm.location(),
339 "Inline assembly may cause SMTChecker to produce spurious warnings (false positives)."
340 );
341 return false;
342 }
343
pushInlineFrame(CallableDeclaration const &)344 void SMTEncoder::pushInlineFrame(CallableDeclaration const&)
345 {
346 pushPathCondition(currentPathConditions());
347 }
348
popInlineFrame(CallableDeclaration const &)349 void SMTEncoder::popInlineFrame(CallableDeclaration const&)
350 {
351 popPathCondition();
352 }
353
endVisit(VariableDeclarationStatement const & _varDecl)354 void SMTEncoder::endVisit(VariableDeclarationStatement const& _varDecl)
355 {
356 if (auto init = _varDecl.initialValue())
357 expressionToTupleAssignment(_varDecl.declarations(), *init);
358 }
359
visit(Assignment const & _assignment)360 bool SMTEncoder::visit(Assignment const& _assignment)
361 {
362 // RHS must be visited before LHS; as opposed to what Assignment::accept does
363 _assignment.rightHandSide().accept(*this);
364 _assignment.leftHandSide().accept(*this);
365 return false;
366 }
367
endVisit(Assignment const & _assignment)368 void SMTEncoder::endVisit(Assignment const& _assignment)
369 {
370 createExpr(_assignment);
371
372 Token op = _assignment.assignmentOperator();
373 solAssert(TokenTraits::isAssignmentOp(op), "");
374
375 if (!isSupportedType(*_assignment.annotation().type))
376 {
377 // Give it a new index anyway to keep the SSA scheme sound.
378
379 Expression const* base = &_assignment.leftHandSide();
380 if (auto const* indexAccess = dynamic_cast<IndexAccess const*>(base))
381 base = leftmostBase(*indexAccess);
382
383 if (auto varDecl = identifierToVariable(*base))
384 m_context.newValue(*varDecl);
385 }
386 else
387 {
388 if (dynamic_cast<TupleType const*>(_assignment.rightHandSide().annotation().type))
389 tupleAssignment(_assignment.leftHandSide(), _assignment.rightHandSide());
390 else
391 {
392 auto const& type = _assignment.annotation().type;
393 auto rightHandSide = op == Token::Assign ?
394 expr(_assignment.rightHandSide(), type) :
395 compoundAssignment(_assignment);
396 defineExpr(_assignment, rightHandSide);
397 assignment(
398 _assignment.leftHandSide(),
399 expr(_assignment, type),
400 type
401 );
402 }
403 }
404 }
405
endVisit(TupleExpression const & _tuple)406 void SMTEncoder::endVisit(TupleExpression const& _tuple)
407 {
408 if (_tuple.annotation().type->category() == Type::Category::Function)
409 return;
410
411 if (_tuple.annotation().type->category() == Type::Category::TypeType)
412 return;
413
414 createExpr(_tuple);
415
416 if (_tuple.isInlineArray())
417 {
418 // Add constraints for the length and values as it is known.
419 auto symbArray = dynamic_pointer_cast<smt::SymbolicArrayVariable>(m_context.expression(_tuple));
420 solAssert(symbArray, "");
421
422 addArrayLiteralAssertions(*symbArray, applyMap(_tuple.components(), [&](auto const& c) { return expr(*c); }));
423 }
424 else
425 {
426 auto values = applyMap(_tuple.components(), [this](auto const& component) -> optional<smtutil::Expression> {
427 if (component)
428 {
429 if (!m_context.knownExpression(*component))
430 createExpr(*component);
431 return expr(*component);
432 }
433 return {};
434 });
435 defineExpr(_tuple, values);
436 }
437 }
438
endVisit(UnaryOperation const & _op)439 void SMTEncoder::endVisit(UnaryOperation const& _op)
440 {
441 /// We need to shortcut here due to potentially unknown
442 /// rational number sizes.
443 if (_op.annotation().type->category() == Type::Category::RationalNumber)
444 return;
445
446 if (TokenTraits::isBitOp(_op.getOperator()))
447 return bitwiseNotOperation(_op);
448
449 createExpr(_op);
450
451 auto const* subExpr = innermostTuple(_op.subExpression());
452 auto type = _op.annotation().type;
453 switch (_op.getOperator())
454 {
455 case Token::Not: // !
456 {
457 solAssert(smt::isBool(*type), "");
458 defineExpr(_op, !expr(*subExpr));
459 break;
460 }
461 case Token::Inc: // ++ (pre- or postfix)
462 case Token::Dec: // -- (pre- or postfix)
463 {
464 solAssert(smt::isInteger(*type) || smt::isFixedPoint(*type), "");
465 solAssert(subExpr->annotation().willBeWrittenTo, "");
466 auto innerValue = expr(*subExpr);
467 auto newValue = arithmeticOperation(
468 _op.getOperator() == Token::Inc ? Token::Add : Token::Sub,
469 innerValue,
470 smtutil::Expression(size_t(1)),
471 _op.annotation().type,
472 _op
473 ).first;
474 defineExpr(_op, _op.isPrefixOperation() ? newValue : innerValue);
475 assignment(*subExpr, newValue);
476 break;
477 }
478 case Token::Sub: // -
479 {
480 defineExpr(_op, 0 - expr(*subExpr));
481 break;
482 }
483 case Token::Delete:
484 {
485 if (auto decl = identifierToVariable(*subExpr))
486 {
487 m_context.newValue(*decl);
488 m_context.setZeroValue(*decl);
489 }
490 else
491 {
492 solAssert(m_context.knownExpression(*subExpr), "");
493 auto const& symbVar = m_context.expression(*subExpr);
494 symbVar->increaseIndex();
495 m_context.setZeroValue(*symbVar);
496 if (
497 dynamic_cast<IndexAccess const*>(subExpr) ||
498 dynamic_cast<MemberAccess const*>(subExpr)
499 )
500 indexOrMemberAssignment(*subExpr, symbVar->currentValue());
501 // Empty push added a zero value anyway, so no need to delete extra.
502 else if (!isEmptyPush(*subExpr))
503 solAssert(false, "");
504 }
505 break;
506 }
507 default:
508 solAssert(false, "");
509 }
510 }
511
visit(UnaryOperation const & _op)512 bool SMTEncoder::visit(UnaryOperation const& _op)
513 {
514 return !shortcutRationalNumber(_op);
515 }
516
visit(BinaryOperation const & _op)517 bool SMTEncoder::visit(BinaryOperation const& _op)
518 {
519 if (shortcutRationalNumber(_op))
520 return false;
521 if (TokenTraits::isBooleanOp(_op.getOperator()))
522 {
523 booleanOperation(_op);
524 return false;
525 }
526 return true;
527 }
528
endVisit(BinaryOperation const & _op)529 void SMTEncoder::endVisit(BinaryOperation const& _op)
530 {
531 /// If _op is const evaluated the RationalNumber shortcut was taken.
532 if (isConstant(_op))
533 return;
534 if (TokenTraits::isBooleanOp(_op.getOperator()))
535 return;
536
537 createExpr(_op);
538
539 if (TokenTraits::isArithmeticOp(_op.getOperator()))
540 arithmeticOperation(_op);
541 else if (TokenTraits::isCompareOp(_op.getOperator()))
542 compareOperation(_op);
543 else if (TokenTraits::isBitOp(_op.getOperator()) || TokenTraits::isShiftOp(_op.getOperator()))
544 bitwiseOperation(_op);
545 else
546 solAssert(false, "");
547 }
548
visit(Conditional const & _op)549 bool SMTEncoder::visit(Conditional const& _op)
550 {
551 _op.condition().accept(*this);
552
553 auto indicesEndTrue = visitBranch(&_op.trueExpression(), expr(_op.condition())).first;
554
555 auto indicesEndFalse = visitBranch(&_op.falseExpression(), !expr(_op.condition())).first;
556
557 mergeVariables(expr(_op.condition()), indicesEndTrue, indicesEndFalse);
558
559 defineExpr(_op, smtutil::Expression::ite(
560 expr(_op.condition()),
561 expr(_op.trueExpression(), _op.annotation().type),
562 expr(_op.falseExpression(), _op.annotation().type)
563 ));
564
565 return false;
566 }
567
visit(FunctionCall const & _funCall)568 bool SMTEncoder::visit(FunctionCall const& _funCall)
569 {
570 auto functionCallKind = *_funCall.annotation().kind;
571 if (functionCallKind != FunctionCallKind::FunctionCall)
572 return true;
573
574 FunctionType const& funType = dynamic_cast<FunctionType const&>(*_funCall.expression().annotation().type);
575 // We do not want to visit the TypeTypes in the second argument of `abi.decode`.
576 // Those types are checked/used in SymbolicState::buildABIFunctions.
577 if (funType.kind() == FunctionType::Kind::ABIDecode)
578 {
579 if (auto arg = _funCall.arguments().front())
580 arg->accept(*this);
581 return false;
582 }
583 // We do not really need to visit the expression in a wrap/unwrap no-op call,
584 // so we just ignore the function call expression to avoid "unsupported" warnings.
585 else if (
586 funType.kind() == FunctionType::Kind::Wrap ||
587 funType.kind() == FunctionType::Kind::Unwrap
588 )
589 {
590 if (auto arg = _funCall.arguments().front())
591 arg->accept(*this);
592 return false;
593 }
594 return true;
595 }
596
endVisit(FunctionCall const & _funCall)597 void SMTEncoder::endVisit(FunctionCall const& _funCall)
598 {
599 auto functionCallKind = *_funCall.annotation().kind;
600
601 createExpr(_funCall);
602 if (functionCallKind == FunctionCallKind::StructConstructorCall)
603 {
604 visitStructConstructorCall(_funCall);
605 return;
606 }
607
608 if (functionCallKind == FunctionCallKind::TypeConversion)
609 {
610 visitTypeConversion(_funCall);
611 return;
612 }
613
614 FunctionType const& funType = dynamic_cast<FunctionType const&>(*_funCall.expression().annotation().type);
615
616 std::vector<ASTPointer<Expression const>> const args = _funCall.arguments();
617 switch (funType.kind())
618 {
619 case FunctionType::Kind::Assert:
620 visitAssert(_funCall);
621 break;
622 case FunctionType::Kind::Require:
623 visitRequire(_funCall);
624 break;
625 case FunctionType::Kind::Revert:
626 // Revert is a special case of require and equals to `require(false)`
627 addPathImpliedExpression(smtutil::Expression(false));
628 break;
629 case FunctionType::Kind::GasLeft:
630 visitGasLeft(_funCall);
631 break;
632 case FunctionType::Kind::External:
633 if (isPublicGetter(_funCall.expression()))
634 visitPublicGetter(_funCall);
635 break;
636 case FunctionType::Kind::ABIDecode:
637 case FunctionType::Kind::ABIEncode:
638 case FunctionType::Kind::ABIEncodePacked:
639 case FunctionType::Kind::ABIEncodeWithSelector:
640 case FunctionType::Kind::ABIEncodeCall:
641 case FunctionType::Kind::ABIEncodeWithSignature:
642 visitABIFunction(_funCall);
643 break;
644 case FunctionType::Kind::Internal:
645 case FunctionType::Kind::BareStaticCall:
646 case FunctionType::Kind::BareCall:
647 break;
648 case FunctionType::Kind::KECCAK256:
649 case FunctionType::Kind::ECRecover:
650 case FunctionType::Kind::SHA256:
651 case FunctionType::Kind::RIPEMD160:
652 visitCryptoFunction(_funCall);
653 break;
654 case FunctionType::Kind::BlockHash:
655 defineExpr(_funCall, state().blockhash(expr(*_funCall.arguments().at(0))));
656 break;
657 case FunctionType::Kind::AddMod:
658 case FunctionType::Kind::MulMod:
659 visitAddMulMod(_funCall);
660 break;
661 case FunctionType::Kind::Unwrap:
662 case FunctionType::Kind::Wrap:
663 visitWrapUnwrap(_funCall);
664 break;
665 case FunctionType::Kind::Send:
666 case FunctionType::Kind::Transfer:
667 {
668 auto const& memberAccess = dynamic_cast<MemberAccess const&>(_funCall.expression());
669 auto const& address = memberAccess.expression();
670 auto const& value = args.front();
671 solAssert(value, "");
672
673 smtutil::Expression thisBalance = state().balance();
674 setSymbolicUnknownValue(thisBalance, TypeProvider::uint256(), m_context);
675
676 state().transfer(state().thisAddress(), expr(address), expr(*value));
677 break;
678 }
679 case FunctionType::Kind::ArrayPush:
680 arrayPush(_funCall);
681 break;
682 case FunctionType::Kind::ArrayPop:
683 arrayPop(_funCall);
684 break;
685 case FunctionType::Kind::Event:
686 case FunctionType::Kind::Error:
687 // This can be safely ignored.
688 break;
689 case FunctionType::Kind::ObjectCreation:
690 visitObjectCreation(_funCall);
691 return;
692 case FunctionType::Kind::DelegateCall:
693 case FunctionType::Kind::BareCallCode:
694 case FunctionType::Kind::BareDelegateCall:
695 case FunctionType::Kind::Creation:
696 default:
697 m_errorReporter.warning(
698 4588_error,
699 _funCall.location(),
700 "Assertion checker does not yet implement this type of function call."
701 );
702 }
703 }
704
visit(ModifierInvocation const & _node)705 bool SMTEncoder::visit(ModifierInvocation const& _node)
706 {
707 if (auto const* args = _node.arguments())
708 for (auto const& arg: *args)
709 if (arg)
710 arg->accept(*this);
711 return false;
712 }
713
initContract(ContractDefinition const & _contract)714 void SMTEncoder::initContract(ContractDefinition const& _contract)
715 {
716 solAssert(m_currentContract == nullptr, "");
717 m_currentContract = &_contract;
718
719 m_context.reset();
720 m_context.pushSolver();
721 createStateVariables(_contract);
722 clearIndices(m_currentContract, nullptr);
723 m_variableUsage.setCurrentContract(_contract);
724 m_checked = true;
725 }
726
initFunction(FunctionDefinition const & _function)727 void SMTEncoder::initFunction(FunctionDefinition const& _function)
728 {
729 solAssert(m_callStack.empty(), "");
730 solAssert(m_currentContract, "");
731 m_context.pushSolver();
732 m_pathConditions.clear();
733 pushCallStack({&_function, nullptr});
734 m_uninterpretedTerms.clear();
735 createStateVariables(*m_currentContract);
736 createLocalVariables(_function);
737 m_arrayAssignmentHappened = false;
738 clearIndices(m_currentContract, &_function);
739 m_checked = true;
740 }
741
visitAssert(FunctionCall const & _funCall)742 void SMTEncoder::visitAssert(FunctionCall const& _funCall)
743 {
744 auto const& args = _funCall.arguments();
745 solAssert(args.size() == 1, "");
746 solAssert(args.front()->annotation().type->category() == Type::Category::Bool, "");
747 }
748
visitRequire(FunctionCall const & _funCall)749 void SMTEncoder::visitRequire(FunctionCall const& _funCall)
750 {
751 auto const& args = _funCall.arguments();
752 solAssert(args.size() >= 1, "");
753 solAssert(args.front()->annotation().type->category() == Type::Category::Bool, "");
754 addPathImpliedExpression(expr(*args.front()));
755 }
756
visitABIFunction(FunctionCall const & _funCall)757 void SMTEncoder::visitABIFunction(FunctionCall const& _funCall)
758 {
759 auto symbFunction = state().abiFunction(&_funCall);
760 auto const& [name, inTypes, outTypes] = state().abiFunctionTypes(&_funCall);
761
762 auto const& funType = dynamic_cast<FunctionType const&>(*_funCall.expression().annotation().type);
763 auto kind = funType.kind();
764 auto const& args = _funCall.sortedArguments();
765 auto argsActualLength = kind == FunctionType::Kind::ABIDecode ? 1 : args.size();
766
767 solAssert(inTypes.size() == argsActualLength, "");
768 if (argsActualLength == 0)
769 {
770 defineExpr(_funCall, smt::zeroValue(TypeProvider::bytesMemory()));
771 return;
772 }
773 vector<smtutil::Expression> symbArgs;
774 for (unsigned i = 0; i < argsActualLength; ++i)
775 if (args.at(i))
776 symbArgs.emplace_back(expr(*args.at(i), inTypes.at(i)));
777
778 optional<smtutil::Expression> arg;
779 if (inTypes.size() == 1)
780 arg = expr(*args.at(0), inTypes.at(0));
781 else
782 {
783 auto inputSort = dynamic_cast<smtutil::ArraySort&>(*symbFunction.sort).domain;
784 arg = smtutil::Expression::tuple_constructor(
785 smtutil::Expression(make_shared<smtutil::SortSort>(inputSort), ""),
786 symbArgs
787 );
788 }
789
790 auto out = smtutil::Expression::select(symbFunction, *arg);
791 if (outTypes.size() == 1)
792 defineExpr(_funCall, out);
793 else
794 {
795 auto symbTuple = dynamic_pointer_cast<smt::SymbolicTupleVariable>(m_context.expression(_funCall));
796 solAssert(symbTuple, "");
797 solAssert(symbTuple->components().size() == outTypes.size(), "");
798 solAssert(out.sort->kind == smtutil::Kind::Tuple, "");
799
800 symbTuple->increaseIndex();
801 for (unsigned i = 0; i < symbTuple->components().size(); ++i)
802 m_context.addAssertion(symbTuple->component(i) == smtutil::Expression::tuple_get(out, i));
803 }
804 }
805
visitCryptoFunction(FunctionCall const & _funCall)806 void SMTEncoder::visitCryptoFunction(FunctionCall const& _funCall)
807 {
808 auto const& funType = dynamic_cast<FunctionType const&>(*_funCall.expression().annotation().type);
809 auto kind = funType.kind();
810 auto arg0 = expr(*_funCall.arguments().at(0));
811 optional<smtutil::Expression> result;
812 if (kind == FunctionType::Kind::KECCAK256)
813 result = smtutil::Expression::select(state().cryptoFunction("keccak256"), arg0);
814 else if (kind == FunctionType::Kind::SHA256)
815 result = smtutil::Expression::select(state().cryptoFunction("sha256"), arg0);
816 else if (kind == FunctionType::Kind::RIPEMD160)
817 result = smtutil::Expression::select(state().cryptoFunction("ripemd160"), arg0);
818 else if (kind == FunctionType::Kind::ECRecover)
819 {
820 auto e = state().cryptoFunction("ecrecover");
821 auto arg0 = expr(*_funCall.arguments().at(0));
822 auto arg1 = expr(*_funCall.arguments().at(1));
823 auto arg2 = expr(*_funCall.arguments().at(2));
824 auto arg3 = expr(*_funCall.arguments().at(3));
825 auto inputSort = dynamic_cast<smtutil::ArraySort&>(*e.sort).domain;
826 auto ecrecoverInput = smtutil::Expression::tuple_constructor(
827 smtutil::Expression(make_shared<smtutil::SortSort>(inputSort), ""),
828 {arg0, arg1, arg2, arg3}
829 );
830 result = smtutil::Expression::select(e, ecrecoverInput);
831 }
832 else
833 solAssert(false, "");
834
835 defineExpr(_funCall, *result);
836 }
837
visitGasLeft(FunctionCall const & _funCall)838 void SMTEncoder::visitGasLeft(FunctionCall const& _funCall)
839 {
840 string gasLeft = "gasleft";
841 // We increase the variable index since gasleft changes
842 // inside a tx.
843 defineGlobalVariable(gasLeft, _funCall, true);
844 auto const& symbolicVar = m_context.globalSymbol(gasLeft);
845 unsigned index = symbolicVar->index();
846 // We set the current value to unknown anyway to add type constraints.
847 m_context.setUnknownValue(*symbolicVar);
848 if (index > 0)
849 m_context.addAssertion(symbolicVar->currentValue() <= symbolicVar->valueAtIndex(index - 1));
850 }
851
visitAddMulMod(FunctionCall const & _funCall)852 void SMTEncoder::visitAddMulMod(FunctionCall const& _funCall)
853 {
854 auto const& funType = dynamic_cast<FunctionType const&>(*_funCall.expression().annotation().type);
855 auto kind = funType.kind();
856 solAssert(kind == FunctionType::Kind::AddMod || kind == FunctionType::Kind::MulMod, "");
857 auto const& args = _funCall.arguments();
858 solAssert(args.at(0) && args.at(1) && args.at(2), "");
859 auto x = expr(*args.at(0));
860 auto y = expr(*args.at(1));
861 auto k = expr(*args.at(2));
862 auto const& intType = dynamic_cast<IntegerType const&>(*_funCall.annotation().type);
863
864 if (kind == FunctionType::Kind::AddMod)
865 defineExpr(_funCall, divModWithSlacks(x + y, k, intType).second);
866 else
867 defineExpr(_funCall, divModWithSlacks(x * y, k, intType).second);
868 }
869
visitWrapUnwrap(FunctionCall const & _funCall)870 void SMTEncoder::visitWrapUnwrap(FunctionCall const& _funCall)
871 {
872 auto const& args = _funCall.arguments();
873 solAssert(args.size() == 1, "");
874 defineExpr(_funCall, expr(*args.front()));
875 }
876
visitObjectCreation(FunctionCall const & _funCall)877 void SMTEncoder::visitObjectCreation(FunctionCall const& _funCall)
878 {
879 auto const& args = _funCall.arguments();
880 solAssert(args.size() >= 1, "");
881 auto argType = args.front()->annotation().type->category();
882 solAssert(argType == Type::Category::Integer || argType == Type::Category::RationalNumber, "");
883
884 smtutil::Expression arraySize = expr(*args.front());
885 setSymbolicUnknownValue(arraySize, TypeProvider::uint256(), m_context);
886
887 auto symbArray = dynamic_pointer_cast<smt::SymbolicArrayVariable>(m_context.expression(_funCall));
888 solAssert(symbArray, "");
889 smt::setSymbolicZeroValue(*symbArray, m_context);
890 auto zeroElements = symbArray->elements();
891 symbArray->increaseIndex();
892 m_context.addAssertion(symbArray->length() == arraySize);
893 m_context.addAssertion(symbArray->elements() == zeroElements);
894 }
895
endVisit(Identifier const & _identifier)896 void SMTEncoder::endVisit(Identifier const& _identifier)
897 {
898 if (auto decl = identifierToVariable(_identifier))
899 {
900 if (decl->isConstant())
901 defineExpr(_identifier, constantExpr(_identifier, *decl));
902 else
903 defineExpr(_identifier, currentValue(*decl));
904 }
905 else if (_identifier.annotation().type->category() == Type::Category::Function)
906 visitFunctionIdentifier(_identifier);
907 else if (_identifier.name() == "now")
908 defineGlobalVariable(_identifier.name(), _identifier);
909 else if (_identifier.name() == "this")
910 {
911 defineExpr(_identifier, state().thisAddress());
912 m_uninterpretedTerms.insert(&_identifier);
913 }
914 // Ignore type identifiers
915 else if (dynamic_cast<TypeType const*>(_identifier.annotation().type))
916 return;
917 // Ignore module identifiers
918 else if (dynamic_cast<ModuleType const*>(_identifier.annotation().type))
919 return;
920 // Ignore user defined value type identifiers
921 else if (dynamic_cast<UserDefinedValueType const*>(_identifier.annotation().type))
922 return;
923 // Ignore the builtin abi, it is handled in FunctionCall.
924 // TODO: ignore MagicType in general (abi, block, msg, tx, type)
925 else if (auto magicType = dynamic_cast<MagicType const*>(_identifier.annotation().type); magicType && magicType->kind() == MagicType::Kind::ABI)
926 {
927 solAssert(_identifier.name() == "abi", "");
928 return;
929 }
930 else
931 createExpr(_identifier);
932 }
933
endVisit(ElementaryTypeNameExpression const & _typeName)934 void SMTEncoder::endVisit(ElementaryTypeNameExpression const& _typeName)
935 {
936 auto const& typeType = dynamic_cast<TypeType const&>(*_typeName.annotation().type);
937 auto result = smt::newSymbolicVariable(
938 *TypeProvider::uint256(),
939 typeType.actualType()->toString(false),
940 m_context
941 );
942 solAssert(!result.first && result.second, "");
943 m_context.createExpression(_typeName, result.second);
944 }
945
946 namespace // helpers for SMTEncoder::visitPublicGetter
947 {
948
isReturnedFromStructGetter(Type const * _type)949 bool isReturnedFromStructGetter(Type const* _type)
950 {
951 // So far it seems that only Mappings and ordinary Arrays are not returned.
952 auto category = _type->category();
953 if (category == Type::Category::Mapping)
954 return false;
955 if (category == Type::Category::Array)
956 return dynamic_cast<ArrayType const&>(*_type).isByteArray();
957 // default
958 return true;
959 }
960
structGetterReturnedMembers(StructType const & _structType)961 vector<string> structGetterReturnedMembers(StructType const& _structType)
962 {
963 vector<string> returnedMembers;
964 for (auto const& member: _structType.nativeMembers(nullptr))
965 if (isReturnedFromStructGetter(member.type))
966 returnedMembers.push_back(member.name);
967 return returnedMembers;
968 }
969
970 }
971
visitPublicGetter(FunctionCall const & _funCall)972 void SMTEncoder::visitPublicGetter(FunctionCall const& _funCall)
973 {
974 MemberAccess const& access = dynamic_cast<MemberAccess const&>(_funCall.expression());
975 auto var = dynamic_cast<VariableDeclaration const*>(access.annotation().referencedDeclaration);
976 solAssert(var, "");
977 solAssert(m_context.knownExpression(_funCall), "");
978 auto paramExpectedTypes = replaceUserTypes(FunctionType(*var).parameterTypes());
979 auto actualArguments = _funCall.arguments();
980 solAssert(actualArguments.size() == paramExpectedTypes.size(), "");
981 deque<smtutil::Expression> symbArguments;
982 for (unsigned i = 0; i < paramExpectedTypes.size(); ++i)
983 symbArguments.push_back(expr(*actualArguments[i], paramExpectedTypes[i]));
984
985 // See FunctionType::FunctionType(VariableDeclaration const& _varDecl)
986 // to understand the return types of public getters.
987 Type const* type = var->type();
988 smtutil::Expression currentExpr = currentValue(*var);
989 while (true)
990 {
991 if (
992 type->isValueType() ||
993 (type->category() == Type::Category::Array && dynamic_cast<ArrayType const&>(*type).isByteArray())
994 )
995 {
996 solAssert(symbArguments.empty(), "");
997 defineExpr(_funCall, currentExpr);
998 return;
999 }
1000 switch (type->category())
1001 {
1002 case Type::Category::Array:
1003 case Type::Category::Mapping:
1004 {
1005 solAssert(!symbArguments.empty(), "");
1006 // For nested arrays/mappings, each argument in the call is an index to the next layer.
1007 // We mirror this with `select` after unpacking the SMT-LIB array expression.
1008 currentExpr = smtutil::Expression::select(smtutil::Expression::tuple_get(currentExpr, 0), symbArguments.front());
1009 symbArguments.pop_front();
1010 if (auto arrayType = dynamic_cast<ArrayType const*>(type))
1011 type = arrayType->baseType();
1012 else if (auto mappingType = dynamic_cast<MappingType const*>(type))
1013 type = mappingType->valueType();
1014 else
1015 solAssert(false, "");
1016 break;
1017 }
1018 case Type::Category::Struct:
1019 {
1020 solAssert(symbArguments.empty(), "");
1021 smt::SymbolicStructVariable structVar(dynamic_cast<StructType const*>(type), "struct_temp_" + to_string(_funCall.id()), m_context);
1022 m_context.addAssertion(structVar.currentValue() == currentExpr);
1023 auto returnedMembers = structGetterReturnedMembers(dynamic_cast<StructType const&>(*structVar.type()));
1024 solAssert(!returnedMembers.empty(), "");
1025 auto returnedValues = applyMap(returnedMembers, [&](string const& memberName) -> optional<smtutil::Expression> { return structVar.member(memberName); });
1026 defineExpr(_funCall, returnedValues);
1027 return;
1028 }
1029 default:
1030 {
1031 // Unsupported cases, do nothing and the getter will be abstracted.
1032 return;
1033 }
1034 }
1035 }
1036 }
1037
shouldAnalyze(ContractDefinition const & _contract) const1038 bool SMTEncoder::shouldAnalyze(ContractDefinition const& _contract) const
1039 {
1040 if (!_contract.canBeDeployed())
1041 return false;
1042
1043 return m_settings.contracts.isDefault() ||
1044 m_settings.contracts.has(_contract.sourceUnitName(), _contract.name());
1045 }
1046
visitTypeConversion(FunctionCall const & _funCall)1047 void SMTEncoder::visitTypeConversion(FunctionCall const& _funCall)
1048 {
1049 solAssert(*_funCall.annotation().kind == FunctionCallKind::TypeConversion, "");
1050 solAssert(_funCall.arguments().size() == 1, "");
1051
1052 auto argument = _funCall.arguments().front();
1053 auto const argType = argument->annotation().type;
1054 auto const funCallType = _funCall.annotation().type;
1055
1056 auto symbArg = expr(*argument, funCallType);
1057
1058 if (smt::isStringLiteral(*argType) && smt::isFixedBytes(*funCallType))
1059 {
1060 defineExpr(_funCall, symbArg);
1061 return;
1062 }
1063
1064 ArrayType const* arrayType = dynamic_cast<ArrayType const*>(argType);
1065 if (auto sliceType = dynamic_cast<ArraySliceType const*>(argType))
1066 arrayType = &sliceType->arrayType();
1067
1068 if (arrayType && arrayType->isByteArray() && smt::isFixedBytes(*funCallType))
1069 {
1070 auto array = dynamic_pointer_cast<smt::SymbolicArrayVariable>(m_context.expression(*argument));
1071 bytesToFixedBytesAssertions(*array, _funCall);
1072 return;
1073 }
1074
1075 // TODO Simplify this whole thing for 0.8.0 where weird casts are disallowed.
1076
1077 unsigned argSize = argType->storageBytes();
1078 unsigned castSize = funCallType->storageBytes();
1079 bool castIsSigned = smt::isNumber(*funCallType) && smt::isSigned(funCallType);
1080 bool argIsSigned = smt::isNumber(*argType) && smt::isSigned(argType);
1081 optional<smtutil::Expression> symbMin;
1082 optional<smtutil::Expression> symbMax;
1083 if (smt::isNumber(*funCallType))
1084 {
1085 symbMin = smt::minValue(funCallType);
1086 symbMax = smt::maxValue(funCallType);
1087 }
1088 if (argSize == castSize)
1089 {
1090 // If sizes are the same, it's possible that the signs are different.
1091 if (smt::isNumber(*funCallType) && smt::isNumber(*argType))
1092 {
1093 // castIsSigned && !argIsSigned => might overflow if arg > castType.max
1094 // !castIsSigned && argIsSigned => might underflow if arg < castType.min
1095 // !castIsSigned && !argIsSigned => ok
1096 // castIsSigned && argIsSigned => ok
1097
1098 if (castIsSigned && !argIsSigned)
1099 {
1100 auto wrap = smtutil::Expression::ite(
1101 symbArg > *symbMax,
1102 symbArg - (*symbMax - *symbMin + 1),
1103 symbArg
1104 );
1105 defineExpr(_funCall, wrap);
1106 }
1107 else if (!castIsSigned && argIsSigned)
1108 {
1109 auto wrap = smtutil::Expression::ite(
1110 symbArg < *symbMin,
1111 symbArg + (*symbMax + 1),
1112 symbArg
1113 );
1114 defineExpr(_funCall, wrap);
1115 }
1116 else
1117 defineExpr(_funCall, symbArg);
1118 }
1119 else
1120 defineExpr(_funCall, symbArg);
1121 }
1122 else if (castSize > argSize)
1123 {
1124 solAssert(smt::isNumber(*funCallType), "");
1125 // RationalNumbers have size 32.
1126 solAssert(argType->category() != Type::Category::RationalNumber, "");
1127
1128 // castIsSigned && !argIsSigned => ok
1129 // castIsSigned && argIsSigned => ok
1130 // !castIsSigned && !argIsSigned => ok except for FixedBytesType, need to adjust padding
1131 // !castIsSigned && argIsSigned => might underflow if arg < castType.min
1132
1133 if (!castIsSigned && argIsSigned)
1134 {
1135 auto wrap = smtutil::Expression::ite(
1136 symbArg < *symbMin,
1137 symbArg + (*symbMax + 1),
1138 symbArg
1139 );
1140 defineExpr(_funCall, wrap);
1141 }
1142 else if (!castIsSigned && !argIsSigned)
1143 {
1144 if (auto const* fixedCast = dynamic_cast<FixedBytesType const*>(funCallType))
1145 {
1146 auto const* fixedArg = dynamic_cast<FixedBytesType const*>(argType);
1147 solAssert(fixedArg, "");
1148 auto diff = fixedCast->numBytes() - fixedArg->numBytes();
1149 solAssert(diff > 0, "");
1150 auto bvSize = fixedCast->numBytes() * 8;
1151 defineExpr(
1152 _funCall,
1153 smtutil::Expression::bv2int(smtutil::Expression::int2bv(symbArg, bvSize) << smtutil::Expression::int2bv(diff * 8, bvSize))
1154 );
1155 }
1156 else
1157 defineExpr(_funCall, symbArg);
1158 }
1159 else
1160 defineExpr(_funCall, symbArg);
1161 }
1162 else // castSize < argSize
1163 {
1164 solAssert(smt::isNumber(*funCallType), "");
1165
1166 RationalNumberType const* rationalType = isConstant(*argument);
1167 if (rationalType)
1168 {
1169 // The TypeChecker guarantees that a constant fits in the cast size.
1170 defineExpr(_funCall, symbArg);
1171 return;
1172 }
1173
1174 auto const* fixedCast = dynamic_cast<FixedBytesType const*>(funCallType);
1175 auto const* fixedArg = dynamic_cast<FixedBytesType const*>(argType);
1176 if (fixedCast && fixedArg)
1177 {
1178 createExpr(_funCall);
1179 auto diff = argSize - castSize;
1180 solAssert(fixedArg->numBytes() - fixedCast->numBytes() == diff, "");
1181
1182 auto argValueBV = smtutil::Expression::int2bv(symbArg, argSize * 8);
1183 auto shr = smtutil::Expression::int2bv(diff * 8, argSize * 8);
1184 solAssert(!castIsSigned, "");
1185 defineExpr(_funCall, smtutil::Expression::bv2int(argValueBV >> shr));
1186 }
1187 else
1188 {
1189 auto argValueBV = smtutil::Expression::int2bv(symbArg, castSize * 8);
1190 defineExpr(_funCall, smtutil::Expression::bv2int(argValueBV, castIsSigned));
1191 }
1192 }
1193 }
1194
visitFunctionIdentifier(Identifier const & _identifier)1195 void SMTEncoder::visitFunctionIdentifier(Identifier const& _identifier)
1196 {
1197 auto const& fType = dynamic_cast<FunctionType const&>(*_identifier.annotation().type);
1198 if (replaceUserTypes(fType.returnParameterTypes()).size() == 1)
1199 {
1200 defineGlobalVariable(fType.identifier(), _identifier);
1201 m_context.createExpression(_identifier, m_context.globalSymbol(fType.identifier()));
1202 }
1203 }
1204
visitStructConstructorCall(FunctionCall const & _funCall)1205 void SMTEncoder::visitStructConstructorCall(FunctionCall const& _funCall)
1206 {
1207 solAssert(*_funCall.annotation().kind == FunctionCallKind::StructConstructorCall, "");
1208 if (smt::isNonRecursiveStruct(*_funCall.annotation().type))
1209 {
1210 auto& structSymbolicVar = dynamic_cast<smt::SymbolicStructVariable&>(*m_context.expression(_funCall));
1211 auto structType = dynamic_cast<StructType const*>(structSymbolicVar.type());
1212 solAssert(structType, "");
1213 auto const& structMembers = structType->structDefinition().members();
1214 solAssert(structMembers.size() == _funCall.sortedArguments().size(), "");
1215 auto args = _funCall.sortedArguments();
1216 structSymbolicVar.assignAllMembers(applyMap(
1217 ranges::views::zip(args, structMembers),
1218 [this] (auto const& argMemberPair) { return expr(*argMemberPair.first, argMemberPair.second->type()); }
1219 ));
1220 }
1221
1222 }
1223
endVisit(Literal const & _literal)1224 void SMTEncoder::endVisit(Literal const& _literal)
1225 {
1226 solAssert(_literal.annotation().type, "Expected type for AST node");
1227 Type const& type = *_literal.annotation().type;
1228 if (smt::isNumber(type))
1229 defineExpr(_literal, smtutil::Expression(type.literalValue(&_literal)));
1230 else if (smt::isBool(type))
1231 defineExpr(_literal, smtutil::Expression(_literal.token() == Token::TrueLiteral ? true : false));
1232 else if (smt::isStringLiteral(type))
1233 {
1234 createExpr(_literal);
1235
1236 // Add constraints for the length and values as it is known.
1237 auto symbArray = dynamic_pointer_cast<smt::SymbolicArrayVariable>(m_context.expression(_literal));
1238 solAssert(symbArray, "");
1239
1240 addArrayLiteralAssertions(
1241 *symbArray,
1242 applyMap(_literal.value(), [](unsigned char c) { return smtutil::Expression{size_t(c)}; })
1243 );
1244 }
1245 else
1246 solAssert(false, "");
1247 }
1248
addArrayLiteralAssertions(smt::SymbolicArrayVariable & _symArray,vector<smtutil::Expression> const & _elementValues)1249 void SMTEncoder::addArrayLiteralAssertions(
1250 smt::SymbolicArrayVariable& _symArray,
1251 vector<smtutil::Expression> const& _elementValues
1252 )
1253 {
1254 m_context.addAssertion(_symArray.length() == _elementValues.size());
1255 for (size_t i = 0; i < _elementValues.size(); i++)
1256 m_context.addAssertion(smtutil::Expression::select(_symArray.elements(), i) == _elementValues[i]);
1257 }
1258
bytesToFixedBytesAssertions(smt::SymbolicArrayVariable & _symArray,Expression const & _fixedBytes)1259 void SMTEncoder::bytesToFixedBytesAssertions(
1260 smt::SymbolicArrayVariable& _symArray,
1261 Expression const& _fixedBytes
1262 )
1263 {
1264 auto const& fixed = dynamic_cast<FixedBytesType const&>(*_fixedBytes.annotation().type);
1265 auto intType = TypeProvider::uint256();
1266 string suffix = to_string(_fixedBytes.id()) + "_" + to_string(m_context.newUniqueId());
1267 smt::SymbolicIntVariable k(intType, intType, "k_" + suffix, m_context);
1268 m_context.addAssertion(k.currentValue() == 0);
1269 size_t n = fixed.numBytes();
1270 for (size_t i = 0; i < n; i++)
1271 {
1272 auto kPrev = k.currentValue();
1273 m_context.addAssertion((smtutil::Expression::select(_symArray.elements(), i) * (u256(1) << ((n - i - 1) * 8))) + kPrev == k.increaseIndex());
1274 }
1275 m_context.addAssertion(expr(_fixedBytes) == k.currentValue());
1276 }
1277
endVisit(Return const & _return)1278 void SMTEncoder::endVisit(Return const& _return)
1279 {
1280 if (_return.expression() && m_context.knownExpression(*_return.expression()))
1281 {
1282 auto returnParams = m_callStack.back().first->returnParameters();
1283 if (returnParams.size() > 1)
1284 {
1285 auto const& symbTuple = dynamic_pointer_cast<smt::SymbolicTupleVariable>(m_context.expression(*_return.expression()));
1286 solAssert(symbTuple, "");
1287 solAssert(symbTuple->components().size() == returnParams.size(), "");
1288
1289 auto const* tupleType = dynamic_cast<TupleType const*>(_return.expression()->annotation().type);
1290 solAssert(tupleType, "");
1291 auto const& types = tupleType->components();
1292 solAssert(types.size() == returnParams.size(), "");
1293
1294 for (unsigned i = 0; i < returnParams.size(); ++i)
1295 assignment(*returnParams.at(i), symbTuple->component(i, types.at(i), returnParams.at(i)->type()));
1296 }
1297 else if (returnParams.size() == 1)
1298 assignment(*returnParams.front(), expr(*_return.expression(), returnParams.front()->type()));
1299 }
1300 }
1301
visit(MemberAccess const & _memberAccess)1302 bool SMTEncoder::visit(MemberAccess const& _memberAccess)
1303 {
1304 auto const& accessType = _memberAccess.annotation().type;
1305 if (accessType->category() == Type::Category::Function)
1306 return true;
1307
1308 createExpr(_memberAccess);
1309
1310 Expression const* memberExpr = innermostTuple(_memberAccess.expression());
1311
1312 auto const& exprType = memberExpr->annotation().type;
1313 solAssert(exprType, "");
1314 if (exprType->category() == Type::Category::Magic)
1315 {
1316 if (auto const* identifier = dynamic_cast<Identifier const*>(memberExpr))
1317 {
1318 auto const& name = identifier->name();
1319 solAssert(name == "block" || name == "msg" || name == "tx", "");
1320 defineExpr(_memberAccess, state().txMember(name + "." + _memberAccess.memberName()));
1321 }
1322 else if (auto magicType = dynamic_cast<MagicType const*>(exprType))
1323 {
1324 if (magicType->kind() == MagicType::Kind::Block)
1325 defineExpr(_memberAccess, state().txMember("block." + _memberAccess.memberName()));
1326 else if (magicType->kind() == MagicType::Kind::Message)
1327 defineExpr(_memberAccess, state().txMember("msg." + _memberAccess.memberName()));
1328 else if (magicType->kind() == MagicType::Kind::Transaction)
1329 defineExpr(_memberAccess, state().txMember("tx." + _memberAccess.memberName()));
1330 else if (magicType->kind() == MagicType::Kind::MetaType)
1331 {
1332 auto const& memberName = _memberAccess.memberName();
1333 if (memberName == "min" || memberName == "max")
1334 {
1335 if (IntegerType const* integerType = dynamic_cast<IntegerType const*>(magicType->typeArgument()))
1336 defineExpr(_memberAccess, memberName == "min" ? integerType->minValue() : integerType->maxValue());
1337 else if (EnumType const* enumType = dynamic_cast<EnumType const*>(magicType->typeArgument()))
1338 defineExpr(_memberAccess, memberName == "min" ? enumType->minValue() : enumType->maxValue());
1339 }
1340 else if (memberName == "interfaceId")
1341 {
1342 ContractDefinition const& contract = dynamic_cast<ContractType const&>(*magicType->typeArgument()).contractDefinition();
1343 defineExpr(_memberAccess, contract.interfaceId());
1344 }
1345 else
1346 // NOTE: supporting name, creationCode, runtimeCode would be easy enough, but the bytes/string they return are not
1347 // at all usable in the SMT checker currently
1348 m_errorReporter.warning(
1349 7507_error,
1350 _memberAccess.location(),
1351 "Assertion checker does not yet support this expression."
1352 );
1353
1354 }
1355 }
1356 else
1357 solAssert(false, "");
1358
1359 return false;
1360 }
1361 else if (smt::isNonRecursiveStruct(*exprType))
1362 {
1363 memberExpr->accept(*this);
1364 auto const& symbStruct = dynamic_pointer_cast<smt::SymbolicStructVariable>(m_context.expression(*memberExpr));
1365 defineExpr(_memberAccess, symbStruct->member(_memberAccess.memberName()));
1366 return false;
1367 }
1368 else if (exprType->category() == Type::Category::TypeType)
1369 {
1370 auto const* decl = expressionToDeclaration(*memberExpr);
1371 if (dynamic_cast<EnumDefinition const*>(decl))
1372 {
1373 auto enumType = dynamic_cast<EnumType const*>(accessType);
1374 solAssert(enumType, "");
1375 defineExpr(_memberAccess, enumType->memberValue(_memberAccess.memberName()));
1376
1377 return false;
1378 }
1379 else if (dynamic_cast<ContractDefinition const*>(decl))
1380 {
1381 if (auto const* var = dynamic_cast<VariableDeclaration const*>(_memberAccess.annotation().referencedDeclaration))
1382 {
1383 defineExpr(_memberAccess, currentValue(*var));
1384 return false;
1385 }
1386 }
1387 }
1388 else if (exprType->category() == Type::Category::Address)
1389 {
1390 memberExpr->accept(*this);
1391 if (_memberAccess.memberName() == "balance")
1392 {
1393 defineExpr(_memberAccess, state().balance(expr(*memberExpr)));
1394 setSymbolicUnknownValue(*m_context.expression(_memberAccess), m_context);
1395 m_uninterpretedTerms.insert(&_memberAccess);
1396 return false;
1397 }
1398 }
1399 else if (exprType->category() == Type::Category::Array)
1400 {
1401 memberExpr->accept(*this);
1402 if (_memberAccess.memberName() == "length")
1403 {
1404 auto symbArray = dynamic_pointer_cast<smt::SymbolicArrayVariable>(m_context.expression(*memberExpr));
1405 solAssert(symbArray, "");
1406 defineExpr(_memberAccess, symbArray->length());
1407 m_uninterpretedTerms.insert(&_memberAccess);
1408 setSymbolicUnknownValue(
1409 expr(_memberAccess),
1410 _memberAccess.annotation().type,
1411 m_context
1412 );
1413 }
1414 return false;
1415 }
1416 else if (
1417 auto const* functionType = dynamic_cast<FunctionType const*>(exprType);
1418 functionType &&
1419 _memberAccess.memberName() == "selector" &&
1420 functionType->hasDeclaration()
1421 )
1422 {
1423 defineExpr(_memberAccess, functionType->externalIdentifier());
1424 return false;
1425 }
1426 else if (exprType->category() == Type::Category::Module)
1427 {
1428 if (auto const* var = dynamic_cast<VariableDeclaration const*>(_memberAccess.annotation().referencedDeclaration))
1429 {
1430 solAssert(var->isConstant(), "");
1431 defineExpr(_memberAccess, constantExpr(_memberAccess, *var));
1432 return false;
1433 }
1434 }
1435
1436 m_errorReporter.warning(
1437 7650_error,
1438 _memberAccess.location(),
1439 "Assertion checker does not yet support this expression."
1440 );
1441
1442 return true;
1443 }
1444
endVisit(IndexAccess const & _indexAccess)1445 void SMTEncoder::endVisit(IndexAccess const& _indexAccess)
1446 {
1447 createExpr(_indexAccess);
1448
1449 if (_indexAccess.annotation().type->category() == Type::Category::TypeType)
1450 return;
1451
1452 makeOutOfBoundsVerificationTarget(_indexAccess);
1453
1454 if (auto const* type = dynamic_cast<FixedBytesType const*>(_indexAccess.baseExpression().annotation().type))
1455 {
1456 smtutil::Expression base = expr(_indexAccess.baseExpression());
1457
1458 if (type->numBytes() == 1)
1459 defineExpr(_indexAccess, base);
1460 else
1461 {
1462 auto [bvSize, isSigned] = smt::typeBvSizeAndSignedness(_indexAccess.baseExpression().annotation().type);
1463 solAssert(!isSigned, "");
1464 solAssert(bvSize >= 16, "");
1465 solAssert(bvSize % 8 == 0, "");
1466
1467 smtutil::Expression idx = expr(*_indexAccess.indexExpression());
1468
1469 auto bvBase = smtutil::Expression::int2bv(base, bvSize);
1470 auto bvShl = smtutil::Expression::int2bv(idx * 8, bvSize);
1471 auto bvShr = smtutil::Expression::int2bv(bvSize - 8, bvSize);
1472 auto result = (bvBase << bvShl) >> bvShr;
1473
1474 auto anyValue = expr(_indexAccess);
1475 m_context.expression(_indexAccess)->increaseIndex();
1476 unsigned numBytes = bvSize / 8;
1477 auto withBound = smtutil::Expression::ite(
1478 idx < numBytes,
1479 smtutil::Expression::bv2int(result, false),
1480 anyValue
1481 );
1482 defineExpr(_indexAccess, withBound);
1483 }
1484 return;
1485 }
1486
1487 shared_ptr<smt::SymbolicVariable> array;
1488 if (auto const* id = dynamic_cast<Identifier const*>(&_indexAccess.baseExpression()))
1489 {
1490 auto varDecl = identifierToVariable(*id);
1491 solAssert(varDecl, "");
1492 array = m_context.variable(*varDecl);
1493
1494 if (varDecl && varDecl->isConstant())
1495 m_context.addAssertion(currentValue(*varDecl) == expr(*id));
1496 }
1497 else
1498 {
1499 solAssert(m_context.knownExpression(_indexAccess.baseExpression()), "");
1500 array = m_context.expression(_indexAccess.baseExpression());
1501 }
1502
1503 auto arrayVar = dynamic_pointer_cast<smt::SymbolicArrayVariable>(array);
1504 solAssert(arrayVar, "");
1505
1506 Type const* baseType = _indexAccess.baseExpression().annotation().type;
1507 defineExpr(_indexAccess, smtutil::Expression::select(
1508 arrayVar->elements(),
1509 expr(*_indexAccess.indexExpression(), keyType(baseType))
1510 ));
1511 setSymbolicUnknownValue(
1512 expr(_indexAccess),
1513 _indexAccess.annotation().type,
1514 m_context
1515 );
1516 m_uninterpretedTerms.insert(&_indexAccess);
1517 }
1518
endVisit(IndexRangeAccess const & _indexRangeAccess)1519 void SMTEncoder::endVisit(IndexRangeAccess const& _indexRangeAccess)
1520 {
1521 createExpr(_indexRangeAccess);
1522 /// The actual slice is created by CHC which also assigns the length.
1523 }
1524
arrayAssignment()1525 void SMTEncoder::arrayAssignment()
1526 {
1527 m_arrayAssignmentHappened = true;
1528 }
1529
indexOrMemberAssignment(Expression const & _expr,smtutil::Expression const & _rightHandSide)1530 void SMTEncoder::indexOrMemberAssignment(Expression const& _expr, smtutil::Expression const& _rightHandSide)
1531 {
1532 auto toStore = _rightHandSide;
1533 auto const* lastExpr = &_expr;
1534 while (true)
1535 {
1536 if (auto const* indexAccess = dynamic_cast<IndexAccess const*>(lastExpr))
1537 {
1538 auto const& base = indexAccess->baseExpression();
1539 if (dynamic_cast<Identifier const*>(&base))
1540 base.accept(*this);
1541
1542 Type const* baseType = base.annotation().type;
1543 auto indexExpr = expr(*indexAccess->indexExpression(), keyType(baseType));
1544 auto symbArray = dynamic_pointer_cast<smt::SymbolicArrayVariable>(m_context.expression(base));
1545 solAssert(symbArray, "");
1546 toStore = smtutil::Expression::tuple_constructor(
1547 smtutil::Expression(make_shared<smtutil::SortSort>(smt::smtSort(*baseType)), baseType->toString(true)),
1548 {smtutil::Expression::store(symbArray->elements(), indexExpr, toStore), symbArray->length()}
1549 );
1550 defineExpr(*indexAccess, smtutil::Expression::select(
1551 symbArray->elements(),
1552 indexExpr
1553 ));
1554 lastExpr = &indexAccess->baseExpression();
1555 }
1556 else if (auto const* memberAccess = dynamic_cast<MemberAccess const*>(lastExpr))
1557 {
1558 auto const& base = memberAccess->expression();
1559 if (dynamic_cast<Identifier const*>(&base))
1560 base.accept(*this);
1561
1562 if (
1563 auto const* structType = dynamic_cast<StructType const*>(base.annotation().type);
1564 structType && structType->recursive()
1565 )
1566 {
1567 m_errorReporter.warning(
1568 4375_error,
1569 memberAccess->location(),
1570 "Assertion checker does not support recursive structs."
1571 );
1572 return;
1573 }
1574 if (auto varDecl = identifierToVariable(*memberAccess))
1575 {
1576 if (varDecl->hasReferenceOrMappingType())
1577 resetReferences(*varDecl);
1578
1579 assignment(*varDecl, toStore);
1580 break;
1581 }
1582
1583 auto symbStruct = dynamic_pointer_cast<smt::SymbolicStructVariable>(m_context.expression(base));
1584 solAssert(symbStruct, "");
1585 symbStruct->assignMember(memberAccess->memberName(), toStore);
1586 toStore = symbStruct->currentValue();
1587 defineExpr(*memberAccess, symbStruct->member(memberAccess->memberName()));
1588 lastExpr = &memberAccess->expression();
1589 }
1590 else if (auto const& id = dynamic_cast<Identifier const*>(lastExpr))
1591 {
1592 auto varDecl = identifierToVariable(*id);
1593 solAssert(varDecl, "");
1594
1595 if (varDecl->hasReferenceOrMappingType())
1596 resetReferences(*varDecl);
1597
1598 assignment(*varDecl, toStore);
1599 defineExpr(*id, currentValue(*varDecl));
1600 break;
1601 }
1602 else
1603 {
1604 auto type = lastExpr->annotation().type;
1605 if (
1606 dynamic_cast<ReferenceType const*>(type) ||
1607 dynamic_cast<MappingType const*>(type)
1608 )
1609 resetReferences(type);
1610
1611 assignment(*m_context.expression(*lastExpr), toStore);
1612 break;
1613 }
1614 }
1615 }
1616
arrayPush(FunctionCall const & _funCall)1617 void SMTEncoder::arrayPush(FunctionCall const& _funCall)
1618 {
1619 auto memberAccess = dynamic_cast<MemberAccess const*>(&_funCall.expression());
1620 solAssert(memberAccess, "");
1621 auto symbArray = dynamic_pointer_cast<smt::SymbolicArrayVariable>(m_context.expression(memberAccess->expression()));
1622 solAssert(symbArray, "");
1623 auto oldLength = symbArray->length();
1624 m_context.addAssertion(oldLength >= 0);
1625 // Real world assumption: the array length is assumed to not overflow.
1626 // This assertion guarantees that both the current and updated lengths have the above property.
1627 m_context.addAssertion(oldLength + 1 < (smt::maxValue(*TypeProvider::uint256()) - 1));
1628
1629 auto const& arguments = _funCall.arguments();
1630 auto arrayType = dynamic_cast<ArrayType const*>(symbArray->type());
1631 solAssert(arrayType, "");
1632 auto elementType = arrayType->baseType();
1633 smtutil::Expression element = arguments.empty() ?
1634 smt::zeroValue(elementType) :
1635 expr(*arguments.front(), elementType);
1636 smtutil::Expression store = smtutil::Expression::store(
1637 symbArray->elements(),
1638 oldLength,
1639 element
1640 );
1641 symbArray->increaseIndex();
1642 m_context.addAssertion(symbArray->elements() == store);
1643 m_context.addAssertion(symbArray->length() == oldLength + 1);
1644
1645 if (arguments.empty())
1646 defineExpr(_funCall, element);
1647
1648 assignment(memberAccess->expression(), symbArray->currentValue());
1649 }
1650
arrayPop(FunctionCall const & _funCall)1651 void SMTEncoder::arrayPop(FunctionCall const& _funCall)
1652 {
1653 auto memberAccess = dynamic_cast<MemberAccess const*>(cleanExpression(_funCall.expression()));
1654 solAssert(memberAccess, "");
1655 auto symbArray = dynamic_pointer_cast<smt::SymbolicArrayVariable>(m_context.expression(memberAccess->expression()));
1656 solAssert(symbArray, "");
1657
1658 makeArrayPopVerificationTarget(_funCall);
1659
1660 auto oldElements = symbArray->elements();
1661 auto oldLength = symbArray->length();
1662
1663 symbArray->increaseIndex();
1664 m_context.addAssertion(symbArray->elements() == oldElements);
1665 auto newLength = smtutil::Expression::ite(
1666 oldLength > 0,
1667 oldLength - 1,
1668 0
1669 );
1670 m_context.addAssertion(symbArray->length() == newLength);
1671
1672 assignment(memberAccess->expression(), symbArray->currentValue());
1673 }
1674
defineGlobalVariable(string const & _name,Expression const & _expr,bool _increaseIndex)1675 void SMTEncoder::defineGlobalVariable(string const& _name, Expression const& _expr, bool _increaseIndex)
1676 {
1677 if (!m_context.knownGlobalSymbol(_name))
1678 {
1679 bool abstract = m_context.createGlobalSymbol(_name, _expr);
1680 if (abstract)
1681 m_errorReporter.warning(
1682 1695_error,
1683 _expr.location(),
1684 "Assertion checker does not yet support this global variable."
1685 );
1686 }
1687 else if (_increaseIndex)
1688 m_context.globalSymbol(_name)->increaseIndex();
1689 // The default behavior is not to increase the index since
1690 // most of the global values stay the same throughout a tx.
1691 if (isSupportedType(*_expr.annotation().type))
1692 defineExpr(_expr, m_context.globalSymbol(_name)->currentValue());
1693 }
1694
shortcutRationalNumber(Expression const & _expr)1695 bool SMTEncoder::shortcutRationalNumber(Expression const& _expr)
1696 {
1697 RationalNumberType const* rationalType = isConstant(_expr);
1698 if (!rationalType)
1699 return false;
1700
1701 if (rationalType->isNegative())
1702 defineExpr(_expr, smtutil::Expression(u2s(rationalType->literalValue(nullptr))));
1703 else
1704 defineExpr(_expr, smtutil::Expression(rationalType->literalValue(nullptr)));
1705 return true;
1706 }
1707
arithmeticOperation(BinaryOperation const & _op)1708 void SMTEncoder::arithmeticOperation(BinaryOperation const& _op)
1709 {
1710 auto type = _op.annotation().commonType;
1711 solAssert(type, "");
1712 solAssert(type->category() == Type::Category::Integer || type->category() == Type::Category::FixedPoint, "");
1713 switch (_op.getOperator())
1714 {
1715 case Token::Add:
1716 case Token::Sub:
1717 case Token::Mul:
1718 case Token::Div:
1719 case Token::Mod:
1720 {
1721 auto values = arithmeticOperation(
1722 _op.getOperator(),
1723 expr(_op.leftExpression()),
1724 expr(_op.rightExpression()),
1725 _op.annotation().commonType,
1726 _op
1727 );
1728 defineExpr(_op, values.first);
1729 break;
1730 }
1731 default:
1732 m_errorReporter.warning(
1733 5188_error,
1734 _op.location(),
1735 "Assertion checker does not yet implement this operator."
1736 );
1737 }
1738 }
1739
arithmeticOperation(Token _op,smtutil::Expression const & _left,smtutil::Expression const & _right,Type const * _commonType,Expression const & _operation)1740 pair<smtutil::Expression, smtutil::Expression> SMTEncoder::arithmeticOperation(
1741 Token _op,
1742 smtutil::Expression const& _left,
1743 smtutil::Expression const& _right,
1744 Type const* _commonType,
1745 Expression const& _operation
1746 )
1747 {
1748 static set<Token> validOperators{
1749 Token::Add,
1750 Token::Sub,
1751 Token::Mul,
1752 Token::Div,
1753 Token::Mod
1754 };
1755 solAssert(validOperators.count(_op), "");
1756 solAssert(_commonType, "");
1757 solAssert(
1758 _commonType->category() == Type::Category::Integer || _commonType->category() == Type::Category::FixedPoint,
1759 ""
1760 );
1761
1762 IntegerType const* intType = nullptr;
1763 if (auto type = dynamic_cast<IntegerType const*>(_commonType))
1764 intType = type;
1765 else
1766 intType = TypeProvider::uint256();
1767
1768 auto valueUnbounded = [&]() -> smtutil::Expression {
1769 switch (_op)
1770 {
1771 case Token::Add: return _left + _right;
1772 case Token::Sub: return _left - _right;
1773 case Token::Mul: return _left * _right;
1774 case Token::Div: return divModWithSlacks(_left, _right, *intType).first;
1775 case Token::Mod: return divModWithSlacks(_left, _right, *intType).second;
1776 default: solAssert(false, "");
1777 }
1778 }();
1779
1780 if (m_checked)
1781 return {valueUnbounded, valueUnbounded};
1782
1783 if (_op == Token::Div || _op == Token::Mod)
1784 {
1785 // mod and unsigned division never underflow/overflow
1786 if (_op == Token::Mod || !intType->isSigned())
1787 return {valueUnbounded, valueUnbounded};
1788
1789 // The only case where division overflows is
1790 // - type is signed
1791 // - LHS is type.min
1792 // - RHS is -1
1793 // the result is then -(type.min), which wraps back to type.min
1794 smtutil::Expression maxLeft = _left == smt::minValue(*intType);
1795 smtutil::Expression minusOneRight = _right == numeric_limits<size_t >::max();
1796 smtutil::Expression wrap = smtutil::Expression::ite(maxLeft && minusOneRight, smt::minValue(*intType), valueUnbounded);
1797 return {wrap, valueUnbounded};
1798 }
1799
1800 auto symbMin = smt::minValue(*intType);
1801 auto symbMax = smt::maxValue(*intType);
1802
1803 smtutil::Expression intValueRange = (0 - symbMin) + symbMax + 1;
1804 string suffix = to_string(_operation.id()) + "_" + to_string(m_context.newUniqueId());
1805 smt::SymbolicIntVariable k(intType, intType, "k_" + suffix, m_context);
1806 smt::SymbolicIntVariable m(intType, intType, "m_" + suffix, m_context);
1807
1808 // To wrap around valueUnbounded in case of overflow or underflow, we replace it with a k, given:
1809 // 1. k + m * intValueRange = valueUnbounded
1810 // 2. k is in range of the desired integer type
1811 auto wrap = k.currentValue();
1812 m_context.addAssertion(valueUnbounded == (k.currentValue() + intValueRange * m.currentValue()));
1813 m_context.addAssertion(k.currentValue() >= symbMin);
1814 m_context.addAssertion(k.currentValue() <= symbMax);
1815
1816 // TODO this could be refined:
1817 // for unsigned types it's enough to check only the upper bound.
1818 auto value = smtutil::Expression::ite(
1819 valueUnbounded > symbMax,
1820 wrap,
1821 smtutil::Expression::ite(
1822 valueUnbounded < symbMin,
1823 wrap,
1824 valueUnbounded
1825 )
1826 );
1827
1828 return {value, valueUnbounded};
1829 }
1830
bitwiseOperation(Token _op,smtutil::Expression const & _left,smtutil::Expression const & _right,Type const * _commonType)1831 smtutil::Expression SMTEncoder::bitwiseOperation(
1832 Token _op,
1833 smtutil::Expression const& _left,
1834 smtutil::Expression const& _right,
1835 Type const* _commonType
1836 )
1837 {
1838 static set<Token> validOperators{
1839 Token::BitAnd,
1840 Token::BitOr,
1841 Token::BitXor,
1842 Token::SHL,
1843 Token::SHR,
1844 Token::SAR
1845 };
1846 solAssert(validOperators.count(_op), "");
1847 solAssert(_commonType, "");
1848
1849 auto [bvSize, isSigned] = smt::typeBvSizeAndSignedness(_commonType);
1850
1851 auto bvLeft = smtutil::Expression::int2bv(_left, bvSize);
1852 auto bvRight = smtutil::Expression::int2bv(_right, bvSize);
1853
1854 optional<smtutil::Expression> result;
1855 switch (_op)
1856 {
1857 case Token::BitAnd:
1858 result = bvLeft & bvRight;
1859 break;
1860 case Token::BitOr:
1861 result = bvLeft | bvRight;
1862 break;
1863 case Token::BitXor:
1864 result = bvLeft ^ bvRight;
1865 break;
1866 case Token::SHL:
1867 result = bvLeft << bvRight;
1868 break;
1869 case Token::SHR:
1870 result = bvLeft >> bvRight;
1871 break;
1872 case Token::SAR:
1873 result = isSigned ?
1874 smtutil::Expression::ashr(bvLeft, bvRight) :
1875 bvLeft >> bvRight;
1876 break;
1877 default:
1878 solAssert(false, "");
1879 }
1880
1881 solAssert(result.has_value(), "");
1882 return smtutil::Expression::bv2int(*result, isSigned);
1883 }
1884
compareOperation(BinaryOperation const & _op)1885 void SMTEncoder::compareOperation(BinaryOperation const& _op)
1886 {
1887 auto commonType = _op.annotation().commonType;
1888 solAssert(commonType, "");
1889
1890 if (isSupportedType(*commonType))
1891 {
1892 smtutil::Expression left(expr(_op.leftExpression(), commonType));
1893 smtutil::Expression right(expr(_op.rightExpression(), commonType));
1894 Token op = _op.getOperator();
1895 shared_ptr<smtutil::Expression> value;
1896 if (smt::isNumber(*commonType))
1897 {
1898 value = make_shared<smtutil::Expression>(
1899 op == Token::Equal ? (left == right) :
1900 op == Token::NotEqual ? (left != right) :
1901 op == Token::LessThan ? (left < right) :
1902 op == Token::LessThanOrEqual ? (left <= right) :
1903 op == Token::GreaterThan ? (left > right) :
1904 /*op == Token::GreaterThanOrEqual*/ (left >= right)
1905 );
1906 }
1907 else // Bool
1908 {
1909 solUnimplementedAssert(smt::isBool(*commonType), "Operation not yet supported");
1910 value = make_shared<smtutil::Expression>(
1911 op == Token::Equal ? (left == right) :
1912 /*op == Token::NotEqual*/ (left != right)
1913 );
1914 }
1915 // TODO: check that other values for op are not possible.
1916 defineExpr(_op, *value);
1917 }
1918 else
1919 m_errorReporter.warning(
1920 7229_error,
1921 _op.location(),
1922 "Assertion checker does not yet implement the type " + _op.annotation().commonType->toString() + " for comparisons"
1923 );
1924 }
1925
booleanOperation(BinaryOperation const & _op)1926 void SMTEncoder::booleanOperation(BinaryOperation const& _op)
1927 {
1928 solAssert(_op.getOperator() == Token::And || _op.getOperator() == Token::Or, "");
1929 solAssert(_op.annotation().commonType, "");
1930 solAssert(_op.annotation().commonType->category() == Type::Category::Bool, "");
1931 // @TODO check that both of them are not constant
1932 _op.leftExpression().accept(*this);
1933 if (_op.getOperator() == Token::And)
1934 {
1935 auto indicesAfterSecond = visitBranch(&_op.rightExpression(), expr(_op.leftExpression())).first;
1936 mergeVariables(!expr(_op.leftExpression()), copyVariableIndices(), indicesAfterSecond);
1937 defineExpr(_op, expr(_op.leftExpression()) && expr(_op.rightExpression()));
1938 }
1939 else
1940 {
1941 auto indicesAfterSecond = visitBranch(&_op.rightExpression(), !expr(_op.leftExpression())).first;
1942 mergeVariables(expr(_op.leftExpression()), copyVariableIndices(), indicesAfterSecond);
1943 defineExpr(_op, expr(_op.leftExpression()) || expr(_op.rightExpression()));
1944 }
1945 }
1946
bitwiseOperation(BinaryOperation const & _op)1947 void SMTEncoder::bitwiseOperation(BinaryOperation const& _op)
1948 {
1949 auto op = _op.getOperator();
1950 solAssert(TokenTraits::isBitOp(op) || TokenTraits::isShiftOp(op), "");
1951 auto commonType = _op.annotation().commonType;
1952 solAssert(commonType, "");
1953
1954 defineExpr(_op, bitwiseOperation(
1955 _op.getOperator(),
1956 expr(_op.leftExpression(), commonType),
1957 expr(_op.rightExpression(), commonType),
1958 commonType
1959 ));
1960 }
1961
bitwiseNotOperation(UnaryOperation const & _op)1962 void SMTEncoder::bitwiseNotOperation(UnaryOperation const& _op)
1963 {
1964 solAssert(_op.getOperator() == Token::BitNot, "");
1965
1966 auto [bvSize, isSigned] = smt::typeBvSizeAndSignedness(_op.annotation().type);
1967
1968 auto bvOperand = smtutil::Expression::int2bv(expr(_op.subExpression(), _op.annotation().type), bvSize);
1969 defineExpr(_op, smtutil::Expression::bv2int(~bvOperand, isSigned));
1970 }
1971
divModWithSlacks(smtutil::Expression _left,smtutil::Expression _right,IntegerType const & _type)1972 pair<smtutil::Expression, smtutil::Expression> SMTEncoder::divModWithSlacks(
1973 smtutil::Expression _left,
1974 smtutil::Expression _right,
1975 IntegerType const& _type
1976 )
1977 {
1978 if (m_settings.divModNoSlacks)
1979 return {_left / _right, _left % _right};
1980
1981 IntegerType const* intType = &_type;
1982 string suffix = "div_mod_" + to_string(m_context.newUniqueId());
1983 smt::SymbolicIntVariable dSymb(intType, intType, "d_" + suffix, m_context);
1984 smt::SymbolicIntVariable rSymb(intType, intType, "r_" + suffix, m_context);
1985 auto d = dSymb.currentValue();
1986 auto r = rSymb.currentValue();
1987
1988 // x / y = d and x % y = r iff d * y + r = x and
1989 // either x >= 0 and 0 <= r < abs(y) (or just 0 <= r < y for unsigned)
1990 // or x < 0 and -abs(y) < r <= 0
1991 m_context.addAssertion(((d * _right) + r) == _left);
1992 if (_type.isSigned())
1993 m_context.addAssertion(
1994 (_left >= 0 && 0 <= r && (_right == 0 || r < smtutil::abs(_right))) ||
1995 (_left < 0 && ((_right == 0 || 0 - smtutil::abs(_right) < r) && r <= 0))
1996 );
1997 else // unsigned version
1998 m_context.addAssertion(0 <= r && (_right == 0 || r < _right));
1999
2000 auto divResult = smtutil::Expression::ite(_right == 0, 0, d);
2001 auto modResult = smtutil::Expression::ite(_right == 0, 0, r);
2002 return {divResult, modResult};
2003 }
2004
assignment(Expression const & _left,smtutil::Expression const & _right)2005 void SMTEncoder::assignment(Expression const& _left, smtutil::Expression const& _right)
2006 {
2007 assignment(_left, _right, _left.annotation().type);
2008 }
2009
assignment(Expression const & _left,smtutil::Expression const & _right,Type const * _type)2010 void SMTEncoder::assignment(
2011 Expression const& _left,
2012 smtutil::Expression const& _right,
2013 Type const* _type
2014 )
2015 {
2016 solAssert(
2017 _left.annotation().type->category() != Type::Category::Tuple,
2018 "Tuple assignments should be handled by tupleAssignment."
2019 );
2020
2021 Expression const* left = cleanExpression(_left);
2022
2023 if (!isSupportedType(*_type))
2024 {
2025 // Give it a new index anyway to keep the SSA scheme sound.
2026 if (auto varDecl = identifierToVariable(*left))
2027 m_context.newValue(*varDecl);
2028 }
2029 else if (auto varDecl = identifierToVariable(*left))
2030 {
2031 if (varDecl->hasReferenceOrMappingType())
2032 resetReferences(*varDecl);
2033 assignment(*varDecl, _right);
2034 }
2035 else if (
2036 dynamic_cast<IndexAccess const*>(left) ||
2037 dynamic_cast<MemberAccess const*>(left)
2038 )
2039 indexOrMemberAssignment(*left, _right);
2040 else if (auto const* funCall = dynamic_cast<FunctionCall const*>(left))
2041 {
2042 if (auto funType = dynamic_cast<FunctionType const*>(funCall->expression().annotation().type))
2043 {
2044 if (funType->kind() == FunctionType::Kind::ArrayPush)
2045 {
2046 auto memberAccess = dynamic_cast<MemberAccess const*>(&funCall->expression());
2047 solAssert(memberAccess, "");
2048 auto symbArray = dynamic_pointer_cast<smt::SymbolicArrayVariable>(m_context.expression(memberAccess->expression()));
2049 solAssert(symbArray, "");
2050
2051 auto oldLength = symbArray->length();
2052 auto store = smtutil::Expression::store(
2053 symbArray->elements(),
2054 symbArray->length() - 1,
2055 _right
2056 );
2057 symbArray->increaseIndex();
2058 m_context.addAssertion(symbArray->elements() == store);
2059 m_context.addAssertion(symbArray->length() == oldLength);
2060 assignment(memberAccess->expression(), symbArray->currentValue());
2061 }
2062 else if (funType->kind() == FunctionType::Kind::Internal)
2063 {
2064 for (auto type: replaceUserTypes(funType->returnParameterTypes()))
2065 if (type->category() == Type::Category::Mapping || dynamic_cast<ReferenceType const*>(type))
2066 resetReferences(type);
2067 }
2068 }
2069 }
2070 else
2071 solAssert(false, "");
2072 }
2073
tupleAssignment(Expression const & _left,Expression const & _right)2074 void SMTEncoder::tupleAssignment(Expression const& _left, Expression const& _right)
2075 {
2076 auto lTuple = dynamic_cast<TupleExpression const*>(innermostTuple(_left));
2077 solAssert(lTuple, "");
2078 Expression const* right = innermostTuple(_right);
2079
2080 auto const& lComponents = lTuple->components();
2081
2082 // If both sides are tuple expressions, we individually and potentially
2083 // recursively assign each pair of components.
2084 // This is because of potential type conversion.
2085 if (auto rTuple = dynamic_cast<TupleExpression const*>(right))
2086 {
2087 auto const& rComponents = rTuple->components();
2088 solAssert(lComponents.size() == rComponents.size(), "");
2089 for (unsigned i = 0; i < lComponents.size(); ++i)
2090 {
2091 if (!lComponents.at(i) || !rComponents.at(i))
2092 continue;
2093 auto const& lExpr = *lComponents.at(i);
2094 auto const& rExpr = *rComponents.at(i);
2095 if (lExpr.annotation().type->category() == Type::Category::Tuple)
2096 tupleAssignment(lExpr, rExpr);
2097 else
2098 {
2099 auto type = lExpr.annotation().type;
2100 assignment(lExpr, expr(rExpr, type), type);
2101 }
2102 }
2103 }
2104 else
2105 {
2106 auto rType = dynamic_cast<TupleType const*>(right->annotation().type);
2107 solAssert(rType, "");
2108
2109 auto const& rComponents = rType->components();
2110 solAssert(lComponents.size() == rComponents.size(), "");
2111
2112 auto symbRight = expr(*right);
2113 solAssert(symbRight.sort->kind == smtutil::Kind::Tuple, "");
2114
2115 for (unsigned i = 0; i < lComponents.size(); ++i)
2116 if (auto component = lComponents.at(i); component && rComponents.at(i))
2117 assignment(*component, smtutil::Expression::tuple_get(symbRight, i), component->annotation().type);
2118 }
2119 }
2120
compoundAssignment(Assignment const & _assignment)2121 smtutil::Expression SMTEncoder::compoundAssignment(Assignment const& _assignment)
2122 {
2123 static map<Token, Token> const compoundToArithmetic{
2124 {Token::AssignAdd, Token::Add},
2125 {Token::AssignSub, Token::Sub},
2126 {Token::AssignMul, Token::Mul},
2127 {Token::AssignDiv, Token::Div},
2128 {Token::AssignMod, Token::Mod}
2129 };
2130 static map<Token, Token> const compoundToBitwise{
2131 {Token::AssignBitAnd, Token::BitAnd},
2132 {Token::AssignBitOr, Token::BitOr},
2133 {Token::AssignBitXor, Token::BitXor},
2134 {Token::AssignShl, Token::SHL},
2135 {Token::AssignShr, Token::SHR},
2136 {Token::AssignSar, Token::SAR}
2137 };
2138 Token op = _assignment.assignmentOperator();
2139 solAssert(compoundToArithmetic.count(op) || compoundToBitwise.count(op), "");
2140
2141 auto decl = identifierToVariable(_assignment.leftHandSide());
2142
2143 if (compoundToBitwise.count(op))
2144 return bitwiseOperation(
2145 compoundToBitwise.at(op),
2146 decl ? currentValue(*decl) : expr(_assignment.leftHandSide(), _assignment.annotation().type),
2147 expr(_assignment.rightHandSide(), _assignment.annotation().type),
2148 _assignment.annotation().type
2149 );
2150
2151 auto values = arithmeticOperation(
2152 compoundToArithmetic.at(op),
2153 decl ? currentValue(*decl) : expr(_assignment.leftHandSide(), _assignment.annotation().type),
2154 expr(_assignment.rightHandSide(), _assignment.annotation().type),
2155 _assignment.annotation().type,
2156 _assignment
2157 );
2158 return values.first;
2159 }
2160
expressionToTupleAssignment(vector<shared_ptr<VariableDeclaration>> const & _variables,Expression const & _rhs)2161 void SMTEncoder::expressionToTupleAssignment(vector<shared_ptr<VariableDeclaration>> const& _variables, Expression const& _rhs)
2162 {
2163 auto symbolicVar = m_context.expression(_rhs);
2164 if (_variables.size() > 1)
2165 {
2166 auto symbTuple = dynamic_pointer_cast<smt::SymbolicTupleVariable>(symbolicVar);
2167 solAssert(symbTuple, "");
2168 auto const& symbComponents = symbTuple->components();
2169 solAssert(symbComponents.size() == _variables.size(), "");
2170 auto tupleType = dynamic_cast<TupleType const*>(_rhs.annotation().type);
2171 solAssert(tupleType, "");
2172 auto const& typeComponents = tupleType->components();
2173 solAssert(typeComponents.size() == symbComponents.size(), "");
2174 for (unsigned i = 0; i < symbComponents.size(); ++i)
2175 {
2176 auto param = _variables.at(i);
2177 if (param)
2178 {
2179 solAssert(m_context.knownVariable(*param), "");
2180 assignment(*param, symbTuple->component(i, typeComponents[i], param->type()));
2181 }
2182 }
2183 }
2184 else if (_variables.size() == 1)
2185 {
2186 auto const& var = *_variables.front();
2187 solAssert(m_context.knownVariable(var), "");
2188 assignment(var, _rhs);
2189 }
2190 }
2191
assignment(VariableDeclaration const & _variable,Expression const & _value)2192 void SMTEncoder::assignment(VariableDeclaration const& _variable, Expression const& _value)
2193 {
2194 // In general, at this point, the SMT sorts of _variable and _value are the same,
2195 // even if there is implicit conversion.
2196 // This is a special case where the SMT sorts are different.
2197 // For now we are unaware of other cases where this happens, but if they do appear
2198 // we should extract this into an `implicitConversion` function.
2199 assignment(_variable, expr(_value, _variable.type()));
2200 }
2201
assignment(VariableDeclaration const & _variable,smtutil::Expression const & _value)2202 void SMTEncoder::assignment(VariableDeclaration const& _variable, smtutil::Expression const& _value)
2203 {
2204 Type const* type = _variable.type();
2205 if (type->category() == Type::Category::Mapping)
2206 arrayAssignment();
2207 assignment(*m_context.variable(_variable), _value);
2208 }
2209
assignment(smt::SymbolicVariable & _symVar,smtutil::Expression const & _value)2210 void SMTEncoder::assignment(smt::SymbolicVariable& _symVar, smtutil::Expression const& _value)
2211 {
2212 m_context.addAssertion(_symVar.increaseIndex() == _value);
2213 }
2214
visitBranch(ASTNode const * _statement,smtutil::Expression _condition)2215 pair<SMTEncoder::VariableIndices, smtutil::Expression> SMTEncoder::visitBranch(
2216 ASTNode const* _statement,
2217 smtutil::Expression _condition
2218 )
2219 {
2220 return visitBranch(_statement, &_condition);
2221 }
2222
visitBranch(ASTNode const * _statement,smtutil::Expression const * _condition)2223 pair<SMTEncoder::VariableIndices, smtutil::Expression> SMTEncoder::visitBranch(
2224 ASTNode const* _statement,
2225 smtutil::Expression const* _condition
2226 )
2227 {
2228 auto indicesBeforeBranch = copyVariableIndices();
2229 if (_condition)
2230 pushPathCondition(*_condition);
2231 _statement->accept(*this);
2232 auto pathConditionOnExit = currentPathConditions();
2233 if (_condition)
2234 popPathCondition();
2235 auto indicesAfterBranch = copyVariableIndices();
2236 resetVariableIndices(indicesBeforeBranch);
2237 return {indicesAfterBranch, pathConditionOnExit};
2238 }
2239
initializeFunctionCallParameters(CallableDeclaration const & _function,vector<smtutil::Expression> const & _callArgs)2240 void SMTEncoder::initializeFunctionCallParameters(CallableDeclaration const& _function, vector<smtutil::Expression> const& _callArgs)
2241 {
2242 auto const& funParams = _function.parameters();
2243 solAssert(funParams.size() == _callArgs.size(), "");
2244 for (unsigned i = 0; i < funParams.size(); ++i)
2245 if (createVariable(*funParams[i]))
2246 {
2247 m_context.addAssertion(_callArgs[i] == m_context.newValue(*funParams[i]));
2248 if (funParams[i]->annotation().type->category() == Type::Category::Mapping)
2249 m_arrayAssignmentHappened = true;
2250 }
2251
2252 vector<VariableDeclaration const*> localVars;
2253 if (auto const* fun = dynamic_cast<FunctionDefinition const*>(&_function))
2254 localVars = localVariablesIncludingModifiers(*fun, m_currentContract);
2255 else
2256 localVars = _function.localVariables();
2257 for (auto const& variable: localVars)
2258 if (createVariable(*variable))
2259 {
2260 m_context.newValue(*variable);
2261 m_context.setZeroValue(*variable);
2262 }
2263
2264 if (_function.returnParameterList())
2265 for (auto const& retParam: _function.returnParameters())
2266 if (createVariable(*retParam))
2267 {
2268 m_context.newValue(*retParam);
2269 m_context.setZeroValue(*retParam);
2270 }
2271 }
2272
createStateVariables(ContractDefinition const & _contract)2273 void SMTEncoder::createStateVariables(ContractDefinition const& _contract)
2274 {
2275 for (auto var: stateVariablesIncludingInheritedAndPrivate(_contract))
2276 createVariable(*var);
2277 }
2278
initializeStateVariables(ContractDefinition const & _contract)2279 void SMTEncoder::initializeStateVariables(ContractDefinition const& _contract)
2280 {
2281 for (auto var: _contract.stateVariables())
2282 {
2283 solAssert(m_context.knownVariable(*var), "");
2284 m_context.setZeroValue(*var);
2285 }
2286
2287 for (auto var: _contract.stateVariables())
2288 if (var->value())
2289 {
2290 var->value()->accept(*this);
2291 assignment(*var, *var->value());
2292 }
2293 }
2294
createLocalVariables(FunctionDefinition const & _function)2295 void SMTEncoder::createLocalVariables(FunctionDefinition const& _function)
2296 {
2297 for (auto const& variable: localVariablesIncludingModifiers(_function, m_currentContract))
2298 createVariable(*variable);
2299
2300 for (auto const& param: _function.parameters())
2301 createVariable(*param);
2302
2303 if (_function.returnParameterList())
2304 for (auto const& retParam: _function.returnParameters())
2305 createVariable(*retParam);
2306 }
2307
initializeLocalVariables(FunctionDefinition const & _function)2308 void SMTEncoder::initializeLocalVariables(FunctionDefinition const& _function)
2309 {
2310 for (auto const& variable: localVariablesIncludingModifiers(_function, m_currentContract))
2311 {
2312 solAssert(m_context.knownVariable(*variable), "");
2313 m_context.setZeroValue(*variable);
2314 }
2315
2316 for (auto const& param: _function.parameters())
2317 {
2318 solAssert(m_context.knownVariable(*param), "");
2319 m_context.setUnknownValue(*param);
2320 }
2321
2322 if (_function.returnParameterList())
2323 for (auto const& retParam: _function.returnParameters())
2324 {
2325 solAssert(m_context.knownVariable(*retParam), "");
2326 m_context.setZeroValue(*retParam);
2327 }
2328 }
2329
resetStateVariables()2330 void SMTEncoder::resetStateVariables()
2331 {
2332 m_context.resetVariables([&](VariableDeclaration const& _variable) { return _variable.isStateVariable(); });
2333 }
2334
resetMemoryVariables()2335 void SMTEncoder::resetMemoryVariables()
2336 {
2337 m_context.resetVariables([&](VariableDeclaration const& _variable) {
2338 return _variable.referenceLocation() == VariableDeclaration::Location::Memory;
2339 });
2340 }
2341
resetStorageVariables()2342 void SMTEncoder::resetStorageVariables()
2343 {
2344 m_context.resetVariables([&](VariableDeclaration const& _variable) {
2345 return _variable.referenceLocation() == VariableDeclaration::Location::Storage || _variable.isStateVariable();
2346 });
2347 }
2348
resetBalances()2349 void SMTEncoder::resetBalances()
2350 {
2351 state().newBalances();
2352 }
2353
resetReferences(VariableDeclaration const & _varDecl)2354 void SMTEncoder::resetReferences(VariableDeclaration const& _varDecl)
2355 {
2356 m_context.resetVariables([&](VariableDeclaration const& _var) {
2357 if (_var == _varDecl)
2358 return false;
2359
2360 // If both are state variables no need to clear knowledge.
2361 if (_var.isStateVariable() && _varDecl.isStateVariable())
2362 return false;
2363
2364 return sameTypeOrSubtype(_var.type(), _varDecl.type());
2365 });
2366 }
2367
resetReferences(Type const * _type)2368 void SMTEncoder::resetReferences(Type const* _type)
2369 {
2370 m_context.resetVariables([&](VariableDeclaration const& _var) {
2371 return sameTypeOrSubtype(_var.type(), _type);
2372 });
2373 }
2374
sameTypeOrSubtype(Type const * _a,Type const * _b)2375 bool SMTEncoder::sameTypeOrSubtype(Type const* _a, Type const* _b)
2376 {
2377 bool foundSame = false;
2378
2379 solidity::util::BreadthFirstSearch<Type const*> bfs{{_a}};
2380 bfs.run([&](auto _type, auto&& _addChild) {
2381 if (*typeWithoutPointer(_b) == *typeWithoutPointer(_type))
2382 {
2383 foundSame = true;
2384 bfs.abort();
2385 }
2386 if (auto const* mapType = dynamic_cast<MappingType const*>(_type))
2387 _addChild(mapType->valueType());
2388 else if (auto const* arrayType = dynamic_cast<ArrayType const*>(_type))
2389 _addChild(arrayType->baseType());
2390 else if (auto const* structType = dynamic_cast<StructType const*>(_type))
2391 for (auto const& member: structType->nativeMembers(nullptr))
2392 _addChild(member.type);
2393 });
2394
2395 return foundSame;
2396 }
2397
isSupportedType(Type const & _type) const2398 bool SMTEncoder::isSupportedType(Type const& _type) const
2399 {
2400 return smt::isSupportedType(*underlyingType(&_type));
2401 }
2402
typeWithoutPointer(Type const * _type)2403 Type const* SMTEncoder::typeWithoutPointer(Type const* _type)
2404 {
2405 if (auto refType = dynamic_cast<ReferenceType const*>(_type))
2406 return TypeProvider::withLocationIfReference(refType->location(), _type);
2407 return _type;
2408 }
2409
mergeVariables(smtutil::Expression const & _condition,VariableIndices const & _indicesEndTrue,VariableIndices const & _indicesEndFalse)2410 void SMTEncoder::mergeVariables(smtutil::Expression const& _condition, VariableIndices const& _indicesEndTrue, VariableIndices const& _indicesEndFalse)
2411 {
2412 for (auto const& entry: _indicesEndTrue)
2413 {
2414 VariableDeclaration const* var = entry.first;
2415 auto trueIndex = entry.second;
2416 if (_indicesEndFalse.count(var) && _indicesEndFalse.at(var) != trueIndex)
2417 {
2418 m_context.addAssertion(m_context.newValue(*var) == smtutil::Expression::ite(
2419 _condition,
2420 valueAtIndex(*var, trueIndex),
2421 valueAtIndex(*var, _indicesEndFalse.at(var)))
2422 );
2423 }
2424 }
2425 }
2426
currentValue(VariableDeclaration const & _decl) const2427 smtutil::Expression SMTEncoder::currentValue(VariableDeclaration const& _decl) const
2428 {
2429 solAssert(m_context.knownVariable(_decl), "");
2430 return m_context.variable(_decl)->currentValue();
2431 }
2432
valueAtIndex(VariableDeclaration const & _decl,unsigned _index) const2433 smtutil::Expression SMTEncoder::valueAtIndex(VariableDeclaration const& _decl, unsigned _index) const
2434 {
2435 solAssert(m_context.knownVariable(_decl), "");
2436 return m_context.variable(_decl)->valueAtIndex(_index);
2437 }
2438
createVariable(VariableDeclaration const & _varDecl)2439 bool SMTEncoder::createVariable(VariableDeclaration const& _varDecl)
2440 {
2441 if (m_context.knownVariable(_varDecl))
2442 return true;
2443 bool abstract = m_context.createVariable(_varDecl);
2444 if (abstract)
2445 {
2446 m_errorReporter.warning(
2447 8115_error,
2448 _varDecl.location(),
2449 "Assertion checker does not yet support the type of this variable."
2450 );
2451 return false;
2452 }
2453 return true;
2454 }
2455
expr(Expression const & _e,Type const * _targetType)2456 smtutil::Expression SMTEncoder::expr(Expression const& _e, Type const* _targetType)
2457 {
2458 if (!m_context.knownExpression(_e))
2459 {
2460 m_errorReporter.warning(6031_error, _e.location(), "Internal error: Expression undefined for SMT solver." );
2461 createExpr(_e);
2462 }
2463
2464 return m_context.expression(_e)->currentValue(underlyingType(_targetType));
2465 }
2466
createExpr(Expression const & _e)2467 void SMTEncoder::createExpr(Expression const& _e)
2468 {
2469 bool abstract = m_context.createExpression(_e);
2470 if (abstract)
2471 m_errorReporter.warning(
2472 8364_error,
2473 _e.location(),
2474 "Assertion checker does not yet implement type " + _e.annotation().type->toString()
2475 );
2476 }
2477
defineExpr(Expression const & _e,smtutil::Expression _value)2478 void SMTEncoder::defineExpr(Expression const& _e, smtutil::Expression _value)
2479 {
2480 auto type = _e.annotation().type;
2481 createExpr(_e);
2482 solAssert(_value.sort->kind != smtutil::Kind::Function, "Equality operator applied to type that is not fully supported");
2483 if (!smt::isInaccessibleDynamic(*type))
2484 m_context.addAssertion(expr(_e) == _value);
2485
2486 if (m_checked && smt::isNumber(*type))
2487 m_context.addAssertion(smtutil::Expression::implies(
2488 currentPathConditions(),
2489 smt::symbolicUnknownConstraints(expr(_e), type)
2490 ));
2491 }
2492
defineExpr(Expression const & _e,vector<optional<smtutil::Expression>> const & _values)2493 void SMTEncoder::defineExpr(Expression const& _e, vector<optional<smtutil::Expression>> const& _values)
2494 {
2495 if (_values.size() == 1 && _values.front())
2496 {
2497 defineExpr(_e, *_values.front());
2498 return;
2499 }
2500 auto const& symbTuple = dynamic_pointer_cast<smt::SymbolicTupleVariable>(m_context.expression(_e));
2501 solAssert(symbTuple, "");
2502 symbTuple->increaseIndex();
2503 auto const& symbComponents = symbTuple->components();
2504 solAssert(symbComponents.size() == _values.size(), "");
2505 auto tupleType = dynamic_cast<TupleType const*>(_e.annotation().type);
2506 solAssert(tupleType, "");
2507 solAssert(tupleType->components().size() == symbComponents.size(), "");
2508 for (unsigned i = 0; i < symbComponents.size(); ++i)
2509 if (_values[i] && !smt::isInaccessibleDynamic(*tupleType->components()[i]))
2510 m_context.addAssertion(symbTuple->component(i) == *_values[i]);
2511 }
2512
popPathCondition()2513 void SMTEncoder::popPathCondition()
2514 {
2515 solAssert(m_pathConditions.size() > 0, "Cannot pop path condition, empty.");
2516 m_pathConditions.pop_back();
2517 }
2518
pushPathCondition(smtutil::Expression const & _e)2519 void SMTEncoder::pushPathCondition(smtutil::Expression const& _e)
2520 {
2521 m_pathConditions.push_back(currentPathConditions() && _e);
2522 }
2523
setPathCondition(smtutil::Expression const & _e)2524 void SMTEncoder::setPathCondition(smtutil::Expression const& _e)
2525 {
2526 if (m_pathConditions.empty())
2527 m_pathConditions.push_back(_e);
2528 else
2529 m_pathConditions.back() = _e;
2530 }
2531
currentPathConditions()2532 smtutil::Expression SMTEncoder::currentPathConditions()
2533 {
2534 if (m_pathConditions.empty())
2535 return smtutil::Expression(true);
2536 return m_pathConditions.back();
2537 }
2538
callStackMessage(vector<CallStackEntry> const & _callStack)2539 SecondarySourceLocation SMTEncoder::callStackMessage(vector<CallStackEntry> const& _callStack)
2540 {
2541 SecondarySourceLocation callStackLocation;
2542 solAssert(!_callStack.empty(), "");
2543 callStackLocation.append("Callstack:", SourceLocation());
2544 for (auto const& call: _callStack | ranges::views::reverse)
2545 if (call.second)
2546 callStackLocation.append("", call.second->location());
2547 return callStackLocation;
2548 }
2549
popCallStack()2550 pair<CallableDeclaration const*, ASTNode const*> SMTEncoder::popCallStack()
2551 {
2552 solAssert(!m_callStack.empty(), "");
2553 auto lastCalled = m_callStack.back();
2554 m_callStack.pop_back();
2555 return lastCalled;
2556 }
2557
pushCallStack(CallStackEntry _entry)2558 void SMTEncoder::pushCallStack(CallStackEntry _entry)
2559 {
2560 m_callStack.push_back(_entry);
2561 }
2562
addPathImpliedExpression(smtutil::Expression const & _e)2563 void SMTEncoder::addPathImpliedExpression(smtutil::Expression const& _e)
2564 {
2565 m_context.addAssertion(smtutil::Expression::implies(currentPathConditions(), _e));
2566 }
2567
isRootFunction()2568 bool SMTEncoder::isRootFunction()
2569 {
2570 return m_callStack.size() == 1;
2571 }
2572
visitedFunction(FunctionDefinition const * _funDef)2573 bool SMTEncoder::visitedFunction(FunctionDefinition const* _funDef)
2574 {
2575 for (auto const& call: m_callStack)
2576 if (call.first == _funDef)
2577 return true;
2578 return false;
2579 }
2580
currentScopeContract()2581 ContractDefinition const* SMTEncoder::currentScopeContract()
2582 {
2583 for (auto&& f: m_callStack | ranges::views::reverse | ranges::views::keys)
2584 if (auto fun = dynamic_cast<FunctionDefinition const*>(f))
2585 return fun->annotation().contract;
2586 return nullptr;
2587 }
2588
copyVariableIndices()2589 SMTEncoder::VariableIndices SMTEncoder::copyVariableIndices()
2590 {
2591 VariableIndices indices;
2592 for (auto const& var: m_context.variables())
2593 indices.emplace(var.first, var.second->index());
2594 return indices;
2595 }
2596
resetVariableIndices(VariableIndices const & _indices)2597 void SMTEncoder::resetVariableIndices(VariableIndices const& _indices)
2598 {
2599 for (auto const& var: _indices)
2600 m_context.variable(*var.first)->setIndex(var.second);
2601 }
2602
clearIndices(ContractDefinition const * _contract,FunctionDefinition const * _function)2603 void SMTEncoder::clearIndices(ContractDefinition const* _contract, FunctionDefinition const* _function)
2604 {
2605 solAssert(_contract, "");
2606 for (auto var: stateVariablesIncludingInheritedAndPrivate(*_contract))
2607 m_context.variable(*var)->resetIndex();
2608 if (_function)
2609 {
2610 for (auto const& var: _function->parameters() + _function->returnParameters())
2611 m_context.variable(*var)->resetIndex();
2612 for (auto const& var: localVariablesIncludingModifiers(*_function, _contract))
2613 m_context.variable(*var)->resetIndex();
2614 }
2615 state().reset();
2616 }
2617
leftmostBase(IndexAccess const & _indexAccess)2618 Expression const* SMTEncoder::leftmostBase(IndexAccess const& _indexAccess)
2619 {
2620 Expression const* base = &_indexAccess.baseExpression();
2621 while (auto access = dynamic_cast<IndexAccess const*>(base))
2622 base = &access->baseExpression();
2623 return base;
2624 }
2625
keyType(Type const * _type)2626 Type const* SMTEncoder::keyType(Type const* _type)
2627 {
2628 if (auto const* mappingType = dynamic_cast<MappingType const*>(_type))
2629 return mappingType->keyType();
2630 if (
2631 dynamic_cast<ArrayType const*>(_type) ||
2632 dynamic_cast<ArraySliceType const*>(_type)
2633 )
2634 return TypeProvider::uint256();
2635 else
2636 solAssert(false, "");
2637 }
2638
innermostTuple(Expression const & _expr)2639 Expression const* SMTEncoder::innermostTuple(Expression const& _expr)
2640 {
2641 auto const* tuple = dynamic_cast<TupleExpression const*>(&_expr);
2642 if (!tuple || tuple->isInlineArray())
2643 return &_expr;
2644
2645 Expression const* expr = tuple;
2646 while (tuple && !tuple->isInlineArray() && tuple->components().size() == 1)
2647 {
2648 expr = tuple->components().front().get();
2649 tuple = dynamic_cast<TupleExpression const*>(expr);
2650 }
2651 solAssert(expr, "");
2652 return expr;
2653 }
2654
underlyingType(Type const * _type)2655 Type const* SMTEncoder::underlyingType(Type const* _type)
2656 {
2657 if (auto userType = dynamic_cast<UserDefinedValueType const*>(_type))
2658 _type = &userType->underlyingType();
2659 return _type;
2660 }
2661
replaceUserTypes(TypePointers const & _types)2662 TypePointers SMTEncoder::replaceUserTypes(TypePointers const& _types)
2663 {
2664 return applyMap(_types, [](auto _type) {
2665 if (auto userType = dynamic_cast<UserDefinedValueType const*>(_type))
2666 return &userType->underlyingType();
2667 return _type;
2668 });
2669 }
2670
functionCallExpression(FunctionCall const & _funCall)2671 pair<Expression const*, FunctionCallOptions const*> SMTEncoder::functionCallExpression(FunctionCall const& _funCall)
2672 {
2673 Expression const* callExpr = &_funCall.expression();
2674 auto const* callOptions = dynamic_cast<FunctionCallOptions const*>(callExpr);
2675 if (callOptions)
2676 callExpr = &callOptions->expression();
2677
2678 return {callExpr, callOptions};
2679 }
2680
cleanExpression(Expression const & _expr)2681 Expression const* SMTEncoder::cleanExpression(Expression const& _expr)
2682 {
2683 auto const* expr = &_expr;
2684 if (auto const* tuple = dynamic_cast<TupleExpression const*>(expr))
2685 return cleanExpression(*innermostTuple(*tuple));
2686 if (auto const* functionCall = dynamic_cast<FunctionCall const*>(expr))
2687 if (*functionCall->annotation().kind == FunctionCallKind::TypeConversion)
2688 {
2689 auto typeType = dynamic_cast<TypeType const*>(functionCall->expression().annotation().type);
2690 solAssert(typeType, "");
2691 if (auto const* arrayType = dynamic_cast<ArrayType const*>(typeType->actualType()))
2692 if (arrayType->isByteArray())
2693 {
2694 // this is a cast to `bytes`
2695 solAssert(functionCall->arguments().size() == 1, "");
2696 Expression const& arg = *functionCall->arguments()[0];
2697 if (
2698 auto const* argArrayType = dynamic_cast<ArrayType const*>(arg.annotation().type);
2699 argArrayType && argArrayType->isByteArray()
2700 )
2701 return cleanExpression(arg);
2702 }
2703 }
2704 solAssert(expr, "");
2705 return expr;
2706 }
2707
touchedVariables(ASTNode const & _node)2708 set<VariableDeclaration const*> SMTEncoder::touchedVariables(ASTNode const& _node)
2709 {
2710 vector<CallableDeclaration const*> callStack;
2711 for (auto const& call: m_callStack)
2712 callStack.push_back(call.first);
2713 return m_variableUsage.touchedVariables(_node, callStack);
2714 }
2715
expressionToDeclaration(Expression const & _expr) const2716 Declaration const* SMTEncoder::expressionToDeclaration(Expression const& _expr) const
2717 {
2718 if (auto const* identifier = dynamic_cast<Identifier const*>(&_expr))
2719 return identifier->annotation().referencedDeclaration;
2720 if (auto const* outerMemberAccess = dynamic_cast<MemberAccess const*>(&_expr))
2721 return outerMemberAccess->annotation().referencedDeclaration;
2722 return nullptr;
2723 }
2724
identifierToVariable(Expression const & _expr) const2725 VariableDeclaration const* SMTEncoder::identifierToVariable(Expression const& _expr) const
2726 {
2727 // We do not use `expressionToDeclaration` here because we are not interested in
2728 // struct.field, for example.
2729 if (auto const* identifier = dynamic_cast<Identifier const*>(&_expr))
2730 if (auto const* varDecl = dynamic_cast<VariableDeclaration const*>(identifier->annotation().referencedDeclaration))
2731 {
2732 solAssert(m_context.knownVariable(*varDecl), "");
2733 return varDecl;
2734 }
2735 // But we are interested in "contract.var", because that is the same as just "var".
2736 if (auto const* memberAccess = dynamic_cast<MemberAccess const*>(&_expr))
2737 if (dynamic_cast<ContractDefinition const*>(expressionToDeclaration(memberAccess->expression())))
2738 if (auto const* varDecl = dynamic_cast<VariableDeclaration const*>(memberAccess->annotation().referencedDeclaration))
2739 {
2740 solAssert(m_context.knownVariable(*varDecl), "");
2741 return varDecl;
2742 }
2743
2744 return nullptr;
2745 }
2746
isEmptyPush(Expression const & _expr) const2747 MemberAccess const* SMTEncoder::isEmptyPush(Expression const& _expr) const
2748 {
2749 if (
2750 auto const* funCall = dynamic_cast<FunctionCall const*>(&_expr);
2751 funCall && funCall->arguments().empty()
2752 )
2753 {
2754 auto const& funType = dynamic_cast<FunctionType const&>(*funCall->expression().annotation().type);
2755 if (funType.kind() == FunctionType::Kind::ArrayPush)
2756 return &dynamic_cast<MemberAccess const&>(funCall->expression());
2757 }
2758 return nullptr;
2759 }
2760
isPublicGetter(Expression const & _expr)2761 bool SMTEncoder::isPublicGetter(Expression const& _expr) {
2762 if (!isTrustedExternalCall(&_expr))
2763 return false;
2764 auto varDecl = dynamic_cast<VariableDeclaration const*>(
2765 dynamic_cast<MemberAccess const&>(_expr).annotation().referencedDeclaration
2766 );
2767 return varDecl != nullptr;
2768 }
2769
isTrustedExternalCall(Expression const * _expr)2770 bool SMTEncoder::isTrustedExternalCall(Expression const* _expr) {
2771 auto memberAccess = dynamic_cast<MemberAccess const*>(_expr);
2772 if (!memberAccess)
2773 return false;
2774
2775 auto identifier = dynamic_cast<Identifier const*>(&memberAccess->expression());
2776 return identifier &&
2777 identifier->name() == "this" &&
2778 identifier->annotation().referencedDeclaration &&
2779 dynamic_cast<MagicVariableDeclaration const*>(identifier->annotation().referencedDeclaration)
2780 ;
2781 }
2782
extraComment()2783 string SMTEncoder::extraComment()
2784 {
2785 string extra;
2786 if (m_arrayAssignmentHappened)
2787 extra +=
2788 "\nNote that array aliasing is not supported,"
2789 " therefore all mapping information is erased after"
2790 " a mapping local variable/parameter is assigned.\n"
2791 "You can re-introduce information using require().";
2792 return extra;
2793 }
2794
functionCallToDefinition(FunctionCall const & _funCall,ContractDefinition const * _scopeContract,ContractDefinition const * _contextContract)2795 FunctionDefinition const* SMTEncoder::functionCallToDefinition(
2796 FunctionCall const& _funCall,
2797 ContractDefinition const* _scopeContract,
2798 ContractDefinition const* _contextContract
2799 )
2800 {
2801 if (*_funCall.annotation().kind != FunctionCallKind::FunctionCall)
2802 return {};
2803
2804 auto [calledExpr, callOptions] = functionCallExpression(_funCall);
2805
2806 if (TupleExpression const* fun = dynamic_cast<TupleExpression const*>(calledExpr))
2807 {
2808 solAssert(fun->components().size() == 1, "");
2809 calledExpr = innermostTuple(*calledExpr);
2810 }
2811
2812 auto resolveVirtual = [&](auto const* _ref) -> FunctionDefinition const* {
2813 VirtualLookup lookup = *_ref->annotation().requiredLookup;
2814 solAssert(_contextContract || lookup == VirtualLookup::Static, "No contract context provided for function lookup resolution!");
2815 auto funDef = dynamic_cast<FunctionDefinition const*>(_ref->annotation().referencedDeclaration);
2816 if (!funDef)
2817 return funDef;
2818 switch (lookup)
2819 {
2820 case VirtualLookup::Virtual:
2821 return &(funDef->resolveVirtual(*_contextContract));
2822 case VirtualLookup::Super:
2823 {
2824 solAssert(_scopeContract, "");
2825 auto super = _scopeContract->superContract(*_contextContract);
2826 solAssert(super, "Super contract not available.");
2827 return &funDef->resolveVirtual(*_contextContract, super);
2828 }
2829 case VirtualLookup::Static:
2830 return funDef;
2831 }
2832 solAssert(false, "");
2833 };
2834
2835 if (Identifier const* fun = dynamic_cast<Identifier const*>(calledExpr))
2836 return resolveVirtual(fun);
2837 else if (MemberAccess const* fun = dynamic_cast<MemberAccess const*>(calledExpr))
2838 return resolveVirtual(fun);
2839
2840 return {};
2841 }
2842
stateVariablesIncludingInheritedAndPrivate(ContractDefinition const & _contract)2843 vector<VariableDeclaration const*> SMTEncoder::stateVariablesIncludingInheritedAndPrivate(ContractDefinition const& _contract)
2844 {
2845 return fold(
2846 _contract.annotation().linearizedBaseContracts,
2847 vector<VariableDeclaration const*>{},
2848 [](auto&& _acc, auto _contract) { return _acc + _contract->stateVariables(); }
2849 );
2850 }
2851
stateVariablesIncludingInheritedAndPrivate(FunctionDefinition const & _function)2852 vector<VariableDeclaration const*> SMTEncoder::stateVariablesIncludingInheritedAndPrivate(FunctionDefinition const& _function)
2853 {
2854 return stateVariablesIncludingInheritedAndPrivate(dynamic_cast<ContractDefinition const&>(*_function.scope()));
2855 }
2856
localVariablesIncludingModifiers(FunctionDefinition const & _function,ContractDefinition const * _contract)2857 vector<VariableDeclaration const*> SMTEncoder::localVariablesIncludingModifiers(FunctionDefinition const& _function, ContractDefinition const* _contract)
2858 {
2859 return _function.localVariables() + tryCatchVariables(_function) + modifiersVariables(_function, _contract);
2860 }
2861
tryCatchVariables(FunctionDefinition const & _function)2862 vector<VariableDeclaration const*> SMTEncoder::tryCatchVariables(FunctionDefinition const& _function)
2863 {
2864 struct TryCatchVarsVisitor : public ASTConstVisitor
2865 {
2866 bool visit(TryCatchClause const& _catchClause) override
2867 {
2868 if (_catchClause.parameters())
2869 {
2870 auto const& params = _catchClause.parameters()->parameters();
2871 for (auto param: params)
2872 vars.push_back(param.get());
2873 }
2874
2875 return true;
2876 }
2877
2878 vector<VariableDeclaration const*> vars;
2879 } tryCatchVarsVisitor;
2880 _function.accept(tryCatchVarsVisitor);
2881 return tryCatchVarsVisitor.vars;
2882 }
2883
modifiersVariables(FunctionDefinition const & _function,ContractDefinition const * _contract)2884 vector<VariableDeclaration const*> SMTEncoder::modifiersVariables(FunctionDefinition const& _function, ContractDefinition const* _contract)
2885 {
2886 struct BlockVars: ASTConstVisitor
2887 {
2888 BlockVars(Block const& _block) { _block.accept(*this); }
2889 void endVisit(VariableDeclaration const& _var) { vars.push_back(&_var); }
2890 vector<VariableDeclaration const*> vars;
2891 };
2892
2893 vector<VariableDeclaration const*> vars;
2894 set<ModifierDefinition const*> visited;
2895 for (auto invok: _function.modifiers())
2896 {
2897 if (!invok)
2898 continue;
2899 auto const* modifier = resolveModifierInvocation(*invok, _contract);
2900 if (!modifier || visited.count(modifier))
2901 continue;
2902
2903 visited.insert(modifier);
2904 if (modifier->isImplemented())
2905 {
2906 vars += applyMap(modifier->parameters(), [](auto _var) { return _var.get(); });
2907 vars += BlockVars(modifier->body()).vars;
2908 }
2909 }
2910 return vars;
2911 }
2912
resolveModifierInvocation(ModifierInvocation const & _invocation,ContractDefinition const * _contract)2913 ModifierDefinition const* SMTEncoder::resolveModifierInvocation(ModifierInvocation const& _invocation, ContractDefinition const* _contract)
2914 {
2915 auto const* modifier = dynamic_cast<ModifierDefinition const*>(_invocation.name().annotation().referencedDeclaration);
2916 if (modifier)
2917 {
2918 VirtualLookup lookup = *_invocation.name().annotation().requiredLookup;
2919 solAssert(lookup == VirtualLookup::Virtual || lookup == VirtualLookup::Static, "");
2920 solAssert(_contract || lookup == VirtualLookup::Static, "No contract context provided for modifier lookup resolution!");
2921 if (lookup == VirtualLookup::Virtual)
2922 modifier = &modifier->resolveVirtual(*_contract);
2923 }
2924 return modifier;
2925 }
2926
contractFunctions(ContractDefinition const & _contract)2927 set<FunctionDefinition const*, ASTNode::CompareByID> const& SMTEncoder::contractFunctions(ContractDefinition const& _contract)
2928 {
2929 if (!m_contractFunctions.count(&_contract))
2930 {
2931 auto const& functions = _contract.definedFunctions();
2932 set<FunctionDefinition const*, ASTNode::CompareByID> resolvedFunctions(begin(functions), end(functions));
2933 for (auto const* base: _contract.annotation().linearizedBaseContracts)
2934 {
2935 if (base == &_contract)
2936 continue;
2937 for (auto const* baseFunction: base->definedFunctions())
2938 {
2939 if (baseFunction->isConstructor()) // We don't want to include constructors of parent contracts
2940 continue;
2941 bool overridden = false;
2942 for (auto const* function: resolvedFunctions)
2943 if (
2944 function->name() == baseFunction->name() &&
2945 function->kind() == baseFunction->kind() &&
2946 FunctionType(*function).asExternallyCallableFunction(false)->
2947 hasEqualParameterTypes(*FunctionType(*baseFunction).asExternallyCallableFunction(false))
2948 )
2949 {
2950 overridden = true;
2951 break;
2952 }
2953 if (!overridden)
2954 resolvedFunctions.insert(baseFunction);
2955 }
2956 }
2957 m_contractFunctions.emplace(&_contract, move(resolvedFunctions));
2958 }
2959 return m_contractFunctions.at(&_contract);
2960 }
2961
contractFunctionsWithoutVirtual(ContractDefinition const & _contract)2962 set<FunctionDefinition const*, ASTNode::CompareByID> const& SMTEncoder::contractFunctionsWithoutVirtual(ContractDefinition const& _contract)
2963 {
2964 if (!m_contractFunctionsWithoutVirtual.count(&_contract))
2965 {
2966 auto allFunctions = contractFunctions(_contract);
2967 for (auto const* base: _contract.annotation().linearizedBaseContracts)
2968 for (auto const* baseFun: base->definedFunctions())
2969 allFunctions.insert(baseFun);
2970
2971 m_contractFunctionsWithoutVirtual.emplace(&_contract, move(allFunctions));
2972
2973 }
2974 return m_contractFunctionsWithoutVirtual.at(&_contract);
2975 }
2976
sourceUnitContaining(Scopable const & _scopable)2977 SourceUnit const* SMTEncoder::sourceUnitContaining(Scopable const& _scopable)
2978 {
2979 for (auto const* s = &_scopable; s; s = dynamic_cast<Scopable const*>(s->scope()))
2980 if (auto const* source = dynamic_cast<SourceUnit const*>(s->scope()))
2981 return source;
2982 solAssert(false, "");
2983 }
2984
baseArguments(ContractDefinition const & _contract)2985 map<ContractDefinition const*, vector<ASTPointer<frontend::Expression>>> SMTEncoder::baseArguments(ContractDefinition const& _contract)
2986 {
2987 map<ContractDefinition const*, vector<ASTPointer<Expression>>> baseArgs;
2988
2989 for (auto contract: _contract.annotation().linearizedBaseContracts)
2990 {
2991 /// Collect base contracts and potential constructor arguments.
2992 for (auto specifier: contract->baseContracts())
2993 {
2994 solAssert(specifier, "");
2995 auto const& base = dynamic_cast<ContractDefinition const&>(*specifier->name().annotation().referencedDeclaration);
2996 if (auto args = specifier->arguments())
2997 baseArgs[&base] = *args;
2998 }
2999 /// Collect base constructor arguments given as constructor modifiers.
3000 if (auto constructor = contract->constructor())
3001 for (auto mod: constructor->modifiers())
3002 {
3003 auto decl = mod->name().annotation().referencedDeclaration;
3004 if (auto base = dynamic_cast<ContractDefinition const*>(decl))
3005 {
3006 solAssert(!baseArgs.count(base), "");
3007 if (auto args = mod->arguments())
3008 baseArgs[base] = *args;
3009 }
3010 }
3011 }
3012
3013 return baseArgs;
3014 }
3015
isConstant(Expression const & _expr)3016 RationalNumberType const* SMTEncoder::isConstant(Expression const& _expr)
3017 {
3018 if (auto type = dynamic_cast<RationalNumberType const*>(_expr.annotation().type))
3019 return type;
3020
3021 // _expr may not be constant evaluable.
3022 // In that case we ignore any warnings emitted by the constant evaluator,
3023 // as it will return nullptr in case of failure.
3024 ErrorList l;
3025 ErrorReporter e(l);
3026 if (auto t = ConstantEvaluator::evaluate(e, _expr))
3027 return TypeProvider::rationalNumber(t->value);
3028
3029 return nullptr;
3030 }
3031
collectABICalls(ASTNode const * _node)3032 set<FunctionCall const*> SMTEncoder::collectABICalls(ASTNode const* _node)
3033 {
3034 struct ABIFunctions: public ASTConstVisitor
3035 {
3036 ABIFunctions(ASTNode const* _node) { _node->accept(*this); }
3037 void endVisit(FunctionCall const& _funCall)
3038 {
3039 if (*_funCall.annotation().kind == FunctionCallKind::FunctionCall)
3040 switch (dynamic_cast<FunctionType const&>(*_funCall.expression().annotation().type).kind())
3041 {
3042 case FunctionType::Kind::ABIEncode:
3043 case FunctionType::Kind::ABIEncodePacked:
3044 case FunctionType::Kind::ABIEncodeWithSelector:
3045 case FunctionType::Kind::ABIEncodeCall:
3046 case FunctionType::Kind::ABIEncodeWithSignature:
3047 case FunctionType::Kind::ABIDecode:
3048 abiCalls.insert(&_funCall);
3049 break;
3050 default: {}
3051 }
3052 }
3053
3054 set<FunctionCall const*> abiCalls;
3055 };
3056
3057 return ABIFunctions(_node).abiCalls;
3058 }
3059
sourceDependencies(SourceUnit const & _source)3060 set<SourceUnit const*, ASTNode::CompareByID> SMTEncoder::sourceDependencies(SourceUnit const& _source)
3061 {
3062 set<SourceUnit const*, ASTNode::CompareByID> sources;
3063 sources.insert(&_source);
3064 for (auto const& source: _source.referencedSourceUnits(true))
3065 sources.insert(source);
3066 return sources;
3067 }
3068
createReturnedExpressions(FunctionCall const & _funCall,ContractDefinition const * _contextContract)3069 void SMTEncoder::createReturnedExpressions(FunctionCall const& _funCall, ContractDefinition const* _contextContract)
3070 {
3071 auto funDef = functionCallToDefinition(_funCall, currentScopeContract(), _contextContract);
3072 if (!funDef)
3073 return;
3074
3075 auto const& returnParams = funDef->returnParameters();
3076 for (auto param: returnParams)
3077 createVariable(*param);
3078 auto returnValues = applyMap(returnParams, [this](auto const& param) -> optional<smtutil::Expression> {
3079 solAssert(param && m_context.knownVariable(*param), "");
3080 return currentValue(*param);
3081 });
3082 defineExpr(_funCall, returnValues);
3083 }
3084
symbolicArguments(FunctionCall const & _funCall,ContractDefinition const * _contextContract)3085 vector<smtutil::Expression> SMTEncoder::symbolicArguments(FunctionCall const& _funCall, ContractDefinition const* _contextContract)
3086 {
3087 auto funDef = functionCallToDefinition(_funCall, currentScopeContract(), _contextContract);
3088 solAssert(funDef, "");
3089
3090 vector<smtutil::Expression> args;
3091 Expression const* calledExpr = &_funCall.expression();
3092 auto funType = dynamic_cast<FunctionType const*>(calledExpr->annotation().type);
3093 solAssert(funType, "");
3094
3095 vector<ASTPointer<Expression const>> arguments = _funCall.sortedArguments();
3096 auto functionParams = funDef->parameters();
3097 unsigned firstParam = 0;
3098 if (funType->bound())
3099 {
3100 calledExpr = innermostTuple(*calledExpr);
3101 auto const& boundFunction = dynamic_cast<MemberAccess const*>(calledExpr);
3102 solAssert(boundFunction, "");
3103 args.push_back(expr(boundFunction->expression(), functionParams.front()->type()));
3104 firstParam = 1;
3105 }
3106
3107 solAssert((arguments.size() + firstParam) == functionParams.size(), "");
3108 for (unsigned i = 0; i < arguments.size(); ++i)
3109 args.push_back(expr(*arguments.at(i), functionParams.at(i + firstParam)->type()));
3110
3111 return args;
3112 }
3113
constantExpr(Expression const & _expr,VariableDeclaration const & _var)3114 smtutil::Expression SMTEncoder::constantExpr(Expression const& _expr, VariableDeclaration const& _var)
3115 {
3116 if (RationalNumberType const* rationalType = isConstant(_expr))
3117 {
3118 if (rationalType->isNegative())
3119 return smtutil::Expression(u2s(rationalType->literalValue(nullptr)));
3120 else
3121 return smtutil::Expression(rationalType->literalValue(nullptr));
3122 }
3123 else
3124 {
3125 solAssert(_var.value(), "");
3126 _var.value()->accept(*this);
3127 return expr(*_var.value(), _expr.annotation().type);
3128 }
3129 solAssert(false, "");
3130 }
3131
collectFreeFunctions(set<SourceUnit const *,ASTNode::CompareByID> const & _sources)3132 void SMTEncoder::collectFreeFunctions(set<SourceUnit const*, ASTNode::CompareByID> const& _sources)
3133 {
3134 for (auto source: _sources)
3135 for (auto node: source->nodes())
3136 if (auto function = dynamic_cast<FunctionDefinition const*>(node.get()))
3137 m_freeFunctions.insert(function);
3138 else if (
3139 auto contract = dynamic_cast<ContractDefinition const*>(node.get());
3140 contract && contract->isLibrary()
3141 )
3142 {
3143 for (auto function: contract->definedFunctions())
3144 if (!function->isPublic())
3145 m_freeFunctions.insert(function);
3146 }
3147 }
3148
createFreeConstants(set<SourceUnit const *,ASTNode::CompareByID> const & _sources)3149 void SMTEncoder::createFreeConstants(set<SourceUnit const*, ASTNode::CompareByID> const& _sources)
3150 {
3151 for (auto source: _sources)
3152 for (auto node: source->nodes())
3153 if (auto var = dynamic_cast<VariableDeclaration const*>(node.get()))
3154 createVariable(*var);
3155 else if (
3156 auto contract = dynamic_cast<ContractDefinition const*>(node.get());
3157 contract && contract->isLibrary()
3158 )
3159 for (auto var: contract->stateVariables())
3160 {
3161 solAssert(var->isConstant(), "");
3162 createVariable(*var);
3163 }
3164 }
3165
state()3166 smt::SymbolicState& SMTEncoder::state()
3167 {
3168 return m_context.state();
3169 }
3170