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 #pragma once 20 21 #include <libsmtutil/SolverInterface.h> 22 23 #include <optional> 24 #include <set> 25 26 namespace solidity::frontend 27 { 28 29 struct ModelCheckerContracts 30 { 31 /// By default all contracts are analyzed. DefaultModelCheckerContracts32 static ModelCheckerContracts Default() { return {}; } 33 34 /// Parses a string of the form <path>:<contract>,<path>:contract,... 35 /// and returns nullopt if a path or contract name is empty. 36 static std::optional<ModelCheckerContracts> fromString(std::string const& _contracts); 37 38 /// @returns true if all contracts should be analyzed. isDefaultModelCheckerContracts39 bool isDefault() const { return contracts.empty(); } 40 hasModelCheckerContracts41 bool has(std::string const& _source) const { return contracts.count(_source); } hasModelCheckerContracts42 bool has(std::string const& _source, std::string const& _contract) const 43 { 44 return has(_source) && contracts.at(_source).count(_contract); 45 } 46 47 bool operator!=(ModelCheckerContracts const& _other) const noexcept { return !(*this == _other); } 48 bool operator==(ModelCheckerContracts const& _other) const noexcept { return contracts == _other.contracts; } 49 50 /// Represents which contracts should be analyzed by the SMTChecker 51 /// as the most derived. 52 /// The key is the source file. If the map is empty, all sources must be analyzed. 53 /// For each source, contracts[source] represents the contracts in that source 54 /// that should be analyzed. 55 /// If the set of contracts is empty, all contracts in that source should be analyzed. 56 std::map<std::string, std::set<std::string>> contracts; 57 }; 58 59 struct ModelCheckerEngine 60 { 61 bool bmc = false; 62 bool chc = false; 63 AllModelCheckerEngine64 static constexpr ModelCheckerEngine All() { return {true, true}; } BMCModelCheckerEngine65 static constexpr ModelCheckerEngine BMC() { return {true, false}; } CHCModelCheckerEngine66 static constexpr ModelCheckerEngine CHC() { return {false, true}; } NoneModelCheckerEngine67 static constexpr ModelCheckerEngine None() { return {false, false}; } 68 noneModelCheckerEngine69 bool none() const { return !any(); } anyModelCheckerEngine70 bool any() const { return bmc || chc; } allModelCheckerEngine71 bool all() const { return bmc && chc; } 72 fromStringModelCheckerEngine73 static std::optional<ModelCheckerEngine> fromString(std::string const& _engine) 74 { 75 static std::map<std::string, ModelCheckerEngine> engineMap{ 76 {"all", All()}, 77 {"bmc", BMC()}, 78 {"chc", CHC()}, 79 {"none", None()} 80 }; 81 if (engineMap.count(_engine)) 82 return engineMap.at(_engine); 83 return {}; 84 } 85 86 bool operator!=(ModelCheckerEngine const& _other) const noexcept { return !(*this == _other); } 87 bool operator==(ModelCheckerEngine const& _other) const noexcept { return bmc == _other.bmc && chc == _other.chc; } 88 }; 89 90 enum class InvariantType { Contract, Reentrancy }; 91 92 struct ModelCheckerInvariants 93 { 94 /// Adds the default targets, that is, all except underflow and overflow. DefaultModelCheckerInvariants95 static ModelCheckerInvariants Default() { return *fromString("default"); } 96 /// Adds all targets, including underflow and overflow. AllModelCheckerInvariants97 static ModelCheckerInvariants All() { return *fromString("all"); } NoneModelCheckerInvariants98 static ModelCheckerInvariants None() { return {{}}; } 99 100 static std::optional<ModelCheckerInvariants> fromString(std::string const& _invs); 101 hasModelCheckerInvariants102 bool has(InvariantType _inv) const { return invariants.count(_inv); } 103 104 /// @returns true if the @p _target is valid, 105 /// and false otherwise. 106 bool setFromString(std::string const& _target); 107 108 static std::map<std::string, InvariantType> const validInvariants; 109 110 bool operator!=(ModelCheckerInvariants const& _other) const noexcept { return !(*this == _other); } 111 bool operator==(ModelCheckerInvariants const& _other) const noexcept { return invariants == _other.invariants; } 112 113 std::set<InvariantType> invariants; 114 }; 115 116 enum class VerificationTargetType { ConstantCondition, Underflow, Overflow, UnderOverflow, DivByZero, Balance, Assert, PopEmptyArray, OutOfBounds }; 117 118 struct ModelCheckerTargets 119 { 120 /// Adds the default targets, that is, all except underflow and overflow. DefaultModelCheckerTargets121 static ModelCheckerTargets Default() { return *fromString("default"); } 122 /// Adds all targets, including underflow and overflow. AllModelCheckerTargets123 static ModelCheckerTargets All() { return *fromString("all"); } 124 125 static std::optional<ModelCheckerTargets> fromString(std::string const& _targets); 126 hasModelCheckerTargets127 bool has(VerificationTargetType _type) const { return targets.count(_type); } 128 129 /// @returns true if the @p _target is valid, 130 /// and false otherwise. 131 bool setFromString(std::string const& _target); 132 133 static std::map<std::string, VerificationTargetType> const targetStrings; 134 135 static std::map<VerificationTargetType, std::string> const targetTypeToString; 136 137 bool operator!=(ModelCheckerTargets const& _other) const noexcept { return !(*this == _other); } 138 bool operator==(ModelCheckerTargets const& _other) const noexcept { return targets == _other.targets; } 139 140 std::set<VerificationTargetType> targets; 141 }; 142 143 struct ModelCheckerSettings 144 { 145 ModelCheckerContracts contracts = ModelCheckerContracts::Default(); 146 /// Currently division and modulo are replaced by multiplication with slack vars, such that 147 /// a / b <=> a = b * k + m 148 /// where k and m are slack variables. 149 /// This is the default because Spacer prefers that over precise / and mod. 150 /// This option allows disabling this mechanism since other solvers 151 /// might prefer the precise encoding. 152 bool divModNoSlacks = false; 153 ModelCheckerEngine engine = ModelCheckerEngine::None(); 154 ModelCheckerInvariants invariants = ModelCheckerInvariants::Default(); 155 bool showUnproved = false; 156 smtutil::SMTSolverChoice solvers = smtutil::SMTSolverChoice::All(); 157 ModelCheckerTargets targets = ModelCheckerTargets::Default(); 158 std::optional<unsigned> timeout; 159 160 bool operator!=(ModelCheckerSettings const& _other) const noexcept { return !(*this == _other); } 161 bool operator==(ModelCheckerSettings const& _other) const noexcept 162 { 163 return 164 contracts == _other.contracts && 165 divModNoSlacks == _other.divModNoSlacks && 166 engine == _other.engine && 167 invariants == _other.invariants && 168 showUnproved == _other.showUnproved && 169 solvers == _other.solvers && 170 targets == _other.targets && 171 timeout == _other.timeout; 172 } 173 }; 174 175 } 176