cerc-io/solidity
11
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

[SMTChecker] Handle InaccessibleDynamicType

Browse Source
This commit is contained in:
Martin Blicha
2021-03-24 11:53:06 +01:00
parent a27c9c39b2
commit 852e877ae7
8 changed files with 65 additions and 6 deletions
Download Patch File Download Diff File Expand all files Collapse all files
libsolidity/formal/SMTEncoder.cpp
+8 -6
View File
@@ -2443,14 +2443,13 @@ void SMTEncoder::createExpr(Expression const& _e)
void SMTEncoder::defineExpr(Expression const& _e, smtutil::Expression _value)
{
auto type = _e.annotation().type;
createExpr(_e);
solAssert(_value.sort->kind != smtutil::Kind::Function, "Equality operator applied to type that is not fully supported");
m_context.addAssertion(expr(_e) == _value);
if (!smt::isInaccessibleDynamic(*type))
m_context.addAssertion(expr(_e) == _value);
if (
auto type = _e.annotation().type;
m_checked && smt::isNumber(*type)
)
if (m_checked && smt::isNumber(*type))
m_context.addAssertion(smtutil::Expression::implies(
currentPathConditions(),
smt::symbolicUnknownConstraints(expr(_e), type)
@@ -2469,8 +2468,11 @@ void SMTEncoder::defineExpr(Expression const& _e, vector<optional<smtutil::Expre
symbTuple->increaseIndex();
auto const& symbComponents = symbTuple->components();
solAssert(symbComponents.size() == _values.size(), "");
auto tupleType = dynamic_cast<TupleType const*>(_e.annotation().type);
solAssert(tupleType, "");
solAssert(tupleType->components().size() == symbComponents.size(), "");
for (unsigned i = 0; i < symbComponents.size(); ++i)
if (_values[i])
if (_values[i] && !smt::isInaccessibleDynamic(*tupleType->components()[i]))
m_context.addAssertion(symbTuple->component(i) == *_values[i]);
}
libsolidity/formal/SymbolicTypes.cpp
+5
View File
@@ -386,6 +386,11 @@ bool isNonRecursiveStruct(frontend::Type const& _type)
return structType && !structType->recursive();
}
bool isInaccessibleDynamic(frontend::Type const& _type)
{
return _type.category() == frontend::Type::Category::InaccessibleDynamic;
}
smtutil::Expression minValue(frontend::IntegerType const& _type)
{
return smtutil::Expression(_type.minValue());
libsolidity/formal/SymbolicTypes.h
+1
View File
@@ -59,6 +59,7 @@ bool isArray(frontend::Type const& _type);
bool isTuple(frontend::Type const& _type);
bool isStringLiteral(frontend::Type const& _type);
bool isNonRecursiveStruct(frontend::Type const& _type);
bool isInaccessibleDynamic(frontend::Type const& _type);
/// Returns a new symbolic variable, according to _type.
/// Also returns whether the type is abstract or not,