[SMTChecker] Added support for struct constructor.

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)
 

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<TypeType const*>(_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<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)
 {
 	solAssert(_literal.annotation().type, "Expected type for AST node");

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

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<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();
+}

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<smtutil::Expression> const& _memberValues);
+
 private:
 	std::map<std::string, unsigned> m_memberIndices;
 };

test/libsolidity/smtCheckerTests/complex/warn_on_struct.sol

@@ -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.

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.

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.

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)

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.

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.

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.

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);
+	}
+}

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);
+	}
+}
+// ----

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);
+	}
+}
+// ----

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);
+	}
+}
+// ----

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.

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.