diff --git a/libsolidity/formal/CHC.cpp b/libsolidity/formal/CHC.cpp index 746ea11cd..3b226d4f7 100644 --- a/libsolidity/formal/CHC.cpp +++ b/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 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(_type)) + _addChild(mapType->valueType()); + else if (auto const* arrayType = dynamic_cast(_type)) + _addChild(arrayType->baseType()); + else if (auto const* structType = dynamic_cast(_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)); diff --git a/libsolidity/formal/SymbolicState.cpp b/libsolidity/formal/SymbolicState.cpp index 3755cee64..6801e7717 100644 --- a/libsolidity/formal/SymbolicState.cpp +++ b/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); diff --git a/libsolidity/formal/SymbolicState.h b/libsolidity/formal/SymbolicState.h index c4ac7382f..3cd4271db 100644 --- a/libsolidity/formal/SymbolicState.h +++ b/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); //@} diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_contract_inside_array_struct_trusted_1.sol b/test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_contract_inside_array_struct_trusted_1.sol new file mode 100644 index 000000000..6471146ee --- /dev/null +++ b/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() diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_contract_inside_array_struct_trusted_2.sol b/test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_contract_inside_array_struct_trusted_2.sol new file mode 100644 index 000000000..c702336a9 --- /dev/null +++ b/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() diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_contract_inside_array_trusted_1.sol b/test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_contract_inside_array_trusted_1.sol new file mode 100644 index 000000000..c3b2f5529 --- /dev/null +++ b/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() diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_contract_inside_array_trusted_2.sol b/test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_contract_inside_array_trusted_2.sol new file mode 100644 index 000000000..9c9682f81 --- /dev/null +++ b/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() diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_contract_inside_struct_trusted_1.sol b/test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_contract_inside_struct_trusted_1.sol new file mode 100644 index 000000000..293c22304 --- /dev/null +++ b/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() diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_contract_inside_struct_trusted_2.sol b/test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_contract_inside_struct_trusted_2.sol new file mode 100644 index 000000000..731050262 --- /dev/null +++ b/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. diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_contract_inside_struct_trusted_3.sol b/test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_contract_inside_struct_trusted_3.sol new file mode 100644 index 000000000..05425369f --- /dev/null +++ b/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() diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_contract_inside_struct_trusted_4.sol b/test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_contract_inside_struct_trusted_4.sol new file mode 100644 index 000000000..6a1fb2274 --- /dev/null +++ b/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()