cerc-io/solidity
16
0
Fork 0
mirror of https://github.com/ethereum/solidity synced 2023-10-03 13:03:40 +00:00
Code Issues Actions Packages Projects Releases Wiki Activity

Merge pull request #8611 from ethereum/smt_array_variable_sort

Browse Source 
[SMTChecker] Allow constructing symbolic arrays from smt sort
This commit is contained in:
Leonardo 2020-04-06 12:26:30 +02:00 committed by GitHub
commit 0a72a3b8af
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
2 changed files with 22 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

13
libsolidity/formal/SymbolicVariables.cpp
View File

@ -218,15 +218,28 @@ SymbolicArrayVariable::SymbolicArrayVariable(
solAssert(isArray(m_type->category()), ""); solAssert(isArray(m_type->category()), "");
} }
SymbolicArrayVariable::SymbolicArrayVariable(
SortPointer _sort,
string _uniqueName,
EncodingContext& _context
):
SymbolicVariable(move(_sort), move(_uniqueName), _context)
{
solAssert(m_sort->kind == Kind::Array, "");
}
smt::Expression SymbolicArrayVariable::currentValue(frontend::TypePointer const& _targetType) const smt::Expression SymbolicArrayVariable::currentValue(frontend::TypePointer const& _targetType) const
{ {
if (_targetType) if (_targetType)
{
solAssert(m_originalType, "");
// StringLiterals are encoded as SMT arrays in the generic case, // StringLiterals are encoded as SMT arrays in the generic case,
// but they can also be compared/assigned to fixed bytes, in which // but they can also be compared/assigned to fixed bytes, in which
// case they'd need to be encoded as numbers. // case they'd need to be encoded as numbers.
if (auto strType = dynamic_cast<StringLiteralType const*>(m_originalType)) if (auto strType = dynamic_cast<StringLiteralType const*>(m_originalType))
if (_targetType->category() == frontend::Type::Category::FixedBytes) if (_targetType->category() == frontend::Type::Category::FixedBytes)
return smt::Expression(u256(toHex(util::asBytes(strType->value()), util::HexPrefix::Add))); return smt::Expression(u256(toHex(util::asBytes(strType->value()), util::HexPrefix::Add)));
}
return SymbolicVariable::currentValue(_targetType); return SymbolicVariable::currentValue(_targetType);
} }

9
libsolidity/formal/SymbolicVariables.h
View File

@ -47,6 +47,8 @@ public:
EncodingContext& _context EncodingContext& _context
); );
SymbolicVariable(SymbolicVariable&&) = default;
virtual ~SymbolicVariable() = default; virtual ~SymbolicVariable() = default;
virtual Expression currentValue(frontend::TypePointer const& _targetType = TypePointer{}) const; virtual Expression currentValue(frontend::TypePointer const& _targetType = TypePointer{}) const;
@ -212,6 +214,13 @@ public:
std::string _uniqueName, std::string _uniqueName,
EncodingContext& _context EncodingContext& _context
); );
SymbolicArrayVariable(
SortPointer _sort,
std::string _uniqueName,
EncodingContext& _context
);
SymbolicArrayVariable(SymbolicArrayVariable&&) = default;
Expression currentValue(frontend::TypePointer const& _targetType = TypePointer{}) const override; Expression currentValue(frontend::TypePointer const& _targetType = TypePointer{}) const override;
}; };