Merge pull request #9812 from ethereum/develop

Merge develop into breaking.

test/libsolidity/ASTJSON/documentation.sol

@@ -1,14 +1,14 @@
-// ---- SOURCE: a
+==== Source: a ====
 
 /**This contract is empty*/ contract C {}
 
-// ---- SOURCE: b
+==== Source: b ====
 
 /**This contract is empty
  and has a line-breaking comment.*/
 contract C {}
 
-// ---- SOURCE: c
+==== Source: c ====
 
 contract C {
   /** Some comment on state var.*/ uint public state;

test/libsolidity/ASTJSONTest.cpp

@@ -44,6 +44,8 @@ using namespace boost::unit_test;
 namespace
 {
 
+string const sourceDelimiter("==== Source: ");
+
 void replaceVersionWithTag(string& _input)
 {
 	boost::algorithm::replace_all(
@@ -81,7 +83,6 @@ ASTJSONTest::ASTJSONTest(string const& _filename)
 	string sourceName;
 	string source;
 	string line;
-	string const sourceDelimiter("// ---- SOURCE: ");
 	string const delimiter("// ----");
 	while (getline(file, line))
 	{
@@ -90,7 +91,10 @@ ASTJSONTest::ASTJSONTest(string const& _filename)
 			if (!sourceName.empty())
 				m_sources.emplace_back(sourceName, source);
 
-			sourceName = line.substr(sourceDelimiter.size(), string::npos);
+			sourceName = line.substr(
+				sourceDelimiter.size(),
+				line.size() - " ===="s.size() - sourceDelimiter.size()
+			);
 			source = string();
 		}
 		else if (!line.empty() && !boost::algorithm::starts_with(line, delimiter))
@@ -238,7 +242,7 @@ void ASTJSONTest::printSource(ostream& _stream, string const& _linePrefix, bool
 	for (auto const& source: m_sources)
 	{
 		if (m_sources.size() > 1 || source.first != "a")
-			_stream << _linePrefix << "// ---- SOURCE: " << source.first << endl << endl;
+			_stream << _linePrefix << sourceDelimiter << source.first << endl << endl;
 		stringstream stream(source.second);
 		string line;
 		while (getline(stream, line))

test/libsolidity/smtCheckerTests/control_flow/require.sol

@@ -0,0 +1,33 @@
+pragma experimental SMTChecker;
+
+contract C {
+	function f() pure public {
+		require(false);
+		// This is not reachable.
+		assert(false);
+	}
+
+	function g() pure public {
+		require(false, "require message");
+		// This is not reachable.
+		assert(false);
+	}
+
+	function h(bool b) pure public {
+		if (b)
+			require(false);
+		assert(!b);
+	}
+
+	// Check that arguments are evaluated.
+	bool x = false;
+	function m() view internal returns (string memory) {
+		assert(x != true);
+	}
+	function i() public {
+		x = true;
+		require(false, m());
+	}
+}
+// ----
+// Warning 6328: (448-465): Assertion violation happens here.

test/libsolidity/smtCheckerTests/control_flow/revert.sol

@@ -0,0 +1,35 @@
+pragma experimental SMTChecker;
+
+contract C {
+	function f() pure public {
+		revert();
+		// This is not reachable.
+		assert(false);
+	}
+
+	function g() pure public {
+		revert("revert message");
+		// This is not reachable.
+		assert(false);
+	}
+
+	function h(bool b) pure public {
+		if (b)
+			revert();
+		assert(!b);
+	}
+
+	// Check that arguments are evaluated.
+	bool x = false;
+	function m() view internal returns (string memory) {
+		assert(x != true);
+	}
+	function i() public {
+		x = true;
+		revert(m());
+	}
+}
+// ----
+// Warning 5740: (116-129): Unreachable code.
+// Warning 5740: (221-234): Unreachable code.
+// Warning 6328: (427-444): Assertion violation happens here.

test/libsolidity/smtCheckerTests/control_flow/revert_complex_flow.sol

@@ -0,0 +1,18 @@
+pragma experimental SMTChecker;
+
+contract C {
+	function f(bool b, uint a) pure public {
+		require(a <= 256);
+		if (b)
+			revert();
+		uint c = a + 1;
+		if (b)
+			c--;
+		else
+			c++;
+		assert(c == a);
+	}
+}
+// ----
+// Warning 6328: (183-197): Assertion violation happens here.
+// Warning 6838: (155-156): Condition is always false.

test/libsolidity/smtCheckerTests/invariants/loop_nested.sol

@@ -1,8 +1,5 @@
 pragma experimental SMTChecker;
 
-// This test gets different results on Linux and OSX.
-// Re-enable when fixed (SMTSolvers: z3)
-
 contract Simple {
 	function f() public pure {
 		uint x = 10;
@@ -18,8 +15,4 @@ contract Simple {
 		assert(y == x);
 	}
 }
-// ====
-// SMTSolvers: none
 // ----
-// Warning: (195-209): Error trying to invoke SMT solver.
-// Warning: (195-209): Assertion violation happens here

test/libsolidity/smtCheckerTests/loops/for_1_false_positive.sol

@@ -13,8 +13,6 @@ contract C
 		assert(x > 0);
 	}
 }
-// ====
-// SMTSolvers: cvc4
 // ----
+// Warning 1218: (176-181): Error trying to invoke SMT solver.
 // Warning 2661: (176-181): Overflow (resulting value larger than 2**256 - 1) happens here.
-// Warning 4661: (296-309): Assertion violation happens here.

test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_storage_storage.sol

@@ -20,9 +20,7 @@ contract LoopFor2 {
 		assert(b[0] == 900);
 	}
 }
-// ====
-// SMTSolvers: cvc4
 // ----
-// Warning 4661: (296-316): Assertion violation happens here.
-// Warning 4661: (320-339): Assertion violation happens here.
-// Warning 4661: (343-362): Assertion violation happens here.
+// Warning 1218: (229-234): Error trying to invoke SMT solver.
+// Warning 6328: (320-339): Assertion violation happens here.
+// Warning 6328: (343-362): Assertion violation happens here.

test/libsolidity/smtCheckerTests/operators/delete_multid_array.sol

@@ -37,8 +37,6 @@ contract C {
 		b[x][y] = z;
 	}
 }
-// ====
-// SMTSolvers: cvc4
 // ----
-// Warning 4661: (372-392): Assertion violation happens here.
-// Warning 4661: (617-637): Assertion violation happens here.
+// Warning 6328: (372-392): Assertion violation happens here.
+// Warning 6328: (617-637): Assertion violation happens here.

test/libsolidity/smtCheckerTests/operators/shifts/shift_right_uint8.sol

@@ -0,0 +1,19 @@
+pragma experimental SMTChecker;
+
+contract C {
+    function f(uint8 a, uint8 b) internal pure returns (uint256) {
+        return a >> b;
+    }
+	function t() public pure {
+		assert(f(0x66, 0) == 0x66);
+		// Fails because the above is true.
+		assert(f(0x66, 0) == 0x6);
+
+		assert(f(0x66, 8) == 0);
+		// Fails because the above is true.
+		assert(f(0x66, 8) == 1);
+	}
+}
+// ----
+// Warning 6328: (240-265): Assertion violation happens here.
+// Warning 6328: (335-358): Assertion violation happens here.

test/libsolidity/smtCheckerTests/types/mapping_aliasing_2.sol

@@ -0,0 +1,35 @@
+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 {
+		map1[0] = 2;
+		a[0] = 42;
+		maps[0][0] = 42;
+		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);
+	}
+
+	function g(bool b, uint x, uint y) public {
+		if (b)
+			f(a, maps[y]);
+		else
+			f(maps[x], maps[y]);
+	}
+}
+// ----
+// Warning 6328: (397-417): Assertion violation happens here.
+// Warning 6328: (463-481): Assertion violation happens here.
+// Warning 6328: (533-557): Assertion violation happens here.

test/libsolidity/smtCheckerTests/types/struct/array_struct_array_struct_memory_unsafe.sol

@@ -22,6 +22,8 @@ contract C {
 		assert(s1[2].a[2] == s2.a[2]);
 		s1[0].ts[3].y = 5;
 		assert(s1[0].ts[3].y == s2.ts[3].y);
+		s1[1].ts[4].a[5] = 6;
+		assert(s1[1].ts[4].a[5] == s2.ts[4].a[5]);
 	}
 }
 // ----
@@ -29,4 +31,5 @@ contract C {
 // Warning 6328: (301-328): Assertion violation happens here.
 // Warning 6328: (350-379): Assertion violation happens here.
 // Warning 6328: (404-439): Assertion violation happens here.
+// Warning 6328: (467-508): Assertion violation happens here.
 // Warning 4588: (228-238): Assertion checker does not yet implement this type of function call.

test/libsolidity/smtCheckerTests/types/struct/struct_array_struct_array_memory_unsafe_1.sol

@@ -22,6 +22,8 @@ contract C {
 		assert(s1.a[2] != 4);
 		s1.ts[3].y = 5;
 		assert(s1.ts[3].y != 5);
+		s1.ts[4].a[5] = 6;
+		assert(s1.ts[4].a[5] != 6);
 	}
 }
 // ----
@@ -29,3 +31,4 @@ contract C {
 // Warning 6328: (263-282): Assertion violation happens here.
 // Warning 6328: (301-321): Assertion violation happens here.
 // Warning 6328: (343-366): Assertion violation happens here.
+// Warning 6328: (391-417): Assertion violation happens here.

test/libsolidity/smtCheckerTests/types/struct/struct_array_struct_array_memory_unsafe_2.sol

@@ -0,0 +1,34 @@
+pragma experimental SMTChecker;
+pragma experimental ABIEncoderV2;
+
+contract C {
+	struct T {
+		uint y;
+		uint[] a;
+	}
+	struct S {
+		uint x;
+		T t;
+		uint[] a;
+		T[] ts;
+	}
+	function f(S memory s2) public pure {
+		S memory s1;
+		s1.x = 2;
+		assert(s1.x == s2.x);
+		s1.t.y = 3;
+		assert(s1.t.y == s2.t.y);
+		s1.a[2] = 4;
+		assert(s1.a[2] == s2.a[2]);
+		s1.ts[3].y = 5;
+		assert(s1.ts[3].y == s2.ts[3].y);
+		s1.ts[4].a[5] = 6;
+		assert(s1.ts[4].a[5] == s2.ts[4].a[5]);
+	}
+}
+// ----
+// Warning 6328: (239-259): Assertion violation happens here.
+// Warning 6328: (277-301): Assertion violation happens here.
+// Warning 6328: (320-346): Assertion violation happens here.
+// Warning 6328: (368-400): Assertion violation happens here.
+// Warning 6328: (425-463): Assertion violation happens here.

test/libsolidity/smtCheckerTests/types/struct/struct_array_struct_array_storage_unsafe_1.sol

@@ -21,6 +21,8 @@ contract C {
 		assert(s1.a[2] != 4);
 		s1.ts[3].y = 5;
 		assert(s1.ts[3].y != 5);
+		s1.ts[4].a[5] = 6;
+		assert(s1.ts[4].a[5] != 6);
 	}
 }
 // ----
@@ -28,3 +30,4 @@ contract C {
 // Warning 6328: (216-235): Assertion violation happens here.
 // Warning 6328: (254-274): Assertion violation happens here.
 // Warning 6328: (296-319): Assertion violation happens here.
+// Warning 6328: (344-370): Assertion violation happens here.

test/libsolidity/smtCheckerTests/types/type_interfaceid.sol

@@ -0,0 +1,32 @@
+pragma experimental SMTChecker;
+
+interface I1 {
+}
+
+interface I2 {
+	function f() external;
+}
+
+interface I3 {
+	function f() external;
+	function g(uint, address) external;
+}
+
+contract C {
+	function f() public pure {
+		assert(type(I1).interfaceId == 0);
+		assert(type(I2).interfaceId != 0);
+		assert(type(I2).interfaceId == 0x26121ff0);
+		assert(type(I2).interfaceId != 0);
+		assert(type(I3).interfaceId == 0x822b51c6);
+	}
+	function g() public pure {
+		assert(type(I1).interfaceId == type(I2).interfaceId);
+	}
+	function h() public pure {
+		assert(type(I2).interfaceId == type(I3).interfaceId);
+	}
+}
+// ----
+// Warning 6328: (449-501): Assertion violation happens here.
+// Warning 6328: (536-588): Assertion violation happens here.

test/libsolidity/smtCheckerTests/verification_target/constant_condition_1.sol

@@ -6,4 +6,3 @@ contract C {
 }
 // ----
 // Warning 6838: (94-100): Condition is always true.
-// Warning 4588: (104-112): Assertion checker does not yet implement this type of function call.

test/libsolidity/smtCheckerTests/verification_target/constant_condition_2.sol

@@ -6,4 +6,3 @@ contract C {
 }
 // ----
 // Warning 6838: (109-115): Condition is always false.
-// Warning 4588: (119-127): Assertion checker does not yet implement this type of function call.

test/libsolidity/smtCheckerTests/verification_target/constant_condition_3.sol

@@ -6,4 +6,3 @@ contract C {
     }
 }
 // ----
-// Warning 4588: (136-144): Assertion checker does not yet implement this type of function call.

test/libsolidity/syntaxTests/scoping/name_pseudo_shadowing.sol

@@ -0,0 +1,6 @@
+contract test {
+    function e() external { }
+    function f() public pure { uint e; e = 0; }
+}
+// ----
+// Warning 8760: (77-83): This declaration has the same name as another declaration.

test/libsolidity/syntaxTests/scoping/name_shadowing2.sol

@@ -0,0 +1,6 @@
+function e() {}
+contract test {
+    function f() pure public { uint e; e = 0; }
+}
+// ----
+// Warning 2519: (63-69): This declaration shadows an existing declaration.