Merge pull request #10360 from blishko/struct_constructor

[SMTChecker] Adding support for struct constructor
This commit is contained in:
Leonardo 2020-11-23 12:56:10 -01:00 committed by GitHub
commit cbfd47cc9a
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
18 changed files with 165 additions and 52 deletions

View File

@ -2,7 +2,7 @@
Compiler Features: Compiler Features:
* SMTChecker: Support named arguments in function calls. * SMTChecker: Support named arguments in function calls.
* SMTChecker: Support struct constructor.
### 0.7.5 (2020-11-18) ### 0.7.5 (2020-11-18)

View File

@ -622,11 +622,7 @@ void SMTEncoder::endVisit(FunctionCall const& _funCall)
createExpr(_funCall); createExpr(_funCall);
if (functionCallKind == FunctionCallKind::StructConstructorCall) if (functionCallKind == FunctionCallKind::StructConstructorCall)
{ {
m_errorReporter.warning( visitStructConstructorCall(_funCall);
4639_error,
_funCall.location(),
"Assertion checker does not yet implement this expression."
);
return; return;
} }
@ -861,6 +857,12 @@ void SMTEncoder::endVisit(Identifier const& _identifier)
defineExpr(_identifier, m_context.state().thisAddress()); defineExpr(_identifier, m_context.state().thisAddress());
m_uninterpretedTerms.insert(&_identifier); m_uninterpretedTerms.insert(&_identifier);
} }
// Ignore struct type identifiers in struct constructor calls
else if (
auto typetype = dynamic_cast<TypeType const*>(_identifier.annotation().type);
typetype && typetype->actualType()->category() == Type::Category::Struct
)
return;
// Ignore the builtin abi, it is handled in FunctionCall. // Ignore the builtin abi, it is handled in FunctionCall.
// TODO: ignore MagicType in general (abi, block, msg, tx, type) // TODO: ignore MagicType in general (abi, block, msg, tx, type)
else if (auto magicType = dynamic_cast<MagicType const*>(_identifier.annotation().type); magicType && magicType->kind() == MagicType::Kind::ABI) else if (auto magicType = dynamic_cast<MagicType const*>(_identifier.annotation().type); magicType && magicType->kind() == MagicType::Kind::ABI)
@ -1018,6 +1020,13 @@ void SMTEncoder::visitFunctionIdentifier(Identifier const& _identifier)
} }
} }
void SMTEncoder::visitStructConstructorCall(FunctionCall const& _funCall)
{
solAssert(*_funCall.annotation().kind == FunctionCallKind::StructConstructorCall, "");
auto& structSymbolicVar = dynamic_cast<smt::SymbolicStructVariable&>(*m_context.expression(_funCall));
structSymbolicVar.assignAllMembers(applyMap(_funCall.sortedArguments(), [this](auto const& arg) { return expr(*arg); }));
}
void SMTEncoder::endVisit(Literal const& _literal) void SMTEncoder::endVisit(Literal const& _literal)
{ {
solAssert(_literal.annotation().type, "Expected type for AST node"); solAssert(_literal.annotation().type, "Expected type for AST node");

View File

@ -151,6 +151,7 @@ protected:
virtual void visitAddMulMod(FunctionCall const& _funCall); virtual void visitAddMulMod(FunctionCall const& _funCall);
void visitObjectCreation(FunctionCall const& _funCall); void visitObjectCreation(FunctionCall const& _funCall);
void visitTypeConversion(FunctionCall const& _funCall); void visitTypeConversion(FunctionCall const& _funCall);
void visitStructConstructorCall(FunctionCall const& _funCall);
void visitFunctionIdentifier(Identifier const& _identifier); void visitFunctionIdentifier(Identifier const& _identifier);
/// Encodes a modifier or function body according to the modifier /// Encodes a modifier or function body according to the modifier

View File

@ -360,7 +360,7 @@ SymbolicStructVariable::SymbolicStructVariable(
} }
} }
smtutil::Expression SymbolicStructVariable::member(string const& _member) smtutil::Expression SymbolicStructVariable::member(string const& _member) const
{ {
return smtutil::Expression::tuple_get(currentValue(), m_memberIndices.at(_member)); return smtutil::Expression::tuple_get(currentValue(), m_memberIndices.at(_member));
} }
@ -385,3 +385,18 @@ smtutil::Expression SymbolicStructVariable::assignMember(string const& _member,
return currentValue(); return currentValue();
} }
smtutil::Expression SymbolicStructVariable::assignAllMembers(vector<smtutil::Expression> const& _memberValues)
{
auto structType = dynamic_cast<StructType const*>(m_type);
solAssert(structType, "");
auto const& structDef = structType->structDefinition();
auto const& structMembers = structDef.members();
solAssert(_memberValues.size() == structMembers.size(), "");
increaseIndex();
for (unsigned i = 0; i < _memberValues.size(); ++i)
m_context.addAssertion(_memberValues[i] == member(structMembers[i]->name()));
return currentValue();
}

View File

@ -282,12 +282,16 @@ public:
); );
/// @returns the symbolic expression representing _member. /// @returns the symbolic expression representing _member.
smtutil::Expression member(std::string const& _member); smtutil::Expression member(std::string const& _member) const;
/// @returns the symbolic expression representing this struct /// @returns the symbolic expression representing this struct
/// with field _member updated. /// with field _member updated.
smtutil::Expression assignMember(std::string const& _member, smtutil::Expression const& _memberValue); smtutil::Expression assignMember(std::string const& _member, smtutil::Expression const& _memberValue);
/// @returns the symbolic expression representing this struct
/// with all fields updated with the given values.
smtutil::Expression assignAllMembers(std::vector<smtutil::Expression> const& _memberValues);
private: private:
std::map<std::string, unsigned> m_memberIndices; std::map<std::string, unsigned> m_memberIndices;
}; };

View File

@ -1,15 +0,0 @@
pragma experimental SMTChecker;
contract C {
struct A { uint a; uint b; }
function f() public pure returns (uint) {
A memory a = A({ a: 1, b: 2 });
}
}
// ----
// Warning 6321: (117-121): Unnamed return variable can remain unassigned. Add an explicit return with value to all non-reverting code paths or name the variable.
// Warning 2072: (133-143): Unused local variable.
// Warning 8364: (146-147): Assertion checker does not yet implement type type(struct C.A storage pointer)
// Warning 4639: (146-163): Assertion checker does not yet implement this expression.
// Warning 8364: (146-147): Assertion checker does not yet implement type type(struct C.A storage pointer)
// Warning 4639: (146-163): Assertion checker does not yet implement this expression.

View File

@ -8,11 +8,11 @@ contract C {
} }
} }
// ---- // ----
// Warning 8364: (221-222): Assertion checker does not yet implement type type(struct C.S storage pointer)
// Warning 8364: (231-237): Assertion checker does not yet implement type type(uint256[] memory) // Warning 8364: (231-237): Assertion checker does not yet implement type type(uint256[] memory)
// Warning 8364: (231-240): Assertion checker does not yet implement type type(uint256[] memory[2] memory) // Warning 8364: (231-240): Assertion checker does not yet implement type type(uint256[] memory[2] memory)
// Warning 4588: (202-242): Assertion checker does not yet implement this type of function call.
// Warning 8364: (221-222): Assertion checker does not yet implement type type(struct C.S storage pointer) // Warning 8364: (221-222): Assertion checker does not yet implement type type(struct C.S storage pointer)
// Warning 4588: (202-242): Assertion checker does not yet implement this type of function call.
// Warning 8364: (231-237): Assertion checker does not yet implement type type(uint256[] memory) // Warning 8364: (231-237): Assertion checker does not yet implement type type(uint256[] memory)
// Warning 8364: (231-240): Assertion checker does not yet implement type type(uint256[] memory[2] memory) // Warning 8364: (231-240): Assertion checker does not yet implement type type(uint256[] memory[2] memory)
// Warning 8364: (221-222): Assertion checker does not yet implement type type(struct C.S storage pointer)
// Warning 4588: (202-242): Assertion checker does not yet implement this type of function call. // Warning 4588: (202-242): Assertion checker does not yet implement this type of function call.

View File

@ -11,8 +11,4 @@ contract C
} }
} }
// ---- // ----
// Warning 8364: (159-160): Assertion checker does not yet implement type type(struct C.S storage pointer)
// Warning 4639: (159-163): Assertion checker does not yet implement this expression.
// Warning 6838: (140-144): BMC: Condition is always false. // Warning 6838: (140-144): BMC: Condition is always false.
// Warning 8364: (159-160): Assertion checker does not yet implement type type(struct C.S storage pointer)
// Warning 4639: (159-163): Assertion checker does not yet implement this expression.

View File

@ -16,15 +16,7 @@ contract test {
// Warning 6133: (140-144): Statement has no effect. // Warning 6133: (140-144): Statement has no effect.
// Warning 6133: (148-152): Statement has no effect. // Warning 6133: (148-152): Statement has no effect.
// Warning 6133: (156-163): Statement has no effect. // Warning 6133: (156-163): Statement has no effect.
// Warning 8364: (125-126): Assertion checker does not yet implement type type(struct test.s storage pointer)
// Warning 8364: (130-131): Assertion checker does not yet implement type type(struct test.s storage pointer)
// Warning 4639: (130-136): Assertion checker does not yet implement this expression.
// Warning 8364: (140-141): Assertion checker does not yet implement type type(struct test.s storage pointer)
// Warning 8364: (140-144): Assertion checker does not yet implement type type(struct test.s memory[7] memory) // Warning 8364: (140-144): Assertion checker does not yet implement type type(struct test.s memory[7] memory)
// Warning 8364: (156-163): Assertion checker does not yet implement type type(uint256[7] memory) // Warning 8364: (156-163): Assertion checker does not yet implement type type(uint256[7] memory)
// Warning 8364: (125-126): Assertion checker does not yet implement type type(struct test.s storage pointer)
// Warning 8364: (130-131): Assertion checker does not yet implement type type(struct test.s storage pointer)
// Warning 4639: (130-136): Assertion checker does not yet implement this expression.
// Warning 8364: (140-141): Assertion checker does not yet implement type type(struct test.s storage pointer)
// Warning 8364: (140-144): Assertion checker does not yet implement type type(struct test.s memory[7] memory) // Warning 8364: (140-144): Assertion checker does not yet implement type type(struct test.s memory[7] memory)
// Warning 8364: (156-163): Assertion checker does not yet implement type type(uint256[7] memory) // Warning 8364: (156-163): Assertion checker does not yet implement type type(uint256[7] memory)

View File

@ -0,0 +1,23 @@
pragma experimental SMTChecker;
contract C {
struct S {
uint x;
}
struct T {
S s;
uint y;
}
function test() pure public {
S memory inner = S({x: 43});
T memory outer = T({y: 512, s: inner});
assert(outer.y == 512);
assert(outer.s.x == 43);
assert(outer.s.x == 42);
}
}
// ----
// Warning 6328: (265-288): CHC: Assertion violation happens here.

View File

@ -0,0 +1,20 @@
pragma experimental SMTChecker;
contract C {
struct S {
uint x;
uint y;
uint z;
}
function test() pure public {
S memory s = S({z: 1, y: 2, x: 3});
assert(s.x == 3);
assert(s.y == 2);
assert(s.z == 1);
assert(s.x == 0 || s.y == 0 || s.z == 0); // should fail
}
}
// ----
// Warning 6328: (224-264): CHC: Assertion violation happens here.

View File

@ -0,0 +1,23 @@
pragma experimental SMTChecker;
contract C {
struct S {
uint x;
}
struct T {
S s;
uint y;
}
function test() pure public {
S memory inner = S(43);
T memory outer = T(inner, 512);
assert(outer.y == 512);
assert(outer.s.x == 43);
assert(outer.s.x == 42);
}
}
// ----
// Warning 6328: (252-275): CHC: Assertion violation happens here.

View File

@ -0,0 +1,10 @@
pragma experimental SMTChecker;
contract C {
struct B { uint b1; }
struct A { uint a1; B a2; }
function f() public pure {
A memory a = A({ a1: 1, a2: B({b1: 2}) });
assert(a.a1 == 1 && a.a2.b1 == 2);
}
}

View File

@ -0,0 +1,18 @@
pragma experimental SMTChecker;
contract C {
struct S {
uint x;
}
struct T {
S s;
uint y;
}
function test() pure public {
assert(T(S(42), 1).s.x == 42);
}
}
// ----

View File

@ -0,0 +1,15 @@
pragma experimental SMTChecker;
contract C {
struct S {
uint x;
}
S s = S(42);
function test() view public {
assert(s.x == 42);
}
}
// ----

View File

@ -0,0 +1,13 @@
pragma experimental SMTChecker;
contract C {
struct S {
uint x;
}
function test() pure public {
assert(S(42).x == 42);
}
}
// ----

View File

@ -11,15 +11,7 @@ contract C
function f(uint y, uint v) public { function f(uint y, uint v) public {
smap[y] = S(v); smap[y] = S(v);
S memory smem = S(v); S memory smem = S(v);
assert(smap[y].x == smem.x);
} }
} }
// ---- // ----
// Warning 2072: (157-170): Unused local variable.
// Warning 8364: (149-150): Assertion checker does not yet implement type type(struct C.S storage pointer)
// Warning 4639: (149-153): Assertion checker does not yet implement this expression.
// Warning 8364: (173-174): Assertion checker does not yet implement type type(struct C.S storage pointer)
// Warning 4639: (173-177): Assertion checker does not yet implement this expression.
// Warning 8364: (149-150): Assertion checker does not yet implement type type(struct C.S storage pointer)
// Warning 4639: (149-153): Assertion checker does not yet implement this expression.
// Warning 8364: (173-174): Assertion checker does not yet implement type type(struct C.S storage pointer)
// Warning 4639: (173-177): Assertion checker does not yet implement this expression.

View File

@ -9,13 +9,10 @@ contract C {
function f(uint a) public pure { function f(uint a) public pure {
uint x; uint x;
S memory y; S memory y;
if (a > 100) if (a > 100) {
(x, y) = g(); (x, y) = g();
assert(y.x == 3);
}
} }
} }
// ---- // ----
// Warning 8364: (137-138): Assertion checker does not yet implement type type(struct C.S storage pointer)
// Warning 4639: (137-141): Assertion checker does not yet implement this expression.
// Warning 8364: (137-138): Assertion checker does not yet implement type type(struct C.S storage pointer)
// Warning 4639: (137-141): Assertion checker does not yet implement this expression.
// Warning 4639: (137-141): Assertion checker does not yet implement this expression.