Skip to content

Commit

Permalink
Reorganization of SymCC Runtime (#2)
Browse files Browse the repository at this point in the history
* Reorganize repository
* Symcc to SymCC
* Update bindings README
* Update README.md

---------

Co-authored-by: Aurelien Francillon <[email protected]>
  • Loading branch information
rmalmain and aurelf authored Apr 9, 2024
1 parent f8a0345 commit 91c0034
Show file tree
Hide file tree
Showing 22 changed files with 71 additions and 69 deletions.
2 changes: 1 addition & 1 deletion .gitmodules
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
[submodule "qsym_backend/qsym"]
path = qsym_backend/qsym
path = backends/qsym/qsym
url = https://github.com/eurecom-s3/qsym.git
branch = symcc
39 changes: 18 additions & 21 deletions CMakeLists.txt
Original file line number Diff line number Diff line change
Expand Up @@ -14,7 +14,7 @@
# with the SymCC runtime. If not, see <https://www.gnu.org/licenses/>.

cmake_minimum_required(VERSION 3.16)
project(SymccRuntime)
project(SymCCRuntime)

list(APPEND CMAKE_MODULE_PATH "${CMAKE_SOURCE_DIR}/cmake")

Expand All @@ -38,35 +38,32 @@ set(LLVM_VERSION "" CACHE STRING "LLVM version to use. The corresponding LLVM de
set(CMAKE_LIBRARY_OUTPUT_DIRECTORY ${CMAKE_BINARY_DIR})
set(CMAKE_ARCHIVE_OUTPUT_DIRECTORY ${CMAKE_BINARY_DIR})

set(SYMCC_RT_SRC_DIR "${CMAKE_CURRENT_SOURCE_DIR}/src")
set(SYMCC_RT_INCLUDE_DIR "${CMAKE_CURRENT_SOURCE_DIR}/include")
set(SYMCC_RT_BACKEND_DIR "${CMAKE_CURRENT_SOURCE_DIR}/backends/${SYMCC_RT_BACKEND}")

# There is list(TRANSFORM ... PREPEND ...), but it's not available before CMake 3.12.
set(SHARED_RUNTIME_SOURCES
${CMAKE_CURRENT_SOURCE_DIR}/Config.cpp
${CMAKE_CURRENT_SOURCE_DIR}/RuntimeCommon.cpp
${CMAKE_CURRENT_SOURCE_DIR}/LibcWrappers.cpp
${CMAKE_CURRENT_SOURCE_DIR}/Shadow.cpp
${CMAKE_CURRENT_SOURCE_DIR}/GarbageCollection.cpp)
${SYMCC_RT_SRC_DIR}/Config.cpp
${SYMCC_RT_SRC_DIR}/RuntimeCommon.cpp
${SYMCC_RT_SRC_DIR}/LibcWrappers.cpp
${SYMCC_RT_SRC_DIR}/Shadow.cpp
${SYMCC_RT_SRC_DIR}/GarbageCollection.cpp)

# Backends should produce two targets: SymccRtStatic (static library) and SymccRtShared (shared library).
if (${SYMCC_RT_BACKEND} STREQUAL "qsym")
add_subdirectory(qsym_backend)
elseif (${SYMCC_RT_BACKEND} STREQUAL "simple")
add_subdirectory(simple_backend)
else()
message(FATAL_ERROR "An invalid backend has been selected: \"${SYMCC_RT_BACKEND}\".\
Please select a valid backend with the SYMCC_RT_BACKEND option among ${SYMCC_RT_AVAILABLE_BACKENDS_FMT}.")
endif()
# Backends should produce two targets: SymCCRtStatic (static library) and SymCCRtShared (shared library).
add_subdirectory("${SYMCC_RT_BACKEND_DIR}")

message(STATUS "Using ${SYMCC_RT_BACKEND} backend.")

if (NOT TARGET SymccRtStatic)
message(FATAL_ERROR "The backend \"${SYMCC_RT_BACKEND}\" does not produce the target SymccRtStatic.\
if (NOT TARGET SymCCRtStatic)
message(FATAL_ERROR "The backend \"${SYMCC_RT_BACKEND}\" does not produce the target SymCCRtStatic.\
This is a bug and it should be reported. Please open PR to the symcc-rt repository.")
endif()

if (NOT TARGET SymccRtShared)
message(FATAL_ERROR "The backend \"${SYMCC_RT_BACKEND}\" does not produce the target SymccRtShared.\
if (NOT TARGET SymCCRtShared)
message(FATAL_ERROR "The backend \"${SYMCC_RT_BACKEND}\" does not produce the target SymCCRtShared.\
This is a bug and it should be reported. Please open PR to the symcc-rt repository.")
endif()

set_target_properties(SymccRtStatic PROPERTIES OUTPUT_NAME "symcc-rt")
set_target_properties(SymccRtShared PROPERTIES OUTPUT_NAME "symcc-rt")
set_target_properties(SymCCRtStatic PROPERTIES OUTPUT_NAME "symcc-rt")
set_target_properties(SymCCRtShared PROPERTIES OUTPUT_NAME "symcc-rt")
47 changes: 26 additions & 21 deletions README.md
Original file line number Diff line number Diff line change
@@ -1,31 +1,35 @@
# SymCC Runtime

SymCC Runtime exposes a standard set of functions usable in different Symbolic Execution-related projects as a backend
linkable statically and dynamically.
SymCC Runtime exposes a standard set of functions usable in different Symbolic
Execution-related projects as a backend linkable statically and dynamically.

## Build

To compile `symcc-rt`, run:

```bash
$ git submodule update --init --recursive
$ mkdir build && cd build
$ cmake ..
$ ninja
```

It will compile both `libsymcc-rt.so` (shared library) and `libsymcc-rt.a` (static library) in the `build` directory.
It will compile both `libsymcc-rt.so` (shared library) and `libsymcc-rt.a`
(static library) in the `build` directory.

## Relation with SymCC

SymCC Runtime was originally a subdirectory of [SymCC](https://github.com/eurecom-s3/symcc) under the `runtime`
directory. It has been moved out be more easily usable as a library in different projects, which are not necessarily
related to SymCC's compiler pass.

The export of SymCC Runtime was done at the commit pointed by `3f98002a66f18a5c09856c5e66a6c1e48b0ee1a9`.
The tag `export_runtime_from_symcc` points to the last commit for which `symcc-rt` was the `runtime` subdirectory of
`symcc`.
It has some implications:
- **Pull request IDs** and **Issue IDs** before this commit refer to [SymCC](https://github.com/eurecom-s3/symcc) IDs.
SymCC Runtime was originally a subdirectory of
[SymCC](https://github.com/eurecom-s3/symcc) under the `runtime` directory. It
has been moved out be more easily usable as a library in different projects,
which are not necessarily related to SymCC's compiler pass.

The export of SymCC Runtime was done at the commit pointed by
`3f98002a66f18a5c09856c5e66a6c1e48b0ee1a9`. The tag `export_runtime_from_symcc`
points to the last commit for which `symcc-rt` was the `runtime` subdirectory of
`symcc`. It has some implications:
- **Pull request IDs** and **Issue IDs** before this commit refer to
[SymCC](https://github.com/eurecom-s3/symcc) IDs.
- `symcc-rt` is imported as a submodule in SymCC.

## Citation
Expand All @@ -50,8 +54,8 @@ More information on the paper is available

## Contributing

We welcome Issues and Pull requests. If you wish to contribute, please have a look
to the `CONTRIBUTING.md` file.
We welcome Issues and Pull requests. If you wish to contribute, please have a
look to the `CONTRIBUTING.md` file.

## Bug reporting

Expand All @@ -68,10 +72,11 @@ etc. Alternatively, you can send an email to Sebastian Poeplau

## License

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.
See [SymCC#114](https://github.com/eurecom-s3/symcc/issues/114) for the rationale.
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. See [SymCC#114](https://github.com/eurecom-s3/symcc/issues/114)
for the rationale.

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
Expand All @@ -84,6 +89,6 @@ Lesser General Public License along with SymCC Runtime. If not, see
The following pieces of software have additional or alternate copyrights,
licenses, and/or restrictions:

| Program | Directory |
|---------------|-----------------------------|
| QSYM | `qsym_backend/qsym` |
| Program | Directory |
|---------------|---------------------|
| QSYM | `backend/qsym/qsym` |
26 changes: 13 additions & 13 deletions qsym_backend/CMakeLists.txt → backends/qsym/CMakeLists.txt
Original file line number Diff line number Diff line change
Expand Up @@ -42,7 +42,7 @@ configure CMake with -DZ3_TRUST_SYSTEM_VERSION=on (see also docs/Configuration.t
endif()
endif()

set(SymccRtSrc
set(SymCCRtSrc
${QSYM_SOURCE_DIR}/expr.cpp
${QSYM_SOURCE_DIR}/expr_builder.cpp
${QSYM_SOURCE_DIR}/expr_cache.cpp
Expand All @@ -58,31 +58,31 @@ set(SymccRtSrc
${SHARED_RUNTIME_SOURCES}
Runtime.cpp)

add_library(SymccRtObj OBJECT
${SymccRtSrc})
add_library(SymCCRtObj OBJECT
${SymCCRtSrc})

set_property(TARGET SymccRtObj PROPERTY POSITION_INDEPENDENT_CODE 1)
set_property(TARGET SymCCRtObj PROPERTY POSITION_INDEPENDENT_CODE 1)

add_library(SymccRtShared SHARED $<TARGET_OBJECTS:SymccRtObj>)
add_library(SymccRtStatic STATIC $<TARGET_OBJECTS:SymccRtObj>)
add_library(SymCCRtShared SHARED $<TARGET_OBJECTS:SymCCRtObj>)
add_library(SymCCRtStatic STATIC $<TARGET_OBJECTS:SymCCRtObj>)

target_include_directories(SymccRtObj PRIVATE
target_include_directories(SymCCRtObj PRIVATE
${CMAKE_CURRENT_SOURCE_DIR} # for our fake pin.H and Runtime.h
${CMAKE_CURRENT_SOURCE_DIR}/..) # for common runtime components
${SYMCC_RT_INCLUDE_DIR}) # for common runtime components

target_include_directories(SymccRtObj SYSTEM PRIVATE
target_include_directories(SymCCRtObj SYSTEM PRIVATE
${Z3_CXX_INCLUDE_DIRS} # for Z3 support
${QSYM_SOURCE_DIR})

# We need to get the LLVM support component for llvm::APInt.
llvm_map_components_to_libnames(QSYM_LLVM_DEPS support)

set(SymccRtDeps ${Z3_LIBRARIES} ${QSYM_LLVM_DEPS})
set(SymCCRtDeps ${Z3_LIBRARIES} ${QSYM_LLVM_DEPS})

# Object libraries cannot be linked directly, so we link the final libraries one by one
# https://gitlab.kitware.com/cmake/cmake/-/issues/18090
target_link_libraries(SymccRtShared ${SymccRtDeps})
target_link_libraries(SymccRtStatic ${SymccRtDeps})
target_link_libraries(SymCCRtShared ${SymCCRtDeps})
target_link_libraries(SymCCRtStatic ${SymCCRtDeps})

# We use std::filesystem, which has been added in C++17. Before its official
# inclusion in the standard library, Clang shipped the feature first in
Expand All @@ -92,4 +92,4 @@ target_link_libraries(SymccRtStatic ${SymccRtDeps})
# std::filesystem - we catch this case in order to enable users of such systems
# to build with the default compiler.
find_package(Filesystem COMPONENTS Final Experimental)
target_link_libraries(SymccRtObj std::filesystem)
target_link_libraries(SymCCRtObj std::filesystem)
File renamed without changes.
File renamed without changes.
File renamed without changes.
24 changes: 12 additions & 12 deletions simple_backend/CMakeLists.txt → backends/simple/CMakeLists.txt
Original file line number Diff line number Diff line change
Expand Up @@ -29,26 +29,26 @@ configure CMake with -DZ3_TRUST_SYSTEM_VERSION=on (see also docs/Configuration.t
endif()
endif()

set(SymccRtSrc ${SHARED_RUNTIME_SOURCES} Runtime.cpp)
set(SymCCRtSrc ${SHARED_RUNTIME_SOURCES} Runtime.cpp)

add_library(SymccRtObj OBJECT
${SymccRtSrc})
add_library(SymCCRtObj OBJECT
${SymCCRtSrc})

set_property(TARGET SymccRtObj PROPERTY POSITION_INDEPENDENT_CODE 1)
set_property(TARGET SymCCRtObj PROPERTY POSITION_INDEPENDENT_CODE 1)

add_library(SymccRtShared SHARED $<TARGET_OBJECTS:SymccRtObj>)
add_library(SymccRtStatic STATIC $<TARGET_OBJECTS:SymccRtObj>)
add_library(SymCCRtShared SHARED $<TARGET_OBJECTS:SymCCRtObj>)
add_library(SymCCRtStatic STATIC $<TARGET_OBJECTS:SymCCRtObj>)

set(SymccRtDeps ${Z3_LIBRARIES})
set(SymCCRtDeps ${Z3_LIBRARIES})

# Object libraries cannot be linked directly
# https://gitlab.kitware.com/cmake/cmake/-/issues/18090
target_link_libraries(SymccRtShared ${SymccRtDeps})
target_link_libraries(SymccRtStatic ${SymccRtDeps})
target_link_libraries(SymCCRtShared ${SymCCRtDeps})
target_link_libraries(SymCCRtStatic ${SymCCRtDeps})

target_include_directories(SymccRtObj PRIVATE
target_include_directories(SymCCRtObj PRIVATE
${CMAKE_CURRENT_SOURCE_DIR}
${CMAKE_CURRENT_SOURCE_DIR}/..
${SYMCC_RT_INCLUDE_DIR}
${Z3_C_INCLUDE_DIRS})

set_target_properties(SymccRtObj PROPERTIES COMPILE_FLAGS "-Werror -Wno-error=deprecated-declarations")
set_target_properties(SymCCRtObj PROPERTIES COMPILE_FLAGS "-Werror -Wno-error=deprecated-declarations")
File renamed without changes.
File renamed without changes.
2 changes: 1 addition & 1 deletion bindings/README
Original file line number Diff line number Diff line change
Expand Up @@ -4,6 +4,6 @@


This directory contains bindings to the user-facing functionality of the runtime
(see runtime/RuntimeCommon.h). The bindings give target programs written in
(see include/RuntimeCommon.h). The bindings give target programs written in
different languages access to runtime features like in-memory input or custom
test-case handlers.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.

0 comments on commit 91c0034

Please sign in to comment.