[SMTChecker] Detect errors caused by reentrancy

libsolidity/formal/CHC.cpp

@@ -642,10 +642,20 @@ void CHC::externalFunctionCall(FunctionCall const& _funCall)
 	}
 
 	auto postCallState = vector<smtutil::Expression>{state().state()} + currentStateVariables();
-	auto nondet = (*m_nondetInterfaces.at(m_currentContract))(preCallState + postCallState);
+	auto error = errorFlag().increaseIndex();
+	vector<smtutil::Expression> stateExprs{error, state().thisAddress(), state().abi(), state().crypto()};
+	auto nondet = (*m_nondetInterfaces.at(m_currentContract))(stateExprs + preCallState + postCallState);
 	// TODO this could instead add the summary of the called function, where that summary
 	// basically has the nondet interface of this summary as a constraint.
 	m_context.addAssertion(nondet);
+	solAssert(m_errorDest, "");
+	connectBlocks(m_currentBlock, predicate(*m_errorDest), errorFlag().currentValue() > 0);
+	// To capture the possibility of a reentrant call, we record in the call graph that the  current function
+	// can call any of the external methods of the current contract.
+	solAssert(m_currentContract && m_currentFunction, "");
+	for (auto const* definedFunction: contractFunctions(*m_currentContract))
+		if (!definedFunction->isConstructor() && definedFunction->isPublic())
+			m_callGraph[m_currentFunction].insert(definedFunction);
 
 	m_context.addAssertion(errorFlag().currentValue() == 0);
 }
@@ -889,7 +899,7 @@ void CHC::defineInterfacesAndSummaries(SourceUnit const& _source)
 			/// 0 steps to be taken, used as base for the inductive
 			/// rule for each function.
 			auto const& iface = *m_nondetInterfaces.at(contract);
-			addRule(smt::nondetInterface(iface, *contract, m_context, 0, 0), "base_nondet");
+			addRule(smt::nondetInterface(iface, *contract, m_context, smtutil::Expression(size_t(0)), 0, 0), "base_nondet");
 
 			for (auto const* function: contractFunctions(*contract))
 			{
@@ -907,8 +917,8 @@ void CHC::defineInterfacesAndSummaries(SourceUnit const& _source)
 					auto state1 = stateVariablesAtIndex(1, *contract);
 					auto state2 = stateVariablesAtIndex(2, *contract);
 
-					auto nondetPre = smt::nondetInterface(iface, *contract, m_context, 0, 1);
+					auto nondetPre = smt::nondetInterface(iface, *contract, m_context, smtutil::Expression(size_t(0)), 0, 1);
-					auto nondetPost = smt::nondetInterface(iface, *contract, m_context, 0, 2);
+					auto nondetPost = smt::nondetInterface(iface, *contract, m_context, errorFlag().currentValue(), 0, 2);
 
 					vector<smtutil::Expression> args{errorFlag().currentValue(), state().thisAddress(), state().abi(), state().crypto(), state().tx(), state().state(1)};
 					args += state1 +

libsolidity/formal/PredicateInstance.cpp

@@ -36,14 +36,23 @@ smtutil::Expression interfacePre(Predicate const& _pred, ContractDefinition cons
 
 smtutil::Expression interface(Predicate const& _pred, ContractDefinition const& _contract, EncodingContext& _context)
 {
-	auto& state = _context.state();
+	auto const& state = _context.state();
 	vector<smtutil::Expression> stateExprs{state.thisAddress(0), state.abi(0), state.crypto(0), state.state()};
 	return _pred(stateExprs + currentStateVariables(_contract, _context));
 }
 
-smtutil::Expression nondetInterface(Predicate const& _pred, ContractDefinition const& _contract, EncodingContext& _context, unsigned _preIdx, unsigned _postIdx)
+smtutil::Expression nondetInterface(
+	Predicate const& _pred,
+	ContractDefinition const& _contract,
+	EncodingContext& _context,
+	smtutil::Expression const& _error,
+	unsigned _preIdx,
+	unsigned _postIdx)
 {
+	auto const& state = _context.state();
+	vector<smtutil::Expression> stateExprs{_error, state.thisAddress(), state.abi(), state.crypto()};
 	return _pred(
+		stateExprs +
 		vector<smtutil::Expression>{_context.state().state(_preIdx)} +
 		stateVariablesAtIndex(_preIdx, _contract, _context) +
 		vector<smtutil::Expression>{_context.state().state(_postIdx)} +

libsolidity/formal/PredicateInstance.h

@@ -34,7 +34,7 @@ smtutil::Expression interfacePre(Predicate const& _pred, ContractDefinition cons
 
 smtutil::Expression interface(Predicate const& _pred, ContractDefinition const& _contract, EncodingContext& _context);
 
-smtutil::Expression nondetInterface(Predicate const& _pred, ContractDefinition const& _contract, EncodingContext& _context, unsigned _preIdx, unsigned _postIdx);
+smtutil::Expression nondetInterface(Predicate const& _pred, ContractDefinition const& _contract, EncodingContext& _context, smtutil::Expression const& _error, unsigned _preIdx, unsigned _postIdx);
 
 smtutil::Expression constructor(Predicate const& _pred, EncodingContext& _context);
 smtutil::Expression constructorCall(Predicate const& _pred, EncodingContext& _context);

libsolidity/formal/PredicateSort.cpp

@@ -41,7 +41,11 @@ SortPointer nondetInterfaceSort(ContractDefinition const& _contract, SymbolicSta
 	auto varSorts = stateSorts(_contract);
 	vector<SortPointer> stateSort{_state.stateSort()};
 	return make_shared<FunctionSort>(
-		stateSort + varSorts + stateSort + varSorts,
+		vector<SortPointer>{_state.errorFlagSort(), _state.thisAddressSort(), _state.abiSort(), _state.cryptoSort()} +
+			stateSort +
+			varSorts +
+			stateSort +
+			varSorts,
 		SortProvider::boolSort
 	);
 }

libsolidity/formal/PredicateSort.h

@@ -37,7 +37,7 @@ namespace solidity::frontend::smt
  *
  * 2. Nondet interface
  * The nondeterminism behavior of a contract. Signature:
- * nondet_interface(blockchainState, stateVariables, blockchainState', stateVariables').
+ * nondet_interface(error, this, abiFunctions, cryptoFunctions, blockchainState, stateVariables, blockchainState', stateVariables').
  *
  * 3. Constructor entry/summary
  * The summary of a contract's deployment procedure.