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/SymbolicVariables.h>
20
21 #include <libsolidity/formal/EncodingContext.h>
22 #include <libsolidity/formal/SymbolicTypes.h>
23
24 #include <libsolutil/Algorithms.h>
25
26 using namespace std;
27 using namespace solidity;
28 using namespace solidity::util;
29 using namespace solidity::smtutil;
30 using namespace solidity::frontend;
31 using namespace solidity::frontend::smt;
32
SymbolicVariable(frontend::Type const * _type,frontend::Type const * _originalType,string _uniqueName,EncodingContext & _context)33 SymbolicVariable::SymbolicVariable(
34 frontend::Type const* _type,
35 frontend::Type const* _originalType,
36 string _uniqueName,
37 EncodingContext& _context
38 ):
39 m_type(_type),
40 m_originalType(_originalType),
41 m_uniqueName(move(_uniqueName)),
42 m_context(_context),
43 m_ssa(make_unique<SSAVariable>())
44 {
45 solAssert(m_type, "");
46 m_sort = smtSort(*m_type);
47 solAssert(m_sort, "");
48 }
49
SymbolicVariable(SortPointer _sort,string _uniqueName,EncodingContext & _context)50 SymbolicVariable::SymbolicVariable(
51 SortPointer _sort,
52 string _uniqueName,
53 EncodingContext& _context
54 ):
55 m_sort(move(_sort)),
56 m_uniqueName(move(_uniqueName)),
57 m_context(_context),
58 m_ssa(make_unique<SSAVariable>())
59 {
60 solAssert(m_sort, "");
61 }
62
currentValue(frontend::Type const *) const63 smtutil::Expression SymbolicVariable::currentValue(frontend::Type const*) const
64 {
65 return valueAtIndex(m_ssa->index());
66 }
67
currentName() const68 string SymbolicVariable::currentName() const
69 {
70 return uniqueSymbol(m_ssa->index());
71 }
72
valueAtIndex(unsigned _index) const73 smtutil::Expression SymbolicVariable::valueAtIndex(unsigned _index) const
74 {
75 return m_context.newVariable(uniqueSymbol(_index), m_sort);
76 }
77
nameAtIndex(unsigned _index) const78 string SymbolicVariable::nameAtIndex(unsigned _index) const
79 {
80 return uniqueSymbol(_index);
81 }
82
uniqueSymbol(unsigned _index) const83 string SymbolicVariable::uniqueSymbol(unsigned _index) const
84 {
85 return m_uniqueName + "_" + to_string(_index);
86 }
87
resetIndex()88 smtutil::Expression SymbolicVariable::resetIndex()
89 {
90 m_ssa->resetIndex();
91 return currentValue();
92 }
93
setIndex(unsigned _index)94 smtutil::Expression SymbolicVariable::setIndex(unsigned _index)
95 {
96 m_ssa->setIndex(_index);
97 return currentValue();
98 }
99
increaseIndex()100 smtutil::Expression SymbolicVariable::increaseIndex()
101 {
102 ++(*m_ssa);
103 return currentValue();
104 }
105
SymbolicBoolVariable(frontend::Type const * _type,string _uniqueName,EncodingContext & _context)106 SymbolicBoolVariable::SymbolicBoolVariable(
107 frontend::Type const* _type,
108 string _uniqueName,
109 EncodingContext& _context
110 ):
111 SymbolicVariable(_type, _type, move(_uniqueName), _context)
112 {
113 solAssert(m_type->category() == frontend::Type::Category::Bool, "");
114 }
115
SymbolicIntVariable(frontend::Type const * _type,frontend::Type const * _originalType,string _uniqueName,EncodingContext & _context)116 SymbolicIntVariable::SymbolicIntVariable(
117 frontend::Type const* _type,
118 frontend::Type const* _originalType,
119 string _uniqueName,
120 EncodingContext& _context
121 ):
122 SymbolicVariable(_type, _originalType, move(_uniqueName), _context)
123 {
124 solAssert(isNumber(*m_type), "");
125 }
126
SymbolicAddressVariable(string _uniqueName,EncodingContext & _context)127 SymbolicAddressVariable::SymbolicAddressVariable(
128 string _uniqueName,
129 EncodingContext& _context
130 ):
131 SymbolicIntVariable(TypeProvider::uint(160), TypeProvider::uint(160), move(_uniqueName), _context)
132 {
133 }
134
SymbolicFixedBytesVariable(frontend::Type const * _originalType,unsigned _numBytes,string _uniqueName,EncodingContext & _context)135 SymbolicFixedBytesVariable::SymbolicFixedBytesVariable(
136 frontend::Type const* _originalType,
137 unsigned _numBytes,
138 string _uniqueName,
139 EncodingContext& _context
140 ):
141 SymbolicIntVariable(TypeProvider::uint(_numBytes * 8), _originalType, move(_uniqueName), _context)
142 {
143 }
144
SymbolicFunctionVariable(frontend::Type const * _type,string _uniqueName,EncodingContext & _context)145 SymbolicFunctionVariable::SymbolicFunctionVariable(
146 frontend::Type const* _type,
147 string _uniqueName,
148 EncodingContext& _context
149 ):
150 SymbolicVariable(_type, _type, move(_uniqueName), _context),
151 m_declaration(m_context.newVariable(currentName(), m_sort))
152 {
153 solAssert(m_type->category() == frontend::Type::Category::Function, "");
154 }
155
SymbolicFunctionVariable(SortPointer _sort,string _uniqueName,EncodingContext & _context)156 SymbolicFunctionVariable::SymbolicFunctionVariable(
157 SortPointer _sort,
158 string _uniqueName,
159 EncodingContext& _context
160 ):
161 SymbolicVariable(move(_sort), move(_uniqueName), _context),
162 m_declaration(m_context.newVariable(currentName(), m_sort))
163 {
164 solAssert(m_sort->kind == Kind::Function, "");
165 }
166
currentValue(frontend::Type const * _targetType) const167 smtutil::Expression SymbolicFunctionVariable::currentValue(frontend::Type const* _targetType) const
168 {
169 return m_abstract.currentValue(_targetType);
170 }
171
currentFunctionValue() const172 smtutil::Expression SymbolicFunctionVariable::currentFunctionValue() const
173 {
174 return m_declaration;
175 }
176
valueAtIndex(unsigned _index) const177 smtutil::Expression SymbolicFunctionVariable::valueAtIndex(unsigned _index) const
178 {
179 return m_abstract.valueAtIndex(_index);
180 }
181
functionValueAtIndex(unsigned _index) const182 smtutil::Expression SymbolicFunctionVariable::functionValueAtIndex(unsigned _index) const
183 {
184 return SymbolicVariable::valueAtIndex(_index);
185 }
186
resetIndex()187 smtutil::Expression SymbolicFunctionVariable::resetIndex()
188 {
189 SymbolicVariable::resetIndex();
190 return m_abstract.resetIndex();
191 }
192
setIndex(unsigned _index)193 smtutil::Expression SymbolicFunctionVariable::setIndex(unsigned _index)
194 {
195 SymbolicVariable::setIndex(_index);
196 return m_abstract.setIndex(_index);
197 }
198
increaseIndex()199 smtutil::Expression SymbolicFunctionVariable::increaseIndex()
200 {
201 ++(*m_ssa);
202 resetDeclaration();
203 m_abstract.increaseIndex();
204 return m_abstract.currentValue();
205 }
206
operator ()(vector<smtutil::Expression> _arguments) const207 smtutil::Expression SymbolicFunctionVariable::operator()(vector<smtutil::Expression> _arguments) const
208 {
209 return m_declaration(_arguments);
210 }
211
resetDeclaration()212 void SymbolicFunctionVariable::resetDeclaration()
213 {
214 m_declaration = m_context.newVariable(currentName(), m_sort);
215 }
216
SymbolicEnumVariable(frontend::Type const * _type,string _uniqueName,EncodingContext & _context)217 SymbolicEnumVariable::SymbolicEnumVariable(
218 frontend::Type const* _type,
219 string _uniqueName,
220 EncodingContext& _context
221 ):
222 SymbolicVariable(_type, _type, move(_uniqueName), _context)
223 {
224 solAssert(isEnum(*m_type), "");
225 }
226
SymbolicTupleVariable(frontend::Type const * _type,string _uniqueName,EncodingContext & _context)227 SymbolicTupleVariable::SymbolicTupleVariable(
228 frontend::Type const* _type,
229 string _uniqueName,
230 EncodingContext& _context
231 ):
232 SymbolicVariable(_type, _type, move(_uniqueName), _context)
233 {
234 solAssert(isTuple(*m_type), "");
235 }
236
SymbolicTupleVariable(SortPointer _sort,string _uniqueName,EncodingContext & _context)237 SymbolicTupleVariable::SymbolicTupleVariable(
238 SortPointer _sort,
239 string _uniqueName,
240 EncodingContext& _context
241 ):
242 SymbolicVariable(move(_sort), move(_uniqueName), _context)
243 {
244 solAssert(m_sort->kind == Kind::Tuple, "");
245 }
246
currentValue(frontend::Type const * _targetType) const247 smtutil::Expression SymbolicTupleVariable::currentValue(frontend::Type const* _targetType) const
248 {
249 if (!_targetType || sort() == smtSort(*_targetType))
250 return SymbolicVariable::currentValue();
251
252 auto thisTuple = dynamic_pointer_cast<TupleSort>(sort());
253 auto otherTuple = dynamic_pointer_cast<TupleSort>(smtSort(*_targetType));
254 solAssert(thisTuple && otherTuple, "");
255 solAssert(thisTuple->components.size() == otherTuple->components.size(), "");
256 vector<smtutil::Expression> args;
257 for (size_t i = 0; i < thisTuple->components.size(); ++i)
258 args.emplace_back(component(i, type(), _targetType));
259 return smtutil::Expression::tuple_constructor(
260 smtutil::Expression(make_shared<smtutil::SortSort>(smtSort(*_targetType)), ""),
261 args
262 );
263 }
264
components() const265 vector<SortPointer> const& SymbolicTupleVariable::components() const
266 {
267 auto tupleSort = dynamic_pointer_cast<TupleSort>(m_sort);
268 solAssert(tupleSort, "");
269 return tupleSort->components;
270 }
271
component(size_t _index,frontend::Type const * _fromType,frontend::Type const * _toType) const272 smtutil::Expression SymbolicTupleVariable::component(
273 size_t _index,
274 frontend::Type const* _fromType,
275 frontend::Type const* _toType
276 ) const
277 {
278 optional<smtutil::Expression> conversion = symbolicTypeConversion(_fromType, _toType);
279 if (conversion)
280 return *conversion;
281
282 return smtutil::Expression::tuple_get(currentValue(), _index);
283 }
284
SymbolicArrayVariable(frontend::Type const * _type,frontend::Type const * _originalType,string _uniqueName,EncodingContext & _context)285 SymbolicArrayVariable::SymbolicArrayVariable(
286 frontend::Type const* _type,
287 frontend::Type const* _originalType,
288 string _uniqueName,
289 EncodingContext& _context
290 ):
291 SymbolicVariable(_type, _originalType, move(_uniqueName), _context),
292 m_pair(
293 smtSort(*_type),
294 m_uniqueName + "_length_pair",
295 m_context
296 )
297 {
298 solAssert(isArray(*m_type) || isMapping(*m_type), "");
299 }
300
SymbolicArrayVariable(SortPointer _sort,string _uniqueName,EncodingContext & _context)301 SymbolicArrayVariable::SymbolicArrayVariable(
302 SortPointer _sort,
303 string _uniqueName,
304 EncodingContext& _context
305 ):
306 SymbolicVariable(move(_sort), move(_uniqueName), _context),
307 m_pair(
308 std::make_shared<TupleSort>(
309 "array_length_pair",
310 std::vector<std::string>{"array", "length"},
311 std::vector<SortPointer>{m_sort, SortProvider::uintSort}
312 ),
313 m_uniqueName + "_array_length_pair",
314 m_context
315 )
316 {
317 solAssert(m_sort->kind == Kind::Array, "");
318 }
319
currentValue(frontend::Type const * _targetType) const320 smtutil::Expression SymbolicArrayVariable::currentValue(frontend::Type const* _targetType) const
321 {
322 optional<smtutil::Expression> conversion = symbolicTypeConversion(m_originalType, _targetType);
323 if (conversion)
324 return *conversion;
325
326 return m_pair.currentValue();
327 }
328
valueAtIndex(unsigned _index) const329 smtutil::Expression SymbolicArrayVariable::valueAtIndex(unsigned _index) const
330 {
331 return m_pair.valueAtIndex(_index);
332 }
333
elements() const334 smtutil::Expression SymbolicArrayVariable::elements() const
335 {
336 return m_pair.component(0);
337 }
338
length() const339 smtutil::Expression SymbolicArrayVariable::length() const
340 {
341 return m_pair.component(1);
342 }
343
SymbolicStructVariable(frontend::Type const * _type,string _uniqueName,EncodingContext & _context)344 SymbolicStructVariable::SymbolicStructVariable(
345 frontend::Type const* _type,
346 string _uniqueName,
347 EncodingContext& _context
348 ):
349 SymbolicVariable(_type, _type, move(_uniqueName), _context)
350 {
351 solAssert(isNonRecursiveStruct(*m_type), "");
352 auto const* structType = dynamic_cast<StructType const*>(_type);
353 solAssert(structType, "");
354 auto const& members = structType->structDefinition().members();
355 for (unsigned i = 0; i < members.size(); ++i)
356 {
357 solAssert(members.at(i), "");
358 m_memberIndices.emplace(members.at(i)->name(), i);
359 }
360 }
361
member(string const & _member) const362 smtutil::Expression SymbolicStructVariable::member(string const& _member) const
363 {
364 return smtutil::Expression::tuple_get(currentValue(), m_memberIndices.at(_member));
365 }
366
assignMember(string const & _member,smtutil::Expression const & _memberValue)367 smtutil::Expression SymbolicStructVariable::assignMember(string const& _member, smtutil::Expression const& _memberValue)
368 {
369 auto const* structType = dynamic_cast<StructType const*>(m_type);
370 solAssert(structType, "");
371 auto const& structDef = structType->structDefinition();
372 auto const& structMembers = structDef.members();
373 auto oldMembers = applyMap(
374 structMembers,
375 [&](auto _member) { return member(_member->name()); }
376 );
377 increaseIndex();
378 for (unsigned i = 0; i < structMembers.size(); ++i)
379 {
380 auto const& memberName = structMembers.at(i)->name();
381 auto newMember = memberName == _member ? _memberValue : oldMembers.at(i);
382 m_context.addAssertion(member(memberName) == newMember);
383 }
384
385 return currentValue();
386 }
387
assignAllMembers(vector<smtutil::Expression> const & _memberValues)388 smtutil::Expression SymbolicStructVariable::assignAllMembers(vector<smtutil::Expression> const& _memberValues)
389 {
390 auto structType = dynamic_cast<StructType const*>(m_type);
391 solAssert(structType, "");
392
393 auto const& structDef = structType->structDefinition();
394 auto const& structMembers = structDef.members();
395 solAssert(_memberValues.size() == structMembers.size(), "");
396 increaseIndex();
397 for (unsigned i = 0; i < _memberValues.size(); ++i)
398 m_context.addAssertion(_memberValues[i] == member(structMembers[i]->name()));
399
400 return currentValue();
401 }
402