Merge pull request #6055 from ethereum/smt_arrays

[SMTChecker] Add support to arrays
This commit is contained in:
chriseth 2019-03-06 18:00:23 +01:00 committed by GitHub
commit cdf29277f7
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
39 changed files with 548 additions and 29 deletions

View File

@ -4,6 +4,7 @@ Language Features:
Compiler Features:
* SMTChecker: Support one-dimensional arrays.
Bugfixes:

View File

@ -535,13 +535,6 @@ void SMTChecker::visitGasLeft(FunctionCall const& _funCall)
m_interface->addAssertion(symbolicVar->currentValue() <= symbolicVar->valueAtIndex(index - 1));
}
void SMTChecker::eraseArrayKnowledge()
{
for (auto const& var: m_variables)
if (var.first->annotation().type->category() == Type::Category::Mapping)
newValue(*var.first);
}
void SMTChecker::inlineFunctionCall(FunctionCall const& _funCall)
{
FunctionDefinition const* _funDef = nullptr;
@ -698,17 +691,26 @@ void SMTChecker::endVisit(Literal const& _literal)
solAssert(_literal.annotation().type, "Expected type for AST node");
Type const& type = *_literal.annotation().type;
if (isNumber(type.category()))
defineExpr(_literal, smt::Expression(type.literalValue(&_literal)));
else if (isBool(type.category()))
defineExpr(_literal, smt::Expression(_literal.token() == Token::TrueLiteral ? true : false));
else
{
if (type.category() == Type::Category::StringLiteral)
{
auto stringType = make_shared<ArrayType>(DataLocation::Memory, true);
auto stringLit = dynamic_cast<StringLiteralType const*>(_literal.annotation().type.get());
solAssert(stringLit, "");
auto result = newSymbolicVariable(*stringType, stringLit->richIdentifier(), *m_interface);
m_expressions.emplace(&_literal, result.second);
}
m_errorReporter.warning(
_literal.location(),
"Assertion checker does not yet support the type of this literal (" +
_literal.annotation().type->toString() +
")."
);
}
}
void SMTChecker::endVisit(Return const& _return)
@ -796,7 +798,6 @@ void SMTChecker::endVisit(IndexAccess const& _indexAccess)
void SMTChecker::arrayAssignment()
{
m_arrayAssignmentHappened = true;
eraseArrayKnowledge();
}
void SMTChecker::arrayIndexAssignment(Assignment const& _assignment)
@ -806,12 +807,48 @@ void SMTChecker::arrayIndexAssignment(Assignment const& _assignment)
{
auto const& varDecl = dynamic_cast<VariableDeclaration const&>(*id->annotation().referencedDeclaration);
solAssert(knownVariable(varDecl), "");
if (varDecl.hasReferenceOrMappingType())
resetVariables([&](VariableDeclaration const& _var) {
if (_var == varDecl)
return false;
TypePointer prefix = _var.type();
TypePointer originalType = typeWithoutPointer(varDecl.type());
while (
prefix->category() == Type::Category::Mapping ||
prefix->category() == Type::Category::Array
)
{
if (*originalType == *typeWithoutPointer(prefix))
return true;
if (prefix->category() == Type::Category::Mapping)
{
auto mapPrefix = dynamic_cast<MappingType const*>(prefix.get());
solAssert(mapPrefix, "");
prefix = mapPrefix->valueType();
}
else
{
auto arrayPrefix = dynamic_cast<ArrayType const*>(prefix.get());
solAssert(arrayPrefix, "");
prefix = arrayPrefix->baseType();
}
}
return false;
});
smt::Expression store = smt::Expression::store(
m_variables[&varDecl]->currentValue(),
expr(*indexAccess.indexExpression()),
expr(_assignment.rightHandSide())
);
m_interface->addAssertion(newValue(varDecl) == store);
// Update the SMT select value after the assignment,
// necessary for sound models.
defineExpr(indexAccess, smt::Expression::select(
m_variables[&varDecl]->currentValue(),
expr(*indexAccess.indexExpression())
));
}
else if (dynamic_cast<IndexAccess const*>(&indexAccess.baseExpression()))
m_errorReporter.warning(
@ -1310,6 +1347,13 @@ void SMTChecker::resetVariables(function<bool(VariableDeclaration const&)> const
});
}
TypePointer SMTChecker::typeWithoutPointer(TypePointer const& _type)
{
if (auto refType = dynamic_cast<ReferenceType const*>(_type.get()))
return ReferenceType::copyForLocationIfReference(refType->location(), _type);
return _type;
}
void SMTChecker::mergeVariables(vector<VariableDeclaration const*> const& _variables, smt::Expression const& _condition, VariableIndices const& _indicesEndTrue, VariableIndices const& _indicesEndFalse)
{
set<VariableDeclaration const*> uniqueVars(_variables.begin(), _variables.end());

View File

@ -103,8 +103,6 @@ private:
void arrayAssignment();
/// Handles assignment to SMT array index.
void arrayIndexAssignment(Assignment const& _assignment);
/// Erases information about SMT arrays.
void eraseArrayKnowledge();
/// Division expression in the given type. Requires special treatment because
/// of rounding for signed division.
@ -177,6 +175,9 @@ private:
void resetStorageReferences();
void resetVariables(std::vector<VariableDeclaration const*> _variables);
void resetVariables(std::function<bool(VariableDeclaration const&)> const& _filter);
/// @returns the type without storage pointer information if it has it.
TypePointer typeWithoutPointer(TypePointer const& _type);
/// Given two different branches and the touched variables,
/// merge the touched variables into after-branch ite variables
/// using the branch condition as guard.

View File

@ -57,8 +57,13 @@ smt::SortPointer dev::solidity::smtSort(Type const& _type)
solAssert(mapType, "");
return make_shared<smt::ArraySort>(smtSort(*mapType->keyType()), smtSort(*mapType->valueType()));
}
// TODO Solidity array
return make_shared<smt::Sort>(smt::Kind::Int);
else
{
solAssert(isArray(_type.category()), "");
auto arrayType = dynamic_cast<ArrayType const*>(&_type);
solAssert(arrayType, "");
return make_shared<smt::ArraySort>(make_shared<smt::Sort>(smt::Kind::Int), smtSort(*arrayType->baseType()));
}
}
default:
// Abstract case.
@ -82,7 +87,7 @@ smt::Kind dev::solidity::smtKind(Type::Category _category)
return smt::Kind::Bool;
else if (isFunction(_category))
return smt::Kind::Function;
else if (isMapping(_category))
else if (isMapping(_category) || isArray(_category))
return smt::Kind::Array;
// Abstract case.
return smt::Kind::Int;
@ -92,7 +97,8 @@ bool dev::solidity::isSupportedType(Type::Category _category)
{
return isNumber(_category) ||
isBool(_category) ||
isMapping(_category);
isMapping(_category) ||
isArray(_category);
}
bool dev::solidity::isSupportedTypeDeclaration(Type::Category _category)
@ -140,6 +146,8 @@ pair<bool, shared_ptr<SymbolicVariable>> dev::solidity::newSymbolicVariable(
}
else if (isMapping(_type.category()))
var = make_shared<SymbolicMappingVariable>(type, _uniqueName, _solver);
else if (isArray(_type.category()))
var = make_shared<SymbolicArrayVariable>(type, _uniqueName, _solver);
else
solAssert(false, "");
return make_pair(abstract, var);
@ -198,6 +206,11 @@ bool dev::solidity::isMapping(Type::Category _category)
return _category == Type::Category::Mapping;
}
bool dev::solidity::isArray(Type::Category _category)
{
return _category == Type::Category::Array;
}
smt::Expression dev::solidity::minValue(IntegerType const& _type)
{
return smt::Expression(_type.minValue());

View File

@ -48,6 +48,7 @@ bool isNumber(Type::Category _category);
bool isBool(Type::Category _category);
bool isFunction(Type::Category _category);
bool isMapping(Type::Category _category);
bool isArray(Type::Category _category);
/// Returns a new symbolic variable, according to _type.
/// Also returns whether the type is abstract or not,

View File

@ -136,3 +136,13 @@ SymbolicMappingVariable::SymbolicMappingVariable(
{
solAssert(isMapping(m_type->category()), "");
}
SymbolicArrayVariable::SymbolicArrayVariable(
TypePointer _type,
string const& _uniqueName,
smt::SolverInterface& _interface
):
SymbolicVariable(move(_type), _uniqueName, _interface)
{
solAssert(isArray(m_type->category()), "");
}

View File

@ -153,5 +153,18 @@ public:
);
};
/**
* Specialization of SymbolicVariable for Array
*/
class SymbolicArrayVariable: public SymbolicVariable
{
public:
SymbolicArrayVariable(
TypePointer _type,
std::string const& _uniqueName,
smt::SolverInterface& _interface
);
};
}
}

View File

@ -7,6 +7,4 @@ contract C
int[3*1] x;
}
// ----
// Warning: (92-100): Assertion checker does not yet support the type of this variable.
// Warning: (149-159): Assertion checker does not yet support the type of this variable.
// Warning: (153-156): Assertion checker does not yet implement this operator on non-integer types.

View File

@ -8,6 +8,5 @@ contract C
}
// ----
// Warning: (86-101): Assertion checker does not yet support this expression.
// Warning: (86-94): Assertion checker does not yet support this global variable.
// Warning: (86-101): Internal error: Expression undefined for SMT solver.
// Warning: (79-106): Assertion violation happens here

View File

@ -0,0 +1,31 @@
pragma experimental SMTChecker;
contract C
{
function f(
uint[] memory a,
uint[] memory b,
uint[][] memory cc,
uint8[][] memory dd,
uint[][][] memory eee
) internal pure {
require(a[0] == 2);
require(cc[0][0] == 50);
require(dd[0][0] == 10);
require(eee[0][0][0] == 50);
b[0] = 1;
// Fails because b == a is possible.
assert(a[0] == 2);
// Fails because b == cc[0] is possible.
assert(cc[0][0] == 50);
// Should not fail since knowledge is erased only for uint[].
assert(dd[0][0] == 10);
// Fails because b == ee[0][0] is possible.
assert(eee[0][0][0] == 50);
assert(b[0] == 1);
}
}
// ----
// Warning: (345-362): Assertion violation happens here
// Warning: (409-431): Assertion violation happens here
// Warning: (571-597): Assertion violation happens here

View File

@ -0,0 +1,18 @@
pragma experimental SMTChecker;
contract C
{
uint[] array;
function f(uint[] memory a, uint[] memory b) internal view {
require(array[0] == 42);
require(a[0] == 2);
b[0] = 1;
// Erasing knowledge about memory references should not
// erase knowledge about state variables.
assert(array[0] == 42);
assert(a[0] == 2);
assert(b[0] == 1);
}
}
// ----
// Warning: (314-331): Assertion violation happens here

View File

@ -0,0 +1,22 @@
pragma experimental SMTChecker;
contract C
{
uint[] array;
function f(uint[] memory a, uint[] memory b) internal view {
require(array[0] == 42);
uint[] storage c = array;
require(a[0] == 2);
b[0] = 1;
// Erasing knowledge about memory references should not
// erase knowledge about state variables.
assert(array[0] == 42);
// Erasing knowledge about memory references should not
// erase knowledge about storage references.
assert(c[0] == 42);
assert(a[0] == 2);
assert(b[0] == 1);
}
}
// ----
// Warning: (469-486): Assertion violation happens here

View File

@ -0,0 +1,45 @@
pragma experimental SMTChecker;
contract C
{
uint[] array;
uint[][] array2d;
uint8[] tinyArray;
function f(
uint[] storage a,
uint[] storage b,
uint[][] storage cc,
uint8[][] storage dd,
uint[][][] storage eee
) internal {
require(a[0] == 2);
require(array[0] == 42);
require(array2d[0][0] == 42);
require(tinyArray[0] == 42);
require(cc[0][0] == 42);
require(dd[0][0] == 42);
require(eee[0][0][0] == 42);
b[0] = 1;
// Fails because b == a is possible.
assert(a[0] == 2);
// Fails because b == array is possible.
assert(array[0] == 42);
// Fails because b == array2d[0] is possible.
assert(array2d[0][0] == 42);
// Should not fail since knowledge is erased only for uint[].
assert(tinyArray[0] == 42);
// Fails because b == cc[0] is possible.
assert(cc[0][0] == 42);
// Should not fail since knowledge is erased only for uint[].
assert(dd[0][0] == 42);
// Fails because b == ee[0][0] is possible.
assert(eee[0][0][0] == 42);
assert(b[0] == 1);
}
}
// ----
// Warning: (489-506): Assertion violation happens here
// Warning: (553-575): Assertion violation happens here
// Warning: (627-654): Assertion violation happens here
// Warning: (795-817): Assertion violation happens here
// Warning: (957-983): Assertion violation happens here

View File

@ -0,0 +1,18 @@
pragma experimental SMTChecker;
contract C
{
function f(uint[] storage a, uint[] storage b, uint[] memory c) internal {
require(c[0] == 42);
require(a[0] == 2);
b[0] = 1;
// Erasing knowledge about storage references should not
// erase knowledge about memory references.
assert(c[0] == 42);
// Fails because b == a is possible.
assert(a[0] == 2);
assert(b[0] == 1);
}
}
// ----
// Warning: (347-364): Assertion violation happens here

View File

@ -0,0 +1,22 @@
pragma experimental SMTChecker;
contract C
{
function f(uint[] storage a, uint[] storage b, uint[] memory c) internal {
uint[] memory d = c;
require(c[0] == 42);
require(a[0] == 2);
b[0] = 1;
// Erasing knowledge about storage references should not
// erase knowledge about memory references.
assert(c[0] == 42);
// Erasing knowledge about storage references should not
// erase knowledge about memory references.
assert(d[0] == 42);
// Fails because b == a is possible.
assert(a[0] == 2);
assert(b[0] == 1);
}
}
// ----
// Warning: (497-514): Assertion violation happens here

View File

@ -0,0 +1,19 @@
pragma experimental SMTChecker;
contract C
{
uint[] array;
function f(uint[] storage a, uint[] storage b) internal {
require(a[0] == 2);
require(b[0] == 42);
array[0] = 1;
// Fails because array == a is possible.
assert(a[0] == 2);
// Fails because array == b is possible.
assert(b[0] == 42);
assert(array[0] == 1);
}
}
// ----
// Warning: (226-243): Assertion violation happens here
// Warning: (290-308): Assertion violation happens here

View File

@ -0,0 +1,11 @@
pragma experimental SMTChecker;
contract C
{
uint[] array;
function f(uint x, uint y) public {
array[x] = 200;
require(x == y);
assert(array[y] > 100);
}
}

View File

@ -0,0 +1,13 @@
pragma experimental SMTChecker;
contract C
{
uint[] array;
function f(uint x, uint y) public {
array[x] = 200;
require(x == y);
assert(array[y] > 300);
}
}
// ----
// Warning: (137-159): Assertion violation happens here

View File

@ -0,0 +1,11 @@
pragma experimental SMTChecker;
contract C
{
uint[][] array;
function f(uint x, uint y, uint z, uint t) public view {
require(array[x][y] == 200);
require(x == z && y == t);
assert(array[z][t] > 100);
}
}

View File

@ -0,0 +1,13 @@
pragma experimental SMTChecker;
contract C
{
uint[][] array;
function f(uint x, uint y, uint z, uint t) public view {
require(array[x][y] == 200);
require(x == z && y == t);
assert(array[z][t] > 300);
}
}
// ----
// Warning: (183-208): Assertion violation happens here

View File

@ -0,0 +1,11 @@
pragma experimental SMTChecker;
contract C
{
uint[][][] array;
function f(uint x, uint y, uint z, uint t, uint w, uint v) public view {
require(array[x][y][z] == 200);
require(x == t && y == w && z == v);
assert(array[t][w][v] > 100);
}
}

View File

@ -0,0 +1,13 @@
pragma experimental SMTChecker;
contract C
{
uint[][][] array;
function f(uint x, uint y, uint z, uint t, uint w, uint v) public view {
require(array[x][y][z] == 200);
require(x == t && y == w && z == v);
assert(array[t][w][v] > 300);
}
}
// ----
// Warning: (214-242): Assertion violation happens here

View File

@ -0,0 +1,10 @@
pragma experimental SMTChecker;
contract C
{
function f(uint[] memory array, uint x, uint y) public pure {
array[x] = 200;
require(x == y);
assert(array[y] > 100);
}
}

View File

@ -0,0 +1,12 @@
pragma experimental SMTChecker;
contract C
{
function f(uint[] memory array, uint x, uint y) public pure {
array[x] = 200;
require(x == y);
assert(array[y] > 300);
}
}
// ----
// Warning: (148-170): Assertion violation happens here

View File

@ -0,0 +1,12 @@
pragma experimental SMTChecker;
contract C
{
function f() public pure {
uint[3] memory array = [uint(1), 2, 3];
}
}
// ----
// Warning: (76-96): Unused local variable.
// Warning: (99-114): Assertion checker does not yet implement tuples and inline arrays.
// Warning: (99-114): Internal error: Expression undefined for SMT solver.

View File

@ -0,0 +1,24 @@
pragma experimental SMTChecker;
contract C
{
mapping (uint => uint) singleMap;
mapping (uint => uint)[] severalMaps;
mapping (uint => uint8)[] severalMaps8;
mapping (uint => uint)[][] severalMaps3d;
function f(mapping (uint => uint) storage map) internal {
require(severalMaps[0][0] == 42);
require(severalMaps8[0][0] == 42);
require(severalMaps3d[0][0][0] == 42);
map[0] = 2;
// Should fail since map == severalMaps[0] is possible.
assert(severalMaps[0][0] == 42);
// Should not fail since knowledge is erase only for mapping (uint => uint).
assert(severalMaps8[0][0] == 42);
// Should fail since map == severalMaps3d[0][0] is possible.
assert(severalMaps3d[0][0][0] == 42);
}
}
// ----
// Warning: (451-482): Assertion violation happens here
// Warning: (664-700): Assertion violation happens here

View File

@ -0,0 +1,11 @@
pragma experimental SMTChecker;
contract C
{
uint[10] array;
function f(uint x, uint y) public {
array[x] = 200;
require(x == y);
assert(array[y] > 100);
}
}

View File

@ -0,0 +1,13 @@
pragma experimental SMTChecker;
contract C
{
uint[10] array;
function f(uint x, uint y) public {
array[x] = 200;
require(x == y);
assert(array[y] > 300);
}
}
// ----
// Warning: (139-161): Assertion violation happens here

View File

@ -0,0 +1,11 @@
pragma experimental SMTChecker;
contract C
{
uint[10][20] array;
function f(uint x, uint y, uint z, uint t) public view {
require(array[x][y] == 200);
require(x == z && y == t);
assert(array[z][t] > 100);
}
}

View File

@ -0,0 +1,13 @@
pragma experimental SMTChecker;
contract C
{
uint[10][20] array;
function f(uint x, uint y, uint z, uint t) public view {
require(array[x][y] == 200);
require(x == z && y == t);
assert(array[z][t] > 300);
}
}
// ----
// Warning: (187-212): Assertion violation happens here

View File

@ -0,0 +1,11 @@
pragma experimental SMTChecker;
contract C
{
uint[10][20][30] array;
function f(uint x, uint y, uint z, uint t, uint w, uint v) public view {
require(array[x][y][z] == 200);
require(x == t && y == w && z == v);
assert(array[t][w][v] > 100);
}
}

View File

@ -0,0 +1,13 @@
pragma experimental SMTChecker;
contract C
{
uint[10][20][30] array;
function f(uint x, uint y, uint z, uint t, uint w, uint v) public view {
require(array[x][y][z] == 200);
require(x == t && y == w && z == v);
assert(array[t][w][v] > 300);
}
}
// ----
// Warning: (220-248): Assertion violation happens here

View File

@ -9,8 +9,3 @@ contract C
}
// ----
// Warning: (113-127): Unused local variable.
// Warning: (113-127): Assertion checker does not yet support the type of this variable.
// Warning: (58-72): Assertion checker does not yet support the type of this variable.
// Warning: (95-107): Assertion checker does not yet support the type of this variable.
// Warning: (130-131): Internal error: Expression undefined for SMT solver.
// Warning: (130-131): Assertion checker does not yet implement this type.

View File

@ -0,0 +1,9 @@
pragma experimental SMTChecker;
contract C
{
function f(bytes memory b1, bytes memory b2) public pure {
b1 = b2;
assert(b1[1] == b2[1]);
}
}

View File

@ -0,0 +1,11 @@
pragma experimental SMTChecker;
contract C
{
function f(bytes memory b1, bytes memory b2) public pure {
b1 = b2;
assert(b1[1] == b2[2]);
}
}
// ----
// Warning: (119-141): Assertion violation happens here

View File

@ -0,0 +1,28 @@
pragma experimental SMTChecker;
contract C
{
mapping (uint => uint) a;
mapping (uint => mapping (uint => uint)) maps;
mapping (uint => mapping (uint => uint8)) maps8;
function f(mapping (uint => uint) storage map1, mapping (uint => uint) storage map2) internal {
require(map1[0] == 2);
require(a[0] == 42);
require(maps[0][0] == 42);
require(maps8[0][0] == 42);
map2[0] = 1;
// Fails because map2 == map1 is possible.
assert(map1[0] == 2);
// Fails because map2 == a is possible.
assert(a[0] == 42);
// Fails because map2 == maps[0] is possible.
assert(maps[0][0] == 42);
// Should not fail since knowledge is erased only for mapping (uint => uint).
assert(maps8[0][0] == 42);
assert(map2[0] == 1);
}
}
// ----
// Warning: (437-457): Assertion violation happens here
// Warning: (503-521): Assertion violation happens here
// Warning: (573-597): Assertion violation happens here

View File

@ -9,9 +9,3 @@ contract C
}
}
// ----
// Warning: (89-104): Assertion checker does not yet support the type of this variable.
// Warning: (129-130): Internal error: Expression undefined for SMT solver.
// Warning: (129-130): Assertion checker does not yet implement this type.
// Warning: (155-156): Internal error: Expression undefined for SMT solver.
// Warning: (155-156): Assertion checker does not yet implement this type.
// Warning: (139-158): Assertion violation happens here

View File

@ -0,0 +1,14 @@
pragma experimental SMTChecker;
contract C
{
function f(string memory s1, string memory s2) public pure {
assert(bytes(s1).length == bytes(s2).length);
}
}
// ----
// Warning: (117-133): Assertion checker does not yet support this expression.
// Warning: (137-153): Assertion checker does not yet support this expression.
// Warning: (117-133): Internal error: Expression undefined for SMT solver.
// Warning: (137-153): Internal error: Expression undefined for SMT solver.
// Warning: (110-154): Assertion violation happens here

View File

@ -0,0 +1,11 @@
pragma experimental SMTChecker;
contract C
{
function f() public pure {
string memory s = "Hello World";
}
}
// ----
// Warning: (76-91): Unused local variable.
// Warning: (94-107): Assertion checker does not yet support the type of this literal (literal_string "Hello World").