[SMTChecker] Fix tuple name for arrays

This commit is contained in:
Leonardo Alt 2020-07-27 16:55:54 +02:00
parent 241a564fca
commit ec31d971e6
8 changed files with 64 additions and 6 deletions

View File

@ -10,6 +10,7 @@ Compiler Features:
Bugfixes:
* Optimizer: Keep side-effects of ``x`` in ``byte(a, shr(b, x))`` even if the constants ``a`` and ``b`` would make the expression zero unconditionally. This optimizer rule is very hard if not impossible to trigger in a way that it can result in invalid code, though.
* SMTChecker: Fix internal error in BMC function inlining.
* SMTChecker: Fix internal error on array implicit conversion.
* SMTChecker: Fix internal error on fixed bytes index access.
* References Resolver: Fix internal bug when using constructor for library.

View File

@ -92,13 +92,35 @@ SortPointer smtSort(frontend::Type const& _type)
string tupleName;
if (
auto arrayType = dynamic_cast<ArrayType const*>(&_type);
(arrayType && arrayType->isString()) ||
(arrayType && (arrayType->isString() || arrayType->isByteArray())) ||
_type.category() == frontend::Type::Category::ArraySlice ||
_type.category() == frontend::Type::Category::StringLiteral
)
tupleName = "bytes_tuple";
tupleName = "bytes";
else if (auto arrayType = dynamic_cast<ArrayType const*>(&_type))
{
auto baseType = arrayType->baseType();
// Solidity allows implicit conversion also when assigning arrays.
// So if the base type potentially has a size, that size cannot go
// in the tuple's name.
if (auto tupleSort = dynamic_pointer_cast<TupleSort>(array->range))
tupleName = tupleSort->name;
else if (
baseType->category() == frontend::Type::Category::Integer ||
baseType->category() == frontend::Type::Category::FixedPoint
)
tupleName = "uint";
else if (baseType->category() == frontend::Type::Category::FixedBytes)
tupleName = "fixedbytes";
else
tupleName = arrayType->baseType()->toString(true);
tupleName += "[]";
}
else
tupleName = _type.toString(true) + "_tuple";
tupleName = _type.toString(true);
tupleName += "_tuple";
return make_shared<TupleSort>(
tupleName,

View File

@ -20,6 +20,9 @@ contract LoopFor2 {
assert(b[0] == 900);
}
}
// ====
// SMTSolvers: cvc4
// ----
// Warning 6328: (320-339): Assertion violation happens here
// Warning 6328: (343-362): Assertion violation happens here.
// Warning 4661: (296-316): Assertion violation happens here
// Warning 4661: (320-339): Assertion violation happens here
// Warning 4661: (343-362): Assertion violation happens here

View File

@ -26,4 +26,4 @@ contract C
}
}
// ----
// Warning 6328: (400-457): Assertion violation happens here
// Warning 6328: (400-457): Assertion violation happens here.

View File

@ -0,0 +1,7 @@
pragma experimental SMTChecker;
contract C {
uint[][] a;
function f(uint[1] memory x) public {
a.push(x);
}
}

View File

@ -0,0 +1,7 @@
pragma experimental SMTChecker;
contract C {
uint[][] a;
function f(uint[1][] memory x) public {
a.push(x[2]);
}
}

View File

@ -0,0 +1,9 @@
pragma experimental SMTChecker;
contract D {
bytes16[] inner;
bytes32[][] data;
function t() public {
data.push(inner);
}
}

View File

@ -0,0 +1,9 @@
pragma experimental SMTChecker;
contract D {
int16[] inner;
int[][] data;
function t() public {
data.push(inner);
}
}