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 <libsolidity/formal/SSAVariable.h> 22 #include <libsolidity/ast/Types.h> 23 #include <libsolidity/ast/TypeProvider.h> 24 25 #include <libsmtutil/SolverInterface.h> 26 27 #include <map> 28 #include <memory> 29 30 namespace solidity::frontend::smt 31 { 32 33 class EncodingContext; 34 class Type; 35 36 /** 37 * This abstract class represents the symbolic version of a program variable. 38 */ 39 class SymbolicVariable 40 { 41 public: 42 SymbolicVariable( 43 frontend::Type const* _type, 44 frontend::Type const* _originalType, 45 std::string _uniqueName, 46 EncodingContext& _context 47 ); 48 SymbolicVariable( 49 smtutil::SortPointer _sort, 50 std::string _uniqueName, 51 EncodingContext& _context 52 ); 53 54 SymbolicVariable(SymbolicVariable&&) = default; 55 56 virtual ~SymbolicVariable() = default; 57 58 virtual smtutil::Expression currentValue(frontend::Type const* _targetType = nullptr) const; 59 std::string currentName() const; 60 virtual smtutil::Expression valueAtIndex(unsigned _index) const; 61 virtual std::string nameAtIndex(unsigned _index) const; 62 virtual smtutil::Expression resetIndex(); 63 virtual smtutil::Expression setIndex(unsigned _index); 64 virtual smtutil::Expression increaseIndex(); operator()65 virtual smtutil::Expression operator()(std::vector<smtutil::Expression> /*_arguments*/) const 66 { 67 solAssert(false, "Function application to non-function."); 68 } 69 index()70 unsigned index() const { return m_ssa->index(); } index()71 unsigned& index() { return m_ssa->index(); } 72 sort()73 smtutil::SortPointer const& sort() const { return m_sort; } type()74 frontend::Type const* type() const { return m_type; } originalType()75 frontend::Type const* originalType() const { return m_originalType; } 76 77 protected: 78 std::string uniqueSymbol(unsigned _index) const; 79 80 /// SMT sort. 81 smtutil::SortPointer m_sort; 82 /// Solidity type, used for size and range in number types. 83 frontend::Type const* m_type; 84 /// Solidity original type, used for type conversion if necessary. 85 frontend::Type const* m_originalType; 86 std::string m_uniqueName; 87 EncodingContext& m_context; 88 std::unique_ptr<SSAVariable> m_ssa; 89 }; 90 91 /** 92 * Specialization of SymbolicVariable for Bool 93 */ 94 class SymbolicBoolVariable: public SymbolicVariable 95 { 96 public: 97 SymbolicBoolVariable( 98 frontend::Type const* _type, 99 std::string _uniqueName, 100 EncodingContext& _context 101 ); 102 }; 103 104 /** 105 * Specialization of SymbolicVariable for Integers 106 */ 107 class SymbolicIntVariable: public SymbolicVariable 108 { 109 public: 110 SymbolicIntVariable( 111 frontend::Type const* _type, 112 frontend::Type const* _originalType, 113 std::string _uniqueName, 114 EncodingContext& _context 115 ); 116 }; 117 118 /** 119 * Specialization of SymbolicVariable for Address 120 */ 121 class SymbolicAddressVariable: public SymbolicIntVariable 122 { 123 public: 124 SymbolicAddressVariable( 125 std::string _uniqueName, 126 EncodingContext& _context 127 ); 128 }; 129 130 /** 131 * Specialization of SymbolicVariable for FixedBytes 132 */ 133 class SymbolicFixedBytesVariable: public SymbolicIntVariable 134 { 135 public: 136 SymbolicFixedBytesVariable( 137 frontend::Type const* _originalType, 138 unsigned _numBytes, 139 std::string _uniqueName, 140 EncodingContext& _context 141 ); 142 }; 143 144 /** 145 * Specialization of SymbolicVariable for FunctionType. 146 * Besides containing a symbolic function declaration, 147 * it also has an integer used as abstraction. 148 * By default, the abstract representation is used when 149 * values are requested, and the function declaration is 150 * used when operator() is applied over arguments. 151 */ 152 class SymbolicFunctionVariable: public SymbolicVariable 153 { 154 public: 155 SymbolicFunctionVariable( 156 frontend::Type const* _type, 157 std::string _uniqueName, 158 EncodingContext& _context 159 ); 160 SymbolicFunctionVariable( 161 smtutil::SortPointer _sort, 162 std::string _uniqueName, 163 EncodingContext& _context 164 ); 165 166 smtutil::Expression currentValue(frontend::Type const* _targetType = nullptr) const override; 167 168 // Explicit request the function declaration. 169 smtutil::Expression currentFunctionValue() const; 170 171 smtutil::Expression valueAtIndex(unsigned _index) const override; 172 173 // Explicit request the function declaration. 174 smtutil::Expression functionValueAtIndex(unsigned _index) const; 175 176 smtutil::Expression resetIndex() override; 177 smtutil::Expression setIndex(unsigned _index) override; 178 smtutil::Expression increaseIndex() override; 179 180 smtutil::Expression operator()(std::vector<smtutil::Expression> _arguments) const override; 181 182 private: 183 /// Creates a new function declaration. 184 void resetDeclaration(); 185 186 /// Stores the current function declaration. 187 smtutil::Expression m_declaration; 188 189 /// Abstract representation. 190 SymbolicIntVariable m_abstract{ 191 TypeProvider::uint256(), 192 TypeProvider::uint256(), 193 m_uniqueName + "_abstract", 194 m_context 195 }; 196 }; 197 198 /** 199 * Specialization of SymbolicVariable for Enum 200 */ 201 class SymbolicEnumVariable: public SymbolicVariable 202 { 203 public: 204 SymbolicEnumVariable( 205 frontend::Type const* _type, 206 std::string _uniqueName, 207 EncodingContext& _context 208 ); 209 }; 210 211 /** 212 * Specialization of SymbolicVariable for Tuple 213 */ 214 class SymbolicTupleVariable: public SymbolicVariable 215 { 216 public: 217 SymbolicTupleVariable( 218 frontend::Type const* _type, 219 std::string _uniqueName, 220 EncodingContext& _context 221 ); 222 SymbolicTupleVariable( 223 smtutil::SortPointer _sort, 224 std::string _uniqueName, 225 EncodingContext& _context 226 ); 227 228 smtutil::Expression currentValue(frontend::Type const* _targetType = nullptr) const override; 229 230 std::vector<smtutil::SortPointer> const& components() const; 231 smtutil::Expression component( 232 size_t _index, 233 frontend::Type const* _fromType = nullptr, 234 frontend::Type const* _toType = nullptr 235 ) const; 236 }; 237 238 /** 239 * Specialization of SymbolicVariable for Array 240 */ 241 class SymbolicArrayVariable: public SymbolicVariable 242 { 243 public: 244 SymbolicArrayVariable( 245 frontend::Type const* _type, 246 frontend::Type const* _originalTtype, 247 std::string _uniqueName, 248 EncodingContext& _context 249 ); 250 SymbolicArrayVariable( 251 smtutil::SortPointer _sort, 252 std::string _uniqueName, 253 EncodingContext& _context 254 ); 255 256 SymbolicArrayVariable(SymbolicArrayVariable&&) = default; 257 258 smtutil::Expression currentValue(frontend::Type const* _targetType = nullptr) const override; 259 smtutil::Expression valueAtIndex(unsigned _index) const override; resetIndex()260 smtutil::Expression resetIndex() override { SymbolicVariable::resetIndex(); return m_pair.resetIndex(); } setIndex(unsigned _index)261 smtutil::Expression setIndex(unsigned _index) override { SymbolicVariable::setIndex(_index); return m_pair.setIndex(_index); } increaseIndex()262 smtutil::Expression increaseIndex() override { SymbolicVariable::increaseIndex(); return m_pair.increaseIndex(); } 263 smtutil::Expression elements() const; 264 smtutil::Expression length() const; 265 tupleSort()266 smtutil::SortPointer tupleSort() { return m_pair.sort(); } 267 268 private: 269 SymbolicTupleVariable m_pair; 270 }; 271 272 /** 273 * Specialization of SymbolicVariable for Struct. 274 */ 275 class SymbolicStructVariable: public SymbolicVariable 276 { 277 public: 278 SymbolicStructVariable( 279 frontend::Type const* _type, 280 std::string _uniqueName, 281 EncodingContext& _context 282 ); 283 284 /// @returns the symbolic expression representing _member. 285 smtutil::Expression member(std::string const& _member) const; 286 287 /// @returns the symbolic expression representing this struct 288 /// with field _member updated. 289 smtutil::Expression assignMember(std::string const& _member, smtutil::Expression const& _memberValue); 290 291 /// @returns the symbolic expression representing this struct 292 /// with all fields updated with the given values. 293 smtutil::Expression assignAllMembers(std::vector<smtutil::Expression> const& _memberValues); 294 295 private: 296 std::map<std::string, unsigned> m_memberIndices; 297 }; 298 299 300 301 } 302