Merge pull request #9731 from ethereum/smt_import

[SMTChecker] Fix CHC encoding

Changelog.md

@@ -45,6 +45,7 @@ Bugfixes:
  * SMTChecker: Fix internal error on lvalue unary operators with tuples.
  * SMTChecker: Fix internal error on tuple assignment.
  * SMTChecker: Fix internal error on tuples of one element that have tuple type.
+ * SMTChecker: Fix internal error when using imported code.
  * SMTChecker: Fix soundness of array ``pop``.
  * Type Checker: Disallow ``using for`` directive inside interfaces.
  * Type Checker: Disallow signed literals as exponent in exponentiation operator.

libsmtutil/CHCSmtLib2Interface.cpp

@@ -50,6 +50,7 @@ void CHCSmtLib2Interface::reset()
 {
 	m_accumulatedOutput.clear();
 	m_variables.clear();
+	m_unhandledQueries.clear();
 }
 
 void CHCSmtLib2Interface::registerRelation(Expression const& _expr)

libsolidity/formal/CHC.cpp

@@ -43,19 +43,19 @@ using namespace solidity::frontend;
 CHC::CHC(
 	smt::EncodingContext& _context,
 	ErrorReporter& _errorReporter,
-	map<util::h256, string> const& _smtlib2Responses,
-	ReadCallback::Callback const& _smtCallback,
-	[[maybe_unused]] smtutil::SMTSolverChoice _enabledSolvers
+	[[maybe_unused]] map<util::h256, string> const& _smtlib2Responses,
+	[[maybe_unused]] ReadCallback::Callback const& _smtCallback,
+	smtutil::SMTSolverChoice _enabledSolvers
 ):
 	SMTEncoder(_context),
 	m_outerErrorReporter(_errorReporter),
 	m_enabledSolvers(_enabledSolvers)
 {
-#ifdef HAVE_Z3
-	if (_enabledSolvers.z3)
-		m_interface = make_unique<smtutil::Z3CHCInterface>();
+	bool usesZ3 = _enabledSolvers.z3;
+#ifndef HAVE_Z3
+	usesZ3 = false;
 #endif
-	if (!m_interface)
+	if (!usesZ3)
 		m_interface = make_unique<smtutil::CHCSmtLib2Interface>(_smtlib2Responses, _smtCallback);
 }
 
@@ -63,30 +63,8 @@ void CHC::analyze(SourceUnit const& _source)
 {
 	solAssert(_source.annotation().experimentalFeatures.count(ExperimentalFeature::SMTChecker), "");
 
-	bool usesZ3 = false;
-#ifdef HAVE_Z3
-	usesZ3 = m_enabledSolvers.z3;
-	if (usesZ3)
-	{
-		auto z3Interface = dynamic_cast<smtutil::Z3CHCInterface const*>(m_interface.get());
-		solAssert(z3Interface, "");
-		m_context.setSolver(z3Interface->z3Interface());
-	}
-#endif
-	if (!usesZ3)
-	{
-		auto smtlib2Interface = dynamic_cast<smtutil::CHCSmtLib2Interface const*>(m_interface.get());
-		solAssert(smtlib2Interface, "");
-		m_context.setSolver(smtlib2Interface->smtlib2Interface());
-	}
-	m_context.clear();
-	m_context.setAssertionAccumulation(false);
-
 	resetSourceAnalysis();
 
-	m_genesisPredicate = createSymbolicBlock(arity0FunctionSort(), "genesis");
-	addRule(genesis(), "genesis");
-
 	set<SourceUnit const*, IdCompare> sources;
 	sources.insert(&_source);
 	for (auto const& source: _source.referencedSourceUnits(true))
@@ -131,7 +109,7 @@ bool CHC::visit(ContractDefinition const& _contract)
 void CHC::endVisit(ContractDefinition const& _contract)
 {
 	auto implicitConstructor = (*m_implicitConstructorPredicate)({});
-	connectBlocks(genesis(), implicitConstructor);
+	addRule(implicitConstructor, implicitConstructor.name);
 	m_currentBlock = implicitConstructor;
 	m_context.addAssertion(m_error.currentValue() == 0);
 
@@ -156,7 +134,7 @@ bool CHC::visit(FunctionDefinition const& _function)
 {
 	if (!_function.isImplemented())
 	{
-		connectBlocks(genesis(), summary(_function));
+		addRule(summary(_function), "summary_function_" + to_string(_function.id()));
 		return false;
 	}
 
@@ -184,7 +162,7 @@ bool CHC::visit(FunctionDefinition const& _function)
 	if (_function.isConstructor())
 		connectBlocks(m_currentBlock, functionPred);
 	else
-		connectBlocks(genesis(), functionPred);
+		addRule(functionPred, functionPred.name);
 
 	m_context.addAssertion(m_error.currentValue() == 0);
 	for (auto const* var: m_stateVariables)
@@ -676,6 +654,30 @@ void CHC::resetSourceAnalysis()
 	m_interfaces.clear();
 	m_nondetInterfaces.clear();
 	Predicate::reset();
+	m_blockCounter = 0;
+
+	bool usesZ3 = false;
+#ifdef HAVE_Z3
+	usesZ3 = m_enabledSolvers.z3;
+	if (usesZ3)
+	{
+		/// z3::fixedpoint does not have a reset mechanism, so we need to create another.
+		m_interface.reset(new smtutil::Z3CHCInterface());
+		auto z3Interface = dynamic_cast<smtutil::Z3CHCInterface const*>(m_interface.get());
+		solAssert(z3Interface, "");
+		m_context.setSolver(z3Interface->z3Interface());
+	}
+#endif
+	if (!usesZ3)
+	{
+		auto smtlib2Interface = dynamic_cast<smtutil::CHCSmtLib2Interface*>(m_interface.get());
+		smtlib2Interface->reset();
+		solAssert(smtlib2Interface, "");
+		m_context.setSolver(smtlib2Interface->smtlib2Interface());
+	}
+
+	m_context.clear();
+	m_context.setAssertionAccumulation(false);
 }
 
 void CHC::resetContractAnalysis()
@@ -861,27 +863,23 @@ void CHC::defineInterfacesAndSummaries(SourceUnit const& _source)
 {
 	for (auto const& node: _source.nodes())
 		if (auto const* contract = dynamic_cast<ContractDefinition const*>(node.get()))
+		{
+			string suffix = contract->name() + "_" + to_string(contract->id());
+			m_interfaces[contract] = createSymbolicBlock(interfaceSort(*contract), "interface_" + suffix);
+			m_nondetInterfaces[contract] = createSymbolicBlock(nondetInterfaceSort(*contract), "nondet_interface_" + suffix);
+
+			for (auto const* var: stateVariablesIncludingInheritedAndPrivate(*contract))
+				if (!m_context.knownVariable(*var))
+					createVariable(*var);
+
+			/// Base nondeterministic interface that allows
+			/// 0 steps to be taken, used as base for the inductive
+			/// rule for each function.
+			auto const& iface = *m_nondetInterfaces.at(contract);
+			auto state0 = stateVariablesAtIndex(0, *contract);
+			addRule(iface(state0 + state0), "base_nondet");
+
 			for (auto const* base: contract->annotation().linearizedBaseContracts)
-			{
-				for (auto const* var: SMTEncoder::stateVariablesIncludingInheritedAndPrivate(*base))
-					if (!m_context.knownVariable(*var))
-						createVariable(*var);
-
-				if (!m_interfaces.count(base))
-				{
-					solAssert(!m_nondetInterfaces.count(base), "");
-					string suffix = base->name() + "_" + to_string(base->id());
-					m_interfaces.emplace(base, createSymbolicBlock(interfaceSort(*base), "interface_" + suffix, base));
-					m_nondetInterfaces.emplace(base, createSymbolicBlock(nondetInterfaceSort(*base), "nondet_interface_" + suffix, base));
-
-					/// Base nondeterministic interface that allows
-					/// 0 steps to be taken, used as base for the inductive
-					/// rule for each function.
-					auto const* iface = m_nondetInterfaces.at(base);
-					auto state0 = stateVariablesAtIndex(0, *base);
-					addRule((*iface)(state0 + state0), "base_nondet");
-				}
-
 				for (auto const* function: base->definedFunctions())
 				{
 					for (auto var: function->parameters())
@@ -900,13 +898,11 @@ void CHC::defineInterfacesAndSummaries(SourceUnit const& _source)
 						!base->isInterface()
 					)
 					{
-						auto state1 = stateVariablesAtIndex(1, *base);
-						auto state2 = stateVariablesAtIndex(2, *base);
+						auto state1 = stateVariablesAtIndex(1, *contract);
+						auto state2 = stateVariablesAtIndex(2, *contract);
 
-						auto const* iface = m_nondetInterfaces.at(base);
-						auto state0 = stateVariablesAtIndex(0, *base);
-						auto nondetPre = (*iface)(state0 + state1);
-						auto nondetPost = (*iface)(state0 + state2);
+						auto nondetPre = iface(state0 + state1);
+						auto nondetPost = iface(state0 + state2);
 
 						vector<smtutil::Expression> args{m_error.currentValue()};
 						args += state1 +
@@ -915,10 +911,10 @@ void CHC::defineInterfacesAndSummaries(SourceUnit const& _source)
 							applyMap(function->parameters(), [this](auto _var) { return valueAtIndex(*_var, 1); }) +
 							applyMap(function->returnParameters(), [this](auto _var) { return valueAtIndex(*_var, 1); });
 
-						connectBlocks(nondetPre, nondetPost, (*m_summaries.at(base).at(function))(args));
+						connectBlocks(nondetPre, nondetPost, (*m_summaries.at(contract).at(function))(args));
 					}
-				}
 			}
+		}
 }
 
 smtutil::Expression CHC::interface()
@@ -1210,6 +1206,16 @@ void CHC::addVerificationTarget(
 	smtutil::Expression _errorId
 )
 {
+	solAssert(m_currentContract || m_currentFunction, "");
+	SourceUnit const* source = nullptr;
+	if (m_currentContract)
+		source = sourceUnitContaining(*m_currentContract);
+	else
+		source = sourceUnitContaining(*m_currentFunction);
+	solAssert(source, "");
+	if (!source->annotation().experimentalFeatures.count(ExperimentalFeature::SMTChecker))
+		return;
+
 	m_verificationTargets.emplace(_scope, CHCVerificationTarget{{_type, _from, _constraints}, _errorId});
 }
 
@@ -1459,7 +1465,11 @@ optional<string> CHC::generateCounterexample(CHCSolverInterface::CexGraph const&
 		/// Recurse on the next interface node which represents the previous transaction
 		/// or stop.
 		if (interfaceId)
+		{
+			Predicate const* interfacePredicate = Predicate::predicate(_graph.nodes.at(*interfaceId).first);
+			solAssert(interfacePredicate && interfacePredicate->isInterface(), "");
 			node = *interfaceId;
+		}
 		else
 			break;
 	}

libsolidity/formal/CHC.h

@@ -141,8 +141,6 @@ private:
 	/// in a given _source.
 	void defineInterfacesAndSummaries(SourceUnit const& _source);
 
-	/// Genesis predicate.
-	smtutil::Expression genesis() { return (*m_genesisPredicate)({}); }
 	/// Interface predicate over current variables.
 	smtutil::Expression interface();
 	smtutil::Expression interface(ContractDefinition const& _contract);
@@ -259,9 +257,6 @@ private:
 
 	/// Predicates.
 	//@{
-	/// Genesis predicate.
-	Predicate const* m_genesisPredicate = nullptr;
-
 	/// Implicit constructor predicate.
 	/// Explicit constructors are handled as functions.
 	Predicate const* m_implicitConstructorPredicate = nullptr;
@@ -293,9 +288,6 @@ private:
 		"error",
 		m_context
 	};
-
-	/// Maps predicate names to the ASTNodes they came from.
-	std::map<std::string, ASTNode const*> m_symbolFunction;
 	//@}
 
 	/// Variables.

libsolidity/formal/SMTEncoder.cpp

@@ -133,10 +133,7 @@ bool SMTEncoder::visit(FunctionDefinition const& _function)
 	if (_function.isConstructor())
 		inlineConstructorHierarchy(dynamic_cast<ContractDefinition const&>(*_function.scope()));
 
-	// Base constructors' parameters should be set by explicit calls,
-	// but the most derived one needs to be initialized.
-	if (_function.scope() == m_currentContract)
-		initializeLocalVariables(_function);
+	initializeLocalVariables(_function);
 
 	_function.parameterList().accept(*this);
 	if (_function.returnParameterList())
@@ -2055,6 +2052,14 @@ vector<VariableDeclaration const*> SMTEncoder::stateVariablesIncludingInheritedA
 	return stateVariablesIncludingInheritedAndPrivate(dynamic_cast<ContractDefinition const&>(*_function.scope()));
 }
 
+SourceUnit const* SMTEncoder::sourceUnitContaining(Scopable const& _scopable)
+{
+	for (auto const* s = &_scopable; s; s = dynamic_cast<Scopable const*>(s->scope()))
+		if (auto const* source = dynamic_cast<SourceUnit const*>(s->scope()))
+			return source;
+	solAssert(false, "");
+}
+
 void SMTEncoder::createReturnedExpressions(FunctionCall const& _funCall)
 {
 	FunctionDefinition const* funDef = functionCallToDefinition(_funCall);

libsolidity/formal/SMTEncoder.h

@@ -65,6 +65,9 @@ public:
 	static std::vector<VariableDeclaration const*> stateVariablesIncludingInheritedAndPrivate(ContractDefinition const& _contract);
 	static std::vector<VariableDeclaration const*> stateVariablesIncludingInheritedAndPrivate(FunctionDefinition const& _function);
 
+	/// @returns the SourceUnit that contains _scopable.
+	static SourceUnit const* sourceUnitContaining(Scopable const& _scopable);
+
 protected:
 	// TODO: Check that we do not have concurrent reads and writes to a variable,
 	// because the order of expression evaluation is undefined

test/externalTests/solc-js/solc-js.sh

@@ -48,6 +48,7 @@ function solcjs_test
 
     printLog "Copying SMTChecker tests..."
     cp -Rf "$TEST_DIR"/test/libsolidity/smtCheckerTests test/
+    rm -rf test/smtCheckerTests/imports
 
     # Update version (needed for some tests)
     echo "Updating package.json to version $VERSION"

test/libsolidity/smtCheckerTests/imports/imported_fail_1.sol

@@ -0,0 +1,25 @@
+==== Source:  ====
+import "B.sol";
+pragma experimental SMTChecker;
+contract C is B {
+	function h(uint _x) public view {
+		assert(_x < x);
+	}
+}
+==== Source: A.sol ====
+contract A {
+	uint x;
+	function f(uint _x) public {
+		x = _x;
+	}
+}
+==== Source: B.sol ====
+import "A.sol";
+contract B is A {
+	function g(uint _x) public view {
+		assert(_x > x);
+	}
+}
+// ----
+// Warning 6328: (103-117): Assertion violation happens here.
+// Warning 6328: (B.sol:71-85): Assertion violation happens here.

test/libsolidity/smtCheckerTests/imports/imported_fail_2.sol

@@ -0,0 +1,27 @@
+==== Source:  ====
+import "B.sol";
+pragma experimental SMTChecker;
+contract C is B {
+	function h(uint _x) public view {
+		assert(_x < x);
+	}
+}
+==== Source: A.sol ====
+contract A {
+	uint x;
+	function f(uint _x) public {
+		x = _x;
+	}
+}
+==== Source: B.sol ====
+import "A.sol";
+pragma experimental SMTChecker;
+contract B is A {
+	function g(uint _x) public view {
+		assert(_x > x);
+	}
+}
+// ----
+// Warning 6328: (B.sol:103-117): Assertion violation happens here.
+// Warning 6328: (103-117): Assertion violation happens here.
+// Warning 6328: (B.sol:103-117): Assertion violation happens here.

test/libsolidity/smtCheckerTests/imports/imported_fail_3.sol

@@ -0,0 +1,26 @@
+==== Source:  ====
+import "A.sol";
+pragma experimental SMTChecker;
+contract C is A {
+	function h(uint _x) public view {
+		assert(_x < x);
+	}
+}
+==== Source: A.sol ====
+contract A {
+	uint x;
+	function f(uint _x) public {
+		x = _x;
+	}
+}
+==== Source: B.sol ====
+import "A.sol";
+pragma experimental SMTChecker;
+contract B is A {
+	function g(uint _x) public view {
+		assert(_x > x);
+	}
+}
+// ----
+// Warning 6328: (103-117): Assertion violation happens here.
+// Warning 6328: (B.sol:103-117): Assertion violation happens here.

test/libsolidity/smtCheckerTests/imports/simple.sol

@@ -0,0 +1,6 @@
+==== Source: A.sol ====
+contract A { function f() public {} }
+==== Source:====
+import "A.sol";
+pragma experimental SMTChecker;
+contract C is A {}

test/libsolidity/smtCheckerTests/imports/simple_imported_fail_no_pragma.sol

@@ -0,0 +1,12 @@
+==== Source:  ====
+import "A.sol";
+pragma experimental SMTChecker;
+contract C is A {}
+==== Source: A.sol ====
+contract A {
+	function f(uint x) public pure {
+		assert(x > 0);
+	}
+}
+// ----
+// Warning 6328: (A.sol:49-62): Assertion violation happens here.

test/libsolidity/smtCheckerTests/imports/simple_imported_fail_two_pragmas.sol

@@ -0,0 +1,14 @@
+==== Source:  ====
+import "A.sol";
+pragma experimental SMTChecker;
+contract C is A {}
+==== Source: A.sol ====
+pragma experimental SMTChecker;
+contract A {
+	function f(uint x) public pure {
+		assert(x > 0);
+	}
+}
+// ----
+// Warning 6328: (A.sol:81-94): Assertion violation happens here.
+// Warning 6328: (A.sol:81-94): Assertion violation happens here.

test/libsolidity/smtCheckerTests/operators/shifts/shift_right_uint8.sol

@@ -1,19 +0,0 @@
-pragma experimental SMTChecker;
-
-contract C {
-    function f(uint8 a, uint8 b) internal pure returns (uint256) {
-        return a >> b;
-    }
-	function t() public pure {
-		assert(f(0x66, 0) == 0x66);
-		// Fails because the above is true.
-		assert(f(0x66, 0) == 0x6);
-
-		assert(f(0x66, 8) == 0);
-		// Fails because the above is true.
-		assert(f(0x66, 8) == 1);
-	}
-}
-// ----
-// Warning 6328: (240-265): Assertion violation happens here.
-// Warning 6328: (335-358): Assertion violation happens here.