Havoc the state when state variables of reference type contain contract type

libsolidity/formal/CHC.cpp

@@ -1387,11 +1387,60 @@ void CHC::defineExternalFunctionInterface(FunctionDefinition const& _function, C
 	state().addBalance(state().thisAddress(), k.currentValue());
 
 	if (encodeExternalCallsAsTrusted())
+	{
 		// If the contract has state variables that are addresses to other contracts,
 		// we need to encode the fact that those contracts may have been called in between
 		// transactions to _contract.
-		// We do that by adding nondet_interface constraints for those contracts.
-		addNondetCalls(*m_currentContract);
+		//
+		// We do that by adding nondet_interface constraints for those contracts,
+		// in the last line of this if block.
+		//
+		// If there are state variables of container types like structs or arrays
+		// that indirectly contain contract types, we havoc the state for simplicity,
+		// in the first part of this block.
+		// TODO: This could actually be supported.
+		// For structs: simply collect the SMT expressions of all the indirect contract type members.
+		// For arrays: more involved, needs to traverse the array symbolically and do the same for each contract.
+		// For mappings: way more complicated if the element type is a contract.
+		auto hasContractOrAddressSubType = [&](VariableDeclaration const* _var) -> bool {
+			bool foundContract = false;
+			solidity::util::BreadthFirstSearch<Type const*> bfs{{_var->type()}};
+			bfs.run([&](auto _type, auto&& _addChild) {
+				if (
+					_type->category() == Type::Category::Address ||
+					_type->category() == Type::Category::Contract
+				)
+				{
+					foundContract = true;
+					bfs.abort();
+				}
+				if (auto const* mapType = dynamic_cast<MappingType const*>(_type))
+					_addChild(mapType->valueType());
+				else if (auto const* arrayType = dynamic_cast<ArrayType const*>(_type))
+					_addChild(arrayType->baseType());
+				else if (auto const* structType = dynamic_cast<StructType const*>(_type))
+					for (auto const& member: structType->nativeMembers(nullptr))
+						_addChild(member.type);
+			});
+			return foundContract;
+		};
+		bool found = false;
+		for (auto var: m_currentContract->stateVariables())
+			if (
+				var->type()->category() != Type::Category::Address &&
+				var->type()->category() != Type::Category::Contract &&
+				hasContractOrAddressSubType(var)
+			)
+			{
+				found = true;
+				break;
+			}
+
+		if (found)
+			state().newStorage();
+		else
+			addNondetCalls(*m_currentContract);
+	}
 
 	errorFlag().increaseIndex();
 	m_context.addAssertion(summaryCall(_function));

libsolidity/formal/SymbolicState.cpp

@@ -153,6 +153,16 @@ void SymbolicState::setAddressActive(
 	);
 }
 
+void SymbolicState::newStorage()
+{
+	auto newStorageVar = SymbolicTupleVariable(
+		m_state->member("storage").sort,
+		"havoc_storage_" + to_string(m_context.newUniqueId()),
+		m_context
+	);
+	m_state->assignMember("storage", newStorageVar.currentValue());
+}
+
 void SymbolicState::writeStateVars(ContractDefinition const& _contract, smtutil::Expression _address)
 {
 	auto stateVars = SMTEncoder::stateVariablesIncludingInheritedAndPrivate(_contract);

libsolidity/formal/SymbolicState.h

@@ -132,6 +132,7 @@ public:
 	smtutil::Expression addressActive(smtutil::Expression _address) const;
 	void setAddressActive(smtutil::Expression _address, bool _active);
 
+	void newStorage();
 	void writeStateVars(ContractDefinition const& _contract, smtutil::Expression _address);
 	void readStateVars(ContractDefinition const& _contract, smtutil::Expression _address);
 	//@}

test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_contract_inside_array_struct_trusted_1.sol

@@ -0,0 +1,23 @@
+contract D {
+	uint public x;
+}
+
+contract C {
+	struct S {
+		D d;
+	}
+	S[] ss;
+	constructor() {
+		ss.push(S(new D()));
+		assert(ss[0].d.x() == 0); // should hold
+	}
+	function f() public view {
+		assert(ss[0].d.x() == 0); // should hold, but fails because we havoc the state
+	}
+}
+// ====
+// SMTEngine: chc
+// SMTExtCalls: trusted
+// SMTTargets: assert
+// ----
+// Warning 6328: (192-216): CHC: Assertion violation happens here.\nCounterexample:\nss = [{d: 3}]\n\nTransaction trace:\nC.constructor()\nState: ss = [{d: 3}]\nC.f()

test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_contract_inside_array_struct_trusted_2.sol

@@ -0,0 +1,24 @@
+contract D {
+	uint public x;
+	function setD(uint _x) public { x = _x; }
+}
+
+contract C {
+	struct S {
+		D d;
+	}
+	S[] ss;
+	constructor() {
+		ss.push(S(new D()));
+		assert(ss[0].d.x() == 0); // should hold
+	}
+	function f() public view {
+		assert(ss[0].d.x() == 0); // should fail
+	}
+}
+// ====
+// SMTEngine: chc
+// SMTExtCalls: trusted
+// SMTTargets: assert
+// ----
+// Warning 6328: (235-259): CHC: Assertion violation happens here.\nCounterexample:\nss = [{d: 3}]\n\nTransaction trace:\nC.constructor()\nState: ss = [{d: 3}]\nC.f()

test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_contract_inside_array_trusted_1.sol

@@ -0,0 +1,21 @@
+contract D {
+	uint public x;
+	function setD(uint _x) public { x = _x; }
+}
+
+contract C {
+	D[] ds;
+	constructor() {
+		ds.push(new D());
+		assert(ds[0].x() == 0); // should hold
+	}
+	function f() public view {
+		assert(ds[0].x() == 0); // should fail
+	}
+}
+// ====
+// SMTEngine: chc
+// SMTExtCalls: trusted
+// SMTTargets: assert
+// ----
+// Warning 6328: (208-230): CHC: Assertion violation happens here.\nCounterexample:\nds = [37]\n\nTransaction trace:\nC.constructor()\nState: ds = [37]\nC.f()

test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_contract_inside_array_trusted_2.sol

@@ -0,0 +1,20 @@
+contract D {
+	uint public x;
+}
+
+contract C {
+	D[] ds;
+	constructor() {
+		ds.push(new D());
+		assert(ds[0].x() == 0); // should hold
+	}
+	function f() public view {
+		assert(ds[0].x() == 0); // should hold, but fails because we havoc the state
+	}
+}
+// ====
+// SMTEngine: chc
+// SMTExtCalls: trusted
+// SMTTargets: assert
+// ----
+// Warning 6328: (165-187): CHC: Assertion violation happens here.\nCounterexample:\nds = [37]\n\nTransaction trace:\nC.constructor()\nState: ds = [37]\nC.f()

test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_contract_inside_struct_trusted_1.sol

@@ -0,0 +1,24 @@
+contract D {
+	uint public x;
+	function setD(uint _x) public { x = _x; }
+}
+
+contract C {
+	struct S {
+		D d;
+	}
+	S s;
+	constructor() {
+		s.d = new D();
+		assert(s.d.x() == 0); // should hold
+	}
+	function f() public view {
+		assert(s.d.x() == 0); // should fail
+	}
+}
+// ====
+// SMTEngine: chc
+// SMTExtCalls: trusted
+// SMTTargets: assert
+// ----
+// Warning 6328: (222-242): CHC: Assertion violation happens here.\nCounterexample:\ns = {d: 20819}\n\nTransaction trace:\nC.constructor()\nState: s = {d: 20819}\nC.f()

test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_contract_inside_struct_trusted_2.sol

@@ -0,0 +1,23 @@
+contract D {
+	uint public x;
+}
+
+contract C {
+	struct S {
+		D d;
+	}
+	S s;
+	constructor() {
+		s.d = new D();
+		assert(s.d.x() == 0); // should hold
+	}
+	function f() public view {
+		assert(s.d.x() == 0); // should hold, but fails because we havoc the state
+	}
+}
+// ====
+// SMTEngine: chc
+// SMTExtCalls: trusted
+// SMTTargets: assert
+// ----
+// Warning 6328: (179-199): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_contract_inside_struct_trusted_3.sol

@@ -0,0 +1,26 @@
+contract D {
+	uint public x;
+}
+
+contract C {
+	struct S {
+		D d;
+	}
+	struct T {
+		S s;
+	}
+	T t;
+	constructor() {
+		t.s.d = new D();
+		assert(t.s.d.x() == 0); // should hold
+	}
+	function f() public view {
+		assert(t.s.d.x() == 0); // should hold, but fails because we havoc the state
+	}
+}
+// ====
+// SMTEngine: chc
+// SMTExtCalls: trusted
+// SMTTargets: assert
+// ----
+// Warning 6328: (205-227): CHC: Assertion violation happens here.\nCounterexample:\nt = {s: {d: 20819}}\n\nTransaction trace:\nC.constructor()\nState: t = {s: {d: 20819}}\nC.f()

test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_contract_inside_struct_trusted_4.sol

@@ -0,0 +1,27 @@
+contract D {
+	uint public x;
+	function setD(uint _x) public { x = _x; }
+}
+
+contract C {
+	struct S {
+		D d;
+	}
+	struct T {
+		S s;
+	}
+	T t;
+	constructor() {
+		t.s.d = new D();
+		assert(t.s.d.x() == 0); // should hold
+	}
+	function f() public view {
+		assert(t.s.d.x() == 0); // should fail
+	}
+}
+// ====
+// SMTEngine: chc
+// SMTExtCalls: trusted
+// SMTTargets: assert
+// ----
+// Warning 6328: (248-270): CHC: Assertion violation happens here.\nCounterexample:\nt = {s: {d: 20819}}\n\nTransaction trace:\nC.constructor()\nState: t = {s: {d: 20819}}\nC.f()