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 #10095 from ethereum/smt_fix_conditional

Browse Source 
[SMTChecker] Fix ICE on conditional with tuples of rationals
This commit is contained in:
Harikrishnan Mulackal 2020-10-26 10:15:26 +01:00 committed by GitHub
commit 07e3f60ffc
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
5 changed files with 38 additions and 6 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
Changelog.md
View File

@ -8,6 +8,7 @@ Compiler Features:
Bugfixes:
* SMTChecker: Fix lack of reporting potential violations when using only the CHC engine.
* SMTChecker: Fix internal error on conversion from string literal to byte.
* SMTChecker: Fix internal error when using tuples of rational literals inside the conditional operator.
* Code generator: Fix missing creation dependency tracking for abstract contracts.

4
libsolidity/formal/SMTEncoder.cpp
View File

@ -574,8 +574,8 @@ bool SMTEncoder::visit(Conditional const& _op)
defineExpr(_op, smtutil::Expression::ite(
expr(_op.condition()),
expr(_op.trueExpression()),
expr(_op.falseExpression())
expr(_op.trueExpression(), _op.annotation().type),
expr(_op.falseExpression(), _op.annotation().type)
));
return false;

22
libsolidity/formal/SymbolicVariables.cpp
View File

@ -245,7 +245,25 @@ SymbolicTupleVariable::SymbolicTupleVariable(
solAssert(m_sort->kind == Kind::Tuple, "");
}
vector<SortPointer> const& SymbolicTupleVariable::components()
smtutil::Expression SymbolicTupleVariable::currentValue(frontend::TypePointer const& _targetType) const
{
if (!_targetType || sort() == smtSort(*_targetType))
return SymbolicVariable::currentValue();
auto thisTuple = dynamic_pointer_cast<TupleSort>(sort());
auto otherTuple = dynamic_pointer_cast<TupleSort>(smtSort(*_targetType));
solAssert(thisTuple && otherTuple, "");
solAssert(thisTuple->components.size() == otherTuple->components.size(), "");
vector<smtutil::Expression> args;
for (size_t i = 0; i < thisTuple->components.size(); ++i)
args.emplace_back(component(i, type(), _targetType));
return smtutil::Expression::tuple_constructor(
smtutil::Expression(make_shared<smtutil::SortSort>(smtSort(*_targetType)), ""),
args
);
}
vector<SortPointer> const& SymbolicTupleVariable::components() const
{
auto tupleSort = dynamic_pointer_cast<TupleSort>(m_sort);
solAssert(tupleSort, "");
@ -256,7 +274,7 @@ smtutil::Expression SymbolicTupleVariable::component(
size_t _index,
TypePointer _fromType,
TypePointer _toType
)
) const
{
optional<smtutil::Expression> conversion = symbolicTypeConversion(_fromType, _toType);
if (conversion)

6
libsolidity/formal/SymbolicVariables.h
View File

@ -225,12 +225,14 @@ public:
EncodingContext& _context
);
std::vector<smtutil::SortPointer> const& components();
smtutil::Expression currentValue(frontend::TypePointer const& _targetType = TypePointer{}) const override;
std::vector<smtutil::SortPointer> const& components() const;
smtutil::Expression component(
size_t _index,
TypePointer _fromType = nullptr,
TypePointer _toType = nullptr
);
) const;
};
/**

11
test/libsolidity/smtCheckerTests/operators/tuple_rationals_conditional.sol Normal file
View File

@ -0,0 +1,11 @@
pragma experimental SMTChecker;
contract C {
function f(bool x) public pure {
(uint a, uint b) = x ? (10000000001, 2) : (3, 4);
assert(a != 0);
assert(b != 0);
assert(a % 2 == 1);
assert(b % 2 == 0);
}
}