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/ModelCheckerSettings.h>
20
21 #include <optional>
22 #include <range/v3/view.hpp>
23
24 using namespace std;
25 using namespace solidity;
26 using namespace solidity::frontend;
27
28 map<string, InvariantType> const ModelCheckerInvariants::validInvariants{
29 {"contract", InvariantType::Contract},
30 {"reentrancy", InvariantType::Reentrancy}
31 };
32
fromString(string const & _invs)33 std::optional<ModelCheckerInvariants> ModelCheckerInvariants::fromString(string const& _invs)
34 {
35 set<InvariantType> chosenInvs;
36 if (_invs == "default")
37 {
38 // The default is that no invariants are reported.
39 }
40 else if (_invs == "all")
41 for (auto&& v: validInvariants | ranges::views::values)
42 chosenInvs.insert(v);
43 else
44 for (auto&& t: _invs | ranges::views::split(',') | ranges::to<vector<string>>())
45 {
46 if (!validInvariants.count(t))
47 return {};
48 chosenInvs.insert(validInvariants.at(t));
49 }
50
51 return ModelCheckerInvariants{chosenInvs};
52 }
53
setFromString(string const & _inv)54 bool ModelCheckerInvariants::setFromString(string const& _inv)
55 {
56 if (!validInvariants.count(_inv))
57 return false;
58 invariants.insert(validInvariants.at(_inv));
59 return true;
60 }
61
62 using TargetType = VerificationTargetType;
63 map<string, TargetType> const ModelCheckerTargets::targetStrings{
64 {"constantCondition", TargetType::ConstantCondition},
65 {"underflow", TargetType::Underflow},
66 {"overflow", TargetType::Overflow},
67 {"divByZero", TargetType::DivByZero},
68 {"balance", TargetType::Balance},
69 {"assert", TargetType::Assert},
70 {"popEmptyArray", TargetType::PopEmptyArray},
71 {"outOfBounds", TargetType::OutOfBounds}
72 };
73
74 map<TargetType, string> const ModelCheckerTargets::targetTypeToString{
75 {TargetType::ConstantCondition, "Constant condition"},
76 {TargetType::Underflow, "Underflow"},
77 {TargetType::Overflow, "Overflow"},
78 {TargetType::DivByZero, "Division by zero"},
79 {TargetType::Balance, "Insufficient balance"},
80 {TargetType::Assert, "Assertion failed"},
81 {TargetType::PopEmptyArray, "Empty array pop"},
82 {TargetType::OutOfBounds, "Out of bounds access"}
83 };
84
fromString(string const & _targets)85 std::optional<ModelCheckerTargets> ModelCheckerTargets::fromString(string const& _targets)
86 {
87 set<TargetType> chosenTargets;
88 if (_targets == "default" || _targets == "all")
89 {
90 bool all = _targets == "all";
91 for (auto&& v: targetStrings | ranges::views::values)
92 {
93 if (!all && (v == TargetType::Underflow || v == TargetType::Overflow))
94 continue;
95 chosenTargets.insert(v);
96 }
97 }
98 else
99 for (auto&& t: _targets | ranges::views::split(',') | ranges::to<vector<string>>())
100 {
101 if (!targetStrings.count(t))
102 return {};
103 chosenTargets.insert(targetStrings.at(t));
104 }
105
106 return ModelCheckerTargets{chosenTargets};
107 }
108
setFromString(string const & _target)109 bool ModelCheckerTargets::setFromString(string const& _target)
110 {
111 if (!targetStrings.count(_target))
112 return false;
113 targets.insert(targetStrings.at(_target));
114 return true;
115 }
116
fromString(string const & _contracts)117 std::optional<ModelCheckerContracts> ModelCheckerContracts::fromString(string const& _contracts)
118 {
119 map<string, set<string>> chosen;
120 if (_contracts == "default")
121 return ModelCheckerContracts::Default();
122
123 for (auto&& sourceContract: _contracts | ranges::views::split(',') | ranges::to<vector<string>>())
124 {
125 auto&& names = sourceContract | ranges::views::split(':') | ranges::to<vector<string>>();
126 if (names.size() != 2 || names.at(0).empty() || names.at(1).empty())
127 return {};
128 chosen[names.at(0)].insert(names.at(1));
129 }
130
131 return ModelCheckerContracts{chosen};
132 }
133