Merge pull request #7270 from ethereum/develop

Update develop_060 from develop

.circleci/README.md

@@ -7,8 +7,8 @@ The docker images are build locally on the developer machine:
 ```!sh
 cd .circleci/docker/
 
-docker build -t ethereum/solc-buildpack-deps:ubuntu1904 -f Dockerfile.ubuntu1904 .
-docker push solidity/solc-buildpack-deps:ubuntu1904
+docker build -t ethereum/solidity-buildpack-deps:ubuntu1904 -f Dockerfile.ubuntu1904 .
+docker push ethereum/solidity-buildpack-deps:ubuntu1904
 ```
 
 which you can find on Dockerhub after the push at:
@@ -16,3 +16,13 @@ which you can find on Dockerhub after the push at:
     https://hub.docker.com/r/ethereum/solidity-buildpack-deps
 
 where the image tag reflects the target OS to build Solidity and run its test on.
+
+### Testing docker images locally
+
+```!sh
+cd solidity
+# Mounts your local solidity directory in docker container for testing
+docker run -v `pwd`:/src/solidity -ti ethereum/solidity-buildpack-deps:ubuntu1904 /bin/bash
+cd /src/solidity
+<commands_to_test_build_with_new_docker_image>
+```

.circleci/config.yml

@@ -322,7 +322,7 @@ jobs:
       TERM: xterm
       CC: /usr/bin/clang-8
       CXX: /usr/bin/clang++-8
-      CMAKE_OPTIONS: -DOSSFUZZ=1 -DCMAKE_TOOLCHAIN_FILE=cmake/toolchains/libfuzzer.cmake
+      CMAKE_OPTIONS: -DCMAKE_TOOLCHAIN_FILE=cmake/toolchains/libfuzzer.cmake
     steps:
       - checkout
       - run: *setup_prerelease_commit_hash

.circleci/docker/Dockerfile.ubuntu1904

@@ -33,7 +33,7 @@ RUN set -ex; \
 	apt-get install -qqy --no-install-recommends \
 		build-essential \
 		software-properties-common \
-		cmake ninja-build clang++-8 \
+		cmake ninja-build clang++-8 libc++-8-dev libc++abi-8-dev \
 		libboost-regex-dev libboost-filesystem-dev libboost-test-dev libboost-system-dev \
 		libboost-program-options-dev \
 		libjsoncpp-dev \

Changelog.md

@@ -38,9 +38,11 @@ Compiler Features:
  * Standard JSON Interface: Provide secondary error locations (e.g. the source position of other conflicting declarations).
  * SMTChecker: Do not erase knowledge about storage pointers if another storage pointer is assigned.
  * SMTChecker: Support string literal type.
+ * SMTChecker: New Horn-based algorithm that proves assertions via multi-transaction contract invariants.
  * Standard JSON Interface: Provide AST even on errors if ``--error-recovery`` commandline switch or StandardCompiler `settings.parserErrorRecovery` is true.
  * Yul Optimizer: Do not inline function if it would result in expressions being duplicated that are not cheap.
 
+
 Bugfixes:
  * ABI decoder: Ensure that decoded arrays always point to distinct memory locations.
  * Code Generator: Treat dynamically encoded but statically sized arrays and structs in calldata properly.

cmake/jsoncpp.cmake

@@ -19,7 +19,14 @@ if(EMSCRIPTEN)
     # at the moment.
     set(JSONCPP_CXX_FLAGS -std=c++17)
 else()
-    set(JSONCPP_CXX_FLAGS ${CMAKE_CXX_FLAGS})
+    # jsoncpp uses implicit casts for comparing integer and
+    # floating point numbers. This causes clang-10 (used by ossfuzz builder)
+    # to error on the implicit conversions. Here, we request jsoncpp
+    # to unconditionally use static casts for these conversions by defining the
+    # JSON_USE_INT64_DOUBLE_CONVERSION preprocessor macro. Doing so,
+    # not only gets rid of the implicit conversion error that clang-10 produces
+    # but also forces safer behavior in general.
+    set(JSONCPP_CXX_FLAGS "${CMAKE_CXX_FLAGS} -DJSON_USE_INT64_DOUBLE_CONVERSION")
 endif()
 
 set(byproducts "")

cmake/toolchains/libfuzzer.cmake

@@ -1,2 +1,9 @@
-# Require libfuzzer specific flags
-set(CMAKE_CXX_FLAGS "-O1 -gline-tables-only -fsanitize=address -fsanitize-address-use-after-scope -fsanitize=fuzzer-no-link -stdlib=libstdc++ -fopenmp=libgomp")
+# Inherit default options
+include("${CMAKE_CURRENT_LIST_DIR}/default.cmake")
+# Disable Z3 and CVC4 since none of the existing fuzzers need them
+set(USE_Z3 OFF CACHE BOOL "" FORCE)
+set(USE_CVC4 OFF CACHE BOOL "" FORCE)
+# Build fuzzing binaries
+set(OSSFUZZ 1)
+# clang/libfuzzer specific flags for ASan instrumentation
+set(CMAKE_CXX_FLAGS "-O1 -gline-tables-only -fsanitize=address -fsanitize-address-use-after-scope -fsanitize=fuzzer-no-link -stdlib=libstdc++")

libdevcore/Algorithms.h

@@ -78,17 +78,18 @@ private:
 /**
  * Generic breadth first search.
  *
+ * Note that V needs to be a comparable value type. If it is not, use a pointer type,
+ * but note that this might lead to non-deterministic traversal.
+ *
  * Example: Gather all (recursive) children in a graph starting at (and including) ``root``:
  *
  * Node const* root = ...;
- * std::set<Node> allNodes = BreadthFirstSearch<Node>{{root}}.run([](Node const& _node, auto&& _addChild) {
+ * std::set<Node const*> allNodes = BreadthFirstSearch<Node const*>{{root}}.run([](Node const* _node, auto&& _addChild) {
  *   // Potentially process ``_node``.
- *   for (Node const& _child: _node.children())
+ *   for (Node const& _child: _node->children())
  *     // Potentially filter the children to be visited.
- *     _addChild(_child);
+ *     _addChild(&_child);
  * }).visited;
- *
- * Note that the order of the traversal is *non-deterministic* (the children are stored in a std::set of pointers).
  */
 template<typename V>
 struct BreadthFirstSearch
@@ -102,20 +103,20 @@ struct BreadthFirstSearch
 	{
 		while (!verticesToTraverse.empty())
 		{
-			V const* v = *verticesToTraverse.begin();
+			V v = *verticesToTraverse.begin();
 			verticesToTraverse.erase(verticesToTraverse.begin());
 			visited.insert(v);
 
-			_forEachChild(*v, [this](V const& _vertex) {
-				if (!visited.count(&_vertex))
-					verticesToTraverse.insert(&_vertex);
+			_forEachChild(v, [this](V _vertex) {
+				if (!visited.count(_vertex))
+					verticesToTraverse.emplace(std::move(_vertex));
 			});
 		}
 		return *this;
 	}
 
-	std::set<V const*> verticesToTraverse;
-	std::set<V const*> visited{};
+	std::set<V> verticesToTraverse;
+	std::set<V> visited{};
 };
 
 }

libsolidity/analysis/ControlFlowAnalyzer.cpp

@@ -151,22 +151,22 @@ void ControlFlowAnalyzer::checkUninitializedAccess(CFGNode const* _entry, CFGNod
 void ControlFlowAnalyzer::checkUnreachable(CFGNode const* _entry, CFGNode const* _exit, CFGNode const* _revert) const
 {
 	// collect all nodes reachable from the entry point
-	std::set<CFGNode const*> reachable = BreadthFirstSearch<CFGNode>{{_entry}}.run(
-		[](CFGNode const& _node, auto&& _addChild) {
-			for (CFGNode const* exit: _node.exits)
-				_addChild(*exit);
+	std::set<CFGNode const*> reachable = BreadthFirstSearch<CFGNode const*>{{_entry}}.run(
+		[](CFGNode const* _node, auto&& _addChild) {
+			for (CFGNode const* exit: _node->exits)
+				_addChild(exit);
 		}
 	).visited;
 
 	// traverse all paths backwards from exit and revert
 	// and extract (valid) source locations of unreachable nodes into sorted set
 	std::set<SourceLocation> unreachable;
-	BreadthFirstSearch<CFGNode>{{_exit, _revert}}.run(
-		[&](CFGNode const& _node, auto&& _addChild) {
-			if (!reachable.count(&_node) && !_node.location.isEmpty())
-				unreachable.insert(_node.location);
-			for (CFGNode const* entry: _node.entries)
-				_addChild(*entry);
+	BreadthFirstSearch<CFGNode const*>{{_exit, _revert}}.run(
+		[&](CFGNode const* _node, auto&& _addChild) {
+			if (!reachable.count(_node) && !_node->location.isEmpty())
+				unreachable.insert(_node->location);
+			for (CFGNode const* entry: _node->entries)
+				_addChild(entry);
 		}
 	);
 

libsolidity/formal/CHC.cpp

@@ -135,6 +135,44 @@ bool CHC::visit(FunctionDefinition const& _function)
 	solAssert(!m_currentFunction, "Inlining internal function calls not yet implemented");
 	m_currentFunction = &_function;
 
+	initFunction(_function);
+
+	// Store the constraints related to variable initialization.
+	smt::Expression const& initAssertions = m_context.assertions();
+
+	createFunctionBlock(*m_currentFunction);
+
+	// Rule Interface -> FunctionEntry, uses no constraints.
+	smt::Expression interfaceFunction = smt::Expression::implies(
+		interface(),
+		predicateCurrent(m_currentFunction)
+	);
+	m_interface->addRule(
+		interfaceFunction,
+		m_interfacePredicate->currentName() + "_to_" + m_predicates.at(m_currentFunction)->currentName()
+	);
+
+	pushBlock(predicateCurrent(m_currentFunction));
+
+	createFunctionBlock(m_currentFunction->body());
+
+	// Rule FunctionEntry -> FunctionBody, also no constraints.
+	smt::Expression functionBody = smt::Expression::implies(
+		predicateEntry(m_currentFunction),
+		predicateBodyCurrent(&m_currentFunction->body())
+	);
+	m_interface->addRule(
+		functionBody,
+		m_predicates.at(m_currentFunction)->currentName() + "_to_" + m_predicates.at(&m_currentFunction->body())->currentName()
+	);
+
+	pushBlock(predicateBodyCurrent(&m_currentFunction->body()));
+	// We need to re-add the constraints that were created for initialization of variables.
+	m_context.addAssertion(initAssertions);
+
+	solAssert(m_functionBlocks == 0, "");
+	m_functionBlocks = 2;
+
 	SMTEncoder::visit(*m_currentFunction);
 
 	return false;
@@ -146,7 +184,36 @@ void CHC::endVisit(FunctionDefinition const& _function)
 		return;
 
 	solAssert(m_currentFunction == &_function, "Inlining internal function calls not yet implemented");
+
+	// Create Function Exit block.
+	createFunctionBlock(*m_currentFunction);
+
+	// Rule FunctionBody -> FunctionExit.
+	smt::Expression bodyFunction = smt::Expression::implies(
+		predicateEntry(&_function.body()) && m_context.assertions(),
+		predicateCurrent(&_function)
+	);
+	m_interface->addRule(
+		bodyFunction,
+		m_predicates.at(&_function.body())->currentName() + "_to_" + m_predicates.at(&_function.body())->currentName()
+	);
+
+	// Rule FunctionExit -> Interface, uses no constraints.
+	smt::Expression functionInterface = smt::Expression::implies(
+		predicateCurrent(&_function),
+		interface()
+	);
+	m_interface->addRule(
+		functionInterface,
+		m_predicates.at(&_function)->currentName() + "_to_" + m_interfacePredicate->currentName()
+	);
+
 	m_currentFunction = nullptr;
+	solAssert(m_path.size() == m_functionBlocks, "");
+	for (unsigned i = 0; i < m_path.size(); ++i)
+		m_context.popSolver();
+	m_functionBlocks = 0;
+	m_path.clear();
 
 	SMTEncoder::endVisit(_function);
 }
@@ -155,8 +222,30 @@ bool CHC::visit(IfStatement const& _if)
 {
 	solAssert(m_currentFunction, "");
 
+	bool unknownFunctionCallWasSeen = m_unknownFunctionCallSeen;
+	m_unknownFunctionCallSeen = false;
+
 	SMTEncoder::visit(_if);
 
+	if (m_unknownFunctionCallSeen)
+		eraseKnowledge();
+
+	m_unknownFunctionCallSeen = unknownFunctionCallWasSeen;
+
+	return false;
+}
+
+bool CHC::visit(WhileStatement const& _while)
+{
+	eraseKnowledge();
+	m_context.resetVariables(touchedVariables(_while));
+	return false;
+}
+
+bool CHC::visit(ForStatement const& _for)
+{
+	eraseKnowledge();
+	m_context.resetVariables(touchedVariables(_for));
 	return false;
 }
 
@@ -164,20 +253,74 @@ void CHC::endVisit(FunctionCall const& _funCall)
 {
 	solAssert(_funCall.annotation().kind != FunctionCallKind::Unset, "");
 
-	if (_funCall.annotation().kind == FunctionCallKind::FunctionCall)
+	if (_funCall.annotation().kind != FunctionCallKind::FunctionCall)
 	{
-		FunctionType const& funType = dynamic_cast<FunctionType const&>(*_funCall.expression().annotation().type);
-		if (funType.kind() == FunctionType::Kind::Assert)
-			visitAssert(_funCall);
+		SMTEncoder::endVisit(_funCall);
+		return;
 	}
 
-	SMTEncoder::endVisit(_funCall);
+	FunctionType const& funType = dynamic_cast<FunctionType const&>(*_funCall.expression().annotation().type);
+	switch (funType.kind())
+	{
+	case FunctionType::Kind::Assert:
+		visitAssert(_funCall);
+		SMTEncoder::endVisit(_funCall);
+		break;
+	case FunctionType::Kind::Internal:
+	case FunctionType::Kind::External:
+	case FunctionType::Kind::DelegateCall:
+	case FunctionType::Kind::BareCall:
+	case FunctionType::Kind::BareCallCode:
+	case FunctionType::Kind::BareDelegateCall:
+	case FunctionType::Kind::BareStaticCall:
+	case FunctionType::Kind::Creation:
+	case FunctionType::Kind::KECCAK256:
+	case FunctionType::Kind::ECRecover:
+	case FunctionType::Kind::SHA256:
+	case FunctionType::Kind::RIPEMD160:
+	case FunctionType::Kind::BlockHash:
+	case FunctionType::Kind::AddMod:
+	case FunctionType::Kind::MulMod:
+		SMTEncoder::endVisit(_funCall);
+		unknownFunctionCall(_funCall);
+		break;
+	default:
+		SMTEncoder::endVisit(_funCall);
+		break;
+	}
 
 	createReturnedExpressions(_funCall);
 }
 
-void CHC::visitAssert(FunctionCall const&)
+void CHC::visitAssert(FunctionCall const& _funCall)
 {
+	auto const& args = _funCall.arguments();
+	solAssert(args.size() == 1, "");
+	solAssert(args.front()->annotation().type->category() == Type::Category::Bool, "");
+
+	solAssert(!m_path.empty(), "");
+
+	smt::Expression assertNeg = !(m_context.expression(*args.front())->currentValue());
+	smt::Expression assertionError = smt::Expression::implies(
+		m_path.back() && m_context.assertions() && currentPathConditions() && assertNeg,
+		error()
+	);
+	string predicateName = "assert_" + to_string(_funCall.id());
+	m_interface->addRule(assertionError, predicateName + "_to_error");
+
+	m_verificationTargets.push_back(&_funCall);
+}
+
+void CHC::unknownFunctionCall(FunctionCall const&)
+{
+	/// Function calls are not handled at the moment,
+	/// so always erase knowledge.
+	/// TODO remove when function calls get predicates/blocks.
+	eraseKnowledge();
+
+	/// Used to erase outer scope knowledge in loops and ifs.
+	/// TODO remove when function calls get predicates/blocks.
+	m_unknownFunctionCallSeen = true;
 }
 
 void CHC::reset()
@@ -186,6 +329,13 @@ void CHC::reset()
 	m_stateVariables.clear();
 	m_verificationTargets.clear();
 	m_safeAssertions.clear();
+	m_unknownFunctionCallSeen = false;
+}
+
+void CHC::eraseKnowledge()
+{
+	resetStateVariables();
+	m_context.resetVariables([&](VariableDeclaration const& _variable) { return _variable.hasReferenceOrMappingType(); });
 }
 
 bool CHC::shouldVisit(ContractDefinition const& _contract) const
@@ -208,13 +358,25 @@ bool CHC::shouldVisit(FunctionDefinition const& _function) const
 	return false;
 }
 
+void CHC::pushBlock(smt::Expression const& _block)
+{
+	m_context.pushSolver();
+	m_path.push_back(_block);
+}
+
+void CHC::popBlock()
+{
+	m_context.popSolver();
+	m_path.pop_back();
+}
+
 smt::SortPointer CHC::constructorSort()
 {
 	solAssert(m_currentContract, "");
 	auto boolSort = make_shared<smt::Sort>(smt::Kind::Bool);
 	if (!m_currentContract->constructor())
 		return make_shared<smt::FunctionSort>(vector<smt::SortPointer>{}, boolSort);
-	return functionSort(*m_currentContract->constructor());
+	return sort(*m_currentContract->constructor());
 }
 
 smt::SortPointer CHC::interfaceSort()
@@ -226,14 +388,41 @@ smt::SortPointer CHC::interfaceSort()
 	);
 }
 
-smt::SortPointer CHC::functionSort(FunctionDefinition const& _function)
+smt::SortPointer CHC::sort(FunctionDefinition const& _function)
 {
+	if (m_nodeSorts.count(&_function))
+		return m_nodeSorts.at(&_function);
+
 	auto boolSort = make_shared<smt::Sort>(smt::Kind::Bool);
-	auto const& funType = dynamic_cast<FunctionType const&>(*_function.type());
-	return make_shared<smt::FunctionSort>(
-		smt::smtSort(funType.parameterTypes()),
+	vector<smt::SortPointer> varSorts;
+	for (auto const& var: _function.parameters() + _function.returnParameters())
+		varSorts.push_back(smt::smtSort(*var->type()));
+	auto sort = make_shared<smt::FunctionSort>(
+		m_stateSorts + varSorts,
 		boolSort
 	);
+	return m_nodeSorts[&_function] = move(sort);
+}
+
+smt::SortPointer CHC::sort(Block const& _block)
+{
+	if (m_nodeSorts.count(&_block))
+		return m_nodeSorts.at(&_block);
+
+	solAssert(_block.scope() == m_currentFunction, "");
+
+	auto fSort = dynamic_pointer_cast<smt::FunctionSort>(sort(*m_currentFunction));
+	solAssert(fSort, "");
+
+	auto boolSort = make_shared<smt::Sort>(smt::Kind::Bool);
+	vector<smt::SortPointer> varSorts;
+	for (auto const& var: m_currentFunction->localVariables())
+		varSorts.push_back(smt::smtSort(*var->type()));
+	auto functionBodySort = make_shared<smt::FunctionSort>(
+		fSort->domain + varSorts,
+		boolSort
+	);
+	return m_nodeSorts[&_block] = move(functionBodySort);
 }
 
 unique_ptr<smt::SymbolicFunctionVariable> CHC::createBlock(smt::SortPointer _sort, string const& _name)
@@ -273,6 +462,81 @@ smt::Expression CHC::error()
 	return (*m_errorPredicate)({});
 }
 
+void CHC::createFunctionBlock(FunctionDefinition const& _function)
+{
+	if (m_predicates.count(&_function))
+	{
+		m_predicates.at(&_function)->increaseIndex();
+		m_interface->registerRelation(m_predicates.at(&_function)->currentValue());
+	}
+	else
+		m_predicates[&_function] = createBlock(
+			sort(_function),
+			predicateName(_function)
+		);
+}
+
+void CHC::createFunctionBlock(Block const& _block)
+{
+	solAssert(_block.scope() == m_currentFunction, "");
+	if (m_predicates.count(&_block))
+	{
+		m_predicates.at(&_block)->increaseIndex();
+		m_interface->registerRelation(m_predicates.at(&_block)->currentValue());
+	}
+	else
+		m_predicates[&_block] = createBlock(
+			sort(_block),
+			predicateName(*m_currentFunction) + "_body"
+		);
+}
+
+vector<smt::Expression> CHC::currentFunctionVariables()
+{
+	solAssert(m_currentFunction, "");
+	vector<smt::Expression> paramExprs;
+	for (auto const& var: m_stateVariables)
+		paramExprs.push_back(m_context.variable(*var)->currentValue());
+	for (auto const& var: m_currentFunction->parameters() + m_currentFunction->returnParameters())
+		paramExprs.push_back(m_context.variable(*var)->currentValue());
+	return paramExprs;
+}
+
+vector<smt::Expression> CHC::currentBlockVariables()
+{
+	solAssert(m_currentFunction, "");
+	vector<smt::Expression> paramExprs;
+	for (auto const& var: m_currentFunction->localVariables())
+		paramExprs.push_back(m_context.variable(*var)->currentValue());
+	return currentFunctionVariables() + paramExprs;
+}
+
+string CHC::predicateName(FunctionDefinition const& _function)
+{
+	string functionName = _function.isConstructor() ?
+		"constructor" :
+		_function.isFallback() ?
+			"fallback" :
+			"function_" + _function.name();
+	return functionName + "_" + to_string(_function.id());
+}
+
+smt::Expression CHC::predicateCurrent(ASTNode const* _node)
+{
+	return (*m_predicates.at(_node))(currentFunctionVariables());
+}
+
+smt::Expression CHC::predicateBodyCurrent(ASTNode const* _node)
+{
+	return (*m_predicates.at(_node))(currentBlockVariables());
+}
+
+smt::Expression CHC::predicateEntry(ASTNode const* _node)
+{
+	solAssert(!m_path.empty(), "");
+	return (*m_predicates.at(_node))(m_path.back().arguments);
+}
+
 bool CHC::query(smt::Expression const& _query, langutil::SourceLocation const& _location)
 {
 	smt::CheckResult result;

libsolidity/formal/CHC.h

@@ -58,23 +58,30 @@ private:
 	bool visit(FunctionDefinition const& _node) override;
 	void endVisit(FunctionDefinition const& _node) override;
 	bool visit(IfStatement const& _node) override;
+	bool visit(WhileStatement const&) override;
+	bool visit(ForStatement const&) override;
 	void endVisit(FunctionCall const& _node) override;
 
 	void visitAssert(FunctionCall const& _funCall);
+	void unknownFunctionCall(FunctionCall const& _funCall);
 	//@}
 
 	/// Helpers.
 	//@{
 	void reset();
+	void eraseKnowledge();
 	bool shouldVisit(ContractDefinition const& _contract) const;
 	bool shouldVisit(FunctionDefinition const& _function) const;
+	void pushBlock(smt::Expression const& _block);
+	void popBlock();
 	//@}
 
 	/// Sort helpers.
 	//@{
 	smt::SortPointer constructorSort();
 	smt::SortPointer interfaceSort();
-	smt::SortPointer functionSort(FunctionDefinition const& _function);
+	smt::SortPointer sort(FunctionDefinition const& _function);
+	smt::SortPointer sort(Block const& _block);
 	//@}
 
 	/// Predicate helpers.
@@ -88,6 +95,33 @@ private:
 	smt::Expression interface();
 	/// Error predicate over current variables.
 	smt::Expression error();
+
+	/// Creates a block for the given _function or increases its SSA index
+	/// if the block already exists which in practice creates a new function.
+	/// The predicate parameters are _function input and output parameters.
+	void createFunctionBlock(FunctionDefinition const& _function);
+	/// Creates a block for the given _function or increases its SSA index
+	/// if the block already exists which in practice creates a new function.
+	/// The predicate parameters are m_currentFunction input, output
+	/// and local variables.
+	void createFunctionBlock(Block const& _block);
+
+	/// @returns the current symbolic values of the current function's
+	/// input and output parameters.
+	std::vector<smt::Expression> currentFunctionVariables();
+	/// @returns the samve as currentFunctionVariables plus
+	/// local variables.
+	std::vector<smt::Expression> currentBlockVariables();
+
+	/// @returns the predicate name for a given function.
+	std::string predicateName(FunctionDefinition const& _function);
+	/// @returns a predicate application over the current function's parameters.
+	smt::Expression predicateCurrent(ASTNode const* _node);
+	/// @returns a predicate application over the current function's parameters plus local variables.
+	smt::Expression predicateBodyCurrent(ASTNode const* _node);
+	/// Predicate for block _node over the variables at the latest
+	/// block entry.
+	smt::Expression predicateEntry(ASTNode const* _node);
 	//@}
 
 	/// Solver related.
@@ -109,6 +143,9 @@ private:
 	/// Artificial Error predicate.
 	/// Single error block for all assertions.
 	std::unique_ptr<smt::SymbolicVariable> m_errorPredicate;
+
+	/// Maps AST nodes to their predicates.
+	std::unordered_map<ASTNode const*, std::shared_ptr<smt::SymbolicVariable>> m_predicates;
 	//@}
 
 	/// Variables.
@@ -119,6 +156,9 @@ private:
 	/// State variables.
 	/// Used to create all predicates.
 	std::vector<VariableDeclaration const*> m_stateVariables;
+
+	/// Input sorts for AST nodes.
+	std::map<ASTNode const*, smt::SortPointer> m_nodeSorts;
 	//@}
 
 	/// Verification targets.
@@ -132,6 +172,13 @@ private:
 	/// Control-flow.
 	//@{
 	FunctionDefinition const* m_currentFunction = nullptr;
+
+	/// Number of basic blocks created for the body of the current function.
+	unsigned m_functionBlocks = 0;
+	/// The current control flow path.
+	std::vector<smt::Expression> m_path;
+	/// Whether a function call was seen in the current scope.
+	bool m_unknownFunctionCallSeen = false;
 	//@}
 
 	/// CHC solver.

libyul/SideEffects.h

@@ -73,6 +73,16 @@ struct SideEffects
 		*this = *this + _other;
 		return *this;
 	}
+
+	bool operator==(SideEffects const& _other) const
+	{
+		return
+			movable == _other.movable &&
+			sideEffectFree == _other.sideEffectFree &&
+			sideEffectFreeIfNoMSize == _other.sideEffectFreeIfNoMSize &&
+			invalidatesStorage == _other.invalidatesStorage &&
+			invalidatesMemory == _other.invalidatesMemory;
+	}
 };
 
 }

libyul/optimiser/CallGraphGenerator.cpp

@@ -29,18 +29,24 @@ using namespace std;
 using namespace dev;
 using namespace yul;
 
+map<YulString, set<YulString>> CallGraphGenerator::callGraph(Block const& _ast)
+{
+	CallGraphGenerator gen;
+	gen(_ast);
+	return std::move(gen.m_callGraph);
+}
 
 void CallGraphGenerator::operator()(FunctionalInstruction const& _functionalInstruction)
 {
-	m_callGraph.insert(m_currentFunction, YulString{
-		dev::eth::instructionInfo(_functionalInstruction.instruction).name
-	});
+	string name = dev::eth::instructionInfo(_functionalInstruction.instruction).name;
+	std::transform(name.begin(), name.end(), name.begin(), [](unsigned char _c) { return tolower(_c); });
+	m_callGraph[m_currentFunction].insert(YulString{name});
 	ASTWalker::operator()(_functionalInstruction);
 }
 
 void CallGraphGenerator::operator()(FunctionCall const& _functionCall)
 {
-	m_callGraph.insert(m_currentFunction, _functionCall.functionName.name);
+	m_callGraph[m_currentFunction].insert(_functionCall.functionName.name);
 	ASTWalker::operator()(_functionCall);
 }
 
@@ -48,7 +54,14 @@ void CallGraphGenerator::operator()(FunctionDefinition const& _functionDefinitio
 {
 	YulString previousFunction = m_currentFunction;
 	m_currentFunction = _functionDefinition.name;
+	yulAssert(m_callGraph.count(m_currentFunction) == 0, "");
+	m_callGraph[m_currentFunction] = {};
 	ASTWalker::operator()(_functionDefinition);
 	m_currentFunction = previousFunction;
 }
 
+CallGraphGenerator::CallGraphGenerator()
+{
+	m_callGraph[YulString{}] = {};
+}
+

libyul/optimiser/CallGraphGenerator.h

@@ -40,8 +40,7 @@ namespace yul
 class CallGraphGenerator: public ASTWalker
 {
 public:
-	/// @returns the call graph of the visited AST.
-	InvertibleRelation<YulString> const& callGraph() const { return m_callGraph; }
+	static std::map<YulString, std::set<YulString>> callGraph(Block const& _ast);
 
 	using ASTWalker::operator();
 	void operator()(FunctionalInstruction const& _functionalInstruction) override;
@@ -49,7 +48,9 @@ public:
 	void operator()(FunctionDefinition const& _functionDefinition) override;
 
 private:
-	InvertibleRelation<YulString> m_callGraph;
+	CallGraphGenerator();
+
+	std::map<YulString, std::set<YulString>> m_callGraph;
 	/// The name of the function we are currently visiting during traversal.
 	YulString m_currentFunction;
 };

libyul/optimiser/Semantics.cpp

@@ -28,6 +28,7 @@
 #include <libevmasm/SemanticInformation.h>
 
 #include <libdevcore/CommonData.h>
+#include <libdevcore/Algorithms.h>
 
 using namespace std;
 using namespace dev;
@@ -93,6 +94,33 @@ void MSizeFinder::operator()(FunctionCall const& _functionCall)
 			m_msizeFound = true;
 }
 
+
+map<YulString, SideEffects> SideEffectsPropagator::sideEffects(
+	Dialect const& _dialect,
+	map<YulString, std::set<YulString>> const& _directCallGraph
+)
+{
+	map<YulString, SideEffects> ret;
+	for (auto const& call: _directCallGraph)
+	{
+		YulString funName = call.first;
+		SideEffects sideEffects;
+		BreadthFirstSearch<YulString>{call.second, {funName}}.run(
+			[&](YulString _function, auto&& _addChild) {
+				if (sideEffects == SideEffects::worst())
+					return;
+				if (BuiltinFunction const* f = _dialect.builtin(_function))
+					sideEffects += f->sideEffects;
+				else
+					for (YulString callee: _directCallGraph.at(_function))
+						_addChild(callee);
+			}
+		);
+		ret[funName] = sideEffects;
+	}
+	return ret;
+}
+
 MovableChecker::MovableChecker(Dialect const& _dialect, Expression const& _expression):
 	MovableChecker(_dialect)
 {

libyul/optimiser/Semantics.h

@@ -62,6 +62,21 @@ private:
 	SideEffects m_sideEffects;
 };
 
+/**
+ * This class can be used to determine the side-effects of user-defined functions.
+ *
+ * It is given a dialect and a mapping that represents the direct calls from user-defined
+ * functions to other user-defined functions and built-in functions.
+ */
+class SideEffectsPropagator
+{
+public:
+	static std::map<YulString, SideEffects> sideEffects(
+		Dialect const& _dialect,
+		std::map<YulString, std::set<YulString>> const& _directCallGraph
+	);
+};
+
 /**
  * Class that can be used to find out if certain code contains the MSize instruction.
  *

test/InteractiveTests.h

@@ -27,6 +27,7 @@
 #include <test/libyul/YulOptimizerTest.h>
 #include <test/libyul/YulInterpreterTest.h>
 #include <test/libyul/ObjectCompilerTest.h>
+#include <test/libyul/FunctionSideEffects.h>
 
 #include <boost/filesystem.hpp>
 
@@ -56,6 +57,7 @@ Testsuite const g_interactiveTestsuites[] = {
 	{"Yul Optimizer",       "libyul",      "yulOptimizerTests",   false, false, &yul::test::YulOptimizerTest::create},
 	{"Yul Interpreter",     "libyul",      "yulInterpreterTests", false, false, &yul::test::YulInterpreterTest::create},
 	{"Yul Object Compiler", "libyul",      "objectCompiler",      false, false, &yul::test::ObjectCompilerTest::create},
+	{"Function Side Effects","libyul",     "functionSideEffects", false, false, &yul::test::FunctionSideEffects::create},
 	{"Syntax",              "libsolidity", "syntaxTests",         false, false, &SyntaxTest::create},
 	{"Error Recovery",      "libsolidity", "errorRecoveryTests",  false, false, &SyntaxTest::createErrorRecovery},
 	{"Semantic",            "libsolidity", "semanticTests",       false, true,  &SemanticTest::create},

test/libsolidity/smtCheckerTests/invariants/state_machine_1.sol

@@ -0,0 +1,32 @@
+pragma experimental SMTChecker;
+
+contract C {
+	uint x;
+
+	function f() public {
+		if (x == 0)
+			x = 1;
+	}
+
+	function g() public {
+		if (x == 1)
+			x = 2;
+	}
+
+	function h() public {
+		if (x == 2)
+			x = 0;
+	}
+
+	// This function shows that (x < 9) is not inductive and
+	// a stronger invariant is needed to be found.
+	// (x < 3) is the one found in the end.
+	function j() public {
+		if (x == 7)
+			x = 100;
+	}
+
+	function i() public view {
+		assert(x < 9);
+	}
+}

test/libsolidity/smtCheckerTests/invariants/state_machine_1_fail.sol

@@ -0,0 +1,32 @@
+pragma experimental SMTChecker;
+
+contract C {
+	uint x;
+
+	function f() public {
+		if (x == 0)
+			x = 1;
+	}
+
+	function g() public {
+		if (x == 1)
+			x = 2;
+	}
+
+	function h() public {
+		if (x == 2)
+			x = 0;
+	}
+
+	function j() public {
+		if (x < 2)
+			x = 100;
+	}
+
+	// Fails due to j.
+	function i() public view {
+		assert(x < 2);
+	}
+}
+// ----
+// Warning: (311-324): Assertion violation happens here

test/libsolidity/smtCheckerTests/modifiers/modifier_code_after_placeholder.sol

@@ -15,6 +15,10 @@ contract C
 		assert(x > 0);
 		x = x + 1;
 	}
+
+	function g(uint _x) public {
+		x = _x;
+	}
 }
 // ----
 // Warning: (136-149): Assertion violation happens here

test/libsolidity/smtCheckerTests/modifiers/modifier_multi.sol

@@ -20,6 +20,10 @@ contract C
 	function f() m n public {
 		x = x + 1;
 	}
+
+	function g(uint _x) public {
+		x = _x;
+	}
 }
 // ----
 // Warning: (170-183): Assertion violation happens here

test/libsolidity/smtCheckerTests/modifiers/modifier_two_placeholders.sol

@@ -17,6 +17,10 @@ contract C
 	function f() m public {
 		x = x + 1;
 	}
+
+	function g(uint _x) public {
+		x = _x;
+	}
 }
 // ----
 // Warning: (156-170): Assertion violation happens here

test/libyul/FunctionSideEffects.cpp

@@ -0,0 +1,125 @@
+/*
+	This file is part of solidity.
+
+	solidity is free software: you can redistribute it and/or modify
+	it under the terms of the GNU General Public License as published by
+	the Free Software Foundation, either version 3 of the License, or
+	(at your option) any later version.
+
+	solidity is distributed in the hope that it will be useful,
+	but WITHOUT ANY WARRANTY; without even the implied warranty of
+	MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+	GNU General Public License for more details.
+
+	You should have received a copy of the GNU General Public License
+	along with solidity.  If not, see <http://www.gnu.org/licenses/>.
+*/
+
+#include <test/libyul/FunctionSideEffects.h>
+#include <test/Options.h>
+#include <test/libyul/Common.h>
+
+#include <libdevcore/AnsiColorized.h>
+
+#include <libyul/SideEffects.h>
+#include <libyul/optimiser/CallGraphGenerator.h>
+#include <libyul/optimiser/Semantics.h>
+#include <libyul/Object.h>
+#include <libyul/backends/evm/EVMDialect.h>
+
+#include <libdevcore/StringUtils.h>
+
+#include <boost/algorithm/string.hpp>
+
+
+using namespace dev;
+using namespace langutil;
+using namespace yul;
+using namespace yul::test;
+using namespace dev::solidity;
+using namespace dev::solidity::test;
+using namespace std;
+
+namespace
+{
+string toString(SideEffects const& _sideEffects)
+{
+	vector<string> ret;
+	if (_sideEffects.movable)
+		ret.push_back("movable");
+	if (_sideEffects.sideEffectFree)
+		ret.push_back("sideEffectFree");
+	if (_sideEffects.sideEffectFreeIfNoMSize)
+		ret.push_back("sideEffectFreeIfNoMSize");
+	if (_sideEffects.invalidatesStorage)
+		ret.push_back("invalidatesStorage");
+	if (_sideEffects.invalidatesMemory)
+		ret.push_back("invalidatesMemory");
+	return joinHumanReadable(ret);
+}
+}
+
+FunctionSideEffects::FunctionSideEffects(string const& _filename)
+{
+	ifstream file(_filename);
+	if (!file)
+		BOOST_THROW_EXCEPTION(runtime_error("Cannot open test input: \"" + _filename + "\"."));
+	file.exceptions(ios::badbit);
+
+	m_source = parseSourceAndSettings(file);
+	m_expectation = parseSimpleExpectations(file);}
+
+TestCase::TestResult FunctionSideEffects::run(ostream& _stream, string const& _linePrefix, bool _formatted)
+{
+	Object obj;
+	std::tie(obj.code, obj.analysisInfo) = yul::test::parse(m_source, false);
+	if (!obj.code)
+		BOOST_THROW_EXCEPTION(runtime_error("Parsing input failed."));
+
+	map<YulString, SideEffects> functionSideEffects = SideEffectsPropagator::sideEffects(
+		EVMDialect::strictAssemblyForEVM(langutil::EVMVersion()),
+		CallGraphGenerator::callGraph(*obj.code)
+	);
+
+	std::map<std::string, std::string> functionSideEffectsStr;
+	for (auto const& fun: functionSideEffects)
+		functionSideEffectsStr[fun.first.str()] = toString(fun.second);
+
+	m_obtainedResult.clear();
+	for (auto const& fun: functionSideEffectsStr)
+		m_obtainedResult += fun.first + ": " + fun.second + "\n";
+
+	if (m_expectation != m_obtainedResult)
+	{
+		string nextIndentLevel = _linePrefix + "  ";
+		AnsiColorized(_stream, _formatted, {formatting::BOLD, formatting::CYAN}) << _linePrefix << "Expected result:" << endl;
+		printIndented(_stream, m_expectation, nextIndentLevel);
+		AnsiColorized(_stream, _formatted, {formatting::BOLD, formatting::CYAN}) << _linePrefix << "Obtained result:" << endl;
+		printIndented(_stream, m_obtainedResult, nextIndentLevel);
+		return TestResult::Failure;
+	}
+	return TestResult::Success;
+}
+
+
+void FunctionSideEffects::printSource(ostream& _stream, string const& _linePrefix, bool const) const
+{
+	printIndented(_stream, m_source, _linePrefix);
+}
+
+void FunctionSideEffects::printUpdatedExpectations(ostream& _stream, string const& _linePrefix) const
+{
+	printIndented(_stream, m_obtainedResult, _linePrefix);
+}
+
+void FunctionSideEffects::printIndented(ostream& _stream, string const& _output, string const& _linePrefix) const
+{
+	stringstream output(_output);
+	string line;
+	while (getline(output, line))
+		if (line.empty())
+			// Avoid trailing spaces.
+			_stream << boost::trim_right_copy(_linePrefix) << endl;
+		else
+			_stream << _linePrefix << line << endl;
+}

test/libyul/FunctionSideEffects.h

@@ -0,0 +1,54 @@
+/*
+	This file is part of solidity.
+
+	solidity is free software: you can redistribute it and/or modify
+	it under the terms of the GNU General Public License as published by
+	the Free Software Foundation, either version 3 of the License, or
+	(at your option) any later version.
+
+	solidity is distributed in the hope that it will be useful,
+	but WITHOUT ANY WARRANTY; without even the implied warranty of
+	MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+	GNU General Public License for more details.
+
+	You should have received a copy of the GNU General Public License
+	along with solidity.  If not, see <http://www.gnu.org/licenses/>.
+*/
+
+#pragma once
+
+#include <libdevcore/AnsiColorized.h>
+#include <test/TestCase.h>
+
+#include <iosfwd>
+#include <string>
+#include <vector>
+#include <utility>
+
+namespace yul
+{
+namespace test
+{
+
+class FunctionSideEffects: public dev::solidity::test::TestCase
+{
+public:
+	static std::unique_ptr<TestCase> create(Config const& _config)
+	{ return std::unique_ptr<TestCase>(new FunctionSideEffects(_config.filename)); }
+	explicit FunctionSideEffects(std::string const& _filename);
+
+	TestResult run(std::ostream& _stream, std::string const& _linePrefix = "", bool const _formatted = false) override;
+
+	void printSource(std::ostream& _stream, std::string const& _linePrefix = "", bool const _formatted = false) const override;
+	void printUpdatedExpectations(std::ostream& _stream, std::string const& _linePrefix) const override;
+
+private:
+	void printIndented(std::ostream& _stream, std::string const& _output, std::string const& _linePrefix = "") const;
+
+	std::string m_source;
+	std::string m_expectation;
+	std::string m_obtainedResult;
+};
+
+}
+}

test/libyul/functionSideEffects/cyclic_graph.yul

@@ -0,0 +1,10 @@
+{
+    function a() { b() }
+    function b() { c() }
+    function c() { b() }
+}
+// ----
+// : movable, sideEffectFree, sideEffectFreeIfNoMSize
+// a: movable, sideEffectFree, sideEffectFreeIfNoMSize
+// b: movable, sideEffectFree, sideEffectFreeIfNoMSize
+// c: movable, sideEffectFree, sideEffectFreeIfNoMSize

test/libyul/functionSideEffects/doubly_recursive_function.yul

@@ -0,0 +1,8 @@
+{
+    function a() { b() }
+    function b() { a() }
+}
+// ----
+// : movable, sideEffectFree, sideEffectFreeIfNoMSize
+// a: movable, sideEffectFree, sideEffectFreeIfNoMSize
+// b: movable, sideEffectFree, sideEffectFreeIfNoMSize

test/libyul/functionSideEffects/empty.yul

@@ -0,0 +1,4 @@
+{
+}
+// ----
+// : movable, sideEffectFree, sideEffectFreeIfNoMSize

test/libyul/functionSideEffects/empty_with_sstore.yul

@@ -0,0 +1,5 @@
+{
+    sstore(0, 1)
+}
+// ----
+// : invalidatesStorage

test/libyul/functionSideEffects/multi_calls.yul

@@ -0,0 +1,22 @@
+{
+    function a() {
+        b()
+    }
+    function b() {
+        sstore(0, 1)
+        b()
+    }
+    function c() {
+        mstore(0, 1)
+        a()
+        d()
+    }
+    function d() {
+    }
+}
+// ----
+// : movable, sideEffectFree, sideEffectFreeIfNoMSize
+// a: invalidatesStorage
+// b: invalidatesStorage
+// c: invalidatesStorage, invalidatesMemory
+// d: movable, sideEffectFree, sideEffectFreeIfNoMSize

test/libyul/functionSideEffects/recursive_function.yul

@@ -0,0 +1,6 @@
+{
+    function a() { a() }
+}
+// ----
+// : movable, sideEffectFree, sideEffectFreeIfNoMSize
+// a: movable, sideEffectFree, sideEffectFreeIfNoMSize

test/libyul/functionSideEffects/simple_functions.yul

@@ -0,0 +1,14 @@
+{
+    function a() {}
+    function f() { mstore(0, 1) }
+    function g() { sstore(0, 1) }
+    function h() { let x := msize() }
+    function i() { let z := mload(0) }
+}
+// ----
+// : movable, sideEffectFree, sideEffectFreeIfNoMSize
+// a: movable, sideEffectFree, sideEffectFreeIfNoMSize
+// f: invalidatesMemory
+// g: invalidatesStorage
+// h: sideEffectFree, sideEffectFreeIfNoMSize
+// i: sideEffectFreeIfNoMSize

test/libyul/functionSideEffects/structures.yul

@@ -0,0 +1,40 @@
+{
+    if calldataload(0)
+    {
+        f()
+    }
+    g()
+
+    function f() {
+        pop(mload(0))
+    }
+    function g() {
+        if sload(0)
+        {
+            h()
+        }
+    }
+    function h() {
+        switch t()
+        case 1 {
+            i()
+        }
+    }
+    function t() -> x {
+        mstore(0, 1)
+    }
+    function i() {
+        sstore(0, 1)
+    }
+    function r(a) -> b {
+        b := mul(a, 2)
+    }
+}
+// ----
+// : invalidatesStorage, invalidatesMemory
+// f: sideEffectFreeIfNoMSize
+// g: invalidatesStorage, invalidatesMemory
+// h: invalidatesStorage, invalidatesMemory
+// i: invalidatesStorage
+// r: movable, sideEffectFree, sideEffectFreeIfNoMSize
+// t: invalidatesMemory

test/tools/CMakeLists.txt

@@ -30,6 +30,8 @@ add_executable(isoltest
 	../libsolidity/ABIJsonTest.cpp
 	../libsolidity/ASTJSONTest.cpp
 	../libsolidity/SMTCheckerJSONTest.cpp
+	../libyul/Common.cpp
+	../libyul/FunctionSideEffects.cpp
 	../libyul/ObjectCompilerTest.cpp
 	../libyul/YulOptimizerTest.cpp
 	../libyul/YulInterpreterTest.cpp