2018-10-15 15:32:17 +00:00
|
|
|
/*
|
|
|
|
This file is part of solidity.
|
|
|
|
|
|
|
|
solidity is free software: you can redistribute it and/or modify
|
|
|
|
it under the terms of the GNU General Public License as published by
|
|
|
|
the Free Software Foundation, either version 3 of the License, or
|
|
|
|
(at your option) any later version.
|
|
|
|
|
|
|
|
solidity is distributed in the hope that it will be useful,
|
|
|
|
but WITHOUT ANY WARRANTY; without even the implied warranty of
|
|
|
|
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
|
|
|
|
GNU General Public License for more details.
|
|
|
|
|
|
|
|
You should have received a copy of the GNU General Public License
|
|
|
|
along with solidity. If not, see <http://www.gnu.org/licenses/>.
|
|
|
|
*/
|
|
|
|
|
|
|
|
#include <libsolidity/formal/SymbolicTypes.h>
|
|
|
|
|
2019-04-15 13:33:39 +00:00
|
|
|
#include <libsolidity/ast/TypeProvider.h>
|
2018-10-15 15:32:17 +00:00
|
|
|
#include <libsolidity/ast/Types.h>
|
|
|
|
#include <memory>
|
|
|
|
|
|
|
|
using namespace std;
|
|
|
|
|
2019-05-09 10:16:52 +00:00
|
|
|
namespace dev
|
|
|
|
{
|
|
|
|
namespace solidity
|
|
|
|
{
|
|
|
|
namespace smt
|
|
|
|
{
|
|
|
|
|
|
|
|
SortPointer smtSort(solidity::Type const& _type)
|
2018-11-21 14:13:50 +00:00
|
|
|
{
|
|
|
|
switch (smtKind(_type.category()))
|
|
|
|
{
|
2019-05-09 10:16:52 +00:00
|
|
|
case Kind::Int:
|
|
|
|
return make_shared<Sort>(Kind::Int);
|
|
|
|
case Kind::Bool:
|
|
|
|
return make_shared<Sort>(Kind::Bool);
|
|
|
|
case Kind::Function:
|
2018-11-21 15:57:02 +00:00
|
|
|
{
|
2019-05-09 10:16:52 +00:00
|
|
|
auto fType = dynamic_cast<solidity::FunctionType const*>(&_type);
|
2018-11-21 15:57:02 +00:00
|
|
|
solAssert(fType, "");
|
2019-05-09 10:16:52 +00:00
|
|
|
vector<SortPointer> parameterSorts = smtSort(fType->parameterTypes());
|
2018-11-21 15:57:02 +00:00
|
|
|
auto returnTypes = fType->returnParameterTypes();
|
2019-05-09 10:16:52 +00:00
|
|
|
SortPointer returnSort;
|
2018-12-10 16:23:36 +00:00
|
|
|
// TODO change this when we support tuples.
|
|
|
|
if (returnTypes.size() == 0)
|
|
|
|
// We cannot declare functions without a return sort, so we use the smallest.
|
2019-05-09 10:16:52 +00:00
|
|
|
returnSort = make_shared<Sort>(Kind::Bool);
|
2018-12-10 16:23:36 +00:00
|
|
|
else if (returnTypes.size() > 1)
|
|
|
|
// Abstract sort.
|
2019-05-09 10:16:52 +00:00
|
|
|
returnSort = make_shared<Sort>(Kind::Int);
|
2018-12-10 16:23:36 +00:00
|
|
|
else
|
2019-05-09 11:17:00 +00:00
|
|
|
returnSort = smtSort(*returnTypes.front());
|
2019-05-09 10:16:52 +00:00
|
|
|
return make_shared<FunctionSort>(parameterSorts, returnSort);
|
2018-11-21 15:57:02 +00:00
|
|
|
}
|
2019-05-09 10:16:52 +00:00
|
|
|
case Kind::Array:
|
2018-11-22 10:24:12 +00:00
|
|
|
{
|
2018-11-09 16:06:30 +00:00
|
|
|
if (isMapping(_type.category()))
|
|
|
|
{
|
2019-05-09 10:16:52 +00:00
|
|
|
auto mapType = dynamic_cast<solidity::MappingType const*>(&_type);
|
2018-11-09 16:06:30 +00:00
|
|
|
solAssert(mapType, "");
|
2019-05-09 10:16:52 +00:00
|
|
|
return make_shared<ArraySort>(smtSort(*mapType->keyType()), smtSort(*mapType->valueType()));
|
2018-11-09 16:06:30 +00:00
|
|
|
}
|
2019-08-07 08:48:09 +00:00
|
|
|
else if (isStringLiteral(_type.category()))
|
|
|
|
{
|
|
|
|
auto stringLitType = dynamic_cast<solidity::StringLiteralType const*>(&_type);
|
|
|
|
solAssert(stringLitType, "");
|
|
|
|
auto intSort = make_shared<Sort>(Kind::Int);
|
|
|
|
return make_shared<ArraySort>(intSort, intSort);
|
|
|
|
}
|
2019-02-20 11:34:52 +00:00
|
|
|
else
|
|
|
|
{
|
|
|
|
solAssert(isArray(_type.category()), "");
|
2019-05-09 10:16:52 +00:00
|
|
|
auto arrayType = dynamic_cast<solidity::ArrayType const*>(&_type);
|
2019-02-20 11:34:52 +00:00
|
|
|
solAssert(arrayType, "");
|
2019-05-09 10:16:52 +00:00
|
|
|
return make_shared<ArraySort>(make_shared<Sort>(Kind::Int), smtSort(*arrayType->baseType()));
|
2019-02-20 11:34:52 +00:00
|
|
|
}
|
2018-11-22 10:24:12 +00:00
|
|
|
}
|
2018-12-10 16:23:36 +00:00
|
|
|
default:
|
|
|
|
// Abstract case.
|
2019-05-09 10:16:52 +00:00
|
|
|
return make_shared<Sort>(Kind::Int);
|
2018-11-21 14:13:50 +00:00
|
|
|
}
|
|
|
|
}
|
|
|
|
|
2019-05-09 10:16:52 +00:00
|
|
|
vector<SortPointer> smtSort(vector<solidity::TypePointer> const& _types)
|
2018-11-21 15:57:02 +00:00
|
|
|
{
|
2019-05-09 10:16:52 +00:00
|
|
|
vector<SortPointer> sorts;
|
2018-11-21 15:57:02 +00:00
|
|
|
for (auto const& type: _types)
|
|
|
|
sorts.push_back(smtSort(*type));
|
|
|
|
return sorts;
|
|
|
|
}
|
|
|
|
|
2019-05-09 10:16:52 +00:00
|
|
|
Kind smtKind(solidity::Type::Category _category)
|
2018-10-25 14:00:09 +00:00
|
|
|
{
|
|
|
|
if (isNumber(_category))
|
2019-05-09 10:16:52 +00:00
|
|
|
return Kind::Int;
|
2018-10-25 14:00:09 +00:00
|
|
|
else if (isBool(_category))
|
2019-05-09 10:16:52 +00:00
|
|
|
return Kind::Bool;
|
2018-12-10 16:23:36 +00:00
|
|
|
else if (isFunction(_category))
|
2019-05-09 10:16:52 +00:00
|
|
|
return Kind::Function;
|
2019-02-20 11:34:52 +00:00
|
|
|
else if (isMapping(_category) || isArray(_category))
|
2019-05-09 10:16:52 +00:00
|
|
|
return Kind::Array;
|
2018-12-10 16:23:36 +00:00
|
|
|
// Abstract case.
|
2019-05-09 10:16:52 +00:00
|
|
|
return Kind::Int;
|
2018-10-25 14:00:09 +00:00
|
|
|
}
|
|
|
|
|
2019-05-09 10:16:52 +00:00
|
|
|
bool isSupportedType(solidity::Type::Category _category)
|
2018-10-15 15:32:17 +00:00
|
|
|
{
|
2018-10-17 16:00:42 +00:00
|
|
|
return isNumber(_category) ||
|
2018-11-09 16:06:30 +00:00
|
|
|
isBool(_category) ||
|
2019-02-20 11:34:52 +00:00
|
|
|
isMapping(_category) ||
|
2019-04-26 12:57:29 +00:00
|
|
|
isArray(_category) ||
|
|
|
|
isTuple(_category);
|
2018-12-10 16:23:36 +00:00
|
|
|
}
|
|
|
|
|
2019-05-09 10:16:52 +00:00
|
|
|
bool isSupportedTypeDeclaration(solidity::Type::Category _category)
|
2018-12-10 16:23:36 +00:00
|
|
|
{
|
|
|
|
return isSupportedType(_category) ||
|
2018-10-17 16:00:42 +00:00
|
|
|
isFunction(_category);
|
2018-10-17 13:56:44 +00:00
|
|
|
}
|
|
|
|
|
2019-05-09 10:16:52 +00:00
|
|
|
pair<bool, shared_ptr<SymbolicVariable>> newSymbolicVariable(
|
|
|
|
solidity::Type const& _type,
|
2018-10-17 13:56:44 +00:00
|
|
|
std::string const& _uniqueName,
|
2019-07-03 14:05:56 +00:00
|
|
|
EncodingContext& _context
|
2018-10-17 13:56:44 +00:00
|
|
|
)
|
|
|
|
{
|
2018-10-17 16:00:42 +00:00
|
|
|
bool abstract = false;
|
|
|
|
shared_ptr<SymbolicVariable> var;
|
2019-05-09 10:16:52 +00:00
|
|
|
solidity::TypePointer type = &_type;
|
2018-12-10 16:23:36 +00:00
|
|
|
if (!isSupportedTypeDeclaration(_type))
|
2018-10-17 16:00:42 +00:00
|
|
|
{
|
|
|
|
abstract = true;
|
2019-08-07 08:48:09 +00:00
|
|
|
var = make_shared<SymbolicIntVariable>(solidity::TypeProvider::uint256(), type, _uniqueName, _context);
|
2018-10-17 16:00:42 +00:00
|
|
|
}
|
|
|
|
else if (isBool(_type.category()))
|
2019-07-03 14:05:56 +00:00
|
|
|
var = make_shared<SymbolicBoolVariable>(type, _uniqueName, _context);
|
2018-10-17 16:00:42 +00:00
|
|
|
else if (isFunction(_type.category()))
|
2019-07-03 14:05:56 +00:00
|
|
|
var = make_shared<SymbolicFunctionVariable>(type, _uniqueName, _context);
|
2018-10-17 13:56:44 +00:00
|
|
|
else if (isInteger(_type.category()))
|
2019-08-07 08:48:09 +00:00
|
|
|
var = make_shared<SymbolicIntVariable>(type, type, _uniqueName, _context);
|
2018-10-22 08:29:03 +00:00
|
|
|
else if (isFixedBytes(_type.category()))
|
|
|
|
{
|
2019-05-09 10:16:52 +00:00
|
|
|
auto fixedBytesType = dynamic_cast<solidity::FixedBytesType const*>(type);
|
2018-10-22 08:29:03 +00:00
|
|
|
solAssert(fixedBytesType, "");
|
2019-08-07 08:48:09 +00:00
|
|
|
var = make_shared<SymbolicFixedBytesVariable>(type, fixedBytesType->numBytes(), _uniqueName, _context);
|
2018-10-22 08:29:03 +00:00
|
|
|
}
|
2019-04-17 14:08:02 +00:00
|
|
|
else if (isAddress(_type.category()) || isContract(_type.category()))
|
2019-07-03 14:05:56 +00:00
|
|
|
var = make_shared<SymbolicAddressVariable>(_uniqueName, _context);
|
2019-03-06 00:10:43 +00:00
|
|
|
else if (isEnum(_type.category()))
|
2019-07-03 14:05:56 +00:00
|
|
|
var = make_shared<SymbolicEnumVariable>(type, _uniqueName, _context);
|
2018-10-17 16:00:42 +00:00
|
|
|
else if (isRational(_type.category()))
|
|
|
|
{
|
2019-05-09 10:16:52 +00:00
|
|
|
auto rational = dynamic_cast<solidity::RationalNumberType const*>(&_type);
|
2018-10-17 16:00:42 +00:00
|
|
|
solAssert(rational, "");
|
|
|
|
if (rational->isFractional())
|
2019-08-07 08:48:09 +00:00
|
|
|
var = make_shared<SymbolicIntVariable>(solidity::TypeProvider::uint256(), type, _uniqueName, _context);
|
2018-10-17 16:00:42 +00:00
|
|
|
else
|
2019-08-07 08:48:09 +00:00
|
|
|
var = make_shared<SymbolicIntVariable>(type, type, _uniqueName, _context);
|
2018-10-17 16:00:42 +00:00
|
|
|
}
|
2018-11-09 16:06:30 +00:00
|
|
|
else if (isMapping(_type.category()))
|
2019-07-03 14:05:56 +00:00
|
|
|
var = make_shared<SymbolicMappingVariable>(type, _uniqueName, _context);
|
2019-02-20 11:34:52 +00:00
|
|
|
else if (isArray(_type.category()))
|
2019-08-07 08:48:09 +00:00
|
|
|
var = make_shared<SymbolicArrayVariable>(type, type, _uniqueName, _context);
|
2019-04-26 12:57:29 +00:00
|
|
|
else if (isTuple(_type.category()))
|
2019-07-03 14:05:56 +00:00
|
|
|
var = make_shared<SymbolicTupleVariable>(type, _uniqueName, _context);
|
2019-08-07 08:48:09 +00:00
|
|
|
else if (isStringLiteral(_type.category()))
|
|
|
|
{
|
|
|
|
auto stringType = TypeProvider::stringMemory();
|
|
|
|
var = make_shared<SymbolicArrayVariable>(stringType, type, _uniqueName, _context);
|
|
|
|
}
|
2018-10-17 13:56:44 +00:00
|
|
|
else
|
|
|
|
solAssert(false, "");
|
2018-10-17 16:00:42 +00:00
|
|
|
return make_pair(abstract, var);
|
2018-10-15 15:32:17 +00:00
|
|
|
}
|
|
|
|
|
2019-05-09 10:16:52 +00:00
|
|
|
bool isSupportedType(solidity::Type const& _type)
|
2018-10-15 15:32:17 +00:00
|
|
|
{
|
|
|
|
return isSupportedType(_type.category());
|
|
|
|
}
|
|
|
|
|
2019-05-09 10:16:52 +00:00
|
|
|
bool isSupportedTypeDeclaration(solidity::Type const& _type)
|
2018-12-10 16:23:36 +00:00
|
|
|
{
|
|
|
|
return isSupportedTypeDeclaration(_type.category());
|
|
|
|
}
|
|
|
|
|
2019-05-09 10:16:52 +00:00
|
|
|
bool isInteger(solidity::Type::Category _category)
|
2018-10-15 15:32:17 +00:00
|
|
|
{
|
2019-05-09 10:16:52 +00:00
|
|
|
return _category == solidity::Type::Category::Integer;
|
2018-10-15 15:32:17 +00:00
|
|
|
}
|
|
|
|
|
2019-05-09 10:16:52 +00:00
|
|
|
bool isRational(solidity::Type::Category _category)
|
2018-10-15 15:32:17 +00:00
|
|
|
{
|
2019-05-09 10:16:52 +00:00
|
|
|
return _category == solidity::Type::Category::RationalNumber;
|
2018-10-15 15:32:17 +00:00
|
|
|
}
|
|
|
|
|
2019-05-09 10:16:52 +00:00
|
|
|
bool isFixedBytes(solidity::Type::Category _category)
|
2018-10-22 08:29:03 +00:00
|
|
|
{
|
2019-05-09 10:16:52 +00:00
|
|
|
return _category == solidity::Type::Category::FixedBytes;
|
2018-10-22 08:29:03 +00:00
|
|
|
}
|
|
|
|
|
2019-05-09 10:16:52 +00:00
|
|
|
bool isAddress(solidity::Type::Category _category)
|
2018-10-17 13:56:44 +00:00
|
|
|
{
|
2019-05-09 10:16:52 +00:00
|
|
|
return _category == solidity::Type::Category::Address;
|
2018-10-17 13:56:44 +00:00
|
|
|
}
|
|
|
|
|
2019-05-09 10:16:52 +00:00
|
|
|
bool isContract(solidity::Type::Category _category)
|
2019-04-17 14:08:02 +00:00
|
|
|
{
|
2019-05-09 10:16:52 +00:00
|
|
|
return _category == solidity::Type::Category::Contract;
|
2019-04-17 14:08:02 +00:00
|
|
|
}
|
|
|
|
|
2019-05-09 10:16:52 +00:00
|
|
|
bool isEnum(solidity::Type::Category _category)
|
2019-03-06 00:10:43 +00:00
|
|
|
{
|
2019-05-09 10:16:52 +00:00
|
|
|
return _category == solidity::Type::Category::Enum;
|
2019-03-06 00:10:43 +00:00
|
|
|
}
|
|
|
|
|
2019-05-09 10:16:52 +00:00
|
|
|
bool isNumber(solidity::Type::Category _category)
|
2018-10-17 13:56:44 +00:00
|
|
|
{
|
|
|
|
return isInteger(_category) ||
|
2018-10-17 16:00:42 +00:00
|
|
|
isRational(_category) ||
|
2018-10-22 08:29:03 +00:00
|
|
|
isFixedBytes(_category) ||
|
2019-03-06 00:10:43 +00:00
|
|
|
isAddress(_category) ||
|
2019-04-17 14:08:02 +00:00
|
|
|
isContract(_category) ||
|
2019-03-06 00:10:43 +00:00
|
|
|
isEnum(_category);
|
2018-10-17 13:56:44 +00:00
|
|
|
}
|
|
|
|
|
2019-05-09 10:16:52 +00:00
|
|
|
bool isBool(solidity::Type::Category _category)
|
2018-10-15 15:32:17 +00:00
|
|
|
{
|
2019-05-09 10:16:52 +00:00
|
|
|
return _category == solidity::Type::Category::Bool;
|
2018-10-15 15:32:17 +00:00
|
|
|
}
|
|
|
|
|
2019-05-09 10:16:52 +00:00
|
|
|
bool isFunction(solidity::Type::Category _category)
|
2018-10-15 15:32:17 +00:00
|
|
|
{
|
2019-05-09 10:16:52 +00:00
|
|
|
return _category == solidity::Type::Category::Function;
|
2018-10-15 15:32:17 +00:00
|
|
|
}
|
|
|
|
|
2019-05-09 10:16:52 +00:00
|
|
|
bool isMapping(solidity::Type::Category _category)
|
2018-11-09 16:06:30 +00:00
|
|
|
{
|
2019-05-09 10:16:52 +00:00
|
|
|
return _category == solidity::Type::Category::Mapping;
|
2018-11-09 16:06:30 +00:00
|
|
|
}
|
|
|
|
|
2019-05-09 10:16:52 +00:00
|
|
|
bool isArray(solidity::Type::Category _category)
|
2019-02-20 11:34:52 +00:00
|
|
|
{
|
2019-08-07 08:48:09 +00:00
|
|
|
return _category == solidity::Type::Category::Array ||
|
|
|
|
_category == solidity::Type::Category::StringLiteral;
|
2019-02-20 11:34:52 +00:00
|
|
|
}
|
|
|
|
|
2019-05-09 10:16:52 +00:00
|
|
|
bool isTuple(solidity::Type::Category _category)
|
2019-04-26 12:57:29 +00:00
|
|
|
{
|
2019-05-09 10:16:52 +00:00
|
|
|
return _category == solidity::Type::Category::Tuple;
|
2019-04-26 12:57:29 +00:00
|
|
|
}
|
|
|
|
|
2019-08-07 08:48:09 +00:00
|
|
|
bool isStringLiteral(solidity::Type::Category _category)
|
|
|
|
{
|
|
|
|
return _category == solidity::Type::Category::StringLiteral;
|
|
|
|
}
|
|
|
|
|
2019-05-09 10:16:52 +00:00
|
|
|
Expression minValue(solidity::IntegerType const& _type)
|
2018-10-15 15:32:17 +00:00
|
|
|
{
|
2019-05-09 10:16:52 +00:00
|
|
|
return Expression(_type.minValue());
|
2018-10-15 15:32:17 +00:00
|
|
|
}
|
|
|
|
|
2019-05-09 10:16:52 +00:00
|
|
|
Expression maxValue(solidity::IntegerType const& _type)
|
2018-10-17 13:56:44 +00:00
|
|
|
{
|
2019-05-09 10:16:52 +00:00
|
|
|
return Expression(_type.maxValue());
|
2018-10-17 13:56:44 +00:00
|
|
|
}
|
2018-11-22 13:48:31 +00:00
|
|
|
|
2019-07-03 14:05:56 +00:00
|
|
|
void setSymbolicZeroValue(SymbolicVariable const& _variable, EncodingContext& _context)
|
2018-11-22 13:48:31 +00:00
|
|
|
{
|
2019-07-03 14:05:56 +00:00
|
|
|
setSymbolicZeroValue(_variable.currentValue(), _variable.type(), _context);
|
2018-11-22 13:48:31 +00:00
|
|
|
}
|
|
|
|
|
2019-07-03 14:05:56 +00:00
|
|
|
void setSymbolicZeroValue(Expression _expr, solidity::TypePointer const& _type, EncodingContext& _context)
|
2018-11-22 13:48:31 +00:00
|
|
|
{
|
2019-04-12 12:44:18 +00:00
|
|
|
solAssert(_type, "");
|
2019-08-22 13:44:30 +00:00
|
|
|
_context.addAssertion(_expr == zeroValue(_type));
|
|
|
|
}
|
|
|
|
|
|
|
|
Expression zeroValue(solidity::TypePointer const& _type)
|
|
|
|
{
|
|
|
|
solAssert(_type, "");
|
|
|
|
if (isSupportedType(_type->category()))
|
|
|
|
{
|
|
|
|
if (isNumber(_type->category()))
|
|
|
|
return 0;
|
|
|
|
if (isBool(_type->category()))
|
|
|
|
return Expression(false);
|
|
|
|
if (isArray(_type->category()) || isMapping(_type->category()))
|
|
|
|
{
|
|
|
|
if (auto arrayType = dynamic_cast<ArrayType const*>(_type))
|
|
|
|
return Expression::const_array(Expression(arrayType), zeroValue(arrayType->baseType()));
|
|
|
|
auto mappingType = dynamic_cast<MappingType const*>(_type);
|
|
|
|
solAssert(mappingType, "");
|
|
|
|
return Expression::const_array(Expression(mappingType), zeroValue(mappingType->valueType()));
|
|
|
|
}
|
|
|
|
solAssert(false, "");
|
|
|
|
}
|
|
|
|
// Unsupported types are abstracted as Int.
|
|
|
|
return 0;
|
2018-11-22 13:48:31 +00:00
|
|
|
}
|
|
|
|
|
2019-07-03 14:05:56 +00:00
|
|
|
void setSymbolicUnknownValue(SymbolicVariable const& _variable, EncodingContext& _context)
|
2018-11-22 13:48:31 +00:00
|
|
|
{
|
2019-07-03 14:05:56 +00:00
|
|
|
setSymbolicUnknownValue(_variable.currentValue(), _variable.type(), _context);
|
2018-11-22 13:48:31 +00:00
|
|
|
}
|
|
|
|
|
2019-07-03 14:05:56 +00:00
|
|
|
void setSymbolicUnknownValue(Expression _expr, solidity::TypePointer const& _type, EncodingContext& _context)
|
2018-11-22 13:48:31 +00:00
|
|
|
{
|
2019-04-12 12:44:18 +00:00
|
|
|
solAssert(_type, "");
|
2019-03-06 00:10:43 +00:00
|
|
|
if (isEnum(_type->category()))
|
|
|
|
{
|
2019-05-09 10:16:52 +00:00
|
|
|
auto enumType = dynamic_cast<solidity::EnumType const*>(_type);
|
2019-03-06 00:10:43 +00:00
|
|
|
solAssert(enumType, "");
|
2019-07-03 14:05:56 +00:00
|
|
|
_context.addAssertion(_expr >= 0);
|
|
|
|
_context.addAssertion(_expr < enumType->numberOfMembers());
|
2019-03-06 00:10:43 +00:00
|
|
|
}
|
|
|
|
else if (isInteger(_type->category()))
|
2018-11-22 13:48:31 +00:00
|
|
|
{
|
2019-05-09 10:16:52 +00:00
|
|
|
auto intType = dynamic_cast<solidity::IntegerType const*>(_type);
|
2018-11-22 13:48:31 +00:00
|
|
|
solAssert(intType, "");
|
2019-07-03 14:05:56 +00:00
|
|
|
_context.addAssertion(_expr >= minValue(*intType));
|
|
|
|
_context.addAssertion(_expr <= maxValue(*intType));
|
2018-11-22 13:48:31 +00:00
|
|
|
}
|
|
|
|
}
|
2019-05-09 10:16:52 +00:00
|
|
|
|
|
|
|
}
|
|
|
|
}
|
|
|
|
}
|