diff --git a/Changelog.md b/Changelog.md index 85c71df8e..47cb71732 100644 --- a/Changelog.md +++ b/Changelog.md @@ -2,7 +2,7 @@ Compiler Features: * SMTChecker: Support named arguments in function calls. - + * SMTChecker: Support struct constructor. ### 0.7.5 (2020-11-18) diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp index 23ed1b339..9a5cce9b3 100644 --- a/libsolidity/formal/SMTEncoder.cpp +++ b/libsolidity/formal/SMTEncoder.cpp @@ -622,11 +622,7 @@ void SMTEncoder::endVisit(FunctionCall const& _funCall) createExpr(_funCall); if (functionCallKind == FunctionCallKind::StructConstructorCall) { - m_errorReporter.warning( - 4639_error, - _funCall.location(), - "Assertion checker does not yet implement this expression." - ); + visitStructConstructorCall(_funCall); return; } @@ -861,6 +857,12 @@ void SMTEncoder::endVisit(Identifier const& _identifier) defineExpr(_identifier, m_context.state().thisAddress()); m_uninterpretedTerms.insert(&_identifier); } + // Ignore struct type identifiers in struct constructor calls + else if ( + auto typetype = dynamic_cast(_identifier.annotation().type); + typetype && typetype->actualType()->category() == Type::Category::Struct + ) + return; // Ignore the builtin abi, it is handled in FunctionCall. // TODO: ignore MagicType in general (abi, block, msg, tx, type) else if (auto magicType = dynamic_cast(_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(*m_context.expression(_funCall)); + structSymbolicVar.assignAllMembers(applyMap(_funCall.sortedArguments(), [this](auto const& arg) { return expr(*arg); })); +} + void SMTEncoder::endVisit(Literal const& _literal) { solAssert(_literal.annotation().type, "Expected type for AST node"); diff --git a/libsolidity/formal/SMTEncoder.h b/libsolidity/formal/SMTEncoder.h index a2e8f2336..8dffc2682 100644 --- a/libsolidity/formal/SMTEncoder.h +++ b/libsolidity/formal/SMTEncoder.h @@ -151,6 +151,7 @@ protected: virtual void visitAddMulMod(FunctionCall const& _funCall); void visitObjectCreation(FunctionCall const& _funCall); void visitTypeConversion(FunctionCall const& _funCall); + void visitStructConstructorCall(FunctionCall const& _funCall); void visitFunctionIdentifier(Identifier const& _identifier); /// Encodes a modifier or function body according to the modifier diff --git a/libsolidity/formal/SymbolicVariables.cpp b/libsolidity/formal/SymbolicVariables.cpp index 2d58704d1..5c23fbf66 100644 --- a/libsolidity/formal/SymbolicVariables.cpp +++ b/libsolidity/formal/SymbolicVariables.cpp @@ -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)); } @@ -385,3 +385,18 @@ smtutil::Expression SymbolicStructVariable::assignMember(string const& _member, return currentValue(); } + +smtutil::Expression SymbolicStructVariable::assignAllMembers(vector const& _memberValues) +{ + auto structType = dynamic_cast(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(); +} \ No newline at end of file diff --git a/libsolidity/formal/SymbolicVariables.h b/libsolidity/formal/SymbolicVariables.h index 6dda692b1..ff6373332 100644 --- a/libsolidity/formal/SymbolicVariables.h +++ b/libsolidity/formal/SymbolicVariables.h @@ -282,12 +282,16 @@ public: ); /// @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 /// with field _member updated. 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 const& _memberValues); + private: std::map m_memberIndices; }; diff --git a/test/libsolidity/smtCheckerTests/complex/warn_on_struct.sol b/test/libsolidity/smtCheckerTests/complex/warn_on_struct.sol deleted file mode 100644 index f5af0f820..000000000 --- a/test/libsolidity/smtCheckerTests/complex/warn_on_struct.sol +++ /dev/null @@ -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. diff --git a/test/libsolidity/smtCheckerTests/special/abi_decode_memory_v2.sol b/test/libsolidity/smtCheckerTests/special/abi_decode_memory_v2.sol index 7249b9e99..94a71b1fa 100644 --- a/test/libsolidity/smtCheckerTests/special/abi_decode_memory_v2.sol +++ b/test/libsolidity/smtCheckerTests/special/abi_decode_memory_v2.sol @@ -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-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 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-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. diff --git a/test/libsolidity/smtCheckerTests/types/mapping_struct_assignment.sol b/test/libsolidity/smtCheckerTests/types/mapping_struct_assignment.sol index 33c3ded48..ae1da3202 100644 --- a/test/libsolidity/smtCheckerTests/types/mapping_struct_assignment.sol +++ b/test/libsolidity/smtCheckerTests/types/mapping_struct_assignment.sol @@ -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 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. diff --git a/test/libsolidity/smtCheckerTests/types/no_effect_statements.sol b/test/libsolidity/smtCheckerTests/types/no_effect_statements.sol index a5f78824c..fac8cce48 100644 --- a/test/libsolidity/smtCheckerTests/types/no_effect_statements.sol +++ b/test/libsolidity/smtCheckerTests/types/no_effect_statements.sol @@ -16,15 +16,7 @@ contract test { // Warning 6133: (140-144): Statement has no effect. // Warning 6133: (148-152): 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: (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: (156-163): Assertion checker does not yet implement type type(uint256[7] memory) diff --git a/test/libsolidity/smtCheckerTests/types/struct/struct_constructor_named_args.sol b/test/libsolidity/smtCheckerTests/types/struct/struct_constructor_named_args.sol new file mode 100644 index 000000000..8022b39d5 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/types/struct/struct_constructor_named_args.sol @@ -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. diff --git a/test/libsolidity/smtCheckerTests/types/struct/struct_constructor_named_args_2.sol b/test/libsolidity/smtCheckerTests/types/struct/struct_constructor_named_args_2.sol new file mode 100644 index 000000000..7c78645d1 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/types/struct/struct_constructor_named_args_2.sol @@ -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. diff --git a/test/libsolidity/smtCheckerTests/types/struct/struct_nested_constructor.sol b/test/libsolidity/smtCheckerTests/types/struct/struct_nested_constructor.sol new file mode 100644 index 000000000..5fcc3b246 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/types/struct/struct_nested_constructor.sol @@ -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. diff --git a/test/libsolidity/smtCheckerTests/types/struct/struct_nested_constructor_named_args.sol b/test/libsolidity/smtCheckerTests/types/struct/struct_nested_constructor_named_args.sol new file mode 100644 index 000000000..7fae9133d --- /dev/null +++ b/test/libsolidity/smtCheckerTests/types/struct/struct_nested_constructor_named_args.sol @@ -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); + } +} diff --git a/test/libsolidity/smtCheckerTests/types/struct/struct_nested_temporary.sol b/test/libsolidity/smtCheckerTests/types/struct/struct_nested_temporary.sol new file mode 100644 index 000000000..9cc180219 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/types/struct/struct_nested_temporary.sol @@ -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); + } +} +// ---- diff --git a/test/libsolidity/smtCheckerTests/types/struct/struct_state_constructor.sol b/test/libsolidity/smtCheckerTests/types/struct/struct_state_constructor.sol new file mode 100644 index 000000000..46237c934 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/types/struct/struct_state_constructor.sol @@ -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); + } +} +// ---- diff --git a/test/libsolidity/smtCheckerTests/types/struct/struct_temporary.sol b/test/libsolidity/smtCheckerTests/types/struct/struct_temporary.sol new file mode 100644 index 000000000..b6451dd2a --- /dev/null +++ b/test/libsolidity/smtCheckerTests/types/struct/struct_temporary.sol @@ -0,0 +1,13 @@ +pragma experimental SMTChecker; + +contract C { + + struct S { + uint x; + } + + function test() pure public { + assert(S(42).x == 42); + } +} +// ---- diff --git a/test/libsolidity/smtCheckerTests/types/struct_1.sol b/test/libsolidity/smtCheckerTests/types/struct_1.sol index d8152d6e0..37035c806 100644 --- a/test/libsolidity/smtCheckerTests/types/struct_1.sol +++ b/test/libsolidity/smtCheckerTests/types/struct_1.sol @@ -11,15 +11,7 @@ contract C function f(uint y, uint v) public { smap[y] = 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. diff --git a/test/libsolidity/smtCheckerTests/types/tuple_return_branch.sol b/test/libsolidity/smtCheckerTests/types/tuple_return_branch.sol index 3d3336eb1..2642c979a 100644 --- a/test/libsolidity/smtCheckerTests/types/tuple_return_branch.sol +++ b/test/libsolidity/smtCheckerTests/types/tuple_return_branch.sol @@ -9,13 +9,10 @@ contract C { function f(uint a) public pure { uint x; S memory y; - if (a > 100) + if (a > 100) { (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.