Backend Rust/Foreign Language Support

CMakeLists.txt

@@ -16,6 +16,7 @@ cmake_minimum_required(VERSION 3.5)
 project(SymbolicCompiler)
 
 option(QSYM_BACKEND "Use the Qsym backend instead of our own" OFF)
+option(RUST_BACKEND "Build the support code required for a Rust backend as a static archive." OFF)
 option(TARGET_32BIT "Make the compiler work correctly with -m32" OFF)
 
 # We need to build the runtime as an external project because CMake otherwise
@@ -29,6 +30,7 @@ set(SYM_RUNTIME_BUILD_ARGS
   -DCMAKE_CXX_COMPILER=${CMAKE_CXX_COMPILER}
   -DCMAKE_CXX_FLAGS=${CMAKE_CXX_FLAGS}
   -DCMAKE_SHARED_LINKER_FLAGS=${CMAKE_SHARED_LINKER_FLAGS}
+  -DRUST_BACKEND=${RUST_BACKEND}
   -DQSYM_BACKEND=${QSYM_BACKEND}
   -DCMAKE_BUILD_TYPE=${CMAKE_BUILD_TYPE}
   -DZ3_TRUST_SYSTEM_VERSION=${Z3_TRUST_SYSTEM_VERSION})

runtime/CMakeLists.txt

@@ -22,6 +22,7 @@ set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -std=c++17 \
 -Wmissing-format-attribute -Wformat-nonliteral")
 
 option(QSYM_BACKEND "Use the Qsym backend instead of our own" OFF)
+option(RUST_BACKEND "Build the support code required for a Rust backend as a static archive." OFF)
 option(Z3_TRUST_SYSTEM_VERSION "Use the system-provided Z3 without a version check" OFF)
 
 # Place the final product in the top-level output directory
@@ -35,7 +36,9 @@ set(SHARED_RUNTIME_SOURCES
   ${CMAKE_CURRENT_SOURCE_DIR}/Shadow.cpp
   ${CMAKE_CURRENT_SOURCE_DIR}/GarbageCollection.cpp)
 
-if (${QSYM_BACKEND})
+if (${RUST_BACKEND})
+  add_subdirectory(rust_backend)
+elseif (${QSYM_BACKEND})
   add_subdirectory(qsym_backend)
 else()
   add_subdirectory(simple_backend)

runtime/RuntimeCommon.h

@@ -26,9 +26,11 @@
 #define RUNTIMECOMMON_H
 
 #ifdef __cplusplus
+#include <cstddef> // for size_t
 #include <cstdint>
 extern "C" {
 #else
+#include <stddef.h> // for size_t
 #include <stdint.h>
 #endif
 

runtime/Shadow.h

@@ -23,8 +23,6 @@
 
 #include <Runtime.h>
 
-#include <z3.h>
-
 //
 // This file is dedicated to the management of shadow memory.
 //

runtime/rust_backend/CMakeLists.txt

@@ -0,0 +1,25 @@
+# This file is part of SymCC.
+#
+# 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.
+#
+# 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 <https://www.gnu.org/licenses/>.
+
+add_library(SymRuntime STATIC
+  ${SHARED_RUNTIME_SOURCES}
+  Runtime.cpp)
+
+target_include_directories(SymRuntime PRIVATE
+  ${CMAKE_CURRENT_SOURCE_DIR}
+  ${CMAKE_CURRENT_SOURCE_DIR}/..)
+
+set_target_properties(SymRuntime PROPERTIES COMPILE_FLAGS "-Werror")
+
+INSTALL(TARGETS SymRuntime)

runtime/rust_backend/README.md

@@ -0,0 +1,24 @@
+# SymCC Rust Runtime
+
+This runtime is a wrapper around a stripped down runtime which can be implemented in Rust (or any other language).
+This wrapper implements Garbage Collection like the the Simple and QSym runtimes and implements the `_sym_bits_helper`.
+
+The functions that are left to be implemented by the wrapped runtime are defined in `RustRuntime.h` and mirror those which are defined in `RuntimeCommon.h` except for having new name prefixes and missing those which are related to memory management and utilites.
+
+## GC implementation
+The GC implementation works by keeping track of all expressions that the wrapped runtime generates and calling a new method (`_rsym_expression_unreachable(RSymExpr)`) for each expression that became unreachable in terms of the GC.
+The details of this implementation are the same as those of the Simple backend (it's a straight copy).
+
+## Bits Helper
+The bits helper is implemented by embedding the number of bits inside the expression pointer.
+Specifically, the least significant byte contains the bit width of the expression.
+Boolean expressions have a bit width of 0.
+The actual expression pointer is shifted towards the MSB to make space for the bit width.
+This reduces the amount of available bits in the expression pointer by 8.
+The runtime panics if an expression pointer is returned that would not fit, but this is not expected on 64-bit systems.
+(On 32-bit systems this may be a problem, but at this point, we don't care about 32-bit.)
+
+On a high level, this means that there are two `SymExpr` types now: `SymExpr`, which is used by the wrapper, and `RSymExpr`, which is used by the wrapped runtime.
+The wrapper takes care of translating between the two representations as necessary.
+
+The wrapper also takes care of maintaining the correct bit widths by calculating the resulting width when a width-changing instruction is encountered.