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/ModelChecker.h>
20 #ifdef HAVE_Z3
21 #include <libsmtutil/Z3Interface.h>
22 #endif
23
24 #include <range/v3/algorithm/any_of.hpp>
25 #include <range/v3/view.hpp>
26
27 using namespace std;
28 using namespace solidity;
29 using namespace solidity::util;
30 using namespace solidity::langutil;
31 using namespace solidity::frontend;
32
ModelChecker(ErrorReporter & _errorReporter,langutil::CharStreamProvider const & _charStreamProvider,map<h256,string> const & _smtlib2Responses,ModelCheckerSettings _settings,ReadCallback::Callback const & _smtCallback)33 ModelChecker::ModelChecker(
34 ErrorReporter& _errorReporter,
35 langutil::CharStreamProvider const& _charStreamProvider,
36 map<h256, string> const& _smtlib2Responses,
37 ModelCheckerSettings _settings,
38 ReadCallback::Callback const& _smtCallback
39 ):
40 m_errorReporter(_errorReporter),
41 m_settings(move(_settings)),
42 m_context(),
43 m_bmc(m_context, m_uniqueErrorReporter, _smtlib2Responses, _smtCallback, m_settings, _charStreamProvider),
44 m_chc(m_context, m_uniqueErrorReporter, _smtlib2Responses, _smtCallback, m_settings, _charStreamProvider)
45 {
46 }
47
48 // TODO This should be removed for 0.9.0.
enableAllEnginesIfPragmaPresent(vector<shared_ptr<SourceUnit>> const & _sources)49 void ModelChecker::enableAllEnginesIfPragmaPresent(vector<shared_ptr<SourceUnit>> const& _sources)
50 {
51 bool hasPragma = ranges::any_of(_sources, [](auto _source) {
52 return _source && _source->annotation().experimentalFeatures.count(ExperimentalFeature::SMTChecker);
53 });
54 if (hasPragma)
55 m_settings.engine = ModelCheckerEngine::All();
56 }
57
checkRequestedSourcesAndContracts(vector<shared_ptr<SourceUnit>> const & _sources)58 void ModelChecker::checkRequestedSourcesAndContracts(vector<shared_ptr<SourceUnit>> const& _sources)
59 {
60 map<string, set<string>> exist;
61 for (auto const& source: _sources)
62 for (auto node: source->nodes())
63 if (auto contract = dynamic_pointer_cast<ContractDefinition>(node))
64 exist[contract->sourceUnitName()].insert(contract->name());
65
66 // Requested sources
67 for (auto const& sourceName: m_settings.contracts.contracts | ranges::views::keys)
68 {
69 if (!exist.count(sourceName))
70 {
71 m_uniqueErrorReporter.warning(
72 9134_error,
73 SourceLocation(),
74 "Requested source \"" + sourceName + "\" does not exist."
75 );
76 continue;
77 }
78 auto const& source = exist.at(sourceName);
79 // Requested contracts in source `s`.
80 for (auto const& contract: m_settings.contracts.contracts.at(sourceName))
81 if (!source.count(contract))
82 m_uniqueErrorReporter.warning(
83 7400_error,
84 SourceLocation(),
85 "Requested contract \"" + contract + "\" does not exist in source \"" + sourceName + "\"."
86 );
87 }
88 }
89
analyze(SourceUnit const & _source)90 void ModelChecker::analyze(SourceUnit const& _source)
91 {
92 // TODO This should be removed for 0.9.0.
93 if (_source.annotation().experimentalFeatures.count(ExperimentalFeature::SMTChecker))
94 {
95 PragmaDirective const* smtPragma = nullptr;
96 for (auto node: _source.nodes())
97 if (auto pragma = dynamic_pointer_cast<PragmaDirective>(node))
98 if (
99 pragma->literals().size() >= 2 &&
100 pragma->literals().at(1) == "SMTChecker"
101 )
102 {
103 smtPragma = pragma.get();
104 break;
105 }
106 solAssert(smtPragma, "");
107 m_uniqueErrorReporter.warning(
108 5523_error,
109 smtPragma->location(),
110 "The SMTChecker pragma has been deprecated and will be removed in the future. "
111 "Please use the \"model checker engine\" compiler setting to activate the SMTChecker instead. "
112 "If the pragma is enabled, all engines will be used."
113 );
114 }
115
116 if (m_settings.engine.none())
117 return;
118
119 if (m_settings.engine.chc)
120 m_chc.analyze(_source);
121
122 auto solvedTargets = m_chc.safeTargets();
123 for (auto const& [node, targets]: m_chc.unsafeTargets())
124 solvedTargets[node] += targets | ranges::views::keys;
125
126 if (m_settings.engine.bmc)
127 m_bmc.analyze(_source, solvedTargets);
128
129 m_errorReporter.append(m_uniqueErrorReporter.errors());
130 m_uniqueErrorReporter.clear();
131 }
132
unhandledQueries()133 vector<string> ModelChecker::unhandledQueries()
134 {
135 return m_bmc.unhandledQueries() + m_chc.unhandledQueries();
136 }
137
availableSolvers()138 solidity::smtutil::SMTSolverChoice ModelChecker::availableSolvers()
139 {
140 smtutil::SMTSolverChoice available = smtutil::SMTSolverChoice::SMTLIB2();
141 #ifdef HAVE_Z3
142 available.z3 = solidity::smtutil::Z3Interface::available();
143 #endif
144 #ifdef HAVE_CVC4
145 available.cvc4 = true;
146 #endif
147 return available;
148 }
149