[SMTChecker] Implement support for memory allocation

Changelog.md

@@ -10,6 +10,7 @@ Compiler Features:
  * SMTChecker: Support ``revert()``.
  * SMTChecker: Support shifts.
  * SMTChecker: Support compound and, or, and xor operators.
+ * SMTChecker: Support memory allocation, e.g. ``new bytes(123)``.
  * SMTChecker: Support structs.
  * SMTChecker: Support ``type(T).min``, ``type(T).max``, and ``type(I).interfaceId``.
  * SMTChecker: Support ``address`` type conversion with literals, e.g. ``address(0)``.

libsolidity/formal/SMTEncoder.cpp

@@ -663,6 +663,9 @@ void SMTEncoder::endVisit(FunctionCall const& _funCall)
 	case FunctionType::Kind::Event:
 		// These can be safely ignored.
 		break;
+	case FunctionType::Kind::ObjectCreation:
+		visitObjectCreation(_funCall);
+		return;
 	default:
 		m_errorReporter.warning(
 			4588_error,
@@ -735,6 +738,25 @@ void SMTEncoder::visitGasLeft(FunctionCall const& _funCall)
 		m_context.addAssertion(symbolicVar->currentValue() <= symbolicVar->valueAtIndex(index - 1));
 }
 
+void SMTEncoder::visitObjectCreation(FunctionCall const& _funCall)
+{
+	auto const& args = _funCall.arguments();
+	solAssert(args.size() >= 1, "");
+	auto argType = args.front()->annotation().type->category();
+	solAssert(argType == Type::Category::Integer || argType == Type::Category::RationalNumber, "");
+
+	smtutil::Expression arraySize = expr(*args.front());
+	setSymbolicUnknownValue(arraySize, TypeProvider::uint256(), m_context);
+
+	auto symbArray = dynamic_pointer_cast<smt::SymbolicArrayVariable>(m_context.expression(_funCall));
+	solAssert(symbArray, "");
+	smt::setSymbolicZeroValue(*symbArray, m_context);
+	auto zeroElements = symbArray->elements();
+	symbArray->increaseIndex();
+	m_context.addAssertion(symbArray->length() == arraySize);
+	m_context.addAssertion(symbArray->elements() == zeroElements);
+}
+
 void SMTEncoder::endVisit(Identifier const& _identifier)
 {
 	if (auto decl = identifierToVariable(_identifier))

libsolidity/formal/SMTEncoder.h

@@ -137,6 +137,7 @@ protected:
 	void visitAssert(FunctionCall const& _funCall);
 	void visitRequire(FunctionCall const& _funCall);
 	void visitGasLeft(FunctionCall const& _funCall);
+	void visitObjectCreation(FunctionCall const& _funCall);
 	void visitTypeConversion(FunctionCall const& _funCall);
 	void visitFunctionIdentifier(Identifier const& _identifier);
 

test/libsolidity/smtCheckerTests/operators/bytes_new.sol

@@ -0,0 +1,36 @@
+pragma experimental SMTChecker;
+
+contract C {
+	function f() public pure {
+		bytes memory x = new bytes(0);
+		assert(x.length == 0);
+	}
+	function g() public pure {
+		bytes memory x = new bytes(3);
+		assert(x.length == 3);
+		assert(x[0] == 0);
+		assert(x[1] == 0);
+		assert(x[2] == 0);
+	}
+	function h() public pure {
+		bytes memory x = new bytes(3);
+		assert(x.length == 3);
+		x[0] = 0x12;
+		x[1] = 0x34;
+		assert(x[0] == 0x12);
+		assert(x[1] == 0x34);
+		// This should be an out-of-bounds assertion.
+		x[5] = 0xff;
+		assert(x[5] == 0xff);
+	}
+	function h(uint size) public pure {
+		bytes memory x = new bytes(size);
+		assert(x.length == size);
+		require(size >= 2);
+		x[0] = 0x12;
+		x[1] = 0x34;
+		assert(x[0] == 0x12);
+		assert(x[1] == 0x34);
+	}
+}
+// ----

test/libsolidity/smtCheckerTests/operators/integer_new.sol

@@ -0,0 +1,36 @@
+pragma experimental SMTChecker;
+
+contract C {
+	function f() public pure {
+		uint[] memory x = new uint[](0);
+		assert(x.length == 0);
+	}
+	function g() public pure {
+		uint[] memory x = new uint[](3);
+		assert(x.length == 3);
+		assert(x[0] == 0);
+		assert(x[1] == 0);
+		assert(x[2] == 0);
+	}
+	function h() public pure {
+		uint[] memory x = new uint[](3);
+		assert(x.length == 3);
+		x[0] = 0x12;
+		x[1] = 0x34;
+		assert(x[0] == 0x12);
+		assert(x[1] == 0x34);
+		// This should be an out-of-bounds assertion.
+		x[5] = 0xff;
+		assert(x[5] == 0xff);
+	}
+	function h(uint size) public pure {
+		uint[] memory x = new uint[](size);
+		assert(x.length == size);
+		require(size >= 2);
+		x[0] = 0x12;
+		x[1] = 0x34;
+		assert(x[0] == 0x12);
+		assert(x[1] == 0x34);
+	}
+}
+// ----

test/libsolidity/smtCheckerTests/types/function_type_arrays.sol

@@ -7,8 +7,8 @@ contract C {
         function(uint) returns (uint)[10] storage b = y;
         function(uint) external returns (uint)[] memory c;
         c = new function(uint) external returns (uint)[](200);
+        assert(c.length == 200);
         a; b;
     }
 }
 // ----
-// Warning 4588: (361-410): Assertion checker does not yet implement this type of function call.

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

@@ -14,6 +14,7 @@ contract C {
 	}
 	function f() public pure {
 		S[] memory s1 = new S[](3);
+		assert(s1.length == 3);
 		s1[0].x = 2;
 		assert(s1[0].x == 2);
 		s1[1].t.y = 3;
@@ -27,4 +28,3 @@ contract C {
 	}
 }
 // ----
-// Warning 4588: (217-227): Assertion checker does not yet implement this type of function call.

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

@@ -14,6 +14,7 @@ contract C {
 	}
 	function f(S memory s2) public pure {
 		S[] memory s1 = new S[](3);
+		assert(s1.length == 3);
 		s1[0].x = 2;
 		assert(s1[0].x == s2.x);
 		s1[1].t.y = 3;
@@ -27,9 +28,8 @@ contract C {
 	}
 }
 // ----
-// Warning 6328: (257-280): Assertion violation happens here.
+// Warning 6328: (283-306): Assertion violation happens here.
-// Warning 6328: (301-328): Assertion violation happens here.
+// Warning 6328: (327-354): Assertion violation happens here.
-// Warning 6328: (350-379): Assertion violation happens here.
+// Warning 6328: (376-405): Assertion violation happens here.
-// Warning 6328: (404-439): Assertion violation happens here.
+// Warning 6328: (430-465): Assertion violation happens here.
-// Warning 6328: (467-508): Assertion violation happens here.
+// Warning 6328: (493-534): Assertion violation happens here.
-// Warning 4588: (228-238): Assertion checker does not yet implement this type of function call.