Merge pull request #11852 from ethereum/smt_fix_at

Fix ICE on multi-source use of abi.*

Author: Leonardo

Changelog.md

@@ -12,6 +12,7 @@ Compiler Features:
 
 Bugfixes:
  * SMTChecker: Fix false positive in external calls from constructors.
+ * SMTChecker: Fix internal error on some multi-source uses of ``abi.*``, cryptographic functions and constants.
 
 
 

libsolidity/formal/BMC.cpp

@@ -75,30 +75,30 @@ void BMC::analyze(SourceUnit const& _source, map<ASTNode const*, set<Verificatio
 		return;
 	}
 
-	if (SMTEncoder::analyze(_source))
-	{
-		m_solvedTargets = move(_solvedTargets);
-		m_context.setSolver(m_interface.get());
-		m_context.reset();
-		m_context.setAssertionAccumulation(true);
-		m_variableUsage.setFunctionInlining(shouldInlineFunctionCall);
-		createFreeConstants(sourceDependencies(_source));
-		m_unprovedAmt = 0;
+	SMTEncoder::resetSourceAnalysis();
 
-		_source.accept(*this);
+	m_solvedTargets = move(_solvedTargets);
+	m_context.setSolver(m_interface.get());
+	m_context.reset();
+	m_context.setAssertionAccumulation(true);
+	m_variableUsage.setFunctionInlining(shouldInlineFunctionCall);
+	createFreeConstants(sourceDependencies(_source));
+	state().prepareForSourceUnit(_source);
+	m_unprovedAmt = 0;
 
-		if (m_unprovedAmt > 0 && !m_settings.showUnproved)
-			m_errorReporter.warning(
-				2788_error,
-				{},
-				"BMC: " +
-				to_string(m_unprovedAmt) +
-				" verification condition(s) could not be proved." +
-				" Enable the model checker option \"show unproved\" to see all of them." +
-				" Consider choosing a specific contract to be verified in order to reduce the solving problems." +
-				" Consider increasing the timeout per query."
-			);
-	}
+	_source.accept(*this);
+
+	if (m_unprovedAmt > 0 && !m_settings.showUnproved)
+		m_errorReporter.warning(
+			2788_error,
+			{},
+			"BMC: " +
+			to_string(m_unprovedAmt) +
+			" verification condition(s) could not be proved." +
+			" Enable the model checker option \"show unproved\" to see all of them." +
+			" Consider choosing a specific contract to be verified in order to reduce the solving problems." +
+			" Consider increasing the timeout per query."
+		);
 
 	// If this check is true, Z3 and CVC4 are not available
 	// and the query answers were not provided, since SMTPortfolio

libsolidity/formal/CHC.cpp

@@ -87,20 +87,19 @@ void CHC::analyze(SourceUnit const& _source)
 		return;
 	}
 
-	if (SMTEncoder::analyze(_source))
-	{
-		resetSourceAnalysis();
+	resetSourceAnalysis();
 
-		auto sources = sourceDependencies(_source);
-		collectFreeFunctions(sources);
-		createFreeConstants(sources);
-		for (auto const* source: sources)
-			defineInterfacesAndSummaries(*source);
-		for (auto const* source: sources)
-			source->accept(*this);
+	auto sources = sourceDependencies(_source);
+	collectFreeFunctions(sources);
+	createFreeConstants(sources);
+	state().prepareForSourceUnit(_source);
 
-		checkVerificationTargets();
-	}
+	for (auto const* source: sources)
+		defineInterfacesAndSummaries(*source);
+	for (auto const* source: sources)
+		source->accept(*this);
+
+	checkVerificationTargets();
 
 	bool ranSolver = true;
 	// If ranSolver is true here it's because an SMT solver callback was
@@ -947,6 +946,8 @@ pair<smtutil::Expression, smtutil::Expression> CHC::arithmeticOperation(
 
 void CHC::resetSourceAnalysis()
 {
+	SMTEncoder::resetSourceAnalysis();
+
 	m_safeTargets.clear();
 	m_unsafeTargets.clear();
 	m_unprovedTargets.clear();

libsolidity/formal/SMTEncoder.cpp

@@ -56,11 +56,9 @@ SMTEncoder::SMTEncoder(
 {
 }
 
-bool SMTEncoder::analyze(SourceUnit const& _source)
+void SMTEncoder::resetSourceAnalysis()
 {
-	state().prepareForSourceUnit(_source);
-
-	return true;
+	m_freeFunctions.clear();
 }
 
 bool SMTEncoder::visit(ContractDefinition const& _contract)

libsolidity/formal/SMTEncoder.h

@@ -59,9 +59,6 @@ class SMTEncoder: public ASTConstVisitor
 		langutil::CharStreamProvider const& _charStreamProvider
 	);
 
-	/// @returns true if engine should proceed with analysis.
-	bool analyze(SourceUnit const& _sources);
-
 	/// @returns the leftmost identifier in a multi-d IndexAccess.
 	static Expression const* leftmostBase(IndexAccess const& _indexAccess);
 
@@ -123,6 +120,8 @@ class SMTEncoder: public ASTConstVisitor
 	static std::set<SourceUnit const*, ASTNode::CompareByID> sourceDependencies(SourceUnit const& _source);
 
 protected:
+	void resetSourceAnalysis();
+
 	// TODO: Check that we do not have concurrent reads and writes to a variable,
 	// because the order of expression evaluation is undefined
 	// TODO: or just force a certain order, but people might have a different idea about that.

libsolidity/formal/SymbolicState.cpp

@@ -78,10 +78,8 @@ void SymbolicState::reset()
 	m_state.reset();
 	m_tx.reset();
 	m_crypto.reset();
-	/// We don't reset m_abi's pointer nor clear m_abiMembers on purpose,
-	/// since it only helps to keep the already generated types.
-	solAssert(m_abi, "");
-	m_abi->reset();
+	if (m_abi)
+		m_abi->reset();
 }
 
 smtutil::Expression SymbolicState::balances() const

test/libsolidity/smtCheckerTests/file_level/abi_function_different_source.sol

@@ -0,0 +1,9 @@
+==== Source: s1.sol ====
+function f() {
+	ecrecover("1234", 1, "0", abi.decode("", (bytes2)));
+}
+==== Source: s2.sol ====
+contract C {}
+// ----
+// Warning 6133: (s1.sol:16-67): Statement has no effect.
+// Warning 2018: (s1.sol:0-70): Function state mutability can be restricted to pure

test/libsolidity/smtCheckerTests/file_level/abi_function_different_source_2.sol

@@ -0,0 +1,9 @@
+==== Source: s1.sol ====
+function f() {
+	ecrecover("", 1, "", "");
+}
+==== Source: s2.sol ====
+contract C {}
+// ----
+// Warning 6133: (s1.sol:16-40): Statement has no effect.
+// Warning 2018: (s1.sol:0-43): Function state mutability can be restricted to pure

test/libsolidity/smtCheckerTests/file_level/constant_different_source.sol

@@ -0,0 +1,12 @@
+==== Source: l.sol ====
+library L {
+	int constant one = 1;
+	function f() internal {
+		one;
+	}
+}
+==== Source: s1.sol ====
+library L {}
+// ----
+// Warning 6133: (l.sol:62-65): Statement has no effect.
+// Warning 2018: (l.sol:36-69): Function state mutability can be restricted to pure

test/libsolidity/smtCheckerTests/verification_target/simple_assert.sol

@@ -3,5 +3,6 @@ contract C {
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreCex: yes
 // ----
-// Warning 6328: (50-64): CHC: Assertion violation happens here.\nCounterexample:\n\na = 0\n\nTransaction trace:\nC.constructor()\nC.f(0)
+// Warning 6328: (50-64): CHC: Assertion violation happens here.