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/CHC.h>
20
21 #ifdef HAVE_Z3
22 #include <libsmtutil/Z3CHCInterface.h>
23 #endif
24
25 #include <libsolidity/formal/ArraySlicePredicate.h>
26 #include <libsolidity/formal/Invariants.h>
27 #include <libsolidity/formal/PredicateInstance.h>
28 #include <libsolidity/formal/PredicateSort.h>
29 #include <libsolidity/formal/SymbolicTypes.h>
30
31 #include <libsolidity/ast/TypeProvider.h>
32
33 #include <libsmtutil/CHCSmtLib2Interface.h>
34 #include <liblangutil/CharStreamProvider.h>
35 #include <libsolutil/Algorithms.h>
36
37 #ifdef HAVE_Z3_DLOPEN
38 #include <z3_version.h>
39 #endif
40
41 #include <boost/algorithm/string.hpp>
42
43 #include <range/v3/algorithm/for_each.hpp>
44 #include <range/v3/view.hpp>
45 #include <range/v3/view/enumerate.hpp>
46 #include <range/v3/view/reverse.hpp>
47
48 #include <charconv>
49 #include <queue>
50
51 using namespace std;
52 using namespace solidity;
53 using namespace solidity::util;
54 using namespace solidity::langutil;
55 using namespace solidity::smtutil;
56 using namespace solidity::frontend;
57 using namespace solidity::frontend::smt;
58
CHC(EncodingContext & _context,UniqueErrorReporter & _errorReporter,map<util::h256,string> const & _smtlib2Responses,ReadCallback::Callback const & _smtCallback,ModelCheckerSettings const & _settings,CharStreamProvider const & _charStreamProvider)59 CHC::CHC(
60 EncodingContext& _context,
61 UniqueErrorReporter& _errorReporter,
62 [[maybe_unused]] map<util::h256, string> const& _smtlib2Responses,
63 [[maybe_unused]] ReadCallback::Callback const& _smtCallback,
64 ModelCheckerSettings const& _settings,
65 CharStreamProvider const& _charStreamProvider
66 ):
67 SMTEncoder(_context, _settings, _errorReporter, _charStreamProvider)
68 {
69 bool usesZ3 = m_settings.solvers.z3;
70 #ifdef HAVE_Z3
71 usesZ3 = usesZ3 && Z3Interface::available();
72 #else
73 usesZ3 = false;
74 #endif
75 if (!usesZ3 && m_settings.solvers.smtlib2)
76 m_interface = make_unique<CHCSmtLib2Interface>(_smtlib2Responses, _smtCallback, m_settings.timeout);
77 }
78
analyze(SourceUnit const & _source)79 void CHC::analyze(SourceUnit const& _source)
80 {
81 if (!m_settings.solvers.z3 && !m_settings.solvers.smtlib2)
82 {
83 if (!m_noSolverWarning)
84 {
85 m_noSolverWarning = true;
86 m_errorReporter.warning(
87 7649_error,
88 SourceLocation(),
89 "CHC analysis was not possible since no Horn solver was enabled."
90 );
91 }
92 return;
93 }
94
95 resetSourceAnalysis();
96
97 auto sources = sourceDependencies(_source);
98 collectFreeFunctions(sources);
99 createFreeConstants(sources);
100 state().prepareForSourceUnit(_source);
101
102 for (auto const* source: sources)
103 defineInterfacesAndSummaries(*source);
104 for (auto const* source: sources)
105 source->accept(*this);
106
107 checkVerificationTargets();
108
109 bool ranSolver = true;
110 // If ranSolver is true here it's because an SMT solver callback was
111 // actually given and the queries were solved.
112 if (auto const* smtLibInterface = dynamic_cast<CHCSmtLib2Interface const*>(m_interface.get()))
113 ranSolver = smtLibInterface->unhandledQueries().empty();
114 if (!ranSolver && !m_noSolverWarning)
115 {
116 m_noSolverWarning = true;
117 m_errorReporter.warning(
118 3996_error,
119 SourceLocation(),
120 #ifdef HAVE_Z3_DLOPEN
121 "CHC analysis was not possible since libz3.so." + to_string(Z3_MAJOR_VERSION) + "." + to_string(Z3_MINOR_VERSION) + " was not found."
122 #else
123 "CHC analysis was not possible. No Horn solver was available."
124 " None of the installed solvers was enabled."
125 #endif
126 );
127 }
128 }
129
unhandledQueries() const130 vector<string> CHC::unhandledQueries() const
131 {
132 if (auto smtlib2 = dynamic_cast<CHCSmtLib2Interface const*>(m_interface.get()))
133 return smtlib2->unhandledQueries();
134
135 return {};
136 }
137
visit(ContractDefinition const & _contract)138 bool CHC::visit(ContractDefinition const& _contract)
139 {
140 resetContractAnalysis();
141 initContract(_contract);
142 clearIndices(&_contract);
143
144 m_scopes.push_back(&_contract);
145
146 m_stateVariables = SMTEncoder::stateVariablesIncludingInheritedAndPrivate(_contract);
147 solAssert(m_currentContract, "");
148
149 SMTEncoder::visit(_contract);
150 return false;
151 }
152
endVisit(ContractDefinition const & _contract)153 void CHC::endVisit(ContractDefinition const& _contract)
154 {
155 for (auto base: _contract.annotation().linearizedBaseContracts)
156 {
157 if (auto constructor = base->constructor())
158 constructor->accept(*this);
159 defineContractInitializer(*base, _contract);
160 }
161
162 auto const& entry = *createConstructorBlock(_contract, "implicit_constructor_entry");
163
164 // In case constructors use uninitialized state variables,
165 // they need to be zeroed.
166 // This is not part of `initialConstraints` because it's only true here,
167 // at the beginning of the deployment routine.
168 smtutil::Expression zeroes(true);
169 for (auto var: stateVariablesIncludingInheritedAndPrivate(_contract))
170 zeroes = zeroes && currentValue(*var) == smt::zeroValue(var->type());
171 // The contract's address might already have funds before deployment,
172 // so the balance must be at least `msg.value`, but not equals.
173 auto initialBalanceConstraint = state().balance(state().thisAddress()) >= state().txMember("msg.value");
174 addRule(smtutil::Expression::implies(
175 initialConstraints(_contract) && zeroes && initialBalanceConstraint,
176 predicate(entry)
177 ), entry.functor().name);
178 setCurrentBlock(entry);
179
180 solAssert(!m_errorDest, "");
181 m_errorDest = m_constructorSummaries.at(&_contract);
182 // We need to evaluate the base constructor calls (arguments) from derived -> base
183 auto baseArgs = baseArguments(_contract);
184 for (auto base: _contract.annotation().linearizedBaseContracts)
185 if (base != &_contract)
186 {
187 m_callGraph[&_contract].insert(base);
188
189 auto baseConstructor = base->constructor();
190 if (baseConstructor && baseArgs.count(base))
191 {
192 vector<ASTPointer<Expression>> const& args = baseArgs.at(base);
193 auto const& params = baseConstructor->parameters();
194 solAssert(params.size() == args.size(), "");
195 for (unsigned i = 0; i < params.size(); ++i)
196 {
197 args.at(i)->accept(*this);
198 if (params.at(i))
199 {
200 solAssert(m_context.knownVariable(*params.at(i)), "");
201 m_context.addAssertion(currentValue(*params.at(i)) == expr(*args.at(i), params.at(i)->type()));
202 }
203 }
204 }
205 }
206 m_errorDest = nullptr;
207 // Then call initializer_Base from base -> derived
208 for (auto base: _contract.annotation().linearizedBaseContracts | ranges::views::reverse)
209 {
210 errorFlag().increaseIndex();
211 m_context.addAssertion(smt::constructorCall(*m_contractInitializers.at(&_contract).at(base), m_context));
212 connectBlocks(m_currentBlock, summary(_contract), errorFlag().currentValue() > 0);
213 m_context.addAssertion(errorFlag().currentValue() == 0);
214 }
215
216 connectBlocks(m_currentBlock, summary(_contract));
217
218 setCurrentBlock(*m_constructorSummaries.at(&_contract));
219
220 solAssert(&_contract == m_currentContract, "");
221 if (shouldAnalyze(_contract))
222 {
223 auto constructor = _contract.constructor();
224 auto txConstraints = state().txTypeConstraints();
225 if (!constructor || !constructor->isPayable())
226 txConstraints = txConstraints && state().txNonPayableConstraint();
227 m_queryPlaceholders[&_contract].push_back({txConstraints, errorFlag().currentValue(), m_currentBlock});
228 connectBlocks(m_currentBlock, interface(), txConstraints && errorFlag().currentValue() == 0);
229 }
230
231 solAssert(m_scopes.back() == &_contract, "");
232 m_scopes.pop_back();
233
234 SMTEncoder::endVisit(_contract);
235 }
236
visit(FunctionDefinition const & _function)237 bool CHC::visit(FunctionDefinition const& _function)
238 {
239 // Free functions need to be visited in the context of a contract.
240 if (!m_currentContract)
241 return false;
242
243 if (
244 !_function.isImplemented() ||
245 abstractAsNondet(_function)
246 )
247 {
248 smtutil::Expression conj(true);
249 if (
250 _function.stateMutability() == StateMutability::Pure ||
251 _function.stateMutability() == StateMutability::View
252 )
253 conj = conj && currentEqualInitialVarsConstraints(stateVariablesIncludingInheritedAndPrivate(_function));
254
255 conj = conj && errorFlag().currentValue() == 0;
256 addRule(smtutil::Expression::implies(conj, summary(_function)), "summary_function_" + to_string(_function.id()));
257 return false;
258 }
259
260 // No inlining.
261 solAssert(!m_currentFunction, "Function inlining should not happen in CHC.");
262 m_currentFunction = &_function;
263
264 m_scopes.push_back(&_function);
265
266 initFunction(_function);
267
268 auto functionEntryBlock = createBlock(m_currentFunction, PredicateType::FunctionBlock);
269 auto bodyBlock = createBlock(&m_currentFunction->body(), PredicateType::FunctionBlock);
270
271 auto functionPred = predicate(*functionEntryBlock);
272 auto bodyPred = predicate(*bodyBlock);
273
274 addRule(functionPred, functionPred.name);
275
276 solAssert(m_currentContract, "");
277 m_context.addAssertion(initialConstraints(*m_currentContract, &_function));
278
279 connectBlocks(functionPred, bodyPred);
280
281 setCurrentBlock(*bodyBlock);
282
283 solAssert(!m_errorDest, "");
284 m_errorDest = m_summaries.at(m_currentContract).at(&_function);
285 SMTEncoder::visit(*m_currentFunction);
286 m_errorDest = nullptr;
287
288 return false;
289 }
290
endVisit(FunctionDefinition const & _function)291 void CHC::endVisit(FunctionDefinition const& _function)
292 {
293 // Free functions need to be visited in the context of a contract.
294 if (!m_currentContract)
295 return;
296
297 if (
298 !_function.isImplemented() ||
299 abstractAsNondet(_function)
300 )
301 return;
302
303 solAssert(m_currentFunction && m_currentContract, "");
304 // No inlining.
305 solAssert(m_currentFunction == &_function, "");
306
307 solAssert(m_scopes.back() == &_function, "");
308 m_scopes.pop_back();
309
310 connectBlocks(m_currentBlock, summary(_function));
311 setCurrentBlock(*m_summaries.at(m_currentContract).at(&_function));
312
313 // Query placeholders for constructors are not created here because
314 // of contracts without constructors.
315 // Instead, those are created in endVisit(ContractDefinition).
316 if (
317 !_function.isConstructor() &&
318 _function.isPublic() &&
319 contractFunctions(*m_currentContract).count(&_function) &&
320 shouldAnalyze(*m_currentContract)
321 )
322 {
323 defineExternalFunctionInterface(_function, *m_currentContract);
324 setCurrentBlock(*m_interfaces.at(m_currentContract));
325
326 // Create the rule
327 // interface \land externalFunctionEntry => interface'
328 auto ifacePre = smt::interfacePre(*m_interfaces.at(m_currentContract), *m_currentContract, m_context);
329 auto sum = externalSummary(_function);
330
331 m_queryPlaceholders[&_function].push_back({sum, errorFlag().currentValue(), ifacePre});
332 connectBlocks(ifacePre, interface(), sum && errorFlag().currentValue() == 0);
333 }
334
335 m_currentFunction = nullptr;
336
337 SMTEncoder::endVisit(_function);
338 }
339
visit(Block const & _block)340 bool CHC::visit(Block const& _block)
341 {
342 m_scopes.push_back(&_block);
343 return SMTEncoder::visit(_block);
344 }
345
endVisit(Block const & _block)346 void CHC::endVisit(Block const& _block)
347 {
348 solAssert(m_scopes.back() == &_block, "");
349 m_scopes.pop_back();
350 SMTEncoder::endVisit(_block);
351 }
352
visit(IfStatement const & _if)353 bool CHC::visit(IfStatement const& _if)
354 {
355 solAssert(m_currentFunction, "");
356
357 bool unknownFunctionCallWasSeen = m_unknownFunctionCallSeen;
358 m_unknownFunctionCallSeen = false;
359
360 solAssert(m_currentFunction, "");
361 auto const& functionBody = m_currentFunction->body();
362
363 auto ifHeaderBlock = createBlock(&_if, PredicateType::FunctionBlock, "if_header_");
364 auto trueBlock = createBlock(&_if.trueStatement(), PredicateType::FunctionBlock, "if_true_");
365 auto falseBlock = _if.falseStatement() ? createBlock(_if.falseStatement(), PredicateType::FunctionBlock, "if_false_") : nullptr;
366 auto afterIfBlock = createBlock(&functionBody, PredicateType::FunctionBlock);
367
368 connectBlocks(m_currentBlock, predicate(*ifHeaderBlock));
369
370 setCurrentBlock(*ifHeaderBlock);
371 _if.condition().accept(*this);
372 auto condition = expr(_if.condition());
373
374 connectBlocks(m_currentBlock, predicate(*trueBlock), condition);
375 if (_if.falseStatement())
376 connectBlocks(m_currentBlock, predicate(*falseBlock), !condition);
377 else
378 connectBlocks(m_currentBlock, predicate(*afterIfBlock), !condition);
379
380 setCurrentBlock(*trueBlock);
381 _if.trueStatement().accept(*this);
382 connectBlocks(m_currentBlock, predicate(*afterIfBlock));
383
384 if (_if.falseStatement())
385 {
386 setCurrentBlock(*falseBlock);
387 _if.falseStatement()->accept(*this);
388 connectBlocks(m_currentBlock, predicate(*afterIfBlock));
389 }
390
391 setCurrentBlock(*afterIfBlock);
392
393 if (m_unknownFunctionCallSeen)
394 eraseKnowledge();
395
396 m_unknownFunctionCallSeen = unknownFunctionCallWasSeen;
397
398 return false;
399 }
400
visit(WhileStatement const & _while)401 bool CHC::visit(WhileStatement const& _while)
402 {
403 bool unknownFunctionCallWasSeen = m_unknownFunctionCallSeen;
404 m_unknownFunctionCallSeen = false;
405
406 solAssert(m_currentFunction, "");
407 auto const& functionBody = m_currentFunction->body();
408
409 auto namePrefix = string(_while.isDoWhile() ? "do_" : "") + "while";
410 auto loopHeaderBlock = createBlock(&_while, PredicateType::FunctionBlock, namePrefix + "_header_");
411 auto loopBodyBlock = createBlock(&_while.body(), PredicateType::FunctionBlock, namePrefix + "_body_");
412 auto afterLoopBlock = createBlock(&functionBody, PredicateType::FunctionBlock);
413
414 auto outerBreakDest = m_breakDest;
415 auto outerContinueDest = m_continueDest;
416 m_breakDest = afterLoopBlock;
417 m_continueDest = loopHeaderBlock;
418
419 if (_while.isDoWhile())
420 _while.body().accept(*this);
421
422 connectBlocks(m_currentBlock, predicate(*loopHeaderBlock));
423
424 setCurrentBlock(*loopHeaderBlock);
425
426 _while.condition().accept(*this);
427 auto condition = expr(_while.condition());
428
429 connectBlocks(m_currentBlock, predicate(*loopBodyBlock), condition);
430 connectBlocks(m_currentBlock, predicate(*afterLoopBlock), !condition);
431
432 // Loop body visit.
433 setCurrentBlock(*loopBodyBlock);
434 _while.body().accept(*this);
435
436 m_breakDest = outerBreakDest;
437 m_continueDest = outerContinueDest;
438
439 // Back edge.
440 connectBlocks(m_currentBlock, predicate(*loopHeaderBlock));
441 setCurrentBlock(*afterLoopBlock);
442
443 if (m_unknownFunctionCallSeen)
444 eraseKnowledge();
445
446 m_unknownFunctionCallSeen = unknownFunctionCallWasSeen;
447
448 return false;
449 }
450
visit(ForStatement const & _for)451 bool CHC::visit(ForStatement const& _for)
452 {
453 m_scopes.push_back(&_for);
454
455 bool unknownFunctionCallWasSeen = m_unknownFunctionCallSeen;
456 m_unknownFunctionCallSeen = false;
457
458 solAssert(m_currentFunction, "");
459 auto const& functionBody = m_currentFunction->body();
460
461 auto loopHeaderBlock = createBlock(&_for, PredicateType::FunctionBlock, "for_header_");
462 auto loopBodyBlock = createBlock(&_for.body(), PredicateType::FunctionBlock, "for_body_");
463 auto afterLoopBlock = createBlock(&functionBody, PredicateType::FunctionBlock);
464 auto postLoop = _for.loopExpression();
465 auto postLoopBlock = postLoop ? createBlock(postLoop, PredicateType::FunctionBlock, "for_post_") : nullptr;
466
467 auto outerBreakDest = m_breakDest;
468 auto outerContinueDest = m_continueDest;
469 m_breakDest = afterLoopBlock;
470 m_continueDest = postLoop ? postLoopBlock : loopHeaderBlock;
471
472 if (auto init = _for.initializationExpression())
473 init->accept(*this);
474
475 connectBlocks(m_currentBlock, predicate(*loopHeaderBlock));
476 setCurrentBlock(*loopHeaderBlock);
477
478 auto condition = smtutil::Expression(true);
479 if (auto forCondition = _for.condition())
480 {
481 forCondition->accept(*this);
482 condition = expr(*forCondition);
483 }
484
485 connectBlocks(m_currentBlock, predicate(*loopBodyBlock), condition);
486 connectBlocks(m_currentBlock, predicate(*afterLoopBlock), !condition);
487
488 // Loop body visit.
489 setCurrentBlock(*loopBodyBlock);
490 _for.body().accept(*this);
491
492 if (postLoop)
493 {
494 connectBlocks(m_currentBlock, predicate(*postLoopBlock));
495 setCurrentBlock(*postLoopBlock);
496 postLoop->accept(*this);
497 }
498
499 m_breakDest = outerBreakDest;
500 m_continueDest = outerContinueDest;
501
502 // Back edge.
503 connectBlocks(m_currentBlock, predicate(*loopHeaderBlock));
504 setCurrentBlock(*afterLoopBlock);
505
506 if (m_unknownFunctionCallSeen)
507 eraseKnowledge();
508
509 m_unknownFunctionCallSeen = unknownFunctionCallWasSeen;
510
511 return false;
512 }
513
endVisit(ForStatement const & _for)514 void CHC::endVisit(ForStatement const& _for)
515 {
516 solAssert(m_scopes.back() == &_for, "");
517 m_scopes.pop_back();
518 }
519
endVisit(FunctionCall const & _funCall)520 void CHC::endVisit(FunctionCall const& _funCall)
521 {
522 auto functionCallKind = *_funCall.annotation().kind;
523
524 if (functionCallKind != FunctionCallKind::FunctionCall)
525 {
526 SMTEncoder::endVisit(_funCall);
527 return;
528 }
529
530 FunctionType const& funType = dynamic_cast<FunctionType const&>(*_funCall.expression().annotation().type);
531 switch (funType.kind())
532 {
533 case FunctionType::Kind::Assert:
534 visitAssert(_funCall);
535 SMTEncoder::endVisit(_funCall);
536 break;
537 case FunctionType::Kind::Internal:
538 internalFunctionCall(_funCall);
539 break;
540 case FunctionType::Kind::External:
541 case FunctionType::Kind::BareStaticCall:
542 case FunctionType::Kind::BareCall:
543 externalFunctionCall(_funCall);
544 SMTEncoder::endVisit(_funCall);
545 break;
546 case FunctionType::Kind::DelegateCall:
547 case FunctionType::Kind::BareCallCode:
548 case FunctionType::Kind::BareDelegateCall:
549 case FunctionType::Kind::Creation:
550 SMTEncoder::endVisit(_funCall);
551 unknownFunctionCall(_funCall);
552 break;
553 case FunctionType::Kind::KECCAK256:
554 case FunctionType::Kind::ECRecover:
555 case FunctionType::Kind::SHA256:
556 case FunctionType::Kind::RIPEMD160:
557 case FunctionType::Kind::BlockHash:
558 case FunctionType::Kind::AddMod:
559 case FunctionType::Kind::MulMod:
560 case FunctionType::Kind::Unwrap:
561 case FunctionType::Kind::Wrap:
562 [[fallthrough]];
563 default:
564 SMTEncoder::endVisit(_funCall);
565 break;
566 }
567
568
569 createReturnedExpressions(_funCall, m_currentContract);
570 }
571
endVisit(Break const & _break)572 void CHC::endVisit(Break const& _break)
573 {
574 solAssert(m_breakDest, "");
575 connectBlocks(m_currentBlock, predicate(*m_breakDest));
576
577 // Add an unreachable ghost node to collect unreachable statements after a break.
578 auto breakGhost = createBlock(&_break, PredicateType::FunctionBlock, "break_ghost_");
579 m_currentBlock = predicate(*breakGhost);
580 }
581
endVisit(Continue const & _continue)582 void CHC::endVisit(Continue const& _continue)
583 {
584 solAssert(m_continueDest, "");
585 connectBlocks(m_currentBlock, predicate(*m_continueDest));
586
587 // Add an unreachable ghost node to collect unreachable statements after a continue.
588 auto continueGhost = createBlock(&_continue, PredicateType::FunctionBlock, "continue_ghost_");
589 m_currentBlock = predicate(*continueGhost);
590 }
591
endVisit(IndexRangeAccess const & _range)592 void CHC::endVisit(IndexRangeAccess const& _range)
593 {
594 createExpr(_range);
595
596 auto baseArray = dynamic_pointer_cast<SymbolicArrayVariable>(m_context.expression(_range.baseExpression()));
597 auto sliceArray = dynamic_pointer_cast<SymbolicArrayVariable>(m_context.expression(_range));
598 solAssert(baseArray && sliceArray, "");
599
600 auto const& sliceData = ArraySlicePredicate::create(sliceArray->sort(), m_context);
601 if (!sliceData.first)
602 {
603 for (auto pred: sliceData.second.predicates)
604 m_interface->registerRelation(pred->functor());
605 for (auto const& rule: sliceData.second.rules)
606 addRule(rule, "");
607 }
608
609 auto start = _range.startExpression() ? expr(*_range.startExpression()) : 0;
610 auto end = _range.endExpression() ? expr(*_range.endExpression()) : baseArray->length();
611 auto slicePred = (*sliceData.second.predicates.at(0))({
612 baseArray->elements(),
613 sliceArray->elements(),
614 start,
615 end
616 });
617
618 m_context.addAssertion(slicePred);
619 m_context.addAssertion(sliceArray->length() == end - start);
620 }
621
endVisit(Return const & _return)622 void CHC::endVisit(Return const& _return)
623 {
624 SMTEncoder::endVisit(_return);
625
626 connectBlocks(m_currentBlock, predicate(*m_returnDests.back()));
627
628 // Add an unreachable ghost node to collect unreachable statements after a return.
629 auto returnGhost = createBlock(&_return, PredicateType::FunctionBlock, "return_ghost_");
630 m_currentBlock = predicate(*returnGhost);
631 }
632
visit(TryCatchClause const & _tryStatement)633 bool CHC::visit(TryCatchClause const& _tryStatement)
634 {
635 m_scopes.push_back(&_tryStatement);
636 return SMTEncoder::visit(_tryStatement);
637 }
638
endVisit(TryCatchClause const & _tryStatement)639 void CHC::endVisit(TryCatchClause const& _tryStatement)
640 {
641 solAssert(m_scopes.back() == &_tryStatement, "");
642 m_scopes.pop_back();
643 }
644
visit(TryStatement const & _tryStatement)645 bool CHC::visit(TryStatement const& _tryStatement)
646 {
647 FunctionCall const* externalCall = dynamic_cast<FunctionCall const*>(&_tryStatement.externalCall());
648 solAssert(externalCall && externalCall->annotation().tryCall, "");
649 solAssert(m_currentFunction, "");
650
651 auto tryHeaderBlock = createBlock(&_tryStatement, PredicateType::FunctionBlock, "try_header_");
652 auto afterTryBlock = createBlock(&m_currentFunction->body(), PredicateType::FunctionBlock);
653
654 auto const& clauses = _tryStatement.clauses();
655 solAssert(clauses[0].get() == _tryStatement.successClause(), "First clause of TryStatement should be the success clause");
656 auto clauseBlocks = applyMap(clauses, [this](ASTPointer<TryCatchClause> clause) {
657 return createBlock(clause.get(), PredicateType::FunctionBlock, "try_clause_" + std::to_string(clause->id()));
658 });
659
660 connectBlocks(m_currentBlock, predicate(*tryHeaderBlock));
661 setCurrentBlock(*tryHeaderBlock);
662 // Visit everything, except the actual external call.
663 externalCall->expression().accept(*this);
664 ASTNode::listAccept(externalCall->arguments(), *this);
665 // Branch directly to all catch clauses, since in these cases, any effects of the external call are reverted.
666 for (size_t i = 1; i < clauseBlocks.size(); ++i)
667 connectBlocks(m_currentBlock, predicate(*clauseBlocks[i]));
668 // Only now visit the actual call to record its effects and connect to the success clause.
669 endVisit(*externalCall);
670 if (_tryStatement.successClause()->parameters())
671 expressionToTupleAssignment(_tryStatement.successClause()->parameters()->parameters(), *externalCall);
672
673 connectBlocks(m_currentBlock, predicate(*clauseBlocks[0]));
674
675 for (size_t i = 0; i < clauses.size(); ++i)
676 {
677 setCurrentBlock(*clauseBlocks[i]);
678 clauses[i]->accept(*this);
679 connectBlocks(m_currentBlock, predicate(*afterTryBlock));
680 }
681 setCurrentBlock(*afterTryBlock);
682
683 return false;
684 }
685
pushInlineFrame(CallableDeclaration const & _callable)686 void CHC::pushInlineFrame(CallableDeclaration const& _callable)
687 {
688 m_returnDests.push_back(createBlock(&_callable, PredicateType::FunctionBlock, "return_"));
689 }
690
popInlineFrame(CallableDeclaration const & _callable)691 void CHC::popInlineFrame(CallableDeclaration const& _callable)
692 {
693 solAssert(!m_returnDests.empty(), "");
694 auto const& ret = *m_returnDests.back();
695 solAssert(ret.programNode() == &_callable, "");
696 connectBlocks(m_currentBlock, predicate(ret));
697 setCurrentBlock(ret);
698 m_returnDests.pop_back();
699 }
700
visitAssert(FunctionCall const & _funCall)701 void CHC::visitAssert(FunctionCall const& _funCall)
702 {
703 auto const& args = _funCall.arguments();
704 solAssert(args.size() == 1, "");
705 solAssert(args.front()->annotation().type->category() == Type::Category::Bool, "");
706
707 solAssert(m_currentContract, "");
708 solAssert(m_currentFunction, "");
709 auto errorCondition = !m_context.expression(*args.front())->currentValue();
710 verificationTargetEncountered(&_funCall, VerificationTargetType::Assert, errorCondition);
711 }
712
visitAddMulMod(FunctionCall const & _funCall)713 void CHC::visitAddMulMod(FunctionCall const& _funCall)
714 {
715 solAssert(_funCall.arguments().at(2), "");
716
717 verificationTargetEncountered(&_funCall, VerificationTargetType::DivByZero, expr(*_funCall.arguments().at(2)) == 0);
718
719 SMTEncoder::visitAddMulMod(_funCall);
720 }
721
internalFunctionCall(FunctionCall const & _funCall)722 void CHC::internalFunctionCall(FunctionCall const& _funCall)
723 {
724 solAssert(m_currentContract, "");
725
726 auto function = functionCallToDefinition(_funCall, currentScopeContract(), m_currentContract);
727 if (function)
728 {
729 if (m_currentFunction && !m_currentFunction->isConstructor())
730 m_callGraph[m_currentFunction].insert(function);
731 else
732 m_callGraph[m_currentContract].insert(function);
733 }
734
735 m_context.addAssertion(predicate(_funCall));
736
737 solAssert(m_errorDest, "");
738 connectBlocks(
739 m_currentBlock,
740 predicate(*m_errorDest),
741 errorFlag().currentValue() > 0
742 );
743 m_context.addAssertion(errorFlag().currentValue() == 0);
744 }
745
externalFunctionCall(FunctionCall const & _funCall)746 void CHC::externalFunctionCall(FunctionCall const& _funCall)
747 {
748 /// In external function calls we do not add a "predicate call"
749 /// because we do not trust their function body anyway,
750 /// so we just add the nondet_interface predicate.
751
752 solAssert(m_currentContract, "");
753 auto [callExpr, callOptions] = functionCallExpression(_funCall);
754
755 if (isTrustedExternalCall(callExpr))
756 {
757 externalFunctionCallToTrustedCode(_funCall);
758 return;
759 }
760
761 FunctionType const& funType = dynamic_cast<FunctionType const&>(*callExpr->annotation().type);
762 auto kind = funType.kind();
763 solAssert(
764 kind == FunctionType::Kind::External ||
765 kind == FunctionType::Kind::BareCall ||
766 kind == FunctionType::Kind::BareStaticCall,
767 ""
768 );
769
770 bool usesStaticCall = kind == FunctionType::Kind::BareStaticCall;
771
772 solAssert(m_currentContract, "");
773 auto function = functionCallToDefinition(_funCall, currentScopeContract(), m_currentContract);
774 if (function)
775 {
776 usesStaticCall |= function->stateMutability() == StateMutability::Pure ||
777 function->stateMutability() == StateMutability::View;
778 for (auto var: function->returnParameters())
779 m_context.variable(*var)->increaseIndex();
780 }
781
782 if (!m_currentFunction || m_currentFunction->isConstructor())
783 return;
784
785 if (callOptions)
786 {
787 optional<unsigned> valueIndex;
788 for (auto&& [i, name]: callOptions->names() | ranges::views::enumerate)
789 if (name && *name == "value")
790 {
791 valueIndex = i;
792 break;
793 }
794 if (valueIndex)
795 state().addBalance(state().thisAddress(), 0 - expr(*callOptions->options().at(*valueIndex)));
796 }
797
798 auto preCallState = vector<smtutil::Expression>{state().state()} + currentStateVariables();
799
800 if (!usesStaticCall)
801 {
802 state().newState();
803 for (auto const* var: m_stateVariables)
804 m_context.variable(*var)->increaseIndex();
805 }
806
807 auto error = errorFlag().increaseIndex();
808
809 Predicate const& callPredicate = *createSymbolicBlock(
810 nondetInterfaceSort(*m_currentContract, state()),
811 "nondet_call_" + uniquePrefix(),
812 PredicateType::ExternalCallUntrusted,
813 &_funCall
814 );
815 auto postCallState = vector<smtutil::Expression>{state().state()} + currentStateVariables();
816 vector<smtutil::Expression> stateExprs{error, state().thisAddress(), state().abi(), state().crypto()};
817
818 auto nondet = (*m_nondetInterfaces.at(m_currentContract))(stateExprs + preCallState + postCallState);
819 auto nondetCall = callPredicate(stateExprs + preCallState + postCallState);
820
821 addRule(smtutil::Expression::implies(nondet, nondetCall), nondetCall.name);
822
823 m_context.addAssertion(nondetCall);
824 solAssert(m_errorDest, "");
825 connectBlocks(m_currentBlock, predicate(*m_errorDest), errorFlag().currentValue() > 0);
826
827 // To capture the possibility of a reentrant call, we record in the call graph that the current function
828 // can call any of the external methods of the current contract.
829 if (m_currentFunction)
830 for (auto const* definedFunction: contractFunctions(*m_currentContract))
831 if (!definedFunction->isConstructor() && definedFunction->isPublic())
832 m_callGraph[m_currentFunction].insert(definedFunction);
833
834 m_context.addAssertion(errorFlag().currentValue() == 0);
835 }
836
externalFunctionCallToTrustedCode(FunctionCall const & _funCall)837 void CHC::externalFunctionCallToTrustedCode(FunctionCall const& _funCall)
838 {
839 solAssert(m_currentContract, "");
840 FunctionType const& funType = dynamic_cast<FunctionType const&>(*_funCall.expression().annotation().type);
841 auto kind = funType.kind();
842 solAssert(kind == FunctionType::Kind::External || kind == FunctionType::Kind::BareStaticCall, "");
843
844 auto function = functionCallToDefinition(_funCall, currentScopeContract(), m_currentContract);
845 if (!function)
846 return;
847
848 // External call creates a new transaction.
849 auto originalTx = state().tx();
850 auto txOrigin = state().txMember("tx.origin");
851 state().newTx();
852 // set the transaction sender as this contract
853 m_context.addAssertion(state().txMember("msg.sender") == state().thisAddress());
854 // set the transaction value as 0
855 m_context.addAssertion(state().txMember("msg.value") == 0);
856 // set the origin to be the current transaction origin
857 m_context.addAssertion(state().txMember("tx.origin") == txOrigin);
858
859 smtutil::Expression pred = predicate(_funCall);
860
861 auto txConstraints = state().txTypeConstraints() && state().txFunctionConstraints(*function);
862 m_context.addAssertion(pred && txConstraints);
863 // restore the original transaction data
864 state().newTx();
865 m_context.addAssertion(originalTx == state().tx());
866
867 solAssert(m_errorDest, "");
868 connectBlocks(
869 m_currentBlock,
870 predicate(*m_errorDest),
871 (errorFlag().currentValue() > 0)
872 );
873 m_context.addAssertion(errorFlag().currentValue() == 0);
874 }
875
unknownFunctionCall(FunctionCall const &)876 void CHC::unknownFunctionCall(FunctionCall const&)
877 {
878 /// Function calls are not handled at the moment,
879 /// so always erase knowledge.
880 /// TODO remove when function calls get predicates/blocks.
881 eraseKnowledge();
882
883 /// Used to erase outer scope knowledge in loops and ifs.
884 /// TODO remove when function calls get predicates/blocks.
885 m_unknownFunctionCallSeen = true;
886 }
887
makeArrayPopVerificationTarget(FunctionCall const & _arrayPop)888 void CHC::makeArrayPopVerificationTarget(FunctionCall const& _arrayPop)
889 {
890 FunctionType const& funType = dynamic_cast<FunctionType const&>(*_arrayPop.expression().annotation().type);
891 solAssert(funType.kind() == FunctionType::Kind::ArrayPop, "");
892
893 auto memberAccess = dynamic_cast<MemberAccess const*>(cleanExpression(_arrayPop.expression()));
894 solAssert(memberAccess, "");
895 auto symbArray = dynamic_pointer_cast<SymbolicArrayVariable>(m_context.expression(memberAccess->expression()));
896 solAssert(symbArray, "");
897
898 verificationTargetEncountered(&_arrayPop, VerificationTargetType::PopEmptyArray, symbArray->length() <= 0);
899 }
900
makeOutOfBoundsVerificationTarget(IndexAccess const & _indexAccess)901 void CHC::makeOutOfBoundsVerificationTarget(IndexAccess const& _indexAccess)
902 {
903 if (_indexAccess.annotation().type->category() == Type::Category::TypeType)
904 return;
905
906 auto baseType = _indexAccess.baseExpression().annotation().type;
907
908 optional<smtutil::Expression> length;
909 if (smt::isArray(*baseType))
910 length = dynamic_cast<smt::SymbolicArrayVariable const&>(
911 *m_context.expression(_indexAccess.baseExpression())
912 ).length();
913 else if (auto const* type = dynamic_cast<FixedBytesType const*>(baseType))
914 length = smtutil::Expression(static_cast<size_t>(type->numBytes()));
915
916 optional<smtutil::Expression> target;
917 if (
918 auto index = _indexAccess.indexExpression();
919 index && length
920 )
921 target = expr(*index) < 0 || expr(*index) >= *length;
922
923 if (target)
924 verificationTargetEncountered(&_indexAccess, VerificationTargetType::OutOfBounds, *target);
925 }
926
arithmeticOperation(Token _op,smtutil::Expression const & _left,smtutil::Expression const & _right,Type const * _commonType,frontend::Expression const & _expression)927 pair<smtutil::Expression, smtutil::Expression> CHC::arithmeticOperation(
928 Token _op,
929 smtutil::Expression const& _left,
930 smtutil::Expression const& _right,
931 Type const* _commonType,
932 frontend::Expression const& _expression
933 )
934 {
935 // Unchecked does not disable div by 0 checks.
936 if (_op == Token::Mod || _op == Token::Div)
937 verificationTargetEncountered(&_expression, VerificationTargetType::DivByZero, _right == 0);
938
939 auto values = SMTEncoder::arithmeticOperation(_op, _left, _right, _commonType, _expression);
940
941 if (!m_checked)
942 return values;
943
944 IntegerType const* intType = nullptr;
945 if (auto const* type = dynamic_cast<IntegerType const*>(_commonType))
946 intType = type;
947 else
948 intType = TypeProvider::uint256();
949
950 // Mod does not need underflow/overflow checks.
951 // Div only needs overflow check for signed types.
952 if (_op == Token::Mod || (_op == Token::Div && !intType->isSigned()))
953 return values;
954
955 if (_op == Token::Div)
956 verificationTargetEncountered(&_expression, VerificationTargetType::Overflow, values.second > intType->maxValue());
957 else if (intType->isSigned())
958 {
959 verificationTargetEncountered(&_expression, VerificationTargetType::Underflow, values.second < intType->minValue());
960 verificationTargetEncountered(&_expression, VerificationTargetType::Overflow, values.second > intType->maxValue());
961 }
962 else if (_op == Token::Sub)
963 verificationTargetEncountered(&_expression, VerificationTargetType::Underflow, values.second < intType->minValue());
964 else if (_op == Token::Add || _op == Token::Mul)
965 verificationTargetEncountered(&_expression, VerificationTargetType::Overflow, values.second > intType->maxValue());
966 else
967 solAssert(false, "");
968 return values;
969 }
970
resetSourceAnalysis()971 void CHC::resetSourceAnalysis()
972 {
973 SMTEncoder::resetSourceAnalysis();
974
975 m_unprovedTargets.clear();
976 m_invariants.clear();
977 m_functionTargetIds.clear();
978 m_verificationTargets.clear();
979 m_queryPlaceholders.clear();
980 m_callGraph.clear();
981 m_summaries.clear();
982 m_externalSummaries.clear();
983 m_interfaces.clear();
984 m_nondetInterfaces.clear();
985 m_constructorSummaries.clear();
986 m_contractInitializers.clear();
987 Predicate::reset();
988 ArraySlicePredicate::reset();
989 m_blockCounter = 0;
990
991 bool usesZ3 = false;
992 #ifdef HAVE_Z3
993 usesZ3 = m_settings.solvers.z3 && Z3Interface::available();
994 if (usesZ3)
995 {
996 /// z3::fixedpoint does not have a reset mechanism, so we need to create another.
997 m_interface = std::make_unique<Z3CHCInterface>(m_settings.timeout);
998 auto z3Interface = dynamic_cast<Z3CHCInterface const*>(m_interface.get());
999 solAssert(z3Interface, "");
1000 m_context.setSolver(z3Interface->z3Interface());
1001 }
1002 #endif
1003 if (!usesZ3)
1004 {
1005 auto smtlib2Interface = dynamic_cast<CHCSmtLib2Interface*>(m_interface.get());
1006 solAssert(smtlib2Interface, "");
1007 smtlib2Interface->reset();
1008 m_context.setSolver(smtlib2Interface->smtlib2Interface());
1009 }
1010
1011 m_context.reset();
1012 m_context.resetUniqueId();
1013 m_context.setAssertionAccumulation(false);
1014 }
1015
resetContractAnalysis()1016 void CHC::resetContractAnalysis()
1017 {
1018 m_stateVariables.clear();
1019 m_unknownFunctionCallSeen = false;
1020 m_breakDest = nullptr;
1021 m_continueDest = nullptr;
1022 m_returnDests.clear();
1023 errorFlag().resetIndex();
1024 }
1025
eraseKnowledge()1026 void CHC::eraseKnowledge()
1027 {
1028 resetStorageVariables();
1029 resetBalances();
1030 }
1031
clearIndices(ContractDefinition const * _contract,FunctionDefinition const * _function)1032 void CHC::clearIndices(ContractDefinition const* _contract, FunctionDefinition const* _function)
1033 {
1034 SMTEncoder::clearIndices(_contract, _function);
1035 for (auto const* var: m_stateVariables)
1036 /// SSA index 0 is reserved for state variables at the beginning
1037 /// of the current transaction.
1038 m_context.variable(*var)->increaseIndex();
1039 if (_function)
1040 {
1041 for (auto const& var: _function->parameters() + _function->returnParameters())
1042 m_context.variable(*var)->increaseIndex();
1043 for (auto const& var: localVariablesIncludingModifiers(*_function, _contract))
1044 m_context.variable(*var)->increaseIndex();
1045 }
1046
1047 state().newState();
1048 }
1049
setCurrentBlock(Predicate const & _block)1050 void CHC::setCurrentBlock(Predicate const& _block)
1051 {
1052 if (m_context.solverStackHeigh() > 0)
1053 m_context.popSolver();
1054 solAssert(m_currentContract, "");
1055 clearIndices(m_currentContract, m_currentFunction);
1056 m_context.pushSolver();
1057 m_currentBlock = predicate(_block);
1058 }
1059
transactionVerificationTargetsIds(ASTNode const * _txRoot)1060 set<unsigned> CHC::transactionVerificationTargetsIds(ASTNode const* _txRoot)
1061 {
1062 set<unsigned> verificationTargetsIds;
1063 struct ASTNodeCompare: EncodingContext::IdCompare
1064 {
1065 bool operator<(ASTNodeCompare _other) const { return operator()(node, _other.node); }
1066 ASTNode const* node;
1067 };
1068 solidity::util::BreadthFirstSearch<ASTNodeCompare>{{{{}, _txRoot}}}.run([&](auto _node, auto&& _addChild) {
1069 verificationTargetsIds.insert(m_functionTargetIds[_node.node].begin(), m_functionTargetIds[_node.node].end());
1070 for (ASTNode const* called: m_callGraph[_node.node])
1071 _addChild({{}, called});
1072 });
1073 return verificationTargetsIds;
1074 }
1075
natspecOptionFromString(string const & _option)1076 optional<CHC::CHCNatspecOption> CHC::natspecOptionFromString(string const& _option)
1077 {
1078 static map<string, CHCNatspecOption> options{
1079 {"abstract-function-nondet", CHCNatspecOption::AbstractFunctionNondet}
1080 };
1081 if (options.count(_option))
1082 return options.at(_option);
1083 return {};
1084 }
1085
smtNatspecTags(FunctionDefinition const & _function)1086 set<CHC::CHCNatspecOption> CHC::smtNatspecTags(FunctionDefinition const& _function)
1087 {
1088 set<CHC::CHCNatspecOption> options;
1089 string smtStr = "custom:smtchecker";
1090 for (auto const& [tag, value]: _function.annotation().docTags)
1091 if (tag == smtStr)
1092 {
1093 string const& content = value.content;
1094 if (auto option = natspecOptionFromString(content))
1095 options.insert(*option);
1096 else
1097 m_errorReporter.warning(3130_error, _function.location(), "Unknown option for \"" + smtStr + "\": \"" + content + "\"");
1098 }
1099 return options;
1100 }
1101
abstractAsNondet(FunctionDefinition const & _function)1102 bool CHC::abstractAsNondet(FunctionDefinition const& _function)
1103 {
1104 return smtNatspecTags(_function).count(CHCNatspecOption::AbstractFunctionNondet);
1105 }
1106
sort(FunctionDefinition const & _function)1107 SortPointer CHC::sort(FunctionDefinition const& _function)
1108 {
1109 return functionBodySort(_function, m_currentContract, state());
1110 }
1111
sort(ASTNode const * _node)1112 SortPointer CHC::sort(ASTNode const* _node)
1113 {
1114 if (auto funDef = dynamic_cast<FunctionDefinition const*>(_node))
1115 return sort(*funDef);
1116
1117 solAssert(m_currentFunction, "");
1118 return functionBodySort(*m_currentFunction, m_currentContract, state());
1119 }
1120
createSymbolicBlock(SortPointer _sort,string const & _name,PredicateType _predType,ASTNode const * _node,ContractDefinition const * _contractContext)1121 Predicate const* CHC::createSymbolicBlock(SortPointer _sort, string const& _name, PredicateType _predType, ASTNode const* _node, ContractDefinition const* _contractContext)
1122 {
1123 auto const* block = Predicate::create(_sort, _name, _predType, m_context, _node, _contractContext, m_scopes);
1124 m_interface->registerRelation(block->functor());
1125 return block;
1126 }
1127
defineInterfacesAndSummaries(SourceUnit const & _source)1128 void CHC::defineInterfacesAndSummaries(SourceUnit const& _source)
1129 {
1130 for (auto const& node: _source.nodes())
1131 if (auto const* contract = dynamic_cast<ContractDefinition const*>(node.get()))
1132 {
1133 string suffix = contract->name() + "_" + to_string(contract->id());
1134 m_interfaces[contract] = createSymbolicBlock(interfaceSort(*contract, state()), "interface_" + uniquePrefix() + "_" + suffix, PredicateType::Interface, contract, contract);
1135 m_nondetInterfaces[contract] = createSymbolicBlock(nondetInterfaceSort(*contract, state()), "nondet_interface_" + uniquePrefix() + "_" + suffix, PredicateType::NondetInterface, contract, contract);
1136 m_constructorSummaries[contract] = createConstructorBlock(*contract, "summary_constructor");
1137
1138 for (auto const* var: stateVariablesIncludingInheritedAndPrivate(*contract))
1139 if (!m_context.knownVariable(*var))
1140 createVariable(*var);
1141
1142 /// Base nondeterministic interface that allows
1143 /// 0 steps to be taken, used as base for the inductive
1144 /// rule for each function.
1145 auto const& iface = *m_nondetInterfaces.at(contract);
1146 addRule(smtutil::Expression::implies(errorFlag().currentValue() == 0, smt::nondetInterface(iface, *contract, m_context, 0, 0)), "base_nondet");
1147
1148 auto const& resolved = contractFunctions(*contract);
1149 for (auto const* function: contractFunctionsWithoutVirtual(*contract) + allFreeFunctions())
1150 {
1151 for (auto var: function->parameters())
1152 createVariable(*var);
1153 for (auto var: function->returnParameters())
1154 createVariable(*var);
1155 for (auto const* var: localVariablesIncludingModifiers(*function, contract))
1156 createVariable(*var);
1157
1158 m_summaries[contract].emplace(function, createSummaryBlock(*function, *contract));
1159
1160 if (!function->isConstructor() && function->isPublic() && resolved.count(function))
1161 {
1162 m_externalSummaries[contract].emplace(function, createSummaryBlock(*function, *contract));
1163
1164 auto state1 = stateVariablesAtIndex(1, *contract);
1165 auto state2 = stateVariablesAtIndex(2, *contract);
1166
1167 auto errorPre = errorFlag().currentValue();
1168 auto nondetPre = smt::nondetInterface(iface, *contract, m_context, 0, 1);
1169 auto errorPost = errorFlag().increaseIndex();
1170 auto nondetPost = smt::nondetInterface(iface, *contract, m_context, 0, 2);
1171
1172 vector<smtutil::Expression> args{errorPost, state().thisAddress(), state().abi(), state().crypto(), state().tx(), state().state(1)};
1173 args += state1 +
1174 applyMap(function->parameters(), [this](auto _var) { return valueAtIndex(*_var, 0); }) +
1175 vector<smtutil::Expression>{state().state(2)} +
1176 state2 +
1177 applyMap(function->parameters(), [this](auto _var) { return valueAtIndex(*_var, 1); }) +
1178 applyMap(function->returnParameters(), [this](auto _var) { return valueAtIndex(*_var, 1); });
1179
1180 connectBlocks(nondetPre, nondetPost, errorPre == 0 && (*m_externalSummaries.at(contract).at(function))(args));
1181 }
1182 }
1183 }
1184 }
1185
defineExternalFunctionInterface(FunctionDefinition const & _function,ContractDefinition const & _contract)1186 void CHC::defineExternalFunctionInterface(FunctionDefinition const& _function, ContractDefinition const& _contract)
1187 {
1188 // Create a rule that represents an external call to this function.
1189 // This contains more things than the function body itself,
1190 // such as balance updates because of ``msg.value``.
1191 auto functionEntryBlock = createBlock(&_function, PredicateType::FunctionBlock);
1192 auto functionPred = predicate(*functionEntryBlock);
1193 addRule(functionPred, functionPred.name);
1194 setCurrentBlock(*functionEntryBlock);
1195
1196 m_context.addAssertion(initialConstraints(_contract, &_function));
1197 m_context.addAssertion(state().txTypeConstraints() && state().txFunctionConstraints(_function));
1198
1199 // The contract may have received funds through a selfdestruct or
1200 // block.coinbase, which do not trigger calls into the contract.
1201 // So the only constraint we can add here is that the balance of
1202 // the contract grows by at least `msg.value`.
1203 SymbolicIntVariable k{TypeProvider::uint256(), TypeProvider::uint256(), "funds_" + to_string(m_context.newUniqueId()), m_context};
1204 m_context.addAssertion(k.currentValue() >= state().txMember("msg.value"));
1205 // Assume that address(this).balance cannot overflow.
1206 m_context.addAssertion(smt::symbolicUnknownConstraints(state().balance(state().thisAddress()) + k.currentValue(), TypeProvider::uint256()));
1207 state().addBalance(state().thisAddress(), k.currentValue());
1208
1209 errorFlag().increaseIndex();
1210 m_context.addAssertion(summaryCall(_function));
1211
1212 connectBlocks(functionPred, externalSummary(_function));
1213 }
1214
defineContractInitializer(ContractDefinition const & _contract,ContractDefinition const & _contextContract)1215 void CHC::defineContractInitializer(ContractDefinition const& _contract, ContractDefinition const& _contextContract)
1216 {
1217 m_contractInitializers[&_contextContract][&_contract] = createConstructorBlock(_contract, "contract_initializer");
1218 auto const& implicitConstructorPredicate = *createConstructorBlock(_contract, "contract_initializer_entry");
1219
1220 auto implicitFact = smt::constructor(implicitConstructorPredicate, m_context);
1221 addRule(smtutil::Expression::implies(initialConstraints(_contract), implicitFact), implicitFact.name);
1222 setCurrentBlock(implicitConstructorPredicate);
1223
1224 auto prevErrorDest = m_errorDest;
1225 m_errorDest = m_contractInitializers.at(&_contextContract).at(&_contract);
1226 for (auto var: _contract.stateVariables())
1227 if (var->value())
1228 {
1229 var->value()->accept(*this);
1230 assignment(*var, *var->value());
1231 }
1232 m_errorDest = prevErrorDest;
1233
1234 auto const& afterInit = *createConstructorBlock(_contract, "contract_initializer_after_init");
1235 connectBlocks(m_currentBlock, predicate(afterInit));
1236 setCurrentBlock(afterInit);
1237
1238 if (auto constructor = _contract.constructor())
1239 {
1240 errorFlag().increaseIndex();
1241 m_context.addAssertion(smt::functionCall(*m_summaries.at(&_contextContract).at(constructor), &_contextContract, m_context));
1242 connectBlocks(m_currentBlock, initializer(_contract, _contextContract), errorFlag().currentValue() > 0);
1243 m_context.addAssertion(errorFlag().currentValue() == 0);
1244 }
1245
1246 connectBlocks(m_currentBlock, initializer(_contract, _contextContract));
1247 }
1248
interface()1249 smtutil::Expression CHC::interface()
1250 {
1251 solAssert(m_currentContract, "");
1252 return interface(*m_currentContract);
1253 }
1254
interface(ContractDefinition const & _contract)1255 smtutil::Expression CHC::interface(ContractDefinition const& _contract)
1256 {
1257 return ::interface(*m_interfaces.at(&_contract), _contract, m_context);
1258 }
1259
error()1260 smtutil::Expression CHC::error()
1261 {
1262 return (*m_errorPredicate)({});
1263 }
1264
error(unsigned _idx)1265 smtutil::Expression CHC::error(unsigned _idx)
1266 {
1267 return m_errorPredicate->functor(_idx)({});
1268 }
1269
initializer(ContractDefinition const & _contract,ContractDefinition const & _contractContext)1270 smtutil::Expression CHC::initializer(ContractDefinition const& _contract, ContractDefinition const& _contractContext)
1271 {
1272 return predicate(*m_contractInitializers.at(&_contractContext).at(&_contract));
1273 }
1274
summary(ContractDefinition const & _contract)1275 smtutil::Expression CHC::summary(ContractDefinition const& _contract)
1276 {
1277 return predicate(*m_constructorSummaries.at(&_contract));
1278 }
1279
summary(FunctionDefinition const & _function,ContractDefinition const & _contract)1280 smtutil::Expression CHC::summary(FunctionDefinition const& _function, ContractDefinition const& _contract)
1281 {
1282 return smt::function(*m_summaries.at(&_contract).at(&_function), &_contract, m_context);
1283 }
1284
summaryCall(FunctionDefinition const & _function,ContractDefinition const & _contract)1285 smtutil::Expression CHC::summaryCall(FunctionDefinition const& _function, ContractDefinition const& _contract)
1286 {
1287 return smt::functionCall(*m_summaries.at(&_contract).at(&_function), &_contract, m_context);
1288 }
1289
externalSummary(FunctionDefinition const & _function,ContractDefinition const & _contract)1290 smtutil::Expression CHC::externalSummary(FunctionDefinition const& _function, ContractDefinition const& _contract)
1291 {
1292 return smt::function(*m_externalSummaries.at(&_contract).at(&_function), &_contract, m_context);
1293 }
1294
summary(FunctionDefinition const & _function)1295 smtutil::Expression CHC::summary(FunctionDefinition const& _function)
1296 {
1297 solAssert(m_currentContract, "");
1298 return summary(_function, *m_currentContract);
1299 }
1300
summaryCall(FunctionDefinition const & _function)1301 smtutil::Expression CHC::summaryCall(FunctionDefinition const& _function)
1302 {
1303 solAssert(m_currentContract, "");
1304 return summaryCall(_function, *m_currentContract);
1305 }
1306
externalSummary(FunctionDefinition const & _function)1307 smtutil::Expression CHC::externalSummary(FunctionDefinition const& _function)
1308 {
1309 solAssert(m_currentContract, "");
1310 return externalSummary(_function, *m_currentContract);
1311 }
1312
createBlock(ASTNode const * _node,PredicateType _predType,string const & _prefix)1313 Predicate const* CHC::createBlock(ASTNode const* _node, PredicateType _predType, string const& _prefix)
1314 {
1315 auto block = createSymbolicBlock(
1316 sort(_node),
1317 "block_" + uniquePrefix() + "_" + _prefix + predicateName(_node),
1318 _predType,
1319 _node,
1320 m_currentContract
1321 );
1322
1323 solAssert(m_currentFunction, "");
1324 return block;
1325 }
1326
createSummaryBlock(FunctionDefinition const & _function,ContractDefinition const & _contract,PredicateType _type)1327 Predicate const* CHC::createSummaryBlock(FunctionDefinition const& _function, ContractDefinition const& _contract, PredicateType _type)
1328 {
1329 return createSymbolicBlock(
1330 functionSort(_function, &_contract, state()),
1331 "summary_" + uniquePrefix() + "_" + predicateName(&_function, &_contract),
1332 _type,
1333 &_function,
1334 &_contract
1335 );
1336 }
1337
createConstructorBlock(ContractDefinition const & _contract,string const & _prefix)1338 Predicate const* CHC::createConstructorBlock(ContractDefinition const& _contract, string const& _prefix)
1339 {
1340 return createSymbolicBlock(
1341 constructorSort(_contract, state()),
1342 _prefix + "_" + uniquePrefix() + "_" + contractSuffix(_contract),
1343 PredicateType::ConstructorSummary,
1344 &_contract,
1345 &_contract
1346 );
1347 }
1348
createErrorBlock()1349 void CHC::createErrorBlock()
1350 {
1351 m_errorPredicate = createSymbolicBlock(
1352 arity0FunctionSort(),
1353 "error_target_" + to_string(m_context.newUniqueId()),
1354 PredicateType::Error
1355 );
1356 m_interface->registerRelation(m_errorPredicate->functor());
1357 }
1358
connectBlocks(smtutil::Expression const & _from,smtutil::Expression const & _to,smtutil::Expression const & _constraints)1359 void CHC::connectBlocks(smtutil::Expression const& _from, smtutil::Expression const& _to, smtutil::Expression const& _constraints)
1360 {
1361 smtutil::Expression edge = smtutil::Expression::implies(
1362 _from && m_context.assertions() && _constraints,
1363 _to
1364 );
1365 addRule(edge, _from.name + "_to_" + _to.name);
1366 }
1367
initialConstraints(ContractDefinition const & _contract,FunctionDefinition const * _function)1368 smtutil::Expression CHC::initialConstraints(ContractDefinition const& _contract, FunctionDefinition const* _function)
1369 {
1370 smtutil::Expression conj = state().state() == state().state(0);
1371 conj = conj && errorFlag().currentValue() == 0;
1372 conj = conj && currentEqualInitialVarsConstraints(stateVariablesIncludingInheritedAndPrivate(_contract));
1373
1374 FunctionDefinition const* function = _function ? _function : _contract.constructor();
1375 if (function)
1376 conj = conj && currentEqualInitialVarsConstraints(applyMap(function->parameters(), [](auto&& _var) -> VariableDeclaration const* { return _var.get(); }));
1377
1378 return conj;
1379 }
1380
initialStateVariables()1381 vector<smtutil::Expression> CHC::initialStateVariables()
1382 {
1383 return stateVariablesAtIndex(0);
1384 }
1385
stateVariablesAtIndex(unsigned _index)1386 vector<smtutil::Expression> CHC::stateVariablesAtIndex(unsigned _index)
1387 {
1388 solAssert(m_currentContract, "");
1389 return stateVariablesAtIndex(_index, *m_currentContract);
1390 }
1391
stateVariablesAtIndex(unsigned _index,ContractDefinition const & _contract)1392 vector<smtutil::Expression> CHC::stateVariablesAtIndex(unsigned _index, ContractDefinition const& _contract)
1393 {
1394 return applyMap(
1395 SMTEncoder::stateVariablesIncludingInheritedAndPrivate(_contract),
1396 [&](auto _var) { return valueAtIndex(*_var, _index); }
1397 );
1398 }
1399
currentStateVariables()1400 vector<smtutil::Expression> CHC::currentStateVariables()
1401 {
1402 solAssert(m_currentContract, "");
1403 return currentStateVariables(*m_currentContract);
1404 }
1405
currentStateVariables(ContractDefinition const & _contract)1406 vector<smtutil::Expression> CHC::currentStateVariables(ContractDefinition const& _contract)
1407 {
1408 return applyMap(SMTEncoder::stateVariablesIncludingInheritedAndPrivate(_contract), [this](auto _var) { return currentValue(*_var); });
1409 }
1410
currentEqualInitialVarsConstraints(vector<VariableDeclaration const * > const & _vars) const1411 smtutil::Expression CHC::currentEqualInitialVarsConstraints(vector<VariableDeclaration const*> const& _vars) const
1412 {
1413 return fold(_vars, smtutil::Expression(true), [this](auto&& _conj, auto _var) {
1414 return move(_conj) && currentValue(*_var) == m_context.variable(*_var)->valueAtIndex(0);
1415 });
1416 }
1417
predicateName(ASTNode const * _node,ContractDefinition const * _contract)1418 string CHC::predicateName(ASTNode const* _node, ContractDefinition const* _contract)
1419 {
1420 string prefix;
1421 if (auto funDef = dynamic_cast<FunctionDefinition const*>(_node))
1422 {
1423 prefix += TokenTraits::toString(funDef->kind());
1424 if (!funDef->name().empty())
1425 prefix += "_" + funDef->name() + "_";
1426 }
1427 else if (m_currentFunction && !m_currentFunction->name().empty())
1428 prefix += m_currentFunction->name();
1429
1430 auto contract = _contract ? _contract : m_currentContract;
1431 solAssert(contract, "");
1432 return prefix + "_" + to_string(_node->id()) + "_" + to_string(contract->id());
1433 }
1434
predicate(Predicate const & _block)1435 smtutil::Expression CHC::predicate(Predicate const& _block)
1436 {
1437 switch (_block.type())
1438 {
1439 case PredicateType::Interface:
1440 solAssert(m_currentContract, "");
1441 return ::interface(_block, *m_currentContract, m_context);
1442 case PredicateType::ConstructorSummary:
1443 return constructor(_block, m_context);
1444 case PredicateType::FunctionSummary:
1445 case PredicateType::InternalCall:
1446 case PredicateType::ExternalCallTrusted:
1447 case PredicateType::ExternalCallUntrusted:
1448 return smt::function(_block, m_currentContract, m_context);
1449 case PredicateType::FunctionBlock:
1450 case PredicateType::FunctionErrorBlock:
1451 solAssert(m_currentFunction, "");
1452 return functionBlock(_block, *m_currentFunction, m_currentContract, m_context);
1453 case PredicateType::Error:
1454 return _block({});
1455 case PredicateType::NondetInterface:
1456 // Nondeterministic interface predicates are handled differently.
1457 solAssert(false, "");
1458 case PredicateType::Custom:
1459 // Custom rules are handled separately.
1460 solAssert(false, "");
1461 }
1462 solAssert(false, "");
1463 }
1464
predicate(FunctionCall const & _funCall)1465 smtutil::Expression CHC::predicate(FunctionCall const& _funCall)
1466 {
1467 FunctionType const& funType = dynamic_cast<FunctionType const&>(*_funCall.expression().annotation().type);
1468 auto kind = funType.kind();
1469 solAssert(kind == FunctionType::Kind::Internal || kind == FunctionType::Kind::External || kind == FunctionType::Kind::BareStaticCall, "");
1470
1471 solAssert(m_currentContract, "");
1472 auto function = functionCallToDefinition(_funCall, currentScopeContract(), m_currentContract);
1473 if (!function)
1474 return smtutil::Expression(true);
1475
1476 auto contractAddressValue = [this](FunctionCall const& _f) {
1477 auto [callExpr, callOptions] = functionCallExpression(_f);
1478
1479 FunctionType const& funType = dynamic_cast<FunctionType const&>(*callExpr->annotation().type);
1480 if (funType.kind() == FunctionType::Kind::Internal)
1481 return state().thisAddress();
1482 if (MemberAccess const* callBase = dynamic_cast<MemberAccess const*>(callExpr))
1483 return expr(callBase->expression());
1484 solAssert(false, "Unreachable!");
1485 };
1486 errorFlag().increaseIndex();
1487 vector<smtutil::Expression> args{errorFlag().currentValue(), contractAddressValue(_funCall), state().abi(), state().crypto(), state().tx(), state().state()};
1488
1489 auto const* contract = function->annotation().contract;
1490 auto const& hierarchy = m_currentContract->annotation().linearizedBaseContracts;
1491 solAssert(kind != FunctionType::Kind::Internal || function->isFree() || (contract && contract->isLibrary()) || contains(hierarchy, contract), "");
1492
1493 bool usesStaticCall = function->stateMutability() == StateMutability::Pure || function->stateMutability() == StateMutability::View;
1494
1495 args += currentStateVariables(*m_currentContract);
1496 args += symbolicArguments(_funCall, m_currentContract);
1497 if (!m_currentContract->isLibrary() && !usesStaticCall)
1498 {
1499 state().newState();
1500 for (auto const& var: m_stateVariables)
1501 m_context.variable(*var)->increaseIndex();
1502 }
1503 args += vector<smtutil::Expression>{state().state()};
1504 args += currentStateVariables(*m_currentContract);
1505
1506 for (auto var: function->parameters() + function->returnParameters())
1507 {
1508 if (m_context.knownVariable(*var))
1509 m_context.variable(*var)->increaseIndex();
1510 else
1511 createVariable(*var);
1512 args.push_back(currentValue(*var));
1513 }
1514
1515 Predicate const& summary = *m_summaries.at(m_currentContract).at(function);
1516 auto from = smt::function(summary, m_currentContract, m_context);
1517 Predicate const& callPredicate = *createSummaryBlock(
1518 *function,
1519 *m_currentContract,
1520 kind == FunctionType::Kind::Internal ? PredicateType::InternalCall : PredicateType::ExternalCallTrusted
1521 );
1522 auto to = smt::function(callPredicate, m_currentContract, m_context);
1523 addRule(smtutil::Expression::implies(from, to), to.name);
1524
1525 return callPredicate(args);
1526 }
1527
addRule(smtutil::Expression const & _rule,string const & _ruleName)1528 void CHC::addRule(smtutil::Expression const& _rule, string const& _ruleName)
1529 {
1530 m_interface->addRule(_rule, _ruleName);
1531 }
1532
query(smtutil::Expression const & _query,langutil::SourceLocation const & _location)1533 tuple<CheckResult, smtutil::Expression, CHCSolverInterface::CexGraph> CHC::query(smtutil::Expression const& _query, langutil::SourceLocation const& _location)
1534 {
1535 CheckResult result;
1536 smtutil::Expression invariant(true);
1537 CHCSolverInterface::CexGraph cex;
1538 tie(result, invariant, cex) = m_interface->query(_query);
1539 switch (result)
1540 {
1541 case CheckResult::SATISFIABLE:
1542 {
1543 #ifdef HAVE_Z3
1544 if (m_settings.solvers.z3)
1545 {
1546 // Even though the problem is SAT, Spacer's pre processing makes counterexamples incomplete.
1547 // We now disable those optimizations and check whether we can still solve the problem.
1548 auto* spacer = dynamic_cast<Z3CHCInterface*>(m_interface.get());
1549 solAssert(spacer, "");
1550 spacer->setSpacerOptions(false);
1551
1552 CheckResult resultNoOpt;
1553 smtutil::Expression invariantNoOpt(true);
1554 CHCSolverInterface::CexGraph cexNoOpt;
1555 tie(resultNoOpt, invariantNoOpt, cexNoOpt) = m_interface->query(_query);
1556
1557 if (resultNoOpt == CheckResult::SATISFIABLE)
1558 cex = move(cexNoOpt);
1559
1560 spacer->setSpacerOptions(true);
1561 }
1562 #endif
1563 break;
1564 }
1565 case CheckResult::UNSATISFIABLE:
1566 break;
1567 case CheckResult::UNKNOWN:
1568 break;
1569 case CheckResult::CONFLICTING:
1570 m_errorReporter.warning(1988_error, _location, "CHC: At least two SMT solvers provided conflicting answers. Results might not be sound.");
1571 break;
1572 case CheckResult::ERROR:
1573 m_errorReporter.warning(1218_error, _location, "CHC: Error trying to invoke SMT solver.");
1574 break;
1575 }
1576 return {result, invariant, cex};
1577 }
1578
verificationTargetEncountered(ASTNode const * const _errorNode,VerificationTargetType _type,smtutil::Expression const & _errorCondition)1579 void CHC::verificationTargetEncountered(
1580 ASTNode const* const _errorNode,
1581 VerificationTargetType _type,
1582 smtutil::Expression const& _errorCondition
1583 )
1584 {
1585 if (!m_settings.targets.has(_type))
1586 return;
1587
1588 if (!(m_currentContract || m_currentFunction))
1589 return;
1590
1591 bool scopeIsFunction = m_currentFunction && !m_currentFunction->isConstructor();
1592 auto errorId = newErrorId();
1593 solAssert(m_verificationTargets.count(errorId) == 0, "Error ID is not unique!");
1594 m_verificationTargets.emplace(errorId, CHCVerificationTarget{{_type, _errorCondition, smtutil::Expression(true)}, errorId, _errorNode});
1595 if (scopeIsFunction)
1596 m_functionTargetIds[m_currentFunction].push_back(errorId);
1597 else
1598 m_functionTargetIds[m_currentContract].push_back(errorId);
1599 auto previousError = errorFlag().currentValue();
1600 errorFlag().increaseIndex();
1601
1602 Predicate const* localBlock = m_currentFunction ?
1603 createBlock(m_currentFunction, PredicateType::FunctionErrorBlock) :
1604 createConstructorBlock(*m_currentContract, "local_error");
1605
1606 auto pred = predicate(*localBlock);
1607 connectBlocks(
1608 m_currentBlock,
1609 pred,
1610 _errorCondition && errorFlag().currentValue() == errorId
1611 );
1612 solAssert(m_errorDest, "");
1613 addRule(smtutil::Expression::implies(pred, predicate(*m_errorDest)), pred.name);
1614
1615 m_context.addAssertion(errorFlag().currentValue() == previousError);
1616 }
1617
checkVerificationTargets()1618 void CHC::checkVerificationTargets()
1619 {
1620 // The verification conditions have been collected per function where they have been encountered (m_verificationTargets).
1621 // Also, all possible contexts in which an external function can be called has been recorded (m_queryPlaceholders).
1622 // Here we combine every context in which an external function can be called with all possible verification conditions
1623 // in its call graph. Each such combination forms a unique verification target.
1624 map<unsigned, vector<CHCQueryPlaceholder>> targetEntryPoints;
1625 for (auto const& [function, placeholders]: m_queryPlaceholders)
1626 {
1627 auto functionTargets = transactionVerificationTargetsIds(function);
1628 for (auto const& placeholder: placeholders)
1629 for (unsigned id: functionTargets)
1630 targetEntryPoints[id].push_back(placeholder);
1631 }
1632
1633 set<unsigned> checkedErrorIds;
1634 for (auto const& [targetId, placeholders]: targetEntryPoints)
1635 {
1636 string errorType;
1637 ErrorId errorReporterId;
1638
1639 auto const& target = m_verificationTargets.at(targetId);
1640
1641 if (target.type == VerificationTargetType::PopEmptyArray)
1642 {
1643 solAssert(dynamic_cast<FunctionCall const*>(target.errorNode), "");
1644 errorType = "Empty array \"pop\"";
1645 errorReporterId = 2529_error;
1646 }
1647 else if (target.type == VerificationTargetType::OutOfBounds)
1648 {
1649 solAssert(dynamic_cast<IndexAccess const*>(target.errorNode), "");
1650 errorType = "Out of bounds access";
1651 errorReporterId = 6368_error;
1652 }
1653 else if (
1654 target.type == VerificationTargetType::Underflow ||
1655 target.type == VerificationTargetType::Overflow
1656 )
1657 {
1658 auto const* expr = dynamic_cast<Expression const*>(target.errorNode);
1659 solAssert(expr, "");
1660 auto const* intType = dynamic_cast<IntegerType const*>(expr->annotation().type);
1661 if (!intType)
1662 intType = TypeProvider::uint256();
1663
1664 if (target.type == VerificationTargetType::Underflow)
1665 {
1666 errorType = "Underflow (resulting value less than " + formatNumberReadable(intType->minValue()) + ")";
1667 errorReporterId = 3944_error;
1668 }
1669 else if (target.type == VerificationTargetType::Overflow)
1670 {
1671 errorType = "Overflow (resulting value larger than " + formatNumberReadable(intType->maxValue()) + ")";
1672 errorReporterId = 4984_error;
1673 }
1674 }
1675 else if (target.type == VerificationTargetType::DivByZero)
1676 {
1677 errorType = "Division by zero";
1678 errorReporterId = 4281_error;
1679 }
1680 else if (target.type == VerificationTargetType::Assert)
1681 {
1682 errorType = "Assertion violation";
1683 errorReporterId = 6328_error;
1684 }
1685 else
1686 solAssert(false, "");
1687
1688 checkAndReportTarget(target, placeholders, errorReporterId, errorType + " happens here.", errorType + " might happen here.");
1689 checkedErrorIds.insert(target.errorId);
1690 }
1691
1692 auto toReport = m_unsafeTargets;
1693 if (m_settings.showUnproved)
1694 for (auto const& [node, targets]: m_unprovedTargets)
1695 for (auto const& [target, info]: targets)
1696 toReport[node].emplace(target, info);
1697
1698 for (auto const& [node, targets]: toReport)
1699 for (auto const& [target, info]: targets)
1700 m_errorReporter.warning(
1701 info.error,
1702 info.location,
1703 info.message
1704 );
1705
1706 if (!m_settings.showUnproved && !m_unprovedTargets.empty())
1707 m_errorReporter.warning(
1708 5840_error,
1709 {},
1710 "CHC: " +
1711 to_string(m_unprovedTargets.size()) +
1712 " verification condition(s) could not be proved." +
1713 " Enable the model checker option \"show unproved\" to see all of them." +
1714 " Consider choosing a specific contract to be verified in order to reduce the solving problems." +
1715 " Consider increasing the timeout per query."
1716 );
1717
1718 if (!m_settings.invariants.invariants.empty())
1719 {
1720 string msg;
1721 for (auto pred: m_invariants | ranges::views::keys)
1722 {
1723 ASTNode const* node = pred->programNode();
1724 string what;
1725 if (auto contract = dynamic_cast<ContractDefinition const*>(node))
1726 what = contract->fullyQualifiedName();
1727 else
1728 solAssert(false, "");
1729
1730 string invType;
1731 if (pred->type() == PredicateType::Interface)
1732 invType = "Contract invariant(s)";
1733 else if (pred->type() == PredicateType::NondetInterface)
1734 invType = "Reentrancy property(ies)";
1735 else
1736 solAssert(false, "");
1737
1738 msg += invType + " for " + what + ":\n";
1739 for (auto const& inv: m_invariants.at(pred))
1740 msg += inv + "\n";
1741 }
1742 if (msg.find("<errorCode>") != string::npos)
1743 {
1744 set<unsigned> seenErrors;
1745 msg += "<errorCode> = 0 -> no errors\n";
1746 for (auto const& [id, target]: m_verificationTargets)
1747 if (!seenErrors.count(target.errorId))
1748 {
1749 seenErrors.insert(target.errorId);
1750 string loc = string(m_charStreamProvider.charStream(*target.errorNode->location().sourceName).text(target.errorNode->location()));
1751 msg += "<errorCode> = " + to_string(target.errorId) + " -> " + ModelCheckerTargets::targetTypeToString.at(target.type) + " at " + loc + "\n";
1752
1753 }
1754 }
1755 if (!msg.empty())
1756 m_errorReporter.info(1180_error, msg);
1757 }
1758
1759 // There can be targets in internal functions that are not reachable from the external interface.
1760 // These are safe by definition and are not even checked by the CHC engine, but this information
1761 // must still be reported safe by the BMC engine.
1762 set<unsigned> allErrorIds;
1763 for (auto const& entry: m_functionTargetIds)
1764 for (unsigned id: entry.second)
1765 allErrorIds.insert(id);
1766
1767 set<unsigned> unreachableErrorIds;
1768 set_difference(
1769 allErrorIds.begin(),
1770 allErrorIds.end(),
1771 checkedErrorIds.begin(),
1772 checkedErrorIds.end(),
1773 inserter(unreachableErrorIds, unreachableErrorIds.begin())
1774 );
1775 for (auto id: unreachableErrorIds)
1776 m_safeTargets[m_verificationTargets.at(id).errorNode].insert(m_verificationTargets.at(id).type);
1777 }
1778
checkAndReportTarget(CHCVerificationTarget const & _target,vector<CHCQueryPlaceholder> const & _placeholders,ErrorId _errorReporterId,string _satMsg,string _unknownMsg)1779 void CHC::checkAndReportTarget(
1780 CHCVerificationTarget const& _target,
1781 vector<CHCQueryPlaceholder> const& _placeholders,
1782 ErrorId _errorReporterId,
1783 string _satMsg,
1784 string _unknownMsg
1785 )
1786 {
1787 if (m_unsafeTargets.count(_target.errorNode) && m_unsafeTargets.at(_target.errorNode).count(_target.type))
1788 return;
1789
1790 createErrorBlock();
1791 for (auto const& placeholder: _placeholders)
1792 connectBlocks(
1793 placeholder.fromPredicate,
1794 error(),
1795 placeholder.constraints && placeholder.errorExpression == _target.errorId
1796 );
1797 auto const& location = _target.errorNode->location();
1798 auto [result, invariant, model] = query(error(), location);
1799 if (result == CheckResult::UNSATISFIABLE)
1800 {
1801 m_safeTargets[_target.errorNode].insert(_target.type);
1802 set<Predicate const*> predicates;
1803 for (auto const* pred: m_interfaces | ranges::views::values)
1804 predicates.insert(pred);
1805 for (auto const* pred: m_nondetInterfaces | ranges::views::values)
1806 predicates.insert(pred);
1807 map<Predicate const*, set<string>> invariants = collectInvariants(invariant, predicates, m_settings.invariants);
1808 for (auto pred: invariants | ranges::views::keys)
1809 m_invariants[pred] += move(invariants.at(pred));
1810 }
1811 else if (result == CheckResult::SATISFIABLE)
1812 {
1813 solAssert(!_satMsg.empty(), "");
1814 auto cex = generateCounterexample(model, error().name);
1815 if (cex)
1816 m_unsafeTargets[_target.errorNode][_target.type] = {
1817 _errorReporterId,
1818 location,
1819 "CHC: " + _satMsg + "\nCounterexample:\n" + *cex
1820 };
1821 else
1822 m_unsafeTargets[_target.errorNode][_target.type] = {
1823 _errorReporterId,
1824 location,
1825 "CHC: " + _satMsg
1826 };
1827 }
1828 else if (!_unknownMsg.empty())
1829 m_unprovedTargets[_target.errorNode][_target.type] = {
1830 _errorReporterId,
1831 location,
1832 "CHC: " + _unknownMsg
1833 };
1834 }
1835
1836 /**
1837 The counterexample DAG has the following properties:
1838 1) The root node represents the reachable error predicate.
1839 2) The root node has 1 or 2 children:
1840 - One of them is the summary of the function that was called and led to that node.
1841 If this is the only child, this function must be the constructor.
1842 - If it has 2 children, the function is not the constructor and the other child is the interface node,
1843 that is, it represents the state of the contract before the function described above was called.
1844 3) Interface nodes also have property 2.
1845
1846 We run a BFS on the DAG from the root node collecting the reachable function summaries from the given node.
1847 When a function summary is seen, the search continues with that summary as the new root for its subgraph.
1848 The result of the search is a callgraph containing:
1849 - Functions calls needed to reach the root node, that is, transaction entry points.
1850 - Functions called by other functions (internal calls or external calls/internal transactions).
1851 The BFS visit order and the shape of the DAG described in the previous paragraph guarantee that the order of
1852 the function summaries in the callgraph of the error node is the reverse transaction trace.
1853
1854 The first function summary seen contains the values for the state, input and output variables at the
1855 error point.
1856 */
generateCounterexample(CHCSolverInterface::CexGraph const & _graph,string const & _root)1857 optional<string> CHC::generateCounterexample(CHCSolverInterface::CexGraph const& _graph, string const& _root)
1858 {
1859 optional<unsigned> rootId;
1860 for (auto const& [id, node]: _graph.nodes)
1861 if (node.name == _root)
1862 {
1863 rootId = id;
1864 break;
1865 }
1866 if (!rootId)
1867 return {};
1868
1869 vector<string> path;
1870 string localState;
1871
1872 auto callGraph = summaryCalls(_graph, *rootId);
1873
1874 auto nodePred = [&](auto _node) { return Predicate::predicate(_graph.nodes.at(_node).name); };
1875 auto nodeArgs = [&](auto _node) { return _graph.nodes.at(_node).arguments; };
1876
1877 bool first = true;
1878 for (auto summaryId: callGraph.at(*rootId))
1879 {
1880 CHCSolverInterface::CexNode const& summaryNode = _graph.nodes.at(summaryId);
1881 Predicate const* summaryPredicate = Predicate::predicate(summaryNode.name);
1882 auto const& summaryArgs = summaryNode.arguments;
1883
1884 auto stateVars = summaryPredicate->stateVariables();
1885 solAssert(stateVars.has_value(), "");
1886 auto stateValues = summaryPredicate->summaryStateValues(summaryArgs);
1887 solAssert(stateValues.size() == stateVars->size(), "");
1888
1889 if (first)
1890 {
1891 first = false;
1892 /// Generate counterexample message local to the failed target.
1893 localState = formatVariableModel(*stateVars, stateValues, ", ") + "\n";
1894
1895 if (auto calledFun = summaryPredicate->programFunction())
1896 {
1897 auto inValues = summaryPredicate->summaryPostInputValues(summaryArgs);
1898 auto const& inParams = calledFun->parameters();
1899 if (auto inStr = formatVariableModel(inParams, inValues, "\n"); !inStr.empty())
1900 localState += inStr + "\n";
1901 auto outValues = summaryPredicate->summaryPostOutputValues(summaryArgs);
1902 auto const& outParams = calledFun->returnParameters();
1903 if (auto outStr = formatVariableModel(outParams, outValues, "\n"); !outStr.empty())
1904 localState += outStr + "\n";
1905
1906 optional<unsigned> localErrorId;
1907 solidity::util::BreadthFirstSearch<unsigned> bfs{{summaryId}};
1908 bfs.run([&](auto _nodeId, auto&& _addChild) {
1909 auto const& children = _graph.edges.at(_nodeId);
1910 if (
1911 children.size() == 1 &&
1912 nodePred(children.front())->isFunctionErrorBlock()
1913 )
1914 {
1915 localErrorId = children.front();
1916 bfs.abort();
1917 }
1918 ranges::for_each(children, _addChild);
1919 });
1920
1921 if (localErrorId.has_value())
1922 {
1923 auto const* localError = nodePred(*localErrorId);
1924 solAssert(localError && localError->isFunctionErrorBlock(), "");
1925 auto const [localValues, localVars] = localError->localVariableValues(nodeArgs(*localErrorId));
1926 if (auto localStr = formatVariableModel(localVars, localValues, "\n"); !localStr.empty())
1927 localState += localStr + "\n";
1928 }
1929 }
1930 }
1931 else
1932 {
1933 auto modelMsg = formatVariableModel(*stateVars, stateValues, ", ");
1934 /// We report the state after every tx in the trace except for the last, which is reported
1935 /// first in the code above.
1936 if (!modelMsg.empty())
1937 path.emplace_back("State: " + modelMsg);
1938 }
1939
1940 string txCex = summaryPredicate->formatSummaryCall(summaryArgs, m_charStreamProvider);
1941
1942 list<string> calls;
1943 auto dfs = [&](unsigned parent, unsigned node, unsigned depth, auto&& _dfs) -> void {
1944 auto pred = nodePred(node);
1945 auto parentPred = nodePred(parent);
1946 solAssert(pred && pred->isSummary(), "");
1947 solAssert(parentPred && parentPred->isSummary(), "");
1948 auto callTraceSize = calls.size();
1949 if (!pred->isConstructorSummary())
1950 for (unsigned v: callGraph[node])
1951 _dfs(node, v, depth + 1, _dfs);
1952
1953 bool appendTxVars = pred->isConstructorSummary() || pred->isFunctionSummary() || pred->isExternalCallUntrusted();
1954
1955 calls.push_front(string(depth * 4, ' ') + pred->formatSummaryCall(nodeArgs(node), m_charStreamProvider, appendTxVars));
1956 if (pred->isInternalCall())
1957 calls.front() += " -- internal call";
1958 else if (pred->isExternalCallTrusted())
1959 calls.front() += " -- trusted external call";
1960 else if (pred->isExternalCallUntrusted())
1961 {
1962 calls.front() += " -- untrusted external call";
1963 if (calls.size() > callTraceSize + 1)
1964 calls.front() += ", synthesized as:";
1965 }
1966 else if (pred->isFunctionSummary() && parentPred->isExternalCallUntrusted())
1967 calls.front() += " -- reentrant call";
1968 };
1969 dfs(summaryId, summaryId, 0, dfs);
1970 path.emplace_back(boost::algorithm::join(calls, "\n"));
1971 }
1972
1973 return localState + "\nTransaction trace:\n" + boost::algorithm::join(path | ranges::views::reverse, "\n");
1974 }
1975
summaryCalls(CHCSolverInterface::CexGraph const & _graph,unsigned _root)1976 map<unsigned, vector<unsigned>> CHC::summaryCalls(CHCSolverInterface::CexGraph const& _graph, unsigned _root)
1977 {
1978 map<unsigned, vector<unsigned>> calls;
1979
1980 auto compare = [&](unsigned _a, unsigned _b) {
1981 auto extract = [&](string const& _s) {
1982 // We want to sort sibling predicates in the counterexample graph by their unique predicate id.
1983 // For most predicates, this actually doesn't matter.
1984 // The cases where this matters are internal and external function calls which have the form:
1985 // summary_<CALLID>_<suffix>
1986 // nondet_call_<CALLID>_<suffix>
1987 // Those have the extra unique <CALLID> numbers based on the traversal order, and are necessary
1988 // to infer the call order so that's shown property in the counterexample trace.
1989 // Predicates that do not have a CALLID have a predicate id at the end of <suffix>,
1990 // so the assertion below should still hold.
1991 auto beg = _s.data();
1992 while (beg != _s.data() + _s.size() && !isdigit(*beg)) ++beg;
1993 auto end = beg;
1994 while (end != _s.data() + _s.size() && isdigit(*end)) ++end;
1995
1996 solAssert(beg != end, "Expected to find numerical call or predicate id.");
1997
1998 int result;
1999 auto [p, ec] = std::from_chars(beg, end, result);
2000 solAssert(ec == std::errc(), "Id should be a number.");
2001
2002 return result;
2003 };
2004 return extract(_graph.nodes.at(_a).name) > extract(_graph.nodes.at(_b).name);
2005 };
2006
2007 queue<pair<unsigned, unsigned>> q;
2008 q.push({_root, _root});
2009 while (!q.empty())
2010 {
2011 auto [node, root] = q.front();
2012 q.pop();
2013
2014 Predicate const* nodePred = Predicate::predicate(_graph.nodes.at(node).name);
2015 Predicate const* rootPred = Predicate::predicate(_graph.nodes.at(root).name);
2016 if (nodePred->isSummary() && (
2017 _root == root ||
2018 nodePred->isInternalCall() ||
2019 nodePred->isExternalCallTrusted() ||
2020 nodePred->isExternalCallUntrusted() ||
2021 rootPred->isExternalCallUntrusted()
2022 ))
2023 {
2024 calls[root].push_back(node);
2025 root = node;
2026 }
2027 auto const& edges = _graph.edges.at(node);
2028 for (unsigned v: set<unsigned, decltype(compare)>(begin(edges), end(edges), compare))
2029 q.push({v, root});
2030 }
2031
2032 return calls;
2033 }
2034
cex2dot(CHCSolverInterface::CexGraph const & _cex)2035 string CHC::cex2dot(CHCSolverInterface::CexGraph const& _cex)
2036 {
2037 string dot = "digraph {\n";
2038
2039 auto pred = [&](CHCSolverInterface::CexNode const& _node) {
2040 vector<string> args = applyMap(
2041 _node.arguments,
2042 [&](auto const& arg) { return arg.name; }
2043 );
2044 return "\"" + _node.name + "(" + boost::algorithm::join(args, ", ") + ")\"";
2045 };
2046
2047 for (auto const& [u, vs]: _cex.edges)
2048 for (auto v: vs)
2049 dot += pred(_cex.nodes.at(v)) + " -> " + pred(_cex.nodes.at(u)) + "\n";
2050
2051 dot += "}";
2052 return dot;
2053 }
2054
uniquePrefix()2055 string CHC::uniquePrefix()
2056 {
2057 return to_string(m_blockCounter++);
2058 }
2059
contractSuffix(ContractDefinition const & _contract)2060 string CHC::contractSuffix(ContractDefinition const& _contract)
2061 {
2062 return _contract.name() + "_" + to_string(_contract.id());
2063 }
2064
newErrorId()2065 unsigned CHC::newErrorId()
2066 {
2067 unsigned errorId = m_context.newUniqueId();
2068 // We need to make sure the error id is not zero,
2069 // because error id zero actually means no error in the CHC encoding.
2070 if (errorId == 0)
2071 errorId = m_context.newUniqueId();
2072 return errorId;
2073 }
2074
errorFlag()2075 SymbolicIntVariable& CHC::errorFlag()
2076 {
2077 return state().errorFlag();
2078 }
2079