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 #9049 from ethereum/smt_fix_fp

Browse Source 
[SMTChecker] Fix fixed point inc/dec
This commit is contained in:
Leonardo 2020-05-28 13:13:23 +02:00 committed by GitHub
commit 097954bc80
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
4 changed files with 12 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
Changelog.md
View File

@ -24,6 +24,7 @@ Bugfixes:
* NatSpec: DocString block is terminated when encountering an empty line. * NatSpec: DocString block is terminated when encountering an empty line.
* Scanner: Fix bug when two empty NatSpec comments lead to scanning past EOL. * Scanner: Fix bug when two empty NatSpec comments lead to scanning past EOL.
* Code Generator: Trigger proper unimplemented errors on certain array copy operations. * Code Generator: Trigger proper unimplemented errors on certain array copy operations.
* SMTChecker: Fix internal error when applying arithmetic operators to fixed point variables.
### 0.6.8 (2020-05-14) ### 0.6.8 (2020-05-14)

7
libsolidity/formal/SMTEncoder.cpp
View File

@ -463,9 +463,6 @@ void SMTEncoder::endVisit(UnaryOperation const& _op)
createExpr(_op); createExpr(_op);
if (_op.annotation().type->category() == Type::Category::FixedPoint)
return;
switch (_op.getOperator()) switch (_op.getOperator())
{ {
case Token::Not: // ! case Token::Not: // !
@ -477,8 +474,8 @@ void SMTEncoder::endVisit(UnaryOperation const& _op)
case Token::Inc: // ++ (pre- or postfix) case Token::Inc: // ++ (pre- or postfix)
case Token::Dec: // -- (pre- or postfix) case Token::Dec: // -- (pre- or postfix)
{ {
auto cat = _op.annotation().type->category();
solAssert(smt::isInteger(_op.annotation().type->category()), ""); solAssert(smt::isInteger(cat) || smt::isFixedPoint(cat), "");
solAssert(_op.subExpression().annotation().willBeWrittenTo, ""); solAssert(_op.subExpression().annotation().willBeWrittenTo, "");
if (auto identifier = dynamic_cast<Identifier const*>(&_op.subExpression())) if (auto identifier = dynamic_cast<Identifier const*>(&_op.subExpression()))
{ {

8
libsolidity/formal/SymbolicTypes.cpp
View File

@ -224,6 +224,8 @@ pair<bool, shared_ptr<SymbolicVariable>> newSymbolicVariable(
} }
else if (isInteger(_type.category())) else if (isInteger(_type.category()))
var = make_shared<SymbolicIntVariable>(type, type, _uniqueName, _context); var = make_shared<SymbolicIntVariable>(type, type, _uniqueName, _context);
else if (isFixedPoint(_type.category()))
var = make_shared<SymbolicIntVariable>(type, type, _uniqueName, _context);
else if (isFixedBytes(_type.category())) else if (isFixedBytes(_type.category()))
{ {
auto fixedBytesType = dynamic_cast<frontend::FixedBytesType const*>(type); auto fixedBytesType = dynamic_cast<frontend::FixedBytesType const*>(type);
@ -272,6 +274,11 @@ bool isInteger(frontend::Type::Category _category)
return _category == frontend::Type::Category::Integer; return _category == frontend::Type::Category::Integer;
} }
bool isFixedPoint(frontend::Type::Category _category)
{
return _category == frontend::Type::Category::FixedPoint;
}
bool isRational(frontend::Type::Category _category) bool isRational(frontend::Type::Category _category)
{ {
return _category == frontend::Type::Category::RationalNumber; return _category == frontend::Type::Category::RationalNumber;
@ -300,6 +307,7 @@ bool isEnum(frontend::Type::Category _category)
bool isNumber(frontend::Type::Category _category) bool isNumber(frontend::Type::Category _category)
{ {
return isInteger(_category) || return isInteger(_category) ||
isFixedPoint(_category) ||
isRational(_category) || isRational(_category) ||
isFixedBytes(_category) || isFixedBytes(_category) ||
isAddress(_category) || isAddress(_category) ||

1
libsolidity/formal/SymbolicTypes.h
View File

@ -43,6 +43,7 @@ bool isSupportedTypeDeclaration(frontend::Type::Category _category);
bool isSupportedTypeDeclaration(frontend::Type const& _type); bool isSupportedTypeDeclaration(frontend::Type const& _type);
bool isInteger(frontend::Type::Category _category); bool isInteger(frontend::Type::Category _category);
bool isFixedPoint(frontend::Type::Category _category);
bool isRational(frontend::Type::Category _category); bool isRational(frontend::Type::Category _category);
bool isFixedBytes(frontend::Type::Category _category); bool isFixedBytes(frontend::Type::Category _category);
bool isAddress(frontend::Type::Category _category); bool isAddress(frontend::Type::Category _category);