diff --git a/.adacore-gitlab-ci.yml b/.adacore-gitlab-ci.yml
new file mode 100644
index 00000000..9f70bcaf
--- /dev/null
+++ b/.adacore-gitlab-ci.yml
@@ -0,0 +1,24 @@
+workflow:
+ rules:
+ - if: '$CI_PIPELINE_SOURCE == "merge_request_event"'
+
+anod_build:
+ services:
+ - image:sandbox
+ - cpu:8
+ - mem:16
+ stage: build
+ script:
+ - export ANOD_DEFAULT_SANDBOX_DIR=/it/wave
+
+ # Check out QSYM
+ - cd runtime/qsym_backend
+ - git clone -b symcc https://gitlab-ci-token:${CI_JOB_TOKEN}@${CI_SERVER_HOST}:${CI_SERVER_PORT}/eng/fuzz/qsym
+
+ # Use our repositories
+ - anod vcs --add-repo symcc $CI_PROJECT_DIR
+ - anod vcs --add-repo qsym $CI_PROJECT_DIR/runtime/qsym_backend/qsym
+
+ # Build SymCC
+ - anod source symcc
+ - anod build symcc
diff --git a/.clang-format b/.clang-format
new file mode 100644
index 00000000..f007ce43
--- /dev/null
+++ b/.clang-format
@@ -0,0 +1,3 @@
+---
+BasedOnStyle: LLVM
+...
diff --git a/.github/workflows/check_style.yml b/.github/workflows/check_style.yml
new file mode 100644
index 00000000..f3580388
--- /dev/null
+++ b/.github/workflows/check_style.yml
@@ -0,0 +1,19 @@
+name: Check coding style
+on: [pull_request]
+jobs:
+ coding_style:
+ runs-on: ubuntu-22.04
+ steps:
+ - uses: actions/checkout@v3
+ with:
+ fetch-depth: 0
+ - name: Run clang-format
+ shell: bash
+ run: |
+ format_changes=$(git clang-format-14 --quiet --diff \
+ ${{ github.event.pull_request.base.sha }} \
+ ${{ github.event.pull_request.head.sha }} | wc -c)
+ if [[ $format_changes -ne 0 ]]; then
+ echo "Please format your changes with clang-format using the LLVM style, e.g., git clang-format --style LLVM before committing"
+ exit 1
+ fi
diff --git a/.github/workflows/run_tests.yml b/.github/workflows/run_tests.yml
index fe2c0f82..e3666317 100644
--- a/.github/workflows/run_tests.yml
+++ b/.github/workflows/run_tests.yml
@@ -1,5 +1,5 @@
name: Compile and test SymCC
-on: [push, pull_request]
+on: [pull_request, workflow_dispatch]
jobs:
build_and_test_symcc:
runs-on: ubuntu-20.04
@@ -15,3 +15,64 @@ jobs:
run: docker build --target builder_qsym -t symcc .
- name: Creation of the final SymCC docker image with Qsym backend and libcxx
run: docker build -t symcc .
+ llvm_compatibility:
+ runs-on: ubuntu-22.04
+ strategy:
+ matrix:
+ llvm_version: [11, 12, 13, 14, 15]
+ steps:
+ - uses: actions/checkout@v3
+ with:
+ submodules: true
+ - name: Install dependencies
+ run: |
+ sudo apt-get update
+ sudo apt-get install -y \
+ llvm-${{ matrix.llvm_version }}-dev \
+ libz3-dev \
+ python2
+ - name: Build SymCC with the QSYM backend
+ run: |
+ mkdir build
+ cd build
+ cmake \
+ -DCMAKE_BUILD_TYPE=Release \
+ -DZ3_TRUST_SYSTEM_VERSION=ON \
+ -DQSYM_BACKEND=ON \
+ -DLLVM_DIR=/usr/lib/llvm-${{ matrix.llvm_version }}/cmake \
+ ..
+ make
+ llvm_compatibility_latest_llvm:
+ runs-on: ubuntu-22.04
+ strategy:
+ matrix:
+ llvm_version: [16, 17]
+ steps:
+ - uses: actions/checkout@v3
+ with:
+ submodules: true
+ - name: Add LLVM project deb repository
+ uses: myci-actions/add-deb-repo@11
+ with:
+ repo: deb http://apt.llvm.org/jammy/ llvm-toolchain-jammy-${{ matrix.llvm_version }} main
+ repo-name: llvm
+ update: false
+ keys-asc: https://apt.llvm.org/llvm-snapshot.gpg.key
+ - name: Install dependencies
+ run: |
+ sudo apt-get update
+ sudo apt-get install -y \
+ llvm-${{ matrix.llvm_version }}-dev \
+ libz3-dev \
+ python2
+ - name: Build SymCC with the QSYM backend
+ run: |
+ mkdir build
+ cd build
+ cmake \
+ -DCMAKE_BUILD_TYPE=Release \
+ -DZ3_TRUST_SYSTEM_VERSION=ON \
+ -DQSYM_BACKEND=ON \
+ -DLLVM_DIR=/usr/lib/llvm-${{ matrix.llvm_version }}/cmake \
+ ..
+ make
diff --git a/.gitignore b/.gitignore
index 9aba1266..a5522f87 100644
--- a/.gitignore
+++ b/.gitignore
@@ -40,3 +40,7 @@ TAGS
# Clang tooling
compile_commands.json
.clangd
+.cache
+
+# Build directories
+build*
diff --git a/CMakeLists.txt b/CMakeLists.txt
index d9832256..5d98a9cb 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -15,6 +15,8 @@
cmake_minimum_required(VERSION 3.5)
project(SymbolicCompiler)
+list(APPEND CMAKE_MODULE_PATH "${CMAKE_SOURCE_DIR}/cmake")
+
option(QSYM_BACKEND "Use the Qsym backend instead of our own" OFF)
option(TARGET_32BIT "Make the compiler work correctly with -m32" OFF)
@@ -33,10 +35,12 @@ set(SYM_RUNTIME_BUILD_ARGS
-DCMAKE_CXX_FLAGS_INIT=${CMAKE_CXX_FLAGS_INIT}
-DCMAKE_EXE_LINKER_FLAGS=${CMAKE_EXE_LINKER_FLAGS}
-DCMAKE_EXE_LINKER_FLAGS_INIT=${CMAKE_EXE_LINKER_FLAGS_INIT}
+ -DCMAKE_MAKE_PROGRAM=${CMAKE_MAKE_PROGRAM}
-DCMAKE_MODULE_LINKER_FLAGS=${CMAKE_MODULE_LINKER_FLAGS}
-DCMAKE_MODULE_LINKER_FLAGS_INIT=${CMAKE_MODULE_LINKER_FLAGS_INIT}
-DCMAKE_SHARED_LINKER_FLAGS=${CMAKE_SHARED_LINKER_FLAGS}
-DCMAKE_SHARED_LINKER_FLAGS_INIT=${CMAKE_SHARED_LINKER_FLAGS_INIT}
+ -DCMAKE_MODULE_PATH=${CMAKE_MODULE_PATH}
-DCMAKE_SYSROOT=${CMAKE_SYSROOT}
-DQSYM_BACKEND=${QSYM_BACKEND}
-DCMAKE_BUILD_TYPE=${CMAKE_BUILD_TYPE}
@@ -76,8 +80,8 @@ find_package(LLVM 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 11)
- message(WARNING "The software has been developed for LLVM 8 through 11; \
+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()
@@ -87,7 +91,7 @@ include_directories(SYSTEM ${LLVM_INCLUDE_DIRS})
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 -Werror")
+-Wmissing-format-attribute -Wformat-nonliteral -Werror -Wno-error=deprecated-declarations")
# Mark nodelete to work around unload bug in upstream LLVM 5.0+
set(CMAKE_MODULE_LINKER_FLAGS "${CMAKE_MODULE_LINKER_FLAGS} -Wl,-z,nodelete")
@@ -114,6 +118,12 @@ if (NOT CLANG_BINARY)
message(FATAL_ERROR "Clang not found; please make sure that the version corresponding to your LLVM installation is available.")
endif()
+if (${LLVM_VERSION_MAJOR} LESS 13)
+ set(CLANG_LOAD_PASS "-Xclang -load -Xclang ")
+else()
+ set(CLANG_LOAD_PASS "-fpass-plugin=")
+endif()
+
configure_file("compiler/symcc.in" "symcc" @ONLY)
configure_file("compiler/sym++.in" "sym++" @ONLY)
diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md
new file mode 100644
index 00000000..be09db8d
--- /dev/null
+++ b/CONTRIBUTING.md
@@ -0,0 +1,17 @@
+# Contributing to SymCC
+
+We encourage everyone to contribute improvements and bug fixes to SymCC. Our
+preferred way of accepting contributions is via GitHub pull requests. Please be
+sure to run clang-format on any C/C++ code you change; an easy way to do so is
+with `git clang-format --style LLVM` just before committing. (On Ubuntu, you can
+get `git-clang-format` via `apt install clang-format`.) Ideally, also add a test
+to your patch (see the
+[docs](https://github.com/eurecom-s3/symcc/blob/master/docs/Testing.txt) for
+details). Unfortunately, since the project is a bit short on developers at the
+moment, we have to ask for your patience while we review your PR.
+
+Please note that any contributions you make are licensed under the same terms as
+the code you're contributing to, as per the GitHub Terms of Service, [section
+D.6](https://docs.github.com/en/site-policy/github-terms/github-terms-of-service#6-contributions-under-repository-license).
+At the time of writing, this means LGPL (version 3 or later) for the SymCC
+runtime, and GPL (version 3 or later) for the rest of SymCC.
diff --git a/Dockerfile b/Dockerfile
index 1d695ac0..5d93d01d 100644
--- a/Dockerfile
+++ b/Dockerfile
@@ -15,19 +15,19 @@
#
# The base image
#
-FROM ubuntu:20.04 AS builder
+FROM ubuntu:22.04 AS builder
# Install dependencies
RUN apt-get update \
&& DEBIAN_FRONTEND=noninteractive apt-get install -y \
cargo \
- clang-10 \
+ clang-15 \
cmake \
g++ \
git \
libz3-dev \
- llvm-10-dev \
- llvm-10-tools \
+ llvm-15-dev \
+ llvm-15-tools \
ninja-build \
python2 \
python3-pip \
@@ -42,7 +42,7 @@ RUN git clone -b v2.56b https://github.com/google/AFL.git afl \
# Download the LLVM sources already so that we don't need to get them again when
# SymCC changes
-RUN git clone -b llvmorg-10.0.1 --depth 1 https://github.com/llvm/llvm-project.git /llvm_source
+RUN git clone -b llvmorg-15.0.0 --depth 1 https://github.com/llvm/llvm-project.git /llvm_source
# Build a version of SymCC with the simple backend to compile libc++
COPY . /symcc_source
@@ -105,14 +105,14 @@ RUN cmake -G Ninja \
#
# The final image
#
-FROM ubuntu:20.04
+FROM ubuntu:22.04
RUN apt-get update \
&& DEBIAN_FRONTEND=noninteractive apt-get install -y \
build-essential \
- clang-10 \
+ clang-15 \
g++ \
- libllvm10 \
+ libllvm15 \
zlib1g \
sudo \
&& rm -rf /var/lib/apt/lists/* \
@@ -127,8 +127,8 @@ COPY --from=builder_qsym /afl /afl
ENV PATH /symcc_build:$PATH
ENV AFL_PATH /afl
-ENV AFL_CC clang-10
-ENV AFL_CXX clang++-10
+ENV AFL_CC clang-15
+ENV AFL_CXX clang++-15
ENV SYMCC_LIBCXX_PATH=/libcxx_symcc_install
USER ubuntu
diff --git a/LICENSE.lgpl b/LICENSE.lgpl
new file mode 100644
index 00000000..0a041280
--- /dev/null
+++ b/LICENSE.lgpl
@@ -0,0 +1,165 @@
+ 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 075a5b60..4e6cea09 100644
--- a/README.md
+++ b/README.md
@@ -1,23 +1,32 @@
[![Compile and test SymCC](https://github.com/eurecom-s3/symcc/actions/workflows/run_tests.yml/badge.svg)](https://github.com/eurecom-s3/symcc/actions/workflows/run_tests.yml)
+Note: The SymCC project is currently understaffed and therefore maintained in a
+best effort mode. In fact, we are hiring, in case you are interested to join
+the [S3 group at Eurecom](https://www.s3.eurecom.fr/) to work on this (and other
+projects in the group) please [contact us](mailto:aurelien.francillon@eurecom.fr).
+We nevertheless appreciate PRs and apologize in advance for the slow processing
+of PRs, we will try to merge them when possible.
+
# SymCC: efficient compiler-based symbolic execution
-SymCC is a compiler wrapper which embeds symbolic execution into the program
+SymCC is a compiler pass which embeds symbolic execution into the program
during compilation, and an associated run-time support library. In essence, the
compiler inserts code that computes symbolic expressions for each value in the
program. The actual computation happens through calls to the support library at
run time.
-To build the pass and the support library, make sure that LLVM 8, 9, 10 or 11
-and Z3 version 4.5 or later, as well as a C++ compiler with support for C++17
-are installed. "lit" is also needed which is not always packaged with LLVM.
+To build the pass and the support library, install LLVM (any version between 8
+and 17) 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:
```
-sudo apt install -y git cargo clang-10 cmake g++ git libz3-dev llvm-10-dev llvm-10-tools ninja-build python2 python3-pip zlib1g-dev && sudo pip3 install lit
+sudo apt install -y git cargo clang-14 cmake g++ git libz3-dev llvm-14-dev llvm-14-tools ninja-build python2 python3-pip zlib1g-dev && sudo pip3 install lit
```
+
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).
@@ -173,6 +182,57 @@ every change to SymCC (which is, in principle the right thing to do), whereas in
many cases it is sufficient to let the build system figure out what to rebuild
(and recompile, e.g., libc++ only when necessary).
+## FAQ / BUGS / TODOs
+
+### 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
+see [issue #14](https://github.com/eurecom-s3/symcc/issues/14)
+
+### Why does SymCC not generate some test cases?
+
+There are multiple possible reasons:
+
+#### QSym backend performs pruning
+
+When built with the QSym backend exploration (e.g., loops) symcc is
+subject to path pruning, this is part of the optimizations that makes
+SymCC/QSym fast, it isn't sound. This is not a problem for using in
+hybrid fuzzing, but this may be a problem for other uses. See for
+example [issue #88](https://github.com/eurecom-s3/symcc/issues/88).
+
+When building with the simple backend the paths should be found. If
+the paths are not found with the simple backend this may be a bug (or
+possibly a limitation of the simple backend).
+
+#### Incomplete symbolic handing of functions, systems interactions.
+
+The current symbolic understanding of libc is incomplete. So when an
+unsupported libc function is called SymCC can't trace the computations
+that happen in the function.
+
+1. Adding the function to the [collection of wrapped libc
+ functions](https://github.com/eurecom-s3/symcc/blob/master/runtime/LibcWrappers.cpp)
+ and [register the
+ wrapper](https://github.com/eurecom-s3/symcc/blob/b29dc4db2803830ebf50798e72b336473a567655/compiler/Runtime.cpp#L159)
+ in the compiler.
+2. Build a fully instrumented libc.
+3. Cherry-pick individual libc functions from a libc implementation (e.g., musl)
+
+See [issue #23](https://github.com/eurecom-s3/symcc/issues/23) for more details.
+
+
+### Rust support ?
+
+This would be possible to support RUST, see [issue
+#1](https://github.com/eurecom-s3/symcc/issues/1) for tracking this.
+
+### Bug reporting
+
+We appreciate bugs with test cases and steps to reproduce, PR with
+corresponding test cases. SymCC is currently understaffed, we hope to
+catch up and get back to active development at some point.
## Contact
@@ -210,17 +270,24 @@ 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.
-You should have received a copy of the GNU General Public License along with
-SymCC. If not, see .
+You should have received a copy of the GNU General Public License and the GNU
+Lesser General Public License along with SymCC. If not, see
+.
The following pieces of software have additional or alternate copyrights,
licenses, and/or restrictions:
-| Program | Directory |
-| --- | --- |
-| QSYM | `runtime/qsym_backend/qsym` |
+| Program | Directory |
+|---------------|-----------------------------|
+| QSYM | `runtime/qsym_backend/qsym` |
+| SymCC runtime | `runtime` |
diff --git a/cmake/FindFilesystem.cmake b/cmake/FindFilesystem.cmake
new file mode 100644
index 00000000..a152e522
--- /dev/null
+++ b/cmake/FindFilesystem.cmake
@@ -0,0 +1,247 @@
+# 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/Main.cpp b/compiler/Main.cpp
index 9be71ff6..e4c7d4e7 100644
--- a/compiler/Main.cpp
+++ b/compiler/Main.cpp
@@ -13,19 +13,85 @@
// SymCC. If not, see .
#include
+#if LLVM_VERSION_MAJOR <= 15
#include
+#endif
+#include
+#include
+
+#if LLVM_VERSION_MAJOR >= 13
+#include
+#include
+
+#if LLVM_VERSION_MAJOR >= 14
+#include
+#else
+using OptimizationLevel = llvm::PassBuilder::OptimizationLevel;
+#endif
+#endif
+
+#if LLVM_VERSION_MAJOR >= 15
+#include
+#else
+#include
+#endif
#include "Pass.h"
-void addSymbolizePass(const llvm::PassManagerBuilder & /* unused */,
- llvm::legacy::PassManagerBase &PM) {
- PM.add(new SymbolizePass());
+using namespace llvm;
+
+//
+// Legacy pass registration (up to LLVM 13)
+//
+
+#if LLVM_VERSION_MAJOR <= 15
+
+void addSymbolizeLegacyPass(const PassManagerBuilder & /* unused */,
+ legacy::PassManagerBase &PM) {
+ PM.add(createScalarizerPass());
+ PM.add(createLowerAtomicPass());
+ PM.add(new SymbolizeLegacyPass());
}
// Make the pass known to opt.
-static llvm::RegisterPass X("symbolize", "Symbolization Pass");
+static RegisterPass X("symbolize", "Symbolization Pass");
// Tell frontends to run the pass automatically.
-static struct llvm::RegisterStandardPasses
- Y(llvm::PassManagerBuilder::EP_VectorizerStart, addSymbolizePass);
-static struct llvm::RegisterStandardPasses
- Z(llvm::PassManagerBuilder::EP_EnabledOnOptLevel0, addSymbolizePass);
+static struct RegisterStandardPasses Y(PassManagerBuilder::EP_VectorizerStart,
+ addSymbolizeLegacyPass);
+static struct RegisterStandardPasses
+ Z(PassManagerBuilder::EP_EnabledOnOptLevel0, addSymbolizeLegacyPass);
+
+#endif
+
+//
+// New pass registration (LLVM 13 and above)
+//
+
+#if LLVM_VERSION_MAJOR >= 13
+
+PassPluginLibraryInfo getSymbolizePluginInfo() {
+ return {LLVM_PLUGIN_API_VERSION, "Symbolization Pass", LLVM_VERSION_STRING,
+ [](PassBuilder &PB) {
+ // We need to act on the entire module as well as on each function.
+ // Those actions are independent from each other, so we register a
+ // module pass at the start of the pipeline and a function pass just
+ // before the vectorizer. (There doesn't seem to be a way to run
+ // module passes at the start of the vectorizer, hence the split.)
+ PB.registerPipelineStartEPCallback(
+ [](ModulePassManager &PM, OptimizationLevel) {
+ PM.addPass(SymbolizePass());
+ });
+ PB.registerVectorizerStartEPCallback(
+ [](FunctionPassManager &PM, OptimizationLevel) {
+ PM.addPass(ScalarizerPass());
+ PM.addPass(LowerAtomicPass());
+ PM.addPass(SymbolizePass());
+ });
+ }};
+}
+
+extern "C" LLVM_ATTRIBUTE_WEAK PassPluginLibraryInfo llvmGetPassPluginInfo() {
+ return getSymbolizePluginInfo();
+}
+
+#endif
diff --git a/compiler/Pass.cpp b/compiler/Pass.cpp
index 122fd571..af0d88a8 100644
--- a/compiler/Pass.cpp
+++ b/compiler/Pass.cpp
@@ -15,11 +15,22 @@
#include "Pass.h"
#include
+#include
+#include
+#include
#include
#include
#include
+#include
+#include
#include
+#if LLVM_VERSION_MAJOR < 14
+#include
+#else
+#include
+#endif
+
#include "Runtime.h"
#include "Symbolizer.h"
@@ -34,10 +45,14 @@ using namespace llvm;
#define DEBUG(X) ((void)0)
#endif
-char SymbolizePass::ID = 0;
+char SymbolizeLegacyPass::ID = 0;
-bool SymbolizePass::doInitialization(Module &M) {
- DEBUG(errs() << "Symbolizer module init\n");
+namespace {
+
+static constexpr char kSymCtorName[] = "__sym_ctor";
+
+bool instrumentModule(Module &M) {
+ DEBUG(errs() << "Symbolizer module instrumentation\n");
// Redirect calls to external functions to the corresponding wrappers and
// rename internal functions.
@@ -56,7 +71,95 @@ bool SymbolizePass::doInitialization(Module &M) {
return true;
}
-bool SymbolizePass::runOnFunction(Function &F) {
+bool canLower(const CallInst *CI) {
+ const Function *Callee = CI->getCalledFunction();
+ if (!Callee)
+ return false;
+
+ switch (Callee->getIntrinsicID()) {
+ case Intrinsic::expect:
+ case Intrinsic::ctpop:
+ case Intrinsic::ctlz:
+ case Intrinsic::cttz:
+ case Intrinsic::prefetch:
+ case Intrinsic::pcmarker:
+ case Intrinsic::dbg_declare:
+ case Intrinsic::dbg_label:
+ case Intrinsic::eh_typeid_for:
+ case Intrinsic::annotation:
+ case Intrinsic::ptr_annotation:
+ case Intrinsic::assume:
+#if LLVM_VERSION_MAJOR > 11
+ case Intrinsic::experimental_noalias_scope_decl:
+#endif
+ case Intrinsic::var_annotation:
+ case Intrinsic::sqrt:
+ case Intrinsic::log:
+ case Intrinsic::log2:
+ case Intrinsic::log10:
+ case Intrinsic::exp:
+ case Intrinsic::exp2:
+ case Intrinsic::pow:
+ case Intrinsic::sin:
+ case Intrinsic::cos:
+ case Intrinsic::floor:
+ case Intrinsic::ceil:
+ case Intrinsic::trunc:
+ case Intrinsic::round:
+#if LLVM_VERSION_MAJOR > 10
+ case Intrinsic::roundeven:
+#endif
+ case Intrinsic::copysign:
+#if LLVM_VERSION_MAJOR < 16
+ case Intrinsic::flt_rounds:
+#else
+ case Intrinsic::get_rounding:
+#endif
+ case Intrinsic::invariant_start:
+ case Intrinsic::lifetime_start:
+ case Intrinsic::invariant_end:
+ case Intrinsic::lifetime_end:
+ return true;
+ default:
+ return false;
+ }
+
+ llvm_unreachable("Control cannot reach here");
+}
+
+void liftInlineAssembly(CallInst *CI) {
+ // TODO When we don't have to worry about the old pass manager anymore, move
+ // the initialization to the pass constructor. (Currently there are two
+ // passes, but only if we're on a recent enough LLVM...)
+
+ Function *F = CI->getFunction();
+ Module *M = F->getParent();
+ auto triple = M->getTargetTriple();
+
+ std::string error;
+ auto target = TargetRegistry::lookupTarget(triple, error);
+ if (!target) {
+ errs() << "Warning: can't get target info to lift inline assembly\n";
+ return;
+ }
+
+ auto cpu = F->getFnAttribute("target-cpu").getValueAsString();
+ auto features = F->getFnAttribute("target-features").getValueAsString();
+
+ std::unique_ptr TM(
+ target->createTargetMachine(triple, cpu, features, TargetOptions(), {}));
+ auto subTarget = TM->getSubtargetImpl(*F);
+ if (subTarget == nullptr)
+ return;
+
+ auto targetLowering = subTarget->getTargetLowering();
+ if (targetLowering == nullptr)
+ return;
+
+ targetLowering->ExpandInlineAsm(CI);
+}
+
+bool instrumentFunction(Function &F) {
auto functionName = F.getName();
if (functionName == kSymCtorName)
return false;
@@ -69,6 +172,21 @@ bool SymbolizePass::runOnFunction(Function &F) {
for (auto &I : instructions(F))
allInstructions.push_back(&I);
+ IntrinsicLowering IL(F.getParent()->getDataLayout());
+ for (auto *I : allInstructions) {
+ if (auto *CI = dyn_cast(I)) {
+ if (canLower(CI)) {
+ IL.LowerIntrinsicCall(CI);
+ } else if (isa(CI->getCalledOperand())) {
+ liftInlineAssembly(CI);
+ }
+ }
+ }
+
+ allInstructions.clear();
+ for (auto &I : instructions(F))
+ allInstructions.push_back(&I);
+
Symbolizer symbolizer(*F.getParent());
symbolizer.symbolizeFunctionArguments(F);
@@ -87,3 +205,27 @@ bool SymbolizePass::runOnFunction(Function &F) {
return true;
}
+
+} // namespace
+
+bool SymbolizeLegacyPass::doInitialization(Module &M) {
+ return instrumentModule(M);
+}
+
+bool SymbolizeLegacyPass::runOnFunction(Function &F) {
+ return instrumentFunction(F);
+}
+
+#if LLVM_VERSION_MAJOR >= 13
+
+PreservedAnalyses SymbolizePass::run(Function &F, FunctionAnalysisManager &) {
+ return instrumentFunction(F) ? PreservedAnalyses::none()
+ : PreservedAnalyses::all();
+}
+
+PreservedAnalyses SymbolizePass::run(Module &M, ModuleAnalysisManager &) {
+ return instrumentModule(M) ? PreservedAnalyses::none()
+ : PreservedAnalyses::all();
+}
+
+#endif
diff --git a/compiler/Pass.h b/compiler/Pass.h
index 53764931..b06377dc 100644
--- a/compiler/Pass.h
+++ b/compiler/Pass.h
@@ -19,21 +19,31 @@
#include
#include
-class SymbolizePass : public llvm::FunctionPass {
+#if LLVM_VERSION_MAJOR >= 13
+#include
+#endif
+
+class SymbolizeLegacyPass : public llvm::FunctionPass {
public:
static char ID;
- SymbolizePass() : FunctionPass(ID) {}
+ SymbolizeLegacyPass() : FunctionPass(ID) {}
- bool doInitialization(llvm::Module &M) override;
- bool runOnFunction(llvm::Function &F) override;
+ virtual bool doInitialization(llvm::Module &M) override;
+ virtual bool runOnFunction(llvm::Function &F) override;
+};
-private:
- static constexpr char kSymCtorName[] = "__sym_ctor";
+#if LLVM_VERSION_MAJOR >= 13
- /// Mapping from global variables to their corresponding symbolic expressions.
- llvm::ValueMap
- globalExpressions;
+class SymbolizePass : public llvm::PassInfoMixin {
+public:
+ llvm::PreservedAnalyses run(llvm::Function &F,
+ llvm::FunctionAnalysisManager &);
+ llvm::PreservedAnalyses run(llvm::Module &M, llvm::ModuleAnalysisManager &);
+
+ static bool isRequired() { return true; }
};
#endif
+
+#endif
diff --git a/compiler/Runtime.cpp b/compiler/Runtime.cpp
index 81768841..a97b30f6 100644
--- a/compiler/Runtime.cpp
+++ b/compiler/Runtime.cpp
@@ -39,27 +39,25 @@ Runtime::Runtime(Module &M) {
auto *intPtrType = M.getDataLayout().getIntPtrType(M.getContext());
auto *ptrT = IRB.getInt8PtrTy();
auto *int8T = IRB.getInt8Ty();
+ auto *int1T = IRB.getInt1Ty();
auto *voidT = IRB.getVoidTy();
buildInteger = import(M, "_sym_build_integer", ptrT, IRB.getInt64Ty(), int8T);
buildInteger128 = import(M, "_sym_build_integer128", ptrT, IRB.getInt64Ty(),
IRB.getInt64Ty());
- buildFloat =
- import(M, "_sym_build_float", ptrT, IRB.getDoubleTy(), IRB.getInt1Ty());
+ buildFloat = import(M, "_sym_build_float", ptrT, IRB.getDoubleTy(), int1T);
buildNullPointer = import(M, "_sym_build_null_pointer", ptrT);
buildTrue = import(M, "_sym_build_true", ptrT);
buildFalse = import(M, "_sym_build_false", ptrT);
- buildBool = import(M, "_sym_build_bool", ptrT, IRB.getInt1Ty());
+ buildBool = import(M, "_sym_build_bool", ptrT, int1T);
buildSExt = import(M, "_sym_build_sext", ptrT, ptrT, int8T);
buildZExt = import(M, "_sym_build_zext", ptrT, ptrT, int8T);
buildTrunc = import(M, "_sym_build_trunc", ptrT, ptrT, int8T);
buildBswap = import(M, "_sym_build_bswap", ptrT, ptrT);
- buildIntToFloat = import(M, "_sym_build_int_to_float", ptrT, ptrT,
- IRB.getInt1Ty(), IRB.getInt1Ty());
- buildFloatToFloat =
- import(M, "_sym_build_float_to_float", ptrT, ptrT, IRB.getInt1Ty());
- buildBitsToFloat =
- import(M, "_sym_build_bits_to_float", ptrT, ptrT, IRB.getInt1Ty());
+ buildIntToFloat =
+ import(M, "_sym_build_int_to_float", ptrT, ptrT, int1T, int1T);
+ buildFloatToFloat = import(M, "_sym_build_float_to_float", ptrT, ptrT, int1T);
+ buildBitsToFloat = import(M, "_sym_build_bits_to_float", ptrT, ptrT, int1T);
buildFloatToBits = import(M, "_sym_build_float_to_bits", ptrT, ptrT);
buildFloatToSignedInt =
import(M, "_sym_build_float_to_signed_integer", ptrT, ptrT, int8T);
@@ -69,9 +67,34 @@ Runtime::Runtime(Module &M) {
buildBoolAnd = import(M, "_sym_build_bool_and", ptrT, ptrT, ptrT);
buildBoolOr = import(M, "_sym_build_bool_or", ptrT, ptrT, ptrT);
buildBoolXor = import(M, "_sym_build_bool_xor", ptrT, ptrT, ptrT);
- buildBoolToBits = import(M, "_sym_build_bool_to_bits", ptrT, ptrT, int8T);
- pushPathConstraint = import(M, "_sym_push_path_constraint", voidT, ptrT,
- IRB.getInt1Ty(), intPtrType);
+ buildBoolToBit = import(M, "_sym_build_bool_to_bit", ptrT, ptrT);
+ buildBitToBool = import(M, "_sym_build_bit_to_bool", ptrT, ptrT);
+ buildConcat =
+ import(M, "_sym_concat_helper", ptrT, ptrT,
+ ptrT); // doesn't follow naming convention for historic reasons
+ pushPathConstraint =
+ import(M, "_sym_push_path_constraint", voidT, ptrT, int1T, intPtrType);
+
+ // Overflow arithmetic
+ buildAddOverflow =
+ import(M, "_sym_build_add_overflow", ptrT, ptrT, ptrT, int1T, int1T);
+ buildSubOverflow =
+ import(M, "_sym_build_sub_overflow", ptrT, ptrT, ptrT, int1T, int1T);
+ buildMulOverflow =
+ import(M, "_sym_build_mul_overflow", ptrT, ptrT, ptrT, int1T, int1T);
+
+ // Saturating arithmetic
+ buildSAddSat = import(M, "_sym_build_sadd_sat", ptrT, ptrT, ptrT);
+ buildUAddSat = import(M, "_sym_build_uadd_sat", ptrT, ptrT, ptrT);
+ buildSSubSat = import(M, "_sym_build_ssub_sat", ptrT, ptrT, ptrT);
+ buildUSubSat = import(M, "_sym_build_usub_sat", ptrT, ptrT, ptrT);
+ buildSShlSat = import(M, "_sym_build_sshl_sat", ptrT, ptrT, ptrT);
+ buildUShlSat = import(M, "_sym_build_ushl_sat", ptrT, ptrT, ptrT);
+
+ buildFshl = import(M, "_sym_build_funnel_shift_left", ptrT, ptrT, ptrT, ptrT);
+ buildFshr =
+ import(M, "_sym_build_funnel_shift_right", ptrT, ptrT, ptrT, ptrT);
+ buildAbs = import(M, "_sym_build_abs", ptrT, ptrT);
setParameterExpression =
import(M, "_sym_set_parameter_expression", voidT, int8T, ptrT);
@@ -107,6 +130,14 @@ Runtime::Runtime(Module &M) {
#undef LOAD_BINARY_OPERATOR_HANDLER
+#define LOAD_UNARY_OPERATOR_HANDLER(constant, name) \
+ unaryOperatorHandlers[Instruction::constant] = \
+ import(M, "_sym_build_" #name, ptrT, ptrT);
+
+ LOAD_UNARY_OPERATOR_HANDLER(FNeg, fp_neg)
+
+#undef LOAD_UNARY_OPERATOR_HANDLER
+
#define LOAD_COMPARISON_HANDLER(constant, name) \
comparisonHandlers[CmpInst::constant] = \
import(M, "_sym_build_" #name, ptrT, ptrT, ptrT);
@@ -144,13 +175,14 @@ Runtime::Runtime(Module &M) {
memset = import(M, "_sym_memset", voidT, ptrT, ptrT, intPtrType);
memmove = import(M, "_sym_memmove", voidT, ptrT, ptrT, intPtrType);
readMemory =
- import(M, "_sym_read_memory", ptrT, intPtrType, intPtrType, int8T);
+ import(M, "_sym_read_memory", ptrT, intPtrType, intPtrType, int1T);
writeMemory = import(M, "_sym_write_memory", voidT, intPtrType, intPtrType,
- ptrT, int8T);
+ ptrT, int1T);
+ buildZeroBytes = import(M, "_sym_build_zero_bytes", ptrT, intPtrType);
buildInsert =
- import(M, "_sym_build_insert", ptrT, ptrT, ptrT, IRB.getInt64Ty(), int8T);
+ import(M, "_sym_build_insert", ptrT, ptrT, ptrT, IRB.getInt64Ty(), int1T);
buildExtract = import(M, "_sym_build_extract", ptrT, ptrT, IRB.getInt64Ty(),
- IRB.getInt64Ty(), int8T);
+ IRB.getInt64Ty(), int1T);
notifyCall = import(M, "_sym_notify_call", voidT, intPtrType);
notifyRet = import(M, "_sym_notify_ret", voidT, intPtrType);
@@ -160,10 +192,11 @@ Runtime::Runtime(Module &M) {
/// Decide whether a function is called symbolically.
bool isInterceptedFunction(const Function &f) {
static const StringSet<> kInterceptedFunctions = {
- "malloc", "calloc", "mmap", "mmap64", "open", "read", "lseek",
- "lseek64", "fopen", "fopen64", "fread", "fseek", "fseeko", "rewind",
- "fseeko64", "getc", "ungetc", "memcpy", "memset", "strncpy", "strchr",
- "memcmp", "memmove", "ntohl", "fgets", "fgetc", "getchar"};
+ "malloc", "calloc", "mmap", "mmap64", "open", "read",
+ "lseek", "lseek64", "fopen", "fopen64", "fread", "fseek",
+ "fseeko", "rewind", "fseeko64", "getc", "ungetc", "memcpy",
+ "memset", "strncpy", "strchr", "memcmp", "memmove", "ntohl",
+ "fgets", "fgetc", "getchar", "bcopy", "bcmp", "bzero"};
return (kInterceptedFunctions.count(f.getName()) > 0);
}
diff --git a/compiler/Runtime.h b/compiler/Runtime.h
index 7bf4a769..3f26c76d 100644
--- a/compiler/Runtime.h
+++ b/compiler/Runtime.h
@@ -19,9 +19,9 @@
#include
#if LLVM_VERSION_MAJOR >= 9 && LLVM_VERSION_MAJOR < 11
- using SymFnT = llvm::Value *;
+using SymFnT = llvm::Value *;
#else
- using SymFnT = llvm::FunctionCallee;
+using SymFnT = llvm::FunctionCallee;
#endif
/// Runtime functions
@@ -49,7 +49,21 @@ struct Runtime {
SymFnT buildBoolAnd{};
SymFnT buildBoolOr{};
SymFnT buildBoolXor{};
- SymFnT buildBoolToBits{};
+ SymFnT buildBoolToBit{};
+ SymFnT buildBitToBool{};
+ SymFnT buildAddOverflow{};
+ SymFnT buildSubOverflow{};
+ SymFnT buildMulOverflow{};
+ SymFnT buildSAddSat{};
+ SymFnT buildUAddSat{};
+ SymFnT buildSSubSat{};
+ SymFnT buildUSubSat{};
+ SymFnT buildSShlSat{};
+ SymFnT buildUShlSat{};
+ SymFnT buildFshl{};
+ SymFnT buildFshr{};
+ SymFnT buildAbs{};
+ SymFnT buildConcat{};
SymFnT pushPathConstraint{};
SymFnT getParameterExpression{};
SymFnT setParameterExpression{};
@@ -60,6 +74,7 @@ struct Runtime {
SymFnT memmove{};
SymFnT readMemory{};
SymFnT writeMemory{};
+ SymFnT buildZeroBytes{};
SymFnT buildInsert{};
SymFnT buildExtract{};
SymFnT notifyCall{};
@@ -68,13 +83,15 @@ struct Runtime {
/// Mapping from icmp predicates to the functions that build the corresponding
/// symbolic expressions.
- std::array
- comparisonHandlers{};
+ std::array comparisonHandlers{};
/// Mapping from binary operators to the functions that build the
/// corresponding symbolic expressions.
- std::array
- binaryOperatorHandlers{};
+ std::array binaryOperatorHandlers{};
+
+ /// Mapping from unary operators to the functions that build the
+ /// corresponding symbolic expressions.
+ std::array unaryOperatorHandlers{};
};
bool isInterceptedFunction(const llvm::Function &f);
diff --git a/compiler/Symbolizer.cpp b/compiler/Symbolizer.cpp
index a6206823..d111c52d 100644
--- a/compiler/Symbolizer.cpp
+++ b/compiler/Symbolizer.cpp
@@ -180,15 +180,9 @@ void Symbolizer::handleIntrinsicCall(CallBase &I) {
auto *callee = I.getCalledFunction();
switch (callee->getIntrinsicID()) {
- case Intrinsic::lifetime_start:
- case Intrinsic::lifetime_end:
- case Intrinsic::dbg_declare:
case Intrinsic::dbg_value:
case Intrinsic::is_constant:
case Intrinsic::trap:
- case Intrinsic::invariant_start:
- case Intrinsic::invariant_end:
- case Intrinsic::assume:
// These are safe to ignore.
break;
case Intrinsic::memcpy: {
@@ -258,22 +252,13 @@ void Symbolizer::handleIntrinsicCall(CallBase &I) {
registerSymbolicComputation(abs, &I);
break;
}
- case Intrinsic::cttz:
- case Intrinsic::ctpop:
- case Intrinsic::ctlz: {
- // Various bit-count operations. Expressing these symbolically is
- // difficult, so for now we just concretize.
-
- errs() << "Warning: losing track of symbolic expressions at bit-count "
- "operation "
- << I << "\n";
- break;
- }
- case Intrinsic::returnaddress: {
+ case Intrinsic::returnaddress:
+ case Intrinsic::frameaddress:
+ case Intrinsic::addressofreturnaddress: {
// Obtain the return address of the current function or one of its parents
// on the stack. We just concretize.
- errs() << "Warning: using concrete value for return address\n";
+ errs() << "Warning: using concrete value for return/frame address\n";
break;
}
case Intrinsic::bswap: {
@@ -284,6 +269,74 @@ void Symbolizer::handleIntrinsicCall(CallBase &I) {
registerSymbolicComputation(swapped, &I);
break;
}
+
+// Overflow arithmetic
+#define DEF_OVF_ARITH_BUILDER(intrinsic_op, runtime_name) \
+ case Intrinsic::s##intrinsic_op##_with_overflow: \
+ case Intrinsic::u##intrinsic_op##_with_overflow: { \
+ IRBuilder<> IRB(&I); \
+ \
+ bool isSigned = \
+ I.getIntrinsicID() == Intrinsic::s##intrinsic_op##_with_overflow; \
+ auto overflow = buildRuntimeCall( \
+ IRB, runtime.build##runtime_name, \
+ {{I.getOperand(0), true}, \
+ {I.getOperand(1), true}, \
+ {IRB.getInt1(isSigned), false}, \
+ {IRB.getInt1(dataLayout.isLittleEndian() ? 1 : 0), false}}); \
+ registerSymbolicComputation(overflow, &I); \
+ \
+ break; \
+ }
+
+ DEF_OVF_ARITH_BUILDER(add, AddOverflow)
+ DEF_OVF_ARITH_BUILDER(sub, SubOverflow)
+ DEF_OVF_ARITH_BUILDER(mul, MulOverflow)
+
+#undef DEF_OVF_ARITH_BUILDER
+
+// Saturating arithmetic
+#define DEF_SAT_ARITH_BUILDER(intrinsic_op, runtime_name) \
+ case Intrinsic::intrinsic_op##_sat: { \
+ IRBuilder<> IRB(&I); \
+ auto result = buildRuntimeCall(IRB, runtime.build##runtime_name, \
+ {I.getOperand(0), I.getOperand(1)}); \
+ registerSymbolicComputation(result, &I); \
+ break; \
+ }
+
+ DEF_SAT_ARITH_BUILDER(sadd, SAddSat)
+ DEF_SAT_ARITH_BUILDER(uadd, UAddSat)
+ DEF_SAT_ARITH_BUILDER(ssub, SSubSat)
+ DEF_SAT_ARITH_BUILDER(usub, USubSat)
+#if LLVM_VERSION_MAJOR > 11
+ DEF_SAT_ARITH_BUILDER(sshl, SShlSat)
+ DEF_SAT_ARITH_BUILDER(ushl, UShlSat)
+#endif
+
+#undef DEF_SAT_ARITH_BUILDER
+
+ case Intrinsic::fshl:
+ case Intrinsic::fshr: {
+ IRBuilder<> IRB(&I);
+ auto funnelShift = buildRuntimeCall(
+ IRB,
+ I.getIntrinsicID() == Intrinsic::fshl ? runtime.buildFshl
+ : runtime.buildFshr,
+ {I.getOperand(0), I.getOperand(1), I.getOperand(2)});
+ registerSymbolicComputation(funnelShift, &I);
+ break;
+ }
+#if LLVM_VERSION_MAJOR > 11
+ case Intrinsic::abs: {
+ // Integer absolute value
+
+ IRBuilder<> IRB(&I);
+ auto abs = buildRuntimeCall(IRB, runtime.buildAbs, I.getOperand(0));
+ registerSymbolicComputation(abs, &I);
+ break;
+ }
+#endif
default:
errs() << "Warning: unhandled LLVM intrinsic " << callee->getName()
<< "; the result will be concretized\n";
@@ -369,6 +422,15 @@ void Symbolizer::visitBinaryOperator(BinaryOperator &I) {
registerSymbolicComputation(runtimeCall, &I);
}
+void Symbolizer::visitUnaryOperator(UnaryOperator &I) {
+ IRBuilder<> IRB(&I);
+ SymFnT handler = runtime.unaryOperatorHandlers.at(I.getOpcode());
+
+ assert(handler && "Unable to handle unary operator");
+ auto runtimeCall = buildRuntimeCall(IRB, handler, I.getOperand(0));
+ registerSymbolicComputation(runtimeCall, &I);
+}
+
void Symbolizer::visitSelectInst(SelectInst &I) {
// Select is like the ternary operator ("?:") in C. We push the (potentially
// negated) condition to the path constraints and copy the symbolic
@@ -380,6 +442,13 @@ void Symbolizer::visitSelectInst(SelectInst &I) {
{I.getCondition(), false},
{getTargetPreferredInt(&I), false}});
registerSymbolicComputation(runtimeCall);
+ if (getSymbolicExpression(I.getTrueValue()) ||
+ getSymbolicExpression(I.getFalseValue())) {
+ auto *data = IRB.CreateSelect(
+ I.getCondition(), getSymbolicExpressionOrNull(I.getTrueValue()),
+ getSymbolicExpressionOrNull(I.getFalseValue()));
+ symbolicExpressions[&I] = data;
+ }
}
void Symbolizer::visitCmpInst(CmpInst &I) {
@@ -465,14 +534,9 @@ void Symbolizer::visitLoadInst(LoadInst &I) {
runtime.readMemory,
{IRB.CreatePtrToInt(addr, intPtrType),
ConstantInt::get(intPtrType, dataLayout.getTypeStoreSize(dataType)),
- ConstantInt::get(IRB.getInt8Ty(), isLittleEndian(dataType) ? 1 : 0)});
-
- if (dataType->isFloatingPointTy()) {
- data = IRB.CreateCall(runtime.buildBitsToFloat,
- {data, IRB.getInt1(dataType->isDoubleTy())});
- }
+ IRB.getInt1(isLittleEndian(dataType) ? 1 : 0)});
- symbolicExpressions[&I] = data;
+ symbolicExpressions[&I] = convertBitVectorExprForType(IRB, data, dataType);
}
void Symbolizer::visitStoreInst(StoreInst &I) {
@@ -480,18 +544,22 @@ void Symbolizer::visitStoreInst(StoreInst &I) {
tryAlternative(IRB, I.getPointerOperand());
- auto *data = getSymbolicExpressionOrNull(I.getValueOperand());
- auto *dataType = I.getValueOperand()->getType();
- if (dataType->isFloatingPointTy()) {
- data = IRB.CreateCall(runtime.buildFloatToBits, data);
- }
+ // Make sure that the expression corresponding to the stored value is of
+ // bit-vector kind. Shortcutting the runtime calls that we emit here (e.g.,
+ // for floating-point values) is tricky, so instead we make sure that any
+ // runtime function we call can handle null expressions.
+
+ auto V = I.getValueOperand();
+ auto maybeConversion =
+ convertExprForTypeToBitVectorExpr(IRB, V, getSymbolicExpression(V));
IRB.CreateCall(
runtime.writeMemory,
{IRB.CreatePtrToInt(I.getPointerOperand(), intPtrType),
- ConstantInt::get(intPtrType, dataLayout.getTypeStoreSize(dataType)),
- data,
- ConstantInt::get(IRB.getInt8Ty(), dataLayout.isLittleEndian() ? 1 : 0)});
+ ConstantInt::get(intPtrType, dataLayout.getTypeStoreSize(V->getType())),
+ maybeConversion ? maybeConversion->lastInstruction
+ : getSymbolicExpressionOrNull(V),
+ IRB.getInt1(isLittleEndian(V->getType()) ? 1 : 0)});
}
void Symbolizer::visitGetElementPtrInst(GetElementPtrInst &I) {
@@ -612,11 +680,25 @@ void Symbolizer::visitBitCastInst(BitCastInst &I) {
void Symbolizer::visitTruncInst(TruncInst &I) {
IRBuilder<> IRB(&I);
- auto trunc = buildRuntimeCall(
+
+ if (getSymbolicExpression(I.getOperand(0)) == nullptr)
+ return;
+
+ SymbolicComputation symbolicComputation;
+ symbolicComputation.merge(forceBuildRuntimeCall(
IRB, runtime.buildTrunc,
{{I.getOperand(0), true},
- {IRB.getInt8(I.getDestTy()->getIntegerBitWidth()), false}});
- registerSymbolicComputation(trunc, &I);
+ {IRB.getInt8(I.getDestTy()->getIntegerBitWidth()), false}}));
+
+ if (I.getDestTy()->isIntegerTy() &&
+ I.getDestTy()->getIntegerBitWidth() == 1) {
+ // convert from byte back to a bool (i1)
+ symbolicComputation.merge(
+ forceBuildRuntimeCall(IRB, runtime.buildBitToBool,
+ {{symbolicComputation.lastInstruction, false}}));
+ }
+
+ registerSymbolicComputation(symbolicComputation, &I);
}
void Symbolizer::visitIntToPtrInst(IntToPtrInst &I) {
@@ -696,30 +778,36 @@ void Symbolizer::visitCastInst(CastInst &I) {
IRBuilder<> IRB(&I);
+ SymFnT target;
+
+ switch (I.getOpcode()) {
+ case Instruction::SExt:
+ target = runtime.buildSExt;
+ break;
+ case Instruction::ZExt:
+ target = runtime.buildZExt;
+ break;
+ default:
+ llvm_unreachable("Unknown cast opcode");
+ }
+
// LLVM bitcode represents Boolean values as i1. In Z3, those are a not a
// bit-vector sort, so trying to cast one into a bit vector of any length
// raises an error. The run-time library provides a dedicated conversion
// function for this case.
if (I.getSrcTy()->getIntegerBitWidth() == 1) {
- auto boolToBitConversion = buildRuntimeCall(
- IRB, runtime.buildBoolToBits,
- {{I.getOperand(0), true},
- {IRB.getInt8(I.getDestTy()->getIntegerBitWidth()), false}});
- registerSymbolicComputation(boolToBitConversion, &I);
- } else {
- SymFnT target;
- switch (I.getOpcode()) {
- case Instruction::SExt:
- target = runtime.buildSExt;
- break;
- case Instruction::ZExt:
- target = runtime.buildZExt;
- break;
- default:
- llvm_unreachable("Unknown cast opcode");
- }
+ SymbolicComputation symbolicComputation;
+ symbolicComputation.merge(forceBuildRuntimeCall(IRB, runtime.buildBoolToBit,
+ {{I.getOperand(0), true}}));
+ symbolicComputation.merge(forceBuildRuntimeCall(
+ IRB, target,
+ {{symbolicComputation.lastInstruction, false},
+ {IRB.getInt8(I.getDestTy()->getIntegerBitWidth() - 1), false}}));
+
+ registerSymbolicComputation(symbolicComputation, &I);
+ } else {
auto symbolicCast =
buildRuntimeCall(IRB, target,
{{I.getOperand(0), true},
@@ -751,28 +839,61 @@ void Symbolizer::visitPHINode(PHINode &I) {
void Symbolizer::visitInsertValueInst(InsertValueInst &I) {
IRBuilder<> IRB(&I);
- auto insert = buildRuntimeCall(
- IRB, runtime.buildInsert,
- {{I.getAggregateOperand(), true},
- {I.getInsertedValueOperand(), true},
- {IRB.getInt64(aggregateMemberOffset(I.getAggregateOperand()->getType(),
- I.getIndices())),
- false},
- {IRB.getInt8(isLittleEndian(I.getInsertedValueOperand()->getType()) ? 1 : 0), false}});
- registerSymbolicComputation(insert, &I);
+ auto target = I.getAggregateOperand();
+ auto insertedValue = I.getInsertedValueOperand();
+
+ if (getSymbolicExpression(target) == nullptr &&
+ getSymbolicExpression(insertedValue) == nullptr)
+ return;
+
+ // We may have to convert the expression to bit-vector kind...
+ auto maybeConversion = convertExprForTypeToBitVectorExpr(
+ IRB, insertedValue, getSymbolicExpressionOrNull(insertedValue));
+
+ auto insert = IRB.CreateCall(
+ runtime.buildInsert,
+ {getSymbolicExpressionOrNull(target),
+ // If we had to convert the expression, use the result of the conversion.
+ maybeConversion ? maybeConversion->lastInstruction
+ : getSymbolicExpressionOrNull(insertedValue),
+ IRB.getInt64(aggregateMemberOffset(target->getType(), I.getIndices())),
+ IRB.getInt1(isLittleEndian(insertedValue->getType()) ? 1 : 0)});
+ auto insertComputation =
+ SymbolicComputation(insert, insert, {Input(target, 0, insert)});
+
+ if (!maybeConversion) {
+ // If we didn't have to convert, then the inserted value is first used in
+ // the insertion.
+ insertComputation.inputs.push_back(Input(insertedValue, 1, insert));
+ } else {
+ // Otherwise, the full computation consists of the conversion followed by
+ // the insertion.
+ maybeConversion->merge(insertComputation);
+ }
+
+ registerSymbolicComputation(maybeConversion.value_or(insertComputation), &I);
}
void Symbolizer::visitExtractValueInst(ExtractValueInst &I) {
IRBuilder<> IRB(&I);
- auto extract = buildRuntimeCall(
- IRB, runtime.buildExtract,
- {{I.getAggregateOperand(), true},
- {IRB.getInt64(aggregateMemberOffset(I.getAggregateOperand()->getType(),
- I.getIndices())),
- false},
- {IRB.getInt64(dataLayout.getTypeStoreSize(I.getType())), false},
- {IRB.getInt8(isLittleEndian(I.getType()) ? 1 : 0), false}});
- registerSymbolicComputation(extract, &I);
+ auto target = I.getAggregateOperand();
+ auto targetExpr = getSymbolicExpression(target);
+ auto resultType = I.getType();
+
+ if (targetExpr == nullptr)
+ return;
+
+ auto extractedBits = IRB.CreateCall(
+ runtime.buildExtract,
+ {targetExpr,
+ IRB.getInt64(aggregateMemberOffset(target->getType(), I.getIndices())),
+ IRB.getInt64(dataLayout.getTypeStoreSize(resultType)),
+ IRB.getInt1(isLittleEndian(resultType) ? 1 : 0)});
+
+ Instruction *result =
+ convertBitVectorExprForType(IRB, extractedBits, resultType);
+ registerSymbolicComputation(
+ {extractedBits, result, {{target, 0, extractedBits}}}, &I);
}
void Symbolizer::visitSwitchInst(SwitchInst &I) {
@@ -818,7 +939,7 @@ void Symbolizer::visitInstruction(Instruction &I) {
<< "; the result will be concretized\n";
}
-CallInst *Symbolizer::createValueExpression(Value *V, IRBuilder<> &IRB) {
+Instruction *Symbolizer::createValueExpression(Value *V, IRBuilder<> &IRB) {
auto *valueType = V->getType();
if (isa(V)) {
@@ -860,12 +981,12 @@ CallInst *Symbolizer::createValueExpression(Value *V, IRBuilder<> &IRB) {
{IRB.CreatePtrToInt(V, IRB.getInt64Ty()), IRB.getInt8(ptrBits)});
}
- if (valueType->isStructTy()) {
+ if (auto structType = dyn_cast(valueType)) {
// In unoptimized code we may see structures in SSA registers. What we
// want is a single bit-vector expression describing their contents, but
- // unfortunately we can't take the address of a register. We fix the
- // problem with a hack: we write the register to memory and initialize the
- // expression from there.
+ // unfortunately we can't take the address of a register. What we do instead
+ // is to build the expression recursively by iterating over the elements of
+ // the structure.
//
// An alternative would be to change the representation of structures in
// SSA registers to "shadow structures" that contain one expression per
@@ -873,22 +994,80 @@ CallInst *Symbolizer::createValueExpression(Value *V, IRBuilder<> &IRB) {
// cast instructions, because expressions would have to be converted
// between different representations according to the type.
- auto *memory = IRB.CreateAlloca(V->getType());
- IRB.CreateStore(V, memory);
- return IRB.CreateCall(
- runtime.readMemory,
- {IRB.CreatePtrToInt(memory, intPtrType),
- ConstantInt::get(intPtrType,
- dataLayout.getTypeStoreSize(V->getType())),
- IRB.getInt8(0)});
+ if (isa(V)) {
+ // This is just an optimization for completely undefined structs; we
+ // create an all-zeros expression without iterating over the elements.
+ return IRB.CreateCall(
+ runtime.buildZeroBytes,
+ {ConstantInt::get(intPtrType,
+ dataLayout.getTypeStoreSize(valueType))});
+ } else {
+ // Iterate over the elements of the struct and concatenate the
+ // corresponding expressions (along with any padding that might be
+ // needed).
+
+ auto structLayout = dataLayout.getStructLayout(structType);
+ auto constantStructValue = dyn_cast(V);
+ size_t offset = 0; // The end of the expressed portion in bytes.
+ Instruction *expr = nullptr;
+ auto append = [&](Instruction *newExpr) {
+ expr = expr ? IRB.CreateCall(runtime.buildConcat, {expr, newExpr})
+ : newExpr;
+ };
+
+ for (size_t i = 0; i < structType->getNumElements(); i++) {
+ // Build an expression for any padding preceding the current element.
+ if (auto padding = structLayout->getElementOffset(i) - offset;
+ padding > 0) {
+ append(IRB.CreateCall(runtime.buildZeroBytes,
+ {ConstantInt::get(intPtrType, padding)}));
+ }
+
+ // Build the expression for the current element. If the struct is not a
+ // constant, we need to read the element with extractvalue.
+ auto element = constantStructValue
+ ? constantStructValue->getAggregateElement(i)
+ : IRB.CreateExtractValue(V, i);
+ auto elementExpr = createValueExpression(element, IRB);
+
+ // The expression may be of a different kind than bit vector; in this
+ // case, we need to convert it.
+ if (auto conversion =
+ convertExprForTypeToBitVectorExpr(IRB, element, elementExpr)) {
+ elementExpr = conversion->lastInstruction;
+ }
+
+ // If the element is represented in little-endian byte order in memory,
+ // swap the bytes.
+ auto elementType = structType->getElementType(i);
+ if (isLittleEndian(elementType) &&
+ dataLayout.getTypeStoreSize(elementType) > 1) {
+ elementExpr = IRB.CreateCall(runtime.buildBswap, {elementExpr});
+ }
+
+ append(elementExpr);
+
+ offset = structLayout->getElementOffset(i) +
+ dataLayout.getTypeStoreSize(structType->getElementType(i));
+ }
+
+ // Insert padding at the end, if any.
+ if (auto finalPadding = dataLayout.getTypeStoreSize(structType) - offset;
+ finalPadding > 0) {
+ append(IRB.CreateCall(runtime.buildZeroBytes,
+ {ConstantInt::get(intPtrType, finalPadding)}));
+ }
+
+ return expr;
+ }
}
llvm_unreachable("Unhandled type for constant expression");
}
-Symbolizer::SymbolicComputation
-Symbolizer::forceBuildRuntimeCall(IRBuilder<> &IRB, SymFnT function,
- ArrayRef> args) {
+Symbolizer::SymbolicComputation Symbolizer::forceBuildRuntimeCall(
+ IRBuilder<> &IRB, SymFnT function,
+ ArrayRef> args) const {
std::vector functionArgs;
for (const auto &[arg, symbolic] : args) {
functionArgs.push_back(symbolic ? getSymbolicExpressionOrNull(arg) : arg);
@@ -899,7 +1078,7 @@ Symbolizer::forceBuildRuntimeCall(IRBuilder<> &IRB, SymFnT function,
for (unsigned i = 0; i < args.size(); i++) {
const auto &[arg, symbolic] = args[i];
if (symbolic)
- inputs.push_back({arg, i, call});
+ inputs.push_back(Input(arg, i, call));
}
return SymbolicComputation(call, call, inputs);
@@ -916,7 +1095,7 @@ void Symbolizer::tryAlternative(IRBuilder<> &IRB, Value *V) {
runtime.pushPathConstraint,
{destAssertion, IRB.getInt1(true), getTargetPreferredInt(V)});
registerSymbolicComputation(SymbolicComputation(
- concreteDestExpr, pushAssertion, {{V, 0, destAssertion}}));
+ concreteDestExpr, pushAssertion, {Input(V, 0, destAssertion)}));
}
}
@@ -942,3 +1121,41 @@ uint64_t Symbolizer::aggregateMemberOffset(Type *aggregateType,
return offset;
}
+
+Instruction *Symbolizer::convertBitVectorExprForType(llvm::IRBuilder<> &IRB,
+ Instruction *I,
+ Type *T) const {
+ Instruction *result = I;
+
+ if (T->isFloatingPointTy()) {
+ result = IRB.CreateCall(runtime.buildBitsToFloat,
+ {I, IRB.getInt1(T->isDoubleTy())});
+ } else if (T->isIntegerTy() && T->getIntegerBitWidth() == 1) {
+ result = IRB.CreateCall(runtime.buildTrunc,
+ {I, ConstantInt::get(IRB.getInt8Ty(), 1)});
+ result = IRB.CreateCall(runtime.buildBitToBool, {result});
+ }
+
+ return result;
+}
+
+std::optional
+Symbolizer::convertExprForTypeToBitVectorExpr(IRBuilder<> &IRB, Value *V,
+ Value *Expr) const {
+ if (Expr == nullptr)
+ return {};
+
+ auto T = V->getType();
+
+ if (T->isFloatingPointTy()) {
+ auto floatBits = IRB.CreateCall(runtime.buildFloatToBits, {Expr});
+ return SymbolicComputation(floatBits, floatBits, {Input(V, 0, floatBits)});
+ } else if (T->isIntegerTy() && T->getIntegerBitWidth() == 1) {
+ auto bitExpr = IRB.CreateCall(runtime.buildBoolToBit, {Expr});
+ auto bitVectorExpr = IRB.CreateCall(runtime.buildZExt,
+ {bitExpr, IRB.getInt8(7 /* 1 byte */)});
+ return SymbolicComputation(bitExpr, bitVectorExpr, {Input(V, 0, bitExpr)});
+ } else {
+ return {};
+ }
+}
diff --git a/compiler/Symbolizer.h b/compiler/Symbolizer.h
index 8ab440af..808712ee 100644
--- a/compiler/Symbolizer.h
+++ b/compiler/Symbolizer.h
@@ -103,6 +103,7 @@ class Symbolizer : public llvm::InstVisitor {
// Implementation of InstVisitor
//
void visitBinaryOperator(llvm::BinaryOperator &I);
+ void visitUnaryOperator(llvm::UnaryOperator &I);
void visitSelectInst(llvm::SelectInst &I);
void visitCmpInst(llvm::CmpInst &I);
void visitReturnInst(llvm::ReturnInst &I);
@@ -142,6 +143,14 @@ class Symbolizer : public llvm::InstVisitor {
unsigned operandIndex;
llvm::Instruction *user;
+ Input() = default;
+
+ Input(llvm::Value *concrete, unsigned idx, llvm::Instruction *user)
+ : concreteValue(concrete), operandIndex(idx), user(user) {
+ assert(getSymbolicOperand()->getType() ==
+ llvm::Type::getInt8PtrTy(user->getContext()));
+ }
+
llvm::Value *getSymbolicOperand() const {
return user->getOperand(operandIndex);
}
@@ -186,22 +195,23 @@ class Symbolizer : public llvm::InstVisitor {
<< "\n...ending at " << *computation.lastInstruction
<< "\n...with inputs:\n";
for (const auto &input : computation.inputs) {
- out << '\t' << *input.concreteValue << '\n';
+ out << '\t' << *input.concreteValue << " => " << *input.user << '\n';
}
return out;
}
};
/// Create an expression that represents the concrete value.
- llvm::CallInst *createValueExpression(llvm::Value *V, llvm::IRBuilder<> &IRB);
+ llvm::Instruction *createValueExpression(llvm::Value *V,
+ llvm::IRBuilder<> &IRB);
/// Get the (already created) symbolic expression for a value.
- llvm::Value *getSymbolicExpression(llvm::Value *V) {
+ llvm::Value *getSymbolicExpression(llvm::Value *V) const {
auto exprIt = symbolicExpressions.find(V);
return (exprIt != symbolicExpressions.end()) ? exprIt->second : nullptr;
}
- llvm::Value *getSymbolicExpressionOrNull(llvm::Value *V) {
+ llvm::Value *getSymbolicExpressionOrNull(llvm::Value *V) const {
auto *expr = getSymbolicExpression(V);
if (expr == nullptr)
return llvm::ConstantPointerNull::get(
@@ -214,9 +224,9 @@ class Symbolizer : public llvm::InstVisitor {
}
/// Like buildRuntimeCall, but the call is always generated.
- SymbolicComputation
- forceBuildRuntimeCall(llvm::IRBuilder<> &IRB, SymFnT function,
- llvm::ArrayRef> args);
+ SymbolicComputation forceBuildRuntimeCall(
+ llvm::IRBuilder<> &IRB, SymFnT function,
+ llvm::ArrayRef> args) const;
/// Create a call to the specified function in the run-time library.
///
@@ -229,7 +239,7 @@ class Symbolizer : public llvm::InstVisitor {
/// instruction is emitted and the function returns null.
std::optional
buildRuntimeCall(llvm::IRBuilder<> &IRB, SymFnT function,
- llvm::ArrayRef> args) {
+ llvm::ArrayRef> args) const {
if (std::all_of(args.begin(), args.end(),
[this](std::pair arg) {
return (getSymbolicExpression(arg.first) == nullptr);
@@ -243,7 +253,7 @@ class Symbolizer : public llvm::InstVisitor {
/// Convenience overload that treats all arguments as symbolic.
std::optional
buildRuntimeCall(llvm::IRBuilder<> &IRB, SymFnT function,
- llvm::ArrayRef symbolicArgs) {
+ llvm::ArrayRef symbolicArgs) const {
std::vector> args;
for (const auto &arg : symbolicArgs) {
args.emplace_back(arg, true);
@@ -298,6 +308,27 @@ class Symbolizer : public llvm::InstVisitor {
uint64_t aggregateMemberOffset(llvm::Type *aggregateType,
llvm::ArrayRef indices) const;
+ /// Emit code that converts the bit-vector expression represented by I to an
+ /// expression that is appropriate for T; return the instruction that computes
+ /// the result (which may be I if no conversion is needed).
+ ///
+ /// The solver doesn't represent all values as bit vectors. For example,
+ /// floating-point values and Booleans are of separate kinds, so we emit code
+ /// that changes the solver kind of the expression to whatever is needed.
+ llvm::Instruction *convertBitVectorExprForType(llvm::IRBuilder<> &IRB,
+ llvm::Instruction *I,
+ llvm::Type *T) const;
+
+ /// Emit code that converts the expression Expr for V to a bit-vector
+ /// expression. Return the SymbolicComputation representing the conversion
+ /// (if a conversion is necessary); the last instruction computes the result.
+ ///
+ /// This is the inverse operation of convertBitVectorExprForType (see details
+ /// there).
+ std::optional
+ convertExprForTypeToBitVectorExpr(llvm::IRBuilder<> &IRB, llvm::Value *V,
+ llvm::Value *Expr) const;
+
const Runtime runtime;
/// The data layout of the currently processed module.
diff --git a/compiler/sym++.in b/compiler/sym++.in
index 82221945..2b775739 100755
--- a/compiler/sym++.in
+++ b/compiler/sym++.in
@@ -55,7 +55,7 @@ if [ $# -eq 0 ]; then
fi
exec $compiler \
- -Xclang -load -Xclang "$pass" \
+ @CLANG_LOAD_PASS@"$pass" \
$stdlib_cflags \
"$@" \
$stdlib_ldflags \
diff --git a/compiler/symcc.in b/compiler/symcc.in
index a0694c06..4e0ad37e 100755
--- a/compiler/symcc.in
+++ b/compiler/symcc.in
@@ -39,7 +39,7 @@ if [ $# -eq 0 ]; then
fi
exec $compiler \
- -Xclang -load -Xclang "$pass" \
+ @CLANG_LOAD_PASS@"$pass" \
"$@" \
-L"$runtime_dir" \
-lSymRuntime \
diff --git a/docs/32-bit.txt b/docs/32-bit.txt
index f5f6dda8..eae0e9cb 100644
--- a/docs/32-bit.txt
+++ b/docs/32-bit.txt
@@ -26,12 +26,12 @@ install the 32-bit version of Z3 in your system.
Once the dependencies for 32-bit SymCC are available (as well as the 64-bit
dependencies mentioned in the main README), configure and build SymCC as usual
but add "-DTARGET_32BIT=ON" to the CMake invocation. If the build system doesn't
-find your 32-bit versions of LLVM and Z3, specify their locations with
+find your 32-bit versions of LLVM and Z3, and specify their locations with
"-DLLVM_32BIT_DIR=/some/path" and "-DZ3_32BIT_DIR=/some/other/path",
respectively - analogously to how you would hint at the 64-bit versions.
The resulting "symcc" and "sym++" scripts work like regular SymCC, but they
-additionally understand the "-m32" switch, which tells clang to build 32-bit
+additionally understand the "-m32" switch, which tells Clang to build 32-bit
artifacts. If you build anything with "-m32", SymCC will make sure that the
32-bit version of the symbolic backend is linked to it instead of the 64-bit
variant that would normally be used. Note that, in order to compile C++ code
diff --git a/docs/Backends.txt b/docs/Backends.txt
index 358412b1..ec3e53ff 100644
--- a/docs/Backends.txt
+++ b/docs/Backends.txt
@@ -13,7 +13,7 @@ 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" defined to be something of pointer width).
+"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
diff --git a/docs/Concreteness.txt b/docs/Concreteness.txt
index 91eba7a2..26d0e9a1 100644
--- a/docs/Concreteness.txt
+++ b/docs/Concreteness.txt
@@ -18,9 +18,9 @@ There are two stages at which data can be identified as concrete:
If we detect in the compiler pass that a value is a compile-time constant (case
1 above), we do not emit code for symbolic handling at all. However, for any
-other type of data we need to generate code that handles the case of it being
+other type of data, we need to generate code that handles the case of it being
symbolic at run time. Concretely (no pun intended), we mark concrete values at
-run time by setting its corresponding symbolic expression in shadow memory to
+run time by setting their corresponding symbolic expression in shadow memory to
null. This makes it very cheap to check concreteness during execution: just run
a null check on the symbolic expression.
diff --git a/docs/Configuration.txt b/docs/Configuration.txt
index 123aec34..e1239151 100644
--- a/docs/Configuration.txt
+++ b/docs/Configuration.txt
@@ -9,7 +9,7 @@ SymCC is configured at two different stages:
compilation time and the set of dependencies. This is done via arguments to
CMake.
-2. When you run programs that have been compiled with SymCC, environment
+2. When you run programs that have been compiled with SymCC, the environment
variables control various aspects of the execution and analysis.
We list all available options for each stage in turn.
@@ -56,11 +56,19 @@ environment variables.
uninstrumented counterparts.
- SYMCC_OUTPUT_DIR (default "/tmp/output"): This is the directory where SymCC
- will store new inputs (QSYM backend only).
+ will store new inputs (QSYM backend only). If you prefer to handle them
+ programmatically, make your program call symcc_set_test_case_handler; the
+ handler will be called instead of the default handler each time the backend
+ generates a new input.
- SYMCC_INPUT_FILE (default empty): When empty, SymCC treats data read from
standard input as symbolic; when set to a file name, any data read from that
- file is considered symbolic.
+ file is considered symbolic. Ignored if SYMCC_NO_SYMBOLIC_INPUT is set to 1.
+
+- SYMCC_MEMORY_INPUT=0/1 (default 0): When set to 1, expect the program under
+ test to communicate symbolic inputs with one or more calls to
+ symcc_make_symbolic. Can't be combined with SYMCC_INPUT_FILE. Ignored if
+ SYMCC_NO_SYMBOLIC_INPUT is set to 1.
- SYMCC_LOG_FILE (default empty): When set to a file name, SymCC creates the
file (or overwrites any existing file!) and uses it to log backend activity
@@ -71,12 +79,15 @@ environment variables.
repeatedly (QSYM backend only). See the QSYM paper for details; highly
recommended for fuzzing and enabled automatically by the fuzzing helper.
-- SYMCC_AFL_COVERAGE_MAP (default empty): When set to the file name of an AFL
- coverage map, load the map before executing the target program and use it to
- skip solver queries for paths that have already been covered (QSYM backend
- only). The map is updated in place, so beware of races when running multiple
- instances of SymCC! The fuzzing helper uses this to remember the state of
- exploration across multiple executions of the target program.
+- SYMCC_AFL_COVERAGE_MAP (default empty): When set to the file name of an
+ AFL-style coverage map, load the map before executing the target program and
+ use it to skip solver queries for paths that have already been covered (QSYM
+ backend only). The map is updated in place, so beware of races when running
+ multiple instances of SymCC! The fuzzing helper uses this to remember the
+ state of exploration across multiple executions of the target program.
+ Warning: This setting has a misleading name - while the format of the map
+ follows (classic) AFL, the variable isn't meant to point at a map file that
+ AFL uses too!
(Most people should stop reading here.)
@@ -88,7 +99,7 @@ There is actually a third category of options: when compiling with SymCC, you
can specify the location of its various components via environment variables.
This is not necessary in most cases because the build system makes sure that all
components know about each other; however, in some advanced setups you may need
-to move files around after building them, and in that case you can use the
+to move files around after building them, and in that case, you can use the
variables documented below to communicate the new locations:
- SYMCC_RUNTIME_DIR and SYMCC_RUNTIME32_DIR: The directory that contains the
diff --git a/docs/Experiments.txt b/docs/Experiments.txt
index 81751a4a..001a06fc 100644
--- a/docs/Experiments.txt
+++ b/docs/Experiments.txt
@@ -8,6 +8,8 @@ Here we document how to reproduce the experiments that we show in the paper
are available on our website [1], which also provides our raw results. Feel free
to reach out to us if you encounter problems with reproducing the benchmarks.
+The datasets are also archived on figshare [10].
+
In the paper, we describe two sets of experiments: we first benchmark SymCC on
the CGC programs, then we run it on real-world software.
@@ -37,7 +39,7 @@ regular 32-bit binaries built by cb-multios.
The analysis of real-world software always follows the same procedure. Assuming
you have exported CC=symcc, CXX=sym++ and SYMCC_NO_SYMBOLIC_INPUT=1, first
-download the code, then build it using its own build system, finally unset
+download the code, then build it using its own build system, and finally unset
SYMCC_NO_SYMBOLIC_INPUT and analyze the program in concert with AFL (which
requires building a second time for AFL, see docs/Fuzzing.txt). We used AFL
2.56b and built the targets with AFL_USE_ASAN=1. Note that the fuzzing helper is
@@ -50,7 +52,7 @@ OpenJPEG [4]: we used revision 1f1e9682, built with CMake as described in the
files file1.jp2 and file8.jp2 [5].
libarchive [6]: we used revision 9ebb2484, built with CMake as described in the
- poject's INSTALL (but adding "-DCMAKE_BUILD_TYPE=Release"), and analyzed
+ project's INSTALL (but adding "-DCMAKE_BUILD_TYPE=Release"), and analyzed
"bin/bsdtar tf @@"; the corpus consisted of just a single dummy file
containing the character "A".
@@ -78,3 +80,4 @@ running it with AFL according to the QSYM authors' instructions [9].
[7] https://github.com/the-tcpdump-group/tcpdump.git
[8] https://github.com/the-tcpdump-group/libpcap.git
[9] https://github.com/sslab-gatech/qsym#run-hybrid-fuzzing-with-afl
+[10] https://doi.org/10.6084/m9.figshare.24270709.v1 or https://figshare.com/articles/dataset/SymCC_evaluation_data/24270709
diff --git a/docs/Ideas.txt b/docs/Ideas.txt
index a2720617..219236ae 100644
--- a/docs/Ideas.txt
+++ b/docs/Ideas.txt
@@ -35,7 +35,7 @@ because intermediate values are rarely computed without being used: typically,
they end up being inputs to future computations, so we couldn't free the
corresponding expressions anyway. A notable exception is the computation of
values only for output - the expressions for such values could be freed after
-the value is output, which would reduce memory consumption especially with
+the value is output, which would reduce memory consumption, especially with
output-heavy target programs.
@@ -63,6 +63,6 @@ improvements they have made over AFL (e.g., AFL++ or Honggfuzz).
Forking version
Instead of working with a fuzzer, we could also implement forking and some
-scheduling strategy ourselves. Georgia Tech has developed some OS-level
+scheduling strategies ourselves. Georgia Tech has developed some OS-level
primitives that could help to implement such a feature:
https://github.com/sslab-gatech/perf-fuzz.
diff --git a/docs/Libc.txt b/docs/Libc.txt
index 7057ec0e..08ad920e 100644
--- a/docs/Libc.txt
+++ b/docs/Libc.txt
@@ -11,7 +11,7 @@ as the sanitizers and intercept calls to libc functions, wrapping them with
symbolic handling. For example, the wrapper for "memset" obtains the symbolic
expression for the value to be written in memory and pushes it to the shadow
region of the destination memory. In the future, we may experiment with
-compiling (parts of) libc to avoid the effort of manually defining wrappers.
+compiling (parts of) the libc to avoid the effort of manually defining wrappers.
Initially, we tried the interception mechanism that the LLVM sanitizers use,
implemented in the compiler-rt library. The Linux version basically just defines
@@ -25,11 +25,11 @@ replaces a given libc function, in the executable and in all libraries that it
loads. However, our run-time support library is loaded into the same process and
makes heavy use of libc, so we need the ability to use wrappers in one part of
the program and concrete functions in another. This turned out to complicate the
-compiler-rt based implementation so much that we eventually abandoned the
+compiler-rt-based implementation so much that we eventually abandoned the
approach.
Function renaming provided a convenient alternative: we control all code that is
-supposed to call wrappers rather the libc functions proper, so we just rename
+supposed to call wrappers rather than the libc functions properly, so we just rename
the targets of their calls. For example, a call to "memset" in the program under
test is turned into a call to "memset_symbolized", which we can easily define as
a regular function wrapping "memset". Calls from our run-time library, on the
diff --git a/docs/Optimization.txt b/docs/Optimization.txt
index 6b4f2c83..97efdbc2 100644
--- a/docs/Optimization.txt
+++ b/docs/Optimization.txt
@@ -7,7 +7,7 @@ A popular technique for experimenting with compiler passes is to produce bitcode
with "clang -emit-llvm" and run the pass on the resulting bitcode with opt. Note
that this approach does not mix well with optimization: simply running "opt -O3"
on the instrumented bitcode yields inferior results. Why? In principle, the
-instrumentation that adds symbolic-execution capabilities does not interfere
+instrumentation that adds symbolic execution capabilities does not interfere
with the compiler's regular optimization. However, while "opt -O3" runs the same
middle-end optimizations as clang does internally, "clang -O3" performs
additional analysis before invoking the middle end. In particular, type-based
diff --git a/runtime/CMakeLists.txt b/runtime/CMakeLists.txt
index 637fc1ce..07277b8f 100644
--- a/runtime/CMakeLists.txt
+++ b/runtime/CMakeLists.txt
@@ -1,16 +1,17 @@
-# This file is part of SymCC.
+# This file is part of the SymCC runtime.
#
-# 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.
+# 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.
#
-# 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.
+# 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 General Public License along with
-# SymCC. If not, see .
+# 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)
diff --git a/runtime/Config.cpp b/runtime/Config.cpp
index c7d45ee0..23a28df6 100644
--- a/runtime/Config.cpp
+++ b/runtime/Config.cpp
@@ -1,16 +1,17 @@
-// This file is part of SymCC.
+// This file is part of the SymCC runtime.
//
-// 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.
+// 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.
//
-// 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.
+// 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 General Public License along with
-// SymCC. If not, see .
+// You should have received a copy of the GNU Lesser General Public License
+// along with the SymCC runtime. If not, see .
#include "Config.h"
@@ -19,6 +20,7 @@
#include
#include
#include
+#include
namespace {
@@ -41,17 +43,26 @@ bool checkFlagString(std::string value) {
Config g_config;
void loadConfig() {
- auto *fullyConcrete = getenv("SYMCC_NO_SYMBOLIC_INPUT");
- if (fullyConcrete != nullptr)
- g_config.fullyConcrete = checkFlagString(fullyConcrete);
-
auto *outputDir = getenv("SYMCC_OUTPUT_DIR");
if (outputDir != nullptr)
g_config.outputDir = outputDir;
auto *inputFile = getenv("SYMCC_INPUT_FILE");
if (inputFile != nullptr)
- g_config.inputFile = inputFile;
+ 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)
@@ -76,7 +87,8 @@ void loadConfig() {
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();
+ 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
index 450344eb..a866821c 100644
--- a/runtime/Config.h
+++ b/runtime/Config.h
@@ -1,32 +1,48 @@
-// This file is part of SymCC.
+// This file is part of the SymCC runtime.
//
-// 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.
+// 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.
//
-// 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.
+// 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 General Public License along with
-// SymCC. If not, see .
+// 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 {
- /// Should we allow symbolic data in the program?
- bool fullyConcrete = false;
+ 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 input file, if any.
- std::string inputFile;
-
/// The file to log constraint solving information to.
std::string logFile = "";
diff --git a/runtime/GarbageCollection.cpp b/runtime/GarbageCollection.cpp
index 8c1edc37..8afdd327 100644
--- a/runtime/GarbageCollection.cpp
+++ b/runtime/GarbageCollection.cpp
@@ -1,16 +1,17 @@
-// This file is part of SymCC.
+// This file is part of the SymCC runtime.
//
-// 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.
+// 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.
//
-// 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.
+// 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 General Public License along with
-// SymCC. If not, see .
+// You should have received a copy of the GNU Lesser General Public License
+// along with SymCC. If not, see .
#include "GarbageCollection.h"
diff --git a/runtime/GarbageCollection.h b/runtime/GarbageCollection.h
index da77ff83..81b0b8c2 100644
--- a/runtime/GarbageCollection.h
+++ b/runtime/GarbageCollection.h
@@ -1,16 +1,17 @@
-// This file is part of SymCC.
+// This file is part of the SymCC runtime.
//
-// 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.
+// 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.
//
-// 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.
+// 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 General Public License along with
-// SymCC. If not, see .
+// 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
diff --git a/runtime/LibcWrappers.cpp b/runtime/LibcWrappers.cpp
index 319ae9f5..cfe55525 100644
--- a/runtime/LibcWrappers.cpp
+++ b/runtime/LibcWrappers.cpp
@@ -1,16 +1,33 @@
-// This file is part of SymCC.
+// This file is part of the SymCC runtime.
//
-// 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.
+// 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.
//
-// 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.
+// 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 General Public License along with
-// SymCC. If not, see .
+// 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
@@ -18,6 +35,7 @@
#include
#include
#include
+#include
#include
#include
@@ -56,13 +74,28 @@ template
void tryAlternative(E *value, SymExpr valueExpr, F caller) {
tryAlternative(reinterpret_cast(value), valueExpr, caller);
}
-} // namespace
-void initLibcWrappers() {
- if (g_config.fullyConcrete)
+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 (g_config.inputFile.empty()) {
+ 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;
}
@@ -95,10 +128,31 @@ void *SYM(calloc)(size_t nmemb, size_t size) {
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));
- _sym_set_return_expression(nullptr);
return result;
}
@@ -111,15 +165,8 @@ 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 && !g_config.fullyConcrete && !g_config.inputFile.empty() &&
- strstr(path, g_config.inputFile.c_str()) != nullptr) {
- if (inputFileDescriptor != -1)
- std::cerr << "Warning: input file opened multiple times; this is not yet "
- "supported"
- << std::endl;
- inputFileDescriptor = result;
- inputOffset = 0;
- }
+ if (result >= 0)
+ maybeSetInputFile(path, result);
return result;
}
@@ -136,9 +183,8 @@ ssize_t SYM(read)(int fildes, void *buf, size_t nbyte) {
if (fildes == inputFileDescriptor) {
// Reading symbolic input.
- ReadWriteShadow shadow(buf, result);
- std::generate(shadow.begin(), shadow.end(),
- []() { return _sym_get_input_byte(inputOffset++); });
+ _sym_make_symbolic(buf, result, inputOffset);
+ inputOffset += result;
} else if (!isConcrete(buf, result)) {
ReadWriteShadow shadow(buf, result);
std::fill(shadow.begin(), shadow.end(), nullptr);
@@ -193,16 +239,8 @@ FILE *SYM(fopen)(const char *pathname, const char *mode) {
auto *result = fopen(pathname, mode);
_sym_set_return_expression(nullptr);
- if (result != nullptr && !g_config.fullyConcrete &&
- !g_config.inputFile.empty() &&
- strstr(pathname, g_config.inputFile.c_str()) != nullptr) {
- if (inputFileDescriptor != -1)
- std::cerr << "Warning: input file opened multiple times; this is not yet "
- "supported"
- << std::endl;
- inputFileDescriptor = fileno(result);
- inputOffset = 0;
- }
+ if (result != nullptr)
+ maybeSetInputFile(pathname, fileno(result));
return result;
}
@@ -211,16 +249,8 @@ FILE *SYM(fopen64)(const char *pathname, const char *mode) {
auto *result = fopen64(pathname, mode);
_sym_set_return_expression(nullptr);
- if (result != nullptr && !g_config.fullyConcrete &&
- !g_config.inputFile.empty() &&
- strstr(pathname, g_config.inputFile.c_str()) != nullptr) {
- if (inputFileDescriptor != -1)
- std::cerr << "Warning: input file opened multiple times; this is not yet "
- "supported"
- << std::endl;
- inputFileDescriptor = fileno(result);
- inputOffset = 0;
- }
+ if (result != nullptr)
+ maybeSetInputFile(pathname, fileno(result));
return result;
}
@@ -235,9 +265,8 @@ size_t SYM(fread)(void *ptr, size_t size, size_t nmemb, FILE *stream) {
if (fileno(stream) == inputFileDescriptor) {
// Reading symbolic input.
- ReadWriteShadow shadow(ptr, result * size);
- std::generate(shadow.begin(), shadow.end(),
- []() { return _sym_get_input_byte(inputOffset++); });
+ _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);
@@ -255,9 +284,9 @@ char *SYM(fgets)(char *str, int n, FILE *stream) {
if (fileno(stream) == inputFileDescriptor) {
// Reading symbolic input.
- ReadWriteShadow shadow(str, sizeof(char) * strlen(str));
- std::generate(shadow.begin(), shadow.end(),
- []() { return _sym_get_input_byte(inputOffset++); });
+ 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);
@@ -338,7 +367,7 @@ int SYM(getc)(FILE *stream) {
if (fileno(stream) == inputFileDescriptor)
_sym_set_return_expression(_sym_build_zext(
- _sym_get_input_byte(inputOffset++), sizeof(int) * 8 - 8));
+ _sym_get_input_byte(inputOffset++, result), sizeof(int) * 8 - 8));
else
_sym_set_return_expression(nullptr);
@@ -354,16 +383,14 @@ int SYM(fgetc)(FILE *stream) {
if (fileno(stream) == inputFileDescriptor)
_sym_set_return_expression(_sym_build_zext(
- _sym_get_input_byte(inputOffset++), sizeof(int) * 8 - 8));
+ _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(getchar)(void) { return SYM(getc)(stdin); }
int SYM(ungetc)(int c, FILE *stream) {
auto result = ungetc(c, stream);
@@ -399,6 +426,20 @@ void *SYM(memset)(void *s, int c, size_t n) {
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));
@@ -412,6 +453,22 @@ void *SYM(memmove)(void *dest, const void *src, size_t n) {
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));
@@ -495,6 +552,43 @@ int SYM(memcmp)(const void *a, const void *b, size_t n) {
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);
diff --git a/runtime/LibcWrappers.h b/runtime/LibcWrappers.h
index d84c1f47..2304a3a0 100644
--- a/runtime/LibcWrappers.h
+++ b/runtime/LibcWrappers.h
@@ -1,16 +1,17 @@
-// This file is part of SymCC.
+// This file is part of the SymCC runtime.
//
-// 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.
+// 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.
//
-// 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.
+// 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 General Public License along with
-// SymCC. If not, see .
+// 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
diff --git a/runtime/RuntimeCommon.cpp b/runtime/RuntimeCommon.cpp
index 32081e3e..127c81de 100644
--- a/runtime/RuntimeCommon.cpp
+++ b/runtime/RuntimeCommon.cpp
@@ -1,23 +1,29 @@
-// This file is part of SymCC.
+// This file is part of the SymCC runtime.
//
-// 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.
+// 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.
//
-// 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.
+// 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 General Public License along with
-// SymCC. If not, see .
+// 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"
@@ -31,6 +37,51 @@ 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; }
@@ -68,6 +119,10 @@ void _sym_memset(uint8_t *memory, SymExpr value, size_t length) {
}
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;
@@ -171,7 +226,9 @@ SymExpr _sym_build_insert(SymExpr target, SymExpr to_insert, uint64_t offset,
SymExpr beforeInsert =
(offset == 0) ? nullptr : _sym_build_extract(target, 0, offset, false);
- SymExpr newPiece = little_endian ? _sym_build_bswap(to_insert) : to_insert;
+ 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 =
@@ -193,6 +250,239 @@ SymExpr _sym_build_insert(SymExpr target, SymExpr to_insert, uint64_t offset,
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
index f00176ea..4c05ceb0 100644
--- a/runtime/RuntimeCommon.h
+++ b/runtime/RuntimeCommon.h
@@ -3,32 +3,41 @@
// 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.
+// 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 SymCC.
+// This file is part of the SymCC runtime.
//
-// 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.
+// 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.
//
-// 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.
+// 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 General Public License along with
-// SymCC. If not, see .
+// 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
@@ -42,6 +51,7 @@ void _sym_initialize(void);
*/
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);
@@ -49,7 +59,7 @@ SymExpr _sym_build_false(void);
SymExpr _sym_build_bool(bool value);
/*
- * Arithmetic and shifts
+ * Integer arithmetic and shifts
*/
SymExpr _sym_build_neg(SymExpr expr);
SymExpr _sym_build_add(SymExpr a, SymExpr b);
@@ -62,13 +72,40 @@ 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
@@ -90,6 +127,7 @@ 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);
@@ -109,9 +147,9 @@ SymExpr _sym_build_float_unordered_not_equal(SymExpr a, SymExpr b);
/*
* Casts
*/
-SymExpr _sym_build_sext(SymExpr expr, uint8_t bits);
-SymExpr _sym_build_zext(SymExpr expr, uint8_t bits);
-SymExpr _sym_build_trunc(SymExpr expr, uint8_t bits);
+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);
@@ -119,7 +157,8 @@ 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_bits(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
@@ -131,27 +170,30 @@ size_t _sym_bits_helper(SymExpr expr);
/*
* Function-call helpers
*/
-void _sym_set_parameter_expression(uint8_t index, SymExpr expr);
+void _sym_set_parameter_expression(uint8_t index, nullable SymExpr expr);
SymExpr _sym_get_parameter_expression(uint8_t index);
-void _sym_set_return_expression(SymExpr expr);
+void _sym_set_return_expression(nullable SymExpr expr);
SymExpr _sym_get_return_expression(void);
/*
* Constraint handling
*/
-void _sym_push_path_constraint(SymExpr constraint, int taken,
+void _sym_push_path_constraint(nullable SymExpr constraint, int taken,
uintptr_t site_id);
-SymExpr _sym_get_input_byte(size_t offset);
+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, SymExpr expr,
+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,
@@ -176,8 +218,20 @@ bool _sym_feasible(SymExpr expr);
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
index 2b69a08a..2852fad1 100644
--- a/runtime/Shadow.cpp
+++ b/runtime/Shadow.cpp
@@ -1,16 +1,17 @@
-// This file is part of SymCC.
+// This file is part of the SymCC runtime.
//
-// 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.
+// 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.
//
-// 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.
+// 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 General Public License along with
-// SymCC. If not, see .
+// You should have received a copy of the GNU Lesser General Public License
+// along with SymCC. If not, see .
#include "Shadow.h"
diff --git a/runtime/Shadow.h b/runtime/Shadow.h
index 967e11ca..fe630bb4 100644
--- a/runtime/Shadow.h
+++ b/runtime/Shadow.h
@@ -1,16 +1,17 @@
-// This file is part of SymCC.
+// This file is part of the SymCC runtime.
//
-// 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.
+// 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.
//
-// 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.
+// 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 General Public License along with
-// SymCC. If not, see .
+// 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
@@ -18,7 +19,6 @@
#include
#include
#include
-#include
#include