klee: upgrade to LLVM 19

.github/workflows/build.yaml

@@ -6,8 +6,6 @@ jobs:
     strategy:
       matrix:
         include:
-          - os: ubuntu-22.04
-            clang_version: 15
           - os: ubuntu-24.04
             clang_version: 19
     steps:
@@ -34,10 +32,10 @@ jobs:
             libcurl4-openssl-dev \
             libedit-dev \
             libpfm4-dev \
-            llvm-14-dev \
-            clang-format-14 \
+            llvm-19-dev \
+            clang-format-19 \
             libmlir-14-dev \
-            clang-14
+            clang-19
 
       - name: Install OS-specific clang version
         run: |

.github/workflows/docker.yaml

@@ -19,6 +19,6 @@ jobs:
 
           mkdir -p $HOME/s2e/env/build
           cd $HOME/s2e/env/build
-          docker run -t --rm -e SYSTEM_CLANG_VERSION=15 -e S2E_PREFIX="$HOME/s2e/env/install" -w $(pwd) -v $HOME:$HOME s2e-build-env /run_as.sh $(id -u) $(id -g) make  -f $GITHUB_WORKSPACE/Makefile.tools install
+          docker run -t --rm -e S2E_PREFIX="$HOME/s2e/env/install" -w $(pwd) -v $HOME:$HOME s2e-build-env /run_as.sh $(id -u) $(id -g) make  -f $GITHUB_WORKSPACE/Makefile.tools install
 
       - run: echo "🍏 This job's status is ${{ job.status }}."

CLAUDE.md

@@ -29,13 +29,16 @@ S2E is a symbolic execution platform. This repository builds `libs2e.so`, a shar
 - Use C++20 in all components.
 - **Header guards**: `#ifndef S2E_*_H` / `#define` / `#endif`
 - Use `///` for license headers
+- Use braces for all if/for/while, etc. blocks, even when there is only a single instructions.
+- **Member variables**:
+   - `m_` prefix + `snake_case` (e.g., `m_devices`)
+   - Class member variables should go at the beginning of the class.
+- **Namespaces**: lowercase (e.g., `s2e::kvm`)
+- **Class names**: `PascalCase` (e.g., `VirtualDeviceManager`)
 
 ## Code Style for `libs2e/*`
-
-- **Class names**: `PascalCase` (e.g., `VirtualDeviceManager`)
 - **Method/function names**: `snake_case` (e.g., `mmio_read`, `find_device`)
-- **Member variables**: `m_` prefix + `snake_case` (e.g., `m_devices`)
-- **Namespaces**: lowercase (e.g., `s2e::kvm`)
+
 
 ## Commit Messages
 

Dockerfile

@@ -20,7 +20,7 @@
 
 # Installs S2E and its associated libraries and tools to /opt/s2e
 
-FROM ubuntu:22.04 AS s2e-build-env
+FROM ubuntu:24.04 AS s2e-build-env
 
 # Install build dependencies.
 # The unzip and libgomp1 dependencies are needed to unzip and run binary Z3
@@ -41,33 +41,27 @@ RUN apt-get update && dpkg --add-architecture i386 && apt-get update &&
     libcurl4-openssl-dev \
     libedit-dev \
     libpfm4-dev \
-    llvm-14-dev \
-    clang-format-14 \
-    clang-14 \
-    clang-15
+    llvm-19-dev \
+    clang-format-19 \
+    clang-19 \
+    clang-17
 
 # This scripts allows running commands as a host user inside the container.
 # For example, guest tools can be built as follows:
 # cd $HOME/s2e/env/source/s2e
 # docker build --target s2e-build-env -t s2e-build-env .
 # cd $HOME/s2e/env/build
-# docker run -ti --rm -e SYSTEM_CLANG_VERSION=15 -e S2E_PREFIX="$HOME/s2e/env/install" -w $(pwd) -v $HOME:$HOME s2e-build-env /run_as.sh $(id -u) $(id -g) make  -f $HOME/s2e/env/source/s2e/Makefile.tools install
+# docker run -ti --rm -e SYSTEM_CLANG_VERSION=19 -e S2E_PREFIX="$HOME/s2e/env/install" -w $(pwd) -v $HOME:$HOME s2e-build-env /run_as.sh $(id -u) $(id -g) make  -f $HOME/s2e/env/source/s2e/Makefile.tools install
 COPY scripts/run_as.sh /
 
 ###############################################################################
 FROM s2e-build-env AS s2e-build-all
 
-# Required for C++17
-RUN DEBIAN_FRONTEND=noninteractive apt-get install -y software-properties-common
-RUN add-apt-repository ppa:ubuntu-toolchain-r/test && apt update
-RUN DEBIAN_FRONTEND=noninteractive apt-get install -y gcc-9 g++-9
-
 RUN mkdir s2e && mkdir s2e-build
 COPY Makefile Makefile.tools Makefile.common s2e/
 
 # Be explicit about not building Z3 from source, even though its default
 ARG USE_Z3_BINARY=yes
-ARG SYSTEM_CLANG_VERSION=15
 
 RUN cd s2e-build &&                                                         \
     make -f ../s2e/Makefile S2E_PREFIX=/opt/s2e stamps/z3

Dockerfile.tools

@@ -0,0 +1,52 @@
+# Copyright (C) 2017-2022, Cyberhaven
+#
+# Permission is hereby granted, free of charge, to any person obtaining a copy
+# of this software and associated documentation files (the "Software"), to deal
+# in the Software without restriction, including without limitation the rights
+# to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+# copies of the Software, and to permit persons to whom the Software is
+# furnished to do so, subject to the following conditions:
+#
+# The above copyright notice and this permission notice shall be included in all
+# copies or substantial portions of the Software.
+#
+# THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+# IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+# FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+# AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+# LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+# OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
+# SOFTWARE.
+
+# This creates the build environment for guest tools.
+
+FROM ubuntu:22.04 AS s2e-build-env-tools
+
+# Install build dependencies.
+# The unzip and libgomp1 dependencies are needed to unzip and run binary Z3
+# distributions.
+
+RUN apt-get update && dpkg --add-architecture i386 && apt-get update &&                       \
+    apt-get -y install sudo git ca-certificates build-essential cmake curl wget texinfo flex bison  \
+    python-is-python3 python3-dev python3-venv python3-distro mingw-w64 lsb-release \
+    autoconf libtool libprotobuf-dev protobuf-compiler protobuf-c-compiler \
+    libdwarf-dev libelf-dev libelf-dev:i386 \
+    libboost-dev zlib1g-dev libjemalloc-dev nasm pkg-config                 \
+    libmemcached-dev libpq-dev libc6-dev-i386 binutils-dev                  \
+    libboost-system-dev libboost-serialization-dev libboost-regex-dev       \
+    libbsd-dev libpixman-1-dev                                              \
+    libglib2.0-dev libglib2.0-dev:i386 python3-docutils libpng-dev          \
+    gcc-multilib g++-multilib libgomp1 unzip libzstd-dev \
+    libgmock-dev libgtest-dev libsoci-dev libcapstone-dev \
+    libcurl4-openssl-dev \
+    libedit-dev \
+    libpfm4-dev \
+    clang-15
+
+# This scripts allows running commands as a host user inside the container.
+# For example, guest tools can be built as follows:
+# cd $HOME/s2e/env/source/s2e
+# docker build --target s2e-build-env -t s2e-build-env .
+# cd $HOME/s2e/env/build
+# docker run -ti --rm -e SYSTEM_CLANG_VERSION=19 -e S2E_PREFIX="$HOME/s2e/env/install" -w $(pwd) -v $HOME:$HOME s2e-build-env /run_as.sh $(id -u) $(id -g) make  -f $HOME/s2e/env/source/s2e/Makefile.tools install
+COPY scripts/run_as.sh /

Makefile

@@ -32,8 +32,8 @@
 #  USE_Z3_BINARY=yes
 #      Whether to use the Z3 binary or to build Z3 from source
 #
-#  SYSTEM_LLVM_CONFIG=llvm-config-14
-#      Override the default llvm-config command (defaults to llvm-config-14)
+#  SYSTEM_LLVM_CONFIG=llvm-config-19
+#      Override the default llvm-config command (defaults to llvm-config-19)
 #
 #  SYSTEM_CLANG_VERSION=19
 #      Override the default clang version (defaults to clang-19)
@@ -62,17 +62,17 @@ S2E_BUILD:=$(CURDIR)
 USE_Z3_BINARY?=yes
 
 # System LLVM variables
-SYSTEM_LLVM_CONFIG?=llvm-config-14
+SYSTEM_LLVM_CONFIG?=llvm-config-19
 LLVM_VERSION := $(shell $(SYSTEM_LLVM_CONFIG) --version)
 LLVM_PREFIX := $(shell $(SYSTEM_LLVM_CONFIG) --prefix)
 LLVM_INCLUDEDIR := $(shell $(SYSTEM_LLVM_CONFIG) --includedir)
 LLVM_LIBDIR := $(shell $(SYSTEM_LLVM_CONFIG) --libdir)
 LLVM_CMAKE_DIR := $(LLVM_LIBDIR)/cmake/llvm
 
-# Verify LLVM version is 14.x
+# Verify LLVM version is 19.x
 LLVM_MAJOR_VERSION := $(shell echo $(LLVM_VERSION) | cut -d. -f1)
-ifneq ($(LLVM_MAJOR_VERSION),14)
-$(error LLVM version $(LLVM_VERSION) found, but version 14.x is required)
+ifneq ($(LLVM_MAJOR_VERSION),19)
+$(error LLVM version $(LLVM_VERSION) found, but version 19.x is required)
 endif
 
 KLEE_DIRS=$(foreach suffix,-debug -release -coverage,$(addsuffix $(suffix),klee))
@@ -236,9 +236,10 @@ stamps/libdwarf-make: stamps/libdwarf-configure
 
 RAPIDJSON_CONFIGURE_FLAGS = -DCMAKE_INSTALL_PREFIX=$(S2E_PREFIX)                                 \
                             -DCMAKE_C_FLAGS="$(CFLAGS_ARCH) -fno-omit-frame-pointer -fPIC"       \
-                            -DCMAKE_C_COMPILER=$(SYSTEM_CLANG_CC)                                       \
-                            -DCMAKE_CXX_COMPILER=$(SYSTEM_CLANG_CXX)                                    \
-                            -DRAPIDJSON_BUILD_TESTS=OFF
+                            -DCMAKE_C_COMPILER=$(SYSTEM_CLANG_CC)                                \
+                            -DCMAKE_CXX_COMPILER=$(SYSTEM_CLANG_CXX)                             \
+                            -DRAPIDJSON_BUILD_TESTS=OFF \
+                            -DCMAKE_POLICY_VERSION_MINIMUM=3.5
 
 
 stamps/rapidjson-configure: $(RAPIDJSON_BUILD_DIR)

docs/src/s2e-env.rst

@@ -13,7 +13,7 @@ You will find in the documentation various tutorials that go deeper into various
 
 .. note::
 
-    S2E builds and runs on Ubuntu 22.04, 24.04 and Debian 12/13 (64-bit).
+    S2E builds and runs on Ubuntu 24.04, 26.04 and Debian 12/13 (64-bit).
     Earlier versions may still work, but we do not support them anymore.
 
 

klee/CMakeLists.txt

@@ -31,25 +31,16 @@ set(KLEE_LIBRARY_DIR "${CMAKE_CURRENT_BINARY_DIR}/lib")
 configure_file(KLEEConfig.cmake.in ${CMAKE_CONFIG_FILE} @ONLY)
 
 
-if (POLICY CMP0054)
-  # FIXME: This is horrible. With the old behaviour,
-  # quoted strings like "MSVC" in if() conditionals
-  # get implicitly dereferenced. The NEW behaviour
-  # doesn't do this but CMP0054 was only introduced
-  # in CMake 3.1 and we support lower versions as the
-  # minimum. We could set NEW here but it would be very
-  # confusing to use NEW for some builds and OLD for others
-  # which could lead to some subtle bugs. Instead when the
-  # minimum version is 3.1 change this policy to NEW and remove
-  # the hacks in place to work around it.
-  cmake_policy(SET CMP0054 OLD)
-endif()
-
 if (POLICY CMP0042)
   # Enable `MACOSX_RPATH` by default.
   cmake_policy(SET CMP0042 NEW)
 endif()
 
+if (POLICY CMP0075)
+  # Honor CMAKE_REQUIRED_LIBRARIES in check_include_file() (required by LLVM 19's FindLibEdit).
+  cmake_policy(SET CMP0075 NEW)
+endif()
+
 # This overrides the default flags for the different CMAKE_BUILD_TYPEs
 set(CMAKE_USER_MAKE_RULES_OVERRIDE_C
   "${CMAKE_CURRENT_SOURCE_DIR}/cmake/c_flags_override.cmake")
@@ -168,8 +159,8 @@ set(KLEE_COMPONENT_EXTRA_LIBRARIES "")
 ################################################################################
 # Find LLVM
 ################################################################################
+find_package(LLVM 19.1...<20 REQUIRED)
 include(${CMAKE_SOURCE_DIR}/cmake/find_llvm.cmake)
-find_package(LLVM 14...<15 REQUIRED)
 
 
 foreach (vname ${NEEDED_LLVM_VARS})

klee/cmake/find_llvm.cmake

@@ -7,8 +7,6 @@
 #
 #===------------------------------------------------------------------------===#
 
-find_package(LLVM 14...<15 CONFIG REQUIRED)
-
 # Provide function to map LLVM components to libraries.
 function(klee_get_llvm_libs output_var)
     llvm_map_components_to_libnames(${output_var} ${ARGN})

klee/include/klee/Expr.h

@@ -508,7 +508,7 @@ class ConstantExpr : public Expr {
 
     /// isAllOnes - Is this constant all ones.
     bool isAllOnes() const {
-        return getAPValue().isAllOnesValue();
+        return getAPValue().isAllOnes();
     }
 
     /* Constant Operations */

klee/include/klee/Internal/Module/KInstruction.h

@@ -44,13 +44,21 @@ struct KInstruction {
 
 struct KGEPInstruction : KInstruction {
     /// indices - The list of variable sized adjustments to add to the pointer
-    /// operand to execute the instruction. The first element is the operand
-    /// index into the GetElementPtr instruction, and the second element is the
-    /// element size to multiple that index by.
+    /// operand to execute the getelementptr instruction. The first element is
+    /// the operand index and the second is the element size to multiply by.
     std::vector<std::pair<unsigned, uint64_t>> indices;
 
-    /// offset - A constant offset to add to the pointer operand to execute the
-    /// insturction.
+    /// offset - A constant byte offset to add to the pointer operand.
+    uint64_t offset;
+};
+
+struct KInsertValueInstruction : KInstruction {
+    /// offset - Constant byte offset of the insertion point within the aggregate.
+    uint64_t offset;
+};
+
+struct KExtractValueInstruction : KInstruction {
+    /// offset - Constant byte offset of the extracted element within the aggregate.
     uint64_t offset;
 };
 

klee/include/klee/Internal/Module/KModule.h

@@ -38,6 +38,8 @@ class Executor;
 class Expr;
 struct KInstruction;
 struct KGEPInstruction;
+struct KInsertValueInstruction;
+struct KExtractValueInstruction;
 class KModule;
 template <class T> class ref;
 
@@ -119,12 +121,9 @@ class KModule {
     KModule() {
     }
 
-    template <typename SqType, typename TypeIt>
-    void computeOffsetsSeqTy(const GlobalAddresses &globalAddresses, KGEPInstruction *kgepi,
-                             ref<ConstantExpr> &constantOffset, uint64_t index, const TypeIt it);
-
-    template <typename TypeIt>
-    void computeOffsets(const GlobalAddresses &globalAddresses, KGEPInstruction *kgepi, TypeIt ib, TypeIt ie);
+    void bindGEPInstructionConstants(KGEPInstruction *kgepi);
+    void bindInsertValueConstants(KInsertValueInstruction *kivi);
+    void bindExtractValueConstants(KExtractValueInstruction *kevi);
 
     /// bindInstructionConstants - Initialize any necessary per instruction
     /// constant values.