feat: --yul-backend option to compile Yul with libyulc

CMakeLists.txt

@@ -36,6 +36,7 @@ endif()
 
 option(SOLC_LINK_STATIC "Link solc executable statically on supported platforms" OFF)
 option(SOLC_STATIC_STDLIBS "Link solc against static versions of libgcc and libstdc++ on supported platforms" OFF)
+option(SOLC_STRIP_SYMBOLS "Discard the symbol table from the solc executable at link time on supported platforms" OFF)
 option(STRICT_Z3_VERSION "Require the exact version of Z3 solver expected by our test suite." ON)
 option(PEDANTIC "Enable extra warnings and pedantic build flags. Treat all warnings as errors." ON)
 option(PROFILE_OPTIMIZER_STEPS "Output performance metrics for the optimiser steps." OFF)
@@ -50,6 +51,11 @@ option(
 	"Only build library targets that can be statically linked against. Do not build executables or tests."
 	OFF
 )
+option(
+	USE_YULC
+	"Link solc against libyulc, the powdr-labs verified Yul -> EVM compiler, and enable --yul-backend=yulc."
+	OFF
+)
 mark_as_advanced(PROFILE_OPTIMIZER_STEPS)
 mark_as_advanced(IGNORE_VENDORED_DEPENDENCIES)
 mark_as_advanced(ONLY_BUILD_SOLIDITY_LIBRARIES)
@@ -72,6 +78,10 @@ endif()
 
 find_package(Threads)
 
+if (USE_YULC)
+  include(yulc)
+endif()
+
 if(NOT PEDANTIC)
   message(WARNING "-- Pedantic build flags turned off. Warnings will not make compilation fail. This is NOT recommended in development builds.")
 endif()

cmake/EthOptions.cmake

@@ -52,6 +52,7 @@ if (SUPPORT_TOOLS)
 endif()
 	message("------------------------------------------------------------------ flags")
 	message("-- OSSFUZZ                                                   ${OSSFUZZ}")
+	message("-- USE_YULC         libyulc Yul backend                      ${USE_YULC}")
 	message("-- PROPERTY_BASED_TESTS (FuzzTest)                           ${PROPERTY_BASED_TESTS}")
 	message("-- PROPERTY_BASED_TESTS_MODE                                 ${PROPERTY_BASED_TESTS_MODE}")
 	message("------------------------------------------------------------------------")

cmake/yulc.cmake

@@ -0,0 +1,74 @@
+# Makes the powdr-labs verified Yul -> EVM compiler (libyulc) available as the
+# imported target Yulc::yulc.
+#
+# libyulc is a prebuilt binary release of https://github.com/powdr-labs/yul-compiler:
+# a Lean-compiled compiler behind a small C interface (yulc.h). It is not built
+# from source here -- that would require the Lean toolchain and a Mathlib build.
+# By default the pinned release below is downloaded and cached in the build
+# directory; point YULC_ROOT at an extracted release (or at yul-compiler's own
+# .lake/build/c) to use a local build instead.
+#
+# The static archive is used deliberately. It is a merged archive containing the
+# whole closure, Lean runtime included, so solc stays a single self-contained
+# binary with no runtime library search path to get right. This only works when
+# linking an executable: the Lean runtime is compiled with local-exec TLS, which
+# no linker accepts inside a shared object. The release also ships libyulc.so
+# for that case, but solc does not need it.
+
+set(YULC_VERSION "0.0.1" CACHE STRING "Version of the libyulc release to download")
+set(YULC_RELEASE_SHA256
+	"1b8bf1c09cb6b3feaef4efe3d10c3c3348d0a96dc3cf17ba818aabe357d0f32f"
+	CACHE STRING "SHA-256 of the libyulc release tarball"
+)
+set(YULC_ROOT "" CACHE PATH
+	"Directory containing a prebuilt libyulc (yulc.h and libyulc.a). \
+Downloads the pinned release when empty."
+)
+
+if (NOT UNIX OR APPLE)
+	message(FATAL_ERROR "USE_YULC is only supported on Linux; libyulc is released for x86_64 Linux only.")
+endif()
+
+if (SOLC_LINK_STATIC)
+	# libyulc.a already brings its own libc++ and glibc-dependent Lean runtime.
+	# Folding that into a fully static binary is untested; refuse rather than
+	# produce something subtly broken.
+	message(FATAL_ERROR "USE_YULC is not supported together with SOLC_LINK_STATIC.")
+endif()
+
+if (YULC_ROOT)
+	set(_yulc_dir "${YULC_ROOT}")
+	message(STATUS "Using libyulc from ${_yulc_dir}")
+else()
+	# The release workflow derives the tarball name from the tag by stripping only
+	# the "libyulc-" prefix, so the "v" stays in it.
+	set(_yulc_name "libyulc-v${YULC_VERSION}-x86_64-linux")
+	include(FetchContent)
+	FetchContent_Declare(
+		yulc
+		URL "https://github.com/powdr-labs/yul-compiler/releases/download/libyulc-v${YULC_VERSION}/${_yulc_name}.tar.gz"
+		URL_HASH "SHA256=${YULC_RELEASE_SHA256}"
+		DOWNLOAD_EXTRACT_TIMESTAMP TRUE
+	)
+	# The tarball has no CMakeLists.txt, so this only downloads and extracts it.
+	FetchContent_MakeAvailable(yulc)
+	set(_yulc_dir "${yulc_SOURCE_DIR}")
+endif()
+
+find_library(YULC_LIBRARY NAMES libyulc.a PATHS "${_yulc_dir}" NO_DEFAULT_PATH REQUIRED
+	DOC "Path to the merged libyulc static archive"
+)
+find_file(YULC_HEADER NAMES yulc.h PATHS "${_yulc_dir}" NO_DEFAULT_PATH REQUIRED
+	DOC "Path to the libyulc public header"
+)
+get_filename_component(_yulc_includedir "${YULC_HEADER}" DIRECTORY)
+
+add_library(Yulc::yulc STATIC IMPORTED GLOBAL)
+set_target_properties(Yulc::yulc PROPERTIES
+	IMPORTED_LOCATION "${YULC_LIBRARY}"
+	INTERFACE_INCLUDE_DIRECTORIES "${_yulc_includedir}"
+	# What `leanc --print-ldflags` requires of the runtime baked into the archive.
+	INTERFACE_LINK_LIBRARIES "Threads::Threads;${CMAKE_DL_LIBS};rt;m"
+)
+
+message(STATUS "Found libyulc: ${YULC_LIBRARY}")

docs/installing-solidity.rst

@@ -536,6 +536,71 @@ but their presence is checked only at runtime, they are not needed for the build
 
     The emscripten builds require Z3 and will statically link against it instead.
 
+.. _yulc-build:
+
+The libyulc Yul Backend
+-----------------------
+
+``-DUSE_YULC=ON`` links ``solc`` against
+`libyulc <https://github.com/powdr-labs/yul-compiler>`_ and enables
+:ref:`--yul-backend=yulc <yul-backend>`. It is off by default.
+
+libyulc is a Lean-compiled compiler and is not built from source here; a prebuilt
+release is downloaded and cached in the build directory. The merged static archive
+is linked in, so ``solc`` remains a single self-contained binary -- a considerably
+larger one, since the archive carries the Lean runtime.
+
+.. code-block:: sh
+
+    cmake .. -DUSE_YULC=ON
+
+To build against a local checkout of yul-compiler instead of the pinned release,
+point ``YULC_ROOT`` at a directory holding ``yulc.h`` and ``libyulc.a`` (which is
+what ``scripts/build-c-lib.sh`` writes to ``.lake/build/c``):
+
+.. code-block:: sh
+
+    cmake .. -DUSE_YULC=ON -DYULC_ROOT=/path/to/yul-compiler/.lake/build/c
+
+Only x86-64 Linux is supported, and the option cannot be combined with
+``-DSOLC_LINK_STATIC=ON``.
+
+Most of the size the archive adds is code, but a large part of it is just the
+symbol table; see :ref:`stripping-symbols` if that matters to you.
+
+.. _stripping-symbols:
+
+Stripping Symbols
+-----------------
+
+``-DSOLC_STRIP_SYMBOLS=ON`` passes ``-s`` to the linker when ``solc`` is linked,
+which leaves the symbol table (``.symtab``/``.strtab``) out of the executable. It
+is off by default and currently only takes effect on Linux.
+
+This is worth its own option mostly because of :ref:`libyulc <yulc-build>`, whose
+Lean-mangled symbol names are far bigger than the code they name. With
+``-DUSE_YULC=ON -DCMAKE_BUILD_TYPE=Release``, the symbol table is a third of the
+binary:
+
+.. code-block:: text
+
+    -DSOLC_STRIP_SYMBOLS=OFF   339 MiB
+    -DSOLC_STRIP_SYMBOLS=ON    226 MiB
+
+Without libyulc there is much less to gain: the same build goes from 20 MiB to
+17 MiB.
+
+Note that ``-s`` discards debug info together with the symbol table, so turning it
+on in a ``RelWithDebInfo`` build -- which is what a build from a git checkout
+defaults to -- leaves you with a binary you cannot debug. That is why it is opt-in
+rather than tied to the build type.
+
+Solidity itself never symbolizes anything at runtime: it installs no crash handler
+and does not use ``boost::stacktrace``, so its own error output is unaffected. What
+you lose is the ability of external tools -- ``gdb``, ``perf``, ``addr2line`` -- to
+name anything but the handful of exported dynamic symbols. Keep an unstripped copy
+around if you expect to need that.
+
 The Version String in Detail
 ============================
 

docs/yul.rst

@@ -128,6 +128,42 @@ to code as data to deploy contracts. This Yul mode is available for the commandl
     Yul is in active development and bytecode generation is only fully implemented for the EVM dialect of Yul
     with EVM 1.0 as target.
 
+.. _yul-backend:
+
+Choosing the Code Generator
+---------------------------
+
+In stand-alone mode, ``--yul-backend`` selects which code generator turns Yul into
+EVM bytecode:
+
+``solc`` (the default)
+    The code generator built into this compiler, described in the rest of this
+    document.
+
+``yulc``
+    `libyulc <https://github.com/powdr-labs/yul-compiler>`_, a Yul to EVM compiler
+    written and proved correct in Lean.
+
+.. code-block:: sh
+
+    solc --strict-assembly --yul-backend yulc input.yul
+
+``--yul-backend=yulc`` requires a compiler built with ``-DUSE_YULC=ON``; see
+:ref:`building the compiler <yulc-build>`. It accepts the same input as the default
+backend -- a Yul block or a Yul object, with child objects and data segments
+resolved during compilation -- but it produces only the ``--bin`` output. There is
+no assembly text, no assembly JSON, no AST and no source mapping to report, and
+because the compiler only emits code it has proved correct, it rejects
+``--optimize`` and the other optimizer options rather than silently ignoring them.
+It also cannot resolve ``--libraries`` placeholders.
+
+Passing a program that the verified compiler does not cover is an error rather than
+a fallback to the default backend:
+
+.. code-block:: none
+
+    Error: input.yul: parsed, but uses unsupported compiler features (libyulc)
+
 
 Informal Description of Yul
 ===========================

solc/CMakeLists.txt

@@ -7,6 +7,14 @@ set(libsolcli_sources
 add_library(solcli ${libsolcli_sources})
 target_link_libraries(solcli PUBLIC solidity Boost::boost Boost::program_options)
 
+if (USE_YULC)
+	# PRIVATE: yulc.h is an implementation detail of CommandLineInterface.cpp and
+	# nothing outside solcli refers to it. The archive itself still propagates to
+	# the solc link, as it must -- it may only be linked into an executable.
+	target_link_libraries(solcli PRIVATE Yulc::yulc)
+	target_compile_definitions(solcli PRIVATE SOLC_HAVE_YULC)
+endif()
+
 set(sources main.cpp)
 
 add_executable(solc ${sources})
@@ -31,3 +39,14 @@ elseif(SOLC_STATIC_STDLIBS AND UNIX AND NOT APPLE)
 		LINK_FLAGS "-static-libgcc -static-libstdc++"
 	)
 endif()
+
+if(SOLC_STRIP_SYMBOLS AND UNIX AND NOT APPLE)
+	# Tell the linker to omit .symtab/.strtab. Note that this discards the debug
+	# info of a RelWithDebInfo build along with them, which is why it is opt-in
+	# even though the default build type is not Release.
+	#
+	# target_link_options() rather than the LINK_FLAGS property above, because
+	# this has to compose with whatever SOLC_LINK_STATIC or SOLC_STATIC_STDLIBS
+	# already put there.
+	target_link_options(solc PRIVATE "LINKER:-s")
+endif()

solc/CommandLineInterface.cpp

@@ -43,6 +43,10 @@
 
 #include <libyul/YulStack.h>
 
+#ifdef SOLC_HAVE_YULC
+#include <yulc.h>
+#endif
+
 #include <libevmasm/Ethdebug.h>
 #include <libevmasm/Disassemble.h>
 
@@ -859,7 +863,10 @@ void CommandLineInterface::processInput()
 		serveLSP();
 		break;
 	case InputMode::Assembler:
-		assembleYul(m_options.assembly.targetMachine);
+		if (m_options.assembly.yulBackend == YulBackend::Yulc)
+			assembleYulWithYulc();
+		else
+			assembleYul(m_options.assembly.targetMachine);
 		break;
 	case InputMode::Linker:
 		link();
@@ -1295,6 +1302,46 @@ std::string CommandLineInterface::objectWithLinkRefsHex(evmasm::LinkerObject con
 	return out;
 }
 
+void CommandLineInterface::assembleYulWithYulc()
+{
+	solAssert(m_options.input.mode == InputMode::Assembler);
+	solAssert(m_options.assembly.yulBackend == YulBackend::Yulc);
+
+#ifndef SOLC_HAVE_YULC
+	solThrow(
+		CommandLineExecutionError,
+		"This binary was built without libyulc support. Rebuild solc with -DUSE_YULC=ON to use "
+		"--yul-backend=yulc."
+	);
+#else
+	// libyulc accepts exactly what its own CLI accepts: one complete Yul program,
+	// block- or object-rooted, with child objects and data segments resolved
+	// during compilation. So each source unit is handed over verbatim and comes
+	// back as finished creation bytecode.
+	for (auto const& [sourceUnitName, yulSource]: m_fileReader.sourceUnits())
+	{
+		uint8_t* bytecode = nullptr;
+		size_t bytecodeLength = 0;
+		int const status = yulc_compile(yulSource.c_str(), &bytecode, &bytecodeLength);
+
+		if (status != YULC_OK)
+			solThrow(
+				CommandLineExecutionError,
+				sourceUnitName + ": " + yulc_status_string(status) + " (libyulc)"
+			);
+
+		// yulc_compile() hands over ownership of the buffer.
+		bytes bytecodeBytes(bytecode, bytecode + bytecodeLength);
+		yulc_free(bytecode);
+
+		sout() << std::endl << "======= " << sourceUnitName << " (EVM) =======" << std::endl;
+		solAssert(m_options.compiler.outputs.binary);
+		sout() << std::endl << "Binary representation:" << std::endl;
+		sout() << util::toHex(bytecodeBytes) << std::endl;
+	}
+#endif
+}
+
 void CommandLineInterface::assembleYul(yul::YulStack::Machine _targetMachine)
 {
 	solAssert(m_options.input.mode == InputMode::Assembler);

solc/CommandLineInterface.h

@@ -96,6 +96,9 @@ class CommandLineInterface
 	static std::string objectWithLinkRefsHex(evmasm::LinkerObject const& _obj);
 
 	void assembleYul(yul::YulStack::Machine _targetMachine);
+	/// Assembles the Yul input with libyulc instead of solc's own code generator.
+	/// Only produces the binary output; see --yul-backend.
+	void assembleYulWithYulc();
 
 	void outputCompilationResults();