diff --git a/.dockerignore b/.dockerignore index fe29c605..6d35f2e4 100644 --- a/.dockerignore +++ b/.dockerignore @@ -11,4 +11,8 @@ TAGS compile_commands.json # The Dockerfile itself doesn't need to be copied -Dockerfile \ No newline at end of file +Dockerfile + +# Do not include build directories +build/ +cmake-* diff --git a/.github/workflows/run_tests.yml b/.github/workflows/run_tests.yml index 0242f1d0..8e06e447 100644 --- a/.github/workflows/run_tests.yml +++ b/.github/workflows/run_tests.yml @@ -32,15 +32,18 @@ jobs: sudo apt-get update sudo apt-get install -y \ llvm-${{ matrix.llvm_version }}-dev \ - libz3-dev + libz3-dev \ + git + - name: Build SymCC with the QSYM backend run: | + git submodule update --init --recursive runtime mkdir build cd build cmake \ -DCMAKE_BUILD_TYPE=Release \ -DZ3_TRUST_SYSTEM_VERSION=ON \ - -DQSYM_BACKEND=ON \ + -DSYMCC_RT_BACKEND=qsym \ -DLLVM_DIR=/usr/lib/llvm-${{ matrix.llvm_version }}/cmake \ .. make @@ -67,15 +70,17 @@ jobs: sudo apt-get update sudo apt-get install -y \ llvm-${{ matrix.llvm_version }}-dev \ - libz3-dev + libz3-dev \ + git - name: Build SymCC with the QSYM backend run: | + git submodule update --init --recursive runtime mkdir build cd build cmake \ -DCMAKE_BUILD_TYPE=Release \ -DZ3_TRUST_SYSTEM_VERSION=ON \ - -DQSYM_BACKEND=ON \ + -DSYMCC_RT_BACKEND=qsym \ -DLLVM_DIR=/usr/lib/llvm-${{ matrix.llvm_version }}/cmake \ .. make diff --git a/.gitignore b/.gitignore index a5522f87..8c2e98ad 100644 --- a/.gitignore +++ b/.gitignore @@ -43,4 +43,4 @@ compile_commands.json .cache # Build directories -build* +*build* diff --git a/.gitmodules b/.gitmodules index 993f41b2..8480f74b 100644 --- a/.gitmodules +++ b/.gitmodules @@ -1,4 +1,4 @@ -[submodule "qsym_backend/qsym"] - path = runtime/qsym_backend/qsym - url = https://github.com/eurecom-s3/qsym.git - branch = symcc +[submodule "runtime"] + path = runtime + url = https://github.com/eurecom-s3/symcc-rt.git + branch = main diff --git a/CMakeLists.txt b/CMakeLists.txt index 3db2ba8e..edbd7d0d 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -12,12 +12,11 @@ # You should have received a copy of the GNU General Public License along with # SymCC. If not, see . -cmake_minimum_required(VERSION 3.5) -project(SymbolicCompiler) +cmake_minimum_required(VERSION 3.16) +project(SymCC) -list(APPEND CMAKE_MODULE_PATH "${CMAKE_SOURCE_DIR}/cmake") - -option(QSYM_BACKEND "Use the Qsym backend instead of our own" OFF) +set(LLVM_VERSION "" CACHE STRING "LLVM version to use. The corresponding LLVM dev package must be installed.") +set(SYMCC_RT_BACKEND "qsym" CACHE STRING "The symbolic backend to use. Please check symcc-rt to get a list of the available backends.") option(TARGET_32BIT "Make the compiler work correctly with -m32" OFF) # We need to build the runtime as an external project because CMake otherwise @@ -25,6 +24,17 @@ option(TARGET_32BIT "Make the compiler work correctly with -m32" OFF) # and one 64-bit variant). include(ExternalProject) +# Find LLVM +find_package(LLVM ${LLVM_VERSION} REQUIRED CONFIG) + +message(STATUS "Found LLVM ${LLVM_PACKAGE_VERSION}") +message(STATUS "Using LLVMConfig.cmake from ${LLVM_DIR}") + +if (${LLVM_VERSION_MAJOR} LESS 8 OR ${LLVM_VERSION_MAJOR} GREATER 17) + message(WARNING "The software has been developed for LLVM 8 through 17; \ +it is unlikely to work with other versions!") +endif() + set(SYM_RUNTIME_BUILD_ARGS -DCMAKE_AR=${CMAKE_AR} -DCMAKE_C_COMPILER=${CMAKE_C_COMPILER} @@ -42,11 +52,12 @@ set(SYM_RUNTIME_BUILD_ARGS -DCMAKE_SHARED_LINKER_FLAGS_INIT=${CMAKE_SHARED_LINKER_FLAGS_INIT} -DCMAKE_MODULE_PATH=${CMAKE_MODULE_PATH} -DCMAKE_SYSROOT=${CMAKE_SYSROOT} - -DQSYM_BACKEND=${QSYM_BACKEND} + -DSYMCC_RT_BACKEND=${SYMCC_RT_BACKEND} + -DLLVM_VERSION=${LLVM_PACKAGE_VERSION} -DCMAKE_BUILD_TYPE=${CMAKE_BUILD_TYPE} -DZ3_TRUST_SYSTEM_VERSION=${Z3_TRUST_SYSTEM_VERSION}) -ExternalProject_Add(SymRuntime +ExternalProject_Add(SymCCRuntime SOURCE_DIR ${CMAKE_SOURCE_DIR}/runtime CMAKE_ARGS ${SYM_RUNTIME_BUILD_ARGS} @@ -56,11 +67,11 @@ ExternalProject_Add(SymRuntime INSTALL_COMMAND "" BUILD_ALWAYS TRUE) -ExternalProject_Get_Property(SymRuntime BINARY_DIR) -set(SYM_RUNTIME_DIR ${BINARY_DIR}) +ExternalProject_Get_Property(SymCCRuntime BINARY_DIR) +set(SYMCC_RUNTIME_DIR ${BINARY_DIR}) if (${TARGET_32BIT}) - ExternalProject_Add(SymRuntime32 + ExternalProject_Add(SymCCRuntime32 SOURCE_DIR ${CMAKE_SOURCE_DIR}/runtime CMAKE_ARGS ${SYM_RUNTIME_BUILD_ARGS} @@ -71,8 +82,8 @@ if (${TARGET_32BIT}) INSTALL_COMMAND "" BUILD_ALWAYS TRUE) - ExternalProject_Get_Property(SymRuntime32 BINARY_DIR) - set(SYM_RUNTIME_32BIT_DIR ${BINARY_DIR}) + ExternalProject_Get_Property(SymCCRuntime32 BINARY_DIR) + set(SYMCC_RUNTIME_32BIT_DIR ${BINARY_DIR}) endif() find_package(LLVM REQUIRED CONFIG) @@ -88,7 +99,8 @@ endif() add_definitions(${LLVM_DEFINITIONS}) include_directories(SYSTEM ${LLVM_INCLUDE_DIRS}) -set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -std=c++17 \ +set(CMAKE_CXX_STANDARD 17) +set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} \ -Wredundant-decls -Wcast-align -Wmissing-include-dirs -Wswitch-default \ -Wextra -Wall -Winvalid-pch -Wredundant-decls -Wformat=2 \ -Wmissing-format-attribute -Wformat-nonliteral -Werror -Wno-error=deprecated-declarations") @@ -99,13 +111,15 @@ set(CMAKE_MODULE_LINKER_FLAGS "${CMAKE_MODULE_LINKER_FLAGS} -Wl,-z,nodelete") # This is the compiler pass that we later load into clang or opt. If LLVM is # built without RTTI we have to disable it for our library too, otherwise we'll # get linker errors. -add_library(Symbolize MODULE +add_library(SymCC MODULE compiler/Symbolizer.cpp compiler/Pass.cpp compiler/Runtime.cpp compiler/Main.cpp) + +set_target_properties(SymCC PROPERTIES OUTPUT_NAME "symcc") if (NOT LLVM_ENABLE_RTTI) - set_target_properties(Symbolize PROPERTIES COMPILE_FLAGS "-fno-rtti") + set_target_properties(SymCC PROPERTIES COMPILE_FLAGS "-fno-rtti") endif() find_program(CLANG_BINARY "clang" diff --git a/Dockerfile b/Dockerfile index ca7c871b..f2e2c758 100644 --- a/Dockerfile +++ b/Dockerfile @@ -21,19 +21,20 @@ FROM ubuntu:22.04 AS builder RUN apt-get update \ && DEBIAN_FRONTEND=noninteractive apt-get install -y \ cargo \ - clang-15 \ cmake \ g++ \ git \ libz3-dev \ - llvm-15-dev \ - llvm-15-tools \ ninja-build \ python3-pip \ zlib1g-dev \ + llvm-15 \ + clang-15 \ && rm -rf /var/lib/apt/lists/* RUN pip3 install lit +WORKDIR / + # Build AFL. RUN git clone -b v2.56b https://github.com/google/AFL.git afl \ && cd afl \ @@ -48,11 +49,7 @@ COPY . /symcc_source # Init submodules if they are not initialiazed yet WORKDIR /symcc_source -RUN if git submodule status | grep "^-">/dev/null ; then \ - echo "Initializing submodules"; \ - git submodule init; \ - git submodule update; \ - fi +RUN git submodule update --init --recursive # @@ -61,7 +58,7 @@ RUN if git submodule status | grep "^-">/dev/null ; then \ FROM builder AS builder_simple WORKDIR /symcc_build_simple RUN cmake -G Ninja \ - -DQSYM_BACKEND=OFF \ + -DSYMCC_RT_BACKEND=simple \ -DCMAKE_BUILD_TYPE=RelWithDebInfo \ -DZ3_TRUST_SYSTEM_VERSION=on \ /symcc_source \ @@ -93,7 +90,7 @@ RUN export SYMCC_REGULAR_LIBCXX=yes SYMCC_NO_SYMBOLIC_INPUT=yes \ FROM builder_libcxx AS builder_qsym WORKDIR /symcc_build RUN cmake -G Ninja \ - -DQSYM_BACKEND=ON \ + -DSYMCC_RT_BACKEND=qsym \ -DCMAKE_BUILD_TYPE=RelWithDebInfo \ -DZ3_TRUST_SYSTEM_VERSION=on \ /symcc_source \ @@ -109,9 +106,7 @@ FROM ubuntu:22.04 RUN apt-get update \ && DEBIAN_FRONTEND=noninteractive apt-get install -y \ build-essential \ - clang-15 \ g++ \ - libllvm15 \ zlib1g \ sudo \ && rm -rf /var/lib/apt/lists/* \ diff --git a/LICENSE.lgpl b/LICENSE.lgpl deleted file mode 100644 index 0a041280..00000000 --- a/LICENSE.lgpl +++ /dev/null @@ -1,165 +0,0 @@ - GNU LESSER GENERAL PUBLIC LICENSE - Version 3, 29 June 2007 - - Copyright (C) 2007 Free Software Foundation, Inc. - Everyone is permitted to copy and distribute verbatim copies - of this license document, but changing it is not allowed. - - - This version of the GNU Lesser General Public License incorporates -the terms and conditions of version 3 of the GNU General Public -License, supplemented by the additional permissions listed below. - - 0. Additional Definitions. - - As used herein, "this License" refers to version 3 of the GNU Lesser -General Public License, and the "GNU GPL" refers to version 3 of the GNU -General Public License. - - "The Library" refers to a covered work governed by this License, -other than an Application or a Combined Work as defined below. - - An "Application" is any work that makes use of an interface provided -by the Library, but which is not otherwise based on the Library. -Defining a subclass of a class defined by the Library is deemed a mode -of using an interface provided by the Library. - - A "Combined Work" is a work produced by combining or linking an -Application with the Library. The particular version of the Library -with which the Combined Work was made is also called the "Linked -Version". - - The "Minimal Corresponding Source" for a Combined Work means the -Corresponding Source for the Combined Work, excluding any source code -for portions of the Combined Work that, considered in isolation, are -based on the Application, and not on the Linked Version. - - The "Corresponding Application Code" for a Combined Work means the -object code and/or source code for the Application, including any data -and utility programs needed for reproducing the Combined Work from the -Application, but excluding the System Libraries of the Combined Work. - - 1. Exception to Section 3 of the GNU GPL. - - You may convey a covered work under sections 3 and 4 of this License -without being bound by section 3 of the GNU GPL. - - 2. Conveying Modified Versions. - - If you modify a copy of the Library, and, in your modifications, a -facility refers to a function or data to be supplied by an Application -that uses the facility (other than as an argument passed when the -facility is invoked), then you may convey a copy of the modified -version: - - a) under this License, provided that you make a good faith effort to - ensure that, in the event an Application does not supply the - function or data, the facility still operates, and performs - whatever part of its purpose remains meaningful, or - - b) under the GNU GPL, with none of the additional permissions of - this License applicable to that copy. - - 3. Object Code Incorporating Material from Library Header Files. - - The object code form of an Application may incorporate material from -a header file that is part of the Library. You may convey such object -code under terms of your choice, provided that, if the incorporated -material is not limited to numerical parameters, data structure -layouts and accessors, or small macros, inline functions and templates -(ten or fewer lines in length), you do both of the following: - - a) Give prominent notice with each copy of the object code that the - Library is used in it and that the Library and its use are - covered by this License. - - b) Accompany the object code with a copy of the GNU GPL and this license - document. - - 4. Combined Works. - - You may convey a Combined Work under terms of your choice that, -taken together, effectively do not restrict modification of the -portions of the Library contained in the Combined Work and reverse -engineering for debugging such modifications, if you also do each of -the following: - - a) Give prominent notice with each copy of the Combined Work that - the Library is used in it and that the Library and its use are - covered by this License. - - b) Accompany the Combined Work with a copy of the GNU GPL and this license - document. - - c) For a Combined Work that displays copyright notices during - execution, include the copyright notice for the Library among - these notices, as well as a reference directing the user to the - copies of the GNU GPL and this license document. - - d) Do one of the following: - - 0) Convey the Minimal Corresponding Source under the terms of this - License, and the Corresponding Application Code in a form - suitable for, and under terms that permit, the user to - recombine or relink the Application with a modified version of - the Linked Version to produce a modified Combined Work, in the - manner specified by section 6 of the GNU GPL for conveying - Corresponding Source. - - 1) Use a suitable shared library mechanism for linking with the - Library. A suitable mechanism is one that (a) uses at run time - a copy of the Library already present on the user's computer - system, and (b) will operate properly with a modified version - of the Library that is interface-compatible with the Linked - Version. - - e) Provide Installation Information, but only if you would otherwise - be required to provide such information under section 6 of the - GNU GPL, and only to the extent that such information is - necessary to install and execute a modified version of the - Combined Work produced by recombining or relinking the - Application with a modified version of the Linked Version. (If - you use option 4d0, the Installation Information must accompany - the Minimal Corresponding Source and Corresponding Application - Code. If you use option 4d1, you must provide the Installation - Information in the manner specified by section 6 of the GNU GPL - for conveying Corresponding Source.) - - 5. Combined Libraries. - - You may place library facilities that are a work based on the -Library side by side in a single library together with other library -facilities that are not Applications and are not covered by this -License, and convey such a combined library under terms of your -choice, if you do both of the following: - - a) Accompany the combined library with a copy of the same work based - on the Library, uncombined with any other library facilities, - conveyed under the terms of this License. - - b) Give prominent notice with the combined library that part of it - is a work based on the Library, and explaining where to find the - accompanying uncombined form of the same work. - - 6. Revised Versions of the GNU Lesser General Public License. - - The Free Software Foundation may publish revised and/or new versions -of the GNU Lesser General Public License from time to time. Such new -versions will be similar in spirit to the present version, but may -differ in detail to address new problems or concerns. - - Each version is given a distinguishing version number. If the -Library as you received it specifies that a certain numbered version -of the GNU Lesser General Public License "or any later version" -applies to it, you have the option of following the terms and -conditions either of that published version or of any later version -published by the Free Software Foundation. If the Library as you -received it does not specify a version number of the GNU Lesser -General Public License, you may choose any version of the GNU Lesser -General Public License ever published by the Free Software Foundation. - - If the Library as you received it specifies that a proxy can decide -whether future versions of the GNU Lesser General Public License shall -apply, that proxy's public statement of acceptance of any version is -permanent authorization for you to choose that version for the -Library. diff --git a/README.md b/README.md index 4356d0b2..25155711 100644 --- a/README.md +++ b/README.md @@ -20,7 +20,7 @@ and 18) and Z3 (version 4.5 or later), as well as a C++ compiler with support for C++17. LLVM lit is only needed to run the tests; if it's not packaged with your LLVM, you can get it with `pip install lit`. -Under Ubuntu Groovy the following one liner should install all required +Under Ubuntu Groovy the following one-liner should install all required packages: ``` @@ -31,11 +31,10 @@ Alternatively, see below for using the provided Dockerfile, or the file `util/quicktest.sh` for exact steps to perform under Ubuntu (or use with the provided Vagrant file). -Make sure to pull the QSYM code: +Make sure to pull the SymCC Runtime: ``` -$ git submodule init -$ git submodule update +$ git submodule update --init --recursive ``` Note that it is not necessary or recommended to build the QSYM submodule - our @@ -46,7 +45,7 @@ Create a build directory somewhere, and execute the following commands inside it: ``` -$ cmake -G Ninja -DQSYM_BACKEND=ON /path/to/compiler/sources +$ cmake -G Ninja -DSYMCC_RT_BACKEND=qsym /path/to/compiler/sources $ ninja check ``` @@ -153,8 +152,6 @@ Docker image enables optional C++ support from source, so creating the image can take quite some time!) ``` -$ git submodule init -$ git submodule update $ docker build -t symcc . $ docker run -it --rm symcc ``` @@ -196,8 +193,8 @@ many cases it is sufficient to let the build system figure out what to rebuild ### Why is SymCC only exploring one path and not all paths? -SymCC is currently a concolic executor it follows the concrete -path. In theory, it would be possible to make it a forking executor +SymCC is currently a concolic executor. As such, it follows the concrete +path. In theory, it would be possible to make it a forking executor - see [issue #14](https://github.com/eurecom-s3/symcc/issues/14) ### Why does SymCC not generate some test cases? @@ -291,11 +288,6 @@ SymCC 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. -As an exception from the above, you can redistribute and/or modify the SymCC -runtime under the terms of the GNU Lesser General Public License as published by -the Free Software Foundation, either version 3 of the License, or (at your -option) any later version. See #114 for the rationale. - SymCC 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. @@ -309,6 +301,4 @@ licenses, and/or restrictions: | Program | Directory | |---------------|-----------------------------| -| QSYM | `runtime/qsym_backend/qsym` | -| SymCC runtime | `runtime` | - +| SymCC Runtime | `runtime` | diff --git a/cmake/FindFilesystem.cmake b/cmake/FindFilesystem.cmake deleted file mode 100644 index a152e522..00000000 --- a/cmake/FindFilesystem.cmake +++ /dev/null @@ -1,247 +0,0 @@ -# Distributed under the OSI-approved BSD 3-Clause License. See accompanying -# file Copyright.txt or https://cmake.org/licensing for details. - -#[=======================================================================[.rst: - -FindFilesystem -############## - -This module supports the C++17 standard library's filesystem utilities. Use the -:imp-target:`std::filesystem` imported target to - -Options -******* - -The ``COMPONENTS`` argument to this module supports the following values: - -.. find-component:: Experimental - :name: fs.Experimental - - Allows the module to find the "experimental" Filesystem TS version of the - Filesystem library. This is the library that should be used with the - ``std::experimental::filesystem`` namespace. - -.. find-component:: Final - :name: fs.Final - - Finds the final C++17 standard version of the filesystem library. - -If no components are provided, behaves as if the -:find-component:`fs.Final` component was specified. - -If both :find-component:`fs.Experimental` and :find-component:`fs.Final` are -provided, first looks for ``Final``, and falls back to ``Experimental`` in case -of failure. If ``Final`` is found, :imp-target:`std::filesystem` and all -:ref:`variables ` will refer to the ``Final`` version. - - -Imported Targets -**************** - -.. imp-target:: std::filesystem - - The ``std::filesystem`` imported target is defined when any requested - version of the C++ filesystem library has been found, whether it is - *Experimental* or *Final*. - - If no version of the filesystem library is available, this target will not - be defined. - - .. note:: - This target has ``cxx_std_17`` as an ``INTERFACE`` - :ref:`compile language standard feature `. Linking - to this target will automatically enable C++17 if no later standard - version is already required on the linking target. - - -.. _fs.variables: - -Variables -********* - -.. variable:: CXX_FILESYSTEM_IS_EXPERIMENTAL - - Set to ``TRUE`` when the :find-component:`fs.Experimental` version of C++ - filesystem library was found, otherwise ``FALSE``. - -.. variable:: CXX_FILESYSTEM_HAVE_FS - - Set to ``TRUE`` when a filesystem header was found. - -.. variable:: CXX_FILESYSTEM_HEADER - - Set to either ``filesystem`` or ``experimental/filesystem`` depending on - whether :find-component:`fs.Final` or :find-component:`fs.Experimental` was - found. - -.. variable:: CXX_FILESYSTEM_NAMESPACE - - Set to either ``std::filesystem`` or ``std::experimental::filesystem`` - depending on whether :find-component:`fs.Final` or - :find-component:`fs.Experimental` was found. - - -Examples -******** - -Using `find_package(Filesystem)` with no component arguments: - -.. code-block:: cmake - - find_package(Filesystem REQUIRED) - - add_executable(my-program main.cpp) - target_link_libraries(my-program PRIVATE std::filesystem) - - -#]=======================================================================] - - -if(TARGET std::filesystem) - # This module has already been processed. Don't do it again. - return() -endif() - -cmake_minimum_required(VERSION 3.10) - -include(CMakePushCheckState) -include(CheckIncludeFileCXX) - -# If we're not cross-compiling, try to run test executables. -# Otherwise, assume that compile + link is a sufficient check. -if(CMAKE_CROSSCOMPILING) - include(CheckCXXSourceCompiles) - macro(_cmcm_check_cxx_source code var) - check_cxx_source_compiles("${code}" ${var}) - endmacro() -else() - include(CheckCXXSourceRuns) - macro(_cmcm_check_cxx_source code var) - check_cxx_source_runs("${code}" ${var}) - endmacro() -endif() - -cmake_push_check_state() - -set(CMAKE_REQUIRED_QUIET ${Filesystem_FIND_QUIETLY}) - -# All of our tests required C++17 or later -set(CMAKE_CXX_STANDARD 17) - -# Normalize and check the component list we were given -set(want_components ${Filesystem_FIND_COMPONENTS}) -if(Filesystem_FIND_COMPONENTS STREQUAL "") - set(want_components Final) -endif() - -# Warn on any unrecognized components -set(extra_components ${want_components}) -list(REMOVE_ITEM extra_components Final Experimental) -foreach(component IN LISTS extra_components) - message(WARNING "Extraneous find_package component for Filesystem: ${component}") -endforeach() - -# Detect which of Experimental and Final we should look for -set(find_experimental TRUE) -set(find_final TRUE) -if(NOT "Final" IN_LIST want_components) - set(find_final FALSE) -endif() -if(NOT "Experimental" IN_LIST want_components) - set(find_experimental FALSE) -endif() - -if(find_final) - check_include_file_cxx("filesystem" _CXX_FILESYSTEM_HAVE_HEADER) - mark_as_advanced(_CXX_FILESYSTEM_HAVE_HEADER) - if(_CXX_FILESYSTEM_HAVE_HEADER) - # We found the non-experimental header. Don't bother looking for the - # experimental one. - set(find_experimental FALSE) - endif() -else() - set(_CXX_FILESYSTEM_HAVE_HEADER FALSE) -endif() - -if(find_experimental) - check_include_file_cxx("experimental/filesystem" _CXX_FILESYSTEM_HAVE_EXPERIMENTAL_HEADER) - mark_as_advanced(_CXX_FILESYSTEM_HAVE_EXPERIMENTAL_HEADER) -else() - set(_CXX_FILESYSTEM_HAVE_EXPERIMENTAL_HEADER FALSE) -endif() - -if(_CXX_FILESYSTEM_HAVE_HEADER) - set(_have_fs TRUE) - set(_fs_header filesystem) - set(_fs_namespace std::filesystem) - set(_is_experimental FALSE) -elseif(_CXX_FILESYSTEM_HAVE_EXPERIMENTAL_HEADER) - set(_have_fs TRUE) - set(_fs_header experimental/filesystem) - set(_fs_namespace std::experimental::filesystem) - set(_is_experimental TRUE) -else() - set(_have_fs FALSE) -endif() - -set(CXX_FILESYSTEM_HAVE_FS ${_have_fs} CACHE BOOL "TRUE if we have the C++ filesystem headers") -set(CXX_FILESYSTEM_HEADER ${_fs_header} CACHE STRING "The header that should be included to obtain the filesystem APIs") -set(CXX_FILESYSTEM_NAMESPACE ${_fs_namespace} CACHE STRING "The C++ namespace that contains the filesystem APIs") -set(CXX_FILESYSTEM_IS_EXPERIMENTAL ${_is_experimental} CACHE BOOL "TRUE if the C++ filesystem library is the experimental version") - -set(_found FALSE) - -if(CXX_FILESYSTEM_HAVE_FS) - # We have some filesystem library available. Do link checks - string(CONFIGURE [[ - #include - #include <@CXX_FILESYSTEM_HEADER@> - - int main() { - auto cwd = @CXX_FILESYSTEM_NAMESPACE@::current_path(); - printf("%s", cwd.c_str()); - return EXIT_SUCCESS; - } - ]] code @ONLY) - - # Check a simple filesystem program without any linker flags - _cmcm_check_cxx_source("${code}" CXX_FILESYSTEM_NO_LINK_NEEDED) - - set(can_link ${CXX_FILESYSTEM_NO_LINK_NEEDED}) - - if(NOT CXX_FILESYSTEM_NO_LINK_NEEDED) - set(prev_libraries ${CMAKE_REQUIRED_LIBRARIES}) - # Add the libstdc++ flag - set(CMAKE_REQUIRED_LIBRARIES ${prev_libraries} -lstdc++fs) - _cmcm_check_cxx_source("${code}" CXX_FILESYSTEM_STDCPPFS_NEEDED) - set(can_link ${CXX_FILESYSTEM_STDCPPFS_NEEDED}) - if(NOT CXX_FILESYSTEM_STDCPPFS_NEEDED) - # Try the libc++ flag - set(CMAKE_REQUIRED_LIBRARIES ${prev_libraries} -lc++fs) - _cmcm_check_cxx_source("${code}" CXX_FILESYSTEM_CPPFS_NEEDED) - set(can_link ${CXX_FILESYSTEM_CPPFS_NEEDED}) - endif() - endif() - - if(can_link) - add_library(std::filesystem INTERFACE IMPORTED) - set_property(TARGET std::filesystem APPEND PROPERTY INTERFACE_COMPILE_FEATURES cxx_std_17) - set(_found TRUE) - - if(CXX_FILESYSTEM_NO_LINK_NEEDED) - # Nothing to add... - elseif(CXX_FILESYSTEM_STDCPPFS_NEEDED) - set_property(TARGET std::filesystem APPEND PROPERTY INTERFACE_LINK_LIBRARIES -lstdc++fs) - elseif(CXX_FILESYSTEM_CPPFS_NEEDED) - set_property(TARGET std::filesystem APPEND PROPERTY INTERFACE_LINK_LIBRARIES -lc++fs) - endif() - endif() -endif() - -cmake_pop_check_state() - -set(Filesystem_FOUND ${_found} CACHE BOOL "TRUE if we can run a program using std::filesystem" FORCE) - -if(Filesystem_FIND_REQUIRED AND NOT Filesystem_FOUND) - message(FATAL_ERROR "Cannot run simple program using std::filesystem") -endif() diff --git a/compiler/sym++.in b/compiler/sym++.in index 2b775739..6e2f9661 100755 --- a/compiler/sym++.in +++ b/compiler/sym++.in @@ -14,9 +14,9 @@ # You should have received a copy of the GNU General Public License along with # SymCC. If not, see . -runtime_64bit_dir="${SYMCC_RUNTIME_DIR:-@SYM_RUNTIME_DIR@}" -runtime_32bit_dir="${SYMCC_RUNTIME32_DIR:-@SYM_RUNTIME_32BIT_DIR@}" -pass="${SYMCC_PASS_DIR:-@CMAKE_CURRENT_BINARY_DIR@}/libSymbolize.so" +runtime_64bit_dir="${SYMCC_RUNTIME_DIR:-@SYMCC_RUNTIME_DIR@}" +runtime_32bit_dir="${SYMCC_RUNTIME32_DIR:-@SYMCC_RUNTIME_32BIT_DIR@}" +pass="${SYMCC_PASS_DIR:-@CMAKE_CURRENT_BINARY_DIR@}/libsymcc.so" libcxx_var=SYMCC_LIBCXX_PATH compiler="${SYMCC_CLANGPP:-@CLANGPP_BINARY@}" @@ -60,6 +60,6 @@ exec $compiler \ "$@" \ $stdlib_ldflags \ -L"$runtime_dir" \ - -lSymRuntime \ + -lsymcc-rt \ -Wl,-rpath,"$runtime_dir" \ -Qunused-arguments diff --git a/compiler/symcc.in b/compiler/symcc.in index 4e0ad37e..c5bd6022 100755 --- a/compiler/symcc.in +++ b/compiler/symcc.in @@ -14,9 +14,9 @@ # You should have received a copy of the GNU General Public License along with # SymCC. If not, see . -runtime_64bit_dir="${SYMCC_RUNTIME_DIR:-@SYM_RUNTIME_DIR@}" -runtime_32bit_dir="${SYMCC_RUNTIME32_DIR:-@SYM_RUNTIME_32BIT_DIR@}" -pass="${SYMCC_PASS_DIR:-@CMAKE_CURRENT_BINARY_DIR@}/libSymbolize.so" +runtime_64bit_dir="${SYMCC_RUNTIME_DIR:-@SYMCC_RUNTIME_DIR@}" +runtime_32bit_dir="${SYMCC_RUNTIME32_DIR:-@SYMCC_RUNTIME_32BIT_DIR@}" +pass="${SYMCC_PASS_DIR:-@CMAKE_CURRENT_BINARY_DIR@}/libsymcc.so" compiler="${SYMCC_CLANG:-@CLANG_BINARY@}" # Find out if we're cross-compiling for a 32-bit architecture @@ -38,10 +38,10 @@ if [ $# -eq 0 ]; then exit 1 fi -exec $compiler \ +exec "$compiler" \ @CLANG_LOAD_PASS@"$pass" \ "$@" \ -L"$runtime_dir" \ - -lSymRuntime \ + -lsymcc-rt \ -Wl,-rpath,"$runtime_dir" \ -Qunused-arguments diff --git a/docs/Backends.txt b/docs/Backends.txt deleted file mode 100644 index ec3e53ff..00000000 --- a/docs/Backends.txt +++ /dev/null @@ -1,36 +0,0 @@ - - - Symbolic backends - - -We support different symbolic backends; currently, we have our own backend, -which is a custom thin wrapper around Z3, and the QSYM backend. Users choose -with a build option which backend to use. This file documents the internals of -this mechanism. - -At compile time, we always insert the same calls, no matter which backend is -used. Also, we always link against "libSymRuntime.so", so the choice of backend -is deferred until run time. From the target program's point of view, the only -requirement on a backend is that it be a shared library with the expected name -that implements the interface defined in runtime/RuntimeCommon.h (with type -"SymExpr" is defined to be something of pointer width). - -Depending on the build option QSYM_BACKEND we build either our own backend or -parts of QSYM (which are pulled in via a git submodule) and a small translation -layer. The code used by both backends is in the directory "runtime", while the -specific parts are in "runtime/simple" and "runtime/qsym". - -The QSYM backend expects to be passed the program counter at each jump -instruction, which is used to uniquely identify the jump site and implement a -per-site back-off mechanism. However, there is no reason for the supplied value -to be the program counter as long as it is a unique identifier. Since it is -somewhat challenging to obtain the current program counter in our -compilation-based setting, we follow an alternative approach: in the compiler -pass, we identify each jump site by the address of the LLVM object that -represents the instruction; experiments suggest that it is a good enough -identifier. This value is embedded into the target program as a constant and -passed to the backend at run time. - -Before compiling the QSYM code, we are expected to execute two Python scripts -that the QSYM authors use for code generation; two custom CMake targets take -care of running the scripts and tracking changes to the relevant source files. diff --git a/runtime b/runtime new file mode 160000 index 00000000..892f817f --- /dev/null +++ b/runtime @@ -0,0 +1 @@ +Subproject commit 892f817f38f5abfa083dd0c1caa7ced821566bf5 diff --git a/runtime/CMakeLists.txt b/runtime/CMakeLists.txt deleted file mode 100644 index 07277b8f..00000000 --- a/runtime/CMakeLists.txt +++ /dev/null @@ -1,43 +0,0 @@ -# This file is part of the SymCC runtime. -# -# The SymCC runtime is free software: you can redistribute it and/or modify it -# under the terms of the GNU Lesser General Public License as published by the -# Free Software Foundation, either version 3 of the License, or (at your option) -# any later version. -# -# The SymCC runtime 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 Lesser General Public License -# for more details. -# -# You should have received a copy of the GNU Lesser General Public License along -# with the SymCC runtime. If not, see . - -cmake_minimum_required(VERSION 3.5) -project(SymRuntime) - -set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -std=c++17 \ --Wredundant-decls -Wcast-align \ --Wmissing-include-dirs -Wswitch-default \ --Wextra -Wall -Winvalid-pch -Wredundant-decls -Wformat=2 \ --Wmissing-format-attribute -Wformat-nonliteral") - -option(QSYM_BACKEND "Use the Qsym backend instead of our own" OFF) -option(Z3_TRUST_SYSTEM_VERSION "Use the system-provided Z3 without a version check" OFF) - -# Place the final product in the top-level output directory -set(CMAKE_LIBRARY_OUTPUT_DIRECTORY ${CMAKE_BINARY_DIR}) - -# There is list(TRANSFORM ... PREPEND ...), but it's not available before CMake 3.12. -set(SHARED_RUNTIME_SOURCES - ${CMAKE_CURRENT_SOURCE_DIR}/Config.cpp - ${CMAKE_CURRENT_SOURCE_DIR}/RuntimeCommon.cpp - ${CMAKE_CURRENT_SOURCE_DIR}/LibcWrappers.cpp - ${CMAKE_CURRENT_SOURCE_DIR}/Shadow.cpp - ${CMAKE_CURRENT_SOURCE_DIR}/GarbageCollection.cpp) - -if (${QSYM_BACKEND}) - add_subdirectory(qsym_backend) -else() - add_subdirectory(simple_backend) -endif() diff --git a/runtime/Config.cpp b/runtime/Config.cpp deleted file mode 100644 index 23a28df6..00000000 --- a/runtime/Config.cpp +++ /dev/null @@ -1,95 +0,0 @@ -// This file is part of the SymCC runtime. -// -// The SymCC runtime is free software: you can redistribute it and/or modify it -// under the terms of the GNU Lesser General Public License as published by the -// Free Software Foundation, either version 3 of the License, or (at your -// option) any later version. -// -// The SymCC runtime 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 Lesser General Public License -// for more details. -// -// You should have received a copy of the GNU Lesser General Public License -// along with the SymCC runtime. If not, see . - -#include "Config.h" - -#include -#include -#include -#include -#include -#include - -namespace { - -bool checkFlagString(std::string value) { - std::transform(value.begin(), value.end(), value.begin(), - [](unsigned char c) { return std::tolower(c); }); - if (value == "1" || value == "on" || value == "yes") - return true; - - if (value.empty() || value == "0" || value == "off" || value == "no") - return false; - - std::stringstream msg; - msg << "Unknown flag value " << value; - throw std::runtime_error(msg.str()); -} - -} // namespace - -Config g_config; - -void loadConfig() { - auto *outputDir = getenv("SYMCC_OUTPUT_DIR"); - if (outputDir != nullptr) - g_config.outputDir = outputDir; - - auto *inputFile = getenv("SYMCC_INPUT_FILE"); - if (inputFile != nullptr) - g_config.input = FileInput{inputFile}; - - auto *memoryInput = getenv("SYMCC_MEMORY_INPUT"); - if (memoryInput != nullptr && checkFlagString(memoryInput)) { - if (std::holds_alternative(g_config.input)) - throw std::runtime_error{ - "Can't enable file and memory input at the same time"}; - - g_config.input = MemoryInput{}; - } - - auto *fullyConcrete = getenv("SYMCC_NO_SYMBOLIC_INPUT"); - if (fullyConcrete != nullptr && checkFlagString(fullyConcrete)) - g_config.input = NoInput{}; - - auto *logFile = getenv("SYMCC_LOG_FILE"); - if (logFile != nullptr) - g_config.logFile = logFile; - - auto *pruning = getenv("SYMCC_ENABLE_LINEARIZATION"); - if (pruning != nullptr) - g_config.pruning = checkFlagString(pruning); - - auto *aflCoverageMap = getenv("SYMCC_AFL_COVERAGE_MAP"); - if (aflCoverageMap != nullptr) - g_config.aflCoverageMap = aflCoverageMap; - - auto *garbageCollectionThreshold = getenv("SYMCC_GC_THRESHOLD"); - if (garbageCollectionThreshold != nullptr) { - try { - g_config.garbageCollectionThreshold = - std::stoul(garbageCollectionThreshold); - } catch (std::invalid_argument &) { - std::stringstream msg; - msg << "Can't convert " << garbageCollectionThreshold << " to an integer"; - throw std::runtime_error(msg.str()); - } catch (std::out_of_range &) { - std::stringstream msg; - msg << "The GC threshold must be between 0 and " - << std::numeric_limits::max(); - throw std::runtime_error(msg.str()); - } - } -} diff --git a/runtime/Config.h b/runtime/Config.h deleted file mode 100644 index a866821c..00000000 --- a/runtime/Config.h +++ /dev/null @@ -1,83 +0,0 @@ -// This file is part of the SymCC runtime. -// -// The SymCC runtime is free software: you can redistribute it and/or modify it -// under the terms of the GNU Lesser General Public License as published by the -// Free Software Foundation, either version 3 of the License, or (at your -// option) any later version. -// -// The SymCC runtime 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 Lesser General Public License -// for more details. -// -// You should have received a copy of the GNU Lesser General Public License -// along with the SymCC runtime. If not, see . - -#ifndef CONFIG_H -#define CONFIG_H - -#include -#include - -/// Marker struct for fully concrete execution. -struct NoInput {}; - -/// Marker struct for symbolic input from stdin. -struct StdinInput {}; - -/// Marker struct for symbolic input via _sym_make_symbolic. -struct MemoryInput {}; - -/// Configuration for symbolic input from a file. -struct FileInput { - /// The name of input file. - std::string fileName; -}; - -struct Config { - using InputConfig = std::variant; - - /// The configuration for our symbolic input. - InputConfig input = StdinInput{}; - - /// The directory for storing new outputs. - std::string outputDir = "/tmp/output"; - - /// The file to log constraint solving information to. - std::string logFile = ""; - - /// Do we prune expressions on hot paths? - bool pruning = false; - - /// The AFL coverage map to initialize with. - /// - /// Specifying a file name here allows us to track already covered program - /// locations across multiple program executions. - std::string aflCoverageMap = ""; - - /// The garbage collection threshold. - /// - /// We will start collecting unused symbolic expressions if the total number - /// of allocated expressions in the target program exceeds this number. - /// - /// Collecting too often hurts performance, whereas delaying garbage - /// collection for too long might make us run out of memory. The goal of this - /// empirically determined constant is to keep peek memory consumption below - /// 2GB on most workloads because requiring that amount of memory per core - /// participating in the analysis seems reasonable. - size_t garbageCollectionThreshold = 5'000'000; -}; - -/// The global configuration object. -/// -/// It should be initialized once before we start executing the program and -/// never changed afterwards. -extern Config g_config; - -/// Populate g_config from the environment. -/// -/// The function will throw std::runtime_error if the value of an environment -/// variable used for configuration cannot be interpreted. -void loadConfig(); - -#endif diff --git a/runtime/GarbageCollection.cpp b/runtime/GarbageCollection.cpp deleted file mode 100644 index 8afdd327..00000000 --- a/runtime/GarbageCollection.cpp +++ /dev/null @@ -1,50 +0,0 @@ -// This file is part of the SymCC runtime. -// -// The SymCC runtime is free software: you can redistribute it and/or modify it -// under the terms of the GNU Lesser General Public License as published by the -// Free Software Foundation, either version 3 of the License, or (at your -// option) any later version. -// -// The SymCC runtime 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 Lesser General Public License -// for more details. -// -// You should have received a copy of the GNU Lesser General Public License -// along with SymCC. If not, see . - -#include "GarbageCollection.h" - -#include - -#include -#include - -/// A list of memory regions that are known to contain symbolic expressions. -std::vector expressionRegions; - -void registerExpressionRegion(ExpressionRegion r) { - expressionRegions.push_back(std::move(r)); -} - -std::set collectReachableExpressions() { - std::set reachableExpressions; - auto collectReachableExpressions = [&](ExpressionRegion r) { - auto *end = r.first + r.second; - for (SymExpr *expr_ptr = r.first; expr_ptr < end; expr_ptr++) { - if (*expr_ptr != nullptr) { - reachableExpressions.insert(*expr_ptr); - } - } - }; - - for (auto &r : expressionRegions) { - collectReachableExpressions(r); - } - - for (const auto &mapping : g_shadow_pages) { - collectReachableExpressions({mapping.second, kPageSize}); - } - - return reachableExpressions; -} diff --git a/runtime/GarbageCollection.h b/runtime/GarbageCollection.h deleted file mode 100644 index 81b0b8c2..00000000 --- a/runtime/GarbageCollection.h +++ /dev/null @@ -1,35 +0,0 @@ -// This file is part of the SymCC runtime. -// -// The SymCC runtime is free software: you can redistribute it and/or modify it -// under the terms of the GNU Lesser General Public License as published by the -// Free Software Foundation, either version 3 of the License, or (at your -// option) any later version. -// -// The SymCC runtime 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 Lesser General Public License -// for more details. -// -// You should have received a copy of the GNU Lesser General Public License -// along with the SymCC runtime. If not, see . - -#ifndef GARBAGECOLLECTION_H -#define GARBAGECOLLECTION_H - -#include -#include - -#include - -/// An imitation of std::span (which is not available before C++20) for symbolic -/// expressions. -using ExpressionRegion = std::pair; - -/// Add the specified region to the list of places to search for symbolic -/// expressions. -void registerExpressionRegion(ExpressionRegion r); - -/// Return the set of currently reachable symbolic expressions. -std::set collectReachableExpressions(); - -#endif diff --git a/runtime/LibcWrappers.cpp b/runtime/LibcWrappers.cpp deleted file mode 100644 index cfe55525..00000000 --- a/runtime/LibcWrappers.cpp +++ /dev/null @@ -1,611 +0,0 @@ -// This file is part of the SymCC runtime. -// -// The SymCC runtime is free software: you can redistribute it and/or modify it -// under the terms of the GNU Lesser General Public License as published by the -// Free Software Foundation, either version 3 of the License, or (at your -// option) any later version. -// -// The SymCC runtime 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 Lesser General Public License -// for more details. -// -// You should have received a copy of the GNU Lesser General Public License -// along with SymCC. If not, see . - -// -// Libc wrappers -// -// This file contains the wrappers around libc functions which add symbolic -// computations; using the wrappers frees instrumented code from having to link -// against an instrumented libc. -// -// We define a wrapper for function X with SYM(X), which just changes the name -// "X" to something predictable and hopefully unique. It is then up to the -// compiler pass to replace calls of X with calls of SYM(X). -// -// In general, the wrappers ask the solver to generate alternative parameter -// values, then call the wrapped function, create and store symbolic expressions -// matching the libc function's semantics, and finally return the wrapped -// function's result. - -#include -#include -#include -#include -#include -#include -#include -#include - -#include -#include -#include -#include -#include - -#include "Config.h" -#include "Shadow.h" -#include - -#define SYM(x) x##_symbolized - -namespace { - -/// The file descriptor referring to the symbolic input. -int inputFileDescriptor = -1; - -/// The current position in the (symbolic) input. -uint64_t inputOffset = 0; - -/// Tell the solver to try an alternative value than the given one. -template -void tryAlternative(V value, SymExpr valueExpr, F caller) { - if (valueExpr) { - _sym_push_path_constraint( - _sym_build_equal(valueExpr, - _sym_build_integer(value, sizeof(value) * 8)), - true, reinterpret_cast(caller)); - } -} - -// A partial specialization for pointer types for convenience. -template -void tryAlternative(E *value, SymExpr valueExpr, F caller) { - tryAlternative(reinterpret_cast(value), valueExpr, caller); -} - -void maybeSetInputFile(const char *path, int fd) { - auto *fileInput = std::get_if(&g_config.input); - if (fileInput == nullptr) - return; - - if (strstr(path, fileInput->fileName.c_str()) == nullptr) - return; - - if (inputFileDescriptor != -1) - std::cerr << "Warning: input file opened multiple times; this is not yet " - "supported" - << std::endl; - - inputFileDescriptor = fd; - inputOffset = 0; -} - -} // namespace - -void initLibcWrappers() { - if (std::holds_alternative(g_config.input)) { - // Symbolic data comes from standard input. - inputFileDescriptor = 0; - } -} - -extern "C" { - -void *SYM(malloc)(size_t size) { - auto *result = malloc(size); - - tryAlternative(size, _sym_get_parameter_expression(0), SYM(malloc)); - - _sym_set_return_expression(nullptr); - return result; -} - -void *SYM(calloc)(size_t nmemb, size_t size) { - auto *result = calloc(nmemb, size); - - tryAlternative(nmemb, _sym_get_parameter_expression(0), SYM(calloc)); - tryAlternative(size, _sym_get_parameter_expression(1), SYM(calloc)); - - _sym_set_return_expression(nullptr); - return result; -} - -// See comment on lseek and lseek64 below; the same applies to the "off" -// parameter of mmap. - -void *SYM(mmap64)(void *addr, size_t len, int prot, int flags, int fildes, - uint64_t off) { - auto *result = mmap64(addr, len, prot, flags, fildes, off); - _sym_set_return_expression(nullptr); - - if (result == MAP_FAILED) // mmap failed - return result; - - if (fildes == inputFileDescriptor) { - /* we update the inputOffset only when mmap() is reading from input file - * HACK! update inputOffset with off parameter sometimes will be dangerous - * We don't know whether there is read() before/after mmap, - * if there is, we have to fix this tricky method :P - */ - inputOffset = off + len; - // Reading symbolic input. - ReadWriteShadow shadow(result, len); - uint8_t *resultBytes = (uint8_t *)result; - std::generate(shadow.begin(), shadow.end(), [resultBytes, i = 0]() mutable { - return _sym_get_input_byte(inputOffset, resultBytes[i++]); - }); - } else if (!isConcrete(result, len)) { - ReadWriteShadow shadow(result, len); - std::fill(shadow.begin(), shadow.end(), nullptr); - } - - tryAlternative(len, _sym_get_parameter_expression(1), SYM(mmap64)); - - return result; -} - -void *SYM(mmap)(void *addr, size_t len, int prot, int flags, int fildes, - uint32_t off) { - return SYM(mmap64)(addr, len, prot, flags, fildes, off); -} - -int SYM(open)(const char *path, int oflag, mode_t mode) { - auto result = open(path, oflag, mode); - _sym_set_return_expression(nullptr); - - if (result >= 0) - maybeSetInputFile(path, result); - - return result; -} - -ssize_t SYM(read)(int fildes, void *buf, size_t nbyte) { - tryAlternative(buf, _sym_get_parameter_expression(1), SYM(read)); - tryAlternative(nbyte, _sym_get_parameter_expression(2), SYM(read)); - - auto result = read(fildes, buf, nbyte); - _sym_set_return_expression(nullptr); - - if (result < 0) - return result; - - if (fildes == inputFileDescriptor) { - // Reading symbolic input. - _sym_make_symbolic(buf, result, inputOffset); - inputOffset += result; - } else if (!isConcrete(buf, result)) { - ReadWriteShadow shadow(buf, result); - std::fill(shadow.begin(), shadow.end(), nullptr); - } - - return result; -} - -// lseek is a bit tricky because, depending on preprocessor macros, glibc -// defines it to be a function operating on 32-bit values or aliases it to -// lseek64. Therefore, we cannot know in general whether calling lseek in our -// code takes a 32 or a 64-bit offset and whether it returns a 32 or a 64-bit -// result. In fact, since we compile this library against LLVM which requires us -// to compile with "-D_FILE_OFFSET_BITS=64", we happen to know that, for us, -// lseek is an alias to lseek64, but this may change any time. More importantly, -// client code may call one or the other, depending on its preprocessor -// definitions. -// -// Therefore, we define symbolic versions of both lseek and lseek64, but -// internally we only use lseek64 because it's the only one on whose -// availability we can rely. - -uint64_t SYM(lseek64)(int fd, uint64_t offset, int whence) { - auto result = lseek64(fd, offset, whence); - _sym_set_return_expression(nullptr); - if (result == (off_t)-1) - return result; - - if (whence == SEEK_SET) - _sym_set_return_expression(_sym_get_parameter_expression(1)); - - if (fd == inputFileDescriptor) - inputOffset = result; - - return result; -} - -uint32_t SYM(lseek)(int fd, uint32_t offset, int whence) { - uint64_t result = SYM(lseek64)(fd, offset, whence); - - // Perform the same overflow check as glibc in the 32-bit version of lseek. - - auto result32 = (uint32_t)result; - if (result == result32) - return result32; - - errno = EOVERFLOW; - return (uint32_t)-1; -} - -FILE *SYM(fopen)(const char *pathname, const char *mode) { - auto *result = fopen(pathname, mode); - _sym_set_return_expression(nullptr); - - if (result != nullptr) - maybeSetInputFile(pathname, fileno(result)); - - return result; -} - -FILE *SYM(fopen64)(const char *pathname, const char *mode) { - auto *result = fopen64(pathname, mode); - _sym_set_return_expression(nullptr); - - if (result != nullptr) - maybeSetInputFile(pathname, fileno(result)); - - return result; -} - -size_t SYM(fread)(void *ptr, size_t size, size_t nmemb, FILE *stream) { - tryAlternative(ptr, _sym_get_parameter_expression(0), SYM(fread)); - tryAlternative(size, _sym_get_parameter_expression(1), SYM(fread)); - tryAlternative(nmemb, _sym_get_parameter_expression(2), SYM(fread)); - - auto result = fread(ptr, size, nmemb, stream); - _sym_set_return_expression(nullptr); - - if (fileno(stream) == inputFileDescriptor) { - // Reading symbolic input. - _sym_make_symbolic(ptr, result * size, inputOffset); - inputOffset += result * size; - } else if (!isConcrete(ptr, result * size)) { - ReadWriteShadow shadow(ptr, result * size); - std::fill(shadow.begin(), shadow.end(), nullptr); - } - - return result; -} - -char *SYM(fgets)(char *str, int n, FILE *stream) { - tryAlternative(str, _sym_get_parameter_expression(0), SYM(fgets)); - tryAlternative(n, _sym_get_parameter_expression(1), SYM(fgets)); - - auto result = fgets(str, n, stream); - _sym_set_return_expression(_sym_get_parameter_expression(0)); - - if (fileno(stream) == inputFileDescriptor) { - // Reading symbolic input. - const auto length = sizeof(char) * strlen(str); - _sym_make_symbolic(str, length, inputOffset); - inputOffset += length; - } else if (!isConcrete(str, sizeof(char) * strlen(str))) { - ReadWriteShadow shadow(str, sizeof(char) * strlen(str)); - std::fill(shadow.begin(), shadow.end(), nullptr); - } - - return result; -} - -void SYM(rewind)(FILE *stream) { - rewind(stream); - _sym_set_return_expression(nullptr); - - if (fileno(stream) == inputFileDescriptor) { - inputOffset = 0; - } -} - -int SYM(fseek)(FILE *stream, long offset, int whence) { - tryAlternative(offset, _sym_get_parameter_expression(1), SYM(fseek)); - - auto result = fseek(stream, offset, whence); - _sym_set_return_expression(nullptr); - if (result == -1) - return result; - - if (fileno(stream) == inputFileDescriptor) { - auto pos = ftell(stream); - if (pos == -1) - return -1; - inputOffset = pos; - } - - return result; -} - -int SYM(fseeko)(FILE *stream, off_t offset, int whence) { - tryAlternative(offset, _sym_get_parameter_expression(1), SYM(fseeko)); - - auto result = fseeko(stream, offset, whence); - _sym_set_return_expression(nullptr); - if (result == -1) - return result; - - if (fileno(stream) == inputFileDescriptor) { - auto pos = ftello(stream); - if (pos == -1) - return -1; - inputOffset = pos; - } - - return result; -} - -int SYM(fseeko64)(FILE *stream, uint64_t offset, int whence) { - tryAlternative(offset, _sym_get_parameter_expression(1), SYM(fseeko64)); - - auto result = fseeko64(stream, offset, whence); - _sym_set_return_expression(nullptr); - if (result == -1) - return result; - - if (fileno(stream) == inputFileDescriptor) { - auto pos = ftello64(stream); - if (pos == -1) - return -1; - inputOffset = pos; - } - - return result; -} - -int SYM(getc)(FILE *stream) { - auto result = getc(stream); - if (result == EOF) { - _sym_set_return_expression(nullptr); - return result; - } - - if (fileno(stream) == inputFileDescriptor) - _sym_set_return_expression(_sym_build_zext( - _sym_get_input_byte(inputOffset++, result), sizeof(int) * 8 - 8)); - else - _sym_set_return_expression(nullptr); - - return result; -} - -int SYM(fgetc)(FILE *stream) { - auto result = fgetc(stream); - if (result == EOF) { - _sym_set_return_expression(nullptr); - return result; - } - - if (fileno(stream) == inputFileDescriptor) - _sym_set_return_expression(_sym_build_zext( - _sym_get_input_byte(inputOffset++, result), sizeof(int) * 8 - 8)); - else - _sym_set_return_expression(nullptr); - - return result; -} - -int SYM(getchar)(void) { return SYM(getc)(stdin); } - -int SYM(ungetc)(int c, FILE *stream) { - auto result = ungetc(c, stream); - _sym_set_return_expression(_sym_get_parameter_expression(0)); - - if (fileno(stream) == inputFileDescriptor && result != EOF) - inputOffset--; - - return result; -} - -void *SYM(memcpy)(void *dest, const void *src, size_t n) { - auto *result = memcpy(dest, src, n); - - tryAlternative(dest, _sym_get_parameter_expression(0), SYM(memcpy)); - tryAlternative(src, _sym_get_parameter_expression(1), SYM(memcpy)); - tryAlternative(n, _sym_get_parameter_expression(2), SYM(memcpy)); - - _sym_memcpy(static_cast(dest), static_cast(src), - n); - _sym_set_return_expression(_sym_get_parameter_expression(0)); - return result; -} - -void *SYM(memset)(void *s, int c, size_t n) { - auto *result = memset(s, c, n); - - tryAlternative(s, _sym_get_parameter_expression(0), SYM(memset)); - tryAlternative(n, _sym_get_parameter_expression(2), SYM(memset)); - - _sym_memset(static_cast(s), _sym_get_parameter_expression(1), n); - _sym_set_return_expression(_sym_get_parameter_expression(0)); - return result; -} - -void SYM(bzero)(void *s, size_t n) { - bzero(s, n); - - // No return value, hence no corresponding expression. - _sym_set_return_expression(nullptr); - - tryAlternative(s, _sym_get_parameter_expression(0), SYM(bzero)); - tryAlternative(n, _sym_get_parameter_expression(1), SYM(bzero)); - - // Concretize the memory region, which now is all zeros. - ReadWriteShadow shadow(s, n); - std::fill(shadow.begin(), shadow.end(), nullptr); -} - -void *SYM(memmove)(void *dest, const void *src, size_t n) { - tryAlternative(dest, _sym_get_parameter_expression(0), SYM(memmove)); - tryAlternative(src, _sym_get_parameter_expression(1), SYM(memmove)); - tryAlternative(n, _sym_get_parameter_expression(2), SYM(memmove)); - - auto *result = memmove(dest, src, n); - _sym_memmove(static_cast(dest), static_cast(src), - n); - - _sym_set_return_expression(_sym_get_parameter_expression(0)); - return result; -} - -void SYM(bcopy)(const void *src, void *dest, size_t n) { - tryAlternative(src, _sym_get_parameter_expression(0), SYM(bcopy)); - tryAlternative(dest, _sym_get_parameter_expression(1), SYM(bcopy)); - tryAlternative(n, _sym_get_parameter_expression(2), SYM(bcopy)); - - bcopy(src, dest, n); - - // bcopy is mostly equivalent to memmove, so we can use our symbolic version - // of memmove to copy any symbolic expressions over to the destination. - _sym_memmove(static_cast(dest), static_cast(src), - n); - - // void function, so there is no return value and hence no expression for it. - _sym_set_return_expression(nullptr); -} - -char *SYM(strncpy)(char *dest, const char *src, size_t n) { - tryAlternative(dest, _sym_get_parameter_expression(0), SYM(strncpy)); - tryAlternative(src, _sym_get_parameter_expression(1), SYM(strncpy)); - tryAlternative(n, _sym_get_parameter_expression(2), SYM(strncpy)); - - auto *result = strncpy(dest, src, n); - _sym_set_return_expression(nullptr); - - size_t srcLen = strnlen(src, n); - size_t copied = std::min(n, srcLen); - if (isConcrete(src, copied) && isConcrete(dest, n)) - return result; - - auto srcShadow = ReadOnlyShadow(src, copied); - auto destShadow = ReadWriteShadow(dest, n); - - std::copy(srcShadow.begin(), srcShadow.end(), destShadow.begin()); - if (copied < n) { - ReadWriteShadow destRestShadow(dest + copied, n - copied); - std::fill(destRestShadow.begin(), destRestShadow.end(), nullptr); - } - - return result; -} - -const char *SYM(strchr)(const char *s, int c) { - tryAlternative(s, _sym_get_parameter_expression(0), SYM(strchr)); - tryAlternative(c, _sym_get_parameter_expression(1), SYM(strchr)); - - auto *result = strchr(s, c); - _sym_set_return_expression(nullptr); - - auto *cExpr = _sym_get_parameter_expression(1); - if (isConcrete(s, result != nullptr ? (result - s) : strlen(s)) && - cExpr == nullptr) - return result; - - if (cExpr == nullptr) - cExpr = _sym_build_integer(c, 8); - else - cExpr = _sym_build_trunc(cExpr, 8); - - size_t length = result != nullptr ? (result - s) : strlen(s); - auto shadow = ReadOnlyShadow(s, length); - auto shadowIt = shadow.begin(); - for (size_t i = 0; i < length; i++) { - _sym_push_path_constraint( - _sym_build_not_equal( - (*shadowIt != nullptr) ? *shadowIt : _sym_build_integer(s[i], 8), - cExpr), - /*taken*/ 1, reinterpret_cast(SYM(strchr))); - ++shadowIt; - } - - return result; -} - -int SYM(memcmp)(const void *a, const void *b, size_t n) { - tryAlternative(a, _sym_get_parameter_expression(0), SYM(memcmp)); - tryAlternative(b, _sym_get_parameter_expression(1), SYM(memcmp)); - tryAlternative(n, _sym_get_parameter_expression(2), SYM(memcmp)); - - auto result = memcmp(a, b, n); - _sym_set_return_expression(nullptr); - - if (isConcrete(a, n) && isConcrete(b, n)) - return result; - - auto aShadowIt = ReadOnlyShadow(a, n).begin_non_null(); - auto bShadowIt = ReadOnlyShadow(b, n).begin_non_null(); - auto *allEqual = _sym_build_equal(*aShadowIt, *bShadowIt); - for (size_t i = 1; i < n; i++) { - ++aShadowIt; - ++bShadowIt; - allEqual = - _sym_build_bool_and(allEqual, _sym_build_equal(*aShadowIt, *bShadowIt)); - } - - _sym_push_path_constraint(allEqual, result == 0, - reinterpret_cast(SYM(memcmp))); - return result; -} - -int SYM(bcmp)(const void *a, const void *b, size_t n) { - tryAlternative(a, _sym_get_parameter_expression(0), SYM(bcmp)); - tryAlternative(b, _sym_get_parameter_expression(1), SYM(bcmp)); - tryAlternative(n, _sym_get_parameter_expression(2), SYM(bcmp)); - - auto result = bcmp(a, b, n); - - // bcmp returns zero if the input regions are equal and an unspecified - // non-zero value otherwise. Instead of expressing this symbolically, we - // directly ask the solver for an alternative solution (assuming that the - // result is used for a conditional branch later), and return a concrete - // value. - _sym_set_return_expression(nullptr); - - // The result of the comparison depends on whether the input regions are equal - // byte by byte. Construct the corresponding expression, but only if there is - // at least one symbolic byte in either of the regions; otherwise, the result - // is concrete. - - if (isConcrete(a, n) && isConcrete(b, n)) - return result; - - auto aShadowIt = ReadOnlyShadow(a, n).begin_non_null(); - auto bShadowIt = ReadOnlyShadow(b, n).begin_non_null(); - auto *allEqual = _sym_build_equal(*aShadowIt, *bShadowIt); - for (size_t i = 1; i < n; i++) { - ++aShadowIt; - ++bShadowIt; - allEqual = - _sym_build_bool_and(allEqual, _sym_build_equal(*aShadowIt, *bShadowIt)); - } - - _sym_push_path_constraint(allEqual, result == 0, - reinterpret_cast(SYM(bcmp))); - return result; -} - -uint32_t SYM(ntohl)(uint32_t netlong) { - auto netlongExpr = _sym_get_parameter_expression(0); - auto result = ntohl(netlong); - - if (netlongExpr == nullptr) { - _sym_set_return_expression(nullptr); - return result; - } - -#if __BYTE_ORDER__ == __ORDER_LITTLE_ENDIAN__ - _sym_set_return_expression(_sym_build_bswap(netlongExpr)); -#elif __BYTE_ORDER__ == __ORDER_BIG_ENDIAN__ - _sym_set_return_expression(netlongExpr); -#else -#error Unsupported __BYTE_ORDER__ -#endif - - return result; -} -} diff --git a/runtime/LibcWrappers.h b/runtime/LibcWrappers.h deleted file mode 100644 index 2304a3a0..00000000 --- a/runtime/LibcWrappers.h +++ /dev/null @@ -1,25 +0,0 @@ -// This file is part of the SymCC runtime. -// -// The SymCC runtime is free software: you can redistribute it and/or modify it -// under the terms of the GNU Lesser General Public License as published by the -// Free Software Foundation, either version 3 of the License, or (at your -// option) any later version. -// -// The SymCC runtime 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 Lesser General Public License -// for more details. -// -// You should have received a copy of the GNU Lesser General Public License -// along with the SymCC runtime. If not, see . - -#ifndef LIBCWRAPPERS_H -#define LIBCWRAPPERS_H - -/// Initialize the libc wrappers. -/// -/// The configuration needs to be loaded so that we can apply settings related -/// to symbolic input. -void initLibcWrappers(); - -#endif diff --git a/runtime/RuntimeCommon.cpp b/runtime/RuntimeCommon.cpp deleted file mode 100644 index 127c81de..00000000 --- a/runtime/RuntimeCommon.cpp +++ /dev/null @@ -1,488 +0,0 @@ -// This file is part of the SymCC runtime. -// -// The SymCC runtime is free software: you can redistribute it and/or modify it -// under the terms of the GNU Lesser General Public License as published by the -// Free Software Foundation, either version 3 of the License, or (at your -// option) any later version. -// -// The SymCC runtime 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 Lesser General Public License -// for more details. -// -// You should have received a copy of the GNU Lesser General Public License -// along with SymCC. If not, see . - -#include - -#include -#include -#include -#include -#include -#include -#include - -#include "Config.h" -#include "GarbageCollection.h" -#include "RuntimeCommon.h" -#include "Shadow.h" - -namespace { - -constexpr int kMaxFunctionArguments = 256; - -/// Global storage for function parameters and the return value. -SymExpr g_return_value; -std::array g_function_arguments; -// TODO make thread-local - -SymExpr buildMinSignedInt(uint8_t bits) { - return _sym_build_integer((uint64_t)(1) << (bits - 1), bits); -} - -SymExpr buildMaxSignedInt(uint8_t bits) { - uint64_t mask = ((uint64_t)(1) << bits) - 1; - return _sym_build_integer(((uint64_t)(~0) & mask) >> 1, bits); -} - -SymExpr buildMaxUnsignedInt(uint8_t bits) { - uint64_t mask = ((uint64_t)(1) << bits) - 1; - return _sym_build_integer((uint64_t)(~0) & mask, bits); -} - -/// Construct an expression describing the in-memory representation of the -/// bitcode structure {iN, i1} returned by the intrinsics for arithmetic with -/// overflow (see -/// https://llvm.org/docs/LangRef.html#arithmetic-with-overflow-intrinsics). The -/// overflow parameter is expected to be a symbolic Boolean. -SymExpr buildOverflowResult(SymExpr result_expr, SymExpr overflow, - bool little_endian) { - auto result_bits = _sym_bits_helper(result_expr); - assert(result_bits % 8 == 0 && - "Arithmetic with overflow on integers of invalid length"); - - // When storing {iN, i1} in memory, the compiler would insert padding between - // the two elements, extending the Boolean to the same size as the integer. We - // simulate the same here, taking endianness into account. - - auto result_expr_mem = - little_endian ? _sym_build_bswap(result_expr) : result_expr; - auto overflow_byte = _sym_build_zext(_sym_build_bool_to_bit(overflow), 7); - - // There's no padding if the result is a single byte. - if (result_bits == 8) { - return _sym_concat_helper(result_expr_mem, overflow_byte); - } - - auto padding = _sym_build_zero_bytes(result_bits / 8 - 1); - return _sym_concat_helper(result_expr_mem, - little_endian - ? _sym_concat_helper(overflow_byte, padding) - : _sym_concat_helper(padding, overflow_byte)); -} - -} // namespace - -void _sym_set_return_expression(SymExpr expr) { g_return_value = expr; } - -SymExpr _sym_get_return_expression(void) { - auto *result = g_return_value; - // TODO this is a safeguard that can eventually be removed - g_return_value = nullptr; - return result; -} - -void _sym_set_parameter_expression(uint8_t index, SymExpr expr) { - g_function_arguments[index] = expr; -} - -SymExpr _sym_get_parameter_expression(uint8_t index) { - return g_function_arguments[index]; -} - -void _sym_memcpy(uint8_t *dest, const uint8_t *src, size_t length) { - if (isConcrete(src, length) && isConcrete(dest, length)) - return; - - ReadOnlyShadow srcShadow(src, length); - ReadWriteShadow destShadow(dest, length); - std::copy(srcShadow.begin(), srcShadow.end(), destShadow.begin()); -} - -void _sym_memset(uint8_t *memory, SymExpr value, size_t length) { - if ((value == nullptr) && isConcrete(memory, length)) - return; - - ReadWriteShadow shadow(memory, length); - std::fill(shadow.begin(), shadow.end(), value); -} - -void _sym_memmove(uint8_t *dest, const uint8_t *src, size_t length) { - // Unless both the source and the destination are fully concrete memory - // regions, we need to copy the symbolic expressions over. (In the case where - // only the destination is symbolic, this means making it concrete.) - - if (isConcrete(src, length) && isConcrete(dest, length)) - return; - - ReadOnlyShadow srcShadow(src, length); - ReadWriteShadow destShadow(dest, length); - if (dest > src) - std::copy_backward(srcShadow.begin(), srcShadow.end(), destShadow.end()); - else - std::copy(srcShadow.begin(), srcShadow.end(), destShadow.begin()); -} - -SymExpr _sym_read_memory(uint8_t *addr, size_t length, bool little_endian) { - assert(length && "Invalid query for zero-length memory region"); - -#ifdef DEBUG_RUNTIME - std::cerr << "Reading " << length << " bytes from address " << P(addr) - << std::endl; - dump_known_regions(); -#endif - - // If the entire memory region is concrete, don't create a symbolic expression - // at all. - if (isConcrete(addr, length)) - return nullptr; - - ReadOnlyShadow shadow(addr, length); - return std::accumulate(shadow.begin_non_null(), shadow.end_non_null(), - static_cast(nullptr), - [&](SymExpr result, SymExpr byteExpr) { - if (result == nullptr) - return byteExpr; - - return little_endian - ? _sym_concat_helper(byteExpr, result) - : _sym_concat_helper(result, byteExpr); - }); -} - -void _sym_write_memory(uint8_t *addr, size_t length, SymExpr expr, - bool little_endian) { - assert(length && "Invalid query for zero-length memory region"); - -#ifdef DEBUG_RUNTIME - std::cerr << "Writing " << length << " bytes to address " << P(addr) - << std::endl; - dump_known_regions(); -#endif - - if (expr == nullptr && isConcrete(addr, length)) - return; - - ReadWriteShadow shadow(addr, length); - if (expr == nullptr) { - std::fill(shadow.begin(), shadow.end(), nullptr); - } else { - size_t i = 0; - for (SymExpr &byteShadow : shadow) { - byteShadow = little_endian - ? _sym_extract_helper(expr, 8 * (i + 1) - 1, 8 * i) - : _sym_extract_helper(expr, (length - i) * 8 - 1, - (length - i - 1) * 8); - i++; - } - } -} - -SymExpr _sym_build_extract(SymExpr expr, uint64_t offset, uint64_t length, - bool little_endian) { - size_t totalBits = _sym_bits_helper(expr); - assert((totalBits % 8 == 0) && "Aggregate type contains partial bytes"); - - SymExpr result; - if (little_endian) { - result = _sym_extract_helper(expr, totalBits - offset * 8 - 1, - totalBits - offset * 8 - 8); - for (size_t i = 1; i < length; i++) { - result = _sym_concat_helper( - _sym_extract_helper(expr, totalBits - (offset + i) * 8 - 1, - totalBits - (offset + i + 1) * 8), - result); - } - } else { - result = _sym_extract_helper(expr, totalBits - offset * 8 - 1, - totalBits - (offset + length) * 8); - } - - return result; -} - -SymExpr _sym_build_bswap(SymExpr expr) { - size_t bits = _sym_bits_helper(expr); - assert((bits % 16 == 0) && "bswap is not applicable"); - return _sym_build_extract(expr, 0, bits / 8, true); -} - -SymExpr _sym_build_insert(SymExpr target, SymExpr to_insert, uint64_t offset, - bool little_endian) { - size_t bitsToInsert = _sym_bits_helper(to_insert); - assert((bitsToInsert % 8 == 0) && - "Expression to insert contains partial bytes"); - - SymExpr beforeInsert = - (offset == 0) ? nullptr : _sym_build_extract(target, 0, offset, false); - SymExpr newPiece = (little_endian && bitsToInsert > 8) - ? _sym_build_bswap(to_insert) - : to_insert; - uint64_t afterLen = - (_sym_bits_helper(target) / 8) - offset - (bitsToInsert / 8); - SymExpr afterInsert = - (afterLen == 0) ? nullptr - : _sym_build_extract(target, offset + (bitsToInsert / 8), - afterLen, false); - - SymExpr result = beforeInsert; - if (result == nullptr) { - result = newPiece; - } else { - result = _sym_concat_helper(result, newPiece); - } - - if (afterInsert != nullptr) { - result = _sym_concat_helper(result, afterInsert); - } - - return result; -} - -SymExpr _sym_build_zero_bytes(size_t length) { - auto zero_byte = _sym_build_integer(0, 8); - - auto result = zero_byte; - for (size_t i = 1; i < length; i++) { - result = _sym_concat_helper(result, zero_byte); - } - - return result; -} - -SymExpr _sym_build_sadd_sat(SymExpr a, SymExpr b) { - size_t bits = _sym_bits_helper(a); - SymExpr min = buildMinSignedInt(bits); - SymExpr max = buildMaxSignedInt(bits); - SymExpr add_sext = - _sym_build_add(_sym_build_sext(a, 1), _sym_build_sext(b, 1)); - - return _sym_build_ite( - // If the result is less than the min signed integer... - _sym_build_signed_less_equal(add_sext, _sym_build_sext(min, 1)), - // ... Return the min signed integer - min, - _sym_build_ite( - // Otherwise, if the result is greater than the max signed integer... - _sym_build_signed_greater_equal(add_sext, _sym_build_sext(max, 1)), - // ... Return the max signed integer - max, - // Otherwise, return the addition - _sym_build_add(a, b))); -} - -SymExpr _sym_build_uadd_sat(SymExpr a, SymExpr b) { - size_t bits = _sym_bits_helper(a); - SymExpr max = buildMaxUnsignedInt(bits); - SymExpr add_zext = - _sym_build_add(_sym_build_zext(a, 1), _sym_build_zext(b, 1)); - - return _sym_build_ite( - // If the top bit is set, an overflow has occurred and... - _sym_build_bit_to_bool(_sym_extract_helper(add_zext, bits, bits)), - // ... Return the max unsigned integer - max, - // Otherwise, return the addition - _sym_build_add(a, b)); -} - -SymExpr _sym_build_ssub_sat(SymExpr a, SymExpr b) { - size_t bits = _sym_bits_helper(a); - SymExpr min = buildMinSignedInt(bits); - SymExpr max = buildMaxSignedInt(bits); - - SymExpr sub_sext = - _sym_build_sub(_sym_build_sext(a, 1), _sym_build_sext(b, 1)); - - return _sym_build_ite( - // If the result is less than the min signed integer... - _sym_build_signed_less_equal(sub_sext, _sym_build_sext(min, 1)), - // ... Return the min signed integer - min, - _sym_build_ite( - // Otherwise, if the result is greater than the max signed integer... - _sym_build_signed_greater_equal(sub_sext, _sym_build_sext(max, 1)), - // ... Return the max signed integer - max, - // Otherwise, return the subtraction - _sym_build_sub(a, b))); -} - -SymExpr _sym_build_usub_sat(SymExpr a, SymExpr b) { - size_t bits = _sym_bits_helper(a); - - return _sym_build_ite( - // If `a >= b`, then no overflow occurs and... - _sym_build_unsigned_greater_equal(a, b), - // ... Return the subtraction - _sym_build_sub(a, b), - // Otherwise, saturate at zero - _sym_build_integer(0, bits)); -} - -static SymExpr _sym_build_shift_left_overflow(SymExpr a, SymExpr b) { - return _sym_build_not_equal( - _sym_build_arithmetic_shift_right(_sym_build_shift_left(a, b), b), a); -} - -SymExpr _sym_build_sshl_sat(SymExpr a, SymExpr b) { - size_t bits = _sym_bits_helper(a); - - return _sym_build_ite( - // If an overflow occurred... - _sym_build_shift_left_overflow(a, b), - _sym_build_ite( - // ... And the LHS is negative... - _sym_build_bit_to_bool(_sym_extract_helper(a, bits - 1, bits - 1)), - // ... Return the min signed integer... - buildMinSignedInt(bits), - // ... Otherwise, return the max signed integer - buildMaxSignedInt(bits)), - // Otherwise, return the left shift - _sym_build_shift_left(a, b)); -} - -SymExpr _sym_build_ushl_sat(SymExpr a, SymExpr b) { - size_t bits = _sym_bits_helper(a); - - return _sym_build_ite( - // If an overflow occurred... - _sym_build_shift_left_overflow(a, b), - // ... Return the max unsigned integer - buildMaxUnsignedInt(bits), - // Otherwise, return the left shift - _sym_build_shift_left(a, b)); -} - -SymExpr _sym_build_add_overflow(SymExpr a, SymExpr b, bool is_signed, - bool little_endian) { - size_t bits = _sym_bits_helper(a); - SymExpr overflow = [&]() { - if (is_signed) { - // Check if the additions are different - SymExpr add_sext = - _sym_build_add(_sym_build_sext(a, 1), _sym_build_sext(b, 1)); - return _sym_build_not_equal(add_sext, - _sym_build_sext(_sym_build_add(a, b), 1)); - } else { - // Check if the addition overflowed into the extra bit - SymExpr add_zext = - _sym_build_add(_sym_build_zext(a, 1), _sym_build_zext(b, 1)); - return _sym_build_equal(_sym_extract_helper(add_zext, bits, bits), - _sym_build_true()); - } - }(); - - return buildOverflowResult(_sym_build_add(a, b), overflow, little_endian); -} - -SymExpr _sym_build_sub_overflow(SymExpr a, SymExpr b, bool is_signed, - bool little_endian) { - size_t bits = _sym_bits_helper(a); - SymExpr overflow = [&]() { - if (is_signed) { - // Check if the subtractions are different - SymExpr sub_sext = - _sym_build_sub(_sym_build_sext(a, 1), _sym_build_sext(b, 1)); - return _sym_build_not_equal(sub_sext, - _sym_build_sext(_sym_build_sub(a, b), 1)); - } else { - // Check if the subtraction overflowed into the extra bit - SymExpr sub_zext = - _sym_build_sub(_sym_build_zext(a, 1), _sym_build_zext(b, 1)); - return _sym_build_equal(_sym_extract_helper(sub_zext, bits, bits), - _sym_build_true()); - } - }(); - - return buildOverflowResult(_sym_build_sub(a, b), overflow, little_endian); -} - -SymExpr _sym_build_mul_overflow(SymExpr a, SymExpr b, bool is_signed, - bool little_endian) { - size_t bits = _sym_bits_helper(a); - SymExpr overflow = [&]() { - if (is_signed) { - // Check if the multiplications are different - SymExpr mul_sext = - _sym_build_mul(_sym_build_sext(a, bits), _sym_build_sext(b, bits)); - return _sym_build_not_equal(mul_sext, - _sym_build_sext(_sym_build_mul(a, b), bits)); - } else { - // Check if the multiplication overflowed into the extra bit - SymExpr mul_zext = - _sym_build_mul(_sym_build_zext(a, bits), _sym_build_zext(b, bits)); - return _sym_build_equal( - _sym_extract_helper(mul_zext, 2 * bits - 1, 2 * bits - 1), - _sym_build_true()); - } - }(); - - return buildOverflowResult(_sym_build_mul(a, b), overflow, little_endian); -} - -SymExpr _sym_build_funnel_shift_left(SymExpr a, SymExpr b, SymExpr c) { - size_t bits = _sym_bits_helper(c); - SymExpr concat = _sym_concat_helper(a, b); - SymExpr shift = _sym_build_unsigned_rem(c, _sym_build_integer(bits, bits)); - - return _sym_extract_helper(_sym_build_shift_left(concat, shift), 0, bits); -} - -SymExpr _sym_build_funnel_shift_right(SymExpr a, SymExpr b, SymExpr c) { - size_t bits = _sym_bits_helper(c); - SymExpr concat = _sym_concat_helper(a, b); - SymExpr shift = _sym_build_unsigned_rem(c, _sym_build_integer(bits, bits)); - - return _sym_extract_helper(_sym_build_logical_shift_right(concat, shift), 0, - bits); -} - -SymExpr _sym_build_abs(SymExpr expr) { - size_t bits = _sym_bits_helper(expr); - return _sym_build_ite( - _sym_build_signed_greater_equal(expr, _sym_build_integer(0, bits)), expr, - _sym_build_sub(_sym_build_integer(0, bits), expr)); -} - -void _sym_register_expression_region(SymExpr *start, size_t length) { - registerExpressionRegion({start, length}); -} - -void _sym_make_symbolic(const void *data, size_t byte_length, - size_t input_offset) { - ReadWriteShadow shadow(data, byte_length); - const uint8_t *data_bytes = reinterpret_cast(data); - std::generate(shadow.begin(), shadow.end(), [&, i = 0]() mutable { - return _sym_get_input_byte(input_offset++, data_bytes[i++]); - }); -} - -void symcc_make_symbolic(const void *start, size_t byte_length) { - if (!std::holds_alternative(g_config.input)) - throw std::runtime_error{"Calls to symcc_make_symbolic aren't allowed when " - "SYMCC_MEMORY_INPUT isn't set"}; - - static size_t inputOffset = 0; // track the offset across calls - _sym_make_symbolic(start, byte_length, inputOffset); - inputOffset += byte_length; -} - -SymExpr _sym_build_bit_to_bool(SymExpr expr) { - if (expr == nullptr) - return nullptr; - - return _sym_build_not_equal(expr, - _sym_build_integer(0, _sym_bits_helper(expr))); -} diff --git a/runtime/RuntimeCommon.h b/runtime/RuntimeCommon.h deleted file mode 100644 index 4c05ceb0..00000000 --- a/runtime/RuntimeCommon.h +++ /dev/null @@ -1,237 +0,0 @@ -// Run-time library interface -*- C++ -*- -// -// This header defines the interface of the run-time library. It is not actually -// used anywhere because the compiler pass inserts calls to the library -// functions at the level of LLVM bitcode, but it serves as documentation of the -// intended interface. Unless documented otherwise, functions taking symbolic -// expressions can't handle null values (i.e., they shouldn't be called for -// concrete values); exceptions are made if it's too difficult to check for -// concreteness in bitcode. -// -// Whoever uses this file has to define the type "SymExpr" first; we use it to -// keep this header independent of the back-end implementation. - -// This file is part of the SymCC runtime. -// -// The SymCC runtime is free software: you can redistribute it and/or modify it -// under the terms of the GNU Lesser General Public License as published by the -// Free Software Foundation, either version 3 of the License, or (at your -// option) any later version. -// -// The SymCC runtime 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 Lesser General Public License -// for more details. -// -// You should have received a copy of the GNU Lesser General Public License -// along with the SymCC runtime. If not, see . - -#ifndef RUNTIMECOMMON_H -#define RUNTIMECOMMON_H - -/* Marker for expression parameters which may be null. */ -#define nullable - -#ifdef __cplusplus -#include -#include -extern "C" { -#else -#include -#include -#endif - -/* - * Initialization - */ -void _sym_initialize(void); - -/* - * Construction of simple values - */ -SymExpr _sym_build_integer(uint64_t value, uint8_t bits); -SymExpr _sym_build_integer128(uint64_t high, uint64_t low); -SymExpr _sym_build_integer_from_buffer(void *buffer, unsigned num_bits); -SymExpr _sym_build_float(double value, int is_double); -SymExpr _sym_build_null_pointer(void); -SymExpr _sym_build_true(void); -SymExpr _sym_build_false(void); -SymExpr _sym_build_bool(bool value); - -/* - * Integer arithmetic and shifts - */ -SymExpr _sym_build_neg(SymExpr expr); -SymExpr _sym_build_add(SymExpr a, SymExpr b); -SymExpr _sym_build_sub(SymExpr a, SymExpr b); -SymExpr _sym_build_mul(SymExpr a, SymExpr b); -SymExpr _sym_build_unsigned_div(SymExpr a, SymExpr b); -SymExpr _sym_build_signed_div(SymExpr a, SymExpr b); -SymExpr _sym_build_unsigned_rem(SymExpr a, SymExpr b); -SymExpr _sym_build_signed_rem(SymExpr a, SymExpr b); -SymExpr _sym_build_shift_left(SymExpr a, SymExpr b); -SymExpr _sym_build_logical_shift_right(SymExpr a, SymExpr b); -SymExpr _sym_build_arithmetic_shift_right(SymExpr a, SymExpr b); -SymExpr _sym_build_funnel_shift_left(SymExpr a, SymExpr b, SymExpr c); -SymExpr _sym_build_funnel_shift_right(SymExpr a, SymExpr b, SymExpr c); -SymExpr _sym_build_abs(SymExpr expr); - -/* - * Arithmetic with overflow - */ -SymExpr _sym_build_add_overflow(SymExpr a, SymExpr b, bool is_signed, - bool little_endian); -SymExpr _sym_build_sub_overflow(SymExpr a, SymExpr b, bool is_signed, - bool little_endian); -SymExpr _sym_build_mul_overflow(SymExpr a, SymExpr b, bool is_signed, - bool little_endian); - -/* - * Saturating integer arithmetic and shifts - */ -SymExpr _sym_build_sadd_sat(SymExpr a, SymExpr b); -SymExpr _sym_build_uadd_sat(SymExpr a, SymExpr b); -SymExpr _sym_build_ssub_sat(SymExpr a, SymExpr b); -SymExpr _sym_build_usub_sat(SymExpr a, SymExpr b); -SymExpr _sym_build_sshl_sat(SymExpr a, SymExpr b); -SymExpr _sym_build_ushl_sat(SymExpr a, SymExpr b); - -/* - * Floating-point arithmetic and shifts - */ -SymExpr _sym_build_fp_add(SymExpr a, SymExpr b); -SymExpr _sym_build_fp_sub(SymExpr a, SymExpr b); -SymExpr _sym_build_fp_mul(SymExpr a, SymExpr b); -SymExpr _sym_build_fp_div(SymExpr a, SymExpr b); -SymExpr _sym_build_fp_rem(SymExpr a, SymExpr b); -SymExpr _sym_build_fp_abs(SymExpr a); -SymExpr _sym_build_fp_neg(SymExpr a); - -/* - * Boolean operations - */ -SymExpr _sym_build_not(SymExpr expr); -SymExpr _sym_build_signed_less_than(SymExpr a, SymExpr b); -SymExpr _sym_build_signed_less_equal(SymExpr a, SymExpr b); -SymExpr _sym_build_signed_greater_than(SymExpr a, SymExpr b); -SymExpr _sym_build_signed_greater_equal(SymExpr a, SymExpr b); -SymExpr _sym_build_unsigned_less_than(SymExpr a, SymExpr b); -SymExpr _sym_build_unsigned_less_equal(SymExpr a, SymExpr b); -SymExpr _sym_build_unsigned_greater_than(SymExpr a, SymExpr b); -SymExpr _sym_build_unsigned_greater_equal(SymExpr a, SymExpr b); -SymExpr _sym_build_equal(SymExpr a, SymExpr b); -SymExpr _sym_build_not_equal(SymExpr a, SymExpr b); -SymExpr _sym_build_bool_and(SymExpr a, SymExpr b); -SymExpr _sym_build_and(SymExpr a, SymExpr b); -SymExpr _sym_build_bool_or(SymExpr a, SymExpr b); -SymExpr _sym_build_or(SymExpr a, SymExpr b); -SymExpr _sym_build_bool_xor(SymExpr a, SymExpr b); -SymExpr _sym_build_xor(SymExpr a, SymExpr b); -SymExpr _sym_build_ite(SymExpr cond, SymExpr a, SymExpr b); - -SymExpr _sym_build_float_ordered_greater_than(SymExpr a, SymExpr b); -SymExpr _sym_build_float_ordered_greater_equal(SymExpr a, SymExpr b); -SymExpr _sym_build_float_ordered_less_than(SymExpr a, SymExpr b); -SymExpr _sym_build_float_ordered_less_equal(SymExpr a, SymExpr b); -SymExpr _sym_build_float_ordered_equal(SymExpr a, SymExpr b); -SymExpr _sym_build_float_ordered_not_equal(SymExpr a, SymExpr b); -SymExpr _sym_build_float_ordered(SymExpr a, SymExpr b); -SymExpr _sym_build_float_unordered(SymExpr a, SymExpr b); -SymExpr _sym_build_float_unordered_greater_than(SymExpr a, SymExpr b); -SymExpr _sym_build_float_unordered_greater_equal(SymExpr a, SymExpr b); -SymExpr _sym_build_float_unordered_less_than(SymExpr a, SymExpr b); -SymExpr _sym_build_float_unordered_less_equal(SymExpr a, SymExpr b); -SymExpr _sym_build_float_unordered_equal(SymExpr a, SymExpr b); -SymExpr _sym_build_float_unordered_not_equal(SymExpr a, SymExpr b); - -/* - * Casts - */ -SymExpr _sym_build_sext(nullable SymExpr expr, uint8_t bits); -SymExpr _sym_build_zext(nullable SymExpr expr, uint8_t bits); -SymExpr _sym_build_trunc(nullable SymExpr expr, uint8_t bits); -SymExpr _sym_build_bswap(SymExpr expr); -SymExpr _sym_build_int_to_float(SymExpr value, int is_double, int is_signed); -SymExpr _sym_build_float_to_float(SymExpr expr, int to_double); -SymExpr _sym_build_bits_to_float(SymExpr expr, int to_double); -SymExpr _sym_build_float_to_bits(SymExpr expr); -SymExpr _sym_build_float_to_signed_integer(SymExpr expr, uint8_t bits); -SymExpr _sym_build_float_to_unsigned_integer(SymExpr expr, uint8_t bits); -SymExpr _sym_build_bool_to_bit(nullable SymExpr expr); -SymExpr _sym_build_bit_to_bool(nullable SymExpr expr); - -/* - * Bit-array helpers - */ -SymExpr _sym_concat_helper(SymExpr a, SymExpr b); -SymExpr _sym_extract_helper(SymExpr expr, size_t first_bit, size_t last_bit); -size_t _sym_bits_helper(SymExpr expr); - -/* - * Function-call helpers - */ -void _sym_set_parameter_expression(uint8_t index, nullable SymExpr expr); -SymExpr _sym_get_parameter_expression(uint8_t index); -void _sym_set_return_expression(nullable SymExpr expr); -SymExpr _sym_get_return_expression(void); - -/* - * Constraint handling - */ -void _sym_push_path_constraint(nullable SymExpr constraint, int taken, - uintptr_t site_id); -SymExpr _sym_get_input_byte(size_t offset, uint8_t concrete_value); -void _sym_make_symbolic(const void *data, size_t byte_length, - size_t input_offset); - -/* - * Memory management - */ -SymExpr _sym_read_memory(uint8_t *addr, size_t length, bool little_endian); -void _sym_write_memory(uint8_t *addr, size_t length, nullable SymExpr expr, - bool little_endian); -void _sym_memcpy(uint8_t *dest, const uint8_t *src, size_t length); -void _sym_memset(uint8_t *memory, SymExpr value, size_t length); -void _sym_memmove(uint8_t *dest, const uint8_t *src, size_t length); -SymExpr _sym_build_zero_bytes(size_t length); -SymExpr _sym_build_insert(SymExpr target, SymExpr to_insert, uint64_t offset, - bool little_endian); -SymExpr _sym_build_extract(SymExpr expr, uint64_t offset, uint64_t length, - bool little_endian); - -/* - * Call-stack tracing - */ -void _sym_notify_call(uintptr_t site_id); -void _sym_notify_ret(uintptr_t site_id); -void _sym_notify_basic_block(uintptr_t site_id); - -/* - * Debugging - */ -const char *_sym_expr_to_string(SymExpr expr); // statically allocated -bool _sym_feasible(SymExpr expr); - -/* - * Garbage collection - */ -void _sym_register_expression_region(SymExpr *start, size_t length); -void _sym_collect_garbage(void); - -/* - * User-facing functionality - * - * These are the only functions in the interface that we expect to be called by - * users (i.e., calls to it aren't auto-generated by our compiler pass). - */ -void symcc_make_symbolic(const void *start, size_t byte_length); -typedef void (*TestCaseHandler)(const void *, size_t); -void symcc_set_test_case_handler(TestCaseHandler handler); - -#ifdef __cplusplus -} -#endif - -#undef nullable - -#endif diff --git a/runtime/Shadow.cpp b/runtime/Shadow.cpp deleted file mode 100644 index 2852fad1..00000000 --- a/runtime/Shadow.cpp +++ /dev/null @@ -1,18 +0,0 @@ -// This file is part of the SymCC runtime. -// -// The SymCC runtime is free software: you can redistribute it and/or modify it -// under the terms of the GNU Lesser General Public License as published by the -// Free Software Foundation, either version 3 of the License, or (at your -// option) any later version. -// -// The SymCC runtime 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 Lesser General Public License -// for more details. -// -// You should have received a copy of the GNU Lesser General Public License -// along with SymCC. If not, see . - -#include "Shadow.h" - -std::map g_shadow_pages; diff --git a/runtime/Shadow.h b/runtime/Shadow.h deleted file mode 100644 index fe630bb4..00000000 --- a/runtime/Shadow.h +++ /dev/null @@ -1,227 +0,0 @@ -// This file is part of the SymCC runtime. -// -// The SymCC runtime is free software: you can redistribute it and/or modify it -// under the terms of the GNU Lesser General Public License as published by the -// Free Software Foundation, either version 3 of the License, or (at your -// option) any later version. -// -// The SymCC runtime 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 Lesser General Public License -// for more details. -// -// You should have received a copy of the GNU Lesser General Public License -// along with the SymCC runtime. If not, see . - -#ifndef SHADOW_H -#define SHADOW_H - -#include -#include -#include -#include - -#include - -#include - -// -// This file is dedicated to the management of shadow memory. -// -// We manage shadows at page granularity. Since the shadow for each page is -// malloc'ed and thus at an unpredictable location in memory, we need special -// handling for memory allocations that cross page boundaries. This header -// provides iterators over shadow memory that automatically handle jumps between -// memory pages (and thus shadow regions). They should work with the C++ -// standard library. -// -// We represent shadowed memory as a sequence of 8-bit expressions. The -// iterators therefore expose the shadow in the form of byte expressions. -// - -constexpr uintptr_t kPageSize = 4096; - -/// Compute the corresponding page address. -constexpr uintptr_t pageStart(uintptr_t addr) { - return (addr & ~(kPageSize - 1)); -} - -/// Compute the corresponding offset into the page. -constexpr uintptr_t pageOffset(uintptr_t addr) { - return (addr & (kPageSize - 1)); -} - -/// A mapping from page addresses to the corresponding shadow regions. Each -/// shadow is large enough to hold one expression per byte on the shadowed page. -extern std::map g_shadow_pages; - -/// An iterator that walks over the shadow bytes corresponding to a memory -/// region. If there is no shadow for any given memory address, it just returns -/// null. -class ReadShadowIterator { -public: - explicit ReadShadowIterator(uintptr_t address) - : address_(address), shadow_(getShadow(address)) {} - - // The STL requires iterator types to expose the following type definitions - // (see std::iterator_traits). Before C++17, it was possible to get them by - // deriving from std::iterator, which is just an empty template struct with - // five typedefs. However, std::iterator was deprecated in C++17 and hence its - // use causes a warning in recent compilers. - using iterator_category = std::bidirectional_iterator_tag; - using value_type = SymExpr; - using difference_type = ptrdiff_t; - using pointer = SymExpr *; - using reference = SymExpr &; - - ReadShadowIterator &operator++() { - auto previousAddress = address_++; - if (shadow_ != nullptr) - shadow_++; - if (pageStart(address_) != pageStart(previousAddress)) - shadow_ = getShadow(address_); - return *this; - } - - ReadShadowIterator &operator--() { - auto previousAddress = address_--; - if (shadow_ != nullptr) - shadow_--; - if (pageStart(address_) != pageStart(previousAddress)) - shadow_ = getShadow(address_); - return *this; - } - - SymExpr operator*() { - assert((shadow_ == nullptr || *shadow_ == nullptr || - _sym_bits_helper(*shadow_) == 8) && - "Shadow memory always represents bytes"); - return shadow_ != nullptr ? *shadow_ : nullptr; - } - - bool operator==(const ReadShadowIterator &other) const { - return (address_ == other.address_); - } - - bool operator!=(const ReadShadowIterator &other) const { - return !(*this == other); - } - -protected: - static SymExpr *getShadow(uintptr_t address) { - if (auto shadowPageIt = g_shadow_pages.find(pageStart(address)); - shadowPageIt != g_shadow_pages.end()) - return shadowPageIt->second + pageOffset(address); - - return nullptr; - } - - uintptr_t address_; - SymExpr *shadow_; -}; - -/// Like ReadShadowIterator, but return an expression for the concrete memory -/// value if a region does not have a shadow. -class NonNullReadShadowIterator : public ReadShadowIterator { -public: - explicit NonNullReadShadowIterator(uintptr_t address) - : ReadShadowIterator(address) {} - - SymExpr operator*() { - if (auto *symbolicResult = ReadShadowIterator::operator*()) - return symbolicResult; - - return _sym_build_integer(*reinterpret_cast(address_), 8); - } -}; - -/// An iterator that walks over the shadow corresponding to a memory region and -/// exposes it for modification. If there is no shadow yet, it creates a new -/// one. -class WriteShadowIterator : public ReadShadowIterator { -public: - WriteShadowIterator(uintptr_t address) : ReadShadowIterator(address) { - shadow_ = getOrCreateShadow(address); - } - - WriteShadowIterator &operator++() { - auto previousAddress = address_++; - shadow_++; - if (pageStart(address_) != pageStart(previousAddress)) - shadow_ = getOrCreateShadow(address_); - return *this; - } - - WriteShadowIterator &operator--() { - auto previousAddress = address_--; - shadow_--; - if (pageStart(address_) != pageStart(previousAddress)) - shadow_ = getOrCreateShadow(address_); - return *this; - } - - SymExpr &operator*() { return *shadow_; } - -protected: - static SymExpr *getOrCreateShadow(uintptr_t address) { - if (auto *shadow = getShadow(address)) - return shadow; - - auto *newShadow = - static_cast(malloc(kPageSize * sizeof(SymExpr))); - memset(newShadow, 0, kPageSize * sizeof(SymExpr)); - g_shadow_pages[pageStart(address)] = newShadow; - return newShadow + pageOffset(address); - } -}; - -/// A view on shadow memory that exposes read-only functionality. -struct ReadOnlyShadow { - template - ReadOnlyShadow(T *addr, size_t len) - : address_(reinterpret_cast(addr)), length_(len) {} - - ReadShadowIterator begin() const { return ReadShadowIterator(address_); } - ReadShadowIterator end() const { - return ReadShadowIterator(address_ + length_); - } - - NonNullReadShadowIterator begin_non_null() const { - return NonNullReadShadowIterator(address_); - } - - NonNullReadShadowIterator end_non_null() const { - return NonNullReadShadowIterator(address_ + length_); - } - - uintptr_t address_; - size_t length_; -}; - -/// A view on shadow memory that allows modifications. -template struct ReadWriteShadow { - ReadWriteShadow(T *addr, size_t len) - : address_(reinterpret_cast(addr)), length_(len) {} - - WriteShadowIterator begin() { return WriteShadowIterator(address_); } - WriteShadowIterator end() { return WriteShadowIterator(address_ + length_); } - - uintptr_t address_; - size_t length_; -}; - -/// Check whether the indicated memory range is concrete, i.e., there is no -/// symbolic byte in the entire region. -template bool isConcrete(T *addr, size_t nbytes) { - // Fast path for allocations within one page. - auto byteBuf = reinterpret_cast(addr); - if (pageStart(byteBuf) == pageStart(byteBuf + nbytes) && - !g_shadow_pages.count(pageStart(byteBuf))) - return true; - - ReadOnlyShadow shadow(addr, nbytes); - return std::all_of(shadow.begin(), shadow.end(), - [](SymExpr expr) { return (expr == nullptr); }); -} - -#endif diff --git a/runtime/bindings/README b/runtime/bindings/README deleted file mode 100644 index d36686f4..00000000 --- a/runtime/bindings/README +++ /dev/null @@ -1,9 +0,0 @@ - - - Runtime bindings - - -This directory contains bindings to the user-facing functionality of the runtime -(see runtime/RuntimeCommon.h). The bindings give target programs written in -different languages access to runtime features like in-memory input or custom -test-case handlers. diff --git a/runtime/bindings/ada/README b/runtime/bindings/ada/README deleted file mode 100644 index 312576ac..00000000 --- a/runtime/bindings/ada/README +++ /dev/null @@ -1,36 +0,0 @@ - - - Ada bindings - - -This directory contains Ada bindings for the SymCC runtime. To use them in your -Ada code, you can either point gprbuild here directly (e.g., by setting -GPR_PROJECT_PATH appropriately), or you can install them in the system: - -$ gprbuild -Psymcc -$ gprinstall -Psymcc - -Either way, you'll then be able to include SymCC in your project definition -(i.e., the .gpr file for your project): - - with "symcc"; - -This will let you use the bindings in your Ada code, for example: - - with SymCC; use SymCC; - - -- ... - - -- Register a procedure that receives new program inputs. - SymCC_Set_Test_Case_Handler (My_Handler); - - -- Tell SymCC where to find the input in memory. Note that the variable needs - -- to be declared with the "aliased" keyword. - SymCC_Make_Symbolic (Input'Address, Input'Size / System.Storage_Unit); - - -- Run your code on the input; SymCC will follow the computations - -- symbolically and call My_Handler whenever it produces a new test input. - My_Code_Under_Test (Input); - -See the doc comments in symcc.ads for details, or generate HTML documentation -with "gnatdoc -Psymcc". diff --git a/runtime/bindings/ada/symcc.ads b/runtime/bindings/ada/symcc.ads deleted file mode 100644 index bdda6c41..00000000 --- a/runtime/bindings/ada/symcc.ads +++ /dev/null @@ -1,45 +0,0 @@ --- This file is part of the SymCC runtime. - --- The SymCC runtime is free software: you can redistribute it and/or modify --- it under the terms of the GNU Lesser General Public License as published by --- the Free Software Foundation, either version 3 of the License, or (at your --- option) any later version. - --- The SymCC runtime 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 Lesser General Public --- License for more details. - -with Interfaces.C; -with System; - --- @summary --- Ada bindings to the SymCC runtime API. --- --- @description --- This package provides thin bindings to the user-facing functionality of the --- SymCC runtime (see RuntimeCommon.h). -package SymCC is - - procedure Make_Symbolic - (Address : System.Address; Size : Interfaces.C.size_t) with - Import => True, Convention => C, External_Name => "symcc_make_symbolic"; - -- Mark a memory region as symbolic program input. - -- @param Address The start of the region containing the input data. - -- @param Size The length in bytes of the region. - - type Test_Case_Handler_Callback_Type is - access procedure - (Data_Block : System.Address; Size : Interfaces.C.size_t) with - Convention => C; - -- Type of functions that the runtime can call when it generates new - -- program inputs (see Set_Test_Case_Handler). - - procedure Set_Test_Case_Handler - (Callback : Test_Case_Handler_Callback_Type) with - Import => True, Convention => C, - External_Name => "symcc_set_test_case_handler"; - -- Define a custom handler for new program inputs. - -- @param Callback The procedure to be called for each new input. - -end SymCC; diff --git a/runtime/bindings/ada/symcc.gpr b/runtime/bindings/ada/symcc.gpr deleted file mode 100644 index 31305fc9..00000000 --- a/runtime/bindings/ada/symcc.gpr +++ /dev/null @@ -1,21 +0,0 @@ --- This file is part of the SymCC runtime. - --- The SymCC runtime is free software: you can redistribute it and/or modify --- it under the terms of the GNU Lesser General Public License as published by --- the Free Software Foundation, either version 3 of the License, or (at your --- option) any later version. - --- The SymCC runtime 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 Lesser General Public --- License for more details. - -library project SymCC is - - for Library_Name use "symcc"; - for Library_Dir use "lib"; - - for Languages use ("Ada"); - for Object_Dir use "obj"; - -end SymCC; diff --git a/runtime/qsym_backend/CMakeLists.txt b/runtime/qsym_backend/CMakeLists.txt deleted file mode 100644 index 3df23d26..00000000 --- a/runtime/qsym_backend/CMakeLists.txt +++ /dev/null @@ -1,78 +0,0 @@ -# This file is part of the SymCC runtime. -# -# The SymCC runtime is free software: you can redistribute it and/or modify it -# under the terms of the GNU Lesser General Public License as published by the -# Free Software Foundation, either version 3 of the License, or (at your option) -# any later version. -# -# The SymCC runtime 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 Lesser General Public License -# for more details. -# -# You should have received a copy of the GNU Lesser General Public License along -# with SymCC. If not, see . - -# Build the parts of the Qsym backend that are relevant for us - -set(QSYM_SOURCE_DIR "qsym/qsym/pintool") - -find_package(LLVM REQUIRED CONFIG) -add_definitions(${LLVM_DEFINITIONS}) -include_directories(SYSTEM ${LLVM_INCLUDE_DIRS}) - -# Qsym doesn't work with old versions of Z3 -find_package(Z3 4.5 CONFIG) -if (NOT Z3_FOUND) - if (NOT Z3_TRUST_SYSTEM_VERSION) - message(FATAL_ERROR "Couldn't locate Z3. \ -If you want me to trust that a suitable version is available nonetheless, \ -configure CMake with -DZ3_TRUST_SYSTEM_VERSION=on (see also docs/Configuration.txt).") - else() - if (EXISTS "/usr/include/z3") - set(Z3_CXX_INCLUDE_DIRS "/usr/include/z3") - else() - set(Z3_CXX_INCLUDE_DIRS) - endif() - set(Z3_LIBRARIES "z3") - endif() -endif() - -add_library(SymRuntime SHARED - ${QSYM_SOURCE_DIR}/expr.cpp - ${QSYM_SOURCE_DIR}/expr_builder.cpp - ${QSYM_SOURCE_DIR}/expr_cache.cpp - ${QSYM_SOURCE_DIR}/expr_evaluate.cpp - ${QSYM_SOURCE_DIR}/solver.cpp - ${QSYM_SOURCE_DIR}/dependency.cpp - ${QSYM_SOURCE_DIR}/logging.cpp - ${QSYM_SOURCE_DIR}/afl_trace_map.cpp - ${QSYM_SOURCE_DIR}/allocation.cpp - ${QSYM_SOURCE_DIR}/call_stack_manager.cpp - ${QSYM_SOURCE_DIR}/third_party/llvm/range.cpp - ${QSYM_SOURCE_DIR}/third_party/xxhash/xxhash.cpp - ${SHARED_RUNTIME_SOURCES} - Runtime.cpp) - -target_include_directories(SymRuntime PRIVATE - ${CMAKE_CURRENT_SOURCE_DIR} # for our fake pin.H and Runtime.h - ${CMAKE_CURRENT_SOURCE_DIR}/..) # for common runtime components - -target_include_directories(SymRuntime SYSTEM PRIVATE - ${Z3_CXX_INCLUDE_DIRS} # for Z3 support - ${QSYM_SOURCE_DIR}) - -# We need to get the LLVM support component for llvm::APInt. -llvm_map_components_to_libnames(QSYM_LLVM_DEPS support) - -target_link_libraries(SymRuntime ${Z3_LIBRARIES} ${QSYM_LLVM_DEPS}) - -# We use std::filesystem, which has been added in C++17. Before its official -# inclusion in the standard library, Clang shipped the feature first in -# libc++experimental and later in libc++fs; GCC used to require libstdc++fs. We -# make no attempt to support those older compiler versions, with one exception: -# some current LTS distributions ship a GCC that requires libstdc++fs for -# std::filesystem - we catch this case in order to enable users of such systems -# to build with the default compiler. -find_package(Filesystem COMPONENTS Final Experimental) -target_link_libraries(SymRuntime std::filesystem) diff --git a/runtime/qsym_backend/Runtime.cpp b/runtime/qsym_backend/Runtime.cpp deleted file mode 100644 index 650787bf..00000000 --- a/runtime/qsym_backend/Runtime.cpp +++ /dev/null @@ -1,488 +0,0 @@ -// This file is part of the SymCC runtime. -// -// The SymCC runtime is free software: you can redistribute it and/or modify it -// under the terms of the GNU Lesser General Public License as published by the -// Free Software Foundation, either version 3 of the License, or (at your -// option) any later version. -// -// The SymCC runtime 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 Lesser General Public License -// for more details. -// -// You should have received a copy of the GNU Lesser General Public License -// along with SymCC. If not, see . - -// -// Definitions that we need for the QSYM backend -// - -#include "Runtime.h" -#include "GarbageCollection.h" - -// C++ -#if __has_include() -#define HAVE_FILESYSTEM 1 -#elif __has_include() -#define HAVE_FILESYSTEM 0 -#else -#error "We need either or the older ." -#endif - -#include -#include -#include -#include -#include -#include -#include - -#if HAVE_FILESYSTEM -#include -#else -#include -#endif - -#ifdef DEBUG_RUNTIME -#include -#endif - -// C -#include -#include - -// QSYM -#include -#include -#include -#include - -// LLVM -#include -#include - -// Runtime -#include -#include -#include - -namespace qsym { - -ExprBuilder *g_expr_builder; -Solver *g_solver; -CallStackManager g_call_stack_manager; -z3::context *g_z3_context; - -} // namespace qsym - -namespace { - -/// Indicate whether the runtime has been initialized. -std::atomic_flag g_initialized = ATOMIC_FLAG_INIT; - -/// A mapping of all expressions that we have ever received from QSYM to the -/// corresponding shared pointers on the heap. -/// -/// We can't expect C clients to handle std::shared_ptr, so we maintain a single -/// copy per expression in order to keep the expression alive. The garbage -/// collector decides when to release our shared pointer. -/// -/// std::map seems to perform slightly better than std::unordered_map on our -/// workload. -std::map allocatedExpressions; - -SymExpr registerExpression(const qsym::ExprRef &expr) { - SymExpr rawExpr = expr.get(); - - if (allocatedExpressions.count(rawExpr) == 0) { - // We don't know this expression yet. Create a copy of the shared pointer to - // keep the expression alive. - allocatedExpressions[rawExpr] = expr; - } - - return rawExpr; -} - -/// The user-provided test case handler, if any. -/// -/// If the user doesn't register a handler, we use QSYM's default behavior of -/// writing the test case to a file in the output directory. -TestCaseHandler g_test_case_handler = nullptr; - -/// A QSYM solver that doesn't require the entire input on initialization. -class EnhancedQsymSolver : public qsym::Solver { - // Warning! - // - // Before we can override methods of qsym::Solver, we need to declare them - // virtual because the QSYM code refers to the solver with a pointer of type - // qsym::Solver*; for non-virtual methods, it will always choose the - // implementation of the base class. Beware that making a method virtual adds - // a small performance overhead and requires us to change QSYM code. - // - // Subclassing the QSYM solver is ugly but helps us to avoid making too many - // changes in the QSYM codebase. - -public: - EnhancedQsymSolver() - : qsym::Solver("/dev/null", g_config.outputDir, g_config.aflCoverageMap) { - } - - void pushInputByte(size_t offset, uint8_t value) { - if (inputs_.size() <= offset) - inputs_.resize(offset + 1); - - inputs_[offset] = value; - } - - void saveValues(const std::string &suffix) override { - if (auto handler = g_test_case_handler) { - auto values = getConcreteValues(); - // The test-case handler may be instrumented, so let's call it with - // argument expressions to meet instrumented code's expectations. - // Otherwise, we might end up erroneously using whatever expression was - // last registered for a function parameter. - _sym_set_parameter_expression(0, nullptr); - _sym_set_parameter_expression(1, nullptr); - handler(values.data(), values.size()); - } else { - Solver::saveValues(suffix); - } - } -}; - -EnhancedQsymSolver *g_enhanced_solver; - -} // namespace - -using namespace qsym; - -#if HAVE_FILESYSTEM -namespace fs = std::filesystem; -#else -namespace fs = std::experimental::filesystem; -#endif - -void _sym_initialize(void) { - if (g_initialized.test_and_set()) - return; - - loadConfig(); - initLibcWrappers(); - std::cerr << "This is SymCC running with the QSYM backend" << std::endl; - if (std::holds_alternative(g_config.input)) { - std::cerr - << "Performing fully concrete execution (i.e., without symbolic input)" - << std::endl; - return; - } - - // Check the output directory - if (!fs::exists(g_config.outputDir) || - !fs::is_directory(g_config.outputDir)) { - std::cerr << "Error: the output directory " << g_config.outputDir - << " (configurable via SYMCC_OUTPUT_DIR) does not exist." - << std::endl; - exit(-1); - } - - g_z3_context = new z3::context{}; - g_enhanced_solver = new EnhancedQsymSolver{}; - g_solver = g_enhanced_solver; // for QSYM-internal use - g_expr_builder = g_config.pruning ? PruneExprBuilder::create() - : SymbolicExprBuilder::create(); -} - -SymExpr _sym_build_integer(uint64_t value, uint8_t bits) { - // QSYM's API takes uintptr_t, so we need to be careful when compiling for - // 32-bit systems: the compiler would helpfully truncate our uint64_t to fit - // into 32 bits. - if constexpr (sizeof(uint64_t) == sizeof(uintptr_t)) { - // 64-bit case: all good. - return registerExpression(g_expr_builder->createConstant(value, bits)); - } else { - // 32-bit case: use the regular API if possible, otherwise create an - // llvm::APInt. - if (uintptr_t value32 = value; value32 == value) - return registerExpression(g_expr_builder->createConstant(value32, bits)); - - return registerExpression( - g_expr_builder->createConstant({64, value}, bits)); - } -} - -SymExpr _sym_build_integer128(uint64_t high, uint64_t low) { - std::array words = {low, high}; - return registerExpression(g_expr_builder->createConstant({128, words}, 128)); -} - -SymExpr _sym_build_integer_from_buffer(void *buffer, unsigned num_bits) { - assert(num_bits % 64 == 0); - return registerExpression(g_expr_builder->createConstant( - {num_bits, num_bits / 64, (uint64_t *)buffer}, num_bits)); -} - -SymExpr _sym_build_null_pointer() { - return registerExpression( - g_expr_builder->createConstant(0, sizeof(uintptr_t) * 8)); -} - -SymExpr _sym_build_true() { - return registerExpression(g_expr_builder->createTrue()); -} - -SymExpr _sym_build_false() { - return registerExpression(g_expr_builder->createFalse()); -} - -SymExpr _sym_build_bool(bool value) { - return registerExpression(g_expr_builder->createBool(value)); -} - -#define DEF_BINARY_EXPR_BUILDER(name, qsymName) \ - SymExpr _sym_build_##name(SymExpr a, SymExpr b) { \ - return registerExpression(g_expr_builder->create##qsymName( \ - allocatedExpressions.at(a), allocatedExpressions.at(b))); \ - } - -DEF_BINARY_EXPR_BUILDER(add, Add) -DEF_BINARY_EXPR_BUILDER(sub, Sub) -DEF_BINARY_EXPR_BUILDER(mul, Mul) -DEF_BINARY_EXPR_BUILDER(unsigned_div, UDiv) -DEF_BINARY_EXPR_BUILDER(signed_div, SDiv) -DEF_BINARY_EXPR_BUILDER(unsigned_rem, URem) -DEF_BINARY_EXPR_BUILDER(signed_rem, SRem) - -DEF_BINARY_EXPR_BUILDER(shift_left, Shl) -DEF_BINARY_EXPR_BUILDER(logical_shift_right, LShr) -DEF_BINARY_EXPR_BUILDER(arithmetic_shift_right, AShr) - -DEF_BINARY_EXPR_BUILDER(signed_less_than, Slt) -DEF_BINARY_EXPR_BUILDER(signed_less_equal, Sle) -DEF_BINARY_EXPR_BUILDER(signed_greater_than, Sgt) -DEF_BINARY_EXPR_BUILDER(signed_greater_equal, Sge) -DEF_BINARY_EXPR_BUILDER(unsigned_less_than, Ult) -DEF_BINARY_EXPR_BUILDER(unsigned_less_equal, Ule) -DEF_BINARY_EXPR_BUILDER(unsigned_greater_than, Ugt) -DEF_BINARY_EXPR_BUILDER(unsigned_greater_equal, Uge) -DEF_BINARY_EXPR_BUILDER(equal, Equal) -DEF_BINARY_EXPR_BUILDER(not_equal, Distinct) - -DEF_BINARY_EXPR_BUILDER(bool_and, LAnd) -DEF_BINARY_EXPR_BUILDER(and, And) -DEF_BINARY_EXPR_BUILDER(bool_or, LOr) -DEF_BINARY_EXPR_BUILDER(or, Or) -DEF_BINARY_EXPR_BUILDER(bool_xor, Distinct) -DEF_BINARY_EXPR_BUILDER(xor, Xor) - -#undef DEF_BINARY_EXPR_BUILDER - -SymExpr _sym_build_neg(SymExpr expr) { - return registerExpression( - g_expr_builder->createNeg(allocatedExpressions.at(expr))); -} - -SymExpr _sym_build_not(SymExpr expr) { - return registerExpression( - g_expr_builder->createNot(allocatedExpressions.at(expr))); -} - -SymExpr _sym_build_ite(SymExpr cond, SymExpr a, SymExpr b) { - return registerExpression(g_expr_builder->createIte( - allocatedExpressions.at(cond), allocatedExpressions.at(a), - allocatedExpressions.at(b))); -} - -SymExpr _sym_build_sext(SymExpr expr, uint8_t bits) { - if (expr == nullptr) - return nullptr; - - return registerExpression(g_expr_builder->createSExt( - allocatedExpressions.at(expr), bits + expr->bits())); -} - -SymExpr _sym_build_zext(SymExpr expr, uint8_t bits) { - if (expr == nullptr) - return nullptr; - - return registerExpression(g_expr_builder->createZExt( - allocatedExpressions.at(expr), bits + expr->bits())); -} - -SymExpr _sym_build_trunc(SymExpr expr, uint8_t bits) { - if (expr == nullptr) - return nullptr; - - return registerExpression( - g_expr_builder->createTrunc(allocatedExpressions.at(expr), bits)); -} - -void _sym_push_path_constraint(SymExpr constraint, int taken, - uintptr_t site_id) { - if (constraint == nullptr) - return; - - g_solver->addJcc(allocatedExpressions.at(constraint), taken != 0, site_id); -} - -SymExpr _sym_get_input_byte(size_t offset, uint8_t value) { - g_enhanced_solver->pushInputByte(offset, value); - return registerExpression(g_expr_builder->createRead(offset)); -} - -SymExpr _sym_concat_helper(SymExpr a, SymExpr b) { - return registerExpression(g_expr_builder->createConcat( - allocatedExpressions.at(a), allocatedExpressions.at(b))); -} - -SymExpr _sym_extract_helper(SymExpr expr, size_t first_bit, size_t last_bit) { - return registerExpression(g_expr_builder->createExtract( - allocatedExpressions.at(expr), last_bit, first_bit - last_bit + 1)); -} - -size_t _sym_bits_helper(SymExpr expr) { return expr->bits(); } - -SymExpr _sym_build_bool_to_bit(SymExpr expr) { - if (expr == nullptr) - return nullptr; - - return registerExpression( - g_expr_builder->boolToBit(allocatedExpressions.at(expr), 1)); -} - -// -// Floating-point operations (unsupported in QSYM) -// - -// Even if we don't generally support operations on floats in this backend, we -// need dummy implementations of a few functions to help the parts of the -// instrumentation that deal with structures; if structs contain floats, the -// instrumentation expects to be able to create bit-vector expressions for -// them. - -SymExpr _sym_build_float(double, int is_double) { - // We create an all-zeros bit vector, mainly to capture the length of the - // value. This is compatible with our dummy implementation of - // _sym_build_float_to_bits. - return registerExpression( - g_expr_builder->createConstant(0, is_double ? 64 : 32)); -} - -SymExpr _sym_build_float_to_bits(SymExpr expr) { return expr; } - -#define UNSUPPORTED(prototype) \ - prototype { return nullptr; } - -UNSUPPORTED(SymExpr _sym_build_fp_add(SymExpr, SymExpr)) -UNSUPPORTED(SymExpr _sym_build_fp_sub(SymExpr, SymExpr)) -UNSUPPORTED(SymExpr _sym_build_fp_mul(SymExpr, SymExpr)) -UNSUPPORTED(SymExpr _sym_build_fp_div(SymExpr, SymExpr)) -UNSUPPORTED(SymExpr _sym_build_fp_rem(SymExpr, SymExpr)) -UNSUPPORTED(SymExpr _sym_build_fp_abs(SymExpr)) -UNSUPPORTED(SymExpr _sym_build_fp_neg(SymExpr)) -UNSUPPORTED(SymExpr _sym_build_float_ordered_greater_than(SymExpr, SymExpr)) -UNSUPPORTED(SymExpr _sym_build_float_ordered_greater_equal(SymExpr, SymExpr)) -UNSUPPORTED(SymExpr _sym_build_float_ordered_less_than(SymExpr, SymExpr)) -UNSUPPORTED(SymExpr _sym_build_float_ordered_less_equal(SymExpr, SymExpr)) -UNSUPPORTED(SymExpr _sym_build_float_ordered_equal(SymExpr, SymExpr)) -UNSUPPORTED(SymExpr _sym_build_float_ordered_not_equal(SymExpr, SymExpr)) -UNSUPPORTED(SymExpr _sym_build_float_ordered(SymExpr, SymExpr)) -UNSUPPORTED(SymExpr _sym_build_float_unordered(SymExpr, SymExpr)) -UNSUPPORTED(SymExpr _sym_build_float_unordered_greater_than(SymExpr, SymExpr)) -UNSUPPORTED(SymExpr _sym_build_float_unordered_greater_equal(SymExpr, SymExpr)) -UNSUPPORTED(SymExpr _sym_build_float_unordered_less_than(SymExpr, SymExpr)) -UNSUPPORTED(SymExpr _sym_build_float_unordered_less_equal(SymExpr, SymExpr)) -UNSUPPORTED(SymExpr _sym_build_float_unordered_equal(SymExpr, SymExpr)) -UNSUPPORTED(SymExpr _sym_build_float_unordered_not_equal(SymExpr, SymExpr)) -UNSUPPORTED(SymExpr _sym_build_int_to_float(SymExpr, int, int)) -UNSUPPORTED(SymExpr _sym_build_float_to_float(SymExpr, int)) -UNSUPPORTED(SymExpr _sym_build_bits_to_float(SymExpr, int)) -UNSUPPORTED(SymExpr _sym_build_float_to_signed_integer(SymExpr, uint8_t)) -UNSUPPORTED(SymExpr _sym_build_float_to_unsigned_integer(SymExpr, uint8_t)) - -#undef UNSUPPORTED -#undef H - -// -// Call-stack tracing -// - -void _sym_notify_call(uintptr_t site_id) { - g_call_stack_manager.visitCall(site_id); -} - -void _sym_notify_ret(uintptr_t site_id) { - g_call_stack_manager.visitRet(site_id); -} - -void _sym_notify_basic_block(uintptr_t site_id) { - g_call_stack_manager.visitBasicBlock(site_id); -} - -// -// Debugging -// - -const char *_sym_expr_to_string(SymExpr expr) { - static char buffer[4096]; - - auto expr_string = expr->toString(); - auto copied = expr_string.copy( - buffer, std::min(expr_string.length(), sizeof(buffer) - 1)); - buffer[copied] = '\0'; - - return buffer; -} - -bool _sym_feasible(SymExpr expr) { - expr->simplify(); - - g_solver->push(); - g_solver->add(expr->toZ3Expr()); - bool feasible = (g_solver->check() == z3::sat); - g_solver->pop(); - - return feasible; -} - -// -// Garbage collection -// - -void _sym_collect_garbage() { - if (allocatedExpressions.size() < g_config.garbageCollectionThreshold) - return; - -#ifdef DEBUG_RUNTIME - auto start = std::chrono::high_resolution_clock::now(); -#endif - - auto reachableExpressions = collectReachableExpressions(); - for (auto expr_it = allocatedExpressions.begin(); - expr_it != allocatedExpressions.end();) { - if (reachableExpressions.count(expr_it->first) == 0) { - expr_it = allocatedExpressions.erase(expr_it); - } else { - ++expr_it; - } - } - -#ifdef DEBUG_RUNTIME - auto end = std::chrono::high_resolution_clock::now(); - - std::cerr << "After garbage collection: " << allocatedExpressions.size() - << " expressions remain" << std::endl - << "\t(collection took " - << std::chrono::duration_cast(end - - start) - .count() - << " milliseconds)" << std::endl; -#endif -} - -// -// Test-case handling -// - -void symcc_set_test_case_handler(TestCaseHandler handler) { - g_test_case_handler = handler; -} diff --git a/runtime/qsym_backend/Runtime.h b/runtime/qsym_backend/Runtime.h deleted file mode 100644 index 8f19d2af..00000000 --- a/runtime/qsym_backend/Runtime.h +++ /dev/null @@ -1,24 +0,0 @@ -// This file is part of the SymCC runtime. -// -// The SymCC runtime is free software: you can redistribute it and/or modify it -// under the terms of the GNU Lesser General Public License as published by the -// Free Software Foundation, either version 3 of the License, or (at your -// option) any later version. -// -// The SymCC runtime 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 Lesser General Public License -// for more details. -// -// You should have received a copy of the GNU Lesser General Public License -// along with the SymCC runtime. If not, see . - -#ifndef RUNTIME_H -#define RUNTIME_H - -#include "expr.h" - -typedef qsym::Expr *SymExpr; -#include - -#endif diff --git a/runtime/qsym_backend/pin.H b/runtime/qsym_backend/pin.H deleted file mode 100644 index 083d79a8..00000000 --- a/runtime/qsym_backend/pin.H +++ /dev/null @@ -1,48 +0,0 @@ -// This file is part of the SymCC runtime. -// -// The SymCC runtime is free software: you can redistribute it and/or modify it -// under the terms of the GNU Lesser General Public License as published by the -// Free Software Foundation, either version 3 of the License, or (at your -// option) any later version. -// -// The SymCC runtime 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 Lesser General Public License -// for more details. -// -// You should have received a copy of the GNU Lesser General Public License -// along with the SymCC runtime. If not, see . - -#ifndef PIN_H -#define PIN_H - -// -// This file provides mocks for everything that would normally be included from -// Pin, so that we don't have to change all the Qsym code. -// - -#include -#include -#include - -using namespace std; - -typedef uint8_t UINT8; -typedef unsigned int USIZE; -typedef unsigned int UINT; -typedef int INT; -typedef int32_t INT32; -typedef uint32_t UINT32; -typedef uint64_t __uint64; -typedef uintptr_t ADDRINT; - -/// Return the hex representation of a number. -template string hexstr(T arg) { - stringstream stream; - stream << hex << arg; - return stream.str(); -} - -#define decstr(x) to_string(x) - -#endif diff --git a/runtime/qsym_backend/qsym b/runtime/qsym_backend/qsym deleted file mode 160000 index ccd2f41f..00000000 --- a/runtime/qsym_backend/qsym +++ /dev/null @@ -1 +0,0 @@ -Subproject commit ccd2f41f2efb1b0517b83458c181e060497fa589 diff --git a/runtime/simple_backend/CMakeLists.txt b/runtime/simple_backend/CMakeLists.txt deleted file mode 100644 index 64822050..00000000 --- a/runtime/simple_backend/CMakeLists.txt +++ /dev/null @@ -1,43 +0,0 @@ -# This file is part of the SymCC runtime. -# -# The SymCC runtime is free software: you can redistribute it and/or modify it -# under the terms of the GNU Lesser General Public License as published by the -# Free Software Foundation, either version 3 of the License, or (at your option) -# any later version. -# -# The SymCC runtime 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 Lesser General Public License -# for more details. -# -# You should have received a copy of the GNU Lesser General Public License along -# with SymCC. If not, see . - -find_package(Z3 4 CONFIG) -if (NOT Z3_FOUND) - if (NOT Z3_TRUST_SYSTEM_VERSION) - message(FATAL_ERROR "Couldn't locate Z3. \ -If you want me to trust that a suitable version is available nonetheless, \ -configure CMake with -DZ3_TRUST_SYSTEM_VERSION=on (see also docs/Configuration.txt).") - else() - if (EXISTS "/usr/include/z3") - set(Z3_C_INCLUDE_DIRS "/usr/include/z3") - else() - set(Z3_C_INCLUDE_DIRS) - endif() - set(Z3_LIBRARIES "z3") - endif() -endif() - -add_library(SymRuntime SHARED - ${SHARED_RUNTIME_SOURCES} - Runtime.cpp) - -target_link_libraries(SymRuntime ${Z3_LIBRARIES}) - -target_include_directories(SymRuntime PRIVATE - ${CMAKE_CURRENT_SOURCE_DIR} - ${CMAKE_CURRENT_SOURCE_DIR}/.. - ${Z3_C_INCLUDE_DIRS}) - -set_target_properties(SymRuntime PROPERTIES COMPILE_FLAGS "-Werror -Wno-error=deprecated-declarations") diff --git a/runtime/simple_backend/Runtime.cpp b/runtime/simple_backend/Runtime.cpp deleted file mode 100644 index 53ca28cd..00000000 --- a/runtime/simple_backend/Runtime.cpp +++ /dev/null @@ -1,574 +0,0 @@ -// This file is part of the SymCC runtime. -// -// The SymCC runtime is free software: you can redistribute it and/or modify it -// under the terms of the GNU Lesser General Public License as published by the -// Free Software Foundation, either version 3 of the License, or (at your -// option) any later version. -// -// The SymCC runtime 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 Lesser General Public License -// for more details. -// -// You should have received a copy of the GNU Lesser General Public License -// along with the SymCC runtime. If not, see . - -#include - -#include -#include -#include -#include -#include -#include -#include -#include - -#ifndef NDEBUG -#include -#endif - -#include "Config.h" -#include "GarbageCollection.h" -#include "LibcWrappers.h" -#include "Shadow.h" - -#ifndef NDEBUG -// Helper to print pointers properly. -#define P(ptr) reinterpret_cast(ptr) -#endif - -#define FSORT(is_double) \ - ((is_double) ? Z3_mk_fpa_sort_double(g_context) \ - : Z3_mk_fpa_sort_single(g_context)) - -/* TODO Eventually we'll want to inline as much of this as possible. I'm keeping - it in C for now because that makes it easier to experiment with new features, - but I expect that a lot of the functions will stay so simple that we can - generate the corresponding bitcode directly in the compiler pass. */ - -namespace { - -/// Indicate whether the runtime has been initialized. -std::atomic_flag g_initialized = ATOMIC_FLAG_INIT; - -/// The global Z3 context. -Z3_context g_context; - -/// The global floating-point rounding mode. -Z3_ast g_rounding_mode; - -/// The global Z3 solver. -Z3_solver g_solver; // TODO make thread-local - -// Some global constants for efficiency. -Z3_ast g_null_pointer, g_true, g_false; - -FILE *g_log = stderr; - -#ifndef NDEBUG -[[maybe_unused]] void dump_known_regions() { - std::cerr << "Known regions:" << std::endl; - for (const auto &[page, shadow] : g_shadow_pages) { - std::cerr << " " << P(page) << " shadowed by " << P(shadow) << std::endl; - } -} - -void handle_z3_error(Z3_context c [[maybe_unused]], Z3_error_code e) { - assert(c == g_context && "Z3 error in unknown context"); - std::cerr << Z3_get_error_msg(g_context, e) << std::endl; - assert(!"Z3 error"); -} -#endif - -SymExpr build_variable(const char *name, uint8_t bits) { - Z3_symbol sym = Z3_mk_string_symbol(g_context, name); - auto *sort = Z3_mk_bv_sort(g_context, bits); - Z3_inc_ref(g_context, (Z3_ast)sort); - Z3_ast result = Z3_mk_const(g_context, sym, sort); - Z3_inc_ref(g_context, result); - Z3_dec_ref(g_context, (Z3_ast)sort); - return result; -} - -/// The set of all expressions we have ever passed to client code. -std::set allocatedExpressions; - -SymExpr registerExpression(SymExpr expr) { - if (allocatedExpressions.count(expr) == 0) { - // We don't know this expression yet. Record it and increase the reference - // counter. - allocatedExpressions.insert(expr); - Z3_inc_ref(g_context, expr); - } - - return expr; -} - -} // namespace - -void _sym_initialize(void) { - if (g_initialized.test_and_set()) - return; - -#ifndef NDEBUG - std::cerr << "Initializing symbolic runtime" << std::endl; -#endif - - loadConfig(); - initLibcWrappers(); - std::cerr << "This is SymCC running with the simple backend" << std::endl - << "For anything but debugging SymCC itself, you will want to use " - "the QSYM backend instead (see README.md for build instructions)" - << std::endl; - - Z3_config cfg; - - cfg = Z3_mk_config(); - Z3_set_param_value(cfg, "model", "true"); - Z3_set_param_value(cfg, "timeout", "10000"); // milliseconds - g_context = Z3_mk_context_rc(cfg); - Z3_del_config(cfg); - -#ifndef NDEBUG - Z3_set_error_handler(g_context, handle_z3_error); -#endif - - g_rounding_mode = Z3_mk_fpa_round_nearest_ties_to_even(g_context); - Z3_inc_ref(g_context, g_rounding_mode); - - g_solver = Z3_mk_solver(g_context); - Z3_solver_inc_ref(g_context, g_solver); - - auto *pointerSort = Z3_mk_bv_sort(g_context, 8 * sizeof(void *)); - Z3_inc_ref(g_context, (Z3_ast)pointerSort); - g_null_pointer = Z3_mk_int(g_context, 0, pointerSort); - Z3_inc_ref(g_context, g_null_pointer); - Z3_dec_ref(g_context, (Z3_ast)pointerSort); - g_true = Z3_mk_true(g_context); - Z3_inc_ref(g_context, g_true); - g_false = Z3_mk_false(g_context); - Z3_inc_ref(g_context, g_false); - - if (g_config.logFile.empty()) { - g_log = stderr; - } else { - g_log = fopen(g_config.logFile.c_str(), "w"); - } -} - -Z3_ast _sym_build_integer(uint64_t value, uint8_t bits) { - auto *sort = Z3_mk_bv_sort(g_context, bits); - Z3_inc_ref(g_context, (Z3_ast)sort); - auto *result = - registerExpression(Z3_mk_unsigned_int64(g_context, value, sort)); - Z3_dec_ref(g_context, (Z3_ast)sort); - return result; -} - -Z3_ast _sym_build_integer128(uint64_t high, uint64_t low) { - return registerExpression(Z3_mk_concat( - g_context, _sym_build_integer(high, 64), _sym_build_integer(low, 64))); -} - -Z3_ast _sym_build_float(double value, int is_double) { - auto *sort = FSORT(is_double); - Z3_inc_ref(g_context, (Z3_ast)sort); - auto *result = - registerExpression(Z3_mk_fpa_numeral_double(g_context, value, sort)); - Z3_dec_ref(g_context, (Z3_ast)sort); - return result; -} - -Z3_ast _sym_get_input_byte(size_t offset, uint8_t) { - static std::vector stdinBytes; - - if (offset < stdinBytes.size()) - return stdinBytes[offset]; - - auto varName = "stdin" + std::to_string(stdinBytes.size()); - auto *var = build_variable(varName.c_str(), 8); - - stdinBytes.resize(offset); - stdinBytes.push_back(var); - - return var; -} - -Z3_ast _sym_build_null_pointer(void) { return g_null_pointer; } -Z3_ast _sym_build_true(void) { return g_true; } -Z3_ast _sym_build_false(void) { return g_false; } -Z3_ast _sym_build_bool(bool value) { return value ? g_true : g_false; } - -Z3_ast _sym_build_neg(Z3_ast expr) { - return registerExpression(Z3_mk_bvneg(g_context, expr)); -} - -#define DEF_BINARY_EXPR_BUILDER(name, z3_name) \ - SymExpr _sym_build_##name(SymExpr a, SymExpr b) { \ - return registerExpression(Z3_mk_##z3_name(g_context, a, b)); \ - } - -DEF_BINARY_EXPR_BUILDER(add, bvadd) -DEF_BINARY_EXPR_BUILDER(sub, bvsub) -DEF_BINARY_EXPR_BUILDER(mul, bvmul) -DEF_BINARY_EXPR_BUILDER(unsigned_div, bvudiv) -DEF_BINARY_EXPR_BUILDER(signed_div, bvsdiv) -DEF_BINARY_EXPR_BUILDER(unsigned_rem, bvurem) -DEF_BINARY_EXPR_BUILDER(signed_rem, bvsrem) -DEF_BINARY_EXPR_BUILDER(shift_left, bvshl) -DEF_BINARY_EXPR_BUILDER(logical_shift_right, bvlshr) -DEF_BINARY_EXPR_BUILDER(arithmetic_shift_right, bvashr) - -DEF_BINARY_EXPR_BUILDER(signed_less_than, bvslt) -DEF_BINARY_EXPR_BUILDER(signed_less_equal, bvsle) -DEF_BINARY_EXPR_BUILDER(signed_greater_than, bvsgt) -DEF_BINARY_EXPR_BUILDER(signed_greater_equal, bvsge) -DEF_BINARY_EXPR_BUILDER(unsigned_less_than, bvult) -DEF_BINARY_EXPR_BUILDER(unsigned_less_equal, bvule) -DEF_BINARY_EXPR_BUILDER(unsigned_greater_than, bvugt) -DEF_BINARY_EXPR_BUILDER(unsigned_greater_equal, bvuge) -DEF_BINARY_EXPR_BUILDER(equal, eq) - -DEF_BINARY_EXPR_BUILDER(and, bvand) -DEF_BINARY_EXPR_BUILDER(or, bvor) -DEF_BINARY_EXPR_BUILDER(bool_xor, xor) -DEF_BINARY_EXPR_BUILDER(xor, bvxor) - -DEF_BINARY_EXPR_BUILDER(float_ordered_greater_than, fpa_gt) -DEF_BINARY_EXPR_BUILDER(float_ordered_greater_equal, fpa_geq) -DEF_BINARY_EXPR_BUILDER(float_ordered_less_than, fpa_lt) -DEF_BINARY_EXPR_BUILDER(float_ordered_less_equal, fpa_leq) -DEF_BINARY_EXPR_BUILDER(float_ordered_equal, fpa_eq) - -#undef DEF_BINARY_EXPR_BUILDER - -Z3_ast _sym_build_ite(Z3_ast cond, Z3_ast a, Z3_ast b) { - return registerExpression(Z3_mk_ite(g_context, cond, a, b)); -} - -Z3_ast _sym_build_fp_add(Z3_ast a, Z3_ast b) { - return registerExpression(Z3_mk_fpa_add(g_context, g_rounding_mode, a, b)); -} - -Z3_ast _sym_build_fp_sub(Z3_ast a, Z3_ast b) { - return registerExpression(Z3_mk_fpa_sub(g_context, g_rounding_mode, a, b)); -} - -Z3_ast _sym_build_fp_mul(Z3_ast a, Z3_ast b) { - return registerExpression(Z3_mk_fpa_mul(g_context, g_rounding_mode, a, b)); -} - -Z3_ast _sym_build_fp_div(Z3_ast a, Z3_ast b) { - return registerExpression(Z3_mk_fpa_div(g_context, g_rounding_mode, a, b)); -} - -Z3_ast _sym_build_fp_rem(Z3_ast a, Z3_ast b) { - return registerExpression(Z3_mk_fpa_rem(g_context, a, b)); -} - -Z3_ast _sym_build_fp_abs(Z3_ast a) { - return registerExpression(Z3_mk_fpa_abs(g_context, a)); -} - -Z3_ast _sym_build_fp_neg(Z3_ast a) { - return registerExpression(Z3_mk_fpa_neg(g_context, a)); -} - -Z3_ast _sym_build_not(Z3_ast expr) { - return registerExpression(Z3_mk_bvnot(g_context, expr)); -} - -Z3_ast _sym_build_not_equal(Z3_ast a, Z3_ast b) { - return registerExpression(Z3_mk_not(g_context, Z3_mk_eq(g_context, a, b))); -} - -Z3_ast _sym_build_bool_and(Z3_ast a, Z3_ast b) { - Z3_ast operands[] = {a, b}; - return registerExpression(Z3_mk_and(g_context, 2, operands)); -} - -Z3_ast _sym_build_bool_or(Z3_ast a, Z3_ast b) { - Z3_ast operands[] = {a, b}; - return registerExpression(Z3_mk_or(g_context, 2, operands)); -} - -Z3_ast _sym_build_float_ordered_not_equal(Z3_ast a, Z3_ast b) { - return registerExpression( - Z3_mk_not(g_context, _sym_build_float_ordered_equal(a, b))); -} - -Z3_ast _sym_build_float_ordered(Z3_ast a, Z3_ast b) { - return registerExpression( - Z3_mk_not(g_context, _sym_build_float_unordered(a, b))); -} - -Z3_ast _sym_build_float_unordered(Z3_ast a, Z3_ast b) { - Z3_ast checks[2]; - checks[0] = Z3_mk_fpa_is_nan(g_context, a); - checks[1] = Z3_mk_fpa_is_nan(g_context, b); - return registerExpression(Z3_mk_or(g_context, 2, checks)); -} - -Z3_ast _sym_build_float_unordered_greater_than(Z3_ast a, Z3_ast b) { - Z3_ast checks[3]; - checks[0] = Z3_mk_fpa_is_nan(g_context, a); - checks[1] = Z3_mk_fpa_is_nan(g_context, b); - checks[2] = _sym_build_float_ordered_greater_than(a, b); - return registerExpression(Z3_mk_or(g_context, 2, checks)); -} - -Z3_ast _sym_build_float_unordered_greater_equal(Z3_ast a, Z3_ast b) { - Z3_ast checks[3]; - checks[0] = Z3_mk_fpa_is_nan(g_context, a); - checks[1] = Z3_mk_fpa_is_nan(g_context, b); - checks[2] = _sym_build_float_ordered_greater_equal(a, b); - return registerExpression(Z3_mk_or(g_context, 2, checks)); -} - -Z3_ast _sym_build_float_unordered_less_than(Z3_ast a, Z3_ast b) { - Z3_ast checks[3]; - checks[0] = Z3_mk_fpa_is_nan(g_context, a); - checks[1] = Z3_mk_fpa_is_nan(g_context, b); - checks[2] = _sym_build_float_ordered_less_than(a, b); - return registerExpression(Z3_mk_or(g_context, 2, checks)); -} - -Z3_ast _sym_build_float_unordered_less_equal(Z3_ast a, Z3_ast b) { - Z3_ast checks[3]; - checks[0] = Z3_mk_fpa_is_nan(g_context, a); - checks[1] = Z3_mk_fpa_is_nan(g_context, b); - checks[2] = _sym_build_float_ordered_less_equal(a, b); - return registerExpression(Z3_mk_or(g_context, 2, checks)); -} - -Z3_ast _sym_build_float_unordered_equal(Z3_ast a, Z3_ast b) { - Z3_ast checks[3]; - checks[0] = Z3_mk_fpa_is_nan(g_context, a); - checks[1] = Z3_mk_fpa_is_nan(g_context, b); - checks[2] = _sym_build_float_ordered_equal(a, b); - return registerExpression(Z3_mk_or(g_context, 2, checks)); -} - -Z3_ast _sym_build_float_unordered_not_equal(Z3_ast a, Z3_ast b) { - Z3_ast checks[3]; - checks[0] = Z3_mk_fpa_is_nan(g_context, a); - checks[1] = Z3_mk_fpa_is_nan(g_context, b); - checks[2] = _sym_build_float_ordered_not_equal(a, b); - return registerExpression(Z3_mk_or(g_context, 2, checks)); -} - -Z3_ast _sym_build_sext(Z3_ast expr, uint8_t bits) { - if (expr == nullptr) - return nullptr; - return registerExpression(Z3_mk_sign_ext(g_context, bits, expr)); -} - -Z3_ast _sym_build_zext(Z3_ast expr, uint8_t bits) { - if (expr == nullptr) - return nullptr; - return registerExpression(Z3_mk_zero_ext(g_context, bits, expr)); -} - -Z3_ast _sym_build_trunc(Z3_ast expr, uint8_t bits) { - if (expr == nullptr) - return nullptr; - - return registerExpression(Z3_mk_extract(g_context, bits - 1, 0, expr)); -} - -Z3_ast _sym_build_int_to_float(Z3_ast value, int is_double, int is_signed) { - auto *sort = FSORT(is_double); - Z3_inc_ref(g_context, (Z3_ast)sort); - auto *result = registerExpression( - is_signed - ? Z3_mk_fpa_to_fp_signed(g_context, g_rounding_mode, value, sort) - : Z3_mk_fpa_to_fp_unsigned(g_context, g_rounding_mode, value, sort)); - Z3_dec_ref(g_context, (Z3_ast)sort); - return result; -} - -Z3_ast _sym_build_float_to_float(Z3_ast expr, int to_double) { - auto *sort = FSORT(to_double); - Z3_inc_ref(g_context, (Z3_ast)sort); - auto *result = registerExpression( - Z3_mk_fpa_to_fp_float(g_context, g_rounding_mode, expr, sort)); - Z3_dec_ref(g_context, (Z3_ast)sort); - return result; -} - -Z3_ast _sym_build_bits_to_float(Z3_ast expr, int to_double) { - if (expr == nullptr) - return nullptr; - - auto *sort = FSORT(to_double); - Z3_inc_ref(g_context, (Z3_ast)sort); - auto *result = registerExpression(Z3_mk_fpa_to_fp_bv(g_context, expr, sort)); - Z3_dec_ref(g_context, (Z3_ast)sort); - return result; -} - -Z3_ast _sym_build_float_to_bits(Z3_ast expr) { - if (expr == nullptr) - return nullptr; - return registerExpression(Z3_mk_fpa_to_ieee_bv(g_context, expr)); -} - -Z3_ast _sym_build_float_to_signed_integer(Z3_ast expr, uint8_t bits) { - return registerExpression(Z3_mk_fpa_to_sbv( - g_context, Z3_mk_fpa_round_toward_zero(g_context), expr, bits)); -} - -Z3_ast _sym_build_float_to_unsigned_integer(Z3_ast expr, uint8_t bits) { - return registerExpression(Z3_mk_fpa_to_ubv( - g_context, Z3_mk_fpa_round_toward_zero(g_context), expr, bits)); -} - -Z3_ast _sym_build_bool_to_bit(Z3_ast expr) { - if (expr == nullptr) - return nullptr; - return _sym_build_ite(expr, _sym_build_integer(1, 1), - _sym_build_integer(0, 1)); -} - -void _sym_push_path_constraint(Z3_ast constraint, int taken, - uintptr_t site_id [[maybe_unused]]) { - if (constraint == nullptr) - return; - - constraint = Z3_simplify(g_context, constraint); - Z3_inc_ref(g_context, constraint); - - /* Check the easy cases first: if simplification reduced the constraint to - "true" or "false", there is no point in trying to solve the negation or * - pushing the constraint to the solver... */ - - if (Z3_is_eq_ast(g_context, constraint, g_true)) { - assert(taken && "We have taken an impossible branch"); - Z3_dec_ref(g_context, constraint); - return; - } - - if (Z3_is_eq_ast(g_context, constraint, g_false)) { - assert(!taken && "We have taken an impossible branch"); - Z3_dec_ref(g_context, constraint); - return; - } - - /* Generate a solution for the alternative */ - Z3_ast not_constraint = - Z3_simplify(g_context, Z3_mk_not(g_context, constraint)); - Z3_inc_ref(g_context, not_constraint); - - Z3_solver_push(g_context, g_solver); - Z3_solver_assert(g_context, g_solver, taken ? not_constraint : constraint); - fprintf(g_log, "Trying to solve:\n%s\n", - Z3_solver_to_string(g_context, g_solver)); - - Z3_lbool feasible = Z3_solver_check(g_context, g_solver); - if (feasible == Z3_L_TRUE) { - Z3_model model = Z3_solver_get_model(g_context, g_solver); - Z3_model_inc_ref(g_context, model); - fprintf(g_log, "Found diverging input:\n%s\n", - Z3_model_to_string(g_context, model)); - Z3_model_dec_ref(g_context, model); - } else { - fprintf(g_log, "Can't find a diverging input at this point\n"); - } - fflush(g_log); - - Z3_solver_pop(g_context, g_solver, 1); - - /* Assert the actual path constraint */ - Z3_ast newConstraint = (taken ? constraint : not_constraint); - Z3_inc_ref(g_context, newConstraint); - Z3_solver_assert(g_context, g_solver, newConstraint); - assert((Z3_solver_check(g_context, g_solver) == Z3_L_TRUE) && - "Asserting infeasible path constraint"); - Z3_dec_ref(g_context, constraint); - Z3_dec_ref(g_context, not_constraint); -} - -SymExpr _sym_concat_helper(SymExpr a, SymExpr b) { - return registerExpression(Z3_mk_concat(g_context, a, b)); -} - -SymExpr _sym_extract_helper(SymExpr expr, size_t first_bit, size_t last_bit) { - return registerExpression( - Z3_mk_extract(g_context, first_bit, last_bit, expr)); -} - -size_t _sym_bits_helper(SymExpr expr) { - auto *sort = Z3_get_sort(g_context, expr); - Z3_inc_ref(g_context, (Z3_ast)sort); - auto result = Z3_get_bv_sort_size(g_context, sort); - Z3_dec_ref(g_context, (Z3_ast)sort); - return result; -} - -/* No call-stack tracing */ -void _sym_notify_call(uintptr_t) {} -void _sym_notify_ret(uintptr_t) {} -void _sym_notify_basic_block(uintptr_t) {} - -/* Debugging */ -const char *_sym_expr_to_string(SymExpr expr) { - return Z3_ast_to_string(g_context, expr); -} - -bool _sym_feasible(SymExpr expr) { - expr = Z3_simplify(g_context, expr); - Z3_inc_ref(g_context, expr); - - Z3_solver_push(g_context, g_solver); - Z3_solver_assert(g_context, g_solver, expr); - Z3_lbool feasible = Z3_solver_check(g_context, g_solver); - Z3_solver_pop(g_context, g_solver, 1); - - Z3_dec_ref(g_context, expr); - return (feasible == Z3_L_TRUE); -} - -/* Garbage collection */ -void _sym_collect_garbage() { - if (allocatedExpressions.size() < g_config.garbageCollectionThreshold) - return; - -#ifndef NDEBUG - auto start = std::chrono::high_resolution_clock::now(); - auto startSize = allocatedExpressions.size(); -#endif - - auto reachableExpressions = collectReachableExpressions(); - for (auto expr_it = allocatedExpressions.begin(); - expr_it != allocatedExpressions.end();) { - if (reachableExpressions.count(*expr_it) == 0) { - expr_it = allocatedExpressions.erase(expr_it); - } else { - ++expr_it; - } - } - -#ifndef NDEBUG - auto end = std::chrono::high_resolution_clock::now(); - auto endSize = allocatedExpressions.size(); - - std::cerr << "After garbage collection: " << endSize - << " expressions remain (before: " << startSize << ")" << std::endl - << "\t(collection took " - << std::chrono::duration_cast(end - - start) - .count() - << " milliseconds)" << std::endl; -#endif -} - -/* Test-case handling */ -void symcc_set_test_case_handler(TestCaseHandler) { - // The simple backend doesn't support test-case handlers. However, let's not - // make this a fatal error; otherwise, users would have to change their - // programs to make them work with the simple backend. - fprintf( - g_log, - "Warning: test-case handlers aren't supported in the simple backend\n"); -} diff --git a/runtime/simple_backend/Runtime.h b/runtime/simple_backend/Runtime.h deleted file mode 100644 index 66fe8b91..00000000 --- a/runtime/simple_backend/Runtime.h +++ /dev/null @@ -1,24 +0,0 @@ -// This file is part of the SymCC runtime. -// -// The SymCC runtime is free software: you can redistribute it and/or modify it -// under the terms of the GNU Lesser General Public License as published by the -// Free Software Foundation, either version 3 of the License, or (at your -// option) any later version. -// -// The SymCC runtime 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 Lesser General Public License -// for more details. -// -// You should have received a copy of the GNU Lesser General Public License -// along with SymCC. If not, see . - -#ifndef RUNTIME_H -#define RUNTIME_H - -#include - -typedef Z3_ast SymExpr; -#include - -#endif diff --git a/test/CMakeLists.txt b/test/CMakeLists.txt index c6b0d1b5..3dd5bc21 100644 --- a/test/CMakeLists.txt +++ b/test/CMakeLists.txt @@ -12,10 +12,12 @@ # You should have received a copy of the GNU General Public License along with # SymCC. If not, see . -if (QSYM_BACKEND) +if (SYMCC_RT_BACKEND STREQUAL "qsym") set(SYM_TEST_FILECHECK_ARGS "--check-prefix=QSYM --check-prefix=ANY") -else() +elseif (SYMCC_RT_BACKEND STREQUAL "simple") set(SYM_TEST_FILECHECK_ARGS "--check-prefix=SIMPLE --check-prefix=ANY") +else() + message(FATAL_ERROR "Unknown backend to test: ${SYMCC_RT_BACKEND}") endif() if (${LLVM_VERSION_MAJOR} VERSION_GREATER_EQUAL 14) @@ -35,7 +37,7 @@ add_custom_target(check COMMENT "Testing the system..." USES_TERMINAL) -add_dependencies(check SymRuntime Symbolize) -if (TARGET SymRuntime32) - add_dependencies(check SymRuntime32) +add_dependencies(check SymCCRuntime SymCC) +if (TARGET SymCCRuntime32) + add_dependencies(check SymCCRuntime32 SymCC) endif() diff --git a/util/quicktest.sh b/util/quicktest.sh index aead0f98..dd9ccd7d 100755 --- a/util/quicktest.sh +++ b/util/quicktest.sh @@ -27,13 +27,12 @@ git clone https://github.com/eurecom-s3/symcc.git cd symcc # init/update submodules -git submodule init -git submodule update +git submodule update --init --recursive # build mkdir ../symcc-build cd ../symcc-build -cmake -G Ninja -DQSYM_BACKEND=ON -DZ3_TRUST_SYSTEM_VERSION=on ../symcc +cmake -G Ninja -DSYMCC_RT_BACKEND=qsym -DZ3_TRUST_SYSTEM_VERSION=on ../symcc ninja check # create a test case